advanced addition world almost done

Game/Levels/AdvAddition.lean

@@ -1,23 +1,32 @@
 import Game.Levels.Addition
 import Game.MyNat.AdvAddition -- `zero_ne_succ` and `succ_inj`
 import Game.Levels.AdvAddition.L01assumption
-import Game.Levels.AdvAddition.L02more_assumption
+import Game.Levels.AdvAddition.L02assumption2
 import Game.Levels.AdvAddition.L03apply
-import Game.Levels.AdvAddition.L04succ_inj1
+import Game.Levels.AdvAddition.L04succ_inj
 import Game.Levels.AdvAddition.L05succ_inj2
 import Game.Levels.AdvAddition.L06intro
+import Game.Levels.AdvAddition.L07intro2
+import Game.Levels.AdvAddition.L08add_right_cancel
+import Game.Levels.AdvAddition.L09add_left_cancel
+import Game.Levels.AdvAddition.L10add_left_eq_self
+import Game.Levels.AdvAddition.L11add_right_eq_self
+
 
 World "AdvAddition"
 Title "Advanced Addition World"
 
 Introduction
 "
-In Advanced Addition World we'll learn the `apply` tactic,
-and several other tactics, enabling us to argue both forwards
-and backwards.
+We've proved that $2+2=4$; in Advanced Addition World we'll learn
+how to prove that $2+2\\neq 5$.
 
-We'll use this technique to prove that $2+2\\neq5$
-and much more.
+In Addition World we proved *equalities* like `x + y = y + x`.
+In this world we'll learn how to prove *implications*
+like $x+n=y+n \\implies x=y$. We'll have to learn three new
+tactics to do this: `assumption`, `apply` and `intro`.
+We'll also learn two new fundamental facts about
+natural numbers, which Peano introduced as axioms.
 
 Click on \"Start\" to proceed.
 "

Game/Levels/AdvAddition/L01assumption.lean

@@ -32,5 +32,5 @@ one of our hypotheses.
 
 /-- Assuming $x+y=37$ and $3x+z=42$, we have $x+y=37$. -/
 Statement (x y z : ℕ) (h1 : x + y = 37) (h2 : 3 * x + z = 42) : x + y = 37 := by
-  Hint "The goal is `h1`. Solve the goal by casting `assumption`."
+  Hint "The goal is one of our hypotheses. Solve the goal by casting `assumption`."
   assumption

Game/Levels/AdvAddition/L02assumption2.lean

@@ -0,0 +1,19 @@
+import Game.Levels.Addition
+import Game.MyNat.AdvAddition
+
+World "AdvAddition"
+Level 2
+Title "`assumption` practice."
+
+namespace MyNat
+
+Introduction "If the goal is not *exactly* a hypothesis, we can sometimes
+use rewrites to fix things up."
+
+/-- Assuming $0+x=(0+y)+2$, we have $x=y+2$. -/
+Statement (x : ℕ) (h : 0 + x = 0 + y + 2) : x = y + 2 := by
+  Hint "Rewrite `zero_add` at `h` twice, to change `h` into the goal."
+  repeat rw [zero_add] at h
+  Hint "Now you could finish with `rw [h]` then `rfl`, but `assumption`
+  does it in one line."
+  assumption

Game/Levels/AdvAddition/L03apply.lean

@@ -16,7 +16,7 @@ If `t : P → Q` is a proof that $P\\implies Q$, and `h : P` is a proof of `P`,
 then `apply t at h` will change `h` to a proof of `Q`. The idea is that if
 you know `P` is true, then you can deduce from `t` that `Q` is true.
 
-If the goal is `Q`, then `apply t` will \"argue backwards\" and change the
+If the *goal* is `Q`, then `apply t` will \"argue backwards\" and change the
 goal to `P`. The idea here is that if you want to prove `Q`, then by `t`
 it suffices to prove `P`, so you can reduce the goal to proving `P`.
 
@@ -43,8 +43,8 @@ hypothesis with the `apply` tactic.
 "
 
 /-- If $x=37$ and we know that $x=37\implies y=42$ then we can deduce $y=42$. -/
-Statement (x y : ℕ) (hx : x = 37) (h : x = 37 → y = 42) : y = 42 := by
-  Hint "Start with `apply h at hx`."
-  apply h at hx
+Statement (x y : ℕ) (h : x = 37) (imp : x = 37 → y = 42) : y = 42 := by
+  Hint "Start with `apply imp at h`. This will change `h` to `y = 42`."
+  apply imp at h
   Hint "Now finish with `assumption`."
   assumption

Game/Levels/AdvAddition/L04succ_inj1.lean → Game/Levels/AdvAddition/L04succ_inj.lean

@@ -16,9 +16,10 @@ that `succ a = succ b` implies `a = b`. Click on this theorem in the *Peano*
 tab for more information.
 
 Peano had this theorem as an axiom, but in Functional Programming World
