The Coq mailing list

[Victor Porton <porton AT narod.ru>]

09.11.2011, 03:19, "Alexandre Pilkiewicz" 
<alexandre.pilkiewicz AT polytechnique.org>:
> On Tue, Nov 8, 2011 at 5:50 PM, Victor Porton 
>Â <porton AT narod.ru>
>  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.

If I just remove "have (num C2=0) using tauto" it verifies, but my point is 
not just to verify the theory but to study how to write proofs of type 
classes validity.

Well, Alexandre, you are right supposing that my knowledge of tactics is 
weak. I want to learn more about tactics, but only after I will know how to 
denote the current instance in an instance proof.

> <<<
> Proof. reflexivity. Qed.
>
>> šproof.
>> ššhave (num C2=0) using tauto.
>> šend proof.
>>
>> š--
>> šVictor Porton - http://portonvictor.org

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