+-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 *-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 * zero ≡ zero
*-zero zero = refl
*-zero (suc m) rewrite *-zero m = refl
-- NOTE: manually w/o rewrite
-- *-zero (suc m) =
  -- begin
  --   suc m * zero
  -- ≡⟨⟩
  --   zero + m * zero
  -- ≡⟨⟩
  --   m * zero
  -- ≡⟨ *-zero m ⟩
  --   zero
  -- ∎
-- Like inductive `*` but on the right operand
*-sucʳ : ∀ (m n : ℕ) → n * suc m ≡ n + n * m
*-sucʳ m zero = refl
*-sucʳ m (suc n) =
  begin
    suc n * suc m
  ≡⟨⟩
    suc m + n * suc m
  ≡⟨ cong (\x → suc m + x) (*-sucʳ m n) ⟩
    suc m + (n + n * m)
  ≡⟨ +-comm (suc m) (n + n * m) ⟩
    (n + n * m) + suc m
  ≡⟨ +-suc (n + n * m) m ⟩
    suc (n + n * m + m)
  ≡⟨ cong suc (+-assoc n (n * m) m) ⟩
    suc (n + (n * m + m))
  ≡⟨ cong (\x → suc (n + x)) (+-comm (n * m) m) ⟩
    suc (n + (m + n * m))
  ∎
-- *-sucʳ zero n = {!!}
-- *-sucʳ (suc m) n = {!!}
*-comm : ∀ (m n : ℕ) → m * n ≡ n * m
*-comm zero n rewrite *-zero n = refl
*-comm (suc m) n rewrite *-comm m n | sym (*-sucʳ m n) = refl
-- NOTE: manually w/o rewrite
-- *-comm (suc m) n =
--   begin
--     suc m * n
--   ≡⟨⟩
--     n + m * n
--   ≡⟨ cong (n +_) (*-comm m n) ⟩
--     n + n * m
--   ≡⟨ sym (*-sucʳ m n) ⟩
--     n * suc m
--   ∎a

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

-- ∸-suc-∸-suc : ∀ (m n p : ℕ) → m ∸ n ∸ p ≡ m ∸ (n + p)
-- -- Goal: m ∸ suc n ∸ suc p ≡ m ∸ suc (n + suc p)
-- ∸-suc-∸-suc m n p = {!!}
∸-+-assoc : ∀ (m n p : ℕ) → m ∸ n ∸ p ≡ m ∸ (n + p)
∸-+-assoc m zero zero = refl
∸-+-assoc m (suc n) zero rewrite +-identityʳ n = refl
∸-+-assoc m zero (suc p) = refl
∸-+-assoc zero (suc n) (suc p) = refl
∸-+-assoc (suc m) (suc n) p =
  begin
    m ∸ n ∸ p
  ≡⟨ ∸-+-assoc m n p ⟩
    m ∸ (n + p)
  ∎
-- NOTE: Why is this so much harder to proof than the case above?
-- Goal: m ∸ suc n ∸ suc p ≡ m ∸ suc (n + suc p)
-- ∸-+-assoc m (suc n) (suc p) =
--   begin
--     m ∸ suc n ∸ suc p
--   ≡⟨⟩
--     (m ∸ suc n) ∸ suc p
--   ≡⟨⟩
--     (m ∸ suc n ∸ suc p)
--   ≡⟨ {!!} ⟩
--     (m ∸ (suc n + suc p))
--   ≡⟨⟩
--     m ∸ suc (n + suc p)
--   ∎

*-identityʳ : ∀ (m : ℕ) → m * 1 ≡ m
*-identityʳ zero = refl
*-identityʳ (suc m) =
  begin
    suc (m * 1)
  ≡⟨ cong suc (*-identityʳ m) ⟩
    suc m
  ∎
^-distribˡ-+-* : ∀ (m n p : ℕ) → m ^ (n + p) ≡ (m ^ n) * (m ^ p)
^-distribˡ-+-* m zero zero = refl
^-distribˡ-+-* m zero (suc p) =
  begin
    m * m ^ p
  ≡⟨ sym (+-identityʳ (m * m ^ p)) ⟩
    m * m ^ p + zero
  ∎
^-distribˡ-+-* m (suc n) zero =
  begin
    m * m ^ (n + zero)
  ≡⟨ cong (\x → m * m ^ x) (+-identityʳ n) ⟩
    m * m ^ n
  ≡⟨ sym (*-identityʳ (m * m ^ n)) ⟩
    (m * m ^ n) * 1
  ∎
^-distribˡ-+-* zero (suc n) (suc p) = refl
^-distribˡ-+-* (suc m) (suc n) (suc p) =
  begin
    suc m * suc m ^ (n + suc p)
  ≡⟨ cong (\x → suc m * suc m ^ x) (+-suc n p) ⟩
    suc m * (suc m * suc m ^ (n + p))
  ≡⟨ sym (*-assoc (suc m) (suc m) (suc m ^ (n + p))) ⟩
    suc m * suc m * (suc m ^ (n + p))
  ≡⟨ cong (\x → suc m * suc m * x) (^-distribˡ-+-* (suc m) n p) ⟩
    suc m * suc m * ((suc m ^ n) * (suc m ^ p))
  ≡⟨ sym (*-assoc (suc m * suc m) (suc m ^ n) (suc m ^ p)) ⟩
    suc m * suc m * suc m ^ n * suc m ^ p
  ≡⟨ cong (\x → x * (suc m ^ p)) (*-assoc (suc m) (suc m) (suc m ^ n)) ⟩
    suc m * (suc m * suc m ^ n) * (suc m ^ p)
  ≡⟨ cong (\x → x * (suc m ^ p)) (*-comm (suc m) (suc m * suc m ^ n)) ⟩
    (suc m * suc m ^ n) * suc m * suc m ^ p
  ≡⟨ *-assoc (suc m * suc m ^ n) (suc m) (suc m ^ p) ⟩
    (suc m * suc m ^ n) * (suc m * suc m ^ p)
  ≡⟨⟩
    (suc m ^ suc n) * (suc m ^ suc p)
  ∎
