Skip to content
GitLab
Menu
Projects
Groups
Snippets
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in / Register
Toggle navigation
Menu
Open sidebar
Marianna Rapoport
iris-coq
Commits
de7262e2
Commit
de7262e2
authored
Aug 08, 2016
by
Ralf Jung
Browse files
Merge branch 'master' of gitlab.mpi-sws.org:FP/iris-coq
parents
c792139c
cb16e4bd
Changes
1
Show whitespace changes
Inline
Side-by-side
program_logic/adequacy.v
View file @
de7262e2
...
...
@@ -115,7 +115,7 @@ Lemma wptp_safe n e1 e2 t1 t2 σ1 σ2 Φ :
world
σ
1
★
WP
e1
{{
Φ
}}
★
wptp
t1
⊢
Nat
.
iter
(
S
(
S
n
))
(
λ
P
,
|=
r
=>
▷
P
)
(
■
(
is_Some
(
to_val
e2
)
∨
reducible
e2
σ
2
)).
Proof
.
intros
?
He2
.
rewrite
wptp_steps
//
(
Nat_iter_S_r
(
S
n
))
;
apply
:
rvs_iter_mono
.
intros
?
He2
.
rewrite
wptp_steps
//
;
rewrite
(
Nat_iter_S_r
(
S
n
))
.
apply
rvs_iter_mono
.
iDestruct
1
as
(
e2'
t2'
)
"(% & Hw & H & Htp)"
;
simplify_eq
.
apply
elem_of_cons
in
He2
as
[<-|?]
;
first
(
iApply
wp_safe
;
by
iFrame
"Hw H"
).
iApply
wp_safe
.
iFrame
"Hw"
.
...
...
Write
Preview
Supports
Markdown
0%
Try again
or
attach a new file
.
Attach a 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