The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

Which version of Coq are you using?  In both 8.4pl2 and trunk from a few months ago, copy/pasting your new code (which is indeed what I meant) gives me (approximately):

1 subgoals, subgoal 1 (ID 7)                                                                                                                
                                                                                                                                            
  a : nat                                                                                                                                   
  var_ : nat                                                                                                                                
  H_eq_var_ : var_ = a + 2                                                                                                                  
  ============================                                                                                                              
   var_ = 2                                                                                                                                 
(dependent evars:)

On Tue, Jun 25, 2013 at 1:42 PM, t x <txrev319 AT gmail.com> wrote:

Hi Jason,

  I tried the following, and it still says nH. Did I misinterpret your response?

Ltac simp_rem v :=

  let nV := fresh "var_" in

  let nH := fresh "H_eq_var_" in

    remember v as nV eqn:nH.

Lemma lem_000:

  forall (a : nat), (a+2) = 2.

Proof.

  intro a.

  simp_rem (a+2).

(* output:

1 subgoal

a : nat

var_ : nat

nH : var_ = a + 2

====================================================================== (1/1)

var_ = 2

*)

  Abort.

On Mon, Jun 24, 2013 at 8:51 PM, Jason Gross <jasongross9 AT gmail.com> wrote:

Remove the space after "eqn:".  I'm not sure why this doesn't raise a warning or error, as remember doesn't otherwise take multiple arguments...

-Jason

On Mon, Jun 24, 2013 at 10:08 PM, t x <txrev319 AT gmail.com> wrote:

Hi,

Consider the following block of code:

== BEGIN ==

Ltac simp_rem v :=

  let nV := fresh "var_" in

  let nH := fresh "H_eq_var_" in

    remember v as nV eqn: nH.

Lemma lem_000:

  forall (a : nat), (a+2) = 2.

Proof.

  intro a.

  simp_rem (a+2).

  Abort.

== END ==

The output I get is:

1 subgoal

a : nat

var_ : nat

nH : var_ = a + 2

====================================================================== (1/1)

var_ = 2

I like the fact that the newly introduced var has prefix "var_"

I don't like the fact that the equation is named nH instead of something with prefix "H_eq_var_"

It is important to me that (1) I don't clash with existing hypothesis names and (2) I know the name of the newly introduced equation so that I can apply other transforms to it.

Question:

1) What am I doing wrong?

2) How do I fix this?