Require Export Sorting.
Require Import EquivDec.
Require Import List.
Require Import LibUtilsCoqLibAdd.
Require Import LibUtilsListAdd.
Require Import Permutation.
Require Import Eqdep_dec.
Require Import RelationClasses.

Section SortingAdd.

Insertion sort

  Section InsertionSort.
    Context {A:Type}.
    Context {R:A->A->Prop}.
    Context (R_dec : forall a a', {R a a'} + {~R a a'}).

    Fixpoint insertion_sort_insert a l
      := match l with
         | nil => a :: nil
         | b::xs => if (R_dec a b)
                    then a::b::xs
                    else if (R_dec b a) then
                           b::insertion_sort_insert a xs
                         else b::xs
         end.

    Fixpoint insertion_sort (l:list A)
      := match l with
         | nil => nil
         | a::xs => insertion_sort_insert a (insertion_sort xs)
         end.

    Hint Constructors LocallySorted : fml.

    Lemma insertion_sort_insert_Sorted a (l:list A) :
      Sorted R l -> Sorted R (insertion_sort_insert a l).

    Hint Resolve insertion_sort_insert_Sorted : fml.

    Lemma insertion_sort_Sorted (l:list A) : Sorted R (insertion_sort l).

    Fixpoint is_list_sorted (l:list A) :=
      match l with
      | nil => true
      | x::xs => match xs with
                 | nil => true
                 | y::ls => if R_dec x y then is_list_sorted xs else false
                 end
      end.

    Lemma is_list_sorted_Sorted_iff l:
      is_list_sorted l = true <-> Sorted R l.

    Lemma is_list_sorted_ext : forall l (p1 p2:is_list_sorted l = true), p1 = p2.

    Lemma sorted_StronglySorted `{Transitive A R}:
      forall l, is_list_sorted l = true <-> StronglySorted R l.

    Lemma Forall_nin_irr `{Irreflexive A R}:
      forall a l, Forall (R a) l -> ~ In a l.

    Lemma StronglySorted_NoDup `{Irreflexive A R}:
      forall l, StronglySorted R l -> NoDup l.

    Lemma Sorted_NoDup `{StrictOrder A R}:
      forall l, Sorted R l -> NoDup l.

    Lemma is_list_sorted_NoDup `{StrictOrder A R} :
      forall l, is_list_sorted l = true -> NoDup l.

    Lemma is_list_sorted_cons a r :
      is_list_sorted (a::r) = true
      <->
      (is_list_sorted r = true
       /\ match r with
          | nil => True
          | y::_ => R a y
          end).

    Lemma is_list_sorted_cons_inv {a r} :
      is_list_sorted (a::r) = true ->
      is_list_sorted r = true.

    Lemma StronglySorted_cons_in {x a l} :
      StronglySorted R (a::l) ->
      In x l ->
      R a x.

    Lemma insertion_sort_sorted_is_id l :
      is_list_sorted l = true ->
      insertion_sort l = l.

    Lemma insertion_sort_idempotent l :
      insertion_sort (insertion_sort l) =
      insertion_sort l.

    Lemma insertion_sort_insert_not_nil a l :
      insertion_sort_insert a l <> nil.
    
    Lemma insertion_sort_nil l :
      insertion_sort l = nil -> l = nil.
    
    Lemma insertion_sort_insert_swap a a0 l `{StrictOrder A R}:
      R a a0 ->
      insertion_sort_insert a (insertion_sort_insert a0 l) =
      insertion_sort_insert a0 (insertion_sort_insert a l).

  End InsertionSort.

Properties of filter on sorted lists

  
  Section Filter.
    Lemma StronglySorted_filter {A} {R} f {l} :
      @StronglySorted A R l -> StronglySorted R (filter f l).
  End Filter.

Properties of In on sorted lists

  
  Section In.
    Lemma in_insertion_sort_insert {A R R_dec} {x l a} :
      In x (@insertion_sort_insert A R R_dec a l) -> a = x \/ In x l.

    Lemma in_insertion_sort {A R R_dec} {x l} :
      In x (@insertion_sort A R R_dec l) -> In x l.

    Hint Resolve asymmetric_over_cons_inv : fml.
    
    Lemma insertion_sort_insert_in_strong {A R R_dec} {x l a}
          (contr:asymmetric_over R (a::l)) :
      a = x \/ In x l -> In x (@insertion_sort_insert A R R_dec a l).

    Lemma insertion_sort_insert_in {A R R_dec} {x l a}
          (contr:forall x y, ~R x y -> ~R y x -> x = y) :
      a = x \/ In x l -> In x (@insertion_sort_insert A R R_dec a l).

    Lemma insertion_sort_in_strong {A R R_dec} {x l}
          (contr:asymmetric_over R l) :
      In x l -> In x (@insertion_sort A R R_dec l).

    Hint Resolve asymmetric_asymmetric_over : fml.

    Lemma insertion_sort_in {A R R_dec} {x l}
          (contr:forall x y, ~R x y -> ~R y x -> x = y) :
      In x l -> In x (@insertion_sort A R R_dec l).

    Lemma equivlist_insertion_sort_strong {A R} R_dec {l l'}
          (contr:asymmetric_over R l) :
      equivlist l l' ->
      equivlist (@insertion_sort A R R_dec l) (@insertion_sort A R R_dec l').

    Lemma equivlist_insertion_sort {A R} R_dec {l l'}
          (contr:forall x y, ~R x y -> ~R y x -> x = y) :
      equivlist l l' ->
      equivlist (@insertion_sort A R R_dec l) (@insertion_sort A R R_dec l').

    Lemma insertion_sort_insert_insertion_nin {A:Type} lt dec
          `{StrictOrder A lt}
          (trich:forall a b, {lt a b} + {eq a b} + {lt b a})
          (a:A) a0 l :
      ~ lt a0 a ->
      ~ lt a a0 ->
      insertion_sort_insert dec a0
                            (insertion_sort_insert dec a l)
      = @insertion_sort_insert A lt dec a l.

    Lemma insertion_sort_insert_cons_app {A:Type} lt dec
          `{StrictOrder A lt}
          (trich:forall a b, {lt a b} + {eq a b} + {lt b a}) a l l2 :
      insertion_sort dec (insertion_sort_insert dec a l ++ l2) = @insertion_sort A lt dec (a::l ++ l2).

    Lemma insertion_sort_insertion_sort_app1 {A} lt dec `{StrictOrder A lt}
          (trich:forall a b, {lt a b} + {eq a b} + {lt b a}) l1 l2 :
      insertion_sort dec (insertion_sort dec l1 ++ l2) =
      @insertion_sort A lt dec (l1 ++ l2).

    
    Lemma insertion_sort_trich_equiv {A:Type} lt dec
          (trich:forall a b, {lt a b} + {eq a b} + {lt b a}) (l:list A)
      : equivlist (@insertion_sort A lt dec l) l.

    Lemma insertion_sort_insert_forall_lt
          {A:Type} lt dec (a:A) (l:list A) :
      Forall (lt a) l ->
      @insertion_sort_insert A lt dec a l = a :: l.

    Lemma sort_insert_filter_true {A:Type} f lt dec `{StrictOrder A lt}
          (trich:forall a b, {lt a b} + {eq a b} + {lt b a})
          (a:A) (l:list A) :
      StronglySorted lt l ->
      f a = true ->
      filter f (@insertion_sort_insert A lt dec a l)
      = insertion_sort_insert dec a (filter f l).
    
    Lemma sort_insert_filter_false {A:Type} f lt dec (a:A) (l:list A) :
      f a = false ->
      filter f (@insertion_sort_insert A lt dec a l) =
      filter f l.
    
    Lemma sort_filter_commute {A:Type} f lt dec
          `{StrictOrder A lt}
          (trich:forall a b, {lt a b} + {eq a b} + {lt b a})
          (l:list A) :
      filter f (@insertion_sort A lt dec l)
      = insertion_sort dec (filter f l).

    Lemma Forall_insertion_sort {A R R_dec} {P} l :
      Forall P l -> Forall P (@insertion_sort A R R_dec l).
    
  End In.

Properties of map on sorted lists

  
  Section Map.

    Lemma map_insertion_sort_insert {A B}
          {R1 R2}
          (R1_dec : forall a a' : A, {R1 a a'} + {~ R1 a a'})
          (R2_dec : forall b b' : B, {R2 b b'} + {~ R2 b b'})
          (f:A->B)
          (consistent:forall x y, R1 x y <->
                                  R2 (f x) (f y)) a l :
      map f (insertion_sort_insert R1_dec a l) =
      insertion_sort_insert R2_dec (f a) (map f l).
    
    Lemma map_insertion_sort {A B}
          {R1 R2}
          (R1_dec : forall a a' : A, {R1 a a'} + {~ R1 a a'})
          (R2_dec : forall b b' : B, {R2 b b'} + {~ R2 b b'})
          (f:A->B)
          (consistent:forall x y, R1 x y <->
                                  R2 (f x) (f y)) l :
      map f (insertion_sort R1_dec l) =
      insertion_sort R2_dec (map f l).

  End Map.

  Lemma insertion_sort_insert_nin_eq_inv {A R} dec (a:A) l₁ l₂ :
    insertion_sort_insert (R:=R) dec a l₁ = insertion_sort_insert dec a l₂ ->
    ~ In a l₁ ->
    ~ In a l₂ ->
    l₁ = l₂.

End SortingAdd.