From b606bab48b4bd615d353904146ece8bb5b9bf610 Mon Sep 17 00:00:00 2001
From: pmbittner <paul.bittner@uni-ulm.de>
Date: Wed, 25 Jun 2025 13:08:19 +0200
Subject: [PATCH 01/12] [add]: lemmata for if_then_else_

---
 src/Data/Bool/Properties.agda | 44 +++++++++++++++++++++++++++++++++++
 1 file changed, 44 insertions(+)

diff --git a/src/Data/Bool/Properties.agda b/src/Data/Bool/Properties.agda
index 9ebc0291ae..a1c0786259 100644
--- a/src/Data/Bool/Properties.agda
+++ b/src/Data/Bool/Properties.agda
@@ -745,6 +745,50 @@ if-float : ∀ (f : A → B) b {x y} →
 if-float _ true  = refl
 if-float _ false = refl
 
+if-eta : ∀ b {x : A} →
+         (if b then x else x) ≡ x
+if-eta false = refl
+if-eta true  = refl
+
+if-swap : ∀ b c {x y : A} →
+          (if b then x else (if c then x else y)) ≡ (if c then x else (if b then x else y))
+if-swap false _     = refl
+if-swap true  false = refl
+if-swap true  true  = refl
+
+if-not : ∀ b {x y : A} →
+         (if not b then x else y) ≡ (if b then y else x)
+if-not false = refl
+if-not true  = refl
+
+if-∧ : ∀ b {c} {x y : A} →
+       (if b ∧ c then x else y) ≡ (if b then (if c then x else y) else y)
+if-∧ false = refl
+if-∧ true  = refl
+
+if-∨ : ∀ b {c} {x y : A} →
+       (if b ∨ c then x else y) ≡ (if b then x else (if c then x else y))
+if-∨ false = refl
+if-∨ true  = refl
+
+if-xor : ∀ b {c} {x y : A} →
+         (if b xor c then x else y) ≡ (if b then (if c then y else x) else (if c then x else y))
+if-xor false = refl
+if-xor true {false} = refl
+if-xor true {true } = refl
+
+if-congˡ : ∀ b {x y z : A} → x ≡ z →
+           (if b then x else y) ≡ (if b then z else y)
+if-congˡ _ refl = refl
+
+if-congʳ : ∀ b {x y z : A} → y ≡ z →
+           (if b then x else y) ≡ (if b then x else z)
+if-congʳ _ refl = refl
+
+if-cong : ∀ b {x y z w : A} → x ≡ z → y ≡ w →
+          (if b then x else y) ≡ (if b then z else w)
+if-cong _ refl refl = refl
+
 ------------------------------------------------------------------------
 -- Properties of T
 

From e84b61402b878816a3b1cfedd1a963bd30b33cf8 Mon Sep 17 00:00:00 2001
From: pmbittner <paul.bittner@uni-ulm.de>
Date: Wed, 25 Jun 2025 13:08:31 +0200
Subject: [PATCH 02/12] [changelog]: lemmata for if_then_else_

---
 CHANGELOG.md | 13 +++++++++++++
 1 file changed, 13 insertions(+)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 14e75e9ca5..eb7f74f02b 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -239,6 +239,19 @@ Additions to existing modules
   ∙-cong-∣ : x ∣ y → a ∣ b → x ∙ a ∣ y ∙ b
   ```
 
+* In `Data.Bool.Properties`:
+  ```agda
+  if-eta : ∀ b → (if b then x else x) ≡ x
+  if-swap : ∀ b c → (if b then x else (if c then x else y)) ≡ (if c then x else (if b then x else y))
+  if-not : ∀ b → (if not b then x else y) ≡ (if b then y else x)
+  if-∧ : ∀ b → (if b ∧ c then x else y) ≡ (if b then (if c then x else y) else y)
+  if-∨ : ∀ b → (if b ∨ c then x else y) ≡ (if b then x else (if c then x else y))
+  if-xor : ∀ b → (if b xor c then x else y) ≡ (if b then (if c then y else x) else (if c then x else y))
+  if-congˡ : ∀ b → x ≡ z → (if b then x else y) ≡ (if b then z else y)
+  if-congʳ : ∀ b → y ≡ z → (if b then x else y) ≡ (if b then x else z)
+  if-cong : ∀ b → x ≡ z → y ≡ w → (if b then x else y) ≡ (if b then z else w)
+  ```
+
 * In `Data.Fin.Base`:
   ```agda
   _≰_ : Rel (Fin n) 0ℓ

