在Coq中证明merge_l_reduce命题：有序归并列表的归纳证明难题

定义与命题 #

首先是merge关系的归纳定义，描述两个列表的交错归并（保持各自内部元素顺序）：

Inductive merge {X:Type} : list X -> list X -> list X -> Prop :=
  | merge0 : merge [] [] []
  | merge1 n l1 l2 l (H: merge l1 l2 l) : merge (n::l1) l2 (n::l)
  | merge2 n l1 l2 l (H: merge l1 l2 l) : merge l1 (n::l2) (n::l).

基于此提出的待证命题：

Proposition merge_l_reduce: forall (X: Type) (n: X) l1 l2 l,
  merge (n::l1) l2 (n::l) -> merge l1 l2 l.

尝试的证明困境 #

使用inversion策略拆分H的构造后，merge1分支可直接通过子目标推导，但merge2分支卡住：此时inversion会得到l2 = n::l2'，且子目标为merge (n::l1) l2' l，但需要证明的结论是merge l1 (n::l2') l，两者结构无法直接关联。

可证性与完整证明 #

该命题可证，但需要先证明一个辅助引理，用于将第一个列表头部的元素“转移”到第二个列表头部，同时保持归并关系：

辅助引理：swap_merge #

Lemma swap_merge : forall X a l1 l2 l,
  merge (a::l1) l2 l -> merge l1 (a::l2) l.
Proof.
intros X a l1 l2 l H.
induction H.
- (* merge0 分支：不可能触发，因为左列表为非空的 a::l1 *)
  inversion H.
- (* merge1 分支：归并结果的头部来自第一个列表 *)
  inversion H as [= <- <- <-].
  apply merge1 with (n := a).
  apply IHmerge.
- (* merge2 分支：归并结果的头部来自第二个列表 *)
  inversion H as [= <- <- <-].
  apply merge2 with (n := n).
  apply IHmerge.
Qed.

原命题的完整证明 #

Proof.
intros X n l1 l2 l H.
inversion H as [
  | m l1' l2' l' Q eq_n_m eq_l1 eq_l2 eq_l
  | m l1' l2' l' Q eq_n_m eq_l1 eq_l2 eq_l
].
- (* merge0 分支：不可能触发 *)
  contradiction.
- (* merge1 分支：直接应用子目标 Q *)
  rewrite <- eq_l1, <- eq_l in Q.
  apply Q.
- (* merge2 分支：借助辅助引理转换子目标 *)
  rewrite eq_n_m in eq_l2, eq_l.
  rewrite <- eq_l1 in Q.
  rewrite <- eq_l in Q.
  apply swap_merge in Q.
  apply Q.
Qed.

证明思路说明 #

1. 辅助引理swap_merge：通过对归并关系H的结构归纳，证明若a::l1与l2可归并为l，则l1与a::l2也可归并为l——本质是将第一个列表的头部元素“移到”第二个列表头部，不改变交错归并的结果。
2. 原命题证明：
   • 对H做inversion拆分构造分支；
   • merge1分支直接利用子目标完成证明；
   • merge2分支通过等式替换将子目标转换为swap_merge的输入，借助引理得到所需结论。

内容的提问来源于stack exchange，提问作者Henry Hsuan-Ju Chen