add simp_add tactic

Game/Levels/Algorithm/L03add_algo2.lean

@@ -39,9 +39,5 @@ Statement (a b c d e f g h : ℕ) :
 
 Conclusion
 "
-You can even make your own tactics. For example the Lean code
-```
-macro_rules | `(tactic| simp_add) => `(tactic| simp only [add_assoc, add_left_comm, add_comm])
-```
-will create a new tactic `simp_add` which solves this level and any others of this form.
+Let's now make our own tactic to do this.
 "

Game/Levels/Algorithm/L04add_algo3.lean

@@ -0,0 +1,48 @@
+import Game.Levels.Algorithm.L03add_algo2
+
+World "Algorithm"
+Level 4
+Title "the simplest approach"
+
+LemmaTab "+"
+
+namespace MyNat
+
+macro "simp_add" : tactic => `(tactic|(
+  simp only [add_assoc, add_left_comm, add_comm]))
+
+TacticDoc simp_add "
+# Overview
+
+Our home-made tactic `simp_add` will solve arbitrary goals of
+the form `a + (b + c) + (d + e) = e + (d + (c + b)) + a`.
+"
+
+NewTactic simp_add
+
+Introduction
+"
+You can even make your own tactics in Lean.
+This code here
+```
+macro \"simp_add\" : tactic => `(tactic|(
+  simp only [add_assoc, add_left_comm, add_comm]))
+```
+creates a new tactic `simp_add`, which runs
+`simp only [add_assoc, add_left_comm, add_comm]`.
+Try it!
+"
+
+
+
+/-- If $a, b,\ldots h$ are arbitrary natural numbers, we have
+$(d + f) + (h + (a + c)) + (g + e + b) = a + b + c + d + e + f + g + h$. -/
+Statement (a b c d e f g h : ℕ) :
+    (d + f) + (h + (a + c)) + (g + e + b) = a + b + c + d + e + f + g + h := by
+  simp_add
+
+Conclusion
+"
+Let's now move on to a more efficient approach to questions
+involving numerals, such as `20 + 20 = 40`.
+"

Game/Levels/Algorithm/L05pred.lean

@@ -1,4 +1,4 @@
-import Game.Levels.Algorithm.L03add_algo2
+import Game.Levels.Algorithm.L04add_algo3
 import Game.Levels.Implication
 
 World "Algorithm"

Game/Levels/Algorithm/L06is_zero.lean

@@ -1,7 +1,7 @@
-import Game.Levels.Algorithm.L04pred
+import Game.Levels.Algorithm.L05pred
 
 World "Algorithm"
-Level 5
+Level 6
 Title "is_zero"
 
 LemmaTab "Peano"

Game/Levels/Algorithm/L07succ_ne_succ.lean

@@ -1,7 +1,7 @@
-import Game.Levels.Algorithm.L05is_zero
+import Game.Levels.Algorithm.L06is_zero
 
 World "Algorithm"
-Level 6
+Level 7
 Title "An algorithm for equality"
 
 LemmaTab "Peano"

Game/Levels/Algorithm/L08decide.lean

@@ -1,8 +1,8 @@
-import Game.Levels.Algorithm.L06succ_ne_succ
+import Game.Levels.Algorithm.L07succ_ne_succ
 import Game.MyNat.DecidableEq
 
 World "Algorithm"
-Level 7
+Level 8
 Title "decide"
 
 LemmaTab "Peano"

Game/Levels/Algorithm/L09decide2.lean

@@ -1,7 +1,7 @@
-import Game.Levels.Algorithm.L07decide
+import Game.Levels.Algorithm.L08decide
 
 World "Algorithm"
-Level 8
+Level 9
 Title "decide again"
 
 LemmaTab "Peano"