[Haskell-cafe] (names for) invariants for Eq and Ord?

[Joachim Breitner]

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#L14

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 at joachim-breitner.de
  http://www.joachim-breitner.de/
-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 833 bytes
Desc: This is a digitally signed message part
URL: <http://mail.haskell.org/pipermail/haskell-cafe/attachments/20180602/ff6320f8/attachment.sig>