Merge pull request #5 from subfish-zhou/update

update inductive_type

SUMMARY.md

@@ -21,7 +21,7 @@
 
 [Lean 4 定理证明](./title_page.md)
 
-- [介绍](./introduction.md)
+- [简介](./introduction.md)
 - [依值类型论](./dependent_type_theory.md)
 - [命题与证明](./propositions_and_proofs.md)
 - [量词与等价](./quantifiers_and_equality.md)

conv.md

@@ -1,14 +1,29 @@
+<!--
 The Conversion Tactic Mode
 =========================
+-->
 
+转换策略模式
+=========================
+
+<!--
 Inside a tactic block, one can use the keyword `conv` to enter
 conversion mode. This mode allows to travel inside assumptions and
 goals, even inside function abstractions and dependent arrows, to apply rewriting or
 simplifying steps.
+-->
+
+在策略块中，可以使用关键字`conv`进入转换模式(conversion mode)。这种模式允许在假设和目标内部，甚至在函数抽象和依赖箭头内部移动，以应用重写或简化步骤。
 
+<!--
 Basic navigation and rewriting
 -------
+-->
+
+基本导航和重写
+-------
 
+<!--
 As a first example, let us prove example
 `(a b c : Nat) : a * (b * c) = a * (c * b)`
 (examples in this file are somewhat artificial since
@@ -19,6 +34,16 @@ very first multiplication appearing in the term. There are several
 ways to fix this issue, and one way is to use a more precise tool:
 the conversion mode. The following code block shows the current target
 after each line.
+-->
+
+作为第一个例子，让我们证明`(a b c : Nat) : a * (b * c) = a * (c * b)`（本段中的例子有些刻意设计，因为其他策略可以立即完成它们）。首次简单的尝试是尝试`rw [Nat.mul_comm]`，但这将目标转化为`b * c * a = a * (c * b)`，因为它作用于项中出现的第一个乘法。有几种方法可以解决这个问题，其中一个方法是
+
+```lean
+example (a b c : Nat) : a * (b * c) = a * (c * b) := by
+    rw [Nat.mul_comm b c]
+```
+
+不过本节介绍一个更精确的工具：转换模式。下面的代码块显示了每行之后的当前目标。
 
 ```lean
 example (a b c : Nat) : a * (b * c) = a * (c * b) := by
@@ -33,6 +58,7 @@ example (a b c : Nat) : a * (b * c) = a * (c * b) := by
     rw [Nat.mul_comm]
 ```
 
+<!--
 The above snippet shows three navigation commands:
 
 - `lhs` navigates to the left hand side of a relation (here equality), there is also a `rhs` navigating to the right hand side.
@@ -48,6 +74,17 @@ binders. Suppose we want to prove example
 `(fun x : Nat => 0 + x) = (fun x => x)`.
 The naive first attempt is to enter tactic mode and try
 `rw [Nat.zero_add]`. But this fails with a frustrating
+-->
+
+上面这段涉及三个导航指令：
+
+- `lhs`（left hand side）导航到关系（此处是等式）左边。同理`rhs`导航到右边。
+- `congr`创建与当前头函数的(非依赖的和显式的)参数数量一样多的目标（此处的头函数是乘法）。
+- `skip`走到下一个目标。
+
+一旦到达相关目标，我们就可以像在普通策略模式中一样使用`rw`。
+
+使用转换模式的第二个主要原因是在约束器下重写。假设我们想证明`(fun x : Nat => 0 + x) = (fun x => x)`。首次简单的尝试`rw [zero_add]`是失败的。报错：
 
 ```
 error: tactic 'rewrite' failed, did not find instance of the pattern
@@ -56,7 +93,13 @@ error: tactic 'rewrite' failed, did not find instance of the pattern
 ⊢ (fun x => 0 + x) = fun x => x
 ```
 
+（错误：'rewrite'策略失败了，没有找到目标表达式中的模式0 + ?n）
+
+<!--
 The solution is:
+-->
+
+解决方案为：
 
 ```lean
 example : (fun x : Nat => 0 + x) = (fun x => x) := by
@@ -66,34 +109,59 @@ example : (fun x : Nat => 0 + x) = (fun x => x) := by
     rw [Nat.zero_add]
 ```
 
+<!--
 where `intro x` is the navigation command entering inside the `fun` binder.
 Note that this example is somewhat artificial, one could also do:
+-->
+
+其中`intro x`是导航命令，它进入了`fun`约束器。这个例子有点刻意，你也可以这样做：
 
 ```lean
 example : (fun x : Nat => 0 + x) = (fun x => x) := by
   funext x; rw [Nat.zero_add]
 ```
 
+<!--
 or just
+-->
+
+或者这样：
 
 ```lean
 example : (fun x : Nat => 0 + x) = (fun x => x) := by
   simp
 ```
 
+<!--
 `conv` can also rewrite a hypothesis `h` from the local context, using `conv at h`.
+-->
+
+所有这些也可以用`conv at h`从局部上下文重写一个假设`h`。
 
+<!--
 Pattern matching
 -------
+-->
 
+模式匹配
+-------
+
+<!--
 Navigation using the above commands can be tedious. One can shortcut it using pattern matching as follows:
+-->
+
+使用上面的命令进行导航可能很无聊。使用下面的模式匹配来简化它：
 
 ```lean
 example (a b c : Nat) : a * (b * c) = a * (c * b) := by
   conv in b * c => rw [Nat.mul_comm]
 ```
 
+<!--
 which is just syntax sugar for
+-->
+
+这是下面代码的语法糖：
 
 ```lean
 example (a b c : Nat) : a * (b * c) = a * (c * b) := by
@@ -102,17 +170,30 @@ example (a b c : Nat) : a * (b * c) = a * (c * b) := by
     rw [Nat.mul_comm]
 ```
 
+<!--
 Of course, wildcards are allowed:
+-->
+
+当然也可以用通配符：
 
 ```lean
 example (a b c : Nat) : a * (b * c) = a * (c * b) := by
   conv in _ * c => rw [Nat.mul_comm]
 ```
 
+<!--
 Structuring conversion tactics
 -------
+-->
 
+结构化转换策略
+-------
+
+<!--
 Curly brackets and `.` can also be used in `conv` mode to structure tactics.
+-->
+
+大括号和`.`也可以在`conv`模式下用于结构化策略。
 
 ```lean
 example (a b c : Nat) : (0 + a) * (b * c) = a * (c * b) := by
@@ -123,10 +204,19 @@ example (a b c : Nat) : (0 + a) * (b * c) = a * (c * b) := by
     . rw [Nat.mul_comm]
 ```
 
+<!--
 Other tactics inside conversion mode
 ----------
+-->
+
+转换模式中的其他策略
+----------
 
+<!--
 - `arg i` enter the `i`-th nondependent explicit argument of an application.
+-->
+
+- `arg i`进入一个应用的第`i`个非独立显式参数。
 
 ```lean
 example (a b c : Nat) : a * (b * c) = a * (c * b) := by
@@ -139,9 +229,15 @@ example (a b c : Nat) : a * (b * c) = a * (c * b) := by
     rw [Nat.mul_comm]
 ```
 
+<!--
 - `args` alternative name for `congr`.
 
 - `simp` applies the simplifier to the current goal. It supports the same options available in regular tactic mode.
+-->
+
+- `args`是`congr`的替代品。
+
+- `simp`将简化器应用于当前目标。它支持常规策略模式中的相同选项。
 
 ```lean
 def f (x : Nat) :=
@@ -154,7 +250,11 @@ example (g : Nat → Nat) (h₁ : g x = x + 1) (h₂ : x > 0) : g x = f x := by
   exact h₁
 ```
 
+<!--
 - `enter [1, x, 2, y]` iterate `arg` and `intro` with the given arguments. It is just the macro:
+-->
+
+- `enter [1, x, 2, y]`是`arg`和`intro`使用给定参数的宏。
 
 ```
 syntax enterArg := ident <|> group("@"? num)
@@ -166,6 +266,7 @@ macro_rules
   | `(conv| enter [$arg:enterArg, $args,*]) => `(conv| (enter [$arg]; enter [$args,*]))
 ```
 
+<!--
 - `done` fail if there are unsolved goals.
 
 - `trace_state` display the current tactic state.
@@ -175,6 +276,15 @@ macro_rules
 - `tactic => <tactic sequence>` go back to regular tactic mode. This
   is useful for discharging goals not supported by `conv` mode, and
   applying custom congruence and extensionality lemmas.
+-->
+
+- `done`会失败如果有未解决的目标。
+
+- `traceState`显示当前策略状态。
+
+- `whnf` put term in weak head normal form.
+
+- `tactic => <tactic sequence>`回到常规策略模式。这对于退出`conv`模式不支持的目标，以及应用自定义的一致性和扩展性引理很有用。
 
 ```lean
 example (g : Nat → Nat → Nat)
@@ -192,7 +302,11 @@ example (g : Nat → Nat → Nat)
     . tactic => exact h₂
 ```
 
+<!--
 - `apply <term>` is syntax sugar for `tactic => apply <term>`
+-->
+
+- `apply <term>`是`tactic => apply <term>`的语法糖。
 
 ```lean
 example (g : Nat → Nat → Nat)

dependent_type_theory.md

@@ -1264,7 +1264,7 @@ and the difference between the round and curly braces will be
 explained momentarily.
 -->
 
-这就是*依值函数类型*，或者*依值箭头类型*的一个例子。给定 ``α : Type`` 和 ``β : α → Type``，把 ``β`` 考虑成 ``α`` 之上的类型族，也就是说，对于每个 ``a : α`` 都有类型 ``β a``。在这种情况下，类型 ``(a : α) → β a`` 表示的是具有如下性质的函数 ``f`` 的类型：对于每个 ``a : α``，``f a`` 是 ``β a`` 的一个元素。换句话说，``f`` 返回值的类型取决于其输入。
+这就是*依值函数类型*，或者*依值箭头类型*的一个例子。给定 ``α : Type`` 和 ``β : α → Type``，把 ``β`` 考虑成 ``α`` 之上的类型类，也就是说，对于每个 ``a : α`` 都有类型 ``β a``。在这种情况下，类型 ``(a : α) → β a`` 表示的是具有如下性质的函数 ``f`` 的类型：对于每个 ``a : α``，``f a`` 是 ``β a`` 的一个元素。换句话说，``f`` 返回值的类型取决于其输入。
 
 注意到 ``(a : α) → β`` 对于任意表达式 ``β : Type`` 都有意义。当 ``β`` 的值依赖于 ``a``（例如，在前一段的表达式 ``β a``），``(a : α) → β`` 表示一个依值函数类型。当 ``β`` 的值不依赖于 ``a``，``(a : α) → β`` 与类型 ``α → β`` 无异。实际上，在依值类型论（以及Lean）中，``α → β`` 表达的意思就是当 ``β`` 的值不依赖于 ``a`` 时的 ``(a : α) → β``。【注】