The Coq mailing list

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

Le Tue, 06 Apr 2010 15:07:32 +0200, andré hirschowitz <ah AT unice.fr> a  
écrit:

> In fact I doubt that assert is what andre wishes, as I think andre  
> wanted to
> > say,
> >  "assert (H: P)." produces an opaque term, and sometimes (it happened to
> > me), we
> >  should want a transparent term with usable definition.
>
> Exactly. I just want to give a name to an awful term which I am unable to
> write although I am able to produce it in proof mode.
>
> > That makes me think of a maybe real solution, but I am not sure it  
> > works:
> > instead of a "pose (H := _ : P).", you should try a "Lemma H: P."
>
> No, this does not work because the local environment is not taken into
> account by this command (if my experiment is correct). Neither does
> Definition for the same reason.

:( you are right, sorry for having spammed this list with this (wrong)  
solution...
I think this feature should be "consistant with Coq spirit",
but it is not implemented so.
It seems I will continue to make those awful Defined Lemma before starting  
a proof...

By the way, is there a way to remove them without
"
Section foo.
Let awfull_lemma : lot_of_awful_hypotheses -> awful_goal.
Proof.
 awful_proof.
Defined.

Lemma lemma: pretty_goal.
 pretty_proof_with_awful_lemma.
Qed.
End foo.
"

> Thanks to all.
>
> ah
>
> > >


--
Cédric AUGER

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