Dominik Kirst (Dec 10 2020 at 11:45): Dominik Kirst (Dec 10 2020 at 11:45):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.
Matthieu Sozeau (Dec 11 2020 at 11:46):Yes, setoid_rewriting in type is slightly different. You need to use the primitives from CMorphisms, CRelationClasses (C for computational)
Yannick Forster (Dec 11 2020 at 11:46):Even when the relation goes to Prop?
Matthieu Sozeau (Dec 11 2020 at 11:47):Hmm, right, that's probably different
Matthieu Sozeau (Dec 11 2020 at 11:49):I guess you're getting a universe error here?
Matthieu Sozeau (Dec 11 2020 at 11:49):That would point to a bug in setoid_rewrite that does not do enough universe refreshing
Yannick Forster (Dec 11 2020 at 11:49):The error message is just "no homogenous relation found to rewrite"
Yannick Forster (Dec 11 2020 at 11:49):But it might still be related to a universe bug under the hood
Yannick Forster (Dec 11 2020 at 11:52):The error also occurs in the C-variants:
Yannick Forster (Dec 11 2020 at 11:52):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
Dominik Kirst (Dec 11 2020 at 12:03):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)
Matthieu Sozeau (Dec 11 2020 at 12:06):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...
Matthieu Sozeau (Dec 11 2020 at 12:08):Can you report it on Coq's issue tracker ?
Dominik Kirst (Dec 11 2020 at 16:42):done :peace_sign:
https://github.com/coq/coq/issues/13618
Last updated: Sep 30 2023 at 07:01 UTC