Module Qcert.NRA.Typing.TNRAExt


Require Import String.
Require Import List.
Require Import Compare_dec.
Require Import DataSystem.
Require Import NRAExt.
Require Import TNRA.

Section TNRAExt.
  Local Open Scope nraext_scope.
  
Typing for NRA

  Context {m:basic_model}.

  Definition nraext_type Op C A B := nra_type C (nra_of_nraext Op) A B.

  Notation "OpA >=> BC" := (nraext_type Op C A B) (at level 70) : nraext_scope.

Main typing soundness theorem for the Extended NRA

  Theorem typed_nraext_yields_typed_datac} {τin τout} (d:data) c (op:nraext):
    (bindings_type c τc) ->
    (d ▹ τin) -> (op ▷ τin >=> τout ⊣ τc) ->
    (exists x, (brand_relation_brandsop @ₓ dc = Some x /\ (x ▹ τout))).
Proof.
    unfold nraext_eval, nraext_type; intros.
    apply (@typed_nra_yields_typed_data m τc τin τout); assumption.
  Qed.

Corrolaries of the main type soudness theorem

  Definition typed_nraext_totalc} {τin τout} (op:nraext) (d:data) c :
    (bindings_type c τc) ->
    (d ▹ τin) -> (op ▷ τin >=> τout ⊣ τc) ->
    { x:data | x ▹ τout }.
Proof.
    unfold nraext_eval, nraext_type; intros.
    apply (@typed_nra_total m τc τin τout (nra_of_nraext op) H1 c d); assumption.
  Defined.

  Definition tnraext_evalc} {τin τout} (op:nraext) (d:data) c :
    (bindings_type c τc) ->
    (d ▹ τin) -> (op ▷ τin >=> τout ⊣ τc) -> data.
Proof.
    unfold nraext_eval, nraext_type; intros.
    apply (@tnra_eval m τc τin τout (nra_of_nraext op) H1 c d); assumption.
  Defined.
End TNRAExt.


Notation "OpA >=> BC" := (nraext_type Op C A B) (at level 70) : nraext_scope.
Notation "Op @▷ dc" := (tnraext_eval Op d c) (at level 70) : nraext_scope.