Skip to content

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

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
wants to merge 1 commit into
base: master
Choose a base branch
from
+76 −9
Open

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

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
21 changes: 21 additions & 0 deletions CHANGELOG.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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`:
Expand Down
64 changes: 55 additions & 9 deletions src/Data/Fin/Properties.agda
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -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₁
------------------------------------------------------------------------
Expand Down Expand Up @@ -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 ⟩
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

We have a notation for this in case you are not aware:

Suggested change
searchMinimalCounterexample : ∀ {P : Pred (Fin n) p} → Decidable P → (∀ i → P i) ⊎ μ⟨¬ P ⟩
searchMinimalCounterexample : ∀ {P : Pred (Fin n) p} → Decidable P → Π[ P ] ⊎ μ⟨¬ P ⟩

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

So to this, I am going to hint that this suggestion (and the syntax underlying it) doesn't find universal (sic) favour with the other maintainers (see the feedback on the original #2744 from which this is derived)... and my choice of μ⟨¬_⟩ is deliberately as a synonym/alias, and not as syntax, as a consequence.

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 ⟩
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Should this be a toplevel lemma?

∀[ Decidable ⇒ suc ⊢ μ⟨¬_⟩ ⇒ μ⟨¬_⟩ ]

Copy link
Contributor Author

@jamesmckinna jamesmckinna Aug 5, 2025 •
edited
Loading

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Hmmm... I perhaps find that formulation compelling, if, as with all these things, the notational economy comes with an associated decompression penalty...
... while the simplicity of the proof makes me wonder whether it's 'worth' putting at top-level? The advantage of local lemmas is that they can always be promoted downstream, but adding new top-level lemmas requires (slightly) more justification?

Still, it is a direct analogue of ∀-cons, so maybe that's reason enough?

Oh... hang on, where does p₀ : P zero fit in your re-formulation?

μ⁺ (μ 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.
Expand Down