The Coq mailing list

[Samuel Gruetter <gruetter AT mit.edu>]

Hi Adam,

I don't think this is an Ltac bug, I'd even call it a feature! For instance, I could match on the name of the argument of temp, and use a variable myA to refer to that name when I apply the lemma, as follows:

Lemma temp{A:Type} : forall (a:A), a = a.

Proof.

  trivial.

Defined.

 

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.

And regarding hints on how to debug: I replaced match by lazymatch (so that the decision which branch to take only depends on the pattern and not on whether the tactic to the right of => succeeds), which makes debugging easier in the case where the pattern matches, but the tactic fails: You get the precise error message, rather than just "No matching clauses for match".

Hope that helps,

Sam

On Mon, 2020-12-07 at 21:28 +0000, Petz, Adam Michael wrote:

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.