Pierre Courtieu (Oct 22 2020 at 12:25): Pierre Courtieu (Oct 22 2020 at 12:25):Hi
For various reasons I would like to be able to have multigoal intros and write things like:
all:intros [> x y H | x y z Hxy Hxz | ...].
tac h;intros [> x y H | x y z Hxy Hxz | ...].
tac h;intros [> x y [H1 H2] | x y z [Hxy Hxz] H' | ...].
...
instead of
all:[> intros x y H | intros x y z Hxy Hxz | intros ...].
tac h ; [intros x y H |intros x y z Hxy Hxz | intros ...].
tac h; [ intros x y [H1 H2] | intros x y z [Hxy Hxz] H' | ...].
...
Is it already possible? Would it be feasible?
Pierre Courtieu (Oct 22 2020 at 12:27):all:intros [> x y H ...]: I tend to use multigoal tactics instead of queuing ; to much.tac h;intros [> x y H | x y ...]:I have tacticals that automatically generalize "new" hypothesis generated by a tactic and hope using these to help PG users naming there hypothesis after "inversion" for instance (instead of the current creepy as clause). Paolo Giarrusso (Oct 22 2020 at 17:45):in the latter case: is the problem with as clauses, or with _inversion_’s as clauses?
Paolo Giarrusso (Oct 22 2020 at 17:46):because generally, I think as is a better syntax than intros.
Paolo Giarrusso (Oct 22 2020 at 17:48):inversion is an exception — I’m not sure if it is designed for something, but it does not seem “name new things that you get in the context” — or at least not the ones after inversion; subst.
Paolo Giarrusso (Oct 22 2020 at 17:49):(I’m aware of inversion_clear H, but IIRC it is not an bug-free replacement of inversion H; subst; clear H)
Pierre Courtieu (Oct 24 2020 at 21:46):What are things that intros cannot do?
The main problem with as is inversion... And all tactics that don’t support as. Like ˋdecomposeˋ or any user defined tactic.
Paolo Giarrusso (Oct 25 2020 at 03:26):I didn’t say that intros cannot do something, just expressed a preference on syntax... but I realize that ssreflect => supports what you want (but with ssreflect intro patterns).
Paolo Giarrusso (Oct 25 2020 at 03:27):ahem: it works after tac h => [x y H | x y z Hxy Hxz | ... ], not after all:
Last updated: Oct 13 2024 at 01:02 UTC