From 38d1e89e719b598b1a9065196883ef645fa7d00b Mon Sep 17 00:00:00 2001
From: pmbittner <paul.bittner@uni-ulm.de>
Date: Thu, 26 Jun 2025 08:33:23 +0200
Subject: [PATCH 03/12] [refactor]: rename if-swap to if-swap-else

---
 src/Data/Bool/Properties.agda | 11 ++++++-----
 1 file changed, 6 insertions(+), 5 deletions(-)

diff --git a/src/Data/Bool/Properties.agda b/src/Data/Bool/Properties.agda
index a1c0786259..3cd6c6ae8f 100644
--- a/src/Data/Bool/Properties.agda
+++ b/src/Data/Bool/Properties.agda
@@ -750,11 +750,12 @@ if-eta : ∀ b {x : A} →
 if-eta false = refl
 if-eta true  = refl
 
-if-swap : ∀ b c {x y : A} →
-          (if b then x else (if c then x else y)) ≡ (if c then x else (if b then x else y))
-if-swap false _     = refl
-if-swap true  false = refl
-if-swap true  true  = refl
+if-swap-else : ∀ b c {x y : A} →
+          (if b then x else (if c then x else y))
+        ≡ (if c then x else (if b then x else y))
+if-swap-else false _     = refl
+if-swap-else true  false = refl
+if-swap-else true  true  = refl
 
 if-not : ∀ b {x y : A} →
          (if not b then x else y) ≡ (if b then y else x)

From 871d0db861153d1eceea0541b0bc173440a99bcf Mon Sep 17 00:00:00 2001
From: pmbittner <paul.bittner@uni-ulm.de>
Date: Thu, 26 Jun 2025 08:33:49 +0200
Subject: [PATCH 04/12] [changelog]: rename if-swap to if-swap-else

---
 CHANGELOG.md | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index eb7f74f02b..06467fd1ef 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -242,7 +242,7 @@ Additions to existing modules
 * In `Data.Bool.Properties`:
   ```agda
   if-eta : ∀ b → (if b then x else x) ≡ x
-  if-swap : ∀ b c → (if b then x else (if c then x else y)) ≡ (if c then x else (if b then x else y))
+  if-swap-else : ∀ b c → (if b then x else (if c then x else y)) ≡ (if c then x else (if b then x else y))
   if-not : ∀ b → (if not b then x else y) ≡ (if b then y else x)
   if-∧ : ∀ b → (if b ∧ c then x else y) ≡ (if b then (if c then x else y) else y)
   if-∨ : ∀ b → (if b ∨ c then x else y) ≡ (if b then x else (if c then x else y))

From 653f6a1945f34db86188bc37827f9158a5f26f3c Mon Sep 17 00:00:00 2001
From: pmbittner <paul.bittner@uni-ulm.de>
Date: Thu, 26 Jun 2025 08:34:06 +0200
Subject: [PATCH 05/12] [add]: Data.Bool.Properties.if-swap-then

---
 src/Data/Bool/Properties.agda | 7 +++++++
 1 file changed, 7 insertions(+)

diff --git a/src/Data/Bool/Properties.agda b/src/Data/Bool/Properties.agda
index 3cd6c6ae8f..0f4992decd 100644
--- a/src/Data/Bool/Properties.agda
+++ b/src/Data/Bool/Properties.agda
@@ -750,6 +750,13 @@ if-eta : ∀ b {x : A} →
 if-eta false = refl
 if-eta true  = refl
 
+if-swap-then : ∀ b c {x y : A} →
+          (if b then (if c then x else y) else y)
+        ≡ (if c then (if b then x else y) else y)
+if-swap-then false false = refl
+if-swap-then false true  = refl
+if-swap-then true  _     = refl
+
 if-swap-else : ∀ b c {x y : A} →
           (if b then x else (if c then x else y))
         ≡ (if c then x else (if b then x else y))

From 08c80f60f556f1c410305b96c6dd530c3f7a72a8 Mon Sep 17 00:00:00 2001
From: pmbittner <paul.bittner@uni-ulm.de>
Date: Thu, 26 Jun 2025 08:34:20 +0200
Subject: [PATCH 06/12] [add]: Data.Bool.Properties.if-swap-then

---
 CHANGELOG.md | 1 +
 1 file changed, 1 insertion(+)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 06467fd1ef..725239c351 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -242,6 +242,7 @@ Additions to existing modules
 * In `Data.Bool.Properties`:
   ```agda
   if-eta : ∀ b → (if b then x else x) ≡ x
