Require Import Lists.List.
Require Import Sorting.Sorted Sorting.Permutation.
Require Import Recdef.
Require Import Structures.Orders.

Module Sort (Import X: TotalLeBool').

Local Coercion is_true: bool >-> Sortclass.
Local Notation Sorted := (LocallySorted leb) (only parsing).

Definition filter_gt p := filter (fun x => x <=? p).
Definition filter_le p := filter (fun x => negb (x <=? p)).

Function sort (xs: list t) {measure length xs}: list t :=
  match xs with
  | nil => nil
  | p :: xs => sort (filter_gt p xs) ++ p :: sort (filter_le p xs)
  end.
Proof.
intros _ p xs _.
induction xs.
  auto.

  simpl; case leb; auto with arith.

intros _ p xs _.
induction xs.
  auto.

  simpl; case leb; auto with arith.
Defined.

Lemma Permutation_partition xs p: Permutation xs ((filter_gt p xs) ++ (filter_le p xs)).
Proof.
induction xs; simpl.
  reflexivity.

  case leb; simpl.
    apply perm_skip; assumption.

    etransitivity.
      apply perm_skip; eassumption.

      apply Permutation_middle.
Qed.

Theorem sort_permuting xs: Permutation xs (sort xs).
Proof.
functional induction (sort xs).
  reflexivity.

  etransitivity.
    apply perm_skip.
    etransitivity.
      apply Permutation_partition.

      apply Permutation_app; eassumption.

    apply Permutation_middle.
Qed.

Add Morphism sort
  with signature (@Permutation t) ==> (@Permutation t)
  as qs_permutation_morphism.
Proof.
intros x y.
intro H.
etransitivity.
symmetry; apply sort_permuting.
symmetry; etransitivity.
symmetry; apply sort_permuting.
symmetry; assumption.
Qed.

Lemma Sorted_partition p xs ys:
  Sorted xs -> Sorted ys ->
  Forall (fun x => (x <=? p) = true) xs ->
  Forall (fun x => (x <=? p) = false) ys ->
  Sorted (xs ++ p :: ys).
Proof.
intros Sx Sy Ox Oy.
induction xs as [| x xs IHx]; simpl.
  induction ys as [| y ys IHy]; simpl.
    apply LSorted_cons1.

    apply LSorted_consn; try assumption.
      inversion Oy.
      destruct (leb_total p y); [assumption | congruence].

  induction xs; simpl.
    apply LSorted_consn.
      apply IHx.
        apply LSorted_nil.

        trivial.

      inversion Ox; assumption.

  apply LSorted_consn.
    apply IHx.
      inversion Sx; assumption.

      inversion Ox; assumption.

    inversion Sx; assumption.
Qed.

Lemma Permutation_Forall (p: t -> Prop) xs ys:
  Permutation xs ys -> Forall p xs -> Forall p ys.
Proof.
intros P F.
induction ys as [| y ys].
  trivial.

  constructor.
    destruct (Forall_forall p xs) as [E _].
    apply E; try assumption.
      eapply Permutation_in.
        symmetry; eassumption.

        simpl; auto.

    destruct (Forall_forall p ys) as [_ D].
    apply D.
    intros.
    destruct (Forall_forall p xs) as [E _].
    apply E; try assumption.
      eapply Permutation_in.
        symmetry; eassumption.

        simpl; auto.
Qed.

Proposition filter_gt_le p xs: Forall (fun x => (x <=? p) = true) (filter_gt p xs).
Proof.
induction xs; simpl.
  trivial.

  case_eq (a <=? p); intro A; simpl; auto.
Qed.

Proposition filter_le_gt p xs: Forall (fun x => (x <=? p) = false) (filter_le p xs).
Proof.
induction xs; simpl.
  trivial.

  case_eq (a <=? p); intro A; simpl; auto.
Qed.


Theorem sort_sorting xs: Sorted (sort xs).
Proof.
functional induction (sort xs) as [| xs' p xs s IHg IHl].
  apply LSorted_nil.

  induction xs as [| x xs IHx].
    compute; apply LSorted_cons1.

    revert IHg IHl; simpl.
    case_eq (x <=? p); simpl; intros.
      apply Sorted_partition; try assumption.
        eapply Permutation_Forall.
          apply sort_permuting.

          constructor; [assumption | apply filter_gt_le].

        eapply Permutation_Forall.
          apply sort_permuting.

          apply filter_le_gt.

      apply Sorted_partition; try assumption.
        eapply Permutation_Forall.
          apply sort_permuting.

          apply filter_gt_le.

        eapply Permutation_Forall.
          apply sort_permuting.

          constructor; [assumption | apply filter_le_gt].
Qed.

End Sort.

Module Nat <: TotalLeBool.
  Require Arith.Compare_dec.
  Definition t := nat.
  Definition leb := Compare_dec.leb.
  Definition leb_total x y: leb x y = true \/ leb y x = true.
  Proof.
  elim (Compare_dec.le_ge_dec x y); [left | right];
  auto using Compare_dec.leb_correct.
  Defined.
End Nat.

Module NatSort := Sort Nat.

Extraction Language Ocaml.
Extraction "quicksort.ml" NatSort.sort.

Extraction Language Haskell.
Extraction "quicksort.hs" NatSort.sort.