Require Import Program. (* for compose *)
Require Import Bool. (* for not_true_is_false *) 
(* Bool MUST be before Arith for leb to work right *)
Require Import Arith.  (* for leb, negb *)
Require Import List. (* for filter *)

Infix "o" := compose (at level 40, left associativity).

(* Define what it means for a list to be sorted. *)

Inductive sorted {A:Type} (R:A->A->Prop) : list A -> Prop :=
  Sorted0 : sorted R nil
 |Sorted1 : forall (x:A), sorted R (x::nil)
 |Sorted2 : forall (x y:A) (l:list A),
       (R x y) -> sorted R (y::l) -> sorted R (x::y::l).
Print Implicit sorted.

(* some "inversion lemmas" *)
Theorem sorted1_inv: forall (A:Type) (le:A->A->Prop) (x:A) (l:list A),
   sorted le (x::l) -> sorted le l.
inversion 1.
 apply Sorted0.

 exact H3.
Qed.

Theorem sorted2_inv: forall (A:Type) (le:A->A->Prop) (x y:A) (l:list A),
   sorted le (x::y::l) -> le x y.
inversion 1.
exact H2.
Qed.


(* Define what it means for a function to sort: *)
(*   A function sorts if the result is ordered (according to 'sorted', above)
     and the result has the same elements as its argument
     (according to 'same_elt', below). *)

Definition nbr_occ {N:Type} (re:N->N->bool) (z:N) (l:list N) := 
  fold_left (fun n x => if (re x z) then (n + 1) else n) l 0.

Check beq_nat.  (* use this for 're' - equality, not <= *)

Definition same_elt {N:Type} r l l' := forall (z:N), nbr_occ r z l = nbr_occ r z l'.


(* Now define the sorting function in question. 
   It is fully polymorphic, and sorts lists of any type (A)
   with respect to an ordering relation 'leb' on A. *)

Fixpoint quicksort_l {A:Type} (leb:A->A->bool) (lst:list A) (len:nat) := 
  match len with
     0 => nil
   | S l => 
       match lst with 
          nil => nil 
        | cons x xs => 
           let less := filter (compose negb (leb x)) xs in 
           let more := filter (leb x) xs in
           (quicksort_l leb less l) ++ (cons x nil) ++ (quicksort_l leb more l)
       end
  end.

Check length.

Definition quicksort {A:Type} leb (lst:list A) := quicksort_l leb lst (length lst).
Check leb.


(* An example to show how 'sorted' is used in proofs. *)
Locate "_ <= _".
Check le.
Check leb.
Compute map (leb 3) [1;2;3;4;5;6;7;78;8].

Hint Resolve Sorted0 Sorted1 Sorted2 : sort.

Theorem qcheck: sorted le (quicksort leb [5;1;3;67;8;3;4;5]).
compute.
apply Sorted2.
apply leb_complete.
simpl.
reflexivity.
apply Sorted2. apply leb_complete; simpl; reflexivity.
apply Sorted2. apply leb_complete; simpl; reflexivity.
apply Sorted2. apply leb_complete; simpl; reflexivity.
apply Sorted2. apply leb_complete; simpl; reflexivity.
apply Sorted2. apply leb_complete; simpl; reflexivity.
apply Sorted2. apply leb_complete; simpl; reflexivity.
apply Sorted1. 
Qed.

(* don't do this one. 
Theorem qcheck2: same_elt beq_nat 
                         [5;1;3;67;8;3;4;5] 
          (quicksort leb [5;1;3;67;8;3;4;5]).
*)

(* Goals: 

Theorem quicksort_sorts : 
  forall (l : list nat),
       sorted le (quicksort leb l)
    /\ same_elt beq_nat l (quicksort leb l).

Lemma quicksort_elt_preservation :
  forall (l : list nat), 
       same_elt beq_nat l (quicksort leb l).
Admitted.

Lemma quicksort_orders : 
  forall (l : list nat), 
       sorted le (quicksort leb l).
Admitted.

intros; split.
(* exact quicksort_orders. *)
revert l.
exact quicksort_orders.
revert l; exact quicksort_elt_preservation.
Qed.
 *)

Lemma length_0_inv : forall A (l:list A), 0 = (length l) -> l = [].
  intros.
  destruct l.
  reflexivity.
  absurd (0 = length (a::l)).
  simpl.
  auto.
  exact H.
Qed.

Lemma filter_not_longer : forall (A : Type) (l : list A) (f : A -> bool), 
  (length (filter f l)) <= (length l).

intros.
induction l.
 simpl.
 intuition.
 
 simpl.
 case (f a).
  simpl.
SearchPattern (_ <= _).
  apply le_n_S.
  exact IHl.
  
SearchPattern (?x <= S ?y).
  apply le_S.
  exact IHl.
Qed.

Lemma qsort_rewrite_len :
  forall l2 l1 (A:Type) R (lst: list A),
    length lst <= l1 -> 
    length lst <= l2 -> 
    quicksort_l R lst l1 = quicksort_l R lst l2.
Proof.
 intros.
 revert H0; revert H; revert lst; revert l2.
 induction l1.
  (* base case - l1 *)
  intros.
