From b81f2eccedd8530174c111af833dbd29913f3624 Mon Sep 17 00:00:00 2001 From: Kevin Buzzard Date: Thu, 21 Dec 2023 17:12:40 +0000 Subject: [PATCH] Advanced multiplication minor reorganisation --- .../L03one_le_of_zero_ne.lean | 30 -------------- .../L04one_le_of_zero_ne.lean | 26 ++++++++++++ ...le_mul_right.lean => L05le_mul_right.lean} | 14 +++---- Game/Levels/AdvMultiplication/L05le_one.lean | 40 ------------------- .../L06mul_right_eq_one.lean | 18 +++++---- 5 files changed, 43 insertions(+), 85 deletions(-) delete mode 100644 Game/Levels/AdvMultiplication/L03one_le_of_zero_ne.lean create mode 100644 Game/Levels/AdvMultiplication/L04one_le_of_zero_ne.lean rename Game/Levels/AdvMultiplication/{L04le_mul_right.lean => L05le_mul_right.lean} (65%) delete mode 100644 Game/Levels/AdvMultiplication/L05le_one.lean diff --git a/Game/Levels/AdvMultiplication/L03one_le_of_zero_ne.lean b/Game/Levels/AdvMultiplication/L03one_le_of_zero_ne.lean deleted file mode 100644 index 1653b26..0000000 --- a/Game/Levels/AdvMultiplication/L03one_le_of_zero_ne.lean +++ /dev/null @@ -1,30 +0,0 @@ -import Game.Levels.AdvMultiplication.L02mul_left_ne_zero - -World "AdvMultiplication" -Level 3 -Title "one_le_of_zero_ne" - -LemmaTab "≤" - -namespace MyNat - -LemmaDoc MyNat.one_le_of_zero_ne as "one_le_of_zero_ne" in "≤" " -`one_le_of_zero_ne a` is a proof that `a ≠ 0 → 1 ≤ a`. -" - -Introduction -"We need to understand how to use a hypothesis like `a ≠ 0`. -Here is a useful lemma. I talk through how to get started in the hidden hints. -Access them by clicking on \"Show more help!\" -" - -Statement one_le_of_zero_ne (a : ℕ) (ha : a ≠ 0) : 1 ≤ a := by - Hint (hidden := true) "Start with `cases a with n` to do a case split on `a = 0` and `a = succ n`." - cases a with n - · Hint (hidden := true) "You have a false hypothesis so you can just solve this with the logic - tactic `tauto`." - tauto - · use n - rw [succ_eq_add_one] - rw [add_comm] - rfl diff --git a/Game/Levels/AdvMultiplication/L04one_le_of_zero_ne.lean b/Game/Levels/AdvMultiplication/L04one_le_of_zero_ne.lean new file mode 100644 index 0000000..7d85759 --- /dev/null +++ b/Game/Levels/AdvMultiplication/L04one_le_of_zero_ne.lean @@ -0,0 +1,26 @@ +import Game.Levels.AdvMultiplication.L03eq_succ_of_ne_zero + +World "AdvMultiplication" +Level 4 +Title "one_le_of_ne_zero" + +LemmaTab "≤" + +namespace MyNat + +LemmaDoc MyNat.one_le_of_ne_zero as "one_le_of_ne_zero" in "≤" " +`one_le_of_ne_zero a` is a proof that `a ≠ 0 → 1 ≤ a`. +" + +Introduction +"The previous lemma can be used to prove this one. +" + +Statement one_le_of_ne_zero (a : ℕ) (ha : a ≠ 0) : 1 ≤ a := by + Hint (hidden := true) "Use the previous lemma with `apply eq_succ_of_ne_zero at ha`." + apply eq_succ_of_ne_zero at ha + Hint (hidden := true) "Now take apart the existence statement with `cases ha with n hn`." + cases ha with n hn + use n + rw [hn, succ_eq_add_one, add_comm] + rfl diff --git a/Game/Levels/AdvMultiplication/L04le_mul_right.lean b/Game/Levels/AdvMultiplication/L05le_mul_right.lean similarity index 65% rename from Game/Levels/AdvMultiplication/L04le_mul_right.lean rename to Game/Levels/AdvMultiplication/L05le_mul_right.lean index 6a693e0..95a482a 100644 --- a/Game/Levels/AdvMultiplication/L04le_mul_right.lean +++ b/Game/Levels/AdvMultiplication/L05le_mul_right.lean @@ -1,7 +1,7 @@ -import Game.Levels.AdvMultiplication.L03one_le_of_zero_ne +import Game.Levels.AdvMultiplication.L04one_le_of_zero_ne World "AdvMultiplication" -Level 4 +Level 5 Title "le_mul_right" LemmaTab "≤" @@ -18,15 +18,15 @@ has to be at most that number. Introduction " In Prime Number World we will be proving that $2$ is prime. -To do this, we will have to rule out things like $2 \neq 323846224*3453453459182.$ +To do this, we will have to rule out things like $2 ≠ 323846224 \times 3453453459182.$ We will do this by proving that any factor of $2$ is at most $2$, -which we will do using this lemma. The proof I have in mind uses -everything which we've proved in this world so far. +which we will do using this lemma. The proof I have in mind manipulates the hypothesis +until it becomes the goal, using pretty much everything which we've proved in this world so far. " Statement le_mul_right (a b : ℕ) (h : a * b ≠ 0) : a ≤ a * b := by apply mul_left_ne_zero at h - apply one_le_of_zero_ne at h + apply one_le_of_ne_zero at h apply mul_le_mul_right 1 b a at h rw [one_mul, mul_comm] at h exact h @@ -34,7 +34,7 @@ Statement le_mul_right (a b : ℕ) (h : a * b ≠ 0) : a ≤ a * b := by Conclusion "Here's what I was thinking of: ``` apply mul_left_ne_zero at h -apply one_le_of_zero_ne at h +apply one_le_of_ne_zero at h apply mul_le_mul_right 1 b a at h rw [one_mul, mul_comm] at h exact h diff --git a/Game/Levels/AdvMultiplication/L05le_one.lean b/Game/Levels/AdvMultiplication/L05le_one.lean deleted file mode 100644 index 7598462..0000000 --- a/Game/Levels/AdvMultiplication/L05le_one.lean +++ /dev/null @@ -1,40 +0,0 @@ -import Game.Levels.AdvMultiplication.L04le_mul_right - -World "AdvMultiplication" -Level 5 -Title "le_one" - -LemmaTab "≤" - -namespace MyNat - -LemmaDoc MyNat.le_one as "le_one" in "≤" " -`le_one a b` is a proof that `a * b ≠ 0 → a ≤ a * b`. - -It's one way of saying that a divisor of a positive number -has to be at most that number. -" - -Introduction -"We could have proved this result in ≤ World. I leave some hidden hints. -" - -Statement le_one (a : ℕ) (ha : a ≤ 1) : a = 0 ∨ a = 1 := by - Hint (hidden := true) "Start with `cases a with b` to break into `a = 0` and `a = succ b` cases." - cases a with b - · left - rfl - · Hint (hidden := true) "Now `cases b with c`." - cases b with c - · right - rw [one_eq_succ_zero] - rfl - · Hint (hidden := true) "Now `cases ha with x hx` and work on `hx` until it's `False`. - Then use a logic tactic to finish." - cases ha with x hx - rw [succ_add, succ_add] at hx - rw [one_eq_succ_zero] at hx - apply succ_inj at hx - apply zero_ne_succ at hx - Hint (hidden := true) "Now finish with `tauto`." - tauto diff --git a/Game/Levels/AdvMultiplication/L06mul_right_eq_one.lean b/Game/Levels/AdvMultiplication/L06mul_right_eq_one.lean index da8e69d..bb60779 100644 --- a/Game/Levels/AdvMultiplication/L06mul_right_eq_one.lean +++ b/Game/Levels/AdvMultiplication/L06mul_right_eq_one.lean @@ -1,4 +1,4 @@ -import Game.Levels.AdvMultiplication.L05le_one +import Game.Levels.AdvMultiplication.L05le_mul_right World "AdvMultiplication" Level 6 @@ -53,8 +53,11 @@ LemmaDoc MyNat.mul_right_eq_one as "mul_right_eq_one" in "*" " Introduction " -This is the multiplicative analogue of Advanced Addition World's `x + y = 0 → x = 0`. -We'll prove it using a new tactic called `have`. +This level proves `x * y = 1 → x = 1`, the multiplicative analogue of Advanced Addition +World's `x + y = 0 → x = 0`. The strategy is to prove that `x ≤ 1` and then use the +lemma `le_one` from `≤` world. + +We'll prove it using a new and very useful tactic called `have`. " Statement mul_right_eq_one (x y : ℕ) (h : x * y = 1) : x = 1 := by @@ -63,9 +66,8 @@ Statement mul_right_eq_one (x y : ℕ) (h : x * y = 1) : x = 1 := by prove it, and then you'll have a new hypothesis which you can apply `le_mul_right` to." have hx : x * y ≠ 0 - rw [h, one_eq_succ_zero] - symm - apply zero_ne_succ + rw [h] + exact one_ne_zero Hint (hidden := true) "Now you can `apply le_mul_right at hx`." apply le_mul_right at hx Hint (hidden := true) "Now `rw [h] at hx` so you can `apply le_one at hx`." @@ -75,6 +77,6 @@ Statement mul_right_eq_one (x y : ℕ) (h : x * y = 1) : x = 1 := by cases separately." cases hx with h0 h1 · rw [h0, zero_mul] at h - apply zero_ne_succ at h + Hint (hidden := true) "`tauto` is good enough to solve this goal." tauto - exact h1 + · exact h1