Programming Language Foundations in Agda: Induction

Duction.agda

module Duction where

-- https://plfa.github.io/Induction/

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

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

+assoc : ∀ (a b c : ℕ) → (a + b) + c ≡ a + (b + c)
+assoc zero    b c                      = refl
+assoc (suc a) b c rewrite +assoc a b c = refl

+id : ∀ (a : ℕ) → a + zero ≡ a
+id zero                  = refl
+id (suc a) rewrite +id a = refl

+suc : ∀ (a b : ℕ) → a + suc b ≡ suc (a + b)
+suc zero    b                  = refl
+suc (suc a) b rewrite +suc a b = refl

+comm : ∀ (a b : ℕ) → a + b ≡ b + a
+comm a zero = +id a
+comm a (suc b)             --   a + suc b ≡ suc b + a
  rewrite +suc a b          -- suc (a + b) ≡ suc (b + a)
        | +comm a b = refl  --       a + b ≡ b + a

+swap : ∀ (a b c : ℕ) → a + (b + c) ≡ b + (a + c)
+swap a b c
  rewrite sym (+assoc a b c)  --   a + b + c ≡ b + (a + c)
        | +comm a b           --   b + a + c ≡ b + (a + c)
        | +assoc b a c = refl -- b + (a + c) ≡ b + (a + c)

*zero : ∀ (a : ℕ) → a * zero ≡ zero
*zero zero                    = refl
*zero (suc a) rewrite *zero a = refl

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

*suc : ∀ (a b : ℕ) → a * suc b ≡ a * b + a
*suc zero b = refl
*suc (suc a) b                              --         suc a * suc b ≡ suc a * b + suc a
  rewrite *suc a b                          -- suc (b + (a * b + a)) ≡ b + a * b + suc a
        | sym (+assoc b (a * b) a)          --   suc (b + a * b + a) ≡ b + a * b + suc a
        | sym (+suc (b + (a * b)) a) = refl --     b + a * b + suc a ≡ b + a * b + suc a

*distrib+ : ∀ (a b c : ℕ) → (a + b) * c ≡ a * c + b * c
*distrib+ a b zero        -- (a + b) * zero ≡ a * zero + b * zero
  rewrite *zero (a + b)   --           zero ≡ a * zero + b * zero
        | *zero a         --           zero ≡ zero + b * zero
        | *zero b = refl  --           zero ≡ zero + zero
*distrib+ a b (suc c)                           --       (a + b) * suc c ≡ a * suc c + b * suc c
  rewrite *suc (a + b) c                        -- (a + b) * c + (a + b) ≡ a * suc c + b * suc c
        | *suc a c                              -- (a + b) * c + (a + b) ≡ a * c + a + b * suc c
        | *suc b c                              -- (a + b) * c + (a + b) ≡ a * c + a + (b * c + b)
        | +assoc (a * c) a (b * c + b)          -- (a + b) * c + (a + b) ≡ a * c + (a + (b * c + b))
        | +comm a (b * c + b)                   -- (a + b) * c + (a + b) ≡ a * c + (b * c + b + a)
        | +assoc (b * c) b a                    -- (a + b) * c + (a + b) ≡ a * c + (b * c + (b + a))
        | sym (+assoc (a * c) (b * c) (b + a))  -- (a + b) * c + (a + b) ≡ a * c + b * c + (b + a)
        | +comm b a                             -- (a + b) * c + (a + b) ≡ a * c + b * c + (a + b)
        | *distrib+ a b c = refl

*assoc : ∀ (a b c : ℕ) → (a * b) * c ≡ a * (b * c)
*assoc zero    b c = refl
*assoc (suc a) b c              --     suc a * b * c ≡ suc a * (b * c)
  rewrite *suc a b              --   (b + a * b) * c ≡ b * c + a * (b * c)
        | *distrib+ b (a * b) c -- b * c + a * b * c ≡ b * c + a * (b * c)
        | *assoc a b c = refl

*comm : ∀ (a b : ℕ) → a * b ≡ b * a
*comm zero b rewrite *zero b = refl
*comm (suc a) b           -- suc a * b ≡ b * suc a
  rewrite *suc a b        -- b + a * b ≡ b * suc a
        | *suc b a        -- b + a * b ≡ b * a + b
        | +comm (b * a) b -- b + a * b ≡ b + b * a
        | *comm a b = refl

-- _∸_ : ℕ → ℕ → ℕ
-- a     ∸ zero  = a
-- zero  ∸ suc b = zero
-- suc a ∸ suc b = a ∸ b

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

∸assoc+ : ∀ (a b c : ℕ) → a ∸ b ∸ c ≡ a ∸ (b + c)
∸assoc+ a zero c = refl
∸assoc+ zero (suc b) c    -- zero ∸ suc b ∸ c ≡ zero ∸ (suc b + c)
  rewrite ∸zero b         --         zero ∸ c ≡ zero
        | ∸zero c = refl  --             zero ≡ zero
∸assoc+ (suc a) (suc b) c rewrite ∸assoc+ a b c = refl

-- _^_ : ℕ → ℕ → ℕ
-- a ^ zero  = 1
-- a ^ suc b = a * a ^ b

