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
Jonas Kastberg
iris
Commits
5524871e
Commit
5524871e
authored
Dec 04, 2017
by
Jacques-Henri Jourdan
Browse files
AffineBI -> BiAffine, PositiveBI -> BiPositive.
parent
d831f1e2
Changes
7
Hide whitespace changes
Inline
Side-by-side
theories/base_logic/derived.v
View file @
5524871e
...
...
@@ -32,7 +32,7 @@ Proof.
Qed
.
(* Affine *)
Global
Instance
uPred_affine
:
Affine
BI
(
uPredI
M
)
|
0
.
Global
Instance
uPred_affine
:
Bi
Affine
(
uPredI
M
)
|
0
.
Proof
.
intros
P
.
rewrite
/
Affine
.
by
apply
bi
.
pure_intro
.
Qed
.
(* Own and valid derived *)
...
...
@@ -131,6 +131,6 @@ Proof. split; [split; try apply _|]. apply ownM_op. apply ownM_unit'. Qed.
End
derived
.
(* Also add this to the global hint database, otherwise [eauto] won't work for
many lemmas that have [Affine
BI
] as a premise. *)
many lemmas that have [
Bi
Affine] as a premise. *)
Hint
Immediate
uPred_affine
.
End
uPred
.
theories/bi/big_op.v
View file @
5524871e
...
...
@@ -55,7 +55,7 @@ Section sep_list.
Lemma
big_sepL_nil
Φ
:
([
∗
list
]
k
↦
y
∈
nil
,
Φ
k
y
)
⊣
⊢
emp
.
Proof
.
done
.
Qed
.
Lemma
big_sepL_nil'
`
{
Affine
BI
PROP
}
P
Φ
:
P
⊢
[
∗
list
]
k
↦
y
∈
nil
,
Φ
k
y
.
Lemma
big_sepL_nil'
`
{
Bi
Affine
PROP
}
P
Φ
:
P
⊢
[
∗
list
]
k
↦
y
∈
nil
,
Φ
k
y
.
Proof
.
apply
(
affine
_
).
Qed
.
Lemma
big_sepL_cons
Φ
x
l
:
([
∗
list
]
k
↦
y
∈
x
::
l
,
Φ
k
y
)
⊣
⊢
Φ
0
x
∗
[
∗
list
]
k
↦
y
∈
l
,
Φ
(
S
k
)
y
.
...
...
@@ -75,7 +75,7 @@ Section sep_list.
(
∀
k
y
,
l
!!
k
=
Some
y
→
Φ
k
y
⊣
⊢
Ψ
k
y
)
→
([
∗
list
]
k
↦
y
∈
l
,
Φ
k
y
)
⊣
⊢
([
∗
list
]
k
↦
y
∈
l
,
Ψ
k
y
).
Proof
.
apply
big_opL_proper
.
Qed
.
Lemma
big_sepL_submseteq
`
{
Affine
BI
PROP
}
(
Φ
:
A
→
PROP
)
l1
l2
:
Lemma
big_sepL_submseteq
`
{
Bi
Affine
PROP
}
(
Φ
:
A
→
PROP
)
l1
l2
:
l1
⊆
+
l2
→
([
∗
list
]
y
∈
l2
,
Φ
y
)
⊢
[
∗
list
]
y
∈
l1
,
Φ
y
.
Proof
.
intros
[
l
->]%
submseteq_Permutation
.
by
rewrite
big_sepL_app
sep_elim_l
.
...
...
@@ -125,16 +125,16 @@ Section sep_list.
⊢
([
∗
list
]
k
↦
x
∈
l
,
Φ
k
x
)
∧
([
∗
list
]
k
↦
x
∈
l
,
Ψ
k
x
).
Proof
.
auto
using
and_intro
,
big_sepL_mono
,
and_elim_l
,
and_elim_r
.
Qed
.
Lemma
big_sepL_plainly
`
{
Affine
BI
PROP
}
Φ
l
:
Lemma
big_sepL_plainly
`
{
Bi
Affine
PROP
}
Φ
l
:
bi_plainly
([
∗
list
]
k
↦
x
∈
l
,
Φ
k
x
)
⊣
⊢
[
∗
list
]
k
↦
x
∈
l
,
bi_plainly
(
Φ
k
x
).
Proof
.
apply
(
big_opL_commute
_
).
Qed
.
Lemma
big_sepL_persistently
`
{
Affine
BI
PROP
}
Φ
l
:
Lemma
big_sepL_persistently
`
{
Bi
Affine
PROP
}
Φ
l
:
bi_persistently
([
∗
list
]
k
↦
x
∈
l
,
Φ
k
x
)
⊣
⊢
[
∗
list
]
k
↦
x
∈
l
,
bi_persistently
(
Φ
k
x
).
Proof
.
apply
(
big_opL_commute
_
).
Qed
.
Lemma
big_sepL_forall
`
{
Affine
BI
PROP
}
Φ
l
:
Lemma
big_sepL_forall
`
{
Bi
Affine
PROP
}
Φ
l
:
(
∀
k
x
,
Persistent
(
Φ
k
x
))
→
([
∗
list
]
k
↦
x
∈
l
,
Φ
k
x
)
⊣
⊢
(
∀
k
x
,
⌜
l
!!
k
=
Some
x
⌝
→
Φ
k
x
).
Proof
.
...
...
@@ -287,7 +287,7 @@ Section and_list.
[
∧
list
]
k
↦
x
∈
l
,
bi_persistently
(
Φ
k
x
).
Proof
.
apply
(
big_opL_commute
_
).
Qed
.
Lemma
big_andL_forall
`
{
Affine
BI
PROP
}
Φ
l
:
Lemma
big_andL_forall
`
{
Bi
Affine
PROP
}
Φ
l
:
([
∧
list
]
k
↦
x
∈
l
,
Φ
k
x
)
⊣
⊢
(
∀
k
x
,
⌜
l
!!
k
=
Some
x
⌝
→
Φ
k
x
).
Proof
.
apply
(
anti_symm
_
).
...
...
@@ -328,7 +328,7 @@ Section gmap.
(
∀
k
x
,
m
!!
k
=
Some
x
→
Φ
k
x
⊣
⊢
Ψ
k
x
)
→
([
∗
map
]
k
↦
x
∈
m
,
Φ
k
x
)
⊣
⊢
([
∗
map
]
k
↦
x
∈
m
,
Ψ
k
x
).
Proof
.
apply
big_opM_proper
.
Qed
.
Lemma
big_sepM_subseteq
`
{
Affine
BI
PROP
}
Φ
m1
m2
:
Lemma
big_sepM_subseteq
`
{
Bi
Affine
PROP
}
Φ
m1
m2
:
m2
⊆
m1
→
([
∗
map
]
k
↦
x
∈
m1
,
Φ
k
x
)
⊢
[
∗
map
]
k
↦
x
∈
m2
,
Φ
k
x
.
Proof
.
intros
.
by
apply
big_sepL_submseteq
,
map_to_list_submseteq
.
Qed
.
...
...
@@ -339,7 +339,7 @@ Section gmap.
Lemma
big_sepM_empty
Φ
:
([
∗
map
]
k
↦
x
∈
∅
,
Φ
k
x
)
⊣
⊢
emp
.
Proof
.
by
rewrite
big_opM_empty
.
Qed
.
Lemma
big_sepM_empty'
`
{
Affine
BI
PROP
}
P
Φ
:
P
⊢
[
∗
map
]
k
↦
x
∈
∅
,
Φ
k
x
.
Lemma
big_sepM_empty'
`
{
Bi
Affine
PROP
}
P
Φ
:
P
⊢
[
∗
map
]
k
↦
x
∈
∅
,
Φ
k
x
.
Proof
.
rewrite
big_sepM_empty
.
apply
:
affine
.
Qed
.
Lemma
big_sepM_insert
Φ
m
i
x
:
...
...
@@ -420,16 +420,16 @@ Section gmap.
⊢
([
∗
map
]
k
↦
x
∈
m
,
Φ
k
x
)
∧
([
∗
map
]
k
↦
x
∈
m
,
Ψ
k
x
).
Proof
.
auto
using
and_intro
,
big_sepM_mono
,
and_elim_l
,
and_elim_r
.
Qed
.
Lemma
big_sepM_plainly
`
{
Affine
BI
PROP
}
Φ
m
:
Lemma
big_sepM_plainly
`
{
Bi
Affine
PROP
}
Φ
m
:
bi_plainly
([
∗
map
]
k
↦
x
∈
m
,
Φ
k
x
)
⊣
⊢
[
∗
map
]
k
↦
x
∈
m
,
bi_plainly
(
Φ
k
x
).
Proof
.
apply
(
big_opM_commute
_
).
Qed
.
Lemma
big_sepM_persistently
`
{
Affine
BI
PROP
}
Φ
m
:
Lemma
big_sepM_persistently
`
{
Bi
Affine
PROP
}
Φ
m
:
(
bi_persistently
([
∗
map
]
k
↦
x
∈
m
,
Φ
k
x
))
⊣
⊢
([
∗
map
]
k
↦
x
∈
m
,
bi_persistently
(
Φ
k
x
)).
Proof
.
apply
(
big_opM_commute
_
).
Qed
.
Lemma
big_sepM_forall
`
{
Affine
BI
PROP
}
Φ
m
:
Lemma
big_sepM_forall
`
{
Bi
Affine
PROP
}
Φ
m
:
(
∀
k
x
,
Persistent
(
Φ
k
x
))
→
([
∗
map
]
k
↦
x
∈
m
,
Φ
k
x
)
⊣
⊢
(
∀
k
x
,
⌜
m
!!
k
=
Some
x
⌝
→
Φ
k
x
).
Proof
.
...
...
@@ -499,7 +499,7 @@ Section gset.
(
∀
x
,
x
∈
X
→
Φ
x
⊣
⊢
Ψ
x
)
→
([
∗
set
]
x
∈
X
,
Φ
x
)
⊣
⊢
([
∗
set
]
x
∈
X
,
Ψ
x
).
Proof
.
apply
big_opS_proper
.
Qed
.
Lemma
big_sepS_subseteq
`
{
Affine
BI
PROP
}
Φ
X
Y
:
Lemma
big_sepS_subseteq
`
{
Bi
Affine
PROP
}
Φ
X
Y
:
Y
⊆
X
→
([
∗
set
]
x
∈
X
,
Φ
x
)
⊢
[
∗
set
]
x
∈
Y
,
Φ
x
.
Proof
.
intros
.
by
apply
big_sepL_submseteq
,
elements_submseteq
.
Qed
.
...
...
@@ -509,7 +509,7 @@ Section gset.
Lemma
big_sepS_empty
Φ
:
([
∗
set
]
x
∈
∅
,
Φ
x
)
⊣
⊢
emp
.
Proof
.
by
rewrite
big_opS_empty
.
Qed
.
Lemma
big_sepS_empty'
`
{!
Affine
BI
PROP
}
P
Φ
:
P
⊢
[
∗
set
]
x
∈
∅
,
Φ
x
.
Lemma
big_sepS_empty'
`
{!
Bi
Affine
PROP
}
P
Φ
:
P
⊢
[
∗
set
]
x
∈
∅
,
Φ
x
.
Proof
.
rewrite
big_sepS_empty
.
apply
:
affine
.
Qed
.
Lemma
big_sepS_insert
Φ
X
x
:
...
...
@@ -575,12 +575,12 @@ Section gset.
by
apply
sep_mono_r
,
wand_intro_l
.
Qed
.
Lemma
big_sepS_filter
`
{
Affine
BI
PROP
}
Lemma
big_sepS_filter
`
{
Bi
Affine
PROP
}
(
P
:
A
→
Prop
)
`
{
∀
x
,
Decision
(
P
x
)}
Φ
X
:
([
∗
set
]
y
∈
filter
P
X
,
Φ
y
)
⊣
⊢
([
∗
set
]
y
∈
X
,
⌜
P
y
⌝
→
Φ
y
).
Proof
.
setoid_rewrite
<-
decide_emp
.
apply
big_sepS_filter'
.
Qed
.
Lemma
big_sepS_filter_acc
`
{
Affine
BI
PROP
}
Lemma
big_sepS_filter_acc
`
{
Bi
Affine
PROP
}
(
P
:
A
→
Prop
)
`
{
∀
y
,
Decision
(
P
y
)}
Φ
X
Y
:
(
∀
y
,
y
∈
Y
→
P
y
→
y
∈
X
)
→
([
∗
set
]
y
∈
X
,
Φ
y
)
-
∗
...
...
@@ -596,15 +596,15 @@ Section gset.
([
∗
set
]
y
∈
X
,
Φ
y
∧
Ψ
y
)
⊢
([
∗
set
]
y
∈
X
,
Φ
y
)
∧
([
∗
set
]
y
∈
X
,
Ψ
y
).
Proof
.
auto
using
and_intro
,
big_sepS_mono
,
and_elim_l
,
and_elim_r
.
Qed
.
Lemma
big_sepS_plainly
`
{
Affine
BI
PROP
}
Φ
X
:
Lemma
big_sepS_plainly
`
{
Bi
Affine
PROP
}
Φ
X
:
bi_plainly
([
∗
set
]
y
∈
X
,
Φ
y
)
⊣
⊢
[
∗
set
]
y
∈
X
,
bi_plainly
(
Φ
y
).
Proof
.
apply
(
big_opS_commute
_
).
Qed
.
Lemma
big_sepS_persistently
`
{
Affine
BI
PROP
}
Φ
X
:
Lemma
big_sepS_persistently
`
{
Bi
Affine
PROP
}
Φ
X
:
bi_persistently
([
∗
set
]
y
∈
X
,
Φ
y
)
⊣
⊢
[
∗
set
]
y
∈
X
,
bi_persistently
(
Φ
y
).
Proof
.
apply
(
big_opS_commute
_
).
Qed
.
Lemma
big_sepS_forall
`
{
Affine
BI
PROP
}
Φ
X
:
Lemma
big_sepS_forall
`
{
Bi
Affine
PROP
}
Φ
X
:
(
∀
x
,
Persistent
(
Φ
x
))
→
([
∗
set
]
x
∈
X
,
Φ
x
)
⊣
⊢
(
∀
x
,
⌜
x
∈
X
⌝
→
Φ
x
).
Proof
.
intros
.
apply
(
anti_symm
_
).
...
...
@@ -671,7 +671,7 @@ Section gmultiset.
(
∀
x
,
x
∈
X
→
Φ
x
⊣
⊢
Ψ
x
)
→
([
∗
mset
]
x
∈
X
,
Φ
x
)
⊣
⊢
([
∗
mset
]
x
∈
X
,
Ψ
x
).
Proof
.
apply
big_opMS_proper
.
Qed
.
Lemma
big_sepMS_subseteq
`
{
Affine
BI
PROP
}
Φ
X
Y
:
Lemma
big_sepMS_subseteq
`
{
Bi
Affine
PROP
}
Φ
X
Y
:
Y
⊆
X
→
([
∗
mset
]
x
∈
X
,
Φ
x
)
⊢
[
∗
mset
]
x
∈
Y
,
Φ
x
.
Proof
.
intros
.
by
apply
big_sepL_submseteq
,
gmultiset_elements_submseteq
.
Qed
.
...
...
@@ -681,7 +681,7 @@ Section gmultiset.
Lemma
big_sepMS_empty
Φ
:
([
∗
mset
]
x
∈
∅
,
Φ
x
)
⊣
⊢
emp
.
Proof
.
by
rewrite
big_opMS_empty
.
Qed
.
Lemma
big_sepMS_empty'
`
{!
Affine
BI
PROP
}
P
Φ
:
P
⊢
[
∗
mset
]
x
∈
∅
,
Φ
x
.
Lemma
big_sepMS_empty'
`
{!
Bi
Affine
PROP
}
P
Φ
:
P
⊢
[
∗
mset
]
x
∈
∅
,
Φ
x
.
Proof
.
rewrite
big_sepMS_empty
.
apply
:
affine
.
Qed
.
Lemma
big_sepMS_union
Φ
X
Y
:
...
...
@@ -714,11 +714,11 @@ Section gmultiset.
([
∗
mset
]
y
∈
X
,
Φ
y
∧
Ψ
y
)
⊢
([
∗
mset
]
y
∈
X
,
Φ
y
)
∧
([
∗
mset
]
y
∈
X
,
Ψ
y
).
Proof
.
auto
using
and_intro
,
big_sepMS_mono
,
and_elim_l
,
and_elim_r
.
Qed
.
Lemma
big_sepMS_plainly
`
{
Affine
BI
PROP
}
Φ
X
:
Lemma
big_sepMS_plainly
`
{
Bi
Affine
PROP
}
Φ
X
:
bi_plainly
([
∗
mset
]
y
∈
X
,
Φ
y
)
⊣
⊢
[
∗
mset
]
y
∈
X
,
bi_plainly
(
Φ
y
).
Proof
.
apply
(
big_opMS_commute
_
).
Qed
.
Lemma
big_sepMS_persistently
`
{
Affine
BI
PROP
}
Φ
X
:
Lemma
big_sepMS_persistently
`
{
Bi
Affine
PROP
}
Φ
X
:
bi_persistently
([
∗
mset
]
y
∈
X
,
Φ
y
)
⊣
⊢
[
∗
mset
]
y
∈
X
,
bi_persistently
(
Φ
y
).
Proof
.
apply
(
big_opMS_commute
_
).
Qed
.
...
...
@@ -756,11 +756,11 @@ Section list.
Implicit
Types
l
:
list
A
.
Implicit
Types
Φ
Ψ
:
nat
→
A
→
PROP
.
Lemma
big_sepL_later
`
{
Affine
BI
PROP
}
Φ
l
:
Lemma
big_sepL_later
`
{
Bi
Affine
PROP
}
Φ
l
:
▷
([
∗
list
]
k
↦
x
∈
l
,
Φ
k
x
)
⊣
⊢
([
∗
list
]
k
↦
x
∈
l
,
▷
Φ
k
x
).
Proof
.
apply
(
big_opL_commute
_
).
Qed
.
Lemma
big_sepL_laterN
`
{
Affine
BI
PROP
}
Φ
n
l
:
Lemma
big_sepL_laterN
`
{
Bi
Affine
PROP
}
Φ
n
l
:
▷
^
n
([
∗
list
]
k
↦
x
∈
l
,
Φ
k
x
)
⊣
⊢
([
∗
list
]
k
↦
x
∈
l
,
▷
^
n
Φ
k
x
).
Proof
.
apply
(
big_opL_commute
_
).
Qed
.
...
...
@@ -781,11 +781,11 @@ Section gmap.
Implicit
Types
m
:
gmap
K
A
.
Implicit
Types
Φ
Ψ
:
K
→
A
→
PROP
.
Lemma
big_sepM_later
`
{
Affine
BI
PROP
}
Φ
m
:
Lemma
big_sepM_later
`
{
Bi
Affine
PROP
}
Φ
m
:
▷
([
∗
map
]
k
↦
x
∈
m
,
Φ
k
x
)
⊣
⊢
([
∗
map
]
k
↦
x
∈
m
,
▷
Φ
k
x
).
Proof
.
apply
(
big_opM_commute
_
).
Qed
.
Lemma
big_sepM_laterN
`
{
Affine
BI
PROP
}
Φ
n
m
:
Lemma
big_sepM_laterN
`
{
Bi
Affine
PROP
}
Φ
n
m
:
▷
^
n
([
∗
map
]
k
↦
x
∈
m
,
Φ
k
x
)
⊣
⊢
([
∗
map
]
k
↦
x
∈
m
,
▷
^
n
Φ
k
x
).
Proof
.
apply
(
big_opM_commute
_
).
Qed
.
...
...
@@ -803,11 +803,11 @@ Section gset.
Implicit
Types
X
:
gset
A
.
Implicit
Types
Φ
:
A
→
PROP
.
Lemma
big_sepS_later
`
{
Affine
BI
PROP
}
Φ
X
:
Lemma
big_sepS_later
`
{
Bi
Affine
PROP
}
Φ
X
:
▷
([
∗
set
]
y
∈
X
,
Φ
y
)
⊣
⊢
([
∗
set
]
y
∈
X
,
▷
Φ
y
).
Proof
.
apply
(
big_opS_commute
_
).
Qed
.
Lemma
big_sepS_laterN
`
{
Affine
BI
PROP
}
Φ
n
X
:
Lemma
big_sepS_laterN
`
{
Bi
Affine
PROP
}
Φ
n
X
:
▷
^
n
([
∗
set
]
y
∈
X
,
Φ
y
)
⊣
⊢
([
∗
set
]
y
∈
X
,
▷
^
n
Φ
y
).
Proof
.
apply
(
big_opS_commute
_
).
Qed
.
...
...
@@ -825,11 +825,11 @@ Section gmultiset.
Implicit
Types
X
:
gmultiset
A
.
Implicit
Types
Φ
:
A
→
PROP
.
Lemma
big_sepMS_later
`
{
Affine
BI
PROP
}
Φ
X
:
Lemma
big_sepMS_later
`
{
Bi
Affine
PROP
}
Φ
X
:
▷
([
∗
mset
]
y
∈
X
,
Φ
y
)
⊣
⊢
([
∗
mset
]
y
∈
X
,
▷
Φ
y
).
Proof
.
apply
(
big_opMS_commute
_
).
Qed
.
Lemma
big_sepMS_laterN
`
{
Affine
BI
PROP
}
Φ
n
X
:
Lemma
big_sepMS_laterN
`
{
Bi
Affine
PROP
}
Φ
n
X
:
▷
^
n
([
∗
mset
]
y
∈
X
,
Φ
y
)
⊣
⊢
([
∗
mset
]
y
∈
X
,
▷
^
n
Φ
y
).
Proof
.
apply
(
big_opMS_commute
_
).
Qed
.
...
...
theories/bi/counter_examples.v
View file @
5524871e
...
...
@@ -5,7 +5,7 @@ Set Default Proof Using "Type*".
(** This proves that we need the ▷ in a "Saved Proposition" construction with
name-dependent allocation. *)
Module
savedprop
.
Section
savedprop
.
Context
`
{
Affine
BI
PROP
}.
Context
`
{
Bi
Affine
PROP
}.
Notation
"¬ P"
:
=
(
□
(
P
→
False
))%
I
:
bi_scope
.
Implicit
Types
P
:
PROP
.
...
...
@@ -65,7 +65,7 @@ End savedprop. End savedprop.
(** This proves that we need the ▷ when opening invariants. *)
Module
inv
.
Section
inv
.
Context
`
{
Affine
BI
PROP
}.
Context
`
{
Bi
Affine
PROP
}.
Implicit
Types
P
:
PROP
.
(** Assumptions *)
...
...
theories/bi/derived.v
View file @
5524871e
...
...
@@ -39,11 +39,11 @@ Arguments Affine {_} _%I : simpl never.
Arguments
affine
{
_
}
_
%
I
{
_
}.
Hint
Mode
Affine
+
!
:
typeclass_instances
.
Class
Affine
BI
(
PROP
:
bi
)
:
=
absorbing_bi
(
Q
:
PROP
)
:
Affine
Q
.
Class
Bi
Affine
(
PROP
:
bi
)
:
=
absorbing_bi
(
Q
:
PROP
)
:
Affine
Q
.
Existing
Instance
absorbing_bi
|
0
.
Class
Positive
BI
(
PROP
:
bi
)
:
=
positive
_bi
(
P
Q
:
PROP
)
:
bi_affinely
(
P
∗
Q
)
⊢
bi_affinely
P
∗
Q
.
Class
Bi
Positive
(
PROP
:
bi
)
:
=
bi_
positive
(
P
Q
:
PROP
)
:
bi_affinely
(
P
∗
Q
)
⊢
bi_affinely
P
∗
Q
.
Definition
bi_absorbingly
{
PROP
:
bi
}
(
P
:
PROP
)
:
PROP
:
=
(
True
∗
P
)%
I
.
Arguments
bi_absorbingly
{
_
}
_
%
I
:
simpl
never
.
...
...
@@ -732,11 +732,11 @@ Proof.
-
by
rewrite
!
and_elim_l
right_id
.
-
by
rewrite
!
and_elim_r
.
Qed
.
Lemma
affinely_sep
`
{
Positive
BI
PROP
}
P
Q
:
Lemma
affinely_sep
`
{
Bi
Positive
PROP
}
P
Q
:
bi_affinely
(
P
∗
Q
)
⊣
⊢
bi_affinely
P
∗
bi_affinely
Q
.
Proof
.
apply
(
anti_symm
_
),
affinely_sep_2
.
by
rewrite
-{
1
}
affinely_idemp
positive
_bi
!(
comm
_
(
bi_affinely
P
)%
I
)
positive
_bi
.
by
rewrite
-{
1
}
affinely_idemp
bi_
positive
!(
comm
_
(
bi_affinely
P
)%
I
)
bi_
positive
.
Qed
.
Lemma
affinely_forall
{
A
}
(
Φ
:
A
→
PROP
)
:
bi_affinely
(
∀
a
,
Φ
a
)
⊢
∀
a
,
bi_affinely
(
Φ
a
).
...
...
@@ -815,7 +815,7 @@ Proof. by rewrite /bi_absorbingly !assoc (comm _ P). Qed.
Lemma
absorbingly_sep_lr
P
Q
:
bi_absorbingly
P
∗
Q
⊣
⊢
P
∗
bi_absorbingly
Q
.
Proof
.
by
rewrite
absorbingly_sep_l
absorbingly_sep_r
.
Qed
.
Lemma
affinely_absorbingly
`
{!
Positive
BI
PROP
}
P
:
Lemma
affinely_absorbingly
`
{!
Bi
Positive
PROP
}
P
:
bi_affinely
(
bi_absorbingly
P
)
⊣
⊢
bi_affinely
P
.
Proof
.
apply
(
anti_symm
_
),
affinely_mono
,
absorbingly_intro
.
...
...
@@ -875,12 +875,12 @@ Proof. apply (anti_symm _); auto using True_sep_2. Qed.
Lemma
sep_True
P
`
{!
Absorbing
P
}
:
P
∗
True
⊣
⊢
P
.
Proof
.
by
rewrite
comm
True_sep
.
Qed
.
Section
affine
_bi
.
Context
`
{
Affine
BI
PROP
}.
Section
bi_
affine
.
Context
`
{
Bi
Affine
PROP
}.
Global
Instance
affine_
bi_
absorbing
P
:
Absorbing
P
|
0
.
Global
Instance
bi_
affine_absorbing
P
:
Absorbing
P
|
0
.
Proof
.
by
rewrite
/
Absorbing
/
bi_absorbingly
(
affine
True
%
I
)
left_id
.
Qed
.
Global
Instance
affine_
bi_
positive
:
Positive
BI
PROP
.
Global
Instance
bi_
affine_positive
:
Bi
Positive
PROP
.
Proof
.
intros
P
Q
.
by
rewrite
!
affine_affinely
.
Qed
.
Lemma
True_emp
:
True
⊣
⊢
emp
.
...
...
@@ -906,7 +906,7 @@ Section affine_bi.
-
by
rewrite
pure_True
//
True_impl
.
-
by
rewrite
pure_False
//
False_impl
True_emp
.
Qed
.
End
affine
_bi
.
End
bi_
affine
.
(* Properties of the persistence modality *)
Hint
Resolve
persistently_mono
.
...
...
@@ -1044,7 +1044,7 @@ Qed.
Lemma
persistently_sep_2
P
Q
:
bi_persistently
P
∗
bi_persistently
Q
⊢
bi_persistently
(
P
∗
Q
).
Proof
.
by
rewrite
-
persistently_and_sep
persistently_and
-
and_sep_persistently
.
Qed
.
Lemma
persistently_sep
`
{
Positive
BI
PROP
}
P
Q
:
Lemma
persistently_sep
`
{
Bi
Positive
PROP
}
P
Q
:
bi_persistently
(
P
∗
Q
)
⊣
⊢
bi_persistently
P
∗
bi_persistently
Q
.
Proof
.
apply
(
anti_symm
_
)
;
auto
using
persistently_sep_2
.
...
...
@@ -1076,7 +1076,7 @@ Lemma impl_wand_persistently_2 P Q : (bi_persistently P -∗ Q) ⊢ (bi_persiste
Proof
.
apply
impl_intro_l
.
by
rewrite
persistently_and_sep_l_1
wand_elim_r
.
Qed
.
Section
persistently_affinely_bi
.
Context
`
{
Affine
BI
PROP
}.
Context
`
{
Bi
Affine
PROP
}.
Lemma
persistently_emp
:
bi_persistently
emp
⊣
⊢
emp
.
Proof
.
by
rewrite
-!
True_emp
persistently_pure
.
Qed
.
...
...
@@ -1243,7 +1243,7 @@ Qed.
Lemma
plainly_sep_2
P
Q
:
bi_plainly
P
∗
bi_plainly
Q
⊢
bi_plainly
(
P
∗
Q
).
Proof
.
by
rewrite
-
plainly_and_sep
plainly_and
-
and_sep_plainly
.
Qed
.
Lemma
plainly_sep
`
{
Positive
BI
PROP
}
P
Q
:
Lemma
plainly_sep
`
{
Bi
Positive
PROP
}
P
Q
:
bi_plainly
(
P
∗
Q
)
⊣
⊢
bi_plainly
P
∗
bi_plainly
Q
.
Proof
.
apply
(
anti_symm
_
)
;
auto
using
plainly_sep_2
.
...
...
@@ -1271,7 +1271,7 @@ Lemma impl_wand_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
`
{
Affine
BI
PROP
}.
Context
`
{
Bi
Affine
PROP
}.
Lemma
plainly_emp
:
bi_plainly
emp
⊣
⊢
emp
.
Proof
.
by
rewrite
-!
True_emp
plainly_pure
.
Qed
.
...
...
@@ -1316,7 +1316,7 @@ Lemma affinely_persistently_exist {A} (Φ : A → PROP) : □ (∃ x, Φ x) ⊣
Proof
.
by
rewrite
persistently_exist
affinely_exist
.
Qed
.
Lemma
affinely_persistently_sep_2
P
Q
:
□
P
∗
□
Q
⊢
□
(
P
∗
Q
).
Proof
.
by
rewrite
affinely_sep_2
persistently_sep_2
.
Qed
.
Lemma
affinely_persistently_sep
`
{
Positive
BI
PROP
}
P
Q
:
□
(
P
∗
Q
)
⊣
⊢
□
P
∗
□
Q
.
Lemma
affinely_persistently_sep
`
{
Bi
Positive
PROP
}
P
Q
:
□
(
P
∗
Q
)
⊣
⊢
□
P
∗
□
Q
.
Proof
.
by
rewrite
-
affinely_sep
-
persistently_sep
.
Qed
.
Lemma
affinely_persistently_idemp
P
:
□
□
P
⊣
⊢
□
P
.
...
...
@@ -1368,7 +1368,7 @@ Lemma affinely_plainly_exist {A} (Φ : A → PROP) : ■ (∃ x, Φ x) ⊣⊢
Proof
.
by
rewrite
plainly_exist
affinely_exist
.
Qed
.
Lemma
affinely_plainly_sep_2
P
Q
:
■
P
∗
■
Q
⊢
■
(
P
∗
Q
).
Proof
.
by
rewrite
affinely_sep_2
plainly_sep_2
.
Qed
.
Lemma
affinely_plainly_sep
`
{
Positive
BI
PROP
}
P
Q
:
■
(
P
∗
Q
)
⊣
⊢
■
P
∗
■
Q
.
Lemma
affinely_plainly_sep
`
{
Bi
Positive
PROP
}
P
Q
:
■
(
P
∗
Q
)
⊣
⊢
■
P
∗
■
Q
.
Proof
.
by
rewrite
-
affinely_sep
-
plainly_sep
.
Qed
.
Lemma
affinely_plainly_idemp
P
:
■
■
P
⊣
⊢
■
P
.
...
...
@@ -1427,7 +1427,7 @@ Proof. destruct p; simpl; auto using affinely_exist. Qed.
Lemma
affinely_if_sep_2
p
P
Q
:
bi_affinely_if
p
P
∗
bi_affinely_if
p
Q
⊢
bi_affinely_if
p
(
P
∗
Q
).
Proof
.
destruct
p
;
simpl
;
auto
using
affinely_sep_2
.
Qed
.
Lemma
affinely_if_sep
`
{
Positive
BI
PROP
}
p
P
Q
:
Lemma
affinely_if_sep
`
{
Bi
Positive
PROP
}
p
P
Q
:
bi_affinely_if
p
(
P
∗
Q
)
⊣
⊢
bi_affinely_if
p
P
∗
bi_affinely_if
p
Q
.
Proof
.
destruct
p
;
simpl
;
auto
using
affinely_sep
.
Qed
.
...
...
@@ -1466,7 +1466,7 @@ Proof. destruct p; simpl; auto using persistently_exist. Qed.
Lemma
persistently_if_sep_2
p
P
Q
:
bi_persistently_if
p
P
∗
bi_persistently_if
p
Q
⊢
bi_persistently_if
p
(
P
∗
Q
).
Proof
.
destruct
p
;
simpl
;
auto
using
persistently_sep_2
.
Qed
.
Lemma
persistently_if_sep
`
{
Positive
BI
PROP
}
p
P
Q
:
Lemma
persistently_if_sep
`
{
Bi
Positive
PROP
}
p
P
Q
:
bi_persistently_if
p
(
P
∗
Q
)
⊣
⊢
bi_persistently_if
p
P
∗
bi_persistently_if
p
Q
.
Proof
.
destruct
p
;
simpl
;
auto
using
persistently_sep
.
Qed
.
...
...
@@ -1496,7 +1496,7 @@ Lemma affinely_persistently_if_exist {A} p (Ψ : A → PROP) :
Proof
.
destruct
p
;
simpl
;
auto
using
affinely_persistently_exist
.
Qed
.
Lemma
affinely_persistently_if_sep_2
p
P
Q
:
□
?p
P
∗
□
?p
Q
⊢
□
?p
(
P
∗
Q
).
Proof
.
destruct
p
;
simpl
;
auto
using
affinely_persistently_sep_2
.
Qed
.
Lemma
affinely_persistently_if_sep
`
{
Positive
BI
PROP
}
p
P
Q
:
Lemma
affinely_persistently_if_sep
`
{
Bi
Positive
PROP
}
p
P
Q
:
□
?p
(
P
∗
Q
)
⊣
⊢
□
?p
P
∗
□
?p
Q
.
Proof
.
destruct
p
;
simpl
;
auto
using
affinely_persistently_sep
.
Qed
.
...
...
@@ -1527,7 +1527,7 @@ Lemma plainly_if_or p P Q : bi_plainly_if p (P ∨ Q) ⊣⊢ bi_plainly_if p P
Proof
.
destruct
p
;
simpl
;
auto
using
plainly_or
.
Qed
.
Lemma
plainly_if_exist
{
A
}
p
(
Ψ
:
A
→
PROP
)
:
(
bi_plainly_if
p
(
∃
a
,
Ψ
a
))
⊣
⊢
∃
a
,
bi_plainly_if
p
(
Ψ
a
).
Proof
.
destruct
p
;
simpl
;
auto
using
plainly_exist
.
Qed
.
Lemma
plainly_if_sep
`
{
Positive
BI
PROP
}
p
P
Q
:
Lemma
plainly_if_sep
`
{
Bi
Positive
PROP
}
p
P
Q
:
bi_plainly_if
p
(
P
∗
Q
)
⊣
⊢
bi_plainly_if
p
P
∗
bi_plainly_if
p
Q
.
Proof
.
destruct
p
;
simpl
;
auto
using
plainly_sep
.
Qed
.
...
...
@@ -1557,7 +1557,7 @@ Lemma affinely_plainly_if_exist {A} p (Ψ : A → PROP) :
Proof
.
destruct
p
;
simpl
;
auto
using
affinely_plainly_exist
.
Qed
.
Lemma
affinely_plainly_if_sep_2
p
P
Q
:
■
?p
P
∗
■
?p
Q
⊢
■
?p
(
P
∗
Q
).
Proof
.
destruct
p
;
simpl
;
auto
using
affinely_plainly_sep_2
.
Qed
.
Lemma
affinely_plainly_if_sep
`
{
Positive
BI
PROP
}
p
P
Q
:
Lemma
affinely_plainly_if_sep
`
{
Bi
Positive
PROP
}
p
P
Q
:
■
?p
(
P
∗
Q
)
⊣
⊢
■
?p
P
∗
■
?p
Q
.
Proof
.
destruct
p
;
simpl
;
auto
using
affinely_plainly_sep
.
Qed
.
...
...
@@ -1626,7 +1626,7 @@ Lemma impl_wand_2 P `{!Persistent P} Q : (P -∗ Q) ⊢ P → Q.
Proof
.
apply
impl_intro_l
.
by
rewrite
persistent_and_sep_1
wand_elim_r
.
Qed
.
Section
persistent_bi_absorbing
.
Context
`
{
Affine
BI
PROP
}.
Context
`
{
Bi
Affine
PROP
}.
Lemma
persistent_and_sep
P
Q
`
{
HPQ
:
!
TCOr
(
Persistent
P
)
(
Persistent
Q
)}
:
P
∧
Q
⊣
⊢
P
∗
Q
.
...
...
@@ -1858,11 +1858,11 @@ Proof.
split
;
[
split
|]
;
try
apply
_
.
apply
plainly_or
.
apply
plainly_pure
.
Qed
.
Global
Instance
bi_plainly_sep_weak_homomorphism
`
{
Positive
BI
PROP
}
:
Global
Instance
bi_plainly_sep_weak_homomorphism
`
{
Bi
Positive
PROP
}
:
WeakMonoidHomomorphism
bi_sep
bi_sep
(
≡
)
(@
bi_plainly
PROP
).
Proof
.
split
;
try
apply
_
.
apply
plainly_sep
.
Qed
.
Global
Instance
bi_plainly_sep_homomorphism
`
{
Affine
BI
PROP
}
:
Global
Instance
bi_plainly_sep_homomorphism
`
{
Bi
Affine
PROP
}
:
MonoidHomomorphism
bi_sep
bi_sep
(
≡
)
(@
bi_plainly
PROP
).
Proof
.
split
.
apply
_
.
apply
plainly_emp
.
Qed
.
...
...
@@ -1886,11 +1886,11 @@ Proof.
split
;
[
split
|]
;
try
apply
_
.
apply
persistently_or
.
apply
persistently_pure
.
Qed
.
Global
Instance
bi_persistently_sep_weak_homomorphism
`
{
Positive
BI
PROP
}
:
Global
Instance
bi_persistently_sep_weak_homomorphism
`
{
Bi
Positive
PROP
}
:
WeakMonoidHomomorphism
bi_sep
bi_sep
(
≡
)
(@
bi_persistently
PROP
).
Proof
.
split
;
try
apply
_
.
apply
persistently_sep
.
Qed
.
Global
Instance
bi_persistently_sep_homomorphism
`
{
Affine
BI
PROP
}
:
Global
Instance
bi_persistently_sep_homomorphism
`
{
Bi
Affine
PROP
}
:
MonoidHomomorphism
bi_sep
bi_sep
(
≡
)
(@
bi_persistently
PROP
).
Proof
.
split
.
apply
_
.
apply
persistently_emp
.
Qed
.
...
...
@@ -1978,7 +1978,7 @@ Qed.
Lemma
later_True
:
▷
True
⊣
⊢
True
.
Proof
.
apply
(
anti_symm
(
⊢
))
;
auto
using
later_intro
.
Qed
.
Lemma
later_emp
`
{!
Affine
BI
PROP
}
:
▷
emp
⊣
⊢
emp
.
Lemma
later_emp
`
{!
Bi
Affine
PROP
}
:
▷
emp
⊣
⊢
emp
.
Proof
.
by
rewrite
-
True_emp
later_True
.
Qed
.
Lemma
later_forall
{
A
}
(
Φ
:
A
→
PROP
)
:
(
▷
∀
a
,
Φ
a
)
⊣
⊢
(
∀
a
,
▷
Φ
a
).
Proof
.
...
...
@@ -2059,7 +2059,7 @@ Proof. induction n as [|n IH]; simpl; by rewrite -?later_intro. Qed.
Lemma
laterN_True
n
:
▷
^
n
True
⊣
⊢
True
.
Proof
.
apply
(
anti_symm
(
⊢
))
;
auto
using
laterN_intro
,
True_intro
.
Qed
.
Lemma
laterN_emp
`
{!
Affine
BI
PROP
}
n
:
▷
^
n
emp
⊣
⊢
emp
.
Lemma
laterN_emp
`
{!
Bi
Affine
PROP
}
n
:
▷
^
n
emp
⊣
⊢
emp
.
Proof
.
by
rewrite
-
True_emp
laterN_True
.
Qed
.
Lemma
laterN_forall
{
A
}
n
(
Φ
:
A
→
PROP
)
:
(
▷
^
n
∀
a
,
Φ
a
)
⊣
⊢
(
∀
a
,
▷
^
n
Φ
a
).
Proof
.
induction
n
as
[|
n
IH
]
;
simpl
;
rewrite
-
?later_forall
?IH
;
auto
.
Qed
.
...
...
@@ -2124,7 +2124,7 @@ Proof. apply (anti_symm _); rewrite /bi_except_0; auto. Qed.
Lemma
except_0_True
:
◇
True
⊣
⊢
True
.
Proof
.
rewrite
/
bi_except_0
.
apply
(
anti_symm
_
)
;
auto
.
Qed
.
Lemma
except_0_emp
`
{!
Affine
BI
PROP
}
:
◇
emp
⊣
⊢
emp
.
Lemma
except_0_emp
`
{!
Bi
Affine
PROP
}
:
◇
emp
⊣
⊢
emp
.
Proof
.
by
rewrite
-
True_emp
except_0_True
.
Qed
.
Lemma
except_0_or
P
Q
:
◇
(
P
∨
Q
)
⊣
⊢
◇
P
∨
◇
Q
.
Proof
.
rewrite
/
bi_except_0
.
apply
(
anti_symm
_
)
;
auto
.
Qed
.
...
...
@@ -2208,7 +2208,7 @@ Proof.
rewrite
/
Timeless
/
bi_except_0
pure_alt
later_exist_false
.
apply
or_elim
,
exist_elim
;
[
auto
|]=>
H
φ
.
rewrite
-(
exist_intro
H
φ
).
auto
.
Qed
.
Global
Instance
emp_timeless
`
{
Affine
BI
PROP
}
:
Timeless
(
emp
:
PROP
)%
I
.
Global
Instance
emp_timeless
`
{
Bi
Affine
PROP
}
:
Timeless
(
emp
:
PROP
)%
I
.
Proof
.
rewrite
-
True_emp
.
apply
_
.
Qed
.
Global
Instance
and_timeless
P
Q
:
Timeless
P
→
Timeless
Q
→
Timeless
(
P
∧
Q
).
...
...
@@ -2305,13 +2305,13 @@ Global Instance bi_except_0_sep_weak_homomorphism :
WeakMonoidHomomorphism
bi_sep
bi_sep
(
≡
)
(@
bi_except_0
PROP
).
Proof
.
split
;
try
apply
_
.
apply
except_0_sep
.
Qed
.
Global
Instance
bi_later_monoid_sep_homomorphism
`
{!
Affine
BI
PROP
}
:
Global
Instance
bi_later_monoid_sep_homomorphism
`
{!
Bi
Affine
PROP
}
:
MonoidHomomorphism
bi_sep
bi_sep
(
≡
)
(@
bi_later
PROP
).
Proof
.
split
;
try
apply
_
.
apply
later_emp
.
Qed
.
Global
Instance
bi_laterN_sep_homomorphism
`
{!
Affine
BI
PROP
}
n
:
Global
Instance
bi_laterN_sep_homomorphism
`
{!
Bi
Affine
PROP
}
n
:
MonoidHomomorphism
bi_sep
bi_sep
(
≡
)
(@
bi_laterN
PROP
n
).
Proof
.
split
;
try
apply
_
.
apply
laterN_emp
.
Qed
.
Global
Instance
bi_except_0_sep_homomorphism
`
{!
Affine
BI
PROP
}
:
Global
Instance
bi_except_0_sep_homomorphism
`
{!
Bi
Affine
PROP
}
:
MonoidHomomorphism
bi_sep
bi_sep
(
≡
)
(@
bi_except_0
PROP
).
Proof
.
split
;
try
apply
_
.
apply
except_0_emp
.
Qed
.
...
...
theories/bi/tactics.v
View file @
5524871e
...
...
@@ -32,7 +32,7 @@ Module bi_reflection. Section bi_reflection.
Qed
.
(* Can be related to the RHS being affine *)
Lemma
flatten_entails
`
{
Affine
BI
PROP
}
Σ
e1
e2
:
Lemma
flatten_entails
`
{
Bi
Affine
PROP
}
Σ
e1
e2
:
flatten
e2
⊆
+
flatten
e1
→
eval
Σ
e1
⊢
eval
Σ
e2
.
Proof
.
intros
.
rewrite
!
eval_flatten
.
by
apply
big_sepL_submseteq
.
Qed
.
Lemma
flatten_equiv
Σ
e1
e2
:
...
...
theories/proofmode/class_instances.v
View file @
5524871e
...
...
@@ -50,7 +50,7 @@ Proof.
rewrite
/
FromAssumption
/=
=><-.
by
rewrite
persistently_elim
plainly_elim_persistently
.
Qed
.
Global
Instance
from_assumption_plainly_l_false
`
{
Affine
BI
PROP
}
P
Q
:
Global
Instance
from_assumption_plainly_l_false
`
{
Bi
Affine
PROP
}
P
Q
:
FromAssumption
true
P
Q
→
FromAssumption
false
(
bi_plainly
P
)
Q
.
Proof
.
rewrite
/
FromAssumption
/=
=><-.
...
...
@@ -62,7 +62,7 @@ Proof. rewrite /FromAssumption /= =><-. by rewrite affinely_persistently_if_elim
Global
Instance
from_assumption_persistently_l_true
P
Q
:
FromAssumption
true
P
Q
→
FromAssumption
true
(
bi_persistently
P
)
Q
.
Proof
.
rewrite
/
FromAssumption
/=
=><-.
by
rewrite
persistently_idemp
.
Qed
.
Global
Instance
from_assumption_persistently_l_false
`
{
Affine
BI
PROP
}
P
Q
:
Global
Instance
from_assumption_persistently_l_false
`
{
Bi
Affine
PROP
}
P
Q
:
FromAssumption
true
P
Q
→
FromAssumption
false
(
bi_persistently
P
)
Q
.
Proof
.
rewrite
/
FromAssumption
/=
=><-.
by
rewrite
affine_affinely
.
Qed
.
Global
Instance
from_assumption_affinely_l_true
p
P
Q
:
...
...
@@ -224,7 +224,7 @@ Proof.
rewrite
/
FromAssumption
/
IntoWand
=>
HP
.
by
rewrite
HP
affinely_persistently_if_elim
.
Qed
.
Global
Instance
into_wand_impl_false_false
`
{!
Affine
BI
PROP
}
P
Q
P'
:
Global
Instance
into_wand_impl_false_false
`
{!
Bi
Affine
PROP
}
P
Q
P'
:
FromAssumption
false
P
P'
→
IntoWand
false
false
(
P'
→
Q
)
P
Q
.
Proof
.