Validation of the Quick Sort

coq_qsort.v

(******************************************************)
(** //// Validation of the Quick Sort ////            *)
(******************************************************)

Section QuickSort.

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


(*////////////////////////////////////////////////////*)
(** Preliminaries                                     *)
(*////////////////////////////////////////////////////*)

Section Preliminaries.

Variable A : Type.

(* Predicate : sublist l1 l2 <=> l1 is a sublist of l2. *)
Inductive sublist : list A -> list A -> Prop :=
    | Sublist_nil   : forall l : list A,
                      sublist nil l
    | Sublist_cons1 : forall (x : A) (l1 l2 : list A),
                      sublist l1 l2 ->
                      sublist l1 (x :: l2)
    | Sublist_cons2 : forall (x : A) (l1 l2 : list A),
                      sublist l1 l2 ->
                      sublist (x :: l1) (x :: l2).

(* Definition : Filter for the negatation *)
Fixpoint antifilter {A : Type} (f : A -> bool) (l : list A)
                    : list A :=
    match l with
    | nil     => nil
    | x :: l' => if f x
                     then      antifilter f l'
                     else x :: antifilter f l'
    end.

(* (filter f l) is a sublist of l. *) 
Lemma filter_sublist : forall (f : A -> bool) (l : list A),
                       sublist (filter f l) l.
Proof.
     intros f l.
     induction l as [| x l' H_l'].
     
         (* Case : l = nil *)
         simpl.
         apply Sublist_nil.
     
         (* Case : l = x :: l' *)
         simpl.
         case (f x).
         
             (* Case : f x = true *)
             apply Sublist_cons2.
             apply H_l'.
         
             (* Case : f x = false *)
             apply Sublist_cons1.
             apply H_l'.
Qed.

(* (antifilter f l) is a sublist of l. *) 
Lemma antifilter_sublist : forall (f : A -> bool) (l : list A),
                           sublist (antifilter f l) l.
Proof.
    intros f l.
    induction l as [| x l' H_l'].
    
        (* Case : l = nil *)
        simpl.
        apply Sublist_nil.
    
        (* Case : l = x :: l' *)
        simpl.
        case (f x).
        
            (* Case : f x = true *)
            apply Sublist_cons1.
            apply H_l'.
        
            (* Case : f x = false *)
            apply Sublist_cons2.
            apply H_l'.
Qed.

(* Sublists are shorter than or equal to the superlists. *)
Lemma sublist_length : forall l1 l2 : list A,
                       sublist l1 l2 ->
                       (l1 = l2 \/ length l1 < length l2).
Proof.
    intros l1 l2 H_sub.
    induction H_sub as [l2 | x l1 l2' H_sub H_ind |
                             x l1' l2' H_sub H_ind].
    
        (* Case : l1 = nil *)
        induction l2 as [| x l2' H_l2'].
        
            (* Case : l2 = nil *)
            left.
            reflexivity.
        
            (* Case : l2 = x1 :: l2' *)
            right.
            simpl.
            apply lt_O_Sn.
    
        (* Case : l2 = x :: l2' *)
        right.
        destruct H_ind as [H | H].
        
            (* Case : l1 = l2' *)
            rewrite H.
            simpl.
            apply lt_n_Sn.
        
            (* Case : length l1 < length l2' *)
            simpl.
            apply (lt_trans (length l1) (length l2')
                            (S (length l2')) H).
            apply lt_n_Sn.
    
        (* Case : l1 = x :: l1', l2 = x :: l2' *)
        destruct H_ind as [H | H].
        
            (* Case : l1' = l2' *)
            left.
            rewrite H.
            reflexivity.
        
            (* Case : length l1' < length l2' *)
            right.
            simpl.
            apply lt_n_S.
            apply H.
Qed.

(* All components of (filter f l) are true for test function f. *)
Lemma filter_true : forall (f : A -> bool) (l : list A) (x : A),
                    In x (filter f l) -> f x = true.
Proof.
    intros f l x H.
    induction l as [| y l' H_l'].
    
        (* Case : l = nil *)
        simpl in H.
        contradiction.
    
        (* Case : l = y :: l' *)
        simpl in H.
        case_eq (f y).
        
            (* Case : f y = true *)
            intro H_y.
            rewrite H_y in H.
            unfold In in H.
            destruct H as [H | H].
            
                (* Case : y = x *)
                rewrite <- H.
                apply H_y.
            
                (* Case : In x (filter f l') *)
                apply H_l' in H.
                apply H.
        
            (* Case : f y = false *)
            intro H_y.
            rewrite H_y in H.
            apply H_l' in H.
            apply H.
Qed.

(* All components of (filter f l) are false for test function f. *)
Lemma antifilter_false : forall (f : A -> bool)
                                (l : list A) (x : A),
                         In x (antifilter f l) -> f x = false.
Proof.
    intros f l x H.
    induction l as [| y l' H_l'].
    
        (* Case : l = nil *)
        simpl in H.
        contradiction.
    
        (* Case : l = y :: l' *)
        simpl in H.
        case_eq (f y).
        
            (* Case : f y = true *)
            intro H_y.
            rewrite H_y in H.
            apply H_l' in H.
            apply H.
        
            (* Case : f y = false *)
            intro H_y.
            rewrite H_y in H.
            destruct H as [H | H].
            
                (* Case : y = x *)
                rewrite <- H.
                apply H_y.
            
                (* Case : In x (antifilter f l') *)
                apply H_l' in H.
                apply H.
Qed.

(* sublist relation implies inclusion as component sets. *)
Lemma sublist_in : forall (l1 l2 : list A) (x : A),
                   In x l1 -> sublist l1 l2 -> In x l2.
Proof.
    intros l1 l2 x H_in H_sub.
    induction H_sub as [ | y l1 l2' H_sub H_ind |
                           y l1' l2' H_sub H_ind].
    
        (* Case : l1 = nil *)
        contradiction.
    
        (* Case : l2 = y :: l2' *)
        right.
        apply (H_ind H_in).
    
        (* Case : l1 = y :: l1', l2 = y :: l2' *)
        destruct H_in as [H_in | H_in].
        
            (* Case : y = x *)
            left.
            apply H_in.
        
            (* Case : In x l1' *)
            right.
            apply (H_ind H_in).
Qed.

(* filter and antifilter split lists. *)
Lemma filter_or : forall (f : A -> bool) (l : list A) (x : A),
                  In x l <->
                  (In x (filter f l) \/ In x (antifilter f l)).
Proof.
    intros f l x.
    split.
    
        (* Proof : Direction -> *)
        intro H.
        induction l as [| y l' H_l'].
        
            (* Case : l = nil *)
            left.
            change (In x nil).
            apply H.
        
            (* Case : l = y :: l' *)
            unfold In in H.
            fold (In x l') in H.
            destruct H as [H | H].
            
                (* Case : y = x *)
                rewrite H.
                case_eq (f x).
                
                    (* Case : f x = true *)
                    intro H_x.
                    left.
                    unfold filter.
                    rewrite H_x.
                    left.
                    reflexivity.
                
                    (* Case : f x = false *)
                    intro H_x.
                    right.
                    unfold antifilter.
                    rewrite H_x.
                    left.
                    reflexivity.
            
                (* Case : In x l' *)
                apply H_l' in H.
                destruct H as [H | H].
                
                    (* Case : In x (filter f l') *)
                    left.
                    case_eq (f y).
                    
                        (* Case : f y = true *)
                        intro H_y.
                        unfold filter.
                        rewrite H_y.
                        right.
                        apply H.
                    
                        (* Case : f y = false *)
                        intro H_y.
                        unfold filter.
                        rewrite H_y.
                        apply H.
                
                    (* Case : In x (antifilter f l') *)
                    right.
                    case_eq (f y).
                    
                        (* Case : f y = true *)
                        intro H_y.
                        unfold antifilter.
                        rewrite H_y.
                        apply H.
                    
                        (* Case : f y = false *)
                        intro H_y.
                        unfold antifilter.
                        rewrite H_y.
                        right.
                        apply H.
    
        (* Proof : Direction <- *)
        intro H.
        destruct H as [H | H].
        
            (* Case : In x (filter f l) *)
            apply (sublist_in (filter f l) l x H). 
            apply filter_sublist.
        
            (* Case : In x (antifilter f l) *)
            apply (sublist_in (antifilter f l) l x H). 
            apply antifilter_sublist.
Qed.

(* The merger of filter and antifilter *) 
(* is the permutation of the original. *)
Lemma filter_Permutation : forall (f : A -> bool) (l : list A),
                           Permutation
                           (filter f l ++ antifilter f l) l.
Proof.
    intros f l.
    induction l as [| x l' H_l'].
    
        (* Case : l = nil *)
        simpl.
        apply perm_nil.
    
        (* Case : l = x :: l' *)
        simpl.
        case (f x).
        
            (* Case : f x = true *)
            simpl.
            apply perm_skip.
            apply H_l'.
        
            (* Case : f x = false *)
            simpl.
            apply Permutation_sym.
            apply Permutation_cons_app.
            apply Permutation_sym.
            apply H_l'.
Qed.

End Preliminaries.


(*////////////////////////////////////////////////////*)
(** Algorithm                                         *)
(*////////////////////////////////////////////////////*)

(* Definition : Quick sort *)
Function qsort (l : list nat) {measure length} : list nat :=
    match l with
    | nil     => nil
    | n :: l' => let lts := antifilter (leb n) l' in
                 let ges := filter (leb n) l' in
                 (qsort lts) ++ n :: (qsort ges)
    end.
Proof.
        (* Proof : length (filter (beb n) l') < length l *)
        intros l n l' H_l.
        simpl.
        apply le_lt_trans with (length l').
        
            (* Proof : length (filter (leb n) l') <= length l' *)
            assert (filter (leb n) l' = l' \/
                    length (filter (leb n) l') < length l')
                   as H_len.
            
                (* Proof of the assertion *)
                apply sublist_length.
                apply filter_sublist.
            
            destruct H_len as [H_eq | H_lt].
            
                (* Case : filter (leb n) l' = l' *)
                rewrite H_eq.
                reflexivity.
            
                (* Case : length (filter (leb n) l') < length l' *)
                apply lt_le_weak.
                apply H_lt.
        
            (* Proof : length l' < S (length l') *)
            apply lt_n_Sn.
    
        (* Proof : length (antifilter (leb n) l') < length l *)
        intros l n l' H_l.
        simpl.
        apply le_lt_trans with (length l').
        
            (* Proof : length (antifilter (leb n) l') <=
                       length l' *)
            assert (antifilter (leb n) l' = l' \/
                    length (antifilter (leb n) l') < length l')
                   as H_len.
            
                (* Proof of the assertion *)
                apply sublist_length.
                apply antifilter_sublist.
            
            destruct H_len as [H_eq | H_lt].
            
                (* Case : antifilter (leb n) l' = l' *)
                rewrite H_eq.
                reflexivity.
            
                (* Case : length (antifilter (leb n) l' <
                          length l' *)
                apply lt_le_weak.
                apply H_lt.
        
            (* Proof : length l' < S (length l') *)
            apply lt_n_Sn.
Defined.


(*////////////////////////////////////////////////////*)
(** Validation 1 : Sorted                             *)
(*////////////////////////////////////////////////////*)

(* Compatibility of HdRel with appending *)
Lemma HdRel_app : forall (n : nat) (l1 l2 : list nat),
                  HdRel le n l1 -> HdRel le n l2 ->
                  HdRel le n (l1 ++ l2).
Proof.
    intro n.
    induction l1 as [| m l1' H_l1'].
    
        (* Case : l1 = nil *)
        intros l2 H_1 H_2.
        simpl.
        apply H_2.
    
        (* Case : l1 = m :: l1' *)
        intros l2 H_1 H_2.
        simpl. Print HdRel_cons.
        apply HdRel_cons.
        inversion H_1 as [| tmp1 tmp2 H_le (tmp3, tmp4)].
        clear tmp1 tmp2 tmp3 tmp4.
        apply H_le.
Qed.

(* Compatibility of sorted property with appending *)
Lemma Sorted_app : forall (l1 l2 : list nat),
                   Sorted le l1 -> Sorted le l2 ->
                   (forall n1 n2 : nat,
                    In n1 l1 -> In n2 l2 -> n1 <= n2) ->
                   Sorted le (l1 ++ l2).
Proof.
    induction l1 as [| m l1' H_l1'].
    
        (* Case : l1 = nil *)
        intros l2 H_1 H_2 H_le.
        simpl.
        apply H_2.
    
        (* Case : l1 = m :: l1' *)
        intros l2 H_1 H_2 H_le.
        simpl.
        inversion H_1 as [| tmp1 tmp2 H_sort H_hr (tmp3, tmp4)].
        clear tmp1 tmp2 tmp3 tmp4.
        apply Sorted_cons.
        
            (* Proof : Sorted le (l1' ++ l2) *)
            apply H_l1'.
            
                (* Proof : Sorted le l1' *)
                apply H_sort.
            
                (* Proof : Sorted le l2 *)
                apply H_2.
            
                (* Proof : In n1 l1' -> In n2 l2 -> n1 <= n2 *)
                intros n1 n2 H_n1 H_n2.
                apply H_le.
                
                    (* Proof : In n1 (m :: l1') *)
                    unfold In.
                    right.
                    apply H_n1.
                
                    (* Proof : In n2 l2 *)
                    apply H_n2.
            
            (* Proof : HdRel m (l1' ++ l2) *)
            apply HdRel_app.
            
                (* Proof : HdRel le m l1' *)
                apply H_hr.
            
                (* Proof : HdRel le m l2 *)
                induction l2 as [| p l2' H_l2'].
                
                    (* Case : l2 = nil *)
                    apply HdRel_nil.
                
                    (* Case : l2 = p :: l2' *)
                    apply HdRel_cons.
                    apply (H_le m p).
                    
                        (* Proof : In m (m :: l1') *)
                        unfold In.
                        left.
                        reflexivity.
                    
                        (* Proof : In m (m :: l1') *)
                        unfold In.
                        left.
                        reflexivity.
Qed.

(* Compatibility of In with qsort *)
Lemma qsort_in : forall (l : list nat) (n : nat),
                 In n l <-> In n (qsort l).
Proof.
    intros l n.
    split.
    
        (* Proof : Direction -> *)
        intro H.
        functional induction (qsort l)
            as [| _ m l' _ H' H'' H_lt H_ge].
        
            (* Case : l = nil *)
            apply H.
        
            (* Case : l = m :: l' *)
            apply in_app_iff.
            unfold In in H.
            fold (In n l') in H.
            destruct H as [H | H].
            
                (* Case : m = n *)
                right.
                rewrite H.
                unfold In.
                left.
                reflexivity.
           
                (* Case : In n l' *)
                apply (filter_or nat (leb m) l' n) in H.
                destruct H as [H | H].
                
                    (* Case : In n (filter (leb m) l') *)
                    right.
                    unfold In.
                    right.
                    apply H_ge.
                    apply H.
                
                    (* Case : In n (antifilter (leb m) l') *)
                    left.
                    apply H_lt.
                    apply H.
    
        (* Proof : Direction <- *)
        intro H.
        functional induction (qsort l)
            as [| _ m l' _ H' H'' H_lt H_ge].
        
            (* Case : l = nil *)
            apply H.
            apply in_app_iff in H.
            unfold In.
            fold (In n l').
            destruct H as [H | H].
            
                (* Case : In n (qsort (antifilter (leb m) l')) *)
                right.
                apply (filter_or nat (leb m) l' n).
                right.
                apply H_lt.
                apply H.
            
                (* Case : In n (m :: qsort (filter (leb m) l')) *)
                unfold In in H.
                fold (In n (qsort (filter (leb m) l'))) in H.
                destruct H as [H | H].
                
                    (* Case : m = n *)
                    left.
                    apply H.
                
                    (* Case : In n (qsort (filter (leb m) l')) *)
                    right.
                    apply (filter_or nat (leb m) l' n).
                    left.
                    apply H_ge.
                    apply H.
Qed.

(* Validation 1 : The outputs of qsort are sorted. *)
Theorem qsort_Sorted : forall l : list nat, Sorted le (qsort l).
Proof.
    intro l.
    functional induction (qsort l) as [| _ n l' _ H H' H_lt H_ge].
    
        (* Case : l = nil *)
        apply Sorted_nil.
    
        (* Case : l = n :: l' *)
        apply Sorted_app.
        
            (* Proof : Sorted le (qsort (antifilter (leb n) l')) *)
            apply H_lt.
        
            (* Proof : Sorted le (n :: qsort (filter (leb n) l')) *)
            apply Sorted_cons.
            
                (* Proof : Sorted le (qsort (filter (leb n) l')) *)
                apply H_ge.
            
                (* Proof : HdRel le n (qsort (filter (leb n) l')) *)
                remember (qsort (filter (leb n) l')) as ms.
                induction ms as [| m l'' H_l''].
                
                    (* Case : ms = nil *)
                    apply HdRel_nil.
                
                    (* Case : ms = m :: l'' *)
                    apply HdRel_cons.
                    assert (In m (filter (leb n) l')) as H_m.
                    
                        (* Proof of the assertion *)
                        apply qsort_in.
                        rewrite <- Heqms.
                        unfold In.
                        left.
                        reflexivity.
                    
                    apply filter_true in H_m.
                    apply leb_complete.
                    apply H_m.
        
            (* Proof : Properties of lts and ges. *)
            intros n1 n2 H_n1 H_n2.
            apply lt_le_weak.
            apply lt_le_trans with n.
            
                (* Proof : n1 < n *)
                apply leb_complete_conv.
                apply (antifilter_false nat (leb n) l').
                apply qsort_in.
                apply H_n1.
            
                (* Proof : n <= n2 *)
                destruct H_n2 as [H_n2 | H_n2].
                
                    (* Case : n = n2 *)
                    rewrite H_n2.
                    apply le_refl.
                
                    (* Case : In n2 (qsort (filter (leb n) l')) *)
                    apply leb_complete.
                    apply (filter_true nat (leb n) l').
                    apply qsort_in.
                    apply H_n2.
Qed.


(*////////////////////////////////////////////////////*)
(** Validation 2 : Permutation                        *)
(*////////////////////////////////////////////////////*)

(* Validation 2 : The outputs of qsort are        *)
(*                the permutations of the inputs. *)
Theorem qsort_Permutation : forall l : list nat,
                            Permutation (qsort l) l.
Proof.
    intro l.
    functional induction (qsort l) as [| _ n l' _ H H' H_lt H_ge].
    
        (* Case : l = nil *)
        apply perm_nil.
    
        (* Case : l = n :: l' *)
        symmetry.
        apply Permutation_cons_app.
        apply perm_trans with (antifilter (leb n) l' ++
                               filter (leb n) l').
        
            (* Proof : Permutation l'(antifilter (leb n) l' ++
                                      filter (leb n) l') *)
            rewrite Permutation_app_comm.
            apply Permutation_sym.
            apply filter_Permutation.
        
            (* Proof : Permutation (antifilter (leb n) l' ++
                                    filter (leb n) l')
                                   (qsort (antifilter (leb n) l') ++
                                    qsort (filter (leb n) l')) *)
            apply Permutation_app.
            
                (* Proof : Permutation
                               (antifilter (leb n) l')
                               (qsort (antifilter (leb n) l')) *)
                apply Permutation_sym.
                apply H_lt.
            
                (* Proof : Permutation
                               (filter (leb n) l')
                               (qsort (filter (leb n) l')) *)
                apply Permutation_sym.
                apply H_ge.
Qed.

End QuickSort.