Qcert.Basic.Util.RSort

Section RSort.


  Section Strongly.

    Context {A:Type}.
    Context {R:A→A→Prop}.
    Context (R_dec : ∀ 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.

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

    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 : ∀ l (p1 p2:is_list_sorted l = true), p1 = p2.

    Lemma sorted_StronglySorted `{Transitive A R}: ∀ l, is_list_sorted l = true ↔ StronglySorted R l.

    Lemma Forall_nin_irr `{Irreflexive A R}: ∀ a l, Forall (R a) l → ¬ In a l.

    Lemma StronglySorted_NoDup `{Irreflexive A R}:
      ∀ l, StronglySorted R l → NoDup l.

    Lemma Sorted_NoDup `{StrictOrder A R}:
      ∀ l, Sorted R l → NoDup l.

    Lemma is_list_sorted_NoDup `{StrictOrder A R} :
      ∀ 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 Strongly.

  Section In.
    Lemma StronglySorted_filter {A} {R} f {l} :
      @StronglySorted A R l → StronglySorted R (filter f l).

    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.

    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:∀ 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).


    Lemma insertion_sort_in {A R R_dec} {x l}
          (contr:∀ 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:∀ 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:∀ 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:∀ 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:∀ 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:∀ 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:∀ 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:∀ 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.

  Section map.

  Lemma map_insertion_sort_insert {A B}
        {R1 R2}
        (R1_dec : ∀ a a' : A, {R1 a a'} + {¬ R1 a a'})
        (R2_dec : ∀ b b' : B, {R2 b b'} + {¬ R2 b b'})
        (f:A→B)
    (consistent:∀ 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 : ∀ a a' : A, {R1 a a'} + {¬ R1 a a'})
        (R2_dec : ∀ b b' : B, {R2 b b'} + {¬ R2 b b'})
        (f:A→B)
    (consistent:∀ 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.

End RSort.