Induction.agda

module plfa.part1.Induction where

import Relation.Binary.PropositionalEquality as Eq
open Eq using (_≡_; refl; cong; sym)
open Eq.≡-Reasoning using (begin_; _≡⟨⟩_; _≡⟨_⟩_; _∎)
open import Data.Nat using (ℕ; zero; suc; _+_; _*_; _∸_)


-- left identity:   C op n ≡ n
-- right identity:  n op C ≡ n
-- associativity:  (a op b) op c ≡ a op (b op c) -- It doesn't matter wich direction you associate, left or right
-- commutivity:    a op b ≡ b op a -- you can commute and stil work. Where is our work from home ativity?
-- distibutivity: op¹ over op²


-- how can we prove that this is true in the general case
_ : (3 + 4) + 5 ≡ 3 + (4 + 5)
_ =
  begin
    (3 + 4) + 5
  ≡⟨⟩
    7 + 5
  ≡⟨⟩
    12
  ≡⟨⟩
    3 + 9
  ≡⟨⟩
    3 + (4 + 5)
  ∎

+-assoc : ∀ (m n p : ℕ) → (m + n) + p ≡ m + (n + p)
+-assoc zero n p =
  begin
    (zero + n) + p
  ≡⟨⟩ -- 0 + n ≡  n
    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) ⟩ -- construct a proof for the statement with suc applied to both sides
    suc (m + (n + p))
  ≡⟨⟩ -- move suc back to m using the reverse of the inductive case of addition
    suc m + (n + p)
  ∎

{-
  Commutivity
-}

-- Lemmas: left and right identities as well as right recursion

-- this is given to us by addition
+-identityˡ : ∀ (n : ℕ) → zero + n ≡ n
+-identityˡ n = refl



+-identityʳ : ∀ (n : ℕ) → n + zero ≡ n
+-identityʳ zero = refl -- 0+0 = zero. No worries
+-identityʳ (suc n) =
  begin
    suc n + zero
  ≡⟨⟩
    suc (n + zero)
  ≡⟨ cong suc (+-identityʳ n) ⟩
    suc n
  ∎

+-suc : ∀ (m n : ℕ) → m + suc n ≡ suc (m + n)
+-suc zero n =
  begin
    zero + suc n
  ≡⟨⟩
    suc n
  ≡⟨⟩
   suc (zero + n)
  ∎
+-suc (suc m) n =
  begin
    suc m + suc n
  ≡⟨⟩
    suc (m + suc n) -- inductive case of addition
    -- what is inside the () looks like the definition to +-suc…
    -- Apply The Lemma! (read in the same voice as "man your battlestations")
  ≡⟨ cong suc (+-suc m n) ⟩
  -- This looks like a big leap, but +-suc on m and n is literally
  --  taking (m + suc n) and proving that is equal to suc (m + n)
    suc (suc m + n)
  ∎


-- Time to try and tackle commutivity
+-comm : ∀ (m n : ℕ) → m + n ≡ n + m
+-comm m zero =
  begin
    m + zero
  ≡⟨ +-identityʳ m ⟩
    m
  ∎
+-comm m (suc n) =
  begin
    m + suc n
  ≡⟨ +-suc m n ⟩
    suc (m + n)
  ≡⟨ cong suc (+-comm m n) ⟩
    suc (n + m)
  ≡⟨⟩
    suc n + m
  ∎

-- what if we recurse left?
+-commᵐ : ∀ ( m n : ℕ) → m + n ≡ n + m
+-commᵐ zero n  =
  begin
    zero + n
  ≡⟨⟩
    n
  ≡⟨ sym (+-identityʳ n) ⟩
    n + zero
  ∎
+-commᵐ (suc m) n =
  begin
    suc m + n
  ≡⟨⟩
    suc (m + n)
  ≡⟨ cong suc (+-commᵐ m n) ⟩
    suc (n + m)
  ≡⟨ sym (+-suc n m) ⟩
    n + suc m
  ∎

-- turns out you need the symmetries of the lemmas


-- Collorary, rearrange
+-rearrange : ∀ (m n p q : ℕ) → (m + n) + (p + q) ≡ m + (n + p) + q
+-rearrange m n p q =
  begin
    (m + n) + (p + q)
  ≡⟨ +-assoc m n (p + q) ⟩
    m + (n + (p + q))
  ≡⟨ cong (m +_) (sym (+-assoc n p q)) ⟩ -- we need to move the parens from p and q to n and p, the reverse direction of assoc
    m + ((n + p) + q)
  ≡⟨ sym (+-assoc m (n + p) q) ⟩ -- again, move parens left
    (m + (n + p)) + q
  ≡⟨⟩ -- the parens around the m - p term are superfluous
    m + (n + p) + q
  ∎


+-swap : ∀ (m n p : ℕ) → m + (n + p) ≡ n + (m + p)
+-swap m n p =
  begin
    m + (n + p)
  ≡⟨ sym (+-assoc m n p) ⟩
    (m + n) + p
  ≡⟨ cong (_+ p) (+-comm m n) ⟩
    (n + m) + p
  ≡⟨ +-assoc n m p ⟩
    n + (m + p)
  ∎

*-distrib-+ : ∀ (a b m : ℕ) → (a + b) * m ≡ a * m + b * m
*-distrib-+ zero b m =
  begin
    (zero + b) * m
  ≡⟨⟩
    b * m
  ≡⟨⟩
    zero + (b * m)
  ≡⟨⟩
    (zero * m) + (b * m)
  ∎
*-distrib-+ a zero m =
  begin
    (a + zero) * m
  ≡⟨ cong (_* m) (+-comm a zero) ⟩
    (zero + a) * m
  ≡⟨⟩
    a * m
  ≡⟨   sym (+-identityʳ (a * m)) ⟩
    (a * m) + zero
  ≡⟨⟩
    (a * m) + (zero * m)
  ∎
*-distrib-+ (suc a) b m
  begin
    (suc a + b) * m
  ≡⟨⟩
    (suc (a + b)) * m
  ≡⟨⟩
    m + ((a + b) * m)
  ≡⟨ cong (m +_) (*-distrib-+ a b m) ⟩
    m + (a * m + b * m)
  ≡⟨ sym (+-assoc m (a * m) (b * m)) ⟩
    (m + a * m) + b * m
  ≡⟨⟩
    (suc a * m) + (b * m)
  ∎