Coq 常用证明

化简等式

对于简单的等式，可以使用 simpl 将等式进行化简，然后用 reflexivity 即等号的自反性证明。

Theorem plus_O_n : forall n : nat, 0 + n = n.
Proof.
  intros n. simpl. reflexivity.  Qed.

Coq 系统中可以自动化简，故只使用 reflexivity 也可证明定理。

Theorem plus_O_n : forall n : nat, 0 + n = n.
Proof.
  intros n. reflexivity.  Qed.

根据条件重写式子

当定理中含有条件时，如下 n=m 为条件，则需要将条件引入，即 intros H，此时 H 表示 n=m 这个条件。然后使用 rewrite 命令，根据条件重写式子。有两种方式使用 rewrite:

• rewrite <- H：得到 n+n=n+n
• rewrite -> H：得到 m+m=m+m

有时需要分析应该使用哪种方式。

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

分类讨论

分类讨论是根据变量的类型进行分情况讨论。如下，引入 n，n 的类型为 nat。nat 有两种情况，第一种情况是 O，即数字 0，第二种情况为 S n'，其中 n' 为需要的参数。

Theorem plus_1_neq_0 : forall n : nat,
  (n + 1) =? 0 = false.
Proof.
  intros n. destruct n as [| n'] eqn:E.
  - reflexivity.
  - reflexivity.   Qed.

可将 intros n. destruct n as [| n'] eqn:E. 简写为 intros [|n'].。