Qcert.Basic.Util.RSublist

Section RSublist.



  Section sublist.
    Context {A:Type}.
    Inductive sublist : list A → list A → Prop :=
    | sublist_nil : sublist nil nil
    | sublist_cons :
        ∀ x l1 l2, sublist l1 l2 → sublist (x::l1) (x::l2)
    | sublist_skip :
        ∀ x l1 l2, sublist l1 l2 → sublist l1 (x::l2)
    .


    Lemma sublist_In {l1 l2:list A} :
      sublist l1 l2 → ∀ x, In x l1 → In x l2.

    Lemma sublist_nil_l l : sublist nil l.

    Lemma sublist_nil_r l : sublist l nil → l = nil.

    Global Instance sublist_incl_sub : subrelation sublist (@incl A).



    Global Instance sublist_pre : PreOrder sublist.

    Lemma sublist_trans l1 l2 l3:
      sublist l1 l2 → sublist l2 l3 → sublist l1 l3.

    Lemma sublist_length {l1 l2} : sublist l1 l2 → length l1 ≤ length l2.

    Lemma sublist_length_eq {l1 l2} :
      sublist l1 l2 → length l1 = length l2 → l1 = l2.

    Global Instance sublist_antisymm : Antisymmetric (list A) eq sublist.

    Global Instance sublist_part : PartialOrder eq sublist.

    Global Instance sublist_NoDup : Proper (sublist --> impl) (@NoDup A).

    Lemma sublist_app {a1 b1 a2 b2:list A}:
      sublist a1 b1 →
      sublist a2 b2 →
      sublist (a1 ++ a2) (b1 ++ b2).

    Lemma sublist_app_l (l1 l2:list A) : sublist l1 (l1 ++ l2).

    Lemma sublist_app_r (l1 l2:list A) : sublist l2 (l1 ++ l2).

    Lemma filter_sublist f (l:list A) : sublist (filter f l) l.

  End sublist.


  Lemma cut_down_to_sublist
        {A B} {dec:EqDec A eq}
        (l:list (A×B)) (l2:list A) :
    sublist (cut_down_to l l2) l.

  Lemma sublist_map {A B} {l1 l2} (f:A→B) :
    sublist l1 l2 → sublist (map f l1) (map f l2).

  Lemma sublist_domain {A B} {l1 l2:list(A×B)} :
    sublist l1 l2 → sublist (domain l1) (domain l2).

  Lemma sublist_set_inter {A} dec (l1 l2 l3:list A):
    sublist l1 l3 →
    sublist (set_inter dec l1 l2) l3.

  Global Instance Forall_sublist {A} {P:A→Prop} :
    Proper (sublist --> impl) (Forall P).

  Lemma forallb_sublist {A} f (l1 l2:list A) :
    sublist l1 l2 →
    forallb f l2 = true →
    forallb f l1 = true.

  Lemma forallb_ordpairs_sublist {A} f (l1 l2:list A) :
    sublist l1 l2 →
    forallb_ordpairs f l2 = true →
    forallb_ordpairs f l1 = true.

  Lemma forallb_ordpairs_refl_sublist {A} f (l1 l2:list A) :
    sublist l1 l2 →
    forallb_ordpairs_refl f l2 = true →
    forallb_ordpairs_refl f l1 = true.

  Global Instance StronglySorted_sublist {A} {R:A→A→Prop} : Proper (sublist --> impl) (StronglySorted R).

  Lemma is_list_sorted_sublist {A} {R} {Rdec} {l l':list A}
        `{Transitive A R} :
    @is_list_sorted A R Rdec l = true →
    sublist l' l →
    is_list_sorted Rdec l' = true.


  Lemma StronglySorted_incl_sublist {A R l1 l2} `{EqDec A eq} `{StrictOrder A R} :
    StronglySorted R l1 →
    StronglySorted R l2 →
    (∀ x : A, In x l1 → In x l2) →
    sublist l1 l2.

  Lemma Sorted_incl_sublist {A R l1 l2} `{EqDec A eq} `{StrictOrder A R}:
    Sorted R l1 →
    Sorted R l2 →
    (∀ x : A, In x l1 → In x l2) →
    sublist l1 l2.

  Lemma Sorted_incl_both_eq {A R l1 l2} `{EqDec A eq} `{StrictOrder A R}:
    Sorted R l1 →
    Sorted R l2 →
    (∀ x : A, In x l1 → In x l2) →
    (∀ x : A, In x l2 → In x l1) →
    l1 = l2.

  Lemma insertion_sort_equivlist_strong {A R R_dec} `{EqDec A eq} `{StrictOrder A R} l l' (contr:asymmetric_over R l) :
    equivlist l l' →
    @insertion_sort A R R_dec l =
    @insertion_sort A R R_dec l'.

  Lemma insertion_sort_equivlist {A R R_dec} `{EqDec A eq} `{StrictOrder A R} (contr:∀ x y, ¬R x y → ¬R y x → x = y) l l' :
    equivlist l l' →
    @insertion_sort A R R_dec l =
    @insertion_sort A R R_dec l'.

  Lemma sublist_skip_l {A} (a:A) {l1 l2} :
    sublist (a::l1) l2 →
    sublist l1 l2.

  Lemma sublist_cons_eq_inv {A a l1 l2} :
    @sublist A (a::l1) (a::l2) →
    sublist l1 l2.

  Lemma sublist_filter {A} (f:A→bool) {l1 l2} :
    sublist l1 l2 → sublist (filter f l1) (filter f l2).

  Lemma sublist_cons_inv' {A B l1 a l2} :
    sublist l1(a::l2) →
    NoDup (@domain A B (a::l2)) →
    (∃ l',
        l1 = a::l' ∧ sublist l' l2)
    ∨
    (¬ In (fst a) (domain l1)
     ∧ sublist l1 l2).

  Lemma sublist_cons_inv {A B l1 a l2 R R_dec} `{StrictOrder A R}:
    sublist l1(a::l2) →
    @is_list_sorted A R R_dec (@domain _ B (a::l2)) = true →
    (∃ l',
        l1 = a::l' ∧ sublist l' l2)
    ∨
    (¬ In (fst a) (domain l1)
     ∧ sublist l1 l2).

  Lemma sublist_cons_inv_simple {A l1} {a:A} {l2} :
    sublist l1(a::l2) →
    NoDup (a::l2) →
    (∃ l',
       l1 = a::l' ∧ sublist l' l2)
    ∨
    (¬ In a l1
     ∧ sublist l1 l2).

  Lemma sublist_dec {A} {dec:EqDec A eq} (l1 l2 : list A) :
    {sublist l1 l2} + { ¬ sublist l1 l2}.

  Lemma sublist_remove {A} dec (x:A) l1 l2 :
    sublist l1 l2 →
    sublist (remove dec x l1) (remove dec x l2).

  Lemma sublist_nin_remove {A} dec (l1 l2:list (A)) a :
    ¬ In a l1 → sublist l1 l2 → sublist l1 (remove dec a l2).


  Lemma assoc_lookupr_nodup_sublist {A B} {R_dec:∀ a a' : A, {a = a'} + {a ≠ a'}} {l1 l2} {a:A} {b:B} :
    NoDup (domain l2) →
    sublist l1 l2 →
    assoc_lookupr R_dec l1 a = Some b →
    assoc_lookupr R_dec l2 a = Some b.


    Lemma insertion_sort_insert_sublist_self {A R}
        R_dec (a:A) l :
    sublist l (@insertion_sort_insert A R R_dec a l).

  Lemma insertion_sort_insert_sublist_prop {A R} {rstrict:StrictOrder R}
        (trich:∀ a b, {R a b} + {a = b} + {R b a})
        R_dec a l1 l2:
  is_list_sorted R_dec l2 = true →
  sublist l1 l2 →
  sublist (@insertion_sort_insert A R R_dec a l1)
          (@insertion_sort_insert A R R_dec a l2).

Lemma insertion_sort_sublist_proper {A R} {rstrict:StrictOrder R}
        (trich:∀ a b, {R a b} + {a = b} + {R b a}) R_dec :
  Proper (sublist ==> sublist) (@insertion_sort A R R_dec).

Lemma sublist_of_sorted_sublist {A R} {rstrict:StrictOrder R}
      (trich:∀ a b, {R a b} + {a = b} + {R b a})
      R_dec {l1 l2} :
  sublist (@insertion_sort A R R_dec l1) l2 →
  ∀ l1',
        sublist l1' l1 →
        sublist (insertion_sort R_dec l1') l2.

End RSublist.