I encountered some surprising (to me) behavior while writing an Ltac procedure involving a “with” clause. A minimal example appears below. The problem occurs when binding a variable from a hypothesis, then using that variable in the LHS of a with binding in the Ltac body. My expectation is that the LHS (x in the assignment x:=y) is unaffected by substitution, and must simply match the name of a bound variable in the type of the Lemma to which it is being applied.
I suspected a scoping issue, so I found a workaround in temp_ltac’ below by changing the name of the bound variable to one that does not appear in the type of the Lemma. However, I fear this could become tedious in larger developments.
Finally, some questions: Is this a bug in Ltac? If not, are there tricks/best practices to avoid it?
Lemma temp {A:Type} : forall (a:A), a = a.
Proof.
trivial.
Defined.
Ltac temp_ltac :=
match goal with
| [H: ?a = _ |- _] => apply temp with (a:=a); eauto
end.
Example temp_ex{A:Type} : forall (c:A), c = c -> c = c.
Proof.
intros.
Fail temp_ltac.
(* Does this evaluate to: apply temp with (c:=c) ? *)
(* Intent is as follows: *)
apply temp with (a:=c).
Qed.
Ltac temp_ltac' :=
match goal with
| [H: ?b = _ |- _] => apply temp with (a:=b); eauto
end.
Example temp_ex' {A:Type} : forall (c:A), c = c -> c = c.
Proof.
intros.
temp_ltac'.
Qed.
The verdict: It’s a feature! Thanks to Sam Gruetter on the Coq club for this snippet:
Ltac generic lem :=
lazymatch type of lem with
| forall (myA: Type) (mya: myA), _ =>
lazymatch goal with
| H: ?b = _ |- _ => apply lem with (mya := b)
end
end.
Example temp_ex {A:Type} : forall (c:A), c = c -> c = c.
Proof.
intros.
generic @temp.
As is often the case with Coq, it’s as expressive as you want it to be…and more! This snippet shows the ability to match on the type of a lemma-as-parameter, thus binding its universally bound inputs to variables (see generic above). Those bound names can then be used in the LHS of a with clause. This strategy, while somewhat verbose, removes the dependency on the chosen name for the bound variable in the original lemma temp, making proofs robust against naming changes.
An extra tip I learned: using lazymatch instead of match helps debugging Ltac. With lazymatch, the decision which branch to take only depends on the pattern and not on whether the tactic to the right of => succeeds. This gives a precise error message when all patterns match, but the tactic fails (rather than just “No matching clauses for match”).