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
0ea64978
Commit
0ea64978
authored
Aug 31, 2017
by
Robbert Krebbers
Committed by
Jacques-Henri Jourdan
Oct 30, 2017
Browse files
Swap names of bare_and_l and bare_and_r.
parent
3fbebb7c
Changes
3
Hide whitespace changes
Inline
Side-by-side
theories/bi/derived.v
View file @
0ea64978
...
...
@@ -727,10 +727,12 @@ Proof. by rewrite /bi_bare and_exist_l. Qed.
Lemma
bare_True_emp
:
■
True
⊣
⊢
■
emp
.
Proof
.
apply
(
anti_symm
_
)
;
rewrite
/
bi_bare
;
auto
.
Qed
.
Lemma
bare_and_l
P
Q
:
P
∧
■
Q
⊣
⊢
■
(
P
∧
Q
).
Proof
.
by
rewrite
/
bi_bare
!
assoc
(
comm
_
P
).
Qed
.
Lemma
bare_and_r
P
Q
:
■
P
∧
Q
⊣
⊢
■
(
P
∧
Q
).
Lemma
bare_and_l
P
Q
:
■
P
∧
Q
⊣
⊢
■
(
P
∧
Q
).
Proof
.
by
rewrite
/
bi_bare
assoc
.
Qed
.
Lemma
bare_and_r
P
Q
:
P
∧
■
Q
⊣
⊢
■
(
P
∧
Q
).
Proof
.
by
rewrite
/
bi_bare
!
assoc
(
comm
_
P
).
Qed
.
Lemma
bare_and_lr
P
Q
:
■
P
∧
Q
⊣
⊢
P
∧
■
Q
.
Proof
.
by
rewrite
bare_and_l
bare_and_r
.
Qed
.
(* Affine propositions *)
Global
Instance
Affine_proper
:
Proper
((
≡
)
==>
iff
)
(@
Affine
PROP
).
...
...
@@ -1073,10 +1075,10 @@ Qed.
Lemma
persistently_and_bare_sep_r
P
Q
:
P
∧
□
Q
⊣
⊢
P
∗
⬕
Q
.
Proof
.
by
rewrite
!(
comm
_
P
)
persistently_and_bare_sep_l
.
Qed
.
Lemma
and_sep_bare_persistently
P
Q
:
⬕
P
∧
⬕
Q
⊣
⊢
⬕
P
∗
⬕
Q
.
Proof
.
by
rewrite
-
persistently_and_bare_sep_l
-
bare_and
bare_and_
l
.
Qed
.
Proof
.
by
rewrite
-
persistently_and_bare_sep_l
-
bare_and
bare_and_
r
.
Qed
.
Lemma
bare_persistently_sep_dup
P
:
⬕
P
⊣
⊢
⬕
P
∗
⬕
P
.
Proof
.
by
rewrite
-
persistently_and_bare_sep_l
bare_and_
l
bare_and
idemp
.
Qed
.
Proof
.
by
rewrite
-
persistently_and_bare_sep_l
bare_and_
r
bare_and
idemp
.
Qed
.
(* Conditional bare modality *)
Global
Instance
bare_if_ne
p
:
NonExpansive
(@
bi_bare_if
PROP
p
).
...
...
theories/proofmode/class_instances.v
View file @
0ea64978
...
...
@@ -180,7 +180,7 @@ Global Instance into_wand_impl_true_false P Q P' :
IntoWand
true
false
(
P'
→
Q
)
P
Q
.
Proof
.
rewrite
/
FromAssumption
/
IntoWand
/=
=>
?
HP
.
apply
wand_intro_r
.
rewrite
-
persistently_and_bare_sep_l
HP
-{
2
}(
affine_bare
P'
)
bare_and_l
-
bare_and_r
.
rewrite
-
persistently_and_bare_sep_l
HP
-{
2
}(
affine_bare
P'
)
-
bare_and_
l
r
.
by
rewrite
bare_persistently_elim
impl_elim_l
.
Qed
.
...
...
@@ -288,13 +288,13 @@ Global Instance into_and_and_affine_l P Q Q' :
Affine
P
→
FromBare
Q'
Q
→
IntoAnd
false
(
P
∧
Q
)
P
Q'
.
Proof
.
intros
.
rewrite
/
IntoAnd
/=.
by
rewrite
-(
affine_bare
P
)
bare_and_
r
bare_and
(
from_bare
Q'
).
by
rewrite
-(
affine_bare
P
)
bare_and_
l
bare_and
(
from_bare
Q'
).
Qed
.
Global
Instance
into_and_and_affine_r
P
P'
Q
:
Affine
Q
→
FromBare
P'
P
→
IntoAnd
false
(
P
∧
Q
)
P'
Q
.
Proof
.
intros
.
rewrite
/
IntoAnd
/=.
by
rewrite
-(
affine_bare
Q
)
bare_and_
l
bare_and
(
from_bare
P'
).
by
rewrite
-(
affine_bare
Q
)
bare_and_
r
bare_and
(
from_bare
P'
).
Qed
.
Global
Instance
into_and_sep
`
{
PositiveBI
PROP
}
P
Q
:
IntoAnd
true
(
P
∗
Q
)
P
Q
.
...
...
@@ -333,7 +333,7 @@ Global Instance into_sep_and_persistent_l P P' Q Q' :
Persistent
P
→
AndIntoSep
P
P'
Q
Q'
→
IntoSep
(
P
∧
Q
)
P'
Q'
.
Proof
.
destruct
2
as
[
P
Q
Q'
|
P
Q
]
;
rewrite
/
IntoSep
.
-
rewrite
-(
from_bare
Q'
)
-(
affine_bare
P
)
bare_and_
r
-
bare_and_
l
.
-
rewrite
-(
from_bare
Q'
)
-(
affine_bare
P
)
bare_and_l
r
.
by
rewrite
persistent_and_bare_sep_l_1
.
-
by
rewrite
persistent_and_bare_sep_l_1
.
Qed
.
...
...
@@ -341,7 +341,7 @@ Global Instance into_sep_and_persistent_r P P' Q Q' :
Persistent
Q
→
AndIntoSep
Q
Q'
P
P'
→
IntoSep
(
P
∧
Q
)
P'
Q'
.
Proof
.
destruct
2
as
[
Q
P
P'
|
Q
P
]
;
rewrite
/
IntoSep
.
-
rewrite
-(
from_bare
P'
)
-(
affine_bare
Q
)
bare_and_l
-
bare_and_r
.
-
rewrite
-(
from_bare
P'
)
-(
affine_bare
Q
)
-
bare_and_
l
r
.
by
rewrite
persistent_and_bare_sep_r_1
.
-
by
rewrite
persistent_and_bare_sep_r_1
.
Qed
.
...
...
theories/proofmode/coq_tactics.v
View file @
0ea64978
...
...
@@ -339,7 +339,7 @@ Lemma env_spatial_is_nil_bare_persistently Δ :
env_spatial_is_nil
Δ
=
true
→
Δ
⊢
⬕
Δ
.
Proof
.
intros
.
unfold
of_envs
;
destruct
Δ
as
[?
[]]
;
simplify_eq
/=.
rewrite
!
right_id
{
1
}
bare_and_
l
persistently_and
.
rewrite
!
right_id
{
1
}
bare_and_
r
persistently_and
.
by
rewrite
persistently_bare
persistently_idemp
persistently_pure
.
Qed
.
...
...
@@ -556,7 +556,7 @@ Proof.
intros
???
<-.
destruct
(
env_spatial_is_nil
Δ
)
eqn
:
?.
-
rewrite
(
env_spatial_is_nil_bare_persistently
Δ
)
//
;
simpl
.
apply
impl_intro_l
.
rewrite
envs_app_singleton_sound
//
;
simpl
.
rewrite
-(
from_bare
P'
)
bare_and_l
-
bare_and_r
.
rewrite
-(
from_bare
P'
)
-
bare_and_
l
r
.
by
rewrite
persistently_and_bare_sep_r
bare_persistently_elim
wand_elim_r
.
-
apply
impl_intro_l
.
rewrite
envs_app_singleton_sound
//
;
simpl
.
by
rewrite
-(
from_bare
P'
)
persistent_and_bare_sep_l_1
wand_elim_r
.
...
...
@@ -712,7 +712,7 @@ Proof.
by
rewrite
sep_elim_r
persistently_and_bare_sep_l
wand_elim_r
.
-
destruct
Hpos
.
rewrite
-(
affine_bare
R
)
(
_
:
R
=
□
?false
R
)%
I
//
(
into_persistent
_
R
).
rewrite
bare_and_
r
-
bare_and_
l
bare_sep
sep_elim_r
bare_elim
.
rewrite
bare_and_l
r
bare_sep
sep_elim_r
bare_elim
.
by
rewrite
persistently_and_bare_sep_l
wand_elim_r
.
Qed
.
...
...
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