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
Rice Wine
Iris
Commits
26e93ebf
Commit
26e93ebf
authored
Mar 10, 2017
by
Ralf Jung
Browse files
rename wp_fupd_step -> wp_step_fupd. All other lemmas call them step_fupd.
parent
40d953c6
Changes
1
Hide whitespace changes
Inline
Side-by-side
theories/program_logic/weakestpre.v
View file @
26e93ebf
...
...
@@ -162,7 +162,7 @@ Proof.
iDestruct
"H"
as
%(?
&
?
&
?
&
?).
by
edestruct
(
Hatomic
_
_
_
_
Hstep
).
Qed
.
Lemma
wp_
fupd_step
E1
E2
e
P
Φ
:
Lemma
wp_
step_fupd
E1
E2
e
P
Φ
:
to_val
e
=
None
→
E2
⊆
E1
→
(|={
E1
,
E2
}
▷
=>
P
)
-
∗
WP
e
@
E2
{{
v
,
P
={
E1
}=
∗
Φ
v
}}
-
∗
WP
e
@
E1
{{
Φ
}}.
Proof
.
...
...
@@ -218,7 +218,7 @@ Lemma wp_frame_step_l E1 E2 e Φ R :
to_val
e
=
None
→
E2
⊆
E1
→
(|={
E1
,
E2
}
▷
=>
R
)
∗
WP
e
@
E2
{{
Φ
}}
⊢
WP
e
@
E1
{{
v
,
R
∗
Φ
v
}}.
Proof
.
iIntros
(??)
"[Hu Hwp]"
.
iApply
(
wp_
fupd_step
with
"Hu"
)
;
try
done
.
iIntros
(??)
"[Hu Hwp]"
.
iApply
(
wp_
step_fupd
with
"Hu"
)
;
try
done
.
iApply
(
wp_mono
with
"Hwp"
).
by
iIntros
(?)
"$$"
.
Qed
.
Lemma
wp_frame_step_r
E1
E2
e
Φ
R
:
...
...
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