done with induction

plfa/Induction.agda

@@ -0,0 +1,206 @@
+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