Generalize lemmas about if

agda · Sep 20, 2024 · be3c6d2 · be3c6d2
1 parent 078622c
commit be3c6d2
Show file tree

Hide file tree

Showing 2 changed files with 15 additions and 5 deletions.
diff --git 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
@@ -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)