Qcert.Basic.Typing.TOps

Section TOps.

  Section u.
    Context {fdata:foreign_data}.
    Context {fuop:foreign_unary_op}.
    Context {ftype:foreign_type}.
    Context {fdtyping:foreign_data_typing}.
    Context {m:brand_model}.
    Context {fuoptyping:foreign_unary_op_typing}.

    Inductive unaryOp_type : unaryOp → rtype → rtype → Prop :=
    | ATIdOp τ : unaryOp_type AIdOp τ τ
    | ATNeg: unaryOp_type ANeg Bool Bool
    | ATColl {τ} : unaryOp_type AColl τ (Coll τ)
    | ATSingleton τ :
        unaryOp_type ASingleton (Coll τ) (Option τ)
    | ATFlatten τ: unaryOp_type AFlatten (Coll (Coll τ)) (Coll τ)
    | ATDistinct τ: unaryOp_type ADistinct (Coll τ) (Coll τ)
    | ATOrderBy {τ} k sl pf1 pf2:
        sublist (List.map fst sl) (domain τ) →
        order_by_has_sortable_type τ (List.map fst sl) →
        unaryOp_type (AOrderBy sl) (Coll (Rec k τ pf1)) (Coll (Rec k τ pf2))
    | ATRec {τ} s pf : unaryOp_type (ARec s) τ (Rec Closed ((s,τ)::nil) pf)
    | ATDot {τ' τout} k s pf :
        tdot τ' s = Some τout →
        unaryOp_type (ADot s) (Rec k τ' pf) τout
    | ATRecRemove {τ} k s pf1 pf2 :
        unaryOp_type (ARecRemove s) (Rec k τ pf1) (Rec k (rremove τ s) pf2)
    | ATRecProject {τ} k sl pf1 pf2 :
        sublist sl (domain τ) →
        unaryOp_type (ARecProject sl) (Rec k τ pf1) (Rec Closed (rproject τ sl) pf2)
    | ATCount τ: unaryOp_type ACount (Coll τ) Nat
    | ATSum : unaryOp_type ASum (Coll Nat) Nat
    | ATNumMin : unaryOp_type ANumMin (Coll Nat) Nat
    | ATNumMax : unaryOp_type ANumMax (Coll Nat) Nat
    | ATArithMean : unaryOp_type AArithMean (Coll Nat) Nat
    | ATToString τ: unaryOp_type AToString τ String
    | ATSubstring start olen: unaryOp_type (ASubstring start olen) String String
    | ATLike pat oescape: unaryOp_type (ALike pat oescape) String Bool
    | ATLeft τl τr: unaryOp_type ALeft τl (Either τl τr)
    | ATRight τl τr: unaryOp_type ARight τr (Either τl τr)
    | ATBrand b :
        unaryOp_type (ABrand b) (brands_type b) (Brand b)
    | ATUnbrand {bs} :
        unaryOp_type AUnbrand (Brand bs) (brands_type bs)
    | ATCast br {bs} :
        unaryOp_type (ACast br) (Brand bs) (Option (Brand br))
    | ATUArith (u:ArithUOp) : unaryOp_type (AUArith u) Nat Nat
    | ATForeignUnaryOp {fu τin τout} :
        foreign_unary_op_typing_has_type fu τin τout →
        unaryOp_type (AForeignUnaryOp fu) τin τout.
  End u.

  Tactic Notation "unaryOp_type_cases" tactic(first) ident(c) :=
  first;
    [ Case_aux c "ATIdOp"%string
    | Case_aux c "ATNeg"%string
    | Case_aux c "ATColl"%string
    | Case_aux c "ATSingleton"%string
    | Case_aux c "ATFlatten"%string
    | Case_aux c "ATDistinct"%string
    | Case_aux c "ATOrderBy"%string
    | Case_aux c "ATRec"%string
    | Case_aux c "ATDot"%string
    | Case_aux c "ATRecRemove"%string
    | Case_aux c "ATRecProject"%string
    | Case_aux c "ATCount"%string
    | Case_aux c "ATSum"%string
    | Case_aux c "ATNumMin"%string
    | Case_aux c "ATNumMax"%string
    | Case_aux c "ATArithMean"%string
    | Case_aux c "ATToString"%string
    | Case_aux c "ATSubstring"%string
    | Case_aux c "ATLike"%string
    | Case_aux c "ATLeft"%string
    | Case_aux c "ATRight"%string
    | Case_aux c "ATBrand"%string
    | Case_aux c "ATUnbrand"%string
    | Case_aux c "ATCast"%string
    | Case_aux c "ATUArith"%string
    | Case_aux c "ATForeignUnaryOp"%string].

  Section b.

    Context {fdata:foreign_data}.
    Context {fbop:foreign_binary_op}.
    Context {ftype:foreign_type}.
    Context {fdtyping:foreign_data_typing}.
    Context {m:brand_model}.
    Context {fboptyping:foreign_binary_op_typing}.

    Inductive binOp_type: binOp → rtype → rtype → rtype → Prop :=
    | ATEq {τ} : binOp_type AEq τ τ Bool
    | ATConcat {τ₁ τ₂ τ₃} pf1 pf2 pf3 :
        rec_concat_sort τ₁ τ₂ = τ₃ →
        binOp_type AConcat (Rec Closed τ₁ pf1) (Rec Closed τ₂ pf2) (Rec Closed τ₃ pf3)
    | ATMergeConcat {τ₁ τ₂ τ₃} pf1 pf2 pf3 :
        merge_bindings τ₁ τ₂ = Some τ₃ →
        binOp_type AMergeConcat (Rec Closed τ₁ pf1) (Rec Closed τ₂ pf2) (Coll (Rec Closed τ₃ pf3))
    | ATMergeConcatOpen {τ₁ τ₂ τ₃} pf1 pf2 pf3 :
        merge_bindings τ₁ τ₂ = Some τ₃ →
        binOp_type AMergeConcat (Rec Open τ₁ pf1) (Rec Open τ₂ pf2) (Coll (Rec Open τ₃ pf3))
    | ATAnd : binOp_type AAnd Bool Bool Bool
    | ATOr : binOp_type AOr Bool Bool Bool
    | ATBArith (b:ArithBOp) : binOp_type (ABArith b) Nat Nat Nat
    | ATLt : binOp_type ALt Nat Nat Bool
    | ATLe : binOp_type ALe Nat Nat Bool
    | ATUnion {τ} : binOp_type AUnion (Coll τ) (Coll τ) (Coll τ)
    | ATMinus {τ} : binOp_type AMinus (Coll τ) (Coll τ) (Coll τ)
    | ATMin {τ} : binOp_type AMin (Coll τ) (Coll τ) (Coll τ)
    | ATMax {τ} : binOp_type AMax (Coll τ) (Coll τ) (Coll τ)
    | ATContains {τ} : binOp_type AContains τ (Coll τ) Bool
    | ATSConcat : binOp_type ASConcat String String String
    | ATForeignBinaryOp {fb τin₁ τin₂ τout} :
        foreign_binary_op_typing_has_type fb τin₁ τin₂ τout →
        binOp_type (AForeignBinaryOp fb) τin₁ τin₂ τout
    .
  End b.

  Tactic Notation "binOp_type_cases" tactic(first) ident(c) :=
    first;
    [ Case_aux c "ATEq"%string
    | Case_aux c "ATConcat"%string
    | Case_aux c "ATMergeConcat"%string
    | Case_aux c "ATMergeConcatOpen"%string
    | Case_aux c "ATAnd"%string
    | Case_aux c "ATOr"%string
    | Case_aux c "ATBArith"%string
    | Case_aux c "ATLt"%string
    | Case_aux c "ATLe"%string
    | Case_aux c "ATUnion"%string
    | Case_aux c "ATMinus"%string
    | Case_aux c "ATMin"%string
    | Case_aux c "ATMax"%string
    | Case_aux c "ATContains"%string
    | Case_aux c "ATSConcat"%string
    | Case_aux c "ATForeignBinaryOp"%string].

    Context {fdata:foreign_data}.
    Context {fuop:foreign_unary_op}.
    Context {fbop:foreign_binary_op}.
    Context {ftype:foreign_type}.
    Context {fdtyping:foreign_data_typing}.
    Context {h:brand_model}.
    Context {fuoptyping:foreign_unary_op_typing}.
    Context {fboptyping:foreign_binary_op_typing}.

  Lemma forall_typed_bunion {τ} d1 d2:
    Forall (fun d : data ⇒ data_type d τ) d1 →
    Forall (fun d : data ⇒ data_type d τ) d2 →
    Forall (fun d : data ⇒ data_type d τ) (bunion d1 d2).

  Lemma bminus_in_remove (x a:data) (d1 d2:list data) :
    In x (bminus d1 (remove_one a d2)) → In x (bminus d1 d2).

  Lemma forall_typed_bminus {τ} d1 d2:
    Forall (fun d : data ⇒ data_type d τ) d1 →
    Forall (fun d : data ⇒ data_type d τ) d2 →
    Forall (fun d : data ⇒ data_type d τ) (bminus d1 d2).

  Lemma forall_typed_bmin {τ} d1 d2:
    Forall (fun d : data ⇒ data_type d τ) d1 →
    Forall (fun d : data ⇒ data_type d τ) d2 →
    Forall (fun d : data ⇒ data_type d τ) (bmin d1 d2).

  Lemma forall_typed_bmax {τ} d1 d2:
    Forall (fun d : data ⇒ data_type d τ) d1 →
    Forall (fun d : data ⇒ data_type d τ) d2 →
    Forall (fun d : data ⇒ data_type d τ) (bmax d1 d2).

  Lemma forall_in_weaken {A} (P Q:A → Prop) l:
    (∀ x : A, P x ∨ In x l → Q x)
    → (∀ x : A, In x l → Q x).

  Lemma forall_typed_bdistinct {τ} d1:
    Forall (fun d : data ⇒ data_type d τ) d1 →
    Forall (fun d : data ⇒ data_type d τ) (bdistinct d1).

  Lemma Forall2_lookupr_none (l : list (string × data)) (l' : list (string × rtype)) (s:string):
    (Forall2
       (fun (d : string × data) (r : string × rtype) ⇒
          fst d = fst r ∧ data_type (snd d) (snd r)) l l') →
    assoc_lookupr ODT_eqdec l' s = None →
    assoc_lookupr ODT_eqdec l s = None.

  Lemma Forall2_lookupr_some (l : list (string × data)) (l' : list (string × rtype)) (s:string) (d':rtype):
    (Forall2
       (fun (d : string × data) (r : string × rtype) ⇒
          fst d = fst r ∧ data_type (snd d) (snd r)) l l') →
    assoc_lookupr ODT_eqdec l' s = Some d' →
    (∃ d'', assoc_lookupr ODT_eqdec l s = Some d'' ∧ data_type d'' d').

  Lemma rec_concat_with_drec_concat_well_typed dl dl0 τ₁ τ₂:
    is_list_sorted ODT_lt_dec (domain τ₁) = true →
    is_list_sorted ODT_lt_dec (domain τ₂) = true →
      is_list_sorted ODT_lt_dec (domain (rec_concat_sort τ₁ τ₂)) = true →
      Forall2
        (fun (d : string × data) (r : string × rtype) ⇒
           fst d = fst r ∧ data_type (snd d) (snd r)) dl τ₁ →
      Forall2
        (fun (d : string × data) (r : string × rtype) ⇒
           fst d = fst r ∧ data_type (snd d) (snd r)) dl0 τ₂ →
      Forall2
        (fun (d : string × data) (r : string × rtype) ⇒
           fst d = fst r ∧ data_type (snd d) (snd r)) (rec_sort (dl ++ dl0))
        (rec_concat_sort τ₁ τ₂).

  Lemma concat_well_typed {τ₁ τ₂ τ₃} d1 d2 pf1 pf2 pf3:
    rec_concat_sort τ₁ τ₂ = τ₃ →
    data_type d1 (Rec Closed τ₁ pf1) →
    data_type d2 (Rec Closed τ₂ pf2) →
    ∃ dl dl0 d3,
      d1 = drec dl ∧
      d2 = drec dl0 ∧
      ((rec_sort (dl ++ dl0)) = d3) ∧
      data_type (drec d3) (Rec Closed τ₃ pf3).

  Lemma rremove_well_typed τ s dl:
    Forall2
      (fun (d : string × data) (r : string × rtype) ⇒
         fst d = fst r ∧ data_type (snd d) (snd r)) dl τ →
    Forall2
      (fun (d : string × data) (r : string × rtype) ⇒
         fst d = fst r ∧ data_type (snd d) (snd r)) (rremove dl s)
      (rremove τ s).

  Lemma rproject_well_typed τ rl s dl:
    Forall2
      (fun (d : string × data) (r : string × rtype) ⇒
         fst d = fst r ∧ data_type (snd d) (snd r)) dl rl →
    sublist s (domain τ) →
    sublist τ rl →
    is_list_sorted ODT_lt_dec (domain τ) = true →
    is_list_sorted ODT_lt_dec (domain rl) = true →
    Forall2
      (fun (d : string × data) (r : string × rtype) ⇒
         fst d = fst r ∧ data_type (snd d) (snd r)) (rproject dl s)
      (rproject τ s).

  Definition mapTopNotSub s l2 (l:list (string×rtype)) :=
    map (fun xy ⇒ (fst xy, if in_dec string_dec (fst xy) s
                            then snd xy
                            else match lookup string_dec l2 (fst xy) with
                                   | Some y' ⇒ y'
                                   | None ⇒ Top
                                 end
                   )) l.

  Lemma mapTopNotSub_domain s l2 l :
    domain (mapTopNotSub s l2 l) = domain l.

  Lemma mapTopNotSub_in {s l x} l2:
    In (fst x) s → In x l → In x (mapTopNotSub s l2 l).

  Lemma mapTopNotSub_in2 {s l x y} l2:
      ¬ In x s → In x (domain l) → lookup string_dec l2 x = Some y → In (x,y) (mapTopNotSub s l2 l).

    Lemma in_mapTopNotSub {s l x} l2:
    In (fst x) s → In x (mapTopNotSub s l2 l) → In x l.

  Lemma mapTopNotSub_in_sublist {s l x} l2 :
    sublist s l →
      In x s → In x (mapTopNotSub (domain s) l2 l).

  Lemma mapTopNotSub_sublist {s l s'} l2:
    sublist s l →
    sublist s s' →
    sublist s (mapTopNotSub (domain s') l2 l).

  Lemma mapTopNotSub_sublist_same {s l} l2:
    sublist s l →
    sublist s (mapTopNotSub (domain s) l2 l).

  Lemma mapTopNotSub_in_inv {s l2 l x} :
    In x (mapTopNotSub s l2 l) →
    (In (fst x) s ∧ In x l) ∨
    (¬ In (fst x) s ∧
     (In x l2 ∨
      (¬ In (fst x) (domain l2) ∧ snd x = Top))).

  Lemma mapTopNotSub_compatible {t1 t2} rl1 rl2 :
    NoDup (domain rl1) → NoDup (domain rl2) →
    sublist t1 rl1 →
    sublist t2 rl2 →
  compatible t1 t2 = true →
    compatible (mapTopNotSub (domain t1) t2 rl1)
               (mapTopNotSub (domain t2) t1 rl2) = true.


  Lemma Forall2_compat_mapTopNotSub {x x0 rl rl0 t2} t1:
    is_list_sorted ODT_lt_dec (domain rl) = true →
    is_list_sorted ODT_lt_dec (domain rl0) = true →
    sublist t2 rl0 →
    Forall2 (fun (d : string × data) (r : string × rtype) ⇒
                fst d = fst r ∧ snd d ▹ snd r) x rl →
        Forall2 (fun (d : string × data) (r : string × rtype) ⇒
                fst d = fst r ∧ snd d ▹ snd r) x0 rl0 →
        compatible x x0 = true →
        Forall2
          (fun (d : string × data) (r : string × rtype) ⇒
             fst d = fst r ∧ snd d ▹ snd r) x (mapTopNotSub t1 t2 rl).

  Lemma Forall2_compat_app_strengthen {x x0 rl rl0 t1 t2}:
    is_list_sorted ODT_lt_dec (domain rl) = true →
    is_list_sorted ODT_lt_dec (domain rl0) = true →
    sublist t1 rl →
    sublist t2 rl0 →
    compatible t1 t2 = true →
    Forall2 (fun (d : string × data) (r : string × rtype) ⇒
                fst d = fst r ∧ snd d ▹ snd r) x rl →
        Forall2 (fun (d : string × data) (r : string × rtype) ⇒
                fst d = fst r ∧ snd d ▹ snd r) x0 rl0 →
        compatible x x0 = true →
        ∃ rl' rl0',
          compatible rl' rl0' = true ∧
          sublist t1 rl' ∧
          sublist t2 rl0' ∧
          Forall2 (fun (d : string × data) (r : string × rtype) ⇒
                      fst d = fst r ∧ snd d ▹ snd r) x rl' ∧
          Forall2 (fun (d : string × data) (r : string × rtype) ⇒
                      fst d = fst r ∧ snd d ▹ snd r) x0 rl0'.

  Lemma sorted_sublists_sorted_concat (τ₁ τ₂ rl rl0:list (string×rtype)):
    is_list_sorted ODT_lt_dec (domain τ₁) = true →
    is_list_sorted ODT_lt_dec (domain τ₂) = true →
    is_list_sorted ODT_lt_dec (domain rl) = true →
    is_list_sorted ODT_lt_dec (domain rl0) = true →
    compatible rl rl0 = true →
    sublist τ₁ rl →
    sublist τ₂ rl0 →
    sublist (rec_sort (τ₁ ++ τ₂)) (rec_sort (rl ++ rl0)).

  Lemma typed_binop_yields_typed_data {τ₁ τ₂ τout} (d1 d2:data) (b:binOp) :
    (d1 ▹ τ₁) → (d2 ▹ τ₂) → (binOp_type b τ₁ τ₂ τout) →
    (∃ x, fun_of_binop brand_relation_brands b d1 d2 = Some x ∧ x ▹ τout).

  Definition canon_brands_alt {br:brand_relation} (b:brands) :=
    fold_right meet [] (map (fun x ⇒ x::nil) b).

  Lemma canon_brands_alt_is_canon {br:brand_relation} (b:brands) :
    is_canon_brands brand_relation_brands (canon_brands_alt b).

  Lemma canon_brands_fold_right_hoist {br:brand_relation} (l:list brands) :
    fold_right
      (fun a b : brands ⇒ canon_brands brand_relation_brands (a ++ b))
      [] l =
    canon_brands brand_relation_brands
                 (fold_right (fun a b : brands ⇒ (a ++ b))
                             [] l).

  Lemma canon_brands_alt_equiv {br:brand_relation} (b:brands) :
    canon_brands brand_relation_brands b
    = canon_brands_alt b.

  Lemma typed_unop_yields_typed_data {τ₁ τout} (d1:data) (u:unaryOp) :
    (d1 ▹ τ₁) → (unaryOp_type u τ₁ τout) →
    (∃ x, fun_of_unaryop brand_relation_brands u d1 = Some x ∧ x ▹ τout).

  Lemma tdot_rec_concat_sort_neq {A} (l:list (string×A)) a b xv :
       a ≠ b →
       tdot (rec_concat_sort l [(a, xv)]) b =
       tdot (rec_sort l) b.

  Lemma tdot_rec_concat_sort_eq {A} (l : list (string × A)) a b :
               ¬ In a (domain l) →
               tdot (rec_concat_sort l [(a, b)]) a = Some b.

End TOps.

  Tactic Notation "unaryOp_type_cases" tactic(first) ident(c) :=
  first;
    [ Case_aux c "ATIdOp"%string
    | Case_aux c "ATNeg"%string
    | Case_aux c "ATColl"%string
    | Case_aux c "ATSingleton"%string
    | Case_aux c "ATFlatten"%string
    | Case_aux c "ATDistinct"%string
    | Case_aux c "ATOrderBy"%string
    | Case_aux c "ATRec"%string
    | Case_aux c "ATDot"%string
    | Case_aux c "ATRecRemove"%string
    | Case_aux c "ATRecProject"%string
    | Case_aux c "ATCount"%string
    | Case_aux c "ATSum"%string
    | Case_aux c "ATNumMin"%string
    | Case_aux c "ATNumMax"%string
    | Case_aux c "ATArithMean"%string
    | Case_aux c "ATToString"%string
    | Case_aux c "ATSubstring"%string
    | Case_aux c "ATLike"%string
    | Case_aux c "ATLeft"%string
    | Case_aux c "ATRight"%string
    | Case_aux c "ATBrand"%string
    | Case_aux c "ATUnbrand"%string
    | Case_aux c "ATCast"%string
    | Case_aux c "ATUArith"%string
    | Case_aux c "ATForeignUnaryOp"%string].

  Tactic Notation "binOp_type_cases" tactic(first) ident(c) :=
    first;
    [ Case_aux c "ATEq"%string
    | Case_aux c "ATConcat"%string
    | Case_aux c "ATMergeConcat"%string
    | Case_aux c "ATMergeConcatOpen"%string
    | Case_aux c "ATAnd"%string
    | Case_aux c "ATOr"%string
    | Case_aux c "ATBArith"%string
    | Case_aux c "ATLt"%string
    | Case_aux c "ATLe"%string
    | Case_aux c "ATUnion"%string
    | Case_aux c "ATMinus"%string
    | Case_aux c "ATMin"%string
    | Case_aux c "ATMax"%string
    | Case_aux c "ATContains"%string
    | Case_aux c "ATSConcat"%string
    | Case_aux c "ATForeignBinaryOp"%string].