Andrej Dudenhefner (Oct 23 2020 at 13:44): Andrej Dudenhefner (Oct 23 2020 at 13:44):Consider Goal forall (P: Prop), P /\ P -> P.
Using 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 => tactical.
For some reason move=> P => [[H1 H2]]. works, which confuses me even more.
Why is this?
Emilio Jesús Gallego Arias (Oct 23 2020 at 13:49):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.
Kenji Maillard (Oct 23 2020 at 13:49):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]
Emilio Jesús Gallego Arias (Oct 23 2020 at 13:49):To avoid this use move => -[foo bar]
Andrej Dudenhefner (Oct 23 2020 at 13:55):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.
Paolo Giarrusso (Oct 23 2020 at 20:28):Yeah; IIRC, you can skip the - right after move =>, but not in general.
Paolo Giarrusso (Oct 23 2020 at 20:29):But I don’t get the examples with move=>- ... I assume those are for illustration, but that dash can be dropped.
Enrico Tassi (Oct 23 2020 at 21:14):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 case or 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