From c55724787c7b9ac13455e1bd826dfac2ad244cf2 Mon Sep 17 00:00:00 2001
From: Aleksander Wolska <odderwiser@gmail.com>
Date: Wed, 17 Apr 2024 18:10:07 +0200
Subject: [PATCH 1/6] Nat Ord proof

---
 lib/Haskell/Law/Ord.agda     |  1 +
 lib/Haskell/Law/Ord/Def.agda |  2 -
 lib/Haskell/Law/Ord/Nat.agda | 85 ++++++++++++++++++++++++++++++++++++
 3 files changed, 86 insertions(+), 2 deletions(-)
 create mode 100644 lib/Haskell/Law/Ord/Nat.agda

diff --git a/lib/Haskell/Law/Ord.agda b/lib/Haskell/Law/Ord.agda
index ab66490c..827a09ae 100644
--- a/lib/Haskell/Law/Ord.agda
+++ b/lib/Haskell/Law/Ord.agda
@@ -3,4 +3,5 @@ module Haskell.Law.Ord where
 open import Haskell.Law.Ord.Def      public
 open import Haskell.Law.Ord.Bool     public
 open import Haskell.Law.Ord.Maybe    public
+open import Haskell.Law.Ord.Nat      public
 open import Haskell.Law.Ord.Ordering public
diff --git a/lib/Haskell/Law/Ord/Def.agda b/lib/Haskell/Law/Ord/Def.agda
index 4acb6fe4..a0524274 100644
--- a/lib/Haskell/Law/Ord/Def.agda
+++ b/lib/Haskell/Law/Ord/Def.agda
@@ -176,8 +176,6 @@ gt2gte x y h
 -- Postulated instances
 
 postulate instance
-  iLawfulOrdNat : IsLawfulOrd Nat
-
   iLawfulOrdInteger : IsLawfulOrd Integer
 
   iLawfulOrdInt : IsLawfulOrd Int
