Qcert.NRAEnv.Typing.TcNRAEnv

Section TcNRAEnv.

Typing for NRA

  Section typ.
    Context {m:basic_model}.
    Context (τconstants:tbindings).

  Inductive cnraenv_type : cnraenv → rtype → rtype → rtype → Prop :=
  | ANTID {τenv τ} :
      cnraenv_type ANID τ env τ τ
  | ANTConst {τenv τin τout} c :
      data_type (normalize_data brand_relation_brands c) τ out → cnraenv_type (ANConst c) τ env τin τ out
  | ANTBinop {τenv τin τ₁ τ₂ τout} b op1 op2 :
      binOp_type b τ ₁ τ ₂ τ out →
      cnraenv_type op1 τ env τin τ ₁ →
      cnraenv_type op2 τ env τin τ ₂ →
      cnraenv_type (ANBinop b op1 op2) τ env τin τ out
  | ANTUnop {τenv τin τ τout} u op :
      unaryOp_type u τ τ out →
      cnraenv_type op τ env τin τ →
      cnraenv_type (ANUnop u op) τ env τin τ out
  | ANTMap {τenv τin τ₁ τ₂} op1 op2 :
      cnraenv_type op1 τ env τ ₁ τ ₂ →
      cnraenv_type op2 τ env τin (Coll τ ₁) →
      cnraenv_type (ANMap op1 op2) τ env τin (Coll τ ₂)
  | ANTMapConcat {τenv τin τ₁ τ₂ τ₃} op1 op2 pf1 pf2 pf3 :
      cnraenv_type op1 τ env (Rec Closed τ ₁ pf1) (Coll (Rec Closed τ ₂ pf2)) →
      cnraenv_type op2 τ env τin (Coll (Rec Closed τ ₁ pf1)) →
      rec_concat_sort τ ₁ τ ₂ = τ ₃ →
      cnraenv_type (ANMapConcat op1 op2) τ env τin (Coll (Rec Closed τ ₃ pf3))
  | ANTProduct {τenv τin τ₁ τ₂ τ₃} op1 op2 pf1 pf2 pf3 :
      cnraenv_type op1 τ env τin (Coll (Rec Closed τ ₁ pf1)) →
      cnraenv_type op2 τ env τin (Coll (Rec Closed τ ₂ pf2)) →
      rec_concat_sort τ ₁ τ ₂ = τ ₃ →
      cnraenv_type (ANProduct op1 op2) τ env τin (Coll (Rec Closed τ ₃ pf3))
  | ANTSelect {τenv τin τ} op1 op2 :
      cnraenv_type op1 τ env τ Bool →
      cnraenv_type op2 τ env τin (Coll τ) →
      cnraenv_type (ANSelect op1 op2) τ env τin (Coll τ)
  | ANTDefault {τenv τin τ} op1 op2 :
      cnraenv_type op1 τ env τin (Coll τ) →
      cnraenv_type op2 τ env τin (Coll τ) →
      cnraenv_type (ANDefault op1 op2) τ env τin (Coll τ)
  | ANTEither {τenv τl τr τout} opl opr :
      cnraenv_type opl τ env τ l τ out →
      cnraenv_type opr τ env τ r τ out →
      cnraenv_type (ANEither opl opr) τ env (Either τ l τ r) τ out
  | ANTEitherConcat {τenv τin rll pfl rlr pfr rlo pfo lo ro} op1 op2 pflo pfro :
      cnraenv_type op1 τ env τin (Either (Rec Closed rll pfl) (Rec Closed rlr pfr)) →
      cnraenv_type op2 τ env τin (Rec Closed rlo pfo) →
      rec_concat_sort rll rlo = lo →
      rec_concat_sort rlr rlo = ro →
      cnraenv_type (ANEitherConcat op1 op2) τ env τin (Either (Rec Closed lo pflo) (Rec Closed ro pfro))
  | ANTApp {τenv τin τ1 τ2} op2 op1 :
      cnraenv_type op1 τ env τin τ1 →
      cnraenv_type op2 τ env τ1 τ2 →
      cnraenv_type (ANApp op2 op1) τ env τin τ2
  | ANTGetConstant {τenv τin τout} s :
      tdot τ constants s = Some τ out →
      cnraenv_type (ANGetConstant s) τ env τin τ out
  | ANTEnv {τenv τin} :
      cnraenv_type ANEnv τ env τin τ env
  | ANTAppEnv {τenv τenv' τin τ2} op2 op1 :
      cnraenv_type op1 τ env τin τ env' →
      cnraenv_type op2 τ env' τin τ2 →
      cnraenv_type (ANAppEnv op2 op1) τ env τin τ2
  | ANTMapEnv {τenv τin τ₂} op1 :
      cnraenv_type op1 τ env τin τ ₂ →
      cnraenv_type (ANMapEnv op1) (Coll τ env) τin (Coll τ ₂).
  End typ.

  Notation "Op ▷ A >=> B ⊣ C ; E" := (cnraenv_type C Op E A B) (at level 70).

Type lemmas for individual cnraenvebraic expressions

  Context {m:basic_model}.

  Lemma rmap_typed {τc} {τenv τ₁ τ₂ : rtype} c (op1 : cnraenv) (env:data) (dl : list data) :
    (bindings_type c τ c ) →
    (env ▹ τ env ) →
    (Forall (fun d : data ⇒ data_type d τ ₁) dl ) →
    (op1 ▷ τ ₁ >=> τ ₂ ⊣ τ c ; τ env ) →
    (∀ d : data,
       data_type d τ ₁ → ∃ x : data , brand_relation_brands ⊢ₑ op1 @ₑ d ⊣ c ; env = Some x ∧ x ▹ τ ₂ ) →
    ∃ x : list data , (rmap (cnraenv_eval brand_relation_brands c op1 env) dl = Some x ) ∧ data_type (dcoll x) (Coll τ ₂).

  Lemma rmap_env_typed {τc} {τenv τ₁ τ₂ : rtype} c (op1 : cnraenv) (x0:data) (dl : list data) :
    bindings_type c τ c →
    (x0 ▹ τ ₁ ) →
    (Forall (fun d : data ⇒ data_type d τ env) dl ) →
    (op1 ▷ τ ₁ >=> τ ₂ ⊣ τ c ;τ env ) →
    (∀ env : data,
       data_type env τ env →
       ∀ d : data,
         data_type d τ ₁ →
         ∃ x : data , brand_relation_brands ⊢ₑ op1 @ₑ d ⊣ c ;env = Some x ∧ data_type x τ ₂ ) →
    ∃ x : list data , (rmap (fun env' ⇒ (cnraenv_eval brand_relation_brands c op1 env' x0)) dl = Some x ) ∧ data_type (dcoll x) (Coll τ ₂).

  Lemma recover_rec k d r τ pf:
    data_type d r →
    ` r =
    Rec₀ k
      (map
         (fun x : string × {τ₀ : rtype₀ | wf_rtype₀ τ₀ = true } ⇒
            (fst x , ` (snd x ))) τ) →
    data_type d (Rec k τ pf).

  Lemma recover_rec_forall k l r τ pf:
    Forall (fun d : data ⇒ data_type d r) l →
    ` r =
    Rec₀ k
      (map
         (fun x : string × {τ₀ : rtype₀ | wf_rtype₀ τ₀ = true } ⇒
            (fst x , ` (snd x ))) τ) →
    Forall (fun d : data ⇒ data_type d (Rec k τ pf)) l.

  Lemma omap_concat_typed_env
        (τenv:rtype) (τ₁ τ₂ τ₃: list (string × rtype)) (env:data) (dl2: list data)
        (x : list (string × data)) pf1 pf2 pf3:
    (data_type env τ env ) →
    (∀ x : data, In x dl2 → data_type x (Rec Closed τ ₂ pf2)) →
    rec_concat_sort τ ₁ τ ₂ = τ ₃ →
    data_type (drec x) (Rec Closed τ ₁ pf1) →
    (∃ y : list data ,
       rmap (fun x1 : data ⇒ orecconcat (drec x) x1) dl2
       = Some y ∧ data_type (dcoll y) (Coll (Rec Closed τ ₃ pf3))).

  Lemma rproduct_typed_env {τenv:rtype} {τ₁ τ₂ τ₃: list (string × rtype)} (env:data) (dl dl0: list data) pf1 pf2 pf3:
    data_type env τ env →
    Forall (fun d : data ⇒ data_type d (Rec Closed τ ₂ pf2)) dl0 →
    Forall (fun d : data ⇒ data_type d (Rec Closed τ ₁ pf1)) dl →
    rec_concat_sort τ ₁ τ ₂ = τ ₃ →
    ∃ x : list data , (rproduct dl dl0 = Some x ) ∧ data_type (dcoll x) (Coll (Rec Closed τ ₃ pf3)).

  Lemma data_type_concat l1 l2 τ:
    data_type (dcoll l1) (Coll τ) →
    data_type (dcoll l2) (Coll τ) →
    data_type (dcoll (l1 ++ l2)) (Coll τ).

  Lemma rmap_concat_typed_env {τc} {τenv:rtype} {τ₁ τ₂ τ₃ : list (string × rtype)} (op1 : cnraenv) c (env:data) (dl: list data) pf1 pf2 pf3:
    bindings_type c τ c →
    env ▹ τ env →
    rec_concat_sort τ ₁ τ ₂ = τ ₃ →
    Forall (fun d : data ⇒ data_type d (Rec Closed τ ₁ pf1)) dl →
    (op1 ▷ Rec Closed τ ₁ pf1 >=> Coll (Rec Closed τ ₂ pf2) ⊣ τ c ;τ env ) →
    (∀ d : data,
                data_type d (Rec Closed τ ₁ pf1) →
                ∃ x : data ,
                   brand_relation_brands ⊢ₑ op1 @ₑ d ⊣ c ;env = Some x ∧ data_type x (Coll (Rec Closed τ ₂ pf2))) →
    ∃ x : list data , (rmap_concat (cnraenv_eval brand_relation_brands c op1 env) dl = Some x ) ∧ data_type (dcoll x) (Coll (Rec Closed τ ₃ pf3)).

  Lemma rmap_concat_typed2_env {τc} {τenv:rtype} {τ₁ τ₂ τ₃ : list (string × rtype)} τin c (op1 : cnraenv) (env:data) y (dl: list data) pf1 pf2 pf3:
    bindings_type c τ c →
    env ▹ τ env →
    rec_concat_sort τ ₁ τ ₂ = τ ₃ →
    Forall (fun d : data ⇒ data_type d (Rec Closed τ ₁ pf1)) dl →
    (op1 ▷ τin >=> Coll (Rec Closed τ ₂ pf2) ⊣ τ c ;τ env ) →
    (∀ d : data,
                data_type d (Rec Closed τ ₁ pf1) →
                ∃ x : data ,
                   brand_relation_brands ⊢ₑ op1 @ₑ y ⊣ c ;env = Some x ∧ data_type x (Coll (Rec Closed τ ₂ pf2))) →
    ∃ x : list data , (rmap_concat (fun z ⇒ brand_relation_brands ⊢ₑ op1@ₑ y ⊣ c ;env) dl = Some x ) ∧ data_type (dcoll x) (Coll (Rec Closed τ ₃ pf3)).

