module Naturals where

--- natural numbers
--- 0, 1, 2,3, ...

--- type of natural numbers
--- ℕ (set of natural numbers)

--- 0 : ℕ, 1 : ℕ , 2 : ℕ, ...
--- Peano axioms
--- inductive definition

--- base case: zero : ℕ

--- inductive case : given n : ℕ construct a new one by taking the successor (suc n) : ℕ

--- iterating this definition:
--- zero : ℕ
--- suc zero : ℕ
--- suc (suc zero) : ℕ
--- suc (suc (suc zero)) : ℕ

--- base case - axiom:
---   zero : ℕ

--- inductive case - rule:
---   n : ℕ
--- -----------
---  suc n : ℕ

data ℕ : Set where

  zero : ℕ

  suc : (n : ℕ) → ℕ

{-
zero : ℕ
zero = minus-1
-}

one : ℕ
one = suc zero

two : ℕ
two = suc one

three : ℕ
three = suc two

{-# BUILTIN NATURAL ℕ #-}
-- this pragma check that the definition of ℕ has one axiom (and takes the name of the axiom for 0)
-- and that it ahs one unary rule and takes that for successor.
-- names of the axiom / rule do not matter

_ : ℕ
_ = 42

-- exploit the inductive definition as a means to define functions on ℕ

-- (1 + m) + n = 1 + (m + n) by associativity

_+_ : ℕ → ℕ → ℕ
zero + n = n
(suc m) + n = suc (m + n)

import Relation.Binary.PropositionalEquality as Eq
open Eq using (_≡_; refl)
open Eq.≡-Reasoning using (begin_; _≡⟨⟩_; _∎)

_ : 0 + 3 ≡ 3
_ = refl

-- see tomorrow's lecture on inductive proofs
_ : ∀ n → n + 0 ≡ n
_ = {!!}

_ : 2 + 3 ≡ 5  -- also definitional equality
_ = begin
  (2 + 3) ≡⟨⟩
  (suc (suc zero) + suc (suc (suc zero))) ≡⟨⟩
  (suc (suc zero + suc (suc (suc zero)))) ≡⟨⟩
  (suc (suc (zero + suc (suc (suc zero))))) ≡⟨⟩
  (suc (suc (suc (suc (suc zero))))) ≡⟨⟩
  5
  ∎

_ : 2 + 3 ≡ 5
_ = refl

-- multiplication
-- again defined inductively on the first argument

_*_ : ℕ → ℕ → ℕ
zero * n = zero
(suc m) * n = n + (m * n)

_ : 2 * 3 ≡ 6
_ = begin ((2 * 3) ≡⟨⟩
    (((suc (suc zero)) * 3) ≡⟨⟩ 
    ((3 + ((suc zero) * 3)) ≡⟨⟩ 
    ((3 + (3 + (zero * 3))) ≡⟨⟩ 
    ((3 + (3 + zero)) ≡⟨⟩ 
    (6 
    ∎))))))

-- subtraction
-- again defined inductively on the first argument
-- caveat: every function in Agda must be total (defined for all arguments)
-- here we are going to cut off subtraction at 0, this operation is called `monus`

_∸_ : ℕ → ℕ → ℕ
zero ∸ n = zero
suc m ∸ zero = suc m
suc m ∸ suc n = m ∸ n

_ : 2 ∸ 3 ≡ 0
_ = begin
  (2 ∸ 3) ≡⟨⟩ 
  (((suc (suc zero)) ∸ (suc (suc (suc zero)))) ≡⟨⟩ 
  (((suc zero) ∸ (suc (suc zero))) ≡⟨⟩ 
  (zero ∸ (suc zero)) ≡⟨⟩ 
  (zero ≡⟨⟩ 
  (0 ∎))))

-- a glimpse of inductive proof (preview to next lecture)

-- first proof:
-- establish that 0 is neutral element for addition _+_

-- 1. for all n : ℕ, 0 + n ≡ n (left identity)
-- 2. for all n : ℕ, n + 0 ≡ n (right identity)

0+n=n : ∀ (n : ℕ) → 0 + n ≡ n
0+n=n n = refl

m=n->sm=sn : ∀ (m n : ℕ) → m ≡ n → suc m ≡ suc n
m=n->sm=sn m n refl = refl

n+0=n : ∀ (n : ℕ) → n + 0 ≡ n
n+0=n zero = refl
n+0=n (suc n) = m=n->sm=sn (n + 0) n (n+0=n n)