From 20bc9fe61d6b65423e17b65e14747809acbe0988 Mon Sep 17 00:00:00 2001 From: Kevin Buzzard Date: Sat, 14 Oct 2023 19:57:20 +0100 Subject: [PATCH] move all WIP files to level-rewrite branch --- Game/Levels/Map.txt | 105 ++++++++++++++++++ Game/Levels/OldAdvMultiplication.lean | 13 +++ Game/Levels/OldAdvMultiplication/Level_1.lean | 51 +++++++++ Game/Levels/OldAdvMultiplication/Level_2.lean | 39 +++++++ Game/Levels/OldAdvMultiplication/Level_3.lean | 36 ++++++ Game/Levels/OldAdvMultiplication/Level_4.lean | 97 ++++++++++++++++ .../OldAdvMultiplication/mul_left_comm.lean | 75 +++++++++++++ Game/Levels/OldAdvProposition/Level_1.lean | 41 +++++++ Game/Levels/OldAdvProposition/Level_10.lean | 64 +++++++++++ Game/Levels/OldAdvProposition/Level_2.lean | 48 ++++++++ Game/Levels/OldAdvProposition/Level_3.lean | 46 ++++++++ Game/Levels/OldAdvProposition/Level_4.lean | 45 ++++++++ Game/Levels/OldAdvProposition/Level_5.lean | 76 +++++++++++++ Game/Levels/OldAdvProposition/Level_6.lean | 38 +++++++ Game/Levels/OldAdvProposition/Level_7.lean | 55 +++++++++ Game/Levels/OldAdvProposition/Level_8.lean | 53 +++++++++ Game/Levels/OldAdvProposition/Level_9.lean | 52 +++++++++ Game/Levels/WIPAlgorithm/L10annoying.lean | 43 +++++++ Game/Levels/WIPAlgorithm/L11ac_rfl.lean | 36 ++++++ Game/Levels/WIPFuncProg/decide_level.lean | 41 +++++++ Game/Levels/WIPHard.lean | 7 ++ Game/Levels/WIPLessThan.lean | 7 ++ Game/Levels/WIPPrime.lean | 7 ++ Game/Levels/WIPTODOFINDIVANLEVELSEvenOdd.lean | 7 ++ vid_script.txt | 40 +++++++ vid_script.txt~ | 15 +++ 26 files changed, 1137 insertions(+) create mode 100644 Game/Levels/Map.txt create mode 100644 Game/Levels/OldAdvMultiplication.lean create mode 100644 Game/Levels/OldAdvMultiplication/Level_1.lean create mode 100644 Game/Levels/OldAdvMultiplication/Level_2.lean create mode 100644 Game/Levels/OldAdvMultiplication/Level_3.lean create mode 100644 Game/Levels/OldAdvMultiplication/Level_4.lean create mode 100644 Game/Levels/OldAdvMultiplication/mul_left_comm.lean create mode 100644 Game/Levels/OldAdvProposition/Level_1.lean create mode 100644 Game/Levels/OldAdvProposition/Level_10.lean create mode 100644 Game/Levels/OldAdvProposition/Level_2.lean create mode 100644 Game/Levels/OldAdvProposition/Level_3.lean create mode 100644 Game/Levels/OldAdvProposition/Level_4.lean create mode 100644 Game/Levels/OldAdvProposition/Level_5.lean create mode 100644 Game/Levels/OldAdvProposition/Level_6.lean create mode 100644 Game/Levels/OldAdvProposition/Level_7.lean create mode 100644 Game/Levels/OldAdvProposition/Level_8.lean create mode 100644 Game/Levels/OldAdvProposition/Level_9.lean create mode 100644 Game/Levels/WIPAlgorithm/L10annoying.lean create mode 100644 Game/Levels/WIPAlgorithm/L11ac_rfl.lean create mode 100644 Game/Levels/WIPFuncProg/decide_level.lean create mode 100644 Game/Levels/WIPHard.lean create mode 100644 Game/Levels/WIPLessThan.lean create mode 100644 Game/Levels/WIPPrime.lean create mode 100644 Game/Levels/WIPTODOFINDIVANLEVELSEvenOdd.lean create mode 100644 vid_script.txt create mode 100644 vid_script.txt~ diff --git a/Game/Levels/Map.txt b/Game/Levels/Map.txt new file mode 100644 index 0000000..9cb68c2 --- /dev/null +++ b/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 := diff --git a/Game/Levels/OldAdvMultiplication.lean b/Game/Levels/OldAdvMultiplication.lean new file mode 100644 index 0000000..69f34df --- /dev/null +++ b/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. +" diff --git a/Game/Levels/OldAdvMultiplication/Level_1.lean b/Game/Levels/OldAdvMultiplication/Level_1.lean new file mode 100644 index 0000000..f8e315c --- /dev/null +++ b/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 +" + +" diff --git a/Game/Levels/OldAdvMultiplication/Level_2.lean b/Game/Levels/OldAdvMultiplication/Level_2.lean new file mode 100644 index 0000000..01e2e7f --- /dev/null +++ b/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 +" + +" diff --git a/Game/Levels/OldAdvMultiplication/Level_3.lean b/Game/Levels/OldAdvMultiplication/Level_3.lean new file mode 100644 index 0000000..5545789 --- /dev/null +++ b/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 +" + +" diff --git a/Game/Levels/OldAdvMultiplication/Level_4.lean b/Game/Levels/OldAdvMultiplication/Level_4.lean new file mode 100644 index 0000000..a037c47 --- /dev/null +++ b/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 +" + +" diff --git a/Game/Levels/OldAdvMultiplication/mul_left_comm.lean b/Game/Levels/OldAdvMultiplication/mul_left_comm.lean new file mode 100644 index 0000000..4b3a116 --- /dev/null +++ b/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 +-- ``` diff --git a/Game/Levels/OldAdvProposition/Level_1.lean b/Game/Levels/OldAdvProposition/Level_1.lean new file mode 100644 index 0000000..517fb34 --- /dev/null +++ b/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 +" +" diff --git a/Game/Levels/OldAdvProposition/Level_10.lean b/Game/Levels/OldAdvProposition/Level_10.lean new file mode 100644 index 0000000..ecc991b --- /dev/null +++ b/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. diff --git a/Game/Levels/OldAdvProposition/Level_2.lean b/Game/Levels/OldAdvProposition/Level_2.lean new file mode 100644 index 0000000..519f7be --- /dev/null +++ b/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 diff --git a/Game/Levels/OldAdvProposition/Level_3.lean b/Game/Levels/OldAdvProposition/Level_3.lean new file mode 100644 index 0000000..dfab36a --- /dev/null +++ b/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 +" + +" diff --git a/Game/Levels/OldAdvProposition/Level_4.lean b/Game/Levels/OldAdvProposition/Level_4.lean new file mode 100644 index 0000000..8ea0c51 --- /dev/null +++ b/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 diff --git a/Game/Levels/OldAdvProposition/Level_5.lean b/Game/Levels/OldAdvProposition/Level_5.lean new file mode 100644 index 0000000..81e9043 --- /dev/null +++ b/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 +" + +" diff --git a/Game/Levels/OldAdvProposition/Level_6.lean b/Game/Levels/OldAdvProposition/Level_6.lean new file mode 100644 index 0000000..06b778d --- /dev/null +++ b/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 diff --git a/Game/Levels/OldAdvProposition/Level_7.lean b/Game/Levels/OldAdvProposition/Level_7.lean new file mode 100644 index 0000000..2539e52 --- /dev/null +++ b/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. +" diff --git a/Game/Levels/OldAdvProposition/Level_8.lean b/Game/Levels/OldAdvProposition/Level_8.lean new file mode 100644 index 0000000..09bd2a7 --- /dev/null +++ b/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. +" diff --git a/Game/Levels/OldAdvProposition/Level_9.lean b/Game/Levels/OldAdvProposition/Level_9.lean new file mode 100644 index 0000000..6913953 --- /dev/null +++ b/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" diff --git a/Game/Levels/WIPAlgorithm/L10annoying.lean b/Game/Levels/WIPAlgorithm/L10annoying.lean new file mode 100644 index 0000000..11bd704 --- /dev/null +++ b/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. +" diff --git a/Game/Levels/WIPAlgorithm/L11ac_rfl.lean b/Game/Levels/WIPAlgorithm/L11ac_rfl.lean new file mode 100644 index 0000000..09db657 --- /dev/null +++ b/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. +" diff --git a/Game/Levels/WIPFuncProg/decide_level.lean b/Game/Levels/WIPFuncProg/decide_level.lean new file mode 100644 index 0000000..4025e09 --- /dev/null +++ b/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`. +" diff --git a/Game/Levels/WIPHard.lean b/Game/Levels/WIPHard.lean new file mode 100644 index 0000000..616da51 --- /dev/null +++ b/Game/Levels/WIPHard.lean @@ -0,0 +1,7 @@ +import GameServer.Commands + +World "Hard" +Title "Impossible World" + +Introduction +"" diff --git a/Game/Levels/WIPLessThan.lean b/Game/Levels/WIPLessThan.lean new file mode 100644 index 0000000..41eafab --- /dev/null +++ b/Game/Levels/WIPLessThan.lean @@ -0,0 +1,7 @@ +import Game.Levels.Inequality + +World "StrongInduction" +Title "Strong Induction World" + +Introduction +"" diff --git a/Game/Levels/WIPPrime.lean b/Game/Levels/WIPPrime.lean new file mode 100644 index 0000000..86d4871 --- /dev/null +++ b/Game/Levels/WIPPrime.lean @@ -0,0 +1,7 @@ +import Game.Levels.Inequality + +World "Prime" +Title "Prime World" + +Introduction +"" diff --git a/Game/Levels/WIPTODOFINDIVANLEVELSEvenOdd.lean b/Game/Levels/WIPTODOFINDIVANLEVELSEvenOdd.lean new file mode 100644 index 0000000..598378d --- /dev/null +++ b/Game/Levels/WIPTODOFINDIVANLEVELSEvenOdd.lean @@ -0,0 +1,7 @@ +import GameServer.Commands + +World "EvenOdd" +Title "Parity World" + +Introduction +"" diff --git a/vid_script.txt b/vid_script.txt new file mode 100644 index 0000000..f3dae95 --- /dev/null +++ b/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, diff --git a/vid_script.txt~ b/vid_script.txt~ new file mode 100644 index 0000000..2073e53 --- /dev/null +++ b/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,