如何使用Coq证明列表连接运算不满足交换律

核心思路 #

要证明一个全称性质不成立，只需要构造一个反例即可。列表连接的交换律声称「对任意类型A的任意两个列表l1、l2，都有l1 ++ l2 = l2 ++ l1」，我们只要找到一组具体的列表代入后等式不成立，就能完成证明。最易构造的反例就是长度为1的不同元素列表：取l1 = [1]、l2 = [2]，此时l1++l2 = [1;2]，l2++l1 = [2;1]，二者显然不等。

完整实现步骤 #

1. 导入依赖库 #

首先导入Coq标准库的列表模块，开启列表语法糖方便书写：

Require Import List.
Import ListNotations.

2. 编写定理声明 #

我们要证明的是否定命题，写法如下：

Theorem list_app_not_comm : ¬ (forall (A : Type) (l1 l2 : list A), l1 ++ l2 = l2 ++ l1).

3. 编写证明脚本 #

Proof.
  (* 引入「列表连接满足交换律」的假设，我们需要从该假设推出矛盾 *)
  intro comm_hyp.
  (* 将全称假设实例化到我们构造的反例上：自然数类型、列表[1]和[2] *)
  specialize (comm_hyp nat [1] [2]).
  (* 化简等式两边的连接运算，得到[1;2] = [2;1]的矛盾等式 *)
  simpl in comm_hyp.
  (* 识别两个不同构造的列表项不等，直接导出矛盾完成证明 *)
  discriminate comm_hyp.
Qed.

关键说明 #

• intro：处理否定命题的标准操作，把待反驳的假设引入上下文
• specialize：将全称命题实例化为具体的个例，得到我们需要的矛盾等式
• discriminate：Coq内置的用于判断归纳类型不同构造子生成的项不等的tactic，这里两个列表的首元素构造子不同，可直接判定等式不成立

如果仅需要证明特定类型（比如自然数类型）的列表连接不满足交换律，只需要调整定理声明的全称范围即可，证明逻辑完全一致。

内容的提问来源于stack exchange，提问作者Serene M