Qcert.Basic.Data.RRelation

Section RRelation.


  Context {fdata:foreign_data}.

  Definition ldeq := (@Permutation data).
  Notation "X ≅ Y" := (ldeq X Y) (at level 70).
  Definition edot {A} (r:list (string×A)) (a:string) : option A :=
    assoc_lookupr ODT_eqdec r a.

  Lemma edot_nodup_perm {A:Type} (l l':list (string×A)) x :
    NoDup (domain l) → Permutation l l' → edot l x = edot l' x.

  Lemma edot_fresh_concat {A} x (d:A) b :
    ¬ In x (domain b) →
    edot (rec_concat_sort b ((x,d)::nil)) x = Some d.

  Definition unbdbool (f:bool → bool → bool) (d1 d2:data) : option data :=
    match d1 with
      | dbool b1 ⇒
        match d2 with
          | dbool b2 ⇒ Some (dbool (f b1 b2))
          | _ ⇒ None
        end
      | _ ⇒ None
    end.

  Definition unudbool (f:bool → bool) (d:data) : option data :=
    match d with
      | dbool b ⇒Some (dbool (f b))
      | _ ⇒ None
    end.

  Definition unbdnat (f:Z → Z → bool) (d1 d2:data) : option data :=
    match d1 with
      | dnat n1 ⇒
        match d2 with
          | dnat n2 ⇒ Some (dbool (f n1 n2))
          | _ ⇒ None
        end
      | _ ⇒ None
    end.

  Definition unbdata (f:data → data → bool) (d1 d2:data) : option data :=
    Some (dbool (f d1 d2)).

  Definition unsdstring (f:string → string → string) (d1 d2:data) : option data :=
    match d1 with
      | dstring s1 ⇒
        match d2 with
          | dstring s2 ⇒ Some (dstring (f s1 s2))
          | _ ⇒ None
        end
      | _ ⇒ None
    end.

  Lemma unsdstring_is_string f d1 d2 d3:
    unsdstring f d1 d2 = Some d3 → ∃ s:string, d3 = dstring s.

  Definition ondcoll2 {A} : (list data → list data → A) → data → data → option A.
  Defined.

  Definition rondcoll2 (f:(list data → list data → list data)) (d1 d2:data) : option data :=
    lift dcoll (ondcoll2 f d1 d2).

  Definition ondnat {A} (f : Z → A) (d : data) :=
    match d with
      | dnat n ⇒ Some (f n)
      | _ ⇒ None
    end.

  Definition ondcoll {A} (f : list data → A) (d : data) :=
    match d with
      | dcoll l ⇒ Some (f l)
      | _ ⇒ None
    end.

  Definition lift_oncoll {A} (f : list data → option A) (d : data) :=
    match d with
      | dcoll l ⇒ f l
      | _ ⇒ None
    end.

  Lemma lift_oncoll_dcoll {A} (f : list data → option A) (dl : list data) :
    lift_oncoll f (dcoll dl) = f dl.

  Lemma olift_on_lift_dcoll (f:list data→option data) (d1:option (list data)):
    olift (lift_oncoll f) (lift dcoll d1) =
    olift f d1.

  Lemma olift_lift_dcoll (f:list data → option (list data)) (d1:option (list data)):
    olift (fun c1 : list data ⇒ lift dcoll (f c1)) d1 =
    lift dcoll (olift f d1).

  Lemma lift_dcoll_inversion d1 d2:
    d1 = d2 → lift dcoll d1 = lift dcoll d2.

  Definition rondcoll (f:list data → list data) (d:data) : option data :=
    lift dcoll (ondcoll f d).

  Lemma lift_filter_Forall {A} {f:A→option bool} {P} {l x} :
    lift_filter f l = Some x →
    Forall P l →
    Forall P x.

  Fixpoint oflat_map {A B} (f : A → option (list B)) (l:list A) : option (list B) :=
    match l with
      | nil ⇒ Some nil
      | x :: t ⇒
        match f x with
          | None ⇒ None
          | Some x' ⇒
            lift (fun t' ⇒ x' ++ t') (oflat_map f t)
        end
    end.

  Fixpoint rmap {A B} (f : A → option B) (l:list A) : option (list B) :=
    match l with
      | nil ⇒ Some nil
      | x :: t ⇒
        match f x with
          | None ⇒ None
          | Some x' ⇒
            lift (fun t' ⇒ x' :: t') (rmap f t)
        end
    end.

  Lemma rmap_Forall {A B} {f:A→option B} {P} {l x} :
    rmap f l = Some x →
    Forall P l →
    ∀ (P2:B→Prop),
    (∀ x z, f x = Some z → P x → P2 z) →
    Forall P2 x.

  Lemma oflat_map_Forall {A B} {f:A→option (list B)} {P} {l x} :
    oflat_map f l = Some x →
    Forall P l →
    ∀ P2,
    (∀ x z, f x = Some z → P x → Forall P2 z) →
    Forall P2 x.

  Lemma rmap_id l:
    rmap (fun d : data ⇒ Some d) l = Some l.

  Lemma rmap_map {A} (f:data → A) l:
    rmap (fun d : data ⇒ Some (f d)) l = Some (map f l).

  Lemma rmap_map_merge {A} {B} {C} (f1:A → B) (f2:B → option C) (l: list A):
    (rmap (fun d ⇒ f2 (f1 d)) l) =
    rmap f2 (map f1 l).

  Lemma lift_dcoll_cons_rmap d l1 l2 :
    lift dcoll l1 = lift dcoll l2 →
    lift dcoll (lift (fun t ⇒ d :: t) l1) = lift dcoll (lift (fun t ⇒ d :: t) l2).

  Lemma rmap_over_app {A B} (f:A → option B) (l1:list A) (l2:list A) :
    rmap f (l1 ++ l2) = olift2 (fun x y ⇒ Some (x++y)) (rmap f l1) (rmap f l2).

  Fixpoint listo_to_olist {a: Type} (l: list (option a)) : option (list a) :=
    match l with
    | nil ⇒ Some nil
    | Some x :: xs ⇒ match listo_to_olist xs with
                      | None ⇒ None
                      | Some xs ⇒ Some (x::xs)
                      end
    | None :: xs ⇒ None
    end.

  Lemma listo_to_olist_simpl_rmap {A B:Type} (f:A → option B) (l:list A) :
    rmap f l = (listo_to_olist (map f l)).

  Lemma listo_to_olist_some {A:Type} (l:list (option A)) (l':list A) :
    listo_to_olist l = Some l' →
    l = (map Some l').

  Definition rfilter {A} (f:(string×A) → bool) (l:list (string×A)) : list (string×A) :=
    filter f l.

  Definition rremove {A} (l:list (string×A)) (s:string) : list (string×A) :=
    filter (fun x ⇒ if string_dec s (fst x) then false else true) l.

  Definition rproject {A} (l:list (string×A)) (s:list string) : list (string×A) :=
    filter (fun x ⇒ if in_dec string_dec (fst x) s then true else false) l.

  Lemma rproject_nil_l {A} (s:list string) :
    @rproject A [] s = [].

  Lemma rproject_nil_r {A} (l:list (string×A)) :
    @rproject A l [] = [].

  Lemma rproject_rec_sort_commute {B} (l1:list (string×B)) sl:
    rproject (rec_sort l1) sl = rec_sort (rproject l1 sl).

  Lemma rproject_map_fst_same {B C} (f:string×B→string×C) (l:list (string×B)) sl
    (samedom:∀ a, In a l → fst (f a) = fst a) :
      rproject (map f l) sl = map f (rproject l sl).

  Lemma rproject_app {B} (l1 l2:list (string×B)) sl:
    rproject (l1 ++ l2) sl = (rproject l1 sl) ++ (rproject l2 sl).

  Lemma rproject_rproject {B} (l:list (string×B)) sl1 sl2:
   rproject (rproject l sl2) sl1 = rproject l (set_inter string_dec sl2 sl1).

  Lemma rproject_Forall2_same_domain {B C} P (l1:list(string×B)) (l2:list (string×C)) ls :
    Forall2 P l1 l2 →
    domain l1 = domain l2 →
    Forall2 P (rproject l1 ls) (rproject l2 ls).

  Lemma sublist_rproject {A} (l:list(string×A)) sl: sublist (rproject l sl) l.

  Lemma rproject_remove_all {B} s sl (l1:list(string×B)):
    rproject l1 (remove_all s sl) =
    filter (fun x ⇒ nequiv_decb s (fst x)) (rproject l1 sl).

  Lemma rec_sort_rproject_remove_all_in {B} s sl l1 l2 :
    In s sl →
    In s (@domain _ B l2) →
    rec_sort (rproject l1 sl ++ l2) =
    rec_sort (rproject l1 (remove_all s sl) ++ l2).

  Lemma rec_sort_rproject_remove_in {B} s sl l1 l2 :
    In s sl →
    In s (@domain _ B l2) →
    rec_sort (rproject l1 sl ++ l2) =
    rec_sort (rproject l1 (remove string_dec s sl) ++ l2).

  Lemma rondcoll2_dcoll f (l1 l2:list data):
    rondcoll2 f (dcoll l1) (dcoll l2) = Some (dcoll (f l1 l2)).

  Lemma rondcoll_dcoll f (l:list data):
    rondcoll f (dcoll l) = Some (dcoll (f l)).

  Lemma ondcoll_dcoll {A} (f:list data → A) (l:list data):
    ondcoll f (dcoll l) = Some (f l).

  Lemma dcoll_map_app {A} (f:A → data) (l1 l2:list A) :
    Some (dcoll (map f l1 ++ map f l2)) = rondcoll2 bunion (dcoll (map f l1)) (dcoll (map f l2)).

  Definition orecconcat (a:data) (x:data) :=
    match a with
      | drec r2 ⇒
        match x with
          | drec r1 ⇒ Some (drec (rec_concat_sort r2 r1))
          | _ ⇒ None
        end
      | _ ⇒ None
    end.

  Definition omap_concat (a:data) (d1:list data) : option (list data) :=
    rmap (fun x ⇒ orecconcat a x) d1.

  Definition oomap_concat
             (f:data → option data)
             (a:data) :=
    match f a with
      | Some (dcoll y) ⇒ omap_concat a y
      | _ ⇒ None
    end.

  Definition rmap_concat (f:data → option data) (d:list data) : option (list data) :=
    oflat_map (oomap_concat f) d.

  Lemma rmap_concat_cons f d a x y :
    rmap_concat f d = Some x →
    (oomap_concat f a) = Some y →
    rmap_concat f (a :: d) = Some (y ++ x).

  Lemma rmap_concat_cons_none f d a :
    rmap_concat f d = None → rmap_concat f ((drec a) :: d) = None.

  Lemma rmap_concat_cons_none_first f d a :
    (oomap_concat f a) = None → rmap_concat f (a :: d) = None.

  Definition rproduct (d1 d2:list data) : option (list data) :=
    oflat_map (fun x ⇒ omap_concat x d2) d1.

  Lemma rproduct_cons (d1 d2:list data) a x y:
    rproduct d1 d2 = Some x →
    (omap_concat a d2) = Some y →
    rproduct (a::d1) d2 = Some (y ++ x).

  Definition rflatten (d:list data) : option (list data) :=
    oflat_map (fun x ⇒
                 match x with
                   | dcoll y ⇒ Some y
                   | _ ⇒ None end) d.

  Lemma rflatten_cons (l:list data) rest r' :
    rflatten rest = Some r' →
    rflatten ((dcoll l) :: rest) = Some (l ++ r').

  Lemma rflatten_app (l1 l2:list data) r1 r2 :
    rflatten l1 = Some r1 →
    rflatten l2 = Some r2 →
    rflatten (l1 ++ l2) = Some (r1 ++ r2).

  Lemma rflatten_map_dcoll_id coll :
    rflatten (map (fun d : data ⇒ dcoll (d::nil)) coll) = Some coll.

  Lemma rflatten_cons_none (d:data) rest :
    rflatten rest = None →
    rflatten (d :: rest) = None.

  Lemma rflatten_app_none1 l1 l2 :
    rflatten l1 = None →
    rflatten (l1 ++ l2) = None.

  Lemma rflatten_app_none2 l1 l2 :
    rflatten l2 = None →
    rflatten (l1 ++ l2) = None.

  Definition rif {A} (e:A → option bool) (a:A) : option (list A) :=
    match (e a) with
      | None ⇒ None
      | Some b ⇒
        if b then Some (a::nil) else Some nil
    end.

  Definition lrflatten {A} : option (list (list A)) → option (list A) :=
    lift lflatten.

  Definition orfilter {A} (f:A → option bool) (ol:option (list A)) : option (list A) :=
    olift (lift_filter f) ol.

  Lemma filter_eq_flatten_if {A} (e:A → option bool) (ol:option (list A)) :
    orfilter e ol = lrflatten (olift (rmap (rif e)) ol).

 Definition oand (x1 x2: option bool) : option bool :=
    match x1 with
      | None ⇒ None
      | Some b1 ⇒
        match x2 with
          | None ⇒ None
          | Some b2 ⇒ Some (andb b1 b2)
        end
    end.

  Lemma rmap_ext {A B : Type} (f g : A → option B) (l : list A) :
    (∀ x, In x l → f x = g x) →
    rmap f l = rmap g l.

  Lemma oflat_map_ext {A B} (f g:A→option (list B)) l :
    (∀ x, In x l → f x = g x) →
    oflat_map f l = oflat_map g l.

  Lemma oomap_concat_ext_weak f g a :
    (f a = g a) →
    oomap_concat f a = oomap_concat g a.

  Lemma rmap_concat_ext f g l :
    (∀ x, In x l → f x = g x) →
    rmap_concat f l = rmap_concat g l.

  Lemma olift_ext {A B : Type} (f g : A → option B) (x : option A) :
    (∀ a, x = Some a → f a = g a) →
    olift f x = olift g x.

  Lemma lift_oncoll_ext {A : Type} (f g : list data → option A) (d : data) :
    (∀ a, d = dcoll a → f a = g a) →
    lift_oncoll f d = lift_oncoll g d.

  Lemma lift_filter_ext {A : Type} (f g : A → option bool) (l : list A) :
    (∀ x, In x l → f x = g x) →
    lift_filter f l = lift_filter g l.

  Lemma rmap_map_fusion {A B C}
        (f:B→option C) (g:A → B) (l:list A) :
    rmap f (map g l) = rmap (fun x ⇒ f (g x)) l.

  Definition recconcat (r1 r2:list (string×data)) :=
    rec_concat_sort r1 r2.

  Definition map_concat (r2:list (string×data)) (d:list (list (string×data))) :=
    map (fun x ⇒ recconcat r2 x) d.

  Definition product (d1 d2:list (list (string×data))) :=
    (flat_map (fun x ⇒ map_concat x d2) d1).

  Definition ldeqt := (@Permutation (list (string×data))).

  Notation "b1 ⊖ b2" := (bminus b2 b1) (right associativity, at level 70) : rbag_scope.
  Lemma lift_empty_dcoll l :
    olift rflatten (lift (fun t' : list data ⇒ dcoll nil :: t') l) = olift rflatten l.

  Lemma lift_cons_dcoll a l:
    olift rflatten
          (lift (fun t' : list data ⇒ dcoll [a] :: t') l) =
    lift (fun t' ⇒ a::t') (olift rflatten l).

  Lemma rflatten_through_match l1 l2:
     olift rflatten
     match lift dcoll (Some l1) with
     | Some x' ⇒
         lift (fun t' : list data ⇒ x' :: t') l2
     | None ⇒ None
     end =
   lift (fun t' : list data ⇒ l1 ++ t')
     (olift rflatten l2).

End RRelation.

Section Misc.
  Lemma in_rec_sort_insert {A} `{EqDec A eq} (x:string × A) (s:string) (a:A) l:
    In x (insertion_sort_insert rec_field_lt_dec (s, a) l) →
    x = (s, a) ∨ In x l.

End Misc.


Section MergeBindings.


  Definition merge_bindings {A} `{EqDec A eq} (l₁ l₂:list (string × A)) : option (list (string × A)) :=
    if compatible l₁ l₂
    then Some (rec_concat_sort l₁ l₂)
    else None.

  Lemma merge_bindings_nil_r {A} `{EqDec A eq} l : merge_bindings l nil = Some (rec_sort l).

  Lemma merge_bindings_single_nin {A} `{EqDec A eq} b x d :
    ¬ In x (domain b) →
    merge_bindings b ((x,d)::nil) =
    Some (rec_concat_sort b ((x,d)::nil)).

  Lemma merge_bindings_sorted {A} `{EqDec A eq} {g g1 g2} :
    Some g = merge_bindings g1 g2 →
    is_list_sorted ODT_lt_dec (@domain string A g) = true.

  Lemma edot_merge_bindings {A} `{EqDec A eq} (l1 l2:list (string×A)) (s:string) (x:A) :
    merge_bindings l1 [(s, x)] = Some l2 →
    edot l2 s = Some x.

  Lemma merge_bindings_nodup {A} `{EqDec A eq} (l l0 l1:list (string×A)):
    merge_bindings l l0 = Some l1 → NoDup (domain l1).

  Lemma merge_bindings_compatible {A} `{EqDec A eq} (l l0 l1:list (string×A)):
    merge_bindings l l0 = Some l1 → compatible l l0 = true.

  Lemma sorted_cons_is_compatible {A} `{EqDec A eq} (l:list (string×A)) (a:string×A):
    is_list_sorted ODT_lt_dec (domain (a :: l)) = true →
    compatible_with (fst a) (snd a) l = true.

  Lemma compatible_self {A} `{EqDec A eq} (l:list (string×A)):
    is_list_sorted ODT_lt_dec (domain l) = true →
    compatible l l = true.

  Lemma merge_self_sorted {A} `{EqDec A eq} (l:list (string×A)):
    is_list_sorted ODT_lt_dec (domain l) = true →
    merge_bindings l l = Some l.

  Lemma merge_self_sorted_r {A} `{EqDec A eq} (l:list (string×A)):
    is_list_sorted ODT_lt_dec (domain l) = true →
    merge_bindings l (rec_sort l) = Some (rec_sort l).

  Lemma same_domain_merge_bindings_eq
        {A} `{EqDec A eq} (l₁ l₂ l₃:list (string×A)) :
    NoDup (domain l₁) →
    domain l₁ = domain l₂ →
    merge_bindings l₁ l₂ = Some l₃ →
    l₁ = l₂.

  Definition compatible {A:Type} `{x:EqDec A eq} := @compatible string A _ _ _ _.

  Lemma merge_returns_compatible {A} `{equiv:EqDec A eq} (l1 l2 l3:list (string×A)):
    is_list_sorted ODT_lt_dec (domain l1) = true →
    is_list_sorted ODT_lt_dec (domain l2) = true →
    compatible l1 l2 = true →
    rec_concat_sort l1 l2 = l3 →
    compatible l1 l3 = true.

  Lemma merge_idem {A} `{EqDec A eq} (l l0 l1:list (string×A)):
    is_list_sorted ODT_lt_dec (domain l) = true →
    is_list_sorted ODT_lt_dec (domain l0) = true →
    merge_bindings l l0 = Some l1 →
    merge_bindings l l1 = Some l1.


End MergeBindings.

Section RRemove.

  Lemma is_sorted_rremove {A} (l:list (string × A)) (s:string):
    is_list_sorted ODT_lt_dec (domain l) = true →
    is_list_sorted ODT_lt_dec (domain (rremove l s)) = true.

  Lemma domain_rremove {A} s (l:list (string×A)) :
    domain (rremove l s) = remove_all s (domain l).

  Lemma rremove_rec_sort_commute {B} (l1:list (string×B)) s:
    rremove (rec_sort l1) s = rec_sort (rremove l1 s).

  Lemma rremove_app {B} (l1 l2:list (string×B)) s:
    rremove (l1 ++ l2) s = rremove l1 s ++ rremove l2 s.

  Lemma nin_rremove {B} (l:list (string×B)) s :
    ¬ In s (domain l) →
    rremove l s = l.

End RRemove.

Section RProject.
  Lemma rproject_with_lookup {A} (l1 l2:list (string × A)) (s:list string):
    is_list_sorted ODT_lt_dec (domain l1) = true →
    is_list_sorted ODT_lt_dec (domain l2) = true →
    sublist l1 l2 →
    (∀ x, In x s → assoc_lookupr string_dec l1 x = assoc_lookupr string_dec l2 x) →
    rproject l1 s = rproject l2 s.

  Lemma rproject_sublist {A} (l1 l2:list (string × A)) (s:list string) :
    is_list_sorted ODT_lt_dec (domain l1) = true →
    is_list_sorted ODT_lt_dec (domain l2) = true →
    sublist s (domain l1) →
    sublist l1 l2 →
    rproject l1 s = rproject l2 s.

  Lemma rproject_equivlist {B} (l:list (string×B)) sl1 sl2 :
    equivlist sl1 sl2 →
    rproject l sl1 = rproject l sl2.

  Lemma rproject_sortfilter {B} (l:list (string×B)) sl1 :
    rproject l (insertion_sort ODT_lt_dec sl1) = rproject l sl1.

  Lemma rproject_concat_dist {A} (l1 l2:list (string × A)) (s:list string) :
    rproject (rec_concat_sort l1 l2) s = rec_concat_sort (rproject l1 s) (rproject l2 s).

End RProject.

Section SRProject.
  Definition sorted_vector (s:list string) : list string :=
    insertion_sort ODT_lt_dec s.

  Lemma sorted_vector_sorted (s:list string) :
    is_list_sorted ODT_lt_dec (sorted_vector s) = true.

  Definition projected_subset (s1 s2:list string) : list string :=
    filter (fun x ⇒ if in_dec string_dec x s2 then true else false) s1.

  Lemma projected_subst_sorted (s1 s2:list string) :
    is_list_sorted ODT_lt_dec s1 = true →
    is_list_sorted ODT_lt_dec (projected_subset s1 s2) = true.

  Lemma sorted_projected_subset_is_sublist (s1 s2:list string):
    is_list_sorted ODT_lt_dec s1 = true →
    is_list_sorted ODT_lt_dec s2 = true →
    sublist (projected_subset s1 s2) s2.


  Definition srproject {A} (l:list (string×A)) (s:list string) : list (string×A) :=
    let ps := (projected_subset (sorted_vector s) (domain l)) in
    rproject l ps.

  Lemma insertion_sort_insert_equiv_vec (x a:string) (l:list string) :
    In x
       (RSort.insertion_sort_insert ODT_lt_dec a l) ↔
    a = x ∨ In x l.

  Lemma sorted_vector_equivlist l :
    equivlist (sorted_vector l) l.

  Lemma equivlist_in_dec (x:string) (s1 s2:list string) :
    (equivlist s1 s2) →
    (if (in_dec string_dec x s1) then true else false) =
    (if (in_dec string_dec x s2) then true else false).

  Lemma sorted_vector_in_dec (x:string) (s1:list string):
    (if (in_dec string_dec x s1) then true else false) =
    (if (in_dec string_dec x (sorted_vector s1)) then true else false).

  Lemma in_intersection_projected (x:string) (s1 s2:list string) :
    In x s1 ∧ In x s2 → In x (projected_subset s1 s2).

  Lemma in_projected (x:string) (s1 s2:list string) :
    In x (projected_subset s1 s2) → In x s1.

  Lemma sproject_in_dec {A} (x:string) (s1:list string) (l:list (string×A)) :
    In x (domain l) →
    (if (in_dec string_dec x s1) then true else false) =
    (if (in_dec string_dec x (projected_subset s1 (domain l))) then true else false).

  Lemma rproject_sproject {A} (l:list (string×A)) (s:list string) :
    is_list_sorted ODT_lt_dec (domain l) = true →
    rproject l s = srproject l s.

End SRProject.


Notation "X ≅ Y" := (ldeq X Y) (at level 70) : rbag_scope. Notation "b1 ⊎ b2" := (bunion b2 b1) (right associativity, at level 70) : rbag_scope. Notation "b1 ⊖ b2" := (bminus b2 b1) (right associativity, at level 70) : rbag_scope. Notation "b1 × b2" := (rproduct b1 b2) (right associativity, at level 70) : rbag_scope. Notation "b1 min-b b2" := (bmin b1 b2) (right associativity, at level 70) : rbag_scope.
Notation "b1 max-b b2" := (bmax b1 b2) (right associativity, at level 70) : rbag_scope.
Notation "distinct-b b1" := (bdistinct b1) (right associativity, at level 70) : rbag_scope.