+  if-swap-then : ∀ b c → (if b then (if c then x else y) else y) ≡ (if c then (if b then x else y) else y)
   if-swap-else : ∀ b c → (if b then x else (if c then x else y)) ≡ (if c then x else (if b then x else y))
   if-not : ∀ b → (if not b then x else y) ≡ (if b then y else x)
   if-∧ : ∀ b → (if b ∧ c then x else y) ≡ (if b then (if c then x else y) else y)

From 35e753139a789687a8f81b19ac3ead45c384968c Mon Sep 17 00:00:00 2001
From: pmbittner <paul.bittner@uni-ulm.de>
Date: Thu, 26 Jun 2025 08:35:54 +0200
Subject: [PATCH 07/12] [add]: if-idem-then + if-idem-else

---
 src/Data/Bool/Properties.agda | 10 ++++++++++
 1 file changed, 10 insertions(+)

diff --git a/src/Data/Bool/Properties.agda b/src/Data/Bool/Properties.agda
index 0f4992decd..aa26fe8dc0 100644
--- a/src/Data/Bool/Properties.agda
+++ b/src/Data/Bool/Properties.agda
@@ -750,6 +750,16 @@ if-eta : ∀ b {x : A} →
 if-eta false = refl
 if-eta true  = refl
 
+if-idem-then : ∀ b {x y : A} →
+               (if b then (if b then x else y) else y) ≡ (if b then x else y)
+if-idem-then false = refl
+if-idem-then true  = refl
+
+if-idem-else : ∀ b {x y : A} →
+               (if b then x else (if b then x else y)) ≡ (if b then x else y)
+if-idem-else false = refl
+if-idem-else true  = refl
+
 if-swap-then : ∀ b c {x y : A} →
           (if b then (if c then x else y) else y)
         ≡ (if c then (if b then x else y) else y)

From 9cf7e865f00aceade59f05b153b30a87633b997b Mon Sep 17 00:00:00 2001
From: pmbittner <paul.bittner@uni-ulm.de>
Date: Thu, 26 Jun 2025 08:36:03 +0200
Subject: [PATCH 08/12] [changelog]: if-idem-then + if-idem-else

---
 CHANGELOG.md | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 725239c351..6a2233b290 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -242,6 +242,8 @@ Additions to existing modules
 * In `Data.Bool.Properties`:
   ```agda
   if-eta : ∀ b → (if b then x else x) ≡ x
+  if-idem-then : ∀ b → (if b then (if b then x else y) else y) ≡ (if b then x else y)
+  if-idem-else : ∀ b → (if b then x else (if b then x else y)) ≡ (if b then x else y)
   if-swap-then : ∀ b c → (if b then (if c then x else y) else y) ≡ (if c then (if b then x else y) else y)
   if-swap-else : ∀ b c → (if b then x else (if c then x else y)) ≡ (if c then x else (if b then x else y))
   if-not : ∀ b → (if not b then x else y) ≡ (if b then y else x)

From fcf6e447b66cfacd2b8407d1d63f64e2e04bde6c Mon Sep 17 00:00:00 2001
From: pmbittner <paul.bittner@uni-ulm.de>
Date: Thu, 26 Jun 2025 08:41:59 +0200
Subject: [PATCH 09/12] rename and extend if-cong lemmata

---
 CHANGELOG.md                  |  7 ++++---
 src/Data/Bool/Properties.agda | 22 +++++++++++++---------
 2 files changed, 17 insertions(+), 12 deletions(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 6a2233b290..af851dd415 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -250,9 +250,10 @@ Additions to existing modules
   if-∧ : ∀ b → (if b ∧ c then x else y) ≡ (if b then (if c then x else y) else y)
   if-∨ : ∀ b → (if b ∨ c then x else y) ≡ (if b then x else (if c then x else y))
   if-xor : ∀ b → (if b xor c then x else y) ≡ (if b then (if c then y else x) else (if c then x else y))
-  if-congˡ : ∀ b → x ≡ z → (if b then x else y) ≡ (if b then z else y)
-  if-congʳ : ∀ b → y ≡ z → (if b then x else y) ≡ (if b then x else z)
-  if-cong : ∀ b → x ≡ z → y ≡ w → (if b then x else y) ≡ (if b then z else w)
+  if-cong : b ≡ c → (if b then x else y) ≡ (if c then x else y)
+  if-cong-then : ∀ b → x ≡ z → (if b then x else y) ≡ (if b then z else y)
+  if-cong-else : ∀ b → y ≡ z → (if b then x else y) ≡ (if b then x else z)
+  if-cong₂ : ∀ b → x ≡ z → y ≡ w → (if b then x else y) ≡ (if b then z else w)
   ```
 
 * In `Data.Fin.Base`:
