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.
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.
@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.
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
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?
I have reported Coq Issue #17060.
Last updated: Oct 13 2024 at 01:02 UTC