RewriteAbuse.agda

module RewriteAbuse where

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

+-swap : ∀ (m n p : ℕ) → m + (n + p) ≡ n + (m + p)
+-swap m n p rewrite (sym (+-assoc m n p))
             |       (+-comm m n)
             |       (+-assoc n m p)
             = refl

*-annʳ : ∀ (n : ℕ) → (n * 0) ≡ 0
*-annʳ zero                       = refl
*-annʳ (suc n) rewrite (*-annʳ n) = refl

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

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

*-distrib-+ : ∀ (m n p : ℕ) → (m + n) * p ≡ m * p + n * p
*-distrib-+ m n zero rewrite (*-annʳ (m + n))
                     |       (*-annʳ m)
                     |       (*-annʳ n)
                     = refl
*-distrib-+ m n (suc p) rewrite (*-suc (m + n) p)
                        |       (*-distrib-+ m n p)
                        |       (+-comm m n)
                        |       (sym (+-assoc m (m * p) (n * p)))
                        |       (+-rearrange n m (m * p) (n * p))
                        |       (*-add m p)
                        |       (+-comm n (m * suc p))
                        |       (+-assoc (m * suc p) n (n * p))
                        |       (*-add n p)
                        = refl

*-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)
                    |       (*-distrib-+ n (m * n) p)
                    |       (*-assoc m n p)
                    = refl

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

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

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

open import Data.Nat using (_^_)

*-identityʳ : ∀ (n : ℕ) → (n * 1) ≡ n
*-identityʳ zero    = refl
*-identityʳ (suc n) rewrite (*-identityʳ n) = refl

*-identityˡ : ∀ (n : ℕ) → (1 * n) ≡ n
*-identityˡ zero    = refl
*-identityˡ (suc n) rewrite (*-identityˡ n) = refl


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

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

^-*-assoc : ∀ (m n p : ℕ) → (m ^ n) ^ p ≡ m ^ (n * p)
^-*-assoc m n zero    rewrite (*-annʳ n)
                      = refl
^-*-assoc m n (suc p) rewrite (^-*-assoc m n p)
                      |       (sym (^-distribˡ-+-* m n (n * p)))
                      |       (*-comm n p)
                      |       (*-comm (suc p) n)
                      =  refl


-- open import plfa.part1.Naturals using (Bin; from; to)
-- import caga cazzi

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

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

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

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

from∙inc=suc∙from : ∀ (b : Bin) → from (inc b) ≡ suc (from b)
from∙inc=suc∙from ⟨⟩    = refl
from∙inc=suc∙from (b O) rewrite (from∙inc=suc∙from b)
                        |       (+-comm 1 (from b * 2))
                        = refl
from∙inc=suc∙from (b I) rewrite (from∙inc=suc∙from b)
                        |       (+-comm 1 (from b * 2))
                        = refl

-- to∙from=id : ∀ (b : Bin) → to (from b) ≡ b
-- Falso dalla definizione data per to ⟨⟩ ≠ ⟨⟩ O

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