DoctorKey 的博客

化简等式

对于简单的等式，可以使用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'].。