Integer Ord proof

Author: odderwiser

lib/Haskell/Law/Ord/Def.agda

@@ -176,7 +176,7 @@ gt2gte x y h
 -- Postulated instances
 
 postulate instance
-  iLawfulOrdInteger : IsLawfulOrd Integer
+  -- iLawfulOrdInteger : IsLawfulOrd Integer
 
   iLawfulOrdInt : IsLawfulOrd Int
 

lib/Haskell/Law/Ord/Integer.agda

@@ -0,0 +1,62 @@
+module Haskell.Law.Ord.Integer where
+
+open import Haskell.Prim
+open import Haskell.Prim.Bool
+open import Haskell.Prim.Eq
+open import Haskell.Prim.Ord
+
+open import Haskell.Law.Bool
+open import Haskell.Law.Eq
+open import Haskell.Law.Equality
+open import Haskell.Law.Ord.Def
+open import Haskell.Law.Ord.Nat
+open import Haskell.Law.Nat
+
+injectEqSym : ∀ ( a b c d : Nat ) {e e₁ : Bool} { f : Bool → Bool → Bool } → 
+  f (e || a == b ) ( e₁ || c == d) ≡ f (e || b == a) (e₁ || d == c) 
+injectEqSym a b c d 
+  rewrite eqSymmetry a b
+    | eqSymmetry c d 
+    = refl   
+
+inverseEqSym : ∀ ( a b c d : Nat ) (e f : Bool) → 
+  ((e || a == b ) && (f || c == d)) ≡ ((f || d == c) && (e || b == a))
+inverseEqSym a b c d e f 
+  rewrite &&-sym (e || a == b) (f || c == d)  
+  = injectEqSym c d a b {f} {e} {_&&_}
+
+instance
+  iLawfulOrdInteger : IsLawfulOrd Integer
+
+
+  iLawfulOrdInteger .comparability (pos n)    (pos m)    = comparability n m
+  iLawfulOrdInteger .comparability (pos n)    (negsuc m) = refl
+  iLawfulOrdInteger .comparability (negsuc n) (pos m)    = refl
+  iLawfulOrdInteger .comparability (negsuc n) (negsuc m) 
+    rewrite  injectEqSym n m m n {m < n} {n < m} {_||_} 
+     = comparability m n
+    
+  iLawfulOrdInteger .transitivity (pos n)   (pos m)     (pos o)    h₁ = transitivity n m o h₁
+  iLawfulOrdInteger .transitivity (pos n)   (pos m)     (negsuc o) h₁ 
+    rewrite &&-sym (n <= m) False 
+    = h₁
+  iLawfulOrdInteger .transitivity (negsuc n) y          (pos o)    h₁ = refl
+  iLawfulOrdInteger .transitivity (negsuc n) (negsuc m) (negsuc o) h₁ 
+    rewrite eqSymmetry n o 
+    = transitivity o m n (trans (inverseEqSym o m m n (o < m) (m < n)) h₁)
+  
+  iLawfulOrdInteger .reflexivity (pos n)    = reflexivity n
+  iLawfulOrdInteger .reflexivity (negsuc n) = reflexivity n
+  
+  iLawfulOrdInteger .antisymmetry (pos n)    (pos m)    h₁ = antisymmetry n m h₁
+  iLawfulOrdInteger .antisymmetry (negsuc n) (negsuc m) h₁ = antisymmetry n m 
+    $ trans (inverseEqSym n m m n (n < m) (m < n)) h₁
+  
+  iLawfulOrdInteger .lte2gte x y = {!   !}
+  iLawfulOrdInteger .lt2LteNeq x y = {!   !}
+  iLawfulOrdInteger .lt2gt x y = {!   !}
+  iLawfulOrdInteger .compareLt x y = {!   !}
+  iLawfulOrdInteger .compareGt x y = {!   !}
+  iLawfulOrdInteger .compareEq x y = {!   !}
+  iLawfulOrdInteger .min2if x y = {!   !} 
+  iLawfulOrdInteger .max2if x y = {!   !}