Qcert.Basic.Typing.TData
Section TData.
Context {fdata:foreign_data}.
Context {ftype:foreign_type}.
Context {fdtyping:foreign_data_typing}.
Context {m:brand_model}.
Definition Rrec (r1 r2:(string×data)) :=
ODT_lt_dec (fst r1) (fst r2).
Inductive data_type : data → rtype → Prop :=
| dttop d : data_normalized brand_relation_brands d → data_type d Top
| dtunit : data_type dunit Unit
| dtnat n : data_type (dnat n) Nat
| dtbool b : data_type (dbool b) Bool
| dtstring s : data_type (dstring s) String
| dtcoll dl r : Forall (fun d ⇒ data_type d r) dl →
data_type (dcoll dl) (Coll r)
| dtrec k dl rl rl_sub pf
(pf':is_list_sorted ODT_lt_dec (domain rl) = true) :
sublist rl_sub rl →
(k = Closed → rl_sub = rl) →
Forall2
(fun d r ⇒ (fst d) = (fst r) ∧ data_type (snd d) (snd r))
dl rl →
data_type (drec dl) (Rec k rl_sub pf)
| dtleft {d τl} τr : data_type d τl → data_type (dleft d) (Either τl τr)
| dtright {d} τl {τr} : data_type d τr → data_type (dright d) (Either τl τr)
| dtbrand b b' d :
is_canon_brands brand_relation_brands b →
data_normalized brand_relation_brands d →
Forall (fun bb ⇒
∀ τ,
lookup string_dec brand_context_types bb = Some τ →
data_type d τ
) b →
b ≤ b' →
data_type (dbrand b d) (Brand b')
| dtforeign {fd fτ} :
foreign_data_typing_has_type fd fτ →
data_type (dforeign fd) (Foreign fτ)
.
Notation "d ▹ r" := (data_type d r) (at level 70).
Section opt.
Lemma dtsome {d τ} :
data_type d τ →
data_type (dsome d) (Option τ).
Lemma dtnone τ :
data_type dnone (Option τ).
Lemma dtsome_inv {d τ} :
data_type (dsome d) (Option τ) →
data_type d τ.
End opt.
Lemma dtrec_closed_inv {dl rl pf} :
data_type (drec dl) (Rec Closed rl pf) →
Forall2
(fun d r ⇒ (fst d) = (fst r) ∧ data_type (snd d) (snd r))
dl rl.
Lemma dtrec_full k {dl rl} pf:
Forall2
(fun d r ⇒ (fst d) = (fst r) ∧ data_type (snd d) (snd r))
dl rl →
data_type (drec dl) (Rec k rl pf).
Lemma dtrec_open {dl : list (string×data)} {rl rl_sub : list (string×rtype)}
pf (pf':is_list_sorted ODT_lt_dec (domain rl) = true) :
sublist rl_sub rl →
Forall2
(fun d r ⇒ (fst d) = (fst r) ∧ data_type (snd d) (snd r))
dl rl →
data_type (drec dl) (Rec Open rl_sub pf).
Lemma dtrec_open_pf {dl : list (string×data)} {rl rl_sub : list (string×rtype)}
(pf':is_list_sorted ODT_lt_dec (domain rl) = true) :
∀ (sub:sublist rl_sub rl),
Forall2
(fun d r ⇒ (fst d) = (fst r) ∧ data_type (snd d) (snd r))
dl rl →
data_type (drec dl) (Rec Open rl_sub (is_list_sorted_sublist pf' (sublist_domain sub))).
Lemma dtrec_closed_is_open k dl rl pf :
data_type (drec dl) (Rec Closed rl pf) →
data_type (drec dl) (Rec k rl pf).
Lemma dtbrand_inv b b' d :
data_type (dbrand b d) (Brand b') →
is_canon_brands brand_relation_brands b ∧
data_normalized brand_relation_brands d ∧
Forall (fun bb ⇒
∀ τ,
lookup string_dec brand_context_types bb = Some τ →
data_type d τ
) b ∧
b ≤ b'.
Lemma dtbrand_refl {b d}:
is_canon_brands brand_relation_brands b →
data_normalized brand_relation_brands d →
Forall (fun bb ⇒
∀ τ,
lookup string_dec brand_context_types bb = Some τ →
data_type d τ
) b →
data_type (dbrand b d) (Brand b).
Lemma data_type_ext d τ₀ pf1 pf2:
d ▹ (exist _ τ₀ pf1) ↔ d ▹ (exist _ τ₀ pf2).
Lemma data_type_fequal d τ₁ τ₂:
(proj1_sig τ₁) = (proj1_sig τ₂) →
(d ▹ τ₁ ↔ d ▹ τ₂).
Lemma data_type_not_bottom {d} : d ▹ ⊥ → False.
Section inv.
Lemma data_type_dunit_inv {τ}:
isTop τ = false →
dunit ▹ τ → τ = Unit.
Lemma data_type_dnat_inv {n τ}:
isTop τ = false →
dnat n ▹ τ → τ = Nat.
Lemma data_type_dbool_inv {b τ}:
isTop τ = false →
dbool b ▹ τ → τ = Bool.
Lemma data_type_dstring_inv {s τ}:
isTop τ = false →
dstring s ▹ τ → τ = String.
Lemma data_type_dcoll_inv {d τ}:
isTop τ = false →
dcoll d ▹ τ →
{τ' | τ = Coll τ'}.
Lemma data_type_drec_inv {sdl τ}:
isTop τ = false →
drec sdl ▹ τ →
{k : record_kind & {τ' | ∃ pf, τ = Rec k τ' pf}}.
Lemma data_type_dleft_inv {d τ} :
isTop τ = false →
dleft d ▹ τ →
{τl : rtype & {τr | τ = Either τl τr}}.
Lemma data_type_dright_inv {d τ} :
isTop τ = false →
dright d ▹ τ →
{τl : rtype & {τr | τ = Either τl τr}}.
Lemma data_type_dsome_inv {d τ} :
isTop τ = false →
dsome d ▹ τ →
{τl : rtype & {τr | τ = Either τl τr}}.
Lemma data_type_dnone_inv {τ} :
isTop τ = false →
dnone ▹ τ →
{τl : rtype & {τr | τ = Either τl τr}}.
Lemma data_type_Unit_inv {d}:
d ▹ Unit →
d = dunit.
Lemma data_type_Nat_inv {d}:
d ▹ Nat →
{n | d = dnat n}.
Lemma data_type_Bool_inv {d}:
d ▹ Bool →
{b | d = dbool b}.
Lemma data_type_String_inv {d}:
d ▹ String →
{s | d = dstring s}.
Lemma data_type_Col_inv {d τ}:
d ▹ Coll τ →
{dl | d = dcoll dl}.
Lemma Col_inv {d τ}:
dcoll d ▹ Coll τ →
Forall (fun c ⇒ c ▹ τ) d.
Lemma data_type_Rec_inv {d k τ pf} :
d ▹ Rec k τ pf →
{dl | d = drec dl}.
Lemma data_type_Arrow_inv {d τin τout}:
d ▹ Arrow τin τout →
False.
Lemma data_type_Foreign_inv {d ft}:
d ▹ Foreign ft →
{fd | d = dforeign fd}.
Lemma data_type_Either_inv {d τl τr}:
d ▹ Either τl τr →
{dl | d = dleft dl ∧ dl ▹ τl} + {dr | d = dright dr ∧ dr ▹ τr}.
Lemma data_type_Option_inv {d τ}:
d ▹ Option τ →
{ds | d = dsome ds ∧ ds ▹ τ} + {d = dnone}.
Lemma data_type_Brand_inv {d br} :
d ▹ Brand br →
{bs:brands & {d' | d = dbrand bs d'}}.
End inv.
Inversion tactic for typed data
Lemma data_type_Rec_sublist {r k l l' pf} pf' :
drec r ▹ Rec k l pf →
sublist l' l →
drec r ▹ Rec Open l' pf'.
Lemma sorted_forall_same_domain {dl τ}:
Forall2 (fun (d : string × data) (r : string × rtype) ⇒
fst d = fst r ∧ data_type (snd d) (snd r)) dl τ →
(domain dl) = (domain τ).
Lemma data_type_Rec_domain {r k l pf} :
drec r ▹ Rec k l pf →
sublist (domain l) (domain r).
Lemma data_type_Rec_closed_domain {r l pf} :
drec r ▹ Rec Closed l pf →
domain r = domain l.
Lemma data_type_Recs_domain {r k l pf l' pf'} :
drec r ▹ Rec k l pf →
drec r ▹ Rec Closed l' pf' →
sublist (domain l) (domain l').
Lemma data_type_Recs_closed_domain {r l l' pf pf'} :
drec r ▹ Rec Closed l pf →
drec r ▹ Rec Closed l' pf' →
domain l = domain l'.
Lemma dtrec_edot_parts a k τ pf s x y:
drec a ▹ Rec k τ pf →
edot a s = Some x →
edot τ s = Some y →
x ▹ y.
Lemma coll_type_cons a c x:
dcoll (a :: c) ▹ Coll x →
a ▹ x ∧ dcoll c ▹ Coll x.
Lemma dcoll_coll_in_inv {d τ a} :
In a d → dcoll d ▹ Coll τ → a ▹ τ.
Lemma rec_type_closed_cons {x y l l' pf} pf':
drec (x :: l) ▹ Rec Closed (y :: l') pf →
(snd x) ▹ (snd y) ∧ drec l ▹ Rec Closed l' pf'.
Lemma rec_type_cons {k x y l l' pf} pf':
drec (x :: l) ▹ Rec k (y :: l') pf →
((fst x) = (fst y) ∧ (snd x) ▹ (snd y) ∧ drec l ▹ Rec k l' pf')
∨ ((fst x) ≠ (fst y) ∧ drec l ▹ Rec k (y::l') pf).
Lemma sorted_forall_sorted (dl:list (string×data)) (τ:list (string×rtype)):
is_list_sorted ODT_lt_dec (domain τ) = true →
Forall2 (fun (d : string × data) (r : string × rtype) ⇒
fst d = fst r ∧ data_type (snd d) (snd r)) dl τ →
is_list_sorted ODT_lt_dec (domain dl) = true.
Lemma insert_and_foralls_mean_same_sort l1 l2 τ₁ τ₂ x y:
is_list_sorted ODT_lt_dec (domain (rec_sort (τ₁ ++ τ₂))) = true →
Forall2
(fun (d : string × data) (r : string × rtype) ⇒
fst d = fst r ∧ data_type (snd d) (snd r))
(rec_sort (l1 ++ l2)) (rec_sort (τ₁ ++ τ₂)) →
(fst x = fst y) →
is_list_sorted
ODT_lt_dec
(domain
(insertion_sort_insert rec_field_lt_dec y (rec_sort (τ₁ ++ τ₂)))) = true →
is_list_sorted
ODT_lt_dec
(domain
(insertion_sort_insert rec_field_lt_dec x (rec_sort (l1 ++ l2)))) = true.
Lemma sorted_cons_skip {A} (l:list (string×A)) (x x0:string×A) :
is_list_sorted
ODT_lt_dec
(domain (rec_cons_sort x (x0 :: l))) = true
→ is_list_sorted
ODT_lt_dec
(domain (rec_cons_sort x l)) = true.
Lemma Forall2_cons_sorted l1 l2 x y :
Forall2
(fun (d : string × data) (r : string × rtype) ⇒
fst d = fst r ∧ data_type (snd d) (snd r))
l1 l2 →
is_list_sorted ODT_lt_dec
(domain
(insertion_sort_insert rec_field_lt_dec x l1)) =
true →
is_list_sorted ODT_lt_dec
(domain
(insertion_sort_insert rec_field_lt_dec y l2)) =
true → fst x = fst y → data_type (snd x) (snd y) →
Forall2
(fun (d : string × data) (r : string × rtype) ⇒
fst d = fst r ∧ data_type (snd d) (snd r))
(insertion_sort_insert rec_field_lt_dec x l1)
(insertion_sort_insert rec_field_lt_dec y l2).
Lemma dtrec_rec_concat_sort {x xt pfx y yt pfy} pxyt :
drec x ▹ Rec Closed xt pfx →
drec y ▹ Rec Closed yt pfy →
drec (rec_concat_sort x y) ▹ Rec Closed (rec_concat_sort xt yt) pxyt.
Lemma dttop' d : data_normalized brand_relation_brands d → d ▹ ⊤.
Lemma Forall_map {A B} P (f:A→B) l :
Forall P (map f l) ↔ Forall (fun x ⇒ P (f x)) l.
Well typed data must be normalized
Lemma showing that normalization preserves typing
Lemma normalize_preserves_type d τ :
d ▹ τ → normalize_data brand_relation_brands d ▹ τ.
Lemma dttop_weaken {d τ} : data_type d τ → data_type d ⊤.
End TData.
Notation "d ▹ r" := (data_type d r) (at level 70).
Section rmap.
Context {fdata:foreign_data}.
Context {ftype:foreign_type}.
Context {fdtyping:foreign_data_typing}.
Context {m:brand_model}.
Lemma rmap_concat_empty_right τ pf l:
Forall (fun d : data ⇒ d ▹ Rec Closed τ pf) l →
(rmap_concat (fun _ : data ⇒ Some (dcoll (drec nil :: nil))) l) = Some l.
Lemma rmap_concat_empty_left τ pf l:
Forall (fun d : data ⇒ d ▹ Rec Closed τ pf) l →
(rmap_concat (fun _ : data ⇒ Some (dcoll l)) (drec nil::nil)) = Some l.
End rmap.
Section subtype.
Lemma subtype_Rec_sublist_strengthen
{fdata:foreign_data}
{ftype:foreign_type}
{fdtyping:foreign_data_typing}
{m:brand_model} {dl rl srl k1 pf srl0 pf0 k2} :
∀ (f2:Forall2
(fun (d : string × data) (r : string × rtype) ⇒
fst d = fst r ∧ data_type (snd d) (snd r)) dl rl)
(subl:sublist srl rl)
(subt:Rec k1 srl pf <: Rec k2 srl0 pf0)
(pf3:is_list_sorted ODT_lt_dec (domain rl) = true)
(ft:Forallt
(fun ab : string × rtype ⇒
∀ (d : data) (τ₂ : rtype),
snd ab <: τ₂ → data_type d (snd ab) → data_type d τ₂) srl),
∃ l2,
Forall2
(fun (d : string × data) (r : string × rtype) ⇒
fst d = fst r ∧ data_type (snd d) (snd r)) dl l2
∧
sublist srl0 l2.
Global Instance data_type_subtype_prop
{fdata:foreign_data}
{ftype:foreign_type}
{fdtyping:foreign_data_typing}
{m:brand_model} : Proper (eq ==> subtype ==> impl) (data_type).
Global Instance data_type_subtype_prop'
{fdata:foreign_data}
{ftype:foreign_type}
{fdtyping:foreign_data_typing}
{m:brand_model} d : Proper (subtype ==> impl) (data_type d).
Lemma join_preserves_data_type
{fdata:foreign_data}
{ftype:foreign_type}
{fdtyping:foreign_data_typing}
{m:brand_model} {d τ}:
d ▹ τ → ∀ τ₀, d ▹ (τ ⊔ τ₀).
Theorem subtyping_preserves_data_type
{fdata:foreign_data}
{ftype:foreign_type}
{fdtyping:foreign_data_typing}
{m:brand_model} {d τ₁ τ₂}:
d ▹ τ₁ → τ₁ ≤ τ₂ → d ▹ τ₂.
Lemma map_rtype_meet_cons2_nin
{ftype:foreign_type}
{br:brand_relation} s x l1 l2 :
¬ In s (domain l1) →
map_rtype_meet l1 ((s, x) :: l2)
= map_rtype_meet l1 l2.
Lemma lookup_diff_cons2_nin {A B C} dec s x (l1:list (A×B)) (l2:list (A×C)) :
¬ In s (domain l1) →
lookup_diff dec l1 ((s, x) :: l2)
= lookup_diff dec l1 l2.
Lemma lookup_diff_sublist {A B C} (dec:∀ a a':A, {a=a'} + {a≠a'})
(l1:list (A×B)) (l2:list (A×C)):
sublist (lookup_diff dec l1 l2) l1.
Theorem meet_preserves_data_type
{fdata:foreign_data}
{ftype:foreign_type}
{fdtyping:foreign_data_typing}
{m:brand_model} {d τ₁ τ₂}:
d ▹ τ₁ → d ▹ τ₂ → d ▹ (τ₁ ⊓ τ₂).
Theorem meet_data_type_iff
{fdata:foreign_data}
{ftype:foreign_type}
{fdtyping:foreign_data_typing}
{m:brand_model} d τ₁ τ₂:
d ▹ (τ₁ ⊓ τ₂) ↔ (d ▹ τ₁ ∧ d ▹ τ₂).
Lemma brands_type_Forall
{fdata:foreign_data}
{ftype:foreign_type}
{fdtyping:foreign_data_typing}
{m:brand_model} d b :
d ▹ (brands_type b)
↔
(data_normalized brand_relation_brands d ∧
Forall (fun bb ⇒
∀ τ,
lookup string_dec brand_context_types bb = Some τ →
d ▹ τ
) b).
Lemma dtbrand'
{fdata:foreign_data}
{ftype:foreign_type}
{fdtyping:foreign_data_typing}
{m:brand_model} b b' d:
is_canon_brands brand_relation_brands b →
d ▹ (brands_type b) →
b ≤ b' →
data_type (dbrand b d) (Brand b').
Lemma dtbrand'_inv
{fdata:foreign_data}
{ftype:foreign_type}
{fdtyping:foreign_data_typing}
{m:brand_model} b b' d:
data_type (dbrand b d) (Brand b') →
is_canon_brands brand_relation_brands b ∧
d ▹ (brands_type b) ∧
b ≤ b'.
End subtype.
d ▹ τ → normalize_data brand_relation_brands d ▹ τ.
Lemma dttop_weaken {d τ} : data_type d τ → data_type d ⊤.
End TData.
Notation "d ▹ r" := (data_type d r) (at level 70).
Section rmap.
Context {fdata:foreign_data}.
Context {ftype:foreign_type}.
Context {fdtyping:foreign_data_typing}.
Context {m:brand_model}.
Lemma rmap_concat_empty_right τ pf l:
Forall (fun d : data ⇒ d ▹ Rec Closed τ pf) l →
(rmap_concat (fun _ : data ⇒ Some (dcoll (drec nil :: nil))) l) = Some l.
Lemma rmap_concat_empty_left τ pf l:
Forall (fun d : data ⇒ d ▹ Rec Closed τ pf) l →
(rmap_concat (fun _ : data ⇒ Some (dcoll l)) (drec nil::nil)) = Some l.
End rmap.
Section subtype.
Lemma subtype_Rec_sublist_strengthen
{fdata:foreign_data}
{ftype:foreign_type}
{fdtyping:foreign_data_typing}
{m:brand_model} {dl rl srl k1 pf srl0 pf0 k2} :
∀ (f2:Forall2
(fun (d : string × data) (r : string × rtype) ⇒
fst d = fst r ∧ data_type (snd d) (snd r)) dl rl)
(subl:sublist srl rl)
(subt:Rec k1 srl pf <: Rec k2 srl0 pf0)
(pf3:is_list_sorted ODT_lt_dec (domain rl) = true)
(ft:Forallt
(fun ab : string × rtype ⇒
∀ (d : data) (τ₂ : rtype),
snd ab <: τ₂ → data_type d (snd ab) → data_type d τ₂) srl),
∃ l2,
Forall2
(fun (d : string × data) (r : string × rtype) ⇒
fst d = fst r ∧ data_type (snd d) (snd r)) dl l2
∧
sublist srl0 l2.
Global Instance data_type_subtype_prop
{fdata:foreign_data}
{ftype:foreign_type}
{fdtyping:foreign_data_typing}
{m:brand_model} : Proper (eq ==> subtype ==> impl) (data_type).
Global Instance data_type_subtype_prop'
{fdata:foreign_data}
{ftype:foreign_type}
{fdtyping:foreign_data_typing}
{m:brand_model} d : Proper (subtype ==> impl) (data_type d).
Lemma join_preserves_data_type
{fdata:foreign_data}
{ftype:foreign_type}
{fdtyping:foreign_data_typing}
{m:brand_model} {d τ}:
d ▹ τ → ∀ τ₀, d ▹ (τ ⊔ τ₀).
Theorem subtyping_preserves_data_type
{fdata:foreign_data}
{ftype:foreign_type}
{fdtyping:foreign_data_typing}
{m:brand_model} {d τ₁ τ₂}:
d ▹ τ₁ → τ₁ ≤ τ₂ → d ▹ τ₂.
Lemma map_rtype_meet_cons2_nin
{ftype:foreign_type}
{br:brand_relation} s x l1 l2 :
¬ In s (domain l1) →
map_rtype_meet l1 ((s, x) :: l2)
= map_rtype_meet l1 l2.
Lemma lookup_diff_cons2_nin {A B C} dec s x (l1:list (A×B)) (l2:list (A×C)) :
¬ In s (domain l1) →
lookup_diff dec l1 ((s, x) :: l2)
= lookup_diff dec l1 l2.
Lemma lookup_diff_sublist {A B C} (dec:∀ a a':A, {a=a'} + {a≠a'})
(l1:list (A×B)) (l2:list (A×C)):
sublist (lookup_diff dec l1 l2) l1.
Theorem meet_preserves_data_type
{fdata:foreign_data}
{ftype:foreign_type}
{fdtyping:foreign_data_typing}
{m:brand_model} {d τ₁ τ₂}:
d ▹ τ₁ → d ▹ τ₂ → d ▹ (τ₁ ⊓ τ₂).
Theorem meet_data_type_iff
{fdata:foreign_data}
{ftype:foreign_type}
{fdtyping:foreign_data_typing}
{m:brand_model} d τ₁ τ₂:
d ▹ (τ₁ ⊓ τ₂) ↔ (d ▹ τ₁ ∧ d ▹ τ₂).
Lemma brands_type_Forall
{fdata:foreign_data}
{ftype:foreign_type}
{fdtyping:foreign_data_typing}
{m:brand_model} d b :
d ▹ (brands_type b)
↔
(data_normalized brand_relation_brands d ∧
Forall (fun bb ⇒
∀ τ,
lookup string_dec brand_context_types bb = Some τ →
d ▹ τ
) b).
Lemma dtbrand'
{fdata:foreign_data}
{ftype:foreign_type}
{fdtyping:foreign_data_typing}
{m:brand_model} b b' d:
is_canon_brands brand_relation_brands b →
d ▹ (brands_type b) →
b ≤ b' →
data_type (dbrand b d) (Brand b').
Lemma dtbrand'_inv
{fdata:foreign_data}
{ftype:foreign_type}
{fdtyping:foreign_data_typing}
{m:brand_model} b b' d:
data_type (dbrand b d) (Brand b') →
is_canon_brands brand_relation_brands b ∧
d ▹ (brands_type b) ∧
b ≤ b'.
End subtype.