-- Note: Turing machines and lambda calculus are NOT equivalent
-- models of computation as soon as we go beyond first-order functions ℕ → ℕ
-- to higher-order functions (such as functions of type (ℕ → ℕ) → ℕ).
--
-- The reason is that a higher-order Turing machine (ℕ → ℕ) → ℕ is given as input
-- the source code for a Turing machine of type ℕ → ℕ.
--
-- In contrast, a higher-order lambda term of type (ℕ → ℕ) → ℕ is given
-- the input function only as a blackbox, without the source code.

----------

-- Peano arithmetic (PA) is a formal system for expressing
-- and proving statements about natural numbers.

-- Ingredients:
-- Z   zero
-- S   succ
-- +
-- ·

open import Padova2025.ProgrammingBasics.Naturals.Base
open import Padova2025.ProgrammingBasics.Naturals.Arithmetic
open import Padova2025.ProvingBasics.Negation
open import Padova2025.ProvingBasics.Equality.Base
open import Padova2025.ProvingBasics.Connectives.Conjunction
open import Padova2025.ProvingBasics.Connectives.Disjunction
open import Padova2025.ProvingBasics.Termination.Gas using (𝟙; tt)

-- "Fin n" will be an Agda datatype consisting of exactly n many inhabitants.
data Fin : ℕ → Set where
  zero : {n : ℕ} → Fin (succ n)          -- "zero is smaller than succ n, for any n"
  succ : {n : ℕ} → Fin n → Fin (succ n)  -- "if x is smaller than n, then succ x is smaller than succ n"

module _ where private  -- temporary scratch pad
  example-1 : Fin three
  example-1 = zero

  example-2 : Fin three
  example-2 = succ zero

  example-3 : Fin three
  example-3 = succ (succ zero)

  -- example-4 : Fin three
  -- example-4 = succ (succ (succ zero))
  -- should not and does not work

-- Agda datatype of PA terms, more precisely "Term n" will be
-- the Agda datatype of PA terms in which the variables 0, 1, ..., n-1
-- may occur.
data Term (n : ℕ) : Set where
  Z   : Term n
  S   : Term n → Term n
  _⊕_ : Term n → Term n → Term n
  _⊛_ : Term n → Term n → Term n
  var : Fin n → Term n

-- Agda datatype of PA formulas, more precisely "Form n" will be
-- the Agda datatype of PA formulas in which the variables 0, 1, ..., n-1
-- may occur.
data Form (n : ℕ) : Set where
  _∧_ : Form n → Form n → Form n
  _∨_ : Form n → Form n → Form n
  _⇒_ : Form n → Form n → Form n
  top : Form n
  bot : Form n
  fa  : Form (succ n) → Form n    -- ∀
  ex  : Form (succ n) → Form n    -- ∃
  _≈_ : Term n → Term n → Form n
-- Strictly speaking we don't need the _⇒_ constructor, as we could
-- also define (α ⇒ β) as (¬ α ∨ β).

example-commutativity : Form zero
example-commutativity =
  fa (fa ((var (succ zero) ⊕ var zero) ≈ (var zero ⊕ var (succ zero))))
-- ∀x. ∀y. x + y = y + x

-- parse : String → Form n
-- parse "∀x. ∀y. x + y = y + x"

-- We don't need negation as a constructor, as we can define it:
neg : {n : ℕ} → Form n → Form n
neg φ = (φ ⇒ bot)

-- The formula "∀x. ∀y. x + y = y + x" would be regarded as well-formed,
-- but the formula "∀x. ∀y. x + a = y + x" would not.

-- Axioms:
-- ∀x. Z + x = x
-- induction scheme: (P(Z) ∧ (∀n. P(n) ⇒ P(S(n)))) ⇒ ∀n. P(n)
-- (one axiom for each formula P)
-- ...

