The Coq mailing list

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

Le Mon, 21 Nov 2011 08:33:08 -0800,
Daniel Schepler 
<dschepler AT gmail.com>
 a écrit :

> On Monday, November 21, 2011 07:00:51 AM Pierre Casteran wrote:
> > Le 21/11/2011 15:53, Victor Porton a écrit :
> > > Parameter A : Set.
> > > Parameter B : A ->  Prop.
> > > 
> > > Structure Foo := mkFoo { a : A; b : B a }.
> > > 
> > > (* How to prove this lemma? Is it possible at all? *)
> > > Lemma my (u : Foo) : B (@a u).
> > 
> > Is it possible and *******trivial*********
> > 
> > 
> > Lemma my (u : Foo) : B (@a u).
> > destruct u;trivial.
> > Qed.
> 
> Also, Coq defines this lemma for you automatically:
> 
> Check b.
> ==>
> b
>      : forall f : Foo, B (a f)

By the way, I wanted to give the same reply as Daniel, but with this
syntax:

Lemma my (u : Foo) : B (@a u).
Proof (b u).

But it didn't work:
> Error: Command 'Proof ...' can only be used at the beginning of the proof.

I guess it is because "my" has parameter, so an implicit "intros u."
may have been automatically inserted; but the error message is quite
misleading (IMO), as we are at the beginning of the proof!