The Coq mailing list

["Micky Latowicki" <biosap AT gmail.com>]

Hi all.

I was a bit surprised to see that the implementation of List.rev is quadratic-time. Below is a linear-time (and tail-recursive) implementation of rev, along with a proof that the two implementations are equivalent.

My measurements show a 300-550 times speedup for a 1000-item list. This might be significant for extracted programs, if nothing else.

So, I suggest to replace the implementation in the standard library with the one below. My questions are: 
1. is there any reason not to do this
 and 
2. what can I do to bring about this change? Is it just a matter of getting the sources, changing the implementation, and then adapting proofs as needed so that none of the theorems in the standard library is lost?

Cheers.

(*--------- start of implementation and proof ----------*)

Require Import List.
Definition snoc (A:Set) (l:list A) (a:A) := a::l.
Implicit Arguments snoc [A].
Definition reverse (A:Set) (l:list A) := fold_left (snoc (A:=A)) l nil.
Implicit Arguments reverse [A].

Theorem rev_eq_reverse: forall (A:Set) (l:list A), rev l = reverse l.
Proof.
    intro A.
    unfold reverse in |- *.
    set (fold_left_snoc := fold_left (snoc (A:=A))) in |- *.
    assert
     (rev_eq_fold_left_snoc :
      forall l s : list A, rev l ++ s = fold_left_snoc l s).
     induction l; simpl in |- *.
      trivial.
      intro s.
    rewrite app_ass.
    simpl app in |- *.
    unfold snoc in |- *.
    apply IHl.
     intros.
       rewrite <- (rev_eq_fold_left_snoc l nil).
       apply app_nil_end.
Qed.