module Dickson-pc2022 where

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

module Classical where
  data ⊥ : Set where

  ⊥-elim : {X : Set} → ⊥ → X
  ⊥-elim ()

  postulate
    oracle : (A : Set) → A ⊎ (A → ⊥)

  module _ (α : ℕ → ℕ) where
    {-# TERMINATING #-}
    go : ℕ → Σ[ a ∈ ℕ ] ((b : ℕ) → α a ≤ α b)
    go n with oracle (Σ[ m ∈ ℕ ] α m < α n)
    ... | inj₁ (m , αm<αn) = go m
    ... | inj₂ f           = n , g
        where
        g : (b : ℕ) → α n ≤ α b
        g b with ≤-<-connex (α n) (α b)
        ... | inj₁ αn≤αb = αn≤αb
        ... | inj₂ αb<αn = ⊥-elim (f (b , αb<αn))

    min : Σ[ a ∈ ℕ ] ((b : ℕ) → α a ≤ α b)
    min = go 

    thm : Σ[ i ∈ ℕ ] (α i ≤ α (i + ))
    thm with min
    ... | (i , f) = i , f (i + )

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

  ⊥-elim : {X : Set} → ⊥ → ¬¬ X
  ⊥-elim r k = r

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

  _⟫=_ : {A B : Set} → ¬¬ A → (A → ¬¬ B) → ¬¬ B
  m ⟫= f = λ k → m (λ x → f x k)

  pure : {A : Set} → A → ¬¬ A
  pure x = λ k → k x

  escape : ¬¬ ⊥ → ⊥
  escape m = m (λ p → p)

  module _ (α : ℕ → ℕ) where
    Exists-Minimum : Set
    Exists-Minimum = Σ[ a ∈ ℕ ] ((b : ℕ) → ¬¬ (α a ≤ α b))

    {-# TERMINATING #-}
    go : ℕ → ¬¬ Exists-Minimum
    go n = oracle (Σ[ m ∈ ℕ ] α m < α n) ⟫= g
      where
      g : (Σ[ m ∈ ℕ ] α m < α n) ⊎ ((Σ[ m ∈ ℕ ] α m < α n) → ⊥) → ¬¬ Exists-Minimum
      g (inj₁ (m , αm<αn)) = go m
      g (inj₂ f)           = λ k → k (n , h)
        where
        h : (b : ℕ) → ¬¬ (α n ≤ α b)
        h b with ≤-<-connex (α n) (α b)
        ... | inj₁ αn≤αb = pure αn≤αb
        ... | inj₂ αb<αn = ⊥-elim (f (b , αb<αn))

    min : ¬¬ (Σ[ a ∈ ℕ ] ((b : ℕ) → ¬¬ (α a ≤ α b)))
    min = go 

    thm : ¬¬ (Σ[ i ∈ ℕ ] (α i ≤ α (i + )))
    thm = min ⟫= λ (i , f) → f (i + ) ⟫= λ p → pure (i , p)

example-sequence : ℕ → ℕ
example-sequence  = 
example-sequence  = 
example-sequence  = 
example-sequence n = 

module ConstructiveAndInformative where
  module _ (α : ℕ → ℕ) where
    Dickson : Set
    Dickson = Σ[ i ∈ ℕ ] (α i ≤ α (i + ))

    open ConstructiveButUninformative Dickson

    theorem : Dickson
    theorem = escape (thm α)