From fdad0f8a1ec9d82fd91930143e76b9b0a5dc1677 Mon Sep 17 00:00:00 2001 From: Jon Eugster Date: Wed, 27 Mar 2024 01:13:33 +0100 Subject: [PATCH] add empty zh json --- .i18n/zh/Game.json | 741 +++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 741 insertions(+) create mode 100644 .i18n/zh/Game.json diff --git a/.i18n/zh/Game.json b/.i18n/zh/Game.json new file mode 100644 index 0000000..74e5935 --- /dev/null +++ b/.i18n/zh/Game.json @@ -0,0 +1,741 @@ +{"≤ World": "", + "≠": "", + "zero_pow_zero": "", + "zero_pow_succ": "", + "zero_ne_succ": "", + "zero_mul": "", + "zero_add": "", + "x ≤ y or y ≤ x": "", + "x ≤ y and y ≤ z implies x ≤ z": "", + "x ≤ y and y ≤ x implies x = y": "", + "x ≤ succ x": "", + "x ≤ 1": "", + "x ≤ 0 → x = 0": "", + "two_mul": "", + "try rewriting `add_zero`.": "", + "the simplest approach": "", + "the rw tactic": "", + "succ_mul": "", + "succ_inj : the successor function is injective": "", + "succ_add": "", + "succ x ≤ succ y → x ≤ y": "", + "rewriting backwards": "", + "pred": "", + "pow_two": "", + "pow_pow": "", + "pow_one": "", + "pow_add": "", + "one_pow": "", + "one_mul": "", + "one_le_of_ne_zero": "", + "mul_right_eq_self": "", + "mul_right_eq_one": "", + "mul_pow": "", + "mul_one": "", + "mul_ne_zero": "", + "mul_left_ne_zero": "", + "mul_left_cancel": "", + "mul_le_mul_right": "", + "mul_eq_zero": "", + "mul_comm": "", + "mul_assoc": "", + "mul_add": "", + "making life simple": "", + "making life easier": "", + "le_two": "", + "le_mul_right": "", + "is_zero": "", + "intro practice": "", + "intro": "", + "eq_succ_of_ne_zero": "", + "decide again": "", + "decide": "", + "add_succ": "", + "add_sq": "", + "add_right_eq_zero": "", + "add_right_eq_self": "", + "add_right_comm": "", + "add_right_cancel": "", + "add_mul": "", + "add_left_eq_zero": "", + "add_left_eq_self": "", + "add_left_comm": "", + "add_left_cancel": "", + "add_comm (level boss)": "", + "add_assoc (associativity of addition)": "", + "`ℕ` is the natural numbers, just called \\\"numbers\\\" in this game. It's\ndefined via two rules:\n\n* `0 : ℕ` (zero is a number)\n* `succ (n : ℕ) : ℕ` (the successor of a number is a number)\n\n## Game Implementation\n\n*The game uses its own copy of the natural numbers, called `MyNat` with notation `ℕ`.\nIt is distinct from the Lean natural numbers `Nat`, which should hopefully\nnever leak into the natural number game.*": + "", + "`zero_ne_succ n` is the proof that `0 ≠ succ n`.\n\nIn Lean, `a ≠ b` is *defined to mean* `a = b → False`. Hence\n`zero_ne_succ n` is really a proof of `0 = succ n → False`.\nHere `False` is a generic false statement. This means that\nyou can `apply zero_ne_succ at h` if `h` is a proof of `0 = succ n`.": + "", + "`zero_ne_one` is a proof of `0 ≠ 1`.": "", + "`zero_mul x` is the proof that `0 * x = 0`.\n\nNote: `zero_mul` is a `simp` lemma.": + "", + "`zero_le x` is a proof that `0 ≤ x`.": "", + "`zero_add x` is the proof of `0 + x = x`.\n\n`zero_add` is a `simp` lemma, because replacing `0 + x` by `x`\nis almost always what you want to do if you're simplifying an expression.": + "", + "`xyzzy` is an ancient magic spell, believed to be the origin of the\nmodern word `sorry`. The game won't complain - or notice - if you\nprove anything with `xyzzy`.": + "", + "`two_mul m` is the proof that `2 * m = m + m`.": "", + "`two_eq_succ_one` is a proof of `2 = succ 1`.": "", + "`three_eq_succ_two` is a proof of `3 = succ 2`.": "", + "`tauto` is good enough to solve this goal.": "", + "`succ_ne_zero a` is a proof of `succ a ≠ 0`.": "", + "`succ_ne_succ m n` is the proof that `m ≠ n → succ m ≠ succ n`.": "", + "`succ_mul a b` is the proof that `succ a * b = a * b + b`.\n\nIt could be deduced from `mul_succ` and `mul_comm`, however this argument\nwould be circular because the proof of `mul_comm` uses `mul_succ`.": + "", + "`succ_le_succ x y` is a proof that if `succ x ≤ succ y` then `x ≤ y`.": "", + "`succ_eq_add_one n` is the proof that `succ n = n + 1`.": "", + "`succ_add a b` is a proof that `succ a + b = succ (a + b)`.": "", + "`rw [one_eq_succ_zero]` will do this.": "", + "`rw [add_zero]` will change `b + 0` into `b`.": "", + "`rw [add_comm b d]`.": "", + "`pred_succ n` is a proof of `pred (succ n) = n`.": "", + "`pow_zero a : a ^ 0 = 1` is one of the two axioms\ndefining exponentiation in this game.": + "", + "`pow_two a` says that `a ^ 2 = a * a`.": "", + "`pow_succ a b : a ^ (succ b) = a ^ b * a` is one of the\ntwo axioms defining exponentiation in this game.": + "", + "`pow_pow a m n` is a proof that $(a^m)^n=a^{mn}.$": "", + "`pow_one a` says that `a ^ 1 = a`.\n\nNote that this is not quite true by definition: `a ^ 1` is\ndefined to be `a ^ 0 * a` so it's `1 * a`, and to prove\nthat this is equal to `a` you need to use induction somewhere.": + "", + "`pow_add a m n` is a proof that $a^{m+n}=a^ma^n.$": "", + "`one_pow n` is a proof that $1^n=1$.": "", + "`one_ne_zero` is a proof that `1 ≠ 0`.": "", + "`one_mul m` is the proof `1 * m = m`.": "", + "`one_le_of_ne_zero a` is a proof that `a ≠ 0 → 1 ≤ a`.": "", + "`one_eq_succ_zero` is a proof of `1 = succ 0`.\"": "", + "`nth_rewrite 2 [two_eq_succ_one]` is I think quicker than `rw [two_eq_succ_one]`.": + "", + "`mul_zero m` is the proof that `m * 0 = 0`.": "", + "`mul_succ a b` is the proof that `a * succ b = a * b + a`.": "", + "`mul_right_eq_self a b` is a proof that if `a ≠ 0` and `a * b = a` then `b = 1`.": + "", + "`mul_right_eq_one a b` is a proof that `a * b = 1 → a = 1`.": "", + "`mul_pow a b n` is a proof that $(ab)^n=a^nb^n.$": "", + "`mul_one m` is the proof that `m * 1 = m`.": "", + "`mul_ne_zero a b` is a proof that if `a ≠ 0` and `b ≠ 0` then `a * b ≠ 0`.": + "", + "`mul_left_ne_zero a b` is a proof that `a * b ≠ 0 → b ≠ 0`.": "", + "`mul_left_cancel a b c` is a proof that if `a ≠ 0` and `a * b = a * c` then `b = c`.": + "", + "`mul_le_mul_right a b t` is a proof that `a ≤ b → a * t ≤ b * t`.": "", + "`mul_eq_zero a b` is a proof that if `a * b = 0` then `a = 0` or `b = 0`.": + "", + "`mul_comm` is the proof that multiplication is commutative. More precisely,\n`mul_comm a b` is the proof that `a * b = b * a`.": + "", + "`mul_assoc a b c` is a proof that `(a * b) * c = a * (b * c)`.\n\nNote that when Lean says `a * b * c` it means `(a * b) * c`.\n\nNote that `(a * b) * c = a * (b * c)` cannot be proved by \\\"pure thought\\\":\nfor example subtraction is not associative, as `(6 - 2) - 1` is not\nequal to `6 - (2 - 1)`.": + "", + "`le_zero x` is a proof of the implication `x ≤ 0 → x = 0`.": "", + "`le_zero x` is a proof of `x ≤ 0 → x = 0`.": "", + "`le_two x` is a proof that if `x ≤ 2` then `x = 0` or `x = 1` or `x = 2`.": + "", + "`le_trans x y z` is a proof that if `x ≤ y` and `y ≤ z` then `x ≤ z`.\nMore precisely, it is a proof that `x ≤ y → (y ≤ z → x ≤ z)`. In words,\nIf $x \\le y$ then (pause) if $y \\le z$ then $x \\le z$.\n\n## A note on associativity\n\nIn Lean, `a + b + c` means `(a + b) + c`, because `+` is left associative. However\n`→` is right associative. This means that `x ≤ y → y ≤ z → x ≤ z` in Lean means\nexactly that `≤` is transitive. This is different to how mathematicians use\n$P \\implies Q \\implies R$; for them, this usually means that $P \\implies Q$\nand $Q \\implies R$.": + "", + "`le_total x y` is a proof that `x ≤ y` or `y ≤ x`.": "", + "`le_succ_self x` is a proof that `x ≤ succ x`.": "", + "`le_refl x` is a proof of `x ≤ x`.\n\nThe reason for the name is that this lemma is \"reflexivity of $\\le$\"": + "", + "`le_one x` is a proof that if `x ≤ 1` then `x = 0` or `x = 1`.": "", + "`le_mul_right a b` is a proof that `a * b ≠ 0 → a ≤ a * b`.\n\nIt's one way of saying that a divisor of a positive number\nhas to be at most that number.": + "", + "`le_antisymm x y` is a proof that if `x ≤ y` and `y ≤ x` then `x = y`.": "", + "`is_zero_zero` is a proof of `is_zero 0 = True`.": "", + "`is_zero_succ a` is a proof of `is_zero (succ a) = False`.": "", + "`four_eq_succ_three` is a proof of `4 = succ 3`.": "", + "`exact` practice.": "", + "`eq_succ_of_ne_zero a` is a proof that `a ≠ 0 → ∃ n, a = succ n`.": "", + "`add_zero c` is a proof of `c + 0 = c` so that was what got rewritten.\nYou can now change `b + 0` to `b` with `rw [add_zero]` or `rw [add_zero b]`. You\ncan usually stick to `rw [add_zero]` unless you need real precision.": + "", + "`add_zero a` is a proof that `a + 0 = a`.\n\n## Summary\n\n`add_zero` is really a function, which\neats a number, and returns a proof of a theorem\nabout that number. For example `add_zero 37` is\na proof that `37 + 0 = 37`.\n\nThe `rw` tactic will accept `rw [add_zero]`\nand will try to figure out which number you omitted\nto input.\n\n## Details\n\nA mathematician sometimes thinks of `add_zero`\nas \\\"one thing\\\", namely a proof of $\\forall n ∈ ℕ, n + 0 = n$.\nThis is just another way of saying that it's a function which\ncan eat any number n and will return a proof that `n + 0 = n`.": + "", + "`add_succ a b` is the proof of `a + succ b = succ (a + b)`.": "", + "`add_sq a b` is the statement that $(a+b)^2=a^2+b^2+2ab.$": "", + "`add_right_eq_self x y` is the theorem that $x + y = x\\implies y=0.$\nTwo ways to do it spring to mind; I'll mention them when you've solved it.\n": + "", + "`add_right_eq_self x y` is the theorem that $x + y = x \\implies y=0.$": "", + "`add_right_comm a b c` is a proof that `(a + b) + c = (a + c) + b`\n\nIn Lean, `a + b + c` means `(a + b) + c`, so this result gets displayed\nas `a + b + c = a + c + b`.": + "", + "`add_right_cancel a b n` is the theorem that $a+n=b+n \\implies a=b.$": "", + "`add_mul a b c` is a proof that $(a+b)c=ac+bc$.": "", + "`add_left_eq_self x y` is the theorem that $x + y = y \\implies x=0.$": "", + "`add_left_comm a b c` is a proof that `a + (b + c) = b + (a + c)`.": "", + "`add_left_cancel a b n` is the theorem that $n+a=n+b\\implies a=b$.\nYou can prove it by induction on `n` or you can deduce it from `add_right_cancel`.\n": + "", + "`add_left_cancel a b n` is the theorem that $n+a=n+b \\implies a=b.$": "", + "`add_comm x y` is a proof of `x + y = y + x`.": "", + "`add_assoc a b c` is a proof\nthat `(a + b) + c = a + (b + c)`. Note that in Lean `(a + b) + c` prints\nas `a + b + c`, because the notation for addition is defined to be left\nassociative.": + "", + "`a ≤ b` is *notation* for `∃ c, b = a + c`.\n\nBecause this game doesn't have negative numbers, this definition\nis mathematically valid.\n\nThis means that if you have a goal of the form `a ≤ b` you can\nmake progress with the `use` tactic, and if you have a hypothesis\n`h : a ≤ b`, you can make progress with `cases h with c hc`.": + "", + "`a ≠ b` is *notation* for `(a = b) → False`.\n\nThe reason this is mathematically\nvalid is that if `P` is a true-false statement then `P → False`\nis the logical opposite of `P`. Indeed `True → False` is false,\nand `False → False` is true!\n\nThe upshot of this is that use can treat `a ≠ b` in exactly\nthe same way as you treat any implication `P → Q`. For example,\nif your *goal* is of the form `a ≠ b` then you can make progress\nwith `intro h`, and if you have a hypothesis `h` of the\nform `a ≠ b` then you can `apply h at h1` if `h1` is a proof\nof `a = b`.": + "", + "`Pow a b`, with notation `a ^ b`, is the usual\n exponentiation of natural numbers. Internally it is\n defined via two axioms:\n\n * `pow_zero a : a ^ 0 = 1`\n\n * `pow_succ a b : a ^ succ b = a ^ b * a`\n\nNote in particular that `0 ^ 0 = 1`.": + "", + "`Mul a b`, with notation `a * b`, is the usual\n product of natural numbers. Internally it is\n via two axioms:\n\n * `mul_zero a : a * 0 = 0`\n\n * `mul_succ a b : a * succ b = a * b + a`\n\nOther theorems about naturals, such as `zero_mul`,\nare proved by induction from these two basic theorems.": + "", + "`Add a b`, with notation `a + b`, is\nthe usual sum of natural numbers. Internally it is defined\nvia the following two hypotheses:\n\n* `add_zero a : a + 0 = a`\n\n* `add_succ a b : a + succ b = succ (a + b)`\n\nOther theorems about naturals, such as `zero_add a : 0 + a = a`, are proved\nby induction using these two basic theorems.\"": + "", + "[dramatic music]. Now are you ready to face the first boss of the game?": "", + "You want to use `add_right_eq_zero`, which you already\nproved, but you'll have to start with `symm at` your hypothesis.": + "", + "You still don't know which way to go, so do `cases «{e}» with a`.": "", + "You now know enough tactics to prove `2 + 2 = 4`! Let's begin the journey.\n": + "", + "You might want to think about whether induction\non `a` or `b` is the best idea.": + "", + "You can use `rw [zero_add] at «{h}»` to rewrite at `«{h}»` instead\nof at the goal.": + "", + "You can start a proof by induction on `n` by typing:\n`induction n with d hd`.": + "", + "You can read more about the `decide` tactic by clicking\non it in the top right.": + "", + "You can put a `←` in front of any theorem provided to `rw` to rewrite\nthe other way around. Look at the docs for `rw` for an explanation. Type `←` with `\\l`.": + "", + "You can probably take it from here.": "", + "You can now finish with `exact h`.": "", + "You can now `apply mul_left_cancel at h`": "", + "You can just mimic the previous proof to do this one -- or you can figure out a way\nof using it.\n": + "", + "You can do induction on any of the three variables. Some choices\nare harder to push through than others. Can you do the inductive step in\n5 rewrites only?": + "", + "What do you think of this two-liner:\n```\nsymm\nexact zero_ne_one\n```\n\n`exact` doesn't just take hypotheses, it will eat any proof which exists\nin the system.\n": + "", + "Well done!": "", + "Welcome to tutorial world! In this world we learn the basics\nof proving theorems. The boss level of this world\nis the theorem `2 + 2 = 4`.\n\nYou prove theorems by solving puzzles using tools called *tactics*.\nThe aim is to prove the theorem by applying tactics\nin the right order.\n\nLet's learn some basic tactics. Click on \"Start\" below\nto begin your quest.\n": + "", + "We've just seen that `0 ^ 0 = 1`, but if `n`\nis a successor, then `0 ^ n = 0`. We prove that here.": + "", + "We're going to change that `False` into `True`. Start by changing it into\n`is_zero (succ a)` by executing `rw [← is_zero_succ a]`.": + "", + "We want to use `le_mul_right`, but we need a hypothesis `x * y ≠ 0`\nwhich we don't have. Yet. Execute `have h2 : x * y ≠ 0` (you can type `≠` with `\\ne`).\nYou'll be asked to\nprove it, and then you'll have a new hypothesis which you can apply\n`le_mul_right` to.": + "", + "We want to reduce this to a hypothesis `b = 0` and a goal `a * b = 0`,\nwhich is logically equivalent but much easier to prove. Remember that `X ≠ 0`\nis notation for `X = 0 → False`. Click on `Show more help!` if you need hints.": + "", + "We still can't prove `2 + 2 ≠ 5` because we have not talked about the\ndefinition of `≠`. In Lean, `a ≠ b` is *notation* for `a = b → False`.\nHere `False` is a generic false proposition, and `→` is Lean's notation\nfor \"implies\". In logic we learn\nthat `True → False` is false, but `False → False` is true. Hence\n`X → False` is the logical opposite of `X`.\n\nEven though `a ≠ b` does not look like an implication,\nyou should treat it as an implication. The next two levels will show you how.\n\n`False` is a goal which you cannot deduce from a consistent set of assumptions!\nSo if your goal is `False` then you had better hope that your hypotheses\nare contradictory, which they are in this level.\n": + "", + "We have seen how to `apply` theorems and assumptions\nof the form `P → Q`. But what if our *goal* is of the form `P → Q`?\nTo prove this goal, we need to know how to say \"let's assume `P` and deduce `Q`\"\nin Lean. We do this with the `intro` tactic.\n": + "", + "We don't know whether to go left or right yet. So start with `cases «{h}» with hx hy`.": + "", + "Use the previous lemma with `apply eq_succ_of_ne_zero at ha`.": "", + "Use `mul_eq_zero` and remember that `tauto` will solve a goal\nif there are hypotheses `a = 0` and `a ≠ 0`.": + "", + "Use `add_succ`.": "", + "Tutorial World": "", + "Try `rw [← one_eq_succ_zero]` to change `succ 0` into `1`.": "", + "Try `rw [add_zero c]`.": "", + "Try `cases «{hd}» with h1 h2`.": "", + "Those of you interested in speedrunning the game may want to know\nthat `repeat rw [add_zero]` will do both rewrites at once.\n": + "", + "This time, use the `left` tactic.": "", + "The way to start this proof is `induction b with d hd generalizing c`.": "", + "The rfl tactic": "", + "The reason `«{x}» ≤ «{x}»` is because `«{x}» = «{x}» + 0`.\nSo you should start this proof with `use 0`.": + "", + "The previous lemma can be used to prove this one.\n": "", + "The next result we'll need in `≤` World is that if `a + b = 0` then `a = 0` and `b = 0`.\nLet's prove one of these facts in this level, and the other in the next.\n\n## A new tactic: `cases`\n\nThe `cases` tactic will split an object or hypothesis up into the possible ways\nthat it could have been created.\n\nFor example, sometimes you want to deal with the two cases `b = 0` and `b = succ d` separately,\nbut don't need the inductive hypothesis `hd` that comes with `induction b with d hd`.\nIn this situation you can use `cases b with d` instead. There are two ways to make\na number: it's either zero or a successor. So you will end up with two goals, one\nwith `b = 0` and one with `b = succ d`.\n\nAnother example: if you have a hypothesis `h : False` then you are done, because a false statement implies\nany statement. Here `cases h` will close the goal, because there are *no* ways to\nmake a proof of `False`! So you will end up with no goals, meaning you have proved everything.\n\n": + "", + "The lemma proved in the final level of this world will be helpful\nin Divisibility World.\n": + "", + "The inductive hypothesis `hd` is \"For all natural numbers `c`, `a * d = a * c → d = c`\".\nYou can `apply` it `at` any hypothesis of the form `a * d = a * ?`. ": + "", + "The goal in this level is one of our hypotheses. Solve the goal by executing `exact h1`.": + "", + "The classical introduction game for Lean.": "", + "The `use` tactic": "", + "The `exact` tactic": "", + "The `apply` tactic.": "", + "Start with induction on `n`.": "", + "Start with `rw [← pred_succ a]` and take it from there.": "", + "Start with `rw [two_eq_succ_one]` to begin to break `2` down into its definition.": + "", + "Start with `repeat rw [add_assoc]` to push all the brackets to the right.": + "", + "Start with `intro hb`.": "", + "Start with `intro h`.": "", + "Start with `intro h` to assume the hypothesis.": "", + "Start with `intro h` to assume the hypothesis and call its proof `h`.": "", + "Start with `intro h` (remembering that `X ≠ Y` is just notation\nfor `X = Y → False`).": + "", + "Start with `induction «{y}» with d hd`.": "", + "Start with `have h2 := mul_ne_zero a b`.": "", + "Start with `contrapose! h`, to change the goal into its\ncontrapositive, namely a hypothesis of `succ m = succ m` and a goal of `m = n`.": + "", + "Start with `cases «{hxy}» with a ha`.": "", + "Start with `cases a with d` to do a case split on `a = 0` and `a = succ d`.": + "", + "Start with `apply succ_inj` to apply `succ_inj` to the *goal*.": "", + "Start with `apply h2 at h1`. This will change `h1` to `y = 42`.": "", + "Start with `apply eq_succ_of_ne_zero at ha` and `... at hb`": "", + "Start by unravelling the `1`.": "", + "Split into cases `c = 0` and `c = succ e` with `cases c with e`.": "", + "Solve this level in one line with `simp only [add_assoc, add_left_comm, add_comm]`": + "", + "See if you can take it from here. Look at the new lemmas and tactic\navailable on the right.": + "", + "Remember, `x ≠ y` is *notation* for `x = y → False`.": "", + "Remember that when Lean writes `a + b + c`, it means `(a + b) + c`.\nIf you are not sure where the brackets are in an expression, just hover\nyour cursor over it and look at what gets highlighted. For example,\nhover over both `+` symbols on the left hand side of the goal and\nyou'll see where the invisible brackets are.": + "", + "Remember that `h2` is a proof of `x = y → False`. Try\n`apply`ing `h2` either `at h1` or directly to the goal.": + "", + "Reduce to the previous lemma with `nth_rewrite 2 [← mul_one a] at h`": "", + "Precision rewriting": "", + "Power World": "", + "On the set of natural numbers, addition is commutative.\nIn other words, if `a` and `b` are arbitrary natural numbers, then\n$a + b = b + a$.": + "", + "On the set of natural numbers, addition is associative.\nIn other words, if $a, b$ and $c$ are arbitrary natural numbers, we have\n$ (a + b) + c = a + (b + c). $": + "", + "Numbers": "", + "Now you need to figure out which number to `use`. See if you can take it from here.": + "", + "Now you have two goals. Once you proved the first, you will jump to the second one.\nThis first goal is the base case $n = 0$.\n\nRecall that you can rewrite the proof of any lemma which is visible\nin your inventory, or of any assumption displayed above the goal,\nas long as it is of the form `X = Y`.": + "", + "Now you could finish with `rw [«{h}»]` then `rfl`, but `exact «{h}»`\ndoes it in one line.": + "", + "Now you can `rw [add_succ]`": "", + "Now you can `apply zero_ne_succ at h`.": "", + "Now you can `apply le_mul_right at h2`.": "", + "Now we can prove the `or` statement by proving the statement on the right,\nso use the `right` tactic.": + "", + "Now use `rw [add_left_comm b c]` to switch `b` and `c` on the left\nhand side.": + "", + "Now the goal can be deduced from `h2` by pure logic, so use the `tauto`\ntactic.": + "", + "Now take apart the existence statement with `cases ha with n hn`.": "", + "Now rewrite `succ_eq_add_one` backwards at `h`\nto get the right hand side.": + "", + "Now rewrite `four_eq_succ_three` backwards to make the goal\nequal to the hypothesis.": + "", + "Now let's `apply` our new theorem. Execute `apply succ_inj at h`\nto change `h` to a proof of `x = 3`.": + "", + "Now for to the second goal. Here you have the induction hypothesis\n`«{hd}» : 0 + «{d}» = «{d}»`, and you need to prove that `0 + succ «{d}» = succ «{d}»`.": + "", + "Now finish using the `exact` tactic.": "", + "Now finish the job with `rfl`.": "", + "Now finish in one line.": "", + "Now change `1` to `succ 0` in `h`.": "", + "Now `«{ha}»` is a proof that `«{y}» = «{x}» + «{a}»`, and `hxy` has vanished. Similarly, you can destruct\n`«{hyz}»` into its parts with `cases «{hyz}» with b hb`.": + "", + "Now `rw [← two_eq_succ_one]` will change `succ 1` into `2`.": "", + "Now `rw [h]` then `rfl` works, but `exact h` is quicker.": "", + "Now `rw [h] at h2` so you can `apply le_one at hx`.": "", + "Now `rw [add_zero]` will change `c + 0` into `c`.": "", + "Now `rfl` will work.": "", + "Now `repeat rw [← succ_eq_add_one] at h` is the quickest way to\nchange `succ x = succ y`.": + "", + "Now `exact h` finishes the job.": "", + "Now `cases «{h2}» with e he`.": "", + "Now `cases h2 with h0 h1` and deal with the two\ncases separately.": "", + "Now `apply succ_inj at h` to cancel the `succ`s.": "", + "Now `apply h` and you can probably take it from here.": "", + "Note: this lemma will be useful for the final boss!": "", + "Note that `succ a + «{d}»` means `(succ a) + «{d}»`. Put your cursor\non any `succ` in the goal or assumptions to see what exactly it's eating.": + "", + "Nice!": "", + "Next turn `1` into `succ 0` with `rw [one_eq_succ_zero]`.": "", + "Natural Number Game": "", + "My proof:\n```\ncases h with d hd\nuse d * t\nrw [hd, add_mul]\nrfl\n```\n": + "", + "Multiplication usually makes a number bigger, but multiplication by zero can make\nit smaller. Thus many lemmas about inequalities and multiplication need the\nhypothesis `a ≠ 0`. Here is a key lemma enables us to use this hypothesis.\nTo help us with the proof, we can use the `tauto` tactic. Click on the tactic's name\non the right to see what it does.\n": + "", + "Multiplication is distributive over addition on the left.\nIn other words, for all natural numbers $a$, $b$ and $c$, we have\n$a(b + c) = ab + ac$.": + "", + "Multiplication is commutative.": "", + "Multiplication is associative.\nIn other words, for all natural numbers $a$, $b$ and $c$, we have\n$(ab)c = a(bc)$.": + "", + "Multiplication distributes\nover addition on the left.\n\n`mul_add a b c` is the proof that `a * (b + c) = a * b + a * c`.": + "", + "Multiplication World": "", + "Mathematicians sometimes debate what `0 ^ 0` is;\nthe answer depends, of course, on your definitions. In this\ngame, `0 ^ 0 = 1`. See if you can prove it.\n\nCheck out the *Pow* tab in your list of theorems\nto see the new proofs which are available.": + "", + "Mathematicians sometimes argue that `0 ^ 0 = 0` is also\na good convention. But it is not a good convention in this\ngame; all the later levels come out beautifully with the\nconvention that `0 ^ 0 = 1`.": + "", + "Many people find `apply t at h` easy, but some find `apply t` confusing.\nIf you find it confusing, then just argue forwards.\n\nYou can read more about the `apply` tactic in its documentation, which you can view by\nclicking on the tactic in the list on the right.": + "", + "Let's warm up with an easy one, which works even if `t = 0`.": "", + "Let's now begin our approach to the final boss,\nby proving some more subtle facts about powers.": + "", + "Let's first get `h` into the form `succ x = succ 3` so we can\napply `succ_inj`. First execute `rw [four_eq_succ_three] at h`\nto change the 4 on the right hand side.": + "", + "Induction on `a` will not work here. You are still stuck with an `+ b`.\nI suggest you delete this line and try a different approach.": + "", + "Induction on `a` or `b` -- it's all the same in this one.": "", + "Induction on `a` is the most troublesome, then `b`,\nand `c` is the easiest.": + "", + "In this world I will mostly leave you on your own.\n\n`add_right_cancel a b n` is the theorem that $a+n=b+n\\implies a=b$.\n": + "", + "In this game you recreate the natural numbers $\\mathbb{N}$ from the Peano axioms,\nlearning the basics about theorem proving in Lean.\n\nThis is a good first introduction to Lean!": + "", + "In the next level, we'll do the same proof but backwards.": "", + "In the \"base case\" we have a hypothesis `ha : 0 ≠ 0`, and you can deduce anything\nfrom a false statement. The `tauto` tactic will close this goal.": + "", + "In order to use the tactic `rfl` you can enter it in the text box\nunder the goal and hit \"Execute\".": + "", + "Implication World": "", + "If you have completed Algorithm World then you can use the `contrapose!` tactic\nhere. If not then I'll talk you through a manual approach.": + "", + "If you `use` the wrong number, you get stuck with a goal you can't prove.\nWhat number will you `use` here?": + "", + "If the goal is not *exactly* a hypothesis, we can sometimes\nuse rewrites to fix things up.": + "", + "If $x=y$ and $x \\neq y$ then we can deduce a contradiction.": "", + "If $x=37$ or $y=42$, then $y=42$ or $x=37$.": "", + "If $x=37$ and we know that $x=37\\implies y=42$ then we can deduce $y=42$.": + "", + "If $x+1=4$ then $x=3$.": "", + "If $x$ is a number, then $x \\le x$.": "", + "If $x$ is a number, then $x \\le \\operatorname{succ}(x)$.": "", + "If $x$ is a number, then $0 \\le x$.": "", + "If $x$ and $y$ are numbers, then either $x \\leq y$ or $y \\leq x$.": "", + "If $x$ and $y$ are natural numbers, and $y = x + 7$, then $2y = 2(x + 7)$.": + "", + "If $x$ and $q$ are arbitrary natural numbers, then $37x+q=37x+q.$": "", + "If $x \\leq y$ and $y \\leq z$, then $x \\leq z$.": "", + "If $x \\leq y$ and $y \\leq x$, then $x = y$.": "", + "If $x \\leq 2$ then $x = 0$ or $1$ or $2$.": "", + "If $x \\leq 1$ then either $x = 0$ or $x = 1$.": "", + "If $x \\leq 0$, then $x=0$.": "", + "If $a, b,\\ldots h$ are arbitrary natural numbers, we have\n$(d + f) + (h + (a + c)) + (g + e + b) = a + b + c + d + e + f + g + h$.": + "", + "If $a, b, c$ are numbers, then $a+(b+c)=b+(a+c)$.": "", + "If $a, b$, $c$ and $d$ are numbers, we have\n$(a + b) + (c + d) = ((a + c) + d) + b.$": + "", + "If $a, b$ and $c$ are arbitrary natural numbers, we have\n$(a + b) + c = (a + c) + b$.": + "", + "If $a+b=0$ then $b=0$.": "", + "If $a+b=0$ then $a=0$.": "", + "If $a \\neq b$ then $\\operatorname{succ}(a) \\neq\\operatorname{succ}(b)$.": + "", + "If $\\operatorname{succ}(x) \\leq \\operatorname{succ}(y)$ then $x \\leq y$.": + "", + "If $\\operatorname{succ}(a)=\\operatorname{succ}(b)$ then $a=b$.": "", + "How about this for a proof:\n```\nrepeat rw [add_comm n]\nexact add_right_cancel a b n\n```\n": + "", + "How about this for a proof:\n\n```\nrw [add_comm]\nexact add_right_eq_zero b a\n```\n\nThat's the end of Advanced Addition World! You'll need these theorems\nfor the next world, `≤` World. Click on \"Leave World\" to access it.\n": + "", + "Here's what I was thinking of:\n```\napply mul_left_ne_zero at h\napply one_le_of_ne_zero at h\napply mul_le_mul_right 1 b a at h\nrw [one_mul, mul_comm] at h\nexact h\n```\n": + "", + "Here's my proof:\n```\nintro h\nrw [add_succ, add_succ, add_zero] at h\nrepeat apply succ_inj at h\napply zero_ne_succ at h\nexact h\n```\n\nEven though Lean is a theorem prover, right now it's pretty clear that we have not\ndeveloped enough material to make it an adequate calculator. In Algorithm\nWorld, a more computer-sciency world, we will develop machinery which makes\nquestions like this much easier, and goals like $20 + 20 ≠ 41$ feasible.\nAlternatively you can do more mathematics in Advanced Addition World, where we prove\nthe lemmas needed to get a working theory of inequalities. Click \"Leave World\" and\ndecide your route.": + "", + "Here's a two-line proof:\n```\nrepeat rw [zero_add] at h\nexact h\n```\n": "", + "Here's a proof using `add_left_eq_self`:\n```\nrw [add_comm]\nintro h\napply add_left_eq_self at h\nexact h\n```\n\nand here's an even shorter one using the same idea:\n```\nrw [add_comm]\nexact add_left_eq_self y x\n```\n\nAlternatively you can just prove it by induction on `x`\n(the dots in the proof just indicate the two goals and\ncan be omitted):\n\n```\n induction x with d hd\n · intro h\n rw [zero_add] at h\n assumption\n · intro h\n rw [succ_add] at h\n apply succ_inj at h\n apply hd at h\n assumption\n```\n": + "", + "Here's a completely backwards proof:\n```\nintro h\napply succ_inj\nrepeat rw [succ_eq_add_one]\nexact h\n```\n": + "", + "Here we want to deal with the cases `b = 0` and `b ≠ 0` separately,\nso start with `cases b with d`.": + "", + "Having to rearrange variables manually using commutativity and\nassociativity is very tedious. We start by reminding you of this. `add_left_comm`\nis a key component in the first algorithm which we'll explain, but we need\nto prove it manually.\n\nRemember that you can do precision commutativity rewriting\nwith things like `rw [add_comm b c]`. And remember that\n`a + b + c` means `(a + b) + c`.\n": + "", + "For any natural number $m$, we have $ m \\times 1 = m$.": "", + "For any natural number $m$, we have $ 2 \\times m = m+m$.": "", + "For any natural number $m$, we have $ 1 \\times m = m$.": "", + "For all numbers $m$, $0 ^{\\operatorname{succ} (m)} = 0$.": "", + "For all numbers $a$ and $b$, we have\n$$(a+b)^2=a^2+b^2+2ab.$$": "", + "For all naturals $m$, $1 ^ m = 1$.": "", + "For all naturals $a$, $m$, $n$, we have $a^{m + n} = a ^ m a ^ n$.": "", + "For all naturals $a$, $m$, $n$, we have $(a ^ m) ^ n = a ^ {mn}$.": "", + "For all naturals $a$, $b$, $n$, we have $(ab) ^ n = a ^ nb ^ n$.": "", + "For all naturals $a$, $a ^ 2 = a \\times a$.": "", + "For all naturals $a$, $a ^ 1 = a$.": "", + "For all naturals $a$ $b$ $c$ and $n$, we have\n$$(a+1)^{n+3}+(b+1)^{n+3}\\not=(c+1)^{n+3}.$$": + "", + "For all natural numbers $n$, we have $0 + n = n$.": "", + "For all natural numbers $m$, we have $ 0 \\times m = 0$.": "", + "For all natural numbers $a, b$, we have\n$ \\operatorname{succ}(a) + b = \\operatorname{succ}(a + b)$.": + "", + "For all natural numbers $a$, we have $\\operatorname{succ}(a) = a+1$.": "", + "For all natural numbers $a$ and $b$, we have\n$(\\operatorname{succ}\\ a) \\times b = a\\times b + b$.": + "", + "First execute `rw [h]` to replace the `y` with `x + 7`.": "", + "Finally use a targetted `add_comm` to switch `b` and `d`": "", + "Fermat's Last Theorem": "", + "Do that again!\n\n`rw [zero_add] at «{h}»` tries to fill in\nthe arguments to `zero_add` (finding `«{x}»`) then it replaces all occurences of\n`0 + «{x}»` it finds. Therefor, it did not rewrite `0 + «{y}»`, yet.": + "", + "Did you use induction on `y`?\nHere's a two-line proof of `add_left_eq_self` which uses `add_right_cancel`.\nIf you want to inspect it, you can go into editor mode by clicking `` in the top right\nand then just cut and paste the proof and move your cursor around it\nto see the hypotheses and goal at any given point\n(although you'll lose your own proof this way). Click `>_` to get\nback to command line mode.\n```\nnth_rewrite 2 [← zero_add y]\nexact add_right_cancel x 0 y\n```\n": + "", + "Dealing with `or`": "", + "Congratulations! You've finished Algorithm World. These algorithms\nwill be helpful for you in Even-Odd World.": + "", + "Concretely: `rw [← succ_eq_add_one] at h`.": "", + "Can you take it from here? Click on \"Show more help!\" if you need a hint.": + "", + "Can you take it from here? (note: if you try `contrapose! h` again, it will\ntake you back to where you started!)": + "", + "Can you take it from here?": "", + "Can you now change the goal into `2 = 2`?": "", + "At this point you see the term `0 + «{d}»`, so you can use the\ninduction hypothesis with `rw [«{hd}»]`.": + "", + "Assuming $x+y=37$ and $3x+z=42$, we have $x+y=37$.": "", + "Assuming $0+x=(0+y)+2$, we have $x=y+2$.": "", + "Arguing backwards": "", + "Applying a proof of $P\\implies Q$ to the *goal* changes $Q$ to $P$.\nNow try `rw [succ_eq_add_one]` to make the goal more like the hypothesis.": + "", + "And now we've deduced what we wanted to prove: the goal is one of our assumptions.\nFinish the level with `exact h`.": + "", + "And now `rw [add_zero]`": "", + "And finally `rfl`.": "", + "An algorithm for equality": "", + "Although $0^0=1$ in this game, $0^n=0$ if $n>0$, i.e., if\n$n$ is a successor.": + "", + "Algorithm World": "", + "Advanced Multiplication World": "", + "Advanced Addition World": "", + "Addition is distributive over multiplication.\nIn other words, for all natural numbers $a$, $b$ and $c$, we have\n$(a + b) \\times c = ac + bc$.": + "", + "Addition World": "", + "Adding zero": "", + "A proof that $a+b=0 \\implies b=0$.": "", + "A proof that $a+b=0 \\implies a=0$.": "", + "2+2=4": "", + "2 + 2 ≠ 5": "", + "1 ≠ 0": "", + "0 ≤ x": "", + "$x=37\\implies x=37$.": "", + "$x+y=x\\implies y=0$.": "", + "$x+1=y+1 \\implies x=y$.": "", + "$x + y = y\\implies x=0.$": "", + "$n+a=n+b\\implies a=b$.": "", + "$a+n=b+n\\implies a=b$.": "", + "$a+(b+0)+(c+0)=a+b+c.$": "", + "$\\operatorname{succ}(a) \\neq 0$.": "", + "$20+20=40$.": "", + "$2+2≠5$.": "", + "$2+2=4$.": "", + "$2+2 \\neq 5.$": "", + "$2$ is the number after the number after $0$.": "", + "$1\\neq0$.": "", + "$0\\neq1$.": "", + "$0 ^ 0 = 1$": "", + "## Summary\n\n`rfl` proves goals of the form `X = X`.\n\nIn other words, the `rfl` tactic will close any goal of the\nform `A = B` if `A` and `B` are *identical*.\n\n`rfl` is short for \\\"reflexivity (of equality)\\\".\n\n## Example:\n\nIf the goal looks like this:\n\n```\nx + 37 = x + 37\n```\n\nthen `rfl` will close it. But if it looks like `0 + x = x` then `rfl` won't work, because even\nthough $0+x$ and $x$ are always equal as *numbers*, they are not equal as *terms*.\nThe only term which is identical to `0 + x` is `0 + x`.\n\n## Details\n\n`rfl` is short for \\\"reflexivity of equality\\\".\n\n## Game Implementation\n\n*Note that our `rfl` is weaker than the version used in core Lean and `mathlib`,\nfor pedagogical purposes; mathematicians do not distinguish between propositional\nand definitional equality because they think about definitions in a different way\nto type theorists (`zero_add` and `add_zero` are both \\\"facts\\\" as far\nas mathematicians are concerned, and who cares what the definition of addition is).*": + "", + "## Summary\n\n`repeat t` repeatedly applies the tactic `t`\nto the goal. You don't need to use this\ntactic, it just speeds things up sometimes.\n\n## Example\n\n`repeat rw [add_zero]` will turn the goal\n`a + 0 + (0 + (0 + 0)) = b + 0 + 0`\ninto the goal\n`a = b`.\n\"\n\nTacticDoc nth_rewrite \"\n## Summary\n\nIf `h : X = Y` and there are several `X`s in the goal, then\n`nth_rewrite 3 [h]` will just change the third `X` to a `Y`.\n\n## Example\n\nIf the goal is `2 + 2 = 4` then `nth_rewrite 2 [two_eq_succ_one]`\nwill change the goal to `2 + succ 1 = 4`. In contrast, `rw [two_eq_succ_one]`\nwill change the goal to `succ 1 + succ 1 = 4`.": + "", + "## Summary\n\n`repeat t` repeatedly applies the tactic `t`\nto the goal. You don't need to use this\ntactic, it just speeds things up sometimes.\n\n## Example\n\n`repeat rw [add_zero]` will turn the goal\n`a + 0 + (0 + (0 + 0)) = b + 0 + 0`\ninto the goal\n`a = b`.": + "", + "## Summary\n\nThe `use` tactic makes progress with goals which claim something *exists*.\nIf the goal claims that some `x` exists with some property, and you know\nthat `x = 37` will work, then `use 37` will make progress.\n\nBecause `a ≤ b` is notation for \\\"there exists `c` such that `b = a + c`\\\",\nyou can make progress on goals of the form `a ≤ b` by `use`ing the\nnumber which is morally `b - a`.": + "", + "## Summary\n\nThe `symm` tactic will change a goal or hypothesis of\nthe form `X = Y` to `Y = X`. It will also work on `X ≠ Y`\nand on `X ↔ Y`.\n\n### Example\n\nIf the goal is `2 + 2 = 4` then `symm` will change it to `4 = 2 + 2`.\n\n### Example\n\nIf `h : 2 + 2 ≠ 5` then `symm at h` will change `h` to `5 ≠ 2 + 2`.": + "", + "## Summary\n\nIf the goal is a statement `P`, then `exact h` will close the goal if `h` is a proof of `P`.\n\n### Example\n\nIf the goal is `x = 37` and you have a hypothesis `h : x = 37`\nthen `exact h` will solve the goal.\n\n### Example\n\nIf the goal is `x + 0 = x` then `exact add_zero x` will close the goal.\n\n### Exact needs to be exactly right\n\nNote that `exact add_zero` will *not work* in the previous example;\nfor `exact h` to work, `h` has to be *exactly* a proof of the goal.\n`add_zero` is a proof of `∀ n, n + 0 = n` or, if you like,\na proof of `? + 0 = ?` where `?` needs to be supplied by the user.\nThis is in contrast to `rw` and `apply`, which will \\\"guess the inputs\\\"\nif necessary. If the goal is `x + 0 = x` then `rw [add_zero]`\nand `rw [add_zero x]` will both change the goal to `x = x`,\nbecause `rw` guesses the input to the function `add_zero`.": + "", + "## Summary\n\nIf the goal is `P → Q`, then `intro h` will introduce `h : P` as a hypothesis,\nand change the goal to `Q`. Mathematically, it says that to prove $P \\implies Q$,\nwe can assume $P$ and then prove $Q$.\n\n### Example:\n\nIf your goal is `x + 1 = y + 1 → x = y` (the way Lean writes $x+1=y+1 \\implies x=y$)\nthen `intro h` will give you a hypothesis $x+1=y+1$ named `h`, and the goal\nwill change to $x=y$.": + "", + "## Summary\n\nIf `t : P → Q` is a proof that $P \\implies Q$, and `h : P` is a proof of `P`,\nthen `apply t at h` will change `h` to a proof of `Q`. The idea is that if\nyou know `P` is true, then you can deduce from `t` that `Q` is true.\n\nIf the *goal* is `Q`, then `apply t` will \\\"argue backwards\\\" and change the\ngoal to `P`. The idea here is that if you want to prove `Q`, then by `t`\nit suffices to prove `P`, so you can reduce the goal to proving `P`.\n\n### Example:\n\n`succ_inj x y` is a proof that `succ x = succ y → x = y`.\n\nSo if you have a hypothesis `h : succ (a + 37) = succ (b + 42)`\nthen `apply succ_inj at h` will change `h` to `a + 37 = b + 42`.\nYou could write `apply succ_inj (a + 37) (b + 42) at h`\nbut Lean is smart enough to figure out the inputs to `succ_inj`.\n\n### Example\n\nIf the goal is `a * b = 7`, then `apply succ_inj` will turn the\ngoal into `succ (a * b) = succ 7`.": + "", + "## Summary\n\nIf `n` is a number, then `cases n with d` will break the goal into two goals,\none with `n = 0` and the other with `n = succ d`.\n\nIf `h` is a proof (for example a hypothesis), then `cases h with...` will break the\nproof up into the pieces used to prove it.\n\n## Example\n\nIf `n : ℕ` is a number, then `cases n with d` will break the goal into two goals,\none with `n` replaced by 0 and the other with `n` replaced by `succ d`. This\ncorresponds to the mathematical idea that every natural number is either `0`\nor a successor.\n\n## Example\n\nIf `h : P ∨ Q` is a hypothesis, then `cases h with hp hq` will turn one goal\ninto two goals, one with a hypothesis `hp : P` and the other with a\nhypothesis `hq : Q`.\n\n## Example\n\nIf `h : False` is a hypothesis, then `cases h` will turn one goal into no goals,\nbecause there are no ways to make a proof of `False`! And if you have no goals left,\nyou have finished the level.\n\n## Example\n\nIf `h : a ≤ b` is a hypothesis, then `cases h with c hc` will create a new number `c`\nand a proof `hc : b = a + c`. This is because the *definition* of `a ≤ b` is\n`∃ c, b = a + c`.": + "", + "## Summary\n\nIf `n : ℕ` is an object, and the goal mentions `n`, then `induction n with d hd`\nattempts to prove the goal by induction on `n`, with the inductive\nvariable in the successor case being `d`, and the inductive hypothesis being `hd`.\n\n### Example:\nIf the goal is\n```\n0 + n = n\n```\n\nthen\n\n`induction n with d hd`\n\nwill turn it into two goals. The first is `0 + 0 = 0`;\nthe second has an assumption `hd : 0 + d = d` and goal\n`0 + succ d = succ d`.\n\nNote that you must prove the first\ngoal before you can access the second one.": + "", + "## Summary\n\nIf `h` is a proof of an equality `X = Y`, then `rw [h]` will change\nall `X`s in the goal to `Y`s. It's the way to \\\"substitute in\\\".\n\n## Variants\n\n* `rw [← h]` (changes `Y`s to `X`s; get the back arrow by typing `\\left ` or `\\l`.)\n\n* `rw [h1, h2]` (a sequence of rewrites)\n\n* `rw [h] at h2` (changes `X`s to `Y`s in hypothesis `h2`)\n\n* `rw [h] at h1 h2 ⊢` (changes `X`s to `Y`s in two hypotheses and the goal;\nget the `⊢` symbol with `\\|-`.)\n\n* `repeat rw [add_zero]` will keep changing `? + 0` to `?`\nuntil there are no more matches for `? + 0`.\n\n* `nth_rewrite 2 [h]` will change only the second `X` in the goal to `Y`.\n\n### Example:\n\nIf you have the assumption `h : x = y + y` and your goal is\n```\nsucc (x + 0) = succ (y + y)\n```\n\nthen\n\n`rw [add_zero]`\n\nwill change the goal into `succ x = succ (y + y)`, and then\n\n`rw [h]`\n\nwill change the goal into `succ (y + y) = succ (y + y)`, which\ncan be solved with `rfl`.\n\n### Example:\n\nYou can use `rw` to change a hypothesis as well.\nFor example, if you have two hypotheses\n```\nh1 : x = y + 3\nh2 : 2 * y = x\n```\nthen `rw [h1] at h2` will turn `h2` into `h2 : 2 * y = y + 3`.\n\n## Common errors\n\n* You need the square brackets. `rw h` is never correct.\n\n* If `h` is not a *proof* of an *equality* (a statement of the form `A = B`),\nfor example if `h` is a function or an implication,\nthen `rw` is not the tactic you want to use. For example,\n`rw [P = Q]` is never correct: `P = Q` is the theorem *statement*,\nnot the proof. If `h : P = Q` is the proof, then `rw [h]` will work.\n\n## Details\n\nThe `rw` tactic is a way to do \\\"substituting in\\\". There\nare two distinct situations where you can use this tactic.\n\n1) Basic usage: if `h : A = B` is an assumption or\nthe proof of a theorem, and if the goal contains one or more `A`s, then `rw [h]`\nwill change them all to `B`'s. The tactic will error\nif there are no `A`s in the goal.\n\n2) Advanced usage: Assumptions coming from theorem proofs\noften have missing pieces. For example `add_zero`\nis a proof that `? + 0 = ?` because `add_zero` really is a function,\nand `?` is the input. In this situation `rw` will look through the goal\nfor any subterm of the form `x + 0`, and the moment it\nfinds one it fixes `?` to be `x` then changes all `x + 0`s to `x`s.\n\nExercise: think about why `rw [add_zero]` changes the term\n`(0 + 0) + (x + 0) + (0 + 0) + (x + 0)` to\n`0 + (x + 0) + 0 + (x + 0)`\n\nIf you can't remember the name of the proof of an equality, look it up in\nthe list of lemmas on the right.\n\n## Targetted usage\n\nIf your goal is `b + c + a = b + (a + c)` and you want to rewrite `a + c`\nto `c + a`, then `rw [add_comm]` will not work because Lean finds another\naddition first and swaps those inputs instead. Use `rw [add_comm a c]` to\nguarantee that Lean rewrites `a + c` to `c + a`. This works because\n`add_comm` is a proof that `?1 + ?2 = ?2 + ?1`, `add_comm a` is a proof\nthat `a + ? = ? + a`, and `add_comm a c` is a proof that `a + c = c + a`.\n\nIf `h : X = Y` then `rw [h]` will turn all `X`s into `Y`s.\nIf you only want to change the 37th occurrence of `X`\nto `Y` then do `nth_rewrite 37 [h]`.": + "", + "## Summary\n\nIf `h : X = Y` and there are several `X`s in the goal, then\n`nth_rewrite 3 [h]` will just change the third `X` to a `Y`.\n\n## Example\n\nIf the goal is `2 + 2 = 4` then `nth_rewrite 2 [two_eq_succ_one]`\nwill change the goal to `2 + succ 1 = 4`. In contrast, `rw [two_eq_succ_one]`\nwill change the goal to `succ 1 + succ 1 = 4`.": + "", + "# Summary\nThe `right` tactic changes a goal of `P ∨ Q` into a goal of `Q`.\nUse it when your hypotheses guarantee that the reason that `P ∨ Q`\nis true is because in fact `Q` is true.\n\nInternally this tactic is just `apply`ing a theorem\nsaying that $Q \\implies P \\lor Q.$\n\nNote that this tactic can turn a solvable goal into an unsolvable\none.": + "", + "# Summary\nThe `left` tactic changes a goal of `P ∨ Q` into a goal of `P`.\nUse it when your hypotheses guarantee that the reason that `P ∨ Q`\nis true is because in fact `P` is true.\n\nInternally this tactic is just `apply`ing a theorem\nsaying that $P \\implies P \\lor Q.$\n\nNote that this tactic can turn a solvable goal into an unsolvable\none.": + "", + "# Summary\n\n`triv` will solve the goal `True`.": "", + "# Summary\n\n`decide` will attempt to solve a goal if it can find an algorithm which it\ncan run to solve it.\n\n## Example\n\nA term of type `DecidableEq ℕ` is an algorithm to decide whether two naturals\nare equal or different. Hence, once this term is made and made into an `instance`,\nthe `decide` tactic can use it to solve goals of the form `a = b` or `a ≠ b`.": + "", + "# Summary\n\nThe `tauto` tactic will solve any goal which can be solved purely by logic (that is, by\ntruth tables).\n\n## Example\n\nIf you have `False` as a hypothesis, then `tauto` will solve\nthe goal. This is because a false hypothesis implies any hypothesis.\n\n## Example\n\nIf your goal is `True`, then `tauto` will solve the goal.\n\n## Example\n\nIf you have two hypotheses `h1 : a = 37` and `h2 : a ≠ 37` then `tauto` will\nsolve the goal because it can prove `False` from your hypotheses, and thus\nprove the goal (as `False` implies anything).\n\n## Example\n\nIf you have one hypothesis `h : a ≠ a` then `tauto` will solve the goal because\n`tauto` is smart enough to know that `a = a` is true, which gives the contradiction we seek.\n\n## Example\n\nIf you have a hypothesis of the form `a = 0 → a * b = 0` and your goal is `a * b ≠ 0 → a ≠ 0`, then\n`tauto` will solve the goal, because the goal is logically equivalent to the hypothesis.\nIf you switch the goal and hypothesis in this example, `tauto` would solve it too.": + "", + "# Summary\n\nThe `have` tactic can be used to add new hypotheses to a level, but of course\nyou have to prove them.\n\n\n## Example\n\nThe simplest usage is like this. If you have `a` in your context and you execute\n\n`have ha : a = 0`\n\nthen you will get a new goal `a = 0` to prove, and after you've proved\nit you will have a new hypothesis `ha : a = 0` in your original goal.\n\n## Example\n\nIf you already have a proof of what you want to `have`, you\ncan just create it immediately. For example, if you have `a` and `b`\nnumber objects, then\n\n`have h2 : succ a = succ b → a = b := succ_inj a b`\n\nwill directly add a new hypothesis `h2 : succ a = succ b → a = b`\nto the context, because you just supplied the proof of it (`succ_inj a b`).\n\n## Example\n\nIf you have a proof to hand, then you don't even need to state what you\nare proving. example\n\n`have h2 := succ_inj a b`\n\nwill add `h2 : succ a = succ b → a = b` as a hypothesis.": + "", + "# Summary\n\nIf you have a hypothesis\n\n`h : a ≠ b`\n\nand goal\n\n`c ≠ d`\n\nthen `contrapose! h` replaces the set-up with its so-called \\\"contrapositive\\\":\na hypothesis\n\n`h : c = d`\n\nand goal\n\n`a = b`.": + "", + "# Statement\n\nIf $a$ and $b$ are numbers, then\n`succ_inj a b` is the proof that\n$ (\\operatorname{succ}(a) = \\operatorname{succ}(b)) \\implies a=b$.\n\n## More technical details\n\nThere are other ways to think about `succ_inj`.\n\nYou can think about `succ_inj` itself as a function which takes two\nnumbers $$a$$ and $$b$$ as input, and outputs a proof of\n$ ( \\operatorname{succ}(a) = \\operatorname{succ}(b)) \\implies a=b$.\n\nYou can think of `succ_inj` itself as a proof; it is the proof\nthat `succ` is an injective function. In other words,\n`succ_inj` is a proof of\n$\\forall a, b \\in \\mathbb{N}, ( \\operatorname{succ}(a) = \\operatorname{succ}(b)) \\implies a=b$.\n\n`succ_inj` was postulated as an axiom by Peano, but\nin Lean it can be proved using `pred`, a mathematically\npathological function.": + "", + "# Overview\n\nOur home-made tactic `simp_add` will solve arbitrary goals of\nthe form `a + (b + c) + (d + e) = e + (d + (c + b)) + a`.": + "", + "# Overview\n\nLean's simplifier, `simp`, will rewrite every lemma\ntagged with `simp` and every lemma fed to it by the user, as much as it can.\nFurthermore, it will attempt to order variables into an internal order if fed\nlemmas such as `add_comm`, so that it does not go into an infinite loop.": + "", + " Let's see if you can use the tactics we've learnt to prove $x+1=y+1\\implies x=y$.\nTry this one by yourself; if you need help then click on \"Show more help!\".\n": + "", + " How should we define `37 * x`? Just like addition, we need to give definitions\nwhen $x=0$ and when $x$ is a successor.\n\nThe zero case is easy: we define `37 * 0` to be `0`. Now say we know\n`37 * d`. What should `37 * succ d` be? Well, that's $(d+1)$ $37$s,\nso it should be `37 * d + 37`.\n\nHere are the definitions in Lean.\n\n * `mul_zero a : a * 0 = 0`\n * `mul_succ a d : a * succ d = a * d + a`\n\nIn this world, we must not only prove facts about multiplication like `a * b = b * a`,\nwe must also prove facts about how multiplication interacts with addition, like `a * (b + c) = a * b + a * c`.\nLet's get started.\n": + "", + " Good luck!\n\n One last hint. If `h : X = Y` then `rw [h]` will change *all* `X`s into `Y`s.\n If you only want to change one of them, say the 3rd one, then use\n `nth_rewrite 3 [h]`.\n": + "", + " 2 + 2 ≠ 5 is boring to prove in full, given only the tools we have currently.\nTo make it a bit less painful, I have unfolded all of the numerals for you.\nSee if you can use `zero_ne_succ` and `succ_inj` to prove this.\n": + "", + "\n`add_mul` is just as fiddly to prove by induction; but there's a trick\nwhich avoids it. Can you spot it?\n": + "", + "\n`add_left_eq_self x y` is the theorem that $x + y = y\\implies x=0.$\n": "", + "\n`add_comm b c` is a proof that `b + c = c + b`. But if your goal\nis `a + b + c = a + c + b` then `rw [add_comm b c]` will not\nwork! Because the goal means `(a + b) + c = (a + c) + b` so there\nis no `b + c` term *directly* in the goal.\n\nUse associativity and commutativity to prove `add_right_comm`.\nYou don't need induction. `add_assoc` moves brackets around,\nand `add_comm` moves variables around.\n\nRemember that you can do more targetted rewrites by\nadding explicit variables as inputs to theorems. For example `rw [add_comm b]`\nwill only do rewrites of the form `b + ? = ? + b`, and `rw [add_comm b c]`\nwill only do rewrites of the form `b + c = c + b`.\n": + "", + "\n`a ≤ b` is *notation* for `∃ c, b = a + c`. This \"backwards E\"\nmeans \"there exists\". So `a ≤ b` means that there exists\na number `c` such that `b = a + c`. This definition works\nbecause there are no negative numbers in this game.\n\nTo *prove* an \"exists\" statement, use the `use` tactic.\nLet's see an example.\n": + "", + "\n[final boss music]\n": "", + "\n[boss battle music]\n\nLook in your inventory to see the proofs you have available.\nThese should be enough.\n": + "", + "\nYou've now seen all the tactics you need to beat the final boss of the game.\nYou can begin the journey towards this boss by entering Multiplication World.\n\nOr you can go off the beaten track and learn some new tactics in Implication\nWorld. These tactics let you prove more facts about addition, such as\nhow to deduce `a = 0` from `x + a = x`.\n\nClick \"Leave World\" and make your choice.\n": + "", + "\nYou can prove $1\\times m=m$ in at least three ways.\nEither by induction, or by using `succ_mul`, or\nby using commutativity. Which do you think is quickest?\n": + "", + "\nYou can make your own tactics in Lean.\nThis code here\n```\nmacro \"simp_add\" : tactic => `(tactic|(\n simp only [add_assoc, add_left_comm, add_comm]))\n```\nwas used to create a new tactic `simp_add`, which runs\n`simp only [add_assoc, add_left_comm, add_comm]`.\nTry running `simp_add` to solve this level!\n": + "", + "\nWhy did we not just define `succ n` to be `n + 1`? Because we have not\neven *defined* addition yet! We'll do that in the next level.\n": + "", + "\nWell done! You now have enough tools to tackle the main boss of this level.\n": + "", + "\nWelcome to Addition World! In this world we'll learn the `induction` tactic.\nThis will enable us to defeat the boss level of this world, namely `x + y = y + x`.\n\nThe tactics `rw`, `rfl` and `induction` are the only tactics you'll need to\nbeat all the levels in Addition World, Multiplication World, and Power World.\nPower World contains the final boss of the game.\n\nThere are plenty more tactics in this game, but you'll only need to know them if you\nwant to explore the game further (for example if you decide to 100%\nthe game).\n": + "", + "\nWe've seen `le_zero`, the proof that if `x ≤ 0` then `x = 0`.\nNow we'll prove that if `x ≤ 1` then `x = 0` or `x = 1`.\n": + "", + "\nWe've proved that `x ≤ 0` implies `x = 0`. The last two levels\nin this world will prove which numbers are `≤ 1` and `≤ 2`.\nThis lemma will be helpful for them.\n": + "", + "\nWe've proved that $2+2=4$; in Implication World we'll learn\nhow to prove $2+2\\neq 5$.\n\nIn Addition World we proved *equalities* like $x + y = y + x$.\nIn this second tutorial world we'll learn some new tactics,\nenabling us to prove *implications*\nlike $x+1=4 \\implies x=3.$\n\nWe'll also learn two new fundamental facts about\nnatural numbers, which Peano introduced as axioms.\n\nClick on \"Start\" to proceed.\n": + "", + "\nWe'll need this lemma to prove that two is prime!\n\nYou'll need to know that `∨` is right associative. This means that\n`x = 0 ∨ x = 1 ∨ x = 2` actually means `x = 0 ∨ (x = 1 ∨ x = 2)`.\nThis affects how `left` and `right` work.\n": + "", + "\nWe'd like to prove `2 + 2 = 4` but right now\nwe can't even *state* it\nbecause we haven't yet defined addition.\n\n## Defining addition.\n\nHow are we going to add $37$ to an arbitrary number $x$? Well,\nthere are only two ways to make numbers in this game: $0$\nand successors. So to define `37 + x` we will need\nto know what `37 + 0` is and what `37 + succ x` is.\nLet's start with adding `0`.\n\n### Adding 0\n\nTo make addition agree with our intuition, we should *define* `37 + 0`\nto be `37`. More generally, we should define `a + 0` to be `a` for\nany number `a`. The name of this proof in Lean is `add_zero a`.\nFor example `add_zero 37` is a proof of `37 + 0 = 37`,\n`add_zero x` is a proof of `x + 0 = x`, and `add_zero` is a proof\nof `? + 0 = ?`.\n\nWe write `add_zero x : x + 0 = x`, so `proof : statement`.\n": + "", + "\nWe now start work on an algorithm to do addition more efficiently. Recall that\nwe defined addition by recursion, saying what it did on `0` and successors.\nIt is an axiom of Lean that recursion is a valid\nway to define functions from types such as the naturals.\n\nLet's define a new function `pred` from the naturals to the naturals, which\nattempts to subtract 1 from the input. The definition is this:\n\n```\npred 0 := 37\npred (succ n) := n\n```\n\nWe cannot subtract one from 0, so we just return a junk value. As well as this\ndefinition, we also create a new lemma `pred_succ`, which says that `pred (succ n) = n`.\nLet's use this lemma to prove `succ_inj`, the theorem which\nPeano assumed as an axiom and which we have already used extensively without justification.\n": + "", + "\nWe now have enough to state a mathematically accurate, but slightly\nclunky, version of Fermat's Last Theorem.\n\nFermat's Last Theorem states that if $x,y,z>0$ and $m \\geq 3$ then $x^m+y^m\\not =z^m$.\nIf you didn't do inequality world yet then we can't talk about $m \\geq 3$,\nso we have to resort to the hack of using `n + 3` for `m`,\nwhich guarantees it's big enough. Similarly instead of `x > 0` we\nuse `a + 1`.\n\nThis level looks superficially like other levels we have seen,\nbut the shortest solution known to humans would translate into\nmany millions of lines of Lean code. The author of this game,\nKevin Buzzard, is working on translating the proof by Wiles\nand Taylor into Lean, although this task will take many years.\n\n## CONGRATULATIONS!\n\nYou've finished the main quest of the natural number game!\nIf you would like to learn more about how to use Lean to\nprove theorems in mathematics, then take a look\nat [Mathematics In Lean](https://leanprover-community.github.io/mathematics_in_lean/),\nan interactive textbook which you can read in your browser,\nand which explains how to work with many more mathematical concepts in Lean.\n": + "", + "\nWe now have enough to prove that multiplication is associative,\nthe boss level of multiplication world. Good luck!\n": + "", + "\nWe know `zero_ne_succ n` is a proof of `0 = succ n → False` -- but what\nif we have a hypothesis `succ n = 0`? It's the wrong way around!\n\nThe `symm` tactic changes a goal `x = y` to `y = x`, and a goal `x ≠ y`\nto `y ≠ x`. And `symm at h`\ndoes the same for a hypothesis `h`. We've proved $0 \\neq 1$ and called\nthe proof `zero_ne_one`; now try proving $1 \\neq 0$.\n": + "", + "\nWe gave a pretty unsatisfactory proof of `2 + 2 ≠ 5` earlier on; now give a nicer one.\n": + "", + "\nWe define a function `is_zero` thus:\n\n```\nis_zero 0 := True\nis_zero (succ n) := False\n```\n\nWe also create two lemmas, `is_zero_zero` and `is_zero_succ n`, saying that `is_zero 0 = True`\nand `is_zero (succ n) = False`. Let's use these lemmas to prove `succ_ne_zero`, Peano's\nLast Axiom. Actually, we have been using `zero_ne_succ` before, but it's handy to have\nthis opposite version too, which can be proved in the same way. Note: you can\ncheat here by using `zero_ne_succ` but the point of this world is to show\nyou how to *prove* results like that.\n\nIf you can turn your goal into `True`, then the `triv` tactic will solve it.\n": + "", + "\nVery well done.\n\nA passing mathematician remarks that with you've just proved that `ℕ` is totally\nordered.\n\nThe final few levels in this world are much easier.\n": + "", + "\nTotality of `≤` is the boss level of this world, and it's coming up next. It says that\nif `a` and `b` are naturals then either `a ≤ b` or `b ≤ a`.\nBut we haven't talked about `or` at all. Here's a run-through.\n\n1) The notation for \"or\" is `∨`. You won't need to type it, but you can\ntype it with `\\or`.\n\n2) If you have an \"or\" statement in the *goal*, then two tactics made\nprogress: `left` and `right`. But don't choose a direction unless your\nhypotheses guarantee that it's the correct one.\n\n3) If you have an \"or\" statement as a *hypothesis* `h`, then\n`cases h with h1 h2` will create two goals, one where you went left,\nand the other where you went right.\n": + "", + "\nTo solve this level, you need to `use` a number `c` such that `x = 0 + c`.\n": + "", + "\nThis world introduces exponentiation. If you want to define `37 ^ n`\nthen, as always, you will need to know what `37 ^ 0` is, and\nwhat `37 ^ (succ d)` is, given only `37 ^ d`.\n\nYou can probably guess the names of the general theorems:\n\n * `pow_zero (a : ℕ) : a ^ 0 = 1`\n * `pow_succ (a b : ℕ) : a ^ succ b = a ^ b * a`\n\nUsing only these, can you get past the final boss level?\n\nThe levels in this world were designed by Sian Carey, a UROP student\nat Imperial College London, funded by a Mary Lister McCammon Fellowship\nin the summer of 2019. Thanks to Sian and also thanks to Imperial\nCollege for funding her.\n": + "", + "\nThis level proves that if `a ≠ 0` and `b ≠ 0` then `a * b ≠ 0`. One strategy\nis to write both `a` and `b` as `succ` of something, deduce that `a * b` is\nalso `succ` of something, and then `apply zero_ne_succ`.\n": + "", + "\nThis level proves that if `a * b = 0` then `a = 0` or `b = 0`. It is\nlogically equivalent to the last level, so there is a very short proof.\n": + "", + "\nThis level proves `x * y = 1 → x = 1`, the multiplicative analogue of Advanced Addition\nWorld's `x + y = 0 → x = 0`. The strategy is to prove that `x ≤ 1` and then use the\nlemma `le_one` from `≤` world.\n\nWe'll prove it using a new and very useful tactic called `have`.\n": + "", + "\nThis level is more important than you think; it plays\na useful role when battling a big boss later on.\n": + "", + "\nThis level asks you to prove *antisymmetry* of $\\leq$.\nIn other words, if $x \\leq y$ and $y \\leq x$ then $x = y$.\nIt's the trickiest one so far. Good luck!\n": + "", + "\nThis is I think the toughest level yet. Tips: if `a` is a number\nthen `cases a with b` will split into cases `a = 0` and `a = succ b`.\nAnd don't go left or right until your hypotheses guarantee that\nyou can prove the resulting goal!\n\nI've left hidden hints; if you need them, retry from the beginning\nand click on \"Show more help!\"\n": + "", + "\nThe music gets ever more dramatic, as we explore\nthe interplay between exponentiation and multiplication.\n\nIf you're having trouble exchanging the right `x * y`\nbecause `rw [mul_comm]` swaps the wrong multiplication,\nthen read the documentation of `rw` for tips on how to fix this.\n": + "", + "\nThe music dies down. Is that it?\n\nCourse it isn't, you can\nclearly see that there are two worlds left.\n\nA passing mathematician says that mathematicians don't have a name\nfor the structure you just constructed. You feel cheated.\n\nSuddenly the music starts up again. This really is the final boss.\n": + "", + "\nThe first sub-boss of Multiplication World is `mul_comm x y : x * y = y * x`.\n\nWhen you've proved this theorem we will have \"spare\" proofs\nsuch as `zero_mul`, which is now easily deducible from `mul_zero`.\nBut we'll keep hold of these proofs anyway, because it's convenient\nto have exactly the right tool for a job.\n": + "", + "\nSo that's the algorithm: now let's use automation to perform it\nautomatically.\n": + "", + "\nSimilarly we have `mul_succ`\nbut we're going to need `succ_mul` (guess what it says -- maybe you\nare getting the hang of Lean's naming conventions).\n\nThe last level from addition world might help you in this level.\nIf you can't remember what it is, you can go back to the\nhome screen by clicking the house icon and then taking a look.\nYou won't lose any progress.\n": + "", + "\nReady for the boss level of this world?\n": "", + "\nProofs like $2+2=4$ and $a+b+c+d+e=e+d+c+b+a$ are very tedious to do by hand.\nIn Algorithm World we learn how to get the computer to do them for us.\n\nClick on \"Start\" to proceed.\n": + "", + "\nOur next goal is \"left and right distributivity\",\nmeaning $a(b+c)=ab+ac$ and $(b+c)a=ba+ca$. Rather than\nthese slightly pompous names, the name of the proofs\nin Lean are descriptive. Let's start with\n`mul_add a b c`, the proof of `a * (b + c) = a * b + a * c`.\nNote that the left hand side contains a multiplication\nand then an addition.\n": + "", + "\nOur first challenge is `mul_comm x y : x * y = y * x`,\nand we want to prove it by induction. The zero\ncase will need `mul_zero` (which we have)\nand `zero_mul` (which we don't), so let's\nstart with this.\n": + "", + "\nOne of the best named levels in the game, a savage `pow_pow`\nsub-boss appears as the music reaches a frenzy. What\nelse could there be to prove about powers after this?\n": + "", + "\nOh no! On the way to `add_comm`, a wild `succ_add` appears. `succ_add a b`\nis the proof that `(succ a) + b = succ (a + b)` for `a` and `b` numbers.\nThis result is what's standing in the way of `x + y = y + x`. Again\nwe have the problem that we are adding `b` to things, so we need\nto use induction to split into the cases where `b = 0` and `b` is a successor.\n": + "", + "\nNote that you can do `rw [two_eq_succ_one, one_eq_succ_zero]`\nand then `rfl` to solve this level in two lines.\n": + "", + "\nNice! You've proved `succ_inj`!\nLet's now prove Peano's other axiom, that successors can't be $0$.\n": + "", + "\nNice!\n\nThe next step in the development of order theory is to develop\nthe theory of the interplay between `≤` and multiplication.\nIf you've already done Multiplication World, you're now ready for\nAdvanced Multiplication World. Click on \"Leave World\" to access it.\n": + "", + "\nLet's now move on to a more efficient approach to questions\ninvolving numerals, such as `20 + 20 = 40`.\n": + "", + "\nLet's now make our own tactic to do this.\n": "", + "\nLet's now learn about Peano's second axiom for addition, `add_succ`.\n": "", + "\nLean's simplifier, `simp`, is \"`rw` on steroids\". It will rewrite every lemma\ntagged with `simp` and every lemma fed to it by the user, as much as it can.\n\nThis level is not a level which you want to solve by hand.\nGet the simplifier to solve it for you.\n": + "", + "\nIt's all over! You have proved a theorem which has tripped up\nschoolkids for generations (some of them think $(a+b)^2=a^2+b^2$:\nthis is \"the freshman's dream\").\n\nHow many rewrites did you use? I can do it in 12.\n\nBut wait! This boss is stirring...and mutating into a second more powerful form!\n": + "", + "\nIt's \"intuitively obvious\" that there are no numbers less than zero,\nbut to prove it you will need a result which you showed in advanced\naddition world.\n": + "", + "\nIn this world we'll learn how to prove theorems of the form $P\\implies Q$.\nIn other words, how to prove theorems of the form \"if $P$ is true, then $Q$ is true.\"\nTo do that we need to learn some more tactics.\n\nThe `exact` tactic can be used to close a goal which is exactly one of\nthe hypotheses.\n": + "", + "\nIn this world we define `a ≤ b` and prove standard facts\nabout it, such as \"if `a ≤ b` and `b ≤ c` then `a ≤ c`.\"\n\nThe definition of `a ≤ b` is \"there exists a number `c`\nsuch that `b = a + c`. \" So we're going to have to learn\na tactic to prove \"exists\" theorems, and another one\nto use \"exists\" hypotheses.\n\nClick on \"Start\" to proceed.\n": + "", + "\nIn this level, we see inequalities as *hypotheses*. We have not seen this before.\nThe `cases` tactic can be used to take `hxy` apart.\n": + "", + "\nIn this level we're going to prove that $0+n=n$, where $n$ is a secret natural number.\n\nWait, don't we already know that? No! We know that $n+0=n$, but that's `add_zero`.\nThis is `zero_add`, which is different.\n\nThe difficulty with proving `0 + n = n` is that we do not have a *formula* for\n`0 + n` in general, we can only use `add_zero` and `add_succ` once\nwe know whether `n` is `0` or a successor. The `induction` tactic splits into these two cases.\n\nThe base case will require us to prove `0 + 0 = 0`, and the inductive step\nwill ask us to show that if `0 + d = d` then `0 + succ d = succ d`. Because\n`0` and successor are the only way to make numbers, this will cover all the cases.\n\nSee if you can do your first induction proof in Lean.\n\n(By the way, if you are still in the \"Editor mode\" from the last world, you can swap\nback to \"Typewriter mode\" by clicking the `>_` button in the top right.)\n": + "", + "\nIn this level we prove that if `a * b = a * c` and `a ≠ 0` then `b = c`. It is tricky, for\nseveral reasons. One of these is that\nwe need to introduce a new idea: we will need to understand the concept of\nmathematical induction a little better.\n\nStarting with `induction b with d hd` is too naive, because in the inductive step\nthe hypothesis is `a * d = a * c → d = c` but what we know is `a * succ d = a * c`,\nso the induction hypothesis does not apply!\n\nAssume `a ≠ 0` is fixed. The actual statement we want to prove by induction on `b` is\n\"for all `c`, if `a * b = a * c` then `b = c`. This *can* be proved by induction,\nbecause we now have the flexibility to change `c`.\"\n": + "", + "\nIn this level the *goal* is $2y=2(x+7)$ but to help us we\nhave an *assumption* `h` saying that $y = x + 7$. Check that you can see `h` in\nyour list of assumptions. Lean thinks of `h` as being a secret proof of the\nassumption, rather like `x` is a secret number.\n\nBefore we can use `rfl`, we have to \"substitute in for $y$\".\nWe do this in Lean by *rewriting* the proof `h`,\nusing the `rw` tactic.\n": + "", + "\nIn this level one of our hypotheses is an *implication*. We can use this\nhypothesis with the `apply` tactic.\n": + "", + "\nIn some later worlds, we're going to see some much nastier levels,\nlike `(a + a + 1) + (b + b + 1) = (a + b + 1) + (a + b + 1)`.\nBrackets need to be moved around, and variables need to be swapped.\n\nIn this level, `(a + b) + (c + d) = ((a + c) + d) + b`,\nlet's forget about the brackets and just think about\nthe variable order.\nTo turn `a+b+c+d` into `a+c+d+b` we need to swap `b` and `c`,\nand then swap `b` and `d`. But this is easier than you\nthink with `add_left_comm`.\n": + "", + "\nIn Prime Number World we will be proving that $2$ is prime.\nTo do this, we will have to rule out things like $2 ≠ 37 × 42.$\nWe will do this by proving that any factor of $2$ is at most $2$,\nwhich we will do using this lemma. The proof I have in mind manipulates the hypothesis\nuntil it becomes the goal, using pretty much everything which we've proved in this world so far.\n": + "", + "\nIn Advanced Addition World we will prove some basic\naddition facts such as $x+y=x\\implies y=0$. The theorems\nproved in this world will be used to build\na theory of inequalities in `≤` World.\n\nClick on \"Start\" to proceed.\n": + "", + "\nImplementing the algorithm for equality of naturals, and the proof that it is correct,\nlooks like this:\n\n```\ninstance instDecidableEq : DecidableEq ℕ\n| 0, 0 => isTrue <| by\n show 0 = 0\n rfl\n| succ m, 0 => isFalse <| by\n show succ m ≠ 0\n exact succ_ne_zero m\n| 0, succ n => isFalse <| by\n show 0 ≠ succ n\n exact zero_ne_succ n\n| succ m, succ n =>\n match instDecidableEq m n with\n | isTrue (h : m = n) => isTrue <| by\n show succ m = succ n\n rw [h]\n rfl\n | isFalse (h : m ≠ n) => isFalse <| by\n show succ m ≠ succ n\n exact succ_ne_succ m n h\n```\n\nThis Lean code is a formally verified algorithm for deciding equality\nbetween two naturals. I've typed it in already, behind the scenes.\nBecause the algorithm is formally verified to be correct, we can\nuse it in Lean proofs. You can run the algorithm with the `decide` tactic.\n": + "", + "\nIf `h` is a proof of `X = Y` then `rw [h]` will\nturn `X`s into `Y`s. But what if we want to\nturn `Y`s into `X`s? To tell the `rw` tactic\nwe want this, we use a left arrow `←`. Type\n`\\l` and then hit the space bar to get this arrow.\n\nLet's prove that $2$ is the number after the number\nafter $0$ again, this time by changing `succ (succ 0)`\ninto `2`.\n": + "", + "\nIf `a` and `b` are numbers, then `succ_inj a b` is a proof\nthat `succ a = succ b` implies `a = b`. Click on this theorem in the *Peano*\ntab for more information.\n\nPeano had this theorem as an axiom, but in Algorithm World\nwe will show how to prove it in Lean. Right now let's just assume it,\nand let's prove $x+1=4 \\implies x=3$ using it. Again, we will proceed\nby manipulating our hypothesis until it becomes the goal. I will\nwalk you through this level.\n": + "", + "\nHere's my solution:\n```\nrw [two_eq_succ_one, succ_mul, one_mul]\nrfl\n```\n": + "", + "\nHere's my solution:\n```\nrw [mul_comm, mul_one]\nrfl\n```\n": "", + "\nHere's my solution:\n```\ninduction c with d hd\nrw [add_zero, mul_zero, add_zero]\nrfl\nrw [add_succ, mul_succ, hd, mul_succ, add_assoc]\nrfl\n```\n\nInducting on `a` or `b` also works, but might take longer.\n": + "", + "\nHere's my proof:\n```\nrw [mul_comm, mul_add]\nrepeat rw [mul_comm c]\nrfl\n```\n": + "", + "\nHere's my proof:\n```\ncases x with y\nleft\nrfl\nrw [one_eq_succ_zero] at hx ⊢\napply succ_le_succ at hx\napply le_zero at hx\nrw [hx]\nright\nrfl\n```\n\nIf you solved this level then you should be fine with the next level!\n": + "", + "\nHere's my proof:\n```\ncases hxy with a ha\ncases hyx with b hb\nrw [ha]\nrw [ha, add_assoc] at hb\nsymm at hb\napply add_right_eq_self at hb\napply add_right_eq_zero at hb\nrw [hb, add_zero]\nrfl\n```\n\nA passing mathematician remarks that with antisymmetry as well,\nyou have proved that `≤` is a *partial order* on `ℕ`.\n\nThe boss level of this world is to prove\nthat `≤` is a total order. Let's learn two more easy tactics\nfirst.\n": + "", + "\nHere's my proof:\n```\ncases hx with d hd\nuse d\nrw [succ_add] at hd\napply succ_inj at hd\nexact hd\n```\n": + "", + "\nHere's a two-liner:\n```\nuse 1\nexact succ_eq_add_one x\n```\n\nThis works because `succ_eq_add_one x` is a proof of `succ x = x + 1`.\n": + "", + "\nHere we begin to\ndevelop an algorithm which, given two naturals `a` and `b`, returns the answer\nto \"does `a = b`?\"\n\nHere is the algorithm. First note that `a` and `b` are numbers, and hence\nare either `0` or successors.\n\n*) If `a` and `b` are both `0`, return \"yes\".\n\n*) If one is `0` and the other is `succ n`, return \"no\".\n\n*) If `a = succ m` and `b = succ n`, then return the answer to \"does `m = n`?\"\n\nOur job now is to *prove* that this algorithm always gives the correct answer. The proof that\n`0 = 0` is `rfl`. The proof that `0 ≠ succ n` is `zero_ne_succ n`, and the proof\nthat `succ m ≠ 0` is `succ_ne_zero m`. The proof that if `h : m = n` then\n`succ m = succ n` is `rw [h]` and then `rfl`. This level is a proof of the one\nremaining job we have to do: if `a ≠ b` then `succ a ≠ succ b`.\n": + "", + "\nHere is an example proof of 2+2=4 showing off various techniques.\n\n```lean\nnth_rewrite 2 [two_eq_succ_one] -- only change the second `2` to `succ 1`.\nrw [add_succ]\nrw [one_eq_succ_zero]\nrw [add_succ, add_zero] -- two rewrites at once\nrw [← three_eq_succ_two] -- change `succ 2` to `3`\nrw [← four_eq_succ_three]\nrfl\n```\n\nOptional extra: you can run this proof yourself. Switch the game into \"Editor mode\" by clicking\non the `` button in the top right. You can now see your proof\nwritten as several lines of code. Move your cursor between lines to see\nthe goal state at any point. Now cut and paste your code elsewhere if you\nwant to save it, and paste the above proof in instead. Move your cursor\naround to investigate. When you've finished, click the `>_` button in the top right to\nmove back into \"Typewriter mode\".\n\nYou have finished tutorial world!\nClick \"Leave World\" to go back to the\noverworld, and select Addition World, where you will learn\nabout the `induction` tactic.\n": + "", + "\nEvery number in Lean is either $0$ or a successor. We know how to add $0$,\nbut we need to figure out how to add successors. Let's say we already know\nthat `37 + d = q`. What should the answer to `37 + succ d` be? Well,\n`succ d` is one bigger than `d`, so `37 + succ d` should be `succ q`,\nthe number one bigger than `q`. More generally `x + succ d` should\nbe `succ (x + d)`. Let's add this as a lemma.\n\n* `add_succ x d : x + succ d = succ (x + d)`\n\nIf you ever see `... + succ ...` in your goal, `rw [add_succ]` is\nnormally a good idea.\n\nLet's now prove that `succ n = n + 1`. Figure out how to get `+ succ` into\nthe picture, and then `rw [add_succ]`. Switch between the `+` (addition) and\n`012` (numerals) tabs under \"Theorems\" on the right to\nsee which proofs you can rewrite.\n": + "", + "\nCongratulations! You have proved Fermat's Last Theorem!\n\nEither that, or you used magic...\n": + "", + "\nCongratulations! You completed your first verified proof!\n\nRemember that `rfl` is a *tactic*. If you ever want information about the `rfl` tactic,\nyou can click on `rfl` in the list of tactics on the right.\n\nNow click on \"Next\" to learn about the `rw` tactic.\n": + "", + "\nAs warm-up for `2 + 2 ≠ 5` let's prove `0 ≠ 1`. To do this we need to\nintroduce Peano's last axiom `zero_ne_succ n`, a proof that `0 ≠ succ n`.\nTo learn about this result, click on it in the list of lemmas on the right.\n": + "", + "\nAdvanced *Addition* World proved various implications\ninvolving addition, such as `x + y = 0 → x = 0` and `x + y = x → y = 0`.\nThese lemmas were used to prove basic facts about ≤ in ≤ World.\n\nIn Advanced Multiplication World we prove analogous\nfacts about multiplication, such as `x * y = 1 → x = 1`, and\n`x * y = x → y = 1` (assuming `x ≠ 0` in the latter result). This will prepare\nus for Divisibility World.\n\nMultiplication World is more complex than Addition World. In the same\nway, Advanced Multiplication world is more complex than Advanced Addition\nWorld. One reason for this is that certain intermediate results are only\ntrue under the additional hypothesis that one of the variables is non-zero.\nThis causes some unexpected extra twists.\n": + "", + "\nA two-line proof is\n\n```\nnth_rewrite 2 [← mul_one a] at h\nexact mul_left_cancel a b 1 ha h\n```\n\nWe now have all the tools necessary to set up the basic theory of divisibility of naturals.\n": + "", + "\nA passing mathematician remarks that with reflexivity and transitivity out of the way,\nyou have proved that `≤` is a *preorder* on `ℕ`.\n": + "", + "\nA passing mathematician notes that you've proved\nthat the natural numbers are a commutative semiring.\n\nIf you want to begin your journey to the final boss, head for Power World.\n": + "", + "\nA passing mathematician congratulates you on proving that naturals\nare an additive commutative monoid.\n\nLet's practice using `add_assoc` and `add_comm` in one more level,\nbefore we leave addition world.\n": + "", + "\n*Game version: 4.2*\n\n*Recent additions: Inequality world, algorithm world*\n\n## Progress saving\n\nThe game stores your progress in your local browser storage.\nIf you delete it, your progress will be lost!\n\nWarning: In most browsers, deleting cookies will also clear the local storage\n(or \"local site data\"). Make sure to download your game progress first!\n\n## Credits\n\n* **Creators:** Kevin Buzzard, Jon Eugster\n* **Original Lean3-version:** Kevin Buzzard, Mohammad Pedramfar\n* **Game Engine:** Alexander Bentkamp, Jon Eugster, Patrick Massot\n* **Additional levels:** Sian Carey, Ivan Farabella, Archie Browne.\n* **Additional thanks:** All the student beta testers, all the schools\nwho invited Kevin to speak, and all the schoolkids who asked him questions\nabout the material.\n\n## Resources\n\n* The [Lean Zulip chat](https://leanprover.zulipchat.com/) forum\n* [Original Lean3 version](https://www.ma.imperial.ac.uk/~buzzard/xena/natural_number_game/) (no longer maintained)\n\n## Problems?\n\nPlease ask any questions about this game in the\n[Lean Zulip chat](https://leanprover.zulipchat.com/) forum, for example in\nthe stream \"New Members\". The community will happily help. Note that\nthe Lean Zulip chat is a professional research forum.\nPlease use your full real name there, stay on topic, and be nice. If you're\nlooking for somewhere less formal (e.g. you want to post natural number\ngame memes) then head on over to the [Lean Discord](https://discord.gg/WZ9bs9UCvx).\n\nAlternatively, if you experience issues / bugs you can also open github issues:\n\n* For issues with the game engine, please open an\n[issue at the lean4game](https://github.com/leanprover-community/lean4game/issues) repo.\n* For issues about the game's content, please open an\n[issue at the NNG](https://github.com/hhu-adam/NNG4/issues) repo.\n\n": + "", + "\n## The birth of number.\n\nNumbers in Lean are defined by two rules.\n\n* `0` is a number.\n* If `n` is a number, then the *successor* `succ n` of `n` is a number.\n\nThe successor of `n` means the number after `n`. Let's learn to\ncount, and name a few small numbers.\n\n## Counting to four.\n\n`0` is a number, so `succ 0` is a number. Let's call this new number `1`.\nSimilarly let's define `2 = succ 1`, `3 = succ 2` and `4 = succ 3`.\nThis gives us plenty of numbers to be getting along with.\n\nThe *proof* that `2 = succ 1` is called `two_eq_succ_one`.\nCheck out the \"012\" tab in the list of lemmas on the right\nfor this and other proofs.\n\nLet's prove that $2$ is the number after the number after zero.\n": + "", + "\n## Precision rewriting\n\nIn the last level, there was `b + 0` and `c + 0`,\nand `rw [add_zero]` changed the first one it saw,\nwhich was `b + 0`. Let's learn how to tell Lean\nto change `c + 0` first by giving `add_zero` an\nexplicit input.\n": + "", + "\n# Welcome to the Natural Number Game\n#### An introduction to mathematical proof.\n\nIn this game, we will build the basic theory of the natural\nnumbers `{0,1,2,3,4,...}` from scratch. Our first goal is to prove\nthat `2 + 2 = 4`. Next we'll prove that `x + y = y + x`.\nAnd at the end we'll see if we can prove Fermat's Last Theorem.\nWe'll do this by solving levels of a computer puzzle game called Lean.\n\n# Read this.\n\nLearning how to use an interactive theorem prover takes time.\nTests show that the people who get the most out of this game are\nthose who read the help texts like this one.\n\nTo start, click on \"Tutorial World\".\n\nNote: this is a new Lean 4 version of the game containing several\nworlds which were not present in the old Lean 3 version. A new version\nof Advanced Multiplication World is in preparation, and worlds\nsuch as Prime Number World and more will be appearing during October and\nNovember 2023.\n\n## More\n\nClick on the three lines in the top right and select \"Game Info\" for resources,\nlinks, and ways to interact with the Lean community.\n": + "", + "\n# Read this first\n\nEach level in this game involves proving a mathematical theorem (the \"Goal\").\nThe goal will be a statement about *numbers*. Some numbers in this game have known values.\nThose numbers have names like $37$. Other numbers will be secret. They're called things\nlike $x$ and $q$. We know $x$ is a number, we just don't know which one.\n\nIn this first level we're going to prove the theorem that $37x + q = 37x + q$.\nYou can see `x q : ℕ` in the *Objects* below, which means that `x` and `q`\nare numbers.\n\nWe solve goals in Lean using *Tactics*, and the first tactic we're\ngoing to learn is called `rfl`, which proves all theorems of the form $X = X$.\n\nProve that $37x+q=37x+q$ by executing the `rfl` tactic.\n": + "", + "\n We've been adding up two numbers; in this level we will add up three.\n\n What does $x+y+z$ *mean*? It could either mean $(x+y)+z$, or it\n could mean $x+(y+z)$. In Lean, $x+y+z$ means $(x+y)+z$.\n\n But why do we care which one it means; $(x+y)+z$ and $x+(y+z)$ are *equal*!\n\n That's true, but we didn't prove it yet. Let's prove it now by induction.\n": + "", + "\n This lemma would have been easy if we had known that `x + y = y + x`. That theorem\n is called `add_comm` and it is *true*, but unfortunately its proof *uses* both\n `add_zero` and `zero_add`!\n\n Let's continue on our journey to `add_comm`, the proof of `x + y = y + x`.\n": + "", + "\n In the last level, we manipulated the hypothesis `x + 1 = 4`\n until it became the goal `x = 3`. In this level we'll manipulate\n the goal until it becomes our hypothesis! In other words, we\n will \"argue backwards\". The `apply` tactic can do this too.\n Again I will walk you through this one (assuming you're in\n command line mode).\n": + "", + "\n\nSee the new \"*\" tab in your lemmas, containing `mul_zero` and `mul_succ`.\nRight now these are the only facts we know about multiplication.\nLet's prove nine more.\n\nLet's start with a warm-up: no induction needed for this one,\nbecause we know `1` is a successor.\n": + ""} \ No newline at end of file