Do the other 2 problems

This commit is contained in:
Michael Zhang 2021-09-20 13:16:07 -05:00
parent 93f496e3c0
commit 32ed3d6920
Signed by: michael
GPG key ID: BDA47A31A3C8EE6B
2 changed files with 68 additions and 8 deletions

View file

@ -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
];
};
}

View file

@ -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)