module Antwerp.Minimum.Constructive (⊥ : Set) where

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

¬_ : 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