lawful order word

Author: odderwiser

lib/Haskell/Law/Ord.agda

@@ -7,3 +7,4 @@ open import Haskell.Law.Ord.Integer  public
 open import Haskell.Law.Ord.Maybe    public
 open import Haskell.Law.Ord.Nat      public
 open import Haskell.Law.Ord.Ordering public
+open import Haskell.Law.Ord.Word     public

lib/Haskell/Law/Ord/Def.agda

@@ -3,8 +3,6 @@ module Haskell.Law.Ord.Def where
 open import Haskell.Prim
 open import Haskell.Prim.Ord
 open import Haskell.Prim.Bool
-open import Haskell.Prim.Word
-open import Haskell.Prim.Integer
 open import Haskell.Prim.Double
 open import Haskell.Prim.Tuple
 open import Haskell.Prim.Monoid
@@ -178,8 +176,6 @@ reverseLte a b c d
 
 postulate instance
 
-  iLawfulOrdWord : IsLawfulOrd Word
-
   iLawfulOrdDouble : IsLawfulOrd Double
 
   iLawfulOrdChar : IsLawfulOrd Char

lib/Haskell/Law/Ord/Int.agda

@@ -11,6 +11,7 @@ open import Haskell.Law.Bool
 open import Haskell.Law.Equality
 open import Haskell.Law.Eq
 open import Haskell.Law.Ord.Def
+open import Haskell.Law.Ord.Word
 open import Haskell.Law.Int
 
 

lib/Haskell/Law/Ord/Word.agda

@@ -0,0 +1,68 @@
+module Haskell.Law.Ord.Word where
+
+open import Haskell.Prim
+open import Haskell.Prim.Eq
+open import Haskell.Prim.Ord
+open import Haskell.Prim.Word   using ( Word )
+
+open import Haskell.Law.Bool
+open import Haskell.Law.Eq
+open import Haskell.Law.Ord.Def
+open import Haskell.Law.Ord.Nat
+
+instance
+  iLawfulOrdWord : IsLawfulOrd Word
+
+  iLawfulOrdWord .comparability a b 
+    with (w2n a) | (w2n b)
+  ... | x | y  = comparability x y
+  
+  iLawfulOrdWord .transitivity a b c h 
+     with (w2n a) | (w2n b) | (w2n c) 
+  ... | x  | y | z = transitivity x y z h 
+  
+  iLawfulOrdWord .reflexivity a 
+    with (w2n a)
+  ... | x = reflexivity x
+
+  iLawfulOrdWord .antisymmetry a b h 
+    with (w2n a) | (w2n b) 
+  ... | x | y = antisymmetry x y h 
+
+  iLawfulOrdWord .lte2gte a b
+    with (w2n a) | (w2n b) 
+  ... | x | y = lte2gte x y 
+
+  iLawfulOrdWord .lt2LteNeq a b 
+    with (w2n a) | (w2n b) 
+  ... | x | y = lt2LteNeq x y
+
+  iLawfulOrdWord .lt2gt a b 
+    with (w2n a) | (w2n b) 
+  ... | x | y = lt2gt x y
+
+  iLawfulOrdWord .compareLt a b 
+    with (w2n a) | (w2n b) 
+  ... | x | y = compareLt x y
+  
+  iLawfulOrdWord .compareGt a b
+    with (w2n a) | (w2n b) 
+  ... | x | y = compareGt x y
+  
+  iLawfulOrdWord .compareEq a b
+    with (w2n a) | (w2n b) 
+  ... | x | y =  compareEq x y
+  
+  iLawfulOrdWord .min2if a b
+    with (w2n a) | (w2n b)  
+  ... | x | y 
+    rewrite lte2ngt x y 
+    | ifFlip (y < x) a b 
+    = eqReflexivity (if (y < x) then b else a) 
+  
+  iLawfulOrdWord .max2if a b 
+    with (w2n a) | (w2n b)  
+  ... | x | y 
+    rewrite gte2nlt x y
+    | ifFlip (x < y) a b  
+    = eqReflexivity (if (x < y) then b else a)