📥 Download raw
{-# 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 = {!!}