module Dickson where

{-
  Extracting constructive content from classical proofs
  https://agdapad.quasicoherent.io/~cirm2025/Dickson.agda

  Plan:
  0. Entertaining a ludicrous classical proof in English
  1. Formalizing the classical proof
  2. Turning the classical proof into a constructive but
     uninformative proof
  3. Fully constructivizing the proof

  Theorem (mini version of Dickson's lemma):
  For every function f : ℕ → ℕ, there is a number n : ℕ
  such that f(n) ≤ f(n+1).

  Proof (classical). By the law of excluded middle,
  there is a minimum value f(n). Hence, in particular,
  we will have f(n) ≤ f(n+1).

  Beautiful constructive proofs can be found in
  Iosif Petrakis: Constructive Combinatorics of Dickson's Lemma.
  But can we interpret the given classical proof as a blueprint for a
  constructive proof?
-}

open import Data.Nat
open import Data.Sum
open import Data.Product

module Classical where
  open import Data.Empty
  open import Relation.Nullary
  
  postulate
    -- Logical reading: For any A, either A or not A.
    -- Computational reading: "oracle" is a function
    -- which reads a set A as input and outputs
    -- either an element of A or a witness that A is empty.
    oracle : (A : Set) → A ⊎ (A → ⊥)

        -- ∀(f : ℕ → ℕ).  ∃n:ℕ. ∀(m : ℕ). f(n) ≤ f(m)
  {-# TERMINATING #-}
  minimum : (f : ℕ → ℕ) → ∃[ n ] ((m : ℕ) → f n ≤ f m)
  minimum f = go 
    where
    go : ℕ → ∃[ n ] ((m : ℕ) → f n ≤ f m)
    go i with oracle (∃[ j ] f j < f i)
    ... | inj₁ (j , fj<fi) = go j
    ... | inj₂ p           = (i , h)
      where
      h : (m : ℕ) → f i ≤ f m
      h m with ≤-<-connex (f i) (f m)
      ... | inj₁ fi≤fm = fi≤fm
      ... | inj₂ fi>fm = ⊥-elim (p (m , fi>fm))

  --       ∀(f : ℕ → ℕ).  ∃n:ℕ.  f(n) ≤ f(n+1)
  theorem : (f : ℕ → ℕ) → ∃[ n ] f n ≤ f (n + )
  theorem f with minimum f
  ... | (n , p) = (n , p (n + ))
  -- Here, p is a witness that f n is the minimum of f:
  -- Logical reading: p is a witness of ∀(m : ℕ). f(n) ≤ f(m).
  -- Computational reading: p is a function which reads as input
  -- a number m : ℕ and which outputs a witness that f(n) ≤ f(m).

example : ℕ → ℕ
example  = 
example  = 
example  = 
example _ = 

module ConstructiveButUninformative (⊥ : Set) where
  ¬_ : Set → Set
  ¬ X = (X → ⊥)

  escape : ¬ ¬ ⊥ → ⊥
  escape x = x (λ z → z)

  ⊥-elim : {A : Set} → ⊥ → ¬ ¬ A
  ⊥-elim x = λ z → x

  oracle : (A : Set) → ¬ ¬ (A ⊎ (A → ⊥))
  oracle A = λ z → z (inj₂ (λ z₁ → z (inj₁ z₁)))

  return : {A : Set} → A → ¬ ¬ A
  return x = λ z → z x

  -- If ¬¬A, and if A → B, then also ¬¬B.
  -- If ¬¬A, and if A → ¬¬B, then also ¬¬B.
  _>>=_ : {A B : Set} → ¬ ¬ A → (A → ¬ ¬ B) → ¬ ¬ B
  m >>= f = λ z → m (λ z₁ → f z₁ z)

  {-# TERMINATING #-}
  minimum : (f : ℕ → ℕ) → ¬ ¬ (∃[ n ] ((m : ℕ) → ¬ ¬ (f n ≤ f m)))
  minimum f = go 
    where
    go : ℕ → ¬ ¬ (∃[ n ] ((m : ℕ) → ¬ ¬ (f n ≤ f m)))
    go i = oracle (∃[ j ] f j < f i) >>= g
      where
      g : _ → _
      g (inj₁ (j , fj<fi)) = go j
      g (inj₂ p)           = return (i , h)
        where
        h : (m : ℕ) → ¬ ¬ (f i ≤ f m)
        h m with ≤-<-connex (f i) (f m)
        ... | inj₁ fi≤fm = return fi≤fm
        ... | inj₂ fi>fm = ⊥-elim (p (m , fi>fm))

  theorem : (f : ℕ → ℕ) → ¬ ¬ (∃[ n ] f n ≤ f (n + ))
  theorem f = do
    (n , p) ← minimum f
    fn≤fn+1 ← p (n + )
    return (n , fn≤fn+1)

module Constructive (f : ℕ → ℕ) where
  Claim : Set
  Claim = ∃[ n ] f n ≤ f (n + )

  thm : Claim
  thm = escape (theorem f)
    where
    open ConstructiveButUninformative Claim
    -- "Now use all the results of the previous section,
    -- but with Claim in place of ⊥."

-- Barr's theorem:
-- Friedman's trick works for Π² statements, so statements
-- of the form ∀x ∃y ...

-- ZFC is conservative over IZF for arithmetical Π² statements.
-- By applying the L-translation, ZFC is conservative over ZF
-- for arithmetical statements.
-- By applying the ¬¬-translation followed by Friedman's trick,
-- ZF is conservative over IZF for Π² statements.

-- nontrivial exit continuation trick