diff --git a/axioms_and_computation.html b/axioms_and_computation.html index fde8787..e31ef8d 100644 --- a/axioms_and_computation.html +++ b/axioms_and_computation.html @@ -361,7 +361,7 @@
在通过了证明无关的 Prop
之后,可以认为使用排中律 p ∨ ¬p
是合法的,
-其中 p
是任何命题。当然,这也可能根据 CIC 的规则阻止计算,
+其中 p
是任何命题。当然,这也可能根据 CIC 的规则阻止计算,
但它不会阻止字节码求值,如上所述。仅在 :numref:choice
中讨论过的选择原则才能完全消除理论中与证明无关的部分和与数据相关部分之间的区别。
和归纳定义的类型以及相关的构造器和递归器一样,它们也被视为逻辑框架的一部分。
+和归纳定义的类型以及相关的构造子和递归器一样,它们也被视为逻辑框架的一部分。
-结合Quotient.sound
,这意味着商的各个元素精确对应于 α
中各元素的等价类。
结合 Quotient.sound
,这意味着商的各个元素精确对应于 α
中各元素的等价类。
首先,我们导入必要的公理,并定义两个谓词U
和V
:
首先,我们导入必要的公理,并定义两个谓词 U
和 V
:
namespace Hidden
open Classical
theorem em (p : Prop) : p ∨ ¬p :=
diff --git a/dependent_type_theory.html b/dependent_type_theory.html
index fcc56a5..cca6a05 100644
--- a/dependent_type_theory.html
+++ b/dependent_type_theory.html
@@ -155,7 +155,7 @@ 依值类型
hierarchy of non-cumulative universes and inductive types. By the end
of this chapter, you will understand much of what this means.
-->
-依值类型论(Dependent type theory)是一种强大而富有表达力的语言,允许你表达复杂的数学断言,编写复杂的硬件和软件规范,并以自然和统一的方式对这两者进行推理。Lean是基于一个被称为构造演算(Calculus of Constructions)的依值类型论的版本,它拥有一个可数的非累积性宇宙(non-cumulative universe)的层次结构以及归纳类型(Inductive type)。在本章结束时,你将学会一大部分。
+依值类型论(Dependent type theory)是一种强大而富有表达力的语言,允许你表达复杂的数学断言,编写复杂的硬件和软件规范,并以自然和统一的方式对这两者进行推理。Lean 是基于一个被称为构造演算(Calculus of Constructions)的依值类型论的版本,它拥有一个可数的非累积性宇宙(non-cumulative universe)的层次结构以及归纳类型(Inductive type)。在本章结束时,你将学会一大部分。
@@ -167,7 +167,7 @@ 简单类型
numbers. For those who like precise definitions, a Lean natural number
is an arbitrary-precision unsigned integer.
-->
-「类型论」得名于其中每个表达式都有一个类型。举例:在一个给定的语境中,x + 0
可能表示一个自然数,f
可能表示一个定义在自然数上的函数。Lean中的自然数是任意精度的无符号整数。
+「类型论」得名于其中每个表达式都有一个类型。举例:在一个给定的语境中,x + 0
可能表示一个自然数,f
可能表示一个定义在自然数上的函数。Lean 中的自然数是任意精度的无符号整数。
-Lean所依据的依值类型论对简单类型论的其中一项升级是,类型本身(如 Nat
和 Bool
这些东西)也是对象,因此也具有类型。
+Lean 所依据的依值类型论对简单类型论的其中一项升级是,类型本身(如 Nat
和 Bool
这些东西)也是对象,因此也具有类型。
#check Nat -- Type
#check Bool -- Type
#check Nat → Bool -- Type
@@ -438,7 +438,7 @@ 类型
Lean's typing system. Lean's underlying foundation has an infinite
hierarchy of types:
-->
-实际上,这是 Lean 系统的一个最微妙的方面:Lean的底层基础有无限的类型层次:
+实际上,这是 Lean 系统的一个最微妙的方面:Lean 的底层基础有无限的类型层次:
#check Type -- Type 1
#check Type 1 -- Type 2
#check Type 2 -- Type 3
@@ -475,7 +475,7 @@ 类型
``α``, no matter which type universe ``α`` lives in. This explains the
type signature of the function ``List``:
-->
-然而,有些操作需要在类型宇宙上具有多态(polymorphic)。例如,List α
应该对任何类型的 α
都有意义,无论 α
存在于哪种类型的宇宙中。所以函数 List
有如下的类型:
+然而,有些操作需要在类型宇宙上具有多态(Polymorphic)。例如,List α
应该对任何类型的 α
都有意义,无论 α
存在于哪种类型的宇宙中。所以函数 List
有如下的类型:
#check List -- List.{u} (α : Type u) : Type u
函数抽象和求值
-Lean提供 fun
(或 λ
)关键字用于从给定表达式创建函数,如下所示:
+Lean 提供 fun
(或 λ
)关键字用于从给定表达式创建函数,如下所示:
-Lean将这三个例子解释为相同的表达式;在最后一个表达式中,Lean可以从表达式if not y then x + 1 else x + 2
推断 x
和 y
的类型。
+Lean 将这三个例子解释为相同的表达式;在最后一个表达式中,Lean 可以从表达式if not y then x + 1 else x + 2
推断 x
和 y
的类型。
一些数学上常见的函数运算的例子可以用 lambda 抽象的项来描述:
def f (n : Nat) : String := toString n
def g (s : String) : Bool := s.length > 0
@@ -611,7 +611,7 @@
following expressions:
-->
这个表达式表示一个接受三个类型 α
,β
和 γ
和两个函数 g : β → γ
和 f : α → β
,并返回的 g
和 f
的复合的函数。(理解这个函数的类型需要理解依值积类型,下面将对此进行解释。)
-lambda表达式的一般形式是 fun x : α => t
,其中变量 x
是一个绑定变量(bound variable):它实际上是一个占位符,其「作用域」没有扩展到表达式 t
之外。例如,表达式 fun (b : β) (x : α) => b
中的变量 b
与前面声明的常量 b
没有任何关系。事实上,这个表达式表示的函数与 fun (u : β) (z : α) => u
是一样的。形式上,可以通过给绑定变量重命名来使形式相同的表达式被看作是alpha等价的,也就是被认为是「一样的」。Lean认识这种等价性。
+lambda表达式的一般形式是 fun x : α => t
,其中变量 x
是一个绑定变量(Bound Variable):它实际上是一个占位符,其「作用域」没有扩展到表达式 t
之外。例如,表达式 fun (b : β) (x : α) => b
中的变量 b
与前面声明的常量 b
没有任何关系。事实上,这个表达式表示的函数与 fun (u : β) (z : α) => u
是一样的。形式上,可以通过给绑定变量重命名来使形式相同的表达式被看作是alpha等价的,也就是被认为是「一样的」。Lean 认识这种等价性。
注意到项 t : α → β
应用到项 s : α
上导出了表达式 t s : β
。回到前面的例子,为清晰起见给绑定变量重命名,注意以下表达式的类型:
#check (fun x : Nat => x) 1 -- Nat
#check (fun x : Nat => true) 1 -- Bool
@@ -647,7 +647,7 @@
preferred way of testing your functions.
-->
稍后你将看到这些项是如何计算的。现在,请注意这是依值类型论的一个重要特征:每个项都有一个计算行为,并支持「标准化」的概念。从原则上讲,两个可以化约为相同形式的项被称为「定义等价」。它们被 Lean 的类型检查器认为是「相同的」,并且 Lean 尽其所能地识别和支持这些识别结果。
-Lean是个完备的编程语言。它有一个生成二进制可执行文件的编译器,和一个交互式解释器。你可以用#eval
命令执行表达式,这也是测试你的函数的好办法。
+Lean 是个完备的编程语言。它有一个生成二进制可执行文件的编译器,和一个交互式解释器。你可以用#eval
命令执行表达式,这也是测试你的函数的好办法。
-定义的一般形式是 def foo : α := bar
,其中 α
是表达式 bar
返回的类型。Lean通常可以推断类型 α
,但是精确写出它可以澄清你的意图,并且如果定义的右侧没有匹配你的类型,Lean将标记一个错误。
+定义的一般形式是 def foo : α := bar
,其中 α
是表达式 bar
返回的类型。Lean 通常可以推断类型 α
,但是精确写出它可以澄清你的意图,并且如果定义的右侧没有匹配你的类型,Lean 将标记一个错误。
bar
可以是任何一个表达式,不只是一个 lambda 表达式。因此 def
也可以用于给一些值命名,例如:
def pi := 3.141592654
@@ -824,7 +824,7 @@ 局部定义
-
Lean还允许你使用 let
关键字来引入「局部定义」。表达式 let a := t1; t2
定义等价于把 t2
中所有的 a
替换成 t1
的结果。
+Lean 还允许你使用 let
关键字来引入「局部定义」。表达式 let a := t1; t2
定义等价于把 t2
中所有的 a
替换成 t1
的结果。
#check let y := 2 + 2; y * y -- Nat
#eval let y := 2 + 2; y * y -- 16
@@ -891,7 +891,7 @@ 变量和小
Lean provides you with the ``variable`` command to make such
declarations look more compact:
-->
-Lean提供 variable
指令来让这些声明变得紧凑:
+Lean 提供 variable
指令来让这些声明变得紧凑:
variable (α β γ : Type)
def compose (g : β → γ) (f : α → β) (x : α) : γ :=
@@ -937,8 +937,8 @@ 变量和小
a ``section``:
-->
输出结果表明所有三组定义具有完全相同的效果。
-variable
命令指示 Lean 将声明的变量作为绑定变量插入定义中,这些定义通过名称引用它们。Lean足够聪明,它能找出定义中显式或隐式使用哪些变量。因此在写定义时,你可以将 α
、β
、γ
、g
、f
、h
和 x
视为固定的对象,并让 Lean 自动抽象这些定义。
-当以这种方式声明时,变量将一直保持存在,直到所处理的文件结束。然而,有时需要限制变量的作用范围。Lean提供了小节标记 section
来实现这个目的:
+variable
命令指示 Lean 将声明的变量作为绑定变量插入定义中,这些定义通过名称引用它们。Lean 足够聪明,它能找出定义中显式或隐式使用哪些变量。因此在写定义时,你可以将 α
、β
、γ
、g
、f
、h
和 x
视为固定的对象,并让 Lean 自动抽象这些定义。
+当以这种方式声明时,变量将一直保持存在,直到所处理的文件结束。然而,有时需要限制变量的作用范围。Lean 提供了小节标记 section
来实现这个目的:
section useful
variable (α β γ : Type)
variable (g : β → γ) (f : α → β) (h : α → α)
@@ -969,7 +969,7 @@ 命名空间
-
Lean可以让你把定义放进一个「命名空间」(namespace
)里,并且命名空间也是层次化的:
+Lean 可以让你把定义放进一个「命名空间」(namespace
)里,并且命名空间也是层次化的:
namespace Foo
def a : Nat := 5
def f (x : Nat) : Nat := x + 7
@@ -1019,7 +1019,7 @@ 命名空间
当你声明你在命名空间 Foo
中工作时,你声明的每个标识符都有一个前缀 Foo.
。在打开的命名空间中,可以通过较短的名称引用标识符,但是关闭命名空间后,必须使用较长的名称。与 section
不同,命名空间需要一个名称。只有一个匿名命名空间在根级别上。
open
命令使你可以在当前使用较短的名称。通常,当你导入一个模块时,你会想打开它包含的一个或多个命名空间,以访问短标识符。但是,有时你希望将这些信息保留在一个完全限定的名称中,例如,当它们与你想要使用的另一个命名空间中的标识符冲突时。因此,命名空间为你提供了一种在工作环境中管理名称的方法。
-例如,Lean把和列表相关的定义和定理都放在了命名空间 List
之中。
+例如,Lean 把和列表相关的定义和定理都放在了命名空间 List
之中。
#check List.nil
#check List.cons
#check List.map
@@ -1164,7 +1164,7 @@ 量词与等价一章中有更详细的说明。同时,依值类型有着更丰富的引入动机,推荐读者寻找一些拓展读物。
+
译者注:在依值类型论的数学符号体系中,依值类型是用 Π
符号来表达的,在Lean 3中还使用这种表达,例如 Π x : α, β x
。Lean 4抛弃了这种不友好的写法。(x : α) → β x
这种写法在引入「构造子」之后意义会更明朗一些(见下一个注释),对于来自数学背景的读者可以把它类比于 forall x : α, β x
这种写法(这也是合法的 Lean 语句),关于前一种符号在量词与等价一章中有更详细的说明。同时,依值类型有着更丰富的引入动机,推荐读者寻找一些拓展读物。
回到列表的例子,你可以使用#check
命令来检查下列的 List
函数。@
符号以及圆括号和花括号之间的区别将在后面解释。
#check @List.cons -- {α : Type u_1} → α → List α → List α
@@ -1260,9 +1260,9 @@ 隐参数
that the system should fill in the information automatically. This is
known as an "implicit argument."
-->
-由于构造器对类型是多态的【注】,我们需要重复插入类型 Nat
作为一个参数。但是这个信息是多余的:我们可以推断表达式 Lst.cons Nat 5 (Lst.nil Nat)
中参数 α
的类型,这是通过第二个参数 5
的类型是 Nat
来实现的。类似地,我们可以推断 Lst.nil Nat
中参数的类型,这是通过它作为函数 Lst.cons
的一个参数,且这个函数在这个位置需要接收的是一个具有 Lst α
类型的参数来实现的。
+由于构造子对类型是多态的【注】,我们需要重复插入类型 Nat
作为一个参数。但是这个信息是多余的:我们可以推断表达式 Lst.cons Nat 5 (Lst.nil Nat)
中参数 α
的类型,这是通过第二个参数 5
的类型是 Nat
来实现的。类似地,我们可以推断 Lst.nil Nat
中参数的类型,这是通过它作为函数 Lst.cons
的一个参数,且这个函数在这个位置需要接收的是一个具有 Lst α
类型的参数来实现的。
-译者注:「构造器」(Constructor)的概念前文未加解释,对类型论不熟悉的读者可能会困惑。它指的是一种「依值类型的类型」,也可以看作「类型的构造器」,例如 λ α : α -> α
甚至可看成 ⋆ -> ⋆
。当给 α
或者 ⋆
赋予一个具体的类型时,这个表达式就成为了一个类型。前文中 (x : α) → β x
中的 β
就可以看成一个构造器,(x : α)
就是传进的类型参数。原句「构造器对类型是多态的」意为给构造器中放入不同类型时它会变成不同类型。
+译者注:「构造子」(Constructor)的概念前文未加解释,对类型论不熟悉的读者可能会困惑。它指的是一种「依值类型的类型」,也可以看作「类型的构造子」,例如 λ α : α -> α
甚至可看成 ⋆ -> ⋆
。当给 α
或者 ⋆
赋予一个具体的类型时,这个表达式就成为了一个类型。前文中 (x : α) → β x
中的 β
就可以看成一个构造子,(x : α)
就是传进的类型参数。原句「构造子对类型是多态的」意为给构造子中放入不同类型时它会变成不同类型。
这是依值类型论的一个主要特征:项包含大量信息,而且通常可以从上下文推断出一些信息。在 Lean 中,我们使用下划线 _
来指定系统应该自动填写信息。这就是所谓的「隐参数」。
universe u
@@ -1288,7 +1288,7 @@ 隐参数
default, be left implicit. This is done by putting the arguments in
curly braces, as follows:
-->
-然而,敲这么多下划线仍然很无聊。当一个函数接受一个通常可以从上下文推断出来的参数时,Lean允许你指定该参数在默认情况下应该保持隐式。这是通过将参数放入花括号来实现的,如下所示:
+然而,敲这么多下划线仍然很无聊。当一个函数接受一个通常可以从上下文推断出来的参数时,Lean 允许你指定该参数在默认情况下应该保持隐式。这是通过将参数放入花括号来实现的,如下所示:
universe u
def Lst (α : Type u) : Type u := List α
@@ -1363,7 +1363,7 @@ 隐参数
``List.nil``:
-->
此处定义的 ident
和上面那个效果是一样的。
-Lean有非常复杂的机制来实例化隐参数,我们将看到它们可以用来推断函数类型、谓词,甚至证明。实例化这些「洞」或「占位符」的过程通常被称为繁饰(Elaboration)。隐参数的存在意味着有时可能没有足够的信息来精确地确定表达式的含义。像 id
或 List.nil
这样的表达式被认为是「多态的」,因为它可以在不同的上下文中具有不同的含义。
+Lean 有非常复杂的机制来实例化隐参数,我们将看到它们可以用来推断函数类型、谓词,甚至证明。实例化这些「洞」或「占位符」的过程通常被称为繁饰(Elaboration)。隐参数的存在意味着有时可能没有足够的信息来精确地确定表达式的含义。像 id
或 List.nil
这样的表达式被认为是「多态的」,因为它可以在不同的上下文中具有不同的含义。
可以通过写 (e : T)
来指定表达式 e
的类型 T
。这就指导 Lean 的繁饰器在试图解决隐式参数时使用值 T
作为 e
的类型。在下面的第二个例子中,这种机制用于指定表达式 id
和 List.nil
所需的类型:
#check List.nil -- List ?m
#check id -- ?m → ?m
@@ -1378,7 +1378,7 @@ 隐参数
elaborated in the same way, whereas the third ``#check`` command
interprets ``2`` as an integer.
-->
-Lean中数字是重载的,但是当数字的类型不能被推断时,Lean默认假设它是一个自然数。因此,下面的前两个 #check
命令中的表达式以同样的方式进行了繁饰,而第三个 #check
命令将 2
解释为整数。
+Lean 中数字是重载的,但是当数字的类型不能被推断时,Lean 默认假设它是一个自然数。因此,下面的前两个 #check
命令中的表达式以同样的方式进行了繁饰,而第三个 #check
命令将 2
解释为整数。
#check 2 -- Nat
#check (2 : Nat) -- Nat
#check (2 : Int) -- Int
diff --git a/induction_and_recursion.html b/induction_and_recursion.html
index 256c770..904bd2c 100644
--- a/induction_and_recursion.html
+++ b/induction_and_recursion.html
@@ -164,7 +164,7 @@ 归纳和递
of the trusted code base; its output consists of terms that are
checked independently by the kernel.
-->
-在上一章中,我们看到归纳定义提供了在 Lean 中引入新类型的强大手段。此外,构造器和递归器提供了在这些类型上定义函数的唯一手段。命题即类型的对应关系,意味着归纳法是证明的基本方法。
+在上一章中,我们看到归纳定义提供了在 Lean 中引入新类型的强大手段。此外,构造子和递归器提供了在这些类型上定义函数的唯一手段。命题即类型的对应关系,意味着归纳法是证明的基本方法。
Lean 提供了定义递归函数、执行模式匹配和编写归纳证明的自然方法。它允许你通过指定它应该满足的方程来定义一个函数,它允许你通过指定如何处理可能出现的各种情况来证明一个定理。在它内部,这些描述被「方程编译器」程序「编译」成原始递归器。方程编译器不是可信代码库的一部分;它的输出包括由内核独立检查的项。
-对示意图模式的解释是编译过程的第一步。我们已经看到,casesOn
递归器可以通过分情况讨论来定义函数和证明定理,根据归纳定义类型所涉及的构造器。但是复杂的定义可能会使用几个嵌套的 casesOn
应用,而且可能很难阅读和理解。模式匹配提供了一种更方便的方法,并且为函数式编程语言的用户所熟悉。
+对示意图模式的解释是编译过程的第一步。我们已经看到,casesOn
递归器可以通过分情况讨论来定义函数和证明定理,根据归纳定义类型所涉及的构造子。但是复杂的定义可能会使用几个嵌套的 casesOn
应用,而且可能很难阅读和理解。模式匹配提供了一种更方便的方法,并且为函数式编程语言的用户所熟悉。
考虑一下自然数的归纳定义类型。每个自然数要么是 zero
,要么是 succ x
,因此你可以通过在每个情况下指定一个值来定义一个从自然数到任意类型的函数:
open Nat
@@ -238,7 +238,7 @@ 模式匹配
-
因为加法和零符号已经被赋予 [matchPattern]
属性,它们可以被用于模式匹配。Lean 简单地将这些表达式规范化,直到显示构造器 zero
和 succ
。
+因为加法和零符号已经被赋予 [matchPattern]
属性,它们可以被用于模式匹配。Lean 简单地将这些表达式规范化,直到显示构造子 zero
和 succ
。
模式匹配适用于任何归纳类型,如乘积和 Option 类型:
def swap : α × β → β × α
| (a, b) => (b, a)
@@ -284,7 +284,7 @@ 模式匹配
这样解决带逻辑连接词的命题就很紧凑。
-在所有这些例子中,模式匹配被用来进行单一情况的区分。更有趣的是,模式可以涉及嵌套的构造器,如下面的例子。
+在所有这些例子中,模式匹配被用来进行单一情况的区分。更有趣的是,模式可以涉及嵌套的构造子,如下面的例子。
def sub2 : Nat → Nat
| 0 => 0
| 1 => 0
@@ -400,7 +400,7 @@ 模式匹配
-
还要注意的是,当定义中不需要一个参数的值时,你可以用下划线来代替。这个下划线被称为通配符模式,或匿名变量。与方程编译器之外的用法不同,这里的下划线并不表示一个隐参数。使用下划线表示通配符在函数式编程语言中是很常见的,所以 Lean 采用了这种符号。通配符和重叠模式一节阐述了通配符的概念,而不可访问模式一节解释了你如何在模式中使用隐参数。
+还要注意的是,当定义中不需要一个参数的值时,你可以用下划线来代替。这个下划线被称为通配符模式,或匿名变量。与方程编译器之外的用法不同,这里的下划线并不表示一个隐参数。使用下划线表示通配符在函数式编程语言中是很常见的,所以 Lean 采用了这种符号。通配符和重叠模式一节阐述了通配符的概念,而不可访问模式一节解释了你如何在模式中使用隐参数。
正如归纳类型一章中所描述的,归纳数据类型可以依赖于参数。下面的例子使用模式匹配定义了 tail
函数。参数 α : Type
是一个参数,出现在冒号之前,表示它不参与模式匹配。Lean 也允许参数出现在 :
之后,但它不能对其进行模式匹配。
def tail1 {α : Type u} : List α → List α
| [] => []
@@ -422,7 +422,7 @@ 模式匹配
尽管参数 α
在这两个例子中的位置不同,但在这两种情况下,它的处理方式是一样的,即它不参与情况分割。
-Lean也可以处理更复杂的模式匹配形式,其中从属类型的参数对各种情况构成了额外的约束。这种依值模式匹配的例子在依值模式匹配一节中考虑。
+Lean 也可以处理更复杂的模式匹配形式,其中从属类型的参数对各种情况构成了额外的约束。这种依值模式匹配的例子在依值模式匹配一节中考虑。
-在第二种表述中,模式是重叠的;例如,一对参数 0 0
符合所有三种情况。但是Lean通过使用第一个适用的方程来处理这种模糊性,所以在这个例子中,最终结果是一样的。特别是,以下方程在定义上是成立的:
+在第二种表述中,模式是重叠的;例如,一对参数 0 0
符合所有三种情况。但是Lean 通过使用第一个适用的方程来处理这种模糊性,所以在这个例子中,最终结果是一样的。特别是,以下方程在定义上是成立的:
def foo : Nat → Nat → Nat
| 0, n => 0
| m, 0 => 1
@@ -466,7 +466,7 @@ def foo : Nat → Nat → Nat
| 0, _ => 0
| _, 0 => 1
@@ -494,7 +494,7 @@ 类型类中,我们将看到 Lean 可以被告知合适的基础类型是含元素的,并且可以自动推断出其他构造类型是含元素的。在此基础上,标准库提供了一个任意元素arbitrary
,任何含元素的类型。
+
一些函数式编程语言支持不完整的模式。在这些语言中,解释器对不完整的情况产生一个异常或返回一个任意的值。我们可以使用 Inhabited
(含元素的)类型类来模拟任意值的方法。粗略的说,Inhabited α
的一个元素是对 α
拥有一个元素的见证;在类型类中,我们将看到 Lean 可以被告知合适的基础类型是含元素的,并且可以自动推断出其他构造类型是含元素的。在此基础上,标准库提供了一个任意元素 arbitrary
,任何含元素的类型。
我们还可以使用类型Option α
来模拟不完整的模式。我们的想法是对所提供的模式返回some a
,而对不完整的情况使用none
。下面的例子演示了这两种方法。
-这里 (a : α)
是一个参数序列,(b : β)
是进行模式匹配的参数序列,γ
是任何类型,它可以取决于 a
和 b
。每一行应该包含相同数量的模式,对应于 β
的每个元素。正如我们所看到的,模式要么是一个变量,要么是应用于其他模式的构造器,要么是一个正规化为该形式的表达式(其中非构造器用 [matchPattern]
属性标记)。构造器的出现会提示情况拆分,构造器的参数由给定的变量表示。在依值模式匹配一节中,我们将看到有时有必要在模式中包含明确的项,这些项需要进行表达式类型检查,尽管它们在模式匹配中没有起到作用。由于这个原因,这些被称为「不可访问的模式」。但是在依值模式匹配一节之前,我们将不需要使用这种不可访问的模式。
+这里 (a : α)
是一个参数序列,(b : β)
是进行模式匹配的参数序列,γ
是任何类型,它可以取决于 a
和 b
。每一行应该包含相同数量的模式,对应于 β
的每个元素。正如我们所看到的,模式要么是一个变量,要么是应用于其他模式的构造子,要么是一个正规化为该形式的表达式(其中非构造子用 [matchPattern]
属性标记)。构造子的出现会提示情况拆分,构造子的参数由给定的变量表示。在依值模式匹配一节中,我们将看到有时有必要在模式中包含明确的项,这些项需要进行表达式类型检查,尽管它们在模式匹配中没有起到作用。由于这个原因,这些被称为「不可访问的模式」。但是在依值模式匹配一节之前,我们将不需要使用这种不可访问的模式。
正如我们在上一节所看到的,项 t₁,...,tₙ
可以利用任何一个参数 a
,以及在相应模式中引入的任何一个变量。使得递归和归纳成为可能的是,它们也可以涉及对 foo
的递归调用。在本节中,我们将处理结构性递归,其中 foo
的参数出现在 :=
的右侧,是左侧模式的子项。我们的想法是,它们在结构上更小,因此在归纳类型中出现在更早的阶段。下面是上一章的一些结构递归的例子,现在用方程编译器来定义。
open Nat
def add : Nat → Nat → Nat
@@ -657,7 +657,7 @@ open Nat
def add : Nat → Nat → Nat
| m, zero => m
@@ -741,7 +741,7 @@ variable (C : Nat → Type u)
@@ -822,7 +822,7 @@ 局域
-可以使用let rec
关键字定义局域递归声明。
+可以使用 let rec
关键字定义局域递归声明。
def replicate (n : Nat) (a : α) : List α :=
let rec loop : Nat → List α → List α
| 0, as => as
@@ -841,7 +841,7 @@ 局域
You can also use `let rec` in tactic mode and for creating proofs by induction.
-->
-Lean为每个 let rec
创建一个辅助声明。在上面的例子中,它对于出现在 replicate
的 let rec loop
创建了声明 replication.loop
。请注意,Lean 通过添加 let rec
声明中出现的任何局部变量作为附加参数来「关闭」声明。例如,局部变量 a
出现在 let rec
循环中。
+Lean 为每个 let rec
创建一个辅助声明。在上面的例子中,它对于出现在 replicate
的 let rec loop
创建了声明 replication.loop
。请注意,Lean 通过添加 let rec
声明中出现的任何局部变量作为附加参数来「关闭」声明。例如,局部变量 a
出现在 let rec
循环中。
你也可以在策略证明模式中使用 let rec
,并通过归纳来创建证明。
def replicate (n : Nat) (a : α) : List α :=
let rec loop : Nat → List α → List α
@@ -860,7 +860,7 @@ 局域
You can also introduce auxiliary recursive declarations using `where` clause after your definition.
Lean converts them into a `let rec`.
-->
-还可以在定义后使用 where
子句引入辅助递归声明。Lean将它们转换为 let rec
。
+还可以在定义后使用 where
子句引入辅助递归声明。Lean 将它们转换为 let rec
。
def replicate (n : Nat) (a : α) : List α :=
loop n []
where
@@ -956,7 +956,7 @@
Here is essentially the definition of division on the natural numbers that is found in the standard library.
-->
-这里有一大堆字,但我们熟悉第一块:类型 α
,关系 r
和假设 h
,即 r
是有良基的。变量' C
代表递归定义的动机:对于每个元素 x : α
,我们想构造一个 C x
的元素。函数 F
提供了这样做的归纳方法:它告诉我们如何构造一个元素 C x
,给定 C y
的元素对于 x
的每个 y
。
+这里有一大堆字,但我们熟悉第一块:类型 α
,关系 r
和假设 h
,即 r
是有良基的。变量' C
代表递归定义的动机:对于每个元素 x : α
,我们想构造一个 C x
的元素。函数 F
提供了这样做的归纳方法:它告诉我们如何构造一个元素 C x
,给定 C y
的元素对于 x
的每个 y
。
注意 WellFounded.fix
和归纳法原理一样有效。它说如果 ≺
是良基的,而你想要证明 ∀ x, C x
,那么只要证明对于任意的 x
,如果我们有 ∀ y ≺ x, C y
,那么我们就有 C x
就足够了。
在上面的例子中,我们使用了修饰符 noncomputable
,因为代码生成器目前不支持 WellFounded.fix
。函数 WellFounded.fix
是 Lean 用来证明函数终止的另一个工具。
Lean 知道自然数上通常的序 <
是良基的。它还知道许多从其他东西中构造新的良基的序的方法,例如字典序。
@@ -987,7 +987,7 @@
The elaborator is designed to make definitions like this more
convenient. It accepts the following:
-->
-这个定义有点难以理解。这里递归在 x
上, div.F x f : Nat → Nat
为固定的 x
返回「除以 y
」函数。你要记住 div.F
的第二个参数 f
是递归的具体实现,这个函数对所有小于 x
的自然数 x₁
返回「除以 y
」函数。
+这个定义有点难以理解。这里递归在 x
上, div.F x f : Nat → Nat
为固定的 x
返回「除以 y
」函数。你要记住 div.F
的第二个参数 f
是递归的具体实现,这个函数对所有小于 x
的自然数 x₁
返回「除以 y
」函数。
繁饰器(Elaborator)可以使这样的定义更加方便。它接受下列内容:
def div (x y : Nat) : Nat :=
if h : 0 < y ∧ y ≤ x then
@@ -1075,7 +1075,7 @@
Note that a lexicographic order is used in the example above because the instance
`WellFoundedRelation (α × β)` uses a lexicographic order. Lean also defines the instance
-->
-注意,在上面的例子中使用了字典序,因为实例 WellFoundedRelation (α × β)
使用了字典序。Lean还定义了实例
+注意,在上面的例子中使用了字典序,因为实例 WellFoundedRelation (α × β)
使用了字典序。Lean 还定义了实例
instance (priority := low) [SizeOf α] : WellFoundedRelation α :=
sizeOfWFRel
@@ -1254,7 +1254,7 @@ 相互递归
-
构造器even_zero
、even_succ
和 odd_succ
提供了显示数字是偶数还是奇数的积极方法。我们需要利用归纳类型是由这些构造器生成的这一事实来知道零不是奇数,并且后两个含义是相反的。像往常一样,构造器保存在以定义的类型命名的命名空间中,并且命令 open Even Odd
允许我们更方便地访问它们。
+构造子 even_zero
、even_succ
和 odd_succ
提供了显示数字是偶数还是奇数的积极方法。我们需要利用归纳类型是由这些构造子生成的这一事实来知道零不是奇数,并且后两个含义是相反的。像往常一样,构造子保存在以定义的类型命名的命名空间中,并且命令 open Even Odd
允许我们更方便地访问它们。
mutual
inductive Even : Nat → Prop where
| even_zero : Even 0
@@ -1426,7 +1426,7 @@ 依值
equations, and the equation compiler generates all the boilerplate
code automatically for us. Here are a number of similar examples:
-->
-在 nil
的情况下,m
被实例化为 0
,noConfusion
利用了 0 = succ n
不能出现的事实。否则,v
的形式为 a :: w
,我们可以简单地将 w
从长度 m
的向量转换为长度 n
的向量后返回 w
。
+在 nil
的情况下,m
被实例化为 0
,noConfusion
利用了 0 = succ n
不能出现的事实。否则,v
的形式为 a :: w
,我们可以简单地将 w
从长度 m
的向量转换为长度 n
的向量后返回 w
。
定义 tail
的困难在于维持索引之间的关系。 tailAux
中的假设 e : m = n + 1
用于传达 n
与与小前提相关的索引之间的关系。此外,zero = n + 1
的情况是不可达的,而放弃这种情况的规范方法是使用 noConfusion
。
然而,tail
函数很容易使用递归方程来定义,并且方程编译器会自动为我们生成所有样板代码。下面是一些类似的例子:
inductive Vector (α : Type u) : Nat → Type u
@@ -1505,8 +1505,8 @@ 不可
define the function ``inverse`` below, we *have to* mark ``f a``
inaccessible.
-->
-有时候,依值匹配模式中的参数对定义来说并不是必需的,但是必须包含它来适当地确定表达式的类型。Lean 允许用户将这些子项标记为「不可访问」以进行模式匹配。例如,当左侧出现的项既不是变量也不是构造器应用时,这些注解是必不可少的,因为它们不适合用于模式匹配的目标。我们可以将这种不可访问的模式视为模式的「不关心」组件。你可以通过写 .(t)
来声明子项不可访问。如果不可访问的模式可以被推断出来,你也可以写 _
。
-下面的例子中,我们声明了一个归纳类型,它定义了「在 f
的像中」的属性。您可以将 ImageOf f b
类型的元素视为 b
位于 f
的像中的证据,构造器imf
用于构建此类证据。然后,我们可以定义任何函数 f
的「逆」,逆函数将 f
的像中的任何元素赋给映射到它的元素。类型规则迫使我们为第一个参数写 f a
,但是这个项既不是变量也不是构造器应用,并且在模式匹配定义中没有作用。为了定义下面的函数 inverse
,我们必须将 f a
标记为不可访问。
+有时候,依值匹配模式中的参数对定义来说并不是必需的,但是必须包含它来适当地确定表达式的类型。Lean 允许用户将这些子项标记为「不可访问」以进行模式匹配。例如,当左侧出现的项既不是变量也不是构造子应用时,这些注解是必不可少的,因为它们不适合用于模式匹配的目标。我们可以将这种不可访问的模式视为模式的「不关心」组件。你可以通过写 .(t)
来声明子项不可访问。如果不可访问的模式可以被推断出来,你也可以写 _
。
+下面的例子中,我们声明了一个归纳类型,它定义了「在 f
的像中」的属性。您可以将 ImageOf f b
类型的元素视为 b
位于 f
的像中的证据,构造子 imf
用于构建此类证据。然后,我们可以定义任何函数 f
的「逆」,逆函数将 f
的像中的任何元素赋给映射到它的元素。类型规则迫使我们为第一个参数写 f a
,但是这个项既不是变量也不是构造子应用,并且在模式匹配定义中没有作用。为了定义下面的函数 inverse
,我们必须将 f a
标记为不可访问。
inductive ImageOf {α β : Type u} (f : α → β) : β → Type u where
| imf : (a : α) → ImageOf f (f a)
@@ -1596,7 +1596,7 @@ 不可
implements a new feature, *discriminant refinement*, which includes
these extra discriminants automatically for us.
-->
-如前所述,参数 {n : Nat}
是模式匹配的一部分,因为它不能在整个定义中保持固定。在以前的 Lean 版本中,用户经常发现必须包含这些额外的判别符是很麻烦的。因此,Lean 4 实现了一个新特性,判别精炼(discriminant refinement),它自动为我们包含了这些额外的判别。
+如前所述,参数 {n : Nat}
是模式匹配的一部分,因为它不能在整个定义中保持固定。在以前的 Lean 版本中,用户经常发现必须包含这些额外的判别符是很麻烦的。因此,Lean 4 实现了一个新特性,判别精炼(discriminant refinement),它自动为我们包含了这些额外的判别。
inductive Vector (α : Type u) : Nat → Type u
| nil : Vector α 0
| cons : α → {n : Nat} → Vector α n → Vector α (n+1)
@@ -1864,7 +1864,7 @@ 练习
Write a function that evaluates such an expression, evaluating each ``var n`` to ``v n``.
-->
此处 sampleExpr
表示 (v₀ * 7) + (2 * v₁)
。
-写一个函数来计算这些表达式,对每个var n
赋值v n
.
+写一个函数来计算这些表达式,对每个 var n
赋值 v n
.
-我们已经看到Lean的形式基础包括基本类型,Prop, Type 0, Type 1, Type 2, ...
,并允许形成依值函数类型,(x : α) → β
。在例子中,我们还使用了额外的类型,如Bool
、Nat
和Int
,以及类型构造器,如List
和乘积×
。事实上,在Lean的库中,除了宇宙之外的每一个具体类型和除了依值箭头之外的每一个类型构造器都是一个被称为归纳类型的类型构造的一般类别的实例。值得注意的是,仅用类型宇宙、依值箭头类型和归纳类型就可以构建一个内涵丰富的数学大厦;其他一切都源于这些。
-直观地说,一个归纳类型是由一个指定的构造器列表建立起来的。在Lean中,指定这种类型的语法如下:
+我们已经看到Lean 的形式基础包括基本类型,Prop, Type 0, Type 1, Type 2, ...
,并允许形成依值函数类型,(x : α) → β
。在例子中,我们还使用了额外的类型,如 Bool
、Nat
和 Int
,以及类型构造子,如 List
和乘积 ×
。事实上,在Lean 的库中,除了宇宙之外的每一个具体类型和除了依值箭头之外的每一个类型构造子都是一个被称为归纳类型的类型构造的一般类别的实例。值得注意的是,仅用类型宇宙、依值箭头类型和归纳类型就可以构建一个内涵丰富的数学大厦;其他一切都源于这些。
+直观地说,一个归纳类型是由一个指定的构造子列表建立起来的。在Lean 中,指定这种类型的语法如下:
inductive Foo where
| constructor₁ : ... → Foo
| constructor₂ : ... → Foo
@@ -210,11 +210,11 @@ 归纳类型
-
我们的直觉是,每个构造器都指定了一种建立新的对象Foo
的方法,可能是由以前构造的值构成。Foo
类型只不过是由以这种方式构建的对象组成。归纳式声明中的第一个字符也可以用逗号而不是|
来分隔构造器。
-我们将在下面看到,构造器的参数可以包括Foo
类型的对象,但要遵守一定的「正向性」约束,即保证Foo
的元素是自下而上构建的。粗略地说,每个...
可以是由Foo
和以前定义的类型构建的任何箭头类型,其中Foo
如果出现,也只是作为依值箭头类型的「目标」。
+我们的直觉是,每个构造子都指定了一种建立新的对象 Foo
的方法,可能是由以前构造的值构成。Foo
类型只不过是由以这种方式构建的对象组成。归纳式声明中的第一个字符也可以用逗号而不是 |
来分隔构造子。
+我们将在下面看到,构造子的参数可以包括 Foo
类型的对象,但要遵守一定的「正向性」约束,即保证 Foo
的元素是自下而上构建的。粗略地说,每个...
可以是由 Foo
和以前定义的类型构建的任何箭头类型,其中 Foo
如果出现,也只是作为依值箭头类型的「目标」。
我们将提供一些归纳类型的例子。我们还把上述方案稍微扩展,即相互定义的归纳类型,以及所谓的归纳族。
-就像逻辑连接词一样,每个归纳类型都有引入规则,说明如何构造该类型的一个元素;还有消去规则,说明如何在另一个构造中「使用」该类型的一个元素。其实逻辑连接词也是归纳类型结构的例子。你已经看到了归纳类型的引入规则:它们只是在类型的定义中指定的构造器。消去规则提供了类型上的递归原则,其中也包括作为一种特殊情况的归纳原则。
-在下一章中,我们将介绍Lean的函数定义包,它提供了更方便的方法来定义归纳类型上的函数并进行归纳证明。但是由于归纳类型的概念是如此的基本,我们觉得从低级的、实践的理解开始是很重要的。我们将从归纳类型的一些基本例子开始,然后逐步上升到更详细和复杂的例子。
+就像逻辑连接词一样,每个归纳类型都有引入规则,说明如何构造该类型的一个元素;还有消去规则,说明如何在另一个构造中「使用」该类型的一个元素。其实逻辑连接词也是归纳类型结构的例子。你已经看到了归纳类型的引入规则:它们只是在类型的定义中指定的构造子。消去规则提供了类型上的递归原则,其中也包括作为一种特殊情况的归纳原则。
+在下一章中,我们将介绍Lean 的函数定义包,它提供了更方便的方法来定义归纳类型上的函数并进行归纳证明。但是由于归纳类型的概念是如此的基本,我们觉得从低级的、实践的理解开始是很重要的。我们将从归纳类型的一些基本例子开始,然后逐步上升到更详细和复杂的例子。
-inductive
命令创建了一个新类型Weekday
。构造器都在Weekday
命名空间中。
+inductive
命令创建了一个新类型 Weekday
。构造子都在 Weekday
命名空间中。
inductive Weekday where
| sunday : Weekday
| monday : Weekday
@@ -281,8 +281,8 @@ 枚举式类
We will use the `match` expression to define a function from ``Weekday``
to the natural numbers:
-->
-把sunday
、monday
、... 、saturday
看作是Weekday
的不同元素,没有其他有区别的属性。消去规则Weekday.rec
,与Weekday
类型及其构造器一起定义。它也被称为递归器(Recursor),它是使该类型「归纳」的原因:它允许我们通过给每个构造器分配相应的值来定义Weekday
的函数。直观的说,归纳类型是由构造器详尽地生成的,除了它们构造的元素外,没有其他元素。
-我们将使用match
表达式来定义一个从Weekday
到自然数的函数:
+把 sunday
、monday
、... 、saturday
看作是 Weekday
的不同元素,没有其他有区别的属性。消去规则 Weekday.rec
,与 Weekday
类型及其构造子一起定义。它也被称为递归器(Recursor),它是使该类型「归纳」的原因:它允许我们通过给每个构造子分配相应的值来定义Weekday
的函数。直观的说,归纳类型是由构造子详尽地生成的,除了它们构造的元素外,没有其他元素。
+我们将使用match
表达式来定义一个从 Weekday
到自然数的函数:
inductive Weekday where
| sunday : Weekday
| monday : Weekday
@@ -359,9 +359,9 @@ 枚举式类
This function is used by the `#eval` command to display `Weekday` objects.
-->
-译者注:此处详细解释一下递归器rec
。递归器作为归纳类型的消去规则,用于构造归纳类型到其他类型的函数。从最朴素的集合论直觉上讲,枚举类型的函数只需要规定每个元素的对应,也就是match
的方式,但是要注意,match
并不像其他Lean关键字那样是一种简单的语法声明,它实际上是一种功能,而这并不是类型论自带的功能。因此match
需要一个类型论实现,也就是递归器。现在我们通过#check @Weekday.rec
命令的输出来看递归器是如何工作的。首先回忆@
是显式参数的意思。递归器是一个复杂的函数,输入的信息有1)motive:一个「目的」函数,表明想要拿当前类型构造什么类型。这个输出类型足够一般所以在u上;2)motive函数对所有枚举元素的输出值(这里就显得它非常「递归」)。这两点是准备工作,下面是这个函数的实际工作:输入一个具体的属于这个枚举类型的项t
,输出结果motive t
。下文在非枚举类型中,会直接用到这些递归器,届时可以更清晰地看到它们如何被使用。
+译者注:此处详细解释一下递归器rec
。递归器作为归纳类型的消去规则,用于构造归纳类型到其他类型的函数。从最朴素的集合论直觉上讲,枚举类型的函数只需要规定每个元素的对应,也就是match
的方式,但是要注意,match
并不像其他Lean 关键字那样是一种简单的语法声明,它实际上是一种功能,而这并不是类型论自带的功能。因此match
需要一个类型论实现,也就是递归器。现在我们通过#check @Weekday.rec
命令的输出来看递归器是如何工作的。首先回忆@
是显式参数的意思。递归器是一个复杂的函数,输入的信息有1)motive:一个「目的」函数,表明想要拿当前类型构造什么类型。这个输出类型足够一般所以在u上;2)motive函数对所有枚举元素的输出值(这里就显得它非常「递归」)。这两点是准备工作,下面是这个函数的实际工作:输入一个具体的属于这个枚举类型的项t
,输出结果motive t
。下文在非枚举类型中,会直接用到这些递归器,届时可以更清晰地看到它们如何被使用。
-当声明一个归纳数据类型时,你可以使用deriving Repr
来指示Lean生成一个函数,将Weekday
对象转换为文本。这个函数被#eval
命令用来显示Weekday
对象。
+当声明一个归纳数据类型时,你可以使用deriving Repr
来指示Lean 生成一个函数,将Weekday
对象转换为文本。这个函数被#eval
命令用来显示Weekday
对象。
inductive Weekday where
| sunday
| monday
@@ -384,8 +384,8 @@ 枚举式类
We can define functions from ``Weekday`` to ``Weekday``:
-->
-将与某一结构相关的定义和定理归入同名的命名空间通常很有用。例如,我们可以将numberOfDay
函数放在Weekday
命名空间中。然后当我们打开命名空间时,我们就可以使用较短的名称。
-我们可以定义从Weekday
到Weekday
的函数:
+将与某一结构相关的定义和定理归入同名的命名空间通常很有用。例如,我们可以将 numberOfDay
函数放在 Weekday
命名空间中。然后当我们打开命名空间时,我们就可以使用较短的名称。
+我们可以定义从 Weekday
到 Weekday
的函数:
inductive Weekday where
| sunday : Weekday
| monday : Weekday
@@ -429,7 +429,7 @@ 枚举式类
for any Weekday ``d``? You can use `match` to provide a proof of the claim for each
constructor:
-->
-我们如何证明next (previous d) = d
对于任何Weekdayd
的一般定理?你可以使用match
来为每个构造器提供一个证明:
+我们如何证明 next (previous d) = d
对于任何Weekdayd
的一般定理?你可以使用match
来为每个构造子提供一个证明:
inductive Weekday where
| sunday : Weekday
| monday : Weekday
@@ -517,8 +517,8 @@ 枚举式类
enumerated type.
-->
下面的归纳类型的策略一节将介绍额外的策略,这些策略是专门为利用归纳类型而设计。
-命题即类型的对应原则下,我们可以使用match
来证明定理和定义函数。换句话说,逐情况证明是一种逐情况定义的另一表现形式,其中被「定义」的是一个证明而不是一段数据。
-Lean库中的Bool
类型是一个枚举类型的实例。
+命题即类型的对应原则下,我们可以使用 match
来证明定理和定义函数。换句话说,逐情况证明是一种逐情况定义的另一表现形式,其中被「定义」的是一个证明而不是一段数据。
+Lean 库中的Bool
类型是一个枚举类型的实例。
namespace Hidden
inductive Bool where
| false : Bool
@@ -538,8 +538,8 @@ 枚举式类
``Bool`` type, and verifying common identities. Note that you can define a
binary operation like ``and`` using `match`:
-->
-(为了运行这个例子,我们把它们放在一个叫做Hidden
的命名空间中,这样像Bool
这样的名字就不会和标准库中的 Bool
冲突。这是必要的,因为这些类型是Lean「启动工作」的一部分,在系统启动时被自动导入)。
-作为一个练习,你应该思考这些类型的引入和消去规则的作用。作为进一步的练习,我们建议在Bool
类型上定义布尔运算 and
、or
、not
,并验证其共性。提示,你可以使用match
来定义像and
这样的二元运算:
+(为了运行这个例子,我们把它们放在一个叫做 Hidden
的命名空间中,这样像 Bool
这样的名字就不会和标准库中的 Bool
冲突。这是必要的,因为这些类型是Lean「启动工作」的一部分,在系统启动时被自动导入)。
+作为一个练习,你应该思考这些类型的引入和消去规则的作用。作为进一步的练习,我们建议在 Bool
类型上定义布尔运算 and
、or
、not
,并验证其共性。提示,你可以使用match
来定义像and
这样的二元运算:
namespace Hidden
def and (a b : Bool) : Bool :=
match a with
@@ -550,12 +550,12 @@ 枚举式类
-同样地,大多数等式可以通过引入合适的match
,然后使用rfl
来证明。
+同样地,大多数等式可以通过引入合适的match
,然后使用 rfl
来证明。
-带参数的构造器
+带参数的构造子
-枚举类型是归纳类型的一种非常特殊的情况,其中构造器根本不需要参数。一般来说,「构造」可以依赖于数据,然后在构造参数中表示。考虑一下库中的乘积类型和求和类型的定义:
+枚举类型是归纳类型的一种非常特殊的情况,其中构造子根本不需要参数。一般来说,「构造」可以依赖于数据,然后在构造参数中表示。考虑一下库中的乘积类型和求和类型的定义:
namespace Hidden
inductive Prod (α : Type u) (β : Type v)
| mk : α → β → Prod α β
@@ -583,7 +583,7 @@
library defines notation ``α × β`` for ``Prod α β`` and ``(a, b)`` for
``Prod.mk a b``.
-->
-思考一下这些例子中发生了什么。乘积类型有一个构造器Prod.mk
,它需要两个参数。要在Prod α β
上定义一个函数,我们可以假设输入的形式是Prod.mk a b
,而我们必须指定输出,用a
和b
来表示。我们可以用它来定义Prod
的两个投影。标准库定义的符号α × β
表示Prod α β
,(a, b)
表示Prod.mk a b
。
+思考一下这些例子中发生了什么。乘积类型有一个构造子 Prod.mk
,它需要两个参数。要在 Prod α β
上定义一个函数,我们可以假设输入的形式是 Prod.mk a b
,而我们必须指定输出,用 a
和 b
来表示。我们可以用它来定义 Prod
的两个投影。标准库定义的符号 α × β
表示 Prod α β
,(a, b)
表示 Prod.mk a b
。
namespace Hidden
inductive Prod (α : Type u) (β : Type v)
| mk : α → β → Prod α β
@@ -605,7 +605,7 @@
Here is another example where we use the recursor `Prod.casesOn` instead
of `match`.
-->
-函数fst
接收一个对p
。match
将p
解释为一个对Prod.mk a b
。还记得在依值类型论中,为了给这些定义以最大的通用性,我们允许类型α
和β
属于任何宇宙。
+函数 fst
接收一个对 p
。match
将p
解释为一个对 Prod.mk a b
。还记得在依值类型论中,为了给这些定义以最大的通用性,我们允许类型 α
和 β
属于任何宇宙。
下面是另一个例子,我们用递归器Prod.casesOn
代替match
。
def prod_example (p : Bool × Nat) : Nat :=
Prod.casesOn (motive := fun _ => Nat) p (fun b n => cond b (2 * n) (2 * n + 1))
@@ -631,7 +631,7 @@
output value in terms of ``b``.
-->
参数motive
是用来指定你要构造的对象的类型,它是一个依值的函数,_
是被自动推断出的类型,此处即Bool × Nat
。函数cond
是一个布尔条件:cond b t1 t2
,如果b
为真,返回t1
,否则返回t2
。函数prod_example
接收一个由布尔值b
和一个数字n
组成的对,并根据b
为真或假返回2 * n
或2 * n + 1
。
-相比之下,求和类型有两个构造器inl
和inr
(表示「从左引入」和「从右引入」),每个都需要一个(显式的)参数。要在Sum α β
上定义一个函数,我们必须处理两种情况:要么输入的形式是inl a
,由此必须依据a
指定一个输出值;要么输入的形式是inr b
,由此必须依据b
指定一个输出值。
+相比之下,求和类型有两个构造子inl
和inr
(表示「从左引入」和「从右引入」),每个都需要一个(显式的)参数。要在 Sum α β
上定义一个函数,我们必须处理两种情况:要么输入的形式是 inl a
,由此必须依据 a
指定一个输出值;要么输入的形式是 inr b
,由此必须依据 b
指定一个输出值。
def sum_example (s : Sum Nat Nat) : Nat :=
Sum.casesOn (motive := fun _ => Nat) s
(fun n => 2 * n)
@@ -668,11 +668,11 @@
As with function definitions, Lean's inductive definition syntax will
let you put named arguments to the constructors before the colon:
-->
-这个例子与前面的例子类似,但现在输入到sum_example
的内容隐含了inl n
或inr n
的形式。在第一种情况下,函数返回2 * n
,第二种情况下,它返回2 * n + 1
。
-注意,乘积类型取决于参数α β : Type
,这些参数是构造器和Prod
的参数。Lean会检测这些参数何时可以从构造器的参数或返回类型中推断出来,并在这种情况下使其隐式。
-在定义自然数一节中,我们将看到当归纳类型的构造器从归纳类型本身获取参数时会发生什么。本节考虑的例子暂时不是这样:每个构造器只依赖于先前指定的类型。
-一个有多个构造器的类型是析取的:Sum α β
的一个元素要么是inl a
的形式,要么是inl b
的形式。一个有多个参数的构造器引入了合取信息:从Prod.mk a b
的元素Prod α β
中我们可以提取a
和b
。一个任意的归纳类型可以包括这两个特征:拥有任意数量的构造器,每个构造器都需要任意数量的参数。
-和函数定义一样,Lean的归纳定义语法可以让你把构造器的命名参数放在冒号之前:
+这个例子与前面的例子类似,但现在输入到sum_example
的内容隐含了inl n
或inr n
的形式。在第一种情况下,函数返回 2 * n
,第二种情况下,它返回 2 * n + 1
。
+注意,乘积类型取决于参数α β : Type
,这些参数是构造子和Prod
的参数。Lean 会检测这些参数何时可以从构造子的参数或返回类型中推断出来,并在这种情况下使其隐式。
+在定义自然数一节中,我们将看到当归纳类型的构造子从归纳类型本身获取参数时会发生什么。本节考虑的例子暂时不是这样:每个构造子只依赖于先前指定的类型。
+一个有多个构造子的类型是析取的:Sum α β
的一个元素要么是 inl a
的形式,要么是 inl b
的形式。一个有多个参数的构造子引入了合取信息:从 Prod.mk a b
的元素 Prod α β
中我们可以提取 a
和b
。一个任意的归纳类型可以包括这两个特征:拥有任意数量的构造子,每个构造子都需要任意数量的参数。
+和函数定义一样,Lean 的归纳定义语法可以让你把构造子的命名参数放在冒号之前:
namespace Hidden
inductive Prod (α : Type u) (β : Type v) where
| mk (fst : α) (snd : β) : Prod α β
@@ -694,7 +694,7 @@
well as its projections, at the same time.
-->
这些定义的结果与本节前面给出的定义基本相同。
-像Prod
这样只有一个构造器的类型是纯粹的合取型:构造器只是将参数列表打包成一块数据,基本上是一个元组,后续参数的类型可以取决于初始参数的类型。我们也可以把这样的类型看作是一个「记录」或「结构体」。在Lean中,关键词structure
可以用来同时定义这样一个归纳类型以及它的投影。
+像 Prod
这样只有一个构造子的类型是纯粹的合取型:构造子只是将参数列表打包成一块数据,基本上是一个元组,后续参数的类型可以取决于初始参数的类型。我们也可以把这样的类型看作是一个「记录」或「结构体」。在Lean 中,关键词 structure
可以用来同时定义这样一个归纳类型以及它的投影。
namespace Hidden
structure Prod (α : Type u) (β : Type v) where
mk :: (fst : α) (snd : β)
@@ -710,8 +710,8 @@
example, the following defines a record to store a color as a triple
of RGB values:
-->
-这个例子同时引入了归纳类型Prod
,它的构造器mk
,通常的消去器(rec
和recOn
),以及投影fst
和snd
。
-如果你没有命名构造器,Lean使用mk
作为默认值。例如,下面定义了一个记录,将一个颜色存储为RGB值的三元组:
+这个例子同时引入了归纳类型 Prod
,它的构造子 mk
,通常的消去器(rec
和 recOn
),以及投影 fst
和 snd
。
+如果你没有命名构造子,Lean 使用mk
作为默认值。例如,下面定义了一个记录,将一个颜色存储为RGB值的三元组:
structure Color where
(red : Nat) (green : Nat) (blue : Nat)
deriving Repr
@@ -726,7 +726,7 @@
You can avoid the parentheses if you add a line break between each field.
-->
-yellow
的定义形成了有三个值的记录,而投影Color.red
则返回红色成分。
+yellow
的定义形成了有三个值的记录,而投影 Color.red
则返回红色成分。
如果你在每个字段之间加一个换行符,就可以不用括号。
structure Color where
red : Nat
@@ -740,7 +740,7 @@
working with them. Here, for example, is the definition of a
semigroup:
-->
-structure
命令对于定义代数结构特别有用,Lean提供了大量的基础设施来支持对它们的处理。例如,这里是一个半群的定义:
+structure
命令对于定义代数结构特别有用,Lean 提供了大量的基础设施来支持对它们的处理。例如,这里是一个半群的定义:
structure Semigroup where
carrier : Type u
mul : carrier → carrier → carrier
@@ -795,9 +795,9 @@
types is inhabited, and that the type of functions to an inhabited
type is inhabited.
-->
-在依值类型论的语义中,没有内置的部分函数的概念。一个函数类型α → β
或一个依值函数类型(a : α) → β
的每个元素都被假定为在每个输入端有一个值。Option
类型提供了一种表示部分函数的方法。Option β
的一个元素要么是none
,要么是some b
的形式,用于某个值b : β
。因此我们可以认为α → Option β
类型的元素f
是一个从α
到β
的部分函数:对于每一个a : α
,f a
要么返回none
,表示f a
是「未定义」,要么返回some b
。
-Inhabited α
的一个元素只是证明了α
有一个元素的事实。稍后,我们将看到Inhabited
是Lean中类型类的一个例子:Lean可以被告知合适的基础类型是含有元素的,并且可以在此基础上自动推断出其他构造类型是含有元素的。
-作为练习,我们鼓励你建立一个从α
到β
和β
到γ
的部分函数的组合概念,并证明其行为符合预期。我们也鼓励你证明Bool
和Nat
是含有元素的,两个含有元素的类型的乘积是含有元素的,以及到一个含有元素的类型的函数类型是含有元素的。
+在依值类型论的语义中,没有内置的部分函数的概念。一个函数类型 α → β
或一个依值函数类型 (a : α) → β
的每个元素都被假定为在每个输入端有一个值。Option
类型提供了一种表示部分函数的方法。Option β
的一个元素要么是none
,要么是some b
的形式,用于某个值b : β
。因此我们可以认为α → Option β
类型的元素f
是一个从α
到β
的部分函数:对于每一个a : α
,f a
要么返回none
,表示f a
是「未定义」,要么返回some b
。
+Inhabited α
的一个元素只是证明了α
有一个元素的事实。稍后,我们将看到 Inhabited
是Lean 中类型类的一个例子:Lean 可以被告知合适的基础类型是含有元素的,并且可以在此基础上自动推断出其他构造类型是含有元素的。
+作为练习,我们鼓励你建立一个从 α
到 β
和 β
到 γ
的部分函数的组合概念,并证明其行为符合预期。我们也鼓励你证明 Bool
和 Nat
是含有元素的,两个含有元素的类型的乘积是含有元素的,以及到一个含有元素的类型的函数类型是含有元素的。
-你应该想一想这些是如何产生你已经看到的引入和消去规则的。有一些规则规定了归纳类型的消去器可以去消去什么,或者说,哪些类型可以成为递归器的目标。粗略地说,Prop
中的归纳类型的特点是,只能消去成Prop
中的其他类型。这与以下理解是一致的:如果p : Prop
,一个元素hp : p
不携带任何数据。然而,这个规则有一个小的例外,我们将在归纳族一节中讨论。
+你应该想一想这些是如何产生你已经看到的引入和消去规则的。有一些规则规定了归纳类型的消去器可以去消去什么,或者说,哪些类型可以成为递归器的目标。粗略地说,Prop
中的归纳类型的特点是,只能消去成 Prop
中的其他类型。这与以下理解是一致的:如果 p : Prop
,一个元素 hp : p
不携带任何数据。然而,这个规则有一个小的例外,我们将在归纳族一节中讨论。
甚至存在量词也是归纳式定义的:
namespace Hidden
inductive Exists {α : Sort u} (p : α → Prop) : Prop where
@@ -857,8 +857,8 @@
``{x : α // p}``, which is sort of a hybrid between
``∃ x : α, P`` and ``Σ x : α, P``.
-->
-请记住,符号∃ x : α, p
是Exists (fun x : α => p)
的语法糖。
-False
, True
, And
和Or
的定义与Empty
, Unit
, Prod
和Sum
的定义完全类似。不同的是,第一组产生的是Prop
的元素,第二组产生的是Type u
的元素,适用于某些u
。类似地,∃ x : α, p
是Σ x : α, p
的Prop
值的变体。
+请记住,符号 ∃ x : α, p
是 Exists (fun x : α => p)
的语法糖。
+False
, True
, And
和Or
的定义与Empty
, Unit
, Prod
和Sum
的定义完全类似。不同的是,第一组产生的是Prop
的元素,第二组产生的是Type u
的元素,适用于某些u
。类似地,∃ x : α, p
是 Σ x : α, p
的 Prop
值的变体。
这里可以提到另一个归纳类型,表示为{x : α // p}
,它有点像∃ x : α, P
和Σ x : α, P
之间的混合。
namespace Hidden
inductive Subtype {α : Type u} (p : α → Prop) where
@@ -868,7 +868,7 @@
-事实上,在Lean中,Subtype
是用结构体命令定义的。
+事实上,在Lean 中,Subtype
是用结构体命令定义的。
namespace Hidden
structure Subtype {α : Sort u} (p : α → Prop) where
val : α
@@ -880,7 +880,7 @@
It is modeled after subset notation in set theory: the idea is that ``{x : α // p x}``
denotes the collection of elements of ``α`` that have property ``p``.
-->
-符号{x : α // p x}
是Subtype (fun x : α => p x)
的语法糖。它仿照集合理论中的子集表示法:{x : α // p x}
表示具有属性p
的α
元素的集合。
+符号{x : α // p x}
是 Subtype (fun x : α => p x)
的语法糖。它仿照集合理论中的子集表示法:{x : α // p x}
表示具有属性p
的α
元素的集合。
-到目前为止,我们所看到的归纳定义的类型都是「无趣的」:构造器打包数据并将其插入到一个类型中,而相应的递归器则解压数据并对其进行操作。当构造器作用于被定义的类型中的元素时,事情就变得更加有趣了。一个典型的例子是自然数Nat
类型:
+到目前为止,我们所看到的归纳定义的类型都是「无趣的」:构造子打包数据并将其插入到一个类型中,而相应的递归器则解压数据并对其进行操作。当构造子作用于被定义的类型中的元素时,事情就变得更加有趣了。一个典型的例子是自然数 Nat
类型:
namespace Hidden
inductive Nat where
| zero : Nat
@@ -922,8 +922,8 @@ 定义自然
next argument to the recursor specifies a value for ``f (succ n)`` in
terms of ``n`` and ``f n``. If we check the type of the recursor,
-->
-有两个构造器,我们从zero : Nat
开始;它不需要参数,所以我们一开始就有了它。相反,构造器succ
只能应用于先前构造的Nat
。将其应用于zero
,得到succ zero : Nat
。再次应用它可以得到succ (succ zero) : Nat
,依此类推。直观地说,Nat
是具有这些构造器的「最小」类型,这意味着它是通过从zero
开始并重复应用succ
这样无穷无尽地(并且自由地)生成的。
-和以前一样,Nat
的递归器被设计用来定义一个从Nat
到任何域的依值函数f
,也就是一个(n : nat) → motive n
的元素f
,其中motive : Nat → Sort u
。它必须处理两种情况:一种是输入为zero
的情况,另一种是输入为 succ n
的情况,其中n : Nat
。在第一种情况下,我们只需指定一个适当类型的目标值,就像以前一样。但是在第二种情况下,递归器可以假设在n
处的f
的值已经被计算过了。因此,递归器的下一个参数是以n
和f n
来指定f (succ n)
的值。
+有两个构造子,我们从 zero : Nat
开始;它不需要参数,所以我们一开始就有了它。相反,构造子succ
只能应用于先前构造的Nat
。将其应用于 zero
,得到 succ zero : Nat
。再次应用它可以得到succ (succ zero) : Nat
,依此类推。直观地说,Nat
是具有这些构造子的「最小」类型,这意味着它是通过从zero
开始并重复应用succ
这样无穷无尽地(并且自由地)生成的。
+和以前一样,Nat
的递归器被设计用来定义一个从 Nat
到任何域的依值函数f
,也就是一个(n : nat) → motive n
的元素f
,其中motive : Nat → Sort u
。它必须处理两种情况:一种是输入为 zero
的情况,另一种是输入为 succ n
的情况,其中 n : Nat
。在第一种情况下,我们只需指定一个适当类型的目标值,就像以前一样。但是在第二种情况下,递归器可以假设在n
处的f
的值已经被计算过了。因此,递归器的下一个参数是以n
和f n
来指定f (succ n)
的值。
如果我们检查递归器的类型:
namespace Hidden
inductive Nat where
@@ -951,7 +951,7 @@ 定义自然
The `Nat.recOn` is similar to `Nat.rec` but the major premise occurs before the minor premises.
-->
-隐参数motive
,是被定义的函数的陪域。在类型论中,通常说motive
是消去/递归的目的,因为它描述了我们希望构建的对象类型。接下来的两个参数指定了如何计算零和后继的情况,如上所述。它们也被称为小前提minor premises
。最后,t : Nat
,是函数的输入。它也被称为大前提major premise
。
+隐参数 motive
,是被定义的函数的陪域。在类型论中,通常说 motive
是消去/递归的目的,因为它描述了我们希望构建的对象类型。接下来的两个参数指定了如何计算零和后继的情况,如上所述。它们也被称为小前提 minor premises
。最后,t : Nat
,是函数的输入。它也被称为大前提 major premise
。
Nat.recOn
与Nat.rec
类似,但大前提发生在小前提之前。
@Nat.recOn :
{motive : Nat → Sort u}
@@ -967,7 +967,7 @@ 定义自然
successor step, assuming the value ``add m n`` is already determined,
we define ``add m (succ n)`` to be ``succ (add m n)``.
-->
-例如,考虑自然数上的加法函数add m n
。固定m
,我们可以通过递归来定义n
的加法。在基本情况下,我们将add m zero
设为m
。在后续步骤中,假设add m n
的值已经确定,我们将add m (succ n)
定义为succ (add m n)
。
+例如,考虑自然数上的加法函数 add m n
。固定m
,我们可以通过递归来定义n
的加法。在基本情况下,我们将add m zero
设为m
。在后续步骤中,假设add m n
的值已经确定,我们将add m (succ n)
定义为succ (add m n)
。
namespace Hidden
inductive Nat where
| zero : Nat
@@ -989,7 +989,7 @@ 定义自然
then go on to define familiar notation in that namespace. The two
defining equations for addition now hold definitionally:
-->
-将这些定义放入一个命名空间Nat
是很有用的。然后我们可以继续在这个命名空间中定义熟悉的符号。现在加法的两个定义方程是成立的:
+将这些定义放入一个命名空间 Nat
是很有用的。然后我们可以继续在这个命名空间中定义熟悉的符号。现在加法的两个定义方程是成立的:
namespace Hidden
inductive Nat where
| zero : Nat
@@ -1022,8 +1022,8 @@ 定义自然
pattern of an inductive proof: to prove ``∀ n, motive n``, first prove ``motive 0``,
and then, for arbitrary ``n``, assume ``ih : motive n`` and prove ``motive (succ n)``.
-->
-我们将在类型类一章中解释instance
命令如何工作。我们以后的例子将使用Lean自己的自然数版本。
-然而,证明像zero + m = m
这样的事实,需要用归纳法证明。如上所述,归纳原则只是递归原则的一个特例,其中陪域motive n
是Prop
的一个元素。它代表了熟悉的归纳证明模式:要证明∀ n, motive n
,首先要证明motive 0
,然后对于任意的n
,假设ih : motive n
并证明motive (succ n)
。
+我们将在类型类一章中解释 instance
命令如何工作。我们以后的例子将使用Lean 自己的自然数版本。
+然而,证明像 zero + m = m
这样的事实,需要用归纳法证明。如上所述,归纳原则只是递归原则的一个特例,其中陪域 motive n
是 Prop
的一个元素。它代表了熟悉的归纳证明模式:要证明 ∀ n, motive n
,首先要证明 motive 0
,然后对于任意的 n
,假设 ih : motive n
并证明 motive (succ n)
。
namespace Hidden
open Nat
@@ -1044,7 +1044,7 @@ 定义自然
``rewrite`` and ``simp`` tactics tend to be very effective in proofs
like these. In this case, each can be used to reduce the proof to:
-->
-请注意,当Nat.recOn
在证明中使用时,它实际上是变相的归纳原则。rewrite
和simp
策略在这样的证明中往往非常有效。在这种情况下,证明可以化简成:
+请注意,当 Nat.recOn
在证明中使用时,它实际上是变相的归纳原则。rewrite
和 simp
策略在这样的证明中往往非常有效。在这种情况下,证明可以化简成:
namespace Hidden
open Nat
@@ -1061,7 +1061,7 @@ 定义自然
The hardest part is figuring out which variable to do the induction on. Since addition is defined by recursion on the second argument,
``k`` is a good guess, and once we make that choice the proof almost writes itself:
-->
-另一个例子,让我们证明加法结合律,∀ m n k, m + n + k = m + (n + k)
。(我们定义的符号+
是向左结合的,所以m + n + k
实际上是(m + n) + k
。) 最难的部分是确定在哪个变量上做归纳。由于加法是由第二个参数的递归定义的,k
是一个很好的猜测,一旦我们做出这个选择,证明几乎是顺理成章的:
+另一个例子,让我们证明加法结合律,∀ m n k, m + n + k = m + (n + k)
。(我们定义的符号+
是向左结合的,所以m + n + k
实际上是(m + n) + k
。) 最难的部分是确定在哪个变量上做归纳。由于加法是由第二个参数的递归定义的,k
是一个很好的猜测,一旦我们做出这个选择,证明几乎是顺理成章的:
namespace Hidden
open Nat
theorem add_assoc (m n k : Nat) : m + n + k = m + (n + k) :=
@@ -1105,7 +1105,7 @@ 定义自然
At this point, we see that we need another supporting fact, namely, that ``succ (n + m) = succ n + m``.
You can prove this by induction on ``m``:
-->
-在这一点上,我们看到我们需要另一个事实,即succ (n + m) = succ n + m
。你可以通过对m
的归纳来证明这一点:
+在这一点上,我们看到我们需要另一个事实,即 succ (n + m) = succ n + m
。你可以通过对 m
的归纳来证明这一点:
open Nat
theorem succ_add (n m : Nat) : succ n + m = succ (n + m) :=
@@ -1121,7 +1121,7 @@ 定义自然
-然后你可以用succ_add
代替前面证明中的sorry
。然而,证明可以再次压缩:
+然后你可以用 succ_add
代替前面证明中的 sorry
。然而,证明可以再次压缩:
namespace Hidden
open Nat
theorem succ_add (n m : Nat) : succ n + m = succ (n + m) :=
@@ -1145,7 +1145,7 @@ namespace Hidden
inductive List (α : Type u) where
| nil : List α
@@ -1176,7 +1176,7 @@ namespace Hidden
inductive List (α : Type u) where
@@ -1207,7 +1207,7 @@ inductive BinaryTree where
| leaf : BinaryTree
@@ -1251,8 +1251,8 @@
applied to an element ``x`` in the local context. It then reduces the
goal to cases in which ``x`` is replaced by each of the constructions.
-->
-归纳类型在Lean中有最根本的重要性,因此设计了一些方便使用的策略,这里讲几种。
-cases
策略适用于归纳定义类型的元素,正如其名称所示:它根据每个可能的构造器分解元素。在其最基本的形式中,它被应用于局部环境中的元素x
。然后,它将目标还原为x
被每个构成体所取代的情况。
+归纳类型在Lean 中有最根本的重要性,因此设计了一些方便使用的策略,这里讲几种。
+cases
策略适用于归纳定义类型的元素,正如其名称所示:它根据每个可能的构造子分解元素。在其最基本的形式中,它被应用于局部环境中的元素x
。然后,它将目标还原为 x
被每个构成体所取代的情况。
example (p : Nat → Prop) (hz : p 0) (hs : ∀ n, p (Nat.succ n)) : ∀ n, p n := by
intro n
cases n
@@ -1270,7 +1270,7 @@
below, notice that the hypothesis ``h : n ≠ 0`` becomes ``h : 0 ≠ 0``
in the first branch, and ``h : succ m ≠ 0`` in the second.
-->
-还有一些额外的修饰功能。首先,cases
允许你使用with
子句来选择每个选项的名称。例如在下一个例子中,我们为succ
的参数选择m
这个名字,这样第二个情况就指的是succ m
。更重要的是,cases策略将检测局部环境中任何依赖于目标变量的项目。它将这些元素还原,进行拆分,并重新引入它们。在下面的例子中,注意假设h : n ≠ 0
在第一个分支中变成h : 0 ≠ 0
,在第二个分支中变成h : succ m ≠ 0
。
+还有一些额外的修饰功能。首先,cases
允许你使用 with
子句来选择每个选项的名称。例如在下一个例子中,我们为 succ
的参数选择m
这个名字,这样第二个情况就指的是succ m
。更重要的是,cases策略将检测局部环境中任何依赖于目标变量的项目。它将这些元素还原,进行拆分,并重新引入它们。在下面的例子中,注意假设h : n ≠ 0
在第一个分支中变成h : 0 ≠ 0
,在第二个分支中变成h : succ m ≠ 0
。
open Nat
example (n : Nat) (h : n ≠ 0) : succ (pred n) = n := by
@@ -1285,7 +1285,7 @@
-cases
可以用来产生数据,也可以用来证明命题。
+cases
可以用来产生数据,也可以用来证明命题。
def f (n : Nat) : Nat := by
cases n; exact 3; exact 7
@@ -1311,7 +1311,7 @@
-下面是一个带有参数的多个构造器的例子。
+下面是一个带有参数的多个构造子的例子。
inductive Foo where
| bar1 : Nat → Nat → Foo
| bar2 : Nat → Nat → Nat → Foo
@@ -1325,7 +1325,7 @@