List.rev is unexpectedly quadratic

[charguer]

This is probably known to a number of Coq developers, but I discovered only yesterday, after 15 years of using Coq, that List.rev is implemented with quadratic complexity. That could explain numerous of the performance bottleneck that I, and others, have encountered.

I then saw that Coq.Lists.List also defines a rev' function, with the proper tail-rec definition. But I don't recall seeing it used in any Coq script that I have looked at. I suggest to better advertise the issue with the definition of rev. At the very least, I guess there should be a comment above the definition of rev, and possibly also at the top of the file.

Another possibility for tracking down problematic usages would be to develop a profiler version for coqc , that could, among other things, measure the length of arguments of rev and report a warning whenever the length exceeds a couple dozen elements. Such a profiler could be exploited by users who want their scripts to run faster, suggesting hints for improvements.

To see how bad the quadratic behavior gets in practice, I ran the following benchmark. Even for short lists, the computation time is significant.

Set Implicit Arguments.
From Coq Require Import List.

Fixpoint make A (n:nat) (v:A) : list A :=
   match n with
   | 0 => nil
   | S n' => v :: make n' v
   end.

Set Implicit Arguments.
From Coq Require Import List.

Fixpoint make A (n:nat) (v:A) : list A :=
   match n with
   | 0 => nil
   | S n' => v :: make n' v
   end.

Lemma test : forall (v w:nat),
      last (rev (make 300 v)) w = v
  /\  last (rev (make 500 v)) w = v
  /\  last (rev (make 500 v)) w = v
  /\  last (rev (make 1500 v)) w = v
  /\  last (rev (make 5000 v)) w = v
  /\  last (rev' (make 5000 v)) w = v.
Proof. 
  intros. split;[|split;[|split;[|split;[|split]]]].
  time simpl. auto.  (* >1 second for 300 elements *)
  time simpl. auto.  (* 5 seconds for 500 elements *)
  time reflexivity. (* 0.1 seconds for 500 elements *)
  time reflexivity. (* >1 seconds for 1500 elements *)
  time reflexivity. (* 17 seconds for 5000 elements *) 
  time reflexivity. (* 0.01 seconds for 5000 elements with the tail rec version *) 
Abort.

[maximedenes]

Interesting, I also didn't know that (math-comp has a rev function that is documented as linear-time).

I'm surprised that your suggestion is to document the problem rather than fixing it. Can you say why?

[JasonGross]

I'm surprised that your suggestion is to document the problem rather than fixing it. Can you say why?

I'm guessing that making proofs about rev compatible across versions would be a bit of a pain. But that doesn't mean we shouldn't do it.

But I don't recall seeing it used in any Coq script that I have looked at.

I discovered this performance issue a while back (I think around the time I noticed math-comp redefining rev), and since have been using rev_append instead. (I wasn't aware of rev' though.)

[charguer]

I'm surprised that your suggestion is to document the problem rather than fixing it. Can you say why?

Replacing the definition of rev with rev' would probably break many scripts. It's not just the behavior of simpl that would be affected, but also that of reflexivity on goals involving rev. Too see the extend of the issue:

From Coq Require Import List.

Lemma test : forall (x:nat) l,
  rev (x::l) = rev l ++ (x::nil).
Proof. intros. reflexivity. Qed.  

Lemma test' : forall (x:nat) l,
  rev' (x::l) = rev' l ++ (x::nil).
Proof. intros. Fail reflexivity. Abort.

I suspect that numerous user proofs implicitly rely on that conversion. (You might want to evaluate how many user contrib would be broken by a change to rev.)

Since I'm not personally relying on Coq's standard library List module, I don't want to be the one blamed for encouraging a backward-incompatible changes.