module plfa.Induction where

import Relation.Binary.PropositionalEquality as Eq hiding (subst)
open Eq using (_≡_; refl; cong; sym)
open Eq.≡-Reasoning
open import Data.Nat using (ℕ; zero; suc; _+_; _*_; _∸_; _^_)

+-assoc : ∀ (m n p : ℕ) → (m + n) + p ≡ m + (n + p)
+-assoc zero n p = refl
+-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)
  ∎

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

+-suc : ∀ (m n : ℕ) → m + suc n ≡ suc (m + n)
+-suc zero n = refl
+-suc (suc m) n =
  begin
    suc m + suc n
  ≡⟨⟩
    suc (m + suc n)
  ≡⟨ cong suc (+-suc m n) ⟩
    suc (suc (m + n))
  ≡⟨⟩
    suc (suc m + n)
  ∎
  
+-comm : ∀ (m n : ℕ) → m + n ≡ n + m
+-comm m zero =
  begin
    m + zero
  ≡⟨ +-zero m ⟩
    m
  ≡⟨⟩
    zero + 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
  ∎

+-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)) ⟩
    m + ((n + p) + q)
  ≡⟨ sym (+-assoc m (n + p) q) ⟩
    (m + (n + p)) + q
  ≡⟨⟩
    m + (n + p) + q
  ∎


-- stretch finite-+-assoc
-- this one is weird, but maybe:
-- 0 : N
-- 1 : N (0 + 0) + 0 ≡ 0 + (0 + 0)
-- 2 : N (0 + 0) + 0 ≡ 0 + (0 + 0) (1 + 0) + 0 ≡ 1 + (0 + 0) (1 + 1) + 0 ≡ 1 + (1 + 0) ... 
-- 3 : N (0 + 0) + 0 ≡ 0 + (0 + 0) (1 + 0) + 0 ≡ 1 + (0 + 0) ... (2 + 2) + 2 ≡ 2 + (2 + 2)
-- but i’m not really sure here

+-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 + zero ≡ n
+-identity′ zero = refl
+-identity′ (suc n) rewrite +-identity′ n = refl

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

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

+-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-+ : ∀ (m n p : ℕ) → (m + n) * p ≡ m * p + n * p
*-distrib-+ zero n p = refl
*-distrib-+ (suc m) n p rewrite +-suc′ m n | *-distrib-+ m n p | +-assoc p (m * p) (n * p) = refl

*-assoc : ∀ (m n p : ℕ) → (m * n) * p ≡ m * (n * p)
*-assoc zero n p = refl
*-assoc (suc m) n p rewrite *-distrib-+ n (m * n) p | *-assoc m n p = refl

*-zero : ∀ (m : ℕ) → m * 0 ≡ 0
*-zero zero = refl
*-zero (suc m) = *-zero m

*-id : ∀ (m : ℕ) → m * 1 ≡ m
*-id zero = refl
*-id (suc m) rewrite *-id m = refl

*-suc : ∀ (m n : ℕ) → m * suc n ≡ m + m * n
*-suc zero n = refl
*-suc (suc m) n rewrite *-suc m n | +-swap n m (m * n) = refl

*-comm : ∀ (m n : ℕ) → m * n ≡ n * m
*-comm m zero = *-zero m
*-comm m (suc n) rewrite *-suc m n | *-comm m n = refl


0∸n≡0 : ∀ (n : ℕ) → zero ∸ n ≡ zero
0∸n≡0 zero = refl
0∸n≡0 (suc n) = refl

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

+*^-dist :  ∀ (m n p : ℕ) → m ^ (n + p) ≡ (m ^ n) * (m ^ p)
+*^-dist m n zero rewrite +-zero n | *-id (m ^ n) = refl
+*^-dist m n (suc p) rewrite +-suc′ n p | +*^-dist m n p | sym (*-assoc m (m ^ n) (m ^ p)) | *-comm m (m ^ n) | *-assoc (m ^ n) m (m ^ p) = refl

^-zero-pos :  ∀ (m : ℕ) → 0 ^ (suc m) ≡ 0
^-zero-pos m = refl

*^-dist :  ∀ (m n p : ℕ) → (m * n) ^ p ≡ (m ^ p) * (n ^ p)
*^-dist m n zero = refl
*^-dist m zero (suc p) rewrite ^-zero-pos (suc p) | *-comm m (m ^ p) | *-zero m =
  begin
    0
  ≡⟨ sym (*-zero m) ⟩
    m * 0
  ≡⟨ cong (m *_) (sym (*-zero (m ^ p))) ⟩
    m * ((m ^ p) * 0)
  ≡⟨ sym (*-assoc m (m ^ p) 0) ⟩
    m * m ^ p * 0
  ≡⟨ cong (_* 0) (*-comm m (m ^ p)) ⟩
    (m ^ p) * m * 0
  ∎
*^-dist zero (suc n) (suc p) rewrite ^-zero-pos (suc p) = refl
*^-dist (suc m) (suc n) (suc p) rewrite *^-dist m n p = {!!}

data Bin : Set where
  ⟨⟩ : Bin
  _O : Bin → Bin
  _I : Bin → Bin

inc : Bin → Bin
inc ⟨⟩ = ⟨⟩ I
inc (m O) = m I
inc (m I) = inc m O

to : ℕ → Bin
to zero = ⟨⟩
to (suc n) = inc (to n)

from : Bin → ℕ
from ⟨⟩ = 0
from (n O) = 2 * from n
from (n I) = 1 + 2 * from n

--  Exercise

inc-suc : ∀ (x : Bin) → from (inc x) ≡ suc (from x)
inc-suc ⟨⟩ = refl
inc-suc (x O) = refl
inc-suc (x I) rewrite inc-suc x | +-suc (suc (from x)) (from x + 0) = refl

-- to (from b) -> wrong when leading Os are involved

from-to : ∀ (n : ℕ) → from (to n) ≡ n
from-to zero = refl
from-to (suc n) rewrite inc-suc (to n) | from-to n = refl