{-# OPTIONS --allow-unsolved-metas --cubical-compatible #-}
module session08a where

{-
  Proposal for today:

  -1. Review of the last session
  0. Random questions
  1. Limitations of standard Agda
  2. Cubical Agda
  3. Sets as trees
  4. Infinite-time Turing machines
  5. Learn how we can use Agda to inspect what is provable
-}

{-
  Gödel's first incompleteness theorem states:

  For every formal system S (encompassing at least int. logic)
  satisfying some basic requirements (such as MLTT, Peano arithmetic,
  ZFC, ...), there is a statement A such that:
  1. If S proves A, then S is inconsistent.
  2. If S proves ¬ A, then S is inconsistent.

  In this form, Gödel's incompleteness theorem can be proven
  in intuitionistic primitive-recursive arithmetic (IPRA),
  one of the weakest formal systems in use.
-}

{-
  In Agda, we can define the notion of an MLTT-proof
  (or ZFC-proof, or Agda-proof, or PA-proof, ...).
  (If you are interested, we can do this on the projector for PA.)

  With this notion in place, we can explore whether there
  exists an MLTT-proof of a favorite statement.

  We could then discover:
  1. In Agda, we can show that there is no PA-proof of ⊥.
     (In other words, in Agda, we can show that PA is consistent.)
  2. In Agda, we can show that there is no inhabitant of ⊥.
  3. In Agda, we can try to show that there is no Agda-proof of ⊥.
     But we will fail (by Gödel's second incompleteness theorem).

  Gödel's second incompleteness theorem states:

  Let S be a formal system satisfying certain basic requirements.
  Then: If S proves the consistency of S, then S is inconsistent.
-}

{-
  For any type A, there is a function ⊥ → A.

  To specify a function f : ℕ → A, we need to specify f zero, f (succ zero), ...;
  so we need to specify f x for each number x.

  To specify a function f : ⊥ → A, we need to specify f x for each x : ⊥.
  This is a trivial task, since ⊥ does not have any inhabitants.
-}

{-
  In (classical and intuitionistic) logic, there is the following principle:
  "⊥ implies anything." (principle of explosion, ex falso quodlibet)

  There are logics where we do NOT have this principle:

  - minimal logic (which is intuitionistic logic, just without ex falso quodlibet)
  - paraconsistent logics
-}


-- Limitations of standard Agda:
-- 1. No function extensionality
-- 2. No quotients
-- 3. No propositional truncation
-- 4. Vastly under-specified equality types
-- 5. No higher-dimensional types (this limitation is shared by blackboard mathematics)

open import Padova2025.ProgrammingBasics.Naturals.Base
open import Padova2025.ProgrammingBasics.Naturals.Arithmetic
open import Padova2025.ProvingBasics.Equality.Base
open import Padova2025.ProvingBasics.Connectives.Existential
open import Padova2025.ProvingBasics.Connectives.Disjunction

-- The following definition aspires to be a definition of
-- the type of integers, but it falls short of this expectation.
-- Instead, the following definition just defines a type
-- of integer representations.
data ℤ : Set where
  _⊖_ : ℕ → ℕ → ℤ  -- \ominus
  -- We picture `3 ⊖ 7` as the situation where have 3 € but also where
  -- we owe 7 €, making for a total of -4 €. The expression `4 ⊖ 8`
  -- represents the same total of -4 €. But, as elements of this type ℤ,
  -- these two values are distinct. (Also `5 ⊖ 9` describes the same situation.)

succℤ : ℤ → ℤ
succℤ (a ⊖ b) = succ a ⊖ b

predℤ : ℤ → ℤ
predℤ (a ⊖ b) = a ⊖ succ b

pred-succ : (x : ℤ) → predℤ (succℤ x) ≡ x
pred-succ x = {!!}
-- We will not be able to prove this; in fact, we are able to disprove this.
-- a ⊖ b is not literally the same as succ a ⊖ succ b.

-- The true type of integers would arise from the type of integer representations
-- as the "quotient type" by a suitable equivalence relation.

_≈_ : ℤ → ℤ → Set  -- \approx
(a ⊖ b) ≈ (a' ⊖ b') = (a + b' ≡ a' + b)  -- where _≡_ refers to the ordinal equality on ℕ
-- Assuming for a second that we already have the true integers,
-- we could carry out the following computation:
-- a - b = a' - b'    | + b'
-- a - b + b' = a'    | + b
-- a + b' = a' + b

data _≈'_ : ℤ → ℤ → Set where
  ≈'-refl   : {x : ℤ} → x ≈' x
  ≈'-symm   : {x y : ℤ} → x ≈' y → y ≈' x
  ≈'-trans  : {x y z : ℤ} → x ≈' y → y ≈' z → x ≈' z
  ≈'-cancel : {a b : ℕ} → (a ⊖ b) ≈' (succ a ⊖ succ b)
-- "The smallest equivalence relation generated by the wish that (a ⊖ b) ≈' (succ a ⊖ succ b)."

≈→≈' : {x y : ℤ} → x ≈ y → x ≈' y
≈→≈' = {!!}

≈'→≈ : {x y : ℤ} → x ≈' y → x ≈ y
≈'→≈ = {!!}

pred-succ' : (x : ℤ) → predℤ (succℤ x) ≈ x
pred-succ' x = {!!}  -- this can be filled

-- Workarounds in standard agda:
-- 1. Use a different definition with unique representations (not always possible)
-- 2. Awkwardly postulate quotients
-- 3. Awkwardly embrace setoid hell

data ℤ' : Set where
  nonnegative : ℕ → ℤ'
  negative    : ℕ → ℤ'
-- For instance, the integer 3 is then written as nonnegative (succ (succ (succ zero))).
-- The integer 0 is written as `nonnegative zero`.
-- The expression `negative zero` should represent the integer -1.
-- The expression `negative (succ zero)` should represent the integer -2.

-- We could also represent the integers by natural numbers as follows:
--
-- ℕ  intended meaning as an integer
-- 0  0
-- 1  -1
-- 2  1
-- 3  -2
-- 4  2
-- 5  -3
-- 6  3
-- 7  -4
-- 8  4
-- ...

ℤ'' : Set
ℤ'' = Σ[ a ∈ ℕ ] Σ[ b ∈ ℕ ] (a ≡ zero ⊎ b ≡ zero)
-- the type of pairs (a , b) where a is zero or b is zero

-- The integer 3  is then represented as (3 , 0 , right refl).
-- The integer -3 is then represented as (0 , 3 , left  refl).
-- But the integer 0 has two representations, namely (0 , 0 , left refl) and (0 , 0 , right refl).

-- In Cubical Agda, we could employ the propositional truncation ∥_∥
-- to fix this problem:
-- ℤ''' : Set
-- ℤ''' = Σ[ a ∈ ℕ ] Σ[ b ∈ ℕ ] ∥ (a ≡ zero ⊎ b ≡ zero) ∥

ℤ'''' : Set
ℤ'''' = Σ[ a ∈ ℕ ] Σ[ b ∈ ℕ ] a · b ≡ zero
-- The integer 3  is then represented as (3 , 0 , refl).
-- The integer -3 is then represented as (0 , 3 , refl).
-- The integer 0  is then represented as (0 , 0 , refl).

module _
  (X : Set)
  (_≈_ : X → X → Set)
  (≈-refl  : {x : X} → x ≈ x)
  (≈-symm  : {x y : X} → x ≈ y → y ≈ x)
  (≈-trans : {x y z : X} → x ≈ y → y ≈ z → x ≈ z)
  where
  postulate
    Q : Set    -- pictured as the type of equivalence classes
    π : X → Q  -- on a blackboard, often written [_]; π x is pictured as
               -- the equivalence class of x
    π-respects-≈ : {a b : X} → a ≈ b → π a ≡ π b
    effective    : {a b : X} → π a ≡ π b → a ≈ b
    elim         : {R : Set} {f : X → R} → ({a b : X} → a ≈ b → f a ≡ f b) → (Q → R)
    elim-comp    : {R : Set} {f : X → R} → (p : {a b : X} → a ≈ b → f a ≡ f b)
                 → (a : X) → elim p (π a) ≡ f a
    -- ...

The-actual-type-of-integers : Set
The-actual-type-of-integers = Q ℤ _≈_ {!!} {!!} {!!}

-- Workaround 3: Embrace setoid hell / setoid heaven.
-- A setoid is a type together with an equivalence relation, to be used as
-- substitute for the non-existent quotient. It is our duty to not forget
-- proof obligations coming from this idea.

-- Example for a setoid: the type ℤ of integer representations together with _≈_.

-- Example for a proof obligation:
succℤ-respects-≈ : {x y : ℤ} → x ≈ y → succℤ x ≈ succℤ y
succℤ-respects-≈ = {!!}

doublesuccℤ : ℤ → ℤ
doublesuccℤ x = succℤ (succℤ x)

doublesuccℤ-respects-≈ : {x y : ℤ} → x ≈ y → doublesuccℤ x ≈ doublesuccℤ y
doublesuccℤ-respects-≈ = {!!}  -- it is a nuisance that we need to fill this in

-- Problems with setoids:
-- 1. We need to remember the proof obligations, Agda won't warn us if we forget
-- 2. The proof obligations quickly turn into a nuisance


-- Limitation 4: Vastly underspecified identity types

-- In Agda, we can verify that ¬ (ℕ ≡ Bool).
-- But in many cases, the question whether X ≡ Y, where X and Y are types (inhabitants of Set₁),
-- is, from Agda's point of view, an unresolved open question.
--
-- For instance, in standard Agda, it's an unresolved open question whether ℕ ≡ ℤ.

-- By Gödel incompleteness, we cannot expect all questions to be answerable in Agda.
-- But it's embarassing that already such a basic question is unanswerable.

-- As a teaser: In cubical Agda, we have ℕ ≡ ℤ and (ℕ , zero , +) ≢ (ℤ , zeroℤ, +ℤ).
-- In cubical Agda, we have "univalence".


-- Limitation 5: No higher-dimensional types

-- A picture of ℕ:    *     *  *  *  *  ...
-- A picture of Bool: *  *
-- A picture of List Bool: * * * * * * * * * * ...
-- These types are all zero-dimensional.

-- In standard Agda, we cannot define higher-dimensional types such as:
-- the unit interval: [--------]
-- the circle
-- ...

-- Cubical Agda natively supports higher-dimensional types, without any workarounds
-- or auxiliary definitions such as "topological space", "continuous map".
-- The definition of the circle will require three lines of cubical Agda code
-- (and this definition will NOT refer to ℝ², and it will NOT refer to the
-- equation x² + y² = 1).