Int Ord proof

lib/Haskell/Law/Bool.agda

@@ -39,11 +39,9 @@ open import Haskell.Law.Def
 --------------------------------------------------
 -- ||
 
--- if a then True else b
-
-||-excludedMiddle : ∀ (a b : Bool) → (a || not a) ≡ True
-||-excludedMiddle False _ = refl
-||-excludedMiddle True  _ = refl
+||-excludedMiddle : ∀ (a : Bool) → (a || not a) ≡ True
+||-excludedMiddle False = refl
+||-excludedMiddle True  = refl
 
 ||-leftTrue : ∀ (a b : Bool) → a ≡ True → (a || b) ≡ True
 ||-leftTrue .True b refl = refl
@@ -64,10 +62,11 @@ not-not : ∀ (a : Bool) → not (not a) ≡ a
 not-not False = refl
 not-not True = refl
 
-not-involution : ∀ (a b : Bool) → a ≡ not b → not a ≡ b
-not-involution .(not b) b refl = not-not b
+not-involution : ∀ {a b : Bool} → a ≡ not b → not a ≡ b
+not-involution {.(not b)} {b} refl = not-not b
 
 --------------------------------------------------
+
 -- if_then_else_
 
 ifFlip : ∀ (b)

lib/Haskell/Law/Int.agda

@@ -1,7 +1,7 @@
 module Haskell.Law.Int where
 
 open import Haskell.Prim
-open import Haskell.Prim.Int using ( int64 )
+open import Haskell.Prim.Int 
 
 open import Haskell.Law.Def
 

lib/Haskell/Law/Ord.agda

@@ -2,6 +2,7 @@ module Haskell.Law.Ord where
 
 open import Haskell.Law.Ord.Def      public
 open import Haskell.Law.Ord.Bool     public
+open import Haskell.Law.Ord.Int      public
 open import Haskell.Law.Ord.Integer  public
 open import Haskell.Law.Ord.Maybe    public
 open import Haskell.Law.Ord.Nat      public

lib/Haskell/Law/Ord/Def.agda

@@ -3,7 +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.Int
 open import Haskell.Prim.Word
 open import Haskell.Prim.Integer
 open import Haskell.Prim.Double
@@ -85,11 +84,11 @@ lte2LtEq : ⦃ iOrdA : Ord a ⦄ → ⦃ IsLawfulOrd a ⦄
 lte2LtEq x y 
   rewrite lt2LteNeq x y
     with (x <= y) in h₁ | (x == y) in h₂
-...| True | True = refl
+...| True | True  = refl
 ...| True | False = refl
-...| False | True = magic $ exFalso 
-  (reflexivity x) 
-  (trans (cong₂  _<=_ refl (equality x y h₂)) h₁)
+...| False | True 
+  rewrite equality x y h₂ | sym $ h₁ 
+  = reflexivity y
 ...| False | False = refl
 
 gte2GtEq : ⦃ iOrdA : Ord a ⦄ → ⦃ IsLawfulOrd a ⦄
@@ -178,7 +177,6 @@ reverseLte a b c d
 -- Postulated instances
 
 postulate instance
-  iLawfulOrdInt : IsLawfulOrd Int
 
   iLawfulOrdWord : IsLawfulOrd Word
 

lib/Haskell/Law/Ord/Int.agda

