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 13 2024 at 01:02 UTC