Hi Johannes, Am Montag, den 28.05.2018, 16:47 +0200 schrieb Johannes Waldmann:
Do we (Haskell) need something similar to "consistent with equals"?
not authorative, but the formalization of the base library in Coq, as part of the the hs-to-coq project, says Eq and Ord need to be compatible: Class OrdLaws (t : Type) {HEq : Eq_ t} {HOrd : Ord t} {HEqLaw : EqLaws t} := { (* The axioms *) Ord_antisym : forall a b, a <= b = true -> b <= a = true -> a == b = true; Ord_trans_le : forall a b c, a <= b = true -> b <= c = true -> a <= c = true; Ord_total : forall a b, a <= b = true \/ b <= a = true; (* The other operations, in terms of <= or == *) Ord_compare_Lt : forall a b, compare a b = Lt <-> b <= a = false; Ord_compare_Eq : forall a b, compare a b = Eq <-> a == b = true; Ord_compare_Gt : forall a b, compare a b = Gt <-> a <= b = false; Ord_lt_le : forall a b, a < b = negb (b <= a); Ord_ge_le : forall a b, a >= b = (b <= a); Ord_gt_le : forall a b, a > b = negb (a <= b); }. https://github.com/antalsz/hs-to-coq/blob/86f4c36dfe4b096eb7d48205cea3fddeea... Because we have a tactic that automates reasoning with lawfull Ord instances and uses Ord_antisym and Ord_compare_Eq internally I cannot easily check if these laws are actually used in the verification of Data.Set. One could argue that “total order” implies “antisymmetric” which implies a relation with (==). Cheers, Joachim -- Joachim Breitner mail@joachim-breitner.de http://www.joachim-breitner.de/