coqrewriting

Coq: rewriting under a pointwise_relation

I want to rewrite s in the term Forall (P s) l but it fails with my current instance declarations. Did I miss something with the morphisms?

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.
Solution

  • P's signature should also use pointwise_relation.

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