diff --git a/lib/Haskell/Law/Ord/Nat.agda b/lib/Haskell/Law/Ord/Nat.agda
new file mode 100644
index 00000000..4838ddd3
--- /dev/null
+++ b/lib/Haskell/Law/Ord/Nat.agda
@@ -0,0 +1,85 @@
+module Haskell.Law.Ord.Nat 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.Nat
+
+instance
+  iLawfulOrdNat : IsLawfulOrd Nat
+
+  iLawfulOrdNat .comparability zero    zero    = refl
+  iLawfulOrdNat .comparability zero    (suc y) = refl
+  iLawfulOrdNat .comparability (suc x) zero    = refl
+  iLawfulOrdNat .comparability (suc x) (suc y) 
+    rewrite comparability x y 
+    = refl
+
+  iLawfulOrdNat .transitivity zero    y       zero    h₁ = refl
+  iLawfulOrdNat .transitivity zero    y       (suc z) h₁ = refl
+  iLawfulOrdNat .transitivity (suc x) (suc y) zero    h₁ 
+    rewrite &&-sym (x <= y) False  
+    = h₁ 
+  iLawfulOrdNat .transitivity (suc x) (suc y) (suc z) h₁ = transitivity x y z h₁
+  
+  iLawfulOrdNat .reflexivity zero    = refl
+  iLawfulOrdNat .reflexivity (suc x) = reflexivity x
+  
+  iLawfulOrdNat .antisymmetry zero    zero    h₁ = refl
+  iLawfulOrdNat .antisymmetry (suc x) (suc y) h₁ = antisymmetry x y h₁ 
+
+  iLawfulOrdNat .lte2gte zero    zero    = refl
+  iLawfulOrdNat .lte2gte zero    (suc y) = refl
+  iLawfulOrdNat .lte2gte (suc x) zero    = refl
+  iLawfulOrdNat .lte2gte (suc x) (suc y) = lte2gte x y
+  
+  iLawfulOrdNat .lt2LteNeq zero    zero    = refl
+  iLawfulOrdNat .lt2LteNeq zero    (suc y) = refl
+  iLawfulOrdNat .lt2LteNeq (suc x) zero    = refl
+  iLawfulOrdNat .lt2LteNeq (suc x) (suc y) = lt2LteNeq x y
+
+  iLawfulOrdNat .lt2gt zero    y = refl
+  iLawfulOrdNat .lt2gt (suc x) y = refl
+  
+  iLawfulOrdNat .compareLt zero    zero    = refl
+  iLawfulOrdNat .compareLt zero    (suc y) = refl
+  iLawfulOrdNat .compareLt (suc x) zero    = refl
+  iLawfulOrdNat .compareLt (suc x) (suc y) = compareLt x y
+   
+  iLawfulOrdNat .compareGt zero    zero    = refl
+  iLawfulOrdNat .compareGt zero    (suc y) = refl
+  iLawfulOrdNat .compareGt (suc x) zero    = refl
+  iLawfulOrdNat .compareGt (suc x) (suc y) = compareGt x y
+   
+  iLawfulOrdNat .compareEq zero    zero    = refl
+  iLawfulOrdNat .compareEq zero    (suc y) = refl
+  iLawfulOrdNat .compareEq (suc x) zero    = refl
+  iLawfulOrdNat .compareEq (suc x) (suc y) = compareEq x y 
+
+  iLawfulOrdNat .min2if zero    zero                      = refl
+  iLawfulOrdNat .min2if zero    (suc y)                   = refl
+  iLawfulOrdNat .min2if (suc x) zero                      = refl
+  iLawfulOrdNat .min2if (suc x) (suc y) with x <= y in h₁ 
+  ... | True 
+    rewrite (cong (min x y ==_) (sym $ ifTrueEqThen (x <= y) {x} {y} h₁)) 
+    = min2if x y
+  ... | False 
+    rewrite (cong (min x y ==_) (sym $ ifFalseEqElse (x <= y) {x} {y} h₁)) 
+    = min2if x y
+            
+  iLawfulOrdNat .max2if zero    zero                        = refl
+  iLawfulOrdNat .max2if zero    (suc y)                     = eqReflexivity y
+  iLawfulOrdNat .max2if (suc x) zero                        = eqReflexivity x
+  iLawfulOrdNat .max2if (suc x) (suc y) with x >= y in h₁
+  ... | True 
+    rewrite (cong (max x y ==_) (sym $ ifTrueEqThen (x >= y) {x} {y} h₁)) 
+    = max2if x y    
+  ... | False 
+    rewrite (cong (max x y ==_) (sym $ ifFalseEqElse (x >= y) {x} {y} h₁)) 
+    = max2if x y

From 836351fc38ffba92fc3fd8e9c9f25a96c06acddc Mon Sep 17 00:00:00 2001
From: Aleksander Wolska <odderwiser@gmail.com>
Date: Wed, 17 Apr 2024 21:57:26 +0200
Subject: [PATCH 2/6] Integer Ord proof

---
 lib/Haskell/Law/Bool.agda        |   9 ++-
 lib/Haskell/Law/Def.agda         |   3 +
 lib/Haskell/Law/Ord.agda         |   1 +
 lib/Haskell/Law/Ord/Def.agda     |  32 +++++-----
 lib/Haskell/Law/Ord/Integer.agda | 102 +++++++++++++++++++++++++++++++
 5 files changed, 129 insertions(+), 18 deletions(-)
 create mode 100644 lib/Haskell/Law/Ord/Integer.agda

diff --git a/lib/Haskell/Law/Bool.agda b/lib/Haskell/Law/Bool.agda
index d33d5e37..a53b8a7c 100644
--- a/lib/Haskell/Law/Bool.agda
+++ b/lib/Haskell/Law/Bool.agda
@@ -4,11 +4,11 @@ open import Haskell.Prim
 open import Haskell.Prim.Bool
 
 open import Haskell.Law.Equality
