[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

ADT axioms



Why is it that the extensionality axiom is an implication and not an
equivalence?

I have a simple tree datatype:

tree[t:TYPE+] : DATATYPE
  BEGIN
    scalar (scalar: t): scalar?
    pair   (left: tree, right: tree): pair?
  END tree

among the automatically generated axioms I have

  tree_pair_extensionality: AXIOM
        (FORALL (pair?_var: (pair?), pair?_var2: (pair?)):
           left(pair?_var) = left(pair?_var2)
               AND right(pair?_var) = right(pair?_var2)
               IMPLIES pair?_var = pair?_var2);

but I'd like to be able to prove the reverse implication, for instance

  pair(a,b) = pair(c,d) IMPLIES a=c AND b=d

Am I missing something obvious?

Thank you in advance,

	Matteo