module PLFA.Induction where

open import Data.Nat using (ℕ; suc; zero; _+_; _*_; _∸_)

import Relation.Binary.PropositionalEquality as Eq
open Eq using (_≡_; refl; cong; sym)
open Eq.≡-Reasoning


-- properties of operators on ℕ
-- operators _+_; _*_; _∸_
-- identity, associativity, commutativity, distributivity

-- identity: for all n ∈ ℕ, n + 0 ≡ n ≡ 0 + n
-- +-identityʳ : ∀ n → n + 0 ≡ n
-- +-identityˡ : ∀ n → 0 + n ≡ n

-- associativity: for all m, n, p in ℕ, (m + n) + p ≡ m + (n + p)

-- commutativity: for all m, n ∈ ℕ, m + n ≡ n + m

-- distributivity: for all m, n, p ∈ ℕ, (m + n) * p ≡ (m * p) + (n * p)

-- induction, to prove properties for all natural numbers

-- recall their definition

-- axiom:
--       zero : ℕ
-- inference rule:
--       n : ℕ →
--  ---------------
--   suc n : ℕ

-- any n : ℕ is reachable by using axiom zero (once) and then finitely often the rule for suc.

-- back to induction
-- let's say we want to prove property P for all natural numbers
-- so we write
--    ∀ (n : ℕ) → P n

-- the principle of induction tells us:

-- if  P zero
-- and (∀ n → (IH : P n) → P (suc n))
-- then (∀ n → P n)

-- to this end, consider
-- proveP : ∀ (n : ℕ) → P n
-- proveP zero = P zero
-- proveP (suc n) = ... assume (IH : P n) by using (IH = proveP n) ...


-- associativity

_ : (5 + 6) + 7 ≡ 5 + (6 + 7)
_ = 
  begin
    (5 + 6) + 7
  ≡⟨⟩
    11 + 7
  ≡⟨⟩
    18
  ≡⟨⟩
    5 + 13
  ≡⟨⟩
    5 + (6 + 7)
  ∎

-- proof by induction

+-assoc : ∀ (m n p : ℕ) → (m + n) + p ≡ m + (n + p)
+-assoc zero    n p = 
  begin 
    (zero + n) + p 
  ≡⟨⟩
    n + p
  ≡⟨⟩
    zero + (n + p)
  ∎
+-assoc (suc m) n p =
  begin 
    (suc m + n) + p 
  ≡⟨⟩
    suc (m + n) + p
  ≡⟨⟩
    suc ((m + n) + p)
  ≡⟨ cong suc (+-assoc m n p) ⟩
    suc (m + (n + p))
  ≡⟨⟩
    suc m + (n + p)
  ∎ 

-- commutativity

-- requires two lemmas that we discover when attempting to prove +-comm

+-identityʳ : ∀ n → n ≡ n + zero
+-identityʳ zero = refl
+-identityʳ (suc n) = cong suc (+-identityʳ n)

+-suc : ∀ n m → suc (n + m) ≡ n + suc m
+-suc zero m = refl -- alternative: begin suc (zero + m) ≡⟨⟩ suc m ≡⟨⟩ zero + suc m ∎
+-suc (suc n) m = cong suc (+-suc n m)

-- the actual result

+-comm : ∀ (m n : ℕ) → m + n ≡ n + m
+-comm zero n = 
  +-identityʳ n
+-comm (suc m) n = 
  begin
    suc (m + n)
  ≡⟨ cong suc (+-comm m n) ⟩ 
    suc (n + m)
  ≡⟨ +-suc n m ⟩
    n + suc m
  ∎

-- using rewrite (a more concise way of writing these proofs)

+-assoc' : ∀ m n p → (m + n) + p ≡ m + (n + p)
+-assoc' zero n p = refl
+-assoc' (suc m) n p rewrite +-assoc' m n p = refl

+-identityʳ' : ∀ n → n ≡ n + zero
+-identityʳ' zero = refl
+-identityʳ' (suc n) rewrite sym (+-identityʳ' n) = refl

+-suc' : ∀ n m → suc (n + m) ≡ n + suc m
+-suc' zero m = refl
+-suc' (suc n) m rewrite +-suc' n m = refl

+-comm' :  ∀ (m n : ℕ) → m + n ≡ n + m
+-comm' zero n = +-identityʳ' n
+-comm' (suc m) n rewrite +-comm' m n | +-suc' n m = refl