diff --git a/dependent_type_theory.html b/dependent_type_theory.html index 73045e0..d45b96e 100644 --- a/dependent_type_theory.html +++ b/dependent_type_theory.html @@ -453,7 +453,7 @@
可以将 Type 0
看作是一个由「小」或「普通」类型组成的宇宙。然后,Type 1
是一个更大的类型范围,其中包含 Type 0
作为一个元素,而 Type 2
是一个更大的类型范围,其中包含 Type 1
作为一个元素。这个列表是不确定的,所以对于每个自然数 n
都有一个 Type n
。Type
是 Type 0
的缩写:
可以将 Type 0
看作是一个由「小」或「普通」类型组成的宇宙。然后,Type 1
是一个更大的类型范围,其中包含 Type 0
作为一个元素,而 Type 2
是一个更大的类型范围,其中包含 Type 1
作为一个元素。这个列表是无限的,所以对于每个自然数 n
都有一个 Type n
。Type
是 Type 0
的缩写:
#check Type
#check Type 0
diff --git a/print.html b/print.html
index d9570bf..17c8c99 100644
--- a/print.html
+++ b/print.html
@@ -652,7 +652,7 @@ 可以将 Type 0
看作是一个由「小」或「普通」类型组成的宇宙。然后,Type 1
是一个更大的类型范围,其中包含 Type 0
作为一个元素,而 Type 2
是一个更大的类型范围,其中包含 Type 1
作为一个元素。这个列表是不确定的,所以对于每个自然数 n
都有一个 Type n
。Type
是 Type 0
的缩写:
可以将 Type 0
看作是一个由「小」或「普通」类型组成的宇宙。然后,Type 1
是一个更大的类型范围,其中包含 Type 0
作为一个元素,而 Type 2
是一个更大的类型范围,其中包含 Type 1
作为一个元素。这个列表是无限的,所以对于每个自然数 n
都有一个 Type n
。Type
是 Type 0
的缩写:
#check Type
#check Type 0
diff --git a/searchindex.js b/searchindex.js
index c54e80e..fd2ad12 100644
--- a/searchindex.js
+++ b/searchindex.js
@@ -1 +1 @@
-Object.assign(window.search, {"doc_urls":["title_page.html#lean-4-定理证明","introduction.html#简介","introduction.html#计算机和定理证明","introduction.html#关于-lean","introduction.html#关于本书","introduction.html#致谢","dependent_type_theory.html#依值类型论","dependent_type_theory.html#简单类型论","dependent_type_theory.html#类型作为对象","dependent_type_theory.html#函数抽象和求值","dependent_type_theory.html#定义","dependent_type_theory.html#局部定义","dependent_type_theory.html#变量和小节","dependent_type_theory.html#命名空间","dependent_type_theory.html#依值类型论依赖着什么","dependent_type_theory.html#隐参数","propositions_and_proofs.html#命题和证明","propositions_and_proofs.html#命题即类型","propositions_and_proofs.html#以命题即类型的方式工作","propositions_and_proofs.html#命题逻辑","propositions_and_proofs.html#合取","propositions_and_proofs.html#析取","propositions_and_proofs.html#否定和假言","propositions_and_proofs.html#逻辑等价","propositions_and_proofs.html#引入辅助子目标","propositions_and_proofs.html#经典逻辑","propositions_and_proofs.html#练习","quantifiers_and_equality.html#量词与等价","quantifiers_and_equality.html#全称量词","quantifiers_and_equality.html#等价","quantifiers_and_equality.html#计算式证明","quantifiers_and_equality.html#存在量词","quantifiers_and_equality.html#多来点儿证明语法","quantifiers_and_equality.html#练习","tactics.html#证明策略","tactics.html#进入策略模式","tactics.html#基本策略","tactics.html#更多策略","tactics.html#结构化策略证明","tactics.html#策略组合器","tactics.html#重写","tactics.html#简化","tactics.html#拆分","tactics.html#扩展策略","tactics.html#练习","interacting_with_lean.html#与-lean-交互","interacting_with_lean.html#导入文件","interacting_with_lean.html#小节续","interacting_with_lean.html#命名空间续","interacting_with_lean.html#属性","interacting_with_lean.html#隐参数续","interacting_with_lean.html#符号","interacting_with_lean.html#符号和优先级","interacting_with_lean.html#强制转换","interacting_with_lean.html#显示信息","interacting_with_lean.html#设置选项","interacting_with_lean.html#使用库","interacting_with_lean.html#自动约束隐参数","interacting_with_lean.html#隐式lambda","interacting_with_lean.html#简单函数语法糖","interacting_with_lean.html#命名参数","inductive_types.html#归纳类型","inductive_types.html#枚举式类型","inductive_types.html#带参数的构造子","inductive_types.html#归纳定义的命题","inductive_types.html#定义自然数","inductive_types.html#其他递归数据类型","inductive_types.html#归纳类型的策略","inductive_types.html#归纳族","inductive_types.html#公理化细节","inductive_types.html#相互和嵌套的归纳类型","inductive_types.html#练习","induction_and_recursion.html#归纳和递归","induction_and_recursion.html#模式匹配","induction_and_recursion.html#通配符和重叠模式","induction_and_recursion.html#结构化递归和归纳","induction_and_recursion.html#局域递归声明","induction_and_recursion.html#良基递归和归纳","induction_and_recursion.html#相互递归","induction_and_recursion.html#依值模式匹配","induction_and_recursion.html#不可访问模式","induction_and_recursion.html#match-表达式","induction_and_recursion.html#局域递归声明","induction_and_recursion.html#练习","structures_and_records.html#结构体和记录","structures_and_records.html#声明结构体","structures_and_records.html#对象","structures_and_records.html#继承","type_classes.html#类型类","type_classes.html#链接实例","type_classes.html#tostring-方法","type_classes.html#数值","type_classes.html#输出参数","type_classes.html#default-instances","type_classes.html#局部实例","type_classes.html#作用于实例","type_classes.html#可判定的命题","type_classes.html#类型类推断的管理","type_classes.html#使用类型泛型进行强制转换","conv.html#转换策略模式","conv.html#基本导航和重写","conv.html#模式匹配","conv.html#结构化转换策略","conv.html#转换模式中的其他策略","axioms_and_computation.html#公理与计算","axioms_and_computation.html#历史与哲学背景","axioms_and_computation.html#命题外延性","axioms_and_computation.html#函数外延性","axioms_and_computation.html#商","axioms_and_computation.html#选择公理","axioms_and_computation.html#排中律"],"index":{"documentStore":{"docInfo":{"0":{"body":20,"breadcrumbs":4,"title":2},"1":{"body":0,"breadcrumbs":0,"title":0},"10":{"body":177,"breadcrumbs":0,"title":0},"100":{"body":126,"breadcrumbs":0,"title":0},"101":{"body":40,"breadcrumbs":0,"title":0},"102":{"body":17,"breadcrumbs":0,"title":0},"103":{"body":191,"breadcrumbs":0,"title":0},"104":{"body":19,"breadcrumbs":0,"title":0},"105":{"body":27,"breadcrumbs":0,"title":0},"106":{"body":47,"breadcrumbs":0,"title":0},"107":{"body":292,"breadcrumbs":0,"title":0},"108":{"body":1098,"breadcrumbs":0,"title":0},"109":{"body":186,"breadcrumbs":0,"title":0},"11":{"body":97,"breadcrumbs":0,"title":0},"110":{"body":691,"breadcrumbs":0,"title":0},"12":{"body":122,"breadcrumbs":0,"title":0},"13":{"body":162,"breadcrumbs":0,"title":0},"14":{"body":158,"breadcrumbs":0,"title":0},"15":{"body":413,"breadcrumbs":0,"title":0},"16":{"body":1,"breadcrumbs":0,"title":0},"17":{"body":253,"breadcrumbs":0,"title":0},"18":{"body":349,"breadcrumbs":0,"title":0},"19":{"body":56,"breadcrumbs":0,"title":0},"2":{"body":28,"breadcrumbs":0,"title":0},"20":{"body":198,"breadcrumbs":0,"title":0},"21":{"body":148,"breadcrumbs":0,"title":0},"22":{"body":101,"breadcrumbs":0,"title":0},"23":{"body":116,"breadcrumbs":0,"title":0},"24":{"body":72,"breadcrumbs":0,"title":0},"25":{"body":368,"breadcrumbs":0,"title":0},"26":{"body":170,"breadcrumbs":0,"title":0},"27":{"body":0,"breadcrumbs":0,"title":0},"28":{"body":398,"breadcrumbs":0,"title":0},"29":{"body":380,"breadcrumbs":0,"title":0},"3":{"body":19,"breadcrumbs":1,"title":1},"30":{"body":565,"breadcrumbs":0,"title":0},"31":{"body":821,"breadcrumbs":0,"title":0},"32":{"body":178,"breadcrumbs":0,"title":0},"33":{"body":143,"breadcrumbs":0,"title":0},"34":{"body":9,"breadcrumbs":0,"title":0},"35":{"body":305,"breadcrumbs":0,"title":0},"36":{"body":505,"breadcrumbs":0,"title":0},"37":{"body":525,"breadcrumbs":0,"title":0},"38":{"body":429,"breadcrumbs":0,"title":0},"39":{"body":254,"breadcrumbs":0,"title":0},"4":{"body":54,"breadcrumbs":0,"title":0},"40":{"body":255,"breadcrumbs":0,"title":0},"41":{"body":820,"breadcrumbs":0,"title":0},"42":{"body":158,"breadcrumbs":0,"title":0},"43":{"body":59,"breadcrumbs":0,"title":0},"44":{"body":19,"breadcrumbs":0,"title":0},"45":{"body":2,"breadcrumbs":2,"title":1},"46":{"body":15,"breadcrumbs":1,"title":0},"47":{"body":64,"breadcrumbs":1,"title":0},"48":{"body":164,"breadcrumbs":1,"title":0},"49":{"body":156,"breadcrumbs":1,"title":0},"5":{"body":38,"breadcrumbs":0,"title":0},"50":{"body":321,"breadcrumbs":1,"title":0},"51":{"body":10,"breadcrumbs":1,"title":0},"52":{"body":104,"breadcrumbs":1,"title":0},"53":{"body":32,"breadcrumbs":1,"title":0},"54":{"body":30,"breadcrumbs":1,"title":0},"55":{"body":55,"breadcrumbs":1,"title":0},"56":{"body":69,"breadcrumbs":1,"title":0},"57":{"body":79,"breadcrumbs":1,"title":0},"58":{"body":75,"breadcrumbs":2,"title":1},"59":{"body":67,"breadcrumbs":1,"title":0},"6":{"body":8,"breadcrumbs":0,"title":0},"60":{"body":255,"breadcrumbs":1,"title":0},"61":{"body":29,"breadcrumbs":0,"title":0},"62":{"body":501,"breadcrumbs":0,"title":0},"63":{"body":314,"breadcrumbs":0,"title":0},"64":{"body":119,"breadcrumbs":0,"title":0},"65":{"body":648,"breadcrumbs":0,"title":0},"66":{"body":172,"breadcrumbs":0,"title":0},"67":{"body":838,"breadcrumbs":0,"title":0},"68":{"body":232,"breadcrumbs":0,"title":0},"69":{"body":41,"breadcrumbs":0,"title":0},"7":{"body":232,"breadcrumbs":0,"title":0},"70":{"body":76,"breadcrumbs":0,"title":0},"71":{"body":37,"breadcrumbs":0,"title":0},"72":{"body":2,"breadcrumbs":0,"title":0},"73":{"body":375,"breadcrumbs":0,"title":0},"74":{"body":210,"breadcrumbs":0,"title":0},"75":{"body":393,"breadcrumbs":0,"title":0},"76":{"body":133,"breadcrumbs":0,"title":0},"77":{"body":535,"breadcrumbs":0,"title":0},"78":{"body":359,"breadcrumbs":0,"title":0},"79":{"body":329,"breadcrumbs":0,"title":0},"8":{"body":261,"breadcrumbs":0,"title":0},"80":{"body":373,"breadcrumbs":0,"title":0},"81":{"body":232,"breadcrumbs":1,"title":1},"82":{"body":134,"breadcrumbs":0,"title":0},"83":{"body":231,"breadcrumbs":0,"title":0},"84":{"body":15,"breadcrumbs":0,"title":0},"85":{"body":241,"breadcrumbs":0,"title":0},"86":{"body":137,"breadcrumbs":0,"title":0},"87":{"body":75,"breadcrumbs":0,"title":0},"88":{"body":321,"breadcrumbs":0,"title":0},"89":{"body":89,"breadcrumbs":0,"title":0},"9":{"body":309,"breadcrumbs":0,"title":0},"90":{"body":36,"breadcrumbs":1,"title":1},"91":{"body":84,"breadcrumbs":0,"title":0},"92":{"body":156,"breadcrumbs":0,"title":0},"93":{"body":205,"breadcrumbs":2,"title":2},"94":{"body":88,"breadcrumbs":0,"title":0},"95":{"body":125,"breadcrumbs":0,"title":0},"96":{"body":251,"breadcrumbs":0,"title":0},"97":{"body":119,"breadcrumbs":0,"title":0},"98":{"body":582,"breadcrumbs":0,"title":0},"99":{"body":2,"breadcrumbs":0,"title":0}},"docs":{"0":{"body":"作者: Jeremy Avigad, Leonardo de Moura, Soonho Kong and Sebastian Ullrich, 以及来自 Lean 社区的贡献者 Lean-zh 项目组 译 本书假定你使用 Lean 4。安装方式参见 Lean 4 手册 中的 快速开始 一节。 本书的第一版为 Lean 2 编写,Lean 3 版请访问 此处 。","breadcrumbs":"Lean 4 定理证明 » Lean 4 定理证明","id":"0","title":"Lean 4 定理证明"},"1":{"body":"","breadcrumbs":"简介 » 简介","id":"1","title":"简介"},"10":{"body":"def 关键字提供了一个声明新对象的重要方式。 def double (x : Nat) : Nat := x + x 这很类似其他编程语言中的函数。名字 double 被定义为一个函数,它接受一个类型为 Nat 的输入参数 x,其结果是x + x,因此它返回类型 Nat。然后你可以调用这个函数: # def double (x : Nat) : Nat :=\n# x + x\n#eval double 3 -- 6 在这种情况下你可以把 def 想成一种 lambda。下面给出了相同的结果: def double : Nat → Nat := fun x => x + x #eval double 3 -- 6 当 Lean 有足够的信息来推断时,你可以省略类型声明。类型推断是 Lean 的重要组成部分: def double := fun (x : Nat) => x + x 定义的一般形式是 def foo : α := bar,其中 α 是表达式 bar 返回的类型。Lean 通常可以推断类型 α,但是精确写出它可以澄清你的意图,并且如果定义的右侧没有匹配你的类型,Lean 将标记一个错误。 bar 可以是任何一个表达式,不只是一个 lambda 表达式。因此 def 也可以用于给一些值命名,例如: def pi := 3.141592654 def 可以接受多个输入参数。比如定义两自然数之和: def add (x y : Nat) := x + y #eval add 3 2 -- 5 参数列表可以像这样分开写: # def double (x : Nat) : Nat :=\n# x + x\ndef add (x : Nat) (y : Nat) := x + y #eval add (double 3) (7 + 9) -- 22 注意到这里我们使用了 double 函数来创建 add 函数的第一个参数。 你还可以在 def 中写一些更有趣的表达式: def greater (x y : Nat) := if x > y then x else y 猜猜这个可以做什么。 还可以定义一个函数,该函数接受另一个函数作为输入。下面调用一个给定函数两次,将第一次调用的输出传递给第二次: # def double (x : Nat) : Nat :=\n# x + x\ndef doTwice (f : Nat → Nat) (x : Nat) : Nat := f (f x) #eval doTwice double 2 -- 8 现在为了更抽象一点,你也可以指定类型参数等: def compose (α β γ : Type) (g : β → γ) (f : α → β) (x : α) : γ := g (f x) 这句代码的意思是:函数 compose 首先接受任何两个函数作为参数,这其中两个函数各自接受一个输入。类型β → γ和α → β意思是要求第二个函数的输出类型必须与第一个函数的输入类型匹配,否则这两个函数将无法复合。 compose 再接受一个类型为compose 再参数作为第二个函数(这里叫做 f)的输入,通过这个函数之后的返回结果类型为β,再作为第一个函数(这里叫做 g)的输入。第一个函数返回类型为γ,这就是 compose 函数最终返回的类型。 compose 可以在任意的类型α β γ上使用,它可以复合任意两个函数,只要前一个的输出类型是后一个的输入类型。举例: # def compose (α β γ : Type) (g : β → γ) (f : α → β) (x : α) : γ :=\n# g (f x)\n# def double (x : Nat) : Nat :=\n# x + x\ndef square (x : Nat) : Nat := x * x #eval compose Nat Nat Nat double square 3 -- 18","breadcrumbs":"依值类型论 » 定义","id":"10","title":"定义"},"100":{"body":"作为第一个例子,让我们证明(a b c : Nat) : a * (b * c) = a * (c * b)(本段中的例子有些刻意设计,因为其他策略可以立即完成它们)。首次简单的尝试是尝试rw [Nat.mul_comm],但这将目标转化为b * c * a = a * (c * b),因为它作用于项中出现的第一个乘法。有几种方法可以解决这个问题,其中一个方法是 example (a b c : Nat) : a * (b * c) = a * (c * b) := by rw [Nat.mul_comm b c] 不过本节介绍一个更精确的工具:转换模式。下面的代码块显示了每行之后的当前目标。 example (a b c : Nat) : a * (b * c) = a * (c * b) := by conv => -- ⊢ a * (b * c) = a * (c * b) lhs -- ⊢ a * (b * c) congr -- 2 goals: ⊢ a, ⊢ b * c rfl -- ⊢ b * c rw [Nat.mul_comm] 上面这段涉及三个导航指令: lhs(left hand side)导航到关系(此处是等式)左边。同理rhs导航到右边。 congr创建与当前头函数的(非依赖的和显式的)参数数量一样多的目标(此处的头函数是乘法)。 skip走到下一个目标。 一旦到达相关目标,我们就可以像在普通策略模式中一样使用rw。 使用转换模式的第二个主要原因是在约束器下重写。假设我们想证明(fun x : Nat => 0 + x) = (fun x => x)。首次简单的尝试rw [zero_add]是失败的。报错: error: tactic 'rewrite' failed, did not find instance of the pattern in the target expression 0 + ?n\n⊢ (fun x => 0 + x) = fun x => x (错误:'rewrite'策略失败了,没有找到目标表达式中的模式0 + ?n) 解决方案为: example : (fun x : Nat => 0 + x) = (fun x => x) := by conv => lhs intro x rw [Nat.zero_add] 其中intro x是导航命令,它进入了fun约束器。这个例子有点刻意,你也可以这样做: example : (fun x : Nat => 0 + x) = (fun x => x) := by funext x; rw [Nat.zero_add] 或者这样: example : (fun x : Nat => 0 + x) = (fun x => x) := by simp 所有这些也可以用conv at h从局部上下文重写一个假设h。","breadcrumbs":"转换策略模式 » 基本导航和重写","id":"100","title":"基本导航和重写"},"101":{"body":"使用上面的命令进行导航可能很无聊。使用下面的模式匹配来简化它: example (a b c : Nat) : a * (b * c) = a * (c * b) := by conv in b * c => rw [Nat.mul_comm] 这是下面代码的语法糖: example (a b c : Nat) : a * (b * c) = a * (c * b) := by conv => pattern b * c rw [Nat.mul_comm] 当然也可以用通配符: example (a b c : Nat) : a * (b * c) = a * (c * b) := by conv in _ * c => rw [Nat.mul_comm]","breadcrumbs":"转换策略模式 » 模式匹配","id":"101","title":"模式匹配"},"102":{"body":"大括号和.也可以在conv模式下用于结构化策略。 example (a b c : Nat) : (0 + a) * (b * c) = a * (c * b) := by conv => lhs congr . rw [Nat.zero_add] . rw [Nat.mul_comm]","breadcrumbs":"转换策略模式 » 结构化转换策略","id":"102","title":"结构化转换策略"},"103":{"body":"arg i进入一个应用的第i个非独立显式参数。 example (a b c : Nat) : a * (b * c) = a * (c * b) := by conv => -- ⊢ a * (b * c) = a * (c * b) lhs -- ⊢ a * (b * c) arg 2 -- ⊢ b * c rw [Nat.mul_comm] args是congr的替代品。 simp将简化器应用于当前目标。它支持常规策略模式中的相同选项。 def f (x : Nat) := if x > 0 then x + 1 else x + 2 example (g : Nat → Nat) (h₁ : g x = x + 1) (h₂ : x > 0) : g x = f x := by conv => rhs simp [f, h₂] exact h₁ enter [1, x, 2, y]是arg和intro使用给定参数的宏。 syntax enterArg := ident <|> group(\"@\"? num)\nsyntax \"enter \" \"[\" (colGt enterArg),+ \"]\": conv\nmacro_rules | `(conv| enter [$i:num]) => `(conv| arg $i) | `(conv| enter [@$i:num]) => `(conv| arg @$i) | `(conv| enter [$id:ident]) => `(conv| ext $id) | `(conv| enter [$arg:enterArg, $args,*]) => `(conv| (enter [$arg]; enter [$args,*])) done会失败如果有未解决的目标。 traceState显示当前策略状态。 whnf put term in weak head normal form. tactic =>