module transcript05 where
-- Let's state and prove the following fact:
-- Every function f : ℕ → ℕ has a minimal value.
-- ∀f : ℕ → ℕ. ∃a : ℕ. ∀b : ℕ. f(a) ≤ f(b)
open import Padova2025.ProgrammingBasics.Naturals.Base
open import Padova2025.ProgrammingBasics.Naturals.Arithmetic
open import Padova2025.ProvingBasics.Connectives.Existential
open import Padova2025.ProvingBasics.Connectives.Disjunction
open import Padova2025.ProvingBasics.Termination.Ordering
-- Dickson's Lemma: For every function f : ℕ → ℕ,
-- there is a number i : ℕ such that f(i) ≤ f(i+1).
-- (This lemma is relevant in the subject of "well-quasi orderings"
-- in computer science.)
--
-- Proof. The function f has some mimimal value f(i).
-- Then, trivially, f(i) ≤ f(i+1). ∎
Dickson : (ℕ → ℕ) → Set
Dickson f = Σ[ i ∈ ℕ ] f i ≤ f (succ i)
module Classical where
data ⊥ : Set where
¬_ : Set → Set
¬ A = A → ⊥
-- "¬ A" means that A implies ↯.
⊥-elim : {A : Set} → ⊥ → A
⊥-elim ()
postulate
oracle : (A : Set) → A ⊎ ¬ A
-- "x < y" is defined as "succ x ≤ y"
-- The computational interpretation is: "minimum" is
-- a function which inputs a function f : ℕ → ℕ
-- and outputs a pair (a , g) where a : ℕ
-- and g : (b : ℕ) → f a ≤ f b.
-- (For any two numbers x and y, "x ≤ y" is the type of
-- witnesses that x is at most y.)
{-# TERMINATING #-}
go : (f : ℕ → ℕ) → ℕ → Σ[ a ∈ ℕ ] ((b : ℕ) → f a ≤ f b)
go f n with oracle (Σ[ m ∈ ℕ ] f m < f n)
... | left (m , fm<fn) = go f m
... | right p = (n , h)
where
h : (b : ℕ) → f n ≤ f b
h b with ≤-<-connex (f n) (f b)
... | left fn≤fb = fn≤fb
... | right fb<fn = ⊥-elim (p (b , fb<fn))
-- Idea: Check whether f n is minimal.
-- If so (case "right"): awesome, we are done.
-- If not (case "left"): then there exists some m such that f m < f n.
minimum : (f : ℕ → ℕ) → Σ[ a ∈ ℕ ] ((b : ℕ) → f a ≤ f b)
minimum f = go f zero
lemma : (f : ℕ → ℕ) → Dickson f
lemma f with minimum f
... | i , p = (i , p (succ i))
-- Obviously, classical mathematics is larger than constructive mathematics:
-- We have a couple more axioms available (law of excluded middle, axiom of choice).
-- With more axioms, we can prove more stuff.
-- On the other hand, we can also regard constructive mathematics as being larger
-- than classical mathematics: Every* result of classical mathematics can be turned
-- into a result of constructive mathematics, if we just spam sufficiently many
-- double negations.
-- (More precisely: Every proof involving the law of excluded middle can be transformed
-- into a proof not using the law of excluded middle, at the price of a couple of
-- double negations; for eliminating the axiom of choice, other techniques are needed.)
-- Bonus metatheorem: In some case, we can, in the end, even eliminate the double negations.
-- "Let us come to the section titled 'constructive but uninformative'. Fix a type ⊥."
module ConstructiveButUninformative (⊥ : Set) where
¬_ : Set → Set
¬ A = A → ⊥
-- "¬ A" means that A implies ↯.
⊥-elim : {A : Set} → ⊥ → ¬ ¬ A
⊥-elim x = λ z → x
oracle : (A : Set) → ¬ ¬ (A ⊎ ¬ A)
oracle A = λ z → z (right (λ z₁ → z (left z₁)))
-- The "return" here does not have anything to do with the "return" keyword
-- in Python or Java (which would cause an early exit out of a subroutine).
return : {A : Set} → A → ¬ ¬ A
return x = λ z → z x
-- Note: In constructive mathematics, we do NOT have (in general) ¬ ¬ A → A.
-- (Example: Let A be the assertion "there is a position where the keys to my apartment are"
-- in the situation that we don't find our keys. Then we cannot constructively claim A,
-- but we can constructively claim ¬ ¬ A, as it's impossible for the keys to have vanished.)
escape : ¬ ¬ ⊥ → ⊥
escape m = m (λ z → z)
-- Logical reading: If ¬ ¬ A, and if A implies ¬ ¬ B, then ¬ ¬ B.
_⟫=_ : {A B : Set} → ¬ ¬ A → (A → ¬ ¬ B) → ¬ ¬ B
m ⟫= f = λ z → m (λ z₁ → f z₁ z)
-- Note: Double negation constitutes a monad (as in Haskell).
{-# TERMINATING #-}
go : (f : ℕ → ℕ) → ℕ → ¬ (¬ (Σ[ a ∈ ℕ ] ((b : ℕ) → ¬ ¬ (f a ≤ f b))))
go f n = oracle (Σ[ m ∈ ℕ ] f m < f n) ⟫= g
where
g : (Σ[ m ∈ ℕ ] f m < f n) ⊎ ¬ (Σ[ m ∈ ℕ ] f m < f n) → _
g (left (m , fm<fn)) = go f m
g (right p) = return (n , h)
where
h : (b : ℕ) → ¬ ¬ (f n ≤ f b)
h b with ≤-<-connex (f n) (f b)
... | left fn≤fb = return fn≤fb
... | right fb<fn = ⊥-elim (p (b , fb<fn))
minimum : (f : ℕ → ℕ) → ¬ (¬ (Σ[ a ∈ ℕ ] ((b : ℕ) → ¬ ¬ (f a ≤ f b))))
minimum f = go f zero
lemma : (f : ℕ → ℕ) → ¬ ¬ (Dickson f)
lemma f = minimum f ⟫= λ (i , p) → p (succ i) ⟫= λ fi≤fsucci → return (i , fi≤fsucci)
module Constructive where
theorem : (f : ℕ → ℕ) → Dickson f
theorem f = escape (lemma f)
where
open ConstructiveButUninformative (Dickson f)
-- A philosophical interpretation of this state of affairs:
-- Minima of functions are (very useful) convenient fictions.
-- They are not actually available in constructive mathematics (as we cannot compute them),
-- but we can just pretend that they are and still obtain fully valid constructive results in the end.
example-function : ℕ → ℕ
example-function zero = five
example-function (succ zero) = four
example-function (succ (succ zero)) = two
example-function (succ (succ (succ zero))) = zero
example-function (succ (succ (succ (succ zero)))) = four
example-function n = n ²
-- This constructivization technique is variously known as:
-- "Friedman's trick"
-- "the nontrivial exit continuation trick"
-- "Barr's theorem"
-- Option 1: Terminate this session.
-- Option 2: Agda exercises.
-- Option 3: Numbers larger than infinity.
-- Option 4: Program verification.
-- (Ordinal) Numbers larger than infinity!
-- 0, 1, 2, 3, ..., ω, ω+1, ω+2, ..., ω+ω=ω·2, ..., ω·3, ..., ω·ω = ω², ...,
-- ω³, ..., ω^ω, ..., ω^(ω^ω), ..., ω^(ω^(ω^...)) = ε₀, ε₀+1,
-- ε₀^(ε₀^(ε₀^(...))) = ε₁, ..., ε₁^(ε₁^(...)) = ε₂, ..., ε_ω, ..., ε_{ω+1}, ...,
-- ε_{ε_0}, ..., ε_{ε_{ε_0}}, ..., ε_{ε_{ε_...}} = ζ₀, ...
-- ω + 1 > 1 + ω = ω
-- Graphical visualization of these numbers:
{-
7: :-) I I I I I I I
ω: :-) I I I I I I I ...
+-----------------+ +---------+
ω + ω + 1: :-) |I I I I I I I ...| |I I I ...| I
+-----------------+ +---------+
+----------+
1 + ω: :-) I |I I I I...| = ω
+----------+
ω · 2 > 2 · ω = ω
+-----------------+ +---------+
:-) |I I I I I I I ...| |I I I ...|
+-----------------+ +---------+
+---------------+
2 · ω :-) |II II II II ...|
+---------------+
-}
-- Type of (representations of) ordinal numbers
-- Take care, most ordinal numbers will have several representations
-- (compare with the reals: 1.000... = 0.999...)
data O : Set
-- "x ≤ y" the type of witnesses that x is at most y
data _≼_ : O → O → Set
-- "x < y" the type of witnesses that x is strictly smaller than y
_≺_ : O → O → Set
-- "Monotonic f" is the type of witnesses that the function f
-- is strictly increasing: f 0 < f 1 < f 2 < ...
-- More formally, ∀n : ℕ. f n < f (succ n)
Monotonic : (ℕ → O) → Set
Monotonic f = (n : ℕ) → f n ≺ f (succ n)
data O where
zer : O
suc : O → O
lim : (f : ℕ → O) → Monotonic f → O
-- Take care, we may NOT state a constructor "lim : (ℕ → O) → O" here.
-- Such a constructor would indicate that we may take the limit of
-- any sequence of ordinals, even alternating ones which cannot decide
-- to which number to converge to.
x ≺ y = suc x ≼ y
data _≼_ where
≼-zer : {x : O} → zer ≼ x
≼-suc-mon : {x y : O} → x ≼ y → suc x ≼ suc y
≼-trans : {x y z : O} → x ≼ y → y ≼ z → x ≼ z
≼-cocone : {f : ℕ → O} {fmon : Monotonic f} {x : O} {n : ℕ} → x ≼ f n → x ≼ lim f fmon
≼-limiting : {f : ℕ → O} {fmon : Monotonic f} {x : O} → ((n : ℕ) → f n ≼ x) → lim f fmon ≼ x
lim-mon
: {f g : ℕ → O} {fmon : Monotonic f} {gmon : Monotonic g}
→ ((n : ℕ) → f n ≼ g n)
→ lim f fmon ≼ lim g gmon
lim-mon p = ≼-limiting (λ n → ≼-cocone (p n))
≼-refl : {x : O} → x ≼ x
≼-refl {zer} = ≼-zer
≼-refl {suc x} = ≼-suc-mon ≼-refl
≼-refl {lim f x} = lim-mon (λ n → ≼-refl {f n})
uno : O
uno = suc zer
fromℕ : ℕ → O
fromℕ zero = zer
fromℕ (succ n) = suc (fromℕ n)
fromℕ-mon : Monotonic fromℕ
fromℕ-mon n = ≼-refl
ω : O
ω = lim fromℕ fromℕ-mon
-- For instance, the number ω is the limit of the sequence 0, 1, 2, ...
-- For instance, the number ω is the limit of the sequence f,
-- where f : ℕ → O is given by f 0 = 0, f 1 = 1, f 2 = 2, ...
-- In Agda, we can then write: ω = lim f
-- For instance, the number ω is the limit of the sequence 1, 2, 3, ...
-- For instance, the number ω is the limit of the sequence 1, 4, 9, 16, ...
-- For instance, the number ω is the limit of the sequence f,
-- where f : ℕ → O is given f n = (succ n)².
-- For instance, the number ω+ω is the limit of the sequence ω, ω+1, ω+2, ...
-- There are sequences without a limit in the ordinal numbers, for instance
-- 0, 1, 0, 1, 0, 1, ...
open import Padova2025.ProvingBasics.Connectives.Conjunction
_≈_ : O → O → Set
x ≈ y = x ≼ y × y ≼ x
infixl 6 _+'_
_+'_ : O → O → O
+-mon : {x a b : O} → a ≼ b → (x +' a) ≼ (x +' b)
x +' zer = x
x +' suc y = suc (x +' y)
x +' lim f fmon = lim (λ n → x +' f n) (λ n → +-mon {x = x} (fmon n))
-- suc (f n) ≼ f (succ n) is equivalent (by definition) to f n ≺ f (succ n)
+-mon p = {!!}
claim₁ : (uno +' ω) ≼ ω
claim₁ = ≼-limiting (λ n → ≼-cocone (lemma n))
where
lemma : (n : ℕ) → (uno +' fromℕ n) ≼ suc (fromℕ n)
lemma zero = ≼-suc-mon ≼-zer
lemma (succ n) = ≼-suc-mon (lemma n)
claim₂ : ω ≼ (uno +' ω)
claim₂ = {!!}