coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Yves Bertot <Yves.Bertot AT sophia.inria.fr>
- To: ohpato <ohpato AT hanmail.net>
- Cc: coq-club AT pauillac.inria.fr
- Subject: Re: [Coq-Club] a newbie question
- Date: Thu, 19 Feb 2009 13:22:28 +0100
- List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>
ohpato wrote:
Hello,I don't know what you mean by being unique. I agree that assuming rcdid_eq_dec, you do say elements of RecodedID_T can be distinguished from others using this function, but I don't know how to connect this notion with the word "unique".
I am a newbie just started studying Coq and formal methods.
Today I defined a record type as follows:
Record Record_T : Type := mkRecord_T {
rcdID : RecordID_T;
field : Field_T;
}.
and declared axioms (decidability of equality) for two fields like:
Axiom rcdid_eq_dec: forall rid rid':RecordID_T, {rid = rid'} + {rid <> rid'}.
Axiom fieldT_eq_dec: forall ft ft':Field_T, {ft = ft'} + {ft <> ft'}.
and I could prove
Lemma RecordId_is_equal_when_Record_is_equal:
forall (r r':Record_T),
r = r' -> (rcdID r) = (rcdID r')
Now, I have some questions. (The questions might be very basic and
well-known. Sorry for my ignorance in that case.)
- Q1: By doing the above, I assume a (rcdID:RecordID_T) is unique and
distinguishable from others (e.g. rcdID':RecordID_T). Am I right?
- Q2:This property is probably wrong, as soon as your type Record_T contains two distinguishable elements (elements f1 and f2 such that f1 <> f2), you can construct two elements of Record_ID that share the same first component and have different second components, these records are provably different. If you add this property as an axiom, you will get an inconsistent logic, this kills the purpose of using a proof system.
If so, I wanted to have the following properties additionally.
Property1)
Record_is_equal_when_RecoredID_is_same:
forall (r r':Record_T), (rcdID r) = (rcdID r') -> r = r'.
Property2)This property is a consequence from rcdid_eq_dec and fieldT_q_dec.
recored_eq)dec:
forall (r r':Recored_T), {r = r'} + {r <> r'}.
I think Property1 should be declared as an Axiom. If I do that,As already said, property1 is dangerous and property2 can already be derived from other assumptions.
can Property2 be proved as a lemma? (or is Vice Versa possible??)
or shall I make both of them as Axioms?As a beginner, you should consider that axioms are not for you. Try to get acquainted with the system first, and you may discover that you will never need axioms. The only place where axioms are perfectly legitimate is in module interfaces, but then these module interfaces are supposed to be fulfilled by module implementations and in this sense they are not really axioms.
Thanks in advance.
- [Coq-Club] a newbie question, ohpato
- Re: [Coq-Club] a newbie question, Yves Bertot
- Re: [Coq-Club] a newbie question,
ohpato
- Re: [Coq-Club] a newbie question, Yves Bertot
- Re: [Coq-Club] a newbie question,
ohpato
- Re: [Coq-Club] a newbie question, Yves Bertot
Archive powered by MhonArc 2.6.16.