-
+open import Haskell.Law.Def
 --------------------------------------------------
 -- &&
 
-&&-sym : ∀ (a b : Bool) → (a && b) ≡ (b && a)
+&&-sym : F-sym _&&_
 &&-sym False False = refl
 &&-sym False True = refl
 &&-sym True False = refl
@@ -52,6 +52,11 @@ open import Haskell.Law.Equality
 ||-rightTrue False .True refl = refl
 ||-rightTrue True  .True refl = refl
 
+||-sym : F-sym _||_
+||-sym False False = refl
+||-sym False True = refl
+||-sym True False = refl
+||-sym True True = refl
 --------------------------------------------------
 -- not
 
diff --git a/lib/Haskell/Law/Def.agda b/lib/Haskell/Law/Def.agda
index 1099dcf6..d7941f95 100644
--- a/lib/Haskell/Law/Def.agda
+++ b/lib/Haskell/Law/Def.agda
@@ -4,3 +4,6 @@ open import Haskell.Prim
 
 Injective : (a → b) → Set _
 Injective f = ∀ {x y} → f x ≡ f y → x ≡ y
+
+F-sym : (a → a → b) → Set _ 
+F-sym f = ∀ x y → f x y ≡ f y x
diff --git a/lib/Haskell/Law/Ord.agda b/lib/Haskell/Law/Ord.agda
index 827a09ae..c30d9e79 100644
--- a/lib/Haskell/Law/Ord.agda
+++ b/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.Integer  public
 open import Haskell.Law.Ord.Maybe    public
 open import Haskell.Law.Ord.Nat      public
 open import Haskell.Law.Ord.Ordering public
diff --git a/lib/Haskell/Law/Ord/Def.agda b/lib/Haskell/Law/Ord/Def.agda
index a0524274..fa8aeaa3 100644
--- a/lib/Haskell/Law/Ord/Def.agda
+++ b/lib/Haskell/Law/Ord/Def.agda
@@ -84,20 +84,13 @@ lte2LtEq : ⦃ iOrdA : Ord a ⦄ → ⦃ IsLawfulOrd a ⦄
   → ∀ (x y : a) → (x <= y) ≡ (x < y || x == y)
 lte2LtEq x y 
   rewrite lt2LteNeq x y
-    | compareEq x y
-  with (x <= y) in h₁ | (compare x y) in h₂
-... | False | LT = refl
-... | False | EQ = magic $ exFalso (reflexivity x) $ begin 
-    (x <= x)  ≡⟨ (cong (x <=_) (equality x y (begin 
-      (x == y)            ≡⟨ compareEq x y ⟩ 
-      (compare x y == EQ) ≡⟨ equality' (compare x y) EQ h₂ ⟩ 
-      True                ∎ ) ) ) ⟩
-    (x <= y)  ≡⟨ h₁ ⟩ 
-    False ∎
-... | False | GT = refl
-... | True  | LT = refl
-... | True  | EQ = refl
-... | True  | GT = refl
+    with (x <= y) in h₁ | (x == y) in h₂
+...| True | True = refl
+...| True | False = refl
+...| False | True = magic $ exFalso 
+  (reflexivity x) 
+  (trans (cong₂  _<=_ refl (equality x y h₂)) h₁)
+...| False | False = refl
 
 gte2GtEq : ⦃ iOrdA : Ord a ⦄ → ⦃ IsLawfulOrd a ⦄
   → ∀ (x y : a) → (x >= y) ≡ (x > y || x == y)
@@ -172,12 +165,19 @@ gt2gte x y h
     | lte2gte y x
   = refl
 
+reverseLte : ⦃ iOrdA : Ord a ⦄ → ⦃ IsLawfulOrd a ⦄
+  →  ∀ ( a b c d : a ) → 
+  ((a <= b) && (c <= d)) ≡ (( d >= c) && (b >= a))
+reverseLte a b c d 
+  rewrite &&-sym (a <= b) (c <= d)
+  | sym $ lte2gte c d 
+  | sym $ lte2gte a b  
+  = refl
+
 --------------------------------------------------
 -- Postulated instances
 
 postulate instance
