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
"
Op
▷
A
>=>
B
⊣
C
" := (
nraext_type
Op
C
A
B
) (
at
level
70) :
nraext_scope
.
Main typing soundness theorem for the Extended NRA
Theorem
typed_nraext_yields_typed_data
{τ
c
} {τ
in
τ
out
} (
d
:
data
)
c
(
op
:
nraext
):
(
bindings_type
c
τ
c
) ->
(
d
▹ τ
in
) -> (
op
▷ τ
in
>=> τ
out
⊣ τ
c
) ->
(
exists
x
, (
brand_relation_brands
⊢
op
@ₓ
d
⊣
c
=
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_total
{τ
c
} {τ
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_eval
{τ
c
} {τ
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
"
Op
▷
A
>=>
B
⊣
C
" := (
nraext_type
Op
C
A
B
) (
at
level
70) :
nraext_scope
.
Notation
"
Op
@▷
d
⊣
c
" := (
tnraext_eval
Op
d
c
) (
at
level
70) :
nraext_scope
.