[ssr] rewrite is extremely slow when using linearly tupled equations

[anton-trunov]

Version

master (c0f74e3f967f0cc20709100091ee1a01e145f1cf)

Operating system

macOS 10.13.6

Description of the problem

From Coq Require Import ssreflect ssrbool.

Definition test (n : nat) : bool := true.

Lemma rewrite_rules8 {x} : test x ->
  test x * test x * test x * test x * test x * test x * test x * test x.
Proof. by []. Qed.

Lemma rewrite_rules24 {x} : test x ->
  test x * test x * test x * test x * test x * test x * test x * test x *
  test x * test x * test x * test x * test x * test x * test x * test x *
  test x * test x * test x * test x * test x * test x * test x * test x.
Proof. by []. Qed.

Lemma too_slow_from_8_to_24 x : test x -> test x.
Proof. move=> V.
Time rewrite (rewrite_rules8 V).
(* Finished transaction in 0.001 secs (0.001u,0.s) (successful) *)
Undo. Time rewrite (rewrite_rules24 V).
(* Finished transaction in 75.757 secs (75.315u,0.189s) (successful) *)
Abort.

rewrite slows down from instantaneous to unbearable (75 s for a trivial goal).

There is a workaround though: packing equations into nested tuples:

(* this makes life much easier *)
Lemma rewrite_rules24_6x4 {x} : test x ->
  (test x * test x * test x * test x) *
  (test x * test x * test x * test x) *
  (test x * test x * test x * test x) *
  (test x * test x * test x * test x) *
  (test x * test x * test x * test x) *
  (test x * test x * test x * test x).
Proof. by []. Qed.

(* this seems to be even better performance-wise *)
Lemma rewrite_rules24_pairs {x} : test x ->
  ((((test x * test x) * (test x * test x)) *
  ((test x * test x) * (test x * test x))) *
  (((test x * test x) * (test x * test x)) *
  ((test x * test x) * (test x * test x)))) *
  (((test x * test x) * (test x * test x)) *
  ((test x * test x) * (test x * test x))).
Proof. by []. Qed.

Lemma repack24 x : test x -> test x.
Proof. move=> V.
Time rewrite (rewrite_rules24_6x4 V).
(* Finished transaction in 0.008 secs (0.009u,0.s) (successful) *)
Undo. Time rewrite (rewrite_rules24_pairs V).
(* Finished transaction in 0.003 secs (0.003u,0.s) (successful) *)
Abort.

Is there a way of avoiding that repacking? Ideally, I'd like to simply write a linear tuple of equations.

[anton-trunov]

@gares I think this might be the performance issue we talked about at CIW-2018 (but I'm not sure yet, I'll try this workaround with nesting to check it).

[ppedrot]

This is due to the reduction algorithm used in rwprocess_rule. It uses Tacred.hnf_constr which contrarily to what its name suggests does much more than head normal form. It is an alias to whd_simpl_orelse_delta_but_fix which comes with this comment :

(* Same as [whd_simpl] but also reduces constants that do not hide a
   reducible fix, but does this reduction of constants only until it
   immediately hides a non reducible fix or a cofix *)

So it is simpl, in worse.

[maximedenes]

So it is simpl, in worse.

No, it is like whd_simpl, in worse. simpl is like strong whd_simpl IIRC.

[ppedrot]

Fair enough. Still, simpl is marginally worse than whd_simpl both in terms of code and computational complexity.

[maximedenes]

Fair enough. Still, simpl is marginally worse than whd_simpl both in terms of code and computational complexity.

No, in fact I think it is responsible for major slowdowns, because it makes whd_simpl iterate its heuristics to know if something should be reduced or not (which sometimes can be seen only after reducing). IIRC this was one of the original motivations for implementing cbn, but its refolding machinery is not less broken than simpl.