The Coq mailing list

[Pierre Courtieu <pierre.courtieu AT gmail.com>]

Hi,

ASFAIU a nested "Lemma" cannot and never will use the enclosing proof
context. Period. "assert" is made for that, it declares a subgoal
instead of a lemma which is the right thing to do if one wants to use
current proof context. I think there is no point in having anything
else for that.

The goal of a nested lemma is (and has always been) to insert a lemma
*before* the current lemma in the environment, and then keep proving
the current lemma in the new *updated* environment, without replaying
the beginning of its proof. This supposes of course that the side
effect of inserting a lemma in the environment will have no effect on
the beginning of the proof.

While this is very useful (mainly during proof development as said in
this thread), the two reasons why this is currently discouraged are to
my knowledge (please feel to add other ones):

1) It may not be the case that the insertion has no effect (although I
don't really see how this could happen, universes are checked at "Qed"
time anyway). It is therefore a bit "dangerous" for consistency to
have such side effects on the proof environment. However as a
temporary solution this is not a real problem imho.  We could even
enforce the use of Admitted until the nested lemmas are removed.

2) The (very cool) feature of late coq versions allowing for editing a
proof without checking the proofs of previous lemmas (so called "async
edition", allowing to start working almost immediately after opening a
file) heavily relies on the ability to deduce the content of the
environment by only looking at previous lemma statements (+ "proof
using" annotations in sections). However I don't see any reason why we
could not read also the statement of nested lemmas during this
process.

It looks to me that this feature could be implemented cleanly if some
development power were dedicated to it. But there are a lot of cool
features to wish for and not an infinite manpower in the coq dev team.
It is very good news that some effort are currently dedicated to UI in
general.

P

Le mer. 23 janv. 2019 à 11:14, Gaëtan Gilbert
<gaetan.gilbert AT skyskimmer.net>
 a écrit :
>
> 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
> >