Merge branch 'AdvMultiplication' of github.com:leanprover-community/N…

…NG4 into AdvMultiplication

.devcontainer/Dockerfile

@@ -4,7 +4,7 @@ WORKDIR /
 
 ENV ELAN_HOME=/usr/local/elan \
   PATH=/usr/local/elan/bin:$PATH \
-  LEAN_VERSION=leanprover/lean4:v4.0.0-rc4
+  LEAN_VERSION=leanprover/lean4:v4.1.0
   # TODO: read toolchain from `lean-toolchain`
 
 SHELL ["/bin/bash", "-euxo", "pipefail", "-c"]

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/Addition/L01zero_add.lean

@@ -30,7 +30,7 @@ will ask us to show that if `0 + d = d` then `0 + succ d = succ d`. Because
 See if you can do your first induction proof in Lean.
 "
 
-LemmaDoc MyNat.zero_add as "zero_add" in "Add" "
+LemmaDoc MyNat.zero_add as "zero_add" in "+" "
 `zero_add x` is the proof of `0 + x = x`.
 
 `zero_add` is a `simp` lemma, because replacing `0 + x` by `x`
@@ -86,7 +86,7 @@ goal before you can access the second one.
 "
 NewTactic induction
 
-LemmaTab "Add"
+LemmaTab "+"
 
 Conclusion
 "

Game/Levels/Addition/L02succ_add.lean

@@ -16,7 +16,7 @@ we have the problem that we are adding `b` to things, so we need
 to use induction to split into the cases where `b = 0` and `b` is a successor.
 "
 
-LemmaDoc MyNat.succ_add as "succ_add" in "Add"
+LemmaDoc MyNat.succ_add as "succ_add" in "+"
 "`succ_add a b` is a proof that `succ a + b = succ (a + b)`."
 
 /--
@@ -40,7 +40,7 @@ Statement succ_add (a b : ℕ) : succ a + b = succ (a + b)  := by
     rw [add_succ, add_succ, hd]
     rfl
 
-LemmaTab "Add"
+LemmaTab "+"
 
 Conclusion "
 Well done! You now have enough tools to tackle the main boss of this level.

Game/Levels/Addition/L03add_comm.lean

@@ -15,7 +15,7 @@ Look in your inventory to see the proofs you have available.
 These should be enough.
 "
 
-LemmaDoc MyNat.add_comm as "add_comm" in "Add"
+LemmaDoc MyNat.add_comm as "add_comm" in "+"
 "`add_comm x y` is a proof of `x + y = y + x`."
 
 /-- On the set of natural numbers, addition is commutative.
@@ -32,4 +32,4 @@ Statement add_comm (a b : ℕ) : a + b = b + a := by
 -- Adding this instance to make `ac_rfl` work.
 instance : Lean.IsCommutative (α := ℕ) (· + ·) := ⟨add_comm⟩
 
-LemmaTab "Add"
+LemmaTab "+"

Game/Levels/Addition/L04add_assoc.lean

@@ -19,7 +19,7 @@ Introduction
   That's true, but we didn't prove it yet. Let's prove it now by induction.
 "
 
-LemmaDoc MyNat.add_assoc as "add_assoc" in "Add" "`add_assoc a b c` is a proof
+LemmaDoc MyNat.add_assoc as "add_assoc" in "+" "`add_assoc a b c` is a proof
 that `(a + b) + c = a + (b + c)`. Note that in Lean `(a + b) + c` prints
 as `a + b + c`, because the notation for addition is defined to be left
 associative. "
@@ -42,7 +42,7 @@ Statement add_assoc (a b c : ℕ) : a + b + c = a + (b + c) := by
 -- Adding this instance to make `ac_rfl` work.
 instance : Lean.IsAssociative (α := ℕ) (· + ·) := ⟨add_assoc⟩
 
-LemmaTab "Add"
+LemmaTab "+"
 
 Conclusion
 "

Game/Levels/Addition/L05add_right_comm.lean

@@ -23,7 +23,7 @@ will only do rewrites of the form `b + ? = ? + b`, and `rw [add_comm b c]`
 will only do rewrites of the form `b + c = c + b`.
 "
 
-LemmaDoc MyNat.add_right_comm as "add_right_comm" in "Add"
+LemmaDoc MyNat.add_right_comm as "add_right_comm" in "+"
 "`add_right_comm a b c` is a proof that `(a + b) + c = (a + c) + b`.
 
 In Lean, `a + b + c` means `(a + b) + c`, so this result gets displayed
@@ -36,7 +36,7 @@ Statement add_right_comm (a b c : ℕ) : a + b + c = a + c + b := by
   rw [add_comm b, add_assoc]
   rfl
 
-LemmaTab "Add"
+LemmaTab "+"
 
 Conclusion "
 You've now seen all the tactics you need to beat the final boss of the game.

Game/Levels/AdvAddition/L02add_right_cancel.lean

@@ -6,9 +6,9 @@ Title "add_right_cancel"
 
 namespace MyNat
 
-LemmaTab "Add"
+LemmaTab "+"
 
