coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Dependent records conditions

From: Daniel Schepler <dschepler AT gmail.com>
To: coq-club AT inria.fr
Cc: Pierre Casteran <pierre.casteran AT labri.fr>, Victor Porton <porton AT narod.ru>
Subject: Re: [Coq-Club] Dependent records conditions
Date: Mon, 21 Nov 2011 08:33:08 -0800

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)
--
Daniel Schepler

[Coq-Club] Dependent records conditions, Victor Porton
- Re: [Coq-Club] Dependent records conditions, Pierre Casteran
  - Re: [Coq-Club] Dependent records conditions, Daniel Schepler
    - Re: [Coq-Club] Dependent records conditions, AUGER Cedric