some update based on utensil's suggestion
This commit is contained in:
Hydrogenbear
@@ -57,7 +57,7 @@ msgstr ""
|
||||
"\n"
|
||||
"`rfl` 证明形如 `X = X` 的目标。\n"
|
||||
"\n"
|
||||
"换句话说，如果 `A` 和 `B` *完全相同*，`rfl` 策略将关闭任何形如 `A = B` 的目标。\n"
|
||||
"换句话说，如果 `A` 和 `B` *完全相同*，`rfl` 策略将证明形如 `A = B` 的目标。\n"
|
||||
"\n"
|
||||
"`rfl` 是 “reflexivity（等价关系的反身性）”的缩写。\n"
|
||||
"\n"
|
||||
@@ -69,7 +69,7 @@ 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"
|
||||
@@ -103,7 +103,7 @@ msgstr ""
|
||||
"\n"
|
||||
"# 首先阅读此内容\n"
|
||||
"\n"
|
||||
"这个游戏中的每个关卡都涉及到证明一个数学定理（“目标”）。目标将是关于 *自然数* 的陈述。这个游戏中的一些数有已知的值。这些数有像 $37$ 这样的名字。其他数将是秘密的。它们被称为像 $x$ 和 $q$ 这样的名字。我们知道 $x$ 是一个自然数，我们只是不知道它是哪一个。\n"
|
||||
"这个游戏中的每个关卡都涉及到证明一个数学定理（“目标”）。目标将是关于 *自然数* 的定理。这个游戏中的一些数有已知的值。这些数有像 $37$ 这样的名字。其他数将是秘密的。它们被称为像 $x$ 和 $q$ 这样的名字。我们知道 $x$ 是一个自然数，我们只是不知道它是哪一个。\n"
|
||||
"\n"
|
||||
"在这个第一层中，我们将证明定理 $37x + q = 37x + q$。你可以在下面的*对象*中看到 `x q : ℕ`，这意味着 `x` 和 `q` 是自然数。\n"
|
||||
"\n"
|
||||
@@ -240,7 +240,7 @@ 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"
|
||||
@@ -294,7 +294,7 @@ msgstr ""
|
||||
"\n"
|
||||
"* 需要方括号。`rw h` 永远不会正确。\n"
|
||||
"\n"
|
||||
"* 如果 `h` 不是一个 *等式* 的 *证明* （形式为 `A = B` 的语句）、\n"
|
||||
"* 如果 `h` 不是一个 *等式* 的 *证明* （形式为 `A = B` 的定理或假设）、\n"
|
||||
"例如，如果 `h` 是一个函数或蕴涵、\n"
|
||||
"那么 `rw` 就不是您要使用的策略。例如\n"
|
||||
"`rw [P = Q]` 绝对不正确：`P = Q` 是定理*陈述、\n"
|
||||
@@ -330,8 +330,7 @@ msgstr ""
|
||||
"为 `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` 是 RKKlMOjb8Agf07H9 的证明。\n"
|
||||
"是 `a + ? = ? + a` 的证明，而 `add_comm a c` 是 `a + c = c + a` 的证明。\n"
|
||||
"`add_comm` 是 `?1 + ?2 = ?2 + ?1` 的证明，`add_comm a` 是 `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"
|
||||
@@ -355,7 +354,7 @@ msgid ""
|
||||
"\n"
|
||||
"TacticDoc nth_rewrite \"\n"
|
||||
msgstr ""
|
||||
"## 摘要\n"
|
||||
"## 小结\n"
|
||||
"\n"
|
||||
"`repeat t` 反复应用策略 `t` 到目标上。这个是个可选策略，它只是有时可以节省步骤。\n"
|
||||
"\n"
|
||||
@@ -1210,7 +1209,7 @@ msgstr ""
|
||||
"\n"
|
||||
"【Boss战音乐】\n"
|
||||
"\n"
|
||||
"查看您的库存以查看您拥有的可用定理。\n"
|
||||
"查看您的清单以查看您拥有的可用定理。\n"
|
||||
"这些应该足够了。\n"
|
||||
|
||||
#: Game.Levels.Addition.L03add_comm
|
||||
@@ -2137,7 +2136,7 @@ msgid ""
|
||||
msgstr ""
|
||||
"\n"
|
||||
"一切都结束了！你已经证明了一个困扰了几代学生的定理\n"
|
||||
"（他们中的一些人认为 $(a+b)^2=a^2+b^2$ ：这就是“新生的白日梦”）。\n"
|
||||
"（他们中的一些人认为 $(a+b)^2=a^2+b^2$ ：这就是“新生的错觉”）。\n"
|
||||
"\n"
|
||||
"你用了多少次重写？我可以用12次做到。\n"
|
||||
"\n"
|
||||
@@ -2285,7 +2284,7 @@ msgid ""
|
||||
msgstr ""
|
||||
"## 摘要\n"
|
||||
"\n"
|
||||
"如果目标是语句 `P`，那么如果 `h` 是 `P` 的证明，`exact h` 将关闭目标。\n"
|
||||
"如果目标是 `P`，那么如果 `h` 是 `P` 的证明，`exact h` 将证明目标。\n"
|
||||
"\n"
|
||||
"#### 示例\n"
|
||||
"\n"
|
||||
@@ -2294,14 +2293,14 @@ msgstr ""
|
||||
"\n"
|
||||
"### 示例\n"
|
||||
"\n"
|
||||
"如果目标是 `x + 0 = x`，那么 `exact add_zero x` 将关闭目标。\n"
|
||||
"如果目标是 `x + 0 = x`，那么 `exact add_zero x` 将证明目标。\n"
|
||||
"\n"
|
||||
"### 精确需要完全正确\n"
|
||||
"\n"
|
||||
"请注意，`exact add_zero` 在上例中*不起作用；\n"
|
||||
"请注意，`exact add_zero` 在上例中 *不起作用*；\n"
|
||||
"要让 `exact h` 起作用，`h` 必须*完全*是目标的证明。\n"
|
||||
"`add_zero` 是 `∀ n, n + 0 = n` 的证明，或者，如果你愿意的话、\n"
|
||||
"`? + 0 = ?` 的证明，其中 7qYkdnQ5WeV9ScjLHsz 需要由用户提供。\n"
|
||||
"`? + 0 = ?` 的证明，其中 `?` 需要由用户提供。\n"
|
||||
"这与 `rw` 和 `apply` 不同，它们会在必要时 \"猜测输入\"。\n"
|
||||
"如果需要的话。如果目标是 `x + 0 = x`，那么 `rw [add_zero]`\n"
|
||||
"和 `rw [add_zero x]` 都会将目标改为 `x = x`、\n"
|
||||
@@ -2503,18 +2502,18 @@ msgstr ""
|
||||
"\n"
|
||||
"如果 \\( a \\) 和 \\( b \\) 是数字，那么\n"
|
||||
"`succ_inj a b` 是\n"
|
||||
"\\( (\\operatorname{succ}(a) = \\operatorname{succ}(b))\\implies a=b \\) 的证明。\n"
|
||||
"$ (\\operatorname{succ}(a) = \\operatorname{succ}(b))\\implies a=b $ 的证明。\n"
|
||||
"\n"
|
||||
"## 更多技术细节\n"
|
||||
"\n"
|
||||
"你可以用其他方式思考 `succ_inj`。\n"
|
||||
"\n"
|
||||
"你可以把 `succ_inj` 本身想象成一个函数，它接受两个数字 $$a$$ 和 $$b$$ 作为输入，并输出\n"
|
||||
"\\( (\\operatorname{succ}(a) = \\operatorname{succ}(b))\\implies a=b \\) 的证明。\n"
|
||||
"$ (\\operatorname{succ}(a) = \\operatorname{succ}(b))\\implies a=b $ 的证明。\n"
|
||||
"\n"
|
||||
"你可以把 `succ_inj` 本身看作是一个证明；它是 `succ` 是一个单射函数的证明。换句话说，\n"
|
||||
"`succ_inj` 是\n"
|
||||
"\\( \\forall a, b \\in \\mathbb{N}, (\\operatorname{succ}(a) = \\operatorname{succ}(b))\\implies a=b \\) 的证明。\n"
|
||||
"$ \forall a, b \\in \\mathbb{N}, (\\operatorname{succ}(a) = \\operatorname{succ}(b))\\implies a=b $ 的证明。\n"
|
||||
"\n"
|
||||
"`succ_inj` 被皮亚诺假设为一个公理，但在 Lean 中可以使用 `pred` 来证明，这是一个在数学上有病态的函数。"
|
||||
|
||||
@@ -2680,7 +2679,7 @@ msgstr "现在，用 `exact h ` 完成证明。"
|
||||
|
||||
#: Game.Levels.Implication.L07intro2
|
||||
msgid "intro practice"
|
||||
msgstr "入门练习（译注：翻译存疑，没刷过最新版本，有可能是 `intro` 策略的练习。）"
|
||||
msgstr "练习 `intro` 策略"
|
||||
|
||||
#: Game.Levels.Implication.L07intro2
|
||||
msgid ""
|
||||
@@ -2790,7 +2789,7 @@ msgid ""
|
||||
msgstr ""
|
||||
"`a ≠ b` 是由 `(a = b) → False` 定义的 。\n"
|
||||
"\n"
|
||||
" 这在数学上合法的原因是，如果 `P` 是一个真假陈述，那么 `P → False`\n"
|
||||
" 这在数学上合法的原因是，如果 `P` 是一个真假命题，那么 `P → False`\n"
|
||||
" 与 `P` 的逻辑相反。确实 `True → False` 是假的，\n"
|
||||
" `False → False` 是真的！\n"
|
||||
"\n"
|
||||
@@ -3837,7 +3836,7 @@ msgstr ""
|
||||
"\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`！所以你最终会没有目标，意味着你已经证明了一切。\n"
|
||||
"另一个例子：如果你有一个假设 `h : False`，那么你就完成证明了，因为从 `False` 可以推出任何证明。这里 `cases h` 将证明目标，因为没有 *任何* 方法可以证明 `False`！所以你最终会没有目标，意味着你已经证明了一切。\n"
|
||||
|
||||
#: Game.Levels.AdvAddition.L05add_right_eq_zero
|
||||
msgid ""
|
||||
@@ -4033,7 +4032,7 @@ msgstr ""
|
||||
"\n"
|
||||
"`a ≤ b` 是 `∃ c, b = a + c` 的*符号表示*。这个“倒 E”代表“存在”。所以 `a ≤ b` 意味着存在一个数字 `c` 使得 `b = a + c`。这个定义有效是因为在这个游戏中没有负数。\n"
|
||||
"\n"
|
||||
"要*证明*一个“存在”陈述，可以使用 `use` 策略。\n"
|
||||
"要*证明*一个“存在性”定理，可以使用 `use` 策略。\n"
|
||||
"让我们看一个例子。\n"
|
||||
|
||||
#: Game.Levels.LessOrEqual.L01le_refl
|
||||
@@ -4356,7 +4355,7 @@ msgstr ""
|
||||
"\n"
|
||||
"1) “或”的符号是`∨`。你不需要直接打它，你可以用`\\or`来输入它。\n"
|
||||
"\n"
|
||||
"2) 如果你在 *目标* 中有一个“或”语句，那么有两个策略可以取得进展：`left`和`right`。\n"
|
||||
"2) 如果你在 *目标* 中有一个“或”命题，那么有两个策略可以取得进展：`left`和`right`。\n"
|
||||
"但除非你的知道哪边是真的，否则不要选择一个方向。\n"
|
||||
"\n"
|
||||
"3) 如果你在 *假设* 中有一个“或”语句`h`，那么`cases h with h1 h2`会创建两个目标，一个假设左边是真的，另一个假设右边是真的。\n"
|
||||
@@ -4374,7 +4373,7 @@ msgid ""
|
||||
"Now we can prove the `or` statement by proving the statement on the right,\n"
|
||||
"so use the `right` tactic."
|
||||
msgstr ""
|
||||
"现在我们可以通过证明右边的声明来证明 `or` 语句，\n"
|
||||
"现在我们可以通过证明右边的声明来证明 `or` 命题，\n"
|
||||
"所以使用 `right` 策略。"
|
||||
|
||||
#: Game.Levels.LessOrEqual.L07or_symm
|
||||
@@ -4781,7 +4780,7 @@ msgstr "从用 `cases a with d` 开始，对 `a = 0` 和 `a = succ d` 进行类
|
||||
msgid ""
|
||||
"In the \"base case\" we have a hypothesis `ha : 0 ≠ 0`, and you can deduce anything\n"
|
||||
"from a false statement. The `tauto` tactic will close this goal."
|
||||
msgstr "在“基础情形”中，我们有一个假设 `ha : 0 ≠ 0`，你可以从一个错误的声明中推导出任何东西。`tauto` 策略将关闭这个目标。"
|
||||
msgstr "在“基础情形”中，我们有一个假设 `ha : 0 ≠ 0`，你可以从一个假命题中推导出任何东西。`tauto` 策略将证明这个目标。"
|
||||
|
||||
#: Game.Levels.AdvMultiplication.L04one_le_of_ne_zero
|
||||
msgid "one_le_of_ne_zero"
|
||||
@@ -4801,7 +4800,7 @@ msgstr "通过`apply eq_succ_of_ne_zero at ha`来使用前面的引理。"
|
||||
|
||||
#: Game.Levels.AdvMultiplication.L04one_le_of_ne_zero
|
||||
msgid "Now take apart the existence statement with `cases ha with n hn`."
|
||||
msgstr "现在用 `cases ha with n hn` 分类讨论存在性声明。"
|
||||
msgstr "现在用 `cases ha with n hn` 分类讨论存在性定理。"
|
||||
|
||||
#: Game.Levels.AdvMultiplication.L05le_mul_right
|
||||
msgid "le_mul_right"
|
||||
@@ -5049,7 +5048,7 @@ msgstr ""
|
||||
"\n"
|
||||
"从 `induction b with d hd` 开始太天真了，因为在归纳步骤中，假设是 `a * d = a * c → d = c`，但我们所知的是 `a * succ d = a * c`，所以归纳假设不适用！\n"
|
||||
"\n"
|
||||
"现在假设 `a ≠ 0` 是固定的。我们想要通过对 `b` 进行归纳来证明的实际声明是“对于所有的 `c`，如果 `a * b = a * c` 那么 `b = c`。这*可以*通过归纳来证明，因为我们现在有了改变 `c` 的灵活性。”\n"
|
||||
"现在假设 `a ≠ 0` 是固定的。我们想要通过对 `b` 进行归纳来证明“对于所有的 `c`，如果 `a * b = a * c` 那么 `b = c`。这*可以*通过归纳来证明，因为我们现在有了改变 `c` 的灵活性。”\n"
|
||||
|
||||
#: Game.Levels.AdvMultiplication.L09mul_left_cancel
|
||||
msgid "The way to start this proof is `induction b with d hd generalizing c`."
|
||||
|
||||
Reference in New Issue
Block a user