diff --git a/src/Data/Bool/Properties.agda b/src/Data/Bool/Properties.agda
index aa26fe8dc0..b9d94ce342 100644
--- a/src/Data/Bool/Properties.agda
+++ b/src/Data/Bool/Properties.agda
@@ -795,17 +795,21 @@ if-xor false = refl
 if-xor true {false} = refl
 if-xor true {true } = refl
 
-if-congˡ : ∀ b {x y z : A} → x ≡ z →
-           (if b then x else y) ≡ (if b then z else y)
-if-congˡ _ refl = refl
+if-cong : ∀ {b c} {x y : A} → b ≡ c →
+               (if b then x else y) ≡ (if c then x else y)
+if-cong refl = refl
 
-if-congʳ : ∀ b {x y z : A} → y ≡ z →
-           (if b then x else y) ≡ (if b then x else z)
-if-congʳ _ refl = refl
+if-cong-then : ∀ b {x y z : A} → x ≡ z →
+               (if b then x else y) ≡ (if b then z else y)
+if-cong-then _ refl = refl
 
-if-cong : ∀ b {x y z w : A} → x ≡ z → y ≡ w →
-          (if b then x else y) ≡ (if b then z else w)
-if-cong _ refl refl = refl
+if-cong-else : ∀ b {x y z : A} → y ≡ z →
+               (if b then x else y) ≡ (if b then x else z)
+if-cong-else _ refl = refl
+
+if-cong₂ : ∀ b {x y z w : A} → x ≡ z → y ≡ w →
+           (if b then x else y) ≡ (if b then z else w)
+if-cong₂ _ refl refl = refl
 
 ------------------------------------------------------------------------
 -- Properties of T

From 038d64160b57edddb79d35beb9277691012df514 Mon Sep 17 00:00:00 2001
From: pmbittner <paul.bittner@uni-ulm.de>
Date: Wed, 2 Jul 2025 10:31:59 +0200
Subject: [PATCH 10/12] [refactor]: fix indentation of if-cong

---
 src/Data/Bool/Properties.agda | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/Data/Bool/Properties.agda b/src/Data/Bool/Properties.agda
index b9d94ce342..6cdeb694c1 100644
--- a/src/Data/Bool/Properties.agda
+++ b/src/Data/Bool/Properties.agda
@@ -796,7 +796,7 @@ if-xor true {false} = refl
 if-xor true {true } = refl
 
 if-cong : ∀ {b c} {x y : A} → b ≡ c →
-               (if b then x else y) ≡ (if c then x else y)
+          (if b then x else y) ≡ (if c then x else y)
 if-cong refl = refl
 
 if-cong-then : ∀ b {x y z : A} → x ≡ z →

From 3eb32c383344b4bdf6bee1a567e35075f539db2d Mon Sep 17 00:00:00 2001
From: pmbittner <paul.bittner@uni-ulm.de>
Date: Wed, 2 Jul 2025 10:43:22 +0200
Subject: [PATCH 11/12] [docs]: Reasoning behind if-cong lemmas

---
 src/Data/Bool/Properties.agda | 12 ++++++++++++
 1 file changed, 12 insertions(+)

