{-# OPTIONS --cubical --allow-unsolved-metas #-}
module AFF2024.AgdaTutorial.Session2 where

data ℕ : Set where  -- \bN \alpha \to
  zero : ℕ
  succ : ℕ → ℕ
-- Inhabitants of ℕ:
-- zero, succ zero, succ (succ zero), ...

--{-# BUILTIN NATURAL ℕ #-} 

data Bool : Set where
  false : Bool
  true  : Bool

-- in blackboard mathematics: f(x,y)
-- in Agda:                   f x y

one : ℕ
one = succ zero

-- For instance, pred of 7 should be 6.
pred : ℕ → ℕ
pred zero     = zero
pred (succ x) = x

-- For instance, double 7 should be 14.
double : ℕ → ℕ
double zero     = zero
double (succ x) = succ (succ (double x))   -- 2*(1+x) = 2+2x = 1+(1+2x) = 1+(1+double(x))

_·2 : ℕ → ℕ
x ·2 = double x

-- for instance, 3 ! should be 6.
_! : ℕ → ℕ
_! = {!!}

!_ : (b : Bool) → Bool
! false = true
! true  = false

{-
_foo_bar_ : X → Y → Z → A
x foo y bar z = ?

0 + x + y ≡⟨ comm x y ⟩ 0 + y + x ≡⟨ neutr ⟩ y + x
-}

fun : Bool → Set
fun false = ℕ
fun true  = Bool

bar : (b : Bool) → fun b
bar false = succ (succ (succ (succ (succ (succ zero)))))
bar true  = false

-- The following declaration sets up a type/set called "x ≡ y", for each x : ℕ, y : ℕ.
data _≡_ {X : Set} : X → X → Set where
  -- logical reading: for every x : ℕ, x equals x.
  -- computational reading: "refl" is a function which inputs a number x : ℕ
  -- and outputs a witness that x equals x.
  refl : {x : X} → x ≡ x
  -- bailout : {x y : ℕ} → x ≡ y
  -- bogus : {x : ℕ} → x ≡ succ (succ x)

-- In Agda, for every two numbers "x" and "y", there is a type/set "x ≡ y".
-- The inhabitants of this type are witnesses that "x" and "y" are equal.
-- For instance, the type "zero ≡ one" is empty.
-- In constrast, the type "one ≡ one" is inhabited (namely by "refl").
tem : zero ≡ zero   -- \==
tem = refl

tem' : bar false ≡ succ (succ (succ (succ (succ (succ zero)))))
tem' = refl

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

-- logical reading: for every y : ℕ, zero + y equals y.
-- computational reading: "lemma" is a function which inputs a number y : ℕ
-- and outputs a witness that zero + y equals y.
lemma : (y : ℕ) → (zero + y) ≡ y
lemma y = refl

-- logical reading: for every set A, for every set B, for every function f : A → B,
-- for every elements x, y : A, if x equals y, then f x equals f y.
-- computational reading: "cong" is a function which takes 6 inputs, namely
-- 1. a set A
-- 2. a set B
-- 3. a function f : A → B
-- 4. a value/element/inhabitant x : A
-- 5. a value y : A
-- 6. a witness that x equals y
-- and outputs a witness that f x equals f y.
cong : {A B : Set} (f : A → B) {x y : A} → x ≡ y → f x ≡ f y
cong f refl = refl

data ⊥ : Set where

¬_ : Set → Set
¬ A = A → ⊥
-- "¬ A" means (by definition): The assumption that A implies a contradiction.

postulate
  double-negation-elimination : {A : Set} → ¬ ¬ A → A

lemma' : (x : ℕ) → (x + zero) ≡ x
lemma' zero     = refl
lemma' (succ a) = cong succ (lemma' a)

-- induction on a blackboard = recursion in Agda

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

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

---------------------------------------------------------------------------------
-- syntax for equational proofs, please ignore these definitions on first reading
infix   _∎
infixr  _≡⟨_⟩_ _≡⟨⟩_
infix   begin_

_≡⟨_⟩_ : {A : Set} {y z : A} → (x : A) → x ≡ y → y ≡ z → x ≡ z
x ≡⟨ p ⟩ q = trans p q

_≡⟨⟩_ : {A : Set} {y : A} → (x : A) → (q : x ≡ y) → x ≡ y
x ≡⟨⟩ q = q

_∎ : {A : Set} → (x : A) → x ≡ x
x ∎ = refl

begin_ : {A : Set} {x y : A} → x ≡ y → x ≡ y
begin p = p
-- end of syntax for equational proof
---------------------------------------------------------------------------------

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

-- logical reading: for every x : ℕ, for every y : ℕ, x + y equals y + x.
-- computational reading: "comm" is a function which inputs a number x : ℕ
-- and a number y : ℕ and outputs a witness that x + y equals y + x.
comm : (x : ℕ) → (y : ℕ) → (x + y) ≡ (y + x)
comm zero     y = symm (lemma' y)
-- comm (succ x) y = trans (symm (lemma-succ x y)) (trans (comm x (succ y)) (symm (lemma-succ y x)))
comm (succ x) y = begin
  succ x + y   ≡⟨⟩          -- \==\<\>
  succ (x + y) ≡⟨ symm (lemma-succ x y) ⟩
  x + succ y   ≡⟨ comm x (succ y) ⟩
  succ y + x   ≡⟨ symm (lemma-succ y x) ⟩
  y + succ x   ∎  -- \qed

lemma'' : (x : ℕ) → (x + zero) ≡ x
lemma'' x = double-negation-elimination {!!}