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

{-
  Options for today:

  0. Exercises [0]

  1. The infinite hat problem [3]
  
  2. Seemingly impossible programs [2]

  3. Sets as trees, giving (opinionated) answers to questions such as: [3]

     - What is the relation between sets and types?
     - What is a set?
     - Why should we not form the set of all subsets of a set?
       (In predicative mathematics, we don't accept the powerset construction.)
     - Why is the axiom of choice in general false, but why is countable choice true?
     - Why can we not always form the set { x ∈ X | ... }?

  4. The curious world of infinite-time Turing machines [no Agda code] [4]

     - An injection ℝ ↪ ℕ
     - What is problematic about (¬ ¬ (Σ[ n ∈ ℕ ] P n)) → Σ[ n ∈ ℕ ] P n?

  5. Forcing [0]

     - How can we prove that a function f : (ℕ → Bool) → X only inspects finitely
       many values of its argument φ : ℕ → Bool?
     - How can we throw exceptions in pure mathematics?
     - How can we turn any set X into a countable set, i.e. a set with a surjection ℕ ↠ X?
     - How can we construct an intermediate infinity between ℕ and (ℕ → Bool)?

  6. Metamathematics [3]

     - How can Agda talk about provability?
     - Metaproving that the double negation translation is effective
-}

open import Padova2025.Explorations.Uncountability.Applications
open import Padova2025.Explorations.Uncountability.Impossible.Toy
open import Padova2025.ProgrammingBasics.Booleans
open import Padova2025.ProgrammingBasics.Lists
open import Padova2025.ProgrammingBasics.Naturals.Base
open import Padova2025.ProvingBasics.Termination.Gas hiding (𝟙)

-- Given f, g : (ℕ → Bool) → Bool, is it decidable whether f and g produce the same outputs?
-- Is it possible to write an algorithm which determines whether f x ≡ g x for all x?
--
-- The type (ℕ → Bool) contains infinitely many values, in fact uncountably many,
-- so it should be impossible to write such a decision algorithm.

f : (ℕ → Bool) → Bool
f φ = false

open import Padova2025.ProgrammingBasics.Operators

g : (ℕ → Bool) → Bool
g φ = not (φ three) || not (φ one)

wtf : Bool
wtf = f ≡? g

-- Is it possible to determine whether a function f : (ℕ → Bool) → Bool has a root?
-- (A root is a function φ : ℕ → Bool such that f φ ≡ false.)

wtf' : Maybe (List Bool)
wtf' = root g


-- A Σ₁-set is a set of the form { n ∈ ℕ | ∃a ∈ ℕ. ∃b ∈ ℕ. ... ∃z ∈ ℕ. % },
-- with no further quantifiers in % (only =, ∧, ∨, ⇒, ⊥, ⊤)



module InfiniteHatProblem
  (Player : Set)
  (Color  : Set)
  where

  open import Padova2025.ProgrammingBasics.Lists
  open import Padova2025.ProvingBasics.Equality.Base
  open import Padova2025.ProvingBasics.Equality.General
  open import Padova2025.ProvingBasics.Negation
  open import Padova2025.ProvingBasics.Connectives.Disjunction
  open import Padova2025.ProvingBasics.Connectives.Existential
  open import Padova2025.ProvingBasics.Connectives.More

  Configuration : Set
  Configuration = (Player → Color)

  -- The evil monster will pick a configuration.

  BlindedConfiguration : Player → Set
  BlindedConfiguration p = (q : Player) → q ≢ p → Color

  blind : Configuration → (p : Player) → BlindedConfiguration p
  blind c p = λ q _ → c q

  IndividualStrategy : Player → Set
  IndividualStrategy p = BlindedConfiguration p → Color

  TeamStrategy : Set
  TeamStrategy = (p : Player) → IndividualStrategy p

  _≈_ : Configuration → Configuration → Set
  c ≈ c' = Σ[ ps ∈ List Player ] ((p : Player) → (c p ≡ c' p) ⊎ (p ∈ ps))

  -- `run s c` is a function which maps a player `p` to the guess made by player `p`
  -- when following strategy `s` in the situation `c`
  run : TeamStrategy → Configuration → (Player → Color)
  run s c p = s p (blind c p)

  isSuccessful : TeamStrategy → Set
  isSuccessful s = (c : Configuration) → c ≈ run s c


module SetsAsTrees where

  {- Set theory has two fundamental ideas:

     1. Everything is a set. (For instance, the natural number zero
        can be encoded as the empty set ∅. The natural number one can
        be encoded as the set { 0 } = { ∅ } = {{}}. The natural number two
        can be encoded as the set { 0, 1 } = { {}, {{}} }. ...
        The ordinal number ω can be encoded as the set { 0, 1, 2, ... }.
        The ordinal number ω + 1 can be encoded as the set { ω, 0, 1, 2, ... }.)

     2. Up to some limitations, given a collection of sets,
        we can form the set of those sets.

     But formal set theory in the guise of ZFC (Zermelo–Fraenkel with the axiom
     of choice) leaves open the question what a set actually is. ZFC just has
     axioms like the following:

     A. There is a set which is empty.
     B. Given sets X and Y, there is a set which contains both X and Y.
     C. Given a set X, there is a set (typically written ⋃ X) which contains
        all the elements of the elements of X.
     ...

     As a consequence, as predicted by Gödel's incompleteness theorem,
     many assertions about sets are neither provable in ZFC nor refutable in ZFC.
     (For instance the continuum hypothesis is neither provable nor refutable.)
  -}

  -- Let's define, in Agda, the type V of all sets (sets as in set theory).
  -- The type V is not small (so does not belong to Agda's type Set of all small types).
  -- The type V is large (so belongs to Set₁).
  -- This type V will turn out to be a model of CZF (Constructive Zermelo–Fraenkel).
  -- If we activate Agda's classical mode, then V will turn out to be a model of ZF.
  data V : Set₁ where
    sup : {I : Set} → (I → V) → V
    -- We picture a function f : I → V as a family of sets,
    -- namely as the family consisting of the (f i)'s,
    -- where i ranges over the values of I.
    -- We then picture `sup f` as the set which contains
    -- exactly the members of the family `f` as elements.

  ∅ : V
  ∅ = sup {⊥} λ ()
    where
    data ⊥ : Set where

  -- The set { ∅ } = 1.
  uno : V
  uno = sup {𝟙} λ i → ∅
    where
    data 𝟙 : Set where
      * : 𝟙

  -- The set { 0, 1 } = 2.
  due : V
  due = sup {Bool} λ { false → ∅ ; true → uno }
  --       *
  --      / \
  --     *   *
  --         |
  --         *