Stream: Coq users

Topic: Diagnosing slow rewrite


view this post on Zulip Brandon Moore (Mar 11 2021 at 20:30):

I ran into a slow rewrite, and have tracked it down to our code having an instance Proper (R1 ==> R2 ==> prod_relation R1 R2) pair, which makes the typeclass search for a setoid_rewrite of this form slow - exponential in the arity of P takes (testing in 8.12.0):

Lemma rewriteslow
  (A : Type)
  (P : A -> A -> A -> (A * A) -> Prop)
  (a x y : A)
  (H : x = y):
  P a a a (a, x).
Time setoid_rewrite H.

Here are imports and instances

Require Import Setoid Morphisms.
Definition prod_relation {A B} (R1 : relation A) (R2 : relation B) :
  relation (A * B) := fun x y => R1 (fst x) (fst y) /\ R2 (snd x) (snd y).
Global Instance pair_proper' {A} {R1: relation A} {B} {R2 : relation B}:
  Proper (R1 ==> R2 ==> prod_relation R1 R2) pair.
Proof. firstorder eauto. Qed.

I've started to look at Set Typeclasses Debug output. Where should I go from here?

view this post on Zulip Gaƫtan Gilbert (Mar 11 2021 at 20:46):

seems related to https://github.com/coq/coq/issues/7916
you can try Hint Mode Proper ! ! - : typeclass_instances. or variants (+ is stricter than ! is stricter than -, - is default), it makes your example go fast but I have no clue about the impact in general

view this post on Zulip Brandon Moore (Mar 17 2021 at 15:52):

That issue is interesting. The discussion there suggests that setoid_rewrite relies more than I expected on letting typeclass resolution pick what relations to use. That makes setting a mode seems a bit dangerous. I guess your ! ! _ might not get in the way if the goal usually has the form Proper (_ ==> _) _, and the ==> is enough of a head to satisfy the ! mode.

view this post on Zulip Matthieu Sozeau (Mar 19 2021 at 12:01):

! is better, but it does precludes solving Proper ? f, which can come up during resolution.


Last updated: Jan 31 2023 at 13:02 UTC