The Coq mailing list

["Petz, Adam Michael" <ampetz AT ku.edu>]

Hello all,

 

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, a few questions:  Is this a bug in Ltac?  If not, are there tricks/best practices to avoid it?  Any hints on how to debug Ltac errors like this would also be much appreciated!

 

Best,

Adam

 

 

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.