-LemmaDoc MyNat.add_right_cancel as "add_right_cancel" in "Add" "
+LemmaDoc MyNat.add_right_cancel as "add_right_cancel" in "+" "
 
 `add_right_cancel a b n` is the theorem that $a+n=b+n \\implies a=b.$
 "

Game/Levels/AdvAddition/L03add_left_cancel.lean

@@ -6,9 +6,9 @@ Title "add_left_cancel"
 
 namespace MyNat
 
-LemmaTab "Add"
+LemmaTab "+"
 
-LemmaDoc MyNat.add_left_cancel as "add_left_cancel" in "Add" "
+LemmaDoc MyNat.add_left_cancel as "add_left_cancel" in "+" "
 
 `add_left_cancel a b n` is the theorem that $n+a=n+b \\implies a=b.$
 "
@@ -18,7 +18,7 @@ Introduction
 You can prove it by induction on `n` or you can deduce it from `add_right_cancel`.
 "
 
-/-- $a+n=b+n\implies a=b$. -/
+/-- $n+a=n+b\implies a=b$. -/
 Statement add_left_cancel (a b n : ℕ) : n + a = n + b → a = b := by
   repeat rw [add_comm n]
   intro h

Game/Levels/AdvAddition/L04add_left_eq_self.lean

@@ -6,9 +6,9 @@ Title "add_left_eq_self"
 
 namespace MyNat
 
-LemmaTab "Add"
+LemmaTab "+"
 
-LemmaDoc MyNat.add_left_eq_self as "add_left_eq_self" in "Add" "
+LemmaDoc MyNat.add_left_eq_self as "add_left_eq_self" in "+" "
 
 `add_left_eq_self x y` is the theorem that $x + y = y\\implies x=0.$
 "

Game/Levels/AdvAddition/L05add_right_eq_self.lean

@@ -4,11 +4,11 @@ World "AdvAddition"
 Level 5
 Title "add_right_eq_self"
 
-LemmaTab "Add"
+LemmaTab "+"
 
 namespace MyNat
 
-LemmaDoc MyNat.add_right_eq_self as "add_right_eq_self" in "Add" "
+LemmaDoc MyNat.add_right_eq_self as "add_right_eq_self" in "+" "
 
 `add_right_eq_self x y` is the theorem that $x + y = x\\implies y=0.$
 "

Game/Levels/AdvAddition/L06eq_zero_of_add_right_eq_zero.lean

@@ -16,17 +16,42 @@ world by proving one of these in this level, and the other in the next.
 ## Two new tactics
 
 If you have a hypothesis `h : False` then you are done, because a false statement implies
-any statement. You can use the `contradiction` tactic to finish your proof.
+any statement. You can use the `tauto` tactic to finish your proof.
 
 Sometimes you just want to deal with the two cases `b = 0` and `b = succ d` separately,
 and don't need the inductive hypothesis `hd` that comes with `induction b with d hd`.
 In this situation you can use `cases b with d` instead.
 
 "
 
-TacticDoc contradiction "
-The `contradiction` tactic will solve any goal, if you have a hypothesis `h : False`.
+TacticDoc tauto "
+# Summary
+
+The `tauto` tactic will solve any goal which can be solved purely by logic (that is, by
+truth tables).
+
+## Example
+
+If you have `False` as a hypothesis, then `tauto` will solve
+the goal. This is because a false hypothesis implies any hypothesis.
+
+## Example
+
+If your goal is `True`, then `tauto` will solve the goal.
+
+## Example
+
+If you have two hypotheses `h1 : a = 37` and `h2 : a ≠ 37` then `tauto` will
+solve the goal because it can prove `False` from your hypotheses, and thus
+prove the goal (as `False` implies anything).
+
+## Example
+
+If you have a hypothesis of the form `a = 0 → a * b = 0` and your goal is `a * b ≠ 0 → a ≠ 0`, then
+`tauto` will solve the goal, because the goal is logically equivalent to the hypothesis.
+If you switch the goal and hypothesis in this example, `tauto` would solve it too.
 "
+
 TacticDoc cases "
 ## Summary
 
@@ -55,9 +80,9 @@ If `h : P ∨ Q` is a hypothesis, then `cases h with hp hq` will turn one goal
 into two goals, one with a hypothesis `hp : P` and the other with a
 hypothesis `hq : Q`.
 "
-NewTactic contradiction cases
+NewTactic tauto cases
 
-LemmaDoc MyNat.eq_zero_of_add_right_eq_zero as "eq_zero_of_add_right_eq_zero" in "Add" "
+LemmaDoc MyNat.eq_zero_of_add_right_eq_zero as "eq_zero_of_add_right_eq_zero" in "+" "
   A proof that $a+b=0 \\implies a=0$.
 "
 
@@ -76,6 +101,6 @@ Statement eq_zero_of_add_right_eq_zero (a b : ℕ) : a + b = 0 → a = 0 := by
   rw [add_succ] at h
   symm at h
   apply zero_ne_succ at h
-  contradiction
+  tauto
 
 Conclusion "Well done!"

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 "Add"
+LemmaTab "+"
 
 namespace MyNat
 
