module NatProofs where

open import Nat
open import Identity
open import PropositionalLogic

{-
We shall now show how to prove a property (associativity of addition) of natural numbers by induction. We first show how to write the proof by pattern matching:
-}

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

{-
Using propositions as types we can prove the general principle of mathematical induction:
-}

natind : {P : Nat -> Set} -> P zero -> ((n : Nat) -> P n -> P (succ n)) -> (n : Nat) -> P n
natind base step zero     = base
natind base step (succ n) = step n (natind base step n)

{-
We can use this principle to prove associativity of addition without pattern matching:
-}

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

{-
Note that the two proofs are essentially the same! They are fundamentally just two different ways of expressing the same thing. Pattern matching provides "syntactic sugar" for definitions by primitive recursion, but it also opens the possibility for more general recursion schemes than primitive recursion.

The induction axiom is one of Peano's axioms for arithmetic (see wikipedia). Another is the following:
-}

peano-4 : (n : Nat) → ¬ (zero ≡ succ n)
peano-4 n = {!!}

{-
We can prove all Peano's axioms from our definition of Nat
-}