πŸ“₯ 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} ⟫= Ξ»
  { (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 = {!!}

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 = {!!}