Main typing soundness theorem for NRAEnv

  Theorem typed_cnraenv_yields_typed_data {τc} {τenv τin τout} c (env:data) (d:data) (op:cnraenv):
    bindings_type c τ c →
    (env ▹ τ env ) → (d ▹ τin) → (op ▷ τin >=> τ out ⊣ τ c ;τ env ) →
    (∃ x, (brand_relation_brands ⊢ₑ op @ₑ d ⊣ c ;env = Some x ∧ (x ▹ τ out ))).

Corrolaries of the main type soudness theorem

  Definition typed_cnraenv_total {τc} {τenv τin τout} (op:cnraenv) (HOpT: op ▷ τin >=> τ out ⊣ τ c ;τ env) c (env:data) (d:data)
    (dt_c: bindings_type c τ c) :
    (env ▹ τ env ) →
    (d ▹ τin) →
    { x:data | x ▹ τ out }.

  Definition tcnraenv_eval {τc} {τenv τin τout} (op:cnraenv) (HOpT: op ▷ τin >=> τ out ⊣ τ c ;τ env) c (env:data) (d:data)
             (dt_c: bindings_type c τ c) :
    (env ▹ τ env ) → (d ▹ τin) → data.

Auxiliary lemmas specific to some of the NRA expressions used in the translation

  Definition pat_context_type tconst tbind tpid : rtype :=
    Rec Closed (("PBIND"%string,tbind ) :: ("PCONST"%string,tconst ) :: ("PDATA"%string,tpid ) :: nil) (eq_refl _).

  Lemma ATdot {p s τin τ pf τout}:
      p ▷ τin >=> Rec Closed τ pf →
      tdot τ s = Some τ out →
      AUnop (ADot s) p ▷ τin >=> τ out.

  Lemma ATdot_inv {p s τin τout}:
      AUnop (ADot s) p ▷ τin >=> τ out →
      ∃ τ pf k,
      p ▷ τin >=> Rec k τ pf ∧
      tdot τ s = Some τ out.

  Lemma ATpat_data τc τ τin :
    pat_data ▷ pat_context_type τ c τ τin >=> τin.

  Lemma ATpat_data_inv' k τc τ τin pf τout:
      pat_data ▷ Rec k [("PBIND"%string, τ ); ("PCONST"%string, τ c ); ("PDATA"%string, τin)] pf >=> τ out →
      τin = τ out.

  Lemma ATpat_data_inv τc τ τin τout:
    pat_data ▷ pat_context_type τ c τ τin >=> τ out →
    τin = τ out.

  Lemma ATunnest_two (s1 s2:string) (op:NRA.nra) τin τ₁ pf1 τs τrem pf2 :
    op ▷ τin >=> (Coll (Rec Closed τ ₁ pf1)) →
    tdot τ ₁ s1 = Some (Coll τ s) →
    τ rem = (rremove (rec_concat_sort τ ₁ ((s2 ,τ s )::nil)) s1 ) →
    NRAExt.unnest_two s1 s2 op ▷
               τin >=> Coll (Rec Closed τ rem pf2).

  Lemma ATunnest_two_inv (s1 s2:string) (op:NRA.nra) τin rec :
    unnest_two s1 s2 op ▷
                       τin >=> Coll rec →
    ∃ τ₁ pf1 τs τrem pf2,
    op ▷ τin >=> (Coll (Rec Closed τ ₁ pf1)) ∧
    tdot τ ₁ s1 = Some (Coll τ s) ∧
    rec = (Rec Closed τ rem pf2 ) ∧
    τ rem = (rremove (rec_concat_sort τ ₁ ((s2 ,τ s )::nil)) s1 ).

    Lemma ATRecEither s τl τr pf1 pf2:
      nra_type (ARecEither s) (Either τ l τ r)
               (Either
                  (Rec Closed ((s ,τ l )::nil) pf1)
                  (Rec Closed ((s ,τ r )::nil) pf2)).

    Theorem typed_cnraenv_to_typed_nra {τc} pf {τenv τin τout} (op:cnraenv):
    (cnraenv_type τ c op τ env τin τ out ) → (nra_type (nra_of_cnraenv op) (pat_context_type (Rec Closed τ c pf) τ env τin) τ out ).

  Lemma fold_pat_context_type (c env d: {τ₀ : rtype₀ | wf_rtype₀ τ₀ = true }) pf :
    Rec Closed [("PBIND"%string, env ); ("PCONST"%string, c ); ("PDATA"%string, d )] pf
    = pat_context_type c env d.

      Lemma UIP_bool {a b:bool} (pf1 pf2:a = b) : pf1 = pf2.

  Lemma typed_cnraenv_to_typed_nra_inv' {k τc pf0 τenv τin τout pf} (op:cnraenv):
    nra_type (nra_of_cnraenv op) (Rec k [("PBIND"%string, τ env ); ("PCONST"%string, (Rec Closed τ c pf0 )); ("PDATA"%string, τin)] pf) τ out →
    cnraenv_type τ c op τ env τin τ out.

  Theorem typed_cnraenv_to_typed_nra_inv {τc} pf {τenv τin τout} (op:cnraenv):
    nra_type (nra_of_cnraenv op) (pat_context_type (Rec Closed τ c pf) τ env τin) τ out →
    cnraenv_type τ c op τ env τin τ out.

  Lemma typed_cnraenv_const_sort_f {τc op τenv τin τout} :
    cnraenv_type (rec_sort τ c) op τ env τin τ out →
    cnraenv_type τ c op τ env τin τ out.

  Lemma typed_cnraenv_const_sort_b {τc op τenv τin τout} :
      cnraenv_type τ c op τ env τin τ out →
      cnraenv_type (rec_sort τ c) op τ env τin τ out.

  Lemma typed_cnraenv_const_sort τc op τenv τin τout :
    cnraenv_type (rec_sort τ c) op τ env τin τ out ↔
    cnraenv_type τ c op τ env τin τ out.

End TcNRAEnv.

Notation "Op ▷ A >=> B ⊣ C ; E" := (cnraenv_type C Op E A B) (at level 70).
Notation "Op @▷ d ⊣ C ; e" := (tcnraenv_eval C Op e d) (at level 70).