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?

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

`=> +++ /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.

Does the explanation of `+`

answer your question?

Does the explanation of

`+`

answer your question?

I understand `+`

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

.

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).

`ltac:`

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

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.

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.

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 .

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

A +1 would motivate him I guess

It did, I opened coq/coq#13317

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`

.

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

?

“the distinction” = the distinction between `move => /lemma`

and `apply /lemma`

— I know the former applies to an assumption.

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

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.

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