Skip to content

Commit 568f463

Browse files
Geoc2022Geoc2022
committed
Add PowMonoid
1 parent 79080e0 commit 568f463

9 files changed

Lines changed: 223 additions & 64 deletions

File tree

‎Game/Levels/PowMonoid.lean‎

Lines changed: 20 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,20 @@
1+
import Game.Levels.PowMonoid.L01_PowOne
2+
import Game.Levels.PowMonoid.L02_PowSuccLeft
3+
import Game.Levels.PowMonoid.L03_PowAdd
4+
import Game.Levels.PowMonoid.L04_PowMul
5+
import Game.Levels.PowMonoid.L05_PowId
6+
import Game.Levels.PowMonoid.L06_PowCommMul
7+
import Game.Levels.PowMonoid.L07_PowCommPow
8+
9+
10+
World "Monoid Power"
11+
Title "Monoid Power World"
12+
13+
Introduction "
14+
A monoid consists of a set M together with a binary operation (`*`) we represent repeatedly multiplying an element by itself using `mpow` with the following definition:
15+
16+
- `mpow_zero`: `m ^ 0 = 1`
17+
- `mpow_succ_right`: `m ^ (n + 1) = m ^ n * m`
18+
19+
They've also been added to `simp`
20+
"

‎Game/Levels/PowMonoid/L01_PowOne.lean‎

Lines changed: 27 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,27 @@
1+
import Game.Levels.Monoid
2+
import Game.MyAlgebra.PowMonoid
3+
4+
World "Monoid Power"
5+
Level 1
6+
7+
Title "First Power: m¹ = m"
8+
9+
namespace MyAlgebra
10+
11+
Introduction "We’ve defined the power of an element in a monoid recursively.
12+
In this level you’ll prove the basic fact that `m¹ = m`."
13+
14+
/--
15+
If `m` is an element of a monoid, then `m¹ = m`.
16+
-/
17+
TheoremDoc MyAlgebra.mpow_one as "mpow_one" in "Monoid Power"
18+
Statement mpow_one {M} [Monoid M] (m : M) : m ^ 1 = m := by
19+
Hint "Recall the definition: `m ^ (n+1) = m ^ n * m` and `m ^ 0 = 1`."
20+
-- `1` is `0 + 1`, so:
21+
rw [mpow_succ_right]
22+
-- Now `m ^ 0 = 1`, so:
23+
rw [mpow_zero]
24+
-- and `1 * m = m` by the left identity law:
25+
rw [one_mul]
26+
27+
Conclusion "Nice! You've taken the first step in using our power function on monoids."

‎Game/Levels/PowMonoid/L02_PowSuccLeft.lean‎

Lines changed: 31 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,31 @@
1+
import Game.Levels.PowMonoid.L01_PowOne
2+
3+
World "Monoid Power"
4+
Level 2
5+
6+
Title "Succ on the Left"
7+
8+
namespace MyAlgebra
9+
10+
Introduction "We know that `m ^ (n+1) = m ^ n * m`. In this level
11+
you will show the equivalent statement with multiplication on the left:
12+
`m ^ (n+1) = m * m ^ n`."
13+
14+
/--
15+
For any monoid element `m`, `m ^ (n + 1) = m * m ^ n`.
16+
-/
17+
TheoremDoc MyAlgebra.mpow_succ_left as "mpow_succ_left" in "Monoid Power"
18+
Statement mpow_succ_left {M} [Monoid M] (m : M) (n : ℕ) :
19+
m ^ (n + 1) = m * (m ^ n) := by
20+
induction n with
21+
| zero =>
22+
Hint "Start with the case `n = 0`."
23+
rw [Nat.zero_add, mpow_one]
24+
rw [mpow_zero, mul_one]
25+
| succ n ih =>
26+
Hint "Use the induction hypothesis and associativity."
27+
rw [mpow_succ_right]
28+
nth_rw 2 [mpow_succ_right]
29+
rw [ih, mul_assoc]
30+
31+
Conclusion "Good! You’ve learned to move the extra `m` to the left using induction and associativity."

‎Game/Levels/PowMonoid/L03_PowAdd.lean‎

Lines changed: 30 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,30 @@
1+
import Game.Levels.PowMonoid.L02_PowSuccLeft
2+
3+
World "Monoid Power"
4+
Level 3
5+
6+
Title "Adding Exponents"
7+
8+
namespace MyAlgebra
9+
10+
Introduction "Now we prove the fundamental law of exponents in a monoid:
11+
`m ^ (x + y) = m ^ x * m ^ y`."
12+
13+
/--
14+
For any `m` in a monoid and natural numbers `x`, `y`, we have `m ^ (x + y) = m ^ x * m ^ y`.
15+
-/
16+
TheoremDoc MyAlgebra.mpow_add as "mpow_add" in "Monoid Power"
17+
Statement mpow_add {M} [Monoid M] (m : M) (x y : ℕ) :
18+
m ^ (x + y) = (m ^ x) * (m ^ y) := by
19+
induction y with
20+
| zero =>
21+
Hint "Start with `y = 0`."
22+
-- m^(x+0) = m^x and m^x * m^0 = m^x * 1
23+
simp [Nat.add_zero, mpow_zero]
24+
| succ y ih =>
25+
Hint "Use the recursive definition of pow and the induction hypothesis."
26+
-- m^(x + (y+1)) = m^(x + y + 1) = m^(x+y)*m
27+
-- and (m^x * m^y) * m = m^x * (m^y * m)
28+
simp [Nat.add_succ, mpow_succ_right, ih, mul_assoc]
29+
30+
Conclusion "Awesome! You have the exponent law for addition"

