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

    theorem : Dickson α
    theorem with minimum
    ... | i , p = i , p (suc i)

module Example where
  α : ℕ → ℕ
  α  = 
  α  = 
  α  = 
  α _ = 

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 

    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 → ⊥) → ⊥)