The Coq mailing list

[Enrico Tassi <enrico.tassi AT inria.fr>]

On Thu, 2019-01-24 at 20:49 +0100, Jan Bessai wrote:
> On Thu, Jan 24, 2019 at 06:40:38PM +0100, Enrico Tassi wrote:
>  
> > Take this example:
> > 
> >   Lemma a ... 
> >     ..
> >     apply b.
> >     ..
> >       Lemma b ...
> >       ...
> >       Qed.
> >     ..
> >     apply b.
> >     ..
> >   Qed.
> > 
> > Note that the two "apply b" are different, the former is
> > from an Imported module, for example, while the latter is
> > the nested lemma b.
> > 
> > One cannot really check the document as if b was coming before a
> > since he would "capture" both occurrences of "b" and change the
> > meaning of the document.
> 
> Out of curiosity:
> Do nested Lemmas also pose problems in presence of the (co-)fix
> tactic?
> These can change behaviour depending on the exact translation of the
> Lemma: depending on whether the lemma is turned into a local/global
> let
> binding or inlined, 

I think you are right, making things opaque can bother the termination
checker. But as of today nested lemmas are always turned into global
(opaque if prescribed) lemmas, in a way they are hoisted, even if their
"checking" is interleaved.

When the "nested lemma" cannot be predicted statically, eg it is
generated via abstract, it can be inlined as a let or as a beta redex
(depending on opacity) if the enclosing lemma is opaque.
I believe this does not weaken termination/production checking (nobody
reported any related bugs, but I'm not 100% sure).

Best,
-- 
Enrico Tassi