The Coq mailing list

[ohpato <ohpato AT hanmail.net>]

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?

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

  Property2)
    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,
can Property2 be proved as a lemma? (or is Vice Versa possible??)

or shall I make both of them as Axioms?



Thanks in advance.

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