The Coq mailing list

[AUGER <Cedric.Auger AT lri.fr>]

Le Wed, 07 Apr 2010 14:11:24 +0200, Pierre-Marie Pédrot  
<pierremarie.pedrot AT ens-lyon.fr> a écrit:

> AUGER wrote:
> > I think this feature should be "consistant with Coq spirit",
> > but it is not implemented so.
>
> Yet obviously it deserves to, so I filed a bug report:
>
> http://www.lix.polytechnique.fr/coq/bugs/show_bug.cgi?id=2291
>
> Feel free to add some details.
>
> PMP
That is not really what I meant:
I said that nested lemmas should be generalized according to current local  
hypothesis,
and not start an interactive proof with an empty environnement,
allowing you to have:

Section foo.
 Lemma bar: foobar.
 Proof.
  ...
  (*A*)
  Let x : barfoo.
  Proof.
   (*B*)
   ...
  Defined.
  ...
 Qed.
End foo.

So that in point (*B*) we have exactly same hypotheses as in point (*A*).

The tactic assert_body you suggest is less readable, but shorter and  
usable in Ltac;
but I am almost certain it cannot be done without the "Defined/Qed"  
verification at the end
of the new subproof, as we want the terms appearing in hypotheses to be  
well typed/formed,
so that type checking will be performed in more than one place and the  
tactic will be a little
slower than you may expect.

If "x" is very important in the proof, I think it deserves a "Let",
which would be generalized at "Defined" time according to the used  
hypothesis of (*A*)

Personnaly, I would rather call "transparent assert" your "assert_body",  
but that is
purely personnal taste.

--
Cédric AUGER

Univ Paris-Sud, Laboratoire LRI, UMR 8623, F-91405, Orsay