-  iLawfulOrdInteger : IsLawfulOrd Integer
-
   iLawfulOrdInt : IsLawfulOrd Int
 
   iLawfulOrdWord : IsLawfulOrd Word
diff --git a/lib/Haskell/Law/Ord/Integer.agda b/lib/Haskell/Law/Ord/Integer.agda
new file mode 100644
index 00000000..68463419
--- /dev/null
+++ b/lib/Haskell/Law/Ord/Integer.agda
@@ -0,0 +1,102 @@
+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.Integer
+open import Haskell.Law.Ord.Def
+open import Haskell.Law.Ord.Nat
+open import Haskell.Law.Nat
+
+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 sym $ lte2gte m n
+    | sym $ lte2gte 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 (reverseLte 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 (reverseLte n m m n) h₁
+  
+  iLawfulOrdInteger .lte2gte (pos n)    (pos m) 
+    rewrite eqSymmetry n m 
+    = refl
+  iLawfulOrdInteger .lte2gte (pos n)    (negsuc m) = refl
+  iLawfulOrdInteger .lte2gte (negsuc n) (pos m)    = refl
+  iLawfulOrdInteger .lte2gte (negsuc n) (negsuc m) 
+    rewrite eqSymmetry n m 
+    = refl
+    
+  iLawfulOrdInteger .lt2LteNeq (pos n)    (pos m)    = lt2LteNeq n m
+  iLawfulOrdInteger .lt2LteNeq (pos n)    (negsuc m) = refl
+  iLawfulOrdInteger .lt2LteNeq (negsuc n) (pos m)   = refl
+  iLawfulOrdInteger .lt2LteNeq (negsuc n) (negsuc m) 
+    rewrite eqSymmetry n m 
+    = lt2LteNeq m n
+  
+  iLawfulOrdInteger .lt2gt x y = refl
+  
+  iLawfulOrdInteger .compareLt (pos n)    (pos m)    = compareLt n m
+  iLawfulOrdInteger .compareLt (pos n)    (negsuc m) = refl
+  iLawfulOrdInteger .compareLt (negsuc n) (pos m)    = refl
+  iLawfulOrdInteger .compareLt (negsuc n) (negsuc m) 
+    rewrite eqSymmetry n m 
+    = compareLt m n
+  
+  iLawfulOrdInteger .compareGt (pos n)    (pos m)    = compareGt n m 
+  iLawfulOrdInteger .compareGt (pos n)    (negsuc m) = refl
+  iLawfulOrdInteger .compareGt (negsuc n) (pos m)    = refl
+  iLawfulOrdInteger .compareGt (negsuc n) (negsuc m) 
+    rewrite eqSymmetry n m 
+    = compareGt m n
+  
+  iLawfulOrdInteger .compareEq (pos n)    (pos m)    = compareEq n m
+  iLawfulOrdInteger .compareEq (pos n)    (negsuc m) = refl
+  iLawfulOrdInteger .compareEq (negsuc n) (pos m)    = refl
+  iLawfulOrdInteger .compareEq (negsuc n) (negsuc m) 
+    rewrite eqSymmetry n m 
+    = compareEq m n
+  
+  iLawfulOrdInteger .min2if (pos n)    (pos m) 
+    rewrite lte2ngt n m
+    | sym $ ifFlip (m < n) (pos m) (pos n)  
+    = eqReflexivity (min (pos n) (pos m))
+  iLawfulOrdInteger .min2if (pos n)    (negsuc m) = eqReflexivity m
+  iLawfulOrdInteger .min2if (negsuc n) (pos m)    = eqReflexivity n
+  iLawfulOrdInteger .min2if (negsuc n) (negsuc m) 
+    rewrite gte2nlt n m  
+    | sym $ ifFlip (n < m) (negsuc m) (negsuc n) 
+    = eqReflexivity (min (negsuc n) (negsuc m)) 
+   
+  iLawfulOrdInteger .max2if (pos n)    (pos m) 
+    rewrite gte2nlt n m 
+    | sym (ifFlip (n < m) (pos m) (pos n))  
+    = eqReflexivity (max (pos n) (pos m)) 
+  iLawfulOrdInteger .max2if (pos n)    (negsuc m) = eqReflexivity n  
+  iLawfulOrdInteger .max2if (negsuc n) (pos m)    = eqReflexivity m 
+  iLawfulOrdInteger .max2if (negsuc n) (negsuc m) 
+    rewrite lte2ngt n m
+    | sym $ ifFlip (m < n) (negsuc m) (negsuc n) 
+    = eqReflexivity (max (negsuc n) (negsuc m))

From 7c7fc3e9091102fe8442e0458624f7973df78fd7 Mon Sep 17 00:00:00 2001
From: Aleksander Wolska <odderwiser@gmail.com>
Date: Fri, 27 Dec 2024 17:31:22 +0100
Subject: [PATCH 3/6] improve existing Boolean helper proofs

||-excludedMiddle does not require two variables
not-invloution works with implicit arguments, can derive them from the hypothesis
---
 lib/Haskell/Law/Bool.agda | 13 ++++++-------
 test/LawfulOrd.agda       |  2 +-
 2 files changed, 7 insertions(+), 8 deletions(-)

diff --git a/lib/Haskell/Law/Bool.agda b/lib/Haskell/Law/Bool.agda
index a53b8a7c..df4c0a76 100644
--- a/lib/Haskell/Law/Bool.agda
+++ b/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)
diff --git a/test/LawfulOrd.agda b/test/LawfulOrd.agda
index 6027f6ab..5fdb054f 100644
--- a/test/LawfulOrd.agda
+++ b/test/LawfulOrd.agda
@@ -13,7 +13,7 @@ nLtEq2Gt : ⦃ iOrdA : Ord a ⦄ → ⦃ IsLawfulOrd a ⦄
 nLtEq2Gt x y ⦃ h1 ⦄ ⦃ h2 ⦄ =
   begin
     (x > y)
