hw1

src/Homework1.agda

@@ -0,0 +1,173 @@
+open import Relation.Binary.PropositionalEquality using (_≡_; refl; cong; sym; module ≡-Reasoning)
+open ≡-Reasoning using (begin_; _≡⟨⟩_; step-≡; _∎)
+open import Data.Nat using (ℕ; zero; suc; _+_; _*_; _^_)
+open import Data.Nat.Properties using (+-identityʳ; +-assoc; +-suc; +-comm)
+
+module Homework1 where
+
+-- zero property
+0-prop : ∀ (n : ℕ) → n * 0 ≡ 0
+0-prop zero = refl
+0-prop (suc n) = 0-prop n
+
+-- multiplicative identity
+*-identity : ∀ (n : ℕ) → n * 1 ≡ n
+*-identity zero = refl
+*-identity (suc n) = 
+  begin
+    suc n * 1
+  ≡⟨⟩
+    1 + n * 1
+  ≡⟨ cong (1 +_) (*-identity n) ⟩
+    1 + n
+  ∎
+
+
+-- multiplicative commutativity
+-- using induction on both variables
+*-comm : ∀ (a b : ℕ) → a * b ≡ b * a
+*-comm zero zero = refl
+*-comm a zero = 0-prop a
+*-comm zero b = sym (0-prop b)
+*-comm (suc a) (suc b) =
+  begin
+    suc a * suc b
+  ≡⟨⟩
+    suc b + a * suc b
+  ≡⟨ cong (suc b +_) (*-comm a (suc b)) ⟩
+    suc b + suc b * a
+  ≡⟨⟩
+    suc b + (a + b * a)
+  ≡⟨ sym (+-assoc (suc b) a (b * a)) ⟩
+    suc b + a + b * a
+  ≡⟨ cong (_+ (b * a)) (+-comm (suc b) a) ⟩
+    a + suc b + b * a
+  ≡⟨ cong (_+ (b * a)) (+-suc a b) ⟩
+    suc (a + b) + b * a
+  ≡⟨ cong (_+ (b * a)) (cong suc (+-comm a b)) ⟩
+    suc (b + a) + b * a
+  ≡⟨ cong (_+ (b * a)) (sym (+-suc b a)) ⟩
+    b + suc a + b * a
+  ≡⟨ cong (_+ (b * a)) (+-comm b (suc a)) ⟩
+    suc a + b + b * a
+  ≡⟨ cong (suc a + b +_) (*-comm b a) ⟩
+    suc a + b + a * b
+  ≡⟨ +-assoc (suc a) b (a * b) ⟩
+    suc a + (b + a * b)
+  ≡⟨⟩
+    suc a + suc a * b
+  ≡⟨ cong (suc a +_) (*-comm (suc a) b) ⟩
+    suc a + b * suc a
+  ≡⟨⟩
+    suc b * suc a
+  ∎
+
+-- multiplication distributive property
+*-distrib-+ : ∀ (a b c : ℕ) → a * (b + c) ≡ (a * b) + (a * c)
+*-distrib-+ a zero c =
+  begin
+    a * (zero + c)
+  ≡⟨⟩
+    a * c
+  ≡⟨⟩
+    zero + (a * c)
+  ≡⟨ cong (_+ (a * c)) (sym (0-prop a)) ⟩
+    (a * zero) + (a * c)
+  ∎
+*-distrib-+ a (suc b) c =
+  begin
+    a * (suc b + c)
+  ≡⟨⟩
+    a * suc (b + c)
+  ≡⟨ *-comm a (suc (b + c)) ⟩
+    suc (b + c) * a
+  ≡⟨⟩
+    a + (b + c) * a
+  ≡⟨ cong (a +_) (*-comm (b + c) a) ⟩
+    a + a * (b + c)
+  ≡⟨ cong (a +_) (*-distrib-+ a b c) ⟩
+    a + ((a * b) + (a * c))
+  ≡⟨ cong (a +_) (cong (_+ (a * c)) (*-comm a b)) ⟩
+    a + ((b * a) + (a * c))
+  ≡⟨ sym (+-assoc a (b * a) (a * c)) ⟩
+    a + (b * a) + (a * c)
+  ≡⟨⟩
+    (suc b * a) + (a * c)
+  ≡⟨ cong (_+ (a * c)) (*-comm (suc b) a) ⟩
+    (a * suc b) + (a * c)
+  ∎
+
+
+-- multiplicative associativity
+*-assoc : ∀ (a b c : ℕ) → (a * b) * c ≡ a * (b * c)
+*-assoc zero b c = refl
+*-assoc (suc a) b c =
+  begin
+    (suc a * b) * c
+  ≡⟨⟩
+    (b + a * b) * c
+  ≡⟨ *-comm (b + a * b) c ⟩
+    c * (b + a * b)
+  ≡⟨ *-distrib-+ c b (a * b) ⟩
+    (c * b) + (c * (a * b))
+  ≡⟨ cong ((c * b) +_) (sym (*-assoc c a b)) ⟩
+    (c * b) + (c * a * b)
+  ≡⟨ cong (_+ (c * a * b)) (*-comm c b) ⟩
+    (b * c) + (c * a * b)
+  ≡⟨ cong ((b * c) +_) (cong (_* b) (*-comm c a)) ⟩
+    (b * c) + (a * c * b)
+  ≡⟨ cong ((b * c) +_) (*-assoc a c b) ⟩
+    (b * c) + (a * (c * b))
+  ≡⟨ cong ((b * c) +_) (cong (a *_) (*-comm c b)) ⟩
+    (b * c) + (a * (b * c))
+  ∎
+
+
+-- 1-identity
+1-identity : ∀ (n : ℕ) → 1 * n ≡ n
+1-identity n =
+  begin
+    1 * n
+  ≡⟨⟩
+    n + 0 * n
+  ≡⟨⟩
+    n + 0
+  ≡⟨ +-comm n 0 ⟩
+    0 + n
+  ≡⟨⟩
+    n
+  ∎
+
+^-suc : ∀ (a b : ℕ) → a ^ suc b ≡ a * (a ^ b)
+^-suc a zero = refl
+^-suc a (suc b) =
+  begin
+    a ^ suc (suc b)
+  ∎
+
+-- exponentiation distributive property
+^-distribˡ-|-* : ∀ (m n p : ℕ) → m ^ (n + p) ≡ (m ^ n) * (m ^ p)
+^-distribˡ-|-* m zero p =
+  begin
+    m ^ (zero + p)
+  ≡⟨⟩
+    m ^ p
+  ≡⟨ sym (1-identity (m ^ p)) ⟩
+    1 * (m ^ p)
+  ≡⟨⟩
+    (m ^ zero) * (m ^ p)
+  ∎
+^-distribˡ-|-* m (suc n) p =
+  begin
+    m ^ (suc n + p)
+  ≡⟨⟩
+    m ^ (suc (n + p))
+  ≡⟨⟩
+    m * (m ^ (n + p))
+  ≡⟨ cong (m *_) (^-distribˡ-|-* m n p) ⟩
+    m * ((m ^ n) * (m ^ p))
+  ≡⟨ sym (*-assoc m (m ^ n) (m ^ p)) ⟩
+    (m * (m ^ n)) * (m ^ p)
+  ≡⟨ cong (_* (m ^ p)) (sym (^-suc m n)) ⟩
+    (m ^ suc n) * (m ^ p)
+  ∎