Module TNRAEnvEq
Section
TNRAEnvEq
.
Require
Import
Equivalence
.
Require
Import
Morphisms
.
Require
Import
Setoid
.
Require
Import
EquivDec
.
Require
Import
Program
.
Require
Import
List
.
Require
Import
String
.
Require
Import
Utils
BasicSystem
.
Require
Import
NRAEnv
NRAEnvEq
.
Require
Import
TNRAEnv
.
Local
Open
Scope
nraenv_scope
.
Definition
typed_nraenv
{
m
:
basic_model
} τ
c
τ
env
τ
in
τ
out
:= {
op
:
nraenv
|
op
▷ₓ τ
in
>=> τ
out
⊣ τ
c
;τ
env
}.
Definition
tnraenv_eq
{
m
:
basic_model
} {τ
c
τ
env
τ
in
τ
out
} (
op1
op2
:
typed_nraenv
τ
c
τ
env
τ
in
τ
out
) :
Prop
:=
forall
(
x
:
data
)
c
(
env
:
data
)
(
dt_x
:
x
▹ τ
in
)
(
dt_c
:
bindings_type
c
τ
c
)
(
dt_env
:
env
▹ τ
env
),
brand_relation_brands
⊢ (
proj1_sig
op1
) @ₓ
x
⊣
c
;
env
=
brand_relation_brands
⊢ (
proj1_sig
op2
) @ₓ
x
⊣
c
;
env
.
Global
Instance
tnraenv_equiv
{
m
:
basic_model
} {τ
c
} {τ
env
τ
in
τ
out
:
rtype
} :
Equivalence
(@
tnraenv_eq
m
τ
c
τ
env
τ
in
τ
out
).
Proof.
constructor
.
-
unfold
Reflexive
,
tnraenv_eq
;
intros
.
reflexivity
.
-
unfold
Symmetric
,
tnraenv_eq
;
intros
.
rewrite
(
H
x0
c
env
dt_x
dt_c
dt_env
);
reflexivity
.
-
unfold
Transitive
,
tnraenv_eq
;
intros
.
intros
;
rewrite
(
H
x0
c
env
dt_x
dt_c
dt_env
);
rewrite
(
H0
x0
c
env
dt_x
dt_c
dt_env
);
reflexivity
.
Qed.
Notation
"
t1
⇝ₓ
t2
⊣ τ
c
;
tenv
" := (
typed_nraenv
τ
c
tenv
t1
t2
) (
at
level
80).
Notation
"
X
≡τₓ
Y
" := (
tnraenv_eq
X
Y
) (
at
level
80).
Hint
Resolve
data_type_normalized
.
Hint
Resolve
bindings_type_Forall_normalized
.
Lemma
nraenv_eq_impl_tnraenv_eq
{
m
:
basic_model
} {τ
c
τ
env
τ
in
τ
out
} (
op1
op2
: τ
in
⇝ₓ τ
out
⊣ τ
c
;τ
env
) :
`
op1
≡ₓ `
op2
->
op1
≡τₓ
op2
.
Proof.
unfold
tnraenv_eq
,
nraenv_eq
;
intros
.
eapply
H
;
eauto
.
Qed.
Lemma
nraenv_eq_pf_irrel
{
m
:
basic_model
} {
op
} {τ
in
τ
out
τ
c
τ
env
} (
pf1
pf2
:
op
▷ₓ τ
in
>=> τ
out
⊣ τ
c
;τ
env
) :
tnraenv_eq
(
exist
_
op
pf1
) (
exist
_
op
pf2
).
Proof.
red
;
intros
;
simpl
.
reflexivity
.
Qed.
Context
{
m
:
basic_model
}.
Definition
tnraenv_rewrites_to
(
op1
op2
:
nraenv
) :
Prop
:=
forall
τ
c
(τ
env
τ
in
τ
out
:
rtype
),
op1
▷ₓ τ
in
>=> τ
out
⊣ τ
c
;τ
env
->
(
op2
▷ₓ τ
in
>=> τ
out
⊣ τ
c
;τ
env
)
/\ (
forall
(
x
:
data
)
c
env
(
dt_x
:
x
▹ τ
in
)
(
dt_c
:
bindings_type
c
τ
c
)
(
dt_env
:
env
▹ τ
env
),
brand_relation_brands
⊢
op1
@ₓ
x
⊣
c
;
env
=
brand_relation_brands
⊢
op2
@ₓ
x
⊣
c
;
env
).
Notation
"
op1
⇒ₓ
op2
" := (@
tnraenv_rewrites_to
op1
op2
) (
at
level
80).
Lemma
rewrites_typed_with_untyped
(
op1
op2
:
nraenv
) :
op1
≡ₓ
op2
->
(
forall
{τ
c
} {τ
env
τ
in
τ
out
:
rtype
},
op1
▷ₓ τ
in
>=> τ
out
⊣ τ
c
;τ
env
->
op2
▷ₓ τ
in
>=> τ
out
⊣ τ
c
;τ
env
)
->
op1
⇒ₓ
op2
.
Proof.
intros
.
unfold
tnraenv_rewrites_to
;
simpl
;
intros
.
split
;
eauto
.
Qed.
Lemma
talg_rewrites_eq_is_typed_eq
{τ
c
} {τ
env
τ
in
τ
out
:
rtype
} (
op1
op2
:
typed_nraenv
τ
c
τ
env
τ
in
τ
out
):
(`
op1
⇒ₓ `
op2
) -> @
tnraenv_eq
m
τ
c
τ
env
τ
in
τ
out
op1
op2
.
Proof.
unfold
tnraenv_rewrites_to
,
tnraenv_eq
;
intros
.
dependent
induction
op1
.
dependent
induction
op2
;
simpl
in
*.
elim
(
H
τ
c
τ
env
τ
in
τ
out
);
clear
H
;
intros
.
apply
(
H0
x1
c
env
dt_x
dt_c
dt_env
).
assumption
.
Qed.
Thanks to shallow semantics, lifting between nraenv_core and nraenv is easy
Section
eq_lift
.
Require
Import
cNRAEnv
TcNRAEnvEq
.
Open
Scope
nraenv_core_scope
.
Lemma
lift_tnraenv_core_eq_to_tnraenv_eq_r
(
q1
q2
:
nraenv_core
) :
q1
⇒
q2
-> (
nraenv_of_nraenv_core
q1
) ⇒ₓ (
nraenv_of_nraenv_core
q2
).
Proof.
unfold
tnraenv_rewrites_to
.
unfold
tnraenv_core_rewrites_to
.
intros
.
unfold
nraenv_type
in
*.
unfold
nraenv_eval
in
*.
rewrite
nraenv_roundtrip
.
rewrite
nraenv_roundtrip
.
rewrite
nraenv_roundtrip
in
H0
.
auto
.
Qed.
Lemma
lift_tnraenv_core_eq_to_tnraenv_eq_l
(
q1
q2
:
nraenv_core
) :
(
nraenv_of_nraenv_core
q1
) ⇒ₓ (
nraenv_of_nraenv_core
q2
) ->
q1
⇒
q2
.
Proof.
unfold
tnraenv_rewrites_to
.
unfold
tnraenv_core_rewrites_to
.
intros
.
unfold
nraenv_type
in
*.
unfold
nraenv_eval
in
*.
rewrite
nraenv_roundtrip
in
H
.
rewrite
nraenv_roundtrip
in
H
.
specialize
(
H
_
_
_
_
H0
);
intros
.
assumption
.
Qed.
Lemma
lift_tnraenv_core_eq_to_tnraenv_eq
(
q1
q2
:
nraenv_core
) :
q1
⇒
q2
<-> (
nraenv_of_nraenv_core
q1
) ⇒ₓ (
nraenv_of_nraenv_core
q2
).
Proof.
split
.
apply
lift_tnraenv_core_eq_to_tnraenv_eq_r
.
apply
lift_tnraenv_core_eq_to_tnraenv_eq_l
.
Qed.
Lemma
lift_tnraenv_eq_to_tnraenv_core_eq_r
(
q1
q2
:
nraenv
) :
q1
⇒ₓ
q2
-> (
nraenv_core_of_nraenv
q1
) ⇒ (
nraenv_core_of_nraenv
q2
).
Proof.
unfold
tnraenv_rewrites_to
.
unfold
tnraenv_core_rewrites_to
.
intros
.
unfold
nraenv_eval
in
*.
unfold
nraenv_type
in
*.
elim
(
H
_
_
_
_
H0
);
intros
;
clear
H
.
split
;
assumption
.
Qed.
Lemma
lift_tnraenv_eq_to_tnraenv_core_eq_l
(
q1
q2
:
nraenv
) :
(
nraenv_core_of_nraenv
q1
) ⇒ (
nraenv_core_of_nraenv
q2
) ->
q1
⇒ₓ
q2
.
Proof.
unfold
tnraenv_rewrites_to
.
unfold
tnraenv_core_rewrites_to
.
intros
.
unfold
nraenv_eval
in
*.
unfold
nraenv_type
in
*.
elim
(
H
_
_
_
_
H0
);
intros
;
clear
H
.
split
;
assumption
.
Qed.
Lemma
lift_tnraenv_eq_to_tnraenv_core_eq
(
q1
q2
:
nraenv
) :
q1
⇒ₓ
q2
<-> (
nraenv_core_of_nraenv
q1
) ⇒ (
nraenv_core_of_nraenv
q2
).
Proof.
split
.
apply
lift_tnraenv_eq_to_tnraenv_core_eq_r
.
apply
lift_tnraenv_eq_to_tnraenv_core_eq_l
.
Qed.
End
eq_lift
.
Require
Import
ROpsEq
NRAEnvEq
.
Global
Instance
tnraenv_rewrites_to_pre
:
PreOrder
tnraenv_rewrites_to
.
Proof.
constructor
;
red
;
intros
.
-
unfold
tnraenv_rewrites_to
;
intros
.
split
;
try
assumption
;
intros
.
reflexivity
.
-
unfold
tnraenv_rewrites_to
in
*;
intros
.
specialize
(
H
τ
c
τ
env
τ
in
τ
out
H1
).
elim
H
;
clear
H
;
intros
.
specialize
(
H0
τ
c
τ
env
τ
in
τ
out
H
).
elim
H0
;
clear
H0
;
intros
.
split
;
try
assumption
;
intros
.
rewrite
(
H2
x0
c
env
);
try
assumption
.
rewrite
(
H3
x0
c
env
);
try
assumption
.
reflexivity
.
Qed.
Global
Instance
nraenv_id_tproper
:
Proper
tnraenv_rewrites_to
NRAEnvID
.
Proof.
unfold
Proper
,
respectful
;
intros
.
reflexivity
.
Qed.
Global
Instance
nraenv_const_tproper
:
Proper
(
eq
==>
tnraenv_rewrites_to
)
NRAEnvConst
.
Proof.
unfold
Proper
,
respectful
;
intros
.
rewrite
H
;
reflexivity
.
Qed.
Global
Instance
nraenv_binop_tproper
:
Proper
(
eq
==>
tnraenv_rewrites_to
==>
tnraenv_rewrites_to
==>
tnraenv_rewrites_to
)
NRAEnvBinop
.
Proof.
unfold
Proper
,
respectful
;
intros
.
rewrite
lift_tnraenv_eq_to_tnraenv_core_eq
in
H0
.
rewrite
lift_tnraenv_eq_to_tnraenv_core_eq
in
H1
.
rewrite
lift_tnraenv_eq_to_tnraenv_core_eq
.
simpl
.
rewrite
H
;
rewrite
H0
;
rewrite
H1
.
reflexivity
.
Qed.
Global
Instance
nraenv_unop_tproper
:
Proper
(
eq
==>
tnraenv_rewrites_to
==>
tnraenv_rewrites_to
)
NRAEnvUnop
.
Proof.
unfold
Proper
,
respectful
;
intros
.
rewrite
lift_tnraenv_eq_to_tnraenv_core_eq
in
H0
.
rewrite
lift_tnraenv_eq_to_tnraenv_core_eq
.
simpl
.
rewrite
H
;
rewrite
H0
.
reflexivity
.
Qed.
Global
Instance
nraenv_map_tproper
:
Proper
(
tnraenv_rewrites_to
==>
tnraenv_rewrites_to
==>
tnraenv_rewrites_to
)
NRAEnvMap
.
Proof.
unfold
Proper
,
respectful
;
intros
.
rewrite
lift_tnraenv_eq_to_tnraenv_core_eq
in
H
.
rewrite
lift_tnraenv_eq_to_tnraenv_core_eq
in
H0
.
rewrite
lift_tnraenv_eq_to_tnraenv_core_eq
.
simpl
.
rewrite
H
;
rewrite
H0
.
reflexivity
.
Qed.
Global
Instance
nraenv_mapconcat_tproper
:
Proper
(
tnraenv_rewrites_to
==>
tnraenv_rewrites_to
==>
tnraenv_rewrites_to
)
NRAEnvMapConcat
.
Proof.
unfold
Proper
,
respectful
;
intros
.
rewrite
lift_tnraenv_eq_to_tnraenv_core_eq
in
H
.
rewrite
lift_tnraenv_eq_to_tnraenv_core_eq
in
H0
.
rewrite
lift_tnraenv_eq_to_tnraenv_core_eq
.
simpl
.
rewrite
H
;
rewrite
H0
.
reflexivity
.
Qed.
Global
Instance
nraenv_product_tproper
:
Proper
(
tnraenv_rewrites_to
==>
tnraenv_rewrites_to
==>
tnraenv_rewrites_to
)
NRAEnvProduct
.
Proof.
unfold
Proper
,
respectful
;
intros
.
rewrite
lift_tnraenv_eq_to_tnraenv_core_eq
in
H
.
rewrite
lift_tnraenv_eq_to_tnraenv_core_eq
in
H0
.
rewrite
lift_tnraenv_eq_to_tnraenv_core_eq
.
simpl
.
rewrite
H
;
rewrite
H0
.
reflexivity
.
Qed.
Global
Instance
nraenv_select_tproper
:
Proper
(
tnraenv_rewrites_to
==>
tnraenv_rewrites_to
==>
tnraenv_rewrites_to
)
NRAEnvSelect
.
Proof.
unfold
Proper
,
respectful
;
intros
.
rewrite
lift_tnraenv_eq_to_tnraenv_core_eq
in
H
.
rewrite
lift_tnraenv_eq_to_tnraenv_core_eq
in
H0
.
rewrite
lift_tnraenv_eq_to_tnraenv_core_eq
.
simpl
.
rewrite
H
;
rewrite
H0
.
reflexivity
.
Qed.
Global
Instance
nraenv_default_tproper
:
Proper
(
tnraenv_rewrites_to
==>
tnraenv_rewrites_to
==>
tnraenv_rewrites_to
)
NRAEnvDefault
.
Proof.
unfold
Proper
,
respectful
;
intros
.
rewrite
lift_tnraenv_eq_to_tnraenv_core_eq
in
H
.
rewrite
lift_tnraenv_eq_to_tnraenv_core_eq
in
H0
.
rewrite
lift_tnraenv_eq_to_tnraenv_core_eq
.
simpl
.
rewrite
H
;
rewrite
H0
.
reflexivity
.
Qed.
Global
Instance
nraenv_either_tproper
:
Proper
(
tnraenv_rewrites_to
==>
tnraenv_rewrites_to
==>
tnraenv_rewrites_to
)
NRAEnvEither
.
Proof.
unfold
Proper
,
respectful
;
intros
.
rewrite
lift_tnraenv_eq_to_tnraenv_core_eq
in
H
.
rewrite
lift_tnraenv_eq_to_tnraenv_core_eq
in
H0
.
rewrite
lift_tnraenv_eq_to_tnraenv_core_eq
.
simpl
.
rewrite
H
;
rewrite
H0
.
reflexivity
.
Qed.
Global
Instance
nraenv_eitherconcat_tproper
:
Proper
(
tnraenv_rewrites_to
==>
tnraenv_rewrites_to
==>
tnraenv_rewrites_to
)
NRAEnvEitherConcat
.
Proof.
unfold
Proper
,
respectful
;
intros
.
rewrite
lift_tnraenv_eq_to_tnraenv_core_eq
in
H
.
rewrite
lift_tnraenv_eq_to_tnraenv_core_eq
in
H0
.
rewrite
lift_tnraenv_eq_to_tnraenv_core_eq
.
simpl
.
rewrite
H
;
rewrite
H0
.
reflexivity
.
Qed.
Global
Instance
nraenv_app_tproper
:
Proper
(
tnraenv_rewrites_to
==>
tnraenv_rewrites_to
==>
tnraenv_rewrites_to
)
NRAEnvApp
.
Proof.
unfold
Proper
,
respectful
;
intros
.
rewrite
lift_tnraenv_eq_to_tnraenv_core_eq
in
H
.
rewrite
lift_tnraenv_eq_to_tnraenv_core_eq
in
H0
.
rewrite
lift_tnraenv_eq_to_tnraenv_core_eq
.
simpl
.
rewrite
H
;
rewrite
H0
.
reflexivity
.
Qed.
Global
Instance
nraenv_env_tproper
:
Proper
tnraenv_rewrites_to
NRAEnvEnv
.
Proof.
unfold
Proper
,
respectful
;
intros
.
reflexivity
.
Qed.
Global
Instance
nraenv_appenv_tproper
:
Proper
(
tnraenv_rewrites_to
==>
tnraenv_rewrites_to
==>
tnraenv_rewrites_to
)
NRAEnvAppEnv
.
Proof.
unfold
Proper
,
respectful
;
intros
.
rewrite
lift_tnraenv_eq_to_tnraenv_core_eq
in
H
.
rewrite
lift_tnraenv_eq_to_tnraenv_core_eq
in
H0
.
rewrite
lift_tnraenv_eq_to_tnraenv_core_eq
.
simpl
.
rewrite
H
;
rewrite
H0
.
reflexivity
.
Qed.
Global
Instance
nraenv_mapenv_tproper
:
Proper
(
tnraenv_rewrites_to
==>
tnraenv_rewrites_to
)
NRAEnvMapEnv
.
Proof.
unfold
Proper
,
respectful
;
intros
.
rewrite
lift_tnraenv_eq_to_tnraenv_core_eq
in
H
.
rewrite
lift_tnraenv_eq_to_tnraenv_core_eq
.
simpl
.
rewrite
H
.
reflexivity
.
Qed.
Global
Instance
nraenv_flatmap_tproper
:
Proper
(
tnraenv_rewrites_to
==>
tnraenv_rewrites_to
==>
tnraenv_rewrites_to
)
NRAEnvFlatMap
.
Proof.
unfold
Proper
,
respectful
;
intros
.
rewrite
lift_tnraenv_eq_to_tnraenv_core_eq
.
rewrite
lift_tnraenv_eq_to_tnraenv_core_eq
in
H
.
rewrite
lift_tnraenv_eq_to_tnraenv_core_eq
in
H0
.
simpl
.
unfold
flat_map
.
rewrite
H
;
rewrite
H0
;
reflexivity
.
Qed.
Global
Instance
nraenv_join_tproper
:
Proper
(
tnraenv_rewrites_to
==>
tnraenv_rewrites_to
==>
tnraenv_rewrites_to
==>
tnraenv_rewrites_to
)
NRAEnvJoin
.
Proof.
unfold
Proper
,
respectful
;
intros
.
rewrite
lift_tnraenv_eq_to_tnraenv_core_eq
.
rewrite
lift_tnraenv_eq_to_tnraenv_core_eq
in
H
.
rewrite
lift_tnraenv_eq_to_tnraenv_core_eq
in
H0
.
rewrite
lift_tnraenv_eq_to_tnraenv_core_eq
in
H1
.
simpl
.
unfold
join
.
rewrite
H
;
rewrite
H0
;
rewrite
H1
;
reflexivity
.
Qed.
Global
Instance
nraenv_project_tproper
:
Proper
(
eq
==>
tnraenv_rewrites_to
==>
tnraenv_rewrites_to
)
NRAEnvProject
.
Proof.
unfold
Proper
,
respectful
;
intros
.
rewrite
lift_tnraenv_eq_to_tnraenv_core_eq
.
rewrite
lift_tnraenv_eq_to_tnraenv_core_eq
in
H0
.
simpl
.
unfold
project
.
rewrite
H
;
rewrite
H0
;
reflexivity
.
Qed.
Global
Instance
nraenv_group_by_tproper
:
Proper
(
eq
==>
eq
==>
tnraenv_rewrites_to
==>
tnraenv_rewrites_to
)
NRAEnvGroupBy
.
Proof.
unfold
Proper
,
respectful
;
intros
.
rewrite
lift_tnraenv_eq_to_tnraenv_core_eq
.
rewrite
lift_tnraenv_eq_to_tnraenv_core_eq
in
H1
.
simpl
.
unfold
group_by_with_env
.
rewrite
H
;
rewrite
H0
;
rewrite
H1
;
reflexivity
.
Qed.
Global
Instance
nraenv_unnest_tproper
:
Proper
(
eq
==>
eq
==>
tnraenv_rewrites_to
==>
tnraenv_rewrites_to
)
NRAEnvUnnest
.
Proof.
unfold
Proper
,
respectful
;
intros
.
rewrite
lift_tnraenv_eq_to_tnraenv_core_eq
.
rewrite
lift_tnraenv_eq_to_tnraenv_core_eq
in
H1
.
simpl
.
unfold
unnest
.
rewrite
H
;
rewrite
H0
;
rewrite
H1
;
reflexivity
.
Qed.
End
TNRAEnvEq
.
Notation
"
op1
⇒ₓ
op2
" := (
tnraenv_rewrites_to
op1
op2
) (
at
level
80) :
nraenv_scope
.
Notation
"
h
⊧
t1
⇝ₓ
t2
⊣
c
;
tenv
" := (@
typed_nraenv
h
c
tenv
t1
t2
) (
at
level
80) :
nraenv_scope
.
Notation
"
X
≡τₓ
Y
" := (
tnraenv_eq
X
Y
) (
at
level
80) :
nraenv_scope
.
Notation
"
X
≡τ'ₓ
Y
" := (
tnraenv_eq
(
exist
_
_
X
) (
exist
_
_
Y
)) (
at
level
80) :
nraenv_scope
.