在精益(Lean)中对定理进行证明(第一章)

1. 介绍

1.1 计算机与定理证明

形式验证包括使用逻辑和计算方法，以此建立以精确数学术语表达的论述。这些论述可以包括普通的数学定理，以及硬件或软件，网络协议以及机械和混合系统满足其规范的要求的论述。实际上，在验证一个数学定理和验证系统的正确性之间没有明显的区别：形式验证需要用数学术语描述硬件和软件系统，此时建立关于它们正确性的声明成为一种定理证明形式。相反，数学定理的证明可能需要冗长的计算，在这种情况下，验证定理的真实性需要验证计算是否完成它应该做的事情。

支持数学论述的黄金标准是提供证明，二十世纪的逻辑发展表明大多数（如果不是全部）传统证明方法可以在许多基础系统中的任何一个中简化为一小组公理和规则。通过这种减少，计算机可以通过两种方式帮助建立论述：它可以帮助首先找到证明，并且可以帮助验证论述的证明是正确的。

自动定理证明侧重于“发现”方面。求解型定理证明，表格型定理证明，快速可满足性求解等提供了在命题逻辑和一阶逻辑中建立公式有效性的方法。其他系统为特定语言和域提供搜索过程和决策过程，例如整数或实数上的线性或非线性表达式。像SMT ("satisfiability modulo theories") 这样的架构（“可满足性模数理论”）将领域一般搜索方法与特定领域的程序相结合。计算机代数系统和专用数学软件包提供了执行数学计算，建立数学界限或查找数学对象的手段。计算也可以被视为证明，这些系统也有助于建立数学论述。

自动推理系统追求功率和效率，通常以保证稳健性为代价。这样的系统可能存在缺陷，并且可能难以确保它们提供的结果是正确的。相反，交互式定理证明侧重于定理证明的“验证”方面，要求在合适的公理基础中证明支持每一个主张。这就设定了一个非常高的标准：每个推理规则和计算的每一步都必须通过诉诸先前的定义和定理来证明，一直到基本公理和规则。事实上，大多数此类系统提供了完全精心设计的“证明对象”，可以与其他系统进行通信并进行独立检查。构建此类证明通常需要来自用户的更多输入和交互，但它允许我们获得更深入和更复杂的证明。

精益定理证明者（ Lean Theorem Prover）旨在通过在支持用户交互和构建完全指定的公理证明的框架中设置自动化工具和方法来弥合交互式和自动化定理证明之间的差距。目标是支持复杂系统的数学推理和推理，并验证两个方面中的论述。

1.2 关于 Lean

精益项目( Lean project)由Leonardo de Moura于2012年在Microsoft Research Redmond推出。这是一项持续的长期努力，自动化的大部分潜力只会逐渐实现。 Lean是在Apache 2.0许可下发布的，这是一个许可的开源许可证，允许其他人自由使用和扩展代码和数学库。

目前有两种使用精益(Lean)的方法。第一种是从网上运行它：一个Javascript版本的Lean，一个标准的定义和定理库，一个编辑器实际上下载到你的浏览器并在那里运行。这为开始试验系统提供了一种快捷方便的方法。

使用精益(Lean)的第二种方法是在您的计算机上本地安装和运行它。本机版本比Web版本快得多，并且在其他方面也更灵活。它带有一个Emacs模式，为编写和调试校样提供强大的支持，更适合严肃使用。

1.3关于本书

本书旨在教您开发和验证精益(Lean)证明。为了做到这一点，您需要的大部分背景信息都不是Lean特有的。首先，我们将解释Lean所依据的逻辑系统，一种依赖类型理论的版本，其功能足以证明几乎任何传统的数学定理，并且表达足以以自然的方式进行。我们不仅将解释如何定义数学对象并在依赖类型理论中表达数学断言，还将解释如何将其用作编写证明的语言。

事实上，精益支持两种版本的依赖型理论。第一种是称为诱导结构微积分[1,2]或CIC的系统的变体。这是Lean标准库使用的系统，也是本教程的重点。第二版依赖型理论实现了同伦型理论的公理框架，我们将在后面的章节中讨论。

因为完全详细的公理证明是如此复杂，定理证明的挑战是让计算机尽可能多地填写细节。我们将描述在依赖型理论中支持这种情况的各种方法。例如，我们将讨论术语重写，以及Lean自动简化术语和表达式的自动化方法。类似地，我们将讨论精化和类型推断的方法，它们可用于支持灵活的代数推理形式。

最后，当然，我们将讨论精益特有的功能，包括与系统通信的语言，以及精益管理复杂理论和数据的机制。

如果您在Lean的在线教程系统中阅读本书，您将在右侧看到精简编辑器的副本，其下方有一个输出缓冲区。在任何时候，您都可以在编辑器中输入内容，按“播放”按钮，然后查看精益的响应。请注意，如果您愿意，可以调整各种窗口的大小。

