{-# OPTIONS --allow-unsolved-metas #-}
{-
  Session 3

  Proposal for today:
  - equational reasoning
  - logical connectives: ¬, ∨, ∃, ∧
  - (perhaps) termination

  Proposal for tomorrow:
  - (perhaps) program verification
  - (perhaps) computational content of classical logic
-}

-- Shortcut to move to the next hole: C-c C-f

data ℕ : Set where
  zero : ℕ
  succ : ℕ → ℕ

_+_ : ℕ → ℕ → ℕ
zero   + b = b
succ a + b = succ (a + b)

open import Padova2025.ProvingBasics.Equality.Base
open import Padova2025.ProvingBasics.Equality.Reasoning.Core

two : ℕ
two = succ (succ zero)

four : ℕ
four = succ (succ (succ (succ zero)))

grande-teorema : (two + two) ≡ four
grande-teorema = refl

cong : {X Y : Set} {a b : X} (f : X → Y) → a ≡ b → f a ≡ f b
cong f refl = refl

sym : {X : Set} {a b : X} → a ≡ b → b ≡ a
sym refl = refl

+-zero : (y : ℕ) → (y + zero) ≡ y
+-zero zero     = refl
+-zero (succ y) = cong succ (+-zero y)

+-succ : (x y : ℕ) → (x + succ y) ≡ succ (x + y)
+-succ zero     y = refl
+-succ (succ x) y = cong succ (+-succ x y)

-- Agda is a calculator, but not for numbers, and instead for logic!

trans : {X : Set} {a b c : X} → a ≡ b → b ≡ c → a ≡ c
trans = {!!}

+-comm : (x y : ℕ) → (x + y) ≡ (y + x)
+-comm zero     y = sym (+-zero y)
+-comm (succ x) y = trans (sym (+-succ x y)) (trans (+-comm x (succ y)) (sym (+-succ y x)))

+-comm' : (x y : ℕ) → (x + y) ≡ (y + x)
+-comm' zero     y = sym (+-zero y)
+-comm' (succ x) y = begin
  (succ x + y) ≡⟨⟩     -- \< \>
  succ (x + y) ≡˘⟨ +-succ x y ⟩  -- \u{}
  x + succ y   ≡⟨ +-comm' x (succ y) ⟩
  succ (y + x) ≡˘⟨ +-succ y x ⟩
  y + succ x   ∎             -- \qed
-- This style of proving is called "equational reasoning".

data Even : ℕ → Set where
  base-even : Even zero
  step-even : {n : ℕ} → Even n → Even (succ (succ n))

-- Logical reading: For all numbers x, for all numbers y, if x equals y, and if x is even, then y is even.
-- Computational reading: `lemma` is a function which inputs
-- 1. a number x
-- 2. a number y
-- 3. a witness that x equals y
-- 4. a witness that x is even
-- and outputs a witness that y is even.
lemma : {x y : ℕ} → x ≡ y → Even x → Even y
lemma refl q = q

subst : {A : Set} {P : A → Set} {x y : A} → x ≡ y → P x → P y
subst refl q = q
-- `lemma` is the special case of `subst` where `P` is instantiated with `Even`.

-- Option 1: Immediately proceed with the logical connectives ¬, ∨, ...
-- Option 2: Exercises with equational reasoning

-- In logic, we define ¬A as "A implies a contradiction".
-- Formally, we often write "⊥" instead of "contradiction".

-- There is a type of witnesses of contradiction.
data ⊥ : Set where   -- \bot
-- This type is manifestly empty, corresponding to the idea that a contradiction
-- should not have any witnesses.

one : ℕ
one = succ zero

-- "one is not zero"
-- Logical reading: "If one is zero, then ⊥"
-- Computational reading: `theorem` is a function which inputs an (alleged)
-- witness that one equals zero and outputs a witness of ⊥.
theorem : one ≡ zero → ⊥
theorem ()
-- "The empty pattern". This signifies that there are no cases.

one-not-even : Even one → ⊥
one-not-even ()

¬_ : Set → Set
¬ X = (X → ⊥)

one-not-even' : ¬ Even one
one-not-even' = one-not-even

-- Fermat's last theorem: For all positive natural numbers a, b, c, n with n ≥ 3, it is not the case that aⁿ + bⁿ = cⁿ.
-- Fermat's last theorem: For all positive natural numbers a, b, c, n with n ≥ 3, if aⁿ + bⁿ = cⁿ then ⊥.