{-
  Last time:
  - Agda as a programming language
  - Agda as a proof language

  This time: More on Agda as a proof language, i.e.:
  - Recap
  - Equational reasoning
  - Disjunction (∨), existential quantification (∃), conjunction (∧)
  - Well-founded recursion

  And most importantly:
  - Hands-on, supporting you with lots of exercises :-)
-}

data ℕ : Set where
  zero : ℕ
  succ : ℕ → ℕ
-- Inhabitants: zero, succ zero, succ (succ zero), succ (succ (succ zero)), ...

_+_ : ℕ → ℕ → ℕ
zero   + y = y
succ x + y = succ (x + y)

{-
data _≡_ {X : Set} : X → X → Set where
  refl : {x : X} → x ≡ x

cong : {X Y : Set} {a b : X} → (f : X → Y) → a ≡ b → f a ≡ f b
-- cong f refl = refl
cong {X} {Y} {a} {.a} f refl = refl
-- The pattern ".a" matches the contents of the variable "a" without introducing a new variable.

trans : {X : Set} {a b c : X} → a ≡ b → b ≡ c → a ≡ c
trans refl q = q
-}

open import Padova2025.ProvingBasics.Equality.Base
open import Padova2025.ProvingBasics.Equality.General

-- Logical reading: For all number y, it holds that y equals y + zero.
-- Computational reading: "+-zero" is a function which inputs a number y and which outputs
-- a witness that y equals y + zero.
+-zero : (y : ℕ) → y ≡ (y + zero)
+-zero zero     = refl   -- "This holds trivially, by a mere computation / by definition."
+-zero (succ y) = cong succ (+-zero y)

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

open import Padova2025.ProvingBasics.Equality.Reasoning.Core

-- Logical reading: For all numbers x, for all numbers y, it holds that x + y equals y + x.
-- Computational reading: "+-comm" is a function which reads as input two numbers x and y,
-- and which outputs a witness that x + y equals y + x.
+-comm : (x : ℕ) → (y : ℕ) → (x + y) ≡ (y + x)
-- +-comm x y = refl
+-comm zero     y = +-zero y
+-comm (succ a) y = trans (+-succ a y) (trans (+-comm a (succ y)) (+-succ y a))
-- A more beautiful way of writing down this proof is using "equational reasoning".

+-comm' : (a b : ℕ) → (a + b) ≡ (b + a)
+-comm' zero     b = +-zero b
+-comm' (succ a) b = begin
  succ a + b   ≡⟨ refl ⟩
  succ (a + b) ≡⟨ +-succ a b         ⟩
  a + succ b   ≡⟨ +-comm' a (succ b) ⟩
  succ (b + a) ≡⟨ +-succ b a         ⟩
  b + succ a ∎

+-comm'' : (a b : ℕ) → (a + b) ≡ (b + a)
+-comm'' zero     b = +-zero b
+-comm'' (succ a) b = begin
  succ a + b   ≡⟨⟩
  succ (a + b) ≡⟨ +-succ a b          ⟩       -- \u{} 
  a + succ b   ≡⟨ +-comm'' a (succ b) ⟩
  succ (b + a) ≡⟨ +-succ b a          ⟩
  b + succ a   ∎