Stream: Coq users

Topic: RelationPairs rewriting really slow


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

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

view this post on Zulip Jason Gross (Dec 31 2022 at 05:10):

@Andrew Appel add

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.

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

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

view this post on Zulip Andrew Appel (Jan 03 2023 at 18:50):

I have reported Coq Issue #17060.


Last updated: Jun 24 2024 at 14:01 UTC