@@ -0,0 +1,127 @@
+module Haskell.Law.Ord.Int where
+
+open import Haskell.Prim
+open import Haskell.Prim.Int
+open import Haskell.Prim.Bool
+open import Haskell.Prim.Eq
+open import Haskell.Prim.Word
+open import Haskell.Prim.Ord
+
+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.Int
+
+private
+
+  2⁶³ : Nat
+  2⁶³ = 9223372036854775808 
+
+  maxW : Word
+  maxW = (n2w (monusNat 2⁶³ 1))
+
+sign2neq : ∀ (a b : Int) → isNegativeInt a ≡ True → isNegativeInt b ≡ False → ((a == b) ≡ False) 
+sign2neq a@(int64 x) b@(int64 y) h₁ h₂ with a == b in h₃
+... | False = refl --refl
+... | True rewrite equality x y h₃ | sym $ h₁ = h₂
+
+instance
+  iLawfulOrdInt : IsLawfulOrd Int
+
+  iLawfulOrdInt .comparability a@(int64 x) b@(int64 y) 
+    with isNegativeInt a | isNegativeInt b 
+  ... | True  | False = refl
+  ... | False | True 
+    rewrite ||-sym (x == y) True = refl
+  ... | True  | True  = comparability x y
+  ... | False | False = comparability x y 
+
+  iLawfulOrdInt .transitivity a@(int64 x) b@(int64 y) c@(int64 z) h 
+    with isNegativeInt a in h₁ | isNegativeInt b in h₂ | isNegativeInt c in h₃
+  ... | True  | True  | True  =  transitivity x y z h
+  ... | True  | True  | False = refl
+  ... | True  | False | True  rewrite equality y z h 
+    = magic $ exFalso h₃ h₂  
+  ... | True  | False | False = refl
+  ... | False | True  | True  rewrite equality x y (&&-leftTrue (x == y) (y <= z) h) 
+    = magic $ exFalso h₂ h₁
+  ... | False | True  | False rewrite equality x y (&&-leftTrue (x == y) True h) 
+    = magic $ exFalso h₂ h₁
+  ... | False | False | True  rewrite equality y z (&&-rightTrue (x <= y) (y == z) h) 
+    = magic $ exFalso h₃ h₂ 
+  ... | False | False | False = transitivity x y z h
+
+
+  iLawfulOrdInt .reflexivity a 
+    rewrite ||-sym (a < a) (a == a) 
+      | eqReflexivity a 
+    = refl 
+
+  iLawfulOrdInt .antisymmetry a@(int64 x) b@(int64 y) h 
+    with isNegativeInt a | isNegativeInt b 
+  ... | True  | True  = antisymmetry x y h
+  ... | True  | False rewrite eqSymmetry x y = h
+  ... | False | True  = &&-leftTrue (x == y) True h
+  ... | False | False = antisymmetry x y h
+
+
+  iLawfulOrdInt .lte2gte (int64 x) (int64 y) 
+    rewrite eqSymmetry x y 
+    = refl
+
+  iLawfulOrdInt .lt2LteNeq a@(int64 x) b@(int64 y) 
+      with isNegativeInt a in h₁ | isNegativeInt b in h₂ 
+  ...| True  | True  = lt2LteNeq x y
+  ...| True  | False = sym $ not-involution $ sign2neq a b h₁ h₂
+  ...| False | True rewrite eqSymmetry x y | sign2neq b a h₂ h₁ = refl
+  ...| False | False = lt2LteNeq x y
+
+  iLawfulOrdInt .lt2gt a b = refl
+
+  iLawfulOrdInt .compareLt a@(int64 x) b@(int64 y)
+    with isNegativeInt a in h₁ | isNegativeInt b in h₂ 
+  ...| True  | True = compareLt x y
+  ...| True  | False  = refl
+  ...| False | True 
+    rewrite eqSymmetry x y 
+    | sign2neq b a h₂ h₁ = refl
+  ...| False | False = compareLt x y
+
+  iLawfulOrdInt .compareGt a@(int64 x) b@(int64 y)
+    with isNegativeInt a in h₁ | isNegativeInt b in h₂ 
+  ...| True  | True = compareGt x y
+  ...| True  | False  = refl
+  ...| False | True 
+    rewrite eqSymmetry x y 
+    | sign2neq b a h₂ h₁ = refl
+  ...| False | False = compareGt x y
+
+  iLawfulOrdInt .compareEq a@(int64 x) b@(int64 y)
+      with isNegativeInt a in h₁ | isNegativeInt b in h₂ 
+  ...| True  | True = compareEq x y
+  ...| True  | False 
+    rewrite sign2neq a b h₁ h₂ = refl
+  ...| False | True 
+    rewrite eqSymmetry x y | sign2neq b a h₂ h₁ = refl
+  ...| False | False = compareEq x y
+
+  iLawfulOrdInt .min2if a@(int64 x) b@(int64 y)
+    with isNegativeInt a in h₁ | isNegativeInt b in h₂ 
+  ...| True  | True rewrite lte2ngt x y 
+    | sym $ ifFlip (y < x) b a  = eqReflexivity (if (y < x) then b else a)
+  ...| True  | False = eqReflexivity x
+  ...| False | True rewrite eqSymmetry x y 
+    | sign2neq b a h₂ h₁ = eqReflexivity y
+  ...| False | False rewrite lte2ngt x y 
+    | sym $ ifFlip (y < x) b a = eqReflexivity (if (y < x) then b else a) 
+
+  iLawfulOrdInt .max2if a@(int64 x) b@(int64 y)
+      with isNegativeInt a in h₁ | isNegativeInt b in h₂ 
+  ...| False | False rewrite gte2nlt x y | sym $ ifFlip (x < y) b a 
+    = eqReflexivity (if (x < y) then b else a)
+  ...| False | True  = eqReflexivity x
+  ...| True  | False rewrite sign2neq a b h₁ h₂ 
+    = eqReflexivity y
+  ...| True  | True  rewrite gte2nlt x y | sym $ ifFlip (x < y) b a 
+    = eqReflexivity (if (x < y) then b else a)

lib/Haskell/Law/Ord/Integer.agda

@@ -1,7 +1,6 @@
 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
 

lib/Haskell/Prim/Int.agda

@@ -67,15 +67,16 @@ integerToInt : Integer → Int
 integerToInt (pos    n) = int64 (n2w n)
 integerToInt (negsuc n) = negateInt (int64 (n2w (suc n)))
 
-private
+private 
+  -- this function assumes both values to be positive
   ltPosInt : Int → Int → Bool
   ltPosInt (int64 a) (int64 b) = ltWord a b
 
 ltInt : Int → Int → Bool
 ltInt a b with isNegativeInt a | isNegativeInt b
 ... | True  | False = True
 ... | False | True  = False
-... | True  | True  = ltPosInt (negateInt b) (negateInt a)
+... | True  | True  = ltPosInt a b
 ... | False | False = ltPosInt a b
 
 addInt : Int → Int → Int