-we will show how to prove it. Right now let's just assume it,
-and let's solve an equation using it. We will solve the equation
-by manipulating our hypothesis until it becomes the goal.
+we will show how to prove it in Lean. Right now let's just assume it,
+and let's solve an equation using it. Again, we will proceed
+by manipulating our hypothesis until it becomes the goal. I will
+walk you through this level.
 "
 
 LemmaDoc MyNat.succ_inj as "succ_inj" in "Peano" "
@@ -40,7 +41,7 @@ $ (\\operatorname{succ}(a) = \\operatorname{succ}(b))\\implies a=b$.
 You can think of `succ_inj` itself as a proof; it is the proof
 that `succ` is an injective function. In other words,
 `succ_inj` is a proof of
-$\\forall a b\\in \\mathbb{N}, (\\operatorname{succ}(a) = \\operatorname{succ}(b))\\implies a=b$.
+$\\forall a, b\\in \\mathbb{N}, (\\operatorname{succ}(a) = \\operatorname{succ}(b))\\implies a=b$.
 
 `succ_inj` was postulated as an axiom by Peano, but
 in Lean it can be proved using `pred`, a mathematically

Game/Levels/AdvAddition/L05succ_inj2.lean

@@ -12,7 +12,9 @@ Introduction
   In the last level, we manipulated the hypothesis `x + 1 = 4`
   until it became the goal `x = 3`. In this level we'll manipulate
   the goal until it becomes our hypothesis! In other words, we
-  will \"argue backwards\".
+  will \"argue backwards\". The `apply` tactic can do this too.
+  Again I will walk you through this one (assuming you're in
+  command line mode).
 "
 
 /-- If $x+1=4$ then $x=3$. -/

Game/Levels/AdvAddition/L06intro.lean

@@ -7,17 +7,33 @@ Title "intro"
 
 namespace MyNat
 
+TacticDoc intro "
+## Summary
+
+If the goal is `P → Q`, then `intro h` will introduce `h : P` as a hypothesis,
+and change the goal to `Q`. Mathematically, it says that to prove $P\\implies Q$,
+we can assume $P$ and then prove $Q$.
+
+### Example:
+
+If your goal is `x + 1 = y + 1 → x = y` (the way Lean writes $x+1=y+1\\implies x=y$)
+then `intro h` will give you a hypothesis $x+1=y+1$ named `h`, and the goal
+will change to $x=y$.
+"
+NewTactic intro
+
+
 Introduction
-" We have seen how to `apply` theorems and assumptions of
+"We have seen how to `apply` theorems and assumptions of
 of the form `P → Q`. But what if our *goal* is of the form `P → Q`?
-We need to know how to say \"let's assume `P`\" in Lean.
-We do this with the `intro` tactic, the last tactic you need
+To prove this goal, we need to know how to say \"let's assume `P` and deduce `Q`\"
+in Lean. We do this with the `intro` tactic, the last tactic you need
 to learn to solve all the levels in this world.
 "
 
-/-- $x=37\\implies x=37$. -/
+/-- $x=37\implies x=37$. -/
 Statement (x : ℕ) : x = 37 → x = 37 := by
-  Hint "Start with `intro h` to assume the hypothesis."
+  Hint "Start with `intro h` to assume the hypothesis and call its proof `h`."
   intro h
   Hint (hidden := true) "Now `assumption` finishes the job."
   assumption

Game/Levels/AdvAddition/L07intro2.lean

@@ -0,0 +1,28 @@
+import Game.Levels.Addition
+import Game.MyNat.AdvAddition
+
+World "AdvAddition"
+Level 7
+Title "intro practice"
+
+namespace MyNat
+
+Introduction
+" Let's see if you can use the tactics we've learnt to prove $x+1=y+1\\implies x=y$.
+Try this one by yourself; if you need help then click on \"Show more help!\".
+"
+
+/-- $x+1=y+1\implies x=y$. -/
+Statement (x : ℕ) : x + 1 = y + 1 → x = y := by
+  Hint (hidden := true) "Start with `intro h` to assume the hypothesis."
+  intro h
+  Hint (hidden := true) "Now `repeat rw [← succ_eq_add_one] at h` is the quickest way to
+  change `succ x = succ y`."
+  repeat rw [← succ_eq_add_one] at h
+  Hint (hidden := true) "Now `apply succ_inj at h` to cancel the `succ`s."
+  apply succ_inj at h
+  Hint (hidden := true) "Now `rw [h]` then `rfl` works, but `assumption` is quicker."
+  assumption
+
+Conclusion "These worlds have been a tutorial on our new tactics. Now let's use them
+to prove some more fundamental facts about the naturals which we will need in later worlds."

