The Coq mailing list

["Randy Pollack" <rap AT dcs.ed.ac.uk>]

I assume that Laurent was actually looking for a more natural solution
than "prove it as a top-level lemma".  The assumptions needed to prove
the desired new fact may be local to the current goal, and not easily
avalable for a top-level lemma.

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

  Lemma xxx: (a0 = b0)->(b0 = c0)->G.

Then by "Intros Fact1 Fact2" we get to Laurent's example.  

> A: Set
> a0: A
> b0 : A
> c0: A
> Trans: (a,b,c: A) a = b -> b = c -> a = c
> Sym: (a,b) a = b -> b = a 
> Fact1: a0 = b0
> Fact2: b0 = c0
>   ============================
>     G

In this state you can say something like:

  Local_Definition Fact3: a0=c0 := ... Fact1 ... Fact2 ...

*using* the local facts.  When the Goal "xxx" is completly proved, the
local definition "Fact3" becomes just that, a local "let" in the proof
term.

More generally, in Coq you could have new command "Local_Lemma" to
start a new lemma in the current local context.

Best,
Randy