在整个文本中，您将找到如下所示的精益代码示例：

theorem and_commutative (p q : Prop) : p ∧ q → q ∧ p :=
assume Hpq : p ∧ q,
have Hp : p, from and.elim_left Hpq,
have Hq : q, from and.elim_right Hpq,
show q ∧ p, from and.intro Hq Hp

再一次，如果你在网上看书，你会看到一个按钮，上面写着“自己试试”。按下按钮将示例复制到具有足够周围上下文的精益编辑器中，以使示例正确编译，然后运行精益。我们建议您在完成后续章节时自行运行示例并尝试使用代码。

1.4致谢

本教程是在Github上维护的开放式访问项目。许多人为这项工作做出了贡献，提供了更正，建议，示例和文本。我们感谢Ulrik Buchholz，Nathan Carter，Amine Chaieb，Floris van Doorn，Anthony Hart，Sean Leather，Christopher John Mazey，Daniel Velleman和ThéoZimmerman的贡献，我们向那些无意中遗漏了我们名字的人道歉。

参考文献

[1]	Thierry Coquand and Gerard Huet. The calculus of constructions. Inf. Comput., 76(2-3):95--120, February 1988.

[2]

Frank Pfenning and Christine Paulin-Mohring. Inductively defined types in the calculus of constructions. In Michael G. Main, Austin Melton, Michael W. Mislove, and David A. Schmidt, editors, Mathematical Foundations of Programming Semantics, 5th International Conference, Tulane University, New Orleans, Louisiana, USA, March 29 - April 1, 1989, Proceedings, volume 442 of Lecture Notes in Computer Science, pages 209--228. Springer, 1989.

在精益(Lean)中对定理进行证明(第一章)相关推荐

latex中使用定理、证明、缩进
1.定理和证明 1 \documentclass[a4paper,UTF8]{article}2 \usepackage{ctex} 3 \usepackage{amsthm,amsmath,amsf ...
计算机网络（中科大郑烇）第一章笔记
文章目录计算机网络课程内容总结第一章.计算机网络和互联网 1.什么是Internet? 2.网络边缘 3.网络核心 4.接入网和物理媒体 5.Internet结构和ISP 6.分组延时.丢失和吞 ...
惯性力偶矩公式中j_第1讲第一章汽车的动力性 1-1汽车的动力性指标 1-2汽车的驱动力与行驶阻力...
第1讲 2学时教学目的和要求: 1.了解课程的任务.内容,掌握其学习方法 2.掌握汽车驱动力含义 3.掌握发动机转矩的获取教学主要内容: 第一章汽车的动力性 §1-1汽车的动力性指标 §1-2汽车 ...
概率论与数理统计中的算子半群第一讲 Banach-Steinhaus定理1 Baire‘s Category与Banach-Steinhaus定理的证明
概率论与数理统计中的算子半群第一讲 Banach-Steinhaus定理1 Baire's Category与Banach-Steinhaus定理的证明 Baire's Category Theor ...
能否用计算机证明数学定理大全,那些教材中未给出证明的定理，到底能否使用？...
那些教材中未给出证明的定理,到底能否使用? 初中几何知识体系,是基于<几何原本>中的公理体系建立的,可以看作是公理体系的子集,在教材编写中,为了教学方便,并没有直接照搬,而是有选择性地&q ...
二分图最大匹配的König定理及其证明
本文将是这一系列里最短的一篇,因为我只打算把König定理证了,其它的废话一概没有. 以下五个问题我可能会在以后的文章里说,如果你现在很想知道的话,网上去找找答案: 1. 什么是二分图 ...
Sperner定理及其证明
Sperner定理及其证明额,最近看到了一个十分有趣的定理--Sperner定理.其实这个定理在OI中没什么用处,因此我都没把这篇文章放到我的OI标签里(不知道在MO中是否有用?)但是觉得它很有趣于 ...
（转）二分图最大匹配的König定理及其证明
出处:http://www.matrix67.com/blog/archives/116 二分图最大匹配的König定理及其证明如果你看不清楚第二个字母,下面有一个大号字体版本: 二分图最大匹配的K ...
最小公倍数一些性质定理及证明
文章目录写在前面预备定义主要定理 ★\bigstar★ [a,b]×(a,b)=ab[a,b]\times(a,b)=ab[a,b]×(a,b)=ab 推广 ★\bigstar★ a∣t,b∣t ...
【转载】二分图最大匹配的König定理及其证明 Matrix67原创
二分图最大匹配的König定理及其证明本文将是这一系列里最短的一篇,因为我只打算把König定理证了,其它的废话一概没有. 以下五个问题我可能会在以后的文章里说,如果你现在很想知道的话,网上去找找答 ...

在精益(Lean)中对定理进行证明(第一章)

在精益(Lean)中对定理进行证明(第一章)相关推荐

最新文章

热门文章