The Coq mailing list

[Gaëtan Gilbert <gaetan.gilbert AT skyskimmer.net>]

Could you report this on github with enough info to reproduce? Thanks

Gaëtan Gilbert

On 22/01/2019 06:08, Jeremy Dawson wrote:
> 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