-  ≡⟨ sym (not-involution (x <= y) (x > y) (lte2ngt x y)) ⟩
+  ≡⟨ sym (not-involution (lte2ngt x y)) ⟩
     not (x <= y)
   ≡⟨ cong not (lte2LtEq x y) ⟩
     not ((x < y) || (x == y))

From 5a6d00115056185950b1beea8449dca9ae682d26 Mon Sep 17 00:00:00 2001
From: Aleksander Wolska <odderwiser@gmail.com>
Date: Fri, 27 Dec 2024 17:34:08 +0100
Subject: [PATCH 4/6] LawfulOrd Int proofs

---
 lib/Haskell/Law/Bool.agda        |   2 +-
 lib/Haskell/Law/Ord.agda         |   1 +
 lib/Haskell/Law/Ord/Def.agda     |  10 +--
 lib/Haskell/Law/Ord/Int.agda     | 128 +++++++++++++++++++++++++++++++
 lib/Haskell/Law/Ord/Integer.agda |   9 +--
 lib/Haskell/Prim/Int.agda        |   5 +-
 6 files changed, 141 insertions(+), 14 deletions(-)
 create mode 100644 lib/Haskell/Law/Ord/Int.agda

diff --git a/lib/Haskell/Law/Bool.agda b/lib/Haskell/Law/Bool.agda
index df4c0a76..7edd9a08 100644
--- a/lib/Haskell/Law/Bool.agda
+++ b/lib/Haskell/Law/Bool.agda
@@ -73,7 +73,7 @@ ifFlip : ∀ (b)
        → (t : {{not b ≡ True}} → a)
        → (e : {{not b ≡ False}} → a)
        → (if not b then t                             else e) ≡
