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
+"
+
+"