{-# OPTIONS --allow-unsolved-metas #-}
module session07 where

{-
  Proposal for today's plan:

  -1. Organizational stuff
  0. Random questions
  1. Concluding yesterday's correctness proof
  2. Classical mathematics in Agda
  3. Limitations of Agda

  We can also pause the discussion of new material at any point
  to have exercises :-)
-}

{-
  Starting from neutral constructive mathematics, we have three foundational choices:

  1. Embrace the law of excluded middle (A ∨ ¬A), the law of double-negation elimination
     (¬¬A → A) and the axiom of choice to obtain classical mathematics, thereby
     precluding a computational and a geometric/topological/homotopical interpretation.
 
     (The geometric/topological interpretation of constructive mathematics
     turns the (simple) constructive proof of the statement "every finitely generated vector
     space does not not have a basis" into an (involved) constructive proof of
     the statement "on every reduced scheme, every sheaf of finite type is finite
     locally free on a dense open subset" (Grothendieck's generic freeness lemma).)

  2. Embrace anti-classical dream axioms, such as "every function ℕ → ℕ is computable
     by a Turing machine" or "every function ℝ → ℝ is continuous" or "there are
     infinitesimal numbers ε such that ε² = 0" (phrased precisely).

  3. Remain in neutral constructive mathematics.
-}

{-
  There are two ways how to put Agda into "classical mode":

  A. Postulate the law of excluded middle.
  B. Assume the law of excluded middle.
-}

open import Padova2025.ProgrammingBasics.Naturals.Base
open import Padova2025.ProvingBasics.Termination.Ordering
open import Padova2025.ProvingBasics.Connectives.Disjunction
open import Padova2025.ProvingBasics.Connectives.Existential
open import Padova2025.ProvingBasics.Connectives.Conjunction
-- (recall ¬ X = (X → ⊥))

{-
-- Option A
postulate
  oracle : (X : Set) → X ⊎ ¬ X
  -- logical reading: For every proposition X, either X or not X.
  -- computational reading: `oracle` is a function which reads a type `X` as input
  -- and outputs either an element of `X` or a witness that `X` is empty.
  -- (Such a function cannot be computable.)

-- Option B
module _ (oracle : (X : Set) → X ⊎ ¬ X) where
  foo : {!!}
  foo = {!!}

  bar : {!!}
  bar = {!!}
-}

module Classical where
  open import Padova2025.ProvingBasics.Negation

  postulate
    oracle : (X : Set) → X ⊎ ¬ X

  -- Theorem. Every function f : ℕ → ℕ attains a minimum.
  -- (More precisely: For every function f : ℕ → ℕ, there is a number n : ℕ
  -- such that for all numbers m : ℕ, f(n) ≤ f(m).)

  module _ (f : ℕ → ℕ) where
    -- The `go` function should check whether its input happens to be the
    -- minimum of `f`. If so, it should return it. If not, it should recurse
    -- to find the actual of `f`.
    {-# TERMINATING #-}
    go : ℕ → Σ[ n ∈ ℕ ] ((m : ℕ) → f n ≤ f m)
    go n with oracle (Σ[ i ∈ ℕ ] f i < f n)
    ... | left  (i , fi<fn) = go i
    ... | right p           = n , h
      where
      h : (m : ℕ) → f n ≤ f m
      h m with ≤-<-connex (f n) (f m)
      ... | left  fn≤fm = fn≤fm
      ... | right fm<fn = ⊥-elim (p (m , fm<fn))

    minimum : Σ[ n ∈ ℕ ] ((m : ℕ) → f n ≤ f m)
    minimum = go zero

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

  -- Proof (classical). Let f n be the minimal value of f.
  -- Then f n ≤ f m for all numbers m. So in particular, f n ≤ f (1 + n).

  theorem : (f : ℕ → ℕ) → Σ[ n ∈ ℕ ] f n ≤ f (succ n)
  theorem f with minimum f
  ... | (n , p) = n , p (succ n)

{-
  classical logic = intuitionistic logic + law of excluded middle
  intuitionistic logic = minimal logic + principle of explosion (⊥-elim : ⊥ → A)

  classical mathematics = set theory layered on classical logic
  constructive mathematics = set theory layered on intuitionistic logic (one option among many)
-}

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

  oracle : (A : Set) → ¬ ¬ (A ⊎ ¬ A)
  oracle A = λ z → z (right (λ z₁ → z (left z₁)))

  de-morgan : {A B : Set} → ¬ (A × B) → ¬ ¬ ((¬ A) ⊎ (¬ B))
  de-morgan = λ z z₁ → z₁ (left (λ z₂ → z₁ (right (λ z₃ → z (z₂ , z₃)))))

  -- In the metamathematics of constructive mathematics, we learn the following:
  -- By applying the so-called "double-negation translation" to a classical* result,
  -- we obtain a constructive result.
  --
  -- The double-negation translation of a statement A is just A again,
  -- but with ¬¬ inserted in front of each ⊎, ∃ and in front of each atomic formula (≡).
  --
  -- * by "classical result", I mean a result which is proven using the law of excluded middle
  -- (but not using the axiom of choice)

  -- "¬ ¬ A" can be read as follows:
  -- 1. It is impossible that A is false.
  -- 2. A is potentially true.
  -- 3. A is anonymously true.
  -- 4. A is noncomputably true.
  -- 5. A is noncontinuously true.
  -- 6. A is densely true.

  -- The following function is totally UNRELATED with the `return` keyword
  -- of most mainstream programming languages.
  return : {A : Set} → A → ¬ ¬ A
  return x = λ z → z x

  -- We do NOT have: escape : ¬ ¬ A → A
  -- But we do have:
  escape : ¬ ¬ ⊥ → ⊥
  escape f = f λ z → z
 
  fun : {A : Set} → ¬ ¬ ¬ A → ¬ A
  fun = λ z z₁ → z (λ z₂ → z₂ z₁)
  -- Negating thrice is the same as negating once.

  -- logical reading: If A is potentially true, and if the actual truth of A would imply
  -- the potential truth of B, then B is potentially true.
  _>>=_ : {A B : Set} → ¬ ¬ A → (A → ¬ ¬ B) → ¬ ¬ B
  m >>= f = λ z → m (λ z₁ → f z₁ z)
  -- By _>>=_, double negation is not a dead end: Instead, we can continue reasoning.
  -- It's just that we are trapped in the double negation monad.

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

  module _ (f : ℕ → ℕ) where
    {-# TERMINATING #-}
    go : ℕ → ¬ ¬ (Σ[ n ∈ ℕ ] ((m : ℕ) → ¬ ¬ (f n ≤ f m)))
    go n = oracle (Σ[ i ∈ ℕ ] f i < f n) >>= λ
      { (left  (i , fi<fn)) → go i
      ; (right p)           → return (n , h p)
      }
      where
      h : ¬ (Σ[ i ∈ ℕ ] f i < f n) → (m : ℕ) → ¬ ¬ (f n ≤ f m)
      h p m with ≤-<-connex (f n) (f m)
      ... | left  fn≤fm = return fn≤fm
      ... | right fm<fn = ⊥-elim (p (m , fm<fn))

    minimum : ¬ ¬ (Σ[ n ∈ ℕ ] ((m : ℕ) → ¬ ¬ (f n ≤ f m)))
    minimum = go zero

  -- The computational reading of the `theorem` function is unfortunately NOT the following:
  -- "`theorem` is a function which inputs a function f : ℕ → ℕ and outputs a pair (n , q)
  -- consisting of a number n and a witness q : f n ≤ f (succ n)."
  theorem : (f : ℕ → ℕ) → ¬ ¬ (Σ[ n ∈ ℕ ] f n ≤ f (succ n))
  --theorem f = minimum f >>= λ (n , p) → p (succ n) >>= λ q → return (n , q)
  {-with minimum f
  ... | (n , p) = n , p (succ n)-}
  theorem f = do
    (n , p) ← minimum f
    q       ← p (succ n)
    return (n , q)

module ConstructiveAndInformative (f : ℕ → ℕ) where
  Dickson : Set
  Dickson = Σ[ n ∈ ℕ ] f n ≤ f (succ n)

  thm : Dickson
  thm = escape (theorem f)
    where
    open ConstructiveButUninformative Dickson

example : ℕ → ℕ
example zero        = five
example (succ zero) = four
example _           = three

{-
  Philosophical interpretation of this constructivization trick:

    Contrary to what they tell you in the first year of university,
    it IS possible to use auxiliary lemmas whose assumptions are NOT met.
    (In our example, we have used the lemma on the existence of a minimum,
    even though its assumption, namely the law of excluded middle, was not met.)

    We can regard the minimum of a function f : ℕ → ℕ as a "convenient fiction"
    (similar to money or negative integers or complex numbers or ...).

  Computational interpretation of this constructivization trick:

    If somebody asks us what the minimum of a function f : ℕ → ℕ is,
    then we claim that f zero is the minimum. This might, by chance,
    actually be true! It might also be false. If our opponent challenges
    us by exhibiting a number i such that f i < f zero, then we backtrack
    and now claim that f i is the minimum.
-}


-- Limitations of standard Agda (resolved by cubical Agda):
-- 1. no function extensionality
-- 2. no quotient types
-- 3. no propositional truncation
-- 4. vastly underspecified equality types
-- 5. only zero-dimensional types (this limitation is shared by blackboard mathematics)

open import Padova2025.ProgrammingBasics.Booleans
open import Padova2025.ProvingBasics.Equality.Base

-- Function extensionality
example₁ : Bool → Bool
example₁ x = x

example₂ : Bool → Bool
example₂ false = false
example₂ true  = true

example₃ : Bool → Bool
example₃ false = false
example₃ true  = true

-- claim₁₂ : example₁ ≡ example₂
-- claim₁₂ = {!!}  -- this hole cannot be filled

claim₂₃ : example₂ ≡ example₃
claim₂₃ = {!!}  -- this hole cannot be filled

_≗_ : {X Y : Set} → (X → Y) → (X → Y) → Set
f ≗ g = ((x : _) → f x ≡ g x)
-- "f ≗ g" means that f and g are "pointwise equal" (i.e. agree on all inputs).

claim₁₂' : example₁ ≗ example₂
claim₁₂' false = refl
claim₁₂' true  = refl

FunctionExtensionality : Set₁
FunctionExtensionality = {X Y : Set} {f g : X → Y} → f ≗ g → f ≡ g

-- funext : FunctionExtensionality
-- funext = {!!}  -- this hole cannot be filled

postulate
  funext : FunctionExtensionality

claim₁₂ : example₁ ≡ example₂
claim₁₂ = funext claim₁₂'

-- Running `dramatic` will NOT result in a numeral (like zero or succ zero or succ (succ zero) or ...);
-- instead, the computation will get stuck on the postulate. A dramatic failure of canonicity.
dramatic : ℕ
dramatic = foo claim₁₂
  where
  foo : {g : Bool → Bool} → example₁ ≡ g → ℕ
  foo refl = four

-- Ways how to deal with the failure of function extensionality in standard Agda:
-- 1. Use ≗ instead of ≡
-- 2. Postulate funext (thereby destroy canonicity, i.e. running proofs will get stuck)
-- 3. Assume funext



-- Limitation 3: No propositional truncation
-- It is time that I confess: What we have called "existential quantification" is not
-- what's actually understood in blackboard mathematics as existential quantification.

-- For us, an inhabitant of `Σ[ x ∈ A ] B x` is a pair (x , p) where x : A and p : B x.
-- This flavor of existence is called "specified existence", because the element `x` is specified.
--
-- Blackboard mathematics instead uses "mere existence", where such an element `x` is not
-- explicitly given.

-- One rendition of the axiom of choice states the following:
-- If ∀x:X. ∃y:Y. R(x,y), then ∃f:X→Y. ∀x:X. R(x,f(x)).
-- (Such a function f is called a "choice function".)
-- (Recall that functions in mathematics are required to be single-valued.)
-- (Recall that functions in mathematics are required to be deterministic.)

not-the-actual-axiom-of-choice
  : {X Y : Set} {R : X → Y → Set}
  → ((x : X) → Σ[ y ∈ Y ] R x y)
  → Σ[ f ∈ (X → Y) ] ((x : X) → R x (f x))
not-the-actual-axiom-of-choice h = (λ x → fst (h x)) , (λ x → snd (h x))

-- Standard Agda does not have a way of implementing mere existence.
-- In cubical Agda, mere existence is available and is written as ∥ Σ[ x ∈ A ] ... ∥.
-- In fact, for any type X, in cubical Agda we have its propositional truncation ∥ X ∥.
-- One important property of ∥ X ∥ is that for all a, b : ∥ X ∥, a ≡ b (by refl).
-- 1. X → ∥ X ∥
-- 2. ∥ X ∥ → ¬ ¬ X
{-
actual-axiom-of-choice
  : {X Y : Set} {R : X → Y → Set}
  → ((x : X) → ∥ Σ[ y ∈ Y ] R x y ∥)
  → ∥ Σ[ f ∈ (X → Y) ] ((x : X) → R x (f x)) ∥
actual-axiom-of-choice = ?
-}