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
Iris
Fairis
Commits
f372c5c1
Commit
f372c5c1
authored
Mar 29, 2016
by
Robbert Krebbers
Browse files
Rename algebra/fin_maps.v -> algebra/gmap.v
Also remove some superfluous map_ prefixes.
parent
9fd42107
Changes
8
Hide whitespace changes
Inline
Side-by-side
_CoqProject
View file @
f372c5c1
...
...
@@ -41,7 +41,7 @@ algebra/cmra_big_op.v
algebra/cmra_tactics.v
algebra/sts.v
algebra/auth.v
algebra/
fin_
map
s
.v
algebra/
g
map.v
algebra/cofe.v
algebra/base.v
algebra/dra.v
...
...
algebra/
fin_
map
s
.v
→
algebra/
g
map.v
View file @
f372c5c1
...
...
@@ -6,14 +6,14 @@ Section cofe.
Context
`
{
Countable
K
}
{
A
:
cofeT
}
.
Implicit
Types
m
:
gmap
K
A
.
Instance
map_dist
:
Dist
(
gmap
K
A
)
:=
λ
n
m1
m2
,
Instance
g
map_dist
:
Dist
(
gmap
K
A
)
:=
λ
n
m1
m2
,
∀
i
,
m1
!!
i
≡
{
n
}
≡
m2
!!
i
.
Program
Definition
map_chain
(
c
:
chain
(
gmap
K
A
))
Program
Definition
g
map_chain
(
c
:
chain
(
gmap
K
A
))
(
k
:
K
)
:
chain
(
option
A
)
:=
{|
chain_car
n
:=
c
n
!!
k
|}
.
Next
Obligation
.
by
intros
c
k
n
i
?
;
apply
(
chain_cauchy
c
).
Qed
.
Instance
map_compl
:
Compl
(
gmap
K
A
)
:=
λ
c
,
map_imap
(
λ
i
_
,
compl
(
map_chain
c
i
))
(
c
0
).
Definition
map_cofe_mixin
:
CofeMixin
(
gmap
K
A
).
Instance
g
map_compl
:
Compl
(
gmap
K
A
)
:=
λ
c
,
map_imap
(
λ
i
_
,
compl
(
g
map_chain
c
i
))
(
c
0
).
Definition
g
map_cofe_mixin
:
CofeMixin
(
gmap
K
A
).
Proof
.
split
.
-
intros
m1
m2
;
split
.
...
...
@@ -24,15 +24,15 @@ Proof.
+
by
intros
m1
m2
?
k
.
+
by
intros
m1
m2
m3
??
k
;
trans
(
m2
!!
k
).
-
by
intros
n
m1
m2
?
k
;
apply
dist_S
.
-
intros
n
c
k
;
rewrite
/
compl
/
map_compl
lookup_imap
.
-
intros
n
c
k
;
rewrite
/
compl
/
g
map_compl
lookup_imap
.
feed
inversion
(
λ
H
,
chain_cauchy
c
0
n
H
k
);
simpl
;
auto
with
lia
.
by
rewrite
conv_compl
/=
;
apply
reflexive_eq
.
Qed
.
Canonical
Structure
mapC
:
cofeT
:=
CofeT
map_cofe_mixin
.
Global
Instance
map_discrete
:
Discrete
A
→
Discrete
mapC
.
Canonical
Structure
g
mapC
:
cofeT
:=
CofeT
g
map_cofe_mixin
.
Global
Instance
g
map_discrete
:
Discrete
A
→
Discrete
g
mapC
.
Proof
.
intros
?
m
m
'
?
i
.
by
apply
(
timeless
_
).
Qed
.
(
*
why
doesn
'
t
this
go
automatic
?
*
)
Global
Instance
mapC_leibniz
:
LeibnizEquiv
A
→
LeibnizEquiv
mapC
.
Global
Instance
g
mapC_leibniz
:
LeibnizEquiv
A
→
LeibnizEquiv
g
mapC
.
Proof
.
intros
;
change
(
LeibnizEquiv
(
gmap
K
A
));
apply
_.
Qed
.
Global
Instance
lookup_ne
n
k
:
...
...
@@ -62,47 +62,47 @@ Proof.
[
by
constructor
|
by
apply
lookup_ne
].
Qed
.
Instance
map_empty_timeless
:
Timeless
(
∅
:
gmap
K
A
).
Instance
g
map_empty_timeless
:
Timeless
(
∅
:
gmap
K
A
).
Proof
.
intros
m
Hm
i
;
specialize
(
Hm
i
);
rewrite
lookup_empty
in
Hm
|-
*
.
inversion_clear
Hm
;
constructor
.
Qed
.
Global
Instance
map_lookup_timeless
m
i
:
Timeless
m
→
Timeless
(
m
!!
i
).
Global
Instance
g
map_lookup_timeless
m
i
:
Timeless
m
→
Timeless
(
m
!!
i
).
Proof
.
intros
?
[
x
|
]
Hx
;
[
|
by
symmetry
;
apply
:
timeless
].
assert
(
m
≡
{
0
}
≡
<
[
i
:=
x
]
>
m
)
by
(
by
symmetry
in
Hx
;
inversion
Hx
;
cofe_subst
;
rewrite
insert_id
).
by
rewrite
(
timeless
m
(
<
[
i
:=
x
]
>
m
))
// lookup_insert.
Qed
.
Global
Instance
map_insert_timeless
m
i
x
:
Global
Instance
g
map_insert_timeless
m
i
x
:
Timeless
x
→
Timeless
m
→
Timeless
(
<
[
i
:=
x
]
>
m
).
Proof
.
intros
??
m
'
Hm
j
;
destruct
(
decide
(
i
=
j
));
simplify_map_eq
.
{
by
apply
:
timeless
;
rewrite
-
Hm
lookup_insert
.
}
by
apply
:
timeless
;
rewrite
-
Hm
lookup_insert_ne
.
Qed
.
Global
Instance
map_singleton_timeless
i
x
:
Global
Instance
g
map_singleton_timeless
i
x
:
Timeless
x
→
Timeless
(
{
[
i
:=
x
]
}
:
gmap
K
A
)
:=
_.
End
cofe
.
Arguments
mapC
_
{
_
_
}
_.
Arguments
g
mapC
_
{
_
_
}
_.
(
*
CMRA
*
)
Section
cmra
.
Context
`
{
Countable
K
}
{
A
:
cmraT
}
.
Implicit
Types
m
:
gmap
K
A
.
Instance
map_op
:
Op
(
gmap
K
A
)
:=
merge
op
.
Instance
map_core
:
Core
(
gmap
K
A
)
:=
fmap
core
.
Instance
map_valid
:
Valid
(
gmap
K
A
)
:=
λ
m
,
∀
i
,
✓
(
m
!!
i
).
Instance
map_validN
:
ValidN
(
gmap
K
A
)
:=
λ
n
m
,
∀
i
,
✓
{
n
}
(
m
!!
i
).
Instance
g
map_op
:
Op
(
gmap
K
A
)
:=
merge
op
.
Instance
g
map_core
:
Core
(
gmap
K
A
)
:=
fmap
core
.
Instance
g
map_valid
:
Valid
(
gmap
K
A
)
:=
λ
m
,
∀
i
,
✓
(
m
!!
i
).
Instance
g
map_validN
:
ValidN
(
gmap
K
A
)
:=
λ
n
m
,
∀
i
,
✓
{
n
}
(
m
!!
i
).
Lemma
lookup_op
m1
m2
i
:
(
m1
⋅
m2
)
!!
i
=
m1
!!
i
⋅
m2
!!
i
.
Proof
.
by
apply
lookup_merge
.
Qed
.
Lemma
lookup_core
m
i
:
core
m
!!
i
=
core
(
m
!!
i
).
Proof
.
by
apply
lookup_fmap
.
Qed
.
Lemma
map_included_spec
(
m1
m2
:
gmap
K
A
)
:
m1
≼
m2
↔
∀
i
,
m1
!!
i
≼
m2
!!
i
.
Lemma
g
map_included_spec
(
m1
m2
:
gmap
K
A
)
:
m1
≼
m2
↔
∀
i
,
m1
!!
i
≼
m2
!!
i
.
Proof
.
split
;
[
by
intros
[
m
Hm
]
i
;
exists
(
m
!!
i
);
rewrite
-
lookup_op
Hm
|
].
revert
m2
.
induction
m1
as
[
|
i
x
m
Hi
IH
]
using
map_ind
=>
m2
Hm
.
...
...
@@ -118,7 +118,7 @@ Proof.
lookup_insert_ne
// lookup_partial_alter_ne.
Qed
.
Definition
map_cmra_mixin
:
CMRAMixin
(
gmap
K
A
).
Definition
g
map_cmra_mixin
:
CMRAMixin
(
gmap
K
A
).
Proof
.
split
.
-
by
intros
n
m1
m2
m3
Hm
i
;
rewrite
!
lookup_op
(
Hm
i
).
...
...
@@ -132,7 +132,7 @@ Proof.
-
by
intros
m1
m2
i
;
rewrite
!
lookup_op
comm
.
-
by
intros
m
i
;
rewrite
lookup_op
!
lookup_core
cmra_core_l
.
-
by
intros
m
i
;
rewrite
!
lookup_core
cmra_core_idemp
.
-
intros
x
y
;
rewrite
!
map_included_spec
;
intros
Hm
i
.
-
intros
x
y
;
rewrite
!
g
map_included_spec
;
intros
Hm
i
.
by
rewrite
!
lookup_core
;
apply
cmra_core_preserving
.
-
intros
n
m1
m2
Hm
i
;
apply
cmra_validN_op_l
with
(
m2
!!
i
).
by
rewrite
-
lookup_op
.
...
...
@@ -152,25 +152,25 @@ Proof.
pose
proof
(
Hm12
'
i
)
as
Hm12
''
;
rewrite
Hx
in
Hm12
''
.
by
symmetry
;
apply
option_op_positive_dist_r
with
(
m1
!!
i
).
Qed
.
Canonical
Structure
mapR
:
cmraT
:=
CMRAT
map_cofe_mixin
map_cmra_mixin
.
Global
Instance
map_cmra_unit
:
CMRAUnit
mapR
.
Canonical
Structure
g
mapR
:
cmraT
:=
CMRAT
g
map_cofe_mixin
g
map_cmra_mixin
.
Global
Instance
g
map_cmra_unit
:
CMRAUnit
g
mapR
.
Proof
.
split
.
-
by
intros
i
;
rewrite
lookup_empty
.
-
by
intros
m
i
;
rewrite
/=
lookup_op
lookup_empty
(
left_id_L
None
_
).
-
apply
map_empty_timeless
.
-
apply
g
map_empty_timeless
.
Qed
.
Global
Instance
map_cmra_discrete
:
CMRADiscrete
A
→
CMRADiscrete
mapR
.
Global
Instance
g
map_cmra_discrete
:
CMRADiscrete
A
→
CMRADiscrete
g
mapR
.
Proof
.
split
;
[
apply
_
|
].
intros
m
?
i
.
by
apply
:
cmra_discrete_valid
.
Qed
.
(
**
Internalized
properties
*
)
Lemma
map_equivI
{
M
}
m1
m2
:
(
m1
≡
m2
)
⊣⊢
(
∀
i
,
m1
!!
i
≡
m2
!!
i
:
uPred
M
).
Lemma
g
map_equivI
{
M
}
m1
m2
:
(
m1
≡
m2
)
⊣⊢
(
∀
i
,
m1
!!
i
≡
m2
!!
i
:
uPred
M
).
Proof
.
by
uPred
.
unseal
.
Qed
.
Lemma
map_validI
{
M
}
m
:
(
✓
m
)
⊣⊢
(
∀
i
,
✓
(
m
!!
i
)
:
uPred
M
).
Lemma
g
map_validI
{
M
}
m
:
(
✓
m
)
⊣⊢
(
∀
i
,
✓
(
m
!!
i
)
:
uPred
M
).
Proof
.
by
uPred
.
unseal
.
Qed
.
End
cmra
.
Arguments
mapR
_
{
_
_
}
_.
Arguments
g
mapR
_
{
_
_
}
_.
Section
properties
.
Context
`
{
Countable
K
}
{
A
:
cmraT
}
.
...
...
@@ -178,23 +178,23 @@ Implicit Types m : gmap K A.
Implicit
Types
i
:
K
.
Implicit
Types
a
:
A
.
Lemma
map_
lookup_validN
n
m
i
x
:
✓
{
n
}
m
→
m
!!
i
≡
{
n
}
≡
Some
x
→
✓
{
n
}
x
.
Lemma
lookup_validN
n
m
i
x
:
✓
{
n
}
m
→
m
!!
i
≡
{
n
}
≡
Some
x
→
✓
{
n
}
x
.
Proof
.
by
move
=>
/
(
_
i
)
Hm
Hi
;
move
:
Hm
;
rewrite
Hi
.
Qed
.
Lemma
map_
lookup_valid
m
i
x
:
✓
m
→
m
!!
i
≡
Some
x
→
✓
x
.
Lemma
lookup_valid
m
i
x
:
✓
m
→
m
!!
i
≡
Some
x
→
✓
x
.
Proof
.
move
=>
Hm
Hi
.
move
:
(
Hm
i
).
by
rewrite
Hi
.
Qed
.
Lemma
map_
insert_validN
n
m
i
x
:
✓
{
n
}
x
→
✓
{
n
}
m
→
✓
{
n
}
<
[
i
:=
x
]
>
m
.
Lemma
insert_validN
n
m
i
x
:
✓
{
n
}
x
→
✓
{
n
}
m
→
✓
{
n
}
<
[
i
:=
x
]
>
m
.
Proof
.
by
intros
??
j
;
destruct
(
decide
(
i
=
j
));
simplify_map_eq
.
Qed
.
Lemma
map_
insert_valid
m
i
x
:
✓
x
→
✓
m
→
✓
<
[
i
:=
x
]
>
m
.
Lemma
insert_valid
m
i
x
:
✓
x
→
✓
m
→
✓
<
[
i
:=
x
]
>
m
.
Proof
.
by
intros
??
j
;
destruct
(
decide
(
i
=
j
));
simplify_map_eq
.
Qed
.
Lemma
map_
singleton_validN
n
i
x
:
✓
{
n
}
(
{
[
i
:=
x
]
}
:
gmap
K
A
)
↔
✓
{
n
}
x
.
Lemma
singleton_validN
n
i
x
:
✓
{
n
}
(
{
[
i
:=
x
]
}
:
gmap
K
A
)
↔
✓
{
n
}
x
.
Proof
.
split
;
[
|
by
intros
;
apply
map_
insert_validN
,
cmra_unit_validN
].
split
;
[
|
by
intros
;
apply
insert_validN
,
cmra_unit_validN
].
by
move
=>/
(
_
i
);
simplify_map_eq
.
Qed
.
Lemma
map_
singleton_valid
i
x
:
✓
(
{
[
i
:=
x
]
}
:
gmap
K
A
)
↔
✓
x
.
Proof
.
rewrite
!
cmra_valid_validN
.
by
setoid_rewrite
map_
singleton_validN
.
Qed
.
Lemma
singleton_valid
i
x
:
✓
(
{
[
i
:=
x
]
}
:
gmap
K
A
)
↔
✓
x
.
Proof
.
rewrite
!
cmra_valid_validN
.
by
setoid_rewrite
singleton_validN
.
Qed
.
Lemma
map_
insert_singleton_opN
n
m
i
x
:
Lemma
insert_singleton_opN
n
m
i
x
:
m
!!
i
=
None
∨
m
!!
i
≡
{
n
}
≡
Some
(
core
x
)
→
<
[
i
:=
x
]
>
m
≡
{
n
}
≡
{
[
i
:=
x
]
}
⋅
m
.
Proof
.
intros
Hi
j
;
destruct
(
decide
(
i
=
j
))
as
[
->|
];
...
...
@@ -202,24 +202,22 @@ Proof.
rewrite
lookup_op
lookup_insert
lookup_singleton
.
by
destruct
Hi
as
[
->|
->
];
constructor
;
rewrite
?
cmra_core_r
.
Qed
.
Lemma
map_
insert_singleton_op
m
i
x
:
Lemma
insert_singleton_op
m
i
x
:
m
!!
i
=
None
∨
m
!!
i
≡
Some
(
core
x
)
→
<
[
i
:=
x
]
>
m
≡
{
[
i
:=
x
]
}
⋅
m
.
Proof
.
rewrite
!
equiv_dist
;
naive_solver
eauto
using
map_insert_singleton_opN
.
Qed
.
Proof
.
rewrite
!
equiv_dist
;
naive_solver
eauto
using
insert_singleton_opN
.
Qed
.
Lemma
map_
core_singleton
(
i
:
K
)
(
x
:
A
)
:
Lemma
core_singleton
(
i
:
K
)
(
x
:
A
)
:
core
(
{
[
i
:=
x
]
}
:
gmap
K
A
)
=
{
[
i
:=
core
x
]
}
.
Proof
.
apply
map_fmap_singleton
.
Qed
.
Lemma
map_
op_singleton
(
i
:
K
)
(
x
y
:
A
)
:
Lemma
op_singleton
(
i
:
K
)
(
x
y
:
A
)
:
{
[
i
:=
x
]
}
⋅
{
[
i
:=
y
]
}
=
(
{
[
i
:=
x
⋅
y
]
}
:
gmap
K
A
).
Proof
.
by
apply
(
merge_singleton
_
_
_
x
y
).
Qed
.
Global
Instance
map_persistent
m
:
(
∀
x
:
A
,
Persistent
x
)
→
Persistent
m
.
Global
Instance
g
map_persistent
m
:
(
∀
x
:
A
,
Persistent
x
)
→
Persistent
m
.
Proof
.
intros
?
i
.
by
rewrite
lookup_core
persistent
.
Qed
.
Global
Instance
map_singleton_persistent
i
(
x
:
A
)
:
Global
Instance
g
map_singleton_persistent
i
(
x
:
A
)
:
Persistent
x
→
Persistent
{
[
i
:=
x
]
}
.
Proof
.
intros
.
by
rewrite
/
Persistent
map_
core_singleton
persistent
.
Qed
.
Proof
.
intros
.
by
rewrite
/
Persistent
core_singleton
persistent
.
Qed
.
Lemma
singleton_includedN
n
m
i
x
:
{
[
i
:=
x
]
}
≼
{
n
}
m
↔
∃
y
,
m
!!
i
≡
{
n
}
≡
Some
y
∧
x
≼
{
n
}
y
.
...
...
@@ -234,14 +232,14 @@ Proof.
+
rewrite
Hi
lookup_op
lookup_singleton
lookup_insert
.
by
constructor
.
+
by
rewrite
lookup_op
lookup_singleton_ne
// lookup_insert_ne // left_id.
Qed
.
Lemma
map_
dom_op
m1
m2
:
dom
(
gset
K
)
(
m1
⋅
m2
)
≡
dom
_
m1
∪
dom
_
m2
.
Lemma
dom_op
m1
m2
:
dom
(
gset
K
)
(
m1
⋅
m2
)
≡
dom
_
m1
∪
dom
_
m2
.
Proof
.
apply
elem_of_equiv
;
intros
i
;
rewrite
elem_of_union
!
elem_of_dom
.
unfold
is_Some
;
setoid_rewrite
lookup_op
.
destruct
(
m1
!!
i
),
(
m2
!!
i
);
naive_solver
.
Qed
.
Lemma
map_
insert_updateP
(
P
:
A
→
Prop
)
(
Q
:
gmap
K
A
→
Prop
)
m
i
x
:
Lemma
insert_updateP
(
P
:
A
→
Prop
)
(
Q
:
gmap
K
A
→
Prop
)
m
i
x
:
x
~~>:
P
→
(
∀
y
,
P
y
→
Q
(
<
[
i
:=
y
]
>
m
))
→
<
[
i
:=
x
]
>
m
~~>:
Q
.
Proof
.
intros
Hx
%
option_updateP
'
HP
n
mf
Hm
.
...
...
@@ -251,24 +249,22 @@ Proof.
intros
j
;
move
:
(
Hm
j
)
=>{
Hm
}
;
rewrite
!
lookup_op
=>
Hm
.
destruct
(
decide
(
i
=
j
));
simplify_map_eq
/=
;
auto
.
Qed
.
Lemma
map_
insert_updateP
'
(
P
:
A
→
Prop
)
m
i
x
:
Lemma
insert_updateP
'
(
P
:
A
→
Prop
)
m
i
x
:
x
~~>:
P
→
<
[
i
:=
x
]
>
m
~~>:
λ
m
'
,
∃
y
,
m
'
=
<
[
i
:=
y
]
>
m
∧
P
y
.
Proof
.
eauto
using
map_insert_updateP
.
Qed
.
Lemma
map_insert_update
m
i
x
y
:
x
~~>
y
→
<
[
i
:=
x
]
>
m
~~>
<
[
i
:=
y
]
>
m
.
Proof
.
rewrite
!
cmra_update_updateP
;
eauto
using
map_insert_updateP
with
subst
.
Qed
.
Proof
.
eauto
using
insert_updateP
.
Qed
.
Lemma
insert_update
m
i
x
y
:
x
~~>
y
→
<
[
i
:=
x
]
>
m
~~>
<
[
i
:=
y
]
>
m
.
Proof
.
rewrite
!
cmra_update_updateP
;
eauto
using
insert_updateP
with
subst
.
Qed
.
Lemma
map_
singleton_updateP
(
P
:
A
→
Prop
)
(
Q
:
gmap
K
A
→
Prop
)
i
x
:
Lemma
singleton_updateP
(
P
:
A
→
Prop
)
(
Q
:
gmap
K
A
→
Prop
)
i
x
:
x
~~>:
P
→
(
∀
y
,
P
y
→
Q
{
[
i
:=
y
]
}
)
→
{
[
i
:=
x
]
}
~~>:
Q
.
Proof
.
apply
map_
insert_updateP
.
Qed
.
Lemma
map_
singleton_updateP
'
(
P
:
A
→
Prop
)
i
x
:
Proof
.
apply
insert_updateP
.
Qed
.
Lemma
singleton_updateP
'
(
P
:
A
→
Prop
)
i
x
:
x
~~>:
P
→
{
[
i
:=
x
]
}
~~>:
λ
m
,
∃
y
,
m
=
{
[
i
:=
y
]
}
∧
P
y
.
Proof
.
apply
map_
insert_updateP
'
.
Qed
.
Lemma
map_
singleton_update
i
(
x
y
:
A
)
:
x
~~>
y
→
{
[
i
:=
x
]
}
~~>
{
[
i
:=
y
]
}
.
Proof
.
apply
map_
insert_update
.
Qed
.
Proof
.
apply
insert_updateP
'
.
Qed
.
Lemma
singleton_update
i
(
x
y
:
A
)
:
x
~~>
y
→
{
[
i
:=
x
]
}
~~>
{
[
i
:=
y
]
}
.
Proof
.
apply
insert_update
.
Qed
.
Lemma
map_
singleton_updateP_empty
`
{
Empty
A
,
!
CMRAUnit
A
}
Lemma
singleton_updateP_empty
`
{
Empty
A
,
!
CMRAUnit
A
}
(
P
:
A
→
Prop
)
(
Q
:
gmap
K
A
→
Prop
)
i
:
∅
~~>:
P
→
(
∀
y
,
P
y
→
Q
{
[
i
:=
y
]
}
)
→
∅
~~>:
Q
.
Proof
.
...
...
@@ -283,34 +279,34 @@ Proof.
by
rewrite
right_id
.
-
move
:
(
Hg
i
'
).
by
rewrite
!
lookup_op
lookup_singleton_ne
// !left_id.
Qed
.
Lemma
map_
singleton_updateP_empty
'
`
{
Empty
A
,
!
CMRAUnit
A
}
(
P
:
A
→
Prop
)
i
:
Lemma
singleton_updateP_empty
'
`
{
Empty
A
,
!
CMRAUnit
A
}
(
P
:
A
→
Prop
)
i
:
∅
~~>:
P
→
∅
~~>:
λ
m
,
∃
y
,
m
=
{
[
i
:=
y
]
}
∧
P
y
.
Proof
.
eauto
using
map_
singleton_updateP_empty
.
Qed
.
Proof
.
eauto
using
singleton_updateP_empty
.
Qed
.
Section
freshness
.
Context
`
{
Fresh
K
(
gset
K
),
!
FreshSpec
K
(
gset
K
)
}
.
Lemma
map_
updateP_alloc_strong
(
Q
:
gmap
K
A
→
Prop
)
(
I
:
gset
K
)
m
x
:
Lemma
updateP_alloc_strong
(
Q
:
gmap
K
A
→
Prop
)
(
I
:
gset
K
)
m
x
:
✓
x
→
(
∀
i
,
m
!!
i
=
None
→
i
∉
I
→
Q
(
<
[
i
:=
x
]
>
m
))
→
m
~~>:
Q
.
Proof
.
intros
?
HQ
n
mf
Hm
.
set
(
i
:=
fresh
(
I
∪
dom
(
gset
K
)
(
m
⋅
mf
))).
assert
(
i
∉
I
∧
i
∉
dom
(
gset
K
)
m
∧
i
∉
dom
(
gset
K
)
mf
)
as
[
?
[
??
]].
{
rewrite
-
not_elem_of_union
-
map_
dom_op
-
not_elem_of_union
;
apply
is_fresh
.
}
{
rewrite
-
not_elem_of_union
-
dom_op
-
not_elem_of_union
;
apply
is_fresh
.
}
exists
(
<
[
i
:=
x
]
>
m
);
split
.
{
by
apply
HQ
;
last
done
;
apply
not_elem_of_dom
.
}
rewrite
map_
insert_singleton_opN
;
last
by
left
;
apply
not_elem_of_dom
.
rewrite
-
assoc
-
map_
insert_singleton_opN
;
last
by
left
;
apply
not_elem_of_dom
;
rewrite
map_
dom_op
not_elem_of_union
.
by
apply
map_
insert_validN
;
[
apply
cmra_valid_validN
|
].
rewrite
insert_singleton_opN
;
last
by
left
;
apply
not_elem_of_dom
.
rewrite
-
assoc
-
insert_singleton_opN
;
last
by
left
;
apply
not_elem_of_dom
;
rewrite
dom_op
not_elem_of_union
.
by
apply
insert_validN
;
[
apply
cmra_valid_validN
|
].
Qed
.
Lemma
map_
updateP_alloc
(
Q
:
gmap
K
A
→
Prop
)
m
x
:
Lemma
updateP_alloc
(
Q
:
gmap
K
A
→
Prop
)
m
x
:
✓
x
→
(
∀
i
,
m
!!
i
=
None
→
Q
(
<
[
i
:=
x
]
>
m
))
→
m
~~>:
Q
.
Proof
.
move
=>??
.
eapply
map_
updateP_alloc_strong
with
(
I
:=
∅
);
by
eauto
.
Qed
.
Lemma
map_
updateP_alloc_strong
'
m
x
(
I
:
gset
K
)
:
Proof
.
move
=>??
.
eapply
updateP_alloc_strong
with
(
I
:=
∅
);
by
eauto
.
Qed
.
Lemma
updateP_alloc_strong
'
m
x
(
I
:
gset
K
)
:
✓
x
→
m
~~>:
λ
m
'
,
∃
i
,
i
∉
I
∧
m
'
=
<
[
i
:=
x
]
>
m
∧
m
!!
i
=
None
.
Proof
.
eauto
using
map_
updateP_alloc_strong
.
Qed
.
Lemma
map_
updateP_alloc
'
m
x
:
Proof
.
eauto
using
updateP_alloc_strong
.
Qed
.
Lemma
updateP_alloc
'
m
x
:
✓
x
→
m
~~>:
λ
m
'
,
∃
i
,
m
'
=
<
[
i
:=
x
]
>
m
∧
m
!!
i
=
None
.
Proof
.
eauto
using
map_
updateP_alloc
.
Qed
.
Proof
.
eauto
using
updateP_alloc
.
Qed
.
End
freshness
.
(
*
Allocation
is
a
local
update
:
Just
use
composition
with
a
singleton
map
.
*
)
...
...
@@ -319,7 +315,7 @@ End freshness.
deallocation
.
*
)
(
*
Applying
a
local
update
at
a
position
we
own
is
a
local
update
.
*
)
Global
Instance
map_alter_update
`
{!
LocalUpdate
Lv
L
}
i
:
Global
Instance
g
map_alter_update
`
{!
LocalUpdate
Lv
L
}
i
:
LocalUpdate
(
λ
m
,
∃
x
,
m
!!
i
=
Some
x
∧
Lv
x
)
(
alter
L
i
).
Proof
.
split
;
first
apply
_.
...
...
@@ -332,32 +328,32 @@ Qed.
End
properties
.
(
**
Functor
*
)
Instance
map_fmap_ne
`
{
Countable
K
}
{
A
B
:
cofeT
}
(
f
:
A
→
B
)
n
:
Instance
g
map_fmap_ne
`
{
Countable
K
}
{
A
B
:
cofeT
}
(
f
:
A
→
B
)
n
:
Proper
(
dist
n
==>
dist
n
)
f
→
Proper
(
dist
n
==>
dist
n
)
(
fmap
(
M
:=
gmap
K
)
f
).
Proof
.
by
intros
?
m
m
'
Hm
k
;
rewrite
!
lookup_fmap
;
apply
option_fmap_ne
.
Qed
.
Instance
map_fmap_cmra_monotone
`
{
Countable
K
}
{
A
B
:
cmraT
}
(
f
:
A
→
B
)
Instance
g
map_fmap_cmra_monotone
`
{
Countable
K
}
{
A
B
:
cmraT
}
(
f
:
A
→
B
)
`
{!
CMRAMonotone
f
}
:
CMRAMonotone
(
fmap
f
:
gmap
K
A
→
gmap
K
B
).
Proof
.
split
;
try
apply
_.
-
by
intros
n
m
?
i
;
rewrite
lookup_fmap
;
apply
(
validN_preserving
_
).
-
intros
m1
m2
;
rewrite
!
map_included_spec
=>
Hm
i
.
-
intros
m1
m2
;
rewrite
!
g
map_included_spec
=>
Hm
i
.
by
rewrite
!
lookup_fmap
;
apply
:
included_preserving
.
Qed
.
Definition
mapC_map
`
{
Countable
K
}
{
A
B
}
(
f
:
A
-
n
>
B
)
:
mapC
K
A
-
n
>
mapC
K
B
:=
CofeMor
(
fmap
f
:
mapC
K
A
→
mapC
K
B
).
Instance
mapC_map_ne
`
{
Countable
K
}
{
A
B
}
n
:
Proper
(
dist
n
==>
dist
n
)
(
@
mapC_map
K
_
_
A
B
).
Definition
g
mapC_map
`
{
Countable
K
}
{
A
B
}
(
f
:
A
-
n
>
B
)
:
gmapC
K
A
-
n
>
gmapC
K
B
:=
CofeMor
(
fmap
f
:
g
mapC
K
A
→
g
mapC
K
B
).
Instance
g
mapC_map_ne
`
{
Countable
K
}
{
A
B
}
n
:
Proper
(
dist
n
==>
dist
n
)
(
@
g
mapC_map
K
_
_
A
B
).
Proof
.
intros
f
g
Hf
m
k
;
rewrite
/=
!
lookup_fmap
.
destruct
(
_
!!
k
)
eqn
:?
;
simpl
;
constructor
;
apply
Hf
.
Qed
.
Program
Definition
mapCF
K
`
{
Countable
K
}
(
F
:
cFunctor
)
:
cFunctor
:=
{|
cFunctor_car
A
B
:=
mapC
K
(
cFunctor_car
F
A
B
);
cFunctor_map
A1
A2
B1
B2
fg
:=
mapC_map
(
cFunctor_map
F
fg
)
Program
Definition
g
mapCF
K
`
{
Countable
K
}
(
F
:
cFunctor
)
:
cFunctor
:=
{|
cFunctor_car
A
B
:=
g
mapC
K
(
cFunctor_car
F
A
B
);
cFunctor_map
A1
A2
B1
B2
fg
:=
g
mapC_map
(
cFunctor_map
F
fg
)
|}
.
Next
Obligation
.
by
intros
K
??
F
A1
A2
B1
B2
n
f
g
Hfg
;
apply
mapC_map_ne
,
cFunctor_ne
.
by
intros
K
??
F
A1
A2
B1
B2
n
f
g
Hfg
;
apply
g
mapC_map_ne
,
cFunctor_ne
.
Qed
.
Next
Obligation
.
intros
K
??
F
A
B
x
.
rewrite
/=
-{
2
}
(
map_fmap_id
x
).
...
...
@@ -367,18 +363,18 @@ Next Obligation.
intros
K
??
F
A1
A2
A3
B1
B2
B3
f
g
f
'
g
'
x
.
rewrite
/=
-
map_fmap_compose
.
apply
map_fmap_setoid_ext
=>
y
??
;
apply
cFunctor_compose
.
Qed
.
Instance
mapCF_contractive
K
`
{
Countable
K
}
F
:
cFunctorContractive
F
→
cFunctorContractive
(
mapCF
K
F
).
Instance
g
mapCF_contractive
K
`
{
Countable
K
}
F
:
cFunctorContractive
F
→
cFunctorContractive
(
g
mapCF
K
F
).
Proof
.
by
intros
?
A1
A2
B1
B2
n
f
g
Hfg
;
apply
mapC_map_ne
,
cFunctor_contractive
.
by
intros
?
A1
A2
B1
B2
n
f
g
Hfg
;
apply
g
mapC_map_ne
,
cFunctor_contractive
.
Qed
.
Program
Definition
mapRF
K
`
{
Countable
K
}
(
F
:
rFunctor
)
:
rFunctor
:=
{|
rFunctor_car
A
B
:=
mapR
K
(
rFunctor_car
F
A
B
);
rFunctor_map
A1
A2
B1
B2
fg
:=
mapC_map
(
rFunctor_map
F
fg
)
Program
Definition
g
mapRF
K
`
{
Countable
K
}
(
F
:
rFunctor
)
:
rFunctor
:=
{|
rFunctor_car
A
B
:=
g
mapR
K
(
rFunctor_car
F
A
B
);
rFunctor_map
A1
A2
B1
B2
fg
:=
g
mapC_map
(
rFunctor_map
F
fg
)
|}
.
Next
Obligation
.
by
intros
K
??
F
A1
A2
B1
B2
n
f
g
Hfg
;
apply
mapC_map_ne
,
rFunctor_ne
.
by
intros
K
??
F
A1
A2
B1
B2
n
f
g
Hfg
;
apply
g
mapC_map_ne
,
rFunctor_ne
.
Qed
.
Next
Obligation
.
intros
K
??
F
A
B
x
.
rewrite
/=
-{
2
}
(
map_fmap_id
x
).
...
...
@@ -388,8 +384,8 @@ Next Obligation.
intros
K
??
F
A1
A2
A3
B1
B2
B3
f
g
f
'
g
'
x
.
rewrite
/=
-
map_fmap_compose
.
apply
map_fmap_setoid_ext
=>
y
??
;
apply
rFunctor_compose
.
Qed
.
Instance
mapRF_contractive
K
`
{
Countable
K
}
F
:
rFunctorContractive
F
→
rFunctorContractive
(
mapRF
K
F
).
Instance
g
mapRF_contractive
K
`
{
Countable
K
}
F
:
rFunctorContractive
F
→
rFunctorContractive
(
g
mapRF
K
F
).
Proof
.
by
intros
?
A1
A2
B1
B2
n
f
g
Hfg
;
apply
mapC_map_ne
,
rFunctor_contractive
.
by
intros
?
A1
A2
B1
B2
n
f
g
Hfg
;
apply
g
mapC_map_ne
,
rFunctor_contractive
.
Qed
.
heap_lang/lib/heap.v
View file @
f372c5c1
...
...
@@ -7,7 +7,7 @@ Import uPred.
a
finmap
as
their
state
.
Or
maybe
even
beyond
"as their state"
,
i
.
e
.
arbitrary
predicates
over
finmaps
instead
of
just
ownP
.
*
)
Definition
heapR
:
cmraT
:=
mapR
loc
(
fracR
(
dec_agreeR
val
)).
Definition
heapR
:
cmraT
:=
g
mapR
loc
(
fracR
(
dec_agreeR
val
)).
(
**
The
CMRA
we
need
.
*
)
Class
heapG
Σ
:=
HeapG
{
...
...
@@ -108,9 +108,9 @@ Section heap.
induction
σ
as
[
|
l
v
σ
Hl
IH
]
using
map_ind
.
{
rewrite
big_sepM_empty
;
apply
True_intro
.
}
rewrite
to_heap_insert
big_sepM_insert
//.
rewrite
(
map_
insert_singleton_op
(
to_heap
σ
));
rewrite
(
insert_singleton_op
(
to_heap
σ
));
last
by
rewrite
lookup_fmap
Hl
;
auto
.
by
rewrite
auth_own_op
IH
.
by
rewrite
auth_own_op
IH
.
Qed
.
Context
`
{
heapG
Σ
}
.
...
...
@@ -121,16 +121,16 @@ Section heap.
Lemma
heap_mapsto_op_eq
l
q1
q2
v
:
(
l
↦
{
q1
}
v
★
l
↦
{
q2
}
v
)
⊣⊢
(
l
↦
{
q1
+
q2
}
v
).
Proof
.
by
rewrite
-
auth_own_op
map_
op_singleton
Frac_op
dec_agree_idemp
.
Qed
.
Proof
.
by
rewrite
-
auth_own_op
op_singleton
Frac_op
dec_agree_idemp
.
Qed
.
Lemma
heap_mapsto_op
l
q1
q2
v1
v2
:
(
l
↦
{
q1
}
v1
★
l
↦
{
q2
}
v2
)
⊣⊢
(
v1
=
v2
∧
l
↦
{
q1
+
q2
}
v1
).
Proof
.
destruct
(
decide
(
v1
=
v2
))
as
[
->|
].
{
by
rewrite
heap_mapsto_op_eq
const_equiv
// left_id. }
rewrite
-
auth_own_op
map_
op_singleton
Frac_op
dec_agree_ne
//.
rewrite
-
auth_own_op
op_singleton
Frac_op
dec_agree_ne
//.
apply
(
anti_symm
(
⊢
));
last
by
apply
const_elim_l
.
rewrite
auth_own_valid
map_validI
(
forall_elim
l
)
lookup_singleton
.
rewrite
auth_own_valid
g
map_validI
(
forall_elim
l
)
lookup_singleton
.
rewrite
option_validI
frac_validI
discrete_valid
.
by
apply
const_elim_r
.
Qed
.
...
...
@@ -160,8 +160,8 @@ Section heap.
repeat
erewrite
<-
exist_intro
by
apply
_
;
simpl
.
rewrite
-
of_heap_insert
left_id
right_id
.
rewrite
/
heap_mapsto
.
ecancel
[
_
-
★
Φ
_
]
%
I
.
rewrite
-
(
map_
insert_singleton_op
h
);
last
by
apply
of_heap_None
.
rewrite
const_equiv
;
last
by
apply
(
map_
insert_valid
h
).
rewrite
-
(
insert_singleton_op
h
);
last
by
apply
of_heap_None
.
rewrite
const_equiv
;
last
by
apply
(
insert_valid
h
).
by
rewrite
left_id
-
later_intro
.
Qed
.
...
...
program_logic/ghost_ownership.v
View file @
f372c5c1
...
...
@@ -12,7 +12,7 @@ Typeclasses Opaque to_globalF own.
(
**
Properties
about
ghost
ownership
*
)
Section
global
.
Context
`
{
i
:
inG
Λ
Σ
A
}
.
Context
`
{
inG
Λ
Σ
A
}
.
Implicit
Types
a
:
A
.
(
**
*
Transport
empty
*
)
...
...
@@ -35,12 +35,12 @@ Global Instance own_proper γ : Proper ((≡) ==> (⊣⊢)) (own γ) := ne_prope
Lemma
own_op
γ
a1
a2
:
own
γ
(
a1
⋅
a2
)
⊣⊢
(
own
γ
a1
★
own
γ
a2
).
Proof
.
by
rewrite
/
own
-
ownG_op
to_globalF_op
.
Qed
.
Global
Instance
own_mono
γ
:
Proper
(
flip
(
≼
)
==>
(
⊢
))
(
own
γ
).
Proof
.
move
=>
a
b
[
c
H
].
rewrite
H
own_op
.
eauto
with
I
.
Qed
.
Proof
.
move
=>
a
b
[
c
->
].
rewrite
own_op
.
eauto
with
I
.
Qed
.
Lemma
own_valid
γ
a
:
own
γ
a
⊢
✓
a
.
Proof
.
rewrite
/
own
ownG_valid
/
to_globalF
.
rewrite
iprod_validI
(
forall_elim
inG_id
)
iprod_lookup_singleton
.
rewrite
map_validI
(
forall_elim
γ
)
lookup_singleton
option_validI
.
rewrite
g
map_validI
(
forall_elim
γ
)
lookup_singleton
option_validI
.
(
*
implicit
arguments
differ
a
bit
*
)
by
trans
(
✓
cmra_transport
inG_prf
a
:
iPropG
Λ
Σ
)
%
I
;
last
destruct
inG_prf
.
Qed
.
...
...
@@ -60,8 +60,9 @@ Lemma own_alloc_strong a E (G : gset gname) :
Proof
.
intros
Ha
.
rewrite
-
(
pvs_mono
_
_
(
∃
m
,
■
(
∃
γ
,
γ
∉
G
∧
m
=
to_globalF
γ
a
)
∧
ownG
m
)
%
I
).
-
rewrite
ownG_empty
.
eapply
pvs_ownG_updateP
,
(
iprod_singleton_updateP_empty
inG_id
);
first
(
eapply
map_updateP_alloc_strong
'
,
cmra_transport_valid
,
Ha
);
-
rewrite
ownG_empty
.
eapply
pvs_ownG_updateP
,
(
iprod_singleton_updateP_empty
inG_id
);
first
(
eapply
updateP_alloc_strong
'
,
cmra_transport_valid
,
Ha
);
naive_solver
.
-
apply
exist_elim
=>
m
;
apply
const_elim_l
=>-
[
γ
[
Hfresh
->
]].
by
rewrite
-
(
exist_intro
γ
)
const_equiv
// left_id.
...
...
@@ -78,7 +79,7 @@ Proof.
intros
Ha
.
rewrite
-
(
pvs_mono
_
_
(
∃
m
,
■
(
∃
a
'
,
m
=
to_globalF
γ
a
'
∧
P
a
'
)
∧
ownG
m
)
%
I
).
-
eapply
pvs_ownG_updateP
,
iprod_singleton_updateP
;
first
by
(
eapply
map_
singleton_updateP
'
,
cmra_transport_updateP
'
,
Ha
).
first
by
(
eapply
singleton_updateP
'
,
cmra_transport_updateP
'
,
Ha
).
naive_solver
.
-
apply
exist_elim
=>
m
;
apply
const_elim_l
=>-
[
a
'
[
->
HP
]].
rewrite
-
(
exist_intro
a
'
).
by
apply
and_intro
;
[
apply
const_intro
|
].
...
...
@@ -90,13 +91,12 @@ Proof.
by
apply
pvs_mono
,
exist_elim
=>
a
''
;
apply
const_elim_l
=>
->
.
Qed
.
Lemma
own_empty
`
{
Empty
A
,
!
CMRAUnit
A
}
γ
E
:
True
⊢
(
|={
E
}=>
own
γ
∅
).
Lemma
own_empty
`
{
Empty
A
,
!
CMRAUnit
A
}
γ
E
:
True
⊢
(
|={
E
}=>
own
γ
∅
).
Proof
.
rewrite
ownG_empty
/
own
.
apply
pvs_ownG_update
,
cmra_update_updateP
.
eapply
iprod_singleton_updateP_empty
;
first
by
eapply
map_
singleton_updateP_empty
'
,
cmra_transport_updateP
'
,
cmra_update_updateP
,
cmra_update_unit
.
first
by
eapply
singleton_updateP_empty
'
,
cmra_transport_updateP
'
,
cmra_update_updateP
,
cmra_update_unit
.
naive_solver
.
Qed
.
End
global
.
program_logic/global_functor.v
View file @
f372c5c1
...
...
@@ -18,7 +18,7 @@ Definition gid (Σ : gFunctors) := fin (projT1 Σ).
Definition
gname
:=
positive
.
Definition
globalF
(
Σ
:
gFunctors
)
:
iFunctor
:=
IFunctor
(
iprodRF
(
λ
i
,
mapRF
gname
(
projT2
Σ
i
))).
IFunctor
(
iprodRF
(
λ
i
,
g
mapRF
gname
(
projT2
Σ
i
))).
Notation
iPropG
Λ
Σ
:=
(
iProp
Λ
(
globalF
Σ
)).
Class
inG
(
Λ
:
language
)
(
Σ
:
gFunctors
)
(
A
:
cmraT
)
:=
InG
{
...
...
@@ -39,7 +39,7 @@ Proof. by intros a a' Ha; apply iprod_singleton_ne; rewrite Ha. Qed.
Lemma
to_globalF_op
γ
a1
a2
:
to_globalF
γ
(
a1
⋅
a2
)
≡
to_globalF
γ
a1
⋅
to_globalF
γ
a2
.
Proof
.
by
rewrite
/
to_globalF
iprod_op_singleton
map_
op_singleton
cmra_transport_op
.
by
rewrite
/
to_globalF
iprod_op_singleton
op_singleton
cmra_transport_op
.
Qed
.
Global
Instance
to_globalF_timeless
γ
m
:
Timeless
m
→
Timeless
(
to_globalF
γ
m
).
Proof
.
rewrite
/
to_globalF
;
apply
_.
Qed
.
...
...
program_logic/ownership.v
View file @
f372c5c1
...
...
@@ -65,7 +65,7 @@ Proof.
rewrite
/
uPred_holds
/=
res_includedN
/=
singleton_includedN
;
split
.
-
intros
[(
P
'
&
Hi
&
HP
)
_
];
rewrite
Hi
.
apply
Some_dist
,
symmetry
,
agree_valid_includedN
;
last
done
.
by
apply
map_
lookup_validN
with
(
wld
r
)
i
.
by
apply
lookup_validN
with
(
wld
r
)
i
.
-
intros
?
;
split_and
?
;
try
apply
cmra_unit_leastN
;
eauto
.
Qed
.
Lemma
ownP_spec
n
r
σ
:
✓
{
n
}
r
→
(
ownP
σ
)
n
r
↔
pst
r
≡
Excl
σ
.
...
...
program_logic/resources.v
View file @
f372c5c1
From
iris
.
algebra
Require
Export
fin_
map
s
agree
excl
.
From
iris
.
algebra
Require
Export
g
map
agree
excl
.
From
iris
.
algebra
Require
Import
upred
.
From
iris
.
program_logic
Require
Export
language
.
Record
res
(
Λ
:
language
)
(
A
:
cofeT
)
(
M
:
cmraT
)
:=
Res
{
wld
:
mapR
positive
(
agreeR
A
);
wld
:
g
mapR
positive
(
agreeR
A
);
pst
:
exclR
(
stateC
Λ
);
gst
:
M
;
}
.
...
...
@@ -216,7 +216,7 @@ Instance resC_map_ne {Λ A A' M M'} n :
Proper
(
dist
n
==>
dist
n
==>
dist
n
)
(
@
resC_map
Λ
A
A
'
M
M
'
).
Proof
.
intros
f
g
Hfg
r
;
split
;
simpl
;
auto
.
-
by
apply
(
mapC_map_ne
_
(
agreeC_map
f
)
(
agreeC_map
g
)),
agreeC_map_ne
.