Stream: Coq users

Topic: multigoal intros


view this post on Zulip 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?

view this post on Zulip Pierre Courtieu (Oct 22 2020 at 12:27):

view this post on Zulip Paolo Giarrusso (Oct 22 2020 at 17:45):

in the latter case: is the problem with as clauses, or with _inversion_’s as clauses?

view this post on Zulip Paolo Giarrusso (Oct 22 2020 at 17:46):

because generally, I think as is a better syntax than intros.

view this post on Zulip 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.

view this post on Zulip 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)

view this post on Zulip 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.

view this post on Zulip 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).

view this post on Zulip 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: Jan 29 2023 at 01:02 UTC