The Coq mailing list

[Jelle Herold <jelle AT defekt.nl>]

Hello Victor,

I'm afraid this will again go to deaf ears, but you made me laugh so 
I'll return the favour:

Let me begin with the important point: You cannot keep asking questions 
like this.

We understand that you really want to learn Coq quickly, but you have to 
be patient. Coq is a complicated system for many reasons and you *will 
not* learn it over night. So, really, for quick results I advice you to 
*DO THE EXERCISES* in the following texts:

 1. Software foundations: (easy)
    http://www.cis.upenn.edu/~bcpierce/sf/

 2. Trimmed down version of CPDT:
    http://adam.chlipala.net/papers/CpdtJFR/

This should take you at least a week or two so I suggest about no more 
questions until you've done that?

Anyway, here is maybe an answer to your question:

On 11/09/2011 12:27 AM, Victor Porton wrote:
> > >   (*
> > >   What's wrong with the following .v file which does not verify:
> > >   How to correct it?
> > >   *)
> > >
> > >   Class C := {
> > >    num: nat;
> > >    cond: num=0
> > >   }.
> > >
> > >   Instance C2: C := { num:=0 }.
> >
> > When I reach this point, I have to prove "0 = 0". Do you really have
> > difficulties proving "0 = 0"? Maybe Type Classes should wait.
>
> The difficulty is not to prove 0 = 0 but with getting the "num" field of the 
> current class instance in the proof of the instance.

You cannot refer to the current instance; you use type classes to 
generalize your proof *for any instance* of the class.

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
*)
------------------