Skip to content
GitLab
Projects
Groups
Snippets
/
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in / Register
Toggle navigation
Menu
Open sidebar
Dan Frumin
ReLoC-v1
Commits
774956bd
Commit
774956bd
authored
Mar 12, 2016
by
Amin Timany
Browse files
Split F_mu_ref over several files.
parent
67b2ae91
Changes
7
Expand all
Hide whitespace changes
Inline
Side-by-side
F_mu_ref.v
deleted
100644 → 0
View file @
67b2ae91
This diff is collapsed.
Click to expand it.
F_mu_ref/fundamental.v
0 → 100644
View file @
774956bd
Require
Import
iris
.
program_logic
.
hoare
.
Require
Import
iris
.
program_logic
.
lifting
.
Require
Import
iris
.
algebra
.
upred_big_op
.
Require
Import
F_mu_ref
.
lang
F_mu_ref
.
typing
F_mu_ref
.
rules
F_mu_ref
.
logrel
.
From
iris
.
program_logic
Require
Export
lifting
.
From
iris
.
algebra
Require
Import
upred_big_op
frac
dec_agree
.
From
iris
.
program_logic
Require
Export
invariants
ghost_ownership
.
From
iris
.
program_logic
Require
Import
ownership
auth
.
Require
Import
Vlist
.
Import
uPred
.
Section
typed_interp
.
Context
{
Σ
:
gFunctors
}
`
{
i
:
heapG
Σ
}
`
{
L
:
namespace
}
.
Implicit
Types
P
Q
R
:
iPropG
lang
Σ
.
Notation
"# v"
:=
(
of_val
v
)
(
at
level
20
).
Local
Ltac
ipropsimpl
:=
repeat
match
goal
with
|
[
|-
(
_
⊢
(
_
∧
_
))
%
I
]
=>
eapply
and_intro
|
[
|-
(
▷
_
⊢
▷
_
)
%
I
]
=>
apply
later_mono
|
[
|-
(
_
⊢
∃
_
,
_
)
%
I
]
=>
rewrite
-
exist_intro
|
[
|-
((
∃
_
,
_
)
⊢
_
)
%
I
]
=>
let
v
:=
fresh
"v"
in
rewrite
exist_elim
;
[
|
intros
v
]
end
.
Local
Hint
Extern
1
=>
progress
ipropsimpl
.
Local
Tactic
Notation
"smart_wp_bind"
uconstr
(
ctx
)
uconstr
(
t
)
ident
(
v
)
:=
rewrite
-
(
@
wp_bind
_
_
_
[
ctx
])
/=
-
wp_impl_l
;
apply
and_intro
;
[
apply
(
@
always_intro
_
_
_
t
),
forall_intro
=>
v
/=
;
apply
impl_intro_l
|
eauto
with
itauto
].
Local
Tactic
Notation
"smart_wp_bind"
uconstr
(
ctx
)
ident
(
v
)
:=
rewrite
-
(
@
wp_bind
_
_
_
[
ctx
])
/=
-
wp_mono
;
eauto
;
intros
v
;
cbn
.
Create
HintDb
itauto
.
Local
Hint
Extern
3
((
_
∧
_
)
⊢
_
)
%
I
=>
rewrite
and_elim_r
:
itauto
.
Local
Hint
Extern
3
((
_
∧
_
)
⊢
_
)
%
I
=>
rewrite
and_elim_l
:
itauto
.
Local
Hint
Extern
3
(
_
⊢
(
_
∨
_
))
%
I
=>
rewrite
-
or_intro_l
:
itauto
.
Local
Hint
Extern
3
(
_
⊢
(
_
∨
_
))
%
I
=>
rewrite
-
or_intro_r
:
itauto
.
Local
Hint
Extern
2
(
_
⊢
▷
_
)
%
I
=>
etransitivity
;
[
|
rewrite
-
later_intro
]
:
itauto
.
Local
Ltac
value_case
:=
rewrite
-
wp_value
/=
?
to_of_val
//; auto 2.
Lemma
typed_interp
N
k
Δ
Γ
vs
e
τ
(
HNLdisj
:
∀
l
:
loc
,
N
⊥
L
.
@
l
)
(
Htyped
:
typed
k
Γ
e
τ
)
(
Hctx
:
closed_ctx
k
Γ
)
(
HC
:
closed_type
k
τ
)
(
H
Δ
:
VlistAlwaysStable
Δ
)
:
length
Γ
=
length
vs
→
(
heap_ctx
N
∧
Π∧
zip_with
(
λ
τ
v
,
(
@
interp
Σ
i
L
)
k
(
`
τ
)
(
proj2_sig
τ
)
Δ
v
)
(
closed_ctx_list
_
Γ
Hctx
)
vs
)
%
I
⊢
WP
(
e
.[
env_subst
vs
])
@
⊤
{{
λ
v
,
(
@
interp
Σ
i
L
)
k
τ
HC
Δ
v
}}
.
Proof
.
revert
Hctx
HC
H
Δ
vs
.
induction
Htyped
;
intros
Hctx
HC
H
Δ
vs
Hlen
;
cbn
.
-
(
*
var
*
)
destruct
(
lookup_lt_is_Some_2
vs
x
)
as
[
v
Hv
].
{
by
rewrite
-
Hlen
;
apply
lookup_lt_Some
with
τ
.
}
rewrite
/
env_subst
Hv
/=
-
wp_value
;
eauto
using
to_of_val
.
edestruct
(
zipwith_Forall_lookup
_
Hctx
)
as
[
H
τ'
H
τ'
eq
];
eauto
.
rewrite
and_elim_r
.
etransitivity
.
apply
big_and_elem_of
,
elem_of_list_lookup_2
with
x
.
rewrite
lookup_zip_with
;
simplify_option_eq
;
trivial
.
rewrite
interp_closed_irrel
;
trivial
.
-
(
*
unit
*
)
value_case
.
-
(
*
pair
*
)
smart_wp_bind
(
PairLCtx
e2
.[
env_subst
vs
])
_
v
;
eauto
.
(
*
weird
!:
and_alwaysstable
is
an
instance
but
is
not
resolved
!
*
)
smart_wp_bind
(
PairRCtx
v
)
(
and_persistent
_
_
_
_
)
v
'
.
value_case
;
eauto
10
with
itauto
.
-
(
*
fst
*
)
smart_wp_bind
(
FstCtx
)
v
.
ipropsimpl
;
eauto
.
apply
const_elim_l
;
intros
H
;
rewrite
H
.
rewrite
-
wp_fst
;
eauto
using
to_of_val
,
and_elim_l
.
rewrite
and_elim_l
;
rewrite
interp_closed_irrel
;
eauto
.
-
(
*
snd
*
)
smart_wp_bind
SndCtx
v
.
ipropsimpl
;
eauto
.
apply
const_elim_l
;
intros
H
;
rewrite
H
.
rewrite
-
wp_snd
;
eauto
using
to_of_val
,
and_elim_l
.
rewrite
and_elim_r
;
rewrite
interp_closed_irrel
;
eauto
.
-
(
*
injl
*
)
smart_wp_bind
InjLCtx
v
;
value_case
;
eauto
7
with
itauto
.
-
(
*
injr
*
)
smart_wp_bind
InjRCtx
v
;
value_case
;
eauto
7
with
itauto
.
-
(
*
case
*
)
smart_wp_bind
(
CaseCtx
_
_
)
_
v
.
cbn
.
rewrite
(
later_intro
(
heap_ctx
N
∧
Π∧
zip_with
(
λ
(
τ
:
{
τ
:
type
|
closed_type
k
τ
}
)
(
v0
:
leibniz_val
),
((
interp
k
(
`
τ
)
(
proj2_sig
τ
))
Δ
)
v0
)
(
closed_ctx_list
k
Γ
Hctx
)
vs
));
rewrite
or_elim
;
[
apply
impl_elim_l
|
|
].
+
rewrite
exist_elim
;
eauto
;
intros
v
'
.
apply
const_elim_l
;
intros
H
;
rewrite
H
.
rewrite
-
impl_intro_r
//; rewrite -later_and later_mono; eauto.
rewrite
-
wp_case_inl
;
eauto
using
to_of_val
.
asimpl
.
specialize
(
IHHtyped2
Δ
(
typed_closed_ctx
_
_
_
_
Htyped2
)
HC
H
Δ
(
v
'
::
vs
)).
erewrite
<-
?
typed_subst_head_simpl
in
*
by
(
cbn
;
eauto
).
rewrite
-
IHHtyped2
;
cbn
;
auto
.
rewrite
interp_closed_irrel
type_context_closed_irrel
/
closed_ctx_list
.
apply
later_mono
;
repeat
apply
and_intro
;
eauto
3
with
itauto
.
+
rewrite
exist_elim
;
eauto
;
intros
v
'
.
apply
const_elim_l
;
intros
H
;
rewrite
H
.
rewrite
-
impl_intro_r
//; rewrite -later_and later_mono; eauto.
rewrite
-
wp_case_inr
;
eauto
using
to_of_val
.
asimpl
.
specialize
(
IHHtyped3
Δ
(
typed_closed_ctx
_
_
_
_
Htyped3
)
HC
H
Δ
(
v
'
::
vs
)).
erewrite
<-
?
typed_subst_head_simpl
in
*
by
(
cbn
;
eauto
).
rewrite
-
IHHtyped3
;
cbn
;
auto
.
rewrite
interp_closed_irrel
type_context_closed_irrel
/
closed_ctx_list
.
apply
later_mono
;
repeat
apply
and_intro
;
eauto
3
with
itauto
.
-
(
*
lam
*
)
value_case
;
apply
(
always_intro
_
_
),
forall_intro
=>
v
/=
;
apply
impl_intro_l
.
rewrite
-
wp_lam
?
to_of_val
//=.
asimpl
.
erewrite
typed_subst_head_simpl
;
[
|
eauto
|
cbn
];
eauto
.
rewrite
(
later_intro
(
heap_ctx
N
∧
Π∧
_
))
-
later_and
;
apply
later_mono
.
rewrite
interp_closed_irrel
type_context_closed_irrel
/
closed_ctx_list
.
rewrite
-
(
IHHtyped
Δ
(
typed_closed_ctx
_
_
_
_
Htyped
)
(
closed_type_arrow_2
HC
)
H
Δ
(
v
::
vs
));
cbn
;
auto
2
with
f_equal
.
repeat
apply
and_intro
;
eauto
3
with
itauto
.
-
(
*
app
*
)
smart_wp_bind
(
AppLCtx
(
e2
.[
env_subst
vs
]))
_
v
.
rewrite
-
(
@
wp_bind
_
_
_
[
AppRCtx
v
])
/=
.
rewrite
-
wp_impl_l
/=
;
apply
and_intro
.
2
:
etransitivity
;
[
|
apply
IHHtyped2
];
eauto
using
and_elim_r
.
rewrite
and_elim_l
.
apply
always_mono
.
apply
forall_intro
=>
v
'
.
rewrite
forall_elim
.
apply
impl_intro_l
.
rewrite
-
(
later_intro
).
etransitivity
;
[
apply
impl_elim_r
|
].
apply
wp_mono
=>
w
.
rewrite
interp_closed_irrel
;
trivial
.
-
(
*
TLam
*
)
value_case
;
rewrite
-
exist_intro
;
apply
and_intro
;
auto
.
apply
forall_intro
=>
τ
i
;
apply
(
always_intro
_
_
).
rewrite
map_length
in
IHHtyped
.
destruct
τ
i
as
[
τ
i
τ
iAS
].
specialize
(
IHHtyped
(
Vlist_cons
τ
i
Δ
)
(
closed_ctx_map
_
_
_
_
Hctx
(
λ
τ
,
closed_type_S_ren2
τ
1
0
_
))
(
closed_type_forall
HC
)
(
alwyas_stable_Vlist_cons
_
_
_
τ
iAS
)
_
Hlen
).
rewrite
-
wp_impl_l
-
later_intro
.
apply
and_intro
;
[
apply
(
always_intro
_
_
),
forall_intro
=>
v
/=
;
apply
impl_intro_l
|
].
2
:
etransitivity
;
[
|
apply
IHHtyped
].
+
rewrite
and_elim_l
;
trivial
.
+
rewrite
zip_with_closed_ctx_list_subst
;
trivial
.
-
(
*
TApp
*
)
smart_wp_bind
TAppCtx
_
v
;
cbn
.
rewrite
and_elim_l
.
rewrite
exist_elim
;
eauto
=>
e
'
.
apply
const_elim_l
;
intros
H
'
;
rewrite
H
'
.
rewrite
(
forall_elim
((
interp
k
τ'
H
Δ
)
↾
_
)).
rewrite
always_elim
.
rewrite
-
wp_TLam
;
apply
later_mono
.
apply
wp_mono
=>
w
.
eapply
entails_proper
.
+
apply
interp_subst
.
+
eauto
.
+
eauto
.
-
(
*
Fold
*
)
value_case
.
unfold
interp_rec
.
rewrite
fixpoint_unfold
.
cbn
.
rewrite
-
exist_intro
.
apply
(
always_intro
_
_
).
apply
and_intro
;
auto
.
rewrite
map_length
in
IHHtyped
.
specialize
(
IHHtyped
(
Vlist_cons
(
@
interp
Σ
i
L
k
(
TRec
τ
)
HC
Δ
)
Δ
)
(
closed_ctx_map
_
_
_
_
Hctx
(
λ
τ
,
closed_type_S_ren2
τ
1
0
_
))
(
closed_type_rec
HC
)
(
alwyas_stable_Vlist_cons
_
_
_
_
)
_
Hlen
).
rewrite
-
wp_impl_l
-
later_intro
.
apply
and_intro
;
[
apply
(
always_intro
_
_
),
forall_intro
=>
v
/=
;
apply
impl_intro_l
|
].
2
:
etransitivity
;
[
|
apply
IHHtyped
].
+
rewrite
and_elim_l
;
trivial
.
+
rewrite
zip_with_closed_ctx_list_subst
;
trivial
.
-
(
*
Unfold
*
)
smart_wp_bind
UnfoldCtx
_
v
;
cbn
.
rewrite
and_elim_l
.
unfold
interp_rec
.
rewrite
fixpoint_unfold
/
interp_rec_pre
;
cbn
.
replace
(
fixpoint
(
λ
rec_apr
:
leibniz_val
-
n
>
iPropG
lang
Σ
,
CofeMor
(
λ
w
:
leibniz_val
,
□
(
∃
e1
:
expr
,
w
=
FoldV
e1
∧
▷
WP
e1
@
⊤
{{
λ
v1
:
val
,
((
interp
(
S
k
)
τ
(
closed_type_rec
?
HC4
))
(
Vlist_cons
rec_apr
Δ
))
v1
}}
))
%
I
))
with
(
@
interp
Σ
i
L
k
(
TRec
τ
)
(
typed_closed_type
_
_
_
_
Htyped
)
Δ
)
by
(
cbn
;
unfold
interp_rec
;
trivial
).
rewrite
always_elim
.
rewrite
exist_elim
;
eauto
=>
e
'
.
apply
const_elim_l
;
intros
H
'
;
rewrite
H
'
.
rewrite
-
wp_Fold
.
apply
later_mono
,
wp_mono
=>
w
.
rewrite
-
interp_subst
;
eauto
.
-
(
*
Alloc
*
)
smart_wp_bind
AllocCtx
_
v
;
cbn
.
rewrite
-
wp_atomic
;
cbn
;
eauto
using
to_of_val
.
rewrite
-
wp_alloc
.
apply
pvs_intro
.
all
:
eauto
3
using
to_of_val
with
itauto
.
rewrite
-
later_intro
.
apply
forall_intro
=>
l
.
apply
wand_intro_l
.
rewrite
-
exist_intro
.
rewrite
-
pvs_always_l
.
apply
and_intro
;
auto
.
rewrite
-
inv_alloc
;
auto
.
rewrite
-
later_intro
/
interp_ref_pred
.
rewrite
-
exist_intro
.
apply
sep_mono
;
eauto
.
auto
with
itauto
.
-
(
*
Load
*
)
smart_wp_bind
LoadCtx
_
v
;
cbn
.
rewrite
and_exist_r
.
apply
exist_elim
=>
l
.
rewrite
-
and_assoc
.
apply
const_elim_l
;
intros
Heq
;
rewrite
Heq
.
rewrite
-
wp_atomic
;
cbn
;
eauto
using
to_of_val
.
rewrite
-
wp_inv
;
try
match
goal
with
|-
_
⊆
_
=>
trivial
end
.
rewrite
-
pvs_intro
;
eauto
.
cbn
;
eauto
using
to_of_val
.
apply
and_elim_l
.
rewrite
and_elim_r
and_elim_l
.
apply
wand_intro_l
.
unfold
interp_ref_pred
at
1.
apply
wand_elim_l
'
.
etrans
;
[
rewrite
later_exist
|
];
eauto
.
rewrite
exist_elim
;
eauto
=>
w
.
apply
wand_intro_r
.
rewrite
-
(
wp_load
_
_
_
1
);
try
match
goal
with
|-
_
⊆
_
=>
trivial
end
;
eauto
.
rewrite
sep_elim_r
;
auto
with
itauto
.
specialize
(
HNLdisj
l
);
set_solver_ndisj
.
rewrite
sep_elim_l
.
unfold
interp_ref_pred
.
rewrite
-
later_sep
.
apply
later_mono
.
apply
sep_mono
;
eauto
.
apply
wand_intro_l
.
rewrite
-
later_intro
.
rewrite
-
exist_intro
.
rewrite
(
always_sep_dup
(((
interp
k
τ
(
closed_type_ref
_
))
Δ
)
w
)).
rewrite
sep_assoc
.
apply
sep_mono
;
eauto
.
rewrite
-
pvs_intro
.
rewrite
interp_closed_irrel
;
trivial
.
-
(
*
Store
*
)
smart_wp_bind
(
StoreLCtx
_
)
_
v
;
cbn
.
smart_wp_bind
(
StoreRCtx
_
)
_
v
'
;
cbn
.
rewrite
and_comm
?
and_assoc
.
rewrite
!
and_exist_r
.
apply
exist_elim
=>
l
.
rewrite
-!
and_assoc
.
apply
const_elim_l
;
intros
Heq
;
rewrite
Heq
.
rewrite
-
wp_atomic
;
cbn
;
eauto
using
to_of_val
.
rewrite
-
wp_inv
;
try
match
goal
with
|-
_
⊆
_
=>
trivial
end
.
rewrite
-
pvs_intro
;
eauto
.
cbn
;
eauto
using
to_of_val
.
apply
and_elim_l
.
rewrite
and_elim_r
and_comm
-
and_assoc
and_elim_r
.
apply
wand_intro_l
.
unfold
interp_ref_pred
at
1.
apply
wand_elim_l
'
.
etrans
;
[
rewrite
later_exist
|
];
eauto
.
rewrite
exist_elim
;
eauto
=>
w
.
apply
wand_intro_r
.
rewrite
-
wp_store
;
try
match
goal
with
|-
_
⊆
_
=>
trivial
end
;
eauto
using
to_of_val
.
rewrite
sep_elim_r
;
auto
with
itauto
.
specialize
(
HNLdisj
l
);
set_solver_ndisj
.
rewrite
and_elim_l
.
unfold
interp_ref_pred
.
rewrite
(
later_intro
(((
interp
k
τ
_
)
Δ
)
v
'
)).
rewrite
-!
later_sep
.
apply
later_mono
.
rewrite
-
wand_intro_l
.
apply
sep_mono
.
apply
sep_elim_l
.
trivial
.
rewrite
-
later_intro
.
rewrite
-
exist_intro
.
rewrite
(
always_sep_dup
(((
interp
k
τ
_
)
Δ
)
_
)).
rewrite
sep_assoc
.
apply
sep_mono
;
eauto
.
rewrite
interp_closed_irrel
;
trivial
.
rewrite
-
pvs_intro
;
auto
.
(
*
unshelving
*
)
Unshelve
.
all:
solve
[
eauto
2
using
typed_closed_type
|
try
typeclasses
eauto
].
Qed
.
End
typed_interp
.
\ No newline at end of file
F_mu_ref/lang.v
0 → 100644
View file @
774956bd
Require
Export
prelude
.
base
.
Require
Import
iris
.
prelude
.
gmap
.
Require
Import
iris
.
program_logic
.
language
.
Require
Export
Autosubst
.
Autosubst
.
Module
lang
.
Definition
loc
:=
positive
.
Global
Instance
loc_dec_eq
(
l
l
'
:
loc
)
:
Decision
(
l
=
l
'
)
:=
_.
Inductive
expr
:=
|
Var
(
x
:
var
)
|
Lam
(
e
:
{
bind
1
of
expr
}
)
|
App
(
e1
e2
:
expr
)
(
*
Unit
*
)
|
Unit
(
*
Products
*
)
|
Pair
(
e1
e2
:
expr
)
|
Fst
(
e
:
expr
)
|
Snd
(
e
:
expr
)
(
*
Sums
*
)
|
InjL
(
e
:
expr
)
|
InjR
(
e
:
expr
)
|
Case
(
e0
:
expr
)
(
e1
:
{
bind
expr
}
)
(
e2
:
{
bind
expr
}
)
(
*
Recursive
Types
*
)
|
Fold
(
e
:
expr
)
|
Unfold
(
e
:
expr
)
(
*
Polymorphic
Types
*
)
|
TLam
(
e
:
expr
)
|
TApp
(
e
:
expr
)
(
*
Reference
Types
*
)
|
Loc
(
l
:
loc
)
|
Alloc
(
e
:
expr
)
|
Load
(
e
:
expr
)
|
Store
(
e1
:
expr
)
(
e2
:
expr
).
Instance
Ids_expr
:
Ids
expr
.
derive
.
Defined
.
Instance
Rename_expr
:
Rename
expr
.
derive
.
Defined
.
Instance
Subst_expr
:
Subst
expr
.
derive
.
Defined
.
Instance
SubstLemmas_expr
:
SubstLemmas
expr
.
derive
.
Qed
.
Global
Instance
expr_dec_eq
(
e
e
'
:
expr
)
:
Decision
(
e
=
e
'
).
Proof
.
unfold
Decision
.
decide
equality
;
[
apply
eq_nat_dec
|
apply
loc_dec_eq
].
Defined
.
Inductive
val
:=
|
LamV
(
e
:
{
bind
1
of
expr
}
)
|
TLamV
(
e
:
{
bind
1
of
expr
}
)
|
UnitV
|
PairV
(
v1
v2
:
val
)
|
InjLV
(
v
:
val
)
|
InjRV
(
v
:
val
)
|
FoldV
(
e
:
expr
)
|
LocV
(
l
:
loc
).
Global
Instance
val_dec_eq
(
v
v
'
:
val
)
:
Decision
(
v
=
v
'
).
Proof
.
unfold
Decision
;
decide
equality
;
try
apply
expr_dec_eq
;
apply
loc_dec_eq
.
Defined
.
Global
Instance
val_inh
:
Inhabited
val
.
Proof
.
constructor
.
exact
UnitV
.
Qed
.
Fixpoint
of_val
(
v
:
val
)
:
expr
:=
match
v
with
|
LamV
e
=>
Lam
e
|
TLamV
e
=>
TLam
e
|
UnitV
=>
Unit
|
PairV
v1
v2
=>
Pair
(
of_val
v1
)
(
of_val
v2
)
|
InjLV
v
=>
InjL
(
of_val
v
)
|
InjRV
v
=>
InjR
(
of_val
v
)
|
FoldV
e
=>
Fold
e
|
LocV
l
=>
Loc
l
end
.
Fixpoint
to_val
(
e
:
expr
)
:
option
val
:=
match
e
with
|
Lam
e
=>
Some
(
LamV
e
)
|
TLam
e
=>
Some
(
TLamV
e
)
|
Unit
=>
Some
UnitV
|
Pair
e1
e2
=>
v1
←
to_val
e1
;
v2
←
to_val
e2
;
Some
(
PairV
v1
v2
)
|
InjL
e
=>
InjLV
<
$
>
to_val
e
|
InjR
e
=>
InjRV
<
$
>
to_val
e
|
Fold
e
=>
Some
(
FoldV
e
)
|
Loc
l
=>
Some
(
LocV
l
)
|
_
=>
None
end
.
(
**
Evaluation
contexts
*
)
Inductive
ectx_item
:=
|
AppLCtx
(
e2
:
expr
)
|
AppRCtx
(
v1
:
val
)
|
TAppCtx
|
PairLCtx
(
e2
:
expr
)
|
PairRCtx
(
v1
:
val
)
|
FstCtx
|
SndCtx
|
InjLCtx
|
InjRCtx
|
CaseCtx
(
e1
:
{
bind
expr
}
)
(
e2
:
{
bind
expr
}
)
|
UnfoldCtx
|
AllocCtx
|
LoadCtx
|
StoreLCtx
(
e2
:
expr
)
|
StoreRCtx
(
v1
:
val
).
Notation
ectx
:=
(
list
ectx_item
).
Definition
fill_item
(
Ki
:
ectx_item
)
(
e
:
expr
)
:
expr
:=
match
Ki
with
|
AppLCtx
e2
=>
App
e
e2
|
AppRCtx
v1
=>
App
(
of_val
v1
)
e
|
TAppCtx
=>
TApp
e
|
PairLCtx
e2
=>
Pair
e
e2
|
PairRCtx
v1
=>
Pair
(
of_val
v1
)
e
|
FstCtx
=>
Fst
e
|
SndCtx
=>
Snd
e
|
InjLCtx
=>
InjL
e
|
InjRCtx
=>
InjR
e
|
CaseCtx
e1
e2
=>
Case
e
e1
e2
|
UnfoldCtx
=>
Unfold
e
|
AllocCtx
=>
Alloc
e
|
LoadCtx
=>
Load
e
|
StoreLCtx
e2
=>
Store
e
e2
|
StoreRCtx
v1
=>
Store
(
of_val
v1
)
e
end
.
Definition
fill
(
K
:
ectx
)
(
e
:
expr
)
:
expr
:=
fold_right
fill_item
e
K
.
Definition
state
:
Type
:=
gmap
loc
val
.
Inductive
head_step
:
expr
->
state
->
expr
->
state
->
option
expr
->
Prop
:=
(
*
β
*
)
|
BetaS
e1
e2
v2
σ
:
to_val
e2
=
Some
v2
→
head_step
(
App
(
Lam
e1
)
e2
)
σ
e1
.[
e2
/
]
σ
None
(
*
Products
*
)
|
FstS
e1
v1
e2
v2
σ
:
to_val
e1
=
Some
v1
→
to_val
e2
=
Some
v2
→
head_step
(
Fst
(
Pair
e1
e2
))
σ
e1
σ
None
|
SndS
e1
v1
e2
v2
σ
:
to_val
e1
=
Some
v1
→
to_val
e2
=
Some
v2
→
head_step
(
Snd
(
Pair
e1
e2
))
σ
e2
σ
None
(
*
Sums
*
)
|
CaseLS
e0
v0
e1
e2
σ
:
to_val
e0
=
Some
v0
→
head_step
(
Case
(
InjL
e0
)
e1
e2
)
σ
e1
.[
e0
/
]
σ
None
|
CaseRS
e0
v0
e1
e2
σ
:
to_val
e0
=
Some
v0
→
head_step
(
Case
(
InjR
e0
)
e1
e2
)
σ
e2
.[
e0
/
]
σ
None
(
*
Recursive
Types
*
)
|
Unfold_Fold
e
σ
:
head_step
(
Unfold
(
Fold
e
))
σ
e
σ
None
(
*
Polymorphic
Types
*
)
|
TBeta
e
σ
:
head_step
(
TApp
(
TLam
e
))
σ
e
σ
None
(
*
Reference
Types
*
)
|
AllocS
e
v
σ
l
:
to_val
e
=
Some
v
→
σ
!!
l
=
None
→
head_step
(
Alloc
e
)
σ
(
Loc
l
)
(
<
[
l
:=
v
]
>
σ
)
None
|
LoadS
l
v
σ
:
σ
!!
l
=
Some
v
→
head_step
(
Load
(
Loc
l
))
σ
(
of_val
v
)
σ
None
|
StoreS
l
e
v
σ
:
to_val
e
=
Some
v
→
is_Some
(
σ
!!
l
)
→
head_step
(
Store
(
Loc
l
)
e
)
σ
(
Unit
)
(
<
[
l
:=
v
]
>
σ
)
None
.
(
**
Atomic
expressions
:
we
don
'
t
consider
any
atomic
operations
.
*
)
Definition
atomic
(
e
:
expr
)
:=
match
e
with
|
Alloc
e
=>
is_Some
(
to_val
e
)
|
Load
e
=>
is_Some
(
to_val
e
)
|
Store
e1
e2
=>
is_Some
(
to_val
e1
)
∧
is_Some
(
to_val
e2
)
|
_
=>
False
end
.
(
**
Close
reduction
under
evaluation
contexts
.
We
could
potentially
make
this
a
generic
construction
.
*
)
Inductive
prim_step
(
e1
:
expr
)
(
σ
1
:
state
)
(
e2
:
expr
)
(
σ
2
:
state
)
(
ef
:
option
expr
)
:
Prop
:=
Ectx_step
K
e1
'
e2
'
:
e1
=
fill
K
e1
'
→
e2
=
fill
K
e2
'
→
head_step
e1
'
σ
1
e2
'
σ
2
ef
→
prim_step
e1
σ
1
e2
σ
2
ef
.
(
**
Basic
properties
about
the
language
*
)
Lemma
to_of_val
v
:
to_val
(
of_val
v
)
=
Some
v
.
Proof
.
by
induction
v
;
simplify_option_eq
.
Qed
.
Lemma
of_to_val
e
v
:
to_val
e
=
Some
v
→
of_val
v
=
e
.
Proof
.
revert
v
;
induction
e
;
intros
;
simplify_option_eq
;
auto
with
f_equal
.
Qed
.
Instance:
Inj
(
=
)
(
=
)
of_val
.
Proof
.
by
intros
??
Hv
;
apply
(
inj
Some
);
rewrite
-!
to_of_val
Hv
.
Qed
.
Instance
fill_item_inj
Ki
:
Inj
(
=
)
(
=
)
(
fill_item
Ki
).
Proof
.
destruct
Ki
;
intros
???
;
simplify_eq
;
auto
with
f_equal
.
Qed
.
Instance
ectx_fill_inj
K
:
Inj
(
=
)
(
=
)
(
fill
K
).
Proof
.
red
;
induction
K
as
[
|
Ki
K
IH
];
naive_solver
.
Qed
.
Lemma
fill_app
K1
K2
e
:
fill
(
K1
++
K2
)
e
=
fill
K1
(
fill
K2
e
).
Proof
.
revert
e
;
induction
K1
;
simpl
;
auto
with
f_equal
.
Qed
.
Lemma
fill_val
K
e
:
is_Some
(
to_val
(
fill
K
e
))
→
is_Some
(
to_val
e
).
Proof
.
intros
[
v
'
Hv
'
];
revert
v
'
Hv
'
.
induction
K
as
[
|
[]];
intros
;
simplify_option_eq
;
eauto
.
Qed
.
Lemma
fill_not_val
K
e
:
to_val
e
=
None
→
to_val
(
fill
K
e
)
=
None
.
Proof
.
rewrite
!
eq_None_not_Some
;
eauto
using
fill_val
.
Qed
.
Lemma
values_head_stuck
e1
σ
1
e2
σ
2
ef
:
head_step
e1
σ
1
e2
σ
2
ef
→
to_val
e1
=
None
.
Proof
.
destruct
1
;
naive_solver
.
Qed
.
Lemma
values_stuck
e1
σ
1
e2
σ
2
ef
:
prim_step
e1
σ
1
e2
σ
2
ef
→
to_val
e1
=
None
.
Proof
.
intros
[
???
->
->
?
];
eauto
using
fill_not_val
,
values_head_stuck
.
Qed
.
Lemma
atomic_not_val
e
:
atomic
e
→
to_val
e
=
None
.
Proof
.
destruct
e
;
cbn
;
intuition
auto
.
Qed
.
Lemma
atomic_fill_item
Ki
e
:
atomic
(
fill_item
Ki
e
)
→
is_Some
(
to_val
e
).
Proof
.
destruct
Ki
;
cbn
;
intuition
.
Qed
.
Lemma
atomic_fill
K
e
:
atomic
(
fill
K
e
)
→
to_val
e
=
None
→
K
=
[].
Proof
.
destruct
K
as
[
|
k
K
];
cbn
;
trivial
.
rewrite
eq_None_not_Some
.
intros
H
;
apply
atomic_fill_item
,
fill_val
in
H
;
intuition
.
Qed
.
Lemma
atomic_head_step
e1
σ
1
e2
σ
2
ef
:
atomic
e1
→
head_step
e1
σ
1
e2
σ
2
ef
→
is_Some
(
to_val
e2
).
Proof
.
intros
H1
H2
.
destruct
e1
;
inversion
H1
;
inversion
H2
;
subst
;
try
rewrite
to_of_val
;
eauto
using
mk_is_Some
.
Qed
.
Lemma
atomic_step
e1
σ
1
e2
σ
2
ef
:
atomic
e1
→
prim_step
e1
σ
1
e2
σ
2
ef
→
is_Some
(
to_val
e2
).
Proof
.
intros
Hatomic
[
K
e1
'
e2
'
->
->
Hstep
].
assert
(
K
=
[])
as
->
by
eauto
10
using
atomic_fill
,
values_head_stuck
.
naive_solver
eauto
using
atomic_head_step
.
Qed
.
Lemma
head_ctx_step_val
Ki
e
σ
1
e2
σ
2
ef
:
head_step
(
fill_item
Ki
e
)
σ
1
e2
σ
2
ef
→
is_Some
(
to_val
e
).
Proof
.
destruct
Ki
;
inversion_clear
1
;
simplify_option_eq
;
eauto
.
Qed
.
Lemma
fill_item_no_val_inj
Ki1
Ki2
e1
e2
:
to_val
e1
=
None
→
to_val
e2
=
None
→
fill_item
Ki1
e1
=
fill_item
Ki2
e2
→
Ki1
=
Ki2
.
Proof
.
destruct
Ki1
,
Ki2
;
intros
;
try
discriminate
;
simplify_eq
;
repeat
match
goal
with
|
H
:
to_val
(
of_val
_
)
=
None
|-
_
=>
by
rewrite
to_of_val
in
H
end
;
auto
.
Qed
.
(
*
When
something
does
a
step
,
and
another
decomposition
of
the
same
expression
has
a
non
-
val
[
e
]
in
the
hole
,
then
[
K
]
is
a
left
sub
-
context
of
[
K
'
]
-
in
other
words
,
[
e
]
also
contains
the
reducible
expression
*
)
Lemma
step_by_val
K
K
'
e1
e1
'
σ
1
e2
σ
2
ef
:
fill
K
e1
=
fill
K
'
e1
'
→
to_val
e1
=
None
→
head_step
e1
'
σ
1
e2
σ
2
ef
→
K
`prefix_of
`
K
'
.
Proof
.
intros
Hfill
Hred
Hnval
;
revert
K
'
Hfill
.
induction
K
as
[
|
Ki
K
IH
];
simpl
;
intros
K
'
Hfill
;
auto
using
prefix_of_nil
.
destruct
K
'
as
[
|
Ki
'
K
'
];
simplify_eq
.