Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Setoid rewriting on Type #13618

Closed
dominik-kirst opened this issue Dec 11, 2020 · 0 comments · Fixed by #14138
Closed

Setoid rewriting on Type #13618

dominik-kirst opened this issue Dec 11, 2020 · 0 comments · Fixed by #14138
Labels
kind: bug An error, flaw, fault or unintended behaviour. part: rewriting tactics The rewrite, autorewrite, rewrite_strat, and setoid_rewrite tactics.
Milestone

Comments

@dominik-kirst
Copy link

Description of the problem

I ran into an issue with setoid rewriting for equivalences on Type, see below for a minimal example. There is a related Zulip topic.

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.

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.
    (* The command has indeed failed with message: *)
    (* Cannot find an homogeneous relation to rewrite. *)
    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.

Using CMorphism produces the same error and @mattam82 posted another not fully satisfactory workaround on Zulip.

Coq Version

Coq 8.12.0

@Alizter Alizter added kind: bug An error, flaw, fault or unintended behaviour. part: rewriting tactics The rewrite, autorewrite, rewrite_strat, and setoid_rewrite tactics. labels Sep 29, 2021
coqbot-app bot added a commit that referenced this issue Jan 12, 2022
…eneous relations

Reviewed-by: SkySkimmer
Co-authored-by: SkySkimmer <SkySkimmer@users.noreply.github.com>
@Zimmi48 Zimmi48 added this to the 8.16+rc1 milestone Jul 4, 2022
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
kind: bug An error, flaw, fault or unintended behaviour. part: rewriting tactics The rewrite, autorewrite, rewrite_strat, and setoid_rewrite tactics.
Projects
None yet
Development

Successfully merging a pull request may close this issue.

3 participants