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
Dmitry Khalanskiy
Iris
Commits
c792139c
Commit
c792139c
authored
Aug 08, 2016
by
Ralf Jung
Browse files
Fix building with ssreflect 1.6
I do not know why we have to split the rewrite here, but it seems we do.
parent
340afd90
Changes
1
Hide whitespace changes
Inline
Side-by-side
program_logic/adequacy.v
View file @
c792139c
...
...
@@ -94,7 +94,8 @@ Lemma wptp_result n e1 t1 v2 t2 σ1 σ2 φ :
world
σ
1
★
WP
e1
{{
v
,
■
φ
v
}}
★
wptp
t1
⊢
Nat
.
iter
(
S
(
S
n
))
(
λ
P
,
|=
r
=>
▷
P
)
(
■
φ
v2
).
Proof
.
intros
.
rewrite
wptp_steps
//
(
Nat_iter_S_r
(
S
n
))
;
[].
apply
:
rvs_iter_mono
.
intros
.
rewrite
wptp_steps
//.
rewrite
(
Nat_iter_S_r
(
S
n
)).
apply
rvs_iter_mono
.
iDestruct
1
as
(
e2
t2'
)
"(% & (Hw & HE & _) & H & _)"
;
simplify_eq
.
iDestruct
(
wp_value_inv
with
"H"
)
as
"H"
.
rewrite
pvs_eq
/
pvs_def
.
iVs
(
"H"
with
"[Hw HE]"
)
as
">(_ & _ & $)"
;
iFrame
;
auto
.
...
...
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