From 5f3f51144a5a35fab6a1395540b1af522077a700 Mon Sep 17 00:00:00 2001 From: Kevin Buzzard Date: Thu, 5 Oct 2023 14:16:57 +0100 Subject: [PATCH] a little tidying --- Game/Levels/AdvAddition/Level_5.lean | 81 ---------------------------- Game/Levels/AdvAddition/Level_6.lean | 43 --------------- 2 files changed, 124 deletions(-) delete mode 100644 Game/Levels/AdvAddition/Level_5.lean delete mode 100644 Game/Levels/AdvAddition/Level_6.lean diff --git a/Game/Levels/AdvAddition/Level_5.lean b/Game/Levels/AdvAddition/Level_5.lean deleted file mode 100644 index 76f0a50..0000000 --- a/Game/Levels/AdvAddition/Level_5.lean +++ /dev/null @@ -1,81 +0,0 @@ -import Game.Levels.AdvAddition.Level_4 - - - -World "AdvAddition" -Level 5 -Title "add_right_cancel" - -open MyNat - -Introduction -" -The theorem `add_right_cancel` is the theorem that you can cancel on the right -when you're doing addition -- if `a + t = b + t` then `a = b`. -" - -/-- On the set of natural numbers, addition has the right cancellation property. -In other words, if there are natural numbers $a, b$ and $c$ such that -$$ a + t = b + t, $$ -then we have $a = b$. -/ -Statement MyNat.add_right_cancel - (a t b : ℕ) : a + t = b + t → a = b := by - Hint (hidden := true) "You can either start with `induction t` or with - `intro` and you will have to do the other one afterwards." - Branch - intro h - Hint "I'd recommend now induction on `t`. Don't forget that `rw [add_zero] at h` can be used - to do rewriting of hypotheses rather than the goal." - induction t with d hd - · Hint "You might have noticed an old `{h}✝` floating - around in your assumptions. `x✝` marks variables that can't be used - anymore because a new variable got assigned the name `x`. - In your case that is because `induction` deleted the old `{h}` when - it created the `t=0` (or later `succ t`) variants. Just ignore the - `{h}✝`." - rw [add_zero] at h - rw [add_zero] at h - exact h - · Hint "You might have noticed an old `{h}✝` floating - around in your assumptions. `x✝` marks variables that can't be used - anymore because a new variable got assigned the name `x`. - In your case that is because `induction` deleted the old `{h}` when - it created the `succ t` variant. Just ignore the `{h}✝`." - Branch - simp at h - exact hd h - apply hd - rw [add_succ] at h - rw [add_succ] at h - exact succ_inj h - induction t with d hd - · Hint (hidden := true) "You want to look at `intro`." - Branch - simp - intro h - rw [add_zero] at h - rw [add_zero] at h - exact h - · Hint "Since you called `induction t` first, you now have to call - `intro` on each of the subgoals." - Hint (hidden := true) "You want to look at `intro`" - Branch - simp - exact hd - intro h - apply hd - rw [add_succ] at h - rw [add_succ] at h - Hint (hidden := true) "At this point `succ_inj` might be useful." - exact succ_inj h - - --- TODO: Display at this level after induction is confusing: old assumption floating in context - -LemmaTab "Add" -DisabledTactic simp - -Conclusion -" - -" diff --git a/Game/Levels/AdvAddition/Level_6.lean b/Game/Levels/AdvAddition/Level_6.lean deleted file mode 100644 index ed3c788..0000000 --- a/Game/Levels/AdvAddition/Level_6.lean +++ /dev/null @@ -1,43 +0,0 @@ -import Game.Levels.AdvAddition.Level_5 - - -World "AdvAddition" -Level 6 -Title "add_left_cancel" - -open MyNat - -Introduction -" -The theorem `add_left_cancel` is the theorem that you can cancel on the left -when you're doing addition -- if `t + a = t + b` then `a = b`. -" - -/-- On the set of natural numbers, addition has the left cancellation property. -In other words, if there are natural numbers $a, b$ and $t$ such that -$$ t + a = t + b, $$ -then we have $a = b$. -/ -Statement MyNat.add_left_cancel - (t a b : ℕ) : t + a = t + b → a = b := by - Branch - induction t - · simp - · simp - exact n_ih - Hint "There is a three-line proof which ends in `exact add_right_cancel a t b` (or even - `exact add_right_cancel _ _ _`); this - strategy involves changing the goal to the statement of `add_right_cancel` somehow." - rw [add_comm] - rw [add_comm t] - Hint "Now that looks like `add_right_cancel`!" - Hint (hidden := true) "`exact add_right_cancel` does not work. You need - `exact add_right_cancel a t b` or `exact add_right_cancel _ _ _`." - exact add_right_cancel a t b - -LemmaTab "Add" -DisabledTactic simp - -Conclusion -" - -"