{-# 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#

Exercise 1go

go : (α : ℕ → ℕ) → (i : ℕ) → Acc _<'_ (α i) → ¬ ¬ (Σ[ i ∈ ℕ ] ((j : ℕ) → ¬ ¬ α i ≤ α j))
go α i (acc f) = oracle {Σ[ j ∈ ℕ ] α j < α i} ⟫= λ
  { (left  (j , p)) → {!!}
  ; (right q)       → {!!}
  }
  where
  h : ¬ (Σ[ j ∈ ℕ ] α j < α i) → (j : ℕ) → ¬ ¬ (α i ≤ α j)
  h q j with ≤-<-connex (α i) (α j)
  ... | left  αi≤αj = {!!}
  ... | right αj<αi = {!!}

The reference solution uses: <⇒<' return ⊥-elim

Your solution

Reference solution

go : (α : ℕ → ℕ) → (i : ℕ) → Acc _<'_ (α i) → ¬ ¬ (Σ[ i ∈ ℕ ] ((j : ℕ) → ¬ ¬ α i ≤ α j))
go α i (acc f) = oracle {Σ[ j ∈ ℕ ] α j < α i} ⟫= λ
  { (left  (j , p)) → go α j (f (<⇒<' p))
  ; (right q)       → return (i , h q)
  }
  where
  h : ¬ (Σ[ j ∈ ℕ ] α j < α i) → (j : ℕ) → ¬ ¬ (α i ≤ α j)
  h q j with ≤-<-connex (α i) (α j)
  ... | left  αi≤αj = return αi≤αj
  ... | right αj<αi = ⊥-elim (q (j , αj<αi))

Exercise 2minimum

minimum : (α : ℕ → ℕ) → ¬ ¬ (Σ[ i ∈ ℕ ] ((j : ℕ) → ¬ ¬ α i ≤ α j))
minimum = {!!}

The reference solution uses: go zero ℕ-wf

Your solution

Reference solution

minimum : (α : ℕ → ℕ) → ¬ ¬ (Σ[ i ∈ ℕ ] ((j : ℕ) → ¬ ¬ α i ≤ α j))
minimum α = go α zero (ℕ-wf (α zero))

Variant for inhabited sets of natural numbers#

Exercise 3go'

go' : (P : ℕ → Set) (n : ℕ) → P n → Acc _<'_ n → ¬ ¬ (∃[ a ] P a × ((b : ℕ) → b < a → P b → ⊥))
go' = {!!}

The reference solution uses: acc _,_ <⇒<'

Your solution

Reference solution

go' : (P : ℕ → Set) (n : ℕ) → P n → Acc _<'_ n → ¬ ¬ (∃[ a ] P a × ((b : ℕ) → b < a → P b → ⊥))
go' P n Pn (acc f) k = k (n , Pn , λ b b<n Pb → go' P b Pb (f (<⇒<' b<n)) k)

Exercise 4minimum'

minimum' : (P : ℕ → Set) → (∃[ n ] P n) → ¬ ¬ (∃[ a ] P a × ((b : ℕ) → b < a → P b → ⊥))
minimum' = {!!}

The reference solution uses: _,_ go' ℕ-wf

Your solution

Reference solution

minimum' : (P : ℕ → Set) → (∃[ n ] P n) → ¬ ¬ (∃[ a ] P a × ((b : ℕ) → b < a → P b → ⊥))
minimum' P (n , Pn) = go' P n Pn (ℕ-wf n)

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

Exercise 5lemma

lemma : {x : ℕ} → succ x ≤ x → ⊥
lemma = {!!}

The reference solution uses: s≤s

Your solution

Reference solution

lemma : {x : ℕ} → succ x ≤ x → ⊥
lemma (s≤s p) = lemma p

Exercise 6no-largest-number

no-largest-number : ¬ (¬ ¬ (∃[ a ] ((b : ℕ) → ¬ ¬ b ≤ a)))
no-largest-number = {!!}

The reference solution uses: escape _,_ succ return lemma

Your solution

Reference solution

no-largest-number : ¬ (¬ ¬ (∃[ a ] ((b : ℕ) → ¬ ¬ b ≤ a)))
no-largest-number m = escape do
  (a , f) ← m
  absurd  ← f (succ a)
  return (lemma absurd)