Require Import Coq.Sorting.Permutation. slows down rewrite_strat > 10x

[samuelgruetter]

This is a followup on coq/coq#15596, but this time focusing on Require Import, because the fix for coq/coq#15596 only addressed Require.

Require Import Coq.Lists.List. Import ListNotations.
Require Import Coq.Arith.PeanoNat.

(*
Require Import Coq.Sorting.Permutation.
*)

Local Hint Rewrite Nat.add_0_r : mydb.

Goal forall
    (l : list nat)
    (v v0 mscratch: nat)
    (maprep: Type)
    (m: maprep)
    (Array : (nat -> nat -> maprep -> Prop) ->
               nat -> list nat -> nat -> maprep -> Prop)
    (Scalar : nat -> nat -> maprep -> Prop)
    (atAddr : nat -> (nat -> maprep -> Prop) -> maprep -> Prop)
    (A : atAddr mscratch
                (Array Scalar 4
                       ([v0] ++ [v + 0] ++ l)) m),
      False.
Proof.
  intros.
  Time rewrite_strat (topdown (hints mydb)) in A.

Uncommenting the Require Import Coq.Sorting.Permutation. slows down rewrite_strat by > 10x, to ca 3 seconds.

A workaround is

Global Remove Hints Permutation.Permutation_cons Permutation.Permutation_app' :
  typeclass_instances.

However, if I try to minimize the slowness by replacing Require Import Coq.Sorting.Permutation. with just the signatures of the two trouble-making instances, there's no slowdown:

Require Import Coq.Classes.Morphisms.

Definition Permutation{A: Type}: list A -> list A -> Prop. Admitted.

Local Instance Permutation_cons A :
 Proper (Logic.eq ==> @Permutation A ==> @Permutation A) (@cons A).
Admitted.

Local Instance Permutation_app' A :
 Proper (@Permutation A ==> @Permutation A ==> @Permutation A) (@app A).
Admitted.

There seems to be some interesting performance issue in the interaction between rewrite_strat and typeclass search looking for morphisms.

[JasonGross]

However, if I try to minimize the slowness by replacing Require Import Coq.Sorting.Permutation. with just the signatures of the two trouble-making instances, there's no slowdown:

Can you add Set Typeclasses Debug. and pipe the output to a file in the three different configurations, and upload the files here? I think a 3-way diff between the typeclass logs would illuminate what's going on here.

[samuelgruetter]

The above example is completely standalone, so anyone can consider it as a compressed version (with coq being the uncompress tool) of the logs you're asking for 😉

[ppedrot]

It's not surprising that declaring those two instances are not enough. The Permutation file also defines many other instances that might interact with the proof search.

[SkySkimmer]

It seems fast if you Set Typeclasses Filtered Unification.
Anyone know what the downsides of this option are?

[ppedrot]

It breaks everything because the implementation of this flag is crazy. It doesn't perform matching up-to-evars. Please deprecate that option and replace it with something sensible.

[SkySkimmer]

Do we have some bugs or issues about that somewhere?

[Blaisorblade]

Do we have some bugs or issues about that somewhere?

coq/coq#15752

However, if I try to minimize the slowness by replacing Require Import Coq.Sorting.Permutation. with just the signatures of the two trouble-making instances, there's no slowdown:

To minimize the slowdown, you might need to start adding e.g. Reflexive Permutation (or check the typeclass log for such things).

• Using setoid rewriting for Nat.add_0_r of course doesn't make much sense — so maybe rewrite_strat has a bug here?

• Until Coq 8.15, setoid rewriting sometimes loops over reflexive relations to find the one to use ( Fix bug #7916, allowing Reflexive to have mode ! ! coq#13969).