Add PowGroup

Author: Geoc2022

Game/Levels/PowGroup.lean

@@ -0,0 +1,31 @@
+import Game.Levels.PowGroup.L01_PowNegNat
+import Game.Levels.PowGroup.L02_PowNegOne
+import Game.Levels.PowGroup.L03_PowSucc
+import Game.Levels.PowGroup.L04_PowPred
+import Game.Levels.PowGroup.L05_PowAdd
+import Game.Levels.PowGroup.L06_PowNeg
+import Game.Levels.PowGroup.L07_PowSub
+import Game.Levels.PowGroup.L08_PowMul
+
+
+
+World "Group Power"
+Title "Group Power World"
+
+Introduction "
+  A group consists of a set G together with a binary operation (`*`) we represent repeatedly multiplying an element by itself using `gpow`:
+
+  ```
+  def gpow {G : Type} [Group G] (x : G) : ℤ → G
+  | Int.ofNat n => mpow x n
+  | Int.negSucc n => mpow (x⁻¹) (n+1)
+  ```
+  To make it easier to work with, we've created the following lemmas:
+    - `gpow_ofNat`: `g ^ ↑n = g ^ n`
+    - `gpow_negSucc`: `g ^ (Int.negSucc n) = (g⁻¹) ^ (n+1)`
+    - `gpow_zero`: `g ^ (0 : ℤ) = 1`
+    - `gpow_one`: `g ^ (1 : ℤ) = g`
+    - `inv_mpow`: `(g ^ n)⁻¹ = (g⁻¹) ^ n`
+
+  They've also been added to `simp`
+"

Game/Levels/PowGroup/L01_PowNegNat.lean

@@ -0,0 +1,36 @@
+import Game.Levels.Group
+import Game.Levels.PowMonoid
+import Game.MyAlgebra.PowGroup
+
+World "Group Power"
+Level 1
+
+Title "Negative Natural Exponent"
+
+namespace MyAlgebra
+
+Introduction "We now move to powers with integer exponents.
+In this level, you’ll show that `g ^ (-(n : ℤ))` is the inverse of `g ^ n`."
+
+/--
+For a group element `g` and a natural number `n`, we have
+`g ^ (-(n : ℤ)) = (g ^ n)⁻¹`.
+-/
+TheoremDoc MyAlgebra.gpow_neg_mpow as "gpow_neg_mpow" in "Group Power"
+Statement gpow_neg_mpow {G} [Group G] (g : G) (x : ℕ) :
+  g ^ (-(x : ℤ)) = (g ^ x)⁻¹ := by
+  Hint "Do a case split on `n` using `cases n with | zero | succ`."
+  cases x with
+  | zero =>
+    rw [Int.ofNat_zero]
+    rw [Int.neg_zero]
+    rw [gpow_zero g]
+    rw [inv_id]
+    rfl
+  | succ x =>
+    have h: -↑(x + 1) = Int.negSucc x := rfl
+    rw [h]
+    rw [gpow_negSucc]
+    simp [inv_mpow, mpow_add, ← inv_anticomm, mpow_one, mpow_comm_mul]
+
+Conclusion "Great! You’ve connected negative integer exponents with inverses of natural powers."

Game/Levels/PowGroup/L02_PowNegOne.lean

@@ -0,0 +1,24 @@
+import Game.Levels.PowGroup.L01_PowNegNat
+
+World "Group Power"
+Level 2
+
+Title "The Inverse: g⁻¹ = g^(-1)"
+
+namespace MyAlgebra
+
+Introduction "Here you show that exponent `-1` gives the group inverse."
+
+/--
+For any group element `g`, we have `g ^ (-1) = g⁻¹`.
+-/
+TheoremDoc MyAlgebra.gpow_neg_one as "gpow_neg_one" in "Group Power"
+Statement gpow_neg_one {G} [Group G] (g : G) :
+  g ^ (-1) = g⁻¹ := by
+  Hint "Write `-1` as `-(1 : ℤ)` and then use the previous level."
+  have : (1 : ℤ) = (1 : ℕ) := rfl
+  -- or simply: `rw [← Int.ofNat_one]`
+  rw [← Int.ofNat_one, gpow_neg_mpow]
+  simp [mpow_one]
+
+Conclusion "Now you see that the usual inverse `g⁻¹` is just `g` raised to `-1`."

Game/Levels/PowGroup/L03_PowSucc.lean

