何もしてないのに動かなくなった

quicksort.v

Section QSort.
Require Import Arith List Program Bool Recdef.

Variable A : Type.
Variable compare : A -> A -> comparison.

Definition partition (p : A -> bool) l :=
  fold_left (fun (acc : list A * list A) x =>
    let (ltrue, lfalse) := acc in
    if p x then (x :: ltrue, lfalse)
    else (ltrue, x :: lfalse)) l ([], []).

Parameter partition_length_true : forall (p : A -> bool) (l ltrue lfalse : list A),
  partition p l = (ltrue, lfalse) -> length ltrue <= length l.
Parameter partition_length_false : forall (p : A -> bool) (l ltrue lfalse : list A),
  partition p l = (ltrue, lfalse) -> length lfalse <= length l.

Function quicksort (aux l : list A) {measure length l} :=
  match l with
  | [] => aux
  | x :: xs =>
      let (lesser, greater) := partition (fun x' =>
        match compare x' x with
        | Eq => true
        | Lt => true
        | Gt => false
        end) xs in
      quicksort (x :: quicksort aux greater) lesser
  end.
Proof.
  intros.
  apply le_n_S.
  eapply partition_length_false.
  eauto.

  intros.
  apply le_n_S.
  eapply partition_length_true.
  eauto.
Qed.
End QSort.