Qcert.NRAEnv.Typing.TNRAEnv

Section TNRAEnv.

Typing for NRA

  Section typ.
    Context {m:basic_model}.
    Context (τconstants:list (string ×rtype)).
    Definition nraenv_type (q:nraenv) : rtype → rtype → rtype → Prop :=
      @cnraenv_type m τ constants (cnraenv_of_nraenv q).

  End typ.

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

Type lemmas for individual algebraic expressions

Section prop.
Context {m:basic_model}.

Main typing soundness theorem for the NRA

    Lemma typed_nraenv_yields_typed_cnraenv {τc τenv τin τout} (op:nraenv):
      (op ▷ₓ τin >=> τ out ⊣ τ c ;τ env ) → cnraenv_type τ c (cnraenv_of_nraenv op) τ env τin τ out.

    Lemma typed_cnraenv_yields_typed_nraenv {τc τenv τin τout} (op:nraenv):
      cnraenv_type τ c (cnraenv_of_nraenv op) τ env τin τ out → (op ▷ₓ τin >=> τ out ⊣ τ c ;τ env ).

    Theorem typed_cnraenv_iff_typed_nraenv {τc τenv τin τout} (op:nraenv):
      (op ▷ₓ τin >=> τ out ⊣ τ c ;τ env ) ↔ cnraenv_type τ c (cnraenv_of_nraenv op) τ env τin τ out.

    Theorem typed_nraenv_yields_typed_data {τc τenv τin τout} c (env:data) (d:data) (op:nraenv):
      bindings_type c τ c →
      (env ▹ τ env ) → (d ▹ τin) → (op ▷ₓ τin >=> τ out ⊣ τ c ;τ env ) →
      (∃ x, (nraenv_eval brand_relation_brands c op env d = Some x ∧ (x ▹ τ out ))).

Corrolaries of the main type soudness theorem

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

    Definition tnraenv_eval {τc τenv τin τout} (op:nraenv) (HOpT: op ▷ₓ τin >=> τ out ⊣ τ c ;τ env) c (env:data) (d:data):
      bindings_type c τ c →
      (env ▹ τ env ) → (d ▹ τin) → data.
  End prop.

End TNRAEnv.

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