The Coq mailing list

[Laurent Thery <Laurent.Thery AT sophia.inria.fr>]

Hi,

Randy Pollack>> I assume that Laurent was actually looking for a more natural 
solution
Randy Pollack>> than "prove it as a top-level lemma".

As a matter of fact I really want some saturation, going from the
hypothesis to the goal. 

>Randy Pollack>In LEGO, definitions made when in proof mode are local in the 
>context
>Randy Pollack> of the current goal,  rather than at top level as in Coq.

This is possible in Coq using the tactic Cut 

Cut a0=b0; [Intros Fact1 | Idtac]

Macros definition can make the syntax close to what you propose.

In HOL they also have a tactic "by" inspired by Mizard that is pretty handy:

a0=b0 by THE_TACTIC_THAT_PROVES_A0=BO

It gives a nice declarative flavor to your proof scripts. 

>Freek Wiedijk> I don't think Coq has "real" first-class local lets? 

You can define one. In my proofs I often use the following constant:

Definition LetP: (A, B:Set) (h:A) ((u:A) u =h ->B) ->B.
Intros A B h H'.
Apply H' with u := h.
Auto.
Defined.

When I want to name an object locally I simply apply LetP.

--Laurent

Ps: The mailing list of Coq seems to be moderated (a message sometimes
needs more than a day to reach the mailing list). An automatic filtering
that would get rid of 90% of the junk email, could be more appropriate?