Coq中依赖类型向量Forall的正确态射签名求解

要让@Forall D成为参数化态射，需修正签名以匹配它的类型——(D -> Prop) -> forall n : nat, t D n -> Prop。核心是要对向量长度n做全称量化，因为Forall会针对任意长度的向量生成对应的谓词。

正确的签名写法如下：

Add Parametric Morphism : (@Forall D)
    with signature (R ==> iff) ==> (forall n, Forall2 R ==> iff)
     as morph1.

完整证明代码 #

From Coq Require Import Vector Morphisms Setoid.

Parameter D : Type.
Parameter R : relation D.

Add Parametric Morphism : (@Forall D)
    with signature (R ==> iff) ==> (forall n, Forall2 R ==> iff)
     as morph1.
Proof.
  intros P Q Hpq n v1 v2 Hr.
  rewrite 2 Forall_nth_order.
  rewrite Forall2_nth_order in Hr.
  split; intros Hf i Hi; eapply Hpq; eauto.
  Unshelve.
  all: assumption.
Qed.

说明 #

• 原尝试失败的原因是签名未覆盖Forall返回值中对n的全称量化，修正后的签名用forall n, Forall2 R ==> iff匹配forall n, t D n -> Prop这一层类型。
• 证明逻辑和固定长度版本morph2基本一致，仅多了对n的引入步骤。

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