[ add ] clean version of Data.Fin.Properties.searchMinimalCounterexample (#2801)

* [ add ] clean version of `Data.Fin.Properties.searchMinimalCounterexample`

* use: `Π[_]` syntax

* refactor: simplify

* refactor: drastic streamlining

* refactor: remove redundant `import`

* refactor: inlined `lemma` in `¬∀⇒∃¬`

Author: jamesmckinna

CHANGELOG.md

@@ -138,6 +138,17 @@ 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 Least⟨_⟩ (P : Pred (Fin n) p) : Set p where
+    constructor least
+    field
+      witness : Fin n
+      example : P witness
+      minimal : ∀ {j} → .(j < witness) → ¬ P j
+
+  search-least⟨_⟩  : Decidable P → Π[ ∁ P ] ⊎ Least⟨ P ⟩
+  search-least⟨¬_⟩ : Decidable P → Π[ P ] ⊎ Least⟨ ∁ P ⟩
   ```
 
 * In `Data.Nat.ListAction.Properties`

src/Data/Fin/Properties.agda

@@ -48,13 +48,13 @@ 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; contradiction′)
 open import Relation.Nullary.Reflects using (invert)
 open import Relation.Unary as U
-  using (U; Pred; Decidable; _⊆_; Satisfiable; Universal)
-open import Relation.Unary.Properties using (U?)
+  using (U; Pred; Decidable; _⊆_; ∁; Satisfiable; Universal)
+open import Relation.Unary.Properties using (U?; ∁?)
 
 private
   variable
@@ -471,6 +471,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₁
 ------------------------------------------------------------------------
@@ -1036,23 +1040,47 @@ 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 false, or
+-- else we can find the least value for which P is true (and vice versa).
 
-¬∀⇒∃¬-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₀]))))
+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
+
+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
+... | yes p₀ = inj₂ (least zero p₀ λ())
+... | no ¬p₀ = Sum.map (∀-cons ¬p₀) lemma search-least⟨ P? ∘ suc ⟩
+  where
+  lemma : Least⟨ P ∘ suc ⟩ → Least⟨ P ⟩
+  lemma (least i pₛᵢ ∀[j<i]¬P) = least (suc i) pₛᵢ λ where
+    {zero}  _     → ¬p₀
+    {suc _} sj<si → ∀[j<i]¬P (ℕ.s<s⁻¹ sj<si)
+
+search-least⟨¬_⟩ : ∀ {P : Pred (Fin n) p} → Decidable P → Π[ P ] ⊎ Least⟨ ∁ P ⟩
+search-least⟨¬_⟩ {P = P} P? =
+  Sum.map₁ (λ ∀[¬¬P] j → decidable-stable (P? j) (∀[¬¬P] j)) search-least⟨ ∁? P? ⟩
 
 -- When P is a decidable predicate over a finite set the following
--- lemma can be proved.
+-- lemmas can be proved.
+
+¬∀⇒∃¬-smallest : ∀ n {p} (P : Pred (Fin n) p) → Decidable P →
+                 ¬ (∀ i → P i) → ∃ λ i → ¬ P i × ((j : Fin′ i) → P (inject j))
+¬∀⇒∃¬-smallest n P P? ¬∀P = [ contradiction′ ¬∀P , lemma ] $ search-least⟨¬ P? ⟩
+  where
+  lemma : Least⟨ ∁ P ⟩ → ∃ λ i → ¬ P i × ((j : Fin′ i) → P (inject j))
+  lemma (least i ¬pᵢ ∀[j<i]¬¬P) = i , ¬pᵢ , λ j →
+    decidable-stable (P? (inject j)) (∀[j<i]¬¬P (inject-< j))
 
 ¬∀⇒∃¬ : ∀ n {p} (P : Pred (Fin n) p) → Decidable P →
           ¬ (∀ i → P i) → (∃ λ i → ¬ P i)
-¬∀⇒∃¬ n P P? ¬P = map id proj₁ (¬∀⇒∃¬-smallest n P P? ¬P)
+¬∀⇒∃¬ n P P? ¬∀P =
+  [ contradiction′ ¬∀P , (λ (least i ¬pᵢ _) → i , ¬pᵢ) ] $ search-least⟨¬ P? ⟩
 
 -- lifting Dec over Unary subset relation