Some stuff that depends on the ecluded middle.

module Classical where

import Relation.Binary.PropositionalEquality as Eq
open Eq using (_≡_; refl; _≢_; sym; trans; subst)
open import Data.Nat using (ℕ; zero; suc; _≤_; s≤s; z≤n; _<_)
open import Data.Product using (Σ; _×_; _,_; proj₁; proj₂ ; ∃; Σ-syntax; ∃-syntax; ∃₂)
open import Data.Sum using (_⊎_; inj₁; inj₂) renaming ([_,_]′ to case-⊎)
open import Relation.Nullary using (¬_)
open import Data.Empty using (⊥; ⊥-elim)
open import Relation.Unary using (_∈_; Satisfiable)
open import Function using (_∘_; id)

open import Miscellaneous

postulate
  em : {A : Set} → A ⊎ ¬ A

¬¬-elim : {A : Set} → ¬ ¬ A → A
¬¬-elim {A} h with em {A}
... | inj₁ x = x
... | inj₂ y = ⊥-elim (h y)

¬∀⟶∃¬ : {A : Set} {B : A → Set} → ¬ (∀ (x : A) → B x) → Σ[ x ∈ A ] ¬ (B x)
¬∀⟶∃¬ {A} {B} ¬∀xBx = ¬¬-elim (λ ¬∃x¬Bx → ¬∀xBx (λ x → ¬¬-elim (λ ¬Bx → ¬∃x¬Bx (x , ¬Bx))))

¬∀∃⟶∃∀¬ : {A : Set} {B : A → Set} {C : (x : A) → B x → Set}
  → ¬ (∀ (x : A) → Σ[ y ∈ B x ] C x y)
  ------------------------------------
  → Σ[ x ∈ A ] ∀ (y : B x) → ¬ C x y
¬∀∃⟶∃∀¬ ¬∀∃ with ¬∀⟶∃¬ ¬∀∃ 
... | x , ¬∃ = x , (¬∃⟶∀¬ (λ ∃ → ¬∃ ∃))

¬infinite⇒finite : (P : ℕ → Set) → ¬ Infinite P → Finite P
¬infinite⇒finite P h = k , λ l k<l z → [2] (l , k<l , z)
  where
  [1] : Σ[ k ∈ ℕ ] ¬ (Σ[ l ∈ ℕ ] k < l × P l)
  [1] = ¬∀⟶∃¬ h
  k : ℕ
  k = proj₁ [1]
  [2] : ¬ (Σ[ l ∈ ℕ ] k < l × P l)
  [2] = proj₂ [1]

infinite∨finite : (P : ℕ → Set) → Infinite P ⊎ Finite P
infinite∨finite P = case-⊎ inj₁ (λ z → inj₂ (¬infinite⇒finite P z)) (em {A = Infinite P})

¬finite⇒infinite : (P : ℕ → Set) → ¬ Finite P → Infinite P
¬finite⇒infinite P h = ⊎-¬ʳ (infinite∨finite P) h

-- ¬coinfinite⇒cofinite : (P : ℕ → Set) → ¬ Coinfinite P → Cofinite P
-- ¬coinfinite⇒cofinite = {!   !}

-- ¬cofinite⇒coinfinite : (P : ℕ → Set) → ¬ Cofinite P → Coinfinite P
-- ¬cofinite⇒coinfinite P = {!   !}

leastNumber-aux : {A : ℕ → Set} (x : ℕ)
  → A x
  --------------------------------------------
  → Σ[ z ∈ ℕ ] (A z × ((y : ℕ) → A y → z ≤ y))
leastNumber-aux {A} x Ax with x | em {A zero}
... | _     | inj₁ A0  = zero , A0 , λ y _ → z≤n
... | zero  | inj₂ ¬A0 = ⊥-elim (¬A0 Ax)
... | suc x | inj₂ ¬A0 = 
    suc z , A1+z , 
    (λ {zero A0       → ⊥-elim (¬A0 A0)
       ; (suc y) A1+y → s≤s (h′ y A1+y)
       })
  where
  h : Σ[ z ∈ ℕ ] A (suc z) × ((y : ℕ) → A (suc y) → z ≤ y)
  h = leastNumber-aux {A ∘ suc} x Ax
  z = proj₁ h
  A1+z = proj₁ (proj₂ h)
  h′ : (y : ℕ) → A (suc y) → z ≤ y
  h′ = proj₂ (proj₂ h)

leastNumberPrinciple : {A : ℕ → Set} → Satisfiable A → Σ[ z ∈ ℕ ] (z ∈ A × ((y : ℕ) → y ∈ A → z ≤ y))
leastNumberPrinciple (x , Ax) = leastNumber-aux x Ax

leastSeqAt : {S : (ℕ → ℕ) → Set}
  → Satisfiable S
  → (n : ℕ)
  --------------------------------------------------------------
  → Σ[ f ∈ (ℕ → ℕ) ] (f ∈ S × ((g : ℕ → ℕ) → g ∈ S → f n ≤ g n))
leastSeqAt {S} S-nonempty n = f , f∈S , f-minimal
  where
  A : ℕ → Set
  -- A x = Σ[ g ∈ (ℕ → ℕ) ] (S g × g n ≡ x)
  A = (λ g → g n) [ S ]
  A-nonempty : Satisfiable A
  A-nonempty = nonempty-image (λ g → g n) S S-nonempty
  min-A : Σ[ z ∈ ℕ ] (z ∈ A × ((w : ℕ) → w ∈ A → z ≤ w))
  min-A = leastNumberPrinciple A-nonempty
  z : ℕ
  z = proj₁ min-A
  z∈A : z ∈ A
  z∈A = proj₁ (proj₂ min-A)
  z-minimal : (w : ℕ) → w ∈ A → z ≤ w
  z-minimal = proj₂ (proj₂ min-A)
  f : ℕ → ℕ
  f = proj₁ z∈A
  f∈S : f ∈ S
  f∈S = proj₁ (proj₂ z∈A)
  fn≡z : f n ≡ z
  fn≡z = proj₂ (proj₂ z∈A)
  f-minimal : (g : ℕ → ℕ) → g ∈ S → f n ≤ g n
  -- f-minimal g g∈S = subst (_≤ g n) (sym fn≡z) (z-minimal (g n) (member-image (λ g → g n) S g∈S))
  f-minimal g g∈S rewrite fn≡z = z-minimal (g n) (member-image (λ g → g n) S g∈S)