Hi all, I ran into an issue with setoid rewriting for equivalences on Type, see below for a minimal example.

If I just assume an equivalence respecting sum types, rewriting below a sum fails although it can be easily be done by hand. It seems this can be fixed by explicitly aliasing sum with full type annotation and annotating occurring data types as well.

Is this a known issue with a better fix than what I tried? And is setoid rewriting on Type in general known to cause problems?

```
Require Import Morphisms Setoid.
Section Equiv.
Variable equiv : Type -> Type -> Prop.
Hypothesis equiv_equiv : Equivalence equiv.
Hypothesis equiv_sum : Proper (equiv ==> equiv ==> equiv) sum.
Goal forall X, equiv X bool -> equiv (X + X) X.
Proof.
intros X H. Fail rewrite H.
eapply Equivalence_Transitive; try apply equiv_sum; try apply H; try apply Equivalence_Reflexive.
Abort.
Definition sum' : Type -> Type -> Type := sum.
Hypothesis equiv_sum' : Proper (equiv ==> equiv ==> equiv) sum'.
Goal forall X, equiv X (bool : Type) -> equiv (sum' X X) X.
Proof.
intros X H. rewrite H.
Abort.
End Equiv.
```

In case this helps, I'd guess the issue is connected to the universe levels as the annotations probably just fix everything to the same level. It also works if everything is placed in Set but this is too specific in my use case.

Yes, setoid_rewriting in type is slightly different. You need to use the primitives from CMorphisms, CRelationClasses (C for computational)

Even when the relation goes to `Prop`

?

Hmm, right, that's probably different

I guess you're getting a universe error here?

That would point to a bug in setoid_rewrite that does not do enough universe refreshing

The error message is just "no homogenous relation found to rewrite"

But it might still be related to a universe bug under the hood

The error also occurs in the `C`

-variants:

```
Require Import Setoid CMorphisms CRelationClasses.
Section Equiv.
Variable equiv : Type -> Type -> Type.
Hypothesis equiv_equiv : Equivalence equiv.
Hypothesis equiv_sum : Proper (equiv ==> equiv ==> equiv) sum.
Goal forall X, equiv X bool -> equiv (X + X) X.
Proof.
intros X H. Fail setoid_rewrite H.
(* The command has indeed failed with message: *)
(* Cannot find an homogeneous relation to rewrite. *)
Abort.
```

Indeed, that's a bug in setoid_rewrite. It mistakenly tries to compare the types of X and bool, which might differ by cumulativity. Should be easy to fix. Maybe there's a workaround, let me try

For the record, I tried the CMorphisms variant before and it indeed didn't change the outcome.

(edit: I just now realised that Yannick already postet this a few messages before)

```
Require Import Morphisms Setoid.
Section Equiv.
Universe u.
Variable equiv : Type@{u} -> Type@{u} -> Prop.
Hypothesis equiv_equiv : Equivalence equiv.
Hypothesis equiv_sum : Proper (equiv ==> equiv ==> equiv) sum.
Notation equiv_rel x y := (equiv (x : Type@{u}) (y : Type@{u})).
(* (at level 9, x, y at next level). *)
Goal forall X, equiv_rel X bool -> equiv_rel (X + X) X.
Proof.
intros X H. rewrite H.
eapply Equivalence_Transitive; try apply equiv_sum; try apply H; try apply Equivalence_Reflexive.
Abort.
```

This is annoying as you cannot make the printing hide the hack...

Can you report it on Coq's issue tracker ?

done :peace_sign:

https://github.com/coq/coq/issues/13618

Last updated: Sep 30 2023 at 07:01 UTC