[Haskell-cafe] (names for) invariants for Eq and Ord?
Joachim Breitner
mail at joachim-breitner.de
Sat Jun 2 17:32:43 UTC 2018
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>
More information about the Haskell-Cafe
mailing list