面向逻辑学专业的Coq入门系列讲座
时间：12月1日下午3:00-5:30，12月2日下午3:00-5:30，12月3日上午9:30-12:00
地点：北京大学哲学系（人文学苑2号楼）B114（地下）
报告人：曹钦翔（普林斯顿大学计算机系）
【English follows Chinese】
在这个系列讲座中，我将向大家介绍Coq这一款管理形式化的数学证明的软件。在Coq中，用户可以像开发软件一样开发一个大型的“形式化”的数学证明。事实上，Coq在学术界有着广阔的应用前景。其中一个应用方向是数学类论文的审稿。当前，大量的审稿精力用在了判断一个证明究竟是否正确，广泛运用Coq形式化证明将会极大的避免这一问题。另一个类似的应用则是数学类课程的教学。当前大学数学课程的助教需要花费大量时间评判作业、阅读学生书写的证明，把Coq应用在教学中可以让这一过程自动化完成。
UnifySL是由我主要开发一个用于逻辑学研究、 形式化证明逻辑学结论的Coq工具库（在此感谢我的合作者Santiago Cuellar）。在这个系列研讨会上，我将会向大家介绍如何使用Coq和UnifySL。请大家携带笔记本，安装Coq 8.6，相关的文件和练习请在这里下载。
第一次讲座： 在Coq中做证明 （12月1日下午）
我会通过一系列有趣的例子来介绍如何使用Coq。我们会一同证明以下定理：
（1）群论问题：用左单位元和左逆元推导右单位元和右逆元，
（2) Peano算数：从Peano公理证明加法交换律和结合律，
（3) 一阶逻辑的定理：De morgan定律在经典逻辑和直觉主义逻辑中的证明（其中一些在直觉主义中无法证明）。
同时，我会介绍Curry-Howard同构并讲解形式化证明在Coq内部的表示方法。
第二讲：Coq作为元语言 （12月2日下午）
我们会看到Coq可以作为一种元语言用于证明对象语言的性质。在UnifySL中，我们形式化了直觉主义命题逻辑的Kripke语义学、公理系统。我们证明了直觉主义命题逻辑的可靠性。我们也将从命题逻辑的公理推导其有用的内定理。例如，我们会在对象语言中再一次推导De morgan定律。
就像计算机软件工程师总是希望他们的编程语言能够支持代码复用一样，我们也希望我们不需要在Coq中重复输入相似的证明。我们将会看到，Coq系统很好的支持了这一点。
第三讲：在Coq中定义对象语言 （12月3日上午）
在上一次研讨会中，我们还尚未定义任何一种具体的对象语言。所有的关于对象语言的性质的证明，都是在证明“对于一切符合某些性质的对象语言、语义学、推理系统的某些性质”。在这一次讲座中，我们将会完成这个具体化的步骤。 锚点 锚点我们会定义命题语言、模态语言。通过这些定义，我们将一窥Coq如何定义自然数以及Coq自身的逻辑基础: Calculus of Inductive Constructor。我们还将看到UnifySL如何形式化一个对象语言的推理系统的完全性证明。在这一过程中，我们将再一次看到Coq对于“证明复用”的支持。
English abstract:
In these three lectures, I will introduce Coq and UnifySL to my audience. Coq is a formal proof management system. Users can build formal proofs in it. UnifySL is a library built in Coq for formalized logic results and further logic research.
I will teach how to use Coq. I will demonstrate the main feature of UnifySL and some formalized theorems in it.
Lecture 1. Building Proofs in Coq
In this talk, I will show how to write proofs in Coq by some interesting examples. We will prove the following theorems together:
(1) Group theory: right unit property and right reverse property can be derived from left unit property and left reverse property.
(2) Peano arithmetic: commutativity and associativity of addition. There is no greatest natural number.
(3) Intuitionistic/classical first-order logic: De morgan's law.
At the end of the talk, I will introduce Curry-Howard isomorphism and explain what is actually beyond our coq proof script.
Lecture 2. Coq as a Meta Language
In this talk, I start to describe and prove theorems about object languages in Coq. In other words, Coq will be used as a meta-language. We will formalize Kripke semantics and proof theory of intuitionistic propositional logic. We will show its soundness. We will derive useful theorems of object languages. For example, we will rederive intuitionistic De morgan's law, this time, in object languages.
We will see that Coq allows us proof scripts without copy and paste.
Surprisingly, we do not need to define a specific object language. All what we would prove are general theorems.
Lecture 3. Coq: Calculus of Inductive Constructor (Build the Syntax Trees of Object Languages)
In this talk, we will use syntax tree of object languages to introduce the underlying logic of Coq: the Calculus of Inductive Constructor. We will also go through a formalized completeness proof.
发布时间：2017-11-02 18:04:48