msgid "" msgstr "Project-Id-Version: Game v4.21.0\n" "Report-Msgid-Bugs-To: \n" "POT-Creation-Date: 2025-08-09\n" "Last-Translator: \n" "Language-Team: none\n" "Language: en\n" "Content-Type: text/plain; charset=UTF-8\n" "Content-Transfer-Encoding: 8bit" #: Game.Levels.AdvAddition.L01add_right_cancel msgid "`add_right_cancel a b n` is the theorem that $a+n=b+n \\implies a=b.$" msgstr "" #: Game.Levels.LessOrEqual.L08le_total msgid "If $x$ and $y$ are numbers, then either $x \\leq y$ or $y \\leq x$." msgstr "" #: Game.Levels.LessOrEqual.L09succ_le_succ msgid "We've proved that `x ≤ 0` implies `x = 0`. The last two levels\n" "in this world will prove which numbers are `≤ 1` and `≤ 2`.\n" "This lemma will be helpful for them." msgstr "" #: Game.Levels.LessOrEqual.L10le_one msgid "x ≤ 1" msgstr "" #: Game.Levels.Algorithm.L08decide msgid "Implementing the algorithm for equality of naturals, and the proof that it is correct,\n" "looks like this:\n" "\n" "```\n" "instance 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" "\n" "This Lean code is a formally verified algorithm for deciding equality\n" "between two naturals. I've typed it in already, behind the scenes.\n" "Because the algorithm is formally verified to be correct, we can\n" "use it in Lean proofs. You can run the algorithm with the `decide` tactic." msgstr "" #: Game.Levels.Multiplication.L04mul_comm msgid "The first sub-boss of Multiplication World is `mul_comm x y : x * y = y * x`.\n" "\n" "When you've proved this theorem we will have \"spare\" proofs\n" "such as `zero_mul`, which is now easily deducible from `mul_zero`.\n" "But we'll keep hold of these proofs anyway, because it's convenient\n" "to have exactly the right tool for a job." msgstr "" #: Game.Levels.Multiplication.L09mul_assoc msgid "mul_assoc" msgstr "" #: Game.Levels.Tutorial.L07add_succ msgid "Every number in Lean is either $0$ or a successor. We know how to add $0$,\n" "but we need to figure out how to add successors. Let's say we already know\n" "that `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`,\n" "the number one bigger than `q`. More generally `x + succ d` should\n" "be `succ (x + d)`. Let's add this as a lemma.\n" "\n" "* `add_succ x d : x + succ d = succ (x + d)`\n" "\n" "If you ever see `... + succ ...` in your goal, `rw [add_succ]` is\n" "normally a good idea.\n" "\n" "Let's now prove that `succ n = n + 1`. Figure out how to get `+ succ` into\n" "the picture, and then `rw [add_succ]`. Switch between the `+` (addition) and\n" "`012` (numerals) tabs under \"Theorems\" on the right to\n" "see which proofs you can rewrite." msgstr "" #: Game.Levels.Algorithm.L03add_algo2 msgid "Lean's simplifier, `simp`, is \"`rw` on steroids\". It will rewrite every lemma\n" "tagged with `simp` and every lemma fed to it by the user, as much as it can.\n" "\n" "This level is not a level which you want to solve by hand.\n" "Get the simplifier to solve it for you." msgstr "" #: Game.Levels.Implication.L10one_ne_zero msgid "We know `zero_ne_succ n` is a proof of `0 = succ n → False` -- but what\n" "if we have a hypothesis `succ n = 0`? It's the wrong way around!\n" "\n" "The `symm` tactic changes a goal `x = y` to `y = x`, and a goal `x ≠ y`\n" "to `y ≠ x`. And `symm at h`\n" "does the same for a hypothesis `h`. We've proved $0 \\neq 1$ and called\n" "the proof `zero_ne_one`; now try proving $1 \\neq 0$." msgstr "" #: Game.Levels.Implication.L11two_add_two_ne_five msgid "Here's my proof:\n" "```\n" "intro h\n" "rw [add_succ, add_succ, add_zero] at h\n" "repeat apply succ_inj at h\n" "apply zero_ne_succ at h\n" "exact h\n" "```\n" "\n" "Even though Lean is a theorem prover, right now it's pretty clear that we have not\n" "developed enough material to make it an adequate calculator. In Algorithm\n" "World, a more computer-sciency world, we will develop machinery which makes\n" "questions like this much easier, and goals like $20 + 20 ≠ 41$ feasible.\n" "Alternatively you can do more mathematics in Advanced Addition World, where we prove\n" "the lemmas needed to get a working theory of inequalities. Click \"Leave World\" and\n" "decide your route." msgstr "" #: Game.Levels.Addition.L01zero_add msgid "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`." msgstr "" #: Game.Levels.AdvMultiplication.L10mul_right_eq_self msgid "`mul_right_eq_self a b` is a proof that if `a ≠ 0` and `a * b = a` then `b = 1`." msgstr "" #: Game.Levels.Power.L01zero_pow_zero msgid "$0 ^ 0 = 1$" msgstr "" #: Game.Levels.AdvMultiplication.L06mul_right_eq_one msgid "This level proves `x * y = 1 → x = 1`, the multiplicative analogue of Advanced Addition\n" "World's `x + y = 0 → x = 0`. The strategy is to prove that `x ≤ 1` and then use the\n" "lemma `le_one` from `≤` world.\n" "\n" "We'll prove it using a new and very useful tactic called `have`." msgstr "" #: Game.Levels.Tutorial.L02rw msgid "the rw tactic" msgstr "" #: Game.Levels.LessOrEqual.L01le_refl msgid "## Summary\n" "\n" "The `use` tactic makes progress with goals which claim something *exists*.\n" "If the goal claims that some `x` exists with some property, and you know\n" "that `x = 37` will work, then `use 37` will make progress.\n" "\n" "Because `a ≤ b` is notation for \\\"there exists `c` such that `b = a + c`\\\",\n" "you can make progress on goals of the form `a ≤ b` by `use`ing the\n" "number which is morally `b - a` (i.e. `use b - a`)\n" "\n" "Any of the following examples is possible assuming the type of the argument passed to the `use` function is accurate:\n" "\n" "- `use 37`\n" "- `use a`\n" "- `use a * a + 1`" msgstr "" #: Game.Levels.AdvMultiplication.L02mul_left_ne_zero msgid "mul_left_ne_zero" msgstr "" #: Game.Levels.Algorithm.L08decide msgid "You can read more about the `decide` tactic by clicking\n" "on it in the top right." msgstr "" #: Game.Levels.AdvMultiplication.L07mul_ne_zero msgid "mul_ne_zero" msgstr "" #: Game.Levels.LessOrEqual.L10le_one msgid "`le_one x` is a proof that if `x ≤ 1` then `x = 0` or `x = 1`." msgstr "" #: Game.Levels.AdvAddition.L02add_left_cancel msgid "add_left_cancel" msgstr "" #: Game.Levels.Tutorial.L08twoaddtwo msgid "2+2=4" msgstr "" #: Game.Levels.AdvMultiplication msgid "Advanced *Addition* World proved various implications\n" "involving addition, such as `x + y = 0 → x = 0` and `x + y = x → y = 0`.\n" "These lemmas were used to prove basic facts about ≤ in ≤ World.\n" "\n" "In Advanced Multiplication World we prove analogous\n" "facts 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\n" "us for Divisibility World.\n" "\n" "Multiplication World is more complex than Addition World. In the same\n" "way, Advanced Multiplication world is more complex than Advanced Addition\n" "World. One reason for this is that certain intermediate results are only\n" "true under the additional hypothesis that one of the variables is non-zero.\n" "This causes some unexpected extra twists." msgstr "" #: Game.Levels.Power.L01zero_pow_zero msgid "zero_pow_zero" msgstr "" #: Game.Levels.LessOrEqual.L05le_zero msgid "If $x \\leq 0$, then $x=0$." msgstr "" #: Game.Levels.Power.L05pow_two msgid "Note: this lemma will be useful for the final boss!" msgstr "" #: Game.Levels.Implication.L06intro msgid "intro" msgstr "" #: Game.Levels.Implication.L03apply msgid "## Summary\n" "\n" "If `t : P → Q` is a proof that $P \\implies Q$, and `h : P` is a proof of `P`,\n" "then `apply t at h` will change `h` to a proof of `Q`. The idea is that if\n" "you know `P` is true, then you can deduce from `t` that `Q` is true.\n" "\n" "If the *goal* is `Q`, then `apply t` will \\\"argue backwards\\\" and change the\n" "goal to `P`. The idea here is that if you want to prove `Q`, then by `t`\n" "it 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" "\n" "So if you have a hypothesis `h : succ (a + 37) = succ (b + 42)`\n" "then `apply succ_inj at h` will change `h` to `a + 37 = b + 42`.\n" "You could write `apply succ_inj (a + 37) (b + 42) at h`\n" "but Lean is smart enough to figure out the inputs to `succ_inj`.\n" "\n" "### Example\n" "\n" "If the goal is `a * b = 7`, then `apply succ_inj` will turn the\n" "goal into `succ (a * b) = succ 7`." msgstr "" #: Game.Levels.Multiplication.L09mul_assoc msgid "A passing mathematician notes that you've proved\n" "that the natural numbers are a commutative semiring.\n" "\n" "If you want to begin your journey to the final boss, head for Power World." msgstr "" #: Game.Levels.AdvMultiplication.L05le_mul_right msgid "One day this game will have a Prime Number World, with a final boss\n" "of proving that $2$ is prime.\n" "To do this, we will have to rule out things like $2 = 37 × 42.$\n" "We will do this by proving that any factor of $2$ is at most $2$,\n" "which we will do using this lemma. The proof I have in mind manipulates the hypothesis\n" "until it becomes the goal, using `mul_left_ne_zero`, `one_le_of_ne_zero` and\n" "`mul_le_mul_right`." msgstr "" #: Game.Levels.Power.L01zero_pow_zero msgid "`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" "\n" "Note in particular that `0 ^ 0 = 1`." msgstr "" #: Game.Levels.LessOrEqual.L03le_succ_self msgid "If you `use` the wrong number, you get stuck with a goal you can't prove.\n" "What number will you `use` here?" msgstr "" #: Game.Levels.AdvAddition msgid "In Advanced Addition World we will prove some basic\n" "addition facts such as $x+y=x\\implies y=0$. The theorems\n" "proved in this world will be used to build\n" "a theory of inequalities in `≤` World.\n" "\n" "Click on \"Start\" to proceed." msgstr "" #: Game.Levels.Tutorial.L03two_eq_ss0 msgid "`four_eq_succ_three` is a proof of `4 = succ 3`." msgstr "" #: Game.Levels.Addition.L01zero_add msgid "In this level we're going to prove that $0+n=n$, where $n$ is a secret natural number.\n" "\n" "Wait, don't we already know that? No! We know that $n+0=n$, but that's `add_zero`.\n" "This is `zero_add`, which is different.\n" "\n" "The 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\n" "we know whether `n` is `0` or a successor. The `induction` tactic splits into these two cases.\n" "\n" "The base case will require us to prove `0 + 0 = 0`, and the inductive step\n" "will 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" "\n" "See 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\n" "back to \"Typewriter mode\" by clicking the `>_` button in the top right.)" msgstr "" #: Game.Levels.Algorithm.L08decide msgid "decide" msgstr "" #: Game.Levels.Multiplication.L03succ_mul msgid "`succ_mul a b` is the proof that `succ a * b = a * b + b`.\n" "\n" "It could be deduced from `mul_succ` and `mul_comm`, however this argument\n" "would be circular because the proof of `mul_comm` uses `mul_succ`." msgstr "" #: Game.Levels.Algorithm.L09decide2 msgid "We gave a pretty unsatisfactory proof of `2 + 2 ≠ 5` earlier on; now give a nicer one." msgstr "" #: Game.Levels.Addition msgid "Addition World" msgstr "" #: Game.Levels.Algorithm.L05pred msgid "If $\\operatorname{succ}(a)=\\operatorname{succ}(b)$ then $a=b$." msgstr "" #: Game.Levels.Implication.L10one_ne_zero msgid "What do you think of this two-liner:\n" "```\n" "symm\n" "exact zero_ne_one\n" "```\n" "\n" "`exact` doesn't just take hypotheses, it will eat any proof which exists\n" "in the system." msgstr "" #: Game.Levels.Algorithm.L01add_left_comm msgid "add_left_comm" msgstr "" #: Game.Levels.Tutorial.L03two_eq_ss0 msgid "`one_eq_succ_zero` is a proof of `1 = succ 0`.\"" msgstr "" #: Game.Levels.Power.L02zero_pow_succ msgid "We've just seen that `0 ^ 0 = 1`, but if `n`\n" "is a successor, then `0 ^ n = 0`. We prove that here." msgstr "" #: Game.Levels.Power.L10FLT msgid "For all naturals $a$ $b$ $c$ and $n$, we have\n" "$$(a+1)^{n+3}+(b+1)^{n+3}\\not=(c+1)^{n+3}.$$" msgstr "" #: Game.Levels.Algorithm.L09decide2 msgid "Congratulations! You've finished Algorithm World. These algorithms\n" "will be helpful for you in Even-Odd World (when someone gets around to\n" "implementing it)." msgstr "" #: Game.Levels.Implication.L11two_add_two_ne_five msgid "2 + 2 ≠ 5 is boring to prove in full, given only the tools we have currently.\n" "To make it a bit less painful, I have unfolded all of the numerals for you.\n" "See if you can use `zero_ne_succ` and `succ_inj` to prove this." msgstr "" #: Game.Levels.Power.L06pow_add msgid "`pow_add a m n` is a proof that $a^{m+n}=a^ma^n.$" msgstr "" #: Game.Levels.Implication.L05succ_inj2 msgid "Arguing backwards" msgstr "" #: Game.Levels.AdvMultiplication.L01mul_le_mul_right msgid "My proof:\n" "```\n" "cases h with d hd\n" "use d * t\n" "rw [hd, add_mul]\n" "rfl\n" "```" msgstr "" #: Game.Levels.Multiplication.L09mul_assoc msgid "Multiplication is associative.\n" "In other words, for all natural numbers $a$, $b$ and $c$, we have\n" "$(ab)c = a(bc)$." msgstr "" #: Game.Levels.Tutorial.L05add_zero msgid "Those of you interested in speedrunning the game may want to know\n" "that `repeat rw [add_zero]` will do both rewrites at once." msgstr "" #: Game.Levels.AdvMultiplication.L06mul_right_eq_one msgid "mul_right_eq_one" msgstr "" #: Game.Levels.Addition.L04add_assoc msgid "A passing mathematician congratulates you on proving that naturals\n" "are an additive commutative monoid.\n" "\n" "Let's practice using `add_assoc` and `add_comm` in one more level,\n" "before we leave addition world." msgstr "" #: Game.Levels.Algorithm.L06is_zero msgid "`is_zero_succ a` is a proof of `is_zero (succ a) = False`." msgstr "" #: Game.Levels.AdvAddition.L06add_left_eq_zero msgid "A proof that $a+b=0 \\implies b=0$." msgstr "" #: Game.Levels.AdvAddition.L05add_right_eq_zero msgid "A proof that $a+b=0 \\implies a=0$." msgstr "" #: Game.Levels.LessOrEqual.L03le_succ_self msgid "`le_succ_self x` is a proof that `x ≤ succ x`." msgstr "" #: Game.Levels.Algorithm.L05pred msgid "`pred_succ n` is a proof of `pred (succ n) = n`." msgstr "" #: Game.Levels.Algorithm.L06is_zero msgid "`is_zero_zero` is a proof of `is_zero 0 = True`." msgstr "" #: Game.Levels.AdvAddition.L06add_left_eq_zero msgid "If $a+b=0$ then $b=0$." msgstr "" #: Game.Levels.Power.L01zero_pow_zero msgid "`pow_zero a : a ^ 0 = 1` is one of the two axioms\n" "defining exponentiation in this game." msgstr "" #: Game.Levels.Implication.L11two_add_two_ne_five msgid "$2+2≠5$." msgstr "" #: Game.Levels.LessOrEqual.L01le_refl msgid "If $x$ is a number, then $x \\le x$." msgstr "" #: Game.Levels.LessOrEqual.L02zero_le msgid "If $x$ is a number, then $0 \\le x$." msgstr "" #: Game.Levels.AdvAddition.L04add_right_eq_self msgid "$x+y=x\\implies y=0$." msgstr "" #: Game.Levels.Power msgid "This world introduces exponentiation. If you want to define `37 ^ n`\n" "then, as always, you will need to know what `37 ^ 0` is, and\n" "what `37 ^ (succ d)` is, given only `37 ^ d`.\n" "\n" "You 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" "\n" "Using only these, can you get past the final boss level?\n" "\n" "The levels in this world were designed by Sian Carey, a UROP student\n" "at Imperial College London, funded by a Mary Lister McCammon Fellowship\n" "in the summer of 2019. Thanks to Sian and also thanks to Imperial\n" "College for funding her." msgstr "" #: Game.Levels.Algorithm.L06is_zero msgid "$\\operatorname{succ}(a) \\neq 0$." msgstr "" #: Game.Levels.Implication.L01exact msgid "Assuming $x+y=37$ and $3x+z=42$, we have $x+y=37$." msgstr "" #: Game.Levels.Algorithm.L01add_left_comm msgid "Having to rearrange variables manually using commutativity and\n" "associativity is very tedious. We start by reminding you of this. `add_left_comm`\n" "is a key component in the first algorithm which we'll explain, but we need\n" "to prove it manually.\n" "\n" "Remember that you can do precision commutativity rewriting\n" "with things like `rw [add_comm b c]`. And remember that\n" "`a + b + c` means `(a + b) + c`." msgstr "" #: Game.Levels.AdvMultiplication.L09mul_left_cancel msgid "`mul_left_cancel a b c` is a proof that if `a ≠ 0` and `a * b = a * c` then `b = c`." msgstr "" #: Game.Levels.Implication.L11two_add_two_ne_five msgid "2 + 2 ≠ 5" msgstr "" #: Game.Levels.Implication.L08ne msgid "If $x=y$ and $x \\neq y$ then we can deduce a contradiction." msgstr "" #: Game.Levels.Multiplication.L04mul_comm msgid "`mul_comm` is the proof that multiplication is commutative. More precisely,\n" "`mul_comm a b` is the proof that `a * b = b * a`." msgstr "" #: Game.Levels.LessOrEqual.L11le_two msgid "If $x \\leq 2$ then $x = 0$ or $1$ or $2$." msgstr "" #: Game.Levels.Power.L08pow_pow msgid "One of the best named levels in the game, a savage `pow_pow`\n" "sub-boss appears as the music reaches a frenzy. What\n" "else could there be to prove about powers after this?" msgstr "" #: Game.Levels.LessOrEqual.L06le_antisymm msgid "x ≤ y and y ≤ x implies x = y" msgstr "" #: Game.Levels.Multiplication.L01mul_one msgid "`mul_zero m` is the proof that `m * 0 = 0`." msgstr "" #: Game.Levels.Multiplication.L08add_mul msgid "Addition is distributive over multiplication.\n" "In other words, for all natural numbers $a$, $b$ and $c$, we have\n" "$(a + b) \\times c = ac + bc$." msgstr "" #: Game.Levels.Implication.L09zero_ne_succ msgid "`zero_ne_succ n` is the proof that `0 ≠ succ n`.\n" "\n" "In 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`.\n" "Here `False` is a generic false statement. This means that\n" "you can `apply zero_ne_succ at h` if `h` is a proof of `0 = succ n`." msgstr "" #: Game.Levels.Multiplication msgid "Multiplication World" msgstr "" #: Game.Levels.AdvMultiplication.L03eq_succ_of_ne_zero msgid "Multiplication usually makes a number bigger, but multiplication by zero can make\n" "it smaller. Thus many lemmas about inequalities and multiplication need the\n" "hypothesis `a ≠ 0`. Here is a key lemma that enables us to use this hypothesis.\n" "To help us with the proof, we can use the `tauto` tactic. Click on the tactic's name\n" "on the right to see what it does." msgstr "" #: Game.Levels.Power.L02zero_pow_succ msgid "Although $0^0=1$ in this game, $0^n=0$ if $n>0$, i.e., if\n" "$n$ is a successor." msgstr "" #: Game.Levels.LessOrEqual.L08le_total msgid "Very well done.\n" "\n" "A passing mathematician remarks that with you've just proved that `ℕ` is totally\n" "ordered.\n" "\n" "The final few levels in this world are much easier." msgstr "" #: Game.Levels.AdvMultiplication.L05le_mul_right msgid "Here's what I was thinking of:\n" "```\n" "apply mul_left_ne_zero at h\n" "apply one_le_of_ne_zero at h\n" "apply mul_le_mul_right 1 b a at h\n" "rw [one_mul, mul_comm] at h\n" "exact h\n" "```" msgstr "" #: Game.Levels.LessOrEqual.L10le_one msgid "We've seen `le_zero`, the proof that if `x ≤ 0` then `x = 0`.\n" "Now we'll prove that if `x ≤ 1` then `x = 0` or `x = 1`." msgstr "" #: Game.Levels.Power.L02zero_pow_succ msgid "`pow_succ a b : a ^ (succ b) = a ^ b * a` is one of the\n" "two axioms defining exponentiation in this game." msgstr "" #: Game.Levels.Implication.L07intro2 msgid "intro practice" msgstr "" #: Game.Levels.Implication.L10one_ne_zero msgid "## Summary\n" "\n" "The `symm` tactic will change a goal or hypothesis of\n" "the form `X = Y` to `Y = X`. It will also work on `X ≠ Y`\n" "and on `X ↔ Y`.\n" "\n" "### Example\n" "\n" "If the goal is `2 + 2 = 4` then `symm` will change it to `4 = 2 + 2`.\n" "\n" "### Example\n" "\n" "If `h : 2 + 2 ≠ 5` then `symm at h` will change `h` to `5 ≠ 2 + 2`." msgstr "" #: Game.Levels.Addition.L05add_right_comm msgid "`add_right_comm a b c` is a proof that `(a + b) + c = (a + c) + b`\n" "\n" "In Lean, `a + b + c` means `(a + b) + c`, so this result gets displayed\n" "as `a + b + c = a + c + b`." msgstr "" #: Game.Levels.Implication.L09zero_ne_succ msgid "zero_ne_succ" msgstr "" #: Game.Levels.LessOrEqual.L11le_two msgid "Nice!\n" "\n" "The next step in the development of order theory is to develop\n" "the theory of the interplay between `≤` and multiplication.\n" "If you've already done Multiplication World, you're now ready for\n" "Advanced Multiplication World. Click on \"Leave World\" to access it." msgstr "" #: Game.Levels.Algorithm.L05pred msgid "We now start work on an algorithm to do addition more efficiently. Recall that\n" "we defined addition by recursion, saying what it did on `0` and successors.\n" "It is an axiom of Lean that recursion is a valid\n" "way to define functions from types such as the naturals.\n" "\n" "Let's define a new function `pred` from the naturals to the naturals, which\n" "attempts to subtract 1 from the input. The definition is this:\n" "\n" "```\n" "pred 0 := 37\n" "pred (succ n) := n\n" "```\n" "\n" "We cannot subtract one from 0, so we just return a junk value. As well as this\n" "definition, we also create a new lemma `pred_succ`, which says that `pred (succ n) = n`.\n" "Let's use this lemma to prove `succ_inj`, the theorem which\n" "Peano assumed as an axiom and which we have already used extensively without justification." msgstr "" #: Game.Levels.Algorithm.L07succ_ne_succ msgid "`succ_ne_succ m n` is the proof that `m ≠ n → succ m ≠ succ n`." msgstr "" #: Game.Levels.AdvAddition.L02add_left_cancel msgid "`add_left_cancel a b n` is the theorem that $n+a=n+b \\implies a=b.$" msgstr "" #: Game.Levels.Tutorial.L07add_succ msgid "`add_succ a b` is the proof of `a + succ b = succ (a + b)`." msgstr "" #: Game.Levels.AdvMultiplication.L09mul_left_cancel msgid "In this level we prove that if `a * b = a * c` and `a ≠ 0` then `b = c`. It is tricky, for\n" "several reasons. One of these is that\n" "we need to introduce a new idea: we will need to understand the concept of\n" "mathematical induction a little better.\n" "\n" "Starting with `induction b with d hd` is too naive, because in the inductive step\n" "the hypothesis is `a * d = a * c → d = c` but what we know is `a * succ d = a * c`,\n" "so the induction hypothesis does not apply!\n" "\n" "Assume `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,\n" "because we now have the flexibility to change `c`." msgstr "" #: Game.Levels.Implication.L04succ_inj msgid "In the next level, we'll do the same proof but backwards." msgstr "" #: Game.Levels.Multiplication.L01mul_one msgid "`mul_succ a b` is the proof that `a * succ b = a * b + a`." msgstr "" #: Game.Levels.Power.L03pow_one msgid "For all naturals $a$, $a ^ 1 = a$." msgstr "" #: Game.Levels.Algorithm.L03add_algo2 msgid "# Overview\n" "\n" "Lean's simplifier, `simp`, will rewrite every lemma\n" "tagged with `simp` and every lemma fed to it by the user, as much as it can.\n" "Furthermore, it will attempt to order variables into an internal order if fed\n" "lemmas such as `add_comm`, so that it does not go into an infinite loop." msgstr "" #: Game.Levels.LessOrEqual.L05le_zero msgid "x ≤ 0 → x = 0" msgstr "" #: Game.Levels.AdvAddition msgid "Advanced Addition World" msgstr "" #: Game.Levels.Tutorial.L02rw msgid "You now know enough tactics to prove `2 + 2 = 4`! Let's begin the journey." msgstr "" #: Game.Levels.Algorithm.L08decide msgid "# Summary\n" "\n" "`decide` will attempt to solve a goal if it can find an algorithm which it\n" "can run to solve it.\n" "\n" "## Example\n" "\n" "A term of type `DecidableEq ℕ` is an algorithm to decide whether two naturals\n" "are equal or different. Hence, once this term is made and made into an `instance`,\n" "the `decide` tactic can use it to solve goals of the form `a = b` or `a ≠ b`." msgstr "" #: Game.Levels.AdvAddition.L02add_left_cancel msgid "$n+a=n+b\\implies a=b$." msgstr "" #: Game.Levels.Multiplication.L01mul_one msgid "For any natural number $m$, we have $ m \\times 1 = m$." msgstr "" #: Game.Levels.Algorithm.L03add_algo2 msgid "making life simple" msgstr "" #: Game.Levels.Addition.L04add_assoc msgid "add_assoc (associativity of addition)" msgstr "" #: Game.Levels.Algorithm.L09decide2 msgid "$2+2 \\neq 5.$" msgstr "" #: Game.Levels.Multiplication.L04mul_comm msgid "mul_comm" msgstr "" #: Game.Levels.Algorithm.L03add_algo2 #: Game.Levels.Algorithm.L04add_algo3 msgid "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$." msgstr "" #: Game.Levels.Tutorial.L04rw_backwards msgid "If `h` is a proof of `X = Y` then `rw [h]` will\n" "turn `X`s into `Y`s. But what if we want to\n" "turn `Y`s into `X`s? To tell the `rw` tactic\n" "we want this, we use a left arrow `←`. Type\n" "`\\l` and then hit the space bar to get this arrow.\n" "\n" "Let's prove that $2$ is the number after the number\n" "after $0$ again, this time by changing `succ (succ 0)`\n" "into `2`." msgstr "" #: Game.Levels.Power.L01zero_pow_zero msgid "Mathematicians sometimes argue that `0 ^ 0 = 0` is also\n" "a good convention. But it is not a good convention in this\n" "game; all the later levels come out beautifully with the\n" "convention that `0 ^ 0 = 1`." msgstr "" #: Game.Levels.AdvMultiplication.L07mul_ne_zero msgid "`mul_ne_zero a b` is a proof that if `a ≠ 0` and `b ≠ 0` then `a * b ≠ 0`." msgstr "" #: Game.Levels.Multiplication.L07mul_add msgid "Multiplication distributes\n" "over addition on the left.\n" "\n" "`mul_add a b c` is the proof that `a * (b + c) = a * b + a * c`." msgstr "" #: Game.Levels.AdvAddition.L01add_right_cancel msgid "add_right_cancel" msgstr "" #: Game.Levels.Power.L01zero_pow_zero msgid "Mathematicians sometimes debate what `0 ^ 0` is;\n" "the answer depends, of course, on your definitions. In this\n" "game, `0 ^ 0 = 1`. See if you can prove it.\n" "\n" "Check out the *Pow* tab in your list of theorems\n" "to see the new proofs which are available." msgstr "" #: Game.Levels.Addition.L01zero_add msgid "`zero_add x` is the proof of `0 + x = x`.\n" "\n" "`zero_add` is a `simp` lemma, because replacing `0 + x` by `x`\n" "is almost always what you want to do if you're simplifying an expression." msgstr "" #: Game.Levels.AdvAddition.L03add_left_eq_self msgid "add_left_eq_self" msgstr "" #: Game.Levels.Multiplication msgid "How should we define `37 * x`? Just like addition, we need to give definitions\n" "when $x=0$ and when $x$ is a successor.\n" "\n" "The 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,\n" "so it should be `37 * d + 37`.\n" "\n" "Here 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" "\n" "In this world, we must not only prove facts about multiplication like `a * b = b * a`,\n" "we must also prove facts about how multiplication interacts with addition, like `a * (b + c) = a * b + a * c`.\n" "Let's get started." msgstr "" #: Game.Levels.LessOrEqual.L06le_antisymm msgid "Here's my proof:\n" "```\n" "cases hxy with a ha\n" "cases hyx with b hb\n" "rw [ha]\n" "rw [ha, add_assoc] at hb\n" "symm at hb\n" "apply add_right_eq_self at hb\n" "apply add_right_eq_zero at hb\n" "rw [hb, add_zero]\n" "rfl\n" "```\n" "\n" "A passing mathematician remarks that with antisymmetry as well,\n" "you have proved that `≤` is a *partial order* on `ℕ`.\n" "\n" "The boss level of this world is to prove\n" "that `≤` is a total order. Let's learn two more easy tactics\n" "first." msgstr "" #: GameServer.RpcHandlers msgid "level completed with warnings… 🎭" msgstr "" #: Game.Levels.Addition.L02succ_add msgid "Oh no! On the way to `add_comm`, a wild `succ_add` appears. `succ_add a b`\n" "is the proof that `(succ a) + b = succ (a + b)` for `a` and `b` numbers.\n" "This result is what's standing in the way of `x + y = y + x`. Again\n" "we have the problem that we are adding `b` to things, so we need\n" "to use induction to split into the cases where `b = 0` and `b` is a successor." msgstr "" #: Game.Levels.Implication.L05succ_inj2 msgid "Many people find `apply t at h` easy, but some find `apply t` confusing.\n" "If you find it confusing, then just argue forwards.\n" "\n" "You can read more about the `apply` tactic in its documentation, which you can view by\n" "clicking on the tactic in the list on the right." msgstr "" #: Game.Levels.Implication.L10one_ne_zero msgid "`one_ne_zero` is a proof that `1 ≠ 0`." msgstr "" #: Game.Levels.Power.L06pow_add msgid "pow_add" msgstr "" #: Game.Levels.Tutorial.L01rfl msgid "The rfl tactic" msgstr "" #: Game.Levels.Multiplication.L06two_mul msgid "`two_mul m` is the proof that `2 * m = m + m`." msgstr "" #: Game.Levels.LessOrEqual.L07or_symm msgid "If $x=37$ or $y=42$, then $y=42$ or $x=37$." msgstr "" #: Game.Levels.Multiplication.L01mul_one msgid "`mul_one m` is the proof that `m * 1 = m`." msgstr "" #: Game.Levels.Implication.L01exact msgid "The `exact` tactic" msgstr "" #: Game.Levels.Addition.L01zero_add msgid "## Summary\n" "\n" "If `n : ℕ` is an object, and the goal mentions `n`, then `induction n with d hd`\n" "attempts to prove the goal by induction on `n`, with the inductive\n" "variable in the successor case being `d`, and the inductive hypothesis being `hd`.\n" "\n" "### Example:\n" "If the goal is\n" "```\n" "0 + n = n\n" "```\n" "\n" "then\n" "\n" "`induction n with d hd`\n" "\n" "will turn it into two goals. The first is `0 + 0 = 0`;\n" "the second has an assumption `hd : 0 + d = d` and goal\n" "`0 + succ d = succ d`.\n" "\n" "Note that you must prove the first\n" "goal before you can access the second one." msgstr "" #: Game.Levels.Addition.L02succ_add msgid "succ_add" msgstr "" #: Game.Levels.Tutorial msgid "Welcome to tutorial world! In this world we learn the basics\n" "of proving theorems. The boss level of this world\n" "is the theorem `2 + 2 = 4`.\n" "\n" "You prove theorems by solving puzzles using tools called *tactics*.\n" "The aim is to prove the theorem by applying tactics\n" "in the right order.\n" "\n" "Let's learn some basic tactics. Click on \"Start\" below\n" "to begin your quest." msgstr "" #: Game.Levels.Algorithm.L08decide msgid "$20+20=40$." msgstr "" #: Game.Levels.AdvMultiplication.L02mul_left_ne_zero msgid "If you have completed Algorithm World then you can use the `contrapose!` tactic\n" "here. If not then I'll talk you through a manual approach." msgstr "" #: Game.Levels.Multiplication.L03succ_mul msgid "Similarly we have `mul_succ`\n" "but we're going to need `succ_mul` (guess what it says -- maybe you\n" "are getting the hang of Lean's naming conventions).\n" "\n" "The last level from addition world might help you in this level.\n" "If you can't remember what it is, you can go back to the\n" "home screen by clicking the house icon and then taking a look.\n" "You won't lose any progress." msgstr "" #: Game.Levels.AdvAddition.L04add_right_eq_self msgid "`add_right_eq_self x y` is the theorem that $x + y = x \\implies y=0.$" msgstr "" #: Game msgid "*Game version: 4.3*\n" "\n" "*Recent additions: bug fixes*\n" "\n" "## Progress saving\n" "\n" "The game stores your progress in your local browser storage.\n" "If you delete it, your progress will be lost!\n" "\n" "Warning: 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\n" "who invited Kevin to speak, and all the schoolkids who asked him questions\n" "about 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" "\n" "Please ask any questions about this game in the\n" "[Lean Zulip chat](https://leanprover.zulipchat.com/) forum, for example in\n" "the stream \"New Members\". The community will happily help. Note that\n" "the Lean Zulip chat is a professional research forum.\n" "Please use your full real name there, stay on topic, and be nice. If you're\n" "looking for somewhere less formal (e.g. you want to post natural number\n" "game memes) then head on over to the [Lean Discord](https://discord.gg/WZ9bs9UCvx).\n" "\n" "Alternatively, 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." msgstr "" #: Game.Levels.Multiplication.L05one_mul msgid "`one_mul m` is the proof `1 * m = m`." msgstr "" #: Game.Levels.Tutorial.L07add_succ msgid "`succ_eq_add_one n` is the proof that `succ n = n + 1`." msgstr "" #: Game.Levels.Algorithm.L02add_algo1 msgid "If $a, b$, $c$ and $d$ are numbers, we have\n" "$(a + b) + (c + d) = ((a + c) + d) + b.$" msgstr "" #: Game.Levels.Implication msgid "We've proved that $2+2=4$; in Implication World we'll learn\n" "how to prove $2+2\\neq 5$.\n" "\n" "In Addition World we proved *equalities* like $x + y = y + x$.\n" "In this second tutorial world we'll learn some new tactics,\n" "enabling us to prove *implications*\n" "like $x+1=4 \\implies x=3.$\n" "\n" "We'll also learn two new fundamental facts about\n" "natural numbers, which Peano introduced as axioms.\n" "\n" "Click on \"Start\" to proceed." msgstr "" #: Game.Levels.AdvMultiplication.L09mul_left_cancel msgid "mul_left_cancel" msgstr "" #: Game.Levels.AdvAddition.L06add_left_eq_zero msgid "You can just mimic the previous proof to do this one -- or you can figure out a way\n" "of using it." msgstr "" #: Game.Levels.AdvAddition.L03add_left_eq_self msgid "$x + y = y\\implies x=0.$" msgstr "" #: Game.Levels.Addition.L01zero_add msgid "For all natural numbers $n$, we have $0 + n = n$." msgstr "" #: Game.Levels.AdvMultiplication.L10mul_right_eq_self msgid "The lemma proved in the final level of this world will be helpful\n" "in Divisibility World." msgstr "" #: Game.Levels.Implication.L02exact2 msgid "If the goal is not *exactly* a hypothesis, we can sometimes\n" "use rewrites to fix things up." msgstr "" #: Game.Levels.AdvAddition.L03add_left_eq_self msgid "`add_left_eq_self x y` is the theorem that $x + y = y \\implies x=0.$" msgstr "" #: Game.Levels.Implication.L08ne msgid "We still can't prove `2 + 2 ≠ 5` because we have not talked about the\n" "definition of `≠`. In Lean, `a ≠ b` is *notation* for `a = b → False`.\n" "Here `False` is a generic false proposition, and `→` is Lean's notation\n" "for \"implies\". In logic we learn\n" "that `True → False` is false, but `False → False` is true. Hence\n" "`X → False` is the logical opposite of `X`.\n" "\n" "Even though `a ≠ b` does not look like an implication,\n" "you 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!\n" "So if your goal is `False` then you had better hope that your hypotheses\n" "are contradictory, which they are in this level." msgstr "" #: Game.Levels.Multiplication.L07mul_add msgid "Here's my solution:\n" "```\n" "induction c with d hd\n" "rw [add_zero, mul_zero, add_zero]\n" "rfl\n" "rw [add_succ, mul_succ, hd, mul_succ, add_assoc]\n" "rfl\n" "```\n" "\n" "Inducting on `a` or `b` also works, but might take longer." msgstr "" #: Game.Levels.Implication msgid "Implication World" msgstr "" #: Game.Levels.Multiplication.L05one_mul msgid "You can prove $1\\times m=m$ in at least three ways.\n" "Either by induction, or by using `succ_mul`, or\n" "by using commutativity. Which do you think is quickest?" msgstr "" #: Game.Levels.Power.L07mul_pow msgid "`mul_pow a b n` is a proof that $(ab)^n=a^nb^n.$" msgstr "" #: Game.Levels.Addition.L04add_assoc msgid "`add_assoc a b c` is a proof\n" "that `(a + b) + c = a + (b + c)`. Note that in Lean `(a + b) + c` prints\n" "as `a + b + c`, because the notation for addition is defined to be left\n" "associative." msgstr "" #: Game.Levels.Power.L08pow_pow msgid "For all naturals $a$, $m$, $n$, we have $(a ^ m) ^ n = a ^ {mn}$." msgstr "" #: Game.Levels.Implication.L06intro msgid "$x=37\\implies x=37$." msgstr "" #: Game.Levels.Tutorial.L07add_succ msgid "[dramatic music]. Now are you ready to face the first boss of the game?" msgstr "" #: Game.Levels.Tutorial.L01rfl msgid "If $x$ and $q$ are arbitrary natural numbers, then $37x+q=37x+q.$" msgstr "" #: Game.Levels.Implication.L04succ_inj msgid "# Statement\n" "\n" "If $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" "\n" "There are other ways to think about `succ_inj`.\n" "\n" "You can think about `succ_inj` itself as a function which takes two\n" "numbers $$a$$ and $$b$$ as input, and outputs a proof of\n" "$ ( \\operatorname{succ}(a) = \\operatorname{succ}(b)) \\implies a=b$.\n" "\n" "You can think of `succ_inj` itself as a proof; it is the proof\n" "that `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\n" "in Lean it can be proved using `pred`, a mathematically\n" "pathological function." msgstr "" #: Game.Levels.AdvMultiplication.L08mul_eq_zero msgid "`mul_eq_zero a b` is a proof that if `a * b = 0` then `a = 0` or `b = 0`." msgstr "" #: Game.Levels.LessOrEqual.L08le_total msgid "x ≤ y or y ≤ x" msgstr "" #: Game.Levels.Algorithm.L06is_zero msgid "We define a function `is_zero` thus:\n" "\n" "```\n" "is_zero 0 := True\n" "is_zero (succ n) := False\n" "```\n" "\n" "We also create two lemmas, `is_zero_zero` and `is_zero_succ n`, saying that `is_zero 0 = True`\n" "and `is_zero (succ n) = False`. Let's use these lemmas to prove `succ_ne_zero`, Peano's\n" "Last Axiom. Actually, we have been using `zero_ne_succ` before, but it's handy to have\n" "this opposite version too, which can be proved in the same way. Note: you can\n" "cheat here by using `zero_ne_succ` but the point of this world is to show\n" "you how to *prove* results like that.\n" "\n" "If you can turn your goal into `True`, then the `trivial` tactic will solve it." msgstr "" #: Game.Levels.Tutorial.L03two_eq_ss0 msgid "`two_eq_succ_one` is a proof of `2 = succ 1`." msgstr "" #: Game.Levels.Multiplication.L02zero_mul msgid "For all natural numbers $m$, we have $ 0 \\times m = 0$." msgstr "" #: Game.Levels.Tutorial.L08twoaddtwo msgid "$2+2=4$." msgstr "" #: Game.Levels.Tutorial.L06add_zero2 msgid "## Precision rewriting\n" "\n" "In the last level, there was `b + 0` and `c + 0`,\n" "and `rw [add_zero]` changed the first one it saw,\n" "which was `b + 0`. Let's learn how to tell Lean\n" "to change `c + 0` first by giving `add_zero` an\n" "explicit input." msgstr "" #: Game.Levels.Addition.L05add_right_comm msgid "If $a, b$ and $c$ are arbitrary natural numbers, we have\n" "$(a + b) + c = (a + c) + b$." msgstr "" #: Game.Levels.Tutorial.L02rw msgid "## Summary\n" "\n" "If `h` is a proof of an equality `X = Y`, then `rw [h]` will change\n" "all `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;\n" "get the `⊢` symbol with `\\|-`.)\n" "\n" "* `repeat rw [add_zero]` will keep changing `? + 0` to `?`\n" "until 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" "\n" "If you have the assumption `h : x = y + y` and your goal is\n" "```\n" "succ (x + 0) = succ (y + y)\n" "```\n" "\n" "then\n" "\n" "`rw [add_zero]`\n" "\n" "will change the goal into `succ x = succ (y + y)`, and then\n" "\n" "`rw [h]`\n" "\n" "will change the goal into `succ (y + y) = succ (y + y)`, which\n" "can be solved with `rfl`.\n" "\n" "### Example:\n" "\n" "You can use `rw` to change a hypothesis as well.\n" "For example, if you have two hypotheses\n" "```\n" "h1 : x = y + 3\n" "h2 : 2 * y = x\n" "```\n" "then `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`),\n" "for example if `h` is a function or an implication,\n" "then `rw` is not the tactic you want to use. For example,\n" "`rw [P = Q]` is never correct: `P = Q` is the theorem *statement*,\n" "not the proof. If `h : P = Q` is the proof, then `rw [h]` will work.\n" "\n" "## Details\n" "\n" "The `rw` tactic is a way to do \\\"substituting in\\\". There\n" "are two distinct situations where you can use this tactic.\n" "\n" "1) Basic usage: if `h : A = B` is an assumption or\n" "the proof of a theorem, and if the goal contains one or more `A`s, then `rw [h]`\n" "will change them all to `B`s. The tactic will error\n" "if there are no `A`s in the goal.\n" "\n" "2) Advanced usage: Assumptions coming from theorem proofs\n" "often have missing pieces. For example `add_zero`\n" "is a proof that `? + 0 = ?` because `add_zero` really is a function,\n" "and `?` is the input. In this situation `rw` will look through the goal\n" "for any subterm of the form `x + 0`, and the moment it\n" "finds one it fixes `?` to be `x` then changes all `x + 0`s to `x`s.\n" "\n" "Exercise: 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" "\n" "If you can't remember the name of the proof of an equality, look it up in\n" "the list of lemmas on the right.\n" "\n" "## Targetted usage\n" "\n" "If your goal is `b + c + a = b + (a + c)` and you want to rewrite `a + c`\n" "to `c + a`, then `rw [add_comm]` will not work because Lean finds another\n" "addition first and swaps those inputs instead. Use `rw [add_comm a c]` to\n" "guarantee 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\n" "that `a + ? = ? + a`, and `add_comm a c` is a proof that `a + c = c + a`.\n" "\n" "If `h : X = Y` then `rw [h]` will turn all `X`s into `Y`s.\n" "If you only want to change the 37th occurrence of `X`\n" "to `Y` then do `nth_rewrite 37 [h]`." msgstr "" #: Game.Levels.Algorithm.L03add_algo2 msgid "Let's now make our own tactic to do this." msgstr "" #: Game.Levels.LessOrEqual.L07or_symm msgid "Dealing with `or`" msgstr "" #: Game.Levels.AdvAddition.L06add_left_eq_zero msgid "add_left_eq_zero" msgstr "" #: Game msgid "Natural Number Game" msgstr "" #: Game.Levels.Multiplication.L02zero_mul msgid "Our first challenge is `mul_comm x y : x * y = y * x`,\n" "and we want to prove it by induction. The zero\n" "case will need `mul_zero` (which we have)\n" "and `zero_mul` (which we don't), so let's\n" "start with this." msgstr "" #: Game.Levels.Algorithm.L07succ_ne_succ msgid "Here we begin to\n" "develop an algorithm which, given two naturals `a` and `b`, returns the answer\n" "to \"does `a = b`?\"\n" "\n" "Here is the algorithm. First note that `a` and `b` are numbers, and hence\n" "are 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" "\n" "Our 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\n" "that `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\n" "remaining job we have to do: if `a ≠ b` then `succ a ≠ succ b`." msgstr "" #: Game.Levels.Power.L09add_sq msgid "It's all over! You have proved a theorem which has tripped up\n" "schoolkids for generations (some of them think $(a+b)^2=a^2+b^2$:\n" "this is \"the freshman's dream\").\n" "\n" "How many rewrites did you use? I can do it in 12.\n" "\n" "But wait! This boss is stirring...and mutating into a second more powerful form!" msgstr "" #: Game.Levels.Tutorial.L03two_eq_ss0 msgid "Note that you can do `rw [two_eq_succ_one, one_eq_succ_zero]`\n" "and then `rfl` to solve this level in two lines." msgstr "" #: Game.Levels.Implication.L04succ_inj msgid "succ_inj : the successor function is injective" msgstr "" #: Game.Levels.LessOrEqual.L04le_trans msgid "If $x \\leq y$ and $y \\leq z$, then $x \\leq z$." msgstr "" #: Game.Levels.LessOrEqual.L07or_symm msgid "# Summary\n" "The `left` tactic changes a goal of `P ∨ Q` into a goal of `P`.\n" "Use it when your hypotheses guarantee that the reason that `P ∨ Q`\n" "is true is because in fact `P` is true.\n" "\n" "Internally this tactic is just `apply`ing a theorem\n" "saying that $P \\implies P \\lor Q.$\n" "\n" "Note that this tactic can turn a solvable goal into an unsolvable\n" "one." msgstr "" #: Game.Levels.AdvMultiplication.L03eq_succ_of_ne_zero msgid "# Summary\n" "\n" "The `tauto` tactic will solve any goal which can be solved purely by logic (that is, by\n" "truth tables).\n" "\n" "## Details\n" "\n" "`tauto` *does not do magic*! It doesn't know *anything* about addition or multiplication,\n" "it doesn't even know `add_zero`. The only things that `tauto` knows about numbers\n" "are firstly that `a = a` and secondly that `0 ≠ 1`, `0 ≠ 2`, `1 ≠ 2` and so on.\n" "What `tauto`'s strength is, is *logic*. If you have a hypothesis `x < 37`\n" "and another hypothesis `x < 37 → y + z = 42` and your goal is `y + z = 42` then `tauto` will\n" "solve this goal, because to solve that goal you don't need to know any facts\n" "about inequalities or addition, all you need to know is the rules of logic.\n" "\n" "## Example\n" "\n" "If you have `False` as a hypothesis, then `tauto` will solve\n" "the goal. This is because a false hypothesis implies any hypothesis.\n" "\n" "## Example\n" "\n" "If your goal is `True`, then `tauto` will solve the goal.\n" "\n" "## Example\n" "\n" "If you have two hypotheses `h1 : a = 37` and `h2 : a ≠ 37` then `tauto` will\n" "solve the goal because it can prove `False` from your hypotheses, and thus\n" "prove the goal (as `False` implies anything).\n" "\n" "## Example\n" "\n" "If 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" "\n" "If you have a hypothesis `h : 0 = 1` then `tauto` will solve the goal, because\n" "`tauto` knows `0 ≠ 1` and this is enough to prove `False`, which implies any goal.\n" "\n" "## Example\n" "\n" "If 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.\n" "If you switch the goal and hypothesis in this example, `tauto` would solve it too." msgstr "" #: Game.Levels.LessOrEqual.L01le_refl msgid "`le_refl x` is a proof of `x ≤ x`.\n" "\n" "The reason for the name is that this lemma is \"reflexivity of $\\le$\"" msgstr "" #: Game.Levels.LessOrEqual.L05le_zero msgid "`le_zero x` is a proof of the implication `x ≤ 0 → x = 0`." msgstr "" #: Game.Levels.Implication.L04succ_inj msgid "If `a` and `b` are numbers, then `succ_inj a b` is a proof\n" "that `succ a = succ b` implies `a = b`. Click on this theorem in the *Peano*\n" "tab for more information.\n" "\n" "Peano had this theorem as an axiom, but in Algorithm World\n" "we will show how to prove it in Lean. Right now let's just assume it,\n" "and let's prove $x+1=4 \\implies x=3$ using it. Again, we will proceed\n" "by manipulating our hypothesis until it becomes the goal. I will\n" "walk you through this level." msgstr "" #: Game.Levels.Algorithm.L02add_algo1 msgid "In some later worlds, we're going to see some much nastier levels,\n" "like `(a + a + 1) + (b + b + 1) = (a + b + 1) + (a + b + 1)`.\n" "Brackets need to be moved around, and variables need to be swapped.\n" "\n" "In this level, `(a + b) + (c + d) = ((a + c) + d) + b`,\n" "let's forget about the brackets and just think about\n" "the variable order.\n" "To turn `a+b+c+d` into `a+c+d+b` we need to swap `b` and `c`,\n" "and then swap `b` and `d`. But this is easier than you\n" "think with `add_left_comm`." msgstr "" #: Game.Levels.Power.L02zero_pow_succ msgid "For all numbers $m$, $0 ^{\\operatorname{succ} (m)} = 0$." msgstr "" #: Game.Levels.Multiplication.L08add_mul msgid "Here's my proof:\n" "```\n" "rw [mul_comm, mul_add]\n" "repeat rw [mul_comm c]\n" "rfl\n" "```" msgstr "" #: Game.Levels.Implication.L07intro2 msgid "Let's see if you can use the tactics we've learnt to prove $x+1=y+1\\implies x=y$.\n" "Try this one by yourself; if you need help then click on \"Show more help!\"." msgstr "" #: GameServer.RpcHandlers msgid "intermediate goal solved! 🎉" msgstr "" #: Game.Levels.LessOrEqual.L08le_total msgid "`le_total x y` is a proof that `x ≤ y` or `y ≤ x`." msgstr "" #: Game.Levels.Tutorial.L01rfl msgid "Congratulations! You completed your first verified proof!\n" "\n" "Remember that `rfl` is a *tactic*. If you ever want information about the `rfl` tactic,\n" "you can click on `rfl` in the list of tactics on the right.\n" "\n" "Now click on \"Next\" to learn about the `rw` tactic." msgstr "" #: Game.Levels.Power.L05pow_two msgid "`pow_two a` says that `a ^ 2 = a * a`." msgstr "" #: Game.Levels.Multiplication.L01mul_one msgid "See the new \"*\" tab in your lemmas, containing `mul_zero` and `mul_succ`.\n" "Right now these are the only facts we know about multiplication.\n" "Let's prove nine more.\n" "\n" "Let's start with a warm-up: no induction needed for this one,\n" "because we know `1` is a successor." msgstr "" #: Game.Levels.LessOrEqual.L04le_trans msgid "In this level, we see inequalities as *hypotheses*. We have not seen this before.\n" "The `cases` tactic can be used to take `hxy` apart." msgstr "" #: Game.Levels.Tutorial.L03two_eq_ss0 msgid "`ℕ` is the natural numbers, just called \\\"numbers\\\" in this game. It's\n" "defined 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 `ℕ`.\n" "It is distinct from the Lean natural numbers `Nat`, which should hopefully\n" "never leak into the natural number game.*" msgstr "" #: Game.Levels.Tutorial.L08twoaddtwo msgid "Here is an example proof of 2+2=4 showing off various techniques.\n" "\n" "```lean\n" "nth_rewrite 2 [two_eq_succ_one] -- only change the second `2` to `succ 1`.\n" "rw [add_succ]\n" "rw [one_eq_succ_zero]\n" "rw [add_succ, add_zero] -- two rewrites at once\n" "rw [← three_eq_succ_two] -- change `succ 2` to `3`\n" "rw [← four_eq_succ_three]\n" "rfl\n" "```\n" "\n" "Optional extra: you can run this proof yourself. Switch the game into \"Editor mode\" by clicking\n" "on the `` button in the top right. You can now see your proof\n" "written as several lines of code. Move your cursor between lines to see\n" "the goal state at any point. Now cut and paste your code elsewhere if you\n" "want to save it, and paste the above proof in instead. Move your cursor\n" "around to investigate. When you've finished, click the `>_` button in the top right to\n" "move back into \"Typewriter mode\".\n" "\n" "You have finished tutorial world!\n" "Click \"Leave World\" to go back to the\n" "overworld, and select Addition World, where you will learn\n" "about the `induction` tactic." msgstr "" #: Game.Levels.LessOrEqual.L10le_one msgid "Here's my proof:\n" "```\n" "cases x with y\n" "left\n" "rfl\n" "rw [one_eq_succ_zero] at hx ⊢\n" "apply succ_le_succ at hx\n" "apply le_zero at hx\n" "rw [hx]\n" "right\n" "rfl\n" "```\n" "\n" "If you solved this level then you should be fine with the next level!" msgstr "" #: Game.Levels.LessOrEqual.L04le_trans msgid "A passing mathematician remarks that with reflexivity and transitivity out of the way,\n" "you have proved that `≤` is a *preorder* on `ℕ`." msgstr "" #: Game.Levels.Algorithm.L04add_algo3 msgid "Let's now move on to a more efficient approach to questions\n" "involving numerals, such as `20 + 20 = 40`." msgstr "" #: Game.Levels.Tutorial.L02rw msgid "## Summary\n" "\n" "`repeat t` repeatedly applies the tactic `t`\n" "to the goal. You don't need to use this\n" "tactic, 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`\n" "into the goal\n" "`a = b`.\n" "\"\n" "\n" "TacticDoc nth_rewrite \"\n" "## Summary\n" "\n" "If `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" "\n" "If the goal is `2 + 2 = 4` then `nth_rewrite 2 [two_eq_succ_one]`\n" "will change the goal to `2 + succ 1 = 4`. In contrast, `rw [two_eq_succ_one]`\n" "will change the goal to `succ 1 + succ 1 = 4`." msgstr "" #: Game.Levels.Multiplication.L06two_mul msgid "Here's my solution:\n" "```\n" "rw [two_eq_succ_one, succ_mul, one_mul]\n" "rfl\n" "```" msgstr "" #: Game.Levels.Addition.L01zero_add msgid "zero_add" msgstr "" #: Game.Levels.AdvAddition.L05add_right_eq_zero msgid "## Summary\n" "\n" "If `n` is a number, then `cases n with d` will break the goal into two goals,\n" "one with `n = 0` and the other with `n = succ d`.\n" "\n" "If `h` is a proof (for example a hypothesis), then `cases h with...` will break the\n" "proof up into the pieces used to prove it.\n" "\n" "## Example\n" "\n" "If `n : ℕ` is a number, then `cases n with d` will break the goal into two goals,\n" "one with `n` replaced by 0 and the other with `n` replaced by `succ d`. This\n" "corresponds to the mathematical idea that every natural number is either `0`\n" "or a successor.\n" "\n" "## Example\n" "\n" "If `h : P ∨ Q` is a hypothesis, then `cases h with hp hq` will turn one goal\n" "into two goals, one with a hypothesis `hp : P` and the other with a\n" "hypothesis `hq : Q`.\n" "\n" "## Example\n" "\n" "If `h : False` is a hypothesis, then `cases h` will turn one goal into no goals,\n" "because there are no ways to make a proof of `False`! And if you have no goals left,\n" "you have finished the level.\n" "\n" "## Example\n" "\n" "If `h : a ≤ b` is a hypothesis, then `cases h with c hc` will create a new number `c`\n" "and a proof `hc : b = a + c`. This is because the *definition* of `a ≤ b` is\n" "`∃ c, b = a + c`." msgstr "" #: Game.Levels.LessOrEqual.L11le_two msgid "We'll need this lemma to prove that two is prime!\n" "\n" "You'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)`.\n" "This affects how `left` and `right` work." msgstr "" #: Game.Levels.Implication.L08ne msgid "Remember, `x ≠ y` is *notation* for `x = y → False`." msgstr "" #: Game.Levels.Addition msgid "Welcome to Addition World! In this world we'll learn the `induction` tactic.\n" "This will enable us to defeat the boss level of this world, namely `x + y = y + x`.\n" "\n" "The tactics `rw`, `rfl` and `induction` are the only tactics you'll need to\n" "beat all the levels in Addition World, Multiplication World, and Power World.\n" "Power World contains the final boss of the game.\n" "\n" "There are plenty more tactics in this game, but you'll only need to know them if you\n" "want to explore the game further (for example if you decide to 100%\n" "the game)." msgstr "" #: Game.Levels.Multiplication.L01mul_one msgid "mul_one" msgstr "" #: Game.Levels.Implication.L09zero_ne_succ msgid "As warm-up for `2 + 2 ≠ 5` let's prove `0 ≠ 1`. To do this we need to\n" "introduce Peano's last axiom `zero_ne_succ n`, a proof that `0 ≠ succ n`.\n" "To learn about this result, click on it in the list of lemmas on the right." msgstr "" #: Game.Levels.Addition.L02succ_add msgid "For all natural numbers $a, b$, we have\n" "$ \\operatorname{succ}(a) + b = \\operatorname{succ}(a + b)$." msgstr "" #: Game.Levels.LessOrEqual.L01le_refl msgid "The `use` tactic" msgstr "" #: Game.Levels.AdvMultiplication.L03eq_succ_of_ne_zero msgid "`eq_succ_of_ne_zero a` is a proof that `a ≠ 0 → ∃ n, a = succ n`." msgstr "" #: Game.Levels.Implication.L06intro msgid "## Summary\n" "\n" "If the goal is `P → Q`, then `intro h` will introduce `h : P` as a hypothesis,\n" "and change the goal to `Q`. Mathematically, it says that to prove $P \\implies Q$,\n" "we can assume $P$ and then prove $Q$.\n" "\n" "### Example:\n" "\n" "If your goal is `x + 1 = y + 1 → x = y` (the way Lean writes $x+1=y+1 \\implies x=y$)\n" "then `intro h` will give you a hypothesis $x+1=y+1$ named `h`, and the goal\n" "will change to $x=y$." msgstr "" #: Game.Levels.Addition.L03add_comm msgid "add_comm (level boss)" msgstr "" #: Game.Levels.LessOrEqual.L04le_trans msgid "`le_trans x y z` is a proof that if `x ≤ y` and `y ≤ z` then `x ≤ z`.\n" "More precisely, it is a proof that `x ≤ y → (y ≤ z → x ≤ z)`. In words,\n" "If $x \\le y$ then (pause) if $y \\le z$ then $x \\le z$.\n" "\n" "## A note on associativity\n" "\n" "In 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\n" "exactly 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$\n" "and $Q \\implies R$." msgstr "" #: Game.Levels.LessOrEqual.L09succ_le_succ msgid "If $\\operatorname{succ}(x) \\leq \\operatorname{succ}(y)$ then $x \\leq y$." msgstr "" #: Game.Levels.Tutorial.L05add_zero #: Game.Levels.Tutorial.L06add_zero2 msgid "$a+(b+0)+(c+0)=a+b+c.$" msgstr "" #: Game.Levels.Addition.L04add_assoc msgid "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." msgstr "" #: Game.Levels.Power.L10FLT msgid "We now have enough to state a mathematically accurate, but slightly\n" "clunky, version of Fermat's Last Theorem.\n" "\n" "Fermat's Last Theorem states that if $x,y,z>0$ and $m \\geq 3$ then $x^m+y^m\\not =z^m$.\n" "If you didn't do inequality world yet then we can't talk about $m \\geq 3$,\n" "so we have to resort to the hack of using `n + 3` for `m`,\n" "which guarantees it's big enough. Similarly instead of `x > 0` we\n" "use `a + 1`.\n" "\n" "This level looks superficially like other levels we have seen,\n" "but the shortest solution known to humans would translate into\n" "many millions of lines of Lean code. The author of this game,\n" "Kevin Buzzard, is working on translating the proof by Wiles\n" "and Taylor into Lean, although this task will take many years.\n" "\n" "## CONGRATULATIONS!\n" "\n" "You've finished the main quest of the natural number game!\n" "If you would like to learn more about how to use Lean to\n" "prove theorems in mathematics, then take a look\n" "at [Mathematics In Lean](https://leanprover-community.github.io/mathematics_in_lean/),\n" "an interactive textbook which you can read in your browser,\n" "and which explains how to work with many more mathematical concepts in Lean." msgstr "" #: Game.Levels.Multiplication.L09mul_assoc msgid "We now have enough to prove that multiplication is associative,\n" "the boss level of multiplication world. Good luck!" msgstr "" #: Game.Levels.AdvAddition.L04add_right_eq_self msgid "`add_right_eq_self x y` is the theorem that $x + y = x\\implies y=0.$\n" "Two ways to do it spring to mind; I'll mention them when you've solved it." msgstr "" #: Game.Levels.Implication.L03apply msgid "The `apply` tactic." msgstr "" #: Game.Levels.Power.L08pow_pow msgid "pow_pow" msgstr "" #: Game.Levels.Power.L09add_sq msgid "For all numbers $a$ and $b$, we have\n" "$$(a+b)^2=a^2+b^2+2ab.$$" msgstr "" #: Game.Levels.AdvAddition.L05add_right_eq_zero msgid "The next result we'll need in `≤` World is that if `a + b = 0` then `a = 0` and `b = 0`.\n" "Let's prove one of these facts in this level, and the other in the next.\n" "\n" "## A new tactic: `cases`\n" "\n" "The `cases` tactic will split an object or hypothesis up into the possible ways\n" "that it could have been created.\n" "\n" "For example, sometimes you want to deal with the two cases `b = 0` and `b = succ d` separately,\n" "but don't need the inductive hypothesis `hd` that comes with `induction b with d hd`.\n" "In this situation you can use `cases b with d` instead. There are two ways to make\n" "a number: it's either zero or a successor. So you will end up with two goals, one\n" "with `b = 0` and one with `b = succ d`.\n" "\n" "Another example: if you have a hypothesis `h : False` then you are done, because a false statement implies\n" "any statement. Here `cases h` will close the goal, because there are *no* ways to\n" "make a proof of `False`! So you will end up with no goals, meaning you have proved everything." msgstr "" #: Game msgid "In this game you recreate the natural numbers $\\mathbb{N}$ from the Peano axioms,\n" "learning the basics about theorem proving in Lean.\n" "\n" "This is a good first introduction to Lean!" msgstr "" #: Game.Levels.Multiplication.L07mul_add msgid "Our next goal is \"left and right distributivity\",\n" "meaning $a(b+c)=ab+ac$ and $(b+c)a=ba+ca$. Rather than\n" "these slightly pompous names, the name of the proofs\n" "in Lean are descriptive. Let's start with\n" "`mul_add a b c`, the proof of `a * (b + c) = a * b + a * c`.\n" "Note that the left hand side contains a multiplication\n" "and then an addition." msgstr "" #: Game.Levels.Tutorial.L05add_zero msgid "## Summary\n" "\n" "`repeat t` repeatedly applies the tactic `t`\n" "to the goal. You don't need to use this\n" "tactic, 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`\n" "into the goal\n" "`a = b`." msgstr "" #: Game.Levels.Algorithm.L04add_algo3 msgid "You can make your own tactics in Lean.\n" "This code here\n" "```\n" "macro \"simp_add\" : tactic => `(tactic|(\n" " simp only [add_assoc, add_left_comm, add_comm]))\n" "```\n" "was used to create a new tactic `simp_add`, which runs\n" "`simp only [add_assoc, add_left_comm, add_comm]`.\n" "Try running `simp_add` to solve this level!" msgstr "" #: Game.Levels.Power.L06pow_add msgid "Let's now begin our approach to the final boss,\n" "by proving some more subtle facts about powers." msgstr "" #: Game.Levels.AdvAddition.L06add_left_eq_zero msgid "How about this for a proof:\n" "\n" "```\n" "rw [add_comm]\n" "exact add_right_eq_zero b a\n" "```\n" "\n" "That's the end of Advanced Addition World! You'll need these theorems\n" "for the next world, `≤` World. Click on \"Leave World\" to access it." msgstr "" #: Game.Levels.LessOrEqual.L06le_antisymm msgid "`le_antisymm x y` is a proof that if `x ≤ y` and `y ≤ x` then `x = y`." msgstr "" #: Game.Levels.Algorithm.L01add_left_comm msgid "If $a, b, c$ are numbers, then $a+(b+c)=b+(a+c)$." msgstr "" #: Game.Levels.Implication.L08ne msgid "≠" msgstr "" #: Game.Levels.Power.L06pow_add msgid "For all naturals $a$, $m$, $n$, we have $a^{m + n} = a ^ m a ^ n$." msgstr "" #: Game.Levels.AdvMultiplication.L10mul_right_eq_self msgid "mul_right_eq_self" msgstr "" #: Game.Levels.Multiplication.L08add_mul msgid "`add_mul` is just as fiddly to prove by induction; but there's a trick\n" "which avoids it. Can you spot it?" msgstr "" #: Game.Levels.AdvAddition.L03add_left_eq_self msgid "`add_left_eq_self x y` is the theorem that $x + y = y\\implies x=0.$" msgstr "" #: Game.Levels.Tutorial.L03two_eq_ss0 msgid "## The birth of number.\n" "\n" "Numbers 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" "\n" "The successor of `n` means the number after `n`. Let's learn to\n" "count, 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`.\n" "Similarly let's define `2 = succ 1`, `3 = succ 2` and `4 = succ 3`.\n" "This gives us plenty of numbers to be getting along with.\n" "\n" "The *proof* that `2 = succ 1` is called `two_eq_succ_one`.\n" "Check out the \"012\" tab in the list of lemmas on the right\n" "for this and other proofs.\n" "\n" "Let's prove that $2$ is the number after the number after zero." msgstr "" #: Game.Levels.AdvMultiplication.L01mul_le_mul_right msgid "`mul_le_mul_right a b t` is a proof that `a ≤ b → a * t ≤ b * t`." msgstr "" #: Game.Levels.Power.L08pow_pow msgid "`pow_pow a m n` is a proof that $(a^m)^n=a^{mn}.$" msgstr "" #: Game.Levels.AdvMultiplication.L04one_le_of_ne_zero msgid "`one_le_of_ne_zero a` is a proof that `a ≠ 0 → 1 ≤ a`." msgstr "" #: Game.Levels.AdvMultiplication.L10mul_right_eq_self msgid "A two-line proof is\n" "\n" "```\n" "nth_rewrite 2 [← mul_one a] at h\n" "exact mul_left_cancel a b 1 ha h\n" "```\n" "\n" "We now have all the tools necessary to set up the basic theory of divisibility of naturals." msgstr "" #: Game.Levels.Algorithm.L09decide2 msgid "decide again" msgstr "" #: Game.Levels.LessOrEqual.L03le_succ_self msgid "x ≤ succ x" msgstr "" #: Game.Levels.Implication.L04succ_inj #: Game.Levels.Implication.L05succ_inj2 msgid "If $x+1=4$ then $x=3$." msgstr "" #: Game.Levels.Multiplication.L07mul_add msgid "mul_add" msgstr "" #: Game.Levels.LessOrEqual.L06le_antisymm msgid "If $x \\leq y$ and $y \\leq x$, then $x = y$." msgstr "" #: Game.Levels.Tutorial.L02rw msgid "In this level the *goal* is $2y=2(x+7)$ but to help us we\n" "have an *assumption* `h` saying that $y = x + 7$. Check that you can see `h` in\n" "your list of assumptions. Lean thinks of `h` as being a secret proof of the\n" "assumption, rather like `x` is a secret number.\n" "\n" "Before we can use `rfl`, we have to \"substitute in for $y$\".\n" "We do this in Lean by *rewriting* the proof `h`,\n" "using the `rw` tactic." msgstr "" #: Game.Levels.Power.L03pow_one msgid "`pow_one a` says that `a ^ 1 = a`.\n" "\n" "Note that this is not quite true by definition: `a ^ 1` is\n" "defined to be `a ^ 0 * a` so it's `1 * a`, and to prove\n" "that this is equal to `a` you need to use induction somewhere." msgstr "" #: Game.Levels.Algorithm.L02add_algo1 msgid "making life easier" msgstr "" #: Game.Levels.AdvMultiplication.L01mul_le_mul_right msgid "Let's warm up with an easy one, which works even if `t = 0`." msgstr "" #: Game.Levels.AdvMultiplication.L03eq_succ_of_ne_zero msgid "eq_succ_of_ne_zero" msgstr "" #: Game.Levels.LessOrEqual.L07or_symm msgid "# Summary\n" "The `right` tactic changes a goal of `P ∨ Q` into a goal of `Q`.\n" "Use it when your hypotheses guarantee that the reason that `P ∨ Q`\n" "is true is because in fact `Q` is true.\n" "\n" "Internally this tactic is just `apply`ing a theorem\n" "saying that $Q \\implies P \\lor Q.$\n" "\n" "Note that this tactic can turn a solvable goal into an unsolvable\n" "one." msgstr "" #: Game.Levels.Multiplication.L02zero_mul msgid "zero_mul" msgstr "" #: Game.Levels.Power.L07mul_pow msgid "mul_pow" msgstr "" #: Game.Levels.Algorithm.L07succ_ne_succ msgid "If $a \\neq b$ then $\\operatorname{succ}(a) \\neq\\operatorname{succ}(b)$." msgstr "" #: Game.Levels.Multiplication.L05one_mul msgid "one_mul" msgstr "" #: Game.Levels.Algorithm.L05pred msgid "pred" msgstr "" #: Game.Levels.Tutorial.L03two_eq_ss0 #: Game.Levels.Tutorial.L04rw_backwards msgid "$2$ is the number after the number after $0$." msgstr "" #: Game.Levels.Implication.L05succ_inj2 msgid "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)." msgstr "" #: Game.Levels.Multiplication.L06two_mul msgid "For any natural number $m$, we have $ 2 \\times m = m+m$." msgstr "" #: Game.Levels.Tutorial.L02rw msgid "If $x$ and $y$ are natural numbers, and $y = x + 7$, then $2y = 2(x + 7)$." msgstr "" #: Game.Levels.Tutorial.L02rw msgid "## Summary\n" "\n" "If `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" "\n" "If the goal is `2 + 2 = 4` then `nth_rewrite 2 [two_eq_succ_one]`\n" "will change the goal to `2 + succ 1 = 4`. In contrast, `rw [two_eq_succ_one]`\n" "will change the goal to `succ 1 + succ 1 = 4`." msgstr "" #: Game.Levels.Algorithm.L06is_zero msgid "# Summary\n" "\n" "`trivial` will solve the goal `True`." msgstr "" #: Game.Levels.Power.L09add_sq msgid "[final boss music]" msgstr "" #: Game.Levels.Addition.L05add_right_comm msgid "add_right_comm" msgstr "" #: Game.Levels.LessOrEqual msgid "In this world we define `a ≤ b` and prove standard facts\n" "about it, such as \"if `a ≤ b` and `b ≤ c` then `a ≤ c`.\"\n" "\n" "The definition of `a ≤ b` is \"there exists a number `c`\n" "such that `b = a + c`. \" So we're going to have to learn\n" "a tactic to prove \"exists\" theorems, and another one\n" "to use \"exists\" hypotheses.\n" "\n" "Click on \"Start\" to proceed." msgstr "" #: Game.Levels.AdvMultiplication.L04one_le_of_ne_zero msgid "one_le_of_ne_zero" msgstr "" #: Game.Levels.Power.L04one_pow msgid "one_pow" msgstr "" #: Game.Levels.Algorithm.L06is_zero msgid "`succ_ne_zero a` is a proof of `succ a ≠ 0`." msgstr "" #: Game.Levels.AdvAddition.L02add_left_cancel msgid "How about this for a proof:\n" "```\n" "repeat rw [add_comm n]\n" "exact add_right_cancel a b n\n" "```" msgstr "" #: Game.Levels.LessOrEqual.L02zero_le msgid "0 ≤ x" msgstr "" #: Game.Levels.AdvAddition.L04add_right_eq_self msgid "Here's a proof using `add_left_eq_self`:\n" "```\n" "rw [add_comm]\n" "intro h\n" "apply add_left_eq_self at h\n" "exact h\n" "```\n" "\n" "and here's an even shorter one using the same idea:\n" "```\n" "rw [add_comm]\n" "exact add_left_eq_self y x\n" "```\n" "\n" "Alternatively you can just prove it by induction on `x`:\n" "\n" "```\n" "induction x with d hd\n" "intro h\n" "rw [zero_add] at h\n" "exact h\n" "intro h\n" "rw [succ_add] at h\n" "apply succ_inj at h\n" "apply hd at h\n" "exact h\n" "```" msgstr "" #: Game.Levels.Multiplication.L01mul_one msgid "`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" "\n" "Other theorems about naturals, such as `zero_mul`,\n" "are proved by induction from these two basic theorems." msgstr "" #: Game.Levels.Addition.L05add_right_comm msgid "You've now seen all the tactics you need to beat the final boss of the game.\n" "You can begin the journey towards this boss by entering Multiplication World.\n" "\n" "Or you can go off the beaten track and learn some new tactics in Implication\n" "World. These tactics let you prove more facts about addition, such as\n" "how to deduce `a = 0` from `x + a = x`.\n" "\n" "Click \"Leave World\" and make your choice." msgstr "" #: Game.Levels.Multiplication.L08add_mul msgid "add_mul" msgstr "" #: Game.Levels.Addition.L03add_comm msgid "On the set of natural numbers, addition is commutative.\n" "In other words, if `a` and `b` are arbitrary natural numbers, then\n" "$a + b = b + a$." msgstr "" #: Game.Levels.AdvMultiplication.L06mul_right_eq_one msgid "`mul_right_eq_one a b` is a proof that `a * b = 1 → a = 1`." msgstr "" #: Game.Levels.Implication.L09zero_ne_succ #: Game.Levels.AdvAddition.L01add_right_cancel msgid "Nice!" msgstr "" #: Game.Levels.Tutorial.L06add_zero2 msgid "Let's now learn about Peano's second axiom for addition, `add_succ`." msgstr "" #: Game.Levels.LessOrEqual.L09succ_le_succ msgid "Here's my proof:\n" "```\n" "cases hx with d hd\n" "use d\n" "rw [succ_add] at hd\n" "apply succ_inj at hd\n" "exact hd\n" "```" msgstr "" #: Game.Levels.Multiplication.L09mul_assoc msgid "`mul_assoc a b c` is a proof that `(a * b) * c = a * (b * c)`.\n" "\n" "Note that when Lean says `a * b * c` it means `(a * b) * c`.\n" "\n" "Note that `(a * b) * c = a * (b * c)` cannot be proved by \\\"pure thought\\\":\n" "for example subtraction is not associative, as `(6 - 2) - 1` is not\n" "equal to `6 - (2 - 1)`." msgstr "" #: Game.Levels.Tutorial.L01rfl msgid "## Summary\n" "\n" "`rfl` proves goals of the form `X = X`.\n" "\n" "In other words, the `rfl` tactic will close any goal of the\n" "form `A = B` if `A` and `B` are *identical*.\n" "\n" "`rfl` is short for \\\"reflexivity (of equality)\\\".\n" "\n" "## Example:\n" "\n" "If the goal looks like this:\n" "\n" "```\n" "x + 37 = x + 37\n" "```\n" "\n" "then `rfl` will close it. But if it looks like `0 + x = x` then `rfl` won't work, because even\n" "though $0+x$ and $x$ are always equal as *numbers*, they are not equal as *terms*.\n" "The 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`,\n" "for pedagogical purposes; mathematicians do not distinguish between propositional\n" "and definitional equality because they think about definitions in a different way\n" "to type theorists (`zero_add` and `add_zero` are both \\\"facts\\\" as far\n" "as mathematicians are concerned, and who cares what the definition of addition is).*" msgstr "" #: Game.Levels.LessOrEqual.L11le_two msgid "le_two" msgstr "" #: Game.Levels.Power.L05pow_two msgid "pow_two" msgstr "" #: Game.Levels.Algorithm.L05pred msgid "Nice! You've proved `succ_inj`!\n" "Let's now prove Peano's other axiom, that successors can't be $0$." msgstr "" #: Game.Levels.Tutorial.L05add_zero msgid "We'd like to prove `2 + 2 = 4` but right now\n" "we can't even *state* it\n" "because we haven't yet defined addition.\n" "\n" "## Defining addition.\n" "\n" "How are we going to add $37$ to an arbitrary number $x$? Well,\n" "there are only two ways to make numbers in this game: $0$\n" "and successors. So to define `37 + x` we will need\n" "to know what `37 + 0` is and what `37 + succ x` is.\n" "Let's start with adding `0`.\n" "\n" "### Adding 0\n" "\n" "To make addition agree with our intuition, we should *define* `37 + 0`\n" "to be `37`. More generally, we should define `a + 0` to be `a` for\n" "any number `a`. The name of this proof in Lean is `add_zero a`.\n" "For 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\n" "of `? + 0 = ?`.\n" "\n" "We write `add_zero x : x + 0 = x`, so `proof : statement`." msgstr "" #: Game.Levels.Algorithm.L06is_zero msgid "is_zero" msgstr "" #: Game.Levels.Power.L07mul_pow msgid "The music gets ever more dramatic, as we explore\n" "the interplay between exponentiation and multiplication.\n" "\n" "If you're having trouble exchanging the right `a * b`\n" "because `rw [mul_comm]` swaps the wrong multiplication,\n" "then read the documentation of `rw` for tips on how to fix this." msgstr "" #: Game.Levels.Implication.L06intro msgid "We have seen how to `apply` theorems and assumptions\n" "of the form `P → Q`. But what if our *goal* is of the form `P → Q`?\n" "To prove this goal, we need to know how to say \"let's assume `P` and deduce `Q`\"\n" "in Lean. We do this with the `intro` tactic." msgstr "" #: Game.Levels.Power.L10FLT msgid "`xyzzy` is an ancient magic spell, believed to be the origin of the\n" "modern word `sorry`. The game won't complain - or notice - if you\n" "prove anything with `xyzzy`." msgstr "" #: Game.Levels.AdvMultiplication.L04one_le_of_ne_zero msgid "The previous lemma can be used to prove this one." msgstr "" #: Game.Levels.Tutorial.L01rfl msgid "# Read this first\n" "\n" "Each level in this game involves proving a mathematical theorem (the \"Goal\").\n" "The goal will be a statement about *numbers*. Some numbers in this game have known values.\n" "Those numbers have names like $37$. Other numbers will be secret. They're called things\n" "like $x$ and $q$. We know $x$ is a number, we just don't know which one.\n" "\n" "In this first level we're going to prove the theorem that $37x + q = 37x + q$.\n" "You can see `x q : ℕ` in the *Objects* below, which means that `x` and `q`\n" "are numbers.\n" "\n" "We solve goals in Lean using *Tactics*, and the first tactic we're\n" "going to learn is called `rfl`, which proves all theorems of the form $X = X$.\n" "\n" "Prove that $37x+q=37x+q$ by executing the `rfl` tactic." msgstr "" #: Game.Levels.AdvMultiplication.L08mul_eq_zero msgid "mul_eq_zero" msgstr "" #: Game.Levels.Tutorial.L05add_zero msgid "`Add a b`, with notation `a + b`, is\n" "the usual sum of natural numbers. Internally it is defined\n" "via 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" "\n" "Other theorems about naturals, such as `zero_add a : 0 + a = a`, are proved\n" "by induction using these two basic theorems.\"" msgstr "" #: Game.Levels.Implication.L10one_ne_zero msgid "1 ≠ 0" msgstr "" #: Game.Levels.AdvMultiplication.L01mul_le_mul_right msgid "mul_le_mul_right" msgstr "" #: Game.Levels.AdvAddition.L04add_right_eq_self msgid "add_right_eq_self" msgstr "" #: Game.Levels.AdvMultiplication.L08mul_eq_zero msgid "Here's the short proof:\n" "```\n" "have h2 := mul_ne_zero a b\n" "tauto\n" "```\n" "This works because, given `mul_ne_zero a b`,\n" "the argument is reduced to pure logic." msgstr "" #: Game.Levels.LessOrEqual.L04le_trans msgid "x ≤ y and y ≤ z implies x ≤ z" msgstr "" #: Game.Levels.LessOrEqual.L03le_succ_self msgid "If $x$ is a number, then $x \\le \\operatorname{succ}(x)$." msgstr "" #: Game.Levels.Addition.L02succ_add msgid "Well done! You now have enough tools to tackle the main boss of this level." msgstr "" #: Game.Levels.Multiplication.L04mul_comm msgid "Multiplication is commutative." msgstr "" #: Game.Levels.Implication.L02exact2 msgid "Here's a two-line proof:\n" "```\n" "repeat rw [zero_add] at h\n" "exact h\n" "```" msgstr "" #: Game.Levels.Addition.L03add_comm msgid "`add_comm x y` is a proof of `x + y = y + x`." msgstr "" #: Game.Levels.AdvAddition.L02add_left_cancel msgid "`add_left_cancel a b n` is the theorem that $n+a=n+b\\implies a=b$.\n" "You can prove it by induction on `n` or you can deduce it from `add_right_cancel`." msgstr "" #: Game.Levels.Implication.L08ne msgid "`a ≠ b` is *notation* for `(a = b) → False`.\n" "\n" "The reason this is mathematically\n" "valid is that if `P` is a true-false statement then `P → False`\n" "is the logical opposite of `P`. Indeed `True → False` is false,\n" "and `False → False` is true!\n" "\n" "The upshot of this is that you can treat `a ≠ b` in exactly\n" "the same way as you treat any implication `P → Q`. For example,\n" "if your *goal* is of the form `a ≠ b` then you can make progress\n" "with `intro h`, and if you have a hypothesis `h` of the\n" "form `a ≠ b` then you can `apply h at h1` if `h1` is a proof\n" "of `a = b`." msgstr "" #: Game.Levels.Algorithm.L04add_algo3 msgid "# Overview\n" "\n" "Our home-made tactic `simp_add` will solve arbitrary goals of\n" "the form `a + (b + c) + (d + e) = e + (d + (c + b)) + a`." msgstr "" #: Game.Levels.Multiplication.L03succ_mul msgid "succ_mul" msgstr "" #: Game.Levels.Implication.L10one_ne_zero msgid "$1\\neq0$." msgstr "" #: Game.Levels.Implication.L01exact msgid "In this world we'll learn how to prove theorems of the form $P\\implies Q$.\n" "In other words, how to prove theorems of the form \"if $P$ is true, then $Q$ is true.\"\n" "To do that we need to learn some more tactics.\n" "\n" "The `exact` tactic can be used to close a goal which is exactly one of\n" "the hypotheses. It takes the name of the hypothesis as argument: `exact h`." msgstr "" #: Game.Levels.Power.L09add_sq msgid "`add_sq a b` is the statement that $(a+b)^2=a^2+b^2+2ab.$" msgstr "" #: Game.Levels.Tutorial.L03two_eq_ss0 msgid "Numbers" msgstr "" #: Game.Levels.Implication.L07intro2 msgid "$x+1=y+1 \\implies x=y$." msgstr "" #: Game.Levels.Implication.L03apply msgid "In this level, the hypotheses `h2` is an *implication*. It says\n" "that *if* `x = 37` *then* `y = 42`. We can use this\n" "hypothesis with the `apply` tactic. Remember you can click on\n" "`apply` or any other tactic on the right to see a detailed explanation\n" "of what it does, with examples." msgstr "" #: Game.Levels.LessOrEqual.L06le_antisymm msgid "This level asks you to prove *antisymmetry* of $\\leq$.\n" "In other words, if $x \\leq y$ and $y \\leq x$ then $x = y$.\n" "It's the trickiest one so far. Good luck!" msgstr "" #: Game.Levels.Tutorial.L04rw_backwards msgid "Why did we not just define `succ n` to be `n + 1`? Because we have not\n" "even *defined* addition yet! We'll do that in the next level." msgstr "" #: Game.Levels.LessOrEqual.L09succ_le_succ msgid "succ x ≤ succ y → x ≤ y" msgstr "" #: Game.Levels.LessOrEqual.L10le_one msgid "If $x \\leq 1$ then either $x = 0$ or $x = 1$." msgstr "" #: Game.Levels.LessOrEqual.L05le_zero msgid "`le_zero x` is a proof of `x ≤ 0 → x = 0`." msgstr "" #: Game msgid "The classical introduction game for Lean." msgstr "" #: Game.Levels.Power.L10FLT msgid "Fermat's Last Theorem" msgstr "" #: Game.Levels.Implication.L03apply msgid "If $x=37$ and we know that $x=37\\implies y=42$ then we can deduce $y=42$." msgstr "" #: Game.Levels.Multiplication.L03succ_mul msgid "For all natural numbers $a$ and $b$, we have\n" "$(\\operatorname{succ}\\ a) \\times b = a\\times b + b$." msgstr "" #: Game.Levels.AdvMultiplication.L06mul_right_eq_one msgid "# Summary\n" "\n" "The `have` tactic can be used to add new hypotheses to a level, but of course\n" "you have to prove them.\n" "\n" "\n" "## Example\n" "\n" "The simplest usage is like this. If you have `a` in your context and you execute\n" "\n" "`have ha : a = 0`\n" "\n" "then you will get a new goal `a = 0` to prove, and after you've proved\n" "it you will have a new hypothesis `ha : a = 0` in your original goal.\n" "\n" "## Example\n" "\n" "If you already have a proof of what you want to `have`, you\n" "can just create it immediately. For example, if you have `a` and `b`\n" "number objects, then\n" "\n" "`have h2 : succ a = succ b → a = b := succ_inj a b`\n" "\n" "will directly add a new hypothesis `h2 : succ a = succ b → a = b`\n" "to the context, because you just supplied the proof of it (`succ_inj a b`).\n" "\n" "## Example\n" "\n" "If you have a proof to hand, then you don't even need to state what you\n" "are proving. For example\n" "\n" "`have h2 := succ_inj a b`\n" "\n" "will add `h2 : succ a = succ b → a = b` as a hypothesis." msgstr "" #: Game.Levels.Algorithm msgid "Proofs like $2+2=4$ and $a+b+c+d+e=e+d+c+b+a$ are very tedious to do by hand.\n" "In Algorithm World we learn how to get the computer to do them for us.\n" "\n" "Click on \"Start\" to proceed." msgstr "" #: Game.Levels.Power.L09add_sq msgid "add_sq" msgstr "" #: Game.Levels.Power.L04one_pow msgid "`one_pow n` is a proof that $1^n=1$." msgstr "" #: Game.Levels.LessOrEqual.L05le_zero msgid "It's \"intuitively obvious\" that there are no numbers less than zero,\n" "but to prove it you will need a result which you showed in advanced\n" "addition world." msgstr "" #: Game.Levels.Implication.L07intro2 msgid "Here's a completely backwards proof:\n" "```\n" "intro h\n" "apply succ_inj\n" "repeat rw [succ_eq_add_one]\n" "exact h\n" "```" msgstr "" #: Game.Levels.Tutorial.L05add_zero msgid "`add_zero a` is a proof that `a + 0 = a`.\n" "\n" "## Summary\n" "\n" "`add_zero` is really a function, which\n" "eats a number, and returns a proof of a theorem\n" "about that number. For example `add_zero 37` is\n" "a proof that `37 + 0 = 37`.\n" "\n" "The `rw` tactic will accept `rw [add_zero]`\n" "and will try to figure out which number you omitted\n" "to input.\n" "\n" "## Details\n" "\n" "A mathematician sometimes thinks of `add_zero`\n" "as \\\"one thing\\\", namely a proof of $\\forall n ∈ ℕ, n + 0 = n$.\n" "This is just another way of saying that it's a function which\n" "can eat any number n and will return a proof that `n + 0 = n`." msgstr "" #: Game.Levels.LessOrEqual.L01le_refl msgid "`a ≤ b` is *notation* for `∃ c, b = a + c`. This \"backwards E\"\n" "means \"there exists\". So `a ≤ b` means that there exists\n" "a number `c` such that `b = a + c`. This definition works\n" "because there are no negative numbers in this game.\n" "\n" "To *prove* an \"exists\" statement, use the `use` tactic.\n" "Let's see an example." msgstr "" #: Game.Levels.Tutorial.L08twoaddtwo msgid "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]`." msgstr "" #: Game.Levels.LessOrEqual msgid "≤ World" msgstr "" #: Game.Levels.AdvMultiplication.L05le_mul_right msgid "`le_mul_right a b` is a proof that `a * b ≠ 0 → a ≤ a * b`.\n" "\n" "It's one way of saying that a divisor of a positive number\n" "has to be at most that number." msgstr "" #: Game.Levels.Implication.L02exact2 msgid "`exact` practice." msgstr "" #: Game.Levels.Algorithm.L01add_left_comm msgid "`add_left_comm a b c` is a proof that `a + (b + c) = b + (a + c)`." msgstr "" #: Game.Levels.Algorithm.L07succ_ne_succ msgid "An algorithm for equality" msgstr "" #: Game.Levels.LessOrEqual.L11le_two msgid "`le_two x` is a proof that if `x ≤ 2` then `x = 0` or `x = 1` or `x = 2`." msgstr "" #: Game.Levels.Addition.L02succ_add msgid "`succ_add a b` is a proof that `succ a + b = succ (a + b)`." msgstr "" #: Game.Levels.Power msgid "Power World" msgstr "" #: Game.Levels.AdvMultiplication.L05le_mul_right msgid "le_mul_right" msgstr "" #: Game.Levels.Implication.L09zero_ne_succ msgid "$0\\neq1$." msgstr "" #: Game.Levels.AdvAddition.L03add_left_eq_self msgid "Did you use induction on `y`?\n" "Here's a two-line proof of `add_left_eq_self` which uses `add_right_cancel`.\n" "If you want to inspect it, you can go into editor mode by clicking `` in the top right\n" "and then just cut and paste the proof and move your cursor around it\n" "to see the hypotheses and goal at any given point\n" "(although you'll lose your own proof this way). Click `>_` to get\n" "back to command line mode.\n" "```\n" "nth_rewrite 2 [← zero_add y]\n" "exact add_right_cancel x 0 y\n" "```" msgstr "" #: Game.Levels.Multiplication.L06two_mul msgid "two_mul" msgstr "" #: Game.Levels.Algorithm.L04add_algo3 msgid "the simplest approach" msgstr "" #: Game.Levels.AdvAddition.L05add_right_eq_zero msgid "If $a+b=0$ then $a=0$." msgstr "" #: Game.Levels.LessOrEqual.L08le_total msgid "This is I think the toughest level yet. Tips: if `a` is a number\n" "then `cases a with b` will split into cases `a = 0` and `a = succ b`.\n" "And don't go left or right until your hypotheses guarantee that\n" "you can prove the resulting goal!\n" "\n" "I've left hidden hints; if you need them, retry from the beginning\n" "and click on \"Show more help!\"" msgstr "" #: Game.Levels.Algorithm.L02add_algo1 msgid "So that's the algorithm: now let's use automation to perform it\n" "automatically." msgstr "" #: Game.Levels.AdvMultiplication.L02mul_left_ne_zero msgid "`mul_left_ne_zero a b` is a proof that `a * b ≠ 0 → b ≠ 0`." msgstr "" #: Game.Levels.Implication.L09zero_ne_succ msgid "`zero_ne_one` is a proof of `0 ≠ 1`." msgstr "" #: Game.Levels.LessOrEqual.L09succ_le_succ msgid "`succ_le_succ x y` is a proof that if `succ x ≤ succ y` then `x ≤ y`." msgstr "" #: Game.Levels.Tutorial.L07add_succ msgid "For all natural numbers $a$, we have $\\operatorname{succ}(a) = a+1$." msgstr "" #: Game.Levels.LessOrEqual.L02zero_le msgid "`zero_le x` is a proof that `0 ≤ x`." msgstr "" #: Game.Levels.AdvAddition.L05add_right_eq_zero msgid "Well done!" msgstr "" #: Game.Levels.Tutorial.L06add_zero2 msgid "Precision rewriting" msgstr "" #: Game.Levels.Implication.L02exact2 msgid "Assuming $0+x=(0+y)+2$, we have $x=y+2$." msgstr "" #: Game.Levels.Multiplication.L06two_mul msgid "This level is more important than you think; it plays\n" "a useful role when battling a big boss later on." msgstr "" #: Game.Levels.Multiplication.L05one_mul msgid "For any natural number $m$, we have $ 1 \\times m = m$." msgstr "" #: Game.Levels.Power.L08pow_pow msgid "The music dies down. Is that it?\n" "\n" "Course it isn't, you can\n" "clearly see that there are two levels left.\n" "\n" "A passing mathematician says that mathematicians don't have a name\n" "for the structure you just constructed. You feel cheated.\n" "\n" "Suddenly the music starts up again. This really is the final boss." msgstr "" #: Game.Levels.AdvAddition.L01add_right_cancel msgid "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$." msgstr "" #: Game.Levels.Tutorial msgid "Tutorial World" msgstr "" #: Game.Levels.AdvAddition.L01add_right_cancel msgid "$a+n=b+n\\implies a=b$." msgstr "" #: Game.Levels.Addition.L04add_assoc msgid "On the set of natural numbers, addition is associative.\n" "In other words, if $a, b$ and $c$ are arbitrary natural numbers, we have\n" "$ (a + b) + c = a + (b + c). $" msgstr "" #: Game.Levels.LessOrEqual.L07or_symm msgid "Totality of `≤` is the boss level of this world, and it's coming up next. It says that\n" "if `a` and `b` are naturals then either `a ≤ b` or `b ≤ a`.\n" "But we haven't talked about `or` at all. Here's a run-through.\n" "\n" "1) The notation for \"or\" is `∨`. You won't need to type it, but you can\n" "type it with `\\or`.\n" "\n" "2) If you have an \"or\" statement in the *goal*, then two tactics made\n" "progress: `left` and `right`. But don't choose a direction unless your\n" "hypotheses guarantee that it's the correct one.\n" "\n" "3) 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,\n" "and the other where you went right." msgstr "" #: Game.Levels.AdvMultiplication msgid "Advanced Multiplication World" msgstr "" #: Game.Levels.AdvMultiplication.L08mul_eq_zero msgid "This level proves that if `a * b = 0` then `a = 0` or `b = 0`. It is\n" "logically equivalent to the last level, so there is a very short proof." msgstr "" #: GameServer.RpcHandlers msgid "level completed! 🎉" msgstr "" #: Game.Levels.Multiplication.L02zero_mul msgid "`zero_mul x` is the proof that `0 * x = 0`.\n" "\n" "Note: `zero_mul` is a `simp` lemma." msgstr "" #: Game msgid "# Welcome to the Natural Number Game\n" "#### An introduction to mathematical proof.\n" "\n" "In this game, we will build the basic theory of the natural\n" "numbers `{0,1,2,3,4,...}` from scratch. Our first goal is to prove\n" "that `2 + 2 = 4`. Next we'll prove that `x + y = y + x`.\n" "And at the end we'll see if we can prove Fermat's Last Theorem.\n" "We'll do this by solving levels of a computer puzzle game called Lean.\n" "\n" "# Read this.\n" "\n" "Learning how to use an interactive theorem prover takes time.\n" "Tests show that the people who get the most out of this game are\n" "those who read the help texts like this one.\n" "\n" "To start, click on \"Tutorial World\".\n" "\n" "Note: this is a new Lean 4 version of the game containing several\n" "worlds which were not present in the old Lean 3 version. More new worlds\n" "such as Strong Induction World, Even/Odd World and Prime Number World\n" "are in development; if you want to see their state or even help out, checkout\n" "out the [issues in the github repo](https://github.com/leanprover-community/NNG4/issues).\n" "\n" "## More\n" "\n" "Click on the three lines in the top right and select \"Game Info\" for resources,\n" "links, and ways to interact with the Lean community." msgstr "" #: Game.Levels.Power.L05pow_two msgid "For all naturals $a$, $a ^ 2 = a \\times a$." msgstr "" #: Game.Levels.LessOrEqual.L02zero_le msgid "To solve this level, you need to `use` a number `c` such that `x = 0 + c`." msgstr "" #: Game.Levels.LessOrEqual.L01le_refl msgid "`a ≤ b` is *notation* for `∃ c, b = a + c`.\n" "\n" "Because this game doesn't have negative numbers, this definition\n" "is mathematically valid.\n" "\n" "This means that if you have a goal of the form `a ≤ b` you can\n" "make 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`." msgstr "" #: Game.Levels.Tutorial.L03two_eq_ss0 msgid "`three_eq_succ_two` is a proof of `3 = succ 2`." msgstr "" #: Game.Levels.Power.L07mul_pow msgid "For all naturals $a$, $b$, $n$, we have $(ab) ^ n = a ^ nb ^ n$." msgstr "" #: Game.Levels.Multiplication.L05one_mul msgid "Here's my solution:\n" "```\n" "rw [mul_comm, mul_one]\n" "rfl\n" "```" msgstr "" #: Game.Levels.Tutorial.L07add_succ msgid "add_succ" msgstr "" #: Game.Levels.Algorithm.L07succ_ne_succ msgid "# Summary\n" "\n" "If you have a hypothesis\n" "\n" "`h : a ≠ b`\n" "\n" "and goal\n" "\n" "`c ≠ d`\n" "\n" "then `contrapose! h` replaces the set-up with its so-called \\\"contrapositive\\\":\n" "a hypothesis\n" "\n" "`h : c = d`\n" "\n" "and goal\n" "\n" "`a = b`." msgstr "" #: Game.Levels.Power.L03pow_one msgid "pow_one" msgstr "" #: Game.Levels.AdvMultiplication.L07mul_ne_zero msgid "This level proves that if `a ≠ 0` and `b ≠ 0` then `a * b ≠ 0`. One strategy\n" "is to write both `a` and `b` as `succ` of something, deduce that `a * b` is\n" "also `succ` of something, and then `apply zero_ne_succ`." msgstr "" #: Game.Levels.Implication.L01exact msgid "## Summary\n" "\n" "If the goal is a statement `P`, then `exact h` will close the goal if `h` is a proof of `P`.\n" "\n" "### Example\n" "\n" "If the goal is `x = 37` and you have a hypothesis `h : x = 37`\n" "then `exact h` will solve the goal.\n" "\n" "### Example\n" "\n" "If the goal is `x + 0 = x` then `exact add_zero x` will close the goal.\n" "\n" "### Exact needs to be exactly right\n" "\n" "Note that `exact add_zero` will *not work* in the previous example;\n" "for `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,\n" "a proof of `? + 0 = ?` where `?` needs to be supplied by the user.\n" "This is in contrast to `rw` and `apply`, which will \\\"guess the inputs\\\"\n" "if necessary. If the goal is `x + 0 = x` then `rw [add_zero]`\n" "and `rw [add_zero x]` will both change the goal to `x = x`,\n" "because `rw` guesses the input to the function `add_zero`." msgstr "" #: Game.Levels.AdvAddition.L05add_right_eq_zero msgid "add_right_eq_zero" msgstr "" #: Game.Levels.Power.L04one_pow msgid "For all naturals $m$, $1 ^ m = 1$." msgstr "" #: Game.Levels.Tutorial.L05add_zero msgid "Adding zero" msgstr "" #: Game.Levels.Addition.L05add_right_comm msgid "`add_comm b c` is a proof that `b + c = c + b`. But if your goal\n" "is `a + b + c = a + c + b` then `rw [add_comm b c]` will not\n" "work! Because the goal means `(a + b) + c = (a + c) + b` so there\n" "is no `b + c` term *directly* in the goal.\n" "\n" "Use associativity and commutativity to prove `add_right_comm`.\n" "You don't need induction. `add_assoc` moves brackets around,\n" "and `add_comm` moves variables around.\n" "\n" "Remember that you can do more targetted rewrites by\n" "adding explicit variables as inputs to theorems. For example `rw [add_comm b]`\n" "will only do rewrites of the form `b + ? = ? + b`, and `rw [add_comm b c]`\n" "will only do rewrites of the form `b + c = c + b`." msgstr "" #: Game.Levels.Addition.L03add_comm msgid "[boss battle music]\n" "\n" "Look in your inventory to see the proofs you have available.\n" "These should be enough." msgstr "" #: Game.Levels.LessOrEqual.L03le_succ_self msgid "Here's a two-liner:\n" "```\n" "use 1\n" "exact succ_eq_add_one x\n" "```\n" "\n" "This works because `succ_eq_add_one x` is a proof of `succ x = x + 1`." msgstr "" #: Game.Levels.Multiplication.L07mul_add msgid "Multiplication is distributive over addition on the left.\n" "In other words, for all natural numbers $a$, $b$ and $c$, we have\n" "$a(b + c) = ab + ac$." msgstr "" #: Game.Levels.Power.L02zero_pow_succ msgid "zero_pow_succ" msgstr "" #: Game.Levels.LessOrEqual.L07or_symm msgid "Ready for the boss level of this world?" msgstr "" #: Game.Levels.Algorithm msgid "Algorithm World" msgstr "" #: Game.Levels.Power.L10FLT msgid "Congratulations! You have proved Fermat's Last Theorem!\n" "\n" "Either that, or you used magic..." msgstr "" #: Game.Levels.Tutorial.L04rw_backwards msgid "rewriting backwards" msgstr "" #: Game.Levels.Multiplication.L08add_mul msgid "`add_mul a b c` is a proof that $(a+b)c=ac+bc$." msgstr ""