coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- 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
- [Coq-Club] A beginner question in class instances, Victor Porton
- Re: [Coq-Club] A beginner question in class instances,
Alexandre Pilkiewicz
- Re: [Coq-Club] A beginner question in class instances,
Victor Porton
- Re: [Coq-Club] A beginner question in class instances,
Alexandre Pilkiewicz
- Re: [Coq-Club] A beginner question in class instances, Victor Porton
- Re: [Coq-Club] A beginner question in class instances,
Alexandre Pilkiewicz
- Re: [Coq-Club] A beginner question in class instances,
Victor Porton
- Re: [Coq-Club] A beginner question in class instances, Alexandre Pilkiewicz
- Re: [Coq-Club] A beginner question in class instances,
Victor Porton
- Re: [Coq-Club] A beginner question in class instances,
Alexandre Pilkiewicz
- Re: [Coq-Club] A beginner question in class instances, Victor Porton
- Re: [Coq-Club] A beginner question in class instances, Jelle Herold
- Re: [Coq-Club] A beginner question in class instances,
Alexandre Pilkiewicz
- Re: [Coq-Club] A beginner question in class instances,
Victor Porton
- <Possible follow-ups>
- Fwd: [Coq-Club] A beginner question in class instances, Victor Porton
- Re: [Coq-Club] A beginner question in class instances,
Alexandre Pilkiewicz
Archive powered by MhonArc 2.6.16.