module NatProofs where

open import Nat
open import Identity  

-- proving associativity of plus using pattern matching

associativity-plus : (m n p : Nat) → ((m + n) + p) ≡ (m + (n + p))
associativity-plus zero     n p = refl
associativity-plus (succ y) n p = cong succ (associativity-plus y n p)

-- the induction axiom is a dependently typed combinator for primitive recursion (by Curry-Howard)

natind : {C : Nat -> Set} -> C zero -> ((n : Nat) -> C n -> C (succ n)) -> (n : Nat) -> C n
natind d e zero     = d
natind d e (succ n) = e n (natind d e n)

-- proving associativity using the induction axiom

associativity-plus-ind : (m n p : Nat) → ((m + n) + p) ≡ (m + (n + p))
associativity-plus-ind m n p = natind {\m → ((m + n) + p) ≡ (m + (n + p))} refl (λ q r → cong succ r) m

-- note that the two proofs are essentially the same! 
-- Pattern matching provides "syntactic sugar" for primitive recursion, 
-- but also possibility for more general recursion schemes than primitive recursion