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
Iris
RefinedC
Commits
2756aabe
Commit
2756aabe
authored
Jun 09, 2021
by
Michael Sammler
Browse files
update Iris
parent
2262489e
Pipeline
#48355
failed with stage
in 17 minutes and 59 seconds
Changes
2
Pipelines
1
Hide whitespace changes
Inline
Side-by-side
refinedc.opam
View file @
2756aabe
...
...
@@ -17,7 +17,7 @@ dev-repo: "git+https://gitlab.mpi-sws.org/iris/refinedc.git"
depends: [
"coq" { (>= "8.12.0" & < "8.13~") }
"coq-iris" { (= "dev.2021-06-0
3.4.27c78b61
") | (= "dev") }
"coq-iris" { (= "dev.2021-06-0
9.0.07ab4060
") | (= "dev") }
"dune" {>= "2.7.0"}
"cerberus" {= "~dev"}
"cmdliner" {>= "1.0.4"}
...
...
theories/lang/lifting.v
View file @
2756aabe
...
...
@@ -535,7 +535,7 @@ Qed.
Lemma
wps_concat_bind_ind
vs
E
Φ
es
:
foldr
(
λ
e
f
,
(
λ
vl
,
WP
coerce_rtexpr
e
@
E
{{
v
,
f
(
vl
++
[
v
])
}}))
(
λ
vl
,
WP
Concat
(
Val
<$>
(
vs
++
vl
))
@
E
{{
Φ
}})
es
[]
-
∗
(
λ
vl
,
WP
coerce_rtexpr
(
Concat
(
Val
<$>
(
vs
++
vl
))
)
@
E
{{
Φ
}})
es
[]
-
∗
WP
Concat
((
Val
<$>
vs
)
++
es
)
@
E
{{
Φ
}}.
Proof
.
rewrite
-{
2
}(
app_nil_r
vs
).
...
...
@@ -555,7 +555,7 @@ Qed.
Lemma
wp_concat_bind
E
Φ
es
:
foldr
(
λ
e
f
,
(
λ
vl
,
WP
coerce_rtexpr
e
@
E
{{
v
,
f
(
vl
++
[
v
])
}}))
(
λ
vl
,
WP
Concat
(
Val
<$>
vl
)
@
E
{{
Φ
}})
es
[]
-
∗
(
λ
vl
,
WP
coerce_rtexpr
(
Concat
(
Val
<$>
vl
)
)
@
E
{{
Φ
}})
es
[]
-
∗
WP
Concat
es
@
E
{{
Φ
}}.
Proof
.
by
iApply
(
wps_concat_bind_ind
[]).
Qed
.
...
...
@@ -574,7 +574,7 @@ Qed.
Lemma
wp_call_bind_ind
vs
E
Φ
vf
el
:
foldr
(
λ
e
f
,
(
λ
vl
,
WP
coerce_rtexpr
e
@
E
{{
v
,
f
(
vl
++
[
v
])
}}))
(
λ
vl
,
WP
(
Call
(
Val
vf
)
(
Val
<$>
(
vs
++
vl
)))
@
E
{{
Φ
}})
el
[]
-
∗
(
λ
vl
,
WP
coerce_rtexpr
(
Call
(
Val
vf
)
(
Val
<$>
(
vs
++
vl
)))
@
E
{{
Φ
}})
el
[]
-
∗
WP
(
Call
(
Val
vf
)
((
Val
<$>
vs
)
++
el
))
@
E
{{
Φ
}}.
Proof
.
rewrite
-{
2
}(
app_nil_r
vs
).
...
...
@@ -594,7 +594,7 @@ Qed.
Lemma
wp_call_bind
E
Φ
el
ef
:
WP
(
coerce_rtexpr
ef
)
@
E
{{
vf
,
foldr
(
λ
e
f
,
(
λ
vl
,
WP
coerce_rtexpr
e
@
E
{{
v
,
f
(
vl
++
[
v
])
}}))
(
λ
vl
,
WP
(
Call
(
Val
vf
)
(
Val
<$>
vl
))
@
E
{{
Φ
}})
el
[]
}}
-
∗
(
λ
vl
,
WP
coerce_rtexpr
(
Call
(
Val
vf
)
(
Val
<$>
vl
))
@
E
{{
Φ
}})
el
[]
}}
-
∗
WP
(
Call
ef
el
)
@
E
{{
Φ
}}.
Proof
.
iIntros
"HWP"
.
...
...
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