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
Tej Chajed
iris
Commits
3588f204
Commit
3588f204
authored
Oct 27, 2017
by
Jacques-Henri Jourdan
Browse files
Notation for disjointness: replace ⊥ with ##, so that ⊥ can be used for bottom.
This is to be used on top of stdpp's 4b5d254e.
parent
c3c8ce45
Changes
17
Hide whitespace changes
Inline
Side-by-side
CHANGELOG.md
View file @
3588f204
...
...
@@ -113,7 +113,7 @@ sed 's/\bPersistentP\b/Persistent/g; s/\bTimelessP\b/Timeless/g; s/\bCMRADiscret
*
Slightly weaker notion of atomicity: an expression is atomic if it reduces in
one step to something that does not reduce further.
*
Changed notation for embedding Coq assertions into Iris. The new notation is
⌜φ⌝. Also removed
`=`
and
`
⊥
`
from the Iris scope. (The old notations are
⌜φ⌝. Also removed
`=`
and
`
##
`
from the Iris scope. (The old notations are
provided in
`base_logic.deprecated`
.)
*
Up-closure of namespaces is now a notation (↑) instead of a coercion.
*
With invariants and the physical state being handled in the logic, there is no
...
...
opam
View file @
3588f204
...
...
@@ -12,5 +12,5 @@ remove: ["rm" "-rf" "%{lib}%/coq/user-contrib/iris"]
depends: [
"coq" { >= "8.6.1" & < "8.8~" }
"coq-mathcomp-ssreflect" { (>= "1.6.1" & < "1.7~") | (= "dev") }
"coq-stdpp" { (= "dev.2017-10-28.
3
") | (= "dev") }
"coq-stdpp" { (= "dev.2017-10-28.
7
") | (= "dev") }
]
theories/algebra/big_op.v
View file @
3588f204
...
...
@@ -299,7 +299,7 @@ Section gset.
Proof
.
apply
(
big_opS_fn_insert
(
λ
y
,
id
)).
Qed
.
Lemma
big_opS_union
f
X
Y
:
X
⊥
Y
→
X
##
Y
→
([^
o
set
]
y
∈
X
∪
Y
,
f
y
)
≡
([^
o
set
]
y
∈
X
,
f
y
)
`
o
`
([^
o
set
]
y
∈
Y
,
f
y
).
Proof
.
intros
.
induction
X
as
[|
x
X
?
IH
]
using
collection_ind_L
.
...
...
theories/algebra/coPset.v
View file @
3588f204
...
...
@@ -74,7 +74,7 @@ Section coPset_disj.
Instance
coPset_disj_unit
:
Unit
coPset_disj
:
=
CoPset
∅
.
Instance
coPset_disj_op
:
Op
coPset_disj
:
=
λ
X
Y
,
match
X
,
Y
with
|
CoPset
X
,
CoPset
Y
=>
if
decide
(
X
⊥
Y
)
then
CoPset
(
X
∪
Y
)
else
CoPsetBot
|
CoPset
X
,
CoPset
Y
=>
if
decide
(
X
##
Y
)
then
CoPset
(
X
∪
Y
)
else
CoPsetBot
|
_
,
_
=>
CoPsetBot
end
.
Instance
coPset_disj_pcore
:
PCore
coPset_disj
:
=
λ
_
,
Some
ε
.
...
...
@@ -91,11 +91,11 @@ Section coPset_disj.
exists
(
CoPset
Z
).
coPset_disj_solve
.
Qed
.
Lemma
coPset_disj_valid_inv_l
X
Y
:
✓
(
CoPset
X
⋅
Y
)
→
∃
Y'
,
Y
=
CoPset
Y'
∧
X
⊥
Y'
.
✓
(
CoPset
X
⋅
Y
)
→
∃
Y'
,
Y
=
CoPset
Y'
∧
X
##
Y'
.
Proof
.
destruct
Y
;
repeat
(
simpl
||
case_decide
)
;
by
eauto
.
Qed
.
Lemma
coPset_disj_union
X
Y
:
X
⊥
Y
→
CoPset
X
⋅
CoPset
Y
=
CoPset
(
X
∪
Y
).
Lemma
coPset_disj_union
X
Y
:
X
##
Y
→
CoPset
X
⋅
CoPset
Y
=
CoPset
(
X
∪
Y
).
Proof
.
intros
.
by
rewrite
/=
decide_True
.
Qed
.
Lemma
coPset_disj_valid_op
X
Y
:
✓
(
CoPset
X
⋅
CoPset
Y
)
↔
X
⊥
Y
.
Lemma
coPset_disj_valid_op
X
Y
:
✓
(
CoPset
X
⋅
CoPset
Y
)
↔
X
##
Y
.
Proof
.
simpl
.
case_decide
;
by
split
.
Qed
.
Lemma
coPset_disj_ra_mixin
:
RAMixin
coPset_disj
.
...
...
theories/algebra/dra.v
View file @
3588f204
...
...
@@ -9,21 +9,21 @@ Record DraMixin A `{Equiv A, Core A, Disjoint A, Op A, Valid A} := {
mixin_dra_valid_proper
:
Proper
((
≡
)
==>
impl
)
valid
;
mixin_dra_disjoint_proper
x
:
Proper
((
≡
)
==>
impl
)
(
disjoint
x
)
;
(* validity *)
mixin_dra_op_valid
x
y
:
✓
x
→
✓
y
→
x
⊥
y
→
✓
(
x
⋅
y
)
;
mixin_dra_op_valid
x
y
:
✓
x
→
✓
y
→
x
##
y
→
✓
(
x
⋅
y
)
;
mixin_dra_core_valid
x
:
✓
x
→
✓
core
x
;
(* monoid *)
mixin_dra_assoc
x
y
z
:
✓
x
→
✓
y
→
✓
z
→
x
⊥
y
→
x
⋅
y
⊥
z
→
x
⋅
(
y
⋅
z
)
≡
(
x
⋅
y
)
⋅
z
;
mixin_dra_disjoint_ll
x
y
z
:
✓
x
→
✓
y
→
✓
z
→
x
⊥
y
→
x
⋅
y
⊥
z
→
x
⊥
z
;
✓
x
→
✓
y
→
✓
z
→
x
##
y
→
x
⋅
y
##
z
→
x
⋅
(
y
⋅
z
)
≡
(
x
⋅
y
)
⋅
z
;
mixin_dra_disjoint_ll
x
y
z
:
✓
x
→
✓
y
→
✓
z
→
x
##
y
→
x
⋅
y
##
z
→
x
##
z
;
mixin_dra_disjoint_move_l
x
y
z
:
✓
x
→
✓
y
→
✓
z
→
x
⊥
y
→
x
⋅
y
⊥
z
→
x
⊥
y
⋅
z
;
✓
x
→
✓
y
→
✓
z
→
x
##
y
→
x
⋅
y
##
z
→
x
##
y
⋅
z
;
mixin_dra_symmetric
:
Symmetric
(@
disjoint
A
_
)
;
mixin_dra_comm
x
y
:
✓
x
→
✓
y
→
x
⊥
y
→
x
⋅
y
≡
y
⋅
x
;
mixin_dra_core_disjoint_l
x
:
✓
x
→
core
x
⊥
x
;
mixin_dra_comm
x
y
:
✓
x
→
✓
y
→
x
##
y
→
x
⋅
y
≡
y
⋅
x
;
mixin_dra_core_disjoint_l
x
:
✓
x
→
core
x
##
x
;
mixin_dra_core_l
x
:
✓
x
→
core
x
⋅
x
≡
x
;
mixin_dra_core_idemp
x
:
✓
x
→
core
(
core
x
)
≡
core
x
;
mixin_dra_core_mono
x
y
:
∃
z
,
✓
x
→
✓
y
→
x
⊥
y
→
core
(
x
⋅
y
)
≡
core
x
⋅
z
∧
✓
z
∧
core
x
⊥
z
∃
z
,
✓
x
→
✓
y
→
x
##
y
→
core
(
x
⋅
y
)
≡
core
x
⋅
z
∧
✓
z
∧
core
x
##
z
}.
Structure
draT
:
=
DraT
{
dra_car
:
>
Type
;
...
...
@@ -59,30 +59,30 @@ Section dra_mixin.
Proof
.
apply
(
mixin_dra_valid_proper
_
(
dra_mixin
A
)).
Qed
.
Global
Instance
dra_disjoint_proper
x
:
Proper
((
≡
)
==>
impl
)
(
disjoint
x
).
Proof
.
apply
(
mixin_dra_disjoint_proper
_
(
dra_mixin
A
)).
Qed
.
Lemma
dra_op_valid
x
y
:
✓
x
→
✓
y
→
x
⊥
y
→
✓
(
x
⋅
y
).
Lemma
dra_op_valid
x
y
:
✓
x
→
✓
y
→
x
##
y
→
✓
(
x
⋅
y
).
Proof
.
apply
(
mixin_dra_op_valid
_
(
dra_mixin
A
)).
Qed
.
Lemma
dra_core_valid
x
:
✓
x
→
✓
core
x
.
Proof
.
apply
(
mixin_dra_core_valid
_
(
dra_mixin
A
)).
Qed
.
Lemma
dra_assoc
x
y
z
:
✓
x
→
✓
y
→
✓
z
→
x
⊥
y
→
x
⋅
y
⊥
z
→
x
⋅
(
y
⋅
z
)
≡
(
x
⋅
y
)
⋅
z
.
✓
x
→
✓
y
→
✓
z
→
x
##
y
→
x
⋅
y
##
z
→
x
⋅
(
y
⋅
z
)
≡
(
x
⋅
y
)
⋅
z
.
Proof
.
apply
(
mixin_dra_assoc
_
(
dra_mixin
A
)).
Qed
.
Lemma
dra_disjoint_ll
x
y
z
:
✓
x
→
✓
y
→
✓
z
→
x
⊥
y
→
x
⋅
y
⊥
z
→
x
⊥
z
.
Lemma
dra_disjoint_ll
x
y
z
:
✓
x
→
✓
y
→
✓
z
→
x
##
y
→
x
⋅
y
##
z
→
x
##
z
.
Proof
.
apply
(
mixin_dra_disjoint_ll
_
(
dra_mixin
A
)).
Qed
.
Lemma
dra_disjoint_move_l
x
y
z
:
✓
x
→
✓
y
→
✓
z
→
x
⊥
y
→
x
⋅
y
⊥
z
→
x
⊥
y
⋅
z
.
✓
x
→
✓
y
→
✓
z
→
x
##
y
→
x
⋅
y
##
z
→
x
##
y
⋅
z
.
Proof
.
apply
(
mixin_dra_disjoint_move_l
_
(
dra_mixin
A
)).
Qed
.
Global
Instance
dra_symmetric
:
Symmetric
(@
disjoint
A
_
).
Proof
.
apply
(
mixin_dra_symmetric
_
(
dra_mixin
A
)).
Qed
.
Lemma
dra_comm
x
y
:
✓
x
→
✓
y
→
x
⊥
y
→
x
⋅
y
≡
y
⋅
x
.
Lemma
dra_comm
x
y
:
✓
x
→
✓
y
→
x
##
y
→
x
⋅
y
≡
y
⋅
x
.
Proof
.
apply
(
mixin_dra_comm
_
(
dra_mixin
A
)).
Qed
.
Lemma
dra_core_disjoint_l
x
:
✓
x
→
core
x
⊥
x
.
Lemma
dra_core_disjoint_l
x
:
✓
x
→
core
x
##
x
.
Proof
.
apply
(
mixin_dra_core_disjoint_l
_
(
dra_mixin
A
)).
Qed
.
Lemma
dra_core_l
x
:
✓
x
→
core
x
⋅
x
≡
x
.
Proof
.
apply
(
mixin_dra_core_l
_
(
dra_mixin
A
)).
Qed
.
Lemma
dra_core_idemp
x
:
✓
x
→
core
(
core
x
)
≡
core
x
.
Proof
.
apply
(
mixin_dra_core_idemp
_
(
dra_mixin
A
)).
Qed
.
Lemma
dra_core_mono
x
y
:
∃
z
,
✓
x
→
✓
y
→
x
⊥
y
→
core
(
x
⋅
y
)
≡
core
x
⋅
z
∧
✓
z
∧
core
x
⊥
z
.
∃
z
,
✓
x
→
✓
y
→
x
##
y
→
core
(
x
⋅
y
)
≡
core
x
⋅
z
∧
✓
z
∧
core
x
##
z
.
Proof
.
apply
(
mixin_dra_core_mono
_
(
dra_mixin
A
)).
Qed
.
End
dra_mixin
.
...
...
@@ -126,16 +126,16 @@ Proof. by intros x1 x2 Hx; split; rewrite /= Hx. Qed.
Instance
:
Proper
((
≡
)
==>
(
≡
)
==>
iff
)
(
disjoint
:
relation
A
).
Proof
.
intros
x1
x2
Hx
y1
y2
Hy
;
split
.
-
by
rewrite
Hy
(
symmetry_iff
(
⊥
)
x1
)
(
symmetry_iff
(
⊥
)
x2
)
Hx
.
-
by
rewrite
-
Hy
(
symmetry_iff
(
⊥
)
x2
)
(
symmetry_iff
(
⊥
)
x1
)
-
Hx
.
-
by
rewrite
Hy
(
symmetry_iff
(
##
)
x1
)
(
symmetry_iff
(
##
)
x2
)
Hx
.
-
by
rewrite
-
Hy
(
symmetry_iff
(
##
)
x2
)
(
symmetry_iff
(
##
)
x1
)
-
Hx
.
Qed
.
Lemma
dra_disjoint_rl
a
b
c
:
✓
a
→
✓
b
→
✓
c
→
b
⊥
c
→
a
⊥
b
⋅
c
→
a
⊥
b
.
Lemma
dra_disjoint_rl
a
b
c
:
✓
a
→
✓
b
→
✓
c
→
b
##
c
→
a
##
b
⋅
c
→
a
##
b
.
Proof
.
intros
???.
rewrite
!(
symmetry_iff
_
a
).
by
apply
dra_disjoint_ll
.
Qed
.
Lemma
dra_disjoint_lr
a
b
c
:
✓
a
→
✓
b
→
✓
c
→
a
⊥
b
→
a
⋅
b
⊥
c
→
b
⊥
c
.
Lemma
dra_disjoint_lr
a
b
c
:
✓
a
→
✓
b
→
✓
c
→
a
##
b
→
a
⋅
b
##
c
→
b
##
c
.
Proof
.
intros
????.
rewrite
dra_comm
//.
by
apply
dra_disjoint_ll
.
Qed
.
Lemma
dra_disjoint_move_r
a
b
c
:
✓
a
→
✓
b
→
✓
c
→
b
⊥
c
→
a
⊥
b
⋅
c
→
a
⋅
b
⊥
c
.
✓
a
→
✓
b
→
✓
c
→
b
##
c
→
a
##
b
⋅
c
→
a
⋅
b
##
c
.
Proof
.
intros
;
symmetry
;
rewrite
dra_comm
;
eauto
using
dra_disjoint_rl
.
apply
dra_disjoint_move_l
;
auto
;
by
rewrite
dra_comm
.
...
...
@@ -150,7 +150,7 @@ Program Instance validity_pcore : PCore (validity A) := λ x,
Solve
Obligations
with
naive_solver
eauto
using
dra_core_valid
.
Program
Instance
validity_op
:
Op
(
validity
A
)
:
=
λ
x
y
,
Validity
(
validity_car
x
⋅
validity_car
y
)
(
✓
x
∧
✓
y
∧
validity_car
x
⊥
validity_car
y
)
_
.
(
✓
x
∧
✓
y
∧
validity_car
x
##
validity_car
y
)
_
.
Solve
Obligations
with
naive_solver
eauto
using
dra_op_valid
.
Definition
validity_ra_mixin
:
RAMixin
(
validity
A
).
...
...
@@ -185,14 +185,14 @@ Global Instance validity_cmra_total : CmraTotal validityR.
Proof
.
rewrite
/
CmraTotal
;
eauto
.
Qed
.
Lemma
validity_update
x
y
:
(
∀
c
,
✓
x
→
✓
c
→
validity_car
x
⊥
c
→
✓
y
∧
validity_car
y
⊥
c
)
→
x
~~>
y
.
(
∀
c
,
✓
x
→
✓
c
→
validity_car
x
##
c
→
✓
y
∧
validity_car
y
##
c
)
→
x
~~>
y
.
Proof
.
intros
Hxy
;
apply
cmra_discrete_update
=>
z
[?[??]].
split_and
!
;
try
eapply
Hxy
;
eauto
.
Qed
.
Lemma
to_validity_op
a
b
:
(
✓
(
a
⋅
b
)
→
✓
a
∧
✓
b
∧
a
⊥
b
)
→
(
✓
(
a
⋅
b
)
→
✓
a
∧
✓
b
∧
a
##
b
)
→
to_validity
(
a
⋅
b
)
≡
to_validity
a
⋅
to_validity
b
.
Proof
.
split
;
naive_solver
eauto
using
dra_op_valid
.
Qed
.
...
...
theories/algebra/gset.v
View file @
3588f204
...
...
@@ -86,7 +86,7 @@ Section gset_disj.
Instance
gset_disj_unit
:
Unit
(
gset_disj
K
)
:
=
GSet
∅
.
Instance
gset_disj_op
:
Op
(
gset_disj
K
)
:
=
λ
X
Y
,
match
X
,
Y
with
|
GSet
X
,
GSet
Y
=>
if
decide
(
X
⊥
Y
)
then
GSet
(
X
∪
Y
)
else
GSetBot
|
GSet
X
,
GSet
Y
=>
if
decide
(
X
##
Y
)
then
GSet
(
X
∪
Y
)
else
GSetBot
|
_
,
_
=>
GSetBot
end
.
Instance
gset_disj_pcore
:
PCore
(
gset_disj
K
)
:
=
λ
_
,
Some
ε
.
...
...
@@ -102,11 +102,11 @@ Section gset_disj.
-
intros
(
Z
&->&?)%
subseteq_disjoint_union_L
.
exists
(
GSet
Z
).
gset_disj_solve
.
Qed
.
Lemma
gset_disj_valid_inv_l
X
Y
:
✓
(
GSet
X
⋅
Y
)
→
∃
Y'
,
Y
=
GSet
Y'
∧
X
⊥
Y'
.
Lemma
gset_disj_valid_inv_l
X
Y
:
✓
(
GSet
X
⋅
Y
)
→
∃
Y'
,
Y
=
GSet
Y'
∧
X
##
Y'
.
Proof
.
destruct
Y
;
repeat
(
simpl
||
case_decide
)
;
by
eauto
.
Qed
.
Lemma
gset_disj_union
X
Y
:
X
⊥
Y
→
GSet
X
⋅
GSet
Y
=
GSet
(
X
∪
Y
).
Lemma
gset_disj_union
X
Y
:
X
##
Y
→
GSet
X
⋅
GSet
Y
=
GSet
(
X
∪
Y
).
Proof
.
intros
.
by
rewrite
/=
decide_True
.
Qed
.
Lemma
gset_disj_valid_op
X
Y
:
✓
(
GSet
X
⋅
GSet
Y
)
↔
X
⊥
Y
.
Lemma
gset_disj_valid_op
X
Y
:
✓
(
GSet
X
⋅
GSet
Y
)
↔
X
##
Y
.
Proof
.
simpl
.
case_decide
;
by
split
.
Qed
.
Lemma
gset_disj_ra_mixin
:
RAMixin
(
gset_disj
K
).
...
...
@@ -207,19 +207,19 @@ Section gset_disj.
Qed
.
Lemma
gset_disj_alloc_op_local_update
X
Y
Z
:
Z
⊥
X
→
(
GSet
X
,
GSet
Y
)
~l
~>
(
GSet
Z
⋅
GSet
X
,
GSet
Z
⋅
GSet
Y
).
Z
##
X
→
(
GSet
X
,
GSet
Y
)
~l
~>
(
GSet
Z
⋅
GSet
X
,
GSet
Z
⋅
GSet
Y
).
Proof
.
intros
.
apply
op_local_update_discrete
.
by
rewrite
gset_disj_valid_op
.
Qed
.
Lemma
gset_disj_alloc_local_update
X
Y
Z
:
Z
⊥
X
→
(
GSet
X
,
GSet
Y
)
~l
~>
(
GSet
(
Z
∪
X
),
GSet
(
Z
∪
Y
)).
Z
##
X
→
(
GSet
X
,
GSet
Y
)
~l
~>
(
GSet
(
Z
∪
X
),
GSet
(
Z
∪
Y
)).
Proof
.
intros
.
apply
local_update_total_valid
=>
_
_
/
gset_disj_included
?.
rewrite
-!
gset_disj_union
//
;
last
set_solver
.
auto
using
gset_disj_alloc_op_local_update
.
Qed
.
Lemma
gset_disj_alloc_empty_local_update
X
Z
:
Z
⊥
X
→
(
GSet
X
,
GSet
∅
)
~l
~>
(
GSet
(
Z
∪
X
),
GSet
Z
).
Z
##
X
→
(
GSet
X
,
GSet
∅
)
~l
~>
(
GSet
(
Z
∪
X
),
GSet
Z
).
Proof
.
intros
.
rewrite
-{
2
}(
right_id_L
_
union
Z
).
apply
gset_disj_alloc_local_update
;
set_solver
.
...
...
theories/algebra/sts.v
View file @
3588f204
...
...
@@ -27,18 +27,18 @@ Context {sts : stsT}.
(** ** Step relations *)
Inductive
step
:
relation
(
state
sts
*
tokens
sts
)
:
=
|
Step
s1
s2
T1
T2
:
prim_step
s1
s2
→
tok
s1
⊥
T1
→
tok
s2
⊥
T2
→
prim_step
s1
s2
→
tok
s1
##
T1
→
tok
s2
##
T2
→
tok
s1
∪
T1
≡
tok
s2
∪
T2
→
step
(
s1
,
T1
)
(
s2
,
T2
).
Notation
steps
:
=
(
rtc
step
).
Inductive
frame_step
(
T
:
tokens
sts
)
(
s1
s2
:
state
sts
)
:
Prop
:
=
(* Probably equivalent definition: (\mathcal{L}(s')
⊥
T) ∧ s \rightarrow s' *)
(* Probably equivalent definition: (\mathcal{L}(s')
##
T) ∧ s \rightarrow s' *)
|
Frame_step
T1
T2
:
T1
⊥
tok
s1
∪
T
→
step
(
s1
,
T1
)
(
s2
,
T2
)
→
frame_step
T
s1
s2
.
T1
##
tok
s1
∪
T
→
step
(
s1
,
T1
)
(
s2
,
T2
)
→
frame_step
T
s1
s2
.
Notation
frame_steps
T
:
=
(
rtc
(
frame_step
T
)).
(** ** Closure under frame steps *)
Record
closed
(
S
:
states
sts
)
(
T
:
tokens
sts
)
:
Prop
:
=
Closed
{
closed_disjoint
s
:
s
∈
S
→
tok
s
⊥
T
;
closed_disjoint
s
:
s
∈
S
→
tok
s
##
T
;
closed_step
s1
s2
:
s1
∈
S
→
frame_step
T
s1
s2
→
s2
∈
S
}.
Definition
up
(
s
:
state
sts
)
(
T
:
tokens
sts
)
:
states
sts
:
=
...
...
@@ -52,7 +52,7 @@ Hint Extern 50 (equiv (A:=set _) _ _) => set_solver : sts.
Hint
Extern
50
(
¬
equiv
(
A
:
=
set
_
)
_
_
)
=>
set_solver
:
sts
.
Hint
Extern
50
(
_
∈
_
)
=>
set_solver
:
sts
.
Hint
Extern
50
(
_
⊆
_
)
=>
set_solver
:
sts
.
Hint
Extern
50
(
_
⊥
_
)
=>
set_solver
:
sts
.
Hint
Extern
50
(
_
##
_
)
=>
set_solver
:
sts
.
(** ** Setoids *)
Instance
frame_step_mono
:
Proper
(
flip
(
⊆
)
==>
(=)
==>
(=)
==>
impl
)
frame_step
.
...
...
@@ -100,16 +100,16 @@ Proof.
-
apply
Hstep2
with
s3
,
Frame_step
with
T3
T4
;
auto
with
sts
.
Qed
.
Lemma
step_closed
s1
s2
T1
T2
S
Tf
:
step
(
s1
,
T1
)
(
s2
,
T2
)
→
closed
S
Tf
→
s1
∈
S
→
T1
⊥
Tf
→
s2
∈
S
∧
T2
⊥
Tf
∧
tok
s2
⊥
T2
.
step
(
s1
,
T1
)
(
s2
,
T2
)
→
closed
S
Tf
→
s1
∈
S
→
T1
##
Tf
→
s2
∈
S
∧
T2
##
Tf
∧
tok
s2
##
T2
.
Proof
.
inversion_clear
1
as
[????
HR
Hs1
Hs2
]
;
intros
[?
Hstep
]??
;
split_and
?
;
auto
.
-
eapply
Hstep
with
s1
,
Frame_step
with
T1
T2
;
auto
with
sts
.
-
set_solver
-
Hstep
Hs1
Hs2
.
Qed
.
Lemma
steps_closed
s1
s2
T1
T2
S
Tf
:
steps
(
s1
,
T1
)
(
s2
,
T2
)
→
closed
S
Tf
→
s1
∈
S
→
T1
⊥
Tf
→
tok
s1
⊥
T1
→
s2
∈
S
∧
T2
⊥
Tf
∧
tok
s2
⊥
T2
.
steps
(
s1
,
T1
)
(
s2
,
T2
)
→
closed
S
Tf
→
s1
∈
S
→
T1
##
Tf
→
tok
s1
##
T1
→
s2
∈
S
∧
T2
##
Tf
∧
tok
s2
##
T2
.
Proof
.
remember
(
s1
,
T1
)
as
sT1
eqn
:
HsT1
;
remember
(
s2
,
T2
)
as
sT2
eqn
:
HsT2
.
intros
Hsteps
;
revert
s1
T1
HsT1
s2
T2
HsT2
.
...
...
@@ -127,7 +127,7 @@ Lemma elem_of_up_set S T s : s ∈ S → s ∈ up_set S T.
Proof
.
apply
subseteq_up_set
.
Qed
.
Lemma
up_up_set
s
T
:
up
s
T
≡
up_set
{[
s
]}
T
.
Proof
.
by
rewrite
/
up_set
collection_bind_singleton
.
Qed
.
Lemma
closed_up_set
S
T
:
(
∀
s
,
s
∈
S
→
tok
s
⊥
T
)
→
closed
(
up_set
S
T
)
T
.
Lemma
closed_up_set
S
T
:
(
∀
s
,
s
∈
S
→
tok
s
##
T
)
→
closed
(
up_set
S
T
)
T
.
Proof
.
intros
HS
;
unfold
up_set
;
split
.
-
intros
s
;
rewrite
!
elem_of_bind
;
intros
(
s'
&
Hstep
&
Hs'
).
...
...
@@ -137,7 +137,7 @@ Proof.
-
intros
s1
s2
;
rewrite
/
up
;
set_unfold
;
intros
(
s
&?&?)
?
;
exists
s
.
split
;
[
eapply
rtc_r
|]
;
eauto
.
Qed
.
Lemma
closed_up
s
T
:
tok
s
⊥
T
→
closed
(
up
s
T
)
T
.
Lemma
closed_up
s
T
:
tok
s
##
T
→
closed
(
up
s
T
)
T
.
Proof
.
intros
;
rewrite
-(
collection_bind_singleton
(
λ
s
,
up
s
T
)
s
).
apply
closed_up_set
;
set_solver
.
...
...
@@ -192,7 +192,7 @@ Inductive sts_equiv : Equiv (car sts) :=
Existing
Instance
sts_equiv
.
Instance
sts_valid
:
Valid
(
car
sts
)
:
=
λ
x
,
match
x
with
|
auth
s
T
=>
tok
s
⊥
T
|
auth
s
T
=>
tok
s
##
T
|
frag
S'
T
=>
closed
S'
T
∧
∃
s
,
s
∈
S'
end
.
Instance
sts_core
:
Core
(
car
sts
)
:
=
λ
x
,
...
...
@@ -202,9 +202,9 @@ Instance sts_core : Core (car sts) := λ x,
end
.
Inductive
sts_disjoint
:
Disjoint
(
car
sts
)
:
=
|
frag_frag_disjoint
S1
S2
T1
T2
:
(
∃
s
,
s
∈
S1
∩
S2
)
→
T1
⊥
T2
→
frag
S1
T1
⊥
frag
S2
T2
|
auth_frag_disjoint
s
S
T1
T2
:
s
∈
S
→
T1
⊥
T2
→
auth
s
T1
⊥
frag
S
T2
|
frag_auth_disjoint
s
S
T1
T2
:
s
∈
S
→
T1
⊥
T2
→
frag
S
T1
⊥
auth
s
T2
.
(
∃
s
,
s
∈
S1
∩
S2
)
→
T1
##
T2
→
frag
S1
T1
##
frag
S2
T2
|
auth_frag_disjoint
s
S
T1
T2
:
s
∈
S
→
T1
##
T2
→
auth
s
T1
##
frag
S
T2
|
frag_auth_disjoint
s
S
T1
T2
:
s
∈
S
→
T1
##
T2
→
frag
S
T1
##
auth
s
T2
.
Existing
Instance
sts_disjoint
.
Instance
sts_op
:
Op
(
car
sts
)
:
=
λ
x1
x2
,
match
x1
,
x2
with
...
...
@@ -218,7 +218,7 @@ Hint Extern 50 (equiv (A:=set _) _ _) => set_solver : sts.
Hint
Extern
50
(
∃
s
:
state
sts
,
_
)
=>
set_solver
:
sts
.
Hint
Extern
50
(
_
∈
_
)
=>
set_solver
:
sts
.
Hint
Extern
50
(
_
⊆
_
)
=>
set_solver
:
sts
.
Hint
Extern
50
(
_
⊥
_
)
=>
set_solver
:
sts
.
Hint
Extern
50
(
_
##
_
)
=>
set_solver
:
sts
.
Global
Instance
auth_proper
s
:
Proper
((
≡
)
==>
(
≡
))
(@
auth
sts
s
).
Proof
.
by
constructor
.
Qed
.
...
...
@@ -304,11 +304,11 @@ Global Instance sts_frag_up_proper s : Proper ((≡) ==> (≡)) (sts_frag_up s).
Proof
.
solve_proper
.
Qed
.
(** Validity *)
Lemma
sts_auth_valid
s
T
:
✓
sts_auth
s
T
↔
tok
s
⊥
T
.
Lemma
sts_auth_valid
s
T
:
✓
sts_auth
s
T
↔
tok
s
##
T
.
Proof
.
done
.
Qed
.
Lemma
sts_frag_valid
S
T
:
✓
sts_frag
S
T
↔
closed
S
T
∧
∃
s
,
s
∈
S
.
Proof
.
done
.
Qed
.
Lemma
sts_frag_up_valid
s
T
:
✓
sts_frag_up
s
T
↔
tok
s
⊥
T
.
Lemma
sts_frag_up_valid
s
T
:
✓
sts_frag_up
s
T
↔
tok
s
##
T
.
Proof
.
split
.
-
move
=>/
sts_frag_valid
[
H
_
].
apply
H
,
elem_of_up
.
...
...
@@ -340,7 +340,7 @@ Proof.
Qed
.
Lemma
sts_op_frag
S1
S2
T1
T2
:
T1
⊥
T2
→
sts
.
closed
S1
T1
→
sts
.
closed
S2
T2
→
T1
##
T2
→
sts
.
closed
S1
T1
→
sts
.
closed
S2
T2
→
sts_frag
(
S1
∩
S2
)
(
T1
∪
T2
)
≡
sts_frag
S1
T1
⋅
sts_frag
S2
T2
.
Proof
.
intros
HT
HS1
HS2
.
rewrite
/
sts_frag
-
to_validity_op
//.
...
...
@@ -351,7 +351,7 @@ Qed.
two closures is weaker than the closure with the itnersected token
set. Also see up_op.
Lemma sts_op_frag_up s T1 T2 :
T1
⊥
T2 → sts_frag_up s (T1 ∪ T2) ≡ sts_frag_up s T1 ⋅ sts_frag_up s T2.
T1
##
T2 → sts_frag_up s (T1 ∪ T2) ≡ sts_frag_up s T1 ⋅ sts_frag_up s T2.
*)
(** Frame preserving updates *)
...
...
@@ -375,7 +375,7 @@ Proof.
Qed
.
Lemma
sts_update_frag_up
s1
S2
T1
T2
:
(
tok
s1
⊥
T1
→
closed
S2
T2
)
→
s1
∈
S2
→
T2
⊆
T1
→
sts_frag_up
s1
T1
~~>
sts_frag
S2
T2
.
(
tok
s1
##
T1
→
closed
S2
T2
)
→
s1
∈
S2
→
T2
⊆
T1
→
sts_frag_up
s1
T1
~~>
sts_frag
S2
T2
.
Proof
.
intros
HC
?
HT
;
apply
sts_update_frag
.
intros
HC1
;
split
;
last
split
;
eauto
using
closed_steps
.
-
eapply
HC
,
HC1
,
elem_of_up
.
...
...
@@ -405,7 +405,7 @@ Qed.
Lemma sts_frag_included S1 S2 T1 T2 :
closed S2 T2 → S2 ≢ ∅ →
(sts_frag S1 T1 ≼ sts_frag S2 T2) ↔
(closed S1 T1 ∧ S1 ≢ ∅ ∧ ∃ Tf, T2 ≡ T1 ∪ Tf ∧ T1
⊥
Tf ∧
(closed S1 T1 ∧ S1 ≢ ∅ ∧ ∃ Tf, T2 ≡ T1 ∪ Tf ∧ T1
##
Tf ∧
S2 ≡ S1 ∩ up_set S2 Tf).
Proof.
intros ??; split.
...
...
theories/base_logic/big_op.v
View file @
3588f204
...
...
@@ -415,7 +415,7 @@ Section gset.
Proof
.
apply
big_opS_fn_insert'
.
Qed
.
Lemma
big_sepS_union
Φ
X
Y
:
X
⊥
Y
→
X
##
Y
→
([
∗
set
]
y
∈
X
∪
Y
,
Φ
y
)
⊣
⊢
([
∗
set
]
y
∈
X
,
Φ
y
)
∗
([
∗
set
]
y
∈
Y
,
Φ
y
).
Proof
.
apply
big_opS_union
.
Qed
.
...
...
theories/base_logic/deprecated.v
View file @
3588f204
...
...
@@ -8,5 +8,5 @@ Notation "■ φ" := (uPred_pure φ%C%type)
(* Deprecated 2016-11-22. Use ⌜x = y⌝ instead. *)
Notation
"x = y"
:
=
(
uPred_pure
(
x
%
C
%
type
=
y
%
C
%
type
))
(
only
parsing
)
:
uPred_scope
.
(* Deprecated 2016-11-22. Use ⌜x
⊥
y ⌝ instead. *)
Notation
"x
⊥
y"
:
=
(
uPred_pure
(
x
%
C
%
type
⊥
y
%
C
%
type
))
(
only
parsing
)
:
uPred_scope
.
(* Deprecated 2016-11-22. Use ⌜x
##
y ⌝ instead. *)
Notation
"x
##
y"
:
=
(
uPred_pure
(
x
%
C
%
type
##
y
%
C
%
type
))
(
only
parsing
)
:
uPred_scope
.
theories/base_logic/lib/counter_examples.v
View file @
3588f204
...
...
@@ -79,7 +79,7 @@ Module inv. Section inv.
* Using the STS monoid of a two-state STS, where [start] is the
authoritative saying the state is exactly [start], and [finish]
is the "we are at least in state [finish]" typically owned by threads.
* Ex () +_
⊥
()
* Ex () +_
##
()
*)
Context
(
gname
:
Type
).
Context
(
start
finished
:
gname
→
iProp
).
...
...
theories/base_logic/lib/fancy_updates.v
View file @
3588f204
...
...
@@ -70,7 +70,7 @@ Proof.
Qed
.
Lemma
fupd_mask_frame_r'
E1
E2
Ef
P
:
E1
⊥
Ef
→
(|={
E1
,
E2
}=>
⌜
E2
⊥
Ef
⌝
→
P
)
={
E1
∪
Ef
,
E2
∪
Ef
}=
∗
P
.
E1
##
Ef
→
(|={
E1
,
E2
}=>
⌜
E2
##
Ef
⌝
→
P
)
={
E1
∪
Ef
,
E2
∪
Ef
}=
∗
P
.
Proof
.
intros
.
rewrite
fupd_eq
/
fupd_def
ownE_op
//.
iIntros
"Hvs (Hw & HE1 &HEf)"
.
iMod
(
"Hvs"
with
"[Hw HE1]"
)
as
">($ & HE2 & HP)"
;
first
by
iFrame
.
...
...
@@ -110,7 +110,7 @@ Proof.
Qed
.
Lemma
fupd_mask_frame_r
E1
E2
Ef
P
:
E1
⊥
Ef
→
(|={
E1
,
E2
}=>
P
)
={
E1
∪
Ef
,
E2
∪
Ef
}=
∗
P
.
E1
##
Ef
→
(|={
E1
,
E2
}=>
P
)
={
E1
∪
Ef
,
E2
∪
Ef
}=
∗
P
.
Proof
.
iIntros
(?)
"H"
.
iApply
fupd_mask_frame_r'
;
auto
.
iApply
fupd_wand_r
;
iFrame
"H"
;
eauto
.
...
...
@@ -222,7 +222,7 @@ Lemma step_fupd_wand E1 E2 P Q : (|={E1,E2}▷=> P) -∗ (P -∗ Q) -∗ |={E1,E
Proof
.
iIntros
"HP HPQ"
.
by
iApply
"HPQ"
.
Qed
.
Lemma
step_fupd_mask_frame_r
E1
E2
Ef
P
:
E1
⊥
Ef
→
E2
⊥
Ef
→
(|={
E1
,
E2
}
▷
=>
P
)
⊢
|={
E1
∪
Ef
,
E2
∪
Ef
}
▷
=>
P
.
E1
##
Ef
→
E2
##
Ef
→
(|={
E1
,
E2
}
▷
=>
P
)
⊢
|={
E1
∪
Ef
,
E2
∪
Ef
}
▷
=>
P
.
Proof
.
iIntros
(??)
"HP"
.
iApply
fupd_mask_frame_r
.
done
.
iMod
"HP"
.
iModIntro
.
iNext
.
by
iApply
fupd_mask_frame_r
.
...
...
theories/base_logic/lib/fancy_updates_from_vs.v
View file @
3588f204
...
...
@@ -19,7 +19,7 @@ Context (vs_impl : ∀ E P Q, □ (P → Q) ⊢ P ={E,E}=> Q).
Context
(
vs_transitive
:
∀
E1
E2
E3
P
Q
R
,
(
P
={
E1
,
E2
}=>
Q
)
∧
(
Q
={
E2
,
E3
}=>
R
)
⊢
P
={
E1
,
E3
}=>
R
).
Context
(
vs_mask_frame_r
:
∀
E1
E2
Ef
P
Q
,
E1
⊥
Ef
→
(
P
={
E1
,
E2
}=>
Q
)
⊢
P
={
E1
∪
Ef
,
E2
∪
Ef
}=>
Q
).
E1
##
Ef
→
(
P
={
E1
,
E2
}=>
Q
)
⊢
P
={
E1
∪
Ef
,
E2
∪
Ef
}=>
Q
).
Context
(
vs_frame_r
:
∀
E1
E2
P
Q
R
,
(
P
={
E1
,
E2
}=>
Q
)
⊢
P
∗
R
={
E1
,
E2
}=>
Q
∗
R
).
Context
(
vs_exists
:
∀
{
A
}
E1
E2
(
Φ
:
A
→
uPred
M
)
Q
,
(
∀
x
,
Φ
x
={
E1
,
E2
}=>
Q
)
⊢
(
∃
x
,
Φ
x
)
={
E1
,
E2
}=>
Q
).
...
...
@@ -56,7 +56,7 @@ Proof.
Qed
.
Lemma
fupd_mask_frame_r
E1
E2
Ef
P
:
E1
⊥
Ef
→
(|={
E1
,
E2
}=>
P
)
⊢
|={
E1
∪
Ef
,
E2
∪
Ef
}=>
P
.
E1
##
Ef
→
(|={
E1
,
E2
}=>
P
)
⊢
|={
E1
∪
Ef
,
E2
∪
Ef
}=>
P
.
Proof
.
iIntros
(
HE
)
;
iDestruct
1
as
(
R
)
"[HR Hvs]"
.
iExists
R
;
iFrame
"HR"
.
by
iApply
vs_mask_frame_r
.
...
...
theories/base_logic/lib/na_invariants.v
View file @
3588f204
...
...
@@ -46,14 +46,14 @@ Section proofs.
Lemma
na_alloc
:
(|==>
∃
p
,
na_own
p
⊤
)%
I
.
Proof
.
by
apply
own_alloc
.
Qed
.
Lemma
na_own_disjoint
p
E1
E2
:
na_own
p
E1
-
∗
na_own
p
E2
-
∗
⌜
E1
⊥
E2
⌝
.
Lemma
na_own_disjoint
p
E1
E2
:
na_own
p
E1
-
∗
na_own
p
E2
-
∗
⌜
E1
##
E2
⌝
.
Proof
.
apply
wand_intro_r
.
rewrite
/
na_own
-
own_op
own_valid
-
coPset_disj_valid_op
.
by
iIntros
([?
_
]).
Qed
.
Lemma
na_own_union
p
E1
E2
:
E1
⊥
E2
→
na_own
p
(
E1
∪
E2
)
⊣
⊢
na_own
p
E1
∗
na_own
p
E2
.
E1
##
E2
→
na_own
p
(
E1
∪
E2
)
⊣
⊢
na_own
p
E1
∗
na_own
p
E2
.
Proof
.
intros
?.
by
rewrite
/
na_own
-
own_op
pair_op
left_id
coPset_disj_union
.
Qed
.
...
...
theories/base_logic/lib/namespaces.v
View file @
3588f204
...
...
@@ -24,7 +24,7 @@ Notation "N .@ x" := (ndot N x)
(
at
level
19
,
left
associativity
,
format
"N .@ x"
)
:
C_scope
.
Notation
"(.@)"
:
=
ndot
(
only
parsing
)
:
C_scope
.
Instance
ndisjoint
:
Disjoint
namespace
:
=
λ
N1
N2
,
nclose
N1
⊥
nclose
N2
.
Instance
ndisjoint
:
Disjoint
namespace
:
=
λ
N1
N2
,
nclose
N1
##
nclose
N2
.
Section
namespace
.
Context
`
{
Countable
A
}.
...
...
@@ -59,37 +59,37 @@ Section namespace.
Lemma
nclose_infinite
N
:
¬
set_finite
(
↑
N
:
coPset
).
Proof
.
rewrite
nclose_eq
.
apply
coPset_suffixes_infinite
.
Qed
.
Lemma
ndot_ne_disjoint
N
x
y
:
x
≠
y
→
N
.@
x
⊥
N
.@
y
.
Lemma
ndot_ne_disjoint
N
x
y
:
x
≠
y
→
N
.@
x
##
N
.@
y
.
Proof
.
intros
Hxy
a
.
rewrite
!
nclose_eq
!
elem_coPset_suffixes
!
ndot_eq
.
intros
[
qx
->]
[
qy
Hqy
].
revert
Hqy
.
by
intros
[=
?%
encode_inj
]%
list_encode_suffix_eq
.
Qed
.
Lemma
ndot_preserve_disjoint_l
N
E
x
:
↑
N
⊥
E
→
↑
N
.@
x
⊥
E
.
Lemma
ndot_preserve_disjoint_l
N
E
x
:
↑
N
##
E
→
↑
N
.@
x
##
E
.
Proof
.
intros
.
pose
proof
(
nclose_subseteq
N
x
).
set_solver
.
Qed
.
Lemma
ndot_preserve_disjoint_r
N
E
x
:
E
⊥
↑
N
→
E
⊥
↑
N
.@
x
.
Lemma
ndot_preserve_disjoint_r
N
E
x
:
E
##
↑
N
→
E
##
↑
N
.@
x
.
Proof
.
intros
.
by
apply
symmetry
,
ndot_preserve_disjoint_l
.
Qed
.
Lemma
ndisj_subseteq_difference
N
E
F
:
E
⊥
↑
N
→
E
⊆
F
→
E
⊆
F
∖
↑
N
.
Lemma
ndisj_subseteq_difference
N
E
F
:
E
##
↑
N
→
E
⊆
F
→
E
⊆
F
∖
↑
N
.
Proof
.
set_solver
.
Qed
.
Lemma
namespace_subseteq_difference_l
E1
E2
E3
:
E1
⊆
E3
→
E1
∖
E2
⊆
E3
.
Proof
.
set_solver
.
Qed
.
Lemma
ndisj_difference_l
E
N1
N2
:
↑
N2
⊆
(
↑
N1
:
coPset
)
→
E
∖
↑
N1
⊥
↑
N2
.
Lemma
ndisj_difference_l
E
N1
N2
:
↑
N2
⊆
(
↑
N1
:
coPset
)
→
E
∖
↑
N1
##
↑
N2
.
Proof
.
set_solver
.
Qed
.
End
namespace
.
(* The hope is that registering these will suffice to solve most goals
of the forms:
- [N1
⊥
N2]
- [N1
##
N2]
- [↑N1 ⊆ E ∖ ↑N2 ∖ .. ∖ ↑Nn]
- [E1 ∖ ↑N1 ⊆ E2 ∖ ↑N2 ∖ .. ∖ ↑Nn] *)
Create
HintDb
ndisj
.
Hint
Resolve
ndisj_subseteq_difference
:
ndisj
.
Hint
Extern
0
(
_
⊥
_
)
=>
apply
ndot_ne_disjoint
;
congruence
:
ndisj
.
Hint
Extern
0
(
_
##
_
)
=>
apply
ndot_ne_disjoint
;
congruence
:
ndisj
.
Hint
Resolve
ndot_preserve_disjoint_l
ndot_preserve_disjoint_r
:
ndisj
.
Hint
Resolve
nclose_subseteq'
ndisj_difference_l
:
ndisj
.
Hint
Resolve
namespace_subseteq_difference_l
|
100
: