Chuangjie Xu 2011, with changes by Martin Escardo later.

\begin{code}

{-# OPTIONS --safe --without-K --exact-split #-}

open import MLTT.Spartan hiding (_+_)
open import Naturals.Properties

infixl 31 _+_

_+_ : ℕ → ℕ → ℕ
n + 0 = n
n + (succ m) = succ (n + m)

_+ᴸ_ : ℕ → ℕ → ℕ
m +ᴸ n = n + m

{-# BUILTIN NATPLUS _+_ #-}

zero-right-neutral : (n : ℕ) → n + 0 ＝ n
zero-right-neutral n = refl

zero-left-neutral : (n : ℕ) → 0 + n ＝ n
zero-left-neutral = induction base step
where
base : 0 + 0 ＝ 0
base = refl

step : (n : ℕ) → 0 + n ＝ n → 0 + succ n ＝ succ n
step n IH = 0 + succ n   ＝⟨ refl ⟩
succ (0 + n) ＝⟨ ap succ IH ⟩
succ n       ∎

addition-associativity : (l n m : ℕ) → (l + n) + m ＝ l + (n + m)
addition-associativity l n = induction base step
where
base : (l + n) + 0 ＝ l + (n + 0)
base = (l + n) + 0  ＝⟨ refl ⟩
l + n       ＝⟨ refl ⟩
l + (n + 0) ∎

step : (m : ℕ) → (l + n) + m ＝ l + (n + m)
→ (l + n) + succ m ＝ l + (n + succ m)
step m IH = (l + n) + succ m   ＝⟨ refl ⟩
succ ((l + n) + m) ＝⟨ ap succ IH ⟩
succ (l + (n + m)) ＝⟨ refl ⟩
l + succ (n + m)   ＝⟨ refl ⟩
l + (n + succ m)   ∎

addition-commutativity : (n m : ℕ) → n + m ＝ m + n
addition-commutativity n = induction base step
where
base : n + 0 ＝ 0 + n
base = n + 0 ＝⟨ zero-right-neutral n ⟩
n     ＝⟨ (zero-left-neutral n)⁻¹ ⟩
0 + n ∎

step : (m : ℕ) → n + m ＝ m + n → n + succ m ＝ succ m + n
step m IH = n + succ m   ＝⟨ refl ⟩
succ (n + m) ＝⟨ ap succ IH ⟩
succ (m + n) ＝⟨ lemma₀ (m + n) ⟩
1 + (m + n)  ＝⟨ (addition-associativity 1 m n)⁻¹ ⟩
(1 + m) + n  ＝⟨ ap (_+ n) ((lemma₀ m)⁻¹) ⟩
succ m + n   ∎
where
lemma₀ : (k : ℕ) → succ k ＝ 1 + k
lemma₀ = induction base₀ step₀
where
base₀ : succ 0 ＝ 1 + 0
base₀ = refl

step₀ : (k : ℕ) → succ k ＝ 1 + k → succ (succ k) ＝ 1 + succ k
step₀ k IH = succ (succ k) ＝⟨ ap succ IH ⟩
succ (1 + k)  ＝⟨ refl ⟩
1 + succ k    ∎

trivial-addition-rearrangement : (x y z : ℕ) → x + y + z ＝ x + z + y
(x + y) + z ＝⟨ addition-associativity x y z ⟩
x + (y + z) ＝⟨ ap (x +_) (addition-commutativity y z) ⟩
x + (z + y) ＝⟨ (addition-associativity x z y)⁻¹ ⟩
(x + z) + y ∎

\end{code}

Some more simple properties of addition. The proofs all use induction,
apart from addition-right-cancellable which follows from

\begin{code}

succ-right : (x y : ℕ) → x + succ y ＝ succ (x + y)
succ-right x y = refl

succ-left : (x y : ℕ) → succ x + y ＝ succ (x + y)
succ-left x = induction base step
where
base : succ x + 0 ＝ succ (x + 0)
base = succ x + 0   ＝⟨ refl         ⟩
succ x       ＝⟨ ap succ refl ⟩
succ (x + 0) ∎

step : (k : ℕ)
→ succ x + k ＝ succ (x + k)
→ succ x + succ k ＝ succ (x + succ k)
step k IH = succ x + succ k     ＝⟨ refl       ⟩
succ (succ x + k)   ＝⟨ ap succ IH ⟩
succ (succ (x + k)) ＝⟨ refl       ⟩
succ (x + succ k)   ∎

addition-left-cancellable : (x y z : ℕ) → z + x ＝ z + y → x ＝ y
addition-left-cancellable x y = induction base step
where
base : 0 + x ＝ 0 + y → x ＝ y
base h = x      ＝⟨ zero-left-neutral x ⁻¹ ⟩
0 + x  ＝⟨ h                      ⟩
0 + y  ＝⟨ zero-left-neutral y    ⟩
y ∎

step : (k : ℕ)
→ (k + x      ＝ k + y      → x ＝ y)
→ (succ k + x ＝ succ k + y → x ＝ y)
step k IH r = IH (succ-lc (lemma₁ r))
where
lemma₁ : succ k + x ＝ succ k + y → succ (k + x) ＝ succ (k + y)
lemma₁ r = succ (k + x)           ＝⟨ succ-left k x ⁻¹ ⟩
succ k + x             ＝⟨ r                ⟩
succ k + y             ＝⟨ succ-left k y    ⟩
succ (k + y) ∎

addition-right-cancellable : (x y z : ℕ) → x + z ＝ y + z → x ＝ y
where
lemma₀ : z + x ＝ z + y
lemma₀ = z + x      ＝⟨ addition-commutativity z x ⟩
x + z      ＝⟨ r                          ⟩
y + z      ＝⟨ addition-commutativity y z ⟩
z + y ∎

\end{code}

We also have that if the sum of two numbers are zero, then the right
argument is zero. The left argument is zero, which can be proved using
commutativity of addition. This function is needed in the HCF file.

\begin{code}

sum-to-zero-gives-zero : (x y : ℕ) → x + y ＝ 0 → y ＝ 0
sum-to-zero-gives-zero x 0        e = refl
sum-to-zero-gives-zero x (succ y) e = 𝟘-elim (positive-not-zero (x + y) e)

\end{code}