# (names for) invariants for Eq and Ord? Classic List Threaded 7 messages Open this post in threaded view
|

## (names for) invariants for Eq and Ord?

Open this post in threaded view
|

## Re: (names for) invariants for Eq and Ord?

Open this post in threaded view
|

## Re: (names for) invariants for Eq and Ord?

Open this post in threaded view
|

## Re: (names for) invariants for Eq and Ord?

Open this post in threaded view
|

## Re: (names for) invariants for Eq and Ord?

 In reply to this post by Johannes Waldmann-2 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/86f4c36dfe4b096eb7d48205cea3fddeeab23eaa/examples/containers/theories/OrdTactic.v#L14Because 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   [hidden email]   http://www.joachim-breitner.de/_______________________________________________ Haskell-Cafe mailing list To (un)subscribe, modify options or view archives go to: http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafeOnly members subscribed via the mailman list are allowed to post. signature.asc (849 bytes) Download Attachment