The Coq mailing list

[ohpato <ohpato AT hanmail.net>]

Mr. Bertot, 

Thank you for the kind answers and advice.



Yves Bertot wrote:
> 
> ohpato wrote:
>> Hello,
>>
>> 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?
>>
>>   
> 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".
>> - Q2:
>> 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'.
>>   
> 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.
>>   Property2)
>>     recored_eq)dec:
>>     forall (r r':Recored_T), {r = r'} + {r <> r'}.
>>   
> This property is a consequence from rcdid_eq_dec and fieldT_q_dec.
>> I think Property1 should be declared as an Axiom. If I do that,
>> can Property2 be proved as a lemma? (or is Vice Versa possible??)
>>   
> As already said, property1 is dangerous and property2 can already be 
> derived from other assumptions.
>> 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.
>>
>>   
> 
> --------------------------------------------------------
> Bug reports: http://logical.saclay.inria.fr/coq-bugs
> Archives: http://pauillac.inria.fr/pipermail/coq-club
>           http://pauillac.inria.fr/bin/wilma/coq-club
> Info: http://pauillac.inria.fr/mailman/listinfo/coq-club
> 
> 

-- 
View this message in context: 
http://www.nabble.com/a-newbie-question-tp22095657p22113648.html
Sent from the Coq mailing list archive at Nabble.com.