ck
This commit is contained in:
Hydrogenbear
@@ -742,7 +742,7 @@
|
||||
"And now we've deduced what we wanted to prove: the goal is one of our assumptions.\nFinish the level with `exact h`.":
|
||||
"现在我们已经推导出了我们想要证明的了：目标是我们的假设之一。\n用 `exact h` 完成本关。",
|
||||
"And now `rw [add_zero]`": "现在使用`rw [add_zero]`",
|
||||
"And finally `rfl`.": "最后是 \"rfl`\"。",
|
||||
"And finally `rfl`.": "最后是 `rfl`。",
|
||||
"An algorithm for equality": "用于证明等价的算法",
|
||||
"Although $0^0=1$ in this game, $0^n=0$ if $n>0$, i.e., if\n$n$ is a successor.":
|
||||
"虽然在这个游戏中 $0^0=1$，但如果 $n>0$，即如果 $n$ 是后继数，那么 $0^n=0$。",
|
||||
@@ -812,7 +812,7 @@
|
||||
"## Summary\n\nIf `n : ℕ` is an object, and the goal mentions `n`, then `induction n with d hd`\nattempts to prove the goal by induction on `n`, with the inductive\nvariable in the successor case being `d`, and the inductive hypothesis being `hd`.\n\n### Example:\nIf the goal is\n```\n0 + n = n\n```\n\nthen\n\n`induction n with d hd`\n\nwill turn it into two goals. The first is `0 + 0 = 0`;\nthe second has an assumption `hd : 0 + d = d` and goal\n`0 + succ d = succ d`.\n\nNote that you must prove the first\ngoal before you can access the second one.":
|
||||
"## 小结\n\n如果 `n : ℕ` 是一个对象，并且目标提到了 `n`，那么 `induction n with d hd`\n尝试通过对 `n` 进行归纳来证明目标，其中后继数情况下的归纳变量是 `d`，归纳假设是 `hd`。\n\n### 例子:\n如果目标是\n```\n0 + n = n\n```\n\n那么\n\n`induction n with d hd`\n\n将把它变成两个目标。第一个是 `0 + 0 = 0`；\n第二个有一个假设 `hd : 0 + d = d` 和目标\n`0 + succ d = succ d` 。\n\n注意你必须先证明第一个然后才能证第二个。",
|
||||
"## Summary\n\nIf `h` is a proof of an equality `X = Y`, then `rw [h]` will change\nall `X`s in the goal to `Y`s. It's the way to \\\"substitute in\\\".\n\n## Variants\n\n* `rw [← h]` (changes `Y`s to `X`s; get the back arrow by typing `\\left ` or `\\l`.)\n\n* `rw [h1, h2]` (a sequence of rewrites)\n\n* `rw [h] at h2` (changes `X`s to `Y`s in hypothesis `h2`)\n\n* `rw [h] at h1 h2 ⊢` (changes `X`s to `Y`s in two hypotheses and the goal;\nget the `⊢` symbol with `\\|-`.)\n\n* `repeat rw [add_zero]` will keep changing `? + 0` to `?`\nuntil there are no more matches for `? + 0`.\n\n* `nth_rewrite 2 [h]` will change only the second `X` in the goal to `Y`.\n\n### Example:\n\nIf you have the assumption `h : x = y + y` and your goal is\n```\nsucc (x + 0) = succ (y + y)\n```\n\nthen\n\n`rw [add_zero]`\n\nwill change the goal into `succ x = succ (y + y)`, and then\n\n`rw [h]`\n\nwill change the goal into `succ (y + y) = succ (y + y)`, which\ncan be solved with `rfl`.\n\n### Example:\n\nYou can use `rw` to change a hypothesis as well.\nFor example, if you have two hypotheses\n```\nh1 : x = y + 3\nh2 : 2 * y = x\n```\nthen `rw [h1] at h2` will turn `h2` into `h2 : 2 * y = y + 3`.\n\n## Common errors\n\n* You need the square brackets. `rw h` is never correct.\n\n* If `h` is not a *proof* of an *equality* (a statement of the form `A = B`),\nfor example if `h` is a function or an implication,\nthen `rw` is not the tactic you want to use. For example,\n`rw [P = Q]` is never correct: `P = Q` is the theorem *statement*,\nnot the proof. If `h : P = Q` is the proof, then `rw [h]` will work.\n\n## Details\n\nThe `rw` tactic is a way to do \\\"substituting in\\\". There\nare two distinct situations where you can use this tactic.\n\n1) Basic usage: if `h : A = B` is an assumption or\nthe proof of a theorem, and if the goal contains one or more `A`s, then `rw [h]`\nwill change them all to `B`'s. The tactic will error\nif there are no `A`s in the goal.\n\n2) Advanced usage: Assumptions coming from theorem proofs\noften have missing pieces. For example `add_zero`\nis a proof that `? + 0 = ?` because `add_zero` really is a function,\nand `?` is the input. In this situation `rw` will look through the goal\nfor any subterm of the form `x + 0`, and the moment it\nfinds one it fixes `?` to be `x` then changes all `x + 0`s to `x`s.\n\nExercise: think about why `rw [add_zero]` changes the term\n`(0 + 0) + (x + 0) + (0 + 0) + (x + 0)` to\n`0 + (x + 0) + 0 + (x + 0)`\n\nIf you can't remember the name of the proof of an equality, look it up in\nthe list of lemmas on the right.\n\n## Targetted usage\n\nIf your goal is `b + c + a = b + (a + c)` and you want to rewrite `a + c`\nto `c + a`, then `rw [add_comm]` will not work because Lean finds another\naddition first and swaps those inputs instead. Use `rw [add_comm a c]` to\nguarantee that Lean rewrites `a + c` to `c + a`. This works because\n`add_comm` is a proof that `?1 + ?2 = ?2 + ?1`, `add_comm a` is a proof\nthat `a + ? = ? + a`, and `add_comm a c` is a proof that `a + c = c + a`.\n\nIf `h : X = Y` then `rw [h]` will turn all `X`s into `Y`s.\nIf you only want to change the 37th occurrence of `X`\nto `Y` then do `nth_rewrite 37 [h]`.":
|
||||
"## 小结\n\n如果 `h` 是等式 `X = Y` 的证明，那么 `rw [h]` 将改变\n目标中的所有 `X`s 变为 `Y`s。这是 \"代入 \"的方法。\n\n## Variants\n\n* `rw [← h]` （将 `Y`s 更改为 `X`s；通过输入 `\\left ` 或 `\\l` 获取后箭头）。\n\n* `rw [h1, h2]`（重写序列）\n\n* `rw [h] at h2`（将假设 `h2` 中的 `X`s 改为 `Y`s）\n\n* `rw [h] at h1 h2 ⊢` （将两个假设和目标中的 `X`s 改为 `Y`s；\n用 `\\|-` 获取 `⊢` 符号）。\n\n* `repeat rw [add_zero]` 将继续将 `? + 0` 更改为 `?`。\n直到没有更多匹配的 `? + 0`。\n\n* `nth_rewrite 2 [h]` 只会将目标中的第二个 `X` 改为 `Y`。\n\n#### 示例：\n\n如果假设为 `h : x = y + y`，目标为\n```.\nsucc (x + 0) = succ (y + y)\n```.\n\n则\n\n`rw [add_zero]`\n\n会将目标改为 `succ x = succ (y + y)`，然后\n\n`rw [h]`\n\n会将目标变为 `succ (y + y) = succ (y + y)`，这\n可以用 `rfl` 解决。\n\n#### 示例：\n\n你也可以用 `rw` 来改变一个假设。\n例如，如果您有两个假设\n```\nh1 : x = y + 3\nh2 : 2 * y = x\n```\n则 `rw [h1] at h2` 将把 `h2` 变为 `h2 : 2 * y = y + 3`。\n-/\n\n## 常见错误\n\n* 需要方括号。`rw h` 永远不会正确。\n\n* 如果 `h` 不是一个 *等式* 的 *证明* （形式为 `A = B` 的定理或假设）、\n例如，如果 `h` 是一个函数或蕴涵、\n那么 `rw` 就不是您要使用的策略。例如\n`rw [P = Q]` 绝对不正确：`P = Q` 是定理*陈述、\n而不是证明。如果 `h : P = Q` 是证明，那么 `rw [h]` 也可以。\n\n## 详情\n\n`rw` 策略是 \"代入 \"的一种方法。有\n有两种不同的情况可以使用这种策略。\n\n1) 基本用法：如果 `h : A = B` 是一个假设或\n如果目标包含一个或多个 `A`s，那么 `rw [h]`\n会将它们全部改为 `B`。如果没有 OFeTl\n如果目标中没有 `A`s。\n\n2) 高级用法：来自定理证明的假设\n通常会有缺失。例如 `add_zero`\n是 `? + 0 = ?` 的证明，因为 `add_zero` 确实是一个函数、\n而 `?` 是输入。在这种情况下，`rw` 将在目标中查找\n寻找任何形式为 `x + 0` 的子项。\n就会将 `?` 固定为 `x`，然后将所有 `x + 0` 改为 `x`s。\n\n练习：想一想为什么 `rw [add_zero]` 会改变术语\n`(0 + 0) + (x + 0) + (0 + 0) + (x + 0)` 改为\n`0 + (x + 0) + 0 + (x + 0)`\n\n如果您记不起相等证明的名称，请在\n右侧的公例列表中查找。\n\n## 目标用法\n\n如果您的目标是 `b + c + a = b + (a + c)`，而您想将 `a + c` 重写为\n为 `c + a`，那么 `rw [add_comm]` 将不起作用，因为 Lean 会先找到另一个加法，然后交换这些输入\n加法，并交换这些输入。使用 `rw [add_comm a c]` 来\n保证Lean将 `a + c` 改写为 `c + a`。这是因为\n`add_comm` 是 `?1 + ?2 = ?2 + ?1` 的证明，`add_comm a` 是 `a + ? = ? + a` 的证明。\n是 `a + ? = ? + a` 的证明，而 `add_comm a c` 是 `a + c = c + a` 的证明。\n\n如果是 `h : X = Y`，那么 `rw [h]` 将把所有 `X`s 变为 `Y`s。\n如果您只想将第 37 次出现的 `X`\n改为 `Y`，则执行 `nth_rewrite 37 [h]`。",
|
||||
"## 摘要\n\n如果 `h` 是等式 `X = Y` 的证明，那么 `rw [h]` 将改变\n目标中的所有 `X`s 变为 `Y`s。这是 “代入”的方法。\n\n## 变形\n\n* `rw [← h]` （将 `Y`s 更改为 `X`s；通过输入 `\\left ` 或 `\\l` 获取后箭头）。\n\n* `rw [h1, h2]`（重写序列）\n\n* `rw [h] at h2`（将假设 `h2` 中的 `X`s 改为 `Y`s）\n\n* `rw [h] at h1 h2 ⊢` （将两个假设和目标中的 `X`s 改为 `Y`s；\n用 `\\|-` 获取 `⊢` 符号）。\n\n* `repeat rw [add_zero]` 将重复把 `? + 0` 更改为 `?`。\n直到没有更多匹配的 `? + 0`。\n\n* `nth_rewrite 2 [h]` 只会将目标中的第二个 `X` 改为 `Y`。\n\n### 示例：\n\n如果假设为 `h : x = y + y`，目标为\n```\nsucc (x + 0) = succ (y + y)\n```\n\n则\n\n`rw [add_zero]`\n\n会将目标改为 `succ x = succ (y + y)`，然后\n\n`rw [h]`\n\n会将目标变为 `succ (y + y) = succ (y + y)`，这\n可以用 `rfl` 解决。\n\n### 示例：\n\n你也可以用 `rw` 来改变一个假设。\n例如，如果您有两个假设\n```\nh1 : x = y + 3\nh2 : 2 * y = x\n```\n则 `rw [h1] at h2` 将把 `h2` 变为 `h2 : 2 * y = y + 3`。\n\n## 常见错误\n\n* 需要方括号。`rw h` 永远不会正确。\n\n* 如果 `h` 不是一个 *等式* 的 *证明* （形式为 `A = B` 的定理或假设），\n比如 `h` 是一个函数或蕴涵，\n那么 `rw` 就不是您要使用的策略。再比如\n`rw [P = Q]` 绝对不正确，因为`P = Q` 是定理的*陈述*\n而不是证明。但如果 `h : P = Q` 是证明，那么 `rw [h]` 是可以用的。\n\n## 详情\n\n`rw` 策略是 “代入”的一种方法。有\n有两种不同的情况可以使用这种策略。\n\n1) 基本用法：如果 `h : A = B` 是一个假设或\n如果目标包含一个或多个 `A`s，那么 `rw [h]`会将它们全部改为 `B`。如果目标中没有 `A`s，那么策略会报错。\n\n2) 高级用法：来自定理证明的假设通常会有缺失。例如 `add_zero`\n是 `? + 0 = ?` 的证明，因为 `add_zero` 确实是一个函数、\n而 `?` 是输入。在这种情况下，`rw` 将在目标中查找\n寻找任何形式为 `x + 0` 的子项。\n就会将 `?` 固定为 `x`，然后将所有 `x + 0` 改为 `x`s。\n\n练习：想一想为什么 `rw [add_zero]` 会改变术语\n`(0 + 0) + (x + 0) + (0 + 0) + (x + 0)` 改为\n`0 + (x + 0) + 0 + (x + 0)`\n\n如果您记不起相等证明的名称，请在右侧的定理列表中查找。\n\n## 目标用法\n\n如果您的目标是 `b + c + a = b + (a + c)`，而您想将 `a + c` 重写为为 `c + a`，那么 `rw [add_comm]` 将不起作用，因为 Lean 会先找到另一个加法，然后交换这些输入\n加法，并交换这些输入。使用 `rw [add_comm a c]` 来保证Lean将 `a + c` 改写为 `c + a`。这是因为 `add_comm` 是 `?1 + ?2 = ?2 + ?1` 的证明，`add_comm a` 是 `a + ? = ? + a` 的证明。\n而 `add_comm a c` 是 `a + c = c + a` 的证明。\n\n如果是 `h : X = Y`，那么 `rw [h]` 将把所有 `X`s 变为 `Y`s。\n如果您只想将第 37 次出现的 `X` 改为 `Y`，则执行 `nth_rewrite 37 [h]`。",
|
||||
"## Summary\n\nIf `h : X = Y` and there are several `X`s in the goal, then\n`nth_rewrite 3 [h]` will just change the third `X` to a `Y`.\n\n## Example\n\nIf the goal is `2 + 2 = 4` then `nth_rewrite 2 [two_eq_succ_one]`\nwill change the goal to `2 + succ 1 = 4`. In contrast, `rw [two_eq_succ_one]`\nwill change the goal to `succ 1 + succ 1 = 4`.":
|
||||
"## 小结\n\n如果 `h : X = Y` 并且在目标中有多个 `X`，那么 `nth_rewrite 3 [h]` 将仅更改第三个 `X` 为 `Y`。\n\n## 示例\n\n如果目标是 `2 + 2 = 4`，那么 `nth_rewrite 2 [two_eq_succ_one]` 将目标更改为 `2 + succ 1 = 4`。相比之下，`rw [two_eq_succ_one]` 将目标更改为 `succ 1 + succ 1 = 4`。",
|
||||
"## Precision rewriting\n\nIn the last level, there was `b + 0` and `c + 0`,\nand `rw [add_zero]` changed the first one it saw,\nwhich was `b + 0`. Let's learn how to tell Lean\nto change `c + 0` first by giving `add_zero` an\nexplicit input.":
|
||||
|
||||
136
.i18n/zh/Game.po
136
.i18n/zh/Game.po
@@ -81,7 +81,8 @@ msgstr ""
|
||||
"x + 37 = x + 37\n"
|
||||
"```\n"
|
||||
"\n"
|
||||
"那么 `rfl` 将证明它。但如果它看起来像 `0 + x = x`，那么 `rfl` 将无法工作，因为即使 $0+x$ 和 $x$ 作为*数字*总是相等，但它们作为*项*并不相等。唯一与 `0 + x` 相同的项是 `0 + x`。\n"
|
||||
"那么 `rfl` 将证明它。但如果它看起来像 `0 + x = x`，那么 `rfl` 将无法工作，因为即使 $0+x$ 和 $x$ 作为*数字*总是相等，但它们作为*项*并不相等。唯一与 `0 + x` 相同的项是 `0 + "
|
||||
"x`。\n"
|
||||
"\n"
|
||||
"\n"
|
||||
"## 详细信息\n"
|
||||
@@ -90,9 +91,10 @@ msgstr ""
|
||||
"\n"
|
||||
"## 游戏实现\n"
|
||||
"\n"
|
||||
"*请注意，出于教学目的，我们的 `rfl` 比核心 Lean 和 `mathlib` 中使用的版本弱一些；数学家不区分命题等价和定义等价，因为他们以不同于类型理论家的方式思考定义（就数学家而言，`zero_add` 和 `add_zero` 都是 “事实”，谁会在乎加法的定义是什么"
|
||||
"呢）。*\n"
|
||||
"（译注：因为 `add_zero` 是加法定义的一部分，而定义等价是可以直接用 `rfl` 证明的。也就是说 `x + 0 = x` 可以用 `rfl` 证明。所以作者多了一嘴，但实际上因为很少有人知道类型理论家怎么思考，所以这个注解看起来会有些奇怪。）"
|
||||
"*请注意，出于教学目的，我们的 `rfl` 比核心 Lean 和 `mathlib` 中使用的版本弱一些；数学家不区分命题等价和定义等价，因为他们以不同于类型理论家的方式思考定义（就数学家而言，"
|
||||
"`zero_add` 和 `add_zero` 都是 “事实”，谁会在乎加法的定义是什么呢）。*\n"
|
||||
"（译注：因为 `add_zero` 是加法定义的一部分，而定义等价是可以直接用 `rfl` 证明的。也就是说 `x + 0 = x` 可以用 `rfl` 证明。所以作者多了一嘴，但实际上因为很少有人知道类型理论家怎"
|
||||
"么思考，所以这个注解看起来会有些奇怪。）"
|
||||
|
||||
#: Game.Levels.Tutorial.L01rfl
|
||||
msgid ""
|
||||
@@ -114,8 +116,8 @@ msgid ""
|
||||
msgstr ""
|
||||
"# 游戏指南\n"
|
||||
"\n"
|
||||
"在这个游戏的每个关卡中，你都将挑战证明一个数学定理，这里称之为“目标”。这些目标主要与*自然数*相关。游戏中，一些数具有明确的值，例如 $37$ 这类具体的数。然而，还有一些数是未知数，它们被称为 $x$、$q$ 等。虽然我们不知道 $x$ 的具体值，但"
|
||||
"我们知道它代表一个自然数。\n"
|
||||
"在这个游戏的每个关卡中，你都将挑战证明一个数学定理，这里称之为“目标”。这些目标主要与*自然数*相关。游戏中，一些数具有明确的值，例如 $37$ 这类具体的数。然而，还有一些数是未知"
|
||||
"数，它们被称为 $x$、$q$ 等。虽然我们不知道 $x$ 的具体值，但我们知道它代表一个自然数。\n"
|
||||
"\n"
|
||||
"在游戏的第一关，我们的任务是证明定理 $37x + q = 37x + q$。你将在下方的*对象*中看到 `x q : ℕ`，这表示 `x` 和 `q` 都是自然数。\n"
|
||||
"\n"
|
||||
@@ -250,12 +252,12 @@ msgid ""
|
||||
"If you only want to change the 37th occurrence of `X`\n"
|
||||
"to `Y` then do `nth_rewrite 37 [h]`."
|
||||
msgstr ""
|
||||
"## 小结\n"
|
||||
"## 摘要\n"
|
||||
"\n"
|
||||
"如果 `h` 是等式 `X = Y` 的证明，那么 `rw [h]` 将改变\n"
|
||||
"目标中的所有 `X`s 变为 `Y`s。这是 \"代入 \"的方法。\n"
|
||||
"目标中的所有 `X`s 变为 `Y`s。这是 “代入”的方法。\n"
|
||||
"\n"
|
||||
"## Variants\n"
|
||||
"## 变形\n"
|
||||
"\n"
|
||||
"* `rw [← h]` （将 `Y`s 更改为 `X`s；通过输入 `\\left ` 或 `\\l` 获取后箭头）。\n"
|
||||
"\n"
|
||||
@@ -266,17 +268,17 @@ msgstr ""
|
||||
"* `rw [h] at h1 h2 ⊢` （将两个假设和目标中的 `X`s 改为 `Y`s；\n"
|
||||
"用 `\\|-` 获取 `⊢` 符号）。\n"
|
||||
"\n"
|
||||
"* `repeat rw [add_zero]` 将继续将 `? + 0` 更改为 `?`。\n"
|
||||
"* `repeat rw [add_zero]` 将重复把 `? + 0` 更改为 `?`。\n"
|
||||
"直到没有更多匹配的 `? + 0`。\n"
|
||||
"\n"
|
||||
"* `nth_rewrite 2 [h]` 只会将目标中的第二个 `X` 改为 `Y`。\n"
|
||||
"\n"
|
||||
"#### 示例：\n"
|
||||
"### 示例：\n"
|
||||
"\n"
|
||||
"如果假设为 `h : x = y + y`，目标为\n"
|
||||
"```.\n"
|
||||
"```\n"
|
||||
"succ (x + 0) = succ (y + y)\n"
|
||||
"```.\n"
|
||||
"```\n"
|
||||
"\n"
|
||||
"则\n"
|
||||
"\n"
|
||||
@@ -289,7 +291,7 @@ msgstr ""
|
||||
"会将目标变为 `succ (y + y) = succ (y + y)`，这\n"
|
||||
"可以用 `rfl` 解决。\n"
|
||||
"\n"
|
||||
"#### 示例：\n"
|
||||
"### 示例：\n"
|
||||
"\n"
|
||||
"你也可以用 `rw` 来改变一个假设。\n"
|
||||
"例如，如果您有两个假设\n"
|
||||
@@ -298,30 +300,26 @@ msgstr ""
|
||||
"h2 : 2 * y = x\n"
|
||||
"```\n"
|
||||
"则 `rw [h1] at h2` 将把 `h2` 变为 `h2 : 2 * y = y + 3`。\n"
|
||||
"-/\n"
|
||||
"\n"
|
||||
"## 常见错误\n"
|
||||
"\n"
|
||||
"* 需要方括号。`rw h` 永远不会正确。\n"
|
||||
"\n"
|
||||
"* 如果 `h` 不是一个 *等式* 的 *证明* （形式为 `A = B` 的定理或假设）、\n"
|
||||
"例如，如果 `h` 是一个函数或蕴涵、\n"
|
||||
"那么 `rw` 就不是您要使用的策略。例如\n"
|
||||
"`rw [P = Q]` 绝对不正确：`P = Q` 是定理*陈述、\n"
|
||||
"而不是证明。如果 `h : P = Q` 是证明，那么 `rw [h]` 也可以。\n"
|
||||
"* 如果 `h` 不是一个 *等式* 的 *证明* （形式为 `A = B` 的定理或假设），\n"
|
||||
"比如 `h` 是一个函数或蕴涵，\n"
|
||||
"那么 `rw` 就不是您要使用的策略。再比如\n"
|
||||
"`rw [P = Q]` 绝对不正确，因为`P = Q` 是定理的*陈述*\n"
|
||||
"而不是证明。但如果 `h : P = Q` 是证明，那么 `rw [h]` 是可以用的。\n"
|
||||
"\n"
|
||||
"## 详情\n"
|
||||
"\n"
|
||||
"`rw` 策略是 \"代入 \"的一种方法。有\n"
|
||||
"`rw` 策略是 “代入”的一种方法。有\n"
|
||||
"有两种不同的情况可以使用这种策略。\n"
|
||||
"\n"
|
||||
"1) 基本用法：如果 `h : A = B` 是一个假设或\n"
|
||||
"如果目标包含一个或多个 `A`s，那么 `rw [h]`\n"
|
||||
"会将它们全部改为 `B`。如果没有 OFeTl\n"
|
||||
"如果目标中没有 `A`s。\n"
|
||||
"如果目标包含一个或多个 `A`s，那么 `rw [h]`会将它们全部改为 `B`。如果目标中没有 `A`s，那么策略会报错。\n"
|
||||
"\n"
|
||||
"2) 高级用法：来自定理证明的假设\n"
|
||||
"通常会有缺失。例如 `add_zero`\n"
|
||||
"2) 高级用法：来自定理证明的假设通常会有缺失。例如 `add_zero`\n"
|
||||
"是 `? + 0 = ?` 的证明，因为 `add_zero` 确实是一个函数、\n"
|
||||
"而 `?` 是输入。在这种情况下，`rw` 将在目标中查找\n"
|
||||
"寻找任何形式为 `x + 0` 的子项。\n"
|
||||
@@ -331,21 +329,17 @@ msgstr ""
|
||||
"`(0 + 0) + (x + 0) + (0 + 0) + (x + 0)` 改为\n"
|
||||
"`0 + (x + 0) + 0 + (x + 0)`\n"
|
||||
"\n"
|
||||
"如果您记不起相等证明的名称，请在\n"
|
||||
"右侧的公例列表中查找。\n"
|
||||
"如果您记不起相等证明的名称，请在右侧的定理列表中查找。\n"
|
||||
"\n"
|
||||
"## 目标用法\n"
|
||||
"\n"
|
||||
"如果您的目标是 `b + c + a = b + (a + c)`，而您想将 `a + c` 重写为\n"
|
||||
"为 `c + a`，那么 `rw [add_comm]` 将不起作用，因为 Lean 会先找到另一个加法，然后交换这些输入\n"
|
||||
"加法，并交换这些输入。使用 `rw [add_comm a c]` 来\n"
|
||||
"保证Lean将 `a + c` 改写为 `c + a`。这是因为\n"
|
||||
"`add_comm` 是 `?1 + ?2 = ?2 + ?1` 的证明，`add_comm a` 是 `a + ? = ? + a` 的证明。\n"
|
||||
"是 `a + ? = ? + a` 的证明，而 `add_comm a c` 是 `a + c = c + a` 的证明。\n"
|
||||
"如果您的目标是 `b + c + a = b + (a + c)`，而您想将 `a + c` 重写为为 `c + a`，那么 `rw [add_comm]` 将不起作用，因为 Lean 会先找到另一个加法，然后交换这些输入\n"
|
||||
"加法，并交换这些输入。使用 `rw [add_comm a c]` 来保证Lean将 `a + c` 改写为 `c + a`。这是因为 `add_comm` 是 `?1 + ?2 = ?2 + ?1` 的证明，`add_comm a` 是 `a + ? = ? + a` 的证"
|
||||
"明。\n"
|
||||
"而 `add_comm a c` 是 `a + c = c + a` 的证明。\n"
|
||||
"\n"
|
||||
"如果是 `h : X = Y`，那么 `rw [h]` 将把所有 `X`s 变为 `Y`s。\n"
|
||||
"如果您只想将第 37 次出现的 `X`\n"
|
||||
"改为 `Y`，则执行 `nth_rewrite 37 [h]`。"
|
||||
"如果您只想将第 37 次出现的 `X` 改为 `Y`，那么可以用 `nth_rewrite 37 [h]`。"
|
||||
|
||||
#: Game.Levels.Tutorial.L02rw
|
||||
msgid ""
|
||||
@@ -418,7 +412,8 @@ msgid ""
|
||||
"We do this in Lean by *rewriting* the proof `h`,\n"
|
||||
"using the `rw` tactic."
|
||||
msgstr ""
|
||||
"在这个关卡里，*目标*是证明 $2y=2(x+7)$。现在我们有一条*假设* `h`，它指出 $y = x + 7$。请检查假设列表中是否包含了 `h`。在 Lean 中，`h` 被视为一种假设存在的证据，这有点像 `x` 是一个未知的具体数值。\n"
|
||||
"在这个关卡里，*目标*是证明 $2y=2(x+7)$。现在我们有一条*假设* `h`，它指出 $y = x + 7$。请检查假设列表中是否包含了 `h`。在 Lean 中，`h` 被视为一种假设存在的证据，这有点像 `x` 是"
|
||||
"一个未知的具体数值。\n"
|
||||
"\n"
|
||||
"要想使用 `rfl` 完成证明，我们首先需要对 $y$ 进行替换。在 Lean 中，我们可以通过*重写*证明 `h` 来实现这一点，即使用 `rw` 策略。"
|
||||
|
||||
@@ -716,12 +711,13 @@ msgstr ""
|
||||
"\n"
|
||||
"## 加法的定义\n"
|
||||
"\n"
|
||||
"如何实现将任意数字 $x$ 加到 $37$ 上呢？在这个游戏里，我们只有两种方式生成数字：$0$ 和后继数。因此，为了定义 `37 + x`，我们需要明白 `37 + 0` 和 `37 + succ x` 分别是什么。先从加 `0` 的情况开始探索。\n"
|
||||
"如何实现将任意数字 $x$ 加到 $37$ 上呢？在这个游戏里，我们只有两种方式生成数字：$0$ 和后继数。因此，为了定义 `37 + x`，我们需要明白 `37 + 0` 和 `37 + succ x` 分别是什么。先从"
|
||||
"加 `0` 的情况开始探索。\n"
|
||||
"\n"
|
||||
"### 加 0\n"
|
||||
"\n"
|
||||
"为了让加法操作符合直觉，我们应当*定义* `37 + 0` 为 `37`。更广泛来说，对于任何数字 `a`，我们定义 `a + 0` 应等于 `a`。在 Lean 中，从这个定义直接衍生出的定理被命名为 `add_zero a`。比如，`add_zero 37` 证明了 `37 + 0 = 37`，`add_zero "
|
||||
"x` 证明了 `x + 0 = x`，而 `add_zero` 则证明了 `? + 0 = ?`。\n"
|
||||
"为了让加法操作符合直觉，我们应当*定义* `37 + 0` 为 `37`。更广泛来说，对于任何数字 `a`，我们定义 `a + 0` 应等于 `a`。在 Lean 中，从这个定义直接衍生出的定理被命名为 `add_zero "
|
||||
"a`。比如，`add_zero 37` 证明了 `37 + 0 = 37`，`add_zero x` 证明了 `x + 0 = x`，而 `add_zero` 则证明了 `? + 0 = ?`。\n"
|
||||
"\n"
|
||||
"我们将定理记作 `add_zero x : x + 0 = x`，其中定理的名称位于前面，而定理的表述则位于后面。这和之前在*假设*中的记法很像。"
|
||||
|
||||
@@ -773,7 +769,9 @@ msgid ""
|
||||
"`add_zero c` is a proof of `c + 0 = c` so that was what got rewritten.\n"
|
||||
"You can now change `b + 0` to `b` with `rw [add_zero]` or `rw [add_zero b]`. You\n"
|
||||
"can usually stick to `rw [add_zero]` unless you need real precision."
|
||||
msgstr "`add_zero c` 是 `c + 0 = c` 的证明，所以可以用来改写目标了。现在你可以用 `rw [add_zero]` 或 `rw [add_zero b]` 把 `b + 0` 改成 `b`。您通常可以使用 `rw [add_zero]`，除非你需要精准控制改写的内容。"
|
||||
msgstr ""
|
||||
"`add_zero c` 是 `c + 0 = c` 的证明，所以可以用来改写目标了。现在你可以用 `rw [add_zero]` 或 `rw [add_zero b]` 把 `b + 0` 改成 `b`。您通常可以使用 `rw [add_zero]`，除非你需要精"
|
||||
"准控制改写的内容。"
|
||||
|
||||
#: Game.Levels.Tutorial.L06add_zero2
|
||||
msgid "Let's now learn about Peano's second axiom for addition, `add_succ`."
|
||||
@@ -827,14 +825,15 @@ msgstr ""
|
||||
" `012`（数字）选项卡里\n"
|
||||
"看看你可以用哪些证明重写目标。\n"
|
||||
"\n"
|
||||
"在 Lean 中，每个数字要么是 $0$，要么是某个数字的后继数。我们已经掌握了如何加上 $0$，下一步需要明白如何加上后继数。设想我们已经知道 `37 + d = q`。那么 `37 + succ d` 应该是什么呢？由于 `succ d` 比 `d` 多 $1$，所以 `37 + succ d` 应该"
|
||||
"等于 `succ q`，也就是 `q` 加 $1$。更一般地，`x + succ d` 应等于 `succ (x + d)`。我们把这个规则加为一个引理：\n"
|
||||
"在 Lean 中，每个数字要么是 $0$，要么是某个数字的后继数。我们已经掌握了如何加上 $0$，下一步需要明白如何加上后继数。设想我们已经知道 `37 + d = q`。那么 `37 + succ d` 应该是什么"
|
||||
"呢？由于 `succ d` 比 `d` 多 $1$，所以 `37 + succ d` 应该等于 `succ q`，也就是 `q` 加 $1$。更一般地，`x + succ d` 应等于 `succ (x + d)`。我们把这个规则加为一个引理：\n"
|
||||
"\n"
|
||||
"- `add_succ x d : x + succ d = succ (x + d)`\n"
|
||||
"\n"
|
||||
"当你在证明目标中遇到 `... + succ ...` 形式时，使用 `rw [add_succ]` 来重写通常是一个好策略。\n"
|
||||
"\n"
|
||||
"现在，让我们来证明 `succ n = n + 1`。思考如何先引入 `+ succ` 形式，然后再应用 `rw [add_succ]` 策略。请在右侧“定理”部分的 `+`（代表加法）和 `012`（代表数字）标签页中查找可以用来重写目标的定理。"
|
||||
"现在，让我们来证明 `succ n = n + 1`。思考如何先引入 `+ succ` 形式，然后再应用 `rw [add_succ]` 策略。请在右侧“定理”部分的 `+`（代表加法）和 `012`（代表数字）标签页中查找可以用"
|
||||
"来重写目标的定理。"
|
||||
|
||||
#: Game.Levels.Tutorial.L07add_succ
|
||||
msgid "For all natural numbers $a$, we have $\\operatorname{succ}(a) = a+1$."
|
||||
@@ -858,7 +857,7 @@ msgstr "现在使用`rw [add_zero]`"
|
||||
|
||||
#: Game.Levels.Tutorial.L07add_succ
|
||||
msgid "And finally `rfl`."
|
||||
msgstr "最后是 \"rfl`\"。"
|
||||
msgstr "最后是 `rfl`。"
|
||||
|
||||
#: Game.Levels.Tutorial.L07add_succ
|
||||
msgid "[dramatic music]. Now are you ready to face the first boss of the game?"
|
||||
@@ -991,7 +990,8 @@ msgstr ""
|
||||
"\n"
|
||||
"等等，我们不是已经知道这个了吗？不！我们知道的是 $n+0=n$，但那是 `add_zero`。这里的 `zero_add` 是不同的。\n"
|
||||
"\n"
|
||||
"证明 `0 + n = n` 的难点在于我们没有一个一般的*公式*来表示 `0 + n`，我们只能在知道 `n` 是 `0` 还是后继数后，使用 `add_zero` 和 `add_succ`。`induction` 策略会分解成这两种情况。\n"
|
||||
"证明 `0 + n = n` 的难点在于我们没有一个一般的*公式*来表示 `0 + n`，我们只能在知道 `n` 是 `0` 还是后继数后，使用 `add_zero` 和 `add_succ`。`induction` 策略会分解成这两种情"
|
||||
"况。\n"
|
||||
"\n"
|
||||
"基础情况将要求我们证明 `0 + 0 = 0`，归纳步骤将要求我们证明如果 `0 + d = d` 那么 `0 + succ d = succ d`。因为 `0` 和后继数是构造数字的唯一方式，这将涵盖所有情况。\n"
|
||||
"\n"
|
||||
@@ -1297,7 +1297,8 @@ msgid ""
|
||||
"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 ""
|
||||
"`add_comm b c` 是一个 `b + c = c + b` 的证明。但如果您的目标是 `a + b + c = a + c + b`，那么 `rw [add_comm b c]` 将不起作用！因为目标是 `(a + b) + c = (a + c) + b`，所以目标中*直接*没有 `b + c` 项。\n"
|
||||
"`add_comm b c` 是一个 `b + c = c + b` 的证明。但如果您的目标是 `a + b + c = a + c + b`，那么 `rw [add_comm b c]` 将不起作用！因为目标是 `(a + b) + c = (a + c) + b`，所以目标中"
|
||||
"*直接*没有 `b + c` 项。\n"
|
||||
"\n"
|
||||
"使用结合律和交换律来证明 `add_right_comm`。您不需要使用归纳法。`add_assoc` 移动括号，`add_comm` 移动变量。\n"
|
||||
"\n"
|
||||
@@ -2329,7 +2330,8 @@ msgid ""
|
||||
msgstr ""
|
||||
"## 小结\n"
|
||||
"\n"
|
||||
"如果 `t : P → Q` 是一个 $P\\implies Q$ 的证明，而 `h : P` 是一个 `P` 的证明，那么 `apply t at h` 会将 `h` 转换为证明 `Q`。其原理是，如果您知道 `P` 为真，那么您可以从 `t` 推断出 `Q` 为真。\n"
|
||||
"如果 `t : P → Q` 是一个 $P\\implies Q$ 的证明，而 `h : P` 是一个 `P` 的证明，那么 `apply t at h` 会将 `h` 转换为证明 `Q`。其原理是，如果您知道 `P` 为真，那么您可以从 `t` 推断"
|
||||
"出 `Q` 为真。\n"
|
||||
"\n"
|
||||
"如果*目标*是 `Q`，那么 `apply t` 会“逆向推理”并将目标转换为 `P`。在这里，如果您想证明 `Q`，那么根据 `t`，只需证明 `P` 即可，因此您可以将目标简化为证明 `P`。\n"
|
||||
"\n"
|
||||
@@ -2337,7 +2339,8 @@ msgstr ""
|
||||
"\n"
|
||||
"`succ_inj x y` 是一个 `succ x = succ y → x = y` 的证明。\n"
|
||||
"\n"
|
||||
"因此，如果您有一个假设 `h : succ (a + 37) = succ (b + 42)`，那么 `apply succ_inj at h` 会将 `h` 转换为 `a + 37 = b + 42`。您可以写 `apply succ_inj (a + 37) (b + 42) at h`，但 Lean 足够聪明，可以自行推断出 `succ_inj` 的输入。\n"
|
||||
"因此，如果您有一个假设 `h : succ (a + 37) = succ (b + 42)`，那么 `apply succ_inj at h` 会将 `h` 转换为 `a + 37 = b + 42`。您可以写 `apply succ_inj (a + 37) (b + 42) at h`，但 "
|
||||
"Lean 足够聪明，可以自行推断出 `succ_inj` 的输入。\n"
|
||||
"\n"
|
||||
"### 示例：\n"
|
||||
"\n"
|
||||
@@ -2656,7 +2659,8 @@ msgid ""
|
||||
"So if your goal is `False` then you had better hope that your hypotheses\n"
|
||||
"are contradictory, which they are in this level."
|
||||
msgstr ""
|
||||
"我们仍然不能证明 `2 + 2 ≠ 5`，因为我们还没有讨论 `≠` 的定义。在 Lean 中，`a ≠ b` 是 `a = b → False` 的*符号表示*。这里的 `False` 是一个通用的假命题，`→` 是 Lean 中表示“蕴含”的符号\n"
|
||||
"我们仍然不能证明 `2 + 2 ≠ 5`，因为我们还没有讨论 `≠` 的定义。在 Lean 中，`a ≠ b` 是 `a = b → False` 的*符号表示*。这里的 `False` 是一个通用的假命题，`→` 是 Lean 中表示“蕴含”的"
|
||||
"符号\n"
|
||||
"。\n"
|
||||
"在逻辑学中我们学到，`True → False` 是假的，但 `False → False` 是真的。因此，`X → false` 是 `X` 的逻辑取反。\n"
|
||||
"\n"
|
||||
@@ -3120,7 +3124,8 @@ msgid ""
|
||||
"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 ""
|
||||
"我们现在开始研究一个更高效进行加法计算的算法。回想一下，我们通过递归定义了加法，说明了它对 `0` 和后继者的作用。Lean 的一个公理是递归是从像自然数这样的类型定义函数的有效方式。\n"
|
||||
"我们现在开始研究一个更高效进行加法计算的算法。回想一下，我们通过递归定义了加法，说明了它对 `0` 和后继者的作用。Lean 的一个公理是递归是从像自然数这样的类型定义函数的有效方"
|
||||
"式。\n"
|
||||
"\n"
|
||||
"让我们定义一个从自然数到自然数的新函数 `pred`，它试图从输入中减去 1。定义如下：\n"
|
||||
"\n"
|
||||
@@ -3129,8 +3134,8 @@ msgstr ""
|
||||
"pred (succ n) := n\n"
|
||||
"```\n"
|
||||
"\n"
|
||||
"我们不能从 0 中减去 1，所以我们只是返回一个无用的值。除了这个定义之外，我们还创建了一个新的引理 `pred_succ`，它说 `pred (succ n) = n`。让我们使用这个引理来证明 `succ_inj`，这是皮亚诺假设为公理的定理，我们在没有证明它的情况下已经广"
|
||||
"泛使用了。"
|
||||
"我们不能从 0 中减去 1，所以我们只是返回一个无用的值。除了这个定义之外，我们还创建了一个新的引理 `pred_succ`，它说 `pred (succ n) = n`。让我们使用这个引理来证明 `succ_inj`，这"
|
||||
"是皮亚诺假设为公理的定理，我们在没有证明它的情况下已经广泛使用了。"
|
||||
|
||||
#: Game.Levels.Algorithm.L05pred
|
||||
msgid "`pred_succ n` is a proof of `pred (succ n) = n`."
|
||||
@@ -3269,8 +3274,8 @@ msgstr ""
|
||||
"\n"
|
||||
"*) 如果 `a = succ m` 且 `b = succ n`，那么返回对“`m = n`？”的答案。\n"
|
||||
"\n"
|
||||
"现在我们的任务是*证明*这个算法总能给出正确的答案。证明 `0 = 0` 是 `rfl`。证明 `0 ≠ succ n` 的是 `zero_ne_succ n`，证明 `succ m ≠ 0` 的是 `succ_ne_zero m`。如果有假设 `h : m = n`，那么证明 `succ m = succ n` 可以使用 `rw [h]` 然后 "
|
||||
"`rfl`。这一关是证明我们要做的剩余工作之一：如果 `a ≠ b`，那么 `succ a ≠ succ b`。"
|
||||
"现在我们的任务是*证明*这个算法总能给出正确的答案。证明 `0 = 0` 是 `rfl`。证明 `0 ≠ succ n` 的是 `zero_ne_succ n`，证明 `succ m ≠ 0` 的是 `succ_ne_zero m`。如果有假设 `h : m = "
|
||||
"n`，那么证明 `succ m = succ n` 可以使用 `rw [h]` 然后 `rfl`。这一关是证明我们要做的剩余工作之一：如果 `a ≠ b`，那么 `succ a ≠ succ b`。"
|
||||
|
||||
#: Game.Levels.Algorithm.L07succ_ne_succ
|
||||
msgid ""
|
||||
@@ -3555,8 +3560,8 @@ msgid ""
|
||||
"```"
|
||||
msgstr ""
|
||||
"你是否对 `y` 使用了归纳法？\n"
|
||||
"这里有一个使用 `add_right_cancel` 证明 `add_left_eq_self`的两行证明。如果你想查看它，你可以通过点击右上角的 `</>` 进入编辑器模式，然后只需剪切和粘贴证明，并在其周围移动你的光标，以查看在任何给定点的假设和目标（尽管这样做你会失去自"
|
||||
"己的证明）。点击 `>_` 返回命令行模式。\n"
|
||||
"这里有一个使用 `add_right_cancel` 证明 `add_left_eq_self`的两行证明。如果你想查看它，你可以通过点击右上角的 `</>` 进入编辑器模式，然后只需剪切和粘贴证明，并在其周围移动你的光"
|
||||
"标，以查看在任何给定点的假设和目标（尽管这样做你会失去自己的证明）。点击 `>_` 返回命令行模式。\n"
|
||||
"```\n"
|
||||
"nth_rewrite 2 [← zero_add y]\n"
|
||||
"exact add_right_cancel x 0 y\n"
|
||||
@@ -3674,10 +3679,11 @@ msgstr ""
|
||||
"\n"
|
||||
"`cases` 策略会将一个对象或假设分解为可能的创建方式。\n"
|
||||
"\n"
|
||||
"例如，有时你想分别处理 `b = 0` 和 `b = succ d` 这两种情况，但不需要与 `induction b with d hd` 一起来的归纳假设 `hd`。在这种情况下，你可以使用 `cases b with d`。制造一个数字有两种方式：它要么是零，要么是后继者。所以你最终会得到两个"
|
||||
"目标，一个是 `b = 0`，另一个是 `b = succ d`。\n"
|
||||
"例如，有时你想分别处理 `b = 0` 和 `b = succ d` 这两种情况，但不需要与 `induction b with d hd` 一起来的归纳假设 `hd`。在这种情况下，你可以使用 `cases b with d`。制造一个数字有"
|
||||
"两种方式：它要么是零，要么是后继者。所以你最终会得到两个目标，一个是 `b = 0`，另一个是 `b = succ d`。\n"
|
||||
"\n"
|
||||
"另一个例子：如果你有一个假设 `h : False`，那么你就完成证明了，因为从 `False` 可以推出任何证明。这里 `cases h` 将证明目标，因为没有 *任何* 方法可以证明 `False`！所以你最终会没有目标，意味着你已经证明了一切。"
|
||||
"另一个例子：如果你有一个假设 `h : False`，那么你就完成证明了，因为从 `False` 可以推出任何证明。这里 `cases h` 将证明目标，因为没有 *任何* 方法可以证明 `False`！所以你最终会没"
|
||||
"有目标，意味着你已经证明了一切。"
|
||||
|
||||
#: Game.Levels.AdvAddition.L05add_right_eq_zero
|
||||
msgid ""
|
||||
@@ -3722,7 +3728,8 @@ msgstr ""
|
||||
"\n"
|
||||
"## 示例\n"
|
||||
"\n"
|
||||
"如果 `n : ℕ` 是一个数字，那么 `cases n with d` 会将目标分解成两个目标，一个是 `n` 被替换为 0，另一个是 `n` 被替换为 `succ d`。这对应于数学上的观点，即每个自然数要么是 `0`，要么是一个后继数。\n"
|
||||
"如果 `n : ℕ` 是一个数字，那么 `cases n with d` 会将目标分解成两个目标，一个是 `n` 被替换为 0，另一个是 `n` 被替换为 `succ d`。这对应于数学上的观点，即每个自然数要么是 `0`，要"
|
||||
"么是一个后继数。\n"
|
||||
"\n"
|
||||
"## 示例\n"
|
||||
"\n"
|
||||
@@ -4220,7 +4227,8 @@ msgid ""
|
||||
"I've left hidden hints; if you need them, retry from the beginning\n"
|
||||
"and click on \"Show more help!\""
|
||||
msgstr ""
|
||||
"我认为这是迄今为止最难的关卡。提示：如果 `a` 是一个数字，那么 `cases a with b` 会分解为 `a = 0` 和 `a = succ b` 两种情况。不要在你的假设不能保证你能证明最终目标之前选择证明左边或右边！\n"
|
||||
"我认为这是迄今为止最难的关卡。提示：如果 `a` 是一个数字，那么 `cases a with b` 会分解为 `a = 0` 和 `a = succ b` 两种情况。不要在你的假设不能保证你能证明最终目标之前选择证明左"
|
||||
"边或右边！\n"
|
||||
"\n"
|
||||
"我留下了一些隐藏的提示；如果你需要，请从头开始重试并点击“显示更多帮助”！"
|
||||
|
||||
@@ -5048,8 +5056,8 @@ msgstr ""
|
||||
"\n"
|
||||
"## 有问题吗？\n"
|
||||
"\n"
|
||||
"请在 [Lean Zulip 聊天](https://leanprover.zulipchat.com/) 论坛提出关于这个游戏的任何问题，例如在 “新成员” 流中。社区会乐意帮忙。请注意，Lean Zulip 聊天是一个专业研究论坛。请使用您的全名，保持话题相关，且友好。如果你正在寻找一个不那"
|
||||
"么正式的地方（例如，你想发布自然数游戏的表情包），那么可以前往 [Lean Discord](https://discord.gg/WZ9bs9UCvx)。\n"
|
||||
"请在 [Lean Zulip 聊天](https://leanprover.zulipchat.com/) 论坛提出关于这个游戏的任何问题，例如在 “新成员” 流中。社区会乐意帮忙。请注意，Lean Zulip 聊天是一个专业研究论坛。请使"
|
||||
"用您的全名，保持话题相关，且友好。如果你正在寻找一个不那么正式的地方（例如，你想发布自然数游戏的表情包），那么可以前往 [Lean Discord](https://discord.gg/WZ9bs9UCvx)。\n"
|
||||
"\n"
|
||||
"另外，如果你遇到问题/漏洞，你也可以在 github 上提出问题：\n"
|
||||
"\n"
|
||||
|
||||
Reference in New Issue
Block a user