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
891cbf51
Commit
891cbf51
authored
May 24, 2018
by
Ralf Jung
Browse files
bump std++; fix uses of default
parent
497bd8a8
Changes
6
Hide whitespace changes
Inline
Side-by-side
opam
View file @
891cbf51
...
...
@@ -11,5 +11,5 @@ install: [make "install"]
remove: ["rm" "-rf" "%{lib}%/coq/user-contrib/iris"]
depends: [
"coq" { (>= "8.7.0" & < "8.9~") | (= "dev") }
"coq-stdpp" { (= "dev.2018-05-2
3
.0.
a8f65af5
") | (= "dev") }
"coq-stdpp" { (= "dev.2018-05-2
4
.0.
de797b31
") | (= "dev") }
]
theories/program_logic/ectx_lifting.v
View file @
891cbf51
...
...
@@ -68,7 +68,7 @@ Lemma wp_lift_atomic_head_step {s E Φ} e1 :
⌜
head_reducible
e1
σ
1
⌝
∗
▷
∀
e2
σ
2
efs
,
⌜
head_step
e1
σ
1 e2
σ
2
efs
⌝
={
E
}=
∗
state_interp
σ
2
∗
default
False
(
to_val
e2
)
Φ
∗
[
∗
list
]
ef
∈
efs
,
WP
ef
@
s
;
⊤
{{
_
,
True
}})
from_option
Φ
False
(
to_val
e2
)
∗
[
∗
list
]
ef
∈
efs
,
WP
ef
@
s
;
⊤
{{
_
,
True
}})
⊢
WP
e1
@
s
;
E
{{
Φ
}}.
Proof
.
iIntros
(?)
"H"
.
iApply
wp_lift_atomic_step
;
eauto
.
...
...
@@ -82,7 +82,7 @@ Lemma wp_lift_atomic_head_step_no_fork {s E Φ} e1 :
(
∀
σ
1
,
state_interp
σ
1
={
E
}=
∗
⌜
head_reducible
e1
σ
1
⌝
∗
▷
∀
e2
σ
2
efs
,
⌜
head_step
e1
σ
1 e2
σ
2
efs
⌝
={
E
}=
∗
⌜
efs
=
[]
⌝
∗
state_interp
σ
2
∗
default
False
(
to_val
e2
)
Φ
)
⌜
efs
=
[]
⌝
∗
state_interp
σ
2
∗
from_option
Φ
False
(
to_val
e2
))
⊢
WP
e1
@
s
;
E
{{
Φ
}}.
Proof
.
iIntros
(?)
"H"
.
iApply
wp_lift_atomic_head_step
;
eauto
.
...
...
theories/program_logic/lifting.v
View file @
891cbf51
...
...
@@ -72,7 +72,7 @@ Lemma wp_lift_atomic_step {s E Φ} e1 :
⌜
if
s
is
NotStuck
then
reducible
e1
σ
1
else
True
⌝
∗
▷
∀
e2
σ
2
efs
,
⌜
prim_step
e1
σ
1 e2
σ
2
efs
⌝
={
E
}=
∗
state_interp
σ
2
∗
default
False
(
to_val
e2
)
Φ
∗
[
∗
list
]
ef
∈
efs
,
WP
ef
@
s
;
⊤
{{
_
,
True
}})
from_option
Φ
False
(
to_val
e2
)
∗
[
∗
list
]
ef
∈
efs
,
WP
ef
@
s
;
⊤
{{
_
,
True
}})
⊢
WP
e1
@
s
;
E
{{
Φ
}}.
Proof
.
iIntros
(?)
"H"
.
iApply
(
wp_lift_step
s
E
_
e1
)=>//
;
iIntros
(
σ
1
)
"Hσ1"
.
...
...
theories/program_logic/ownp.v
View file @
891cbf51
...
...
@@ -138,7 +138,7 @@ Section lifting.
Lemma
ownP_lift_atomic_step
{
s
E
Φ
}
e1
σ
1
:
(
if
s
is
NotStuck
then
reducible
e1
σ
1
else
to_val
e1
=
None
)
→
(
▷
ownP
σ
1
∗
▷
∀
e2
σ
2
efs
,
⌜
prim_step
e1
σ
1 e2
σ
2
efs
⌝
-
∗
ownP
σ
2
-
∗
default
False
(
to_val
e2
)
Φ
∗
[
∗
list
]
ef
∈
efs
,
WP
ef
@
s
;
⊤
{{
_
,
True
}})
from_option
Φ
False
(
to_val
e2
)
∗
[
∗
list
]
ef
∈
efs
,
WP
ef
@
s
;
⊤
{{
_
,
True
}})
⊢
WP
e1
@
s
;
E
{{
Φ
}}.
Proof
.
iIntros
(?)
"[Hσ H]"
;
iApply
ownP_lift_step
.
...
...
@@ -240,7 +240,7 @@ Section ectx_lifting.
head_reducible
e1
σ
1
→
▷
ownP
σ
1
∗
▷
(
∀
e2
σ
2
efs
,
⌜
head_step
e1
σ
1 e2
σ
2
efs
⌝
-
∗
ownP
σ
2
-
∗
default
False
(
to_val
e2
)
Φ
∗
[
∗
list
]
ef
∈
efs
,
WP
ef
@
s
;
⊤
{{
_
,
True
}})
from_option
Φ
False
(
to_val
e2
)
∗
[
∗
list
]
ef
∈
efs
,
WP
ef
@
s
;
⊤
{{
_
,
True
}})
⊢
WP
e1
@
s
;
E
{{
Φ
}}.
Proof
.
iIntros
(?)
"[? H]"
.
iApply
ownP_lift_atomic_step
;
eauto
.
...
...
theories/program_logic/total_ectx_lifting.v
View file @
891cbf51
...
...
@@ -43,7 +43,7 @@ Lemma twp_lift_atomic_head_step {s E Φ} e1 :
⌜
head_reducible
e1
σ
1
⌝
∗
∀
e2
σ
2
efs
,
⌜
head_step
e1
σ
1 e2
σ
2
efs
⌝
={
E
}=
∗
state_interp
σ
2
∗
default
False
(
to_val
e2
)
Φ
∗
[
∗
list
]
ef
∈
efs
,
WP
ef
@
s
;
⊤
[{
_
,
True
}])
from_option
Φ
False
(
to_val
e2
)
∗
[
∗
list
]
ef
∈
efs
,
WP
ef
@
s
;
⊤
[{
_
,
True
}])
⊢
WP
e1
@
s
;
E
[{
Φ
}].
Proof
.
iIntros
(?)
"H"
.
iApply
twp_lift_atomic_step
;
eauto
.
...
...
@@ -56,7 +56,7 @@ Lemma twp_lift_atomic_head_step_no_fork {s E Φ} e1 :
(
∀
σ
1
,
state_interp
σ
1
={
E
}=
∗
⌜
head_reducible
e1
σ
1
⌝
∗
∀
e2
σ
2
efs
,
⌜
head_step
e1
σ
1 e2
σ
2
efs
⌝
={
E
}=
∗
⌜
efs
=
[]
⌝
∗
state_interp
σ
2
∗
default
False
(
to_val
e2
)
Φ
)
⌜
efs
=
[]
⌝
∗
state_interp
σ
2
∗
from_option
Φ
False
(
to_val
e2
))
⊢
WP
e1
@
s
;
E
[{
Φ
}].
Proof
.
iIntros
(?)
"H"
.
iApply
twp_lift_atomic_head_step
;
eauto
.
...
...
theories/program_logic/total_lifting.v
View file @
891cbf51
...
...
@@ -45,7 +45,7 @@ Lemma twp_lift_atomic_step {s E Φ} e1 :
⌜
if
s
is
NotStuck
then
reducible
e1
σ
1
else
True
⌝
∗
∀
e2
σ
2
efs
,
⌜
prim_step
e1
σ
1 e2
σ
2
efs
⌝
={
E
}=
∗
state_interp
σ
2
∗
default
False
(
to_val
e2
)
Φ
∗
[
∗
list
]
ef
∈
efs
,
WP
ef
@
s
;
⊤
[{
_
,
True
}])
from_option
Φ
False
(
to_val
e2
)
∗
[
∗
list
]
ef
∈
efs
,
WP
ef
@
s
;
⊤
[{
_
,
True
}])
⊢
WP
e1
@
s
;
E
[{
Φ
}].
Proof
.
iIntros
(?)
"H"
.
iApply
(
twp_lift_step
_
E
_
e1
)=>//
;
iIntros
(
σ
1
)
"Hσ1"
.
...
...
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