在Coq中证明列表上点态关系传递性的问题

Agda中的实现 #

在Agda中，若关系R具有传递性，可直接通过依赖模式匹配证明列表上的点态关系同样满足传递性，代码如下：

open import Data.List

Rel : Set → Set₁
Rel A = A → A → Set

private
    variable
        A : Set
        R : A → A → Set 

data Pointwise (R : Rel A) : Rel (List A) where
    p-nil : Pointwise R [] []
    p-cons : ∀ {x y xs ys} → R x y → Pointwise R xs ys → Pointwise R (x ∷ xs) (y ∷ ys) 

Transitive : Rel A → Set
Transitive R = ∀ {x y z} → R x y → R y z → R x z  

TransitivePointwise : Transitive R → Transitive (Pointwise R)
TransitivePointwise t p-nil p-nil = p-nil
TransitivePointwise t (p-cons Rxy ps) (p-cons Ryz qs) = p-cons (t Rxy Ryz) (TransitivePointwise t ps qs) 

Coq中的实现困境 #

尝试在Coq中实现相同功能时，会遇到两个问题：

1. 无法同时对H0 : pointwise R x y和H1 : pointwise R y z进行递归证明，直接用refine结合fixpoint会提示格式不合法；
2. 执行destruct H0, H1时，Coq会生成4种情况，而Agda仅生成2种。

Coq的初始尝试代码：

Inductive pointwise {A} (R : A -> A -> Prop) : list A -> list A -> Prop := 
| p_nil : pointwise R nil nil
| p_cons : forall {x y} {xs ys}, R x y -> pointwise R xs ys -> pointwise R (x :: xs) (y :: ys).

Theorem transitive_pointwise : forall {A} R, transitive R -> transitive (pointwise R). 
Proof.
    unfold transitive.
    intros.
    induction H0.
    - assumption.
    -
Qed.

问题1：完成Coq中的传递性证明 #

要解决递归问题，需同时对两个点态关系假设进行结构分析，可通过同时解构两者并排除矛盾情况，或归纳结合解构的方式实现，以下是完整证明：

方式1：同时解构+排除矛盾

Theorem transitive_pointwise : forall {A} R, transitive R -> transitive (pointwise R).
Proof.
  unfold transitive.
  intros A R trans_r x y z p_xy p_yz.
  (* 同时解构两个点态关系假设 *)
  destruct p_xy as [ | x y xs ys r_xy p_xs_ys ]; destruct p_yz as [ | y' z ys' zs r_yz p_ys_zs ].
  - (* 两种都是空列表的情况 *)
    exact p_nil.
  - (* p_xy是空列表，p_yz是cons结构：此时y=nil，但p_yz的左边是y'::ys'=nil，矛盾 *)
    discriminate.
  - (* p_xy是cons结构，p_yz是空列表：此时y=x::xs，但p_yz的左边是nil=x::xs，矛盾 *)
    discriminate.
  - (* 两种都是cons结构 *)
    apply p_cons.
    + (* 利用R的传递性证明头元素的关系 *)
      apply trans_r; assumption.
    + (* 递归证明尾列表的点态关系传递性 *)
      apply transitive_pointwise; assumption.
Qed.

方式2：归纳+解构

Theorem transitive_pointwise : forall {A} R, transitive R -> transitive (pointwise R).
Proof.
  unfold transitive.
  intros A R trans_r x y z p_xy p_yz.
  induction p_xy; destruct p_yz.
  - exact p_nil.
  - inversion p_yz. (* 空列表无法匹配cons结构，直接排除 *)
  - inversion p_xy. (* cons结构无法匹配空列表，直接排除 *)
  - apply p_cons; [apply trans_r; assumption | apply IHp_xy; assumption].
Qed.

问题2：为何Coq生成4种情况而Agda仅2种 #

核心差异在于依赖模式匹配的能力：

• Agda的模式匹配是完全依赖类型的，当匹配Pointwise R xs ys的p-nil构造子时，会自动推导出xs = []且ys = []，此时另一个参数Pointwise R ys zs的类型变为Pointwise R [] zs，而该类型只有p-nil一种可能，因此Agda会自动排除其他不可能的情况，仅保留有效模式。
• Coq的destruct命令默认仅枚举归纳类型的所有构造子组合，不会主动利用上下文的类型约束（比如ys的具体值）过滤不可能的情况，因此会生成所有4种构造子组合（空+空、空+cons、cons+空、cons+cons），其中后两种在上下文约束下是矛盾的，需要手动用discriminate或inversion排除。

内容的提问来源于stack exchange，提问作者Benjamin Flin