鸡年当然要学习鸡语言啦。

简介

Coq 是一个基于构造演算的定理证明辅助工具。

在开始玩耍之前需要到官网下载 Coq

安装完成后打开 Coq 的 REPL —— Coq.exe 。

打开后能看到类似内容

1
2
3
Welcome to Coq 8.6 (December 2016)

Coq <

输入 "Hello World". 打印 Hello World 。

然而并没有什么 Hello World :P 。

普通的引理

先来证明一个普通的引理，算是 Hello World 吧。

在 Coq 中输入一下内容。 被 (* 和 *) 括起来的是注释不用输入。 「Coq <」 也不用输入。

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
Coq < Section Minimal_Logic. (* 以点号结尾，类似 C 语言的分号 *)

Coq < Variables A B C : Prop. (* 如果还没输入点就换行了，只需输入点就能结束 *)
A is assumed
B is assumed
C is assumed

Coq < Goal (A -> B -> C) -> (A -> B) -> A -> C.
1 subgoal

  A, B, C : Prop
  ============================
  (A -> B -> C) -> (A -> B) -> A -> C

Unnamed_thm < auto.
No more subgoals.

证明完毕！到此结束，手动再见。

简单的过程

既然愿意了解，那么就一步步来。先撤销证明。

1
2
3
4
5
6
Unnamed_thm < Undo. （* U 是大写 *）
1 subgoal

  A, B, C : Prop
  ============================
  (A -> B -> C) -> (A -> B) -> A -> C

输出的内容中 1 subgoal 说明只有一个目标需要证明

A, B, C : Prop 表示 A B C 都是 Prop 。Prop 是命题 （Proposition）的缩写。

============================ 是分割线。上面的内容是假设和条件。下面的内容是需要证明的部分。

(A -> B -> C) -> (A -> B) -> A -> C 需要证明的内容。 用 () 括起来表示视为一个整体， -> 为蕴涵。

A -> B 读作若 A 则 B。

接下来为了方便证明，需要引入一些假设。

使用 intro 引入一个假设。

1
2
3
4
5
6
7
Unnamed_thm < intro H.
1 subgoal

  A, B, C : Prop
  H : A -> B -> C
  ============================
  (A -> B) -> A -> C

引入了假设 H : A -> B ->C 。证明的目标就变成了 (A -> B) -> A -> C。

还可以引入多个假设。

多个假设使用 intros 就是 intro 加了 s 。

1
2
3
4
5
6
7
8
9
Unnamed_thm < intros H' HA.
1 subgoal

  A, B, C : Prop
  H : A -> B -> C
  H' : A -> B
  HA : A
  ============================
  C

现在需要证明的目标变成了 C 。

观察已有条件，发现假设 H : A -> B -> C 蕴涵 C。当然演绎出 C 还需要 A -> B 。

可以先应用假设，转化证明的目标。

应用假设使用 apply 

1
2
3
4
5
6
7
8
9
10
11
12
Unnamed_thm < apply H.
2 subgoals

  A, B, C : Prop
  H : A -> B -> C
  H' : A -> B
  HA : A
  ============================
  A

subgoal 2 is:
 B

现在目标变成了两个，一个 A 一个 B 。

观察已有条件，A 刚好是假设 HA : A 。

使用 exact 表示刚好。

1
2
3
4
5
6
7
8
9
Unnamed_thm < exact HA.
1 subgoal

  A, B, C : Prop
  H : A -> B -> C
  H' : A -> B
  HA : A
  ============================
  B

现在目标变成了 B 。

观察已有条件，假设 H' : A -> B 蕴含了 B 。

那么应用 H' 即可。

1
2
3
4
5
6
7
8
9
Unnamed_thm < apply H'.
1 subgoal

  A, B, C : Prop
  H : A -> B -> C
  H' : A -> B
  HA : A
  ============================
  A

现在目标变成了 A。

之前已经证明了 A 。这里可以用 exact HA. 。

也可以直接总结，表示目标已经证明。

总结使用 assumption。

1
2
Unnamed_thm < assumption.
No more subgoals.

No more subgoals 说明没有需要证明的目标了。证明结束。

证明可以使用 Save 保存。

1
2
3
4
5
6
7
8
9
10
11
Unnamed_thm < Save trivial_lemma.
intro H.
(intros H' HA).
(apply H).
 exact HA.

 (apply H').
 assumption.

Save trivial_lemma.
trivial_lemma is defined

中间的部分就是证明的过程。

最后

这次就简单的写个 Hello World 的笔记。后面的内容还需要慢慢整理。