{-# OPTIONS --cubical-compatible #-}
module Padova2025.ComputationalContent.Fictions.Minima (⊥ : Set) where
Minima
open import Padova2025.ProgrammingBasics.Naturals.Base open import Padova2025.ProvingBasics.Termination.Ordering open import Padova2025.ProvingBasics.Termination.WellFounded.Base open import Padova2025.ProvingBasics.Connectives.Disjunction open import Padova2025.ProvingBasics.Connectives.Existential open import Padova2025.ProvingBasics.Connectives.Conjunction open import Padova2025.ComputationalContent.DoubleNegation (⊥)
Minima of functions up to double negation
go : (α : ℕ → ℕ) → (i : ℕ) → Acc _<'_ (α i) → ¬ ¬ (Σ[ i ∈ ℕ ] ((j : ℕ) → ¬ ¬ α i ≤ α j)) go α i (acc f) = oracle {Σ[ j ∈ ℕ ] α j < α i} ⟫= g where g : ((Σ[ j ∈ ℕ ] α j < α i) ⊎ ((Σ[ j ∈ ℕ ] α j < α i) → ⊥)) → ¬ ¬ (Σ[ i ∈ ℕ ] ((j : ℕ) → ¬ ¬ α i ≤ α j)) g (left (j , p)) = {!!} g (right q) = {!!} where h : (j : ℕ) → ¬ ¬ (α i ≤ α j) h j with ≤-<-connex (α i) (α j) ... | left αi≤αj = {!!} ... | right αj<αi = {!!}
minimum : (α : ℕ → ℕ) → ¬ ¬ (Σ[ i ∈ ℕ ] ((j : ℕ) → ¬ ¬ α i ≤ α j)) minimum = {!!}
Variant for inhabited sets of natural numbers
go' : (P : ℕ → Set) (n : ℕ) → P n → Acc _<'_ n → ¬ ¬ (∃[ a ] P a × ((b : ℕ) → b < a → P b → ⊥)) go' = {!!}
minimum' : (P : ℕ → Set) → (∃[ n ] P n) → ¬ ¬ (∃[ a ] P a × ((b : ℕ) → b < a → P b → ⊥)) minimum' = {!!}
A largest natural number?
Carefully ponder the following code claiming to show, up to double negation, the existence of a largest natural number. How does it try to work, and why does Agda reject it?
largest-number : ¬ ¬ (Σ[ a ∈ ℕ ] ((b : ℕ) → ¬ ¬ a ≥ b))
largest-number = f zero
where
f : ℕ → ¬ ¬ (Σ[ a ∈ ℕ ] ((b : ℕ) → ¬ ¬ a ≥ b))
f a k = k (a , h)
where
h : (b : ℕ) → ¬ ¬ a ≥ b
h b with ≤-<-connex b a
... | left b≤a = return m≤n
... | right a<b = λ k' → f b k
lemma : {x : ℕ} → succ x ≤ x → ⊥ lemma = {!!}
no-largest-number : ¬ (¬ ¬ (∃[ a ] ((b : ℕ) → ¬ ¬ b ≤ a))) no-largest-number = {!!}