I have some problems with `apply`

failing to apply some lemmas. The lemmas are like

`path_empty : forall (G:Graph) (n:node G), path_from G n (@nil (node G))`

the goals are like

`path_from G s (@nil (node (make_symmetric G)))`

where `make_symmetric`

is a function on records such that `node ?G`

and `node (make_symmetric ?G)`

are convertible.

`apply (path_empty G)`

would succeed, but `apply path_empty`

fails with the error `Unable to unify "make_symmetric G" with "G"`

. (It fails whether the type of `s`

in the context is `node G`

or `node (make_symmetric G)`

).

It seems like this comes from the order that subterms are visited, plus the "tactic unification" that `apply`

uses eagerly committing to `?G:=make_unification G`

when trying to unify `(@nil (node ?G))`

against `(@nil (node (make_symmetric G)))`

.

Tactics `refine (path_empty _ _)`

or `rapply path_empty`

do succeed.

Is there any way to adjust definitions or add declarations so this works with `apply`

? Or, is `rapply`

good for general use?

I've considered reordering parameters, but if subterms are examined right-to-left I would need to change the `path_from`

predicate to take the `list (node G)`

argument *before* `G`

itself, not allowed by the dependency between types.

Coq doesn't allow type signatures with explicit convertibility claims (for decent decidability reasons, I know), or I might try giving the lemma a looser signature like `path_empty' : forall (G:Graph) (N1:Type) (HN1: node G === N) (N2:Type) (HN2: node G === N2) (n:N1), path_from G n (@nil N2)`

.

Here is a complete example:

```
Record Graph := { node : Type; edge : node -> node -> Prop}.
Definition make_symmetric (G: Graph)
:= {| node := node G; edge := fun x y => edge G x y \/ edge G y x |}.
Inductive path_from (G: Graph): node G -> list (node G) -> Prop :=
| path_empty : forall (n: node G), path_from G n nil
| path_cons : forall n n', edge G n n' ->
forall tr, path_from G n' tr -> path_from G n (n'::tr).
Goal forall (G:Graph) (is: node (make_symmetric G)),
path_from G is (@nil (node (make_symmetric G))).
Proof.
intros G is.
Fail apply path_empty.
```

Because the example uses a real Record it turns out "Primitive Projections" allows a solution. Add `Set Primitive Projections`

before the record declaration and define a lemma

```
Lemma path_empty' N E n: path_from {|node:=N;edge:=E|} n nil.
Proof. intros; apply path_empty. Qed.
```

I would still be interested in other options, both to understand unification and because the type in my actual code isn't actually a record yet (though I probably can and should change that).

Oh, trying to rely on Primitive Projections works for the first goal, but not the opposite direction:

```
Goal forall (G:Graph) (is: node (make_symmetric G)),
path_from (make_symmetric G) is (@nil (node G)).
Proof.
intros G is.
Fail apply path_empty'.
```

Odd, that can be fixed by explicitly using `N`

more places in the signature: `path_empty'' N E (n:N): path_from {|node:=N;edge:=E|} n (@nil N)`

. But now I'll have to figure out why the previous signature even worked for the first goal, given that the conclusion was actually `path_from {|node:=N;edge:=E|} n (@nil (node {|node:=N;edge:=E|}))`

.

Traces from `Set Debug Tactic Unification`

don't seem to show enough.

Tactics refine (path_empty _ _) or rapply path_empty do succeed.

Is there any way to adjust definitions or add declarations so this works with apply? Or, is rapplygood for general use?

Never heard of `rapply`

but ssreflect's `apply:`

is very stable and should also work here, since it uses `evarconv`

similarly to `refine`

.

"switch between `apply:`

and `apply`

if one doesn't work" is the basic strategy

meanwhile `rapply`

doesn't seem common (few uses in Coq itself) and the stdlib doesn't even provide a variant that accepts terms with holes

(not even the simple `Tactic Notation "urapply" uconstr(p) := rapply p.`

from the testsuite).

Don't you need to import SSReflect to get their `apply:`

? That wouldn't allow switching back and forth in the same file. If there's a way to get just their apply without other tactics I might try that.

Vanilla `apply`

is still available when you load SSReflect because it's not the same syntax. In fact, most if not all vanilla tactics are still available after you load SSReflect. One tactic whose base syntax is overriden is `rewrite`

, but you can still do `rewrite ->`

to get the vanilla version.

Ah, I didn't know `rewrite ->`

got back the vanilla version easily. That's the main thing I worried about. (also remembering SSReflect has behavior for a bare `apply`

, but forgetting that's only an `apply`

with no arguments).

I see there's also a flag `SsrRewrite`

for turning off the syntax entirely.

Last updated: Oct 03 2023 at 02:34 UTC