Software Foundations

Table of Contents

本套丛书是形式化验证与 Programming Language 的入门经典书籍。

Link: https://softwarefoundations.cis.upenn.edu/

Logical Foundations

第一册书主要内容是讲如何写 Coq,我开了一个 repo 来完成书中的样例和习题:https://github.com/yzh119/software-foundations.

Basics

Coq 是一门纯函数式语言,除了函数式语言的一般功能(Function defintion, ADT, Pattern Matching)之外,提供了定义定理和证明的功能。

Coq 中自然数类型(nat)是由 church numerals 定义的,在我之前的博文中有过解释,是一个归纳类型,因而通过简单的 type checking 就可以证明一些正整数上的定理。

通常我们开发软件的时候会写单元测试,里面的 assertion 就相当于定理,不同之处在于单元测试通常是手动设置一些样例判断正确性,而 Coq 中的证明需要保证在所有的情况下命题均成立。

声明一个定理及其证明的格式如下

Theorem plus_id_example : forall n m : nat,
  n = m ->
  n + n = m + m.
Proof.
  intros n m.
  intros H.
  rewrite <- H.
  reflexivity.
  Qed.

其中 intros , rewrite , reflexivity 都属于 tactics,表示我们证明中使用的技巧,需要手动完成。在以上的例子中, intros 的含义是引入变量, rewrite <- H 表示按照 hypothesis (从右到左的方向)改写当前的命题, reflexivity 表示判断左右是否代表同一个对象。

使用 destruct 可以对 inductive type 进行操作,对所有可能的情况进行 pattern matching 并分类证明,即分类讨论。

(* discriminate means hypothesis is not correct *)
Theorem andb_true_elim: forall b c : bool,
  andb b c = true -> c = true.
Proof.
  intros b c.
  destruct b eqn:Eb.
  - simpl.
    intros H.
    rewrite -> H.
    reflexivity.
  - simpl.
    intros H.
    discriminate.
  Qed.

TODO Proof by Induction

Author: expye(Zihao Ye)

Email: expye@outlook.com

Date:

Last modified: 2021-02-19 Fri 21:14

Licensed under CC BY-NC 4.0