From 81a66b0913405fb3a14d3386e58b9171fb1b9d4f Mon Sep 17 00:00:00 2001
From: Kevin Buzzard <k.buzzard@imperial.ac.uk>
Date: Fri, 27 Oct 2023 19:40:15 +0100
Subject: [PATCH] add `simp_add` tactic

---
 Game/Levels/Algorithm/L03add_algo2.lean       |  6 +--
 Game/Levels/Algorithm/L04add_algo3.lean       | 48 +++++++++++++++++++
 .../Algorithm/{L04pred.lean => L05pred.lean}  |  2 +-
 .../{L05is_zero.lean => L06is_zero.lean}      |  4 +-
 ...succ_ne_succ.lean => L07succ_ne_succ.lean} |  4 +-
 .../{L07decide.lean => L08decide.lean}        |  4 +-
 .../{L08decide2.lean => L09decide2.lean}      |  4 +-
 7 files changed, 58 insertions(+), 14 deletions(-)
 create mode 100644 Game/Levels/Algorithm/L04add_algo3.lean
 rename Game/Levels/Algorithm/{L04pred.lean => L05pred.lean} (96%)
 rename Game/Levels/Algorithm/{L05is_zero.lean => L06is_zero.lean} (96%)
 rename Game/Levels/Algorithm/{L06succ_ne_succ.lean => L07succ_ne_succ.lean} (98%)
 rename Game/Levels/Algorithm/{L07decide.lean => L08decide.lean} (96%)
 rename Game/Levels/Algorithm/{L08decide2.lean => L09decide2.lean} (88%)

diff --git a/Game/Levels/Algorithm/L03add_algo2.lean b/Game/Levels/Algorithm/L03add_algo2.lean
index f832b31..a2b4837 100644
--- a/Game/Levels/Algorithm/L03add_algo2.lean
+++ b/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.
 "
diff --git a/Game/Levels/Algorithm/L04add_algo3.lean b/Game/Levels/Algorithm/L04add_algo3.lean
new file mode 100644
index 0000000..2a8e254
--- /dev/null
+++ b/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`.
+"
diff --git a/Game/Levels/Algorithm/L04pred.lean b/Game/Levels/Algorithm/L05pred.lean
similarity index 96%
rename from Game/Levels/Algorithm/L04pred.lean
rename to Game/Levels/Algorithm/L05pred.lean
index aab14f8..bd90577 100644
--- a/Game/Levels/Algorithm/L04pred.lean
+++ b/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"
diff --git a/Game/Levels/Algorithm/L05is_zero.lean b/Game/Levels/Algorithm/L06is_zero.lean
similarity index 96%
rename from Game/Levels/Algorithm/L05is_zero.lean
rename to Game/Levels/Algorithm/L06is_zero.lean
index 6676753..e27d5d7 100644
--- a/Game/Levels/Algorithm/L05is_zero.lean
+++ b/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"
diff --git a/Game/Levels/Algorithm/L06succ_ne_succ.lean b/Game/Levels/Algorithm/L07succ_ne_succ.lean
similarity index 98%
rename from Game/Levels/Algorithm/L06succ_ne_succ.lean
rename to Game/Levels/Algorithm/L07succ_ne_succ.lean
index a180a13..0439a30 100644
--- a/Game/Levels/Algorithm/L06succ_ne_succ.lean
+++ b/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"
diff --git a/Game/Levels/Algorithm/L07decide.lean b/Game/Levels/Algorithm/L08decide.lean
similarity index 96%
rename from Game/Levels/Algorithm/L07decide.lean
rename to Game/Levels/Algorithm/L08decide.lean
index fa0eb12..7f55f66 100644
--- a/Game/Levels/Algorithm/L07decide.lean
+++ b/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"
diff --git a/Game/Levels/Algorithm/L08decide2.lean b/Game/Levels/Algorithm/L09decide2.lean
similarity index 88%
rename from Game/Levels/Algorithm/L08decide2.lean
rename to Game/Levels/Algorithm/L09decide2.lean
index 002bafd..6116eda 100644
--- a/Game/Levels/Algorithm/L08decide2.lean
+++ b/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"