From 32ed3d692006c720f099172ce5d89e77f6deca6b Mon Sep 17 00:00:00 2001
From: Michael Zhang <mail@mzhang.io>
Date: Mon, 20 Sep 2021 13:16:07 -0500
Subject: [PATCH] Do the other 2 problems

---
 flake.nix          | 12 +++++++++
 src/Homework1.agda | 64 ++++++++++++++++++++++++++++++++++++++++------
 2 files changed, 68 insertions(+), 8 deletions(-)

diff --git a/flake.nix b/flake.nix
index 0e81e753..9b6d1c59 100644
--- a/flake.nix
+++ b/flake.nix
@@ -30,6 +30,17 @@
         })
       ]);
 
+      fix-whitespace = "";
+      # fix-whitespace = pkgs.stdenvNoCC.mkDerivation {
+      #   name = "fix-whitespace";
+      #   src = pkgs.fetchFromGitHub {
+      #     owner = "agda";
+      #     repo = "fix-whitespace";
+      #     rev = "a02f03a097943188a7b9aeaee8369edfc455c4fd";
+      #     sha256 = "TGj3DqOJTHRb9TwwGiDRlaXLseuv8mizYP20IR4YVFs=";
+      #   };
+      # };
+
       agda-mode = pkgs.vscode-utils.extensionFromVscodeMarketplace {
         name = "agda-mode";
         publisher = "banacorn";
@@ -58,6 +69,7 @@
         buildInputs = [
           agda
           vscodium
+          fix-whitespace
         ];
       };
     }
diff --git a/src/Homework1.agda b/src/Homework1.agda
index 72ef92de..be6953ae 100644
--- a/src/Homework1.agda
+++ b/src/Homework1.agda
@@ -138,13 +138,6 @@ module Homework1 where
     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 =
@@ -168,6 +161,61 @@ module Homework1 where
     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)
   ∎
+
+-- exponential distribution from the right
+^-distribʳ-* : ∀ (m n p : ℕ) → (m * n) ^ p ≡ (m ^ p) * (n ^ p)
+^-distribʳ-* m n zero = refl
+^-distribʳ-* m n (suc p) =
+  begin
+    (m * n) ^ (suc p)
+  ≡⟨⟩
+    (m * n) * (m * n) ^ p
+  ≡⟨ cong (m * n *_) (^-distribʳ-* m n p) ⟩
+    (m * n) * ((m ^ p) * (n ^ p))
+  ≡⟨ sym (*-assoc (m * n) (m ^ p) (n ^ p)) ⟩
+    (m * n) * (m ^ p) * (n ^ p)
+  ≡⟨ cong (_* (n ^ p)) (*-assoc m n (m ^ p)) ⟩
+    (m * (n * (m ^ p))) * (n ^ p)
+  ≡⟨ cong (_* (n ^ p)) (cong (m *_) (*-comm n (m ^ p))) ⟩
+    (m * ((m ^ p) * n)) * (n ^ p)
+  ≡⟨ cong (_* (n ^ p)) (sym (*-assoc m (m ^ p) n)) ⟩
+    m * (m ^ p) * n * (n ^ p)
+  ≡⟨⟩
+    (m ^ suc p) * n * (n ^ p)
+  ≡⟨ *-assoc (m ^ suc p) n (n ^ p) ⟩
+    (m ^ suc p) * (n * (n ^ p))
+  ≡⟨⟩
+    (m ^ suc p) * (n ^ suc p)
+  ∎
+
+-- exponential association
+^-*-assoc : ∀ (m n p : ℕ) → (m ^ n) ^ p ≡ m ^ (n * p)
+^-*-assoc m n zero =
+  begin
+    (m ^ n) ^ zero
+  ≡⟨⟩
+    1
+  ≡⟨⟩
+    m ^ zero
+  ≡⟨ cong (m ^_) (sym (0-prop n)) ⟩
+    m ^ (n * zero)
+  ∎
+^-*-assoc m n (suc p) =
+  begin
+    (m ^ n) ^ (suc p)
+  ≡⟨⟩
+    (m ^ n) * (m ^ n) ^ p
+  ≡⟨ cong (m ^ n *_) (^-*-assoc m n p) ⟩
+    (m ^ n) * m ^ (n * p)
+  ≡⟨ sym (^-distribˡ-|-* m n (n * p)) ⟩
+    m ^ (n + n * p)
+  ≡⟨ cong (m ^_) (cong (n +_) (*-comm n p)) ⟩
+    m ^ (n + p * n)
+  ≡⟨⟩
+    m ^ (suc p * n)
+  ≡⟨ cong (m ^_) (*-comm (suc p) n) ⟩
+    m ^ (n * suc p)
+  ∎
\ No newline at end of file