algorithm world rc0

Game.lean

@@ -16,8 +16,7 @@ import Game.Levels.LessOrEqual
 --import Game.Levels.Prime
 --import Game.Levels.StrongInduction
 --import Game.Levels.Hard
---import Game.Levels.FunctionalProgram
---import Game.Levels.Algorithm
+import Game.Levels.Algorithm
 
 -- Here's what we'll put on the title screen
 Title "Natural Number Game"
@@ -103,6 +102,7 @@ Dependency Addition → Multiplication → Power
 --Dependency Multiplication → AdvMultiplication
 --Dependency AdvAddition → EvenOdd → Inequality → StrongInduction
 Dependency Addition → Implication → AdvAddition → LessOrEqual
+Dependency AdvAddition → Algorithm
 -- The game automatically computes connections between worlds based on introduced
 -- tactics and theorems, but for example it cannot detect introduced definitions
 

Game/Levels/Algorithm.lean

@@ -1,5 +1,10 @@
 import Game.Levels.Algorithm.L01add_left_comm
 import Game.Levels.Algorithm.L02add_algo1
+import Game.Levels.Algorithm.L03add_algo2
+import Game.Levels.Algorithm.L04pred
+import Game.Levels.Algorithm.L05is_zero
+import Game.Levels.Algorithm.L06succ_ne_succ
+import Game.Levels.Algorithm.L07decide
 
 World "Algorithm"
 Title "Algorithm World"

Game/Levels/Algorithm/L02add_algo1.lean

@@ -11,24 +11,27 @@ namespace MyNat
 Introduction
 "
 In some later worlds, we're going to see some much nastier levels,
-like `(a + b) + (c + d) = ((a + c) + d) + b`. Brackets need
-to be moved around, and variables need to be swapped.
+like `(a + a + 1) + (b + b + 1) = (a + b + 1) + (a + b + 1)`.
+Brackets need to be moved around, and variables need to be swapped.
 
-Forgetting about the brackets for now, we see that to
-turn `a+b+c+d` into `a+c+d+b` we need to swap `b` and `c`,
+In this level, `(a + b) + (c + d) = ((a + c) + b) + d`,
+let's forget about the brackets and just think about
+the variable order.
+To turn `a+b+c+d` into `a+c+d+b` we need to swap `b` and `c`,
 and then swap `b` and `d`. But this is easier than you
 think with `add_left_comm`.
 "
 
 /-- If $a, b$, $c$ and $d$ are numbers, we have
-$(a + b) + (c + d) = ((a + c) + d) + b. -/
+$(a + b) + (c + d) = ((a + c) + d) + b.$ -/
 Statement (a b c d : ℕ) : a + b + (c + d) = a + c + d + b := by
   Hint "Start with `repeat rw [add_assoc]` to push all the brackets to the right."
   repeat rw [add_assoc]
-  Hint "Now use targetted `rw [add_left_comm b c]` to switch `b` and `c` on the left
+  Hint "Now use `rw [add_left_comm b c]` to switch `b` and `c` on the left
   hand side."
   rw [add_left_comm b c]
-  Hint "Finally use `add_comm` to switch `b` and `d`"
+  Hint "Finally use a targetted `add_comm` to switch `b` and `d`"
+  Hint (hidden := true) "`rw [add_comm b d]`."
   rw [add_comm b d]
   rfl
 

Game/Levels/Algorithm/L04pred.lean

@@ -29,11 +29,13 @@ says that `pred (succ n) = n`. Let's use it to prove `succ_inj`, the theorem whi
 Peano assumed as an axiom and which we have already used extensively without justification.
 "
 
-LemmaDoc pred_succ as "pred_succ" in "Peano"
+LemmaDoc MyNat.pred_succ as "pred_succ" in "Peano"
 "
 `pred_succ n` is a proof of `pred (succ n) = n`.
 "
 
+NewLemma MyNat.pred_succ
+
 /-- If $\operatorname{succ}(a)=\operatorname{succ}(b)$ then $a=b$. -/
 Statement (a b : ℕ) (h : succ a = succ b) : a = b := by
   Hint "Start with `rw [← pred_succ a]` and take it from there."

Game/Levels/Algorithm/L05is_zero.lean

@@ -40,15 +40,7 @@ LemmaDoc MyNat.succ_ne_zero as "succ_ne_zero" in "Peano"
 `succ_ne_zero a` is a proof of `succ a ≠ 0`.
 "
 
-TacticDoc tauto "
-# Summary
-
-The `tauto` tactic proves pure logic goals, which can be resolved by truth tables.
-
-## Example
-
-If the goal is `True` then `tauto` will solve it.
-"
+NewLemma MyNat.is_zero_zero MyNat.is_zero_succ
 
 /-- If $\operatorname{succ}(a)=\operatorname{succ}(b)$ then $a=b$. -/
 Statement succ_ne_zero (a : ℕ) : succ a ≠ 0 := by

Game/Levels/Algorithm/L06succ_ne_succ.lean

@@ -60,6 +60,8 @@ then you will get a new goal `a = 0` to prove, and after you've proved
 it you will have a new hypothesis `h : a = 0` in your original goal.
 "
 
+NewTactic «have»
+
 LemmaDoc MyNat.succ_ne_succ as "succ_ne_succ" in "Peano" "
 `succ_ne_succ m n` is the proof that `m ≠ n → succ m ≠ succ n`.
 "

Game/Levels/Algorithm/L07decide.lean

@@ -9,13 +9,28 @@ LemmaTab "Peano"
 
 namespace MyNat
 
+TacticDoc decide "
+# Summary
+
+`decide` will attempt to solve a goal if it can find an algorithm which it
+can run to solve it.
+
+## Example
+
+A term of type `DecidableEq ℕ` is an algorithm to decide whether two naturals
+are equal or difference. Hence, once this term is made and made into an `instance`,
+the `decide` tactic can use it to solve goals of the form `a = b` or `a ≠ b`.
+"
+
+NewTactic decide
+
 Introduction
 "
 Implementing the algorithm for equality of naturals, and the proof that it is correct,
 looks like this:
 
 ```
-instance instDecidableEq : DecidableEq MyNat
+instance instDecidableEq : DecidableEq ℕ
 | 0, 0 => isTrue <| by
   show 0 = 0
   rfl
@@ -43,3 +58,5 @@ between two naturals. Run it with the `decide` tactic.
 /-- $20+20=40$. -/
 Statement : (20 : ℕ) + 20 = 40 := by
   decide
+
+-- need tacticdoc