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' | ...]. ...
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?
all:intros [> x y H ...]: I tend to use multigoal tactics instead of queuing
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
in the latter case: is the problem with
as clauses, or with _inversion_’s
because generally, I think
as is a better syntax than
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
(I’m aware of
inversion_clear H, but IIRC it is not an bug-free replacement of
inversion H; subst; clear H)
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.
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).
ahem: it works after
tac h => [x y H | x y z Hxy Hxz | ... ], not after
Last updated: Jan 29 2023 at 01:02 UTC