Coq 使用笔记
Coq中可分三部分：
1、vernacular：用来处理定义，使用大写字母开头，例如Theorem、Proof、Qed
2、tactics：用作证明过程，以小写字母开头，例如intros、exact
3、Gallina：用来描述定理，例如(forall A : Prop, A -> A)
基本形式
Theorem ident body: type.
Proof.Tactics
Qed.
- 解释：
- Theorem是Coq中的一个命令，它声明了一个应该被证明的新定理;
- ident是新定理的名称；
- body是新定理的主体；
- type为类型；
- Proof开始定理的证明。在此之后需要给出完整的定理证明；
- Tactics为策略类型，接下来主要会介绍：intros, apply, inversion, split, right and left.
- Qed命令证明结尾符，表示证明完成；
- 每个Coq命令都要加上.表示结束；
- (* COMMENTS HERE *)表示注释；
1.Tactics：intros & apply
- 范例1：
1 Theorem example1: forall P:Prop,P -> P.
2 Proof.
3 intros.
4 apply H.
5 Qed.
首先通过Theorem来声明一个名为example1的定理。该定理为forall P:Prop,P -> P。这里的A : Prop表示一个具有Prop类型的A。类似的有0 : nat表示一个自然数0，true : bool表示一个布尔值true。下面的Proof表示证明开始，Qed示证明结束。
1.1 intros： 引入前提
- 基于当前目标，intros有不同的的效果。对
forall T:type将会在上下文(local context)中引入T: type，对T -> U会引入Hn: T。也就是，intros会从目标中按照顺序引入假设。每一次它会消耗 forall 里面的一个自由变量，或者是一个 -> 前面的命题（也就是前提条件）。intros.会引入所有的假设，Coq 会自动给他们命名。如范例1中，执行到第三行时会输出如下：
如上窗口为证明过程展示，即goal windows展示内容。在水平线上的称为假设(hypotheses)或上下文(the context)，在水平线下的是要证明的东西，称为the current subgoal我们要证明的定理(theorem)称为goal，而subgoal指的是我们在证明过程的任意一点需要证明的东西
1.2 apply
- 在范例1中的第三行后，我们得到一个名为H的假设其值为P。其假设值与我们唯一的子目标相同。此时使用apply即可完成证明。也就是，当您有一个与目标相同的假设时就可以用apply完成证明。
- apply的高级用法：
- 范例2：
Theorem example2: forall P Q: Prop,(P -> Q) -> P -> Q.
Proof.intros.apply H in H0.apply H0.
Qed.
在例2中，转到第四行，我们从局部上下文中得到了两个假设，但它们都不与我们的目标相同，如图：
即我们知道了从P->Q,同时得到假设P。可使用策略apply … in …，从而得到假设Q。
1.3 Qed
- 当目标窗口显示
No more subgoals.时，您可以使用Qed命令来完成证明 ，该命令将使Coq保存该定理及其证明。
练习1
- 使用intros 和 apply证明定理：P -> (Q -> P)
Theorem exercise1: forall P Q:Prop,P -> (Q -> P).
Proof.intros.apply H.
Qed.
2.Tactics：inversion & split
2.1 inversion
- 范例3：
Theorem example3: forall P Q: Prop,P/\Q -> Q.
Proof.intros.inversion H.apply H1.
Qed.
inversion用于对在上下文中的连词(Coq中的/\ )进行分解，即将P/\Q分解为
H0:P和H1:Q。
2.1 split
- 范例4：
Theorem example4: forall P Q:Prop,(P /\ Q) -> (Q /\ P).
Proof.intros.inversion H.split.apply H1.apply H0.
Qed.
同inversion,split主要用来分解goal中的连词。如范例3，slpit将
Q /\ P分解成2个goal P 和 Q。
3.Tactics：right & left
- 范例5：
Theorem example5: forall P Q: Prop,(P \/ Q) -> (Q \/ P).
Proof.intros.inversion H.right.apply H0.left.apply H0.
Qed.
- 该策略针对goal中的
\/运算符。对上下文中的\/取inversion策略会生成2个子目标，2个子目标具有相同的结论但在上下文中有不同的H0值。在第一个子目标中，我们需要在假设H0:P的情况下证明Q\/P，由于该运算符只要求左右中一个为真即可成立，因此此时使用right即可证明。在第二个子目标中使用left完成一样的操作。
