Qcert.Basic.Util.RBindings

Section RBindings.



  Class ODT {K:Type}
    := mkODT { ODT_eqdec:>EqDec K eq;
               ODT_lt:K → K → Prop;
               ODT_lt_strorder:>StrictOrder ODT_lt;
               ODT_lt_dec: ∀ (a b:K), {ODT_lt a b} + {¬ODT_lt a b};
               ODT_compare:K → K → comparison;
               ODT_compare_spec: ∀ x y : K, CompareSpec (eq x y) (ODT_lt x y) (ODT_lt y x) (ODT_compare x y) }.

  Context `{odt:@ODT K}.

  Lemma ODT_lt_irr (k:K) :
    ~(ODT_lt k k).


  Lemma trichotemy a b : {ODT_lt a b} + {eq a b} + {ODT_lt b a}.

  Lemma compare_refl_eq a: ODT_compare a a = Eq.

  Lemma compare_eq_iff x y : (ODT_compare x y) = Eq ↔ x=y.

  Lemma ODT_lt_contr (x y : K) : ¬ ODT_lt x y → ¬ ODT_lt y x → x = y.


  Definition rec_field_lt {A} (a b:K×A) :=
    ODT_lt (fst a) (fst b).

  Global Instance rec_field_lt_strict {A} : StrictOrder (@rec_field_lt A).

  Lemma rec_field_lt_dec {A} (a b:K×A) :
    {rec_field_lt a b} + {¬rec_field_lt a b}.

  Lemma rec_field_lt_irr {A} (a:K×A) :
    ~(rec_field_lt a a).

  Lemma Forall_rec_field_lt {A} (a:K×A) l :
    Forall (rec_field_lt a) l ↔ Forall (ODT_lt (fst a)) (domain l).

  Definition rec_cons_sort {A} :=
    @insertion_sort_insert (K×A) rec_field_lt rec_field_lt_dec.

  Definition rec_sort {A} :=
    @insertion_sort (K×A) rec_field_lt rec_field_lt_dec.

  Definition rec_concat_sort {A} (l1 l2:list (K×A)) : (list (K×A)) :=
    rec_sort (l1++l2).


  Lemma sorted_rec_nil {A} :
    is_list_sorted ODT_lt_dec (@domain K A nil) = true.

  Lemma sort_rec_single_type {A} (k:K) (a:A):
    is_list_sorted ODT_lt_dec (domain ((k,a)::nil)) = true.

  Lemma field_less_is_neq (a1 a2:K) :
    ODT_lt a1 a2 → a1 ≠ a2.

  Lemma field_less_is_not_more (a1 a2:K) :
    ODT_lt a1 a2 → ~(ODT_lt a2 a1).

  Lemma field_not_less_and_neq_is_more (a1 a2:K) :
    ~(ODT_lt a1 a2) → ~(eq a1 a2) → ODT_lt a2 a1.

  Lemma rec_cons_lt {A} (l1:list (K×A)) (a1 a2:K×A) :
    is_list_sorted ODT_lt_dec (domain (a2 :: l1)) = true →
    ODT_lt (fst a1) (fst a2) →
    is_list_sorted ODT_lt_dec (domain (a1 :: a2 :: l1)) = true.

  Lemma rec_sorted_skip_first {A} (l1:list (K×A)) (a:K×A) :
    is_list_sorted ODT_lt_dec (domain (a :: l1)) = true →
    is_list_sorted ODT_lt_dec (domain l1) = true.

  Lemma rec_sorted_skip_second {A} (l:list (K×A)) (a1 a2:K×A) :
    is_list_sorted ODT_lt_dec (domain (a1 :: a2 :: l)) = true →
    is_list_sorted ODT_lt_dec (domain (a1 :: l)) = true.

  Lemma rec_sorted_skip_third {A} (l:list (K×A)) (a1 a2 a3:K×A) :
    is_list_sorted ODT_lt_dec (domain (a1 :: a2 :: a3 :: l)) = true →
    is_list_sorted ODT_lt_dec (domain (a1 :: a2 :: l)) = true.

  Lemma rec_sorted_distinct {A} (l:list (K×A)) (a1 a2:K×A) :
    is_list_sorted ODT_lt_dec (domain (a1 :: a2 :: l)) = true →
    (fst a1) ≠ (fst a2).

  Lemma rec_sorted_lt {A} (l:list (K×A)) (a1 a2:K×A) :
    is_list_sorted ODT_lt_dec (domain (a1 :: a2 :: l)) = true →
    ODT_lt (fst a1) (fst a2).

  Lemma sorted_cons_in {A} (l:list (K×A)) (a a':K×A) :
    is_list_sorted ODT_lt_dec (domain (a :: l)) = true →
    In a' l →
    ODT_lt (fst a) (fst a').


  Lemma rec_cons_lt_first {A} (l1:list (K×A)) (a1 a2:K×A) :
    is_list_sorted ODT_lt_dec (domain (a2 :: l1)) = true →
    ODT_lt (fst a1) (fst a2) →
    rec_cons_sort a1 (a2 :: l1) = (a1 :: a2 :: l1).

  Lemma sort_sorted_is_id {A} (l:list (K×A)) :
    is_list_sorted ODT_lt_dec (domain l) = true →
    rec_sort l = l.

  Lemma rec_concat_sort_concats {A} (l1 l2:list (K×A)) :
    rec_concat_sort l1 l2 = rec_sort (l1++l2).

  Lemma rec_cons_sorted_id {A} (l:list (K×A)) (a:K×A) :
    is_list_sorted ODT_lt_dec (domain (a :: l)) = true →
    rec_cons_sort a l = a::l.

  Lemma rec_sorted_id {A} (l:list (K×A)) :
    is_list_sorted ODT_lt_dec (domain l) = true →
    rec_sort l = l.

  Lemma rec_cons_gt_first {A} (l' l:list (K×A)) (a1 a2:K×A) :
    rec_cons_sort a1 l = l' →
    is_list_sorted ODT_lt_dec (domain (a2 :: l)) = true →
    ODT_lt (fst a2) (fst a1) →
    (∃ a3, ∃ l'', rec_cons_sort a1 l = (a3 :: l'')
                           ∧ ODT_lt (fst a2) (fst a3)).

  Lemma rec_cons_sorted {A} (l1 l2:list (K×A)) (a:K×A) :
    is_list_sorted ODT_lt_dec (domain l1) = true →
    rec_cons_sort a l1 = l2 →
    is_list_sorted ODT_lt_dec (domain l2) = true.

  Lemma rec_sort_sorted {A} (l1 l2:list (K×A)) :
    rec_sort l1 = l2 → is_list_sorted ODT_lt_dec (domain l2) = true.

  Lemma rec_sort_pf {A} {l1: list (K×A)} :
    is_list_sorted ODT_lt_dec (domain (rec_sort l1)) = true.

  Lemma rec_concat_sort_sorted {A} (l1 l2 x:list (K×A)) :
    rec_concat_sort l1 l2 = x →
    is_list_sorted ODT_lt_dec (domain x) = true.

  Lemma same_domain_same_sorted {A} {B} (l1:list (K×A)) (l2:list (K×B)) :
    domain l1 = domain l2 →
    is_list_sorted ODT_lt_dec (domain l1) = true →
    is_list_sorted ODT_lt_dec (domain l2) = true.

  Lemma same_domain_insert {A} {B}
        (l1:list (K×A)) (l2:list (K×B))
        (a:K×A) (b:K×B):
    domain l1 = domain l2 →
    fst a = fst b →
    domain (rec_cons_sort a l1) = domain (rec_cons_sort b l2).

  Lemma same_domain_rec_sort {A} {B}
        (l1:list (K×A)) (l2:list (K×B)) :
    domain l1 = domain l2 →
    domain (rec_sort l1) = domain (rec_sort l2).

  Lemma insertion_sort_insert_nin_perm {A:Type} l a :
    ¬ In (fst a) (@domain _ A l) →
  Permutation (a::l) (insertion_sort_insert rec_field_lt_dec a l).

  Lemma insertion_sort_perm_proper {A:Type} (l l':list (K×A)) a :
    ¬ In (fst a) (domain l) →
    Permutation l l' →
    Permutation
      (insertion_sort_insert rec_field_lt_dec a l)
      (insertion_sort_insert rec_field_lt_dec a l').

  Lemma rec_sort_perm {A:Type} l :
    NoDup (@domain _ A l) → Permutation l (rec_sort l).

  Lemma insertion_sort_insert_insertion_nin {A} (a:K×A) a0 l :
    ¬ rec_field_lt a0 a →
    ¬ rec_field_lt a a0 →
    insertion_sort_insert rec_field_lt_dec a0
                          (insertion_sort_insert rec_field_lt_dec a l)
    = insertion_sort_insert rec_field_lt_dec a l.

 Lemma insertion_sort_insert_cons_app {A} (a:K×A) l l2 :
    insertion_sort rec_field_lt_dec (insertion_sort_insert rec_field_lt_dec a l ++ l2) = insertion_sort rec_field_lt_dec (a::l ++ l2).

 Lemma insertion_sort_insertion_sort_app1 {A} l1 l2 :
    insertion_sort rec_field_lt_dec (insertion_sort (@rec_field_lt_dec A) l1 ++ l2) =
    insertion_sort rec_field_lt_dec (l1 ++ l2).

  Lemma insertion_sort_insertion_sort_app {A} l1 l2 l3 :
    insertion_sort rec_field_lt_dec (l1 ++ insertion_sort (@rec_field_lt_dec A) l2 ++ l3) =
    insertion_sort rec_field_lt_dec (l1 ++ l2 ++ l3).

  Lemma insertion_sort_eq_app1 {A l1 l1'} l2 :
    insertion_sort (@rec_field_lt_dec A) l1 = insertion_sort rec_field_lt_dec l1' →
    insertion_sort rec_field_lt_dec (l1 ++ l2) =
    insertion_sort rec_field_lt_dec (l1' ++ l2).

  Lemma rec_sort_rec_sort_app1 {A} l1 l2 :
   rec_sort ((@rec_sort A) l1 ++ l2) =
   rec_sort (l1 ++ l2).

  Lemma rec_sort_rec_sort_app {A} l1 l2 l3 :
    rec_sort (l1 ++ (@rec_sort A) l2 ++ l3) =
    rec_sort (l1 ++ l2 ++ l3).

  Lemma rec_sort_rec_sort_app2 {A} l1 l2 :
    rec_sort (l1 ++ (@rec_sort A) l2) =
    rec_sort (l1 ++ l2).

  Lemma rec_sort_eq_app1 {A l1 l1'} l2 :
    (@rec_sort A) l1 = rec_sort l1' →
    rec_sort (l1 ++ l2) =
    rec_sort (l1' ++ l2).

  Lemma rec_cons_sort_Forall2 {A B} P l1 l2 a b :
    Forall2 P l1 l2 →
    P a b →
    (domain l1) = (domain l2) →
    fst a = fst b →
    Forall2 P
            (insertion_sort_insert (@rec_field_lt_dec A) a l1)
            (insertion_sort_insert (@rec_field_lt_dec B) b l2).

  Lemma rec_sort_Forall2 {A B} P l1 l2 :
      (domain l1) = (domain l2) →
      Forall2 P l1 l2 →
      Forall2 P (@rec_sort A l1) (@rec_sort B l2).

  Lemma rec_concat_sort_nil_r {A} g :
    @rec_concat_sort A g nil = rec_sort g.

  Lemma rec_concat_sort_nil_l {A} g :
    @rec_concat_sort A nil g = rec_sort g.

  Lemma drec_sort_idempotent {A} l : @rec_sort A (rec_sort l) = rec_sort l.

  Lemma insertion_sort_insert_equiv_domain {A:Type} x a (l:list (K×A)) :
    In x
       (domain (RSort.insertion_sort_insert rec_field_lt_dec a l)) ↔
    fst a = x ∨ In x (domain l).

  Lemma drec_sort_equiv_domain {A} l :
    equivlist (domain (@rec_sort A l)) (domain l).


  Lemma insertion_sort_insert_swap_neq {A} a1 (b1:A) a2 b2 l :
    ~(eq a1 a2) →
    insertion_sort_insert rec_field_lt_dec (a1, b1)
                          (insertion_sort_insert rec_field_lt_dec
                                                 (a2, b2) l) =
    insertion_sort_insert rec_field_lt_dec (a2, b2)
                          (insertion_sort_insert rec_field_lt_dec
                                                 (a1, b1) l).

  Lemma insertion_sort_insert_middle {A} l1 l2 a (b:A) :
    ¬ In a (domain l1) →
    RSort.insertion_sort_insert rec_field_lt_dec (a, b)
                                (RSort.insertion_sort rec_field_lt_dec (l1 ++ l2)) =
    RSort.insertion_sort rec_field_lt_dec (l1 ++ (a, b) :: l2).

  Lemma drec_sort_perm_eq {A} l l' :
    NoDup (@domain _ A l) →
    Permutation l l' →
    rec_sort l = rec_sort l'.

  Lemma drec_sorted_perm_eq {A : Type} (l l' : list (K × A)) :
    is_list_sorted ODT_lt_dec (domain l) = true →
    is_list_sorted ODT_lt_dec (domain l') = true →
    Permutation l l' →
    l = l'.

  Lemma drec_concat_sort_app_comm {A} l l':
    NoDup (@domain _ A (l ++l')) →
    rec_concat_sort l l' = rec_concat_sort l' l.

  Lemma in_dom_rec_sort {B} {l x}:
    In x (domain (rec_sort l)) ↔ In x (@domain _ B l).

  Lemma drec_sort_sorted {A} l :
    RSort.is_list_sorted ODT_lt_dec
                         (@domain _ A
                                  (rec_sort l)) = true.

  Lemma drec_concat_sort_sorted {A} l l' :
    RSort.is_list_sorted ODT_lt_dec
                         (@domain _ A
                                  (rec_concat_sort l l')) = true.

  Lemma drec_sort_drec_sort_concat {A} l l' :
    (rec_sort (@rec_concat_sort A l l')) = rec_concat_sort l l'.

  Lemma assoc_lookupr_insertion_sort_insert_neq {B:Type} a x (b:B) l :
    ~(eq x a)→
    assoc_lookupr ODT_eqdec
                  (RSort.insertion_sort_insert rec_field_lt_dec (a, b) l)
                  x
    = assoc_lookupr ODT_eqdec l x.

  Lemma assoc_lookupr_insertion_sort_fresh {B:Type} x (d:B) b :
    ¬ In x (domain b) →
    assoc_lookupr ODT_eqdec
     (RSort.insertion_sort rec_field_lt_dec (b ++ (x, d) :: nil)) x =
    Some d.

  Lemma is_list_sorted_NoDup_strlt {A} l :
    is_list_sorted ODT_lt_dec (@domain _ A l) = true →
    NoDup (domain l).

  Lemma rec_sort_self_cons_middle {A} (l:list (K×A)) (a:K×A):
    is_list_sorted ODT_lt_dec (domain (a::l)) = true →
    rec_sort (l ++ a :: l) = rec_sort ((a :: l) ++ l).

  Lemma rec_field_anti {A} a:
    ¬ (@rec_field_lt A) a a.

  Lemma lt_not_not k1 k2:
    ¬ODT_lt k1 k2 → ¬ODT_lt k2 k1 → eq k1 k2.

  Lemma rec_concat_sort_self {A} (l:list (K×A)):
    is_list_sorted ODT_lt_dec (domain l) = true →
    rec_concat_sort l l = l.

  Lemma insert_first_into_app {A} (l l0:list (K×A)) (a:K×A):
    is_list_sorted ODT_lt_dec (domain (a :: l)) = true →
    rec_sort (l ++ insertion_sort_insert rec_field_lt_dec a (rec_sort (l ++ l0))) =
    insertion_sort_insert rec_field_lt_dec a (rec_sort (l ++ rec_sort (l ++ l0))).

  Lemma rec_concat_sort_idem {A} (l l0:list (K×A)):
    is_list_sorted ODT_lt_dec (domain l) = true →
    is_list_sorted ODT_lt_dec (domain l0) = true →
    rec_concat_sort l (rec_concat_sort l l0) = rec_concat_sort l l0.

  Instance In_equivlist_proper {A}:
    Proper (eq ==> equivlist ==> iff) (@In A).

  Lemma assoc_lookupr_insert B s (d:B) l x :
    assoc_lookupr ODT_eqdec
                  (RSort.insertion_sort_insert rec_field_lt_dec (s, d) l) x =
    match assoc_lookupr ODT_eqdec l x with
    | Some d' ⇒ Some d'
    | None ⇒ if ODT_eqdec x s then Some d else None
    end.

  Lemma assoc_lookupr_drec_sort {A} l x :
    assoc_lookupr ODT_eqdec (@rec_sort A l) x =
    assoc_lookupr ODT_eqdec l x.

  Lemma assoc_lookupr_drec_sort_app_nin {A} l l' x:
    ¬ In x (domain l') →
    assoc_lookupr ODT_eqdec (@rec_sort A (l ++ l')) x
    = assoc_lookupr ODT_eqdec (rec_sort l) x.

  Lemma insertion_sort_insert_domain {B:Type} x a (b:B) l :
    In x (domain
            (RSort.insertion_sort_insert rec_field_lt_dec
                                         (a, b) l)) →
    a = x ∨ In x (domain l).

  Lemma drec_sort_domain {A} x l :
    In x (domain (@rec_sort A l)) → In x (domain l).

  Lemma drec_concat_sort_pullout {A} b x xv y yv :
    NoDup (x::y::(domain b)) →
    (@ rec_concat_sort A (rec_concat_sort b ((x, xv) :: nil))
       ((y, yv) :: nil))
    =
    (rec_concat_sort (rec_concat_sort b ((y, yv) :: nil))
                     ((x, xv) :: nil)).

  Lemma sorted_cons_filter_in_domain {A} (l l':list (K×A)) f a :
    filter f l = a :: l' → In a l.

  Lemma filter_choice {A} (l:list(K×A)) f:
    filter f l = nil ∨ (∃ a, ∃ l', filter f l = a :: l').

  Lemma sorted_over_filter {A} (l:list (K×A)) f:
    is_list_sorted ODT_lt_dec (domain l) = true →
    is_list_sorted ODT_lt_dec (domain (filter f l)) = true.

  Lemma rec_sort_insert_filter_fst_true {A:Type} f
        (a:K×A) (l:list (K×A))
        (fstonly:∀ a b c, f (a,b) = f (a,c)) :
     StronglySorted rec_field_lt l →
     f a = true →
     filter f (insertion_sort_insert rec_field_lt_dec a l)
     = insertion_sort_insert rec_field_lt_dec a (filter f l).

   Lemma rec_sort_insert_filter_fst_false {A:Type} f
        (a:K×A) (l:list (K×A))
         (fstonly:∀ a b c, f (a,b) = f (a,c)) :
     f a = false →
     filter f (insertion_sort_insert rec_field_lt_dec a l) =
     filter f l.

   Lemma rec_sort_filter_fst_commute {A:Type} f (l:list (K×A))
         (fstonly:∀ a b c, f (a,b) = f (a,c)) :
     filter f (rec_sort l)
     = rec_sort (filter f l).

  Lemma forallb_rec_sort {A} f (l:list (K×A)) :
    forallb f l = true →
    forallb f (rec_sort l) = true.

  Lemma forallb_rec_sort_inv {A} f (l:list (K×A)) :
    NoDup (domain l) →
    forallb f (rec_sort l) = true →
    forallb f l = true.


  Lemma domain_rec_sort_insert {B} (a:K×B) l :
    domain (insertion_sort_insert rec_field_lt_dec a l) =
    insertion_sort_insert ODT_lt_dec (fst a) (domain l).

  Lemma domain_rec_sort {B} (l:list (K×B)) :
    domain (rec_sort l) = insertion_sort ODT_lt_dec (domain l).

  Lemma is_list_sorted_domain_rec_field {B} (l:list (K×B)) :
    is_list_sorted rec_field_lt_dec l
    = is_list_sorted ODT_lt_dec (domain l).

    Lemma rec_sort_insert_in_dom {B} a (l:list (K×B)) :
    In (fst a) (domain l) →
    is_list_sorted ODT_lt_dec (domain l) = true →
    insertion_sort_insert rec_field_lt_dec a l = l.

  Lemma rec_sort_filter_latter_from_former {B} s (l1 l2:list (K×B)) :
    In s (domain l2) →
    rec_sort (l1 ++ l2) =
    rec_sort (filter (fun x : K × B ⇒ s ≠b fst x) l1 ++ l2).

  Section Forall.

    Lemma Forall_sorted {A} (P:(K×A) → Prop) (l:list (K×A)):
      Forall P l → Forall P (rec_sort l).

  End Forall.

  Section CompatSort.

    Lemma compatible_app_compatible {A} `{EqDec A eq} {l1 l2:list (K×A)} :
      is_list_sorted ODT_lt_dec (domain l1) = true →
      is_list_sorted ODT_lt_dec (domain l2) = true →
      compatible l1 l2 = true →
      compatible (l1++l2) (l1++l2) = true.

    Lemma compatible_asymmetric_over {A} `{EqDec A eq} {l:list(K×A)} :
      compatible l l = true →
      asymmetric_over rec_field_lt l.

    Lemma compatible_sort_equivlist {A} `{EqDec A eq} {l:list(K×A)} :
      compatible l l = true →
      equivlist l (rec_sort l).

  End CompatSort.

  Section sublist.

    Lemma sublist_rec_concat_sort_bounded {A} r srl :
      incl (domain r) (domain srl) →
      domain (@rec_concat_sort A r srl) = domain (rec_sort srl).

Lemma domain_rec_concat_sort_app_comm:
  ∀ (A : Type) (l l' : list (K × A)),
    domain (rec_concat_sort l l') = domain (rec_concat_sort l' l).

Lemma incl_sort_sublist {A B} a b :
        incl (@domain _ A a) (@domain _ B b) →
        sublist (domain (rec_sort a)) (domain (rec_sort b)).

Lemma rec_concat_sort_sublist {B} l1 l2 :
      sublist (@domain _ B (rec_sort l1)) (domain (rec_concat_sort l1 l2)).

Lemma rec_concat_sort_sublist_sorted {B} l1 l2 :
  is_list_sorted ODT_lt_dec (domain l1) = true →
      sublist (@domain _ B l1) (domain (rec_concat_sort l1 l2)).

End sublist.

End RBindings.

Section map.

  Lemma map_rec_sort {A B C D} `{odta:ODT A} `{odtb:ODT B} (f:A×C→B×D) (l:list(A×C))
        (consistent:∀ x y, rec_field_lt x y ↔
                                rec_field_lt (f x) (f y)) :
    map f (rec_sort l) = rec_sort (map f l).
End map.

Section RBindingsString.


End RBindingsString.