Stream: Coq users

Topic: ssr confusing intro pattern


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

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

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

view this post on Zulip Emilio Jesús Gallego Arias (Oct 23 2020 at 13:49):

To avoid this use move => -[foo bar]

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

view this post on Zulip Paolo Giarrusso (Oct 23 2020 at 20:28):

Yeah; IIRC, you can skip the - right after move =>, but not in general.

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

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