Game/Levels/AdvAddition/L08add_right_cancel.lean

@@ -0,0 +1,36 @@
+import Game.Levels.Addition
+import Game.MyNat.AdvAddition
+
+World "AdvAddition"
+Level 8
+Title "add_right_cancel"
+
+namespace MyNat
+
+LemmaTab "Add"
+
+LemmaDoc MyNat.add_right_cancel as "add_right_cancel" in "Add" "
+
+`add_right_cancel a b n` is the theorem that $a+n=b+n \\implies a=b.$
+"
+
+NewLemma MyNat.add_right_cancel
+
+Introduction
+"`add_right_cancel a b n` is the theorem that $a+n=b+n\\implies a=b$.
+Start with `induction n with d hd` and see if you can take it from there.
+"
+
+/-- $a+n=b+n\\implies a=b$. -/
+Statement add_right_cancel (a b n : ℕ) : a + n = b + n → a = b := by
+  induction n with d hd
+  intro h
+  repeat rw [add_zero] at h
+  assumption
+  intro h
+  repeat rw [add_succ] at h
+  apply succ_inj at h
+  apply hd at h
+  assumption
+
+Conclusion "Nice!"

Game/Levels/AdvAddition/L09add_left_cancel.lean

@@ -0,0 +1,28 @@
+import Game.Levels.AdvAddition.L08add_right_cancel
+
+World "AdvAddition"
+Level 9
+Title "add_left_cancel"
+
+namespace MyNat
+
+LemmaTab "Add"
+
+LemmaDoc MyNat.add_left_cancel as "add_left_cancel" in "Add" "
+
+`add_left_cancel a b n` is the theorem that $n+a=n+b \\implies a=b.$
+"
+
+NewLemma MyNat.add_left_cancel
+
+Introduction
+"`add_left_cancel a b n` is the theorem that $n+a=n+b\\implies a=b$.
+You can prove it by induction on `n` or you can deduce it from `add_left_cancel`.
+"
+
+/-- $a+n=b+n\implies a=b$. -/
+Statement add_left_cancel (a b n : ℕ) : n + a = n + b → a = b := by
+  repeat rw [add_comm n]
+  intro h
+  apply add_right_cancel at h
+  assumption

Game/Levels/AdvAddition/L10add_left_eq_self.lean

@@ -0,0 +1,42 @@
+import Game.Levels.AdvAddition.L09add_left_cancel
+
+World "AdvAddition"
+Level 10
+Title "add_left_eq_self"
+
+namespace MyNat
+
+LemmaTab "Add"
+
+LemmaDoc MyNat.add_left_eq_self as "add_left_eq_self" in "Add" "
+
+`add_left_eq_self x y` is the theorem that $x + y = y\\implies x=0.$
+"
+
+NewLemma MyNat.add_left_eq_self
+
+Introduction
+"
+`add_left_eq_self x y` is the theorem that $x + y = y\\implies x=0.$
+"
+
+/-- $x + y = y\implies x=0.$ -/
+Statement add_left_eq_self (x y : ℕ) : x + y = y → x = 0 := by
+  intro h
+  nth_rewrite 2 [← zero_add y] at h
+  apply add_right_cancel at h
+  assumption
+
+Conclusion "Did you use induction on `y`?
+Here's a proof of `add_left_eq_self` which uses `add_right_cancel`.
+If you want to inspect it, you can go into editor mode by clicking `</>` in the top right
+and then just cut and paste the proof and move your cursor around it
+(although you'll lose your own proof this way if you're not careful). Click `>_` to get
+back to command line mode.
+```
+intro h
+nth_rewrite 2 [← zero_add y] at h
+apply add_right_cancel at h
+assumption
+```
+"

Game/Levels/AdvAddition/L11add_right_eq_self.lean

@@ -0,0 +1,36 @@
+import Game.Levels.AdvAddition.L10add_left_eq_self
+
+World "AdvAddition"
+Level 11
+Title "add_right_eq_self"
+
+LemmaTab "Add"
+
+namespace MyNat
+
+LemmaDoc MyNat.add_right_eq_self as "add_right_eq_self" in "Add" "
+
+`add_right_eq_self x y` is the theorem that $x + y = x\\implies y=0.$
+"
+
+NewLemma MyNat.add_right_eq_self
+
+Introduction
+"`add_right_eq_self x y` is the theorem that $x + y = x\\implies y=0.$
+"
+
+/-- $a+n=b+n\implies a=b$. -/
+Statement add_right_eq_self (x y : ℕ) : x + y = x → y = 0 := by
+  rw [add_comm]
+  intro h
+  apply add_left_eq_self at h
+  assumption
+
+Conclusion "Here's a proof using `add_left_eq_self`:
+```
+rw [add_comm]
+intro h
+apply add_left_eq_self at h
+assumption
+```
+"