- MEMOCODE Paper Accepted
- NFM '21 (Virtual) Conference Presentation
- Paper Accepted to NFM '21
- Ltac Bug or Ltac Feature?
- Deep Field by Eric Whitacre
- Higher-Order Automation
- HotSoS 2020 Poster Presentation
- Dissertation Proposal Defense

Index

Blog

Blog Categories

Announcements

Coq

Music

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