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

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`:

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.