Coq中pointwise_relation下重写失败，请求态射配置排查

你尝试在Forall (P s) l中对s执行setoid重写失败，核心原因是Coq无法自动关联EqSt s1 s2与P s1和P s2之间的点wise谓词等价关系，而Forall的态射依赖这种点wise等价来完成重写。

问题代码回顾 #

From Coq Require Import List Streams Setoid Morphisms.

Parameter T A : Type.
Parameter P : Stream T -> A -> Prop.

Add Parametric Morphism : P
    with signature @EqSt T ==> @eq A ==> iff
      as P_morph.
Admitted.

Add Parametric Morphism : (@Forall A)
    with signature pointwise_relation A iff ==> (@eq (list A)) ==> iff
      as Forall_morph.
Admitted.

Example problematic :
  forall s1 s2 l,
    EqSt s2 s1 ->
    Forall (P s1) l ->
    Forall (P s2) l.
Proof.
  intros * Heq Hf.
  Fail setoid_rewrite Heq.
Abort.

关键问题点 #

你已经注册了两个态射：

1. P的态射：当s1 ≡ s2（EqSt等价）且a = b时，P s1 a ↔ P s2 b。
2. Forall的态射：当两个谓词Q1和Q2满足点wise等价（即forall a, Q1 a ↔ Q2 a）且列表l相等时，Forall Q1 l ↔ Forall Q2 l。

但setoid_rewrite需要的是：从EqSt s1 s2直接推导出P s1和P s2的点wise等价关系——这一步的推导没有被注册为自动可用的态射，所以Coq无法完成重写链。

解决方法 #

添加一个新的参数化态射，将EqSt等价关联到P生成的谓词的点wise等价：

From Coq Require Import List Streams Setoid Morphisms.

Parameter T A : Type.
Parameter P : Stream T -> A -> Prop.

Add Parametric Morphism : P
    with signature @EqSt T ==> @eq A ==> iff
      as P_morph.
Admitted.

Add Parametric Morphism : (@Forall A)
    with signature pointwise_relation A iff ==> (@eq (list A)) ==> iff
      as Forall_morph.
Admitted.

(* 新增态射：将EqSt等价转换为P生成谓词的点wise等价 *)
Add Parametric Morphism : P
    with signature @EqSt T ==> pointwise_relation A iff
      as P_pointwise_morph.
Proof.
  intros s1 s2 Heq a.
  apply P_morph; auto.  (* 利用已有的P_morph实例 *)
  reflexivity.         (* a与自身相等 *)
Qed.

Example fixed_problem :
  forall s1 s2 l,
    EqSt s2 s1 ->
    Forall (P s1) l ->
    Forall (P s2) l.
Proof.
  intros * Heq Hf.
  setoid_rewrite Heq.  (* 现在可以成功重写 *)
  exact Hf.
Qed.

替代手动推导（无需新增态射） #

如果不想新增态射，也可以在证明中手动调用Forall的态射完成推导：

Example fixed_problem_manual :
  forall s1 s2 l,
    EqSt s2 s1 ->
    Forall (P s1) l ->
    Forall (P s2) l.
Proof.
  intros * Heq Hf.
  apply Forall_morph with (l := l); try exact Hf.
  - intros a; apply P_morph; auto; reflexivity.
  - reflexivity.
Qed.

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