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
Rice Wine
Iris
Commits
4397cde3
Commit
4397cde3
authored
Jun 16, 2016
by
Robbert Krebbers
Browse files
Move update stuff to its own file (it used to be in cmra.v).
parent
a20c86e3
Changes
9
Hide whitespace changes
Inline
Side-by-side
_CoqProject
View file @
4397cde3
...
...
@@ -56,6 +56,7 @@ algebra/upred_big_op.v
algebra/frac.v
algebra/csum.v
algebra/list.v
algebra/updates.v
program_logic/model.v
program_logic/adequacy.v
program_logic/hoare_lifting.v
...
...
algebra/auth.v
View file @
4397cde3
From
iris
.
algebra
Require
Export
excl
.
From
iris
.
algebra
Require
Export
excl
updates
.
From
iris
.
algebra
Require
Import
upred
.
Local
Arguments
valid
_
_
!
_
/.
Local
Arguments
validN
_
_
_
!
_
/.
...
...
algebra/cmra.v
View file @
4397cde3
...
...
@@ -217,26 +217,6 @@ Class CMRAMonotone {A B : cmraT} (f : A → B) := {
Arguments
validN_preserving
{
_
_
}
_
{
_
}
_
_
_
.
Arguments
included_preserving
{
_
_
}
_
{
_
}
_
_
_
.
(** * Local updates *)
(** The idea is that lemams taking this class will usually have L explicit,
and leave Lv implicit - it will be inferred by the typeclass machinery. *)
Class
LocalUpdate
{
A
:
cmraT
}
(
Lv
:
A
→
Prop
)
(
L
:
A
→
A
)
:
=
{
local_update_ne
n
:
>
Proper
(
dist
n
==>
dist
n
)
L
;
local_updateN
n
x
y
:
Lv
x
→
✓
{
n
}
(
x
⋅
y
)
→
L
(
x
⋅
y
)
≡
{
n
}
≡
L
x
⋅
y
}.
Arguments
local_updateN
{
_
_
}
_
{
_
}
_
_
_
_
_
.
(** * Frame preserving updates *)
Definition
cmra_updateP
{
A
:
cmraT
}
(
x
:
A
)
(
P
:
A
→
Prop
)
:
=
∀
n
mz
,
✓
{
n
}
(
x
⋅
?
mz
)
→
∃
y
,
P
y
∧
✓
{
n
}
(
y
⋅
?
mz
).
Instance
:
Params
(@
cmra_updateP
)
1
.
Infix
"~~>:"
:
=
cmra_updateP
(
at
level
70
).
Definition
cmra_update
{
A
:
cmraT
}
(
x
y
:
A
)
:
=
∀
n
mz
,
✓
{
n
}
(
x
⋅
?
mz
)
→
✓
{
n
}
(
y
⋅
?
mz
).
Infix
"~~>"
:
=
cmra_update
(
at
level
70
).
Instance
:
Params
(@
cmra_update
)
1
.
(** * Properties **)
Section
cmra
.
Context
{
A
:
cmraT
}.
...
...
@@ -296,17 +276,6 @@ Global Instance cmra_opM_ne n : Proper (dist n ==> dist n ==> dist n) (@opM A).
Proof
.
destruct
2
;
by
cofe_subst
.
Qed
.
Global
Instance
cmra_opM_proper
:
Proper
((
≡
)
==>
(
≡
)
==>
(
≡
))
(@
opM
A
).
Proof
.
destruct
2
;
by
setoid_subst
.
Qed
.
Global
Instance
cmra_updateP_proper
:
Proper
((
≡
)
==>
pointwise_relation
_
iff
==>
iff
)
(@
cmra_updateP
A
).
Proof
.
rewrite
/
pointwise_relation
/
cmra_updateP
=>
x
x'
Hx
P
P'
HP
;
split
=>
?
n
mz
;
setoid_subst
;
naive_solver
.
Qed
.
Global
Instance
cmra_update_proper
:
Proper
((
≡
)
==>
(
≡
)
==>
iff
)
(@
cmra_update
A
).
Proof
.
rewrite
/
cmra_update
=>
x
x'
Hx
y
y'
Hy
;
split
=>
?
n
mz
?
;
setoid_subst
;
auto
.
Qed
.
(** ** Op *)
Lemma
cmra_opM_assoc
x
y
mz
:
(
x
⋅
y
)
⋅
?
mz
≡
x
⋅
(
y
⋅
?
mz
).
...
...
@@ -523,104 +492,6 @@ Proof.
split
;
first
by
apply
cmra_included_includedN
.
intros
[
z
->%(
timeless_iff
_
_
)]
;
eauto
using
cmra_included_l
.
Qed
.
(** ** Local updates *)
Global
Instance
local_update_proper
Lv
(
L
:
A
→
A
)
:
LocalUpdate
Lv
L
→
Proper
((
≡
)
==>
(
≡
))
L
.
Proof
.
intros
;
apply
(
ne_proper
_
).
Qed
.
Lemma
local_update
L
`
{!
LocalUpdate
Lv
L
}
x
y
:
Lv
x
→
✓
(
x
⋅
y
)
→
L
(
x
⋅
y
)
≡
L
x
⋅
y
.
Proof
.
by
rewrite
cmra_valid_validN
equiv_dist
=>??
n
;
apply
(
local_updateN
L
).
Qed
.
Global
Instance
op_local_update
x
:
LocalUpdate
(
λ
_
,
True
)
(
op
x
).
Proof
.
split
.
apply
_
.
by
intros
n
y1
y2
_
_;
rewrite
assoc
.
Qed
.
Global
Instance
id_local_update
:
LocalUpdate
(
λ
_
,
True
)
(@
id
A
).
Proof
.
split
;
auto
with
typeclass_instances
.
Qed
.
Global
Instance
exclusive_local_update
y
:
LocalUpdate
Exclusive
(
λ
_
,
y
)
|
1000
.
Proof
.
split
.
apply
_
.
by
intros
?????%
exclusiveN_r
.
Qed
.
(** ** Updates *)
Lemma
cmra_update_updateP
x
y
:
x
~~>
y
↔
x
~~>
:
(
y
=).
Proof
.
split
=>
Hup
n
z
?
;
eauto
.
destruct
(
Hup
n
z
)
as
(?&<-&?)
;
auto
.
Qed
.
Lemma
cmra_updateP_id
(
P
:
A
→
Prop
)
x
:
P
x
→
x
~~>
:
P
.
Proof
.
intros
?
n
mz
?
;
eauto
.
Qed
.
Lemma
cmra_updateP_compose
(
P
Q
:
A
→
Prop
)
x
:
x
~~>
:
P
→
(
∀
y
,
P
y
→
y
~~>
:
Q
)
→
x
~~>
:
Q
.
Proof
.
intros
Hx
Hy
n
mz
?.
destruct
(
Hx
n
mz
)
as
(
y
&?&?)
;
naive_solver
.
Qed
.
Lemma
cmra_updateP_compose_l
(
Q
:
A
→
Prop
)
x
y
:
x
~~>
y
→
y
~~>
:
Q
→
x
~~>
:
Q
.
Proof
.
rewrite
cmra_update_updateP
.
intros
;
apply
cmra_updateP_compose
with
(
y
=)
;
naive_solver
.
Qed
.
Lemma
cmra_updateP_weaken
(
P
Q
:
A
→
Prop
)
x
:
x
~~>
:
P
→
(
∀
y
,
P
y
→
Q
y
)
→
x
~~>
:
Q
.
Proof
.
eauto
using
cmra_updateP_compose
,
cmra_updateP_id
.
Qed
.
Global
Instance
cmra_update_preorder
:
PreOrder
(@
cmra_update
A
).
Proof
.
split
.
-
intros
x
.
by
apply
cmra_update_updateP
,
cmra_updateP_id
.
-
intros
x
y
z
.
rewrite
!
cmra_update_updateP
.
eauto
using
cmra_updateP_compose
with
subst
.
Qed
.
Lemma
cmra_update_exclusive
`
{!
Exclusive
x
}
y
:
✓
y
→
x
~~>
y
.
Proof
.
move
=>??[
z
|]=>[/
exclusiveN_r
[]|
_
].
by
apply
cmra_valid_validN
.
Qed
.
Lemma
cmra_updateP_op
(
P1
P2
Q
:
A
→
Prop
)
x1
x2
:
x1
~~>
:
P1
→
x2
~~>
:
P2
→
(
∀
y1
y2
,
P1
y1
→
P2
y2
→
Q
(
y1
⋅
y2
))
→
x1
⋅
x2
~~>
:
Q
.
Proof
.
intros
Hx1
Hx2
Hy
n
mz
?.
destruct
(
Hx1
n
(
Some
(
x2
⋅
?
mz
)))
as
(
y1
&?&?).
{
by
rewrite
/=
-
cmra_opM_assoc
.
}
destruct
(
Hx2
n
(
Some
(
y1
⋅
?
mz
)))
as
(
y2
&?&?).
{
by
rewrite
/=
-
cmra_opM_assoc
(
comm
_
x2
)
cmra_opM_assoc
.
}
exists
(
y1
⋅
y2
)
;
split
;
last
rewrite
(
comm
_
y1
)
cmra_opM_assoc
;
auto
.
Qed
.
Lemma
cmra_updateP_op'
(
P1
P2
:
A
→
Prop
)
x1
x2
:
x1
~~>
:
P1
→
x2
~~>
:
P2
→
x1
⋅
x2
~~>
:
λ
y
,
∃
y1
y2
,
y
=
y1
⋅
y2
∧
P1
y1
∧
P2
y2
.
Proof
.
eauto
10
using
cmra_updateP_op
.
Qed
.
Lemma
cmra_update_op
x1
x2
y1
y2
:
x1
~~>
y1
→
x2
~~>
y2
→
x1
⋅
x2
~~>
y1
⋅
y2
.
Proof
.
rewrite
!
cmra_update_updateP
;
eauto
using
cmra_updateP_op
with
congruence
.
Qed
.
Section
total_updates
.
Context
`
{
CMRATotal
A
}.
Lemma
cmra_total_updateP
x
(
P
:
A
→
Prop
)
:
x
~~>
:
P
↔
∀
n
z
,
✓
{
n
}
(
x
⋅
z
)
→
∃
y
,
P
y
∧
✓
{
n
}
(
y
⋅
z
).
Proof
.
split
=>
Hup
;
[
intros
n
z
;
apply
(
Hup
n
(
Some
z
))|].
intros
n
[
z
|]
?
;
simpl
;
[
by
apply
Hup
|].
destruct
(
Hup
n
(
core
x
))
as
(
y
&?&?)
;
first
by
rewrite
cmra_core_r
.
eauto
using
cmra_validN_op_l
.
Qed
.
Lemma
cmra_total_update
x
y
:
x
~~>
y
↔
∀
n
z
,
✓
{
n
}
(
x
⋅
z
)
→
✓
{
n
}
(
y
⋅
z
).
Proof
.
rewrite
cmra_update_updateP
cmra_total_updateP
.
naive_solver
.
Qed
.
Context
`
{
CMRADiscrete
A
}.
Lemma
cmra_discrete_updateP
(
x
:
A
)
(
P
:
A
→
Prop
)
:
x
~~>
:
P
↔
∀
z
,
✓
(
x
⋅
z
)
→
∃
y
,
P
y
∧
✓
(
y
⋅
z
).
Proof
.
rewrite
cmra_total_updateP
;
setoid_rewrite
<-
cmra_discrete_valid_iff
.
naive_solver
eauto
using
0
.
Qed
.
Lemma
cmra_discrete_update
`
{
CMRADiscrete
A
}
(
x
y
:
A
)
:
x
~~>
y
↔
∀
z
,
✓
(
x
⋅
z
)
→
✓
(
y
⋅
z
).
Proof
.
rewrite
cmra_total_update
;
setoid_rewrite
<-
cmra_discrete_valid_iff
.
naive_solver
eauto
using
0
.
Qed
.
End
total_updates
.
End
cmra
.
(** * Properties about CMRAs with a unit element **)
...
...
@@ -646,13 +517,6 @@ Section ucmra.
intros
x
.
destruct
(
cmra_pcore_preserving'
∅
x
∅
)
as
(
cx
&->&?)
;
eauto
using
ucmra_unit_least
,
(
persistent
∅
).
Qed
.
Lemma
ucmra_update_unit
x
:
x
~~>
∅
.
Proof
.
apply
cmra_total_update
=>
n
z
.
rewrite
left_id
;
apply
cmra_validN_op_r
.
Qed
.
Lemma
ucmra_update_unit_alt
y
:
∅
~~>
y
↔
∀
x
,
x
~~>
y
.
Proof
.
split
;
[
intros
;
trans
∅
|]
;
auto
using
ucmra_update_unit
.
Qed
.
End
ucmra
.
Hint
Immediate
cmra_unit_total
.
...
...
@@ -793,12 +657,6 @@ Section cmra_transport.
Proof
.
by
destruct
H
.
Qed
.
Global
Instance
cmra_transport_persistent
x
:
Persistent
x
→
Persistent
(
T
x
).
Proof
.
by
destruct
H
.
Qed
.
Lemma
cmra_transport_updateP
(
P
:
A
→
Prop
)
(
Q
:
B
→
Prop
)
x
:
x
~~>
:
P
→
(
∀
y
,
P
y
→
Q
(
T
y
))
→
T
x
~~>
:
Q
.
Proof
.
destruct
H
;
eauto
using
cmra_updateP_weaken
.
Qed
.
Lemma
cmra_transport_updateP'
(
P
:
A
→
Prop
)
x
:
x
~~>
:
P
→
T
x
~~>
:
λ
y
,
∃
y'
,
y
=
cmra_transport
H
y'
∧
P
y'
.
Proof
.
eauto
using
cmra_transport_updateP
.
Qed
.
End
cmra_transport
.
(** * Instances *)
...
...
@@ -1009,39 +867,10 @@ Section prod.
Persistent
x
→
Persistent
y
→
Persistent
(
x
,
y
).
Proof
.
by
rewrite
/
Persistent
prod_pcore_Some'
.
Qed
.
Global
Instance
pair_exclusive_l
x
y
:
Exclusive
x
→
Exclusive
(
x
,
y
).
Global
Instance
pair_exclusive_l
x
y
:
Exclusive
x
→
Exclusive
(
x
,
y
).
Proof
.
by
intros
?[][?%
exclusive0_r
].
Qed
.
Global
Instance
pair_exclusive_r
x
y
:
Exclusive
y
→
Exclusive
(
x
,
y
).
Global
Instance
pair_exclusive_r
x
y
:
Exclusive
y
→
Exclusive
(
x
,
y
).
Proof
.
by
intros
?[][??%
exclusive0_r
].
Qed
.
Lemma
prod_updateP
P1
P2
(
Q
:
A
*
B
→
Prop
)
x
:
x
.
1
~~>
:
P1
→
x
.
2
~~>
:
P2
→
(
∀
a
b
,
P1
a
→
P2
b
→
Q
(
a
,
b
))
→
x
~~>
:
Q
.
Proof
.
intros
Hx1
Hx2
HP
n
mz
[??]
;
simpl
in
*.
destruct
(
Hx1
n
(
fst
<$>
mz
))
as
(
a
&?&?)
;
first
by
destruct
mz
.
destruct
(
Hx2
n
(
snd
<$>
mz
))
as
(
b
&?&?)
;
first
by
destruct
mz
.
exists
(
a
,
b
)
;
repeat
split
;
destruct
mz
;
auto
.
Qed
.
Lemma
prod_updateP'
P1
P2
x
:
x
.
1
~~>
:
P1
→
x
.
2
~~>
:
P2
→
x
~~>
:
λ
y
,
P1
(
y
.
1
)
∧
P2
(
y
.
2
).
Proof
.
eauto
using
prod_updateP
.
Qed
.
Lemma
prod_update
x
y
:
x
.
1
~~>
y
.
1
→
x
.
2
~~>
y
.
2
→
x
~~>
y
.
Proof
.
rewrite
!
cmra_update_updateP
.
destruct
x
,
y
;
eauto
using
prod_updateP
with
subst
.
Qed
.
Global
Instance
prod_local_update
(
LA
:
A
→
A
)
`
{!
LocalUpdate
LvA
LA
}
(
LB
:
B
→
B
)
`
{!
LocalUpdate
LvB
LB
}
:
LocalUpdate
(
λ
x
,
LvA
(
x
.
1
)
∧
LvB
(
x
.
2
))
(
prod_map
LA
LB
).
Proof
.
constructor
.
-
intros
n
x
y
[??]
;
constructor
;
simpl
;
by
apply
local_update_ne
.
-
intros
n
??
[??]
[??]
;
constructor
;
simpl
in
*
;
eapply
local_updateN
;
eauto
.
Qed
.
End
prod
.
Arguments
prodR
:
clear
implicits
.
...
...
@@ -1216,38 +1045,6 @@ Section option.
Global
Instance
option_persistent
(
mx
:
option
A
)
:
(
∀
x
:
A
,
Persistent
x
)
→
Persistent
mx
.
Proof
.
intros
.
destruct
mx
;
apply
_
.
Qed
.
(** Updates *)
Global
Instance
option_fmap_local_update
L
Lv
:
LocalUpdate
Lv
L
→
LocalUpdate
(
λ
mx
,
if
mx
is
Some
x
then
Lv
x
else
False
)
(
fmap
L
).
Proof
.
split
;
first
apply
_
.
intros
n
[
x
|]
[
z
|]
;
constructor
;
by
eauto
using
(
local_updateN
L
).
Qed
.
Global
Instance
option_const_local_update
Lv
y
:
LocalUpdate
Lv
(
λ
_
,
y
)
→
LocalUpdate
(
λ
mx
,
if
mx
is
Some
x
then
Lv
x
else
False
)
(
λ
_
,
Some
y
).
Proof
.
split
;
first
apply
_
.
intros
n
[
x
|]
[
z
|]
;
constructor
;
by
eauto
using
(
local_updateN
(
λ
_
,
y
)).
Qed
.
Lemma
option_updateP
(
P
:
A
→
Prop
)
(
Q
:
option
A
→
Prop
)
x
:
x
~~>
:
P
→
(
∀
y
,
P
y
→
Q
(
Some
y
))
→
Some
x
~~>
:
Q
.
Proof
.
intros
Hx
Hy
;
apply
cmra_total_updateP
=>
n
[
y
|]
?.
{
destruct
(
Hx
n
(
Some
y
))
as
(
y'
&?&?)
;
auto
.
exists
(
Some
y'
)
;
auto
.
}
destruct
(
Hx
n
None
)
as
(
y'
&?&?)
;
rewrite
?cmra_core_r
;
auto
.
by
exists
(
Some
y'
)
;
auto
.
Qed
.
Lemma
option_updateP'
(
P
:
A
→
Prop
)
x
:
x
~~>
:
P
→
Some
x
~~>
:
from_option
P
False
.
Proof
.
eauto
using
option_updateP
.
Qed
.
Lemma
option_update
x
y
:
x
~~>
y
→
Some
x
~~>
Some
y
.
Proof
.
rewrite
!
cmra_update_updateP
;
eauto
using
option_updateP
with
congruence
.
Qed
.
End
option
.
Arguments
optionR
:
clear
implicits
.
...
...
algebra/csum.v
View file @
4397cde3
From
iris
.
algebra
Require
Export
cmra
.
From
iris
.
algebra
Require
Export
cmra
updates
.
From
iris
.
algebra
Require
Import
upred
.
Local
Arguments
pcore
_
_
!
_
/.
Local
Arguments
cmra_pcore
_
!
_
/.
...
...
algebra/dra.v
View file @
4397cde3
From
iris
.
algebra
Require
Export
cmra
.
From
iris
.
algebra
Require
Export
cmra
updates
.
Record
DRAMixin
A
`
{
Equiv
A
,
Core
A
,
Disjoint
A
,
Op
A
,
Valid
A
}
:
=
{
(* setoids *)
...
...
algebra/gmap.v
View file @
4397cde3
From
iris
.
algebra
Require
Export
cmra
.
From
iris
.
algebra
Require
Export
cmra
updates
.
From
iris
.
prelude
Require
Export
gmap
.
From
iris
.
algebra
Require
Import
upred
.
...
...
algebra/iprod.v
View file @
4397cde3
From
iris
.
algebra
Require
Export
cmra
.
From
iris
.
algebra
Require
Export
cmra
updates
.
From
iris
.
algebra
Require
Import
upred
.
From
iris
.
prelude
Require
Import
finite
.
...
...
algebra/list.v
View file @
4397cde3
From
iris
.
algebra
Require
Export
cmra
.
From
iris
.
algebra
Require
Export
cmra
updates
.
From
iris
.
prelude
Require
Export
list
.
From
iris
.
algebra
Require
Import
upred
.
...
...
algebra/updates.v
0 → 100644
View file @
4397cde3
From
iris
.
algebra
Require
Export
cmra
.
(** * Local updates *)
(** The idea is that lemams taking this class will usually have L explicit,
and leave Lv implicit - it will be inferred by the typeclass machinery. *)
Class
LocalUpdate
{
A
:
cmraT
}
(
Lv
:
A
→
Prop
)
(
L
:
A
→
A
)
:
=
{
local_update_ne
n
:
>
Proper
(
dist
n
==>
dist
n
)
L
;
local_updateN
n
x
y
:
Lv
x
→
✓
{
n
}
(
x
⋅
y
)
→
L
(
x
⋅
y
)
≡
{
n
}
≡
L
x
⋅
y
}.
Arguments
local_updateN
{
_
_
}
_
{
_
}
_
_
_
_
_
.
(** * Frame preserving updates *)
Definition
cmra_updateP
{
A
:
cmraT
}
(
x
:
A
)
(
P
:
A
→
Prop
)
:
=
∀
n
mz
,
✓
{
n
}
(
x
⋅
?
mz
)
→
∃
y
,
P
y
∧
✓
{
n
}
(
y
⋅
?
mz
).
Instance
:
Params
(@
cmra_updateP
)
1
.
Infix
"~~>:"
:
=
cmra_updateP
(
at
level
70
).
Definition
cmra_update
{
A
:
cmraT
}
(
x
y
:
A
)
:
=
∀
n
mz
,
✓
{
n
}
(
x
⋅
?
mz
)
→
✓
{
n
}
(
y
⋅
?
mz
).
Infix
"~~>"
:
=
cmra_update
(
at
level
70
).
Instance
:
Params
(@
cmra_update
)
1
.
(** ** CMRAs *)
Section
cmra
.
Context
{
A
:
cmraT
}.
Implicit
Types
x
y
:
A
.
Global
Instance
cmra_updateP_proper
:
Proper
((
≡
)
==>
pointwise_relation
_
iff
==>
iff
)
(@
cmra_updateP
A
).
Proof
.
rewrite
/
pointwise_relation
/
cmra_updateP
=>
x
x'
Hx
P
P'
HP
;
split
=>
?
n
mz
;
setoid_subst
;
naive_solver
.
Qed
.
Global
Instance
cmra_update_proper
:
Proper
((
≡
)
==>
(
≡
)
==>
iff
)
(@
cmra_update
A
).
Proof
.
rewrite
/
cmra_update
=>
x
x'
Hx
y
y'
Hy
;
split
=>
?
n
mz
?
;
setoid_subst
;
auto
.
Qed
.
(** ** Local updates *)
Global
Instance
local_update_proper
(
L
:
A
→
A
)
Lv
:
LocalUpdate
Lv
L
→
Proper
((
≡
)
==>
(
≡
))
L
.
Proof
.
intros
;
apply
(
ne_proper
_
).
Qed
.
Lemma
local_update
(
L
:
A
→
A
)
`
{!
LocalUpdate
Lv
L
}
x
y
:
Lv
x
→
✓
(
x
⋅
y
)
→
L
(
x
⋅
y
)
≡
L
x
⋅
y
.
Proof
.
by
rewrite
cmra_valid_validN
equiv_dist
=>??
n
;
apply
(
local_updateN
L
).
Qed
.
Global
Instance
op_local_update
x
:
LocalUpdate
(
λ
_
,
True
)
(
op
x
).
Proof
.
split
.
apply
_
.
by
intros
n
y1
y2
_
_;
rewrite
assoc
.
Qed
.
Global
Instance
id_local_update
:
LocalUpdate
(
λ
_
,
True
)
(@
id
A
).
Proof
.
split
;
auto
with
typeclass_instances
.
Qed
.
Global
Instance
exclusive_local_update
y
:
LocalUpdate
Exclusive
(
λ
_
,
y
)
|
1000
.
Proof
.
split
.
apply
_
.
by
intros
?????%
exclusiveN_r
.
Qed
.
(** ** Frame preserving updates *)
Lemma
cmra_update_updateP
x
y
:
x
~~>
y
↔
x
~~>
:
(
y
=).
Proof
.
split
=>
Hup
n
z
?
;
eauto
.
destruct
(
Hup
n
z
)
as
(?&<-&?)
;
auto
.
Qed
.
Lemma
cmra_updateP_id
(
P
:
A
→
Prop
)
x
:
P
x
→
x
~~>
:
P
.
Proof
.
intros
?
n
mz
?
;
eauto
.
Qed
.
Lemma
cmra_updateP_compose
(
P
Q
:
A
→
Prop
)
x
:
x
~~>
:
P
→
(
∀
y
,
P
y
→
y
~~>
:
Q
)
→
x
~~>
:
Q
.
Proof
.
intros
Hx
Hy
n
mz
?.
destruct
(
Hx
n
mz
)
as
(
y
&?&?)
;
naive_solver
.
Qed
.
Lemma
cmra_updateP_compose_l
(
Q
:
A
→
Prop
)
x
y
:
x
~~>
y
→
y
~~>
:
Q
→
x
~~>
:
Q
.
Proof
.
rewrite
cmra_update_updateP
.
intros
;
apply
cmra_updateP_compose
with
(
y
=)
;
naive_solver
.
Qed
.
Lemma
cmra_updateP_weaken
(
P
Q
:
A
→
Prop
)
x
:
x
~~>
:
P
→
(
∀
y
,
P
y
→
Q
y
)
→
x
~~>
:
Q
.
Proof
.
eauto
using
cmra_updateP_compose
,
cmra_updateP_id
.
Qed
.
Global
Instance
cmra_update_preorder
:
PreOrder
(@
cmra_update
A
).
Proof
.
split
.
-
intros
x
.
by
apply
cmra_update_updateP
,
cmra_updateP_id
.
-
intros
x
y
z
.
rewrite
!
cmra_update_updateP
.
eauto
using
cmra_updateP_compose
with
subst
.
Qed
.
Lemma
cmra_update_exclusive
`
{!
Exclusive
x
}
y
:
✓
y
→
x
~~>
y
.
Proof
.
move
=>??[
z
|]=>[/
exclusiveN_r
[]|
_
].
by
apply
cmra_valid_validN
.
Qed
.
Lemma
cmra_updateP_op
(
P1
P2
Q
:
A
→
Prop
)
x1
x2
:
x1
~~>
:
P1
→
x2
~~>
:
P2
→
(
∀
y1
y2
,
P1
y1
→
P2
y2
→
Q
(
y1
⋅
y2
))
→
x1
⋅
x2
~~>
:
Q
.
Proof
.
intros
Hx1
Hx2
Hy
n
mz
?.
destruct
(
Hx1
n
(
Some
(
x2
⋅
?
mz
)))
as
(
y1
&?&?).
{
by
rewrite
/=
-
cmra_opM_assoc
.
}
destruct
(
Hx2
n
(
Some
(
y1
⋅
?
mz
)))
as
(
y2
&?&?).
{
by
rewrite
/=
-
cmra_opM_assoc
(
comm
_
x2
)
cmra_opM_assoc
.
}
exists
(
y1
⋅
y2
)
;
split
;
last
rewrite
(
comm
_
y1
)
cmra_opM_assoc
;
auto
.
Qed
.
Lemma
cmra_updateP_op'
(
P1
P2
:
A
→
Prop
)
x1
x2
:
x1
~~>
:
P1
→
x2
~~>
:
P2
→
x1
⋅
x2
~~>
:
λ
y
,
∃
y1
y2
,
y
=
y1
⋅
y2
∧
P1
y1
∧
P2
y2
.
Proof
.
eauto
10
using
cmra_updateP_op
.
Qed
.
Lemma
cmra_update_op
x1
x2
y1
y2
:
x1
~~>
y1
→
x2
~~>
y2
→
x1
⋅
x2
~~>
y1
⋅
y2
.
Proof
.
rewrite
!
cmra_update_updateP
;
eauto
using
cmra_updateP_op
with
congruence
.
Qed
.
(** ** Frame preserving updates for total CMRAs *)
Section
total_updates
.
Context
`
{
CMRATotal
A
}.
Lemma
cmra_total_updateP
x
(
P
:
A
→
Prop
)
:
x
~~>
:
P
↔
∀
n
z
,
✓
{
n
}
(
x
⋅
z
)
→
∃
y
,
P
y
∧
✓
{
n
}
(
y
⋅
z
).
Proof
.
split
=>
Hup
;
[
intros
n
z
;
apply
(
Hup
n
(
Some
z
))|].
intros
n
[
z
|]
?
;
simpl
;
[
by
apply
Hup
|].
destruct
(
Hup
n
(
core
x
))
as
(
y
&?&?)
;
first
by
rewrite
cmra_core_r
.
eauto
using
cmra_validN_op_l
.
Qed
.
Lemma
cmra_total_update
x
y
:
x
~~>
y
↔
∀
n
z
,
✓
{
n
}
(
x
⋅
z
)
→
✓
{
n
}
(
y
⋅
z
).
Proof
.
rewrite
cmra_update_updateP
cmra_total_updateP
.
naive_solver
.
Qed
.
Context
`
{
CMRADiscrete
A
}.
Lemma
cmra_discrete_updateP
(
x
:
A
)
(
P
:
A
→
Prop
)
:
x
~~>
:
P
↔
∀
z
,
✓
(
x
⋅
z
)
→
∃
y
,
P
y
∧
✓
(
y
⋅
z
).
Proof
.
rewrite
cmra_total_updateP
;
setoid_rewrite
<-
cmra_discrete_valid_iff
.
naive_solver
eauto
using
0
.
Qed
.
Lemma
cmra_discrete_update
`
{
CMRADiscrete
A
}
(
x
y
:
A
)
:
x
~~>
y
↔
∀
z
,
✓
(
x
⋅
z
)
→
✓
(
y
⋅
z
).
Proof
.
rewrite
cmra_total_update
;
setoid_rewrite
<-
cmra_discrete_valid_iff
.
naive_solver
eauto
using
0
.
Qed
.
End
total_updates
.
End
cmra
.
(** ** CMRAs with a unit *)
Section
ucmra
.
Context
{
A
:
ucmraT
}.
Implicit
Types
x
y
:
A
.
Lemma
ucmra_update_unit
x
:
x
~~>
∅
.
Proof
.
apply
cmra_total_update
=>
n
z
.
rewrite
left_id
;
apply
cmra_validN_op_r
.
Qed
.
Lemma
ucmra_update_unit_alt
y
:
∅
~~>
y
↔
∀
x
,
x
~~>
y
.
Proof
.
split
;
[
intros
;
trans
∅
|]
;
auto
using
ucmra_update_unit
.
Qed
.
End
ucmra
.
Section
cmra_transport
.
Context
{
A
B
:
cmraT
}
(
H
:
A
=
B
).
Notation
T
:
=
(
cmra_transport
H
).
Lemma
cmra_transport_updateP
(
P
:
A
→
Prop
)
(
Q
:
B
→
Prop
)
x
:
x
~~>
:
P
→
(
∀
y
,
P
y
→
Q
(
T
y
))
→
T
x
~~>
:
Q
.
Proof
.
destruct
H
;
eauto
using
cmra_updateP_weaken
.
Qed
.
Lemma
cmra_transport_updateP'
(
P
:
A
→
Prop
)
x
:
x
~~>
:
P
→
T
x
~~>
:
λ
y
,
∃
y'
,
y
=
cmra_transport
H
y'
∧
P
y'
.
Proof
.
eauto
using
cmra_transport_updateP
.
Qed
.
End
cmra_transport
.
(** * Product *)
Section
prod
.
Context
{
A
B
:
cmraT
}.
Implicit
Types
x
:
A
*
B
.
Lemma
prod_updateP
P1
P2
(
Q
:
A
*
B
→
Prop
)
x
:
x
.
1
~~>
:
P1
→
x
.
2
~~>
:
P2
→
(
∀
a
b
,
P1
a
→
P2
b
→
Q
(
a
,
b
))
→
x
~~>
:
Q
.
Proof
.
intros
Hx1
Hx2
HP
n
mz
[??]
;
simpl
in
*.
destruct
(
Hx1
n
(
fst
<$>
mz
))
as
(
a
&?&?)
;
first
by
destruct
mz
.
destruct
(
Hx2
n
(
snd
<$>
mz
))
as
(
b
&?&?)
;
first
by
destruct
mz
.
exists
(
a
,
b
)
;
repeat
split
;
destruct
mz
;
auto
.
Qed
.
Lemma
prod_updateP'
P1
P2
x
:
x
.
1
~~>
:
P1
→
x
.
2
~~>
:
P2
→
x
~~>
:
λ
y
,
P1
(
y
.
1
)
∧
P2
(
y
.
2
).
Proof
.
eauto
using
prod_updateP
.
Qed
.
Lemma
prod_update
x
y
:
x
.
1
~~>
y
.
1
→
x
.
2
~~>
y
.
2
→
x
~~>
y
.
Proof
.
rewrite
!
cmra_update_updateP
.
destruct
x
,
y
;
eauto
using
prod_updateP
with
subst
.
Qed
.
Global
Instance
prod_local_update
(
LA
:
A
→
A
)
`
{!
LocalUpdate
LvA
LA
}
(
LB
:
B
→
B
)
`
{!
LocalUpdate
LvB
LB
}
:
LocalUpdate
(
λ
x
,
LvA
(
x
.
1
)
∧
LvB
(
x
.
2
))
(
prod_map
LA
LB
).
Proof
.
constructor
.
-
intros
n
x
y
[??]
;
constructor
;
simpl
;
by
apply
local_update_ne
.
-
intros
n
??
[??]
[??]
;
constructor
;
simpl
in
*
;
eapply
local_updateN
;
eauto
.
Qed
.
End
prod
.
(** * Option *)
Section
option
.
Context
{
A
:
cmraT
}.
Implicit
Types
x
y
:
A
.
Global
Instance
option_fmap_local_update
(
L
:
A
→
A
)
Lv
:
LocalUpdate
Lv
L
→
LocalUpdate
(
λ
mx
,
if
mx
is
Some
x
then
Lv
x
else
False
)
(
fmap
L
).
Proof
.
split
;
first
apply
_
.
intros
n
[
x
|]
[
z
|]
;
constructor
;
by
eauto
using
(
local_updateN
L
).
Qed
.
Global
Instance
option_const_local_update
Lv
y
:
LocalUpdate
Lv
(
λ
_
,
y
)
→
LocalUpdate
(
λ
mx
,
if
mx
is
Some
x
then
Lv
x
else
False
)
(
λ
_
,
Some
y
).
Proof
.
split
;
first
apply
_
.
intros
n
[
x
|]
[
z
|]
;
constructor
;
by
eauto
using
(
local_updateN
(
λ
_
,
y
)).
Qed
.
Lemma
option_updateP
(
P
:
A
→
Prop
)
(
Q
:
option
A
→
Prop
)
x
:
x
~~>
:
P
→
(
∀
y
,
P
y
→
Q
(
Some
y
))
→
Some
x
~~>
:
Q
.
Proof
.
intros
Hx
Hy
;
apply
cmra_total_updateP
=>
n
[
y
|]
?.
{
destruct
(
Hx
n
(
Some
y
))
as
(
y'
&?&?)
;
auto
.
exists
(
Some
y'
)
;
auto
.
}
destruct
(
Hx
n
None
)
as
(
y'
&?&?)
;
rewrite
?cmra_core_r
;
auto
.
by
exists
(
Some
y'
)
;
auto
.
Qed
.
Lemma
option_updateP'
(
P
:
A
→
Prop
)
x
:
x
~~>
:
P
→
Some
x
~~>
:
from_option
P
False
.
Proof
.
eauto
using
option_updateP
.
Qed
.
Lemma
option_update
x
y
:
x
~~>
y
→
Some
x
~~>
Some
y
.
Proof
.
rewrite
!
cmra_update_updateP
;
eauto
using
option_updateP
with
congruence
.
Qed
.