How to implement setoid_rewrite for "partial equivalence-relation" in Coq?

Using Rocq
1

Motivation: I defined a binary relation R (A → A → Prop) in Coq and try to implement setoid_rewrite for it (rewrite on R, not on the Coq equality eq).

Expectation: For example, if (P a_1) and (R a_1 a_2) holds, by using setoid_rewrite we can get (P a_2) holds.

Problem and Details: I have proved the symmetry and transitivity of R but failed to prove the reflexivity
since (R a a) holds only when (ok a) holds where ‘ok’ is a predicate on a.

To be more specific, the following lemma can be proved.

(*
  This lemma can be proved. 
  However, it does not match the pattern of Reflexive in Coq.Equivalence.
*)
Lemma refl_R : forall (a : A),
  ok a -> R a a.
Proof.
  ...
Qed.

So I wonder if it is possible to implement setoid_rewrite for such a relation R in Coq.

2

setoid_rewrite does not care about reflexivity or symmetry or transitivity. The only thing that matters is that, if two elements are related by R, then their images by P are related by iff, which is a statement denoted by Proper (R ==> iff) P.

Require Import Morphisms.

Parameter A : Type.
Parameter R : A -> A -> Prop.
Parameter P : A -> Prop.

Lemma foo : Proper (R ==> iff) P.
Proof. Admitted.
Existing Instance foo.

Lemma L a1 a2 : P a2 -> R a1 a2 -> P a1.
Proof.
intros H1 H2.
now rewrite H2.
Qed.
2 Likes