The Coq mailing list

[Jelle Herold <jelle AT defekt.nl>]

Hi Victor,

On 11/09/2011 01:12 AM, Victor Porton wrote:
> >   So something like this maybe?
> >   -----------------
> >   Class C := {
> >      num: nat;
> >      cond: num=0
> >   }.
> >
> >   Lemma is_nul `(C) : num = 0.
> >   Proof.
> >      apply cond.
> >   Qed.
> >
> >   Check is_nul.
> >   (*
> >   is_nul
> >         : forall H : C, num = 0
> >   *)
> >   ------------------
>
> It does not answer my question. My question was about instance proofs, but there are no 
> keyword "Instance" in your example. I want an example of an instance proof.

You want to proof that C2 with num=2 is an instance of C.
In order to do that you need to specify all the fields. You only 
specified the "num" field, but not the "cond" field (which is ok).

Proof mode is smart enough to figure this out, so when you write

  Instance C2: C := { num:=0 }.
  Proof.

Your goal is automatically set to proving "cond", which states "num=0" 
which for this instance gives you "0=0" so that is why you need to proof 
that.

So alternatively you could write (this makes sense for more complicated 
classes)

  Lemma silly : 0 = 0.
  Proof. reflexivity. Qed.

  Instance C2 : C := { num = 0; cond = silly }.


> I think, I should do these exercises (but now it's late night here).

I agree, take you time.

> Thanks for the exercises. I will look into them.
>
> This is my last message sent before I look into exercises.

Very well, I'm happy about that. It is really a lot of work and new 
concepts so don't expect to finish them in a day (or a week.. month...).

Also you should download SF and/or CPDT and then load them in CoqIDE and 
do the exercises in the file. Hands on, like paper mathematics, don't 
just look at them.