From be3c6d218fc37bcbeed543618ca563c50ff76ffc Mon Sep 17 00:00:00 2001
From: Jesper Cockx <jesper@sikanda.be>
Date: Fri, 20 Sep 2024 14:14:14 +0200
Subject: [PATCH] Generalize lemmas about if

---
 lib/Haskell/Law/Bool.agda      | 16 +++++++++++++---
 lib/Haskell/Law/Ord/Maybe.agda |  4 ++--
 2 files changed, 15 insertions(+), 5 deletions(-)

diff --git a/lib/Haskell/Law/Bool.agda b/lib/Haskell/Law/Bool.agda
index 7f8744fe..d33d5e37 100644
--- a/lib/Haskell/Law/Bool.agda
+++ b/lib/Haskell/Law/Bool.agda
@@ -65,12 +65,22 @@ not-involution .(not b) b refl = not-not b
 --------------------------------------------------
 -- if_then_else_
 
-ifFlip : ∀ (b) (t e : a) → (if b then t else e) ≡ (if not b then e else t)
+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}})
 ifFlip False _ _ = refl
 ifFlip True  _ _ = refl
 
-ifTrueEqThen : ∀ (b : Bool) {thn els : a} → b ≡ True → (if b then thn else els) ≡ thn
+ifTrueEqThen : ∀ (b : Bool)
+             → {thn : {{b ≡ True}} → a}
+             → {els : {{b ≡ False}} → a}
+             → (pf : b ≡ True) → (if b then thn else els) ≡ thn {{pf}}
 ifTrueEqThen .True refl = refl
 
-ifFalseEqElse : ∀ (b : Bool) {thn els : a} → b ≡ False → (if b then thn else els) ≡ els
+ifFalseEqElse : ∀ (b : Bool)
+             → {thn : {{b ≡ True}} → a}
+             → {els : {{b ≡ False}} → a}
+             → (pf : b ≡ False) → (if b then thn else els) ≡ els {{pf}}
 ifFalseEqElse .False refl = refl
diff --git a/lib/Haskell/Law/Ord/Maybe.agda b/lib/Haskell/Law/Ord/Maybe.agda
index 7d154461..b5af98a9 100644
--- a/lib/Haskell/Law/Ord/Maybe.agda
+++ b/lib/Haskell/Law/Ord/Maybe.agda
@@ -114,7 +114,7 @@ min2ifMaybe Nothing  Nothing  = refl
 min2ifMaybe Nothing  (Just _) = refl
 min2ifMaybe (Just _) Nothing = refl
 min2ifMaybe (Just x) (Just y)
-  rewrite ifFlip (compare x y == GT) (Just y) (Just x)
+  rewrite sym (ifFlip (compare x y == GT) (Just x) (Just y))
   = equality'
       (if (compare x y /= GT) then Just x else Just y)
       (if (compare x y /= GT) then Just x else Just y)
@@ -126,7 +126,7 @@ max2ifMaybe Nothing  Nothing  = refl
 max2ifMaybe Nothing  (Just y) = eqReflexivity y
 max2ifMaybe (Just x) Nothing  = eqReflexivity x
 max2ifMaybe (Just x) (Just y)
-  rewrite ifFlip (compare x y == LT) (Just y) (Just x)
+  rewrite sym (ifFlip (compare x y == LT) (Just x) (Just y))
   = equality'
     (if (compare x y /= LT) then Just x else Just y)
     (if (compare x y /= LT) then Just x else Just y)