The Coq mailing list

[Théo Zimmermann <theo.zimmi AT gmail.com>]

Hi Jeremy,

Sorry to insist but the simplest answer to this question is: use a proper interface which will allow you to state your lemma and prove it outside (above) your current proof. Nested lemmas are a feature whose use is strongly discouraged. Some users insist they need it (in particular during computation heavy proofs) and that's the only reason the feature has not been removed but the Coq developers are not interested in fixing bugs it may have...

Théo

Le mar. 22 janv. 2019 à 06:09, Jeremy Dawson <Jeremy.Dawson AT anu.edu.au> a écrit :

Hi,

I get the following errors:

gen_moveL < apply midI3.
Toplevel input, characters 6-11:
 > apply midI3.
 >       ^^^^^
Error: The reference midI3 was not found in the current environment.

gen_moveL < Check midI3.
Toplevel input, characters 6-11:
 > Check midI3.
 >       ^^^^^
Error: The reference midI3 was not found in the current environment.

gen_moveL < Lemma midI3: forall T (a b c d : list T) (x y : T),
   a = c -> b = d -> a ++ x :: b = c ++ x :: d.
gen_moveL < Toplevel input, characters 6-11:
 > Lemma midI3: forall T (a b c d : list T) (x y : T),
 >       ^^^^^
Error: midI3 already exists.

I'm in the middle of a long proof, in which I have previously proved a
useful lemma, called midI3.

Presumably the lemma I've proved is considered (though not actually) to
depend somehow on the particular state of the proof at which I first
proved it.  Would that be right?

but it seems the system won't let me use it at the current point in my
proof, and won't let me prove it again.

So my question is, having decided during a proof that a particular lemma
would be useful, how to I prove and use it?

thanks

Jeremy