-- Inference rules:
-- P ⊢ P        ("from P, we may conclude P")
-- P ∧ Q ⊢ P    ("from P ∧ Q, we may conclude P")
-- ⊤ ⊢ P ∨ ¬ P  ("from ⊤, we may conclude the law of excluded middle for P")
-- ...

data _⊢_ : {n : ℕ} → Form n → Form n → Set where
  identity   : {n : ℕ} {φ : Form n}     → φ ⊢ φ
  conj-elimₗ : {n : ℕ} {α β : Form n}   → (α ∧ β) ⊢ α
  conj-elimᵣ : {n : ℕ} {α β : Form n}   → (α ∧ β) ⊢ β
  cut        : {n : ℕ} {α β γ : Form n} → (α ⊢ β) → (β ⊢ γ) → (α ⊢ γ)
  -- ...

-- Let us verify that HA is consistent, i.e. that HA does NOT prove ⊤ ⊢ Z ≈ S Z.
-- We do that by exhibiting a model.

Env : ℕ → Set
Env n = Fin n → ℕ
-- "Env n" is the type of environments, specifying an actual value
-- for each of the variables 0, ..., n-1.

-- "eval φ" should be the Agda truth value of the HA-formula φ.
-- For instance, the type "eval example-commutativity" should be inhabited,
-- by a witness that addition of natural numbers is commutative.
-- In constrast, the type "eval bot" should be empty.

eval₀ : {n : ℕ} → Env n → Term n → ℕ
eval₀ env Z       = zero
eval₀ env (S x)   = succ (eval₀ env x)
eval₀ env (x ⊕ y) = eval₀ env x + eval₀ env y
eval₀ env (x ⊛ y) = {!!}
eval₀ env (var v) = env v

eval : {n : ℕ} → Env n → Form n → Set
eval env (φ ∧ ψ) = eval env φ × eval env ψ
eval env (φ ∨ ψ) = eval env φ ⊎ eval env ψ
eval env (φ ⇒ ψ) = eval env φ → eval env ψ
eval env top     = 𝟙      -- data 𝟙 : Set where tt : 𝟙
eval env bot     = ⊥
eval env (fa φ)  = (x : ℕ) → eval (λ { zero → x ; (succ v) → env v }) φ
eval env (ex φ)  = {!!}
eval env (x ≈ y) = eval₀ env x ≡ eval₀ env y

-- Let us prove soundness: If PA proves α ⊢ β, then α actually implies β.
sound : {n : ℕ} (α β : Form n) (env : Env n) → (α ⊢ β) → (eval env α → eval env β)
sound α β env identity   = λ z → z
sound α β env conj-elimₗ = fst
sound α β env conj-elimᵣ = {!!}
sound α β env (cut p q)  = λ z → sound _ β env q (sound α _ env p z)

consistency : ¬ (top ⊢ (Z ≈ S Z))
consistency p with sound _ _ _ p tt
... | ()

{-
  ZFC
   |
   ZF
   |  \
   |    IZF
   |     |
   |     |
   PA    |
   |  \  |
   |    HA                         PRA + QF-TI(ε₀)
   |                                    |
   PRA primitive recursive arithmetic---+

  The consistency of PA can be proven in:
  - ZFC, ZF, IZF, ...
  - PRA + QF-TI(ε₀)  "quantifier-free transfinite induction up to ε₀"

  The consistency of ZFC can be proven in:
  - PRA + QF-TI(???),  where we are currently lacking the technology
                       to describe ???
-}

{-
example-higher-order-function : (ℕ → ℕ) → ℕ
example-higher-order-function f = f three + f four
-}

-- Possible follow-up projects:
-- 1. Define Heyting arithmetic (HA), the constructive variant of Peano arithmetic
-- 2. Prove that, if PA proves that some Turing machine terminates, then
--    HA also proves that this Turing machine terminates.
-- 3. Prove that, if PA proves a formula of the form "∀x ∃y P(x,y)", then
--    HA does as well (provided that no further quantifiers appear in P).