coq的一点体会2

下面是谓词逻辑。在coq里，量词的表示如下：

全称量词：forall

存在量词：exists

同样都有自己的引入规则和删除规则

1. forall引入规则 intros x

输入intros x就可以提取出一个前提x，使得结论成为F。intros前面有讲很多，这里就不多说了。

2. forall删除规则 apply H

对于已知的前提H : forall x:A , F.可以用它来简化结论，比如对于H : forall x:A, P x -> forall y:A, R x y -> R x (f y)，输入coq>apply H. 可以看到目标R a (f (f a))被分解为两个：P a 和 R a (f a)

下面来举个课件中的例子。。下面有用到";" 意思就是两句合并到一起执行。注意有时A ; B与A. （换行） B. 的运行结果是不一样的，这两句并不等价。

输入：

Hypothesis Hf : forall x y:A, R x y -> R x (f y).
Hypothesis R_refl : forall x:A, R x x.
Lemma Lf : forall x :A, R x (f (f (f x))).
Proof.
intro x;apply Hf.

1 subgoal

Hf : forall x y : A, R x y -> R x (f y)
R refl : forall x : A, R x x
x : A
============================
R x (f (f x))

repeat apply Hf.

1 subgoal
A : Set
f : A -> A
Hf : forall x y : A, R x y -> R x (f y)
R refl : forall x : A, R x x
x : A
============================
R x x

apply R_refl.
Qed.

有时候应用前提来证明时，系统并不知道如何给forall x:A找到一个合适的赋值，在我们输入apply H时，会给出如下的错误提示：

Error: Unable to find an instance for the variable m.

这时需要给出H的赋值，使用with后缀。下面看一个例子：

Hypothesis lt_trans : forall n m p : nat, n m

n Lemma lt_n_SSn : forall i:nat, i Proof.
intro i.