Skip to content
GitLab
Explore
Sign in
Primary navigation
Search or go to…
Project
I
iris-coq
Manage
Activity
Members
Labels
Plan
Issues
Issue boards
Milestones
Wiki
Code
Merge requests
Repository
Branches
Commits
Tags
Repository graph
Compare revisions
Snippets
Build
Pipelines
Jobs
Pipeline schedules
Artifacts
Deploy
Releases
Model registry
Operate
Environments
Monitor
Incidents
Service Desk
Analyze
Value stream analytics
Contributor analytics
CI/CD analytics
Repository analytics
Model experiments
Help
Help
Support
GitLab documentation
Compare GitLab plans
Community forum
Contribute to GitLab
Provide feedback
Terms and privacy
Keyboard shortcuts
?
Snippets
Groups
Projects
Show more breadcrumbs
Jan
iris-coq
Compare revisions
master to ralf/magic-singleton
Compare revisions
Changes are shown as if the
source
revision was being merged into the
target
revision.
Learn more about comparing revisions.
Source
Quarkbeast/iris-coq
Select target project
No results found
ralf/magic-singleton
Select Git revision
Branches
atomic
ci/janno/vmcast
ci/ralf/atomic
ci/ralf/mtac2-tt
ci/ralf/pm_red
ci/ralf/telescopes
ci/robbert/overloaded_wp
fast_string
gen_proofmode
ipm-notation-broken
iris-3.0
iris-3.1
janno/metacoq
jh/affine_frompure
jh/done_contradiction
jh/evar_iframe
jh/independent_metric
jh/move_bi_affine
jh/sprop_upred
jh_inductive_pairs
joe/defined_pers
less_canonical
less_canonical_new
master
mtac2
mtac2-gt
mtac2-tt
no_always_forall
no_closed
primproj-fail
ralf/auth-frac
ralf/coqbug/ltac-stacktrace
ralf/core
ralf/emp-intro
ralf/magic-singleton
ralf/options-file
ralf/persistently
ralf/plainly
ralf/pm_red
ralf/proofmode-imported
ralf/salways
ralf/tc_control
ralf/tc_control2
ralf/tc_control_full
robbert/cancelable
robbert/iAssert_with
robbert/wp_misc
savedpred
seal_ires
strong_frame
swasey/sequential
telescope
unified_persistent_modality
Tags
appendix-1
appendix-1.0.0
hope-2015-coq-1
iris-1.0
iris-1.1
iris-2.0
iris-2.0-rc1
iris-2.0-rc2
iris-3.0.0
iris-3.1.0
63 results
Swap
Target
iris/iris
Select target project
iris/iris
jeehoon.kang/iris-coq
amintimany/iris-coq
dfrumin/iris-coq
Villetaneuse/iris
gares/iris
shiatsumat/iris
Blaisorblade/iris
jihgfee/iris-coq
mrhaandi/iris
tlsomers/iris
Quarkbeast/iris-coq
janno/iris
amaurremi/iris-coq
proux/iris
tchajed/iris
herbelin/iris-coq
msammler/iris-coq
maximedenes/iris-coq
bpeters/iris
haidang/iris
lepigre/iris
lczch/iris
simonspies/iris
gpirlea/iris
dkhalanskiyjb/iris
gmalecha/iris
germanD/iris
aa755/iris
jules/iris
abeln/iris
simonfv/iris
atrieu/iris
arthuraa/iris
simonh/iris
jung/iris
mattam82/iris
Armael/iris
adamAndMath/iris
gmevel/iris
snyke7/iris
johannes/iris
NiklasM/iris
simonspies/iris-parametric-index
svancollem/iris
proux1/iris
wmansky/iris
LukeXuan/iris
ivanbakel/iris
SkySkimmer/iris
tjhance/iris
yiyunliu/iris
Lee-Janggun/iris
thomas-lamiaux/iris
dongjae/iris
dnezam/iris
Tragicus/iris
clef-men/iris
ffengyu/iris
59 results
master
Select Git revision
Branches
ci/debug
ci/for_proph
ci/general-contractive
ci/hai/siProp
ci/hint-cut-revert
ci/janno/strict-tc-resolution
ci/msammler/nb_state
ci/name-mangle
ci/ralf/Z_of_nat
ci/ralf/bi-language
ci/ralf/options-timing
ci/robbert/big_op_binder
ci/robbert/contractive_ne
ci/robbert/coq_bug_7773
ci/robbert/faster_iDestruct
ci/robbert/faster_iDestruct2
ci/robbert/faster_iFresh_joe
ci/robbert/frame_fractional
ci/robbert/hint_cut_plain
ci/robbert/iFrame
ci/robbert/into_fupd
ci/robbert/into_val_pures
ci/robbert/kill_locked_value_lambdas
ci/robbert/mapsto_persist
ci/robbert/merge_sbi
ci/robbert/naive_solver
ci/robbert/set_solver_eauto
ci/robbert/set_unfold
ci/robbert/tc_opaque
ci/stability
ci/timing
coq-bugs/tc-resolution-cannot-unify-with-self
fast_string
hai/si_embed
iris-3.0
iris-3.1
iris-3.2
iris-3.3
iris-3.4
jh/simplify_na_inv
jh/sprop_upred
less_canonical
less_canonical_new
master
ralf/Z
ralf/bi-persistently-emp
ralf/bi-quant-universe-gone
ralf/coq-bug-13942
ralf/emp-intro
ralf/f_equiv
ralf/f_equiv_ho
ralf/has-lc
ralf/make
ralf/notc-apply
ralf/ra-infer
ralf/sprop
ralf/vs-mask-adjust
ralf/wp_apply-no-simpl
robbert/Qp
robbert/add_sub
robbert/affine_notations
robbert/array_init
robbert/bi_cofe
robbert/big_sepM2
robbert/bupd_be_gone
robbert/clprop
robbert/docs_1_2_lemmas
robbert/fail_ofe_bi
robbert/frame_new_unification
robbert/fupd_elim
robbert/has_lc_if
robbert/hint_cut_plain
robbert/iAssert_with
robbert/iFrame_fail_more_work
robbert/iIntro_iDestruct_fresh
robbert/internal_fractional_tweaks
robbert/into_forall_eta
robbert/issue_331
robbert/level
robbert/local_ltac_proofmode
robbert/lock_G_Σ
robbert/lock_no_gamma
robbert/no_always_forall
robbert/no_native_compute
robbert/own_ghost
robbert/plausibly
robbert/pm_unify_class
robbert/prepend
robbert/pwp
robbert/reservation_map_False
robbert/resolve_tc
robbert/sbi
robbert/stdpp_mr281
robbert/thread_local_wp
robbert/unbundle_chain
robbert/wp_apply_better
seal_ires
simon/parametric-index
step_fupdN_support
strong_frame
Tags
appendix-1
appendix-1.0.0
hope-2015-coq-1
iris-1.0
iris-1.1
iris-2.0
iris-2.0-rc1
iris-2.0-rc2
iris-3.0.0
iris-3.1.0
iris-3.2.0
iris-3.3.0
iris-3.4.0
iris-3.5.0
iris-3.6.0
iris-4.0.0
iris-4.1.0
iris-4.2.0
iris-4.3.0
iris-4.4.0
120 results
Show changes
Only incoming changes from source
Include changes to target since source was created
Compare
Commits on Source (3)
WIP: expr as dependent type
· 2914aeba
Ralf Jung
authored
9 years ago
2914aeba
WIP: nicer definition of head_step
· e0c04005
Ralf Jung
authored
9 years ago
e0c04005
demonstrate a weird issue
· 9bd5532f
Ralf Jung
authored
9 years ago
9bd5532f
Hide whitespace changes
Inline
Side-by-side
Showing
1 changed file
heap_lang/lang.v
+208
-101
208 additions, 101 deletions
heap_lang/lang.v
with
208 additions
and
101 deletions
heap_lang/lang.v
View file @
9bd5532f
From
program_logic
Require
Export
language
.
From
prelude
Require
Export
strings
.
From
prelude
Require
Export
strings
stringmap
.
From
prelude
Require
Import
gmap
.
Module
heap_lang
.
...
...
@@ -15,35 +15,45 @@ Inductive un_op : Set :=
Inductive
bin_op
:
Set
:=
|
PlusOp
|
MinusOp
|
LeOp
|
LtOp
|
EqOp
.
Inductive
expr
:=
(* expr X is the type of expressions with free variables bounded by X.
I removed the "empty binder" hack since it does not go well with
proof irrelevance of the proof required for [Var]. If we really want
that back, we should change the binders in [Rec] to "option string". *)
Inductive
expr
{
X
:
stringset
}
:
Type
:=
(* Base lambda calculus *)
|
Var
(
x
:
string
)
|
Rec
(
f
x
:
string
)
(
e
:
expr
)
|
App
(
e1
e2
:
expr
)
|
Var
(
x
:
string
)
{
H
:
x
∈
X
}
:
@
expr
X
|
Rec
(
f
x
:
string
)
(
e
:
@
expr
((
X
∪
{[
x
]})
∪
{[
f
]}))
:
@
expr
X
|
App
(
e1
e2
:
@
expr
X
)
:
@
expr
X
(* Base types and their operations *)
|
Lit
(
l
:
base_lit
)
|
UnOp
(
op
:
un_op
)
(
e
:
expr
)
|
BinOp
(
op
:
bin_op
)
(
e1
e2
:
expr
)
|
If
(
e0
e1
e2
:
expr
)
|
Lit
(
l
:
base_lit
)
:
@
expr
X
|
UnOp
(
op
:
un_op
)
(
e
:
@
expr
X
)
:
@
expr
X
|
BinOp
(
op
:
bin_op
)
(
e1
e2
:
@
expr
X
)
:
@
expr
X
|
If
(
e0
e1
e2
:
@
expr
X
)
:
@
expr
X
(* Products *)
|
Pair
(
e1
e2
:
expr
)
|
Fst
(
e
:
expr
)
|
Snd
(
e
:
expr
)
|
Pair
(
e1
e2
:
@
expr
X
)
:
@
expr
X
|
Fst
(
e
:
@
expr
X
)
:
@
expr
X
|
Snd
(
e
:
@
expr
X
)
:
@
expr
X
(* Sums *)
|
InjL
(
e
:
expr
)
|
InjR
(
e
:
expr
)
|
Case
(
e0
:
expr
)
(
x1
:
string
)
(
e1
:
expr
)
(
x2
:
string
)
(
e2
:
expr
)
|
InjL
(
e
:
@
expr
X
)
:
@
expr
X
|
InjR
(
e
:
@
expr
X
)
:
@
expr
X
|
Case
(
e0
e1
e2
:
@
expr
X
)
:
@
expr
X
(* Concurrency *)
|
Fork
(
e
:
expr
)
|
Fork
(
e
:
@
expr
X
)
:
@
expr
X
(* Heap *)
|
Loc
(
l
:
loc
)
|
Alloc
(
e
:
expr
)
|
Load
(
e
:
expr
)
|
Store
(
e1
:
expr
)
(
e2
:
expr
)
|
Cas
(
e0
:
expr
)
(
e1
:
expr
)
(
e2
:
expr
)
.
|
Loc
(
l
:
loc
)
:
@
expr
X
|
Alloc
(
e
:
@
expr
X
)
:
@
expr
X
|
Load
(
e
:
@
expr
X
)
:
@
expr
X
|
Store
(
e1
e2
:
@
expr
X
)
:
@
expr
X
|
Cas
(
e0
e1
e2
:
@
expr
X
)
:
@
expr
X
.
(* X should be explicit for a few of them: Those that do not take an expr of the same X *)
Arguments
expr
_
:
clear
implicits
.
Arguments
Var
_
_
{_}
:
clear
implicits
.
Arguments
Rec
_
_
_
_
:
clear
implicits
.
Arguments
Lit
_
_
:
clear
implicits
.
Arguments
Loc
_
_
:
clear
implicits
.
Inductive
val
:=
|
RecV
(
f
x
:
string
)
(
e
:
expr
)
(
* e should be closed *
)
|
RecV
(
f
x
:
string
)
(
e
:
expr
(
(
∅
∪
{[
x
]})
∪
{[
f
]})
)
|
LitV
(
l
:
base_lit
)
|
PairV
(
v1
v2
:
val
)
|
InjLV
(
v
:
val
)
...
...
@@ -56,25 +66,56 @@ Global Instance un_op_dec_eq (op1 op2 : un_op) : Decision (op1 = op2).
Proof
.
solve_decision
.
Defined
.
Global
Instance
bin_op_dec_eq
(
op1
op2
:
bin_op
)
:
Decision
(
op1
=
op2
)
.
Proof
.
solve_decision
.
Defined
.
Global
Instance
expr_dec_eq
(
e1
e2
:
expr
)
:
Decision
(
e1
=
e2
)
.
(*
Global Instance expr_dec_eq
{X}
(e1 e2 : expr
X
) : Decision (e1 = e2).
Proof. solve_decision. Defined.
Global Instance val_dec_eq (v1 v2 : val) : Decision (v1 = v2).
Proof
.
solve_decision
.
Defined
.
Proof. solve_decision. Defined.
*)
Delimit
Scope
lang_scope
with
L
.
Bind
Scope
lang_scope
with
expr
val
.
Fixpoint
of_val
(
v
:
val
)
:
expr
:=
match
v
with
|
RecV
f
x
e
=>
Rec
f
x
e
|
LitV
l
=>
Lit
l
|
PairV
v1
v2
=>
Pair
(
of_val
v1
)
(
of_val
v2
)
|
InjLV
v
=>
InjL
(
of_val
v
)
|
InjRV
v
=>
InjR
(
of_val
v
)
|
LocV
l
=>
Loc
l
Definition
expr_cast
{
X1
X2
}
{
H
:
X1
=
X2
}
(
e
:
expr
X1
)
:
expr
X2
:=
eq_rect
_
(
λ
X
,
expr
X
)
e
_
H
.
Program
Fixpoint
expr_weaken
{
X1
X2
:
stringset
}
{
H
:
X1
⊆
X2
}
(
e
:
expr
X1
)
:
expr
X2
:=
match
e
return
_
with
|
Var
x
Hx
=>
Var
X2
x
|
Rec
f
x
e
=>
Rec
X2
f
x
(
expr_weaken
e
)
|
App
e1
e2
=>
App
(
expr_weaken
(
H
:=
H
)
e1
)
(
expr_weaken
(
H
:=
H
)
e2
)
|
Lit
l
=>
Lit
X2
l
|
UnOp
op
e
=>
UnOp
op
(
expr_weaken
(
H
:=
H
)
e
)
|
BinOp
op
e1
e2
=>
BinOp
op
(
expr_weaken
(
H
:=
H
)
e1
)
(
expr_weaken
(
H
:=
H
)
e2
)
|
If
e0
e1
e2
=>
If
(
expr_weaken
(
H
:=
H
)
e0
)
(
expr_weaken
(
H
:=
H
)
e1
)
(
expr_weaken
(
H
:=
H
)
e2
)
|
Pair
e1
e2
=>
Pair
(
expr_weaken
(
H
:=
H
)
e1
)
(
expr_weaken
(
H
:=
H
)
e2
)
|
Fst
e
=>
Fst
(
expr_weaken
(
H
:=
H
)
e
)
|
Snd
e
=>
Snd
(
expr_weaken
(
H
:=
H
)
e
)
|
InjL
e
=>
InjL
(
expr_weaken
(
H
:=
H
)
e
)
|
InjR
e
=>
InjR
(
expr_weaken
(
H
:=
H
)
e
)
|
Case
e0
e1
e2
=>
Case
(
expr_weaken
(
H
:=
H
)
e0
)
(
expr_weaken
(
H
:=
H
)
e1
)
(
expr_weaken
(
H
:=
H
)
e2
)
|
Fork
e
=>
Fork
(
expr_weaken
(
H
:=
H
)
e
)
|
Loc
l
=>
Loc
X2
l
|
Alloc
e
=>
Alloc
(
expr_weaken
(
H
:=
H
)
e
)
|
Load
e
=>
Load
(
expr_weaken
(
H
:=
H
)
e
)
|
Store
e1
e2
=>
Store
(
expr_weaken
(
H
:=
H
)
e1
)
(
expr_weaken
(
H
:=
H
)
e2
)
|
Cas
e0
e1
e2
=>
Cas
(
expr_weaken
(
H
:=
H
)
e0
)
(
expr_weaken
(
H
:=
H
)
e1
)
(
expr_weaken
(
H
:=
H
)
e2
)
end
.
Fixpoint
to_val
(
e
:
expr
)
:
option
val
:=
match
e
with
Solve
Obligations
with
set_solver
.
Program
Fixpoint
of_val
X
(
v
:
val
)
:
expr
X
:=
match
v
return
expr
X
with
|
RecV
f
x
e
=>
Rec
X
f
x
(
expr_weaken
e
)
|
LitV
l
=>
Lit
X
l
|
PairV
v1
v2
=>
Pair
(
of_val
X
v1
)
(
of_val
X
v2
)
|
InjLV
v
=>
InjL
(
of_val
X
v
)
|
InjRV
v
=>
InjR
(
of_val
X
v
)
|
LocV
l
=>
Loc
X
l
end
.
Solve
Obligations
with
set_solver
.
Fixpoint
to_val
(
e
:
expr
∅
)
:
option
val
:=
match
e
return
option
val
with
(* The LHS of thus ⊆ must be like the argument of Rec, the RHS
must be like the argument of RecV. *)
|
Rec
f
x
e
=>
Some
(
RecV
f
x
e
)
|
Lit
l
=>
Some
(
LitV
l
)
|
Pair
e1
e2
=>
v1
←
to_val
e1
;
v2
←
to_val
e2
;
Some
(
PairV
v1
v2
)
...
...
@@ -89,82 +130,94 @@ Definition state := gmap loc val.
(** Evaluation contexts *)
Inductive
ectx_item
:=
|
AppLCtx
(
e2
:
expr
)
|
AppLCtx
(
e2
:
expr
∅
)
|
AppRCtx
(
v1
:
val
)
|
UnOpCtx
(
op
:
un_op
)
|
BinOpLCtx
(
op
:
bin_op
)
(
e2
:
expr
)
|
BinOpLCtx
(
op
:
bin_op
)
(
e2
:
expr
∅
)
|
BinOpRCtx
(
op
:
bin_op
)
(
v1
:
val
)
|
IfCtx
(
e1
e2
:
expr
)
|
PairLCtx
(
e2
:
expr
)
|
IfCtx
(
e1
e2
:
expr
∅
)
|
PairLCtx
(
e2
:
expr
∅
)
|
PairRCtx
(
v1
:
val
)
|
FstCtx
|
SndCtx
|
InjLCtx
|
InjRCtx
|
CaseCtx
(
x1
:
string
)
(
e1
:
expr
)
(
x2
:
string
)
(
e2
:
expr
)
|
CaseCtx
(
e1
:
expr
∅
)
(
e2
:
expr
∅
)
|
AllocCtx
|
LoadCtx
|
StoreLCtx
(
e2
:
expr
)
|
StoreLCtx
(
e2
:
expr
∅
)
|
StoreRCtx
(
v1
:
val
)
|
CasLCtx
(
e1
:
expr
)
(
e2
:
expr
)
|
CasMCtx
(
v0
:
val
)
(
e2
:
expr
)
|
CasLCtx
(
e1
:
expr
∅
)
(
e2
:
expr
∅
)
|
CasMCtx
(
v0
:
val
)
(
e2
:
expr
∅
)
|
CasRCtx
(
v0
:
val
)
(
v1
:
val
)
.
Notation
ectx
:=
(
list
ectx_item
)
.
Definition
fill_item
(
Ki
:
ectx_item
)
(
e
:
expr
)
:
expr
:=
match
Ki
with
Definition
fill_item
(
Ki
:
ectx_item
)
(
e
:
expr
∅
)
:
expr
∅
:=
match
Ki
return
expr
∅
with
|
AppLCtx
e2
=>
App
e
e2
|
AppRCtx
v1
=>
App
(
of_val
v1
)
e
|
AppRCtx
v1
=>
App
(
of_val
∅
v1
)
e
|
UnOpCtx
op
=>
UnOp
op
e
|
BinOpLCtx
op
e2
=>
BinOp
op
e
e2
|
BinOpRCtx
op
v1
=>
BinOp
op
(
of_val
v1
)
e
|
BinOpRCtx
op
v1
=>
BinOp
op
(
of_val
∅
v1
)
e
|
IfCtx
e1
e2
=>
If
e
e1
e2
|
PairLCtx
e2
=>
Pair
e
e2
|
PairRCtx
v1
=>
Pair
(
of_val
v1
)
e
|
PairRCtx
v1
=>
Pair
(
of_val
∅
v1
)
e
|
FstCtx
=>
Fst
e
|
SndCtx
=>
Snd
e
|
InjLCtx
=>
InjL
e
|
InjRCtx
=>
InjR
e
|
CaseCtx
x1
e1
x2
e2
=>
Case
e
x1
e1
x2
e2
|
CaseCtx
e1
e2
=>
Case
e
e1
e2
|
AllocCtx
=>
Alloc
e
|
LoadCtx
=>
Load
e
|
StoreLCtx
e2
=>
Store
e
e2
|
StoreRCtx
v1
=>
Store
(
of_val
v1
)
e
|
StoreRCtx
v1
=>
Store
(
of_val
∅
v1
)
e
|
CasLCtx
e1
e2
=>
Cas
e
e1
e2
|
CasMCtx
v0
e2
=>
Cas
(
of_val
v0
)
e
e2
|
CasRCtx
v0
v1
=>
Cas
(
of_val
v0
)
(
of_val
v1
)
e
|
CasMCtx
v0
e2
=>
Cas
(
of_val
∅
v0
)
e
e2
|
CasRCtx
v0
v1
=>
Cas
(
of_val
∅
v0
)
(
of_val
∅
v1
)
e
end
.
Definition
fill
(
K
:
ectx
)
(
e
:
expr
)
:
expr
:=
fold_right
fill_item
e
K
.
Definition
fill
(
K
:
ectx
)
(
e
:
expr
∅
)
:
expr
∅
:=
fold_right
fill_item
e
K
.
(** Substitution *)
(** We have [subst e "" v = e] to deal with anonymous binders *)
Fixpoint
subst
(
e
:
expr
)
(
x
:
string
)
(
v
:
val
)
:
expr
:=
match
e
with
|
Var
y
=>
if
decide
(
x
=
y
∧
x
≠
""
)
then
of_val
v
else
Var
y
|
Rec
f
y
e
=>
Rec
f
y
(
if
decide
(
x
≠
f
∧
x
≠
y
)
then
subst
e
x
v
else
e
)
|
App
e1
e2
=>
App
(
subst
e1
x
v
)
(
subst
e2
x
v
)
|
Lit
l
=>
Lit
l
|
UnOp
op
e
=>
UnOp
op
(
subst
e
x
v
)
|
BinOp
op
e1
e2
=>
BinOp
op
(
subst
e1
x
v
)
(
subst
e2
x
v
)
|
If
e0
e1
e2
=>
If
(
subst
e0
x
v
)
(
subst
e1
x
v
)
(
subst
e2
x
v
)
|
Pair
e1
e2
=>
Pair
(
subst
e1
x
v
)
(
subst
e2
x
v
)
|
Fst
e
=>
Fst
(
subst
e
x
v
)
|
Snd
e
=>
Snd
(
subst
e
x
v
)
|
InjL
e
=>
InjL
(
subst
e
x
v
)
|
InjR
e
=>
InjR
(
subst
e
x
v
)
|
Case
e0
x1
e1
x2
e2
=>
Case
(
subst
e0
x
v
)
x1
(
if
decide
(
x
≠
x1
)
then
subst
e1
x
v
else
e1
)
x2
(
if
decide
(
x
≠
x2
)
then
subst
e2
x
v
else
e2
)
|
Fork
e
=>
Fork
(
subst
e
x
v
)
|
Loc
l
=>
Loc
l
|
Alloc
e
=>
Alloc
(
subst
e
x
v
)
|
Load
e
=>
Load
(
subst
e
x
v
)
|
Store
e1
e2
=>
Store
(
subst
e1
x
v
)
(
subst
e2
x
v
)
|
Cas
e0
e1
e2
=>
Cas
(
subst
e0
x
v
)
(
subst
e1
x
v
)
(
subst
e2
x
v
)
Program
Fixpoint
subst
X
(
x
:
string
)
(
v
:
val
)
(
e
:
expr
(
X
∪
{[
x
]}))
:
expr
X
:=
match
e
return
expr
X
with
|
Var
y
Hx
=>
if
decide
(
x
=
y
)
then
of_val
X
v
else
Var
X
y
|
Rec
f
y
e
=>
Rec
X
f
y
(
if
decide
(
x
≠
f
∧
x
≠
y
)
then
subst
((
X
∪
{[
y
]})
∪
{[
f
]})
x
v
(
expr_cast
e
)
else
expr_cast
e
)
|
App
e1
e2
=>
App
(
subst
X
x
v
e1
)
(
subst
X
x
v
e2
)
|
Lit
l
=>
Lit
X
l
|
UnOp
op
e
=>
UnOp
op
(
subst
X
x
v
e
)
|
BinOp
op
e1
e2
=>
BinOp
op
(
subst
X
x
v
e1
)
(
subst
X
x
v
e2
)
|
If
e0
e1
e2
=>
If
(
subst
X
x
v
e0
)
(
subst
X
x
v
e1
)
(
subst
X
x
v
e2
)
|
Pair
e1
e2
=>
Pair
(
subst
X
x
v
e1
)
(
subst
X
x
v
e2
)
|
Fst
e
=>
Fst
(
subst
X
x
v
e
)
|
Snd
e
=>
Snd
(
subst
X
x
v
e
)
|
InjL
e
=>
InjL
(
subst
X
x
v
e
)
|
InjR
e
=>
InjR
(
subst
X
x
v
e
)
|
Case
e0
e1
e2
=>
Case
(
subst
X
x
v
e0
)
(
subst
X
x
v
e1
)
(
subst
X
x
v
e2
)
|
Fork
e
=>
Fork
(
subst
X
x
v
e
)
|
Loc
l
=>
Loc
X
l
|
Alloc
e
=>
Alloc
(
subst
X
x
v
e
)
|
Load
e
=>
Load
(
subst
X
x
v
e
)
|
Store
e1
e2
=>
Store
(
subst
X
x
v
e1
)
(
subst
X
x
v
e2
)
|
Cas
e0
e1
e2
=>
Cas
(
subst
X
x
v
e0
)
(
subst
X
x
v
e1
)
(
subst
X
x
v
e2
)
end
.
Next
Obligation
.
set_solver
.
Qed
.
Next
Obligation
.
set_solver
.
Qed
.
(* FIXME fix this *)
Next
Obligation
.
intros
???????
[
H
%
dec_stable
|
H
%
dec_stable
]
%
not_and_l
;
subst
.
-
apply
elem_of_equiv_L
=>
x
.
destruct
(
decide
(
x
=
f
));
set_solver
.
-
apply
elem_of_equiv_L
=>
x
.
destruct
(
decide
(
x
=
y
));
set_solver
.
Qed
.
(** The stepping relation *)
Definition
un_op_eval
(
op
:
un_op
)
(
l
:
base_lit
)
:
option
base_lit
:=
match
op
,
l
with
...
...
@@ -183,55 +236,61 @@ Definition bin_op_eval (op : bin_op) (l1 l2 : base_lit) : option base_lit :=
|
_,
_,
_
=>
None
end
.
Inductive
head_step
:
expr
→
state
→
expr
→
state
→
option
expr
→
Prop
:=
|
BetaS
f
x
e1
e2
v2
σ
:
Inductive
head_step
:
expr
∅
→
state
→
expr
∅
→
state
→
option
(
expr
∅
)
→
Prop
:=
(* The second "x" in the type of [e1] should be an "f". *)
|
BetaS
(
f
x
:
string
)
(
e1
:
expr
((
∅
∪
{[
x
]})
∪
{[
x
]}))
(
e2
:
expr
∅
)
v2
(
σ
:
state
)
:
to_val
e2
=
Some
v2
→
head_step
(
App
(
Rec
f
x
e1
)
e2
)
σ
(
subst
(
subst
e1
f
(
RecV
f
x
e1
))
x
v2
)
σ
None
head_step
(
App
(
Rec
∅
f
x
e1
)
e2
)
σ
(
subst
∅
x
v2
(
subst
(
∅
∪
{[
x
]})
f
(
RecV
f
x
e1
)
e1
))
σ
None
.
Set
Printing
All
.
Print
head_step
.
|
UnOpS
op
l
l'
σ
:
un_op_eval
op
l
=
Some
l'
→
head_step
(
UnOp
op
(
Lit
l
))
σ
(
Lit
l'
)
σ
None
head_step
(
UnOp
op
(
Lit
∅
l
))
σ
(
Lit
∅
l'
)
σ
None
|
BinOpS
op
l1
l2
l'
σ
:
bin_op_eval
op
l1
l2
=
Some
l'
→
head_step
(
BinOp
op
(
Lit
l1
)
(
Lit
l2
))
σ
(
Lit
l'
)
σ
None
head_step
(
BinOp
op
(
Lit
∅
l1
)
(
Lit
∅
l2
))
σ
(
Lit
∅
l'
)
σ
None
|
IfTrueS
e1
e2
σ
:
head_step
(
If
(
Lit
$
LitBool
true
)
e1
e2
)
σ
e1
σ
None
head_step
(
If
(
Lit
∅
$
LitBool
true
)
e1
e2
)
σ
e1
σ
None
|
IfFalseS
e1
e2
σ
:
head_step
(
If
(
Lit
$
LitBool
false
)
e1
e2
)
σ
e2
σ
None
head_step
(
If
(
Lit
∅
$
LitBool
false
)
e1
e2
)
σ
e2
σ
None
|
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
|
CaseLS
e0
v0
x1
e1
x2
e2
σ
:
|
CaseLS
e0
v0
e1
e2
σ
:
to_val
e0
=
Some
v0
→
head_step
(
Case
(
InjL
e0
)
x1
e1
x2
e2
)
σ
(
subst
e1
x1
v0
)
σ
None
|
CaseRS
e0
v0
x1
e1
x2
e2
σ
:
head_step
(
Case
(
InjL
e0
)
e1
e2
)
σ
(
App
e1
(
of_val
∅
v0
)
)
σ
None
|
CaseRS
e0
v0
e1
e2
σ
:
to_val
e0
=
Some
v0
→
head_step
(
Case
(
InjR
e0
)
x1
e1
x2
e2
)
σ
(
subst
e2
x2
v0
)
σ
None
head_step
(
Case
(
InjR
e0
)
e1
e2
)
σ
(
App
e2
(
of_val
∅
v0
)
)
σ
None
|
ForkS
e
σ
:
head_step
(
Fork
e
)
σ
(
Lit
LitUnit
)
σ
(
Some
e
)
head_step
(
Fork
e
)
σ
(
Lit
∅
LitUnit
)
σ
(
Some
e
)
|
AllocS
e
v
σ
l
:
to_val
e
=
Some
v
→
σ
!!
l
=
None
→
head_step
(
Alloc
e
)
σ
(
Loc
l
)
(
<
[
l
:=
v
]
>
σ
)
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
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
)
σ
(
Lit
LitUnit
)
(
<
[
l
:=
v
]
>
σ
)
None
head_step
(
Store
(
Loc
∅
l
)
e
)
σ
(
Lit
∅
LitUnit
)
(
<
[
l
:=
v
]
>
σ
)
None
|
CasFailS
l
e1
v1
e2
v2
vl
σ
:
to_val
e1
=
Some
v1
→
to_val
e2
=
Some
v2
→
σ
!!
l
=
Some
vl
→
vl
≠
v1
→
head_step
(
Cas
(
Loc
l
)
e1
e2
)
σ
(
Lit
$
LitBool
false
)
σ
None
head_step
(
Cas
(
Loc
∅
l
)
e1
e2
)
σ
(
Lit
∅
$
LitBool
false
)
σ
None
|
CasSucS
l
e1
v1
e2
v2
σ
:
to_val
e1
=
Some
v1
→
to_val
e2
=
Some
v2
→
σ
!!
l
=
Some
v1
→
head_step
(
Cas
(
Loc
l
)
e1
e2
)
σ
(
Lit
$
LitBool
true
)
(
<
[
l
:=
v2
]
>
σ
)
None
.
head_step
(
Cas
(
Loc
∅
l
)
e1
e2
)
σ
(
Lit
∅
$
LitBool
true
)
(
<
[
l
:=
v2
]
>
σ
)
None
.
(** Atomic expressions *)
Definition
atomic
(
e
:
expr
)
:
Prop
:=
Definition
atomic
(
e
:
expr
∅
)
:
Prop
:=
match
e
with
|
Alloc
e
=>
is_Some
(
to_val
e
)
|
Load
e
=>
is_Some
(
to_val
e
)
...
...
@@ -245,25 +304,71 @@ Definition atomic (e: expr) : Prop :=
(** 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
:=
(
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
.
(** The equalities we need for some lemmas. *)
Lemma
stringset_eq_1
{
X
:
stringset
}
:
X
=
∅
∪
X
.
Proof
.
set_solver
.
Qed
.
Lemma
stringset_eq_2
{
f
x
:
string
}
:
(({[
f
;
x
]}
∖
{[
f
]})
∖
{[
x
]})
=
(
∅
:
stringset
)
.
Proof
.
set_solver
.
Qed
.
Lemma
stringset_subseteq_1
{
X
:
stringset
}
:
∅
⊆
X
.
Proof
.
set_solver
.
Qed
.
(** Properties of the cast operators *)
Lemma
not_or_l
{
P
Q
:
Prop
}
`{
Decision
P
}
:
¬
(
P
∨
Q
)
↔
¬
P
∧
¬
Q
.
Proof
.
destruct
(
decide
P
);
tauto
.
Qed
.
Lemma
not_or_r
{
P
Q
:
Prop
}
`{
Decision
Q
}
:
¬
(
P
∨
Q
)
↔
¬
P
∧
¬
Q
.
Proof
.
destruct
(
decide
Q
);
tauto
.
Qed
.
Lemma
expr_weaken_id
{
X
:
stringset
}
{
H
:
X
⊆
X
}
(
e
:
expr
X
)
:
expr_weaken
(
H
:=
H
)
e
=
e
.
Proof
.
induction
e
;
simpl
;
by
(
f_equal
;
try
apply
proof_irrel
;
eauto
)
.
Qed
.
Lemma
expr_weaken_cast_id
{
X
Y
:
stringset
}
{
H1
:
Y
⊆
X
}
{
H2
:
X
=
Y
}
(
e
:
expr
X
)
:
expr_weaken
(
H
:=
H1
)
(
expr_cast
(
H
:=
H2
)
e
)
=
e
.
Proof
.
destruct
H2
.
by
apply
expr_weaken_id
.
Qed
.
Lemma
expr_weaken_cast_weaken_id
{
X
Y
Z
:
stringset
}
{
H1
:
Z
⊆
X
}
{
H2
:
Y
=
Z
}
{
H3
:
X
⊆
Y
}
(
e
:
expr
X
)
:
expr_weaken
(
H
:=
H1
)
(
expr_cast
(
H
:=
H2
)
(
expr_weaken
(
H
:=
H3
)
e
))
=
e
.
Proof
.
destruct
H2
.
assert
(
X
=
Y
)
by
set_solver
.
subst
Y
.
by
rewrite
!
expr_weaken_id
.
Qed
.
Lemma
expr_cast_val
{
X
Y
:
stringset
}
{
H
:
X
=
Y
}
e
:
to_val
(
expr_cast
(
H
:=
H
)
e
)
=
to_val
e
.
Proof
.
destruct
H
.
done
.
Qed
.
(** 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
.
Proof
.
induction
v
;
simpl
;
try
case_match
;
simplify_option_eq
;
try
done
.
-
f_equiv
.
f_equiv
.
by
rewrite
expr_weaken_cast_id
.
-
exfalso
.
apply
H
.
set_solver
+.
Qed
.
Lemma
of_to_val
e
v
:
to_val
e
=
Some
v
→
of_val
v
=
e
.
Lemma
of_to_val
'
X
(
e
:
expr
X
)
v
:
to_val
e
=
Some
v
→
expr_weaken
(
H
:=
stringset_subseteq_1
)
(
of_val
v
)
=
e
.
Proof
.
revert
v
;
induction
e
;
intros
;
simplify_option_eq
;
auto
with
f_equal
.
f_equiv
.
by
rewrite
expr_weaken_cast_weaken_id
.
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
??
?
;
simpl
ify_eq
/=
;
auto
with
f_equal
.
Qed
.
Proof
.
destruct
Ki
;
intros
??
H
;
simpl
in
*
;
inversion_clear
H
;
done
.
Qed
.
Instance
ectx_fill_inj
K
:
Inj
(
=
)
(
=
)
(
fill
K
)
.
Proof
.
red
;
induction
K
as
[|
Ki
K
IH
];
naive_solver
.
Qed
.
...
...
@@ -294,6 +399,7 @@ Lemma atomic_fill_item Ki e : atomic (fill_item Ki e) → is_Some (to_val e).
Proof
.
intros
.
destruct
Ki
;
simplify_eq
/=
;
destruct_conjs
;
repeat
(
case_match
||
contradiction
);
eauto
.
simpl
.
case_match
;
first
by
eauto
.
exfalso
.
apply
n
.
set_solver
+.
Qed
.
Lemma
atomic_fill
K
e
:
atomic
(
fill
K
e
)
→
to_val
e
=
None
→
K
=
[]
.
...
...
@@ -307,6 +413,7 @@ Lemma atomic_head_step e1 σ1 e2 σ2 ef :
Proof
.
destruct
2
;
simpl
;
rewrite
?to_of_val
;
try
by
eauto
.
repeat
(
case_match
||
contradiction
||
simplify_eq
/=
);
eauto
.
rewrite
expr_cast_val
.
Qed
.
Lemma
atomic_step
e1
σ1
e2
σ2
ef
:
...
...
This diff is collapsed.
Click to expand it.