module Antwerp.Minimum.Classical where

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

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
  -- In this case, there is no value α j which would be strictly smaller than α i.
  -- So we are done searching for the minimal value.
    where
    h : (j : ℕ) → α i ≤ α j
    h j with ≤-<-connex (α i) (α j)
    ... | inj₁ αi≤αj = αi≤αj
    ... | inj₂ αj<αi = ⊥-elim (q (j , αj<αi))

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