Library hydras.Prelude.Merge_Sort

From Coq Require Import List Wf_nat Recdef Compare_dec Arith Peano_dec
     Lia RelationClasses Sorting.Sorted Sorting.Permutation.

From hydras Require Import DecPreOrder DecPreOrder_Instances
     Sort_spec.
Import Relations Morphisms.

Section Generic.
  Variables (A:Type).

  Section Splitting.

    Function split (l:list A):=
      match l with
        | nil
        | _::nil ⇒ (l,nil)
        | a::b::l ⇒
          let (l1,l2):= split l in (a::l1,b::l2)
      end.

    Function split'_aux (l l':list A) :=
      match l,l' with
      | x::l,_::_::l' ⇒
        let (l1,l2) := split'_aux l l' in
        (x::l1, l2)
      | _,_ ⇒ (nil,l)
      end.

    Function split' (l:list A) := split'_aux l l.

    Lemma split_decr:
      ∀ l1 l2 a b, l1 = a::b::l2 →
                        length (fst(split l1)) < length l1 ∧
                        length (snd(split l1)) < length l1.

    Lemma split_permutation:
      ∀ l, Permutation ((fst(split l))++snd(split l)) l.


    Lemma split'_aux_length_preserve:
      ∀ l l',
        length(fst(split'_aux l l')) + length(snd (split'_aux l l')) =
        length l.

    Lemma split'_aux_length_fst:
      ∀ l l',
        length(fst(split'_aux l l')) =
 min (Nat.div2(length l')) (length l).




    Lemma split'_decr:
      ∀ l1 l2 a b, l1 = a::b::l2 →
                        length (fst(split' l1)) < length l1 ∧
                        length (snd(split' l1)) < length l1.

    Lemma split'_aux_eq:
      ∀ l l', ((fst(split'_aux l l'))++snd(split'_aux l l')) = l.

    Lemma split'_permutation:
      ∀ l, Permutation ((fst(split' l))++snd(split' l)) l.
  End Splitting.

  Section Merging.

    Fixpoint merge (leb : A → A →bool) l1 l2:=
      let fix merge_aux l2 {struct l2}:=
          match l1,l2 with
            | nil,_ ⇒ l2
            | _,nil ⇒ l1
            | a1::l1',a2::l2' ⇒
              if leb a1 a2 then a1 :: merge leb l1' l2 else a2 :: merge_aux l2'
          end
      in merge_aux l2.

    Variable le : relation A.

    Context (le_total : TotalPreOrder le).
    Context (le_dec : RelDecision le).

    Notation "a <= b" := (le a b).

    Lemma merge_rect:
      ∀ P: list A → list A → list A → Type,
        (∀ l:list A, P nil l l) →
        (∀ l: list A, P l nil l) →
        (∀ a1 l1 a2 l2,
           a1 ≤ a2 →
           P l1 (a2::l2) (merge (fun x y ⇒ bool_decide (x ≤ y)) l1 (a2::l2)) →
           P (a1::l1) (a2::l2) (a1::(merge (fun x y ⇒ bool_decide (x ≤ y))l1 (a2::l2)))) →
        (∀ a1 l1 a2 l2,
           ¬ le a1 a2 →
           P (a1::l1) l2 (merge (fun x y ⇒ bool_decide (x ≤ y))(a1::l1) l2) →
           P (a1::l1) (a2::l2) (a2::(merge (fun x y ⇒ bool_decide (x ≤ y)) (a1::l1) l2))) →
        ∀ l1 l2, P l1 l2 (merge (fun x y ⇒ bool_decide (x ≤ y)) l1 l2).

    Definition merge_ind ( P: list A → list A → list A → Prop) :=
      merge_rect P.

    Definition merge_rec( P: list A → list A → list A → Set) :=
      merge_rect P.

    Ltac induction_merge l1 l2:= pattern (merge (fun x y ⇒ bool_decide (x ≤ y)) l1 l2 ); apply merge_rect.

    Lemma merge_equation:
      ∀ l1 l2,
        merge (fun x y ⇒ bool_decide (x ≤ y)) l1 l2 =
        match l1,l2 with
          | nil,_ ⇒ l2
          | _,nil ⇒ l1
          | a1::l1',a2::l2' ⇒
            if decide (a1 ≤ a2) then a1 :: merge (fun x y ⇒ bool_decide (x ≤ y)) l1' l2
            else a2 :: merge (fun x y ⇒ bool_decide (x ≤ y)) l1 l2'
        end.

    Section Correctness.





      Lemma merge_Forall:
        ∀ (f:A→Prop) l1 l2,
          List.Forall f l1 →
          List.Forall f l2 →
          List.Forall f (merge (fun x y ⇒ bool_decide (x ≤ y)) l1 l2) .

      Lemma merge_LocallySorted:
        ∀ l1 l2, LocallySorted le l1 → LocallySorted le l2 →
                      LocallySorted le (merge (fun x y ⇒ bool_decide (x ≤ y)) l1 l2).

      Lemma merge_permutation:
        ∀ l1 l2, Permutation (l1++l2) (merge (fun x y ⇒ bool_decide (x ≤ y)) l1 l2).

      Section merge_sort.
        Variable split: list A → (list A × list A).

        Hypothesis split_decr:
          ∀ l1 l2 a b, l1 = a::b::l2 →
                        length (fst(split l1)) < length l1 ∧
                        length (snd(split l1)) < length l1.

        Hypothesis split_permutation:
          ∀ l, Permutation ((fst(split l))++snd(split l)) l.


        Function merge_sort (leb : A → A →bool) (l:list A) {measure length l} :=
          match l with
          | nil | _ :: nil ⇒ l
          | _::_::_ ⇒
            let (l1,l2) := split l in
            merge leb (merge_sort leb l1) (merge_sort leb l2)
          end.
        Defined.

        Theorem merge_sort_correct: sort_correct A le (merge_sort (fun x y ⇒ bool_decide (x ≤ y))).
      End merge_sort.
    End Correctness.


    Definition sp_merge_sort:= merge_sort split split_decr.

    Definition stable_merge_sort := merge_sort split' split'_decr.

  End Merging.

End Generic.

Check (sp_merge_sort: sort_fun_t).
Check (stable_merge_sort: sort_fun_t).

Theorem sp_mergesort_OK : sort_spec sp_merge_sort.

Theorem stable_mergesort_OK : sort_spec stable_merge_sort.