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

data ℕ : Set where  -- \bN \to
  zero : ℕ
  succ : ℕ → ℕ
-- The inhabitants of ℕ are:
-- zero, succ zero, succ (succ zero), ...

-- in blackboard maths: f(x)
-- in Agda:             f x

one : ℕ
one = succ zero

-- For instance, pred 5 should be 4.
pred : ℕ → ℕ
pred zero     = zero
pred (succ n) = n

id : ℕ → ℕ
id zero     = zero
id (succ n) = succ n

-- For instance, double 5 should be 10.
double : ℕ → ℕ
double zero     = zero
double (succ n) = succ (succ (double n))  -- 2*(1+n) = 2+2n = 2+double(n)

data Bool : Set where
  false : Bool
  true  : Bool

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

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

addthree : ℕ → ℕ
addthree = _+_ (succ (succ (succ zero)))

-- For instance, 3 ! should be 3 * 2 * 1 = 6.
_! : ℕ → ℕ
n ! = {!!}

-- In Agda, for every x and for every y,
-- there is a type called "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 "zero ≡ zero" is inhabited.

-- This way the activities of proving and programming are unified!

-- For every x : ℕ and for every y : ℕ, the following declaration sets up
-- a type called "x ≡ y" (could be also written as "_≡_ x y")
data _≡_ : ℕ → ℕ → 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

  --bailout : zero ≡ one
  --extreme : {x : ℕ} → x ≡ succ x
  ---- would still NOT have: succ x ≡ x

lemma : zero ≡ zero  -- \==
lemma = refl

-- Logical reading: For every b : ℕ, zero + b equals b.
-- Computational reading: "insight" is a function which reads a number "b" as input
-- and outputs a witness that zero + b equals b.
insight : (b : ℕ) → (zero + b) ≡ b
insight b = refl

impossible : (b : ℕ) → (zero + b) ≡ succ b
impossible b = {!!}

-- Logical reading: For every f : ℕ → ℕ, for every a : ℕ, for every b : ℕ, if a equals b, then
-- succ a equals succ b.
-- Computational reading: "cong" is a function which inputs
-- (0) a function f : ℕ → ℕ
-- (1) a number a : ℕ
-- (2) a number b : ℕ
-- (3) a witness that a equals b
-- and outputs a witness that succ a equals succ b.
-- cong : (f : ℕ → ℕ) → {a : ℕ} → {b : ℕ} → a ≡ b → f a ≡ f b
cong : (f : ℕ → ℕ) {a b : ℕ} → a ≡ b → f a ≡ f b
cong f refl = refl

-- proof of an universal statement (∀x...) on a blackboard =
-- function which works for arbitrary inputs in Agda

-- Logical reading: For every a : ℕ, a + zero equals a.
-- Computational reading: "insight'" is a function which inputs a number a : ℕ
-- and outputs a witness that a + zero equals a.
insight' : (a : ℕ) → (a + zero) ≡ a
insight' zero     = refl
insight' (succ x) = cong succ (insight' x)

addtwo : ℕ → ℕ
-- addtwo n = succ (succ n)
addtwo = λ n → succ (succ n)
-- in Python: addtwo = lambda n: succ(succ(n))

-- the empty type
data ⊥ : Set where

-- in Agda and generally in logic: ⊥ ("bottom")
-- on a blackboard: ↯
¬_ : Set → Set
¬ A = (A → ⊥)
-- In formal logic, the definition of ¬A is that A implies a contradiction.

postulate
  bar : (x : ℕ) → addtwo x ≡ x

  oracle : (A : Set) → ¬ ¬ A → A

-- ∃ X P is the type of witnesses that there is an x : X such that P x.
-- More precisely, an inhabitant of ∃ X P is a pair (x , p)
-- consisting of an x : X and a witness p : P x.
data ∃ (X : Set) (P : X → Set) : Set where
  _,_ : (x : X) → P x → ∃ X P

-- Logical reading: There is a natural number n : ℕ such that succ n equals one.
theorem : ∃ ℕ (λ n → succ n ≡ one)  -- ∃[ n ∈ ℕ ] succ n ≡ one
theorem = zero , refl

-- proof by induction on a blackboard = definition by recursion in Agda

-- typical de Bruijn factor: formalized proofs are ten times longer
-- than blackboard proofs


{-
  Teaser: In Cubical Agda, we can define spaces (homotopy types)
  succinctly as follows:
 
  data Circle : Set where
    north : Circle
    loop  : north ≡ north

  data Segment : Set where
    left  : Segment
    right : Segment
    path  : left ≡ right
-}