^+* : ∀ (a b c : ℕ) → a ^ (b + c) ≡ a ^ b * a ^ c
^+* a zero c          -- (a ^ (zero + c)) ≡ (a ^ zero) * (a ^ c)
  rewrite *id (a ^ c) --          (a ^ c) ≡ (a ^ c) + zero
        | +id (a ^ c) = refl
^+* a (suc b) c                     -- (a ^ (suc b + c)) ≡ (a ^ suc b) * (a ^ c)
                                    -- (a ^ suc (b + c)) ≡ a * (a ^ b) * (a ^ c)
                                    -- a * (a ^ (a + c)) ≡ a * (a ^ b) * (a ^ c)
  rewrite *assoc a (a ^ b) (a ^ c)  -- a * (a ^ (b + c)) ≡ a * ((a ^ b) * (a ^ c))
        | ^+* a b c = refl

^distrib* : ∀ (a b c : ℕ) → (a * b) ^ c ≡ a ^ c * b ^ c
^distrib* a b zero = refl
^distrib* a b (suc c)                           --     ((a * b) ^ suc c) ≡ (a ^ suc c) * (b ^ suc c)
  rewrite sym (*assoc (a * (a ^ c)) b (b ^ c))  -- a * b * ((a * b) ^ c) ≡ a * (a ^ c) * b * (b ^ c)
        | *assoc a (a ^ c) b                    -- a * b * ((a * b) ^ c) ≡ a * ((a ^ c) * b) * (b ^ c)
        | *comm (a ^ c) b                       -- a * b * ((a * b) ^ c) ≡ a * (b * (a ^ c)) * (b ^ c)
        | sym (*assoc a b (a ^ c))              -- a * b * ((a * b) ^ c) ≡ a * b * (a ^ c) * (b ^ c)
        | *assoc (a * b) (a ^ c) (b ^ c)        -- a * b * ((a * b) ^ c) ≡ a * b * ((a ^ c) * (b ^ c))
        | ^distrib* a b c = refl

one^ : ∀ (a : ℕ) → 1 ^ a ≡ 1
one^ zero                   = refl
one^ (suc a) rewrite one^ a = refl

^*^ : ∀ (a b c : ℕ) → a ^ (b * c) ≡ (a ^ b) ^ c
^*^ a zero c  -- a ^ (zero * c) ≡ (a ^ zero) ^ c
              --       a ^ zero ≡ (a ^ zero) ^ c
              --              1 ≡ (a ^ zero) ^ c
              --              1 ≡ 1 ^ c
  rewrite one^ c = refl
^*^ a (suc b) c                 --         a ^ (suc b * c) ≡ (a ^ suc b) ^ c
                                --         a ^ (c + b * c) ≡ (a ^ suc b) ^ c
                                --         a ^ (c + b * c) ≡ (a * a ^ b) ^ c
  rewrite ^+* a c (b * c)       -- (a ^ c) * (a ^ (b * c)) ≡ (a * (a ^ b)) ^ c
        | ^distrib* a (a ^ b) c -- (a ^ c) * (a ^ (b * c)) ≡ (a ^ c) * ((a ^ b) ^ c)
        | ^*^ a b c = refl

data Bin : Set where
  <> : Bin
  _O : Bin → Bin
  _I : Bin → Bin

infixl 10 _O
infixl 10 _I

inc : Bin → Bin
inc <>    = <> I
inc (x O) = x I
inc (x I) = (inc x) O

to : ℕ → Bin
to zero    = <> O
to (suc x) = inc (to x)

from : Bin → ℕ
from <>    = zero
from (x O) = 2 * from x
from (x I) = 2 * from x + 1

+* : ∀ (n : ℕ) → n + n ≡ 2 * n
+* zero                            = refl
+* (suc x) rewrite *zero x | +id x = refl

inc-suc : ∀ (b : Bin) → from (inc b) ≡ suc (from b)
inc-suc <> = refl
inc-suc (x O)                           -- from (inc (x O)) ≡ suc (from (x O))
  rewrite sym (+id (from (x O)))        --       from (x I) ≡ suc (from (x O) + zero)
        | sym (+suc (from (x O)) zero)  --   2 * from x + 1 ≡ from (x O) + suc zero
        | +id (from (x O)) = refl       --   2 * from x + 1 ≡ 2 * from x + 1
inc-suc (x I)                                   --                  from (inc (x I)) ≡ suc (from (x I))
  rewrite sym (*suc 2 (from x))                 -- from (inc x) + (from (inc x) + 0) ≡ suc (from x + (from x + 0) + 1)
        | sym (+suc (from x + (from x + 0)) 1)  -- from (inc x) + (from (inc x) + 0) ≡ from x + (from x + 0) + 2
        | +id (from x)                          -- from (inc x) + (from (inc x) + 0) ≡ from x + from x + 2
        | +id (from (inc x))                    --       from (inc x) + from (inc x) ≡ from x + from x + 2
        | +* (from x)
        | sym (*suc 2 (from x))
        | +* (from (inc x))
        | inc-suc x = refl
-- from (inc (x I)) ≡ suc (from (x I))
-- from ((inc x) O) ≡ suc (2 * from x + 1)
-- 2 * from (inc x) ≡ suc (2 * from x + 1)
-- 2 * from (inc x) ≡ 2 * from x + 2
-- 2 * from (inc x) ≡ 2 * (from x + 1)
-- 2 * from (inc x) ≡ 2 * (suc (from x))
-- ...
-- from (inc x) ≡ suc (from x)

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