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
George Pirlea
Iris
Commits
2ba2ba1e
Commit
2ba2ba1e
authored
Mar 03, 2018
by
Robbert Krebbers
Browse files
Notations <absorb>, <affine> and <pers>.
parent
edc37245
Changes
18
Expand all
Hide whitespace changes
Inline
Side-by-side
theories/base_logic/derived.v
View file @
2ba2ba1e
...
...
@@ -16,8 +16,7 @@ Notation "P ⊢ Q" := (bi_entails (PROP:=uPredI M) P%I Q%I).
Notation
"P ⊣⊢ Q"
:
=
(
equiv
(
A
:
=
uPredI
M
)
P
%
I
Q
%
I
).
(* Own and valid derived *)
Lemma
persistently_cmra_valid_1
{
A
:
cmraT
}
(
a
:
A
)
:
✓
a
⊢
bi_persistently
(
✓
a
:
uPred
M
).
Lemma
persistently_cmra_valid_1
{
A
:
cmraT
}
(
a
:
A
)
:
✓
a
⊢
<
pers
>
(
✓
a
:
uPred
M
).
Proof
.
by
rewrite
{
1
}
plainly_cmra_valid_1
plainly_elim_persistently
.
Qed
.
Lemma
affinely_persistently_ownM
(
a
:
M
)
:
CoreId
a
→
□
uPred_ownM
a
⊣
⊢
uPred_ownM
a
.
Proof
.
...
...
theories/base_logic/upred.v
View file @
2ba2ba1e
...
...
@@ -457,21 +457,21 @@ Proof.
-
(* (P ⊢ Q -∗ R) → P ∗ Q ⊢ R *)
intros
P
Q
R
.
unseal
=>
HPQR
.
split
;
intros
n
x
?
(?&?&?&?&?).
ofe_subst
.
eapply
HPQR
;
eauto
using
cmra_validN_op_l
.
-
(* (P ⊢ Q) →
bi_
pers
istently
P ⊢
bi_
pers
istently
Q *)
-
(* (P ⊢ Q) →
<
pers
>
P ⊢
<
pers
>
Q *)
intros
P
QR
HP
.
unseal
;
split
=>
n
x
?
/=.
by
apply
HP
,
cmra_core_validN
.
-
(*
bi_
pers
istently
P ⊢
bi_
pers
istently (bi_persistently
P
)
*)
-
(*
<
pers
>
P ⊢
<
pers
> <pers>
P *)
intros
P
.
unseal
;
split
=>
n
x
??
/=.
by
rewrite
cmra_core_idemp
.
-
(* P ⊢
bi_
pers
istently
emp (ADMISSIBLE) *)
-
(* P ⊢
<
pers
>
emp (ADMISSIBLE) *)
by
unseal
.
-
(* (∀ a,
bi_
pers
istently
(Ψ a)) ⊢
bi_
pers
istently
(∀ a, Ψ a) *)
-
(* (∀ a,
<
pers
>
(Ψ a)) ⊢
<
pers
>
(∀ a, Ψ a) *)
by
unseal
.
-
(*
bi_
pers
istently
(∃ a, Ψ a) ⊢ ∃ a,
bi_
pers
istently
(Ψ a) *)
-
(*
<
pers
>
(∃ a, Ψ a) ⊢ ∃ a,
<
pers
>
(Ψ a) *)
by
unseal
.
-
(*
bi_
pers
istently
P ∗ Q ⊢
bi_
pers
istently
P (ADMISSIBLE) *)
-
(*
<
pers
>
P ∗ Q ⊢
<
pers
>
P (ADMISSIBLE) *)
intros
P
Q
.
move
:
(
uPred_persistently
P
)=>
P'
.
unseal
;
split
;
intros
n
x
?
(
x1
&
x2
&?&?&
_
)
;
ofe_subst
;
eauto
using
uPred_mono
,
cmra_includedN_l
.
-
(*
bi_
pers
istently
P ∧ Q ⊢ P ∗ Q *)
-
(*
<
pers
>
P ∧ Q ⊢ P ∗ Q *)
intros
P
Q
.
unseal
;
split
=>
n
x
?
[??]
;
simpl
in
*.
exists
(
core
x
),
x
;
rewrite
?cmra_core_l
;
auto
.
Qed
.
...
...
@@ -523,9 +523,9 @@ Proof.
-
(* ▷ P ∗ ▷ Q ⊢ ▷ (P ∗ Q) *)
intros
P
Q
.
unseal
;
split
=>
-[|
n
]
x
?
/=
;
[
done
|
intros
(
x1
&
x2
&
Hx
&?&?)].
exists
x1
,
x2
;
eauto
using
dist_S
.
-
(* ▷
bi_
pers
istently
P ⊢
bi_
pers
istently (
▷ P
)
*)
-
(* ▷
<
pers
>
P ⊢
<
pers
>
▷ P *)
by
unseal
.
-
(*
bi_
pers
istently (
▷ P
)
⊢ ▷
bi_
pers
istently
P *)
-
(*
<
pers
>
▷ P ⊢ ▷
<
pers
>
P *)
by
unseal
.
-
(* ▷ P ⊢ ▷ False ∨ (▷ False → P) *)
intros
P
.
unseal
;
split
=>
-[|
n
]
x
?
/=
HP
;
[
by
left
|
right
].
...
...
@@ -552,13 +552,13 @@ Proof.
unseal
;
split
=>
n'
x
;
split
;
apply
HP
;
eauto
using
@
ucmra_unit_validN
.
-
(* (P ⊢ Q) → ■ P ⊢ ■ Q *)
intros
P
QR
HP
.
unseal
;
split
=>
n
x
?
/=.
by
apply
HP
,
ucmra_unit_validN
.
-
(* ■ P ⊢
bi_
pers
istently
P *)
-
(* ■ P ⊢
<
pers
>
P *)
unseal
;
split
;
simpl
;
eauto
using
uPred_mono
,
@
ucmra_unit_leastN
.
-
(* ■ P ⊢ ■ ■ P *)
unseal
;
split
=>
n
x
??
//.
-
(* (∀ a, ■ (Ψ a)) ⊢ ■ (∀ a, Ψ a) *)
by
unseal
.
-
(* (■ P →
bi_
pers
istently
Q) ⊢
bi_
pers
istently
(■ P → Q) *)
-
(* (■ P →
<
pers
>
Q) ⊢
<
pers
>
(■ P → Q) *)
unseal
;
split
=>
/=
n
x
?
HPQ
n'
x'
????.
eapply
uPred_mono
with
n'
(
core
x
)=>//
;
[|
by
apply
cmra_included_includedN
].
apply
(
HPQ
n'
x
)
;
eauto
using
cmra_validN_le
.
...
...
@@ -665,8 +665,7 @@ Proof.
by
rewrite
(
assoc
op
_
z1
)
-(
comm
op
z1
)
(
assoc
op
z1
)
-(
assoc
op
_
a2
)
(
comm
op
z1
)
-
Hy1
-
Hy2
.
Qed
.
Lemma
persistently_ownM_core
(
a
:
M
)
:
uPred_ownM
a
⊢
bi_persistently
(
uPred_ownM
(
core
a
)).
Lemma
persistently_ownM_core
(
a
:
M
)
:
uPred_ownM
a
⊢
<
pers
>
uPred_ownM
(
core
a
).
Proof
.
rewrite
/
bi_persistently
/=.
unseal
.
split
=>
n
x
Hx
/=.
by
apply
cmra_core_monoN
.
...
...
theories/bi/big_op.v
View file @
2ba2ba1e
...
...
@@ -127,8 +127,7 @@ Section sep_list.
Proof
.
auto
using
and_intro
,
big_sepL_mono
,
and_elim_l
,
and_elim_r
.
Qed
.
Lemma
big_sepL_persistently
`
{
BiAffine
PROP
}
Φ
l
:
bi_persistently
([
∗
list
]
k
↦
x
∈
l
,
Φ
k
x
)
⊣
⊢
[
∗
list
]
k
↦
x
∈
l
,
bi_persistently
(
Φ
k
x
).
<
pers
>
([
∗
list
]
k
↦
x
∈
l
,
Φ
k
x
)
⊣
⊢
[
∗
list
]
k
↦
x
∈
l
,
<
pers
>
(
Φ
k
x
).
Proof
.
apply
(
big_opL_commute
_
).
Qed
.
Lemma
big_sepL_forall
`
{
BiAffine
PROP
}
Φ
l
:
...
...
@@ -266,8 +265,7 @@ Section and_list.
Proof
.
auto
using
and_intro
,
big_andL_mono
,
and_elim_l
,
and_elim_r
.
Qed
.
Lemma
big_andL_persistently
Φ
l
:
bi_persistently
([
∧
list
]
k
↦
x
∈
l
,
Φ
k
x
)
⊣
⊢
[
∧
list
]
k
↦
x
∈
l
,
bi_persistently
(
Φ
k
x
).
<
pers
>
([
∧
list
]
k
↦
x
∈
l
,
Φ
k
x
)
⊣
⊢
[
∧
list
]
k
↦
x
∈
l
,
<
pers
>
(
Φ
k
x
).
Proof
.
apply
(
big_opL_commute
_
).
Qed
.
Lemma
big_andL_forall
`
{
BiAffine
PROP
}
Φ
l
:
...
...
@@ -398,8 +396,7 @@ Section gmap.
Proof
.
auto
using
and_intro
,
big_sepM_mono
,
and_elim_l
,
and_elim_r
.
Qed
.
Lemma
big_sepM_persistently
`
{
BiAffine
PROP
}
Φ
m
:
(
bi_persistently
([
∗
map
]
k
↦
x
∈
m
,
Φ
k
x
))
⊣
⊢
([
∗
map
]
k
↦
x
∈
m
,
bi_persistently
(
Φ
k
x
)).
(<
pers
>
([
∗
map
]
k
↦
x
∈
m
,
Φ
k
x
))
⊣
⊢
([
∗
map
]
k
↦
x
∈
m
,
<
pers
>
(
Φ
k
x
)).
Proof
.
apply
(
big_opM_commute
_
).
Qed
.
Lemma
big_sepM_forall
`
{
BiAffine
PROP
}
Φ
m
:
...
...
@@ -564,7 +561,7 @@ Section gset.
Proof
.
auto
using
and_intro
,
big_sepS_mono
,
and_elim_l
,
and_elim_r
.
Qed
.
Lemma
big_sepS_persistently
`
{
BiAffine
PROP
}
Φ
X
:
bi_
pers
istently
([
∗
set
]
y
∈
X
,
Φ
y
)
⊣
⊢
[
∗
set
]
y
∈
X
,
bi_
pers
istently
(
Φ
y
).
<
pers
>
([
∗
set
]
y
∈
X
,
Φ
y
)
⊣
⊢
[
∗
set
]
y
∈
X
,
<
pers
>
(
Φ
y
).
Proof
.
apply
(
big_opS_commute
_
).
Qed
.
Lemma
big_sepS_forall
`
{
BiAffine
PROP
}
Φ
X
:
...
...
@@ -672,8 +669,7 @@ Section gmultiset.
Proof
.
auto
using
and_intro
,
big_sepMS_mono
,
and_elim_l
,
and_elim_r
.
Qed
.
Lemma
big_sepMS_persistently
`
{
BiAffine
PROP
}
Φ
X
:
bi_persistently
([
∗
mset
]
y
∈
X
,
Φ
y
)
⊣
⊢
[
∗
mset
]
y
∈
X
,
bi_persistently
(
Φ
y
).
<
pers
>
([
∗
mset
]
y
∈
X
,
Φ
y
)
⊣
⊢
[
∗
mset
]
y
∈
X
,
<
pers
>
(
Φ
y
).
Proof
.
apply
(
big_opMS_commute
_
).
Qed
.
Global
Instance
big_sepMS_empty_persistent
Φ
:
...
...
theories/bi/derived_connectives.v
View file @
2ba2ba1e
...
...
@@ -13,7 +13,7 @@ Arguments bi_wand_iff {_} _%I _%I : simpl never.
Instance
:
Params
(@
bi_wand_iff
)
1
.
Infix
"∗-∗"
:
=
bi_wand_iff
(
at
level
95
,
no
associativity
)
:
bi_scope
.
Class
Persistent
{
PROP
:
bi
}
(
P
:
PROP
)
:
=
persistent
:
P
⊢
bi_
pers
istently
P
.
Class
Persistent
{
PROP
:
bi
}
(
P
:
PROP
)
:
=
persistent
:
P
⊢
<
pers
>
P
.
Arguments
Persistent
{
_
}
_
%
I
:
simpl
never
.
Arguments
persistent
{
_
}
_
%
I
{
_
}.
Hint
Mode
Persistent
+
!
:
typeclass_instances
.
...
...
@@ -23,7 +23,10 @@ Definition bi_affinely {PROP : bi} (P : PROP) : PROP := (emp ∧ P)%I.
Arguments
bi_affinely
{
_
}
_
%
I
:
simpl
never
.
Instance
:
Params
(@
bi_affinely
)
1
.
Typeclasses
Opaque
bi_affinely
.
Notation
"□ P"
:
=
(
bi_affinely
(
bi_persistently
P
))%
I
Notation
"'<affine>' P"
:
=
(
bi_affinely
P
)
(
at
level
20
,
right
associativity
)
:
bi_scope
.
Notation
"□ P"
:
=
(<
affine
>
<
pers
>
P
)%
I
(
at
level
20
,
right
associativity
)
:
bi_scope
.
Class
Affine
{
PROP
:
bi
}
(
Q
:
PROP
)
:
=
affine
:
Q
⊢
emp
.
...
...
@@ -36,31 +39,40 @@ Hint Mode BiAffine ! : typeclass_instances.
Existing
Instance
absorbing_bi
|
0
.
Class
BiPositive
(
PROP
:
bi
)
:
=
bi_positive
(
P
Q
:
PROP
)
:
bi_
affine
ly
(
P
∗
Q
)
⊢
bi_
affine
ly
P
∗
Q
.
bi_positive
(
P
Q
:
PROP
)
:
<
affine
>
(
P
∗
Q
)
⊢
<
affine
>
P
∗
Q
.
Hint
Mode
BiPositive
!
:
typeclass_instances
.
Definition
bi_absorbingly
{
PROP
:
bi
}
(
P
:
PROP
)
:
PROP
:
=
(
True
∗
P
)%
I
.
Arguments
bi_absorbingly
{
_
}
_
%
I
:
simpl
never
.
Instance
:
Params
(@
bi_absorbingly
)
1
.
Typeclasses
Opaque
bi_absorbingly
.
Notation
"'<absorb>' P"
:
=
(
bi_absorbingly
P
)
(
at
level
20
,
right
associativity
)
:
bi_scope
.
Class
Absorbing
{
PROP
:
bi
}
(
P
:
PROP
)
:
=
absorbing
:
bi_
absorb
ingly
P
⊢
P
.
Class
Absorbing
{
PROP
:
bi
}
(
P
:
PROP
)
:
=
absorbing
:
<
absorb
>
P
⊢
P
.
Arguments
Absorbing
{
_
}
_
%
I
:
simpl
never
.
Arguments
absorbing
{
_
}
_
%
I
.
Hint
Mode
Absorbing
+
!
:
typeclass_instances
.
Definition
bi_persistently_if
{
PROP
:
bi
}
(
p
:
bool
)
(
P
:
PROP
)
:
PROP
:
=
(
if
p
then
bi_
pers
istently
P
else
P
)%
I
.
(
if
p
then
<
pers
>
P
else
P
)%
I
.
Arguments
bi_persistently_if
{
_
}
!
_
_
%
I
/.
Instance
:
Params
(@
bi_persistently_if
)
2
.
Typeclasses
Opaque
bi_persistently_if
.
Notation
"'<pers>?' p P"
:
=
(
bi_persistently_if
p
P
)
(
at
level
20
,
p
at
level
9
,
P
at
level
20
,
right
associativity
,
format
"'<pers>?' p P"
)
:
bi_scope
.
Definition
bi_affinely_if
{
PROP
:
bi
}
(
p
:
bool
)
(
P
:
PROP
)
:
PROP
:
=
(
if
p
then
bi_
affine
ly
P
else
P
)%
I
.
(
if
p
then
<
affine
>
P
else
P
)%
I
.
Arguments
bi_affinely_if
{
_
}
!
_
_
%
I
/.
Instance
:
Params
(@
bi_affinely_if
)
2
.
Typeclasses
Opaque
bi_affinely_if
.
Notation
"□? p P"
:
=
(
bi_affinely_if
p
(
bi_persistently_if
p
P
))%
I
Notation
"'<affine>?' p P"
:
=
(
bi_affinely_if
p
P
)
(
at
level
20
,
p
at
level
9
,
P
at
level
20
,
right
associativity
,
format
"'<affine>?' p P"
)
:
bi_scope
.
Notation
"□? p P"
:
=
(<
affine
>
?p
<
pers
>
?p
P
)%
I
(
at
level
20
,
p
at
level
9
,
P
at
level
20
,
right
associativity
,
format
"□? p P"
)
:
bi_scope
.
...
...
theories/bi/derived_laws.v
View file @
2ba2ba1e
This diff is collapsed.
Click to expand it.
theories/bi/embedding.v
View file @
2ba2ba1e
...
...
@@ -22,7 +22,7 @@ Record BiEmbedMixin (PROP1 PROP2 : bi) `(Embed PROP1 PROP2) := {
bi_embed_mixin_exist_1
A
(
Φ
:
A
→
PROP1
)
:
⎡
∃
x
,
Φ
x
⎤
⊢
∃
x
,
⎡Φ
x
⎤
;
bi_embed_mixin_sep
P
Q
:
⎡
P
∗
Q
⎤
⊣
⊢
⎡
P
⎤
∗
⎡
Q
⎤
;
bi_embed_mixin_wand_2
P
Q
:
(
⎡
P
⎤
-
∗
⎡
Q
⎤
)
⊢
⎡
P
-
∗
Q
⎤
;
bi_embed_mixin_persistently
P
:
⎡
bi_
pers
istently
P
⎤
⊣
⊢
bi_
pers
istently
⎡
P
⎤
bi_embed_mixin_persistently
P
:
⎡
<
pers
>
P
⎤
⊣
⊢
<
pers
>
⎡
P
⎤
}.
Class
BiEmbed
(
PROP1
PROP2
:
bi
)
:
=
{
...
...
@@ -79,7 +79,7 @@ Section embed_laws.
Proof
.
eapply
bi_embed_mixin_sep
,
bi_embed_mixin
.
Qed
.
Lemma
embed_wand_2
P
Q
:
(
⎡
P
⎤
-
∗
⎡
Q
⎤
)
⊢
⎡
P
-
∗
Q
⎤
.
Proof
.
eapply
bi_embed_mixin_wand_2
,
bi_embed_mixin
.
Qed
.
Lemma
embed_persistently
P
:
⎡
bi_
pers
istently
P
⎤
⊣
⊢
bi_
pers
istently
⎡
P
⎤
.
Lemma
embed_persistently
P
:
⎡
<
pers
>
P
⎤
⊣
⊢
<
pers
>
⎡
P
⎤
.
Proof
.
eapply
bi_embed_mixin_persistently
,
bi_embed_mixin
.
Qed
.
End
embed_laws
.
...
...
@@ -141,14 +141,13 @@ Section embed.
Proof
.
by
rewrite
embed_and
!
embed_impl
.
Qed
.
Lemma
embed_wand_iff
P
Q
:
⎡
P
∗
-
∗
Q
⎤
⊣
⊢
(
⎡
P
⎤
∗
-
∗
⎡
Q
⎤
).
Proof
.
by
rewrite
embed_and
!
embed_wand
.
Qed
.
Lemma
embed_affinely
P
:
⎡
bi_
affine
ly
P
⎤
⊣
⊢
bi_
affine
ly
⎡
P
⎤
.
Lemma
embed_affinely
P
:
⎡
<
affine
>
P
⎤
⊣
⊢
<
affine
>
⎡
P
⎤
.
Proof
.
by
rewrite
embed_and
embed_emp
.
Qed
.
Lemma
embed_absorbingly
P
:
⎡
bi_
absorb
ingly
P
⎤
⊣
⊢
bi_
absorb
ingly
⎡
P
⎤
.
Lemma
embed_absorbingly
P
:
⎡
<
absorb
>
P
⎤
⊣
⊢
<
absorb
>
⎡
P
⎤
.
Proof
.
by
rewrite
embed_sep
embed_pure
.
Qed
.
Lemma
embed_persistently_if
P
b
:
⎡
bi_persistently_if
b
P
⎤
⊣
⊢
bi_persistently_if
b
⎡
P
⎤
.
Lemma
embed_persistently_if
P
b
:
⎡
<
pers
>
?b
P
⎤
⊣
⊢
<
pers
>
?b
⎡
P
⎤
.
Proof
.
destruct
b
;
simpl
;
auto
using
embed_persistently
.
Qed
.
Lemma
embed_affinely_if
P
b
:
⎡
bi_
affine
ly_if
b
P
⎤
⊣
⊢
bi_
affine
ly_if
b
⎡
P
⎤
.
Lemma
embed_affinely_if
P
b
:
⎡
<
affine
>
?
b
P
⎤
⊣
⊢
<
affine
>
?
b
⎡
P
⎤
.
Proof
.
destruct
b
;
simpl
;
auto
using
embed_affinely
.
Qed
.
Lemma
embed_hforall
{
As
}
(
Φ
:
himpl
As
PROP1
)
:
⎡
bi_hforall
Φ⎤
⊣
⊢
bi_hforall
(
hcompose
embed
Φ
).
...
...
theories/bi/fixpoint.v
View file @
2ba2ba1e
...
...
@@ -6,7 +6,7 @@ Import bi.
(** Least and greatest fixpoint of a monotone function, defined entirely inside
the logic. *)
Class
BiMonoPred
{
PROP
:
bi
}
{
A
:
ofeT
}
(
F
:
(
A
→
PROP
)
→
(
A
→
PROP
))
:
=
{
bi_mono_pred
Φ
Ψ
:
(
(
bi_persistently
(
∀
x
,
Φ
x
-
∗
Ψ
x
)
)
→
∀
x
,
F
Φ
x
-
∗
F
Ψ
x
)%
I
;
bi_mono_pred
Φ
Ψ
:
(
<
pers
>
(
∀
x
,
Φ
x
-
∗
Ψ
x
)
→
∀
x
,
F
Φ
x
-
∗
F
Ψ
x
)%
I
;
bi_mono_pred_ne
Φ
:
NonExpansive
Φ
→
NonExpansive
(
F
Φ
)
}.
Arguments
bi_mono_pred
{
_
_
_
_
}
_
_
.
...
...
@@ -14,11 +14,11 @@ Local Existing Instance bi_mono_pred_ne.
Definition
bi_least_fixpoint
{
PROP
:
bi
}
{
A
:
ofeT
}
(
F
:
(
A
→
PROP
)
→
(
A
→
PROP
))
(
x
:
A
)
:
PROP
:
=
(
∀
Φ
:
A
-
n
>
PROP
,
bi_
pers
istently
(
∀
x
,
F
Φ
x
-
∗
Φ
x
)
→
Φ
x
)%
I
.
(
∀
Φ
:
A
-
n
>
PROP
,
<
pers
>
(
∀
x
,
F
Φ
x
-
∗
Φ
x
)
→
Φ
x
)%
I
.
Definition
bi_greatest_fixpoint
{
PROP
:
bi
}
{
A
:
ofeT
}
(
F
:
(
A
→
PROP
)
→
(
A
→
PROP
))
(
x
:
A
)
:
PROP
:
=
(
∃
Φ
:
A
-
n
>
PROP
,
bi_
pers
istently
(
∀
x
,
Φ
x
-
∗
F
Φ
x
)
∧
Φ
x
)%
I
.
(
∃
Φ
:
A
-
n
>
PROP
,
<
pers
>
(
∀
x
,
Φ
x
-
∗
F
Φ
x
)
∧
Φ
x
)%
I
.
Section
least
.
Context
{
PROP
:
bi
}
{
A
:
ofeT
}
(
F
:
(
A
→
PROP
)
→
(
A
→
PROP
))
`
{!
BiMonoPred
F
}.
...
...
theories/bi/interface.v
View file @
2ba2ba1e
...
...
@@ -6,6 +6,7 @@ Reserved Notation "'emp'".
Reserved
Notation
"'⌜' φ '⌝'"
(
at
level
1
,
φ
at
level
200
,
format
"⌜ φ ⌝"
).
Reserved
Notation
"P ∗ Q"
(
at
level
80
,
right
associativity
).
Reserved
Notation
"P -∗ Q"
(
at
level
99
,
Q
at
level
200
,
right
associativity
).
Reserved
Notation
"'<pers>' P"
(
at
level
20
,
right
associativity
).
Reserved
Notation
"▷ P"
(
at
level
20
,
right
associativity
).
Section
bi_mixin
.
...
...
@@ -38,6 +39,7 @@ Section bi_mixin.
(
bi_exist
_
(
λ
x
,
..
(
bi_exist
_
(
λ
y
,
P
))
..)).
Local
Infix
"∗"
:
=
bi_sep
.
Local
Infix
"-∗"
:
=
bi_wand
.
Local
Notation
"'<pers>' P"
:
=
(
bi_persistently
P
).
Local
Notation
"x ≡ y"
:
=
(
sbi_internal_eq
_
x
y
).
Local
Notation
"▷ P"
:
=
(
sbi_later
P
).
...
...
@@ -102,27 +104,23 @@ Section bi_mixin.
(* Persistently *)
(* In the ordered RA model: Holds without further assumptions. *)
bi_mixin_persistently_mono
P
Q
:
(
P
⊢
Q
)
→
bi_persistently
P
⊢
bi_persistently
Q
;
bi_mixin_persistently_mono
P
Q
:
(
P
⊢
Q
)
→
<
pers
>
P
⊢
<
pers
>
Q
;
(* In the ordered RA model: `core` is idempotent *)
bi_mixin_persistently_idemp_2
P
:
bi_persistently
P
⊢
bi_persistently
(
bi_persistently
P
)
;
bi_mixin_persistently_idemp_2
P
:
<
pers
>
P
⊢
<
pers
>
<
pers
>
P
;
(* In the ordered RA model: `ε ≼ core x` *)
bi_mixin_persistently_emp_intro
P
:
P
⊢
bi_
pers
istently
emp
;
bi_mixin_persistently_emp_intro
P
:
P
⊢
<
pers
>
emp
;
bi_mixin_persistently_forall_2
{
A
}
(
Ψ
:
A
→
PROP
)
:
(
∀
a
,
bi_
pers
istently
(
Ψ
a
))
⊢
bi_
pers
istently
(
∀
a
,
Ψ
a
)
;
(
∀
a
,
<
pers
>
(
Ψ
a
))
⊢
<
pers
>
(
∀
a
,
Ψ
a
)
;
bi_mixin_persistently_exist_1
{
A
}
(
Ψ
:
A
→
PROP
)
:
bi_
pers
istently
(
∃
a
,
Ψ
a
)
⊢
∃
a
,
bi_
pers
istently
(
Ψ
a
)
;
<
pers
>
(
∃
a
,
Ψ
a
)
⊢
∃
a
,
<
pers
>
(
Ψ
a
)
;
(* In the ordered RA model: [core x ≼ core (x ⋅ y)].
Note that this implies that the core is monotone. *)
bi_mixin_persistently_absorbing
P
Q
:
bi_persistently
P
∗
Q
⊢
bi_persistently
P
;
bi_mixin_persistently_absorbing
P
Q
:
<
pers
>
P
∗
Q
⊢
<
pers
>
P
;
(* In the ordered RA model: [x ⋅ core x = core x]. *)
bi_mixin_persistently_and_sep_elim
P
Q
:
bi_persistently
P
∧
Q
⊢
P
∗
Q
;
bi_mixin_persistently_and_sep_elim
P
Q
:
<
pers
>
P
∧
Q
⊢
P
∗
Q
;
}.
Record
SbiMixin
:
=
{
...
...
@@ -149,10 +147,8 @@ Section bi_mixin.
(
▷
∃
a
,
Φ
a
)
⊢
▷
False
∨
(
∃
a
,
▷
Φ
a
)
;
sbi_mixin_later_sep_1
P
Q
:
▷
(
P
∗
Q
)
⊢
▷
P
∗
▷
Q
;
sbi_mixin_later_sep_2
P
Q
:
▷
P
∗
▷
Q
⊢
▷
(
P
∗
Q
)
;
sbi_mixin_later_persistently_1
P
:
▷
bi_persistently
P
⊢
bi_persistently
(
▷
P
)
;
sbi_mixin_later_persistently_2
P
:
bi_persistently
(
▷
P
)
⊢
▷
bi_persistently
P
;
sbi_mixin_later_persistently_1
P
:
▷
<
pers
>
P
⊢
<
pers
>
▷
P
;
sbi_mixin_later_persistently_2
P
:
<
pers
>
▷
P
⊢
▷
<
pers
>
P
;
sbi_mixin_later_false_em
P
:
▷
P
⊢
▷
False
∨
(
▷
False
→
P
)
;
}.
...
...
@@ -292,6 +288,7 @@ Notation "∀ x .. y , P" :=
(
bi_forall
(
λ
x
,
..
(
bi_forall
(
λ
y
,
P
))
..)%
I
)
:
bi_scope
.
Notation
"∃ x .. y , P"
:
=
(
bi_exist
(
λ
x
,
..
(
bi_exist
(
λ
y
,
P
))
..)%
I
)
:
bi_scope
.
Notation
"'<pers>' P"
:
=
(
bi_persistently
P
)
:
bi_scope
.
Infix
"≡"
:
=
sbi_internal_eq
:
bi_scope
.
Notation
"▷ P"
:
=
(
sbi_later
P
)
:
bi_scope
.
...
...
@@ -391,25 +388,24 @@ Lemma wand_elim_l' P Q R : (P ⊢ Q -∗ R) → P ∗ Q ⊢ R.
Proof
.
eapply
bi_mixin_wand_elim_l'
,
bi_bi_mixin
.
Qed
.
(* Persistently *)
Lemma
persistently_mono
P
Q
:
(
P
⊢
Q
)
→
bi_
pers
istently
P
⊢
bi_
pers
istently
Q
.
Lemma
persistently_mono
P
Q
:
(
P
⊢
Q
)
→
<
pers
>
P
⊢
<
pers
>
Q
.
Proof
.
eapply
bi_mixin_persistently_mono
,
bi_bi_mixin
.
Qed
.
Lemma
persistently_idemp_2
P
:
bi_persistently
P
⊢
bi_persistently
(
bi_persistently
P
).
Lemma
persistently_idemp_2
P
:
<
pers
>
P
⊢
<
pers
>
<
pers
>
P
.
Proof
.
eapply
bi_mixin_persistently_idemp_2
,
bi_bi_mixin
.
Qed
.
Lemma
persistently_emp_intro
P
:
P
⊢
bi_
pers
istently
emp
.
Lemma
persistently_emp_intro
P
:
P
⊢
<
pers
>
emp
.
Proof
.
eapply
bi_mixin_persistently_emp_intro
,
bi_bi_mixin
.
Qed
.
Lemma
persistently_forall_2
{
A
}
(
Ψ
:
A
→
PROP
)
:
(
∀
a
,
bi_
pers
istently
(
Ψ
a
))
⊢
bi_
pers
istently
(
∀
a
,
Ψ
a
).
(
∀
a
,
<
pers
>
(
Ψ
a
))
⊢
<
pers
>
(
∀
a
,
Ψ
a
).
Proof
.
eapply
bi_mixin_persistently_forall_2
,
bi_bi_mixin
.
Qed
.
Lemma
persistently_exist_1
{
A
}
(
Ψ
:
A
→
PROP
)
:
bi_
pers
istently
(
∃
a
,
Ψ
a
)
⊢
∃
a
,
bi_
pers
istently
(
Ψ
a
).
<
pers
>
(
∃
a
,
Ψ
a
)
⊢
∃
a
,
<
pers
>
(
Ψ
a
).
Proof
.
eapply
bi_mixin_persistently_exist_1
,
bi_bi_mixin
.
Qed
.
Lemma
persistently_absorbing
P
Q
:
bi_
pers
istently
P
∗
Q
⊢
bi_
pers
istently
P
.
Lemma
persistently_absorbing
P
Q
:
<
pers
>
P
∗
Q
⊢
<
pers
>
P
.
Proof
.
eapply
(
bi_mixin_persistently_absorbing
bi_entails
),
bi_bi_mixin
.
Qed
.
Lemma
persistently_and_sep_elim
P
Q
:
bi_
pers
istently
P
∧
Q
⊢
P
∗
Q
.
Lemma
persistently_and_sep_elim
P
Q
:
<
pers
>
P
∧
Q
⊢
P
∗
Q
.
Proof
.
eapply
(
bi_mixin_persistently_and_sep_elim
bi_entails
),
bi_bi_mixin
.
Qed
.
End
bi_laws
.
...
...
@@ -459,9 +455,9 @@ Lemma later_sep_1 P Q : ▷ (P ∗ Q) ⊢ ▷ P ∗ ▷ Q.
Proof
.
eapply
sbi_mixin_later_sep_1
,
sbi_sbi_mixin
.
Qed
.
Lemma
later_sep_2
P
Q
:
▷
P
∗
▷
Q
⊢
▷
(
P
∗
Q
).
Proof
.
eapply
sbi_mixin_later_sep_2
,
sbi_sbi_mixin
.
Qed
.
Lemma
later_persistently_1
P
:
▷
bi_
pers
istently
P
⊢
bi_
pers
istently
(
▷
P
)
.
Lemma
later_persistently_1
P
:
▷
<
pers
>
P
⊢
<
pers
>
▷
P
.
Proof
.
eapply
(
sbi_mixin_later_persistently_1
bi_entails
),
sbi_sbi_mixin
.
Qed
.
Lemma
later_persistently_2
P
:
bi_
pers
istently
(
▷
P
)
⊢
▷
bi_
pers
istently
P
.
Lemma
later_persistently_2
P
:
<
pers
>
▷
P
⊢
▷
<
pers
>
P
.
Proof
.
eapply
(
sbi_mixin_later_persistently_2
bi_entails
),
sbi_sbi_mixin
.
Qed
.
Lemma
later_false_em
P
:
▷
P
⊢
▷
False
∨
(
▷
False
→
P
).
...
...
theories/bi/monpred.v
View file @
2ba2ba1e
...
...
@@ -198,7 +198,7 @@ Definition monPred_wand := unseal monPred_wand_aux.
Definition
monPred_wand_eq
:
@
monPred_wand
=
_
:
=
seal_eq
_
.
Program
Definition
monPred_persistently_def
P
:
monPred
:
=
MonPred
(
λ
i
,
bi_
pers
istently
(
P
i
))
_
.
MonPred
(
λ
i
,
<
pers
>
(
P
i
))
%
I
_
.
Next
Obligation
.
solve_proper
.
Qed
.
Definition
monPred_persistently_aux
:
seal
(@
monPred_persistently_def
).
by
eexists
.
Qed
.
Definition
monPred_persistently
:
=
unseal
monPred_persistently_aux
.
...
...
@@ -555,7 +555,7 @@ Lemma monPred_at_sep i P Q : (P ∗ Q) i ⊣⊢ P i ∗ Q i.
Proof
.
by
unseal
.
Qed
.
Lemma
monPred_at_wand
i
P
Q
:
(
P
-
∗
Q
)
i
⊣
⊢
∀
j
,
⌜
i
⊑
j
⌝
→
P
j
-
∗
Q
j
.
Proof
.
by
unseal
.
Qed
.
Lemma
monPred_at_persistently
i
P
:
bi_
pers
istently
P
i
⊣
⊢
bi_
pers
istently
(
P
i
).
Lemma
monPred_at_persistently
i
P
:
(<
pers
>
P
)
i
⊣
⊢
<
pers
>
(
P
i
).
Proof
.
by
unseal
.
Qed
.
Lemma
monPred_at_in
i
j
:
monPred_at
(
monPred_in
j
)
i
⊣
⊢
⌜
j
⊑
i
⌝
.
Proof
.
by
unseal
.
Qed
.
...
...
@@ -563,15 +563,13 @@ Lemma monPred_at_objectively i P : (<obj> P) i ⊣⊢ ∀ j, P j.
Proof
.
by
unseal
.
Qed
.
Lemma
monPred_at_subjectively
i
P
:
(<
subj
>
P
)
i
⊣
⊢
∃
j
,
P
j
.
Proof
.
by
unseal
.
Qed
.
Lemma
monPred_at_persistently_if
i
p
P
:
bi_persistently_if
p
P
i
⊣
⊢
bi_persistently_if
p
(
P
i
).
Lemma
monPred_at_persistently_if
i
p
P
:
(<
pers
>
?p
P
)
i
⊣
⊢
<
pers
>
?p
(
P
i
).
Proof
.
destruct
p
=>//=.
apply
monPred_at_persistently
.
Qed
.
Lemma
monPred_at_affinely
i
P
:
bi_
affine
ly
P
i
⊣
⊢
bi_
affine
ly
(
P
i
).
Lemma
monPred_at_affinely
i
P
:
(<
affine
>
P
)
i
⊣
⊢
<
affine
>
(
P
i
).
Proof
.
by
rewrite
/
bi_affinely
monPred_at_and
monPred_at_emp
.
Qed
.
Lemma
monPred_at_affinely_if
i
p
P
:
bi_affinely_if
p
P
i
⊣
⊢
bi_affinely_if
p
(
P
i
).
Lemma
monPred_at_affinely_if
i
p
P
:
(<
affine
>
?p
P
)
i
⊣
⊢
<
affine
>
?p
(
P
i
).
Proof
.
destruct
p
=>//=.
apply
monPred_at_affinely
.
Qed
.
Lemma
monPred_at_absorbingly
i
P
:
bi_
absorb
ingly
P
i
⊣
⊢
bi_
absorb
ingly
(
P
i
).
Lemma
monPred_at_absorbingly
i
P
:
(<
absorb
>
P
)
i
⊣
⊢
<
absorb
>
(
P
i
).
Proof
.
by
rewrite
/
bi_absorbingly
monPred_at_sep
monPred_at_pure
.
Qed
.
Lemma
monPred_wand_force
i
P
Q
:
(
P
-
∗
Q
)
i
-
∗
(
P
i
-
∗
Q
i
).
...
...
@@ -700,20 +698,16 @@ Proof.
rewrite
bi
.
pure_impl_forall
.
apply
bi
.
forall_intro
=>
_
.
rewrite
(
objective_at
Q
i
).
by
rewrite
(
objective_at
P
k
).
Qed
.
Global
Instance
persistently_objective
P
`
{!
Objective
P
}
:
Objective
(
bi_persistently
P
).
Global
Instance
persistently_objective
P
`
{!
Objective
P
}
:
Objective
(<
pers
>
P
).
Proof
.
intros
i
j
.
unseal
.
by
rewrite
objective_at
.
Qed
.
Global
Instance
affinely_objective
P
`
{!
Objective
P
}
:
Objective
(
bi_
affine
ly
P
).
Global
Instance
affinely_objective
P
`
{!
Objective
P
}
:
Objective
(
<
affine
>
P
).
Proof
.
rewrite
/
bi_affinely
.
apply
_
.
Qed
.
Global
Instance
absorbingly_objective
P
`
{!
Objective
P
}
:
Objective
(
bi_absorbingly
P
).
Global
Instance
absorbingly_objective
P
`
{!
Objective
P
}
:
Objective
(<
absorb
>
P
).
Proof
.
rewrite
/
bi_absorbingly
.
apply
_
.
Qed
.
Global
Instance
persistently_if_objective
P
p
`
{!
Objective
P
}
:
Objective
(
bi_persistently_if
p
P
).
Global
Instance
persistently_if_objective
P
p
`
{!
Objective
P
}
:
Objective
(<
pers
>
?p
P
).
Proof
.
rewrite
/
bi_persistently_if
.
destruct
p
;
apply
_
.
Qed
.
Global
Instance
affinely_if_objective
P
p
`
{!
Objective
P
}
:
Objective
(
bi_affinely_if
p
P
).
Global
Instance
affinely_if_objective
P
p
`
{!
Objective
P
}
:
Objective
(<
affine
>
?p
P
).
Proof
.
rewrite
/
bi_affinely_if
.
destruct
p
;
apply
_
.
Qed
.
(** monPred_in *)
...
...
theories/bi/plainly.v
View file @
2ba2ba1e
...
...
@@ -13,7 +13,7 @@ Record BiPlainlyMixin (PROP : sbi) `(Plainly PROP) := {
bi_plainly_mixin_plainly_ne
:
NonExpansive
plainly
;
bi_plainly_mixin_plainly_mono
P
Q
:
(
P
⊢
Q
)
→
■
P
⊢
■
Q
;
bi_plainly_mixin_plainly_elim_persistently
P
:
■
P
⊢
bi_
pers
istently
P
;
bi_plainly_mixin_plainly_elim_persistently
P
:
■
P
⊢
<
pers
>
P
;
bi_plainly_mixin_plainly_idemp_2
P
:
■
P
⊢
■
■
P
;
bi_plainly_mixin_plainly_forall_2
{
A
}
(
Ψ
:
A
→
PROP
)
:
...
...
@@ -23,7 +23,7 @@ Record BiPlainlyMixin (PROP : sbi) `(Plainly PROP) := {
for persistently and plainly, but for any modality defined as `M P n x :=
∀ y, R x y → P n y`. *)
bi_plainly_mixin_persistently_impl_plainly
P
Q
:
(
■
P
→
bi_
pers
istently
Q
)
⊢
bi_
pers
istently
(
■
P
→
Q
)
;
(
■
P
→
<
pers
>
Q
)
⊢
<
pers
>
(
■
P
→
Q
)
;
bi_plainly_mixin_plainly_impl_plainly
P
Q
:
(
■
P
→
■
Q
)
⊢
■
(
■
P
→
Q
)
;
bi_plainly_mixin_plainly_emp_intro
P
:
P
⊢
■
emp
;
...
...
@@ -59,14 +59,13 @@ Section plainly_laws.
Lemma
plainly_mono
P
Q
:
(
P
⊢
Q
)
→
■
P
⊢
■
Q
.
Proof
.
eapply
bi_plainly_mixin_plainly_mono
,
bi_plainly_mixin
.
Qed
.
Lemma
plainly_elim_persistently
P
:
■
P
⊢
bi_
pers
istently
P
.
Lemma
plainly_elim_persistently
P
:
■
P
⊢
<
pers
>
P
.
Proof
.
eapply
bi_plainly_mixin_plainly_elim_persistently
,
bi_plainly_mixin
.
Qed
.
Lemma
plainly_idemp_2
P
:
■
P
⊢
■
■
P
.
Proof
.
eapply
bi_plainly_mixin_plainly_idemp_2
,
bi_plainly_mixin
.
Qed
.
Lemma
plainly_forall_2
{
A
}
(
Ψ
:
A
→
PROP
)
:
(
∀
a
,
■
(
Ψ
a
))
⊢
■
(
∀
a
,
Ψ
a
).
Proof
.
eapply
bi_plainly_mixin_plainly_forall_2
,
bi_plainly_mixin
.
Qed
.
Lemma
persistently_impl_plainly
P
Q
:
(
■
P
→
bi_persistently
Q
)
⊢
bi_persistently
(
■
P
→
Q
).
Lemma
persistently_impl_plainly
P
Q
:
(
■
P
→
<
pers
>
Q
)
⊢
<
pers
>
(
■
P
→
Q
).
Proof
.
eapply
bi_plainly_mixin_persistently_impl_plainly
,
bi_plainly_mixin
.
Qed
.
Lemma
plainly_impl_plainly
P
Q
:
(
■
P
→
■
Q
)
⊢
■
(
■
P
→
Q
).
Proof
.
eapply
bi_plainly_mixin_plainly_impl_plainly
,
bi_plainly_mixin
.
Qed
.
...
...
@@ -119,19 +118,19 @@ Global Instance plainly_flip_mono' :
Proper
(
flip
(
⊢
)
==>
flip
(
⊢
))
(@
plainly
PROP
_
).
Proof
.
intros
P
Q
;
apply
plainly_mono
.
Qed
.
Lemma
affinely_plainly_elim
P
:
bi_
affine
ly
(
■
P
)
⊢
P
.
Lemma
affinely_plainly_elim
P
:
<
affine
>
■
P
⊢
P
.
Proof
.
by
rewrite
plainly_elim_persistently
affinely_persistently_elim
.
Qed
.
Lemma
persistently_plainly
P
:
bi_
pers
istently
(
■
P
)
⊣
⊢
■
P
.
Lemma
persistently_plainly
P
:
<
pers
>
■
P
⊣
⊢
■
P
.
Proof
.
apply
(
anti_symm
_
).
-
by
rewrite
persistently_elim_absorbingly
/
bi_absorbingly
comm
plainly_absorb
.
-
by
rewrite
{
1
}
plainly_idemp_2
plainly_elim_persistently
.
Qed
.
Lemma
persistently_if_plainly
P
p
:
bi_
pers
istently_if
p
(
■
P
)
⊣
⊢
■
P
.
Lemma
persistently_if_plainly
P
p
:
<
pers
>
?
p
■
P
⊣
⊢
■
P
.
Proof
.
destruct
p
;
last
done
.
exact
:
persistently_plainly
.
Qed
.
Lemma
plainly_persistently
P
:
■
(
bi_persistently
P
)
⊣
⊢
■
P
.
Lemma
plainly_persistently
P
:
■
<
pers
>
P
⊣
⊢
■
P
.
Proof
.
apply
(
anti_symm
_
).
-
rewrite
-{
1
}(
left_id
True
%
I
bi_and
(
■
_
)%
I
)
(
plainly_emp_intro
True
%
I
).
...
...
@@ -140,7 +139,7 @@ Proof.
-
by
rewrite
{
1
}
plainly_idemp_2
(
plainly_elim_persistently
P
).
Qed
.
Lemma
absorbingly_plainly
P
:
bi_
absorb
ingly
(
■
P
)
⊣
⊢
■
P
.
Lemma
absorbingly_plainly
P
:
<
absorb
>
■
P
⊣
⊢
■
P
.
Proof
.
by
rewrite
-(
persistently_plainly
P
)
absorbingly_persistently
.
Qed
.
Lemma
plainly_and_sep_elim
P
Q
:
■
P
∧
Q
-
∗
(
emp
∧
P
)
∗
Q
.
...
...
@@ -149,7 +148,7 @@ Lemma plainly_and_sep_assoc P Q R : ■ P ∧ (Q ∗ R) ⊣⊢ (■ P ∧ Q) ∗
Proof
.
by
rewrite
-(
persistently_plainly
P
)
persistently_and_sep_assoc
.
Qed
.
Lemma
plainly_and_emp_elim
P
:
emp
∧
■
P
⊢
P
.
Proof
.
by
rewrite
plainly_elim_persistently
persistently_and_emp_elim
.
Qed
.
Lemma
plainly_elim_absorbingly
P
:
■
P
⊢
bi_
absorb
ingly
P
.
Lemma
plainly_elim_absorbingly
P
:
■
P
⊢
<
absorb
>
P
.
Proof
.
by
rewrite
plainly_elim_persistently
persistently_elim_absorbingly
.
Qed
.
Lemma
plainly_elim
P
`
{!
Absorbing
P
}
:
■
P
⊢
P
.
Proof
.
by
rewrite
plainly_elim_persistently
persistently_elim
.
Qed
.
...
...
@@ -214,7 +213,7 @@ Proof.
by
rewrite
plainly_and_sep_assoc
(
comm
bi_and
)
plainly_and_emp_elim
.
Qed
.
Lemma
plainly_affinely
P
:
■
(
bi_
affine
ly
P
)
⊣
⊢
■
P
.
Lemma
plainly_affinely
P
:
■
<
affine
>
P
⊣
⊢
■
P
.
Proof
.
by
rewrite
/
bi_affinely
plainly_and
-
plainly_True_emp
plainly_pure
left_id
.
Qed
.
Lemma
and_sep_plainly
P
Q
:
■
P
∧
■
Q
⊣
⊢
■
P
∗
■
Q
.
...
...
@@ -252,7 +251,7 @@ Qed.
Lemma
impl_wand_plainly_2
P
Q
:
(
■
P
-
∗
Q
)
⊢
(
■
P
→
Q
).
Proof
.
apply
impl_intro_l
.
by
rewrite
plainly_and_sep_l_1
wand_elim_r
.
Qed
.
Lemma
impl_wand_affinely_plainly
P
Q
:
(