Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] A beginner question in class instances

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] A beginner question in class instances


chronological Thread 
  • From: Victor Porton <porton AT narod.ru>
  • To: Alexandre Pilkiewicz <alexandre.pilkiewicz AT polytechnique.org>
  • Cc: Coq <coq-club AT inria.fr>
  • Subject: Re: [Coq-Club] A beginner question in class instances
  • Date: Wed, 09 Nov 2011 03:50:28 +0400
  • Envelope-from: porton AT yandex.ru

09.11.2011, 03:32, "Alexandre Pilkiewicz" 
<alexandre.pilkiewicz AT polytechnique.org>:
> 2011/11/8 Victor Porton 
> <porton AT narod.ru>:
>
>> š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.
>
> C2 does not exist yet, you are defining it. So of course you can't use "num 
> C2"!

OK, you've explained the reason why my code doesn't work.

But how to make it to work as intended, that is how to deal with the 
projector "num" OF THE CURRENT INSTANCE INSIDE AN INSTANCE PROOF?

I need answer this question.

Class C := {
  num: nat;
  cond: num=0
}.

Instance C2: C := { num:=0 }.
proof.
  have (num=0) using tauto.
end proof.

>> š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.
>
> Still.... "0=0" should come first.
>
> Alexandre

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



Archive powered by MhonArc 2.6.16.

Top of Page