The Coq mailing list

[Yves Bertot <Yves.Bertot AT sophia.inria.fr>]

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.
>
>