# How to implement setoid\_rewrite for "partial equivalence-relation" in Coq?

**URL:** <https://discourse.rocq-prover.org/t/how-to-implement-setoid-rewrite-for-partial-equivalence-relation-in-coq/2565>\
**Category:** Using Rocq\
**Created:** [March 14, 2025, 3:30am UTC](https://discourse.rocq-prover.org/t/how-to-implement-setoid-rewrite-for-partial-equivalence-relation-in-coq/2565 "2025-03-14T03:30:04Z")\
**Posts on this page:** 2\
**Page:** 1

<div class="post-metadata">

**Author:** ![Sam-Ni](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/sam-ni/32/1071_2.png) [@Sam-Ni](https://discourse.rocq-prover.org/u/Sam-Ni)\
**Post date:** [March 14, 2025, 3:30am UTC](https://discourse.rocq-prover.org/t/how-to-implement-setoid-rewrite-for-partial-equivalence-relation-in-coq/2565/1 "2025-03-14T03:30:04Z")

</div>

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.

```auto
(*
  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.

---

<div class="post-metadata">

**Author:** ![silene](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/silene/32/485_2.png) [@silene](https://discourse.rocq-prover.org/u/silene)\
**Post date:** [March 14, 2025, 2:39pm UTC](https://discourse.rocq-prover.org/t/how-to-implement-setoid-rewrite-for-partial-equivalence-relation-in-coq/2565/2 "2025-03-14T14:39:16Z")

</div>

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

```coq
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.

```