final tinkering with implication and advanced addition world

Game/Levels/AdvAddition/L01ne_succ_self.lean

@@ -1,4 +1,4 @@
-import Game.Levels.Implication.L11two_add_two_ne_five
+import Game.Levels.Implication
 
 World "AdvAddition"
 Level 1

Game/Levels/AdvAddition/L03add_left_cancel.lean

@@ -26,3 +26,11 @@ Statement add_left_cancel (a b n : ℕ) : n + a = n + b → a = b := by
   intro h
   apply add_right_cancel at h
   exact h
+
+Conclusion
+"How about this for a proof:
+```
+repeat rw [add_comm n]
+exact add_right_cancel a b n
+```
+"

Game/Levels/AdvAddition/L04add_left_eq_self.lean

@@ -28,16 +28,14 @@ Statement add_left_eq_self (x y : ℕ) : x + y = y → x = 0 := by
   exact h
 
 Conclusion "Did you use induction on `y`?
-Here's a proof of `add_left_eq_self` which uses `add_right_cancel`.
+Here's a two-line 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
 to see the hypotheses and goal at any given point
 (although you'll lose your own proof this way). Click `>_` to get
 back to command line mode.
 ```
-intro h
-nth_rewrite 2 [← zero_add y] at h
-apply add_right_cancel at h
-exact h
+nth_rewrite 2 [← zero_add y]
+exact add_right_cancel x 0 y
 ```
 "

Game/Levels/AdvAddition/L06eq_zero_of_add_right_eq_zero.lean

@@ -21,17 +21,15 @@ The `contradiction` tactic will solve any goal, if you have a hypothesis `h : Fa
 "
 NewTactic contradiction
 
-LemmaDoc MyNat.eq_zero_of_add_eq_zero_right as "eq_zero_of_add_eq_zero_right" in "Add" "
+LemmaDoc MyNat.eq_zero_of_add_right_eq_zero as "eq_zero_of_add_right_eq_zero" in "Add" "
   A proof that $a+b=0 \\implies a=0$.
 "
 
--- **TODO** `symm` tactic
-
 -- **TODO** why `add_eq_zero_right` and not `add_right_eq_zero`?
 -- https://leanprover.zulipchat.com/#narrow/stream/348111-std4/topic/eq_zero_of_add_eq_zero_right/near/395716874
 
 /-- If $a+b=0$ then $a=0$. -/
-Statement eq_zero_of_add_eq_zero_right (a b : ℕ) : a + b = 0 → a = 0 := by
+Statement eq_zero_of_add_right_eq_zero (a b : ℕ) : a + b = 0 → a = 0 := by
   Hint "We want to deal with the cases `b = 0` and `b ≠ 0` separately, so start with `induction b with d hd`
   but just ignore the inductive hypothesis in the `succ d` case :-)"
   induction b with d _ -- don't even both naming inductive hypo

Game/Levels/AdvAddition/L07eq_zero_of_add_left_eq_zero.lean

@@ -4,7 +4,7 @@ World "AdvAddition"
 Level 7
 Title "eq_zero_of_add_left_eq_zero"
 
-LemmaTab "Peano"
+LemmaTab "Add"
 
 namespace MyNat
 
@@ -13,22 +13,20 @@ Introduction
 of using it.
 "
 
-LemmaDoc MyNat.eq_zero_of_add_eq_zero_left as "eq_zero_of_add_eq_zero_left" in "Add" "
+LemmaDoc MyNat.eq_zero_of_add_left_eq_zero as "eq_zero_of_add_left_eq_zero" in "Add" "
   A proof that $a+b=0 \\implies b=0$.
 "
 
--- **TODO** why `add_eq_zero_right` and not `add_right_eq_zero`?
-
 /-- If $a+b=0$ then $b=0$. -/
-Statement eq_zero_of_add_eq_zero_left (a b : ℕ) : a + b = 0 → b = 0 := by
+Statement eq_zero_of_add_left_eq_zero (a b : ℕ) : a + b = 0 → b = 0 := by
   rw [add_comm]
-  exact eq_zero_of_add_eq_zero_right b a
+  exact eq_zero_of_add_right_eq_zero b a
 
 Conclusion "How about this for a proof:
 
 ```
 rw [add_comm]
-exact eq_zero_of_add_eq_zero_right b a
+exact eq_zero_of_add_left_eq_zero b a
 ```
 
 You're now ready for LessThanOrEqual World.

Game/Levels/Implication.lean

@@ -18,10 +18,10 @@ Introduction
 We've proved that $2+2=4$; in Implication World we'll learn
 how to prove $2+2\\neq 5$.
 
-In Addition World we proved *equalities* like `x + y = y + x`.
+In Addition World we proved *equalities* like $x + y = y + x$.
 In this second tutorial world we'll learn some new tactics,
 enabling us to prove *implications*
-like $x+1=4 \\implies x=3.
+like $x+1=4 \\implies x=3.$
 
 We'll also learn two new fundamental facts about
 natural numbers, which Peano introduced as axioms.

Game/Levels/Implication/L01exact.lean

@@ -21,9 +21,16 @@ then `exact h` will solve the goal.
 
 If the goal is `x + 0 = x` then `exact add_zero x` will close the goal.
 
-Note that `exact add_zero` will *not work*; the proof has to be exactly
-a proof of the goal. `add_zero` is a proof of `∀ n, n + 0 = n` or, if you like,
-a proof of `? + 0 = ?` where `?` is yet to be supplied.
+### Exact needs to be exactly right
+
+Note that `exact add_zero` will *not work* in the previous example;
+for `exact h` to work, `h` has to be *exactly* a proof of the goal.
+`add_zero` is a proof of `∀ n, n + 0 = n` or, if you like,
+a proof of `? + 0 = ?` where `?` needs to be supplied by the user.
+This is in contrast to `rw` and `apply`, which will \"guess the inputs\"
+if necessary. If the goal is `x + 0 = x` then `rw [add_zero]`
+and `rw [add_zero x]` will both change the goal to `x = x`,
+because `rw` guesses the input to the function `add_zero`.
 "
 
 NewTactic exact

Game/Levels/Implication/L04succ_inj.lean

@@ -16,7 +16,7 @@ tab for more information.
 
 Peano had this theorem as an axiom, but in Functional Programming World
 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
+and let's prove $x+1=4 \\implies x=3$ using it. Again, we will proceed
 by manipulating our hypothesis until it becomes the goal. I will
 walk you through this level.
 "
@@ -51,7 +51,7 @@ NewLemma MyNat.succ_inj
 
 /-- If $x+1=4$ then $x=3$. -/
 Statement (x : ℕ) (h : x + 1 = 4) : x = 3 := by
-  Hint "Let's first get `h` into the form `succ x = succ 3.` so we can
+  Hint "Let's first get `h` into the form `succ x = succ 3` so we can
   apply `succ_inj`. First rewrite
   `four_eq_succ_three` at `h` to change the 4 on the right hand side."
   rw [four_eq_succ_three] at h
@@ -60,7 +60,7 @@ Statement (x : ℕ) (h : x + 1 = 4) : x = 3 := by
   Hint (hidden := true) "`rw [← succ_eq_add_one] at h`. Look at the
   docs for `rw` for an explanation. Type `←` with `\\l`."
   rw [←succ_eq_add_one] at h
-  Hint "Now let's `apply` our new theorem. Cast `apply succ_inj at h`
+  Hint "Now let's `apply` our new theorem. Execute `apply succ_inj at h`
   to change `h` to a proof of `x = 3`."
   apply succ_inj at h
   Hint "Now finish in one line."

Game/Levels/Implication/L07intro2.lean

@@ -22,3 +22,12 @@ Statement (x : ℕ) : x + 1 = y + 1 → x = y := by
   apply succ_inj at h
   Hint (hidden := true) "Now `rw [h]` then `rfl` works, but `exact h` is quicker."
   exact h
+
+Conclusion "Here's a completely backwards proof:
+```
+intro h
+repeat rw [succ_eq_add_one]
+apply succ_inj
+exact h
+```
+"

Game/Levels/Implication/L08ne.lean

@@ -10,9 +10,11 @@ namespace MyNat
 
 Introduction
 "We still can't prove `2 + 2 ≠ 5` because we have not talked about the
-definition of `≠`. In Lean, `a ≠ b` is *defined* to mean `a = b → False`.
-Here `False` is a generic false proposition, and this definition works
-because `True → False` is false, but `False → False` is true.
+definition of `≠`. In Lean, `a ≠ b` is *notation* for `a = b → False`.
+Here `False` is a generic false proposition, and `→` is Lean's notation
+for \"implies\". In logic we learn
+that `True → False` is false, but `False → False` is true. Hence
+`X → false` is the logical opposite of `X`.
 
 Even though `a ≠ b` does not look like an implication,
 you should treat it as an implication. The next two levels will show you how.
@@ -24,8 +26,9 @@ are contradictory, which they are in this level.
 
 /-- If $x=y$ and $x \neq y$ then we can deduce a contradiction. -/
 Statement (x y : ℕ) (h1 : x = y) (h2 : x ≠ y) : False := by
-  Hint "Try `apply`ing `h2` either `at h1` or directly to the goal."
+  Hint "Remember that `h2` is a proof of `x = y → False`. Try
+  `apply`ing `h2` either `at h1` or directly to the goal."
   apply h2 at h1
   exact h1
 
-Conclusion "Remember, `x ≠ y` is *notation* for `x = y → False`"
+Conclusion "Remember, `x ≠ y` is *notation* for `x = y → False`."

Game/Levels/Implication/L09zero_ne_succ.lean

@@ -34,8 +34,10 @@ NewLemma MyNat.zero_ne_succ MyNat.zero_ne_one
 Statement zero_ne_one : (0 : ℕ) ≠ 1 := by
   Hint "Start with `intro h`."
   intro h
+  Hint "Now change `1` to `succ 0` in `h`."
   rw [one_eq_succ_zero] at h  -- **TODO** this line is not needed :-/
+  Hint "Now you can `apply zero_ne_succ at h`."
   apply zero_ne_succ at h -- **TODO** cripple `apply`.
   exact h
 
-Conclusion "Remember, `x ≠ y` is *notation* for `x = y → false`"
+Conclusion "Nice!"

Game/Levels/Implication/L11two_add_two_ne_five.lean

@@ -9,9 +9,9 @@ LemmaTab "Peano"
 namespace MyNat
 
 Introduction
-" 2 + 2 ≠ 5 is really boring to prove, given the tools we have. To make it a lot less
-painful, I have unfolded all of the numerals. See if you can use `zero_ne_succ` and
-`succ_inj` to prove this.
+" 2 + 2 ≠ 5 is boring to prove in full, given only the tools we have currently.
+To make it a bit less painful, I have unfolded all of the numerals for you.
+See if you can use `zero_ne_succ` and `succ_inj` to prove this.
 "
 
 /-- $2+2≠5$. -/