-- Welcome to the Agda tutorial. :-)
-- Heavily inspired by Martín Escardó's tutorial at PC2018.
--
-- Rename this file to "something.agda".

-- Ctrl-C Ctrl-L: check code
-- Ctrl-C Ctrl-C: case split
-- Ctrl-C Ctrl-Space: check hole
-- Ctrl-C Ctrl-A: do automatically

-- \bN    ℕ
-- \alpha α
-- \to    →

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

one : ℕ
one = succ zero
-- in math: sin(5)
-- in Agda: sin 5

two : ℕ
two = succ (succ zero)

{-
add : ℕ → ℕ → ℕ
add n zero     = n
add n (succ k) = succ (add n k)
-}

_+_ : ℕ → ℕ → ℕ
n + zero     = n
n + (succ k) = succ (n + k)

-- pred : ℕ → ℕ
pred : (n : ℕ) → ℕ
pred zero     = zero
pred (succ k) = k

infix  5 _≡_
infixl 6 _+_

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

basic-lemma : _≡_ ℕ two two
basic-lemma = refl two
-}

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

basic-lemma : two ≡ one + one
basic-lemma = refl

--cong : {X : Set} → {Y : Set} → {x : X} → {x' : X} →
--  (f : X → Y) → x ≡ x' → f x ≡ f x'
cong : {X Y : Set} {x x' : X} →
  (f : X → Y) → x ≡ x' → f x ≡ f x'
cong f refl = refl

lemma : (n : ℕ) → zero + n ≡ n
-- lemma = λ n → {!!}
lemma zero     = refl
lemma (succ k) = cong succ (lemma k)
  -- lemma k : zero + k ≡ k
  -- goal    : succ (zero + k) ≡ succ k