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
George Pirlea
Iris
Commits
5fdfeb82
Commit
5fdfeb82
authored
Mar 02, 2016
by
Robbert Krebbers
Browse files
Rename values_stuck -> val_stuck
For consistency's sake.
parent
e88614cb
Changes
4
Hide whitespace changes
Inline
Side-by-side
heap_lang/lang.v
View file @
5fdfeb82
...
...
@@ -293,12 +293,12 @@ 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
val
ues
_head_stuck
e1
σ
1 e2
σ
2
ef
:
Lemma
val_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
val
ues
_stuck
e1
σ
1 e2
σ
2
ef
:
prim_step
e1
σ
1 e2
σ
2
ef
→
to_val
e1
=
None
.
Proof
.
intros
[???
->
->
?]
;
eauto
using
fill_not_val
,
val
ues
_head_stuck
.
Qed
.
Lemma
val_stuck
e1
σ
1 e2
σ
2
ef
:
prim_step
e1
σ
1 e2
σ
2
ef
→
to_val
e1
=
None
.
Proof
.
intros
[???
->
->
?]
;
eauto
using
fill_not_val
,
val_head_stuck
.
Qed
.
Lemma
atomic_not_val
e
:
atomic
e
→
to_val
e
=
None
.
Proof
.
destruct
e
;
naive_solver
.
Qed
.
...
...
@@ -326,7 +326,7 @@ 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
,
val
ues
_head_stuck
.
assert
(
K
=
[])
as
->
by
eauto
10
using
atomic_fill
,
val_head_stuck
.
naive_solver
eauto
using
atomic_head_step
.
Qed
.
...
...
@@ -357,7 +357,7 @@ Proof.
{
exfalso
;
apply
(
eq_None_not_Some
(
to_val
(
fill
K
e1
)))
;
eauto
using
fill_not_val
,
head_ctx_step_val
.
}
cut
(
Ki
=
Ki'
)
;
[
naive_solver
eauto
using
prefix_of_cons
|].
eauto
using
fill_item_no_val_inj
,
val
ues
_head_stuck
,
fill_not_val
.
eauto
using
fill_item_no_val_inj
,
val_head_stuck
,
fill_not_val
.
Qed
.
Lemma
alloc_fresh
e
v
σ
:
...
...
@@ -373,7 +373,7 @@ Program Canonical Structure heap_lang : language := {|
atomic
:
=
heap_lang
.
atomic
;
prim_step
:
=
heap_lang
.
prim_step
;
|}.
Solve
Obligations
with
eauto
using
heap_lang
.
to_of_val
,
heap_lang
.
of_to_val
,
heap_lang
.
val
ues
_stuck
,
heap_lang
.
atomic_not_val
,
heap_lang
.
atomic_step
.
heap_lang
.
val_stuck
,
heap_lang
.
atomic_not_val
,
heap_lang
.
atomic_step
.
Global
Instance
heap_lang_ctx
K
:
LanguageCtx
heap_lang
(
heap_lang
.
fill
K
).
Proof
.
...
...
heap_lang/tactics.v
View file @
5fdfeb82
...
...
@@ -19,7 +19,7 @@ Ltac inv_step :=
simpl
in
H
;
first
[
subst
e
|
discriminate
H
|
injection
H
as
H
]
(* ensure that we make progress for each subgoal *)
|
H
:
head_step
?e
_
_
_
_
,
Hv
:
of_val
?v
=
fill
?K
?e
|-
_
=>
apply
val
ues
_head_stuck
,
(
fill_not_val
K
)
in
H
;
apply
val_head_stuck
,
(
fill_not_val
K
)
in
H
;
by
rewrite
-
Hv
to_of_val
in
H
(* maybe use a helper lemma here? *)
|
H
:
head_step
?e
_
_
_
_
|-
_
=>
try
(
is_var
e
;
fail
1
)
;
(* inversion yields many goals if e is a variable
...
...
program_logic/adequacy.v
View file @
5fdfeb82
...
...
@@ -33,7 +33,7 @@ Proof.
(
Φ
&
Φ
s2
&
r
&
rs2
&->&->&
Hwp
&?)%
Forall3_cons_inv_l
)%
Forall3_app_inv_l
?.
rewrite
wp_eq
in
Hwp
.
destruct
(
wp_step_inv
⊤
∅
Φ
e1
(
k
+
n
)
(
S
(
k
+
n
))
σ
1
r
(
big_op
(
rs1
++
rs2
)))
as
[
_
Hwpstep
]
;
eauto
using
val
ues
_stuck
.
(
big_op
(
rs1
++
rs2
)))
as
[
_
Hwpstep
]
;
eauto
using
val_stuck
.
{
by
rewrite
right_id_L
-
big_op_cons
Permutation_middle
.
}
destruct
(
Hwpstep
e2
σ
2
ef
)
as
(
r2
&
r2'
&
Hwsat
&?&?)
;
auto
;
clear
Hwpstep
.
revert
Hwsat
;
rewrite
big_op_app
right_id_L
=>
Hwsat
.
...
...
program_logic/language.v
View file @
5fdfeb82
...
...
@@ -10,7 +10,7 @@ Structure language := Language {
prim_step
:
expr
→
state
→
expr
→
state
→
option
expr
→
Prop
;
to_of_val
v
:
to_val
(
of_val
v
)
=
Some
v
;
of_to_val
e
v
:
to_val
e
=
Some
v
→
of_val
v
=
e
;
val
ues
_stuck
e
σ
e'
σ
'
ef
:
prim_step
e
σ
e'
σ
'
ef
→
to_val
e
=
None
;
val_stuck
e
σ
e'
σ
'
ef
:
prim_step
e
σ
e'
σ
'
ef
→
to_val
e
=
None
;
atomic_not_val
e
:
atomic
e
→
to_val
e
=
None
;
atomic_step
e1
σ
1 e2
σ
2
ef
:
atomic
e1
→
...
...
@@ -23,7 +23,7 @@ Arguments atomic {_} _.
Arguments
prim_step
{
_
}
_
_
_
_
_
.
Arguments
to_of_val
{
_
}
_
.
Arguments
of_to_val
{
_
}
_
_
_
.
Arguments
val
ues
_stuck
{
_
}
_
_
_
_
_
_
.
Arguments
val_stuck
{
_
}
_
_
_
_
_
_
.
Arguments
atomic_not_val
{
_
}
_
_
.
Arguments
atomic_step
{
_
}
_
_
_
_
_
_
_
.
...
...
@@ -45,7 +45,7 @@ Section language.
step
ρ
1
ρ
2
.
Lemma
reducible_not_val
e
σ
:
reducible
e
σ
→
to_val
e
=
None
.
Proof
.
intros
(?&?&?&?)
;
eauto
using
val
ues
_stuck
.
Qed
.
Proof
.
intros
(?&?&?&?)
;
eauto
using
val_stuck
.
Qed
.
Lemma
atomic_of_val
v
:
¬
atomic
(
of_val
v
).
Proof
.
by
intros
Hat
%
atomic_not_val
;
rewrite
to_of_val
in
Hat
.
Qed
.
Global
Instance
:
Inj
(=)
(=)
(@
of_val
Λ
).
...
...
Write
Preview
Supports
Markdown
0%
Try again
or
attach a new file
.
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Cancel
Please
register
or
sign in
to comment