-         (if b     then (e {{not-involution _ _ it}}) else t {{not-involution _ _ it}})
+         (if b     then (e {{not-involution it}}) else t {{not-involution it}})
 ifFlip False _ _ = refl
 ifFlip True  _ _ = refl
 
diff --git a/lib/Haskell/Law/Ord.agda b/lib/Haskell/Law/Ord.agda
index c30d9e79..7f3f2d81 100644
--- a/lib/Haskell/Law/Ord.agda
+++ b/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
diff --git a/lib/Haskell/Law/Ord/Def.agda b/lib/Haskell/Law/Ord/Def.agda
index fa8aeaa3..2bdfba85 100644
--- a/lib/Haskell/Law/Ord/Def.agda
+++ b/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
 
diff --git a/lib/Haskell/Law/Ord/Int.agda b/lib/Haskell/Law/Ord/Int.agda
new file mode 100644
index 00000000..47d0d4ec
--- /dev/null
+++ b/lib/Haskell/Law/Ord/Int.agda
@@ -0,0 +1,128 @@
+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
+
+
+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 
+    | ifFlip (y < x) a b 
+    = 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 
+    | ifFlip (y < x) a b 
+    = 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 
+    | ifFlip (x < y) a b
+    = 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 
+    | ifFlip (x < y) a b
+    = eqReflexivity (if (x < y) then b else a)
diff --git a/lib/Haskell/Law/Ord/Integer.agda b/lib/Haskell/Law/Ord/Integer.agda
index 68463419..346c53e0 100644
--- a/lib/Haskell/Law/Ord/Integer.agda
+++ b/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
 
@@ -81,22 +80,22 @@ instance
   
   iLawfulOrdInteger .min2if (pos n)    (pos m) 
     rewrite lte2ngt n m
-    | sym $ ifFlip (m < n) (pos m) (pos n)  
+    | ifFlip (m < n) (pos n) (pos m)  
     = eqReflexivity (min (pos n) (pos m))
   iLawfulOrdInteger .min2if (pos n)    (negsuc m) = eqReflexivity m
   iLawfulOrdInteger .min2if (negsuc n) (pos m)    = eqReflexivity n
   iLawfulOrdInteger .min2if (negsuc n) (negsuc m) 
     rewrite gte2nlt n m  
-    | sym $ ifFlip (n < m) (negsuc m) (negsuc n) 
+    | ifFlip (n < m) (negsuc n) (negsuc m) 
     = eqReflexivity (min (negsuc n) (negsuc m)) 
    
   iLawfulOrdInteger .max2if (pos n)    (pos m) 
     rewrite gte2nlt n m 
-    | sym (ifFlip (n < m) (pos m) (pos n))  
+    | ifFlip (n < m) (pos n) (pos m)
     = eqReflexivity (max (pos n) (pos m)) 
   iLawfulOrdInteger .max2if (pos n)    (negsuc m) = eqReflexivity n  
   iLawfulOrdInteger .max2if (negsuc n) (pos m)    = eqReflexivity m 
   iLawfulOrdInteger .max2if (negsuc n) (negsuc m) 
     rewrite lte2ngt n m
-    | sym $ ifFlip (m < n) (negsuc m) (negsuc n) 
+    | ifFlip (m < n) (negsuc n) (negsuc m) 
     = eqReflexivity (max (negsuc n) (negsuc m))
diff --git a/lib/Haskell/Prim/Int.agda b/lib/Haskell/Prim/Int.agda
index 4cc446ef..c819c3dc 100644
--- a/lib/Haskell/Prim/Int.agda
+++ b/lib/Haskell/Prim/Int.agda
@@ -67,7 +67,8 @@ 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
 
@@ -75,7 +76,7 @@ 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

From ef14b3ba4479b76e51fdcaea85353a770798a73b Mon Sep 17 00:00:00 2001
From: Aleksander Wolska <odderwiser@gmail.com>
Date: Mon, 9 Dec 2024 23:17:15 +0100
Subject: [PATCH 5/6] lawful order word

