Stream: Coq users

Topic: ssr views


view this post on Zulip Andrej Dudenhefner (Nov 06 2020 at 08:36):

I'm trying to fully understand ssreflect views.
Looking at https://coq.inria.fr/distrib/current/refman/proof-engine/ssreflect-proof-language.html#id16
I do not understand why the following example works:

Goal forall x, x = 1 -> x = 2 -> 7 = 8.
Proof.
move=> + + + /ltac:(exfalso).
(* new Goal is forall x : nat, x = 1 -> x = 2 -> False *)

It is quite common (for me) to temporarily introduce some arguments (without naming them explicitly), then apply a lemma or tactic, then revert the arguments.
This seems to be covered by views, but I do not understand how. Also , I find move=> H1 H2 H3; exfalso; move: H1 H2 H3. with unnecessary names dissatisfactory.
Is there more documentation on ssreflect views that could explain the above example?

view this post on Zulip Reynald Affeldt (Nov 06 2020 at 08:39):

Maybe these workshop slides? https://staff.aist.go.jp/reynald.affeldt/coq2019/coqws2019-martindorel-tassi-slides.pdf (see slide 7)

view this post on Zulip Enrico Tassi (Nov 06 2020 at 08:43):

=> +++ /ltac:(code) is equivalent to move=> H1 H2 H3; exfalso; move: H1 H2 H3. for well chosen names H1 .. H3.
The + introduces a temporary assumption, which is then moved down to the goal at the very end of the intro pattern.

view this post on Zulip Enrico Tassi (Nov 06 2020 at 08:44):

Does the explanation of + answer your question?

view this post on Zulip Andrej Dudenhefner (Nov 06 2020 at 08:45):

Does the explanation of + answer your question?

I understand +. I cannot find documentation on move=> /ltac:(code).

view this post on Zulip Andrej Dudenhefner (Nov 06 2020 at 08:48):

Most disturbingly, it feels like move=> /something requires the goal to have at least one top argument (the documentation says It first introduces top.). However, in the case of move=> /ltac:(exfalso) it can be executed on any goal (e.g. 7 = 8 in the above example).

view this post on Zulip Reynald Affeldt (Nov 06 2020 at 08:50):

ltac: is documented here: https://coq.inria.fr/refman/proof-engine/ltac.html (not sure it is the best place to look at)

view this post on Zulip Andrej Dudenhefner (Nov 06 2020 at 08:53):

Maybe these workshop slides? https://staff.aist.go.jp/reynald.affeldt/coq2019/coqws2019-martindorel-tassi-slides.pdf (see slide 7)

Slide 7 exactly matches my understanding. However, it does not apply to the above example, as in the above example there is no assumption to be interpreted by the view.

view this post on Zulip Enrico Tassi (Nov 06 2020 at 08:56):

You are right, I cannot find the doc either. I'll summarize here and open a bugreport later.

Views are terms as in /t and they need to be applied to something, which is the top of the stack (the first assumption of the goal). For example if t : A -> B it needs an A to operate on, which is the top of the stack.

You can do many things with a term, but not everything. Hence the possibility to plug a custom ltac piece of code in there. The ltac piece of code does not need an assumption to be useful, hence the discrepancy (it can introduce the top of the stack itself if it needs something to operate on).

See https://github.com/math-comp/math-comp/pull/599 for some use cases. [dup] operates on the top of the stack. [swap] needs 2 slots. Some other examples in the PR linked by that one, such as [! inE], needs 0 stack slots to be useful.

view this post on Zulip Andrej Dudenhefner (Nov 06 2020 at 09:01):

See https://github.com/math-comp/math-comp/pull/599 for some use cases

That is an interesting PR and covers many of my use cases .

view this post on Zulip Enrico Tassi (Nov 06 2020 at 09:03):

May I suggest to ping the author then ;-) The PR is almost ready to be merged

view this post on Zulip Enrico Tassi (Nov 06 2020 at 09:03):

A +1 would motivate him I guess

view this post on Zulip Cyril Cohen (Nov 06 2020 at 11:04):

It did, I opened coq/coq#13317

view this post on Zulip Andrej Dudenhefner (Nov 06 2020 at 11:10):

By the way, isn't there good design space for move=> /lemma in case the current goal has no top assumption?
E.g. it could be a synonym for apply /lemma. This would enable e.g. move=> ++ /lemma1 => /lemma2 => * /lemma3 instead of move=> H1 H1; apply /lemma1; move: H1 H2 => /lemma2 *; apply /lemma3.

view this post on Zulip Paolo Giarrusso (Nov 06 2020 at 11:20):

at least I rely on the distinction when reading — but can’t your example be written as move=> H1 /lemma2 H2; apply /lemma1 /lemma3?

view this post on Zulip Paolo Giarrusso (Nov 06 2020 at 11:22):

“the distinction” = the distinction between move => /lemma and apply /lemma — I know the former applies to an assumption.

view this post on Zulip Paolo Giarrusso (Nov 06 2020 at 11:23):

If you don’t want to specify, I think you can rewrite with bi-implications. It does become annoying that you can’t rewrite by normal implications, but that’d probably be a bad idea

view this post on Zulip Andrej Dudenhefner (Nov 06 2020 at 11:32):

you can’t rewrite by normal implications, but that’d probably be a bad idea

Unidirectional lemma rewriting definitely feels wrong.

“the distinction” = the distinction between move => /lemma and apply /lemma — I know the former applies to an assumption.

As the previous discussion has shown, this is already not the case for /ltac:(code) and has its benefits for more fluent bookkeeping.
Still, I agree that such ambiguity could make the proof less maintainable as the result depends on the current number of arguments in the Goal.
I'm just wondering whether there is some more uniform and fluent principles to the bookkeeping part of ssr.

view this post on Zulip Cyril Cohen (Nov 09 2020 at 00:01):

you could define your own ltac in term for apply/, I cannot make it work for apply/ but it works for apply:
(@Enrico Tassi is there a bug?)

Notation "'[apply:' x ']'" := (ltac:(apply: x))
  (at level 0, x at level 200, only parsing) : ssripat_scope.
Notation "'[apply/' x ']'" := (ltac:(apply/ x))
  (at level 0, x at level 200, only parsing) : ssripat_scope.

Lemma test A B C D
  (lemma1 : B -> C) (lemma2 : D -> A -> B -> C) (lemma3 : True -> B) :
  A -> B -> C.
Proof. Fail by move=> + + /[apply/lemma1] -/lemma2 * /[apply/lemma3]. Restart.
Proof. by move=> + + /[apply: lemma1] -/lemma2 * /[apply: lemma3]. Qed.

Last updated: Jan 27 2023 at 01:03 UTC