Skip to content
GitLab
Menu
Projects
Groups
Snippets
Loading...
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in / Register
Toggle navigation
Menu
Open sidebar
Rodolphe Lepigre
Iris
Commits
1e579d55
Commit
1e579d55
authored
Dec 03, 2017
by
Robbert Krebbers
Browse files
One direction of wand_impl_persistently holds for nonaffine BIs.
parent
35769f67
Changes
1
Hide whitespace changes
Inline
Sidebyside
theories/bi/derived.v
View file @
1e579d55
...
...
@@ 1072,6 +1072,9 @@ Proof.
by
rewrite
(
comm
bi_and
)
persistently_and_emp_elim
wand_elim_l
.
Qed
.
Lemma
wand_impl_persistently_2
P
Q
:
(
bi_persistently
P

∗
Q
)
⊢
(
bi_persistently
P
→
Q
).
Proof
.
apply
impl_intro_l
.
by
rewrite
persistently_and_sep_l_1
wand_elim_r
.
Qed
.
Section
persistently_affinely_bi
.
Context
`
{
AffineBI
PROP
}.
...
...
@@ 1095,6 +1098,11 @@ Section persistently_affinely_bi.
by
rewrite

persistently_and_sep_r
persistently_elim
impl_elim_r
.
Qed
.
Lemma
wand_impl_persistently
P
Q
:
(
bi_persistently
P

∗
Q
)
⊣
⊢
(
bi_persistently
P
→
Q
).
Proof
.
apply
(
anti_symm
(
⊢
)).
apply
wand_impl_persistently_2
.
by
rewrite

impl_wand_1
.
Qed
.
Lemma
wand_alt
P
Q
:
(
P

∗
Q
)
⊣
⊢
∃
R
,
R
∗
bi_persistently
(
P
∗
R
→
Q
).
Proof
.
apply
(
anti_symm
(
⊢
)).
...
...
@@ 1259,6 +1267,9 @@ Proof.
by
rewrite
(
comm
bi_and
)
plainly_and_emp_elim
wand_elim_l
.
Qed
.
Lemma
wand_impl_plainly_2
P
Q
:
(
bi_plainly
P

∗
Q
)
⊢
(
bi_plainly
P
→
Q
).
Proof
.
apply
impl_intro_l
.
by
rewrite
plainly_and_sep_l_1
wand_elim_r
.
Qed
.
Section
plainly_affinely_bi
.
Context
`
{
AffineBI
PROP
}.
...
...
@@ 1280,16 +1291,9 @@ Section plainly_affinely_bi.
by
rewrite

plainly_and_sep_r
plainly_elim
impl_elim_r
.
Qed
.
Lemma
wand_impl_persistently
P
Q
:
(
bi_persistently
P

∗
Q
)
⊣
⊢
(
bi_persistently
P
→
Q
).
Proof
.
apply
(
anti_symm
(
⊢
))
;
[
by
rewrite

impl_wand_1
].
apply
impl_intro_l
.
by
rewrite
persistently_and_sep_l
wand_elim_r
.
Qed
.
Lemma
wand_impl_plainly
P
Q
:
(
bi_plainly
P

∗
Q
)
⊣
⊢
(
bi_plainly
P
→
Q
).
Proof
.
apply
(
anti_symm
(
⊢
))
;
[
by
rewrite

impl_wand_1
].
apply
impl_intro_l
.
by
rewrite
plainly_and_sep_l
wand_elim_r
.
apply
(
anti_symm
(
⊢
)).
by
rewrite
wand_impl_plainly_2
.
by
rewrite

impl_wand_1
.
Qed
.
End
plainly_affinely_bi
.
...
...
Write
Preview
Markdown
is supported
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