@@ -13,7 +13,7 @@ Introduction
 of using it.
 "
 
-LemmaDoc MyNat.eq_zero_of_add_left_eq_zero as "eq_zero_of_add_left_eq_zero" in "Add" "
+LemmaDoc MyNat.eq_zero_of_add_left_eq_zero as "eq_zero_of_add_left_eq_zero" in "+" "
   A proof that $a+b=0 \\implies b=0$.
 "
 

Game/Levels/AdvMultiplication/all_levels.lean

@@ -3,10 +3,9 @@ import Game.Levels.LessOrEqual
 
 namespace MyNat
 
--- should we be using `succ` any more????
 lemma eq_succ_of_ne_zero (a : ℕ) (ha : a ≠ 0) : ∃ n, a = succ n := by
   cases a with d
-  contradiction
+  tauto
   use d
   -- WTF????? **TODO** `use` shouldn't try `rfl`
 
@@ -25,19 +24,18 @@ lemma mul_eq_zero (a b : ℕ) (h : a * b = 0) : a = 0 ∨ b = 0 := by
   tauto
 
 lemma mul_right_ne_zero (a b : ℕ) (h : a * b ≠ 0) : a ≠ 0 := by
-  intro h1
-  apply h
-  rw [h1]
-  rw [zero_mul]
-  rfl
+  by_contra ha
+  rw [ha] at h
+  rw [zero_mul] at h
+  tauto
 
 lemma mul_left_ne_zero (a b : ℕ) (h : a * b ≠ 0) : b ≠ 0 := by
   rw [mul_comm] at h
   exact mul_right_ne_zero b a h
 
 lemma one_le_of_zero_ne (a : ℕ) (ha : a ≠ 0) : 1 ≤ a := by
   cases a with n
-  · contradiction
+  · tauto
   · use n
     rw [succ_eq_add_one]
     rw [add_comm]
@@ -50,7 +48,6 @@ lemma mul_le_mul_right (a b t : ℕ) (h : a ≤ b) : a * t ≤ b * t := by
   rfl
 
 lemma le_mul_right (a b : ℕ) (h : a * b ≠ 0) : a ≤ a * b := by
-  -- do I need `have`?
   apply mul_left_ne_zero at h
   apply one_le_of_zero_ne at h
   apply mul_le_mul_right 1 b a at h
@@ -70,8 +67,9 @@ lemma le_one (a : ℕ) (ha : a ≤ 1) : a = 0 ∨ a = 1 := by
       rw [one_eq_succ_zero] at hx
       apply succ_inj at hx
       apply zero_ne_succ at hx
-      contradiction
+      tauto
 
+-- Archie needs this
 example (c d : ℕ) (h : c * d = 1) : c = 1 := by
   have foo : c ≤ 1 := by
     rw [← h]
@@ -83,26 +81,29 @@ example (c d : ℕ) (h : c * d = 1) : c = 1 := by
   cases foo with h0 h1
   · rw [h0, zero_mul] at h
     apply zero_ne_succ at h
-    contradiction
+    tauto
   exact h1
 
 lemma mul_left_cancel (a b c : ℕ) (ha : a ≠ 0) (h : a * b = a * c) : b = c := by
   induction b with d hd generalizing c -- this is what trips everyone up
   · rw [mul_zero] at h
     symm at h
-    sorry -- this is NNG3 adv mult levels 1 to 3
+    apply mul_eq_zero at h
+    cases h with h1 h2
+    · tauto
+    · rw [h2]
+      rfl
   · cases c with c
     · rw [mul_succ, mul_zero] at h
       apply eq_zero_of_add_left_eq_zero at h
-      contradiction
+      tauto
     · rw [mul_succ, mul_succ] at h
       apply add_right_cancel at h
-      have foo : d = c := by
-        apply hd
-        exact h
-      rw [foo]
+      rw [hd c]
       rfl
+      exact h
 
+-- Archie needs this
 example (a b : ℕ) (h : b = a * b) (hb : b ≠ 0) : a = 1 := by
   rw [mul_comm] at h
   nth_rewrite 1 [← mul_one b] at h

Game/Levels/Algorithm.lean

@@ -0,0 +1,20 @@
+import Game.Levels.Algorithm.L01add_left_comm
+import Game.Levels.Algorithm.L02add_algo1
+import Game.Levels.Algorithm.L03add_algo2
+import Game.Levels.Algorithm.L04add_algo3
+import Game.Levels.Algorithm.L05pred
+import Game.Levels.Algorithm.L06is_zero
+import Game.Levels.Algorithm.L07succ_ne_succ
+import Game.Levels.Algorithm.L08decide
+import Game.Levels.Algorithm.L09decide2
+
+World "Algorithm"
+Title "Algorithm World"
+
+Introduction
+"
+Proofs like $2+2=4$ and $a+b+c+d+e=e+d+c+b+a$ are very tedious to do by hand.
+In Algorithm World we learn how to get the computer to do them for us.
+
+Click on \"Start\" to proceed.
+"