Andrej Dudenhefner (Nov 06 2020 at 08:36): 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?
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)
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.
Enrico Tassi (Nov 06 2020 at 08:44):Does the explanation of + answer your question?
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).
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).
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)
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.
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.
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 .
Enrico Tassi (Nov 06 2020 at 09:03):May I suggest to ping the author then ;-) The PR is almost ready to be merged
Enrico Tassi (Nov 06 2020 at 09:03):A +1 would motivate him I guess
Cyril Cohen (Nov 06 2020 at 11:04):It did, I opened coq/coq#13317
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.
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?
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.
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
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 => /lemmaandapply /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.
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: Oct 05 2023 at 02:01 UTC