形式化方法课程学习笔记（一）|Cop的安装以及简单使用

---

一、Cop的介绍以及安装

---

1、Cop介绍

Coq是一个著名的，也被广泛使用的正式证明管理系统。它提供了一种正式的语言来编写数学定义、可执行的算法和定理，以及用于机器检查证明的半交互式开发的环境。有关Coq的更多信息，以及Coq的文档。

在这门课中，我们将用Coq来做命题逻辑、谓词逻辑和构造逻辑的定理证明。

2、Cop安装

我们将安装使用8.4.0版本之后的Coq，以下是不同平台的安装说明:
Windows/MacOS
直接从从Cop项目发行页面下载安装包
我自己是用Windows系统安装Cop8.11.0
百度云链接：https://pan.baidu.com/s/1RvwKwSk88wPs4hxgvQ9b_g
提取码：1yj2

Linux（Ubuntu/Debian）

  # apt-get install coq

3、使用哪个Coq IDE？

Coq附带的用于编辑Coq源代码的官方IDE是“ CoqIde”。
还有另一个流行的IDE：Proof General，它在Coq社区中更受欢迎。

Proof general的安装很简单：
Ubuntu / Debian：

  ＃apt-get install proofgeneral
  ＃apt-get install proofgeneral-coq

4、Cop热身

打开Coq IDE并输入下面的代码文件，单击Go to end按钮，得到如下结果证明安装成功。

Inductive day : Type := 
| monday : day 
| tuesday : day 
| wednesday : day 
| thursday : day 
| friday : day 
| saturday : day 
| sunday : day. 

Definition next_weekday (d:day) : day := 
match d with 
| monday => tuesday 
| tuesday => wednesday 
| wednesday => thursday 
| thursday => friday 
| friday => monday 
| saturday => monday 
| sunday => monday 
end.

Eval compute in (next_weekday friday). 
Eval compute in (next_weekday (next_weekday saturday)). 

---

二、Coq Tactics——Cop的简单使用

---

在本节中，让我们开始学习如何使用Coq进行证明开发。在证明开发的每个阶段，都有一个要证明的子目标列表。最初，列表由定理本身组成。应用某些策略后，目标列表包含该策略生成的子目标。
基本定理如下：

Theorem ident body: type.
Proof.
    Tactics
Qed.
    

• Theorem - Coq中的一个命令，声明了一个需要证明的新定理；
• ident - 新定理的名称；
• body - 新定理的主体；
• type - forall 新定理中出现的变量名（多个变量用空格隔开）:Prop，所要证明的新定理；
• Proof - 标示着证明新定理的开始；
• Tactics - 指导证明的过程，在结论和前提之间提出演绎规则，实现反向推理。tactic用它产生的子目标来代替原来的目标。
• Qed - 标示着完成了定理的证明。

1、Implication（蕴含）: intros and apply tactic

【蕴含的引入规则：intros】
【蕴含的删除规则：apply】

Example 1:

Theorem example1: forall P:Prop,
    P -> P.
Proof.
    intros.
    apply H.
Qed.

（1）当我们进入第3行时，目标窗口将显示为下图，我们的目标在水平线之下。目前，这与断言中表示的假设相同。在水平线上方没有任何内容表示local context为空，没有东西可以使用。

（2）执行intros策略，Local context得到2个可以使用的前提，如下图所示：

基于当前目标，intros策略具有不同的效果，如果是：

forall T: type, T-> U

将 T: type 和 Hn: T 放入 local context，新的子目标就是U。

（3）在步骤（2）中，我们得到了一个名为H的假设，并且该假设的值与我们唯一的子目标相同，当我们得出与目标相同的假设时，使用 apply 策略。

（4）使用Qed命令完成证明：

exercise1
Use intros and apply to prove the below theorem:
P -> (Q -> P)

Theorem exercise1: forall P Q:Prop,
  P -> (Q -> P).
Proof.
intros.
apply H.
Qed.

执行前3行，结果如下：

依次执行：


Example 2:

Theorem example2: forall P Q: Prop,
    (P -> Q) -> P -> Q.
Proof.
    intros.
    apply H in H0.
    apply H0.
Qed.

如果我们知道x->y,并且x为真，那么我们可以使用apply…in…tactic，在这个例子中，我们有假设H : P -> Q , 我们将它应用到另一个假设H0: P中，可以将H0转化为Q。

Exercise 2:
Use tactic apply … in …, to prove:
P -> (Q -> ( H -> Q ))

Theorem exercise2: forall P Q H:Prop,
  P -> (Q -> (H -> Q)).
Proof.
intros.
apply H1.
Qed.

2、Conjunction: inversion and split tactic

Example 3:

