List.rev has quadratic complexity

[MathisBD]

Is your feature request related to a problem?

The definition of List.rev in the standard library is quadratic :

Fixpoint rev (l:list A) : list A :=
    match l with
      | [] => []
      | x :: l' => rev l' ++ [x]
    end.

This is very bad for such a common function.

Proposed solution

It should instead use an accumulator to obtain linear complexity :

Fixpoint rev (l : list A) :=
  let fix aux l acc :=
    match l with
    | [] => acc
    | x :: l => aux l (x :: acc)
    end
  in aux l []

Alternative solutions

No response

Additional context

No response

[ppedrot]

Duplicate of coq/stdlib#10