SearchAbout le.
Check (le_n_0_eq).
Check (le_n_0_eq (length lst)).
Check (le_n_0_eq (length lst) H).
  rewrite (length_0_inv A lst (le_n_0_eq (length lst) H)).
  simpl.
  destruct l2.
   simpl. reflexivity.

   simpl. reflexivity.

  (* inductive step - l1 *)
  intros.
  destruct l2.
   rewrite (length_0_inv A lst (le_n_0_eq (length lst) H0)).
   simpl.
   reflexivity.

   simpl.
   destruct lst.
     reflexivity.

     rewrite <- (IHl1 l2).
     rewrite <- (IHl1 l2).
     reflexivity.

   SearchAbout le.
   apply le_trans with (m:= (length lst)).
   apply filter_not_longer.

   simpl in H.
   apply le_S_n.
   exact H.

   apply le_trans with (m:= (length lst)).
   apply filter_not_longer.

   simpl in H0.
   apply le_S_n.
   exact H0.

   apply le_trans with (m:= (length lst)).
   apply filter_not_longer.

   simpl in H.
   apply le_S_n.
   exact H.

   apply le_trans with (m:= (length lst)).
   apply filter_not_longer.

   simpl in H0.
   apply le_S_n.
   exact H0.
Qed.

Lemma partition_is_sorted:
   forall (A:Type) (R:A->A->Prop) (y:A) (a b: list A), 
     sorted R a -> sorted R (y::b) -> 
       (forall x, ((In x a) -> R x y)) -> sorted R (a ++ (y :: b)).
intros.
induction a.
 simpl.
 exact H0.
 
 induction a0.
  simpl.
  apply Sorted2.
   apply (H1 a).
   simpl.
   intuition. (* assumption. *)
   
   exact H0.
   
  simpl.
  apply Sorted2.
   apply sorted2_inv with (l := a1).
   exact H.
   
   apply IHa.
    apply (sorted1_inv A R a).
    exact H.
    
    assert
     ((forall x : A, In x (a :: a0 :: a1) -> R x y) ->
      forall x : A, In x (a0 :: a1) -> R x y) as stronger_in.
     intros.
     apply H2.
     simpl in H3.
     destruct H3 as [H4| H5].
      simpl.
      right.
      left.
      exact H4.
      
      simpl.
      right; right; exact H5.
      
     apply stronger_in.
     exact H1.
Qed.

(* === primary lemma 1 === *)
(*Lemma quicksort_orders :
  forall (A:Type) (R:A->A->Prop) (Rb:A->A->bool) (l:list A),
       sorted R  (quicksort Rb l).  *)
Lemma quicksort_orders : 
  forall (l : list nat), 
       sorted le (quicksort leb l).

induction l.
(*base case*)
unfold quicksort.
simpl.
apply Sorted0.

(*induction: toplevel l *)
unfold quicksort.
unfold quicksort in IHl.
simpl.

apply 
(partition_is_sorted nat le a 
  (quicksort_l leb (filter (negb o Compare_dec.leb a) l) (length l))
  (quicksort_l leb (filter (Compare_dec.leb a) l) (length l)) ).

Lemma filter_of_sorted_is_sorted : 
    forall (A:Type) (R:A->A->Prop) (Rb:A->A->bool) (p:A->bool) (l:list A), 
       sorted R (quicksort_l Rb  l           (length l)) ->
       sorted R (quicksort_l Rb (filter p l) (length l)).
intros.
induction l.
 (* base case *)
 simpl.
 apply Sorted0.

 (* lemmas for induction step *)
 (* simpl. *)
   Lemma filter_cons_rewrite_false : 
      forall (A : Type) (p : A -> bool) (x : A) (l : list A),
        (p x) = false -> filter p (x::l) = filter p l.
   intros.
   simpl.
   rewrite H.
   reflexivity.
   Qed.

   Lemma filter_cons_rewrite_true :
      forall (A : Type) (p : A -> bool) (x : A) (l : list A),
        (p x) = true -> filter p (x::l) = x::(filter p l).
   intros.
   simpl.
   rewrite H.
   reflexivity.
   Qed.

 (* induction step *)
 assert (Hcases : forall x y : bool, {x <> y} + {x = y}).
 decide equality.

 destruct (Hcases (p a) true) as [Pfalse | Ptrue].
 apply (not_true_is_false (p a)) in Pfalse.
 rewrite filter_cons_rewrite_false.
 rewrite (qsort_rewrite_len (length l)).
 apply IHl.
   Lemma qsort_cons_inv : 
     forall (A:Type) R Rb l (a:A),
       sorted R (quicksort_l Rb (a :: l) (length (a :: l))) ->
       sorted R (quicksort_l Rb l (length l)).
    (*  intros. 
      simpl in H.
      apply partition_is_sorted with (y:=a) (b:=quicksort_l Rb (filter (Rb a) l) (length l)) in H.
      unfold quicksort_l in H.
      simpl in H.*)
      Admitted.
 apply qsort_cons_inv with (a:=a).
 exact H.
 apply le_trans with (m:=(length l)).
 apply filter_not_longer.
 simpl.
 intuition.
 apply filter_not_longer.
 exact Pfalse.
 
 rewrite filter_cons_rewrite_true.
 (* stuck here *)
Admitted. 
Admitted.

(* === primary lemma 2 === *)
Lemma quicksort_elt_preservation :
  forall (l : list nat), 
       same_elt beq_nat l (quicksort leb l).
Admitted.

Theorem quicksort_sorts : 
  forall (l : list nat),
       sorted le (quicksort leb l)
    /\ same_elt beq_nat l (quicksort leb l).
intros; split.
revert l;
exact quicksort_orders.
revert l; exact quicksort_elt_preservation.
Qed.


(* extraction to more efficient languages. *)

Extraction Language Ocaml.
Extraction quicksort.
Recursive Extraction quicksort quicksort_l.

Extraction Language Haskell.
Recursive Extraction quicksort.

(* see also:  
  Extraction "file.ml" id1 id2... .   [extract everything to file.ml]
  Separate Extraction id1 id2... .    [extract each id (and its dependencies) to its own file]
*)