-- The `Set` of natural numbers is defined as
data Nat : Set where
  zero : Nat
  succ : Nat → Nat

-- which corresponds to th signature Σ = {zero/0 , succ/1}

two : Nat
two = succ (succ zero)

-- this allows us to write `2` instead of `succ (succ zero)`
{-# BUILTIN NATURAL Nat #-}

two' : Nat
two' = 2

-- We declare a function `plus` to be of type `Nat → Nat → Nat`
-- Note that A×B → C ≅ A → B → C     (currying)
plus : Nat → Nat → Nat
-- Now we give a definition via recursion over the first parameter
-- Notice how this corresponds to a term rewriting system
plus zero m = m
plus (succ n) m = succ (plus n m)

-- Agda allows great liberty in naming of variables.  _+_ tells the
-- system that `+` is a (curried) binary function that takes one
-- argument to the left and one argument to the right.
_+_ : Nat → Nat → Nat
zero + m = m
succ n + m = succ (n + m)

--------------------------------------------------------------------------------
-- Now that we have naturals and additions, we want to prove theorems
-- about them.

-- We can reason about equality with the definitions from the standard-libary:
import Relation.Binary.PropositionalEquality as Eq
open Eq using (_≡_; refl)
open Eq.≡-Reasoning

{-
We can ignore the details of this for now, just note that
* `a ≡ b` represents the proposition that "a is equal to b"
* `refl` is a proof that for any `a`, `a ≡ a`
* we can for chains of equalities:
  `begin a ≡⟨ p ⟩ b ≡⟨ q ⟩ c ∎` is a proof that `a ≡ c` given that
   * `p` is a proof of `a ≡ b`
   * `q` is a proof of `b ≡ c`

  (i.e. `_≡_` is transitive)
-}     

-- Now this proof looks remarkably like a reduction sequence of a term rewriting system
l : 4 + 2 ≡ 6
l = begin
  (4 + 2) ≡⟨⟩
  succ (3 + 2) ≡⟨⟩
  succ (succ (2 + 2)) ≡⟨⟩
  succ (succ (succ (1 + 2))) ≡⟨⟩
  succ (succ (succ (succ (0 + 2)))) ≡⟨⟩
  succ (succ (succ (succ 2))) ≡⟨⟩
  6 ∎

{-
The trs for _+_ that we specified is strongly normalizing and confluent ⇒ normal forms are unique!
Agda evaluates these normal forms on both side of the equality:
* `4 + 2` has the normal form `6`
* `6` is already normal

The proof for `4 + 2 ≡ 6` thus turns into a proof of `6 ≡ 6`.
But that is easy! It is already given by reflexivity (`refl`) of `_≡_`.
-}
l' : 4 + 2 ≡ 6
l' = refl