The Coq mailing list

[Victor Porton <porton AT narod.ru>]

Hi Jelle,

09.11.2011, 04:00, "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
> š*)
> š------------------

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.

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

Thanks for the exercises. I will look into them.

This is my last message sent before I look into exercises.

--
Victor Porton - http://portonvictor.org