qsort.v

Require Import Arith.
Require Import Arith.Compare.
Require Import Arith.Compare_dec.
Require Import List.
Require Import Recdef.
Require Import Sorting.Permutation.
Require Import Sorting.Sorted.

Lemma filter_length : forall f : nat -> bool , forall l : list nat , length ( filter f l ) <= length l.
Proof.
  intros.
  induction l.
    simpl.
    constructor.

    simpl.
    case ( f a ).
      simpl.
      apply le_n_S.
      apply IHl.

      apply le_S.
      apply IHl.
Qed.

Lemma list_length : forall n : nat , forall l : list nat , length l < length ( n :: l ).
Proof.
  intros.
  induction l.
    simpl.
    constructor.

    simpl.
    apply lt_n_S.
    simpl in IHl.
    apply IHl.
Qed.

Function qsort ( l : list nat ) { measure length l } : list nat :=
  match l with
  | nil => nil
  | x :: xs => qsort ( filter ( Basics.compose negb ( leb x ) ) xs ) ++ ( x :: qsort ( filter ( leb x ) xs ) )
  end.
Proof.
  intros.
  apply le_lt_trans with ( length xs ).
  apply filter_length.
  apply list_length.

  intros.
  apply le_lt_trans with ( length xs ).
  apply filter_length.
  apply list_length.
Defined.

Lemma perm_equal : forall l : list nat , Permutation l l.
Proof.
  intros.
  induction l.
    apply perm_nil.

    apply perm_skip.
    apply IHl.
Qed.

Lemma filter_permutation : forall f : nat -> bool , forall xs : list nat , Permutation xs ( filter ( Basics.compose negb f ) xs ++ filter f xs ).
Proof.
  intros.
  induction xs.
    simpl.
    apply perm_equal.

    simpl.
    unfold Basics.compose.
    unfold negb.
    case ( f a ).
      apply perm_trans with ( a :: ( filter ( fun x : nat => if f x then false else true ) xs ++ filter f xs ) ).
      apply perm_skip.
      apply IHxs.
      apply Permutation_middle.

      simpl.
      apply perm_skip.
      apply IHxs.
Qed.

Lemma filter_cons_permutation : forall f : nat -> bool , forall x : nat , forall xs : list nat , Permutation ( x :: xs ) ( filter ( Basics.compose negb f ) xs ++ x :: filter f xs ).
Proof.
  intros.
  apply perm_trans with ( x :: ( filter ( Basics.compose negb f ) xs ++ filter f xs ) ).
  apply perm_skip.
  apply filter_permutation.
  apply Permutation_middle.
Qed.

Theorem qsort_permutation : forall l : list nat , Permutation l ( qsort l ).
Proof.
  intros.
  functional induction ( qsort l ).
    apply perm_nil.

    apply perm_trans with ( filter ( Basics.compose negb ( leb x ) ) xs ++ x :: filter ( leb x ) xs ).
    apply filter_cons_permutation.
    apply Permutation_add_inside.
    apply IHl0.
    apply IHl1.
Qed.

Lemma concat_cons_sorted : forall R : nat -> nat -> Prop , forall n : nat , forall l1 l2 : list nat , LocallySorted R ( l1 ++ n :: nil ) -> LocallySorted R ( n :: l2 ) -> LocallySorted R ( l1 ++ n :: l2 ).
Proof.
  intros.
  induction l1.
    simpl.
    apply H0.

    induction l1.
      simpl.
      simpl in H.
      inversion H.
      apply LSorted_consn.
      simpl in IHl1.
      apply IHl1.
      apply H3.
      apply H5.

      simpl.
      apply LSorted_consn.
      simpl in IHl1.
      apply IHl1.
      inversion H.
      apply H3.
      inversion H.
      apply H5.
Qed.

