Unification problem with apply and convertability · Coq users

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

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.

Brandon Moore (Apr 14 2021 at 19:45):

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

Brandon Moore (Apr 14 2021 at 19:52):

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

Brandon Moore (Apr 14 2021 at 21:25):

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

Brandon Moore (Apr 14 2021 at 22:02):

Paolo Giarrusso (Apr 15 2021 at 15:21):

Never heard of rapply but ssreflect's apply: is very stable and should also work here, since it uses evarconv similarly to refine.

Paolo Giarrusso (Apr 15 2021 at 15:26):

Paolo Giarrusso (Apr 15 2021 at 15:27):

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

Brandon Moore (Apr 15 2021 at 16:19):

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.

Théo Zimmermann (Apr 15 2021 at 16:21):

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.

Brandon Moore (Apr 15 2021 at 16:27):

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

Stream: Coq users

Topic: Unification problem with apply and convertability

Brandon Moore (Apr 14 2021 at 18:47):