@@ -0,0 +1,37 @@
+import Game.Levels.PowGroup.L02_PowNegOne
+
+World "Group Power"
+Level 3
+
+Title "Adding 1 to an Integer Exponent"
+
+namespace MyAlgebra
+
+Introduction "Next, you will show a recursive formula for integer exponents:
+`g ^ (n + 1) = g ^ n * g`."
+
+/--
+For any group element `g` and integer `x`,
+`g ^ (x + 1) = (g ^ x) * g`.
+-/
+TheoremDoc MyAlgebra.gpow_succ as "gpow_succ" in "Group Power"
+Statement gpow_succ {G} [Group G] (g : G) (x : ℤ) :
+  g ^ (x + 1) = (g ^ x) * g := by
+  Hint "Use `Int.induction_on` on `x`."
+  induction x using Int.induction_on with
+  | hz =>
+    simp
+  | hp x ih =>
+    Hint "In the nonnegative case, reduce to the natural power `mpow`."
+    repeat rw [←Int.ofNat_one]
+    repeat rw [Int.ofNat_add_out]
+    repeat rw [gpow_ofNat]
+    rfl
+  | hn x ih =>
+    Hint "In the negative case, use `gpow_negSucc`, `mpow_succ_right`, and cancellation."
+    rw [←Int.negSucc_coe', gpow_negSucc, mpow_succ_right, mul_assoc, inv_mul, mul_one]
+    rw [Int.negSucc_eq, Int.neg_add, Int.neg_add_cancel_right, gpow_neg_mpow]
+    exact inv_mpow g x
+
+
+Conclusion "Good! You now have a recursive rule for integer exponents too."

Game/Levels/PowGroup/L04_PowPred.lean

@@ -0,0 +1,34 @@
+import Game.Levels.PowGroup.L03_PowSucc
+
+World "Group Power"
+Level 4
+
+Title "Subtracting 1 from an Integer Exponent"
+
+namespace MyAlgebra
+
+Introduction "Dually to `g^(n+1)`, we can describe `g^(n-1)` by multiplying with `g⁻¹` on the right."
+
+/--
+For any group element `g` and integer `x`,
+`(g ^ x) * g⁻¹ = g ^ (x - 1)`.
+-/
+TheoremDoc MyAlgebra.gpow_pred as "gpow_pred" in "Group Power"
+Statement gpow_pred {G} [Group G] (g : G) (x : ℤ) :
+  (g ^ x) * g⁻¹ = g ^ (x - 1) := by
+  Hint "You can proceed by cases on `x` (nonnegative / negative) as in the definition of `gpow`."
+  induction x with
+  | ofNat x =>
+    simp only [Int.ofNat_eq_coe]
+    cases x with
+    | zero =>
+      rw [Int.ofNat_zero, gpow_zero]
+      rw [one_mul, Int.zero_sub, gpow_neg_one]
+    | succ x =>
+      simp [gpow, Nat.cast_add, Nat.cast_one]
+      rw [gpow_succ, mul_assoc, mul_inv, mul_one]
+  | negSucc x =>
+    rw [Int.negSucc_sub_one, gpow_negSucc, gpow_negSucc]
+    repeat rw [mpow_succ_right]
+
+Conclusion "Great! You can move down in the exponent by multiplying on the right with `g⁻¹`."

Game/Levels/PowGroup/L05_PowAdd.lean

@@ -0,0 +1,36 @@
+import Game.Levels.PowGroup.L04_PowPred
+
+World "Group Power"
+Level 5
+
+Title "Adding Integer Exponents"
+
+namespace MyAlgebra
+
+Introduction "Now you’ll prove the group version of the exponent-addition law:
+`g ^ x * g ^ y = g ^ (x + y)` for all integers `x`, `y`."
+
+/--
+For any group element `g` and integers `x`, `y`,
+`g ^ x * g ^ y = g ^ (x + y)`.
+-/
+TheoremDoc MyAlgebra.gpow_add as "gpow_add" in "Group Power"
+Statement gpow_add {G} [Group G] (g : G) (x y : ℤ) :
+  (g ^ x) * (g ^ y) = g ^ (x + y) := by
+  Hint "Use `Int.induction_on` on `y`."
+  induction y using Int.induction_on with
+  | hz =>
+    -- y = 0
+    simp
+  | hp y ih =>
+    Hint "Use the recursive formula `gpow_succ` and associativity."
+    simp [← Int.add_assoc, gpow_succ, ← ih, mul_assoc]
+  | hn y ih =>
+    Hint "Use `gpow_pred` for the negative step."
+    rw [← gpow_pred]
+    rw [← mul_assoc]
+    rw [ih]
+    rw [gpow_pred]
+    rw [Int.add_sub_assoc]
+
+Conclusion "Excellent! You have generalized the exponent addition law to all integers."

Game/Levels/PowGroup/L06_PowNeg.lean

@@ -0,0 +1,37 @@
+import Game.Levels.PowGroup.L05_PowAdd
+
+World "Group Power"
+Level 6
+
+Title "Negating the Exponent"
+
+namespace MyAlgebra
+
+Introduction "You’ve seen that negative naturals correspond to inverses.
+Now you’ll prove the full statement: `g ^ (-n) = (g ^ n)⁻¹` for any integer `n`."
+
+/--
+For any group element `g` and integer `n`,
+`g ^ (-n) = (g ^ n)⁻¹`.
+-/
+TheoremDoc MyAlgebra.gpow_neg as "gpow_neg" in "Group Power"
+Statement gpow_neg {G} [Group G] (g : G) (n : ℤ) :
+  g ^ (-n) = (g ^ n)⁻¹ := by
+  Hint "Use `Int.induction_on` on `n`."
+  induction n using Int.induction_on with
+  | hz =>
+    -- n = 0
+    simp [gpow_zero, ←inv_id]
+  | hp n ih =>
+    Hint "Relate `-(n+1)` to `-n - 1` and use `gpow_pred`."
+    rw [Int.neg_add, ←Int.sub_eq_add_neg, ←gpow_pred, ih, inv_anticomm, ←Int.add_comm]
+    rw [←gpow_add]
+    rw [gpow_one]
+  | hn n ih =>
+    Hint "Use the case for a natural number via `gpow_neg_mpow` and your previous lemma."
+    simp at *
+    rw [Int.add_comm, gpow_succ, ih, ←gpow_pred, gpow_neg_mpow, inv_anticomm]
+    repeat rw [← inv_inv]
+    rw [← mpow_succ_right, mpow_succ_left]
+
+Conclusion "Nice! You’ve fully connected negative integer exponents with group inverses."

Game/Levels/PowGroup/L07_PowSub.lean

@@ -0,0 +1,29 @@
+import Game.Levels.PowGroup.L06_PowNeg
+
+World "Group Power"
+Level 7
+
+Title "Subtracting Integer Exponents"
+
+namespace MyAlgebra
+
+Introduction "We now prove the exponent law for subtraction:
+multiplying by the inverse of `g ^ y` corresponds to subtracting `y` in the exponent."
+
+/--
+For any group element `g` and integers `x`, `y`, we have
+`g ^ x * (g ^ y)⁻¹ = g ^ (x - y)`.
+-/
+TheoremDoc MyAlgebra.gpow_sub as "gpow_sub" in "Group Power"
+@[simp]
+Statement gpow_sub {G} [Group G] (g : G) (x y : ℤ) :
+    (g ^ x) * (g ^ y)⁻¹ = g ^ (x - y) := by
+  Hint "Recall that `x - y = x + (-y)`."
+  Hint "Try rewriting `x - y` using `sub_eq_add_neg` and then apply the addition rule `gpow_add` and the negation rule `gpow_neg`."
+  -- First rewrite subtraction as addition with a negative exponent:
+  rw [sub_eq_add_neg]
+  -- Now use the addition and negation lemmas:
+  rw [← gpow_add]
+  rw [gpow_neg]
+
+Conclusion "Nice! You’ve shown that a negative exponent in the second factor corresponds to subtracting exponents."

Game/Levels/PowGroup/L08_PowMul.lean

@@ -0,0 +1,39 @@
+import Game.Levels.PowGroup.L07_PowSub
+
+World "Group Power"
+Level 8
+
+Title "Multiplying Integer Exponents"
+
+namespace MyAlgebra
+
+Introduction "Finally, we prove the multiplication law for integer exponents:
+`g ^ (x * y) = (g ^ x) ^ y`."
+
+/--
+For any group element `g` and integers `x`, `y`,
+we have `g ^ (x * y) = (g ^ x) ^ y`.
+-/
+TheoremDoc MyAlgebra.gpow_mul as "gpow_mul" in "Group Power"
+Statement gpow_mul {G} [Group G] (g : G) (x y : ℤ) :
+    g ^ (x * y) = (g ^ x) ^ y := by
+  Hint "Use `Int.induction_on` on `y` as in earlier levels."
+  induction y using Int.induction_on with
+  | hz =>
+    Hint "Start with `y = 0`."
+    -- x * 0 = 0, and (g^x)^0 = 1
+    simp
+  | hp n ih =>
+    Hint "Use the identity `x * (n+1) = x * n + x` and the addition lemma for powers."
+    -- y = n+1
+    -- g^(x*(n+1)) = g^(x*n + x) = g^(x*n) * g^x
+    -- (g^x)^(n+1) = (g^x)^n * g^x
+    rw [mul_add, mul_one, ←gpow_add, gpow_succ, ih]
+  | hn n ih =>
+    Hint "For the negative step, use `Int.mul_sub` and your subtraction lemma `gpow_sub`."
+    -- y = -[n+1]
+    -- x * (-(n+1)) = x * (-n) - x
+    -- use `gpow_sub` and `gpow_pred` to step down
+    rw [Int.mul_sub, mul_one, ←gpow_sub, ←gpow_pred, ih]
+
+Conclusion "Excellent! You’ve proved the full multiplication law for integer exponents."