Dear Coq users,
I have a parametric relation
myeq that I would like to rewrite under the predicate
P whenever both are used with the same parameter. It works well if I declare the appropriate morphism:
From Coq Require Import Setoid Morphisms. Parameter A B : Type. Parameter myeq : A -> relation B. Add Parametric Relation (a : A) : B (myeq a) as myeq_rel. Parameter P : A -> B -> Prop. Add Parametric Morphism (a : A) : (P a) with signature (myeq a) ==> iff as P_morphism. Admitted. Lemma test1 b1 b2 : (forall a, myeq a b1 b2) -> exists a, P a b1. Proof. intro. setoid_rewrite H. (* OK *) Abort.
However it stops working when I try to apply a function, even registered as a morphism for
Parameter Op : B -> B. Add Parametric Morphism (a : A) : Op with signature (myeq a) ==> (myeq a) as op_morphism. Admitted. Lemma test2 b1 b2 : (forall a, myeq a b1 b2) -> exists a, P a (Op b1). Proof. intro. setoid_rewrite H. (* not OK, why? *) Abort.
Typeclasses debug information mention some early unification failure, but it leaves me puzzled.
Did I forget to declare something?