diff --git a/.gitignore b/.gitignore index 1343076..6e39fe2 100644 --- a/.gitignore +++ b/.gitignore @@ -3,4 +3,5 @@ /leanpkg.path out/ .vs/ -.vscode/ \ No newline at end of file +.vscode/ +/src_zh \ No newline at end of file diff --git a/SUMMARY.md b/SUMMARY.md index e922e72..75aa5b1 100644 --- a/SUMMARY.md +++ b/SUMMARY.md @@ -1,3 +1,4 @@ + + +# Lean 4定理证明 + +[Lean 4定理证明](title_page.md) + +- [介绍](./introduction.md) +- [依值类型论](./dependent_type_theory.md) +- [命题和证明](./propositions_and_proofs.md) +- [量词与等价](./quantifiers_and_equality.md) +- [证明策略](./tactics.md) +- [与Lean交互](./interacting_with_lean.md) +- [归纳类型](./inductive_types.md) +- [Induction and Recursion](./induction_and_recursion.md) +- [结构体和记录](./structures_and_records.md) +- [Type Classes](./type_classes.md) +- [转换策略模式](./conv.md) +- [Axioms and Computation](./axioms_and_computation.md) \ No newline at end of file diff --git a/dependent_type_theory.md b/dependent_type_theory.md index 001f166..b99a9df 100644 --- a/dependent_type_theory.md +++ b/dependent_type_theory.md @@ -1,6 +1,11 @@ + + +依值类型论 ===================== + + +依值类型论（Dependent type theory）是一种强大而富有表达力的语言，允许你表达复杂的数学断言，编写复杂的硬件和软件规范，并以自然和统一的方式对这两者进行推理。Lean是基于一个被称为构造演算（Calculus of Constructions）的依值类型论的版本，它拥有一个可数的非累积性宇宙（non-cumulative universe）的层次结构以及归纳类型（Inductive type）。在本章结束时，你将学会一大部分。 + + +## 简单类型论 + +“类型论”得名于其中每个表达式都有一个*类型*。举例：在一个给定的语境中，``x + 0``可能表示一个自然数，``f``可能表示一个定义在自然数上的函数。Lean中的自然数是任意精度的无符号整数。 + + +这里的一些例子展示了如何声明对象以及检查其类型。 + + + +```lean +/- 定义一些常数 -/ +def m : Nat := 1 -- m 是自然数 +def n : Nat := 0 +def b1 : Bool := true -- b1 是布尔型 +def b2 : Bool := false + +/- 检查类型 -/ + +#check m -- 输出: Nat +#check n +#check n + 0 -- Nat +#check m * (n + 0) -- Nat +#check b1 -- Bool +#check b1 && b2 -- "&&" is the Boolean and +#check b1 || b2 -- Boolean or +#check true -- Boolean "true" + +/- 求值（Evaluate） -/ + +#eval 5 * 4 -- 20 +#eval m + 2 -- 3 +#eval b1 && b2 -- false +``` + + +位于``/-``和``-/``之间的文本组成了一个注释块，会被Lean的编译器忽略。类似地，两条横线`--`后面也是注释。注释块可以嵌套，这样就可以“注释掉”一整块代码，这和任何程序语言都是一样的。 + + + +``def``关键字声明工作环境中的新常量符号。在上面的例子中，`def m : Nat := 1`定义了一个`Nat`类型的新常量`m`，其值为`1`。``#check``命令要求Lean给出它的类型，用于向系统询问信息的辅助命令都以井号(#)开头。`#eval`命令让Lean计算给出的表达式。你应该试试自己声明一些常量和检查一些表达式的类型。 + + +简单类型论的强大之处在于，你可以从其他类型中构建新的类型。例如，如果``a``和``b``是类型，``a -> b``表示从``a``到``b``的函数类型，``a × b``表示由``a``元素与``b``元素配对构成的类型，也称为*笛卡尔积*。注意`×`是一个Unicode符号，可以使用``\times``或简写``\tim``来输入。合理使用Unicode提高了易读性，所有现代编辑器都支持它。在Lean标准库中，你经常看到希腊字母表示类型，Unicode符号`→`是`->`的更紧凑版本。 + + +```lean +#check Nat → Nat -- 用"\to" or "\r"来打出这个箭头 +#check Nat -> Nat -- 也可以用 ASCII 符号 +#check Nat × Nat -- 用"\times"打出乘号 +#check Prod Nat Nat -- 换成ASCII 符号 + +#check Nat → Nat → Nat +#check Nat → (Nat → Nat) -- 结果和上一个一样 + +#check Nat × Nat → Nat +#check (Nat → Nat) → Nat -- 一个“泛函” + +#check Nat.succ -- Nat → Nat +#check (0, 1) -- Nat × Nat +#check Nat.add -- Nat → Nat → Nat + +#check Nat.succ 2 -- Nat +#check Nat.add 3 -- Nat → Nat +#check Nat.add 5 2 -- Nat +#check (5, 9).1 -- Nat +#check (5, 9).2 -- Nat + +#eval Nat.succ 2 -- 3 +#eval Nat.add 5 2 -- 7 +#eval (5, 9).1 -- 5 +#eval (5, 9).2 -- 9 +``` + + + +同样，你应该自己尝试一些例子。 + +让我们看一些基本语法。你可以通过输入``\to``或者``\r``或者``\->``来输入``→``。你也可以就用ASCII码``->``，所以表达式``Nat -> Nat``和``Nat → Nat``意思是一样的，都表示以一个自然数作为输入并返回一个自然数作为输出的函数类型。Unicode符号``×``是笛卡尔积，用``\times``输入。小写的希腊字母``α``，``β``，和``γ``等等常用来表示类型变量，可以用``\a``，``\b``，和``\g``来输入。 + +这里还有一些需要注意的事情。第一，函数``f``应用到值``x``上写为``f x``(例：`Nat.succ 2`)。第二，当写类型表达式时，箭头是*右结合*的；例如，``Nat.add``的类型是``Nat → Nat → Nat``，等价于``Nat → (Nat → Nat)``。 + +因此你可以把``Nat.add``看作一个函数，它接受一个自然数并返回另一个函数，该函数接受一个自然数并返回一个自然数。在类型论中，把``Nat.add``函数看作接受一对自然数作为输入并返回一个自然数作为输出的函数通常会更方便。系统允许你“部分应用”函数``Nat.add``，比如``Nat.add 3``具有类型``Nat → Nat``，即``Nat.add 3``返回一个“等待”第二个参数``n``的函数，然后可以继续写``Nat.add 3 n``。 + +> 注：取一个类型为``Nat × Nat → Nat``的函数，然后“重定义”它，让它变成``Nat → Nat → Nat``类型，这个过程被称作*柯里化*（currying）。 + + + +如果你有``m : Nat``和``n : Nat``，那么``(m, n)``表示``m``和``n``组成的有序对，其类型为``Nat × Nat``。这个方法可以制造自然数对。反过来，如果你有``p : Nat × Nat``，之后你可以写``p.1 : Nat``和``p.2 : Nat``。这个方法用于提取它的两个组件。 + + +## 类型作为对象 + + +Lean所依据的依值类型论对简单类型论的其中一项升级是，类型本身（如``Nat``和``Bool``这些东西）也是对象，因此也具有类型。 ```lean #check Nat -- Type @@ -161,8 +277,12 @@ type. #check (Nat → Nat) → Nat ``` + + +上面的每个表达式都是类型为``Type``的对象。你也可以为类型声明新的常量: ```lean def α : Type := Nat @@ -178,8 +298,12 @@ def G : Type → Type → Type := Prod #check G α Nat -- Type ``` + + +正如上面所示，你已经看到了一个类型为``Type → Type → Type``的函数例子，即笛卡尔积 `Prod`： ```lean def α : Type := Nat @@ -192,8 +316,12 @@ def β : Type := Bool #check Nat × Nat -- Type ``` + + +这里有另一个例子：给出任意类型``α``，那么类型``List α``是类型为``α``的元素的列表的类型。 ```lean def α : Type := Nat @@ -202,16 +330,24 @@ def α : Type := Nat #check List Nat -- Type ``` + + +看起来Lean中任何表达式都有一个类型，因此你可能会想到：``Type``自己的类型是什么？ ```lean #check Type -- Type 1 ``` + + +实际上，这是Lean系统的一个最微妙的方面：Lean的底层基础有无限的类型层次： ```lean #check Type -- Type 1 @@ -221,23 +357,30 @@ hierarchy of types: #check Type 4 -- Type 5 ``` + + +可以将``Type 0``看作是一个由“小”或“普通”类型组成的宇宙。然后，``Type 1``是一个更大的类型范围，其中包含``Type 0``作为一个元素，而``Type 2``是一个更大的类型范围，其中包含``Type 1``作为一个元素。这个列表是不确定的，所以对于每个自然数``n``都有一个``Type n``。``Type``是``Type 0``的缩写： ```lean #check Type #check Type 0 ``` - + + +下表可能有助于具体说明所讨论的关系。行方向代表宇宙的变化，列方向代表有时被称为“度”的变化。 | | | | | | | |:------:|:-------------:|:-------------:|:---------------:|:----------------------:|:---:| @@ -246,26 +389,38 @@ along the y-axis represents a change in what is sometimes referred to as | term | trivial | true | fun n => Fin n | fun (_ : Type) => Type | ... | + + +然而，有些操作需要在类型宇宙上具有**多态**（polymorphic）。例如，``List α``应该对任何类型的``α``都有意义，无论``α``存在于哪种类型的宇宙中。所以函数``List``有如下的类型： ```lean #check List -- List.{u} (α : Type u) : Type u ``` + + +这里``u``是一个遍取类型级别的变量。``#check``命令的输出意味着当``α``有类型``Type n``时，``List α``也有类型``Type n``。函数``Prod``具有类似的多态性： ```lean #check Prod -- Prod.{u, v} (α : Type u) (β : Type v) : Type (max u v) ``` + + +你可以使用 `universe` 命令来声明宇宙变量，这样就可以定义多态常量： ```lean universe u @@ -275,7 +430,11 @@ def F (α : Type u) : Type u := Prod α α #check F -- Type u → Type u ``` + + +可以通过在定义F时提供universe参数来避免使用`universe`命令： ```lean def F.{u} (α : Type u) : Type u := Prod α α @@ -284,24 +443,41 @@ def F.{u} (α : Type u) : Type u := Prod α α ``` + + +## 函数抽象和求值 -Lean provides a `fun` (or `λ`) keyword to create a function -from an expression as follows: +Lean提供 `fun` (或 `λ`)关键字用于从给定表达式创建函数，如下所示： + +```lean +#check fun (x : Nat) => x + 5 -- Nat → Nat +#check λ (x : Nat) => x + 5 -- λ 和 fun 是同义词 +#check fun x : Nat => x + 5 -- 同上 +#check λ x : Nat => x + 5 -- 同上 +``` + + + +你可以通过传递所需的参数来计算lambda函数： ```lean #eval (λ x : Nat => x + 5) 10 -- 15 ``` + + +从另一个表达式创建函数的过程称为**lambda 抽象**。假设你有一个变量``x : α``和一个表达式``t : β``，那么表达式``fun (x : α) => t``或者``λ (x : α) => t``是一个类型为``α → β``的对象。这个从``α``到``β``的函数把任意``x``映射到``t``。 + +这有些例子： ```lean #check fun x : Nat => fun y : Bool => if not y then x + 1 else x + 2 @@ -317,12 +498,18 @@ Here are some more examples #check fun x y => if not y then x + 1 else x + 2 -- Nat → Bool → Nat ``` + + +Lean将这三个例子解释为相同的表达式；在最后一个表达式中，Lean可以从表达式`if not y then x + 1 else x + 2`推断``x``和``y``的类型。 + +一些数学上常见的函数运算的例子可以用lambda抽象的项来描述: ```lean def f (n : Nat) : String := toString n @@ -334,6 +521,7 @@ def g (s : String) : Bool := s.length > 0 #check fun x => g (f x) -- Nat → Bool ``` + + +看看这些表达式的意思。表达式``fun x : Nat => x``代表``Nat``上的恒等函数，表达式``fun x : Nat => true``表示一个永远输出``true``的常值函数，表达式``fun x : Nat => g (f x)``表示``f``和``g``的复合。一般来说，你可以省略类型注释，让Lean自己推断它。因此你可以写``fun x => g (f x)``来代替``fun x : Nat => g (f x)``。 + +你可以以函数作为参数，通过给它们命名`f`和`g`，你可以在实现中使用这些函数： ```lean #check fun (g : String → Bool) (f : Nat → String) (x : Nat) => g (f x) -- (String → Bool) → (Nat → String) → Nat → Bool ``` + + +你还可以以类型作为参数： ```lean #check fun (α β γ : Type) (g : β → γ) (f : α → β) (x : α) => g (f x) ``` + + +这个表达式表示一个接受三个类型``α``，``β``和``γ``和两个函数``g : β → γ``和``f : α → β``，并返回的``g``和``f``的复合的函数。(理解这个函数的类型需要理解依值积类型，下面将对此进行解释。) + +lambda表达式的一般形式是``fun x : α => t``，其中变量``x``是一个**绑定变量**（bound variable）：它实际上是一个占位符，其“作用域”没有扩展到表达式``t``之外。例如，表达式``fun (b : β) (x : α) => b``中的变量``b``与前面声明的常量``b``没有任何关系。事实上，这个表达式表示的函数与``fun (u : β) (z : α) => u``是一样的。形式上，可以通过给绑定变量重命名来使形式相同的表达式被看作是**alpha等价**的，也就是被认为是“一样的”。Lean认识这种等价性。 + +注意到项``t : α → β``应用到项``s : α``上导出了表达式``t s : β``。回到前面的例子，为清晰起见给绑定变量重命名，注意以下表达式的类型: ```lean #check (fun x : Nat => x) 1 -- Nat @@ -389,15 +594,20 @@ def g (s : String) : Bool := s.length > 0 -- Bool ``` + + +表达式``(fun x : Nat => x) 1``的类型是``Nat``。实际上，应用``(fun x : Nat => x)``到``1``上返回的值是``1``。 ```lean #eval (fun x : Nat => x) 1 -- 1 #eval (fun x : Nat => true) 1 -- true ``` + + +稍后你将看到这些项是如何计算的。现在，请注意这是依值类型论的一个重要特征：每个项都有一个计算行为，并支持“标准化”的概念。从原则上讲，两个可以化约为相同形式的项被称为“定义等价”。它们被Lean的类型检查器认为是“相同的”，并且Lean尽其所能地识别和支持这些识别结果。 + +Lean是个完备的编程语言。它有一个生成二进制可执行文件的编译器，和一个交互式解释器。你可以用`#eval`命令执行表达式，这也是测试你的函数的好办法。 +> 注意到`#eval`和`#reduce`*不是*等价的。`#eval`命令首先把Lean表达式编译成中间表示（intermediate representation, IR）然后用一个解释器来执行这个IR。某些内建类型（例如，`Nat`、`String`、`Array`）在IR中有更有效率的表示。IR支持使用对Lean不透明的外部函数。 +> ``#reduce``命令建立在一个规约引擎上，类似于在Lean的可信内核中使用的那个，它是负责检查和验证表达式和证明正确性的那一部分。它的效率不如``#eval``，且将所有外部函数视为不透明的常量。之后你将了解到这两个命令之间还有其他一些差异。 + + +## 定义 + + + +``def``关键字提供了一个声明新对象的重要方式。 ```lean def double (x : Nat) : Nat := x + x ``` + + +这很类似其他编程语言中的函数。名字`double`被定义为一个函数，它接受一个类型为`Nat`的输入参数`x`，其结果是`x + x`，因此它返回类型`Nat`。然后你可以调用这个函数: ```lean # def double (x : Nat) : Nat := @@ -450,8 +680,12 @@ can then invoke this function using: #eval double 3 -- 6 ``` + + +在这种情况下你可以把`def`想成一种`lambda`。下面给出了相同的结果： ```lean def double : Nat → Nat := @@ -460,14 +694,19 @@ def double : Nat → Nat := #eval double 3 -- 6 ``` + + +当Lean有足够的信息来推断时，你可以省略类型声明。类型推断是Lean的重要组成部分: ```lean def double := fun (x : Nat) => x + x ``` + + +定义的一般形式是``def foo : α := bar``，其中``α``是表达式``bar``返回的类型。Lean通常可以推断类型``α``，但是精确写出它可以澄清你的意图，并且如果定义的右侧没有匹配你的类型，Lean将标记一个错误。 + +`bar`可以是任何一个表达式，不只是一个lambda表达式。因此`def`也可以用于给一些值命名，例如： + ```lean def pi := 3.141592654 ``` + + +`def`可以接受多个输入参数。比如定义两自然数之和： ```lean def add (x y : Nat) := @@ -492,7 +741,11 @@ def add (x y : Nat) := #eval add 3 2 -- 5 ``` + + +参数列表可以像这样分开写： ```lean # def double (x : Nat) : Nat := @@ -503,10 +756,16 @@ def add (x : Nat) (y : Nat) := #eval add (double 3) (7 + 9) -- 22 ``` + + +注意到这里我们使用了`double`函数来创建`add`函数的第一个参数。 + +你还可以在`def`中写一些更有趣的表达式： ```lean def greater (x y : Nat) := @@ -514,11 +773,17 @@ def greater (x y : Nat) := else y ``` + + +猜猜这个可以做什么。 + +还可以定义一个函数，该函数接受另一个函数作为输入。下面调用一个给定函数两次，将第一次调用的输出传递给第二次: ```lean # def double (x : Nat) : Nat := @@ -529,14 +794,19 @@ def doTwice (f : Nat → Nat) (x : Nat) : Nat := #eval doTwice double 2 -- 8 ``` + + +现在为了更抽象一点，你也可以指定类型参数等： ```lean def compose (α β γ : Type) (g : β → γ) (f : α → β) (x : α) : γ := g (f x) ``` + + +这句代码的意思是：函数`compose`首先接受任何两个函数作为参数，这其中两个函数各自接受一个输入。类型`β → γ`和`α → β`意思是要求第二个函数的输出类型必须与第一个函数的输入类型匹配，否则这两个函数将无法复合。 + +`compose`再接受一个类型为`α`的参数作为第二个函数（这里叫做`f`）的输入，通过这个函数之后的返回结果类型为`β`，再作为第一个函数（这里叫做`g`）的输入。第一个函数返回类型为`γ`，这就是`compose`函数最终返回的类型。 + +`compose`可以在任意的类型`α β γ`上使用，它可以复合任意两个函数，只要前一个的输出类型是后一个的输入类型。举例： ```lean # def compose (α β γ : Type) (g : β → γ) (f : α → β) (x : α) : γ := @@ -566,13 +843,21 @@ def square (x : Nat) : Nat := #eval compose Nat Nat Nat double square 3 -- 18 ``` + + +## 局部定义 + + +Lean还允许你使用``let``关键字来引入“局部定义”。表达式``let a := t1; t2``定义等价于把``t2``中所有的``a``替换成``t1``的结果。 ```lean #check let y := 2 + 2; y * y -- Nat @@ -584,22 +869,34 @@ def twice_double (x : Nat) : Nat := #eval twice_double 2 -- 16 ``` + + +这里``twice_double x``定义等价于``(x + x) * (x + x)``。 + +你可以连续使用多个``let``命令来进行多次替换： ```lean #check let y := 2 + 2; let z := y + y; z * z -- Nat #eval let y := 2 + 2; let z := y + y; z * z -- 64 ``` + + +换行可以省略分号``;``。 + ```lean def t (x : Nat) : Nat := let y := x + x y * y ``` + + +表达式``let a := t1; t2``的意思很类似``(fun a => t2) t1``，但是这两者并不一样。前者中你要把``t2``中每一个``a``的实例考虑成``t1``的一个缩写。后者中``a``是一个变量，表达式``fun a => t2``不依赖于``a``的取值而可以单独具有意义。作为一个对照，考虑为什么下面的``foo``定义是合法的，但``bar``不行（因为在确定了``x``所属的``a``是什么之前，是无法让它``+ 2``的）。 ```lean def foo := let a := Nat; fun x : a => x + 2 @@ -618,9 +918,19 @@ def foo := let a := Nat; fun x : a => x + 2 def bar := (fun a => fun x : a => x + 2) Nat -/ ``` + + +## 变量和小节 + + + +考虑下面这三个函数定义： + ```lean def compose (α β γ : Type) (g : β → γ) (f : α → β) (x : α) : γ := g (f x) @@ -632,8 +942,12 @@ def doThrice (α : Type) (h : α → α) (x : α) : α := h (h (h x)) ``` + + +Lean提供``variable``指令来让这些声明变得紧凑： ```lean variable (α β γ : Type) @@ -647,7 +961,13 @@ def doTwice (h : α → α) (x : α) : α := def doThrice (h : α → α) (x : α) : α := h (h (h x)) ``` + + + +你可以声明任意类型的变量，不只是``Type``类型： + ```lean variable (α β γ : Type) variable (g : β → γ) (f : α → β) (h : α → α) @@ -661,6 +981,8 @@ def doThrice := h (h (h x)) #print doTwice #print doThrice ``` + + + +输出结果表明所有三组定义具有完全相同的效果。 + +``variable``命令指示Lean将声明的变量作为绑定变量插入定义中，这些定义通过名称引用它们。Lean足够聪明，它能找出定义中显式或隐式使用哪些变量。因此在写定义时，你可以将``α``、``β``、``γ``、``g``、``f``、``h``和``x``视为固定的对象，并让Lean自动抽象这些定义。 + +当以这种方式声明时，变量将一直保持存在，直到所处理的文件结束。然而，有时需要限制变量的作用范围。Lean提供了小节标记``section``来实现这个目的： ```lean section useful @@ -689,6 +1018,7 @@ section useful end useful ``` + + +当一个小节结束后，变量不再发挥作用。 +你不需要缩进一个小节中的行。你也不需要命名一个小节，也就是说，你可以使用一个匿名的``section`` /``end``对。但是，如果你确实命名了一个小节，你必须使用相同的名字关闭它。小节也可以嵌套，这允许你逐步增加声明新变量。 + + +## 命名空间 + + + +Lean可以让你把定义放进一个“命名空间”（``namespace``）里，并且命名空间也是层次化的： ```lean namespace Foo @@ -733,6 +1076,7 @@ open Foo #check Foo.fa ``` + + +当你声明你在命名空间``Foo``中工作时，你声明的每个标识符都有一个前缀``Foo.``。在打开的命名空间中，可以通过较短的名称引用标识符，但是关闭命名空间后，必须使用较长的名称。与`section`不同，命名空间需要一个名称。只有一个匿名命名空间在根级别上。 + +``open``命令使你可以在当前使用较短的名称。通常，当你导入一个模块时，你会想打开它包含的一个或多个命名空间，以访问短标识符。但是，有时你希望将这些信息保留在一个完全限定的名称中，例如，当它们与你想要使用的另一个命名空间中的标识符冲突时。因此，命名空间为你提供了一种在工作环境中管理名称的方法。 + +例如，Lean把和列表相关的定义和定理都放在了命名空间``List``之中。 + ```lean #check List.nil #check List.cons #check List.map ``` + + +``open List``命令允许你使用短一点的名字： ```lean open List @@ -763,7 +1119,11 @@ open List #check cons #check map ``` + + +像小节一样，命名空间也是可以嵌套的： ```lean namespace Foo def a : Nat := 5 @@ -790,7 +1150,11 @@ open Foo #check fa #check Bar.ffa ``` + + +关闭的命名空间可以之后重新打开，甚至是在另一个文件里： ```lean namespace Foo @@ -808,6 +1172,7 @@ namespace Foo end Foo ``` + + +与小节一样，嵌套的名称空间必须按照打开的顺序关闭。命名空间和小节有不同的用途：命名空间组织数据，小节声明变量，以便在定义中插入。小节对于分隔``set_option``和``open``等命令的范围也很有用。 + +然而，在许多方面，``namespace ... end``结构块和``section ... end``表现出来的特征是一样的。尤其是你在命名空间中使用``variable``命令时，它的作用范围被限制在命名空间里。类似地，如果你在命名空间中使用``open``命令，它的效果在命名空间关闭后消失。 + + +## 依值类型论“依赖”着什么? + + +简单地说，类型可以依赖于参数。你已经看到了一个很好的例子：类型``List α``依赖于参数``α``，而这种依赖性是区分``List Nat``和``List Bool``的关键。另一个例子，考虑类型``Vector α n``，即长度为``n``的``α``元素的向量类型。这个类型取决于*两个*参数：向量中元素的类型``α : Type``和向量的长度``n : Nat``。 + +假设你希望编写一个函数``cons``，它在列表的开头插入一个新元素。``cons``应该有什么类型？这样的函数是*多态的*（polymorphic）：你期望``Nat``，``Bool``或任意类型``α``的``cons``函数表现相同的方式。因此，将类型作为``cons``的第一个参数是有意义的，因此对于任何类型``α``，``cons α``是类型``α``列表的插入函数。换句话说，对于每个``α``，``cons α``是将元素``a : α``插入列表``as : List α``的函数，并返回一个新的列表，因此有``cons α a as : List α``。 + +很明显，``cons α``具有类型``α → List α → List α``，但是``cons``具有什么类型？如果我们假设是``Type → α → list α → list α``，那么问题在于，这个类型表达式没有意义：``α``没有任何的所指，但它实际上指的是某个类型``Type``。换句话说，*假设*``α : Type``是函数的首个参数，之后的两个参数的类型是``α``和``List α``，它们依赖于首个参数``α``。 ```lean def cons (α : Type) (a : α) (as : List α) : List α := @@ -859,6 +1241,7 @@ def cons (α : Type) (a : α) (as : List α) : List α := #check cons -- (α : Type) → α → List α → List α ``` + + +这就是*依值函数类型*，或者*依值箭头类型*的一个例子。给定``α : Type``和``β : α → Type``，把``β``考虑成``α``之上的类型族，也就是说，对于每个``a : α``都有类型``β a``。在这种情况下，类型``(a : α) → β a``表示的是具有如下性质的函数``f``的类型：对于每个``a : α``，``f a``是``β a``的一个元素。换句话说，``f``返回值的类型取决于其输入。 + +注意到``(a : α) → β``对于任意表达式``β : Type``都有意义。当``β``的值依赖于``a``（例如，在前一段的表达式``β a``），``(a : α) → β``表示一个依值函数类型。当``β``的值不依赖于``a``，``(a : α) → β``与类型``α → β``无异。实际上，在依值类型论（以及Lean）中，``α → β``表达的意思就是当``β``的值不依赖于``a``时的``(a : α) → β``。【注】 + +> 译者注：在依值类型论的数学符号体系中，依值类型是用``Π``符号来表达的，在Lean 3中还使用这种表达，例如``Π x : α, β x``。Lean 4抛弃了这种不友好的写法。``(x : α) → β x``这种写法在引入“构造器”之后意义会更明朗一些（见下一个注释），对于来自数学背景的读者可以把它类比于``forall x : α, β x``这种写法（这也是合法的Lean语句），关于前一种符号在[量词与等价](./quantifiers_and_equality.md)一章中有更详细的说明。同时，依值类型有着更丰富的引入动机，推荐读者寻找一些拓展读物。 + +回到列表的例子，你可以使用`#check`命令来检查下列的`List`函数。``@``符号以及圆括号和花括号之间的区别将在后面解释。 ```lean #check @List.cons -- {α : Type u_1} → α → List α → List α @@ -887,6 +1279,7 @@ explained momentarily. #check @List.append -- {α : Type u_1} → List α → List α → List α ``` + + +就像依值函数类型``(a : α) → β a``通过允许``β``依赖``α``从而推广了函数类型``α → β``，依值笛卡尔积类型``(a : α) × β a``同样推广了笛卡尔积``α × β``。依值积类型又称为*sigma*类型，可写成`Σ a : α, β a`。你可以用`⟨a, b⟩`或者`Sigma.mk a b`来创建依值对。 `⟨`和`⟩`符号可以用`\langle`和`\rangle`或者`\<`和`\>`来输入. ```lean universe u v @@ -915,13 +1311,26 @@ def h2 (x : Nat) : Nat := #eval h2 5 -- 5 ``` + + + +函数`f`和`g`表达的是同样的函数。 + + +## 隐参数 + + +假设我们有一个列表的实现如下： ```lean # universe u @@ -935,7 +1344,11 @@ Suppose we have an implementation of lists as: #check Lst.append -- Lst.append.{u} (α : Type u) (as bs : Lst α) : Lst α ``` + + +然后，你可以建立一个自然数列表如下： ```lean # universe u @@ -955,6 +1368,7 @@ def bs : Lst Nat := Lst.cons Nat 5 (Lst.nil Nat) #check Lst.append Nat as bs ``` + + +由于构造器对类型是多态的【注】，我们需要重复插入类型``Nat``作为一个参数。但是这个信息是多余的：我们可以推断表达式``Lst.cons Nat 5 (Lst.nil Nat)``中参数``α``的类型，这是通过第二个参数``5``的类型是``Nat``来实现的。类似地，我们可以推断``Lst.nil Nat``中参数的类型，这是通过它作为函数``Lst.cons``的一个参数，且这个函数在这个位置需要接收的是一个具有``Lst α``类型的参数来实现的。 + +> 译者注：“构造器”（Constructor）的概念前文未加解释，对类型论不熟悉的读者可能会困惑。它指的是一种“依值类型的类型”，也可以看作“类型的构造器”，例如``λ α : α -> α``甚至可看成``⋆ -> ⋆``。当给``α``或者``⋆``赋予一个具体的类型时，这个表达式就成为了一个类型。前文中``(x : α) → β x``中的``β``就可以看成一个构造器，``(x : α)``就是传进的类型参数。原句“构造器对类型是多态的”意为给构造器中放入不同类型时它会变成不同类型。 + +这是依值类型论的一个主要特征：项包含大量信息，而且通常可以从上下文推断出一些信息。在Lean中，我们使用下划线``_``来指定系统应该自动填写信息。这就是所谓的“隐参数”。 ```lean # universe u @@ -988,11 +1409,15 @@ def bs : Lst Nat := Lst.cons _ 5 (Lst.nil _) #check Lst.append _ as bs ``` + + +然而，敲这么多下划线仍然很无聊。当一个函数接受一个通常可以从上下文推断出来的参数时，Lean允许你指定该参数在默认情况下应该保持隐式。这是通过将参数放入花括号来实现的，如下所示: ```lean universe u @@ -1010,9 +1435,13 @@ def bs : Lst Nat := Lst.cons 5 Lst.nil #check Lst.append as bs ``` + + +唯一改变的是变量声明中``α : Type u``周围的花括号。我们也可以在函数定义中使用这个技巧： ```lean universe u @@ -1024,6 +1453,7 @@ def ident {α : Type u} (x : α) := x #check @ident -- {α : Type u_1} → α → α ``` + + +这使得``ident``的第一个参数是隐式的。从符号上讲，这隐藏了类型的说明，使它看起来好像``ident``只是接受任何类型的参数。事实上，函数``id``在标准库中就是以这种方式定义的。我们在这里选择一个非传统的名字只是为了避免名字的冲突。 + +``variable``命令也可以用这种技巧来来把变量变成隐式的： ```lean universe u @@ -1047,6 +1482,7 @@ end #check ident "hello" ``` + + +此处定义的``ident``和上面那个效果是一样的。 + +Lean有非常复杂的机制来实例化隐参数，我们将看到它们可以用来推断函数类型、谓词，甚至证明。实例化这些“洞”或“占位符”的过程通常被称为**繁饰**（Elaboration）。隐参数的存在意味着有时可能没有足够的信息来精确地确定表达式的含义。像``id``或``List.nil``这样的表达式被认为是“多态的”，因为它可以在不同的上下文中具有不同的含义。 + +可以通过写``(e : T)``来指定表达式``e``的类型``T``。这就指导Lean的繁饰器在试图解决隐式参数时使用值``T``作为``e``的类型。在下面的第二个例子中，这种机制用于指定表达式``id``和``List.nil``所需的类型: ```lean #check List.nil -- List ?m @@ -1075,11 +1518,15 @@ used to specify the desired types of the expressions ``id`` and #check (id : Nat → Nat) -- Nat → Nat ``` + + +Lean中数字是重载的，但是当数字的类型不能被推断时，Lean默认假设它是一个自然数。因此，下面的前两个``#check``命令中的表达式以同样的方式进行了繁饰，而第三个``#check``命令将``2``解释为整数。 ```lean #check 2 -- Nat @@ -1087,11 +1534,15 @@ interprets ``2`` as an integer. #check (2 : Int) -- Int ``` + + +然而，有时我们可能会发现自己处于这样一种情况：我们已经声明了函数的参数是隐式的，但现在想显式地提供参数。如果``foo``是有隐参数的函数，符号``@foo``表示所有参数都是显式的该函数。 ```lean #check @id -- {α : Sort u_1} → α → α @@ -1102,6 +1553,4 @@ made explicit. #check @id Bool true -- Bool ``` -Notice that now the first ``#check`` command gives the type of the -identifier, ``id``, without inserting any placeholders. Moreover, the -output indicates that the first argument is implicit. +第一个``#check``命令给出了标识符的类型``id``，没有插入任何占位符。而且，输出表明第一个参数是隐式的。 diff --git a/deploy b/deploy new file mode 160000 index 0000000..542de18 --- /dev/null +++ b/deploy @@ -0,0 +1 @@ +Subproject commit 542de18886fa27bdde931ba4761d8f22e75d27df diff --git a/interacting_with_lean.md b/interacting_with_lean.md index 19fcd00..e33ca70 100644 --- a/interacting_with_lean.md +++ b/interacting_with_lean.md @@ -1,6 +1,12 @@ + +与Lean交互 +===================== + + + +你现在已经熟悉了依值类型论的基本原理，它既是一种定义数学对象的语言，也是一种构造证明的语言。现在你缺少一个定义新数据类型的机制。下一章介绍*归纳数据类型*的概念来帮你完成这个目标。但首先，在这一章中，我们从类型论的机制中抽身出来，探索与Lean交互的一些实用性问题。 + +并非所有的知识都能马上对你有用。可以略过这一节，然后在必要时再回到这一节以了解Lean的特性。 + +导入文件 +--------------- + + + +Lean的前端的目标是解释用户的输入，构建形式化的表达式，并检查它们是否形式良好和类型正确。Lean还支持使用各种编辑器，这些编辑器提供持续的检查和反馈。更多信息可以在Lean[文档](https://lean-lang.org/documentation/)上找到。 + +Lean的标准库中的定义和定理分布在多个文件中。用户也可能希望使用额外的库，或在多个文件中开发自己的项目。当Lean启动时，它会自动导入库中`Init`文件夹的内容，其中包括一些基本定义和结构。因此，我们在这里介绍的大多数例子都是“开箱即用”的。 + +然而，如果你想使用其他文件，需要通过文件开头的`import'语句手动导入。命令 ``` import Bar.Baz.Blah ``` + +导入文件``Bar/Baz/Blah.olean``，其中的描述是相对于Lean**搜索路径**解释的。关于如何确定搜索路径的信息可以在[文档](https://lean-lang.org/documentation/)中找到。默认情况下，它包括标准库目录，以及（在某些情况下）用户的本地项目的根目录。 + +导入是传递性的。换句话说，如果你导入了 ``Foo``，并且``Foo``导入了``Bar``，那么你也可以访问``Bar``的内容，而不需要明确导入它。 + + + +小节（续） +---------------- + + +Lean提供了各种分段机制来帮助构造理论。你在[变量和小节](./dependent_type_theory.md#变量和小节)中看到，``section``命令不仅可以将理论中的元素组合在一起，还可以在必要时声明变量，作为定理和定义的参数插入。请记住，`variable`命令的意义在于声明变量，以便在定理中使用，如下面的例子： ```lean section @@ -82,16 +121,26 @@ theorem t2 : double (x * y) = double x * y := by end ``` + + +``double``的定义不需要声明``x``作为参数；Lean检测到这种依赖关系并自动插入。同样，Lean检测到``x``在``t1``和``t2``中的出现，也会自动插入。注意，double**没有**``y``作为参数。变量只包括在实际使用的声明中。 + +命名空间（续） +------------------ + + + +在Lean中，标识符是由层次化的*名称*给出的，如``Foo.Bar.baz``。我们在[命名空间](./dependent_type_theory.md#命名空间)一节中看到，Lean提供了处理分层名称的机制。命令``namespace foo``导致``foo``被添加到每个定义和定理的名称中，直到遇到``end foo``。命令``open foo``然后为以`foo`开头的定义和定理创建临时的**别名**。 ```lean namespace Foo @@ -111,13 +163,21 @@ open Foo #check Foo.bar ``` + + +下面的定义 ```lean def Foo.bar : Nat := 1 ``` + + +被看成一个宏；展开成 ```lean namespace Foo @@ -125,12 +185,16 @@ def bar : Nat := 1 end Foo ``` + + +尽管定理和定义的名称必须是唯一的，但标识它们的别名却不是。当我们打开一个命名空间时，一个标识符可能是模糊的。Lean试图使用类型信息来消除上下文中的含义，但你总是可以通过给出全名来消除歧义。为此，字符串``_root_``是对空前缀的明确表述。 ```lean def String.add (a b : String) : String := @@ -153,7 +217,11 @@ open String #check add Nat Nat -- Type ``` + + +我们可以通过使用``protected``关键字来阻止创建较短的别名： ```lean protected def Foo.bar : Nat := 1 @@ -164,10 +232,16 @@ open Foo #check Foo.bar ``` + + +这通常用于像`Nat.rec`和`Nat.recOn`这样的名称，以防止普通名称的重载。 + +``open``命令允许变量。命令 ```lean open Nat (succ zero gcd) @@ -175,7 +249,11 @@ open Nat (succ zero gcd) #eval gcd 15 6 -- 3 ``` + + +仅对列出的标识符创建了别名。命令 ```lean open Nat hiding succ gcd @@ -184,29 +262,49 @@ open Nat hiding succ gcd #eval Nat.gcd 15 6 -- 3 ``` + + +给``Nat``命名空间中**除了**被列出的标识符都创建了别名。命令 ```lean open Nat renaming mul → times, add → plus #eval plus (times 2 2) 3 -- 7 ``` + + +将`Nat.mul`更名为`times`，`Nat.add`更名为`plus`。 + +有时，将别名从一个命名空间导出到另一个命名空间，或者导出到上一层是很有用的。命令 ```lean export Nat (succ add sub) ``` + + +在当前命名空间中为``succ``、``add``和``sub``创建别名，这样无论何时命名空间被打开，这些别名都可以使用。如果这个命令在名字空间之外使用，那么这些别名会被输出到上一层。 + +属性 +---------- + + + +Lean的主要功能是把用户的输入翻译成形式化的表达式，由内核检查其正确性，然后存储在环境中供以后使用。但是有些命令对环境有其他的影响，或者给环境中的对象分配属性，定义符号，或者声明类型族的实例，如[类型族](./type_classes.md)一章所述。这些命令大多具有全局效应，也就是说，它们不仅在当前文件中保持有效，而且在任何导入它的文件中也保持有效。然而，这类命令通常支持``local``修饰符，这表明它们只在当前``section``或``namespace``关闭前或当前文件结束前有效。 + +在[简化](./tactics.md#简化)一节中，我们看到可以用`[simp]`属性来注释定理，这使它们可以被简化器使用。下面的例子定义了列表的前缀关系，证明了这种关系是自反的，并为该定理分配了`[simp]`属性。 ```lean def isPrefix (l₁ : List α) (l₂ : List α) : Prop := @@ -237,9 +340,15 @@ example : isPrefix [1, 2, 3] [1, 2, 3] := by simp ``` + + +然后简化器通过将其改写为``True``来证明``isPrefix [1, 2, 3] [1, 2, 3]``。 + +你也可以在做出定义后的任何时候分配属性： ```lean # def isPrefix (l₁ : List α) (l₂ : List α) : Prop := @@ -250,9 +359,13 @@ theorem List.isPrefix_self (as : List α) : isPrefix as as := attribute [simp] List.isPrefix_self ``` + + +在所有这些情况下，该属性在任何导入该声明的文件中仍然有效。添加``local``修饰符可以限制范围： ```lean # def isPrefix (l₁ : List α) (l₂ : List α) : Prop := @@ -274,10 +387,14 @@ end -- simp ``` + + +另一个例子，我们可以使用`instance`命令来给`isPrefix`关系分配符号`≤`。该命令将在[类型族](./type_classes.md)中解释，它的工作原理是给相关定义分配一个`[instance]`属性。 ```lean def isPrefix (l₁ : List α) (l₂ : List α) : Prop := @@ -290,7 +407,11 @@ theorem List.isPrefix_self (as : List α) : as ≤ as := ⟨[], by simp⟩ ``` + + +这个分配也可以是局部的： ```lean # def isPrefix (l₁ : List α) (l₂ : List α) : Prop := @@ -311,6 +432,7 @@ end -- ⟨[], by simp⟩ ``` + + +在下面的[符号](#符号)一节中，我们将讨论Lean定义符号的机制，并看到它们也支持``local``修饰符。然而，在[设置选项](#设置选项)一节中，我们将讨论Lean设置选项的机制，它并**不**遵循这种模式：选项**只能**在局部设置，也就是说，它们的范围总是限制在当前小节或当前文件中。 + + +隐参数（续） +-------------------------- + + +在[隐参数](./dependent_type_theory.md#隐参数)一节中，我们看到，如果Lean将术语``t``的类型显示为``{x : α} → β x``，那么大括号表示``x``被标记为``t``的*隐参数*。这意味着每当你写``t``时，就会插入一个占位符，或者说“洞”，这样``t``就会被``@t _``取代。如果你不希望这种情况发生，你必须写``@t``来代替。 + +请注意，隐参数是急于插入的。假设我们定义一个函数``f (x : Nat) {y : Nat} (z : Nat)``。那么，当我们写表达式`f 7`时，没有进一步的参数，它会被解析为`f 7 _`。Lean提供了一个较弱的注释，``{{y : ℕ}}``，它指定了一个占位符只应在后一个显式参数之前添加。这个注释也可以写成``⦃y : Nat⦄``，其中的unicode括号输入方式为``\{{``和``\}}``。有了这个注释，表达式`f 7`将被解析为原样，而`f 7 3`将被解析为``f 7 _ 3``，就像使用强注释一样。 + +为了说明这种区别，请看下面的例子，它表明一个自反的欧几里得关系既是对称的又是传递的。 ```lean def reflexive {α : Type u} (r : α → α → Prop) : Prop := @@ -383,6 +521,7 @@ variable (euclr : euclidean r) #check euclr -- r ?m1 ?m2 → r ?m1 ?m3 → r ?m2 ?m3 ``` + + +这些结果被分解成几个小步骤。``th1``表明自反和欧氏的关系是对称的，``th2``表明对称和欧氏的关系是传递的。然后``th3``结合这两个结果。但是请注意，我们必须手动禁用`th1`、`th2`和`euclr`中的隐参数，否则会插入太多的隐参数。如果我们使用弱隐式参数，这个问题就会消失： ```lean def reflexive {α : Type u} (r : α → α → Prop) : Prop := @@ -429,13 +571,23 @@ variable (euclr : euclidean r) #check euclr -- euclidean r ``` + +还有第三种隐式参数，用方括号表示，``[``和``]``。这些是用于类型族的，在[类型族](./type_classes.md)中解释。 + + + +符号 +-------- + + +Lean中的标识符可以包括任何字母数字字符，包括希腊字母（除了∀、Σ和λ，它们在依值类型论中有特殊的含义）。它们还可以包括下标，可以通过输入``\_``，然后再输入所需的下标字符。 + +Lean的解析器是可扩展的，也就是说，我们可以定义新的符号。 +Lean的语法可以由用户在各个层面进行扩展和定制，从基本的“mixfix”符号到自定义的繁饰器。事实上，所有内置的语法都是使用对用户开放的相同机制和API进行解析和处理的。 在本节中，我们将描述和解释各种扩展点。 + +虽然在编程语言中引入新的符号是一个相对罕见的功能，有时甚至因为它有可能使代码变得模糊不清而被人诟病，但它是形式化的一个宝贵工具，可以在代码中简洁地表达各自领域的既定惯例和符号。 除了基本的符号之外，Lean的能力是将普通的样板代码分解成（良好的）宏，并嵌入整个定制的特定领域语言（DSL，domain specific language），对子问题进行高效和可读的文本编码，这对程序员和证明工程师都有很大的好处。 + + + +### 符号和优先级 + + +最基本的语法扩展命令允许引入新的（或重载现有的）前缀、下缀和后缀运算符： + +```lean +infixl:65 " + " => HAdd.hAdd -- 左结合 +infix:50 " = " => Eq -- 非结合 +infixr:80 " ^ " => HPow.hPow -- 右结合 +prefix:100 "-" => Neg.neg +set_option quotPrecheck false +postfix:max "⁻¹" => Inv.inv +``` + + + +语法： + +运算符种类（其“结合方式”） : 解析优先级 " 新的或现有的符号 " => 这个符号应该翻译成的函数 + +优先级是一个自然数，描述一个运算符与它的参数结合的“紧密程度”，编码操作的顺序。我们可以通过查看上述展开的命令来使之更加精确： ```lean notation:65 lhs:65 " + " rhs:66 => HAdd.hAdd lhs rhs @@ -493,6 +681,7 @@ notation:100 "-" arg:100 => Neg.neg arg notation:1024 arg:1024 "⁻¹" => Inv.inv arg -- `max` is a shorthand for precedence 1024 ``` + + +事实证明，第一个代码块中的所有命令实际上都是命令**宏**，翻译成更通用的`notation`命令。我们将在下面学习如何编写这种宏。 `notation`命令不接受单一的记号，而是接受一个混合的记号序列和有优先级的命名项占位符，这些占位符可以在`=>`的右侧被引用，并将被在该位置解析的相应项所取代。 优先级为`p`的占位符在该处只接受优先级至少为`p`的记号。因此，字符串`a + b + c`不能被解析为等同于`a + (b + c)`，因为`infixl`符号的右侧操作数的优先级比该符号本身大。 相反，`infixr`重用了符号右侧操作数的优先级，所以`a ^ b ^ c` *可以*被解析为`a ^ (b ^ c)`。 注意，如果我们直接使用`notation`来引入一个infix符号，如 ```lean # set_option quotPrecheck false notation:65 lhs:65 " ~ " rhs:65 => wobble lhs rhs ``` + + +在上文没有充分确定结合规则的情况下，Lean的解析器将默认为右结合。 更确切地说，Lean的解析器在存在模糊语法的情况下遵循一个局部的*最长解析*规则：当解析`a ~`中`a ~ b ~ c`的右侧时，它将继续尽可能长的解析（在当前的上下文允许的情况下），不在`b`之后停止，而是同时解析`~ c`。因此该术语等同于`a ~ (b ~ c)`。 + +如上所述，`notation`命令允许我们定义任意的*mixfix*语法，自由地混合记号和占位符。 ```lean # set_option quotPrecheck false @@ -530,28 +728,45 @@ notation:max "(" e ")" => e notation:10 Γ " ⊢ " e " : " τ => Typing Γ e τ ``` + + +没有优先级的占位符默认为`0`，也就是说，它们接受任何优先级的符号来代替它们。如果两个记号重叠，我们再次应用最长解析规则： ```lean notation:65 a " + " b:66 " + " c:66 => a + b - c #eval 1 + 2 + 3 -- 0 ``` + + +新的符号比二进制符号要好，因为后者在连锁之前，会在`1 + 2`之后停止解析。 如果有多个符号接受同一个最长的解析，选择将被推迟到阐述，这将失败，除非正好有一个重载是类型正确的。 + + +强制转换 +--------- + + +在Lean中，自然数的类型``Nat``，与整数的类型``Int``不同。但是有一个函数``Int.ofNat``将自然数嵌入整数中，这意味着我们可以在需要时将任何自然数视为整数。Lean有机制来检测和插入这种**强制转换**。 ```lean variable (m n : Nat) @@ -562,9 +777,15 @@ variable (i j : Int) #check i + m + n -- i + Int.ofNat m + Int.ofNat n : Int ``` + + +显示信息 +---------------------- + + +有很多方法可以让你查询Lean的当前状态以及当前上下文中可用的对象和定理的信息。你已经看到了两个最常见的方法，`#check`和`#eval`。请记住，`#check`经常与`@`操作符一起使用，它使定理或定义的所有参数显式化。此外，你可以使用`#print`命令来获得任何标识符的信息。如果标识符表示一个定义或定理，Lean会打印出符号的类型，以及它的定义。如果它是一个常数或公理，Lean会指出它并显示其类型。 + + +```lean +-- 等式 +#check Eq +#check @Eq +#check Eq.symm +#check @Eq.symm + +#print Eq.symm + +-- 与 +#check And +#check And.intro +#check @And.intro + +-- 自定义函数 +def foo {α : Type u} (x : α) : α := x + #check foo #check @foo #print foo ``` + +设置选项 +--------------- + + + +Lean维护着一些内部变量，用户可以通过设置这些变量来控制其行为。语法如下： ``` set_option ``` + + +有一系列非常有用的选项可以控制Lean的**美观打印**显示项的方式。下列选项的输入值为真或假： ``` pp.explicit : display implicit arguments @@ -616,7 +877,11 @@ pp.universes : display hidden universe parameters pp.notation : display output using defined notations ``` + + +例如，以下设置会产生更长的输出: ```lean set_option pp.explicit true @@ -628,12 +893,16 @@ set_option pp.notation false #check (fun x => x + 1) 1 ``` + + +命令``set_option pp.all true``一次性执行这些设置，而``set_option pp.all false``则恢复到之前的值。当你调试一个证明，或试图理解一个神秘的错误信息时，漂亮地打印额外的信息往往是非常有用的。不过太多的信息可能会让人不知所措，Lean的默认值一般来说对普通的交互是足够的。 + + +使用库 +----------------- + + +为了有效地使用Lean，你将不可避免地需要使用库中的定义和定理。回想一下，文件开头的``import``命令会从其他文件中导入之前编译的结果，而且导入是传递的；如果你导入了``Foo``，``Foo``又导入了``Bar``，那么``Bar``的定义和定理也可以被你利用。但是打开一个命名空间的行为，提供了更短的名字，并没有延续下去。在每个文件中，你需要打开你想使用的命名空间。 + +一般来说，你必须熟悉库和它的内容，这样你就知道有哪些定理、定义、符号和资源可供你使用。下面我们将看到Lean的编辑器模式也可以帮助你找到你需要的东西，但直接研究库的内容往往是不可避免的。Lean的标准库在GitHub上。 - [https://github.com/leanprover/lean4/tree/master/src/Init](https://github.com/leanprover/lean4/tree/master/src/Init) - [https://github.com/leanprover/std4/tree/main/Std](https://github.com/leanprover/std4/tree/main/Std) + + +你可以使用GitHub的浏览器界面查看这些目录和文件的内容。如果你在自己的电脑上安装了Lean，你可以在``lean``文件夹中找到这个库，用你的文件管理器探索它。每个文件顶部的注释标题提供了额外的信息。 + +Lean库的开发者遵循一般的命名准则，以便于猜测你所需要的定理的名称，或者在支持Lean模式的编辑器中用Tab自动补全来找到它，这将在下一节讨论。标识符一般是``camelCase``，而类型是`CamelCase`。对于定理的名称，我们依靠描述性的名称，其中不同的组成部分用`_`分开。通常情况下，定理的名称只是描述结论。 ```lean #check Nat.succ_ne_zero @@ -713,6 +999,7 @@ by `_`s. Often the name of theorem simply describes the conclusion: #check Nat.le_of_succ_le_succ ``` + + +Lean中的标识符可以被组织到分层的命名空间中。例如，命名空间``Nat``中名为``le_of_succ_le_succ``的定理有全称``Nat.le_of_succ_le_succ``，但较短的名称可由命令``open Nat``提供（对于未标记为`protected`的名称）。我们将在[归纳类型](./inductive_types.md)和[结构体和记录](./structures_and_records.md)中看到，在Lean中定义结构体和归纳数据类型会产生相关操作，这些操作存储在与被定义类型同名的命名空间。例如，乘积类型带有以下操作： ```lean #check @Prod.mk @@ -731,6 +1021,7 @@ example, the product type comes with the following operations: #check @Prod.rec ``` + + +第一个用于构建一个对，而接下来的两个，``Prod.fst``和``Prod.snd``，投影两个元素。最后一个，``Prod.rec``，提供了另一种机制，用两个元素的函数来定义乘积上的函数。像``Prod.rec``这样的名字是*受保护*的，这意味着即使``Prod``名字空间是打开的，也必须使用全名。 + +由于命题即类型的对应原则，逻辑连接词也是归纳类型的实例，因此我们也倾向于对它们使用点符号： ```lean #check @And.intro @@ -756,12 +1052,21 @@ for them as well: #check @Eq.subst ``` + + +自动约束隐参数 +----------------- + + +在上一节中，我们已经展示了隐参数是如何使函数更方便使用的。然而，像`compose`这样的函数在定义时仍然相当冗长。宇宙多态的`compose`比之前定义的函数还要啰嗦。 ```lean universe u v w @@ -770,7 +1075,11 @@ def compose {α : Type u} {β : Type v} {γ : Type w} g (f x) ``` + + +你可以通过在定义`compose`时提供宇宙参数来避免使用`universe`命令。 ```lean def compose.{u, v, w} @@ -779,10 +1088,14 @@ def compose.{u, v, w} g (f x) ``` + + +Lean 4支持一个名为**自动约束隐参数**的新特性。它使诸如`compose`这样的函数在编写时更加方便。当Lean处理一个声明的头时，**如果**它是一个小写字母或希腊字母，任何未约束的标识符都会被自动添加为隐式参数。有了这个特性，我们可以把`compose`写成 ```lean def compose (g : β → γ) (f : α → β) (x : α) : γ := @@ -792,27 +1105,51 @@ def compose (g : β → γ) (f : α → β) (x : α) : γ := -- {β : Sort u_1} → {γ : Sort u_2} → {α : Sort u_3} → (β → γ) → (α → β) → α → γ ``` + +请注意，Lean使用`Sort`而不是`Type`推断出了一个更通用的类型。 + +虽然我们很喜欢这个功能，并且在实现Lean时广泛使用，但我们意识到有些用户可能会对它感到不舒服。因此，你可以使用`set_option autoBoundImplicitLocal false`命令将其禁用。 + + +```lean +set_option autoImplicit false +/- 这个定义会报错：`unknown identifier` -/ +-- def compose (g : β → γ) (f : α → β) (x : α) : γ := +-- g (f x) +``` + + + +隐式Lambda +--------------- + + +在Lean 3 stdlib中，我们发现了许多[例子](https://github.com/leanprover/lean/blob/master/library/init/category/reader.lean#L39)包含丑陋的`@`+`_`惯用法。当我们的预期类型是一个带有隐参数的函数类型，而我们有一个常量（例子中的`reader_t.pure`）也需要隐参数时，就会经常使用这个惯用法。在Lean 4中，繁饰器自动引入了lambda来消除隐参数。我们仍在探索这一功能并分析其影响，但到目前为止的结果是非常积极的。下面是上面链接中使用Lean 4隐式lambda的例子。 ```lean # variable (ρ : Type) (m : Type → Type) [Monad m] @@ -821,10 +1158,15 @@ instance : Monad (ReaderT ρ m) where bind := ReaderT.bind ``` + +用户可以通过使用`@`或用包含`{}`或`[]`的约束标记编写的lambda表达式来禁用隐式lambda功能。下面是几个例子 + + + +```lean +# namespace ex2 +def id1 : {α : Type} → α → α := + fun x => x + +def listId : List ({α : Type} → α → α) := + (fun x => x) :: [] + +-- 这个例子中，隐式lambda引入被禁用了，因为在`fun`前使用了`@` +def id2 : {α : Type} → α → α := + @fun α (x : α) => id1 x +def id3 : {α : Type} → α → α := + @fun α x => id1 x + +def id4 : {α : Type} → α → α := + fun x => id1 x + +-- 这个例子中，隐式lambda引入被禁用了，因为使用了绑定记号`{...}` +def id5 : {α : Type} → α → α := + fun {α} x => id1 x +# end ex2 +``` + + + +简单函数语法糖 +------------------------- + + +在Lean 3中，我们可以通过使用小括号从infix运算符中创建简单的函数。例如，`(+1)`是`fun x, x + 1`的语法糖。在Lean 4中，我们用`·`作为占位符来扩展这个符号。这里有几个例子： ```lean # namespace ex3 @@ -879,17 +1255,27 @@ def f (x y z : Nat) := # end ex3 ``` + + +如同在Lean 3中，符号是用圆括号激活的，lambda抽象是通过收集嵌套的`·`创建的。这个集合被嵌套的小括号打断。在下面的例子中创建了两个不同的lambda表达式。 ```lean #check (Prod.mk · (· + 1)) -- fun a => (a, fun b => b + 1) ``` + +命名参数 +--------------- + + + +被命名参数使你可以通过用参数的名称而不是参数列表中的位置来指定参数。 如果你不记得参数的顺序但知道它们的名字，你可以以任何顺序传入参数。当Lean未能推断出一个隐参数时，你也可以提供该参数的值。被命名参数还可以通过识别每个参数所代表的内容来提高你的代码的可读性。 ```lean def sum (xs : List Nat) := @@ -910,8 +1299,12 @@ example {a b : Nat} {p : Nat → Nat → Nat → Prop} (h₁ : p a b b) (h₂ : Eq.subst (motive := fun x => p a x b) h₂ h₁ ``` + + +在下面的例子中，我们说明了被命名参数和默认参数之间的交互。 ```lean def f (x : Nat) (y : Nat := 1) (w : Nat := 2) (z : Nat) := @@ -947,8 +1340,12 @@ example (x : α) : g x = fun (c : α) => x + c := rfl example (x y : α) : g x y = fun (c : α) => x + y + c := rfl ``` + + +你可以使用`..`来提供缺少的显式参数作为`_`。这个功能与被命名参数相结合，对编写模式很有用。下面是一个例子： ```lean inductive Term where @@ -966,8 +1363,12 @@ def getBinderType : Term → Option Term | _ => none ``` + + +当显式参数可以由Lean自动推断时，省略号也很有用，而我们想避免一连串的`_`。 ```lean example (f : Nat → Nat) (a b c : Nat) : f (a + b + c) = f (a + (b + c)) := diff --git a/introduction.md b/introduction.md index ddeb863..9548104 100644 --- a/introduction.md +++ b/introduction.md @@ -1,9 +1,14 @@ Introduction ============ + + +计算机和定理证明 ----------------------------- + + +**形式验证**（Formal verification）是指使用逻辑和计算方法来验证用精确的数学术语表达的命题。这包括普通的数学定理，以及硬件或软件、网络协议、机械和混合系统中的形式命题。在实践中，验证数学命题和验证系统的正确性之间很类似：形式验证用数学术语描述硬件和软件系统，在此基础上验证其命题的正确性，这就像定理证明的过程。相反，一个数学定理的证明可能需要冗长的计算，在这种情况下，验证定理的真实性需要验证计算过程是否出错。 + + +二十世纪的逻辑学发展表明，绝大多数传统证明方法可以化为若干基础系统中的一小套公理和规则。有了这种简化，计算机能以两种方式帮助建立命题：1）它可以帮助寻找一个证明，2）可以帮助验证一个所谓的证明是正确的。 + +**自动定理证明**（Automated theorem proving）着眼于 "寻找" 证明。归结(Resolution)定理证明器、表格法(tableau)定理证明器、快速可满足性求解器(Fast satisfiability solvers)等提供了在命题逻辑和一阶逻辑中验证公式有效性的方法；还有些系统为特定的语言和问题提供搜索和决策程序，例如整数或实数上的线性或非线性表达式；像SMT（Satisfiability modulo theories）这样的架构将通用的搜索方法与特定领域的程序相结合；计算机代数系统和专门的数学软件包提供了进行数学计算或寻找数学对象的手段，这些系统中的计算也可以被看作是一种证明，而这些系统也可以帮助建立数学命题。 + + + +自动推理系统努力追求能力和效率，但往往牺牲稳定性。这样的系统可能会有bug，而且很难保证它们所提供的结果是正确的。相比之下，**交互式定理证明器**（Interactive theorem proving）侧重于 "验证" 证明，要求每个命题都有合适的公理基础的证明来支持。这就设定了非常高的标准：每一条推理规则和每一步计算都必须通过求助于先前的定义和定理来证明，一直到基本公理和规则。事实上，大多数这样的系统提供了精心设计的 "证明对象"，可以传给其他系统并独立检查。构建这样的证明通常需要用户更多的输入和交互，但它可以让你获得更深入、更复杂的证明。 + + +**Lean 定理证明器**旨在融合交互式和自动定理证明，它将自动化工具和方法置于一个支持用户交互和构建完整公理化证明的框架中。它的目标是支持数学推理和复杂系统的推理，并验证这两个领域的命题。 + +Lean的底层逻辑有一个计算的解释，与此同时Lean可以被视为一种编程语言。更重要的是，它可以被看作是一个编写具有精确语义的程序的系统，以及对程序所表示的计算功能进行推理。Lean中也有机制使它能够作为它自己的**元编程语言**，这意味着你可以使用Lean本身实现自动化和扩展Lean的功能。Lean的这些方面将在本教程的配套教程[Lean 4函数式编程](https://www.leanprover.cn/fp-lean-zh/)中进行探讨，本书只介绍计算方面。 + + + +关于 Lean ---------- + + +*Lean* 项目由微软Redmond研究院的Leonardo de Moura在2013年发起，这是个长期项目，自动化方法的潜力会在未来逐步被挖掘。Lean是在[Apache 2.0 license](LICENSE)下发布的，这是一个允许他人自由使用和扩展代码和数学库的许可性开源许可证。 + + + +通常有两种办法来运行Lean。第一个是[网页版本](https://live.lean-lang.org/)：由Javascript编写，包含标准定义和定理库，编辑器会下载到你的浏览器上运行。这是个方便快捷的办法。 +第二种是本地版本：本地版本远快于网页版本，并且非常灵活。Visual Studio Code和Emacs扩展模块给编写和调试证明提供了有力支撑，因此更适合正式使用。源代码和安装方法见[https://github.com/leanprover/lean4/](https://github.com/leanprover/lean4/). + +本教程介绍的是Lean的当前版本：Lean 4。 + + + +关于本书 --------------- + + +本书的目的是教你在Lean中编写和验证证明，并且不太需要针对Lean的基础知识。首先，你将学习Lean所基于的逻辑系统，它是**依值类型论**（Dependent type theory）的一个版本，足以证明几乎所有传统的数学定理，并且有足够的表达能力自然地表示数学定理。更具体地说，Lean是基于具有归纳类型（Inductive type）的构造演算（Calculus of Construction）系统的类型论版本。Lean不仅可以定义数学对象和表达依值类型论的数学断言，而且还可以作为一种语言来编写证明。 + + + +由于完全深入细节的公理证明十分复杂，定理证明的难点在于让计算机尽可能多地填补证明细节。你将通过[依值类型论](dependent_type_theory.md)语言来学习各种方法实现自动证明，例如项重写，以及Lean中的项和表达式的自动简化方法。同样，**繁饰**（Elaboration）和**类型推断**（Type inference）的方法，可以用来支持灵活的代数推理。 + + + +最后，你会学到Lean的一些特性，包括与系统交流的语言，和Lean提供的对复杂理论和数据的管理机制。 + +在本书中你会见到类似下面这样的代码： ```lean theorem and_commutative (p q : Prop) : p ∧ q → q ∧ p := @@ -90,12 +156,17 @@ theorem and_commutative (p q : Prop) : p ∧ q → q ∧ p := show q ∧ p from And.intro hq hp ``` + + +如果你在[VS Code](https://code.visualstudio.com/)中阅读本书，你会看到一个按钮，上面写着“try it!”按下按钮将示例复制到编辑器中，并带有足够的周围上下文，以使代码正确编译。您可以在编辑器中输入内容并修改示例，Lean将在您输入时检查结果并不断提供反馈。我们建议您在阅读后面的章节时，自己运行示例并试验代码。你可以通过使用“Lean 4: Open Documentation View”命令在VS Code中打开本书。 + +致谢 --------------- This tutorial is an open access project maintained on Github. Many people have contributed to the effort, providing diff --git a/propositions_and_proofs.md b/propositions_and_proofs.md index 18a22de..099aa39 100644 --- a/propositions_and_proofs.md +++ b/propositions_and_proofs.md @@ -1,14 +1,29 @@ + +命题和证明 +======================= + + + +前一章你已经看到了在Lean中定义对象和函数的一些方法。在本章中，我们还将开始解释如何用依值类型论的语言来编写数学命题和证明。 + +命题即类型 +--------------------- + + + +证明在依值类型论语言中定义的对象的断言（assertion）的一种策略是在定义语言之上分层断言语言和证明语言。但是，没有理由以这种方式重复使用多种语言：依值类型论是灵活和富有表现力的，我们也没有理由不能在同一个总框架中表示断言和证明。 + +例如，我们可引入一种新类型``Prop``，来表示命题，然后引入用其他命题构造新命题的构造器。 ```lean # def Implies (p q : Prop) : Prop := p → q @@ -33,9 +53,13 @@ variable (p q r : Prop) #check Implies (And p q) (And q p) -- Prop ``` + + +对每个元素``p : Prop``，可以引入另一个类型``Proof p``，作为``p``的证明的类型。“公理”是这个类型中的常值。 ```lean # def Implies (p q : Prop) : Prop := p → q @@ -49,6 +73,7 @@ variable (p q : Prop) #check and_comm p q -- Proof (Implies (And p q) (And q p)) ``` + + +然而，除了公理之外，我们还需要从旧证明中建立新证明的规则。例如，在许多命题逻辑的证明系统中，我们有肯定前件式（modus ponens）推理规则: + +> 如果能证明``Implies p q``和``p``，则能证明``q``。 + +我们可以如下地表示它： ```lean # def Implies (p q : Prop) : Prop := p → q @@ -64,11 +96,19 @@ We could represent this as follows: axiom modus_ponens : (p q : Prop) → Proof (Implies p q) → Proof p → Proof q ``` + + +命题逻辑的自然演绎系统通常也依赖于以下规则： + +> 当假设``p``成立时，如果我们能证明``q``. 则我们能证明``Implies p q``. + +我们可以如下地表示它： ```lean # def Implies (p q : Prop) : Prop := p → q @@ -77,6 +117,7 @@ We could render this as follows: axiom implies_intro : (p q : Prop) → (Proof p → Proof q) → Proof (Implies p q) ``` + + +这个功能让我们可以合理地搭建断言和证明。确定表达式``t``是``p``的证明，只需检查``t``具有类型``Proof p``。 + +可以做一些简化。首先，我们可以通过将``Proof p``和``p``本身合并来避免重复地写``Proof``这个词。换句话说，只要我们有``p : Prop``，我们就可以把``p``解释为一种类型，也就是它的证明类型。然后我们可以把``t : p``读作``t``是``p``的证明。 + +此外，我们可以在``Implies p q``和``p → q``之间来回切换。换句话说，命题``p``和``q``之间的含义对应于一个函数，它将``p``的任何元素接受为``q``的一个元素。因此，引入连接词``Implies``是完全多余的：我们可以使用依值类型论中常见的函数空间构造器``p → q``作为我们的蕴含概念。 + +这是在构造演算（Calculus of Constructions）中遵循的方法，因此在Lean中也是如此。自然演绎证明系统中的蕴含规则与控制函数抽象（abstraction）和应用（application）的规则完全一致，这是*Curry-Howard同构*的一个实例，有时也被称为*命题即类型*。事实上，类型``Prop``是上一章描述的类型层次结构的最底部``Sort 0``的语法糖。此外，``Type u``也只是``Sort (u+1)``的语法糖。``Prop``有一些特殊的特性，但像其他类型宇宙一样，它在箭头构造器下是封闭的:如果我们有``p q : Prop``，那么``p → q : Prop``。 + +至少有两种将命题作为类型来思考的方法。对于那些对逻辑和数学中的构造主义者来说，这是对命题含义的忠实诠释：命题``p``代表了一种数据类型，即构成证明的数据类型的说明。``p``的证明就是正确类型的对象``t : p``。 + +非构造主义者可以把它看作是一种简单的编码技巧。对于每个命题``p``，我们关联一个类型，如果``p``为假，则该类型为空，如果``p``为真，则有且只有一个元素，比如``*``。在后一种情况中，让我们说(与之相关的类型)``p``被*占据*（inhabited）。恰好，函数应用和抽象的规则可以方便地帮助我们跟踪``Prop``的哪些元素是被占据的。所以构造一个元素``t : p``告诉我们``p``确实是正确的。你可以把``p``的占据者想象成“``p``为真”的事实。对``p → q``的证明使用“``p``是真的”这个事实来得到“``q``是真的”这个事实。 + +事实上，如果``p : Prop``是任何命题，那么Lean的内核将任意两个元素``t1 t2 : p``看作定义相等，就像它把``(fun x => t) s``和``t[s/x]``看作定义等价。这就是所谓的“证明无关性”（proof irrelevance）。这意味着，即使我们可以把证明``t : p``当作依值类型论语言中的普通对象，它们除了``p``是真的这一事实之外，没有其他信息。 + +我们所建议的思考“命题即类型”范式的两种方式在一个根本性的方面有所不同。从构造的角度看，证明是抽象的数学对象，它被依值类型论中的合适表达式所*表示*。相反，如果我们从上述编码技巧的角度考虑，那么表达式本身并不表示任何有趣的东西。相反，是我们可以写下它们并检查它们是否有良好的类型这一事实确保了有关命题是真的。换句话说，表达式*本身*就是证明。 +在下面的论述中，我们将在这两种说话方式之间来回切换，有时说一个表达式“构造”或“产生”或“返回”一个命题的证明，有时则简单地说它“是”这样一个证明。这类似于计算机科学家偶尔会模糊语法和语义之间的区别，有时说一个程序“计算”某个函数，有时又说该程序“是”该函数。 + +为了用依值类型论的语言正式表达一个数学断言，我们需要展示一个项``p : Prop``。为了*证明*该断言，我们需要展示一个项``t : p``。Lean的任务，作为一个证明助手，是帮助我们构造这样一个项``t``，并验证它的格式是否良好，类型是否正确。 + + + +## 以“命题即类型”的方式工作 + + +在“命题即类型”范式中，只涉及``→``的定理可以通过lambda抽象和应用来证明。在Lean中，``theorem``命令引入了一个新的定理： ```lean variable {p : Prop} @@ -177,6 +247,7 @@ variable {q : Prop} theorem t1 : p → q → p := fun hp : p => fun hq : q => hp ``` + + +这与上一章中常量函数的定义完全相同，唯一的区别是参数是``Prop``的元素，而不是``Type``的元素。直观地说，我们对``p → q → p``的证明假设``p``和``q``为真，并使用第一个假设(平凡地)建立结论``p``为真。 + +请注意，``theorem``命令实际上是``def``命令的一个翻版：在命题和类型对应下，证明定理``p → q → p``实际上与定义关联类型的元素是一样的。对于内核类型检查器，这两者之间没有区别。 + +然而，定义和定理之间有一些实用的区别。正常情况下，永远没有必要展开一个定理的“定义”；通过证明无关性，该定理的任何两个证明在定义上都是相等的。一旦一个定理的证明完成，通常我们只需要知道该证明的存在；证明是什么并不重要。鉴于这一事实，Lean将证明标记为*不可还原*（irreducible），作为对解析器（更确切地说，是**繁饰器**）的提示，在处理文件时一般不需要展开它。事实上，Lean通常能够并行地处理和检查证明，因为评估一个证明的正确性不需要知道另一个证明的细节。 + +和定义一样，``#print``命令可以展示一个定理的证明。 ```lean # variable {p : Prop} @@ -218,10 +298,14 @@ theorem t1 : p → q → p := fun hp : p => fun hq : q => hp #print t1 ``` + + +注意，lambda抽象``hp : p``和``hq : q``可以被视为``t1``的证明中的临时假设。Lean还允许我们通过``show``语句明确指定最后一个项``hp``的类型。 ```lean # variable {p : Prop} @@ -232,6 +316,7 @@ theorem t1 : p → q → p := show p from hp ``` + + +添加这些额外的信息可以提高证明的清晰度，并有助于在编写证明时发现错误。``show``命令只是注释类型，而且在内部，我们看到的所有关于``t1``的表示都产生了相同的项。 + +与普通定义一样，我们可以将lambda抽象的变量移到冒号的左边： ```lean # variable {p : Prop} @@ -248,7 +338,11 @@ theorem t1 (hp : p) (hq : q) : p := hp #print t1 -- p → q → p ``` + + +现在我们可以把定理``t1``作为一个函数应用。 ```lean # variable {p : Prop} @@ -260,24 +354,43 @@ axiom hp : p theorem t2 : q → p := t1 hp ``` + + +这里，``axiom``声明假定存在给定类型的元素，因此可能会破坏逻辑一致性。例如，我们可以使用它来假设空类型`False`有一个元素： + + +```lean +axiom unsound : False +-- false可导出一切 +theorem ex : 1 = 0 := +False.elim unsound +``` + + +声明“公理”``hp : p``等同于声明``p``为真，正如``hp``所证明的那样。应用定理``t1 : p → q → p``到事实``hp : p``（也就是``p``为真）得到定理``t1 hp : q → p``。 + +回想一下，我们也可以这样写定理``t1``: ```lean theorem t1 {p q : Prop} (hp : p) (hq : q) : p := hp @@ -285,18 +398,26 @@ theorem t1 {p q : Prop} (hp : p) (hq : q) : p := hp #print t1 ``` + + +``t1``的类型现在是``∀ {p q : Prop}, p → q → p``。我们可以把它理解为“对于每一对命题``p q``，我们都有``p → q → p``”。例如，我们可以将所有参数移到冒号的右边： ```lean theorem t1 : ∀ {p q : Prop}, p → q → p := fun {p q : Prop} (hp : p) (hq : q) => hp ``` + + +如果``p``和``q``被声明为变量，Lean会自动为我们推广它们： ```lean variable {p q : Prop} @@ -304,8 +425,12 @@ variable {p q : Prop} theorem t1 : p → q → p := fun (hp : p) (hq : q) => hp ``` + + +事实上，通过命题即类型的对应关系，我们可以声明假设``hp``为``p``，作为另一个变量: ```lean variable {p q : Prop} @@ -314,6 +439,7 @@ variable (hp : p) theorem t1 : q → p := fun (hq : q) => hp ``` + + +Lean检测到证明使用``hp``，并自动添加``hp : p``作为前提。在所有情况下，命令``#print t1``仍然会产生``∀ p q : Prop, p → q → p``。这个类型也可以写成``∀ (p q : Prop) (hp : p) (hq :q), p``，因为箭头仅仅表示一个箭头类型，其中目标不依赖于约束变量。 + +当我们以这种方式推广``t1``时，我们就可以将它应用于不同的命题对，从而得到一般定理的不同实例。 ```lean theorem t1 (p q : Prop) (hp : p) (hq : q) : p := hp @@ -338,12 +469,18 @@ variable (h : r → s) #check t1 (r → s) (s → r) h -- (s → r) → r → s ``` + + +同样，使用命题即类型对应，类型为``r → s``的变量``h``可以看作是``r → s``存在的假设或前提。 + +作为另一个例子，让我们考虑上一章讨论的组合函数，现在用命题代替类型。 ```lean variable (p q r s : Prop) @@ -353,15 +490,26 @@ theorem t2 (h₁ : q → r) (h₂ : p → q) : p → r := show r from h₁ (h₂ h₃) ``` + +作为一个命题逻辑定理，``t2``是什么意思？ + +注意，数字unicode下标输入方式为``\0``，``\1``，``\2``，...。 + + + +## 命题逻辑 + + +Lean定义了所有标准的逻辑连接词和符号。命题连接词有以下表示法: + +| Ascii | Unicode | 编辑器缩写 | 定义 | +|------------|-----------|--------------------------|--------| +| True | | | True | +| False | | | False | +| Not | ¬ | ``\not``, ``\neg`` | Not | +| /\\ | ∧ | ``\and`` | And | +| \\/ | ∨ | ``\or`` | Or | +| -> | → | ``\to``, ``\r``, ``\imp``| | +| <-> | ↔ | ``\iff``, ``\lr`` | Iff | + +它们都接收``Prop``值。 ```lean variable (p q : Prop) @@ -384,6 +547,7 @@ variable (p q : Prop) #check p ∨ q → q ∨ p ``` + + +操作符的优先级如下：``¬ > ∧ > ∨ > → > ↔``。举例：``a ∧ b → c ∨ d ∧ e``意为``(a ∧ b) → (c ∨ (d ∧ e))``。``→``等二元关系是右结合的。所以如果我们有``p q r : Prop``，表达式``p → q → r``读作“如果``p``，那么如果``q``，那么``r``”。这是``p ∧ q → r``的柯里化形式。 + +在上一章中，我们观察到lambda抽象可以被看作是``→``的“引入规则”，展示了如何“引入”或建立一个蕴含。应用可以看作是一个“消去规则”，展示了如何在证明中“消去”或使用一个蕴含。其他的命题连接词在Lean的库``Prelude.core``文件中定义。(参见[导入文件](./interacting_with_lean.md#_importing_files)以获得关于库层次结构的更多信息)，并且每个连接都带有其规范引入和消去规则。 + +### 合取 + + + +表达式``And.intro h1 h2``是``p ∧ q``的证明，它使用了``h1 : p``和``h2 : q``的证明。通常把``And.intro``称为*合取引入*规则。下面的例子我们使用``And.intro``来创建``p → q → p ∧ q``的证明。 ```lean variable (p q : Prop) @@ -418,6 +595,7 @@ example (hp : p) (hq : q) : p ∧ q := And.intro hp hq #check fun (hp : p) (hq : q) => And.intro hp hq ``` + + +``example``命令声明了一个没有名字也不会永久保存的定理。本质上，它只是检查给定项是否具有指定的类型。它便于说明，我们将经常使用它。 + +表达式``And.left h``从``h : p ∧ q``建立了一个``p``的证明。类似地，``And.right h``是``q``的证明。它们常被称为左或右*合取消去*规则。 ```lean variable (p q : Prop) @@ -434,7 +617,11 @@ example (h : p ∧ q) : p := And.left h example (h : p ∧ q) : q := And.right h ``` + + +我们现在可以证明``p ∧ q → q ∧ p``： ```lean variable (p q : Prop) @@ -443,6 +630,7 @@ example (h : p ∧ q) : q ∧ p := And.intro (And.right h) (And.left h) ``` + + +请注意，引入和消去与笛卡尔积的配对和投影操作类似。区别在于，给定``hp : p``和``hq : q``，``And.intro hp hq``具有类型``p ∧ q : Prop``，而``Prod hp hq``具有类型``p × q : Type``。``∧``和``×``之间的相似性是Curry-Howard同构的另一个例子，但与蕴涵和函数空间构造器不同，在Lean中``∧``和``×``是分开处理的。然而，通过类比，我们刚刚构造的证明类似于交换一对中的元素的函数。 + +我们将在[结构体和记录](./structures_and_records.md)一章中看到Lean中的某些类型是*Structures*，也就是说，该类型是用单个规范的*构造器*定义的，该构造器从一系列合适的参数构建该类型的一个元素。对于每一组``p q : Prop``， ``p ∧ q``就是一个例子:构造一个元素的规范方法是将``And.intro``应用于合适的参数``hp : p``和``hq : q``。Lean允许我们使用*匿名构造器*表示法``⟨arg1, arg2, ...⟩``在此类情况下，当相关类型是归纳类型并可以从上下文推断时。特别地，我们经常可以写入``⟨hp, hq⟩``，而不是``And.intro hp hq``: ```lean variable (p q : Prop) @@ -471,6 +664,7 @@ variable (hp : p) (hq : q) #check (⟨hp, hq⟩ : p ∧ q) ``` + + +尖括号可以用``\<``和``\>``打出来。 + +Lean提供了另一个有用的语法小工具。给定一个归纳类型``Foo``的表达式``e``(可能应用于一些参数)，符号``e.bar``是``Foo.bar e``的缩写。这为访问函数提供了一种方便的方式，而无需打开名称空间。例如，下面两个表达的意思是相同的： ```lean variable (xs : List Nat) @@ -487,9 +686,13 @@ variable (xs : List Nat) #check xs.length ``` + + +给定``h : p ∧ q``，我们可以写``h.left``来表示``And.left h``以及``h.right``来表示``And.right h``。因此我们可以简写上面的证明如下： ```lean variable (p q : Prop) @@ -498,6 +701,7 @@ example (h : p ∧ q) : q ∧ p := ⟨h.right, h.left⟩ ``` + + +在简洁和含混不清之间有一条微妙的界限，以这种方式省略信息有时会使证明更难阅读。但对于像上面这样简单的结构，当``h``的类型和结构的目标很突出时，符号是干净和有效的。 + +像``And.``这样的迭代结构是很常见的。Lean还允许你将嵌套的构造函数向右结合，这样这两个证明是等价的: ```lean variable (p q : Prop) @@ -518,14 +727,26 @@ example (h : p ∧ q) : q ∧ p ∧ q := ⟨h.right, h.left, h.right⟩ ``` + + +这一点也很常用。 + + +### 析取 + + +表达式``Or.intro_left q hp``从证明``hp : p``建立了``p ∨ q``的证明。类似地，``Or.intro_right p hq``从证明``hq : q``建立了``p ∨ q``的证明。这是左右析取（“或”）引入规则。 ```lean variable (p q : Prop) @@ -533,6 +754,7 @@ example (hp : p) : p ∨ q := Or.intro_left q hp example (hq : q) : p ∨ q := Or.intro_right p hq ``` + + +析取消去规则稍微复杂一点。这个想法是，我们可以从``p ∨ q``证明``r``，通过从``p``证明``r``，且从``q``证明``r``。换句话说，它是一种逐情况证明。在表达式``Or.elim hpq hpr hqr``中，``Or.elim``接受三个论证，``hpq : p ∨ q``，``hpr : p → r``和``hqr : q → r``，生成``r``的证明。在下面的例子中，我们使用``Or.elim``证明``p ∨ q → q ∨ p``。 ```lean variable (p q r : Prop) @@ -552,11 +777,15 @@ example (h : p ∨ q) : q ∨ p := show q ∨ p from Or.intro_left p hq) ``` + + +在大多数情况下，``Or.intro_right``和``Or.intro_left``的第一个参数可以由Lean自动推断出来。因此，Lean提供了``Or.inr``和``Or.inl``作为``Or.intro_right _``和``Or.intro_left _``的缩写。因此，上面的证明项可以写得更简洁: ```lean variable (p q r : Prop) @@ -565,6 +794,7 @@ example (h : p ∨ q) : q ∨ p := Or.elim h (fun hp => Or.inr hp) (fun hq => Or.inl hq) ``` + + +Lean的完整表达式中有足够的信息来推断``hp``和``hq``的类型。但是在较长的版本中使用类型注释可以使证明更具可读性，并有助于捕获和调试错误。 + +因为``Or``有两个构造器，所以不能使用匿名构造器表示法。但我们仍然可以写``h.elim``而不是``Or.elim h``，不过你需要注意这些缩写是增强还是降低了可读性： ```lean variable (p q r : Prop) @@ -581,17 +816,27 @@ example (h : p ∨ q) : q ∨ p := h.elim (fun hp => Or.inr hp) (fun hq => Or.inl hq) ``` + + +### 否定和假言 + + + +否定``¬p``真正的定义是``p → False``，所以我们通过从``p``导出一个矛盾来获得``¬p``。类似地，表达式``hnp hp``从``hp : p``和``hnp : ¬p``产生一个``False``的证明。下一个例子用所有这些规则来证明``(p → q) → ¬q → ¬p``。（``¬``符号可以由``\not``或者``\neg``来写出。） ```lean variable (p q : Prop) @@ -601,10 +846,14 @@ example (hpq : p → q) (hnq : ¬q) : ¬p := show False from hnq (hpq hp) ``` + + +连接词``False``只有一个消去规则``False.elim``，它表达了一个事实，即矛盾能导出一切。这个规则有时被称为*ex falso* 【*ex falso sequitur quodlibet*（无稽之谈）的缩写】，或*爆炸原理*。 ```lean variable (p q : Prop) @@ -612,10 +861,14 @@ variable (p q : Prop) example (hp : p) (hnp : ¬p) : q := False.elim (hnp hp) ``` + + +假命题导出任意的事实``q``，是``False.elim``的一个隐参数，而且是自动推断出来的。这种从相互矛盾的假设中推导出任意事实的模式很常见，用``absurd``来表示。 ```lean variable (p q : Prop) @@ -623,7 +876,11 @@ variable (p q : Prop) example (hp : p) (hnp : ¬p) : q := absurd hp hnp ``` + + +证明``¬p → q → (q → p) → r``： ```lean variable (p q r : Prop) @@ -632,17 +889,29 @@ example (hnp : ¬p) (hq : q) (hqp : q → p) : r := absurd (hqp hq) hnp ``` + +顺便说一句，就像``False``只有一个消去规则，``True``只有一个引入规则``True.intro : true``。换句话说，``True``就是真，并且有一个标准证明``True.intro``。 + + + +### 逻辑等价 + + +表达式``Iff.intro h1 h2``从``h1 : p → q``和``h2 : q → p``生成了``p ↔ q``的证明。表达式``Iff.mp h``从``h : p ↔ q``生成了``p → q``的证明。表达式``Iff.mpr h``从``h : p ↔ q``生成了``q → p``的证明。下面是``p ∧ q ↔ q ∧ p``的证明： ```lean variable (p q : Prop) @@ -660,10 +929,14 @@ variable (h : p ∧ q) example : q ∧ p := Iff.mp (and_swap p q) h ``` + + +我们可以用匿名构造器表示法来，从正反两个方向的证明，来构建``p ↔ q``的证明。我们也可以使用``.``符号连接``mp``和``mpr``。因此，前面的例子可以简写如下： ```lean variable (p q : Prop) @@ -674,13 +947,21 @@ theorem and_swap : p ∧ q ↔ q ∧ p := example (h : p ∧ q) : q ∧ p := (and_swap p q).mp h ``` + + +## 引入辅助子目标 + + +这里介绍Lean提供的另一种帮助构造长证明的方法，即``have``结构，它在证明中引入了一个辅助的子目标。下面是一个小例子，改编自上一节: ```lean variable (p q : Prop) @@ -691,6 +972,7 @@ example (h : p ∧ q) : q ∧ p := show q ∧ p from And.intro hq hp ``` + + +在内部，表达式``have h : p := s; t``产生项``(fun (h : p) => t) s``。换句话说，``s``是``p``的证明，``t``是假设``h : p``的期望结论的证明，并且这两个是由lambda抽象和应用组合在一起的。这个简单的方法在构建长证明时非常有用，因为我们可以使用中间的``have``作为通向最终目标的垫脚石。 + +Lean还支持从目标向后推理的结构化方法，它模仿了普通数学文献中“足以说明某某”（suffices to show）的构造。下一个例子简单地排列了前面证明中的最后两行。 ```lean variable (p q : Prop) @@ -713,20 +1000,32 @@ example (h : p ∧ q) : q ∧ p := show q from And.right h ``` + +``suffices hq : q``给出了两条目标。第一，我们需要证明，通过利用附加假设``hq : q``证明原目标``q ∧ p``，这样足以证明``q``，第二，我们需要证明``q``。 + + + +## 经典逻辑 + + +到目前为止，我们看到的引入和消去规则都是构造主义的，也就是说，它们反映了基于命题即类型对应的逻辑连接词的计算理解。普通经典逻辑在此基础上加上了排中律``p ∨ ¬p``（excluded middle, em）。要使用这个原则，你必须打开经典逻辑命名空间。 ```lean open Classical @@ -735,6 +1034,7 @@ variable (p : Prop) #check em p ``` + + +从直觉上看，构造主义的“或”非常强：断言``p ∨ q``等于知道哪个是真实情况。如果``RH``代表黎曼猜想，经典数学家愿意断言``RH ∨ ¬RH``，即使我们还不能断言析取式的任何一端。 + +排中律的一个结果是双重否定消去规则（double-negation elimination, dne）: ```lean open Classical @@ -752,6 +1057,7 @@ theorem dne {p : Prop} (h : ¬¬p) : p := (fun hnp : ¬p => absurd hnp h) ``` + + +双重否定消去规则给出了一种证明任何命题``p``的方法：通过假设``¬p``来推导出``false``，相当于证明了``p``。换句话说，双重否定消除允许反证法，这在构造主义逻辑中通常是不可能的。作为练习，你可以试着证明相反的情况，也就是说，证明``em``可以由``dne``证明。 + +经典公理还可以通过使用``em``让你获得额外的证明模式。例如，我们可以逐情况进行证明: ```lean open Classical @@ -774,7 +1085,11 @@ example (h : ¬¬p) : p := (fun h1 : ¬p => absurd h1 h) ``` + + +或者你可以用反证法来证明： ```lean open Classical @@ -786,11 +1101,15 @@ example (h : ¬¬p) : p := show False from h h1) ``` + + +如果你不习惯构造主义，你可能需要一些时间来了解经典推理在哪里使用。在下面的例子中，它是必要的，因为从一个构造主义的观点来看，知道``p``和``q``不同时真并不一定告诉你哪一个是假的： ```lean # open Classical @@ -805,6 +1124,7 @@ example (h : ¬(p ∧ q)) : ¬p ∨ ¬q := (fun hp : ¬p => Or.inl hp) ``` + + + +稍后我们将看到，构造逻辑中**有**某些情况允许“排中律”和“双重否定消除律”等，而Lean支持在这种情况下使用经典推理，而不依赖于排中律。 +Lean中使用的公理的完整列表见[公理与计算](./axioms_and_computation.md)。 + + + +逻辑命题的例子 + + +Lean的标准库包含了许多命题逻辑的有效语句的证明，你可以自由地在自己的证明中使用这些证明。下面的列表包括一些常见的逻辑等价式。 + + +交换律： 1. ``p ∧ q ↔ q ∧ p`` 2. ``p ∨ q ↔ q ∨ p`` + + +结合律： 3. ``(p ∧ q) ∧ r ↔ p ∧ (q ∧ r)`` 4. ``(p ∨ q) ∨ r ↔ p ∨ (q ∨ r)`` + + +分配律： 5. ``p ∧ (q ∨ r) ↔ (p ∧ q) ∨ (p ∧ r)`` 6. ``p ∨ (q ∧ r) ↔ (p ∨ q) ∧ (p ∨ r)`` + + +其他性质： 7. ``(p → (q → r)) ↔ (p ∧ q → r)`` 8. ``((p ∨ q) → r) ↔ (p → r) ∧ (q → r)`` @@ -851,7 +1201,11 @@ Other properties: 17. ``¬(p ↔ ¬p)`` 18. ``(p → q) → (¬q → ¬p)`` + + +经典推理： 19. ``(p → r ∨ s) → ((p → r) ∨ (p → s))`` 20. ``¬(p ∧ q) → ¬p ∨ ¬q`` @@ -861,6 +1215,7 @@ These require classical reasoning: 24. ``p ∨ ¬p`` 25. ``(((p → q) → p) → p)`` + +``sorry``标识符神奇地生成任何东西的证明，或者提供任何数据类型的对象。当然，作为一种证明方法，它是不可靠的——例如，你可以使用它来证明``False``——并且当文件使用或导入依赖于它的定理时，Lean会产生严重的警告。但它对于增量地构建长证明非常有用。从上到下写证明，用``sorry``来填子证明。确保Lean接受所有的``sorry``；如果不是，则有一些错误需要纠正。然后返回，用实际的证据替换每个``sorry``，直到做完。 + +有另一个有用的技巧。你可以使用下划线``_``作为占位符，而不是``sorry``。回想一下，这告诉Lean该参数是隐式的，应该自动填充。如果Lean尝试这样做并失败了，它将返回一条错误消息“不知道如何合成占位符”（Don't know how to synthesize placeholder），然后是它所期望的项的类型，以及上下文中可用的所有对象和假设。换句话说，对于每个未解决的占位符，Lean报告在那一点上需要填充的子目标。然后，你可以通过递增填充这些占位符来构造一个证明。 + +这里有两个简单的证明例子作为参考。 + + + +```lean +open Classical + +-- 分配律 +example (p q r : Prop) : p ∧ (q ∨ r) ↔ (p ∧ q) ∨ (p ∧ r) := + Iff.intro + (fun h : p ∧ (q ∨ r) => + have hp : p := h.left + Or.elim (h.right) + (fun hq : q => + show (p ∧ q) ∨ (p ∧ r) from Or.inl ⟨hp, hq⟩) + (fun hr : r => + show (p ∧ q) ∨ (p ∧ r) from Or.inr ⟨hp, hr⟩)) + (fun h : (p ∧ q) ∨ (p ∧ r) => + Or.elim h + (fun hpq : p ∧ q => + have hp : p := hpq.left + have hq : q := hpq.right + show p ∧ (q ∨ r) from ⟨hp, Or.inl hq⟩) + (fun hpr : p ∧ r => + have hp : p := hpr.left + have hr : r := hpr.right + show p ∧ (q ∨ r) from ⟨hp, Or.inr hr⟩)) + +-- 需要一点经典推理的例子 +example (p q : Prop) : ¬(p ∧ ¬q) → (p → q) := + fun h : ¬(p ∧ ¬q) => + fun hp : p => + show q from + Or.elim (em q) + (fun hq : q => hq) + (fun hnq : ¬q => absurd (And.intro hp hnq) h) +``` + +## 练习 + + + +证明以下等式，用真实证明取代“sorry”占位符。 + + +```lean +variable (p q r : Prop) + +-- ∧ 和 ∨ 的交换律 +example : p ∧ q ↔ q ∧ p := sorry +example : p ∨ q ↔ q ∨ p := sorry +-- ∧ 和 ∨ 的结合律 +example : (p ∧ q) ∧ r ↔ p ∧ (q ∧ r) := sorry +example : (p ∨ q) ∨ r ↔ p ∨ (q ∨ r) := sorry + +-- 分配律 +example : p ∧ (q ∨ r) ↔ (p ∧ q) ∨ (p ∧ r) := sorry +example : p ∨ (q ∧ r) ↔ (p ∨ q) ∧ (p ∨ r) := sorry + +-- 其他性质 +example : (p → (q → r)) ↔ (p ∧ q → r) := sorry +example : ((p ∨ q) → r) ↔ (p → r) ∧ (q → r) := sorry +example : ¬(p ∨ q) ↔ ¬p ∧ ¬q := sorry +example : ¬p ∨ ¬q → ¬(p ∧ q) := sorry +example : ¬(p ∧ ¬p) := sorry +example : p ∧ ¬q → ¬(p → q) := sorry +example : ¬p → (p → q) := sorry +example : (¬p ∨ q) → (p → q) := sorry +example : p ∨ False ↔ p := sorry +example : p ∧ False ↔ False := sorry +example : (p → q) → (¬q → ¬p) := sorry +``` + + + +下面这些需要一点经典逻辑。 ```lean open Classical @@ -970,4 +1411,8 @@ example : p ∨ ¬p := sorry example : (((p → q) → p) → p) := sorry ``` + + +最后，证明``¬(p ↔ ¬p)``且不使用经典逻辑。 diff --git a/quantifiers_and_equality.md b/quantifiers_and_equality.md index 6439c22..8d23c95 100644 --- a/quantifiers_and_equality.md +++ b/quantifiers_and_equality.md @@ -1,14 +1,29 @@ + +量词与等价 +======================== + + +上一章介绍了构造包含命题连接词的证明方法。在本章中，我们扩展逻辑结构，包括全称量词和存在量词，以及等价关系。 + + + +全称量词 +------------------------ + + +如果``α``是任何类型，我们可以将``α``上的一元谓词``p``作为``α → Prop``类型的对象。在这种情况下，给定``x : α``， ``p x``表示断言``p``在``x``上成立。类似地，一个对象``r : α → α → Prop``表示``α``上的二元关系：给定``x y : α``，``r x y``表示断言``x``与``y``相关。 + +全称量词``∀ x : α, p x``表示，对于每一个``x : α``，``p x``成立。与命题连接词一样，在自然演绎系统中，“forall”有引入和消去规则。非正式地，引入规则是： + +> 给定``p x``的证明，在``x : α``是任意的情况下，我们得到``∀ x : α, p x``的证明。 + +消去规则是： + +> 给定``∀ x : α, p x``的证明和任何项``t : α``，我们得到``p t``的证明。 + +与蕴含的情况一样，命题即类型。回想依值箭头类型的引入规则: + +> 给定类型为``β x``的项``t``，在``x : α``是任意的情况下，我们有``(fun x : α => t) : (x : α) → β x``。 + +消去规则： + +> 给定项``s : (x : α) → β x``和任何项``t : α``，我们有``s t : β t``。 + +在``p x``具有``Prop``类型的情况下，如果我们用``∀ x : α, p x``替换``(x : α) → β x``，就得到构建涉及全称量词的证明的规则。 + +因此，构造演算用全称表达式来识别依值箭头类型。如果``p``是任何表达式，``∀ x : α, p``不过是``(x : α) → p``的替代符号，在``p``是命题的情况下，前者比后者更自然。通常，表达式``p``取决于``x : α``。回想一下，在普通函数空间中，我们可以将``α → β``解释为``(x : α) → β``的特殊情况，其中``β``不依赖于``x``。类似地，我们可以把命题之间的蕴涵``p → q``看作是``∀ x : p, q``的特殊情况，其中``q``不依赖于``x``。 + +下面是一个例子，说明了如何运用命题即类型对应规则。``∀``可以用``\forall``输入，也可以用前两个字母简写``\fo``。 ```lean example (α : Type) (p q : α → Prop) : (∀ x : α, p x ∧ q x) → ∀ y : α, p y := @@ -63,6 +103,7 @@ example (α : Type) (p q : α → Prop) : (∀ x : α, p x ∧ q x) → ∀ y : show p y from (h y).left ``` + + +作为一种符号约定，我们给予全称量词尽可能最宽的优先级范围，因此上面例子中的假设中，需要用括号将``x``上的量词限制起来。证明``∀ y : α, p y``的标准方法是取任意的``y``，然后证明``p y``。这是引入规则。现在，给定``h``有类型``∀ x : α, p x ∧ q x``，表达式``h y``有类型``p y ∧ q y``。这是消去规则。取合取的左侧得到想要的结论``p y``。 + +只有约束变量名称不同的表达式被认为是等价的。因此，例如，我们可以在假设和结论中使用相同的变量``x``，并在证明中用不同的变量``z``实例化它: ```lean example (α : Type) (p q : α → Prop) : (∀ x : α, p x ∧ q x) → ∀ x : α, p x := @@ -85,7 +131,11 @@ example (α : Type) (p q : α → Prop) : (∀ x : α, p x ∧ q x) → ∀ x : show p z from And.left (h z) ``` + + +再举一个例子，下面是关系``r``的传递性： ```lean variable (α : Type) (r : α → α → Prop) @@ -99,6 +149,7 @@ variable (hab : r a b) (hbc : r b c) #check trans_r a b c hab -- r b c → r a c #check trans_r a b c hab hbc -- r a c ``` + + + +当我们在值``a b c``上实例化``trans_r``时，我们最终得到``r a b → r b c → r a c``的证明。将此应用于“假设”``hab : r a b``，我们得到了``r b c → r a c``的一个证明。最后将它应用到假设``hbc``中，得到结论``r a c``的证明。 ```lean variable (α : Type) (r : α → α → Prop) @@ -122,6 +177,7 @@ variable (hab : r a b) (hbc : r b c) #check trans_r hab hbc ``` + + +优点是我们可以简单地写``trans_r hab hbc``作为``r a c``的证明。一个缺点是Lean没有足够的信息来推断表达式``trans_r``和``trans_r hab``中的参数类型。第一个``#check``命令的输出是``r ?m.1 ?m.2 → r ?m.2 ?m.3 → r ?m.1 ?m.3``，表示在本例中隐式参数未指定。 + +下面是一个用等价关系进行基本推理的例子: ```lean variable (α : Type) (r : α → α → Prop) @@ -142,6 +203,7 @@ example (a b c d : α) (hab : r a b) (hcb : r c b) (hcd : r c d) : r a d := trans_r (trans_r hab (symm_r hcb)) hcd ``` + + +为了习惯使用全称量词，你应该尝试本节末尾的一些练习。 + +依值箭头类型的类型规则，特别是全称量词，体现了``Prop``命题类型与其他对象的类型的不同。假设我们有``α : Sort i``和``β : Sort j``，其中表达式``β``可能依赖于变量``x : α``。那么``(x : α) → β``是``Sort (imax i j)``的一个元素，其中``imax i j``是``i``和``j``在``j``不为0时的最大值，否则为0。 + +其想法如下。如果``j``不是``0``，然后``(x : α) → β``是``Sort (max i j)``类型的一个元素。换句话说，从``α``到``β``的一类依值函数存在于指数为``i``和``j``最大值的宇宙中。然而，假设``β``属于``Sort 0``，即``Prop``的一个元素。在这种情况下，``(x : α) → β``也是``Sort 0``的一个元素，无论``α``生活在哪种类型的宇宙中。换句话说，如果``β``是一个依赖于``α``的命题，那么``∀ x : α, β``又是一个命题。这反映出``Prop``作为一种命题类型而不是数据类型，这也使得``Prop``具有“非直谓性”（impredicative）。 +“直谓性”一词起源于20世纪初的数学基础发展，当时逻辑学家如庞加莱和罗素将集合论的悖论归咎于“恶性循环”：当我们通过量化一个集合来定义一个属性时，这个集合包含了被定义的属性。注意，如果``α``是任何类型，我们可以在``α``上形成所有谓词的类型``α → Prop``(``α``的“幂”类型)。Prop的非直谓性意味着我们可以通过``α → Prop``形成量化命题。特别是，我们可以通过量化所有关于``α``的谓词来定义``α``上的谓词，这正是曾经被认为有问题的循环类型。 + + + +等价 +-------- + + +现在让我们来看看在Lean库中定义的最基本的关系之一，即等价关系。在[归纳类型](inductive_types.md)一章中，我们将解释如何从Lean的逻辑框架中定义等价。在这里我们解释如何使用它。 + +等价关系的基本性质：反身性、对称性、传递性。 + ```lean #check Eq.refl -- Eq.refl.{u_1} {α : Sort u_1} (a : α) : a = a @@ -192,8 +275,12 @@ Of course, a fundamental property of equality is that it is an equivalence relat #check Eq.trans -- Eq.trans.{u} {α : Sort u} {a b c : α} (h₁ : a = b) (h₂ : b = c) : a = c ``` + + +通过告诉Lean不要插入隐参数(在这里显示为元变量)可以使输出更容易阅读。 ```lean universe u @@ -203,9 +290,15 @@ universe u #check @Eq.trans.{u} -- @Eq.trans : ∀ {α : Sort u} {a b c : α}, a = b → b = c → a = c ``` + + +``.{u}``告诉Lean实例化宇宙``u``上的常量。 + +因此，我们可以将上一节中的示例具体化为等价关系: ```lean variable (α : Type) (a b c d : α) @@ -215,7 +308,11 @@ example : a = d := Eq.trans (Eq.trans hab (Eq.symm hcb)) hcd ``` + + +我们也可以使用投影记号： ```lean # variable (α : Type) (a b c d : α) @@ -223,11 +320,15 @@ We can also use the projection notation: example : a = d := (hab.trans hcb.symm).trans hcd ``` + + +反身性比它看上去更强大。回想一下，在构造演算中，项有一个计算解释，可规约为相同形式的项会被逻辑框架视为相同的。因此，一些非平凡的恒等式可以通过自反性来证明： ```lean variable (α β : Type) @@ -237,7 +338,11 @@ example (a : α) (b : β) : (a, b).1 = a := Eq.refl _ example : 2 + 3 = 5 := Eq.refl _ ``` + + +这个特性非常重要，以至于库中为``Eq.refl _``专门定义了一个符号``rfl``： ```lean # variable (α β : Type) @@ -246,12 +351,16 @@ example (a : α) (b : β) : (a, b).1 = a := rfl example : 2 + 3 = 5 := rfl ``` + + +然而，等价不仅仅是一种关系。它有一个重要的性质，即每个断言都遵从等价性，即我们可以在不改变真值的情况下对表达式做等价代换。也就是说，给定``h1 : a = b``和``h2 : p a``，我们可以构造一个证明``p b``，只需要使用代换``Eq.subst h1 h2``。 ```lean example (α : Type) (a b : α) (p : α → Prop) @@ -263,6 +372,7 @@ example (α : Type) (a b : α) (p : α → Prop) h1 ▸ h2 ``` + + +第二个例子中的三角形是建立在``Eq.subst``和``Eq.symm``之上的宏，它可以通过``\t``来输入。 + +规则``Eq.subst``定义了一些辅助规则，用来执行更显式的替换。它们是为处理应用型项，即形式为``s t``的项而设计的。这些辅助规则是，使用``congrArg``来替换参数，使用``congrFun``来替换正在应用的项，并且可以同时使用``congr``来替换两者。 ```lean variable (α : Type) @@ -285,7 +400,11 @@ example : f a = g a := congrFun h₂ a example : f a = g b := congr h₂ h₁ ``` + + +Lean的库包含大量通用的等式，例如： ```lean variable (a b c : Nat) @@ -304,12 +423,18 @@ example : (a + b) * c = a * c + b * c := Nat.add_mul a b c example : (a + b) * c = a * c + b * c := Nat.right_distrib a b c ``` + + +``Nat.mul_add``和``Nat.add_mul``是``Nat.left_distrib``和``Nat.right_distrib``的代称。上面的属性是为自然数类型``Nat``声明的。 + +这是一个使用代换以及结合律、交换律和分配律的自然数计算的例子。 ```lean example (x y : Nat) : (x + y) * (x + y) = x * x + y * x + x * y + y * y := @@ -320,6 +445,7 @@ example (x y : Nat) : (x + y) * (x + y) = x * x + y * x + x * y + y * y := h2.trans (Nat.add_assoc (x * x + y * x) (x * y) (y * y)).symm ``` + +注意，``Eq.subst``的第二个隐式参数提供了将要发生代换的表达式上下文，其类型为``α → Prop``。因此，推断这个谓词需要一个*高阶合一*（higher-order unification）的实例。一般来说，确定高阶合一器是否存在的问题是无法确定的，而Lean充其量只能提供不完美的和近似的解决方案。因此，``Eq.subst``并不总是做你想要它做的事。宏``h ▸ e``使用了更有效的启发式方法来计算这个隐参数，并且在不能应用``Eq.subst``的情况下通常会成功。 + +因为等式推理是如此普遍和重要，Lean提供了许多机制来更有效地执行它。下一节将提供允许你以更自然和清晰的方式编写计算式证明的语法。但更重要的是，等式推理是由项重写器、简化器和其他种类的自动化方法支持的。术语重写器和简化器将在下一节中简要描述，然后在下一章中更详细地描述。 + + + +计算式证明 +-------------------- + + +一个计算式证明是指一串使用诸如等式的传递性等基本规则得到的中间结果。在Lean中，计算式证明从关键字``calc``开始，语法如下： ``` calc @@ -356,11 +496,17 @@ calc '_' 'op_n' _n ':=' _n ``` + + +`calc`下的每一行使用相同的缩进。每个``_i``是``_{i-1} op_i _i``的证明。 + +我们也可以在第一个关系中使用`_`(就在``_0``之后)，这对于对齐关系/证明对的序列很有用: ``` calc _0 @@ -370,7 +516,11 @@ calc _0 '_' 'op_n' _n ':=' _n ``` + + +例子： ```lean variable (a b c d e : Nat) @@ -388,11 +538,15 @@ theorem T : a = e := _ = e := Eq.symm h4 ``` + + +这种写证明的风格在与`simp`和`rewrite`策略（Tactic）结合使用时最为有效，这些策略将在下一章详细讨论。例如，用缩写`rw`表示重写，上面的证明可以写成如下。 ```lean # variable (a b c d e : Nat) @@ -409,6 +563,7 @@ theorem T : a = e := _ = e := by rw [h4] ``` + + +本质上，``rw``策略使用一个给定的等式(它可以是一个假设、一个定理名称或一个复杂的项)来“重写”目标。如果这样做将目标简化为一种等式``t = t``，那么该策略将使用反身性来证明这一点。 + +重写可以一次应用一系列，因此上面的证明可以缩写为： ```lean # variable (a b c d e : Nat) @@ -430,7 +590,11 @@ theorem T : a = e := _ = e := by rw [h4] ``` + + +甚至更简单： ```lean # variable (a b c d e : Nat) @@ -442,11 +606,15 @@ theorem T : a = e := by rw [h1, h2, h3, Nat.add_comm, h4] ``` + + +相反，``simp``策略通过在项中以任意顺序在任何适用的地方重复应用给定的等式来重写目标。它还使用了之前声明给系统的其他规则，并明智地应用交换性以避免循环。因此，我们也可以如下证明定理: ```lean # variable (a b c d e : Nat) @@ -458,10 +626,16 @@ theorem T : a = e := by simp [h1, h2, h3, Nat.add_comm, h4] ``` + + +我们将在下一章讨论``rw``和``simp``的变体。 + +``calc``命令可以配置为任何支持某种形式的传递性的关系式。它甚至可以结合不同的关系式。 ```lean example (a b c d : Nat) (h1 : a = b) (h2 : b ≤ c) (h3 : c + 1 < d) : a < d := @@ -472,9 +646,13 @@ example (a b c d : Nat) (h1 : a = b) (h2 : b ≤ c) (h3 : c + 1 < d) : a < d := _ < d := h3 ``` + + +你可以通过添加`Trans`类型族（Type class）的新实例来“教给”`calc`新的传递性定理。稍后将介绍类型族，但下面的小示例将演示如何使用新的`Trans`实例扩展`calc`表示法。 ```lean def divides (x y : Nat) : Prop := @@ -506,14 +684,22 @@ example (h₁ : divides x y) (h₂ : y = z) : divides x (2*z) := _ ∣ 2*z := divides_mul .. ``` + + +上面的例子也清楚地表明，即使关系式没有中缀符号，也可以使用`calc`。最后，我们注意到上面例子中的竖线`∣`是unicode。我们使用unicode来确保我们不会重载在`match .. with`表达式中使用的ASCII`|`。 + + +使用``calc``，我们可以以一种更自然、更清晰的方式写出上一节的证明。 ```lean example (x y : Nat) : (x + y) * (x + y) = x * x + y * x + x * y + y * y := @@ -524,9 +710,13 @@ example (x y : Nat) : (x + y) * (x + y) = x * x + y * x + x * y + y * y := _ = x * x + y * x + x * y + y * y := by rw [←Nat.add_assoc] ``` + + +这里值得考虑另一种`calc`表示法。当第一个表达式占用这么多空间时，在第一个关系中使用`_`自然会对齐所有关系式: ```lean example (x y : Nat) : (x + y) * (x + y) = x * x + y * x + x * y + y * y := @@ -537,10 +727,14 @@ example (x y : Nat) : (x + y) * (x + y) = x * x + y * x + x * y + y * y := _ = x * x + y * x + x * y + y * y := by rw [←Nat.add_assoc] ``` + + +``Nat.add_assoc``之前的左箭头指挥重写以相反的方向使用等式。(你可以输入``\l``或ascii码``<-``。)如果追求简洁，``rw``和``simp``可以一次性完成这项工作: ```lean example (x y : Nat) : (x + y) * (x + y) = x * x + y * x + x * y + y * y := @@ -550,9 +744,14 @@ example (x y : Nat) : (x + y) * (x + y) = x * x + y * x + x * y + y * y := by simp [Nat.mul_add, Nat.add_mul, Nat.add_assoc] ``` + + +## 存在量词 + + +存在量词可以写成``exists x : α, p x``或``∃ x : α, p x``。这两个写法实际上在Lean的库中的定义为一个更冗长的表达式，``Exists (fun x : α => p x)``。 + +存在量词也有一个引入规则和一个消去规则。引入规则很简单：要证明``∃ x : α, p x``，只需提供一个合适的项``t``和对``p t``的证明即可。``∃``用``\exists``或简写``\ex``输入，下面是一些例子: ```lean example : ∃ x : Nat, x > 0 := @@ -577,8 +781,12 @@ example (x y z : Nat) (hxy : x < y) (hyz : y < z) : ∃ w, x < w ∧ w < z := #check @Exists.intro -- ∀ {α : Sort u_1} {p : α → Prop} (w : α), p w → Exists p ``` + + +当类型可从上下文中推断时，我们可以使用匿名构造器表示法``⟨t, h⟩``替换``Exists.intro t h``。 ```lean example : ∃ x : Nat, x > 0 := @@ -592,6 +800,7 @@ example (x y z : Nat) (hxy : x < y) (hyz : y < z) : ∃ w, x < w ∧ w < z := ⟨y, hxy, hyz⟩ ``` + + +注意``Exists.intro``有隐参数：Lean必须在结论``∃ x, p x``中推断谓词``p : α → Prop``。这不是一件小事。例如，如果我们有``hg : g 0 0 = 0``和``Exists.intro 0 hg``，有许多可能的值的谓词``p``，对应定理``∃ x, g x x = x``，``∃ x, g x x = 0``，``∃ x, g x 0 = x``，等等。Lean使用上下文来推断哪个是合适的。下面的例子说明了这一点，在这个例子中，我们设置了选项``pp.explicit``为true，要求Lean打印隐参数。 + + +```lean +variable (g : Nat → Nat → Nat) +variable (hg : g 0 0 = 0) + +theorem gex1 : ∃ x, g x x = x := ⟨0, hg⟩ +theorem gex2 : ∃ x, g x 0 = x := ⟨0, hg⟩ +theorem gex3 : ∃ x, g 0 0 = x := ⟨0, hg⟩ +theorem gex4 : ∃ x, g x x = 0 := ⟨0, hg⟩ + +set_option pp.explicit true -- 打印隐参数 +#print gex1 +#print gex2 +#print gex3 +#print gex4 +``` + + +我们可以将``Exists.intro``视为信息隐藏操作，因为它将断言的具体实例隐藏起来变成了存在量词。存在消去规则``Exists.elim``执行相反的操作。它允许我们从``∃ x : α, p x``证明一个命题``q``，通过证明对于任意值``w``时``p w``都能推出``q``。粗略地说，既然我们知道有一个``x``满足``p x``，我们可以给它起个名字，比如``w``。如果``q``没有提到``w``，那么表明``p w``能推出``q``就等同于表明``q``从任何这样的``x``的存在而推得。下面是一个例子: ```lean variable (α : Type) (p q : α → Prop) @@ -639,6 +873,7 @@ example (h : ∃ x, p x ∧ q x) : ∃ x, q x ∧ p x := show ∃ x, q x ∧ p x from ⟨w, hw.right, hw.left⟩) ``` + + +把存在消去规则和析取消去规则作个比较可能会带来一些启发。命题``∃ x : α, p x``可以看成一个对所有``α``中的元素``a``所组成的命题``p a``的大型析取。注意到匿名构造器``⟨w, hw.right, hw.left⟩``是嵌套的构造器``⟨w, ⟨hw.right, hw.left⟩⟩``的缩写。 + +存在式命题类型很像依值类型一节所述的sigma类型。给定``a : α``和``h : p a``时，项``Exists.intro a h``具有类型``(∃ x : α, p x) : Prop``，而``Sigma.mk a h``具有类型``(Σ x : α, p x) : Type``。``∃``和``Σ``之间的相似性是Curry-Howard同构的另一例子。 + +Lean提供一个更加方便的消去存在量词的途径，那就是通过``match``表达式。 ```lean variable (α : Type) (p q : α → Prop) @@ -664,6 +906,7 @@ example (h : ∃ x, p x ∧ q x) : ∃ x, q x ∧ p x := | ⟨w, hw⟩ => ⟨w, hw.right, hw.left⟩ ``` + + +``match``表达式是Lean功能定义系统的一部分，它提供了复杂功能的方便且丰富的表达方式。再一次，正是Curry-Howard同构让我们能够采用这种机制来编写证明。``match``语句将存在断言“析构”到组件``w``和``hw``中，然后可以在语句体中使用它们来证明命题。我们可以对match中使用的类型进行注释，以提高清晰度： ```lean # variable (α : Type) (p q : α → Prop) @@ -680,7 +926,11 @@ example (h : ∃ x, p x ∧ q x) : ∃ x, q x ∧ p x := | ⟨(w : α), (hw : p w ∧ q w)⟩ => ⟨w, hw.right, hw.left⟩ ``` + + +我们甚至可以同时使用match语句来分解合取： ```lean # variable (α : Type) (p q : α → Prop) @@ -689,7 +939,11 @@ example (h : ∃ x, p x ∧ q x) : ∃ x, q x ∧ p x := | ⟨w, hpw, hqw⟩ => ⟨w, hqw, hpw⟩ ``` + + +Lean还提供了一个模式匹配的``let``表达式： ```lean # variable (α : Type) (p q : α → Prop) @@ -698,9 +952,14 @@ example (h : ∃ x, p x ∧ q x) : ∃ x, q x ∧ p x := ⟨w, hqw, hpw⟩ ``` + + +这实际上是上面的``match``结构的替代表示法。Lean甚至允许我们在``fun``表达式中使用隐含的``match``： + ```lean # variable (α : Type) (p q : α → Prop) @@ -708,11 +967,18 @@ example : (∃ x, p x ∧ q x) → ∃ x, q x ∧ p x := fun ⟨w, hpw, hqw⟩ => ⟨w, hqw, hpw⟩ ``` + + +我们将在[归纳和递归](./induction_and_recursion.md)一章看到所有这些变体都是更一般的模式匹配构造的实例。 + +在下面的例子中，我们将``even a``定义为``∃ b, a = 2 * b``，然后我们证明两个偶数的和是偶数。 + ```lean def is_even (a : Nat) := ∃ b, a = 2 * b @@ -726,9 +992,13 @@ theorem even_plus_even (h1 : is_even a) (h2 : is_even b) : is_even (a + b) := _ = 2 * (w1 + w2) := by rw [Nat.mul_add]))) ``` + + +使用本章描述的各种小工具——``match``语句、匿名构造器和``rewrite``策略，我们可以简洁地写出如下证明： ```lean # def is_even (a : Nat) := ∃ b, a = 2 * b @@ -737,12 +1007,16 @@ theorem even_plus_even (h1 : is_even a) (h2 : is_even b) : is_even (a + b) := | ⟨w1, hw1⟩, ⟨w2, hw2⟩ => ⟨w1 + w2, by rw [hw1, hw2, Nat.mul_add]⟩ ``` + + +就像构造主义的“或”比古典的“或”强，同样，构造的“存在”也比古典的“存在”强。例如，下面的推论需要经典推理，因为从构造的角度来看，知道并不是每一个``x``都满足``¬ p``，并不等于有一个特定的``x``满足``p``。 ```lean open Classical @@ -759,10 +1033,14 @@ example (h : ¬ ∀ x, ¬ p x) : ∃ x, p x := show False from h h2) ``` + + +下面是一些涉及存在量词的常见等式。在下面的练习中，我们鼓励你尽可能多写出证明。你需要判断哪些是非构造主义的，因此需要一些经典推理。 ```lean open Classical @@ -785,10 +1063,16 @@ example (a : α) : (∃ x, p x → r) ↔ (∀ x, p x) → r := sorry example (a : α) : (∃ x, r → p x) ↔ (r → ∃ x, p x) := sorry ``` + + +注意，第二个例子和最后两个例子要求假设至少有一个类型为``α``的元素``a``。 + +以下是两个比较困难的问题的解： ```lean open Classical @@ -829,9 +1113,14 @@ example : (∃ x, p x → r) ↔ (∀ x, p x) → r := show False from hnap hap))) ``` + +## 多来点儿证明语法 + + + +我们已经看到像``fun``、``have``和``show``这样的关键字使得写出反映非正式数学证明结构的正式证明项成为可能。在本节中，我们将讨论证明语言的一些通常很方便的附加特性。 + +首先，我们可以使用匿名的``have``表达式来引入一个辅助目标，而不需要标注它。我们可以使用关键字``this``'来引用最后一个以这种方式引入的表达式: ```lean variable (f : Nat → Nat) @@ -851,11 +1145,17 @@ example : f 0 ≤ f 3 := show f 0 ≤ f 3 from Nat.le_trans this (h 2) ``` + + +通常证明从一个事实转移到另一个事实，所以这可以有效地消除杂乱的大量标签。 + +当目标可以推断出来时，我们也可以让Lean写``by assumption``来填写证明： ```lean # variable (f : Nat → Nat) @@ -866,6 +1166,7 @@ example : f 0 ≤ f 3 := show f 0 ≤ f 3 from Nat.le_trans (by assumption) (h 2) ``` + + +这告诉Lean使用``assumption``策略，反过来，通过在局部上下文中找到合适的假设来证明目标。我们将在下一章学习更多关于``assumption``策略的内容。 + +我们也可以通过写``‹p›``的形式要求Lean填写证明，其中``p``是我们希望Lean在上下文中找到的证明命题。你可以分别使用``\f<``和``\f>``输入这些角引号。字母“f”表示“French”，因为unicode符号也可以用作法语引号。事实上，这个符号在Lean中定义如下: ```lean notation "‹" p "›" => show p by assumption ``` + + +这种方法比使用``by assumption``更稳健，因为需要推断的假设类型是显式给出的。它还使证明更具可读性。这里有一个更详细的例子: ```lean variable (f : Nat → Nat) @@ -899,21 +1209,38 @@ example : f 0 ≥ f 1 → f 1 ≥ f 2 → f 0 = f 2 := show f 0 = f 2 from Nat.le_antisymm this ‹f 0 ≥ f 2› ``` + + +你可以这样使用法语引号来指代上下文中的“任何东西”，而不仅仅是匿名引入的东西。它的使用也不局限于命题，尽管将它用于数据有点奇怪： ```lean example (n : Nat) : Nat := ‹Nat› ``` + +稍后，我们将展示如何使用Lean中的宏系统扩展证明语言。 + + +练习 +--------- + + + +1. 证明以下等式： ```lean variable (α : Type) (p q : α → Prop) @@ -923,12 +1250,20 @@ example : (∀ x, p x → q x) → (∀ x, p x) → (∀ x, q x) := sorry example : (∀ x, p x) ∨ (∀ x, q x) → ∀ x, p x ∨ q x := sorry ``` + +你还应该想想为什么在最后一个例子中反过来是不能证明的。 + + + +2. 当一个公式的组成部分不依赖于被全称的变量时，通常可以把它提取出一个全称量词的范围。尝试证明这些(第二个命题中的一个方向需要经典逻辑)： ```lean variable (α : Type) (p q : α → Prop) @@ -939,9 +1274,13 @@ example : (∀ x, p x ∨ r) ↔ (∀ x, p x) ∨ r := sorry example : (∀ x, r → p x) ↔ (r → ∀ x, p x) := sorry ``` + + +3. 考虑“理发师悖论”：在一个小镇里，这里有一个（男性）理发师给所有不为自己刮胡子的人刮胡子。证明这里存在矛盾： ```lean variable (men : Type) (barber : men) @@ -950,6 +1289,7 @@ variable (shaves : men → men → Prop) example (h : ∀ x : men, shaves barber x ↔ ¬ shaves x x) : False := sorry ``` + + +4. 如果没有任何参数，类型``Prop``的表达式只是一个断言。填入下面``prime``和``Fermat_prime``的定义，并构造每个给定的断言。例如，通过断言每个自然数``n``都有一个大于``n``的质数，你可以说有无限多个质数。哥德巴赫弱猜想指出，每一个大于5的奇数都是三个素数的和。如果有必要，请查阅费马素数的定义或其他任何资料。 ```lean def even (n : Nat) : Prop := sorry @@ -978,5 +1321,9 @@ def Goldbach's_weak_conjecture : Prop := sorry def Fermat's_last_theorem : Prop := sorry ``` + + +5. 尽可能多地证明存在量词一节列出的等式。 diff --git a/tactics.md b/tactics.md index 13b8aca..93c7b1e 100644 --- a/tactics.md +++ b/tactics.md @@ -1,6 +1,12 @@ + +证明策略 +======= + + + +在本章中，我们描述了另一种构建证明的方法，即使用**策略**（Tactic）。 一个证明项代表一个数学证明；策略是描述如何建立这样一个证明的命令或指令。你可以在数学证明开始时非正式地说：“为了证明条件的必要性，展开定义，应用前面的定理，并进行简化。”就像这些指令告诉读者如何构建证明一样，策略告诉Lean如何构建证明。它们自然而然地支持增量式的证明书写，在这种写作方式中，你将分解一个证明，并一步步地实现目标。 + +> 译者注：tactic和strategy都有策略的意思，其中tactic侧重细节，如排兵布阵，strategy面向整体，如大规模战略。试译strategy为“要略”，与tactic相区分。 +我们将把由策略序列组成的证明描述为“策略式”证明，前几章的证明我们称为“项式”证明。每种风格都有自己的优点和缺点。例如，策略式证明可能更难读，因为它们要求读者预测或猜测每条指令的结果。但它们一般更短，更容易写。此外，策略提供了一个使用Lean自动化的途径，因为自动化程序本身就是策略。 + + + +进入策略模式 +-------------------- + + +从概念上讲，陈述一个定理或引入一个``have``的声明会产生一个目标，即构造一个具有预期类型的项的目标。例如, 下面创建的目标是构建一个类型为``p ∧ q ∧ p``的项，条件有常量``p q : Prop``，``hp : p``和``hq : q``。 ```lean theorem test (p q : Prop) (hp : p) (hq : q) : p ∧ q ∧ p := sorry ``` + + +写成目标如下： ``` p : Prop, q : Prop, hp : p, hq : q ⊢ p ∧ q ∧ p ``` + + +事实上，如果你把上面的例子中的“sorry”换成下划线，Lean会报告说，正是这个目标没有得到解决。 + +通常情况下，你会通过写一个明确的项来满足这样的目标。但在任何需要项的地方，Lean允许我们插入一个``by ``块，其中````是一串命令，用分号或换行符分开。你可以用下面这种方式来证明上面的定理： + ```lean theorem test (p q : Prop) (hp : p) (hq : q) : p ∧ q ∧ p := @@ -61,8 +94,12 @@ theorem test (p q : Prop) (hp : p) (hq : q) : p ∧ q ∧ p := exact hp ``` + + +我们经常将``by``关键字放在前一行，并将上面的例子写为 ```lean theorem test (p q : Prop) (hp : p) (hq : q) : p ∧ q ∧ p := by @@ -73,12 +110,16 @@ theorem test (p q : Prop) (hp : p) (hq : q) : p ∧ q ∧ p := by exact hp ``` + + +``apply``策略应用于一个表达式，被视为表示一个有零或多个参数的函数。它将结论与当前目标中的表达式统一起来，并为剩余的参数创建新的目标，只要后面的参数不依赖于它们。在上面的例子中，命令``apply And.intro``产生了两个子目标： ``` case left @@ -94,6 +135,7 @@ subgoals: ⊢ q ∧ p ``` + + +第一个目标是通过``exact hp``命令来实现的。``exact``命令只是``apply``的一个变体，它表示所给的表达式应该准确地填充目标。在策略证明中使用它很有益，因为它如果失败那么表明出了问题。它也比``apply``更稳健，因为繁饰器在处理被应用的表达式时，会考虑到目标所预期的类型。然而，在这种情况下，``apply``也可以很好地工作。 + +你可以用`#print`命令查看所产生的证明项。 ```lean # theorem test (p q : Prop) (hp : p) (hq : q) : p ∧ q ∧ p := by @@ -115,6 +162,7 @@ You can see the resulting proof term with the ``#print`` command: #print test ``` + + +你可以循序渐进地写一个策略脚本。在VS Code中，你可以通过按`Ctrl-Shift-Enter`打开一个窗口来显示信息，然后只要光标在策略块中，该窗口就会显示当前的目标。在Emacs中，你可以通过按`C-c C-g`看到任何一行末尾的目标，或者通过把光标放在最后一个策略的第一个字符之后，看到一个不完整的证明中的剩余目标。如果证明是不完整的，标记``by``会被装饰成一条红色的斜线，错误信息中包含剩余的目标。 + +策略命令可以接受复合表达式，而不仅仅是单一标识符。下面是前面证明的一个简短版本。 ```lean theorem test (p q : Prop) (hp : p) (hq : q) : p ∧ q ∧ p := by @@ -135,7 +188,11 @@ theorem test (p q : Prop) (hp : p) (hq : q) : p ∧ q ∧ p := by exact And.intro hq hp ``` + + +它产生了相同的证明项。 ```lean # theorem test (p q : Prop) (hp : p) (hq : q) : p ∧ q ∧ p := by @@ -144,13 +201,18 @@ Unsurprisingly, it produces exactly the same proof term. #print test ``` + + +应用多个策略可以通过用分号连接写在一行中。 ```lean theorem test (p q : Prop) (hp : p) (hq : q) : p ∧ q ∧ p := by apply And.intro hp; exact And.intro hq hp ``` + + +可能产生多个子目标的策略通常对子目标进行标记。例如，``apply And.intro``策略将第一个目标标记为``left``，将第二个目标标记为``right``。在``apply``策略的情况下，标签是从``And.intro``声明中使用的参数名称推断出来的。你可以使用符号``case => ``来结构化你的策略。下面是本章中第一个策略证明的结构化版本。 ```lean theorem test (p q : Prop) (hp : p) (hq : q) : p ∧ q ∧ p := by @@ -169,8 +234,12 @@ theorem test (p q : Prop) (hp : p) (hq : q) : p ∧ q ∧ p := by case right => exact hp ``` + + +使用``case``标记，你也可以在``left``之前先解决子目标``right``： ```lean theorem test (p q : Prop) (hp : p) (hq : q) : p ∧ q ∧ p := by @@ -182,6 +251,7 @@ theorem test (p q : Prop) (hp : p) (hq : q) : p ∧ q ∧ p := by case left => exact hp ``` + + +注意，Lean将其他目标隐藏在``case``块内。我们说它“专注”于选定的目标。 此外，如果所选目标在``case``块的末尾没有完全解决，Lean会标记一个错误。 + +对于简单的子目标，可能不值得使用其标签来选择一个子目标，但你可能仍然想要结构化证明。Lean还提供了“子弹”符号``. ``或``· ``。 ```lean theorem test (p q : Prop) (hp : p) (hq : q) : p ∧ q ∧ p := by @@ -201,13 +276,22 @@ theorem test (p q : Prop) (hp : p) (hq : q) : p ∧ q ∧ p := by . exact hp ``` + +基本策略 +------------- + + + +除了``apply``和``exact``之外，另一个有用的策略是``intro``，它引入了一个假设。下面是我们在前一章中证明的命题逻辑中的一个等价性的例子，现在用策略来证明。 ```lean example (p q r : Prop) : p ∧ (q ∨ r) ↔ (p ∧ q) ∨ (p ∧ r) := by @@ -238,7 +322,11 @@ example (p q r : Prop) : p ∧ (q ∨ r) ↔ (p ∧ q) ∨ (p ∧ r) := by exact And.right hpr ``` + + +``intro``命令可以更普遍地用于引入任何类型的变量。 ```lean example (α : Type) : α → α := by @@ -250,7 +338,11 @@ example (α : Type) : ∀ x : α, x = x := by exact Eq.refl x ``` + + +你可以同时引入好几个变量： ```lean example : ∀ a b c : Nat, a = b → a = c → c = b := by @@ -258,11 +350,15 @@ example : ∀ a b c : Nat, a = b → a = c → c = b := by exact Eq.trans (Eq.symm h₂) h₁ ``` + + +由于``apply``策略是一个用于交互式构造函数应用的命令，``intro``策略是一个用于交互式构造函数抽象的命令（即``fun x => e``形式的项）。 与lambda抽象符号一样，``intro``策略允许我们使用隐式的``match``。 ```lean example (α : Type) (p q : α → Prop) : (∃ x, p x ∧ q x) → ∃ x, q x ∧ p x := by @@ -270,7 +366,11 @@ example (α : Type) (p q : α → Prop) : (∃ x, p x ∧ q x) → ∃ x, q x exact ⟨w, hqw, hpw⟩ ``` + + +就像``match``表达式一样，你也可以提供多个选项。 ```lean example (α : Type) (p q : α → Prop) : (∃ x, p x ∨ q x) → ∃ x, q x ∨ p x := by @@ -279,6 +379,7 @@ example (α : Type) (p q : α → Prop) : (∃ x, p x ∨ q x) → ∃ x, q x | ⟨w, Or.inr h⟩ => exact ⟨w, Or.inl h⟩ ``` + +``intros``策略可以在没有任何参数的情况下使用，在这种情况下，它选择名字并尽可能多地引入变量。稍后你会看到一个例子。 + +``assumption``策略在当前目标的背景下查看假设，如果有一个与结论相匹配的假设，它就会应用这个假设。 + + + +```lean +example (x y z w : Nat) (h₁ : x = y) (h₂ : y = z) (h₃ : z = w) : x = w := by + apply Eq.trans h₁ + apply Eq.trans h₂ + assumption -- 应用h₃ +``` + + +若有必要，它会在结论中统一元变量。 + + +```lean +example (x y z w : Nat) (h₁ : x = y) (h₂ : y = z) (h₃ : z = w) : x = w := by + apply Eq.trans + assumption -- 求解了 x = ?b with h₁ + apply Eq.trans + assumption -- 求解了 y = ?h₂.b with h₂ + assumption -- 求解了 z = w with h₃ +``` + + +下面的例子使用``intros``命令来自动引入三个变量和两个假设： ```lean example : ∀ a b c : Nat, a = b → a = c → c = b := by @@ -316,9 +450,13 @@ example : ∀ a b c : Nat, a = b → a = c → c = b := by assumption ``` + + +请注意，由Lean自动生成的名称在默认情况下是不可访问的。其动机是为了确保你的策略证明不依赖于自动生成的名字，并因此而更加强大。然而，你可以使用组合器``unhygienic``来禁用这一限制。 ```lean example : ∀ a b c : Nat, a = b → a = c → c = b := by unhygienic @@ -329,9 +467,13 @@ example : ∀ a b c : Nat, a = b → a = c → c = b := by unhygienic exact a_1 ``` + + +你也可以使用``rename_i``策略来重命名你的上下文中最近的不能访问的名字。在下面的例子中，策略``rename_i h1 _ h2``在你的上下文中重命名了三个假设中的两个。 ```lean example : ∀ a b c d : Nat, a = b → a = d → a = c → c = b := by @@ -343,14 +485,22 @@ example : ∀ a b c d : Nat, a = b → a = d → a = c → c = b := by exact h1 ``` + + +``rfl``策略是``exact rfl``的语法糖。 ```lean example (y : Nat) : (fun x : Nat => 0) y = 0 := by rfl ``` + + +``repeat``组合器可以多次使用一个策略。 ```lean example : ∀ a b c : Nat, a = b → a = c → c = b := by @@ -360,8 +510,12 @@ example : ∀ a b c : Nat, a = b → a = c → c = b := by repeat assumption ``` + + +另一个有时很有用的策略是还原``revert``策略，从某种意义上说，它是对``intro``的逆。 ```lean example (x : Nat) : x = x := by @@ -372,7 +526,11 @@ example (x : Nat) : x = x := by rfl ``` + + +将一个假设还原到目标中会产生一个蕴含。 ```lean example (x y : Nat) (h : x = y) : y = x := by @@ -384,10 +542,14 @@ example (x y : Nat) (h : x = y) : y = x := by assumption ``` + + +但是`revert`更聪明，因为它不仅会还原上下文中的一个元素，还会还原上下文中所有依赖它的后续元素。例如，在上面的例子中，还原`x`会带来`h`。 ```lean example (x y : Nat) (h : x = y) : y = x := by @@ -398,7 +560,11 @@ example (x y : Nat) (h : x = y) : y = x := by assumption ``` + + +你还可以一次性还原多个元素： ```lean example (x y : Nat) (h : x = y) : y = x := by @@ -409,10 +575,14 @@ example (x y : Nat) (h : x = y) : y = x := by assumption ``` + + +你只能``revert``局部环境中的一个元素，也就是一个局部变量或假设。但是你可以使用泛化``generalize``策略将目标中的任意表达式替换为新的变量。 ```lean example : 3 = 3 := by @@ -425,11 +595,15 @@ example : 3 = 3 := by rfl ``` + + +上述符号的记忆法是，你通过将``3``设定为任意变量``x``来泛化目标。要注意：不是每一个泛化都能保留目标的有效性。这里，`generalize`用一个无法证明的目标取代了一个可以用``rfl``证明的目标。 ```lean example : 2 + 3 = 5 := by @@ -438,6 +612,7 @@ example : 2 + 3 = 5 := by admit ``` + + +在这个例子中，``admit``策略是``sorry``证明项的类似物。它关闭了当前的目标，产生了通常的警告：使用了``sorry``。为了保持之前目标的有效性，`generalize`策略允许我们记录`3`已经被`x`所取代的事实。你所需要做的就是提供一个标签，`generalize`使用它来存储局部上下文中的赋值。 ```lean example : 2 + 3 = 5 := by @@ -453,17 +631,30 @@ example : 2 + 3 = 5 := by rw [← h] ``` + +这里``rewrite``策略，缩写为``rw``，用``h``把``x``用``3``换了回来。``rewrite``策略下文将继续讨论。 + + + +更多策略 +------------ + + +一些额外的策略对于建构和析构命题以及数据很有用。例如，当应用于形式为``p ∨ q``的目标时，你可以使用``apply Or.inl``和``apply Or.inr``等策略。 反之，``cases``策略可以用来分解一个析取。 ```lean example (p q : Prop) : p ∨ q → q ∨ p := by @@ -473,8 +664,12 @@ example (p q : Prop) : p ∨ q → q ∨ p := by | inr hq => apply Or.inl; exact hq ``` + + +注意，该语法与`match`表达式中使用的语法相似。新的子目标可以按任何顺序解决。 ```lean example (p q : Prop) : p ∨ q → q ∨ p := by @@ -484,8 +679,12 @@ example (p q : Prop) : p ∨ q → q ∨ p := by | inl hp => apply Or.inr; exact hp ``` + + +你也可以使用一个（非结构化的）`cases`，而不使用`with`，并为每个备选情况制定一个策略。 ```lean example (p q : Prop) : p ∨ q → q ∨ p := by @@ -497,8 +696,12 @@ example (p q : Prop) : p ∨ q → q ∨ p := by assumption ``` + + +（非结构化的）`cases`在你可以用同一个策略来解决子任务时格外有用。 ```lean example (p : Prop) : p ∨ p → p := by @@ -507,8 +710,12 @@ example (p : Prop) : p ∨ p → p := by repeat assumption ``` + + +你也可以使用组合器``tac1 <;> tac2``，将``tac2``应用于策略``tac1``产生的每个子目标。 ```lean example (p : Prop) : p ∨ p → p := by @@ -516,7 +723,11 @@ example (p : Prop) : p ∨ p → p := by cases h <;> assumption ``` + + +你可以与``.``符号相结合使用非结构化的``cases``策略。 ```lean example (p q : Prop) : p ∨ q → q ∨ p := by @@ -547,8 +758,12 @@ example (p q : Prop) : p ∨ q → q ∨ p := by assumption ``` + + +``cases``策略也被用来分解一个析取。 ```lean example (p q : Prop) : p ∧ q → q ∧ p := by @@ -557,11 +772,15 @@ example (p q : Prop) : p ∧ q → q ∧ p := by | intro hp hq => constructor; exact hq; exact hp ``` + + +在这个例子中，应用``cases``策略后只有一个目标，``h : p ∧ q``被一对假设取代，``hp : p``和``hq : q``。``constructor``策略应用了唯一一个合取构造器``And.intro``。有了这些策略，上一节的一个例子可以改写如下。 ```lean example (p q r : Prop) : p ∧ (q ∨ r) ↔ (p ∧ q) ∨ (p ∧ r) := by @@ -582,11 +801,15 @@ example (p q r : Prop) : p ∧ (q ∨ r) ↔ (p ∧ q) ∨ (p ∧ r) := by | intro hp hr => constructor; exact hp; apply Or.inr; exact hr ``` + + +你将在[归纳类型](./inductive_types.md)一章中看到，这些策略是相当通用的。``cases``策略可以用来分解递归定义类型的任何元素；``constructor``总是应用递归定义类型的第一个适用构造器。例如，你可以使用``cases``和``constructor``与一个存在量词： ```lean example (p q : Nat → Prop) : (∃ x, p x) → ∃ x, p x ∨ q x := by @@ -595,6 +818,7 @@ example (p q : Nat → Prop) : (∃ x, p x) → ∃ x, p x ∨ q x := by | intro x px => constructor; apply Or.inl; exact px ``` + + +在这里，``constructor``策略将存在性断言的第一个组成部分，即``x``的值，保留为隐式的。它是由一个元变量表示的，这个元变量以后应该被实例化。在前面的例子中，元变量的正确值是由策略``exact px``决定的，因为``px``的类型是``p x``。如果你想明确指定存在量词的存在者，你可以使用`exists`策略来代替。 ```lean example (p q : Nat → Prop) : (∃ x, p x) → ∃ x, p x ∨ q x := by @@ -610,7 +837,11 @@ example (p q : Nat → Prop) : (∃ x, p x) → ∃ x, p x ∨ q x := by | intro x px => exists x; apply Or.inl; exact px ``` + + +另一个例子： ```lean example (p q : Nat → Prop) : (∃ x, p x ∧ q x) → ∃ x, q x ∧ p x := by @@ -622,9 +853,13 @@ example (p q : Nat → Prop) : (∃ x, p x ∧ q x) → ∃ x, q x ∧ p x := by exists x ``` + + +这些策略既可以用在命题上，也可以用在数上。在下面的两个例子中，它们被用来定义交换乘法和加法类型组件的函数： ```lean def swap_pair : α × β → β × α := by @@ -639,10 +874,14 @@ def swap_sum : Sum α β → Sum β α := by . apply Sum.inl; assumption ``` + + +在我们为变量选择的名称之前，它们的定义与有关合取和析取的类似命题的证明是相同的。``cases``策略也会对自然数进行逐情况区分： ```lean open Nat @@ -652,10 +891,16 @@ example (P : Nat → Prop) (h₀ : P 0) (h₁ : ∀ n, P (succ n)) (m : Nat) : P | succ m' => exact h₁ m' ``` + + +``cases``策略伙同``induction``策略将在[归纳类型的策略](./inductive_types.md#_tactics_for_inductive_types)一节中详述。 + +``contradiction``策略搜索当前目标的假设中的矛盾： ```lean example (p q : Prop) : p ∧ ¬ p → q := by @@ -664,7 +909,11 @@ example (p q : Prop) : p ∧ ¬ p → q := by contradiction ``` + + +你也可以在策略块中使用``match``： ```lean example (p q r : Prop) : p ∧ (q ∨ r) ↔ (p ∧ q) ∨ (p ∧ r) := by @@ -679,7 +928,11 @@ example (p q r : Prop) : p ∧ (q ∨ r) ↔ (p ∧ q) ∨ (p ∧ r) := by | Or.inr ⟨hp, hr⟩ => constructor; exact hp; apply Or.inr; exact hr ``` + + +你可以将``intro h``与``match h ...``结合起来，然后上例就可以如下地写出： ```lean example (p q r : Prop) : p ∧ (q ∨ r) ↔ (p ∧ q) ∨ (p ∧ r) := by @@ -692,9 +945,15 @@ example (p q r : Prop) : p ∧ (q ∨ r) ↔ (p ∧ q) ∨ (p ∧ r) := by | Or.inr ⟨hp, hr⟩ => constructor; assumption; apply Or.inr; assumption ``` + + +结构化策略证明 +------------------------- + + +策略通常提供了建立证明的有效方法，但一长串指令会掩盖论证的结构。在这一节中，我们将描述一些有助于为策略式证明提供结构的方法，使这种证明更易读，更稳健。 + +Lean的证明写作语法的一个优点是，它可以混合项式和策略式证明，并在两者之间自由转换。例如，策略``apply``和``exact``可以传入任意的项，你可以用``have``，``show``等等来写这些项。反之，当写一个任意的Lean项时，你总是可以通过插入一个``by``块来调用策略模式。下面是一个简易例子： ```lean example (p q r : Prop) : p ∧ (q ∨ r) → (p ∧ q) ∨ (p ∧ r) := by @@ -721,7 +985,11 @@ example (p q r : Prop) : p ∧ (q ∨ r) → (p ∧ q) ∨ (p ∧ r) := by | inr hr => exact Or.inr ⟨hp, hr⟩ ``` + + +更自然一点： ```lean example (p q r : Prop) : p ∧ (q ∨ r) ↔ (p ∧ q) ∨ (p ∧ r) := by @@ -736,10 +1004,14 @@ example (p q r : Prop) : p ∧ (q ∨ r) ↔ (p ∧ q) ∨ (p ∧ r) := by | inr hpr => exact ⟨hpr.left, Or.inr hpr.right⟩ ``` + + +事实上，有一个``show``策略，它类似于证明项中的``show``表达式。它只是简单地声明即将被解决的目标的类型，同时保持策略模式。 ```lean example (p q r : Prop) : p ∧ (q ∨ r) ↔ (p ∧ q) ∨ (p ∧ r) := by @@ -762,7 +1034,11 @@ example (p q r : Prop) : p ∧ (q ∨ r) ↔ (p ∧ q) ∨ (p ∧ r) := by exact ⟨hpr.left, Or.inr hpr.right⟩ ``` + + +``show``策略其实可以被用来重写一些定义等价的目标： ```lean example (n : Nat) : n + 1 = Nat.succ n := by @@ -770,7 +1046,11 @@ example (n : Nat) : n + 1 = Nat.succ n := by rfl ``` + + +还有一个``have``策略，它引入了一个新的子目标，就像写证明项时一样。 ```lean example (p q r : Prop) : p ∧ (q ∨ r) → (p ∧ q) ∨ (p ∧ r) := by @@ -787,8 +1067,12 @@ example (p q r : Prop) : p ∧ (q ∨ r) → (p ∧ q) ∨ (p ∧ r) := by exact hpr ``` + + +与证明项一样，你可以省略``have``策略中的标签，在这种情况下，将使用默认标签``this``： ```lean example (p q r : Prop) : p ∧ (q ∨ r) → (p ∧ q) ∨ (p ∧ r) := by @@ -805,10 +1089,14 @@ example (p q r : Prop) : p ∧ (q ∨ r) → (p ∧ q) ∨ (p ∧ r) := by exact this ``` + + +``have``策略中的类型可以省略，所以你可以写``have hp := h.left``和``have hqr := h.right``。 事实上，使用这种符号，你甚至可以省略类型和标签，在这种情况下，新的事实是用标签``this``引入的。 ```lean example (p q r : Prop) : p ∧ (q ∨ r) → (p ∧ q) ∨ (p ∧ r) := by @@ -822,10 +1110,14 @@ example (p q r : Prop) : p ∧ (q ∨ r) → (p ∧ q) ∨ (p ∧ r) := by apply Or.inr; exact this ``` + + +Lean还有一个``let``策略，与``have``策略类似，但用于引入局部定义而不是辅助事实。它是证明项中``let``的策略版。 ```lean example : ∃ x, x + 2 = 8 := by @@ -833,6 +1125,7 @@ example : ∃ x, x + 2 = 8 := by exists a ``` + + +和``have``一样，你可以通过写``let a := 3 * 2``来保留类型为隐式。``let``和``have``的区别在于，``let``在上下文中引入了一个局部定义，因此局部声明的定义可以在证明中展开。 + +我们使用了`.`来创建嵌套的策略块。 在一个嵌套块中，Lean专注于第一个目标，如果在该块结束时还没有完全解决，就会产生一个错误。这对于表明一个策略所引入的多个子目标的单独证明是有帮助的。符号``.``是对空格敏感的，并且依靠缩进来检测策略块是否结束。另外，你也可以用大括号和分号来定义策略块。 ```lean example (p q r : Prop) : p ∧ (q ∨ r) ↔ (p ∧ q) ∨ (p ∧ r) := by @@ -865,11 +1163,15 @@ example (p q r : Prop) : p ∧ (q ∨ r) ↔ (p ∧ q) ∨ (p ∧ r) := by exact ⟨hpr.left, Or.inr hpr.right⟩ } } ``` + + +使用缩进来构造证明很有用：每次一个策略留下一个以上的子目标时，我们通过将它们封装在块中并缩进来分隔剩下的子目标。因此，如果将定理``foo``应用于一个目标产生了四个子目标，那么我们就可以期待这样的证明： ``` apply foo @@ -879,7 +1181,11 @@ expect the proof to look like this: . ``` + + +或 ``` apply foo @@ -889,7 +1195,11 @@ or case => ``` + + +或 ``` apply foo @@ -899,34 +1209,55 @@ or { } ``` + +策略组合器 +------------------ + + + +**策略组合器**是由旧策略形成新策略的操作。``by``隐含了一个序列组合器： ```lean example (p q : Prop) (hp : p) : p ∨ q := by apply Or.inl; assumption ``` + + +这里，`apply Or.inl; assumption`在功能上等同于一个单独的策略，它首先应用`apply Or.inl`，然后应用`assumption`。 + +在`t₁ <;> t₂`中，`<;>`操作符提供了一个*并行*的序列操作。`t₁`被应用于当前目标，然后`t₂`被应用于*所有*产生的子目标： ```lean example (p q : Prop) (hp : p) (hq : q) : p ∧ q := by constructor <;> assumption ``` + + +当所产生的目标能够以统一的方式完成时，或者，至少，当有可能以统一的方式在所有的目标上取得进展时，这就特别有用。 + +``first | t₁ | t₂ | ... | tₙ``应用每个`tᵢ`，直到其中一个成功，否则就失败： ```lean example (p q : Prop) (hp : p) : p ∨ q := by @@ -936,8 +1267,12 @@ example (p q : Prop) (hq : q) : p ∨ q := by first | apply Or.inl; assumption | apply Or.inr; assumption ``` + + +在第一个例子中，左分支成功了，而在第二个例子中，右分支成功了。在接下来的三个例子中，同样的复合策略在每种情况下都能成功。 ```lean example (p q r : Prop) (hp : p) : p ∨ q ∨ r := @@ -950,6 +1285,7 @@ example (p q r : Prop) (hr : r) : p ∨ q ∨ r := by repeat (first | apply Or.inl; assumption | apply Or.inr | assumption) ``` + + +该策略试图通过假设立即解决左边的析取项；如果失败，它就试图关注右边的析取项；如果不成功，它就调用假设策略。 + +毫无疑问，策略可能会失败。事实上，正是这种“失败”状态导致`first`组合器回溯并尝试下一个策略。``try``组合器建立了一个总是成功的策略，尽管可能是以一种平凡的方式：``try t``执行``t``并报告成功，即使``t``失败。它等同于``first | t | skip``，其中``skip``是一个什么都不做的策略（并且成功地做到了“什么都不做”）。在下一个例子中，第二个`constructor`在右边的合取项``q ∧ r``上成功了（注意，合取和析取是右结合的），但在第一个合取项上失败。`try`策略保证了序列组合的成功。 ```lean example (p q r : Prop) (hp : p) (hq : q) (hr : r) : p ∧ q ∧ r := by constructor <;> (try constructor) <;> assumption ``` + + +小心：``repeat (try t)``将永远循环，因为内部策略永远不会失败。 + +在一个证明中，往往有多个目标未完成。并行序列是一种布置方式，以便将一个策略应用于多个目标，但也有其他的方式可以做到这一点。例如，`all_goals t`将`t`应用于所有未完成的目标： ```lean example (p q r : Prop) (hp : p) (hq : q) (hr : r) : p ∧ q ∧ r := by @@ -985,9 +1332,13 @@ example (p q r : Prop) (hp : p) (hq : q) (hr : r) : p ∧ q ∧ r := by all_goals assumption ``` + + +在这种情况下，``any_goals``策略提供了一个更稳健的解决方案。它与``all_goals``类似，只是除非它的参数至少在一个目标上成功，否则就会失败。 ```lean example (p q r : Prop) (hp : p) (hq : q) (hr : r) : p ∧ q ∧ r := by @@ -996,8 +1347,12 @@ example (p q r : Prop) (hp : p) (hq : q) (hr : r) : p ∧ q ∧ r := by any_goals assumption ``` + + +下面``by``块中的第一个策略是反复拆分合取： ```lean example (p q r : Prop) (hp : p) (hq : q) (hr : r) : @@ -1006,7 +1361,11 @@ example (p q r : Prop) (hp : p) (hq : q) (hr : r) : all_goals assumption ``` + + +其实可以将整个策略压缩成一行： ```lean example (p q r : Prop) (hp : p) (hq : q) (hr : r) : @@ -1014,14 +1373,24 @@ example (p q r : Prop) (hp : p) (hq : q) (hr : r) : repeat (any_goals (first | constructor | assumption)) ``` + +组合器``focus t``确保``t``只影响当前的目标，暂时将其他目标从作用范围中隐藏。因此，如果`t`通常只影响当前目标，`focus (all_goals t)`与`t`具有相同的效果。 + + + +重写 +--------- + +在[计算式证明](./quantifiers_and_equality.md#计算式证明)一节中简要介绍了``rewrite``策略（简称``rw``）和 ``simp``策略。在本节和下一节中，我们将更详细地讨论它们。 + +``rewrite``策略提供了一种基本的机制，可以将替换应用于目标和假设，在处理等式时非常方便。该策略的最基本形式是``rewrite [t]``，其中``t``是一个类型断定为等式的项。例如，`t`可以是上下文中的一个假设`h : x = y`；可以是一个一般的法则，如`add_comm : ∀ x y, x + y = y + x`，在这个法则中，重写策略试图找到`x`和`y`的合适实例；或者可以是任何断言具体或一般等式的复合项。在下面的例子中，我们使用这种基本形式，用一个假设重写目标。 + + + +```lean +example (f : Nat → Nat) (k : Nat) (h₁ : f 0 = 0) (h₂ : k = 0) : f k = 0 := by + rw [h₂] -- 用 0 换掉 k + rw [h₁] -- 用 0 换掉 f 0 +``` + + +在上面的例子中，第一次使用``rw``将目标``f k = 0``中的``k``替换成``0``。然后，第二次用``0``替换``f 0``。该策略自动关闭任何形式的目标`t = t`。下面是一个使用复合表达式进行重写的例子。 ```lean example (x y : Nat) (p : Nat → Prop) (q : Prop) (h : q → x = y) @@ -1054,26 +1440,37 @@ example (x y : Nat) (p : Nat → Prop) (q : Prop) (h : q → x = y) rw [h hq]; assumption ``` + + +这里，``h hq``建立了等式``x = y``。``h hq``周围的括号是不必要的，但为了清楚起见，还是加上了括号。 + +多个重写可以使用符号`rw [t_1, ..., t_n]`来组合，这只是`rw t_1; ...; rw t_n`的缩写。前面的例子可以写成如下： ```lean example (f : Nat → Nat) (k : Nat) (h₁ : f 0 = 0) (h₂ : k = 0) : f k = 0 := by rw [h₂, h₁] ``` + + +默认情况下，``rw``正向使用一个等式，用一个表达式匹配左边的等式，然后用右边的等式替换它。符号``←t``可以用来指示策略在反方向上使用等式``t``。 ```lean example (f : Nat → Nat) (a b : Nat) (h₁ : a = b) (h₂ : f a = 0) : f b = 0 := by rw [←h₁, h₂] ``` + + +在这个例子中，项``←h₁``指示重写器用``a``替换``b``。在编辑器中，你可以用``\l``输入反箭头。你也可以使用ascii替代品``<-``。 + +有时一个等式的左侧可以匹配模式中的多个子项，在这种情况下，``rw``策略会在遍历项时选择它发现的第一个匹配。如果这不是你想要的，你可以使用附加参数来指定适当的子项。 ```lean example (a b c : Nat) : a + b + c = a + c + b := by @@ -1095,6 +1497,7 @@ example (a b c : Nat) : a + b + c = a + c + b := by rw [Nat.add_assoc, Nat.add_assoc, Nat.add_comm _ b] ``` + + +在上面的第一个例子中，第一步将``a + b + c``重写为``a + (b + c)``。然后，接下来对项``b + c``使用交换律；如果不指定参数，该策略将把``a + (b + c)``重写为``(b + c) + a``。最后一步以相反的方向应用结合律，将`a + (c + b)`改写为``a + c + b``。接下来的两个例子则是应用结合律将两边的小括号移到右边，然后将``b``和``c``调换。注意最后一个例子通过指定``Nat.add_comm``的第二个参数来指定重写应该在右侧进行。 + +默认情况下，``rewrite``策略只影响目标。符号``rw [t] at h``在假设``h``处应用重写``t``。 ```lean example (f : Nat → Nat) (a : Nat) (h : a + 0 = 0) : f a = f 0 := by @@ -1115,11 +1523,17 @@ example (f : Nat → Nat) (a : Nat) (h : a + 0 = 0) : f a = f 0 := by rw [h] ``` + + +第一步，``rw [Nat.add_zero] at h``将假设``a + 0 = 0``改写为``a = 0``。然后，新的假设`a = 0`被用来把目标重写为`f 0 = f 0`。 + +``rewrite``策略不限于命题。在下面的例子中，我们用`rw [h] at t`来重写假设`t : Tuple α n`为`t : Tuple α 0`。 ```lean def Tuple (α : Type) (n : Nat) := @@ -1130,14 +1544,23 @@ example (n : Nat) (h : n = 0) (t : Tuple α n) : Tuple α 0 := by exact t ``` + + +简化 +-------------------- + + +``rewrite``被设计为操纵目标的手术刀，而简化器提供了一种更强大的自动化形式。Lean库中的一些特性已经被标记为`[simp]`属性，`simp`策略使用它们来反复重写表达式中的子项。 ```lean example (x y z : Nat) : (x + 0) * (0 + y * 1 + z * 0) = x * y := by @@ -1148,6 +1571,7 @@ example (x y z : Nat) (p : Nat → Prop) (h : p (x * y)) simp; assumption ``` + + +在第一个例子中，目标中等式的左侧被简化，使用涉及0和1的通常的同义词，将目标简化为`x * y = x * y'`。此时`simp'`应用反身性（rfl）来完成它。在第二个例子中，`simp`将目标化简为`p (x * y)`，这时假设`h`完成了它。下面是一些关于列表的例子。 ```lean open List @@ -1168,7 +1595,11 @@ example (xs ys : List α) simp [Nat.add_comm] ``` + + +就像``rw``，你也可以用关键字``at``来简化一个假设： ```lean example (x y z : Nat) (p : Nat → Prop) @@ -1176,7 +1607,11 @@ example (x y z : Nat) (p : Nat → Prop) simp at h; assumption ``` + + +此外，你可以使用一个“通配符”星号来简化所有的假设和目标： ```lean attribute [local simp] Nat.mul_comm Nat.mul_assoc Nat.mul_left_comm @@ -1192,6 +1627,7 @@ example (x y z : Nat) (p : Nat → Prop) simp at * <;> constructor <;> assumption ``` + + +上例中前两行的意思是，对于具有交换律和结合律的运算（如自然数的加法和乘法），简化器使用这两个定律来重写表达式，同时还使用*左交换律*。在乘法的情况下，左交换律表达如下：``x * (y * z) = y * (x * z)``。`local`修饰符告诉简化器在当前文件（或小节或命名空间，视情况而定）中使用这些规则。交换律和左交换律是有一个问题是，重复应用其中一个会导致循环。但是简化器检测到了对其参数进行置换的特性，并使用了一种被称为*有序重写*的技术。这意味着系统保持着项的内部次序，只有在这样做会降低次序的情况下才会应用等式。对于上面提到的三个等式，其效果是表达式中的所有小括号都被结合到右边，并且表达式以一种规范的（尽管有些随意）方式排序。两个在交换律和结合律上等价的表达式然后被改写成相同的规范形式。 ```lean # attribute [local simp] Nat.mul_comm Nat.mul_assoc Nat.mul_left_comm @@ -1223,12 +1662,16 @@ example (w x y z : Nat) (p : Nat → Prop) simp; simp at h; assumption ``` + + +与``rewrite``一样，你可以向``simp``提供一个要使用的事实列表，包括一般引理、局部假设、要展开的定义和复合表达式。`simp`策略也能识别`rewrite`的`←t`语法。在任何情况下，额外的规则都会被添加到用于简化项的等式集合中。 ```lean def f (m n : Nat) : Nat := @@ -1238,22 +1681,34 @@ example {m n : Nat} (h : n = 1) (h' : 0 = m) : (f m n) = n := by simp [h, ←h', f] ``` + + +一个常见的习惯是用局部假设来简化一个目标： ```lean example (f : Nat → Nat) (k : Nat) (h₁ : f 0 = 0) (h₂ : k = 0) : f k = 0 := by simp [h₁, h₂] ``` + + +为了在简化时使用局部环境中存在的所有假设，我们可以使用通配符``*``： ```lean example (f : Nat → Nat) (k : Nat) (h₁ : f 0 = 0) (h₂ : k = 0) : f k = 0 := by simp [*] ``` + + +另一例： ```lean example (u w x y z : Nat) (h₁ : x = y + z) (h₂ : w = u + x) @@ -1261,10 +1716,14 @@ example (u w x y z : Nat) (h₁ : x = y + z) (h₂ : w = u + x) simp [*, Nat.add_assoc, Nat.add_comm, Nat.add_left_comm] ``` + + +简化器也会进行命题重写。例如，使用假设``p``，它把``p ∧ q``改写为``q``，把``p ∨ q``改写为``true``，然后以普通方式证明。迭代这样的重写，会生成非平凡的命题推理。 ```lean example (p q : Prop) (hp : p) : p ∧ q ↔ q := by @@ -1277,7 +1736,11 @@ example (p q r : Prop) (hp : p) (hq : q) : p ∧ (q ∨ r) := by simp [*] ``` + + +下一个例子简化了所有的假设，然后用这些假设来证明目标。 ```lean example (u w x x' y y' z : Nat) (p : Nat → Prop) @@ -1287,18 +1750,26 @@ example (u w x x' y y' z : Nat) (p : Nat → Prop) simp [*] ``` + + +使得简化器特别有用的一点是，它的能力可以随着规则库的发展而增强。例如，假设我们定义了一个列表操作，该操作通过拼接其反转来对称其输入： ```lean def mk_symm (xs : List α) := xs ++ xs.reverse ``` + + +那么对于任何列表``xs``，``reverse (mk_symm xs)``等于``mk_symm xs``，这可以通过展开定义轻松证明： ```lean # def mk_symm (xs : List α) := @@ -1308,7 +1779,11 @@ theorem reverse_mk_symm (xs : List α) simp [mk_symm] ``` + + +你可以使用这个定理来证明一些新结果： ```lean # def mk_symm (xs : List α) := @@ -1326,10 +1801,14 @@ example (xs ys : List Nat) (p : List Nat → Prop) simp [reverse_mk_symm] at h; assumption ``` + + +但是使用`reverse_mk_symm`通常是正确的，如果用户不需要明确地调用它，那就更好了。你可以通过在定义该定理时将其标记为简化规则来实现这一点： ```lean # def mk_symm (xs : List α) := @@ -1348,8 +1827,12 @@ example (xs ys : List Nat) (p : List Nat → Prop) simp at h; assumption ``` + + +符号``@[simp]``声明``reverse_mk_symm``具有``[simp]``属性，可以更明确地说明： ```lean # def mk_symm (xs : List α) := @@ -1370,7 +1853,11 @@ example (xs ys : List Nat) (p : List Nat → Prop) simp at h; assumption ``` + + +该属性也可以在定理声明后的任何时候应用： ```lean # def mk_symm (xs : List α) := @@ -1391,11 +1878,15 @@ example (xs ys : List Nat) (p : List Nat → Prop) simp at h; assumption ``` + + +然而，一旦属性被应用，就没有办法永久地删除它；它将在任何导入该属性的文件中持续存在。正如我们将在[属性](./interacting_with_lean.md#属性)一章中进一步讨论的那样，我们可以使用``local``修饰符将属性的范围限制在当前文件或章节中： ```lean # def mk_symm (xs : List α) := @@ -1418,6 +1909,7 @@ example (xs ys : List Nat) (p : List Nat → Prop) end ``` + + +在该部分之外，简化器将不再默认使用``reverse_mk_symm``。 + +请注意，我们讨论过的各种`simp`选项----给出一个明确的规则列表，并使用`at`指定位置----可以合并，但它们的排列顺序是严格的。你可以在编辑器中看到正确的顺序，把光标放在``simp``标识符上，查看与之相关的文档。 + +有两个额外的修饰符是有用的。默认情况下，``simp``包括所有被标记为``[simp]``属性的定理。写`simp only`排除了这些默认值，允许你使用一个更明确的规则列表。在下面的例子中，减号和``only``被用来阻止``reverse_mk_symm``的应用： ```lean def mk_symm (xs : List α) := @@ -1457,34 +1956,56 @@ example (xs ys : List Nat) (p : List Nat → Prop) simp only [List.reverse_append] at h; assumption ``` + + +`simp`策略有很多配置选项，例如，我们可以启用语境简化： ```lean example : if x = 0 then y + x = y else x ≠ 0 := by simp (config := { contextual := true }) ``` + + +当`contextual := true`，`simp`简化`y + x = y`时会使用`x = 0`，同时会用`x ≠ 0`来简化另一侧。另一个例子： ```lean example : ∀ (x : Nat) (h : x = 0), y + x = y := by simp (config := { contextual := true }) ``` + + +另一个有用的配置是`arith := true`，它会简化算术表达式。因为这太常用了所以用`simp_arith`作为`simp (config := { arith := true })`的缩写。 ```lean example : 0 < 1 + x ∧ x + y + 2 ≥ y + 1 := by simp_arith ``` + +拆分 +------------ + + + +``split``策略对于在多情形分支结构中打破嵌套的`if-then-else`和`match`表达式很有用。 +对于包含`n`种情形的`match`表达式，`split`策略最多生成`n`个子目标。例子： ```lean def f (x y z : Nat) : Nat := @@ -1504,7 +2025,11 @@ example (x y z : Nat) : x ≠ 5 → y ≠ 5 → z ≠ 5 → z = w → f x y w = . rfl ``` + + +可以压缩成一行： ```lean # def f (x y z : Nat) : Nat := @@ -1517,9 +2042,15 @@ example (x y z : Nat) : x ≠ 5 → y ≠ 5 → z ≠ 5 → z = w → f x y w = intros; simp [f]; split <;> first | contradiction | rfl ``` + + +策略`split <;> first | contradiction | rfl`首先应用`split`策略，接着对每个生成出的目标尝试`contradiction`，如果失败那么最后`rfl`。 + +类似`simp`，我们对一个特定的假设也可以使用`split`。 ```lean def g (xs ys : List Nat) : Nat := @@ -1532,14 +2063,24 @@ example (xs ys : List Nat) (h : g xs ys = 0) : False := by simp [g] at h; split at h <;> simp_arith at h ``` + +扩展策略 +----------------- + + + +在下面的例子中，我们使用`syntax`命令定义符号`triv`。然后，我们使用`macro_rules`命令来指定使用`triv`时应该做什么。你可以提供不同的扩展，策略解释器将尝试所有的扩展，直到有一个成功。 + + +```lean +-- 定义一个新策略符号 +syntax "triv" : tactic + +macro_rules + | `(tactic| triv) => `(tactic| assumption) + +example (h : p) : p := by + triv + +-- 你不能用`triv`解决下面的定理： +-- example (x : α) : x = x := by +-- triv + +-- 扩展`triv`。策略解释器会尝试所有可能的扩展宏，直到有一个成功。 +macro_rules + | `(tactic| triv) => `(tactic| rfl) + +example (x : α) : x = x := by + triv + +example (x : α) (h : p) : x = x ∧ p := by + apply And.intro <;> triv + +-- 加一个递归扩展 +macro_rules | `(tactic| triv) => `(tactic| apply And.intro <;> triv) + example (x : α) (h : p) : x = x ∧ p := by triv ``` + +练习 +--------- + + + +1. 用策略式证明重做[命题与证明](./propositions_and_proofs.md)和[量词与等价](./quantifiers_and_equality.md)两章的练习。适当使用``rw``和``simp``。 +2. 用策略组合器给下面的例子用一行写一个证明： ```lean example (p q r : Prop) (hp : p) : (p ∨ q ∨ r) ∧ (q ∨ p ∨ r) ∧ (q ∨ r ∨ p) := by