Skip to content
GitLab
Projects
Groups
Snippets
Help
Loading...
Help
What's new
10
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in / Register
Toggle navigation
Open sidebar
Simon Spies
Iris
Commits
8a8c1405
Commit
8a8c1405
authored
Feb 20, 2019
by
Robbert Krebbers
Browse files
Options
Browse Files
Download
Email Patches
Plain Diff
Bump stdpp.
parent
a1cf5cb9
Changes
13
Hide whitespace changes
Inline
Side-by-side
Showing
13 changed files
with
44 additions
and
44 deletions
+44
-44
opam
opam
+1
-1
tests/proofmode.v
tests/proofmode.v
+1
-1
theories/algebra/big_op.v
theories/algebra/big_op.v
+4
-4
theories/algebra/cmra_big_op.v
theories/algebra/cmra_big_op.v
+1
-1
theories/algebra/coPset.v
theories/algebra/coPset.v
+1
-1
theories/algebra/gmultiset.v
theories/algebra/gmultiset.v
+1
-1
theories/algebra/gset.v
theories/algebra/gset.v
+1
-1
theories/algebra/sts.v
theories/algebra/sts.v
+20
-20
theories/base_logic/lib/invariants.v
theories/base_logic/lib/invariants.v
+3
-3
theories/base_logic/lib/na_invariants.v
theories/base_logic/lib/na_invariants.v
+3
-3
theories/bi/big_op.v
theories/bi/big_op.v
+4
-4
theories/heap_lang/lib/ticket_lock.v
theories/heap_lang/lib/ticket_lock.v
+3
-3
theories/heap_lang/proph_map.v
theories/heap_lang/proph_map.v
+1
-1
No files found.
opam
View file @
8a8c1405
...
...
@@ -11,5 +11,5 @@ install: [make "install"]
remove: ["rm" "-rf" "%{lib}%/coq/user-contrib/iris"]
depends: [
"coq" { (>= "8.7.1" & < "8.10~") | (= "dev") }
"coq-stdpp" { (= "dev.2019-02-
07.1.824e9723
") | (= "dev") }
"coq-stdpp" { (= "dev.2019-02-
20.2.c8c298d4
") | (= "dev") }
]
tests/proofmode.v
View file @
8a8c1405
...
...
@@ -152,7 +152,7 @@ Qed.
Lemma
test_iExist_coercion
(
P
:
Z
→
PROP
)
:
(
∀
x
,
P
x
)
-
∗
∃
x
,
P
x
.
Proof
.
iIntros
"HP"
.
iExists
(
0
:
nat
).
iApply
(
"HP"
$!
(
0
:
nat
)).
Qed
.
Lemma
test_iExist_tc
`
{
Collection
A
C
}
P
:
(
∃
x1
x2
:
gset
positive
,
P
-
∗
P
)%
I
.
Lemma
test_iExist_tc
`
{
Set_
A
C
}
P
:
(
∃
x1
x2
:
gset
positive
,
P
-
∗
P
)%
I
.
Proof
.
iExists
{[
1
%
positive
]},
∅
.
auto
.
Qed
.
Lemma
test_iSpecialize_tc
P
:
(
∀
x
y
z
:
gset
positive
,
P
)
-
∗
P
.
...
...
theories/algebra/big_op.v
View file @
8a8c1405
...
...
@@ -314,7 +314,7 @@ Section gset.
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
.
intros
.
induction
X
as
[|
x
X
?
IH
]
using
set
_ind_L
.
{
by
rewrite
left_id_L
big_opS_empty
left_id
.
}
rewrite
-
assoc_L
!
big_opS_insert
;
[|
set_solver
..].
by
rewrite
-
assoc
IH
;
last
set_solver
.
...
...
@@ -332,7 +332,7 @@ Section gset.
Lemma
big_opS_unit
X
:
([^
o
set
]
y
∈
X
,
monoid_unit
)
≡
(
monoid_unit
:
M
).
Proof
.
induction
X
using
collection
_ind_L
;
rewrite
/=
?big_opS_insert
?left_id
//.
induction
X
using
set
_ind_L
;
rewrite
/=
?big_opS_insert
?left_id
//.
Qed
.
Lemma
big_opS_opS
f
g
X
:
...
...
@@ -458,7 +458,7 @@ Section homomorphisms.
`
{!
MonoidHomomorphism
o1
o2
R
h
}
(
f
:
A
→
M1
)
X
:
R
(
h
([^
o1
set
]
x
∈
X
,
f
x
))
([^
o2
set
]
x
∈
X
,
h
(
f
x
)).
Proof
.
intros
.
induction
X
as
[|
x
X
?
IH
]
using
collection
_ind_L
.
intros
.
induction
X
as
[|
x
X
?
IH
]
using
set
_ind_L
.
-
by
rewrite
!
big_opS_empty
monoid_homomorphism_unit
.
-
by
rewrite
!
big_opS_insert
//
monoid_homomorphism
-
IH
.
Qed
.
...
...
@@ -466,7 +466,7 @@ Section homomorphisms.
`
{!
WeakMonoidHomomorphism
o1
o2
R
h
}
(
f
:
A
→
M1
)
X
:
X
≠
∅
→
R
(
h
([^
o1
set
]
x
∈
X
,
f
x
))
([^
o2
set
]
x
∈
X
,
h
(
f
x
)).
Proof
.
intros
.
induction
X
as
[|
x
X
?
IH
]
using
collection
_ind_L
;
[
done
|].
intros
.
induction
X
as
[|
x
X
?
IH
]
using
set
_ind_L
;
[
done
|].
destruct
(
decide
(
X
=
∅
))
as
[->|].
-
by
rewrite
!
big_opS_insert
//
!
big_opS_empty
!
right_id
.
-
by
rewrite
!
big_opS_insert
//
monoid_homomorphism
-
IH
//.
...
...
theories/algebra/cmra_big_op.v
View file @
8a8c1405
...
...
@@ -23,7 +23,7 @@ Qed.
Lemma
big_opS_None
{
M
:
cmraT
}
`
{
Countable
A
}
(
f
:
A
→
option
M
)
X
:
([^
op
set
]
x
∈
X
,
f
x
)
=
None
↔
∀
x
,
x
∈
X
→
f
x
=
None
.
Proof
.
induction
X
as
[|
x
X
?
IH
]
using
collection
_ind_L
;
[
done
|].
induction
X
as
[|
x
X
?
IH
]
using
set
_ind_L
;
[
done
|].
rewrite
-
equiv_None
big_opS_insert
//
equiv_None
op_None
IH
.
set_solver
.
Qed
.
Lemma
big_opMS_None
{
M
:
cmraT
}
`
{
Countable
A
}
(
f
:
A
→
option
M
)
X
:
...
...
theories/algebra/coPset.v
View file @
8a8c1405
From
iris
.
algebra
Require
Export
cmra
.
From
iris
.
algebra
Require
Import
updates
local_updates
.
From
stdpp
Require
Export
collection
s
coPset
.
From
stdpp
Require
Export
set
s
coPset
.
Set
Default
Proof
Using
"Type"
.
(** This is pretty much the same as algebra/gset, but I was not able to
generalize the construction without breaking canonical structures. *)
...
...
theories/algebra/gmultiset.v
View file @
8a8c1405
From
iris
.
algebra
Require
Export
cmra
.
From
iris
.
algebra
Require
Import
updates
local_updates
.
From
stdpp
Require
Export
collection
s
gmultiset
countable
.
From
stdpp
Require
Export
set
s
gmultiset
countable
.
Set
Default
Proof
Using
"Type"
.
(* The multiset union CMRA *)
...
...
theories/algebra/gset.v
View file @
8a8c1405
From
iris
.
algebra
Require
Export
cmra
.
From
iris
.
algebra
Require
Import
updates
local_updates
.
From
stdpp
Require
Export
collection
s
gmap
mapset
.
From
stdpp
Require
Export
set
s
gmap
mapset
.
Set
Default
Proof
Using
"Type"
.
(* The union CMRA *)
...
...
theories/algebra/sts.v
View file @
8a8c1405
From
stdpp
Require
Export
set
.
From
stdpp
Require
Export
prop
set
.
From
iris
.
algebra
Require
Export
cmra
.
From
iris
.
algebra
Require
Import
dra
.
Set
Default
Proof
Using
"Type"
.
...
...
@@ -12,13 +12,13 @@ Structure stsT := Sts {
state
:
Type
;
token
:
Type
;
prim_step
:
relation
state
;
tok
:
state
→
set
token
;
tok
:
state
→
prop
set
token
;
}.
Arguments
Sts
{
_
_
}
_
_
.
Arguments
prim_step
{
_
}
_
_
.
Arguments
tok
{
_
}
_
.
Notation
states
sts
:
=
(
set
(
state
sts
)).
Notation
tokens
sts
:
=
(
set
(
token
sts
)).
Notation
states
sts
:
=
(
prop
set
(
state
sts
)).
Notation
tokens
sts
:
=
(
prop
set
(
token
sts
)).
(** * Theory and definitions *)
Section
sts
.
...
...
@@ -49,8 +49,8 @@ Definition up_set (S : states sts) (T : tokens sts) : states sts :=
(** Tactic setup *)
Hint
Resolve
Step
:
core
.
Hint
Extern
50
(
equiv
(
A
:
=
set
_
)
_
_
)
=>
set_solver
:
sts
.
Hint
Extern
50
(
¬
equiv
(
A
:
=
set
_
)
_
_
)
=>
set_solver
:
sts
.
Hint
Extern
50
(
equiv
(
A
:
=
prop
set
_
)
_
_
)
=>
set_solver
:
sts
.
Hint
Extern
50
(
¬
equiv
(
A
:
=
prop
set
_
)
_
_
)
=>
set_solver
:
sts
.
Hint
Extern
50
(
_
∈
_
)
=>
set_solver
:
sts
.
Hint
Extern
50
(
_
⊆
_
)
=>
set_solver
:
sts
.
Hint
Extern
50
(
_
##
_
)
=>
set_solver
:
sts
.
...
...
@@ -62,7 +62,7 @@ Proof.
eauto
with
sts
;
set_solver
.
Qed
.
Global
Instance
frame_step_proper
:
Proper
((
≡
)
==>
(=)
==>
(=)
==>
iff
)
frame_step
.
Proof
.
move
=>
??
/
collection
_equiv_spec
[??]
;
split
;
by
apply
frame_step_mono
.
Qed
.
Proof
.
move
=>
??
/
set
_equiv_spec
[??]
;
split
;
by
apply
frame_step_mono
.
Qed
.
Instance
closed_proper'
:
Proper
((
≡
)
==>
(
≡
)
==>
impl
)
closed
.
Proof
.
destruct
3
;
constructor
;
intros
;
setoid_subst
;
eauto
.
Qed
.
Global
Instance
closed_proper
:
Proper
((
≡
)
==>
(
≡
)
==>
iff
)
closed
.
...
...
@@ -71,11 +71,11 @@ Global Instance up_preserving : Proper ((=) ==> flip (⊆) ==> (⊆)) up.
Proof
.
intros
s
?
<-
T
T'
HT
;
apply
elem_of_subseteq
.
induction
1
as
[|
s1
s2
s3
[
T1
T2
]]
;
[
constructor
|].
eapply
elem_of_
mk
Set
,
rtc_l
;
[
eapply
Frame_step
with
T1
T2
|]
;
eauto
with
sts
.
eapply
elem_of_
Prop
Set
,
rtc_l
;
[
eapply
Frame_step
with
T1
T2
|]
;
eauto
with
sts
.
Qed
.
Global
Instance
up_proper
:
Proper
((=)
==>
(
≡
)
==>
(
≡
))
up
.
Proof
.
by
move
=>
???
??
/
collection
_equiv_spec
[??]
;
split
;
apply
up_preserving
.
by
move
=>
???
??
/
set
_equiv_spec
[??]
;
split
;
apply
up_preserving
.
Qed
.
Global
Instance
up_set_preserving
:
Proper
((
⊆
)
==>
flip
(
⊆
)
==>
(
⊆
))
up_set
.
Proof
.
...
...
@@ -84,7 +84,7 @@ Proof.
Qed
.
Global
Instance
up_set_proper
:
Proper
((
≡
)
==>
(
≡
)
==>
(
≡
))
up_set
.
Proof
.
move
=>
S1
S2
/
collection
_equiv_spec
[??]
T1
T2
/
collection
_equiv_spec
[??]
;
move
=>
S1
S2
/
set
_equiv_spec
[??]
T1
T2
/
set
_equiv_spec
[??]
;
split
;
by
apply
up_set_preserving
.
Qed
.
...
...
@@ -127,7 +127,7 @@ Proof. intros s ?; apply elem_of_bind; eauto using elem_of_up. Qed.
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
.
Proof
.
by
rewrite
/
up_set
set
_bind_singleton
.
Qed
.
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
.
...
...
@@ -140,7 +140,7 @@ Proof.
Qed
.
Lemma
closed_up
s
T
:
tok
s
##
T
→
closed
(
up
s
T
)
T
.
Proof
.
intros
;
rewrite
-(
collection
_bind_singleton
(
λ
s
,
up
s
T
)
s
).
intros
;
rewrite
-(
set
_bind_singleton
(
λ
s
,
up
s
T
)
s
).
apply
closed_up_set
;
set_solver
.
Qed
.
Lemma
closed_up_set_empty
S
:
closed
(
up_set
S
∅
)
∅
.
...
...
@@ -149,7 +149,7 @@ Lemma closed_up_empty s : closed (up s ∅) ∅.
Proof
.
eauto
using
closed_up
with
sts
.
Qed
.
Lemma
up_closed
S
T
:
closed
S
T
→
up_set
S
T
≡
S
.
Proof
.
intros
?
;
apply
collection
_equiv_spec
;
split
;
auto
using
subseteq_up_set
.
intros
?
;
apply
set
_equiv_spec
;
split
;
auto
using
subseteq_up_set
.
intros
s
;
unfold
up_set
;
rewrite
elem_of_bind
;
intros
(
s'
&
Hstep
&?).
induction
Hstep
;
eauto
using
closed_step
.
Qed
.
...
...
@@ -159,7 +159,7 @@ Lemma up_set_subseteq S1 T S2 : closed S2 T → S1 ⊆ S2 → sts.up_set S1 T
Proof
.
move
=>
??
s
[
s'
[?
?]].
eauto
using
closed_steps
.
Qed
.
Lemma
up_op
s
T1
T2
:
up
s
(
T1
∪
T2
)
⊆
up
s
T1
∩
up
s
T2
.
Proof
.
(* Notice that the other direction does not hold. *)
intros
x
Hx
.
split
;
eapply
elem_of_
mk
Set
,
rtc_subrel
;
try
exact
Hx
.
intros
x
Hx
.
split
;
eapply
elem_of_
Prop
Set
,
rtc_subrel
;
try
exact
Hx
.
-
intros
;
eapply
frame_step_mono
;
last
first
;
try
done
.
set_solver
+.
-
intros
;
eapply
frame_step_mono
;
last
first
;
try
done
.
set_solver
+.
Qed
.
...
...
@@ -171,8 +171,8 @@ Notation frame_steps T := (rtc (frame_step T)).
(* The type of bounds we can give to the state of an STS. This is the type
that we equip with an RA structure. *)
Inductive
car
(
sts
:
stsT
)
:
=
|
auth
:
state
sts
→
set
(
token
sts
)
→
car
sts
|
frag
:
set
(
state
sts
)
→
set
(
token
sts
)
→
car
sts
.
|
auth
:
state
sts
→
prop
set
(
token
sts
)
→
car
sts
|
frag
:
prop
set
(
state
sts
)
→
prop
set
(
token
sts
)
→
car
sts
.
Arguments
auth
{
_
}
_
_
.
Arguments
frag
{
_
}
_
_
.
End
sts
.
...
...
@@ -215,7 +215,7 @@ Instance sts_op : Op (car sts) := λ x1 x2,
|
auth
s
T1
,
auth
_
T2
=>
auth
s
(
T1
∪
T2
)
(* never happens *)
end
.
Hint
Extern
50
(
equiv
(
A
:
=
set
_
)
_
_
)
=>
set_solver
:
sts
.
Hint
Extern
50
(
equiv
(
A
:
=
prop
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
.
...
...
@@ -388,7 +388,7 @@ Lemma sts_up_set_intersection S1 Sf Tf :
Proof
.
intros
Hclf
.
apply
(
anti_symm
(
⊆
)).
-
move
=>
s
[
HS1
HSf
].
split
.
by
apply
HS1
.
by
apply
subseteq_up_set
.
-
move
=>
s
[
HS1
[
s'
[/
elem_of_
mk
Set
Hsup
Hs'
]]].
split
;
first
done
.
-
move
=>
s
[
HS1
[
s'
[/
elem_of_
Prop
Set
Hsup
Hs'
]]].
split
;
first
done
.
eapply
closed_steps
,
Hsup
;
first
done
.
set_solver
+
Hs'
.
Qed
.
...
...
@@ -449,10 +449,10 @@ Structure stsT := Sts {
}.
Arguments
Sts
{
_
}
_
.
Arguments
prim_step
{
_
}
_
_
.
Notation
states
sts
:
=
(
set
(
state
sts
)).
Notation
states
sts
:
=
(
prop
set
(
state
sts
)).
Definition
stsT_token
:
=
Empty_set
.
Definition
stsT_tok
{
sts
:
stsT
}
(
_
:
state
sts
)
:
set
stsT_token
:
=
∅
.
Definition
stsT_tok
{
sts
:
stsT
}
(
_
:
state
sts
)
:
prop
set
stsT_token
:
=
∅
.
Canonical
Structure
sts_notok
(
sts
:
stsT
)
:
sts
.
stsT
:
=
sts
.
Sts
(@
prim_step
sts
)
stsT_tok
.
...
...
theories/base_logic/lib/invariants.v
View file @
8a8c1405
...
...
@@ -43,11 +43,11 @@ Qed.
Lemma
fresh_inv_name
(
E
:
gset
positive
)
N
:
∃
i
,
i
∉
E
∧
i
∈
(
↑
N
:
coPset
).
Proof
.
exists
(
coPpick
(
↑
N
∖
coPset
.
of_g
set
E
)).
rewrite
-
coPset
.
elem_of_
of_g
set
(
comm
and
)
-
elem_of_difference
.
exists
(
coPpick
(
↑
N
∖
gset_to_coP
set
E
)).
rewrite
-
elem_of_
gset_to_coP
set
(
comm
and
)
-
elem_of_difference
.
apply
coPpick_elem_of
=>
Hfin
.
eapply
nclose_infinite
,
(
difference_finite_inv
_
_
),
Hfin
.
apply
of_g
set_finite
.
apply
gset_to_coP
set_finite
.
Qed
.
Lemma
inv_alloc
N
E
P
:
▷
P
={
E
}=
∗
inv
N
P
.
...
...
theories/base_logic/lib/na_invariants.v
View file @
8a8c1405
...
...
@@ -80,11 +80,11 @@ Section proofs.
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
))).
intros
Ef
.
exists
(
coPpick
(
↑
N
∖
coPset
.
of_g
set
Ef
)).
rewrite
-
coPset
.
elem_of_
of_g
set
comm
-
elem_of_difference
.
intros
Ef
.
exists
(
coPpick
(
↑
N
∖
gset_to_coP
set
Ef
)).
rewrite
-
elem_of_
gset_to_coP
set
comm
-
elem_of_difference
.
apply
coPpick_elem_of
=>
Hfin
.
eapply
nclose_infinite
,
(
difference_finite_inv
_
_
),
Hfin
.
apply
of_g
set_finite
.
}
apply
gset_to_coP
set_finite
.
}
simpl
.
iDestruct
"Hm"
as
%(<-
&
i
&
->
&
?).
rewrite
/
na_inv
.
iMod
(
inv_alloc
N
with
"[-]"
)
;
last
(
iModIntro
;
iExists
i
;
eauto
).
...
...
theories/bi/big_op.v
View file @
8a8c1405
From
iris
.
algebra
Require
Export
big_op
.
From
iris
.
bi
Require
Import
derived_laws_sbi
plainly
.
From
stdpp
Require
Import
countable
fin_
collection
s
functions
.
From
stdpp
Require
Import
countable
fin_
set
s
functions
.
Set
Default
Proof
Using
"Type"
.
Import
interface
.
bi
derived_laws_bi
.
bi
derived_laws_sbi
.
bi
.
...
...
@@ -788,7 +788,7 @@ Section gset.
([
∗
set
]
y
∈
filter
P
X
,
Φ
y
)
⊣
⊢
([
∗
set
]
y
∈
X
,
if
decide
(
P
y
)
then
Φ
y
else
emp
).
Proof
.
induction
X
as
[|
x
X
?
IH
]
using
collection
_ind_L
.
induction
X
as
[|
x
X
?
IH
]
using
set
_ind_L
.
{
by
rewrite
filter_empty_L
!
big_sepS_empty
.
}
destruct
(
decide
(
P
x
)).
-
rewrite
filter_union_L
filter_singleton_L
//.
...
...
@@ -841,7 +841,7 @@ Section gset.
intros
.
apply
(
anti_symm
_
).
{
apply
forall_intro
=>
x
.
apply
impl_intro_l
,
pure_elim_l
=>
?
;
by
apply
:
big_sepS_elem_of
.
}
induction
X
as
[|
x
X
?
IH
]
using
collection
_ind_L
;
auto
using
big_sepS_empty'
.
induction
X
as
[|
x
X
?
IH
]
using
set
_ind_L
;
auto
using
big_sepS_empty'
.
rewrite
big_sepS_insert
//
-
persistent_and_sep
.
apply
and_intro
.
-
by
rewrite
(
forall_elim
x
)
pure_True
?True_impl
;
last
set_solver
.
-
rewrite
-
IH
.
apply
forall_mono
=>
y
.
apply
impl_intro_l
,
pure_elim_l
=>
?.
...
...
@@ -853,7 +853,7 @@ Section gset.
□
(
∀
x
,
⌜
x
∈
X
⌝
→
Φ
x
-
∗
Ψ
x
)
-
∗
[
∗
set
]
x
∈
X
,
Ψ
x
.
Proof
.
apply
wand_intro_l
.
induction
X
as
[|
x
X
?
IH
]
using
collection
_ind_L
.
apply
wand_intro_l
.
induction
X
as
[|
x
X
?
IH
]
using
set
_ind_L
.
{
by
rewrite
sep_elim_r
.
}
rewrite
!
big_sepS_insert
//
intuitionistically_sep_dup
.
rewrite
-
assoc
[(
□
_
∗
_
)%
I
]
comm
-!
assoc
assoc
.
apply
sep_mono
.
...
...
theories/heap_lang/lib/ticket_lock.v
View file @
8a8c1405
...
...
@@ -42,7 +42,7 @@ Section proof.
Definition
lock_inv
(
γ
:
gname
)
(
lo
ln
:
loc
)
(
R
:
iProp
Σ
)
:
iProp
Σ
:
=
(
∃
o
n
:
nat
,
lo
↦
#
o
∗
ln
↦
#
n
∗
own
γ
(
●
(
Excl'
o
,
GSet
(
se
q
_se
t
0
n
)))
∗
own
γ
(
●
(
Excl'
o
,
GSet
(
se
t
_se
q
0
n
)))
∗
((
own
γ
(
◯
(
Excl'
o
,
GSet
∅
))
∗
R
)
∨
own
γ
(
◯
(
ε
,
GSet
{[
o
]}))))%
I
.
Definition
is_lock
(
γ
:
gname
)
(
lk
:
val
)
(
R
:
iProp
Σ
)
:
iProp
Σ
:
=
...
...
@@ -117,8 +117,8 @@ Section proof.
-
iMod
(
own_update
with
"Hauth"
)
as
"[Hauth Hofull]"
.
{
eapply
auth_update_alloc
,
prod_local_update_2
.
eapply
(
gset_disj_alloc_empty_local_update
_
{[
n
]}).
apply
(
se
q
_se
t
_S_disjoint
0
).
}
rewrite
-(
se
q
_se
t
_S_union_L
0
).
apply
(
se
t
_se
q
_S_
end_
disjoint
0
).
}
rewrite
-(
se
t
_se
q
_S_
end_
union_L
0
).
wp_cas_suc
.
iModIntro
.
iSplitL
"Hlo' Hln' Haown Hauth"
.
{
iNext
.
iExists
o'
,
(
S
n
).
rewrite
Nat2Z
.
inj_succ
-
Z
.
add_1_r
.
by
iFrame
.
}
...
...
theories/heap_lang/proph_map.v
View file @
8a8c1405
...
...
@@ -35,7 +35,7 @@ Section definitions.
(** The first resolve for [p] in [pvs] *)
Definition
first_resolve
(
pvs
:
proph_val_list
P
V
)
(
p
:
P
)
:
option
V
:
=
(
map_of_list
pvs
:
gmap
P
V
)
!!
p
.
(
list_to_map
pvs
:
gmap
P
V
)
!!
p
.
Definition
first_resolve_in_list
(
R
:
proph_map
P
V
)
(
pvs
:
proph_val_list
P
V
)
:
=
∀
p
v
,
p
∈
dom
(
gset
_
)
R
→
...
...
Write
Preview
Markdown
is supported
0%
Try again
or
attach a new file
.
Attach a 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