From b826881b59d4ff71e51ab215798dbf71e238b025 Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Sat, 2 Aug 2025 18:01:26 +0100
Subject: [PATCH 1/3] [ add ] clean version of
 `Data.Fin.Properties.searchMinimalCounterexample`

---
 CHANGELOG.md                 | 21 ++++++++++++
 src/Data/Fin/Properties.agda | 64 +++++++++++++++++++++++++++++++-----
 2 files changed, 76 insertions(+), 9 deletions(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index ef9533efc6..d6b1a555f0 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -70,6 +70,27 @@ Additions to existing modules
   ≟-≡          : (eq : i ≡ j) → (i ≟ j) ≡ yes eq
   ≟-≡-refl     : (i : Fin n) → (i ≟ i) ≡ yes refl
   ≟-≢          : (i≢j : i ≢ j) → (i ≟ j) ≡ no i≢j
+  inject-< : inject j < i
+
+  record MinimalExample (P : Pred (Fin n) p) : Set p where
+    constructor μ
+    field
+      witness : Fin n
+      example : P witness
+      minimal : ∀ {j} → .(j < witness) → ¬ P j
+
+  record MinimalCounterexample (P : Pred (Fin n) p) : Set p where
+    constructor μ
+    field
+      witness : Fin n
+      .contra : ¬ P witness
+      minimal : ∀ {j} → .(j < witness) → P j
+
+  μ⟨_⟩  : Pred (Fin n) p → Set p
+  μ⟨¬_⟩ : Pred (Fin n) p → Set p
+  ¬¬μ⇒μ : Decidable P → μ⟨¬ ∁ P ⟩ → μ⟨ P ⟩
+  searchMinimalCounterexample : Decidable P → (∀ i → P i) ⊎ μ⟨¬ P ⟩
+  search-μ⟨¬_⟩                : Decidable P → (∀ i → P i) ⊎ μ⟨¬ P ⟩
   ```
 
 * In `Data.Nat.Properties`:
diff --git a/src/Data/Fin/Properties.agda b/src/Data/Fin/Properties.agda
index 48bcf8a5ee..335929a945 100644
--- a/src/Data/Fin/Properties.agda
+++ b/src/Data/Fin/Properties.agda
@@ -48,16 +48,17 @@ open import Relation.Binary.PropositionalEquality.Properties as ≡
 open import Relation.Binary.PropositionalEquality as ≡
   using (≡-≟-identity; ≢-≟-identity)
 open import Relation.Nullary.Decidable as Dec
-  using (Dec; _because_; yes; no; _×-dec_; _⊎-dec_; map′)
+  using (Dec; _because_; yes; no; _×-dec_; _⊎-dec_; map′; decidable-stable)
 open import Relation.Nullary.Negation.Core using (¬_; contradiction)
+open import Relation.Nullary.Recomputable using (¬-recompute)
 open import Relation.Nullary.Reflects using (invert)
 open import Relation.Unary as U
-  using (U; Pred; Decidable; _⊆_; Satisfiable; Universal)
+  using (U; Pred; Decidable; _⊆_; ∁; Satisfiable; Universal)
 open import Relation.Unary.Properties using (U?)
 
 private
   variable
-    a : Level
+    a p q : Level
     A : Set a
     m n o : ℕ
     i j : Fin n
@@ -469,6 +470,10 @@ toℕ-inject : ∀ {i : Fin n} (j : Fin′ i) → toℕ (inject j) ≡ toℕ j
 toℕ-inject {i = suc i} zero    = refl
 toℕ-inject {i = suc i} (suc j) = cong suc (toℕ-inject j)
 
+inject-< : ∀ {i : Fin n} (j : Fin′ i) → inject j < i
+inject-< {i = suc i} zero    = z<s
+inject-< {i = suc i} (suc j) = s<s (inject-< j)
+
 ------------------------------------------------------------------------
 -- inject₁
 ------------------------------------------------------------------------
@@ -1048,16 +1053,57 @@ private
   note P? = Dec.does (P? 0F) ∧ Dec.does (P? 1F) ∧ Dec.does (P? 2F) ∧ true
           , refl
 
--- If a decidable predicate P over a finite set is sometimes false,
--- then we can find the smallest value for which this is the case.
+------------------------------------------------------------------------
+-- A decidable predicate P over a finite set is either always true,
+-- or else we can find the smallest value for which P is false.
+
+module _ (P : Pred (Fin n) p) where
+
+  record MinimalCounterexample : Set p where
+    constructor μ
+    field
+      witness : Fin n
+      .contra : ¬ P witness
+      minimal : ∀ {j} → .(j < witness) → P j
+
+  record MinimalExample : Set p where
+    constructor μ
+    field
+      witness : Fin n
+      example : P witness
+      minimal : ∀ {j} → .(j < witness) → ¬ P j
+
+μ⟨_⟩ : Pred (Fin n) p → Set p
+μ⟨_⟩ = MinimalExample
+
+μ⟨¬_⟩ : Pred (Fin n) p → Set p
+μ⟨¬_⟩ = MinimalCounterexample
+
+¬¬μ⇒μ : ∀ {P : Pred (Fin n) p} → Decidable P → μ⟨¬ ∁ P ⟩ → μ⟨ P ⟩
+¬¬μ⇒μ P? (μ i ¬¬pᵢ ∀[j<i]) = μ i (decidable-stable (P? i) (¬-recompute ¬¬pᵢ)) ∀[j<i]
+
+searchMinimalCounterexample : ∀ {P : Pred (Fin n) p} → Decidable P → (∀ i → P i) ⊎ μ⟨¬ P ⟩
+searchMinimalCounterexample {zero}  {P = _} P? = inj₁ λ()
+searchMinimalCounterexample {suc _} {P = P} P? with P? zero
+... | no ¬p₀ = inj₂ (μ zero ¬p₀ λ())
+... | yes p₀ = Sum.map (∀-cons p₀) μ⁺ (searchMinimalCounterexample (P? ∘ suc))
+  where
+  μ⁺ : μ⟨¬ P ∘ suc ⟩ → μ⟨¬ P ⟩
+  μ⁺ (μ i ¬pₛᵢ ∀[j<i]P) = μ (suc i) ¬pₛᵢ
+    λ where
+      {zero}  _     → p₀
+      {suc _} sj<si → ∀[j<i]P (ℕ.s<s⁻¹ sj<si)
+
+search-μ⟨¬_⟩ : ∀ {P : Pred (Fin n) p} → Decidable P → (∀ i → P i) ⊎ μ⟨¬ P ⟩
+search-μ⟨¬_⟩ = searchMinimalCounterexample
 
 ¬∀⟶∃¬-smallest : ∀ n {p} (P : Pred (Fin n) p) → Decidable P →
                  ¬ (∀ i → P i) → ∃ λ i → ¬ P i × ((j : Fin′ i) → P (inject j))
 ¬∀⟶∃¬-smallest zero    P P? ¬∀P = contradiction (λ()) ¬∀P
-¬∀⟶∃¬-smallest (suc n) P P? ¬∀P with P? zero
-... | false because [¬P₀] = (zero , invert [¬P₀] , λ ())
-... | true  because  [P₀] = map suc (map id (∀-cons (invert [P₀])))
-  (¬∀⟶∃¬-smallest n (P ∘ suc) (P? ∘ suc) (¬∀P ∘ (∀-cons (invert [P₀]))))
+¬∀⟶∃¬-smallest (suc n) P P? ¬∀P = [ flip contradiction ¬∀P , lemma ] $ search-μ⟨¬ P? ⟩
+  where
+  lemma : μ⟨¬ P ⟩ → ∃ λ i → ¬ P i × ((j : Fin′ i) → P (inject j))
+  lemma (μ i ¬pᵢ ∀[j<i]P) = i , ¬-recompute ¬pᵢ , λ j → ∀[j<i]P (inject-< j)
 
 -- When P is a decidable predicate over a finite set the following
 -- lemma can be proved.

From b19cf454d80b5f7daa67908d8a402ad3eb3098f7 Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Tue, 5 Aug 2025 13:28:15 +0100
Subject: [PATCH 2/3] =?UTF-8?q?use:=20`=CE=A0[=5F]`=20syntax?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 CHANGELOG.md                 | 4 ++--
 src/Data/Fin/Properties.agda | 4 ++--
 2 files changed, 4 insertions(+), 4 deletions(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index d6b1a555f0..b33ff71a91 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -89,8 +89,8 @@ Additions to existing modules
   μ⟨_⟩  : Pred (Fin n) p → Set p
   μ⟨¬_⟩ : Pred (Fin n) p → Set p
   ¬¬μ⇒μ : Decidable P → μ⟨¬ ∁ P ⟩ → μ⟨ P ⟩
-  searchMinimalCounterexample : Decidable P → (∀ i → P i) ⊎ μ⟨¬ P ⟩
-  search-μ⟨¬_⟩                : Decidable P → (∀ i → P i) ⊎ μ⟨¬ P ⟩
+  searchMinimalCounterexample : Decidable P → Π[ P ] ⊎ μ⟨¬ P ⟩
+  search-μ⟨¬_⟩                : Decidable P → Π[ P ] ⊎ μ⟨¬ P ⟩
   ```
 
 * In `Data.Nat.Properties`:
diff --git a/src/Data/Fin/Properties.agda b/src/Data/Fin/Properties.agda
index 335929a945..d8bbf76ba1 100644
--- a/src/Data/Fin/Properties.agda
+++ b/src/Data/Fin/Properties.agda
@@ -1082,7 +1082,7 @@ module _ (P : Pred (Fin n) p) where
 ¬¬μ⇒μ : ∀ {P : Pred (Fin n) p} → Decidable P → μ⟨¬ ∁ P ⟩ → μ⟨ P ⟩
 ¬¬μ⇒μ P? (μ i ¬¬pᵢ ∀[j<i]) = μ i (decidable-stable (P? i) (¬-recompute ¬¬pᵢ)) ∀[j<i]
 
-searchMinimalCounterexample : ∀ {P : Pred (Fin n) p} → Decidable P → (∀ i → P i) ⊎ μ⟨¬ P ⟩
+searchMinimalCounterexample : ∀ {P : Pred (Fin n) p} → Decidable P → Π[ P ] ⊎ μ⟨¬ P ⟩
 searchMinimalCounterexample {zero}  {P = _} P? = inj₁ λ()
 searchMinimalCounterexample {suc _} {P = P} P? with P? zero
 ... | no ¬p₀ = inj₂ (μ zero ¬p₀ λ())
@@ -1094,7 +1094,7 @@ searchMinimalCounterexample {suc _} {P = P} P? with P? zero
       {zero}  _     → p₀
       {suc _} sj<si → ∀[j<i]P (ℕ.s<s⁻¹ sj<si)
 
-search-μ⟨¬_⟩ : ∀ {P : Pred (Fin n) p} → Decidable P → (∀ i → P i) ⊎ μ⟨¬ P ⟩
+search-μ⟨¬_⟩ : ∀ {P : Pred (Fin n) p} → Decidable P → Π[ P ] ⊎ μ⟨¬ P ⟩
 search-μ⟨¬_⟩ = searchMinimalCounterexample
 
 ¬∀⟶∃¬-smallest : ∀ n {p} (P : Pred (Fin n) p) → Decidable P →

From 3e04ff46d35f70272c1d4f84bec9615581d50b3e Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Sat, 4 Oct 2025 11:28:11 +0100
Subject: [PATCH 3/3] refactor: simplify

---
 CHANGELOG.md                 | 15 +++++-------
 src/Data/Fin/Properties.agda | 44 ++++++++++++++++--------------------
 2 files changed, 25 insertions(+), 34 deletions(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index c901f367e1..21d17f71ad 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -73,27 +73,24 @@ Additions to existing modules
   ≟-≡          : (eq : i ≡ j) → (i ≟ j) ≡ yes eq
   ≟-≡-refl     : (i : Fin n) → (i ≟ i) ≡ yes refl
   ≟-≢          : (i≢j : i ≢ j) → (i ≟ j) ≡ no i≢j
-  inject-< : inject j < i
+  inject-<     : inject j < i
 
-  record MinimalExample (P : Pred (Fin n) p) : Set p where
-    constructor μ
+  record Least⟨_⟩ (P : Pred (Fin n) p) : Set p where
+    constructor least
     field
       witness : Fin n
       example : P witness
       minimal : ∀ {j} → .(j < witness) → ¬ P j
 
-  record MinimalCounterexample (P : Pred (Fin n) p) : Set p where
+  record Least⟨¬_⟩ (P : Pred (Fin n) p) : Set p where
     constructor μ
     field
       witness : Fin n
       .contra : ¬ P witness
       minimal : ∀ {j} → .(j < witness) → P j
 
-  μ⟨_⟩  : Pred (Fin n) p → Set p
-  μ⟨¬_⟩ : Pred (Fin n) p → Set p
-  ¬¬μ⇒μ : Decidable P → μ⟨¬ ∁ P ⟩ → μ⟨ P ⟩
-  searchMinimalCounterexample : Decidable P → Π[ P ] ⊎ μ⟨¬ P ⟩
-  search-μ⟨¬_⟩                : Decidable P → Π[ P ] ⊎ μ⟨¬ P ⟩
+  search-least⟨¬_⟩ : Decidable P → Π[ P ] ⊎ Least⟨¬ P ⟩
+  ¬¬least⇒least    : Decidable P → Least⟨¬ ∁ P ⟩ → Least⟨ P ⟩
   ```
 
 * In `Data.Nat.ListAction.Properties`
diff --git a/src/Data/Fin/Properties.agda b/src/Data/Fin/Properties.agda
index 57a0816fcc..9366a0a09a 100644
--- a/src/Data/Fin/Properties.agda
+++ b/src/Data/Fin/Properties.agda
@@ -1060,51 +1060,45 @@ private
 
 module _ (P : Pred (Fin n) p) where
 
-  record MinimalCounterexample : Set p where
-    constructor μ
+  record Least⟨¬_⟩ : Set p where
+    constructor least
     field
       witness : Fin n
       .contra : ¬ P witness
       minimal : ∀ {j} → .(j < witness) → P j
 
-  record MinimalExample : Set p where
-    constructor μ
+  record Least⟨_⟩ : Set p where
+    constructor least
     field
       witness : Fin n
       example : P witness
       minimal : ∀ {j} → .(j < witness) → ¬ P j
 
-μ⟨_⟩ : Pred (Fin n) p → Set p
-μ⟨_⟩ = MinimalExample
-
-μ⟨¬_⟩ : Pred (Fin n) p → Set p
-μ⟨¬_⟩ = MinimalCounterexample
-
-¬¬μ⇒μ : ∀ {P : Pred (Fin n) p} → Decidable P → μ⟨¬ ∁ P ⟩ → μ⟨ P ⟩
-¬¬μ⇒μ P? (μ i ¬¬pᵢ ∀[j<i]) = μ i (decidable-stable (P? i) (¬-recompute ¬¬pᵢ)) ∀[j<i]
-
-searchMinimalCounterexample : ∀ {P : Pred (Fin n) p} → Decidable P → Π[ P ] ⊎ μ⟨¬ P ⟩
-searchMinimalCounterexample {zero}  {P = _} P? = inj₁ λ()
-searchMinimalCounterexample {suc _} {P = P} P? with P? zero
-... | no ¬p₀ = inj₂ (μ zero ¬p₀ λ())
-... | yes p₀ = Sum.map (∀-cons p₀) μ⁺ (searchMinimalCounterexample (P? ∘ suc))
+search-least⟨¬_⟩ : ∀ {P : Pred (Fin n) p} → Decidable P → Π[ P ] ⊎ Least⟨¬ P ⟩
+search-least⟨¬_⟩ {n = zero}  {P = _} P? = inj₁ λ()
+search-least⟨¬_⟩ {n = suc _} {P = P} P? with P? zero
+... | no ¬p₀ = inj₂ (least zero ¬p₀ λ())
+... | yes p₀ = Sum.map (∀-cons p₀) least⁺ search-least⟨¬ P? ∘ suc ⟩
   where
-  μ⁺ : μ⟨¬ P ∘ suc ⟩ → μ⟨¬ P ⟩
-  μ⁺ (μ i ¬pₛᵢ ∀[j<i]P) = μ (suc i) ¬pₛᵢ
+  least⁺ : Least⟨¬ P ∘ suc ⟩ → Least⟨¬ P ⟩
+  least⁺ (least i ¬pₛᵢ ∀[j<i]P) = least (suc i) ¬pₛᵢ
     λ where
       {zero}  _     → p₀
       {suc _} sj<si → ∀[j<i]P (ℕ.s<s⁻¹ sj<si)
 
-search-μ⟨¬_⟩ : ∀ {P : Pred (Fin n) p} → Decidable P → Π[ P ] ⊎ μ⟨¬ P ⟩
-search-μ⟨¬_⟩ = searchMinimalCounterexample
+module _ {P : Pred (Fin n) p} (P? : Decidable P) where
+
+  ¬¬least⇒least : Least⟨¬ ∁ P ⟩ → Least⟨ P ⟩
+  ¬¬least⇒least (least i ¬¬pᵢ ∀[j<i]) =
+    least i (decidable-stable (P? i) (¬-recompute ¬¬pᵢ)) ∀[j<i]
 
 ¬∀⟶∃¬-smallest : ∀ n {p} (P : Pred (Fin n) p) → Decidable P →
                  ¬ (∀ i → P i) → ∃ λ i → ¬ P i × ((j : Fin′ i) → P (inject j))
 ¬∀⟶∃¬-smallest zero    P P? ¬∀P = contradiction (λ()) ¬∀P
-¬∀⟶∃¬-smallest (suc n) P P? ¬∀P = [ flip contradiction ¬∀P , lemma ] $ search-μ⟨¬ P? ⟩
+¬∀⟶∃¬-smallest (suc n) P P? ¬∀P = [ contradiction′ ¬∀P , lemma ] $ search-least⟨¬ P? ⟩
   where
-  lemma : μ⟨¬ P ⟩ → ∃ λ i → ¬ P i × ((j : Fin′ i) → P (inject j))
-  lemma (μ i ¬pᵢ ∀[j<i]P) = i , ¬-recompute ¬pᵢ , λ j → ∀[j<i]P (inject-< j)
+  lemma : Least⟨¬ P ⟩ → ∃ λ i → ¬ P i × ((j : Fin′ i) → P (inject j))
+  lemma (least i ¬pᵢ ∀[j<i]P) = i , ¬-recompute ¬pᵢ , λ j → ∀[j<i]P (inject-< j)
 
 -- When P is a decidable predicate over a finite set the following
 -- lemma can be proved.