---
 lib/Haskell/Law/Ord.agda      |  1 +
 lib/Haskell/Law/Ord/Def.agda  |  4 ---
 lib/Haskell/Law/Ord/Int.agda  |  1 +
 lib/Haskell/Law/Ord/Word.agda | 68 +++++++++++++++++++++++++++++++++++
 4 files changed, 70 insertions(+), 4 deletions(-)
 create mode 100644 lib/Haskell/Law/Ord/Word.agda

diff --git a/lib/Haskell/Law/Ord.agda b/lib/Haskell/Law/Ord.agda
index 7f3f2d81..f5aec6f0 100644
--- a/lib/Haskell/Law/Ord.agda
+++ b/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
diff --git a/lib/Haskell/Law/Ord/Def.agda b/lib/Haskell/Law/Ord/Def.agda
index 2bdfba85..ab153c54 100644
--- a/lib/Haskell/Law/Ord/Def.agda
+++ b/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
diff --git a/lib/Haskell/Law/Ord/Int.agda b/lib/Haskell/Law/Ord/Int.agda
index 47d0d4ec..28eee0e1 100644
--- a/lib/Haskell/Law/Ord/Int.agda
+++ b/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
 
 
diff --git a/lib/Haskell/Law/Ord/Word.agda b/lib/Haskell/Law/Ord/Word.agda
new file mode 100644
index 00000000..3b007c81
--- /dev/null
+++ b/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) 
\ No newline at end of file

From 77488d2e3e13248191950e95626d16fcb0a73bf5 Mon Sep 17 00:00:00 2001
From: Aleksander Wolska <odderwiser@gmail.com>
Date: Wed, 25 Dec 2024 20:09:11 +0100
Subject: [PATCH 6/6] iLwfulOrd Char and Unit

---
 lib/Haskell/Law/Ord.agda      |  1 +
 lib/Haskell/Law/Ord/Char.agda | 68 +++++++++++++++++++++++++++++++++++
 lib/Haskell/Law/Ord/Def.agda  |  4 ---
 lib/Haskell/Law/Ord/Unit.agda | 23 ++++++++++++
 4 files changed, 92 insertions(+), 4 deletions(-)
 create mode 100644 lib/Haskell/Law/Ord/Char.agda
 create mode 100644 lib/Haskell/Law/Ord/Unit.agda

diff --git a/lib/Haskell/Law/Ord.agda b/lib/Haskell/Law/Ord.agda
index f5aec6f0..cb7eae82 100644
--- a/lib/Haskell/Law/Ord.agda
+++ b/lib/Haskell/Law/Ord.agda
@@ -7,4 +7,5 @@ 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.Unit     public
 open import Haskell.Law.Ord.Word     public