Lemma remove_last_sorted : forall R : nat -> nat -> Prop , forall x : nat , forall l : list nat , Forall ( Basics.flip R x ) l -> LocallySorted R l -> LocallySorted R ( l ++ x :: nil ).
Proof.
  intros.
  induction l.
    simpl.
    apply LSorted_cons1.

    simpl.
    inversion H0.
    simpl.
    inversion H.
    unfold Basics.flip in H5.
    apply LSorted_consn.
    apply LSorted_cons1.
    apply H5.
    simpl.
    apply LSorted_consn.
    subst.
    simpl in IHl.
    apply IHl.
    inversion H.
    apply H6.
    apply H3.
    apply H4.
Qed.

Lemma skip_sorted : forall R : nat -> nat -> Prop , forall a b : nat , forall l : list nat , ( forall i j k : nat , R i j -> R j k -> R i k ) -> R a b -> Forall ( R b ) l -> LocallySorted R ( a :: l ) -> LocallySorted R ( a :: b :: l ).
Proof.
  intros.
  apply LSorted_consn.
  inversion H2.
  apply LSorted_cons1.
  apply LSorted_consn.
  apply H5.
  subst.
  inversion H1.
  apply H7.
  apply H0.
Qed.

Lemma remove_head_sorted : forall R : nat -> nat -> Prop , forall x : nat , forall l : list nat , ( forall i j k : nat , R i j -> R j k -> R i k ) -> Forall ( R x ) l -> LocallySorted R l -> LocallySorted R ( x :: l ).
Proof.
  intros.
  induction H1.
    apply LSorted_cons1.

    apply LSorted_consn.
    apply LSorted_cons1.
    inversion H0.
    apply H3.
    apply LSorted_consn.
    apply LSorted_consn.
    apply H1.
    apply H2.
    inversion H0.
    apply H5.
Qed.

Lemma forall_permutation : forall R : nat -> Prop , forall l1 l2 : list nat , Permutation l1 l2 -> Forall R l1 -> Forall R l2.
Proof.
  intros.
  induction H.
    apply H0.

    apply Forall_cons.
    inversion H0.
    apply H3.
    apply IHPermutation.
    inversion H0.
    apply H4.

    inversion H0.
    inversion H3.
    apply Forall_cons.
    apply H6.
    apply Forall_cons.
    apply H2.
    apply H7.

    apply IHPermutation2.
    apply IHPermutation1.
    apply H0.
Qed.

Lemma forall_more : forall x : nat , forall xs : list nat , Forall ( Basics.flip le x ) ( filter ( Basics.compose negb ( leb x ) ) xs ).
Proof.
  intros.
  induction xs.
    simpl.
    apply Forall_nil.

    simpl.
    unfold Basics.compose.
    unfold negb.
    case_eq ( leb x a ).
      intros.
      apply IHxs.

      intros.
      apply Forall_cons.
      unfold Basics.flip.
      apply leb_complete_conv in H.
      apply lt_le_weak.
      apply H.      
      apply IHxs.
Qed.

Lemma forall_less : forall x : nat , forall xs : list nat , Forall ( le x ) ( filter ( leb x ) xs ).
Proof.
  intros.
  induction xs.
    simpl.
    apply Forall_nil.

    simpl.
    case_eq ( leb x a ).
      intros.
      apply Forall_cons.
      apply leb_complete in H.
      apply H.
      apply IHxs.

      intros.
      apply IHxs.
Qed.

Theorem qsort_sorted : forall l : list nat , LocallySorted le ( qsort l ).
Proof.
  intros.
  functional induction ( qsort l ).
    apply LSorted_nil.

    apply concat_cons_sorted.
    apply remove_last_sorted.
    apply forall_permutation with ( filter ( Basics.compose negb ( leb x ) ) xs ).
    apply qsort_permutation.
    apply forall_more.
    apply IHl0.
    apply remove_head_sorted.
    intros.
    apply le_trans with j.
    apply H.
    apply H0.
    apply forall_permutation with ( filter ( leb x ) xs ).
    apply qsort_permutation.
    apply forall_less.
    apply IHl1.
Qed.