diff --git a/src/Data/Bool/Properties.agda b/src/Data/Bool/Properties.agda
index 6cdeb694c1..14cb241daf 100644
--- a/src/Data/Bool/Properties.agda
+++ b/src/Data/Bool/Properties.agda
@@ -795,6 +795,18 @@ if-xor false = refl
 if-xor true {false} = refl
 if-xor true {true } = refl
 
+-- The following congruence lemmas are short hands for
+--   cong (if_then x else y)
+--   cong (if b then_else y)
+--   cong (if b then x else_)
+--   cong (if b then_else_)
+-- on the different sub-terms in an if_then_else_ expression.
+-- With these short hands, the branches x and y can be inferred
+-- automatically (i.e., they are implicit arguments) whereas
+-- the branches have to be spelled out explicitly when using cong.
+-- (Using underscores as in "cong (if b then _ else_)"
+-- unfortunately fails to resolve the omitted argument.)
+
 if-cong : ∀ {b c} {x y : A} → b ≡ c →
           (if b then x else y) ≡ (if c then x else y)
 if-cong refl = refl

From 0d55cb9c7c9fb79378082f295c7a487a0d92d1ed Mon Sep 17 00:00:00 2001
From: pmbittner <paul.bittner@uni-ulm.de>
Date: Wed, 2 Jul 2025 10:44:44 +0200
Subject: [PATCH 12/12] [refactor]: add line breaks to some if-lemmas

This (1) follows the style guide of having a line length limit of 72
characters and (2) increases readability because it enables
immediately seeing which sub-terms of an if_then_else_ expression
are substituted.
---
 src/Data/Bool/Properties.agda | 21 ++++++++++++++-------
 1 file changed, 14 insertions(+), 7 deletions(-)

diff --git a/src/Data/Bool/Properties.agda b/src/Data/Bool/Properties.agda
index 14cb241daf..90fdecadde 100644
--- a/src/Data/Bool/Properties.agda
+++ b/src/Data/Bool/Properties.agda
@@ -751,12 +751,14 @@ if-eta false = refl
 if-eta true  = refl
 
 if-idem-then : ∀ b {x y : A} →
-               (if b then (if b then x else y) else y) ≡ (if b then x else y)
+               (if b then (if b then x else y) else y)
+             ≡ (if b then x                    else y)
 if-idem-then false = refl
 if-idem-then true  = refl
 
 if-idem-else : ∀ b {x y : A} →
-               (if b then x else (if b then x else y)) ≡ (if b then x else y)
+               (if b then x else (if b then x else y))
+             ≡ (if b then x else y)
 if-idem-else false = refl
 if-idem-else true  = refl
 
@@ -790,7 +792,8 @@ if-∨ false = refl
 if-∨ true  = refl
 
 if-xor : ∀ b {c} {x y : A} →
-         (if b xor c then x else y) ≡ (if b then (if c then y else x) else (if c then x else y))
+         (if b xor c then x else y)
+       ≡ (if b then (if c then y else x) else (if c then x else y))
 if-xor false = refl
 if-xor true {false} = refl
 if-xor true {true } = refl
@@ -808,19 +811,23 @@ if-xor true {true } = refl
 -- unfortunately fails to resolve the omitted argument.)
 
 if-cong : ∀ {b c} {x y : A} → b ≡ c →
-          (if b then x else y) ≡ (if c then x else y)
+          (if b then x else y)
+        ≡ (if c then x else y)
 if-cong refl = refl
 
 if-cong-then : ∀ b {x y z : A} → x ≡ z →
-               (if b then x else y) ≡ (if b then z else y)
+               (if b then x else y)
+             ≡ (if b then z else y)
 if-cong-then _ refl = refl
 
 if-cong-else : ∀ b {x y z : A} → y ≡ z →
-               (if b then x else y) ≡ (if b then x else z)
+               (if b then x else y)
+             ≡ (if b then x else z)
 if-cong-else _ refl = refl
 
 if-cong₂ : ∀ b {x y z w : A} → x ≡ z → y ≡ w →
-           (if b then x else y) ≡ (if b then z else w)
+           (if b then x else y)
+         ≡ (if b then z else w)
 if-cong₂ _ refl refl = refl
 
 ------------------------------------------------------------------------