diff --git a/lib/Haskell/Law/Ord/Char.agda b/lib/Haskell/Law/Ord/Char.agda
new file mode 100644
index 00000000..1af05afc
--- /dev/null
+++ b/lib/Haskell/Law/Ord/Char.agda
@@ -0,0 +1,68 @@
+module Haskell.Law.Ord.Char where
+
+open import Haskell.Prim
+open import Haskell.Prim.Eq
+open import Haskell.Prim.Ord
+
+open import Haskell.Law.Bool
+open import Haskell.Law.Eq.Def
+open import Haskell.Law.Eq.Instances
+open import Haskell.Law.Ord.Def
+open import Haskell.Law.Ord.Nat
+
+instance
+  iLawfulOrdChar : IsLawfulOrd Char
+
+  iLawfulOrdChar .comparability a b 
+    with (c2n a) | (c2n b) 
+  ... | n | m = comparability n m
+
+  iLawfulOrdChar .transitivity a b c h 
+    with (c2n a) | (c2n b) | (c2n c)
+  ... | n | m | o = transitivity n m o h
+
+  iLawfulOrdChar .reflexivity a
+    with (c2n a)
+  ... | n = reflexivity n
+
+  iLawfulOrdChar .antisymmetry a b h
+    with (c2n a) | (c2n b)
+  ... | n | m = antisymmetry n m h
+  
+  iLawfulOrdChar .lte2gte a b 
+    with (c2n a) | (c2n b)
+  ... | n | m = lte2gte n m
+
+  iLawfulOrdChar .lt2LteNeq a b 
+    with (c2n a) | (c2n b)
+  ... | n | m = lt2LteNeq n m
+
+  iLawfulOrdChar .lt2gt a b 
+    with (c2n a) | (c2n b)
+  ... | n | m = lt2gt n m
+
+  iLawfulOrdChar .compareLt a b 
+    with (c2n a) | (c2n b)
+  ... | n | m = compareLt n m
+
+  iLawfulOrdChar .compareGt a b 
+    with (c2n a) | (c2n b)
+  ... | n | m = compareGt n m
+
+  iLawfulOrdChar .compareEq a b 
+    with (c2n a) | (c2n b)
+  ... | n | m = compareEq n m
+
+  iLawfulOrdChar .min2if a b 
+    with (c2n a) | (c2n b)
+  ... | n | m 
+    rewrite lte2ngt n m 
+    | ifFlip (m < n) a b 
+    = eqReflexivity (if (m < n) then b else a) 
+
+  iLawfulOrdChar .max2if a b
+    with (c2n a) | (c2n b)
+  ... | n | m 
+    rewrite gte2nlt n m
+    | ifFlip (n < m) a b  
+    = eqReflexivity (if (n < m) then b else a)
diff --git a/lib/Haskell/Law/Ord/Def.agda b/lib/Haskell/Law/Ord/Def.agda
index ab153c54..6d3fd2a4 100644
--- a/lib/Haskell/Law/Ord/Def.agda
+++ b/lib/Haskell/Law/Ord/Def.agda
@@ -178,10 +178,6 @@ postulate instance
 
   iLawfulOrdDouble : IsLawfulOrd Double
 
-  iLawfulOrdChar : IsLawfulOrd Char
-
-  iLawfulOrdUnit : IsLawfulOrd ⊤
-
   iLawfulOrdTuple₂ : ⦃ iOrdA : Ord a ⦄ ⦃ iOrdB : Ord b ⦄
                    → ⦃ IsLawfulOrd a ⦄ → ⦃ IsLawfulOrd b ⦄
                    → IsLawfulOrd (a × b)
diff --git a/lib/Haskell/Law/Ord/Unit.agda b/lib/Haskell/Law/Ord/Unit.agda
new file mode 100644
index 00000000..e8b8d268
--- /dev/null
+++ b/lib/Haskell/Law/Ord/Unit.agda
@@ -0,0 +1,23 @@
+module Haskell.Law.Ord.Unit where
+
+open import Haskell.Prim
+open import Haskell.Prim.Ord
+
+open import Haskell.Law.Ord.Def
+open import Haskell.Law.Eq.Instances
+
+instance
+  iLawfulOrdUnit : IsLawfulOrd ⊤
+
+  iLawfulOrdUnit .comparability _ _ = refl
+  iLawfulOrdUnit .transitivity _ _ _ _ = refl
+  iLawfulOrdUnit .reflexivity _ = refl
+  iLawfulOrdUnit .antisymmetry _ _ _ = refl
+  iLawfulOrdUnit .lte2gte _ _ = refl
+  iLawfulOrdUnit .lt2LteNeq _ _ = refl
+  iLawfulOrdUnit .lt2gt _ _ = refl
+  iLawfulOrdUnit .compareLt _ _ = refl
+  iLawfulOrdUnit .compareGt _ _ = refl
+  iLawfulOrdUnit .compareEq _ _ = refl
+  iLawfulOrdUnit .min2if _ _ = refl
+  iLawfulOrdUnit .max2if _ _ = refl