Goal forall (P: Prop), P /\ P -> P.
ssreflect intro patterns I can write
move=> P [H1 H2]. to introduce/destruct the respective assumptions.
However, chaining of
=> does not seem to work, e.g. both
move=> P => [H1 H2]. and
(move=> P) => [H1 H2]. fail.
This is contrary to what I would expect from the
For some reason
move=> P => [[H1 H2]]. works, which confuses me even more.
Why is this?
This is documented [or used to be]; when
[ ...] is the first token after a
=> there is a special case that will handle it as a disjunctive tactic pattern.
I think that the first pair of brackets after a
=> is supposed to be a goal dispatch
[ .. | .. | ... ] and you need to add a
- to obtain the destructuring behaviour
move=> -, so that in your example it should be
move=> P => -[H1 H2]
To avoid this use
move => -[foo bar]
Ah, finally I understand, thank you. Interestingly
move=> P. move=> [H1 H2]. also works although
[H1 H2] is the first token after arrow. But I see that
move cannot introduce disjunction.
Yeah; IIRC, you can skip the - right after move =>, but not in general.
But I don’t get the examples with move=>- ... I assume those are for illustration, but that dash can be dropped.
The exception is documented in this section: https://coq.inria.fr/refman/proof-engine/ssreflect-proof-language.html#intro-patterns
My personal take is that
 is overloaded, it can case or dispatch. After the tactic
elim it would be unhandy to mean "case again", while after
move it would be unhandy to mean "dispatch" (when SSR was invented,
all: did not even exist, no point in dispatching). So this is why the confusing exceptions :-/
There is a PR trying (not really alive, but still) to promote
(..|..|..) for dispatching only. After such a change we could start questioning the use of
 for dispatching, and see if we can remove the exception (in new code), and just say that
 does always case.
Last updated: Sep 23 2023 at 07:01 UTC