Theorem example3: forall P Q: Prop,
    P/\Q -> Q.
Proof.
    intros.
    inversion H.
    apply H1.
Qed.

我们使用inversion tactics去证明含有合取（/\）符号的命题，在这个例子中，我们假设P/\Q为真，当且仅当P、Q都为真的情况下满足，我们可以使用inversion在local context中增加两个假设（H0,H1）。


Exercise 3:
Use the inversion tactics to prove the following proposition:
P/\Q -> P

Theorem exercise3: forall P Q:Prop,
  P/\Q ->P.
Proof.
intros.
inversion H.
apply H0.
Qed.

Example 4:

Theorem example4: forall P Q:Prop,
    (P /\ Q) -> (Q /\ P).
Proof.
    intros.
    inversion H.
    split.
    apply H1.
    apply H0.
Qed.

在例子3中我们知道了如何去处理在context（横线上方）中含有/\的情况，在例子4中我们将讨论在goal（横线下方）中含有/\的情况。


Exercise 4:
With the new tactic split, try to prove:
(P /\ (Q /\ R)) -> ((P /\ Q) /\ R)

Theorem exercise4: forall P Q R:Prop,
  (P /\ (Q /\ R)) -> ((P /\ Q) /\ R).
Proof.
intros.
inversion H.
inversion H1.
split.
split.
apply H0.
apply H2.
apply H3.
Qed.

3、Disjunction: right and left tactic

Example 5:

Theorem example5: forall P Q: Prop,
    (P \/ Q) -> (Q \/ P).
Proof.
    intros.
    inversion H.
    right.
    apply H0.
    left.
    apply H0.
Qed.

执行到第五行的时候，inversion tactic 处理local context 中的/（析取）操作，会产生两个子目标，这两个子目标有相同的结论，但是和local context中的H0不同。

我们需要去证明第一个子目标Q\/P，只需要去证明P,Q其中一个为真即可，所以我们可以使用right tactic 使得子目标和我们的假设H0相同。

同理，证明第二个子目标，使用left tactic。

Exercise 5:
Use tactic left and right to prove:
(P \/ (Q \/ R)) -> ((P \/ Q) \/ R)

Theorem exercise5: forall P Q R:Prop,
  (P \/ (Q \/ R)) -> ((P \/ Q) \/ R).
Proof.
intros.
inversion H.
left.
left.
apply H0.
inversion H0.
left.
right.
apply H1.
right.
apply H1.
Qed.

More Exercises

Exercise 6:
Try to prove:
((P -> R) /\ (Q -> R)) -> (P /\ Q -> R)

Theorem exercise6: forall P Q R:Prop,
  ((P -> R) /\ (Q -> R)) -> (P/\Q -> R).
Proof.
intros.
inversion H.
inversion H0.
apply H1 in H3.
apply H3.
Qed.

Exercise 7:
Try to prove:
(P -> Q /\ R) -> ((P -> Q) /\ (P -> R))
First solution

Theorem exercise7: forall P Q R:Prop,
  (P -> Q /\ R) -> ((P -> Q) /\ (P -> R)).
Proof.
intros.
split.
intros.
apply H in H0.
inversion H0.
apply H1.
intros.
apply H in H0.
inversion H0.
apply H2.
Qed.

Another solution

Theorem exercise7: forall P Q R:Prop,
  (P -> Q /\ R) -> ((P -> Q) /\ (P -> R)).
Proof.
intros.
split.
apply H.
apply H.
Qed.

Challenge1:
Try to prove:
(P /\ Q) /\ R, S /\ T |- Q /\ S

(*(P /\ Q) /\ R, S /\ T |- Q /\ S 
当->左边的两个条件都为真时，可以推出右边的式子为真。
因此，该式子可以改写为
((P /\ Q) /\ R) /\ (S /\ T) -> (Q /\ S)
*)
Theorem challenge1: forall P Q R S T:Prop,
  ((P /\ Q) /\ R) /\ (S /\ T) -> (Q /\ S).
Proof.
intros.
inversion H.
inversion H0.
inversion H1.
inversion H2.
split.
apply H7.
apply H4.
Qed.

Challenge2:
You may find that examples and exercises we’ve studied do not contain any not (aka. ~). Please read the Coq documents and try to prove below theorem:
(P -> Q) -> (~Q -> ~P)

Hint: You may need a new tactic unfold.

(*challenge2*)
(*
有两种方式来消除式子中的"~"
1. unfold not.
2. unfold "~".
*)
Theorem challenge2: forall P Q:Prop,
  (P -> Q) -> (~Q -> ~P).
Proof.
unfold "~".
intros.
apply H in H1.
apply H0 in H1.
apply H1.
Qed.