The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

Try updating to Coq 8.4pl2 (compiled June 2013, for me).

-Jason

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

I'm on OSX 10.8.3

Here's coqtop.opt-v, the fail.v, and the output of running it under coqtop.opt

$ coqtop.opt -v ; echo "**********"; cat fail.v; echo "**********"; cat fail.v | coqtop.opt

The Coq Proof Assistant, version 8.4 (September 2012)

compiled on Sep 25 2012 15:01:39 with OCaml 3.12.1

**********

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

**********

Welcome to Coq 8.4 (September 2012)

Coq < Coq < Coq < Coq < simp_rem is defined

Coq < Coq < Coq < 1 subgoal

  

  ============================

   forall a : nat, a + 2 = 2

lem_000 < 1 subgoal

  

  ============================

   forall a : nat, a + 2 = 2

lem_000 < 1 subgoal

  

  a : nat

  ============================

   a + 2 = 2

lem_000 < 1 subgoal

  

  a : nat

  var_ : nat

  nH : var_ = a + 2

  ============================

   var_ = 2

lem_000 < lem_000 < lem_000 < 

On Tue, Jun 25, 2013 at 10:58 AM, Jason Gross <jasongross9 AT gmail.com> wrote:

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?