{- The following infinite sequence of natural numbers α : 10, 5, 3, 2, 4, 6, 6, 6, 6, 6, 6, ... ^ ^ ^^^^ | \ α 3 ≤ α 4 α 0 α 1 is good because some earlier term in the sequence is smaller than some later term. Dickson's Lemma (simple version). Every infinite sequence of natural numbers is good. More precisely: For every infinite sequence α, there are indices i < j such that α(i) ≤ α(j). In fact, it even holds that: For every infinite sequence α, there is an index i such that α(i) ≤ α(i+1). Proof. The infinite sequence α attains a minimal value somewhere. Let's call this minimal value α(i). Then we observe α(i) ≤ α(i+1). Hence α is good. Note. The hypothetical generalization of Dickson's Lemma to integers is false, as for instance the infinite sequence 0, -1, -2, -3, ... is _not_ good. -} {- Note: The claim that every infinite sequence of natural numbers attains a minimal value is _not_ provable in constructive mathematics. Because if there was a constructive proof of this claim, then there would also be an algorithm witnessing this claim, that is, there would be an algorithm which would be capable of determining the minimal value of any infinite sequence of natural numbers. In other words: In Agda, there is no function minimum : (ℕ → ℕ) → ℕ. -} open import Data.Nat open import Data.Nat.Properties open import Data.Product open import Data.Sum Dickson : (ℕ → ℕ) → Set -- in math: ∃i ∈ ℕ. α(i) ≤ α(i+1) Dickson α = Σ[ i ∈ ℕ ] α i ≤ α (suc i) -- "Dickson α" is the type of pairs (i , p) -- where i is some value of type ℕ -- and where p is a value of type α i ≤ α (suc i). module Classical where data ⊥ : Set where -- "ex falso quodlibet" -- "from a contradiction, anything follows" ⊥-elim : {X : Set} → ⊥ → X ⊥-elim () postulate oracle : (X : Set) → X ⊎ (X → ⊥) -- Logical reading: X holds, or not X holds. -- (Recall: The negation of X is defined as "X → ⊥".) -- Computational reading: "oracle" is a function which -- reads an arbitrary X as input and outputs a witness -- of either X or of X → ⊥. module _ (α : ℕ → ℕ) where {-# TERMINATING #-} go : ℕ → Σ[ i ∈ ℕ ] ((j : ℕ) → α i ≤ α j) go i with oracle (Σ[ j ∈ ℕ ] α j < α i) ... | inj₁ (j , p) = go j -- In this case, there is some value α j which is strictly smaller (<) than α i. -- So α i is not the absolute minimal value. So we need to continue searching -- for the minimal value. ... | inj₂ q = i , h where h : (j : ℕ) → α i ≤ α j h j with ≤-<-connex (α i) (α j) ... | inj₁ αi≤αj = αi≤αj ... | inj₂ αj<αi = ⊥-elim (q (j , αj<αi)) -- In this case, there is value α j which would be strictly smaller than α i. -- So we are done searching for the minimal value. -- Logical reading: There is a number i such that for every number j, -- it holds that α i ≤ α j. -- Computational reading: "minimum" is a pair consisting of a number i -- and a function which reads as input a number j and which outputs -- a witness that α i ≤ α j. minimum : Σ[ i ∈ ℕ ] ((j : ℕ) → α i ≤ α j) minimum = go 0 theorem : Dickson α theorem with minimum ... | i , p = i , p (suc i) module Example where α : ℕ → ℕ α 0 = 50 α 1 = 30 α 2 = 7 α _ = 10 module ConstructiveButUninformative (⊥ : Set) where ¬_ : Set → Set ¬ X = X → ⊥ ⊥-elim : {X : Set} → ⊥ → ¬ ¬ X ⊥-elim p = λ k → p return : {X : Set} → X → ¬ ¬ X return p = λ k → k p -- Constructively, we do NOT have ¬ ¬ X → X. -- That would be the principle of double negation elimination. escape : ¬ ¬ ⊥ → ⊥ escape p = p (λ z → z) oracle : (X : Set) → ¬ ¬ (X ⊎ (X → ⊥)) oracle X = λ k → k (inj₂ (λ x → k (inj₁ x))) _⟫=_ : {A B : Set} → ¬ ¬ A → (A → ¬ ¬ B) → ¬ ¬ B m ⟫= f = λ k → m (λ x → f x k) module _ (α : ℕ → ℕ) where {-# TERMINATING #-} go : ℕ → ¬ ¬ (Σ[ i ∈ ℕ ] ((j : ℕ) → ¬ ¬ (α i ≤ α j))) go i = oracle (Σ[ j ∈ ℕ ] α j < α i) ⟫= g where g : ((Σ[ j ∈ ℕ ] α j < α i) ⊎ ((Σ[ j ∈ ℕ ] α j < α i) → ⊥)) → ¬ ¬ (Σ[ i ∈ ℕ ] ((j : ℕ) → ¬ ¬ (α i ≤ α j))) g (inj₁ (j , p)) = go j g (inj₂ q) = return (i , h) where h : (j : ℕ) → ¬ ¬ (α i ≤ α j) h j with ≤-<-connex (α i) (α j) ... | inj₁ αi≤αj = return αi≤αj ... | inj₂ αj<αi = ⊥-elim (q (j , αj<αi)) minimum : ¬ ¬ (Σ[ i ∈ ℕ ] ((j : ℕ) → ¬ ¬ (α i ≤ α j))) minimum = go 0 theorem : ¬ ¬ (Dickson α) theorem = minimum ⟫= λ (i , p) → p (suc i) ⟫= λ q → return (i , q) module Constructive where module _ (α : ℕ → ℕ) where open ConstructiveButUninformative (Dickson α) thm : Dickson α thm = escape (theorem α) -- The name of this trick: -- - Friedman's A-translation -- - the continuation trick -- - Barr's theorem -- The double negation translation of a statement φ is the same as φ, but -- with ¬¬ introduced in front of every ∃, ∨, =, ≤, ... -- Two metatheorems in logic: -- 1. A statement φ is provable classically iff its double negation translation -- is provable constructively. -- 2. If φ consists just of ∃,∨,∧,=,≤, but NOT of ∀,⇒, -- then the double negation translation of φ is equivalent to just ¬¬φ. -- The double negation monad is called the "continuation monad" in compsci. -- The Haskell definition of the continuation monad is: -- newtype Cont r a = MkCont ((a → r) → r) -- Compare with ¬¬a: -- ¬ ¬ a = ((a → ⊥) → ⊥)