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
Marianna Rapoport
iris-coq
Commits
7c1de72a
Commit
7c1de72a
authored
Sep 06, 2016
by
Robbert Krebbers
Browse files
Non-disjoint CMRA structure on gset and coPset disj.
I had to perform some renaming to avoid name clashes.
parent
f038b880
Changes
5
Hide whitespace changes
Inline
Side-by-side
algebra/coPset.v
View file @
7c1de72a
From
iris
.
algebra
Require
Export
cmra
.
From
iris
.
algebra
Require
Import
updates
local_updates
.
From
iris
.
prelude
Require
Export
collections
coPset
.
(** This is pretty much the same as algebra/gset, but I was not able to
generalize the construction without breaking canonical structures. *)
(* The union CMRA *)
Section
coPset
.
Implicit
Types
X
Y
:
coPset
.
Canonical
Structure
coPsetC
:
=
leibnizC
coPset
.
Instance
coPset_valid
:
Valid
coPset
:
=
λ
_
,
True
.
Instance
coPset_op
:
Op
coPset
:
=
union
.
Instance
coPset_pcore
:
PCore
coPset
:
=
λ
_
,
Some
∅
.
Lemma
coPset_op_union
X
Y
:
X
⋅
Y
=
X
∪
Y
.
Proof
.
done
.
Qed
.
Lemma
coPset_core_empty
X
:
core
X
=
∅
.
Proof
.
done
.
Qed
.
Lemma
coPset_included
X
Y
:
X
≼
Y
↔
X
⊆
Y
.
Proof
.
split
.
-
intros
[
Z
->].
rewrite
coPset_op_union
.
set_solver
.
-
intros
(
Z
&->&?)%
subseteq_disjoint_union_L
.
by
exists
Z
.
Qed
.
Lemma
coPset_ra_mixin
:
RAMixin
coPset
.
Proof
.
apply
ra_total_mixin
;
eauto
.
-
solve_proper
.
-
solve_proper
.
-
solve_proper
.
-
intros
X1
X2
X3
.
by
rewrite
!
coPset_op_union
assoc_L
.
-
intros
X1
X2
.
by
rewrite
!
coPset_op_union
comm_L
.
-
intros
X
.
by
rewrite
coPset_op_union
coPset_core_empty
left_id_L
.
-
intros
X1
X2
_
.
by
rewrite
coPset_included
!
coPset_core_empty
.
Qed
.
Canonical
Structure
coPsetR
:
=
discreteR
coPset
coPset_ra_mixin
.
Lemma
coPset_ucmra_mixin
:
UCMRAMixin
coPset
.
Proof
.
split
.
done
.
intros
X
.
by
rewrite
coPset_op_union
left_id_L
.
done
.
Qed
.
Canonical
Structure
coPsetUR
:
=
discreteUR
coPset
coPset_ra_mixin
coPset_ucmra_mixin
.
Lemma
coPset_opM
X
mY
:
X
⋅
?
mY
=
X
∪
from_option
id
∅
mY
.
Proof
.
destruct
mY
;
by
rewrite
/=
?right_id_L
.
Qed
.
Lemma
coPset_update
X
Y
:
X
~~>
Y
.
Proof
.
done
.
Qed
.
Lemma
coPset_local_update
X
Y
mXf
:
X
⊆
Y
→
X
~l
~>
Y
@
mXf
.
Proof
.
intros
(
Z
&->&?)%
subseteq_disjoint_union_L
.
intros
;
apply
local_update_total
;
split
;
[
done
|]
;
simpl
.
intros
mZ
_
.
rewrite
!
coPset_opM
=>
HX
.
by
rewrite
(
comm_L
_
X
)
-!
assoc_L
HX
.
Qed
.
End
coPset
.
(* The disjoiny union CMRA *)
Inductive
coPset_disj
:
=
|
CoPset
:
coPset
→
coPset_disj
|
CoPsetBot
:
coPset_disj
.
Section
coPset
.
Section
coPset
_disj
.
Arguments
op
_
_
!
_
!
_
/.
Canonical
Structure
coPset_disjC
:
=
leibnizC
coPset_disj
.
...
...
@@ -27,7 +80,7 @@ Section coPset.
repeat
(
simpl
||
case_decide
)
;
first
[
apply
(
f_equal
CoPset
)|
done
|
exfalso
]
;
set_solver
by
eauto
.
Lemma
coPset_included
X
Y
:
CoPset
X
≼
CoPset
Y
↔
X
⊆
Y
.
Lemma
coPset_
disj_
included
X
Y
:
CoPset
X
≼
CoPset
Y
↔
X
⊆
Y
.
Proof
.
split
.
-
move
=>
[[
Z
|]]
;
simpl
;
try
case_decide
;
set_solver
.
...
...
@@ -60,4 +113,4 @@ Section coPset.
Proof
.
split
;
try
apply
_
||
done
.
intros
[
X
|]
;
coPset_disj_solve
.
Qed
.
Canonical
Structure
coPset_disjUR
:
=
discreteUR
coPset_disj
coPset_disj_ra_mixin
coPset_disj_ucmra_mixin
.
End
coPset
.
End
coPset
_disj
.
algebra/gset.v
View file @
7c1de72a
...
...
@@ -2,13 +2,68 @@ From iris.algebra Require Export cmra.
From
iris
.
algebra
Require
Import
updates
local_updates
.
From
iris
.
prelude
Require
Export
collections
gmap
.
(* The union CMRA *)
Section
gset
.
Context
`
{
Countable
K
}.
Implicit
Types
X
Y
:
gset
K
.
Canonical
Structure
gsetC
:
=
leibnizC
(
gset
K
).
Instance
gset_valid
:
Valid
(
gset
K
)
:
=
λ
_
,
True
.
Instance
gset_op
:
Op
(
gset
K
)
:
=
union
.
Instance
gset_pcore
:
PCore
(
gset
K
)
:
=
λ
_
,
Some
∅
.
Lemma
gset_op_union
X
Y
:
X
⋅
Y
=
X
∪
Y
.
Proof
.
done
.
Qed
.
Lemma
gset_core_empty
X
:
core
X
=
∅
.
Proof
.
done
.
Qed
.
Lemma
gset_included
X
Y
:
X
≼
Y
↔
X
⊆
Y
.
Proof
.
split
.
-
intros
[
Z
->].
rewrite
gset_op_union
.
set_solver
.
-
intros
(
Z
&->&?)%
subseteq_disjoint_union_L
.
by
exists
Z
.
Qed
.
Lemma
gset_ra_mixin
:
RAMixin
(
gset
K
).
Proof
.
apply
ra_total_mixin
;
eauto
.
-
solve_proper
.
-
solve_proper
.
-
solve_proper
.
-
intros
X1
X2
X3
.
by
rewrite
!
gset_op_union
assoc_L
.
-
intros
X1
X2
.
by
rewrite
!
gset_op_union
comm_L
.
-
intros
X
.
by
rewrite
gset_op_union
gset_core_empty
left_id_L
.
-
intros
X1
X2
_
.
by
rewrite
gset_included
!
gset_core_empty
.
Qed
.
Canonical
Structure
gsetR
:
=
discreteR
(
gset
K
)
gset_ra_mixin
.
Lemma
gset_ucmra_mixin
:
UCMRAMixin
(
gset
K
).
Proof
.
split
.
done
.
intros
X
.
by
rewrite
gset_op_union
left_id_L
.
done
.
Qed
.
Canonical
Structure
gsetUR
:
=
discreteUR
(
gset
K
)
gset_ra_mixin
gset_ucmra_mixin
.
Lemma
gset_opM
X
mY
:
X
⋅
?
mY
=
X
∪
from_option
id
∅
mY
.
Proof
.
destruct
mY
;
by
rewrite
/=
?right_id_L
.
Qed
.
Lemma
gset_update
X
Y
:
X
~~>
Y
.
Proof
.
done
.
Qed
.
Lemma
gset_local_update
X
Y
mXf
:
X
⊆
Y
→
X
~l
~>
Y
@
mXf
.
Proof
.
intros
(
Z
&->&?)%
subseteq_disjoint_union_L
.
intros
;
apply
local_update_total
;
split
;
[
done
|]
;
simpl
.
intros
mZ
_
.
rewrite
!
gset_opM
=>
HX
.
by
rewrite
(
comm_L
_
X
)
-!
assoc_L
HX
.
Qed
.
End
gset
.
(* The disjoint union CMRA *)
Inductive
gset_disj
K
`
{
Countable
K
}
:
=
|
GSet
:
gset
K
→
gset_disj
K
|
GSetBot
:
gset_disj
K
.
Arguments
GSet
{
_
_
_
}
_
.
Arguments
GSetBot
{
_
_
_
}.
Section
gset
.
Section
gset
_disj
.
Context
`
{
Countable
K
}.
Arguments
op
_
_
!
_
!
_
/.
...
...
@@ -28,7 +83,7 @@ Section gset.
repeat
(
simpl
||
case_decide
)
;
first
[
apply
(
f_equal
GSet
)|
done
|
exfalso
]
;
set_solver
by
eauto
.
Lemma
coPset
_included
X
Y
:
GSet
X
≼
GSet
Y
↔
X
⊆
Y
.
Lemma
gset_disj
_included
X
Y
:
GSet
X
≼
GSet
Y
↔
X
⊆
Y
.
Proof
.
split
.
-
move
=>
[[
Z
|]]
;
simpl
;
try
case_decide
;
set_solver
.
...
...
@@ -63,7 +118,7 @@ Section gset.
Arguments
op
_
_
_
_
:
simpl
never
.
Lemma
gset_alloc_updateP_strong
P
(
Q
:
gset_disj
K
→
Prop
)
X
:
Lemma
gset_
disj_
alloc_updateP_strong
P
(
Q
:
gset_disj
K
→
Prop
)
X
:
(
∀
Y
,
X
⊆
Y
→
∃
j
,
j
∉
Y
∧
P
j
)
→
(
∀
i
,
i
∉
X
→
P
i
→
Q
(
GSet
({[
i
]}
∪
X
)))
→
GSet
X
~~>
:
Q
.
Proof
.
...
...
@@ -74,43 +129,46 @@ Section gset.
-
apply
HQ
;
set_solver
by
eauto
.
-
apply
gset_disj_valid_op
.
set_solver
by
eauto
.
Qed
.
Lemma
gset_alloc_updateP_strong'
P
X
:
Lemma
gset_
disj_
alloc_updateP_strong'
P
X
:
(
∀
Y
,
X
⊆
Y
→
∃
j
,
j
∉
Y
∧
P
j
)
→
GSet
X
~~>
:
λ
Y
,
∃
i
,
Y
=
GSet
({[
i
]}
∪
X
)
∧
i
∉
X
∧
P
i
.
Proof
.
eauto
using
gset_alloc_updateP_strong
.
Qed
.
Proof
.
eauto
using
gset_
disj_
alloc_updateP_strong
.
Qed
.
Lemma
gset_alloc_empty_updateP_strong
P
(
Q
:
gset_disj
K
→
Prop
)
:
Lemma
gset_
disj_
alloc_empty_updateP_strong
P
(
Q
:
gset_disj
K
→
Prop
)
:
(
∀
Y
:
gset
K
,
∃
j
,
j
∉
Y
∧
P
j
)
→
(
∀
i
,
P
i
→
Q
(
GSet
{[
i
]}))
→
GSet
∅
~~>
:
Q
.
Proof
.
intros
.
apply
(
gset_alloc_updateP_strong
P
)
;
eauto
.
intros
.
apply
(
gset_
disj_
alloc_updateP_strong
P
)
;
eauto
.
intros
i
;
rewrite
right_id_L
;
auto
.
Qed
.
Lemma
gset_alloc_empty_updateP_strong'
P
:
Lemma
gset_
disj_
alloc_empty_updateP_strong'
P
:
(
∀
Y
:
gset
K
,
∃
j
,
j
∉
Y
∧
P
j
)
→
GSet
∅
~~>
:
λ
Y
,
∃
i
,
Y
=
GSet
{[
i
]}
∧
P
i
.
Proof
.
eauto
using
gset_alloc_empty_updateP_strong
.
Qed
.
Proof
.
eauto
using
gset_
disj_
alloc_empty_updateP_strong
.
Qed
.
Section
fresh_updates
.
Context
`
{
Fresh
K
(
gset
K
),
!
FreshSpec
K
(
gset
K
)}.
Lemma
gset_alloc_updateP
(
Q
:
gset_disj
K
→
Prop
)
X
:
Lemma
gset_
disj_
alloc_updateP
(
Q
:
gset_disj
K
→
Prop
)
X
:
(
∀
i
,
i
∉
X
→
Q
(
GSet
({[
i
]}
∪
X
)))
→
GSet
X
~~>
:
Q
.
Proof
.
intro
;
eapply
gset_alloc_updateP_strong
with
(
λ
_
,
True
)
;
eauto
.
intro
;
eapply
gset_
disj_
alloc_updateP_strong
with
(
λ
_
,
True
)
;
eauto
.
intros
Y
?
;
exists
(
fresh
Y
)
;
eauto
using
is_fresh
.
Qed
.
Lemma
gset_alloc_updateP'
X
:
GSet
X
~~>
:
λ
Y
,
∃
i
,
Y
=
GSet
({[
i
]}
∪
X
)
∧
i
∉
X
.
Proof
.
eauto
using
gset_alloc_updateP
.
Qed
.
Lemma
gset_disj_alloc_updateP'
X
:
GSet
X
~~>
:
λ
Y
,
∃
i
,
Y
=
GSet
({[
i
]}
∪
X
)
∧
i
∉
X
.
Proof
.
eauto
using
gset_disj_alloc_updateP
.
Qed
.
Lemma
gset_alloc_empty_updateP
(
Q
:
gset_disj
K
→
Prop
)
:
Lemma
gset_
disj_
alloc_empty_updateP
(
Q
:
gset_disj
K
→
Prop
)
:
(
∀
i
,
Q
(
GSet
{[
i
]}))
→
GSet
∅
~~>
:
Q
.
Proof
.
intro
.
apply
gset_alloc_updateP
.
intros
i
;
rewrite
right_id_L
;
auto
.
Qed
.
Lemma
gset_alloc_empty_updateP'
:
GSet
∅
~~>
:
λ
Y
,
∃
i
,
Y
=
GSet
{[
i
]}.
Proof
.
eauto
using
gset_alloc_empty_updateP
.
Qed
.
Proof
.
intro
.
apply
gset_disj_alloc_updateP
.
intros
i
;
rewrite
right_id_L
;
auto
.
Qed
.
Lemma
gset_disj_alloc_empty_updateP'
:
GSet
∅
~~>
:
λ
Y
,
∃
i
,
Y
=
GSet
{[
i
]}.
Proof
.
eauto
using
gset_disj_alloc_empty_updateP
.
Qed
.
End
fresh_updates
.
Lemma
gset_alloc_local_update
X
i
Xf
:
Lemma
gset_
disj_
alloc_local_update
X
i
Xf
:
i
∉
X
→
i
∉
Xf
→
GSet
X
~l
~>
GSet
({[
i
]}
∪
X
)
@
Some
(
GSet
Xf
).
Proof
.
intros
??
;
apply
local_update_total
;
split
;
simpl
.
...
...
@@ -118,13 +176,13 @@ Section gset.
-
intros
mZ
?%
gset_disj_valid_op
HXf
.
rewrite
-
gset_disj_union
-
?assoc
?HXf
?cmra_opM_assoc
;
set_solver
.
Qed
.
Lemma
gset_alloc_empty_local_update
i
Xf
:
Lemma
gset_
disj_
alloc_empty_local_update
i
Xf
:
i
∉
Xf
→
GSet
∅
~l
~>
GSet
{[
i
]}
@
Some
(
GSet
Xf
).
Proof
.
intros
.
rewrite
-(
right_id_L
_
_
{[
i
]}).
apply
gset_alloc_local_update
;
set_solver
.
apply
gset_
disj_
alloc_local_update
;
set_solver
.
Qed
.
End
gset
.
End
gset
_disj
.
Arguments
gset_disjR
_
{
_
_
}.
Arguments
gset_disjUR
_
{
_
_
}.
heap_lang/lib/ticket_lock.v
View file @
7c1de72a
...
...
@@ -141,7 +141,7 @@ Section proof.
-
wp_cas_suc
.
iDestruct
"Hainv"
as
(
s
)
"[Ho %]"
;
subst
.
iVs
(
own_update
with
"Ho"
)
as
"Ho"
.
{
eapply
auth_update_no_frag
,
(
gset_alloc_empty_local_update
n
).
{
eapply
auth_update_no_frag
,
(
gset_
disj_
alloc_empty_local_update
n
).
rewrite
elem_of_seq_set
;
omega
.
}
iDestruct
"Ho"
as
"[Hofull Hofrag]"
.
iVs
(
"Hclose"
with
"[Hlo' Hln' Haown Hofull]"
).
...
...
program_logic/ownership.v
View file @
7c1de72a
...
...
@@ -156,7 +156,7 @@ Proof.
iIntros
(
Hfresh
)
"[Hw HP]"
.
iDestruct
"Hw"
as
(
I
)
"[? HI]"
.
iVs
(
own_empty
(
A
:
=
gset_disjUR
positive
)
disabled_name
)
as
"HE"
.
iVs
(
own_updateP
with
"HE"
)
as
"HE"
.
{
apply
(
gset_alloc_empty_updateP_strong'
(
λ
i
,
I
!!
i
=
None
∧
φ
i
)).
{
apply
(
gset_
disj_
alloc_empty_updateP_strong'
(
λ
i
,
I
!!
i
=
None
∧
φ
i
)).
intros
E
.
destruct
(
Hfresh
(
E
∪
dom
_
I
))
as
(
i
&
[?
HIi
%
not_elem_of_dom
]%
not_elem_of_union
&
?)
;
eauto
.
}
iDestruct
"HE"
as
(
X
)
"[Hi HE]"
;
iDestruct
"Hi"
as
%(
i
&
->
&
HIi
&
?).
...
...
program_logic/thread_local.v
View file @
7c1de72a
...
...
@@ -56,7 +56,7 @@ Section proofs.
iVs
(
own_empty
(
A
:
=
prodUR
coPset_disjUR
(
gset_disjUR
positive
))
tid
)
as
"Hempty"
.
iVs
(
own_updateP
with
"Hempty"
)
as
([
m1
m2
])
"[Hm Hown]"
.
{
apply
prod_updateP'
.
apply
cmra_updateP_id
,
(
reflexivity
(
R
:
=
eq
)).
apply
(
gset_alloc_empty_updateP_strong'
(
λ
i
,
i
∈
nclose
N
)).
apply
(
gset_
disj_
alloc_empty_updateP_strong'
(
λ
i
,
i
∈
nclose
N
)).
intros
Ef
.
exists
(
coPpick
(
nclose
N
∖
coPset
.
of_gset
Ef
)).
rewrite
-
coPset
.
elem_of_of_gset
comm
-
elem_of_difference
.
apply
coPpick_elem_of
=>
Hfin
.
...
...
Write
Preview
Supports
Markdown
0%
Try again
or
attach a new file
.
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Cancel
Please
register
or
sign in
to comment