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
b51af294
Commit
b51af294
authored
Sep 17, 2017
by
Robbert Krebbers
Browse files
Use ε for CMRA unit.
For obsolete reasons, that no longer seem to apply, we used ∅ as the unit.
parent
391e52d7
Changes
19
Hide whitespace changes
Inline
Side-by-side
theories/algebra/auth.v
View file @
b51af294
...
...
@@ -12,7 +12,7 @@ Instance: Params (@Auth) 1.
Instance
:
Params
(@
authoritative
)
1
.
Instance
:
Params
(@
auth_own
)
1
.
Notation
"◯ a"
:
=
(
Auth
None
a
)
(
at
level
20
).
Notation
"● a"
:
=
(
Auth
(
Excl'
a
)
∅
)
(
at
level
20
).
Notation
"● a"
:
=
(
Auth
(
Excl'
a
)
ε
)
(
at
level
20
).
(* COFE *)
Section
cofe
.
...
...
@@ -177,7 +177,7 @@ Proof.
-
by
rewrite
-
cmra_discrete_valid_iff
.
Qed
.
Instance
auth_empty
:
Empty
(
auth
A
)
:
=
Auth
∅
∅
.
Instance
auth_empty
:
Unit
(
auth
A
)
:
=
Auth
ε
ε
.
Lemma
auth_ucmra_mixin
:
UCMRAMixin
(
auth
A
).
Proof
.
split
;
simpl
.
...
...
@@ -226,9 +226,9 @@ Proof.
split
;
last
done
.
exists
bf2
.
by
rewrite
-
assoc
.
Qed
.
Lemma
auth_update_alloc
a
a'
b'
:
(
a
,
∅
)
~l
~>
(
a'
,
b'
)
→
●
a
~~>
●
a'
⋅
◯
b'
.
Lemma
auth_update_alloc
a
a'
b'
:
(
a
,
ε
)
~l
~>
(
a'
,
b'
)
→
●
a
~~>
●
a'
⋅
◯
b'
.
Proof
.
intros
.
rewrite
-(
right_id
_
_
(
●
a
)).
by
apply
auth_update
.
Qed
.
Lemma
auth_update_dealloc
a
b
a'
:
(
a
,
b
)
~l
~>
(
a'
,
∅
)
→
●
a
⋅
◯
b
~~>
●
a'
.
Lemma
auth_update_dealloc
a
b
a'
:
(
a
,
b
)
~l
~>
(
a'
,
ε
)
→
●
a
⋅
◯
b
~~>
●
a'
.
Proof
.
intros
.
rewrite
-(
right_id
_
_
(
●
a'
)).
by
apply
auth_update
.
Qed
.
Lemma
auth_local_update
(
a
b0
b1
a'
b0'
b1'
:
A
)
:
...
...
theories/algebra/cmra.v
View file @
b51af294
...
...
@@ -179,12 +179,13 @@ Instance core' `{PCore A} : Core A := λ x, from_option id x (pcore x).
Arguments
core'
_
_
_
/.
(** * CMRAs with a unit element *)
(** We use the notation ∅ because for most instances (maps, sets, etc) the
`empty' element is the unit. *)
Record
UCMRAMixin
A
`
{
Dist
A
,
Equiv
A
,
PCore
A
,
Op
A
,
Valid
A
,
Empty
A
}
:
=
{
mixin_ucmra_unit_valid
:
✓
∅
;
mixin_ucmra_unit_left_id
:
LeftId
(
≡
)
∅
(
⋅
)
;
mixin_ucmra_pcore_unit
:
pcore
∅
≡
Some
∅
Class
Unit
(
A
:
Type
)
:
=
ε
:
A
.
Arguments
ε
{
_
_
}.
Record
UCMRAMixin
A
`
{
Dist
A
,
Equiv
A
,
PCore
A
,
Op
A
,
Valid
A
,
Unit
A
}
:
=
{
mixin_ucmra_unit_valid
:
✓
ε
;
mixin_ucmra_unit_left_id
:
LeftId
(
≡
)
ε
(
⋅
)
;
mixin_ucmra_pcore_unit
:
pcore
ε
≡
Some
ε
}.
Structure
ucmraT
:
=
UCMRAT'
{
...
...
@@ -195,7 +196,7 @@ Structure ucmraT := UCMRAT' {
ucmra_op
:
Op
ucmra_car
;
ucmra_valid
:
Valid
ucmra_car
;
ucmra_validN
:
ValidN
ucmra_car
;
ucmra_
empty
:
Empty
ucmra_car
;
ucmra_
unit
:
Unit
ucmra_car
;
ucmra_ofe_mixin
:
OfeMixin
ucmra_car
;
ucmra_cmra_mixin
:
CMRAMixin
ucmra_car
;
ucmra_mixin
:
UCMRAMixin
ucmra_car
;
...
...
@@ -215,7 +216,7 @@ Arguments ucmra_ofe_mixin : simpl never.
Arguments
ucmra_cmra_mixin
:
simpl
never
.
Arguments
ucmra_mixin
:
simpl
never
.
Add
Printing
Constructor
ucmraT
.
Hint
Extern
0
(
Empty
_
)
=>
eapply
(@
ucmra_
empty
_
)
:
typeclass_instances
.
Hint
Extern
0
(
Unit
_
)
=>
eapply
(@
ucmra_
unit
_
)
:
typeclass_instances
.
Coercion
ucmra_ofeC
(
A
:
ucmraT
)
:
ofeT
:
=
OfeT
A
(
ucmra_ofe_mixin
A
).
Canonical
Structure
ucmra_ofeC
.
Coercion
ucmra_cmraR
(
A
:
ucmraT
)
:
cmraT
:
=
...
...
@@ -226,11 +227,11 @@ Canonical Structure ucmra_cmraR.
Section
ucmra_mixin
.
Context
{
A
:
ucmraT
}.
Implicit
Types
x
y
:
A
.
Lemma
ucmra_unit_valid
:
✓
(
∅
:
A
).
Lemma
ucmra_unit_valid
:
✓
(
ε
:
A
).
Proof
.
apply
(
mixin_ucmra_unit_valid
_
(
ucmra_mixin
A
)).
Qed
.
Global
Instance
ucmra_unit_left_id
:
LeftId
(
≡
)
∅
(@
op
A
_
).
Global
Instance
ucmra_unit_left_id
:
LeftId
(
≡
)
ε
(@
op
A
_
).
Proof
.
apply
(
mixin_ucmra_unit_left_id
_
(
ucmra_mixin
A
)).
Qed
.
Lemma
ucmra_pcore_unit
:
pcore
(
∅
:
A
)
≡
Some
∅
.
Lemma
ucmra_pcore_unit
:
pcore
(
ε
:
A
)
≡
Some
ε
.
Proof
.
apply
(
mixin_ucmra_pcore_unit
_
(
ucmra_mixin
A
)).
Qed
.
End
ucmra_mixin
.
...
...
@@ -610,27 +611,27 @@ Section ucmra.
Context
{
A
:
ucmraT
}.
Implicit
Types
x
y
z
:
A
.
Lemma
ucmra_unit_validN
n
:
✓
{
n
}
(
∅
:
A
).
Lemma
ucmra_unit_validN
n
:
✓
{
n
}
(
ε
:
A
).
Proof
.
apply
cmra_valid_validN
,
ucmra_unit_valid
.
Qed
.
Lemma
ucmra_unit_leastN
n
x
:
∅
≼
{
n
}
x
.
Lemma
ucmra_unit_leastN
n
x
:
ε
≼
{
n
}
x
.
Proof
.
by
exists
x
;
rewrite
left_id
.
Qed
.
Lemma
ucmra_unit_least
x
:
∅
≼
x
.
Lemma
ucmra_unit_least
x
:
ε
≼
x
.
Proof
.
by
exists
x
;
rewrite
left_id
.
Qed
.
Global
Instance
ucmra_unit_right_id
:
RightId
(
≡
)
∅
(@
op
A
_
).
Global
Instance
ucmra_unit_right_id
:
RightId
(
≡
)
ε
(@
op
A
_
).
Proof
.
by
intros
x
;
rewrite
(
comm
op
)
left_id
.
Qed
.
Global
Instance
ucmra_unit_persistent
:
Persistent
(
∅
:
A
).
Global
Instance
ucmra_unit_persistent
:
Persistent
(
ε
:
A
).
Proof
.
apply
ucmra_pcore_unit
.
Qed
.
Global
Instance
cmra_unit_total
:
CMRATotal
A
.
Proof
.
intros
x
.
destruct
(
cmra_pcore_mono'
∅
x
∅
)
as
(
cx
&->&?)
;
eauto
using
ucmra_unit_least
,
(
persistent
(
∅
:
A
)).
intros
x
.
destruct
(
cmra_pcore_mono'
ε
x
ε
)
as
(
cx
&->&?)
;
eauto
using
ucmra_unit_least
,
(
persistent
(
ε
:
A
)).
Qed
.
Global
Instance
empty_cancelable
:
Cancelable
(
∅
:
A
).
Global
Instance
empty_cancelable
:
Cancelable
(
ε
:
A
).
Proof
.
intros
???.
by
rewrite
!
left_id
.
Qed
.
(* For big ops *)
Global
Instance
cmra_monoid
:
Monoid
(@
op
A
_
)
:
=
{|
monoid_unit
:
=
∅
|}.
Global
Instance
cmra_monoid
:
Monoid
(@
op
A
_
)
:
=
{|
monoid_unit
:
=
ε
|}.
End
ucmra
.
Hint
Immediate
cmra_unit_total
.
...
...
@@ -688,9 +689,9 @@ Section ucmra_leibniz.
Context
{
A
:
ucmraT
}
`
{!
LeibnizEquiv
A
}.
Implicit
Types
x
y
z
:
A
.
Global
Instance
ucmra_unit_left_id_L
:
LeftId
(=)
∅
(@
op
A
_
).
Global
Instance
ucmra_unit_left_id_L
:
LeftId
(=)
ε
(@
op
A
_
).
Proof
.
intros
x
.
unfold_leibniz
.
by
rewrite
left_id
.
Qed
.
Global
Instance
ucmra_unit_right_id_L
:
RightId
(=)
∅
(@
op
A
_
).
Global
Instance
ucmra_unit_right_id_L
:
RightId
(=)
ε
(@
op
A
_
).
Proof
.
intros
x
.
unfold_leibniz
.
by
rewrite
right_id
.
Qed
.
End
ucmra_leibniz
.
...
...
@@ -925,7 +926,7 @@ Section unit.
Proof
.
apply
discrete_cmra_mixin
,
ra_total_mixin
;
by
eauto
.
Qed
.
Canonical
Structure
unitR
:
cmraT
:
=
CMRAT
unit
unit_cmra_mixin
.
Instance
unit_
empty
:
Empty
()
:
=
().
Instance
unit_
unit
:
Unit
()
:
=
().
Lemma
unit_ucmra_mixin
:
UCMRAMixin
().
Proof
.
done
.
Qed
.
Canonical
Structure
unitUR
:
ucmraT
:
=
UCMRAT
unit
unit_ucmra_mixin
.
...
...
@@ -960,7 +961,7 @@ Section nat.
Global
Instance
nat_cmra_discrete
:
CMRADiscrete
natR
.
Proof
.
apply
discrete_cmra_discrete
.
Qed
.
Instance
nat_
empty
:
Empty
nat
:
=
0
.
Instance
nat_
unit
:
Unit
nat
:
=
0
.
Lemma
nat_ucmra_mixin
:
UCMRAMixin
nat
.
Proof
.
split
;
apply
_
||
done
.
Qed
.
Canonical
Structure
natUR
:
ucmraT
:
=
UCMRAT
nat
nat_ucmra_mixin
.
...
...
@@ -972,6 +973,7 @@ End nat.
Definition
mnat
:
=
nat
.
Section
mnat
.
Instance
mnat_unit
:
Unit
mnat
:
=
0
.
Instance
mnat_valid
:
Valid
mnat
:
=
λ
x
,
True
.
Instance
mnat_validN
:
ValidN
mnat
:
=
λ
n
x
,
True
.
Instance
mnat_pcore
:
PCore
mnat
:
=
Some
.
...
...
@@ -997,7 +999,6 @@ Section mnat.
Global
Instance
mnat_cmra_discrete
:
CMRADiscrete
mnatR
.
Proof
.
apply
discrete_cmra_discrete
.
Qed
.
Instance
mnat_empty
:
Empty
mnat
:
=
0
.
Lemma
mnat_ucmra_mixin
:
UCMRAMixin
mnat
.
Proof
.
split
;
apply
_
||
done
.
Qed
.
Canonical
Structure
mnatUR
:
ucmraT
:
=
UCMRAT
mnat
mnat_ucmra_mixin
.
...
...
@@ -1140,7 +1141,7 @@ Arguments prodR : clear implicits.
Section
prod_unit
.
Context
{
A
B
:
ucmraT
}.
Instance
prod_
empty
`
{
Empty
A
,
Empty
B
}
:
Empty
(
A
*
B
)
:
=
(
∅
,
∅
).
Instance
prod_
unit
`
{
Unit
A
,
Unit
B
}
:
Unit
(
A
*
B
)
:
=
(
ε
,
ε
).
Lemma
prod_ucmra_mixin
:
UCMRAMixin
(
A
*
B
).
Proof
.
split
.
...
...
@@ -1150,11 +1151,11 @@ Section prod_unit.
Qed
.
Canonical
Structure
prodUR
:
=
UCMRAT
(
prod
A
B
)
prod_ucmra_mixin
.
Lemma
pair_split
(
x
:
A
)
(
y
:
B
)
:
(
x
,
y
)
≡
(
x
,
∅
)
⋅
(
∅
,
y
).
Lemma
pair_split
(
x
:
A
)
(
y
:
B
)
:
(
x
,
y
)
≡
(
x
,
ε
)
⋅
(
ε
,
y
).
Proof
.
by
rewrite
pair_op
left_id
right_id
.
Qed
.
Lemma
pair_split_L
`
{!
LeibnizEquiv
A
,
!
LeibnizEquiv
B
}
(
x
:
A
)
(
y
:
B
)
:
(
x
,
y
)
=
(
x
,
∅
)
⋅
(
∅
,
y
).
(
x
,
y
)
=
(
x
,
ε
)
⋅
(
ε
,
y
).
Proof
.
unfold_leibniz
.
apply
pair_split
.
Qed
.
End
prod_unit
.
...
...
@@ -1311,7 +1312,7 @@ Section option.
Global
Instance
option_cmra_discrete
:
CMRADiscrete
A
→
CMRADiscrete
optionR
.
Proof
.
split
;
[
apply
_
|].
by
intros
[
x
|]
;
[
apply
(
cmra_discrete_valid
x
)|].
Qed
.
Instance
option_
empty
:
Empty
(
option
A
)
:
=
None
.
Instance
option_
unit
:
Unit
(
option
A
)
:
=
None
.
Lemma
option_ucmra_mixin
:
UCMRAMixin
optionR
.
Proof
.
split
.
done
.
by
intros
[].
done
.
Qed
.
Canonical
Structure
optionUR
:
=
UCMRAT
(
option
A
)
option_ucmra_mixin
.
...
...
theories/algebra/coPset.v
View file @
b51af294
...
...
@@ -12,6 +12,7 @@ Section coPset.
Canonical
Structure
coPsetC
:
=
discreteC
coPset
.
Instance
coPset_valid
:
Valid
coPset
:
=
λ
_
,
True
.
Instance
coPset_unit
:
Unit
coPset
:
=
(
∅
:
coPset
).
Instance
coPset_op
:
Op
coPset
:
=
union
.
Instance
coPset_pcore
:
PCore
coPset
:
=
Some
.
...
...
@@ -70,13 +71,13 @@ Section coPset_disj.
Instance
coPset_disj_valid
:
Valid
coPset_disj
:
=
λ
X
,
match
X
with
CoPset
_
=>
True
|
CoPsetBot
=>
False
end
.
Instance
coPset_disj_
empty
:
Empty
coPset_disj
:
=
CoPset
∅
.
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
|
_
,
_
=>
CoPsetBot
end
.
Instance
coPset_disj_pcore
:
PCore
coPset_disj
:
=
λ
_
,
Some
∅
.
Instance
coPset_disj_pcore
:
PCore
coPset_disj
:
=
λ
_
,
Some
ε
.
Ltac
coPset_disj_solve
:
=
repeat
(
simpl
||
case_decide
)
;
...
...
theories/algebra/gmap.v
View file @
b51af294
...
...
@@ -100,6 +100,7 @@ Section cmra.
Context
`
{
Countable
K
}
{
A
:
cmraT
}.
Implicit
Types
m
:
gmap
K
A
.
Instance
gmap_unit
:
Unit
(
gmap
K
A
)
:
=
(
∅
:
gmap
K
A
).
Instance
gmap_op
:
Op
(
gmap
K
A
)
:
=
merge
op
.
Instance
gmap_pcore
:
PCore
(
gmap
K
A
)
:
=
λ
m
,
Some
(
omap
pcore
m
).
Instance
gmap_valid
:
Valid
(
gmap
K
A
)
:
=
λ
m
,
∀
i
,
✓
(
m
!!
i
).
...
...
@@ -218,8 +219,9 @@ Lemma insert_valid m i x : ✓ x → ✓ m → ✓ <[i:=x]>m.
Proof
.
by
intros
??
j
;
destruct
(
decide
(
i
=
j
))
;
simplify_map_eq
.
Qed
.
Lemma
singleton_validN
n
i
x
:
✓
{
n
}
({[
i
:
=
x
]}
:
gmap
K
A
)
↔
✓
{
n
}
x
.
Proof
.
split
;
[|
by
intros
;
apply
insert_validN
,
ucmra_unit_validN
].
by
move
=>/(
_
i
)
;
simplify_map_eq
.
split
.
-
move
=>/(
_
i
)
;
by
simplify_map_eq
.
-
intros
.
apply
insert_validN
.
done
.
apply
:
ucmra_unit_validN
.
Qed
.
Lemma
singleton_valid
i
x
:
✓
({[
i
:
=
x
]}
:
gmap
K
A
)
↔
✓
x
.
Proof
.
rewrite
!
cmra_valid_validN
.
by
setoid_rewrite
singleton_validN
.
Qed
.
...
...
theories/algebra/gset.v
View file @
b51af294
...
...
@@ -11,6 +11,7 @@ Section gset.
Canonical
Structure
gsetC
:
=
discreteC
(
gset
K
).
Instance
gset_valid
:
Valid
(
gset
K
)
:
=
λ
_
,
True
.
Instance
gset_unit
:
Unit
(
gset
K
)
:
=
(
∅
:
gset
K
).
Instance
gset_op
:
Op
(
gset
K
)
:
=
union
.
Instance
gset_pcore
:
PCore
(
gset
K
)
:
=
λ
X
,
Some
X
.
...
...
@@ -82,13 +83,13 @@ Section gset_disj.
Instance
gset_disj_valid
:
Valid
(
gset_disj
K
)
:
=
λ
X
,
match
X
with
GSet
_
=>
True
|
GSetBot
=>
False
end
.
Instance
gset_disj_
empty
:
Empty
(
gset_disj
K
)
:
=
GSet
∅
.
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
|
_
,
_
=>
GSetBot
end
.
Instance
gset_disj_pcore
:
PCore
(
gset_disj
K
)
:
=
λ
_
,
Some
∅
.
Instance
gset_disj_pcore
:
PCore
(
gset_disj
K
)
:
=
λ
_
,
Some
ε
.
Ltac
gset_disj_solve
:
=
repeat
(
simpl
||
case_decide
)
;
...
...
@@ -183,7 +184,7 @@ Section gset_disj.
End
fresh_updates
.
Lemma
gset_disj_dealloc_local_update
X
Y
:
(
GSet
X
,
GSet
Y
)
~l
~>
(
GSet
(
X
∖
Y
),
∅
).
(
GSet
X
,
GSet
Y
)
~l
~>
(
GSet
(
X
∖
Y
),
GSet
∅
).
Proof
.
apply
local_update_total_valid
=>
_
_
/
gset_disj_included
HYX
.
rewrite
local_update_unital_discrete
=>
-[
Xf
|]
_
/
leibniz_equiv_iff
//=.
...
...
@@ -192,7 +193,7 @@ Section gset_disj.
difference_diag_L
!
left_id_L
difference_disjoint_L
.
Qed
.
Lemma
gset_disj_dealloc_empty_local_update
X
Z
:
(
GSet
Z
⋅
GSet
X
,
GSet
Z
)
~l
~>
(
GSet
X
,
∅
).
(
GSet
Z
⋅
GSet
X
,
GSet
Z
)
~l
~>
(
GSet
X
,
GSet
∅
).
Proof
.
apply
local_update_total_valid
=>
/
gset_disj_valid_op
HZX
_
_
.
assert
(
X
=
(
Z
∪
X
)
∖
Z
)
as
HX
by
set_solver
.
...
...
@@ -201,7 +202,7 @@ Section gset_disj.
Lemma
gset_disj_dealloc_op_local_update
X
Y
Z
:
(
GSet
Z
⋅
GSet
X
,
GSet
Z
⋅
GSet
Y
)
~l
~>
(
GSet
X
,
GSet
Y
).
Proof
.
rewrite
-{
2
}(
left_id
∅
_
(
GSet
Y
)).
rewrite
-{
2
}(
left_id
ε
_
(
GSet
Y
)).
apply
op_local_update_frame
,
gset_disj_dealloc_empty_local_update
.
Qed
.
...
...
theories/algebra/iprod.v
View file @
b51af294
...
...
@@ -128,8 +128,8 @@ Section iprod_cmra.
Qed
.
Canonical
Structure
iprodR
:
=
CMRAT
(
iprod
B
)
iprod_cmra_mixin
.
Instance
iprod_
empty
:
Empty
(
iprod
B
)
:
=
λ
x
,
∅
.
Definition
iprod_lookup_empty
x
:
∅
x
=
∅
:
=
eq_refl
.
Instance
iprod_
unit
:
Unit
(
iprod
B
)
:
=
λ
x
,
ε
.
Definition
iprod_lookup_empty
x
:
ε
x
=
ε
:
=
eq_refl
.
Lemma
iprod_ucmra_mixin
:
UCMRAMixin
(
iprod
B
).
Proof
.
...
...
@@ -141,7 +141,7 @@ Section iprod_cmra.
Canonical
Structure
iprodUR
:
=
UCMRAT
(
iprod
B
)
iprod_ucmra_mixin
.
Global
Instance
iprod_empty_timeless
:
(
∀
i
,
Timeless
(
∅
:
B
i
))
→
Timeless
(
∅
:
iprod
B
).
(
∀
i
,
Timeless
(
ε
:
B
i
))
→
Timeless
(
ε
:
iprod
B
).
Proof
.
intros
?
f
Hf
x
.
by
apply
:
timeless
.
Qed
.
(** Internalized properties *)
...
...
@@ -179,7 +179,7 @@ Arguments iprodR {_ _ _} _.
Arguments
iprodUR
{
_
_
_
}
_
.
Definition
iprod_singleton
`
{
Finite
A
}
{
B
:
A
→
ucmraT
}
(
x
:
A
)
(
y
:
B
x
)
:
iprod
B
:
=
iprod_insert
x
y
∅
.
(
x
:
A
)
(
y
:
B
x
)
:
iprod
B
:
=
iprod_insert
x
y
ε
.
Instance
:
Params
(@
iprod_singleton
)
5
.
Section
iprod_singleton
.
...
...
@@ -195,11 +195,11 @@ Section iprod_singleton.
Lemma
iprod_lookup_singleton
x
(
y
:
B
x
)
:
(
iprod_singleton
x
y
)
x
=
y
.
Proof
.
by
rewrite
/
iprod_singleton
iprod_lookup_insert
.
Qed
.
Lemma
iprod_lookup_singleton_ne
x
x'
(
y
:
B
x
)
:
x
≠
x'
→
(
iprod_singleton
x
y
)
x'
=
∅
.
x
≠
x'
→
(
iprod_singleton
x
y
)
x'
=
ε
.
Proof
.
intros
;
by
rewrite
/
iprod_singleton
iprod_lookup_insert_ne
.
Qed
.
Global
Instance
iprod_singleton_timeless
x
(
y
:
B
x
)
:
(
∀
i
,
Timeless
(
∅
:
B
i
))
→
Timeless
y
→
Timeless
(
iprod_singleton
x
y
).
(
∀
i
,
Timeless
(
ε
:
B
i
))
→
Timeless
y
→
Timeless
(
iprod_singleton
x
y
).
Proof
.
apply
_
.
Qed
.
Lemma
iprod_singleton_validN
n
x
(
y
:
B
x
)
:
✓
{
n
}
iprod_singleton
x
y
↔
✓
{
n
}
y
.
...
...
@@ -243,7 +243,7 @@ Section iprod_singleton.
Proof
.
eauto
using
iprod_insert_update
.
Qed
.
Lemma
iprod_singleton_updateP_empty
x
(
P
:
B
x
→
Prop
)
(
Q
:
iprod
B
→
Prop
)
:
∅
~~>
:
P
→
(
∀
y2
,
P
y2
→
Q
(
iprod_singleton
x
y2
))
→
∅
~~>
:
Q
.
ε
~~>
:
P
→
(
∀
y2
,
P
y2
→
Q
(
iprod_singleton
x
y2
))
→
ε
~~>
:
Q
.
Proof
.
intros
Hx
HQ
;
apply
cmra_total_updateP
.
intros
n
gf
Hg
.
destruct
(
Hx
n
(
Some
(
gf
x
)))
as
(
y2
&?&?)
;
first
apply
Hg
.
...
...
@@ -253,10 +253,10 @@ Section iprod_singleton.
-
rewrite
iprod_lookup_op
iprod_lookup_singleton_ne
//.
apply
Hg
.
Qed
.
Lemma
iprod_singleton_updateP_empty'
x
(
P
:
B
x
→
Prop
)
:
∅
~~>
:
P
→
∅
~~>
:
λ
g
,
∃
y2
,
g
=
iprod_singleton
x
y2
∧
P
y2
.
ε
~~>
:
P
→
ε
~~>
:
λ
g
,
∃
y2
,
g
=
iprod_singleton
x
y2
∧
P
y2
.
Proof
.
eauto
using
iprod_singleton_updateP_empty
.
Qed
.
Lemma
iprod_singleton_update_empty
x
(
y
:
B
x
)
:
∅
~~>
y
→
∅
~~>
iprod_singleton
x
y
.
ε
~~>
y
→
ε
~~>
iprod_singleton
x
y
.
Proof
.
rewrite
!
cmra_update_updateP
;
eauto
using
iprod_singleton_updateP_empty
with
subst
.
...
...
theories/algebra/list.v
View file @
b51af294
...
...
@@ -221,7 +221,7 @@ Section cmra.
Qed
.
Canonical
Structure
listR
:
=
CMRAT
(
list
A
)
list_cmra_mixin
.
Global
Instance
empty_list
:
Empty
(
list
A
)
:
=
[].
Global
Instance
list_unit
:
Unit
(
list
A
)
:
=
[].
Definition
list_ucmra_mixin
:
UCMRAMixin
(
list
A
).
Proof
.
split
.
...
...
@@ -254,7 +254,7 @@ Arguments listR : clear implicits.
Arguments
listUR
:
clear
implicits
.
Instance
list_singletonM
{
A
:
ucmraT
}
:
SingletonM
nat
A
(
list
A
)
:
=
λ
n
x
,
replicate
n
∅
++
[
x
].
replicate
n
ε
++
[
x
].
Section
properties
.
Context
{
A
:
ucmraT
}.
...
...
@@ -298,7 +298,7 @@ Section properties.
Global
Instance
list_singletonM_proper
i
:
Proper
((
≡
)
==>
(
≡
))
(
list_singletonM
i
)
:
=
ne_proper
_
.
Lemma
elem_of_list_singletonM
i
z
x
:
z
∈
({[
i
:
=
x
]}
:
list
A
)
→
z
=
∅
∨
z
=
x
.
Lemma
elem_of_list_singletonM
i
z
x
:
z
∈
({[
i
:
=
x
]}
:
list
A
)
→
z
=
ε
∨
z
=
x
.
Proof
.
rewrite
elem_of_app
elem_of_list_singleton
elem_of_replicate
.
naive_solver
.
Qed
.
...
...
@@ -306,7 +306,7 @@ Section properties.
Proof
.
induction
i
;
by
f_equal
/=.
Qed
.
Lemma
list_lookup_singletonM_ne
i
j
x
:
i
≠
j
→
({[
i
:
=
x
]}
:
list
A
)
!!
j
=
None
∨
({[
i
:
=
x
]}
:
list
A
)
!!
j
=
Some
∅
.
({[
i
:
=
x
]}
:
list
A
)
!!
j
=
None
∨
({[
i
:
=
x
]}
:
list
A
)
!!
j
=
Some
ε
.
Proof
.
revert
j
;
induction
i
;
intros
[|
j
]
;
naive_solver
auto
with
omega
.
Qed
.
Lemma
list_singletonM_validN
n
i
x
:
✓
{
n
}
({[
i
:
=
x
]}
:
list
A
)
↔
✓
{
n
}
x
.
Proof
.
...
...
@@ -351,7 +351,7 @@ Section properties.
x
~~>
:
P
→
(
∀
y
,
P
y
→
Q
[
y
])
→
[
x
]
~~>
:
Q
.
Proof
.
rewrite
!
cmra_total_updateP
=>
Hup
HQ
n
lf
/
list_lookup_validN
Hv
.
destruct
(
Hup
n
(
from_option
id
∅
(
lf
!!
0
)))
as
(
y
&?&
Hv'
).
destruct
(
Hup
n
(
from_option
id
ε
(
lf
!!
0
)))
as
(
y
&?&
Hv'
).
{
move
:
(
Hv
0
).
by
destruct
lf
;
rewrite
/=
?right_id
.
}
exists
[
y
]
;
split
;
first
by
auto
.
apply
list_lookup_validN
=>
i
.
...
...
theories/algebra/local_updates.v
View file @
b51af294
...
...
@@ -105,7 +105,7 @@ Section updates_unital.
split
.
-
intros
Hup
n
z
.
apply
(
Hup
_
(
Some
z
)).
-
intros
Hup
n
[
z
|]
;
simpl
;
[
by
auto
|].
rewrite
-(
right_id
∅
op
y
)
-(
right_id
∅
op
y'
).
auto
.
rewrite
-(
right_id
ε
op
y
)
-(
right_id
ε
op
y'
).
auto
.
Qed
.
Lemma
local_update_unital_discrete
`
{!
CMRADiscrete
A
}
(
x
y
x'
y'
:
A
)
:
...
...
@@ -114,12 +114,12 @@ Section updates_unital.
rewrite
local_update_discrete
.
split
.
-
intros
Hup
z
.
apply
(
Hup
(
Some
z
)).
-
intros
Hup
[
z
|]
;
simpl
;
[
by
auto
|].
rewrite
-(
right_id
∅
op
y
)
-(
right_id
∅
op
y'
).
auto
.
rewrite
-(
right_id
ε
op
y
)
-(
right_id
ε
op
y'
).
auto
.
Qed
.
Lemma
cancel_local_update_
empty
x
y
`
{!
Cancelable
x
}
:
(
x
⋅
y
,
x
)
~l
~>
(
y
,
∅
).
Proof
.
rewrite
-{
2
}(
right_id
∅
op
x
).
by
apply
cancel_local_update
.
Qed
.
Lemma
cancel_local_update_
unit
x
y
`
{!
Cancelable
x
}
:
(
x
⋅
y
,
x
)
~l
~>
(
y
,
ε
).
Proof
.
rewrite
-{
2
}(
right_id
ε
op
x
).
by
apply
cancel_local_update
.
Qed
.
End
updates_unital
.
(** * Product *)
...
...
theories/base_logic/derived.v
View file @
b51af294
...
...
@@ -758,8 +758,8 @@ Lemma ownM_invalid (a : M) : ¬ ✓{0} a → uPred_ownM a ⊢ False.
Proof
.
by
intros
;
rewrite
ownM_valid
cmra_valid_elim
.
Qed
.
Global
Instance
ownM_mono
:
Proper
(
flip
(
≼
)
==>
(
⊢
))
(@
uPred_ownM
M
).
Proof
.
intros
a
b
[
b'
->].
rewrite
ownM_op
.
eauto
.
Qed
.
Lemma
ownM_
empty
'
:
uPred_ownM
∅
⊣
⊢
True
.
Proof
.
apply
(
anti_symm
_
)
;
first
by
auto
.
apply
ownM_
empty
.
Qed
.
Lemma
ownM_
unit
'
:
uPred_ownM
ε
⊣
⊢
True
.
Proof
.
apply
(
anti_symm
_
)
;
first
by
auto
.
apply
ownM_
unit
.
Qed
.
Lemma
always_cmra_valid
{
A
:
cmraT
}
(
a
:
A
)
:
□
✓
a
⊣
⊢
✓
a
.
Proof
.
intros
;
apply
(
anti_symm
_
)
;
first
by
apply
:
always_elim
.
...
...
@@ -990,6 +990,6 @@ Global Instance uPred_except_0_sep_homomorphism :
Proof
.
split
;
[
split
;
try
apply
_
|].
apply
except_0_sep
.
apply
except_0_True
.
Qed
.
Global
Instance
uPred_ownM_sep_homomorphism
:
MonoidHomomorphism
op
uPred_sep
(
≡
)
(@
uPred_ownM
M
).
Proof
.
split
;
[
split
;
try
apply
_
|].
apply
ownM_op
.
apply
ownM_
empty
'
.
Qed
.
Proof
.
split
;
[
split
;
try
apply
_
|].
apply
ownM_op
.
apply
ownM_
unit
'
.
Qed
.
End
derived
.
End
uPred
.
theories/base_logic/double_negation.v
View file @
b51af294
...
...
@@ -307,7 +307,7 @@ Proof.
case
(
decide
(
n'
<
n
)).
-
intros
.
move
:
laterN_small
.
unseal
.
naive_solver
.
-
intros
.
assert
(
n
≤
n'
).
omega
.
exfalso
.
specialize
(
Hupd
n'
∅
).
exfalso
.
specialize
(
Hupd
n'
ε
).
eapply
Hdne
.
intros
Hfal
.
eapply
laterN_big
;
eauto
.
unseal
.
rewrite
right_id
in
Hupd
*
;
naive_solver
.
...
...
@@ -323,7 +323,7 @@ Proof.
-
rewrite
/
uPred_nnupd
.
unseal
=>
k
P
x
Hx
Hf1
Hf2
.
eapply
Hf1
.
intros
Hf3
.
eapply
(
laterN_big
(
S
k
)
(
S
k
))
;
eauto
.
specialize
(
Hf3
(
S
k
)
(
S
k
)
∅
).
rewrite
right_id
in
Hf3
*.
unseal
.
specialize
(
Hf3
(
S
k
)
(
S
k
)
ε
).
rewrite
right_id
in
Hf3
*.
unseal
.
intros
Hf3
.
eapply
Hf3
;
eauto
.
intros
???
Hx'
.
rewrite
left_id
in
Hx'
*=>
Hx'
.
unseal
.
...
...
theories/base_logic/lib/auth.v
View file @
b51af294
...
...
@@ -119,8 +119,8 @@ Section auth.
iMod
(
auth_alloc_strong
N
E
t
∅
with
"Hφ"
)
as
(
γ
)
"[_ ?]"
;
eauto
.
Qed
.
Lemma
auth_empty
γ
:
(|==>
auth_own
γ
∅
)%
I
.
Proof
.
by
rewrite
/
auth_own
-
own_
empty
.
Qed
.
Lemma
auth_empty
γ
:
(|==>
auth_own
γ
ε
)%
I
.
Proof
.
by
rewrite
/
auth_own
-
own_
unit
.
Qed
.
Lemma
auth_acc
E
γ
a
:
▷
auth_inv
γ
f
φ
∗
auth_own
γ
a
={
E
}=
∗
∃
t
,
...
...
theories/base_logic/lib/boxes.v
View file @
b51af294
...
...
@@ -23,10 +23,10 @@ Section box_defs.
Definition
slice_name
:
=
gname
.
Definition
box_own_auth
(
γ
:
slice_name
)
(
a
:
auth
(
option
(
excl
bool
)))
:
iProp
Σ
:
=
own
γ
(
a
,
(
∅
:
option
(
agree
(
later
(
iPreProp
Σ
))))
).
own
γ
(
a
,
None
).
Definition
box_own_prop
(
γ
:
slice_name
)
(
P
:
iProp
Σ
)
:
iProp
Σ
:
=
own
γ
(
∅
:
auth
(
option
(
excl
bool
))
,
Some
(
to_agree
(
Next
(
iProp_unfold
P
)))).
own
γ
(
ε
,
Some
(
to_agree
(
Next
(
iProp_unfold
P
)))).
Definition
slice_inv
(
γ
:
slice_name
)
(
P
:
iProp
Σ
)
:
iProp
Σ
:
=
(
∃
b
,
box_own_auth
γ
(
●
Excl'
b
)
∗
if
b
then
P
else
True
)%
I
.
...
...
theories/base_logic/lib/na_invariants.v
View file @
b51af294
...
...
@@ -19,11 +19,11 @@ Section defs.
Context
`
{
invG
Σ
,
na_invG
Σ
}.
Definition
na_own
(
p
:
na_inv_pool_name
)
(
E
:
coPset
)
:
iProp
Σ
:
=
own
p
(
CoPset
E
,
∅
).
own
p
(
CoPset
E
,
GSet
∅
).
Definition
na_inv
(
p
:
na_inv_pool_name
)
(
N
:
namespace
)
(
P
:
iProp
Σ
)
:
iProp
Σ
:
=
(
∃
i
,
⌜
i
∈
(
↑
N
:
coPset
)
⌝
∧
inv
N
(
P
∗
own
p
(
∅
,
GSet
{[
i
]})
∨
na_own
p
{[
i
]}))%
I
.
inv
N
(
P
∗
own
p
(
CoPset
∅
,
GSet
{[
i
]})
∨
na_own
p
{[
i
]}))%
I
.
End
defs
.
Instance
:
Params
(@
na_inv
)
3
.
...
...
@@ -68,7 +68,7 @@ Section proofs.
Lemma
na_inv_alloc
p
E
N
P
:
▷
P
={
E
}=
∗
na_inv
p
N
P
.
Proof
.
iIntros
"HP"
.
iMod
(
own_
empty
(
prodUR
coPset_disjUR
(
gset_disjUR
positive
))
p
)
as
"Hempty"
.
iMod
(
own_
unit
(
prodUR
coPset_disjUR
(
gset_disjUR
positive
))
p
)
as
"Hempty"
.
iMod
(
own_updateP
with
"Hempty"
)
as
([
m1
m2
])
"[Hm Hown]"
.
{
apply
prod_updateP'
.
apply
cmra_updateP_id
,
(
reflexivity
(
R
:
=
eq
)).
apply
(
gset_disj_alloc_empty_updateP_strong'
(
λ
i
,
i
∈
(
↑
N
:
coPset
))).
...
...
theories/base_logic/lib/own.v
View file @
b51af294
...
...
@@ -119,7 +119,7 @@ Lemma own_alloc_strong a (G : gset gname) :
Proof
.
intros
Ha
.
rewrite
-(
bupd_mono
(
∃
m
,
⌜
∃
γ
,
γ
∉
G
∧
m
=
iRes_singleton
γ
a
⌝
∧
uPred_ownM
m
)%
I
).
-
rewrite
/
uPred_valid
ownM_
empty
.
-
rewrite
/
uPred_valid
ownM_
unit
.
eapply
bupd_ownM_updateP
,
(
iprod_singleton_updateP_empty
(
inG_id
_
))
;
first
(
eapply
alloc_updateP_strong'
,
cmra_transport_valid
,
Ha
)
;
naive_solver
.
...
...
@@ -167,11 +167,11 @@ Arguments own_update {_ _} [_] _ _ _ _.
Arguments
own_update_2
{
_
_
}
[
_
]
_
_
_
_
_
.
Arguments
own_update_3
{
_
_
}
[
_
]
_
_
_
_
_
_
.
Lemma
own_
empty
A
`
{
inG
Σ
(
A
:
ucmraT
)}
γ
:
(|==>
own
γ
∅
)%
I
.
Lemma
own_
unit
A
`
{
inG
Σ
(
A
:
ucmraT
)}
γ
:
(|==>
own
γ
ε
)%
I
.
Proof
.
rewrite
/
uPred_valid
ownM_
empty
!
own_eq
/
own_def
.
rewrite
/
uPred_valid
ownM_
unit
!
own_eq
/
own_def
.
apply
bupd_ownM_update
,
iprod_singleton_update_empty
.
apply
(
alloc_unit_singleton_update
(
cmra_transport
inG_prf
∅
))
;
last
done
.
apply
(
alloc_unit_singleton_update
(
cmra_transport
inG_prf
ε
))
;
last
done
.