‎Game/Levels/PowMonoid/L04_PowMul.lean‎

Lines changed: 29 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,29 @@
1+
import Game.Levels.PowMonoid.L03_PowAdd
2+
3+
World "Monoid Power"
4+
Level 4
5+
6+
Title "Multiplying Exponents"
7+
8+
namespace MyAlgebra
9+
10+
Introduction "Next, you will prove another standard law: `m ^ (x * y) = (m ^ x) ^ y`."
11+
12+
/--
13+
For any `m` in a monoid and naturals `x`, `y`, `m ^ (x * y) = (m ^ x) ^ y`.
14+
-/
15+
TheoremDoc MyAlgebra.mpow_mul as "mpow_mul" in "Monoid Power"
16+
Statement mpow_mul {M} [Monoid M] (m : M) (x y : ℕ) :
17+
m ^ (x * y) = (m ^ x) ^ y := by
18+
induction y with
19+
| zero =>
20+
Hint "Start with `y = 0` first."
21+
-- m^(x*0) = m^0 = 1, and (m^x)^0 = 1
22+
simp [Nat.mul_zero, mpow_zero]
23+
| succ y ih =>
24+
Hint "Use the `mpow_add` lemma from the previous level."
25+
-- m^(x*(y+1)) = m^(x*y + x) = m^(x*y) * m^x
26+
-- and (m^x)^(y+1) = (m^x)^y * m^x
27+
simp [Nat.mul_succ, mpow_add, mpow_succ_right, ih]
28+
29+
Conclusion "Well done! You have derived the law of exponents for multiplication. Can you think of any examples of this law?"

‎Game/Levels/PowMonoid/L05_PowId.lean‎

Lines changed: 26 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,26 @@
1+
import Game.Levels.PowMonoid.L04_PowMul
2+
3+
World "Monoid Power"
4+
Level 5
5+
6+
Title "Powers of the Identity"
7+
8+
namespace MyAlgebra
9+
10+
Introduction "Now show that the identity element is fixed under taking powers:
11+
`1 ^ x = 1`."
12+
13+
/--
14+
For any monoid, `1 ^ x = 1` for all `x : ℕ`.
15+
-/
16+
TheoremDoc MyAlgebra.mpow_id as "mpow_id" in "Monoid Power"
17+
Statement mpow_id {M} [Monoid M] (x : ℕ) : (1 : M) ^ x = 1 := by
18+
induction x with
19+
| zero =>
20+
Hint "What is `1^0` by definition?"
21+
rw [mpow_zero]
22+
| succ x ih =>
23+
Hint "Use the recursive definition of pow and the fact that `1 * 1 = 1`."
24+
rw [mpow_succ_right, ih, mul_one]
25+
26+
Conclusion "Nice! Identity behaves as expected under exponentiation."

‎Game/Levels/PowMonoid/L06_PowCommMul.lean‎

Lines changed: 29 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,29 @@
1+
import Game.Levels.PowMonoid.L05_PowId
2+
3+
World "Monoid"
4+
Level 6
5+
6+
Title "Commuting a Power with its Base"
7+
8+
namespace MyAlgebra
9+
10+
Introduction "In a general monoid, `m` need not commute with all elements, but
11+
it does commute with its own powers. You’ll prove `m ^ x * m = m * m ^ x`."
12+
13+
/--
14+
For any `m` in a monoid and `x : ℕ`,
15+
`m ^ x * m = m * m ^ x`.
16+
-/
17+
TheoremDoc MyAlgebra.mpow_comm_mul as "mpow_comm_mul" in "Monoid"
18+
Statement mpow_comm_mul {M} [Monoid M] (m : M) (x : ℕ) :
19+
(m ^ x) * m = m * (m ^ x) := by
20+
induction x with
21+
| zero =>
22+
Hint "Start with `x = 0`."
23+
rw [mpow_zero, one_mul, mul_one]
24+
| succ x ih =>
25+
Hint "Rewrite `m^(x+1)` and use associativity plus the induction hypothesis."
26+
nth_rw 1 [mpow_succ_left, mpow_succ_right]
27+
simp [ih, mul_assoc]
28+
29+
Conclusion "Great!"

‎Game/Levels/PowMonoid/L07_PowCommPow.lean‎