^-distribʳ-* : ∀ (m n p : ℕ) → (m * n) ^ p ≡ (m ^ p) * (n ^ p)
^-distribʳ-* m n zero = refl
^-distribʳ-* m n (suc p) =
  begin
    (m * n) ^ (suc p)
  ≡⟨⟩
    (m * n) * (m * n) ^ p
  ≡⟨⟩
    (m * n) * ((m * n) ^ p)
  ≡⟨ cong (\x → m * n * x) (^-distribʳ-* m n p) ⟩
    (m * n) * ((m ^ p) * (n ^ p))
  ≡⟨ sym (*-assoc (m * n) (m ^ p) (n ^ p)) ⟩
    (m * n) * (m ^ p) * (n ^ p)
  ≡⟨ cong (\x → x * (m ^ p) * (n ^ p)) (*-comm m n) ⟩
    (n * m) * (m ^ p) * (n ^ p)
  ≡⟨ cong (\x → x * (n ^ p)) (*-assoc n m (m ^ p)) ⟩
    n * (m * (m ^ p)) * (n ^ p)
  ≡⟨ cong (\x → x * (n ^ p)) (*-comm n (m * m ^ p)) ⟩
    (m * m ^ p) * n * n ^ p
  ≡⟨ *-assoc (m * m ^ p) n (n ^ p) ⟩
    (m * m ^ p) * (n * n ^ p)
  ≡⟨⟩
    (m ^ suc p) * (n ^ suc p)
  ∎
^-*-assoc : ∀ (m n p : ℕ) → (m ^ n) ^ p ≡ m ^ (n * p)
^-*-assoc m n zero =
  begin
    (m ^ n) ^ zero
  ≡⟨⟩
    m ^ 0
  ≡⟨⟩
    m ^ (0 * n)
  ≡⟨ cong (\x → m ^ x) (*-comm 0 n) ⟩
    m ^ (n * 0)
  ∎
^-*-assoc m n (suc p) =
  begin
    (m ^ n) ^ (suc p)
  ≡⟨⟩
    m ^ n * (m ^ n) ^ p
  ≡⟨ cong (\x → m ^ n * x) (^-*-assoc m n p) ⟩
    m ^ n * m ^ (n * p)
  ≡⟨ cong (\x → m ^ n * m ^ x) (*-comm n p) ⟩
    (m ^ n) * (m ^ (p * n))
  ≡⟨ sym (^-distribˡ-+-* m n (p * n)) ⟩
    m ^ (n + p * n)
  ≡⟨⟩
    m ^ (suc p * n)
  ≡⟨ cong (\x → m ^ x) (*-comm (suc p) n) ⟩
    m ^ (n * suc p)
  ∎

-- NOTE: This doesn't work:
--
-- open import plfa.part1.Naturals using (inc,to,from)
--
-- It fails with:
-- Duplicate binding for built-in thing NATURAL, previous binding to
-- Agda.Builtin.Nat.Nat
-- when checking the pragma BUILTIN NATURAL ℕ
data Bin : Set where
  ⟨⟩ : Bin
  _O : Bin → Bin
  _I : Bin → Bin
inc : Bin → Bin
inc ⟨⟩ = ⟨⟩ I
inc (rest O) = rest I
inc (rest I) = (inc rest) O
to   : ℕ → Bin
to zero = ⟨⟩ O
to (suc n) = inc (to n)
from : Bin → ℕ
from ⟨⟩ = 0
from (rest O) = 2 * (from rest)
from (rest I) = 1 + 2 * (from rest)
from-inc-suc-from : ∀ (b : Bin) → from (inc b) ≡ suc (from b)
from-inc-suc-from ⟨⟩ = refl
from-inc-suc-from (b O) = refl
from-inc-suc-from (b I) =
  begin
    from (inc (b I))
  ≡⟨⟩
    from ((inc b) O)
  ≡⟨⟩
    2 * (from (inc b))
  ≡⟨ cong (\x → 2 * x) (from-inc-suc-from b) ⟩
    2 * suc (from b)
  ≡⟨⟩
    2 * (1 + (from b))
  ≡⟨ *-comm 2 (1 + (from b)) ⟩
    (1 + (from b)) * 2
  ≡⟨ *-distrib-+ 1 (from b) 2 ⟩
    2 + (from b) * 2
  ≡⟨ cong (\x → 2 + x) (*-comm (from b) 2) ⟩
    2 + 2 * (from b)
  ≡⟨⟩
    suc (1 + 2 * (from b))
  ≡⟨⟩
    suc (from (b I))
  ∎
-- NOTE: Does not hold cause `⟨⟩` isn't equal to canonical zero `⟨⟩ O`
-- to-from-id : ∀ (b : Bin) → to (from b) ≡ b
-- to-from-id ⟨⟩ =
--   begin
--     to (0)
--   ≡⟨⟩
--     ⟨⟩ O
--   ≡⟨⟩
--     ⟨⟩
--   ∎
-- to-from-id (b O) = {!!}
-- to-from-id (b I) = {!!}
from-to-id : ∀ (m : ℕ) → from (to m) ≡ m
from-to-id zero = refl
from-to-id (suc m) =
  begin
    from (to (suc m))
  ≡⟨⟩
    from (inc (to m))
  ≡⟨ from-inc-suc-from (to m) ⟩
    suc (from (to m))
  ≡⟨ cong suc (from-to-id m) ⟩
    suc m
  ∎