qsort.v

gistfile1.txt

Require Import List Arith.
Require Import Recdef.

Lemma lemma1:
  forall (a : Type) (f : a -> bool) (n : a) (xs : list a),
    length (filter f (n :: xs)) = if f n then 1 + length (filter f xs)
                                         else length (filter f xs).
Proof.
  intros a f n xs.
  simpl.
  induction (f n); [reflexivity | reflexivity].
Qed.

Lemma lemma2:
  forall (a : Type) (f : a -> bool) (xs : list a), length (filter f xs) <= length xs.
Proof.
  intros a f xs.
  induction xs.
  simpl.
  apply le_0_n.
  rewrite lemma1.
  induction (f a0).
  simpl.
  apply le_n_S. 
  exact IHxs.
  simpl.
  rewrite IHxs.
  apply le_n_Sn.
Qed.


Fixpoint append (a : Type) (xs ys : list a) :=
  match xs with
  | nil      => ys
  | x :: xs' => x :: append a xs' ys
  end.

Definition append_nat := append nat.

Notation " xs @ ys " := ( append_nat xs ys ) (at level 55, right associativity).
Notation " [ x ] " := ( x :: nil ).

Function qsort (xs : list nat) { measure length xs } :=
  match xs with
  | nil      => nil
  | x :: xs' =>
    let lxs := qsort (filter (fun y => leb y x) xs') in
    let gxs := qsort (filter (fun y => negb (leb y x)) xs') in
    lxs @ [x] @ gxs
  end.
Proof.
  intros.
  simpl.
  apply le_lt_n_Sm.
  apply lemma2.
  intros.  
  simpl.
  apply le_lt_n_Sm.
  apply lemma2.
Defined.

Eval compute in (qsort (1::2::3::nil)).
Eval compute in (qsort (2::1::3::nil)).
Eval compute in (qsort (3::2::1::nil)).