Lines changed: 31 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,31 @@
1+
import Game.Levels.PowMonoid.L06_PowCommMul
2+
3+
World "Monoid Power"
4+
Level 7
5+
6+
Title "Powers Commute with Powers"
7+
8+
namespace MyAlgebra
9+
10+
Introduction "Finally, you will prove the full statement:
11+
`m ^ x * m ^ y = m ^ y * m ^ x`. We already know `m^x` commutes with `m`,
12+
so we use induction to extend this to all powers."
13+
14+
/--
15+
For any `m` in a monoid and naturals `x`, `y`,
16+
`m ^ x * m ^ y = m ^ y * m ^ x`.
17+
-/
18+
TheoremDoc MyAlgebra.mpow_comm_mpow as "mpow_comm_mpow" in "Monoid Power"
19+
Statement mpow_comm_mpow {M} [Monoid M] (m : M) (x y : ℕ) :
20+
(m ^ x) * (m ^ y) = (m ^ y) * (m ^ x) := by
21+
induction y with
22+
| zero => rw [mpow_zero, mul_one, one_mul]
23+
| succ y ih =>
24+
rw [mpow_succ_left]
25+
rw [mul_assoc]
26+
rw [← ih]
27+
rw [← mul_assoc m _ _]
28+
rw [← mul_assoc _ m _]
29+
rw [mpow_comm_mul]
30+
31+
Conclusion "Excellent work! You’ve proven a general version of the previous level - that all powers of an element commute with each other."

‎Game/MyAlgebra/PowMonoid.lean‎

Lines changed: 0 additions & 64 deletions
Original file line numberDiff line numberDiff line change
@@ -20,67 +20,3 @@ lemma mpow_zero (m : M) [Monoid M] : m ^ 0 = 1 := rfl
2020
/-- m ^ (n + 1) = m ^ n * m -/
2121
@[simp]
2222
lemma mpow_succ_right (m : M) [Monoid M] : m ^ (n+1) = (m ^ n) * m := rfl
23-
24-
25-
-- Start of Monoid Order Levels
26-
/-- m¹ = m -/
27-
@[simp]
28-
lemma mpow_one (m : M) [Monoid M] : m ^ 1 = m := by
29-
rw [mpow_succ_right, mpow_zero, one_mul]
30-
31-
/-- m ^ (n + 1) = m * m ^ n-/
32-
lemma mpow_succ_left (m : M) [Monoid M] : m ^ (n + 1) = m * (m ^ n) := by
33-
induction n with
34-
| zero =>
35-
rw [mpow_zero, mpow_one]
36-
rw [mul_one]
37-
| succ n ih =>
38-
rw [mpow_succ_right]
39-
nth_rw 2 [mpow_succ_right]
40-
rw [ih, mul_assoc]
41-
42-
/-- m ^ (x + y) = m ^ x * m ^ y -/
43-
lemma mpow_add (m : M) (x y : ℕ) [Monoid M]: m ^ (x + y) = (m ^ x) * (m ^ y) := by
44-
induction y with
45-
| zero => rw [mpow_zero, mul_one, Nat.add_zero]
46-
| succ y ih =>
47-
rw [Nat.add_succ, mpow_succ_right, ih]
48-
rw [mpow_succ_right]
49-
rw [mul_assoc]
50-
51-
/-- m ^ (x * y) = (m ^ x) ^ y-/
52-
lemma mpow_mul (m : M) (x y : ℕ) [Monoid M] : m ^ (x * y) = (m ^ x) ^ y := by
53-
induction y with
54-
| zero =>
55-
rw [Nat.mul_zero, mpow_zero, mpow_zero]
56-
| succ y ih =>
57-
simp only [mpow_succ_right]
58-
rw [Nat.mul_succ, mpow_add, ih]
59-
60-
/-- 1 ^ x = 1 -/
61-
@[simp]
62-
lemma mpow_id (x : ℕ) [Monoid M] : 1 ^ x = (1 : M) := by
63-
induction x with
64-
| zero => rfl
65-
| succ x ih => rw [mpow_succ_right, ih, mul_one]
66-
67-
/-- m ^ x * m = m * m ^ x -/
68-
lemma mpow_comm_mul (m: M) (x : ℕ) [Monoid M] : (m ^ x) * m = m * (m ^ x) := by
69-
induction x with
70-
| zero => rw [mpow_zero, mul_one, one_mul]
71-
| succ x ih =>
72-
nth_rw 1 [mpow_succ_left, mpow_succ_right]
73-
rw [mul_assoc, ih]
74-
done
75-
76-
/-- m ^ x * m ^ y = m ^ y * m ^ x -/
77-
lemma mpow_comm_mpow (m : M) (x y : ℕ) [Monoid M] : (m ^ x) * (m ^ y) = (m ^ y) * (m ^ x) := by
78-
induction y with
79-
| zero => rw [mpow_zero, mul_one, one_mul]
80-
| succ y ih =>
81-
rw [mpow_succ_left]
82-
rw [mul_assoc]
83-
rw [← ih]
84-
rw [← mul_assoc m _ _]
85-
rw [← mul_assoc _ m _]
86-
rw [mpow_comm_mul]

0 commit comments

Comments
 (0)