(* begin hide *)
Require Import List.
Require Import OrderedType.
Require Import Coq.subtac.Utils.
Notation " [] " := nil.
Notation " [ x ] " := (cons x nil).
Notation " [ x ; .. ; y ] " := (cons x .. (cons y nil) ..).

Set Implicit Arguments.
(* end hide *)

(** An implementation of QuickSort using Program. 
   
   We implement stable quicksort for any ordered type. *)

Module QuickSort(O : OrderedType).

  (** Get the facts about the order. *)

  Module Facts := OrderedTypeFacts O.
  Import O. Import Facts.

  (** We work with a decidable equality, not necessarily leibniz, hence
     all list-processing functions and predicates must be adapted. *)

  Require Import Coq.Lists.SetoidList.
  Require Import Coq.Sorting.Sorting.
  Require Import Coq.Sorting.Permutation.
  Require Import Coq.Sorting.PermutSetoid.
  Notation permutation := (permutation eq eq_dec).


  (** We write [In] for [InA eq] which is appartness up-to the decidable equality. *)

  Notation In:=(InA eq).

  (** First the auxilliary [split] function, which splits a list [l] into 
     elements lower than [pivot] and the rest. *)

  Program Fixpoint split (pivot : t) (l : list t) {struct l} : 
    { (inf,sup) : list O.t * list O.t | 
      (forall x, (In x inf <-> (In x l /\ lt x pivot)) /\
        (In x sup <-> (In x l /\ ~ lt x pivot))) /\
      permutation l (inf ++ sup) } :=
    match l with
      | hd :: tl => 
        dest split pivot tl as (inf,sup) in
          if lt_dec hd pivot then (hd :: inf, sup)
            else (inf, hd :: sup) 
      | nil => ([],[])
    end.

  (** Get back the usual unfold of [In] which is burried in the inductive
     definition of [InA]. *)

  Lemma InA_In : forall x y l, In x (y :: l) -> eq x y \/ In x l.
  Proof.
    intros.
    inversion H ; subst.
    left ; assumption.
    right ; assumption.
  Qed.
    
  Next Obligation.
  Proof.
    intros.
    destruct_call split.
    clear split.
    destruct x as [inf' sup']; simpl in * ; destruct_conjs.
    inversion Heq_anonymous ; subst.
    clear Heq_anonymous.
    
    split.
    intros x ; destruct (H0 x) as [Hinf Hsup].
    unfold iff in Hinf, Hsup ; destruct Hinf as [Hil Hir] ; destruct Hsup as [Hsl Hsr].
        
    split ; split ; intros HIn.
    destruct (InA_In HIn) as [HI|HI].
    pose (eq_lt HI H).
    split ; auto with *.

    destruct (Hil HI).
    split ; auto with *.
    
    destruct HIn as [HIn HIlt].
    destruct (InA_In HIn).
    apply InA_cons_hd ; auto.
    apply InA_cons_tl ; auto.

    destruct (Hsl HIn).
    split ; auto with *.

    destruct HIn as [HIn HIlt].
    destruct (InA_In HIn) as [HIneq|Hintl].
    pose (eq_lt HIneq H).
    contradiction.
    
    auto with *.

    apply permut_cons ; auto.
  Defined.

  Next Obligation.
  Proof.
    intros.
    destruct_call split.
    clear split.
    destruct x as [inf' sup']; simpl in * ; destruct_conjs.
    inversion Heq_anonymous ; subst.
    clear Heq_anonymous.
    
    split.
    intros x ; destruct (H0 x) as [Hinf Hsup].
    unfold iff in Hinf, Hsup ; destruct Hinf as [Hil Hir] ; destruct Hsup as [Hsl Hsr].
        
    split ; split ; intros HIn.

    destruct (Hil HIn).
    split ; auto with *.
    
    destruct HIn as [HIn HIlt].
    destruct (InA_In HIn) as [HIneq|HIntl].
    pose (eq_lt (eq_sym HIneq) HIlt).
    contradiction.
    
    auto with *.

    destruct (InA_In HIn) as [HI|HI].
    split.
    apply InA_cons_hd ; auto.
    red ; intros HIlt.
    pose (eq_lt (eq_sym HI) HIlt).
    contradiction.

    destruct (Hsl HI) ; split ; auto with *.

    destruct HIn as [HIn HInlt].

    destruct (InA_In HIn) as [HIneq|Hintl].
    apply InA_cons_hd ; auto.
    apply InA_cons_tl ; auto with *.

    apply permut_add_cons_inside ; auto.
  Defined.

  Next Obligation.
  Proof.
    intros.
    intuition ; subtac_simpl ; auto with * ; try inversion H ; apply permut_refl.
  Qed.

  (** The predicate [le] is just a synonym for [~ lt] *)

  Definition le x y := ~ lt y x.
  
  (** Obviously decidable. *)

  Program Definition le_dec x y : { le x y } + { le y x } :=
    if lt_dec y x then right _ _ else left _ _.
  
  Next Obligation.
  Proof.
    intros.
    unfold le.
    red ; intros.
    order.
  Qed.
  
  (** That seems right too.. *)

  Lemma lt_le : forall x y, lt x y -> le x y.
  Proof.
    apply lt_not_gt.
  Qed.

  (** We sort using [le] and not [lt], hence we have to adapt this lemma
     from the standard library (see [sort_lt_app]). *)

  Lemma sort_le_app :
    forall l1 l2, sort le l1 -> sort le l2 ->
      (forall x y, In x l1 -> In y l2 -> lt x y) ->
      sort le (l1 ++ l2).
  Proof.
    induction l1; simpl in *; intuition.
    inversion_clear H.
    constructor; auto.
    apply InfA_app; auto.
    destruct l2; auto.
    constructor ; auto.
    apply lt_le.
    apply (H1 a t0) ; auto.
  Qed.

  (** Finally we can [quicksort] a list [l] using the usual definition. 
     Note that we ensure that the resulting list [l'] will be a sorted
     permutation of [l]. The obligations regarding the recursive calls are easily
     solved as [split] returns a permutation of its argument [tl]. From this we can easily
     derive that [length tl = length (inf ++ sup)]. The difficult bit is showing that 
     we are indeed building a sorted permutation. This amounts to a 30 lines proof using quite a 
     few lemmas from the standard library. *)

  Program Fixpoint quicksort (l : list t) {measure length l} : 
    { l' : list t | sort le l' /\ permutation l l'} := 
    match l with
      | hd :: tl => 
        dest split hd tl as (inf, sup) in
          quicksort inf ++ [hd] ++ quicksort sup
      | [] => []
    end.

   Solve Obligations using subtac_simpl ;
     intros ; destruct_call split ; destruct x  ; simpl in * ; 
    apply sym_eq in Heq_anonymous ; myinjection ; destruct y as [Hs Hperm] ;
      pose (Hs hd) ; destruct_conjs ; auto ;
   rewrite (permut_length eq_refl eq_sym eq_trans Hperm) ; rewrite app_length ; auto with arith.

  Next Obligation.
  Proof.  
    intros.
    destruct_call quicksort ; simpl.
    destruct_call quicksort ; simpl.
    simpl in *.
    clear quicksort.
    destruct_conjs ; simpl in *.
    destruct_call split as [l' Hsplit].
    destruct l' ; simpl in * ; myinjection.
    destruct Hsplit as [Hs Hlen].
    split.
    assert(sort le (hd :: x0)).
    apply cons_sort.
    assumption.
    apply (InA_InfA (eqA:=eq)) ; auto with *.
    intros.
    destruct (Hs y).
    pose (permut_InA_InA eq_sym (permut_sym H0) H3).
    intuition ; auto with *.
    apply (sort_le_app H1 H3).
    intros a b.
    destruct (Hs a) ; destruct_conjs.
    intros.
    unfold iff in H4, H5 ; destruct_conjs.
    pose (permut_InA_InA eq_sym (permut_sym H2) H6).
    destruct (InA_In H7) as [bhd|btl].
    destruct (H4 i).
    apply (lt_eq H11 (eq_sym bhd)).
    pose (permut_InA_InA eq_sym (permut_sym H0) btl).
    destruct (proj1 (proj2 (Hs b)) i0).
    pose (proj2 (H4 i)).
    apply lt_le_trans with hd ; auto with *.

    apply permut_add_cons_inside.
    apply permut_tran with (l0 ++ l1) ; auto.
    apply permut_app ; auto.
  Qed.
    

  Next Obligation.
  Proof.  
    intros.
    split ; auto with *.

    apply permut_refl.
  Qed.

End QuickSort.

Require Import OrderedTypeEx.
Module QS := QuickSort(N_as_OT).

Recursive Extraction QS.