## Stream: Coq users

### Topic: RelationPairs rewriting really slow

#### Andrew Appel (Dec 30 2022 at 16:24):

The Coq standard library has a nice-looking feature, RelationPairs, for doing setoid rewrites over pairs. I tried it out, and it's painfully slow. The demonstration is below; look for the lines that say `Time rewrite`.
Am I doing something wrong, or is this feature basically unusable? (in Coq 8.16)

``````Require Import Coq.Relations.Relations Coq.Classes.Morphisms Coq.Classes.RelationPairs Coq.Classes.RelationClasses.
Require Import Coq.Lists.List.

Parameter type: Type.
Parameter ftype: type -> Type.
Parameter feqv: forall {t}, relation (ftype t).
Axiom feqv_refl: forall {t}, reflexive (ftype t) feqv.
Axiom feqv_sym: forall {t}, symmetric (ftype t) feqv.
Axiom feqv_trans: forall {t}, transitive (ftype t) feqv.

Add Parametric Relation {t: type}: (ftype t) (@feqv t)
reflexivity proved by feqv_refl
symmetry proved by feqv_sym
transitivity proved by feqv_trans
as feqv_rel.

Definition list_eqv {t: Type} : relation t ->  relation (list t) :=
@Forall2 t t.

Lemma list_eqv_refl: forall {T} {rel: relation T} {EQrel: Equivalence rel},
reflexive (list T) (list_eqv rel).
Proof.
intros.
red.
induction x; constructor; auto. reflexivity.
Qed.

Lemma list_eqv_sym: forall {T} {rel: relation T} {EQrel: Equivalence rel},
symmetric (list T) (list_eqv rel).
Proof.
intros.
red.
induction x; destruct y; intros; inversion H; clear H; subst;  constructor; auto.
symmetry; auto.
apply IHx; auto.
Qed.

Lemma list_eqv_trans: forall {T} {rel: relation T} {EQrel: Equivalence rel},
transitive (list T) (list_eqv rel).
Proof.
intros.
red.
induction x; destruct y,z; intros; inversion H; inversion H0; clear H H0; subst;  constructor; auto.
rewrite H4; auto.
eapply IHx; eauto.
Qed.

Add Parametric Relation {T: Type} (rel: relation T) {EQrel: Equivalence rel}: (list T) (list_eqv rel)
reflexivity proved by list_eqv_refl
symmetry proved by list_eqv_sym
transitivity proved by list_eqv_trans
as list_eqv_rel.

Lemma test_list_eqv: forall t (a b c: list (ftype t)),
list_eqv feqv a b ->  list_eqv feqv b c -> list_eqv feqv c a.
Proof.
intros.
rewrite H. rewrite H0. reflexivity.
Qed.

Lemma test_pair1: forall t (a a': ftype t) (b b': ftype t),
feqv a a' -> feqv b b' ->
(feqv * feqv)%signature (a,b) (a',b').
Proof.
intros.
Time apply pair_compat; auto.  (* 0.0 seconds *)
Qed.

Lemma test_pair2: forall t (a a': ftype t) (b b': ftype t),
feqv a a' -> feqv b b' ->
(feqv * feqv)%signature (a,b) (a',b').
Proof.
intros.
Time rewrite H.  (*  11 or 12 seconds *)
Time rewrite H0. (* 2 or 12  seconds *)
reflexivity.
Qed.

Lemma test_pairlist1: forall t (a a': ftype t) (b b': list (ftype t)),
feqv a a' -> list_eqv feqv b b' ->
(feqv * list_eqv feqv)%signature (a,b) (a',b').
Proof.
intros.
apply pair_compat; auto. (* 0.0 seconds *)
Qed.

Lemma test_pairlist: forall t (a a': ftype t) (b b': list (ftype t)),
feqv a a' -> list_eqv feqv b b' ->
(feqv * list_eqv feqv)%signature (a,b) (a',b').
Proof.
intros.
Time rewrite H0.  (* 2 to 5 seconds *)
Time rewrite H.  (* 15 seconds *)
reflexivity.
Qed.
``````

#### Stefan Haan (Dec 30 2022 at 23:52):

I recently had a similar problem recently where rewrite would not terminate. You can try to understand what's going on by setting the flag

``````Set Typeclasses Debug Verbosity 1.
``````

#### Jason Gross (Dec 31 2022 at 05:10):

``````Global Instance: forall A B RA1 RA2 RB1 RB2 (RA : relation A) (RB : relation B),
Proper (RA1 ==> RA2 ==> Basics.flip Basics.impl) RA
-> Proper (RB1 ==> RB2 ==> Basics.flip Basics.impl) RB
-> Proper (RA1 * RB1 ==> RA2 * RB2 ==> Basics.flip Basics.impl) (RA * RB)%signature.
Proof. cbv; intuition eauto. Qed.
``````

and everything is basically instantaneous.

#### Jason Gross (Dec 31 2022 at 05:11):

You may need to add a variant with `Basics.impl` instead of `Basics.flip Basics.impl` if you want to rewrite in hypotheses and/or have `rewrite <-` work as well as `rewrite`

#### Andrew Appel (Dec 31 2022 at 18:06):

The unflipped variant is only needed for rewriting in hypotheses, not for rewrite <-. But in any case, it seems to me a bug that these two instances are not already in the RelationPairs library, as their omission makes rewriting in pairs pretty useless. Shall someone file an issue report or a pull request?

#### Andrew Appel (Jan 03 2023 at 18:50):

I have reported Coq Issue #17060.

Last updated: Jun 24 2024 at 14:01 UTC