Stream: Coq users

Topic: Issue with setoid rewriting on Type


view this post on Zulip 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.

view this post on Zulip Dominik Kirst (Dec 10 2020 at 12:16):

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.

view this post on Zulip 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)

view this post on Zulip Yannick Forster (Dec 11 2020 at 11:46):

Even when the relation goes to Prop?

view this post on Zulip Matthieu Sozeau (Dec 11 2020 at 11:47):

Hmm, right, that's probably different

view this post on Zulip Matthieu Sozeau (Dec 11 2020 at 11:49):

I guess you're getting a universe error here?

view this post on Zulip Matthieu Sozeau (Dec 11 2020 at 11:49):

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

view this post on Zulip Yannick Forster (Dec 11 2020 at 11:49):

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

view this post on Zulip Yannick Forster (Dec 11 2020 at 11:49):

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

view this post on Zulip Yannick Forster (Dec 11 2020 at 11:52):

The error also occurs in the C-variants:

view this post on Zulip 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.

view this post on Zulip Matthieu Sozeau (Dec 11 2020 at 11:58):

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

view this post on Zulip 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)

view this post on Zulip 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...

view this post on Zulip Matthieu Sozeau (Dec 11 2020 at 12:08):

Can you report it on Coq's issue tracker ?

view this post on Zulip Dominik Kirst (Dec 11 2020 at 16:42):

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


Last updated: Jan 29 2023 at 06:02 UTC