207 lines
5.3 KiB
Agda
207 lines
5.3 KiB
Agda
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
|