move all WIP files to level-rewrite branch

Game/Levels/Map.txt

@@ -0,0 +1,105 @@
+## Algorithm world
+
+Optional. Learn about automating proofs with `simp` and/or `ac_rfl`.
+
+Note : `add_add_add_comm` is needed for isEven_add_isEven
+and also in power world with pow_add I think it was,
+and also if you choose a lousy variable
+to induct on in one of mul_add/add_mul (the
+one you don't prove via comm)
+
+Where does a reduction tactic which turns all numerals
+into succ succ succ 0 live? Here or functional program world?
+
+**TODO** Aesop levels. Tutorial about how to get aesop proving...something.
+
+## Functional program world
+
+After advanced addition world (because here they learn `apply`).
+Prove succ_ne_zero and succ_inj, and make decidable equality.
+Give proof that 20+20!=41 (note that 2+2!=5 )
+**TODO** find Testa post explaining how to do this.
+
+## Inequality world:
+
+a) 0 ≤ x;
+b) x ≤ x;
+c) x ≤ S(x);
+d) If x ≤ 0 then x = 0.
+a) x ≤ x (reflexivity);
+b) If x ≤ y and y ≤ z then x ≤ z (transitivity);
+c) If x ≤ y and y ≤ x then x = y (antisymmetry);
+d) Either x ≤ y or y ≤ x (totality).
+
+What about succ m ≤ succ n ↔ m ≤ n? This was a lost level (but not about <)
+
+If a ≤ b then a + x ≤ b + x. And iff version?
+
+## Advanced Multiplication world: you can cancel muliplication
+by nonzero x. ad+bc=ac+bd -> a=b or c=d? This should be preparation
+for divisilibity world.
+
+## Divisibility world
+
+a | b and b | c -> a | c
+a | x and a | y -> a | x + y
+a | x -> a | x * y
+
+etc
+
+## Prime world
+
+2 is prime and that's it
+
+## Hard world
+
+twin prime, Goldbach, weak Goldbach, 3n+1.
+
+## Even/Odd world
+
+even + odd = odd etc
+everything is odd or even
+nothing is odd and even
+
+## `<` world
+
+Advanced inequality world should be `<` and strong induction. Nick from Lean 3 version.
+Define a < b to be S(a)<=b
+
+and given NNG3 levels 15 and 16 it should now just
+be a few lines to prove `a < b ↔ `a ≤ b ∧ ¬ (b ≤ a)`,
+
+lemma lt_irrefl (a : mynat) : ¬ (a < a) :=
+lemma ne_of_lt (a b : mynat) : a < b → a ≠ b :=
+-- theorem ne_zero_of_pos (a : mynat) : 0 < a → a ≠ 0 :=
+theorem not_lt_zero (a : mynat) : ¬(a < 0) :=
+theorem lt_of_lt_of_le (a b c : mynat) : a < b → b ≤ c → a < c :=
+theorem lt_of_le_of_lt (a b c : mynat) : a ≤ b → b < c → a < c :=
+theorem lt_trans (a b c : mynat) : a < b → b < c → a < c :=
+theorem lt_iff_le_and_ne (a b : mynat) : a < b ↔ a ≤ b ∧ a ≠ b :=
+theorem lt_succ_self (n : mynat) : n < succ n :=
+lemma succ_le_succ_iff (m n : mynat) : succ m ≤ succ n ↔ m ≤ n :=
+lemma lt_succ_iff_le (m n : mynat) : m < succ n ↔ m ≤ n :=
+lemma le_of_add_le_add_left (a b c : mynat) : a + b ≤ a + c → b ≤ c :=
+lemma lt_of_add_lt_add_left (a b c : mynat) : a + b < a + c → b < c :=
+-- I SHOULD TEACH CONGR
+lemma add_lt_add_right (a b : mynat) : a < b → ∀ c : mynat, a + c < b + c :=
+instance : ordered_comm_monoid mynat :=
+instance : ordered_cancel_comm_monoid mynat :=
+def succ_lt_succ_iff (a b : mynat) : succ a < succ b ↔ a < b :=
+-- multiplication
+theorem mul_le_mul_of_nonneg_left (a b c : mynat) : a ≤ b → 0 ≤ c → c * a ≤ c * b :=
+theorem mul_le_mul_of_nonneg_right (a b c : mynat) : a ≤ b → 0 ≤ c → a * c ≤ b * c :=
+theorem mul_lt_mul_of_pos_left (a b c : mynat) : a < b → 0 < c → c * a < c * b :=
+theorem mul_lt_mul_of_pos_right (a b c : mynat) : a < b → 0 < c → a * c < b * c :=
+instance : ordered_semiring mynat :=
+lemma le_mul (a b c d : mynat) : a ≤ b → c ≤ d → a * c ≤ b * d :=
+lemma pow_le (m n a : mynat) : m ≤ n → m ^ a ≤ n ^ a :=
+lemma strong_induction_aux (P : mynat → Prop)
+  (IH : ∀ m : mynat, (∀ b : mynat, b < m → P b) → P m)
+  (n : mynat) : ∀ c < n, P c :=
+-- is elab_as_eliminator right?
+@[elab_as_eliminator]
+theorem strong_induction (P : mynat → Prop)
+  (IH : ∀ m : mynat, (∀ d : mynat, d < m → P d) → P m) :
+  ∀ n, P n :=

Game/Levels/OldAdvMultiplication.lean

@@ -0,0 +1,13 @@
+import Game.Levels.Multiplication
+import Game.Levels.AdvAddition
+
+World "AdvMultiplication"
+Title "Advanced Multiplication World"
+
+Introduction
+"
+Welcome to Advanced Multiplication World! Before attempting this
+world you should have completed seven other worlds, including
+Multiplication World and Advanced Addition World. There are four
+levels in this world.
+"

Game/Levels/OldAdvMultiplication/Level_1.lean

@@ -0,0 +1,51 @@
+import Game.Levels.Multiplication
+import Game.Levels.AdvAddition
+
+
+World "AdvMultiplication"
+Level 1
+Title "mul_pos"
+
+open MyNat
+
+Introduction
+"
+## Tricks
+
+1) if your goal is `X ≠ Y` then `intro h` will give you `h : X = Y` and
+a goal of `False`. This is because `X ≠ Y` *means* `(X = Y) → False`.
+Conversely if your goal is `False` and you have `h : X ≠ Y` as a hypothesis
+then `apply h` will turn the goal into `X = Y`.
+
+2) if `hab : succ (3 * x + 2 * y + 1) = 0` is a hypothesis and your goal is `False`,
+then `exact succ_ne_zero _ hab` will solve the goal, because Lean will figure
+out that `_` is supposed to be `3 * x + 2 * y + 1`.
+
+"
+-- TODO: cases
+-- Recall that if `b : ℕ` is a hypothesis and you do `cases b with n`,
+-- your one goal will split into two goals,
+-- namely the cases `b = 0` and `b = succ n`. So `cases` here is like
+-- a weaker version of induction (you don't get the inductive hypothesis).
+
+
+/-- The product of two non-zero natural numbers is non-zero. -/
+Statement
+    (a b : ℕ) : a ≠ 0 → b ≠ 0 → a * b ≠ 0 := by
+  intro ha hb
+  intro hab
+  induction b with b
+  apply hb
+  rfl
+  rw [mul_succ] at hab
+  apply ha
+  induction a with a
+  rfl
+  rw [add_succ] at hab
+  exfalso
+  exact succ_ne_zero _ hab
+
+Conclusion
+"
+
+"

Game/Levels/OldAdvMultiplication/Level_2.lean

@@ -0,0 +1,39 @@
+import Game.Levels.AdvMultiplication.Level_1
+
+
+World "AdvMultiplication"
+Level 2
+Title "eq_zero_or_eq_zero_of_mul_eq_zero"
+
+open MyNat
+
+Introduction
+"
+A variant on the previous level.
+"
+
+/-- If $ab = 0$, then at least one of $a$ or $b$ is equal to zero. -/
+Statement MyNat.eq_zero_or_eq_zero_of_mul_eq_zero
+    (a b : ℕ) (h : a * b = 0) :
+  a = 0 ∨ b = 0 := by
+  induction a with d hd
+  · Branch
+      simp
+    left
+    rfl
+  · induction b with e he
+    · Branch
+        simp
+      right
+      rfl
+    · exfalso
+      rw [mul_succ] at h
+      rw [add_succ] at h
+      exact succ_ne_zero _ h
+
+-- TODO: `induction` or `rcases`? Implement the latter.
+
+Conclusion
+"
+
+"

Game/Levels/OldAdvMultiplication/Level_3.lean

@@ -0,0 +1,36 @@
+import Game.Levels.AdvMultiplication.Level_2
+
+
+
+World "AdvMultiplication"
+Level 3
+Title "mul_eq_zero_iff"
+
+open MyNat
+
+Introduction
+"
+Now you have `eq_zero_or_eq_zero_of_mul_eq_zero` this is pretty straightforward.
+"
+
+/-- $ab = 0$, if and only if at least one of $a$ or $b$ is equal to zero.
+ -/
+Statement
+    {a b : ℕ} : a * b = 0 ↔ a = 0 ∨ b = 0 := by
+  constructor
+  intro h
+  exact eq_zero_or_eq_zero_of_mul_eq_zero a b h
+  intro hab
+  rcases hab with hab | hab
+  rw [hab]
+  rw [MyNat.zero_mul]
+  rfl
+  rw [hab]
+  rw [MyNat.mul_zero]
+  rfl
+
+
+Conclusion
+"
+
+"

Game/Levels/OldAdvMultiplication/Level_4.lean

@@ -0,0 +1,97 @@
+import Game.Levels.AdvMultiplication.Level_3
+
+
+World "AdvMultiplication"
+Level 4
+Title "mul_left_cancel"
+
+open MyNat
+
+Introduction
+"
+This is the last of the bonus multiplication levels.
+`mul_left_cancel` will be useful in inequality world.
+
+People find this level hard. I have probably had more questions about this
+level than all the other levels put together, in fact. Many levels in this
+game can just be solved by \"running at it\" -- do induction on one of the
+variables, keep your head, and you're done. In fact, if you like a challenge,
+it might be instructive if you stop reading after the end of this paragraph
+and try solving this level now by induction,
+seeing the trouble you run into, and reading the rest of these comments afterwards.
+This level
+has a sting in the tail. If you are a competent mathematician, try
+and figure out what is going on. Write down a maths proof of the
+theorem in this level. Exactly what statement do you want to prove
+by induction? It is subtle.
+
+Ok so here are some spoilers. The problem with naively running at it,
+is that if you try induction on,
+say, $c$, then you are imagining a and b as fixed, and your inductive
+hypothesis $P(c)$ is $ab=ac \\implies b=c$. So for your inductive step
+you will be able to assume $ab=ad \\implies b=d$ and your goal will
+be to show $ab=a(d+1) \\implies b=d+1$. When you also assume $ab=a(d+1)$
+you will realise that your inductive hypothesis is *useless*, because
+$ab=ad$ is not true! The statement $P(c)$ (with $a$ and $b$ regarded
+as constants) is not provable by induction.
+
+What you *can* prove by induction is the following *stronger* statement.
+Imagine $a\\ne 0$ as fixed, and then prove \"for all $b$, if $ab=ac$ then $b=c$\"
+by induction on $c$. This gives us the extra flexibility we require.
+Note that we are quantifying over all $b$ in the inductive hypothesis -- it
+is essential that $b$ is not fixed.
+
+You can do this in two ways in Lean -- before you start the induction
+you can write `revert b`. The `revert` tactic is the opposite of the `intro`
+tactic; it replaces the `b` in the hypotheses with \"for all $b$\" in the goal.
+
+[TODO: The second way does not work yet in this game]
+
+If you do not modify your technique in this way, then this level seems
+to be impossible (judging by the comments I've had about it!)
+"
+-- Alternatively, you can write `induction c with d hd
+-- generalizing b` as the first line of the proof.
+
+
+/-- If $a \\neq 0$, $b$ and $c$ are natural numbers such that
+$ ab = ac, $
+then $b = c$. -/
+Statement MyNat.mul_left_cancel
+    (a b c : ℕ) (ha : a ≠ 0) : a * b = a * c → b = c := by
+  Hint "NOTE: As is, this level is probably too hard and contains no hints yet.
+  Good luck!
+
+  Your first step should be `revert b`!"
+  revert b
+  induction c with c hc
+  · intro b hb
+    rw [mul_zero] at hb
+    rcases eq_zero_or_eq_zero_of_mul_eq_zero _ _ hb
+    exfalso
+    apply ha
+    exact h
+    exact h
+  · intro b h
+    induction b with b hb
+    exfalso
+    apply ha
+    rw [mul_zero] at h
+    rcases eq_zero_or_eq_zero_of_mul_eq_zero _ _ h.symm with h | h
+    exact h
+    exfalso
+    exact succ_ne_zero _ h
+    rw [mul_succ, mul_succ] at h
+    have j : b = c
+    apply hc
+    exact add_right_cancel _ _ _ h
+    rw [j]
+    rfl
+-- TODO: generalizing b.
+
+NewTactic revert
+
+Conclusion
+"
+
+"

Game/Levels/OldAdvMultiplication/mul_left_comm.lean

@@ -0,0 +1,75 @@
+import Game.Levels.Multiplication.Level_8
+
+
+World "Multiplication"
+Level 9
+Title "mul_left_comm"
+
+open MyNat
+
+Introduction
+"
+You are equipped with
+
+* `mul_assoc (a b c : ℕ) : (a * b) * c = a * (b * c)`
+* `mul_comm (a b : ℕ) : a * b = b * a`
+
+Re-read the docs for `rw` so you know all the tricks.
+You can see them in your inventory on the right.
+
+"
+
+-- TODO
+attribute [simp] MyNat.mul_zero
+attribute [simp] MyNat.mul_succ
+attribute [simp] MyNat.zero_mul
+attribute [simp] MyNat.succ_mul
+attribute [simp] MyNat.mul_one
+attribute [simp] MyNat.one_mul
+
+/-- For all natural numbers $a$ $b$ and $c$, we have $a(bc)=b(ac)$. -/
+Statement MyNat.mul_left_comm
+    (a b c : ℕ) : a * (b * c) = b * (a * c) := by
+  Branch
+    induction c
+    · simp
+    · simp
+      rw [mul_add, n_ih, mul_add, mul_comm a b]
+      rfl
+  rw [← mul_assoc]
+  rw [mul_comm a]
+  rw [mul_assoc]
+  rfl
+
+LemmaTab "Mul"
+
+-- TODO: make simp work:
+-- attribute [simp] mul_assoc mul_comm mul_left_comm
+
+Conclusion
+"
+Now we add a lot of the lemmas you proved to the `simp`, so it can do simplifications
+
+If you feel like attempting Advanced Multiplication world
+you'll have to do Function World and the Proposition Worlds first.
+These worlds assume a certain amount of mathematical maturity
+(perhaps 1st year undergraduate level).
+Your other possibility is Power World, with the \"final boss\".
+"
+
+-- -- TODO: Is it not bad habit that `simp` can prove these? If `simp`
+-- -- solves algebraic equations it's more by accident than by clever algorithm... that's `ring`.
+-- And now I whisper a magic incantation
+
+-- ```
+-- attribute [simp] mul_assoc mul_comm mul_left_comm
+-- ```
+
+-- and all of a sudden Lean can automatically do levels which are
+-- very boring for a human, for example
+
+-- ```
+-- example (a b c d e : ℕ) :
+--     (((a * b) * c) * d) * e = (c * ((b * e) * a)) * d := by
+--   simp
+-- ```

Game/Levels/OldAdvProposition/Level_1.lean

@@ -0,0 +1,41 @@
+import Game.Metadata
+import Game.MyNat.Addition
+
+
+World "AdvProposition"
+Level 1
+Title "the `split` tactic"
+
+open MyNat
+
+Introduction
+"
+The logical symbol `∧` means \"and\". If $P$ and $Q$ are propositions, then
+$P\\land Q$ is the proposition \"$P$ and $Q$\".
+"
+namespace MySet
+
+/-- If $P$ and $Q$ are true, then $P\\land Q$ is true. -/
+Statement
+    (P Q : Prop) (p : P) (q : Q) : P ∧ Q := by
+  Hint "If your *goal* is `P ∧ Q` then
+  you can make progress with the `constructor` tactic, which turns one goal `P ∧ Q`
+  into two goals, namely `P` and `Q`."
+  constructor
+  Hint "Now you have two goals. The first one is `P`, which you can proof now. The
+  second one is `Q` and you see it in the queue \"Other Goals\". You will have to prove it afterwards."
+  Hint (hidden := true) "This first goal can be proved with `exact p`."
+  exact p
+  -- Hint "Observe that now the first goal has been proved, so it disappears and you continue
+  -- proving the second goal."
+  -- Hint (hidden := true) "Like the first goal, this is a case for `exact`."
+  -- -- TODO: It looks like these hints get shown above as well, but weirdly the hints from
+  -- -- above to not get shown here.
+  exact q
+
+NewTactic constructor
+NewDefinition And
+
+Conclusion
+"
+"

Game/Levels/OldAdvProposition/Level_10.lean

@@ -0,0 +1,64 @@
+import Game.Metadata
+import Game.MyNat.Addition
+
+
+World "AdvProposition"
+Level 10
+Title "The law of the excluded middle."
+
+open MyNat
+
+Introduction
+"
+We proved earlier that `(P → Q) → (¬ Q → ¬ P)`. The converse,
+that `(¬ Q → ¬ P) → (P → Q)` is certainly true, but trying to prove
+it using what we've learnt so far is impossible (because it is not provable in
+constructive logic).
+
+"
+
+/-- If $P$ and $Q$ are true/false statements, then
+$$(\\lnot Q\\implies \\lnot P)\\implies(P\\implies Q).$$
+ -/
+Statement
+    (P Q : Prop) : (¬ Q → ¬ P) → (P → Q) := by
+  Hint "For example, you could start as always with
+
+  ```
+  intro h p
+  ```
+  "
+  intro h p
+  Hint "From here there is no way to continue with the tactics you've learned so far.
+
+  Instead you can call `by_cases q : Q`. This creates **two goals**, once under the assumption
+  that `Q` is true, once assuming `Q` is false."
+  by_cases q : Q
+  Hint "This first case is trivial."
+  exact q
+  Hint "The second case needs a bit more work, but you can get there with the tactics you've already
+  learned beforehand!"
+  have j := h q
+  exfalso
+  apply j
+  exact p
+
+NewTactic by_cases
+
+Conclusion
+"
+This approach assumed that `P ∨ ¬ P` is true, which is called \"law of excluded middle\".
+It cannot be proven using just tactics like `intro` or `apply`.
+`by_cases p : P` just does `rcases` on this result `P ∨ ¬ P`.
+
+
+OK that's enough logic -- now perhaps it's time to go on to Advanced Addition World!
+Get to it via the main menu.
+"
+
+-- TODO: I cannot really import `tauto` because of the notation `ℕ` that's used
+-- for `MyNat`.
+-- ## Pro tip
+
+-- In fact the tactic `tauto` just kills this goal (and many other logic goals) immediately. You'll be
+-- able to use it from now on.

Game/Levels/OldAdvProposition/Level_2.lean

@@ -0,0 +1,48 @@
+import Game.Metadata
+import Game.MyNat.Addition
+
+
+World "AdvProposition"
+Level 2
+Title "the `rcases` tactic"
+
+open MyNat
+
+Introduction
+"
+If `P ∧ Q` is in the goal, then we can make progress with `constructor`.
+But what if `P ∧ Q` is a hypothesis? In this case, the `rcases` tactic will enable
+us to extract proofs of `P` and `Q` from this hypothesis.
+"
+
+/-- If $P$ and $Q$ are true/false statements, then $P\\land Q\\implies Q\\land P$. -/
+Statement -- and_symm
+    (P Q : Prop) : P ∧ Q → Q ∧ P :=  by
+  Hint "The lemma below asks us to prove `P ∧ Q → Q ∧ P`, that is,
+  symmetry of the \"and\" relation. The obvious first move is
+
+  ```
+  intro h
+  ```
+
+  because the goal is an implication and this tactic is guaranteed
+  to make progress."
+  intro h
+  Hint "Now `{h} : P ∧ Q` is a hypothesis, and
+
+  ```
+  rcases {h} with ⟨p, q⟩
+  ```
+
+  will change `{h}`, the proof of `P ∧ Q`, into two proofs `p : P`
+  and `q : Q`.
+
+  You can write `⟨p, q⟩` with `\\<>` or `\\<` and `\\>`. Note that `rcases h` by itself will just
+  automatically name the new assumptions."
+  rcases h with ⟨p, q⟩
+  Hint "Now a combination of `constructor` and `exact` will get you home."
+  constructor
+  exact q
+  exact p
+
+NewTactic rcases

Game/Levels/OldAdvProposition/Level_3.lean

@@ -0,0 +1,46 @@
+import Game.Metadata
+import Game.MyNat.Addition
+
+
+World "AdvProposition"
+Level 3
+Title "and_trans"
+
+open MyNat
+
+Introduction
+"
+Here is another exercise to `rcases` and `constructor`.
+"
+
+/-- If $P$, $Q$ and $R$ are true/false statements, then $P\\land Q$ and
+$Q\\land R$ together imply $P\\land R$. -/
+Statement --and_trans
+    (P Q R : Prop) : P ∧ Q → Q ∧ R → P ∧ R := by
+  Hint "Here's a trick:
+
+  Your first steps would probably be
+  ```
+  intro h
+  rcases h with ⟨p, q⟩
+  ```
+  i.e. introducing a new assumption and then immediately take it appart.
+
+  In that case you could do that in a single step:
+
+  ```
+  intro ⟨p, q⟩
+  ```
+  "
+  intro hpq
+  rcases hpq with ⟨p, q⟩
+  intro hqr
+  rcases hqr with ⟨q', r⟩
+  constructor
+  exact p
+  exact r
+
+Conclusion
+"
+
+"

Game/Levels/OldAdvProposition/Level_4.lean

@@ -0,0 +1,45 @@
+import Game.Metadata
+import Game.MyNat.Addition
+
+
+World "AdvProposition"
+Level 4
+Title ""
+
+open MyNat
+
+Introduction
+"
+The mathematical statement $P\\iff Q$ is equivalent to $(P\\implies Q)\\land(Q\\implies P)$. The `rcases`
+and `constructor` tactics work on hypotheses and goals (respectively) of the form `P ↔ Q`. If you need
+to write an `↔` arrow you can do so by typing `\\iff`, but you shouldn't need to.
+
+"
+
+/-- If $P$, $Q$ and $R$ are true/false statements, then
+$P\\iff Q$ and $Q\\iff R$ together imply $P\\iff R$. -/
+Statement --iff_trans
+    (P Q R : Prop) : (P ↔ Q) → (Q ↔ R) → (P ↔ R) := by
+  Hint "Similar to \"and\", you can use `intro` and `rcases` to add the `P ↔ Q` to your
+  assumptions and split it into its constituent parts."
+  Branch
+    intro hpq
+    intro hqr
+    Hint "Now you want to use `rcases {hpq} with ⟨pq, qp⟩`."
+    rcases hpq with ⟨hpq, hqp⟩
+    rcases hqr with ⟨hqr, hrq⟩
+  intro ⟨pq, qp⟩
+  intro ⟨qr, rq⟩
+  Hint "If you want to prove an iff-statement, you can use `constructor` to split it
+  into its two implications."
+  constructor
+  · intro p
+    apply qr
+    apply pq
+    exact p
+  · intro r
+    apply qp
+    apply rq
+    exact r
+
+NewDefinition Iff

Game/Levels/OldAdvProposition/Level_5.lean

@@ -0,0 +1,76 @@
+import Game.Metadata
+import Game.MyNat.Addition
+
+
+World "AdvProposition"
+Level 5
+Title "Easter eggs."
+
+open MyNat
+
+Introduction
+"
+Let's try this again. Try proving it in other ways. (Note that `rcases` is temporarily disabled.)
+
+### A trick.
+
+Instead of using `rcases` on `h : P ↔ Q` you can just access the proofs of `P → Q` and `Q → P`
+directly with `h.1` and `h.2`. So you can solve this level with
+
+```
+intro hpq hqr
+constructor
+intro p
+apply hqr.1
+…
+```
+
+### Another trick
+
+Instead of using `rcases` on `h : P ↔ Q`, you can just `rw [h]`, and this will change all `P`s to `Q`s
+in the goal. You can use this to create a much shorter proof. Note that
+this is an argument for *not* running the `rcases` tactic on an iff statement;
+you cannot rewrite one-way implications, but you can rewrite two-way implications.
+
+
+"
+-- TODO
+-- ### Another trick
+-- `cc` works on this sort of goal too.
+
+/-- If $P$, $Q$ and $R$ are true/false statements, then `P ↔ Q` and `Q ↔ R` together imply `P ↔ R`.
+ -/
+Statement --iff_trans
+    (P Q R : Prop) : (P ↔ Q) → (Q ↔ R) → (P ↔ R) := by
+  intro hpq hqr
+  Hint "Make a choice and continue either with `constructor` or `rw`.
+
+  * if you use `constructor`, you will use `{hqr}.1, {hqr}.2, …` later.
+  * if you use `rw`, you can replace all `P`s with `Q`s using `rw [{hpq}]`"
+  Branch
+    rw [hpq]
+    Branch
+      exact hqr
+    rw [hqr]
+    Hint "Now `rfl` can close this goal.
+
+    TODO: Note that the current modification of `rfl` is too weak to prove this. For now, you can
+    use `simp` instead (which calls the \"real\" `rfl` internally)."
+    simp
+  constructor
+  intro p
+  Hint "Now you can directly `apply {hqr}.1`"
+  apply hqr.1
+  apply hpq.1
+  exact p
+  intro r
+  apply hpq.2
+  apply hqr.2
+  exact r
+
+DisabledTactic rcases
+
+Conclusion
+"
+
+"

Game/Levels/OldAdvProposition/Level_6.lean

@@ -0,0 +1,38 @@
+import Game.Metadata
+import Game.MyNat.Addition
+
+
+World "AdvProposition"
+Level 6
+Title "Or, and the `left` and `right` tactics."
+
+open MyNat
+
+Introduction
+"
+`P ∨ Q` means \"$P$ or $Q$\". So to prove it, you
+need to choose one of `P` or `Q`, and prove that one.
+If `P ∨ Q` is your goal, then `left` changes this
+goal to `P`, and `right` changes it to `Q`.
+"
+-- Note that you can take a wrong turn here. Let's
+-- start with trying to prove $Q\\implies (P\\lor Q)$.
+-- After the `intro`, one of `left` and `right` leads
+-- to an impossible goal, the other to an easy finish.
+
+/-- If $P$ and $Q$ are true/false statements, then $Q\\implies(P\\lor Q)$. -/
+Statement
+    (P Q : Prop) : Q → (P ∨ Q) := by
+  Hint (hidden := true) "Let's start with an initial `intro` again."
+  intro q
+  Hint "Now you need to choose if you want to prove the `left` or `right` side of the goal."
+  Branch
+    left
+    -- TODO: This message is also shown on the correct track. Need strict hints.
+    -- Hint "That was an unfortunate choice, you entered a dead end that cannot be proved anymore.
+    -- Hit \"Undo\"!"
+  right
+  exact q
+
+NewTactic left right
+NewDefinition Or

Game/Levels/OldAdvProposition/Level_7.lean

@@ -0,0 +1,55 @@
+import Game.Metadata
+import Game.MyNat.Addition
+
+
+World "AdvProposition"
+Level 7
+Title "`or_symm`"
+
+open MyNat
+
+Introduction
+"
+Proving that $(P\\lor Q)\\implies(Q\\lor P)$ involves an element of danger.
+"
+
+/-- If $P$ and $Q$ are true/false statements, then
+$$P\\lor Q\\implies Q\\lor P.$$  -/
+Statement --or_symm
+    (P Q : Prop) : P ∨ Q → Q ∨ P := by
+  Hint "`intro h` is the obvious start."
+  intro h
+  Branch
+    left
+    Hint "This is a dead end that is not provable anymore. Hit \"undo\"."
+  Branch
+    right
+    Hint "This is a dead end that is not provable anymore. Hit \"undo\"."
+  Hint "But now, even though the goal is an `∨` statement, both `left` and `right` put
+  you in a situation with an impossible goal. Fortunately,
+  you can do `rcases h with p | q`. (that is a normal vertical slash)
+  "
+  rcases h with p | q
+  Hint " Something new just happened: because
+  there are two ways to prove the assumption `P ∨ Q` (namely, proving `P` or proving `Q`),
+  the `rcases` tactic turns one goal into two, one for each case.
+
+  So now you proof the goal under the assumption that `P` is true, and waiting under \"Other Goals\"
+  there is the same goal but under the assumption that `Q` is true.
+
+  You should be able to make it home from there. "
+  right
+  exact p
+  Hint "Note how now you finished the first goal and jumped to the one, where you assume `Q`."
+  left
+  exact q
+
+Conclusion
+"
+Well done! Note that the syntax for `rcases` is different whether it's an \"or\" or an \"and\".
+
+* `rcases h with ⟨p, q⟩` splits an \"and\" in the assumptions into two parts. You get two assumptions
+but still only one goal.
+* `rcases h with p | q` splits an \"or\" in the assumptions. You get **two goals** which have different
+assumptions, once assumping the lefthand-side of the dismantled \"or\"-assumption, once the righthand-side.
+"

Game/Levels/OldAdvProposition/Level_8.lean

@@ -0,0 +1,53 @@
+import Game.Metadata
+import Game.MyNat.Addition
+
+
+World "AdvProposition"
+Level 8
+Title "`and_or_distrib_left`"
+
+open MyNat
+
+Introduction
+"
+We know that $x(y+z)=xy+xz$ for numbers, and this
+is called distributivity of multiplication over addition.
+The same is true for `∧` and `∨` -- in fact `∧` distributes
+over `∨` and `∨` distributes over `∧`. Let's prove one of these.
+"
+
+/-- If $P$. $Q$ and $R$ are true/false statements, then
+$$P\\land(Q\\lor R)\\iff(P\\land Q)\\lor (P\\land R).$$  -/
+Statement --and_or_distrib_left
+    (P Q R : Prop) : P ∧ (Q ∨ R) ↔ (P ∧ Q) ∨ (P ∧ R) := by
+  constructor
+  intro h
+  rcases h with ⟨hp, hqr⟩
+  rcases hqr with q | r
+  left
+  constructor
+  exact hp
+  exact q
+  right
+  constructor
+  exact hp
+  exact r
+  intro h
+  rcases h with hpq | hpr
+  rcases hpq with ⟨p, q⟩
+  constructor
+  exact p
+  left
+  exact q
+  rcases hpr with ⟨hp, hr⟩
+  constructor
+  exact hp
+  right
+  exact hr
+
+
+Conclusion
+"
+You already know enough to embark on advanced addition world. But the next two levels comprise
+just a couple more things.
+"

Game/Levels/OldAdvProposition/Level_9.lean

@@ -0,0 +1,52 @@
+import Game.Metadata
+import Game.MyNat.Addition
+
+
+World "AdvProposition"
+Level 9
+Title "`exfalso` and proof by contradiction. "
+
+open MyNat
+
+Introduction
+"
+It's certainly true that $P\\land(\\lnot P)\\implies Q$ for any propositions $P$
+and $Q$, because the left hand side of the implication is false. But how do
+we prove that `False` implies any proposition $Q$? A cheap way of doing it in
+Lean is using the `exfalso` tactic, which changes any goal at all to `False`.
+You might think this is a step backwards, but if you have a hypothesis `h : ¬ P`
+then after `rw not_iff_imp_false at h,` you can `apply h,` to make progress.
+Try solving this level without using `cc` or `tauto`, but using `exfalso` instead.
+"
+
+/-- If $P$ and $Q$ are true/false statements, then
+$$(P\\land(\\lnot P))\\implies Q.$$ -/
+Statement --contra
+  (P Q : Prop) : (P ∧ ¬ P) → Q := by
+  Hint "Start as usual with `intro ⟨p, np⟩`."
+  Branch
+    exfalso
+    -- TODO: This hint needs to be strict
+    -- Hint "Not so quick! Now you just threw everything away."
+  intro h
+  Hint "You should also call `rcases` on your assumption `{h}`."
+  rcases h with ⟨p, np ⟩
+  -- TODO: This hint should before the last `exact p` step again.
+  Hint "Now you can call `exfalso` to throw away your goal `Q`. It will be replaced with `False` and
+  which means you will have to prove a contradiction."
+  Branch
+    -- TODO: Would `contradiction` not be more useful to introduce than `exfalso`?
+    contradiction
+  exfalso
+  Hint "Recall that `{np} : ¬ P` means `np : P → False`, which means you can simply `apply {np}` now.
+
+  You can also first call `rw [Not] at {np}` to make this step more explicit."
+  Branch
+    rw [Not] at np
+  apply np
+  exact p
+
+-- TODO: `contradiction`?
+NewTactic exfalso
+-- DisabledTactic cc
+LemmaTab "Prop"

Game/Levels/WIPAlgorithm/L10annoying.lean

@@ -0,0 +1,43 @@
+import Game.Levels.Addition.L09add_left_comm
+
+World "Addition"
+Level 10
+Title "harder goals"
+
+namespace MyNat
+
+--**TODO** introduce `repeat` somehow (not sure how)
+
+Introduction
+"
+Sometimes Lean wants us to solve much messier addition goals,
+where the order of the variables needs to be changed
+and the brackets need to be moved around. In this level we learn
+an algorithm which will work for an arbitrary such problem. Let's
+prove `a + b + (c + d) = a + c + d + b`.
+"
+
+/-- If $a, b$, $c$ and $d$ are arbitrary natural numbers, we have
+$(a + b) + (c + d) = ((a + c) + d) + b. -/
+Statement (a b c d : ℕ) : a + d + (b + c) = a + b + c + d := by
+  Hint "We no longer have to use inducion; `add_assoc` and `add_comm` are
+    all the tools we need.
+    Start with `repeat rw [add_assoc]` to push all the brackets to the right."
+  repeat rw [add_assoc]
+  Hint "Now use targetted `rw [add_comm x y]` and `rw [add_left_comm x y]` to
+  switch consecutive variables `x` and `y` on the left hand side until everything
+  is in the right order. The point is that `add_comm` switches the last two,
+  and `add_left_comm` can be used to switch any oher pair of consecutive
+  variables."
+  Hint (hidden := true) "Start with `add_left_comm d b`, which will switch
+  `d` and `b` on the left hand side."
+  rw [add_left_comm d b, add_comm d c]
+  rfl
+
+LemmaTab "Add"
+
+Conclusion
+"
+In the last level we use automation to perform this algorithm
+automatically.
+"

Game/Levels/WIPAlgorithm/L11ac_rfl.lean

@@ -0,0 +1,36 @@
+import Game.Levels.Addition.L09add_left_comm
+
+World "Addition"
+Level 11
+Title "The final boss"
+
+namespace MyNat
+
+Introduction
+"
+We saw in the last level that by performing an algorithm repeating `add_assoc`
+and then applying `add_comm` and `add_left_comm` to sort variables, enables
+us to manually prove arbitrary identities involving addition of natural
+numbers. Let's now write a tactic which automates this.
+
+**TODO** ac_rfl tactic
+"
+
+macro_rules | `(tactic| ac_rfl) => `(tactic| simp only [add_assoc, add_left_comm, add_comm])
+
+/-- 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
+  ac_rfl
+
+NewTactic ac_rfl
+LemmaTab "Add"
+
+Conclusion
+"
+Congratulations! You finished addition world. Now go back to the overworld by clicking the
+home button in the top left. If you want to press on to the final boss
+of the game then go to Multiplication world next. If you are in no hurry, and would like
+to learn some more tactics, then you can try Advanced Addition World.
+"

Game/Levels/WIPFuncProg/decide_level.lean

@@ -0,0 +1,41 @@
+import Game.Metadata
+import Game.MyNat.Addition
+import Game.MyNat.DecidableEq
+World "Addition"
+Level 4
+Title "Twenty add twenty is forty."
+
+--namespace MyNat
+namespace MyNat
+
+TacticDoc decide "
+The `decide` tactic is able to prove goals involving *known numerals*. It is not
+good with algebra, so don't give it goals with `x`s in, but it can prove
+things like `2 + 2 = 4` and even `20 + 20 = 40` automatically.
+
+When run on `MyNat` goals, the tactic uses the decidable equality instance
+on `MyNat` in `Game.MyNat.DecidableEq`. The implementation
+is not at all optimised: I just wanted to get something which could beat
+humans easily.
+"
+
+NewTactic decide
+
+example : (20 : ℕ) + 20 = 40 := by
+  decide
+
+Introduction
+"
+Oh did I mention there was a new tactic? Find it highlighted in your inventory.
+"
+
+/-- $29+35=64$. -/
+Statement : (29 : ℕ) + 35 = 64 := by
+  decide
+
+LemmaTab "Add"
+
+Conclusion
+"
+The `decide` tactic destroys sub-bosses such as `2 + 2 = 4`.
+"

Game/Levels/WIPHard.lean

@@ -0,0 +1,7 @@
+import GameServer.Commands
+
+World "Hard"
+Title "Impossible World"
+
+Introduction
+""

Game/Levels/WIPLessThan.lean

@@ -0,0 +1,7 @@
+import Game.Levels.Inequality
+
+World "StrongInduction"
+Title "Strong Induction World"
+
+Introduction
+""

Game/Levels/WIPPrime.lean

@@ -0,0 +1,7 @@
+import Game.Levels.Inequality
+
+World "Prime"
+Title "Prime World"
+
+Introduction
+""

Game/Levels/WIPTODOFINDIVANLEVELSEvenOdd.lean

@@ -0,0 +1,7 @@
+import GameServer.Commands
+
+World "EvenOdd"
+Title "Parity World"
+
+Introduction
+""

vid_script.txt

@@ -0,0 +1,40 @@
+How I made the natural number game.
+
+Peter Johnstone taught me that 0 was {}, 1 was {{}}, 2 was {{},{{}}} and so on. But what about all the people who didn't go to that class?
+
+Set theory is *one way of doing mathematics*.
+
+Type theory is *another way of doing mathematics*
+
+Naturals, integers, rationals, reals. Diophantus actually worked with positive rationals, which have a beautiful multiplicative structure: they are the free multiplicative abelian group on the primes. Similarly the positive naturals {1,2,3,4,...} (the British Natural Numbers, as I was taught at the University of Cambridge) as Patrick teaches the French in Saclay.
+
+But when you look at a natural number in type theory b;ah blah
+
+
+In mathematics, when you say "let G be a group" what you mean is that G is a set, and G has elements, and the elements are all individual "atoms", and that it is impossible to split the atom.
+
+Building the natural number game
+
+Think of some good targets.
+2+2=4
+x+y=y+x
+all axioms of a commutative semiring
+(e.g. x*(y+z)=x*y+x*z etc) and maybe several other natural statements (0*x=0 etc)
+All axioms of a total ordering <= 
+Later:
+Archie Browne divisibility world all by himself
+Ivan ... even_odd world
+
+Solving 3*x+4*y=7 and 5*x+6*y=11.
+Diophantus would have understood that
+question and he hadn't even invented 0 yet.
+
+We prove cancellation.
+
+add_comm and add_assoc and then we use simp to make one tactic which can solve this. We make a term called decidable_eq and then all of a sudden we 
+
+
+A theorem
+Load of old nonsense.
+
+IDeas: geometry game, 

vid_script.txt~

@@ -0,0 +1,15 @@
+How I made the natural number game.
+
+Peter Johnstone taught me that 0 was {}, 1 was {{}}, 2 was {{},{{}}} and so on. But what about all the people who didn't go to that class?
+
+Set theory is *one way of doing mathematics*.
+
+Type theory is *another way of doing mathematics*
+
+In mathematics, when you say "let G be a group" what you mean is that G is a set, and G has elements, and the elements are all individual "atoms", and that it is impossible to split the atom.
+
+
+A theorem
+Load of old nonsense.
+
+IDeas: geometry game,