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
eba897cc
Commit
eba897cc
authored
Nov 15, 2016
by
Robbert Krebbers
Browse files
Fix implicit arguments of own_empty.
There is no way to infer the cmra A, so we make it explicit.
parent
e3cb5b14
Changes
3
Hide whitespace changes
Inline
Side-by-side
base_logic/lib/own.v
View file @
eba897cc
...
...
@@ -139,7 +139,7 @@ Arguments own_update {_ _} [_] _ _ _ _.
Arguments
own_update_2
{
_
_
}
[
_
]
_
_
_
_
_
.
Arguments
own_update_3
{
_
_
}
[
_
]
_
_
_
_
_
_
.
Lemma
own_empty
`
{
inG
Σ
(
A
:
ucmraT
)}
γ
:
True
==
∗
own
γ
∅
.
Lemma
own_empty
A
`
{
inG
Σ
(
A
:
ucmraT
)}
γ
:
True
==
∗
own
γ
∅
.
Proof
.
rewrite
ownM_empty
!
own_eq
/
own_def
.
apply
bupd_ownM_update
,
iprod_singleton_update_empty
.
...
...
base_logic/lib/thread_local.v
View file @
eba897cc
...
...
@@ -54,7 +54,7 @@ Section proofs.
Lemma
tl_inv_alloc
tid
E
N
P
:
▷
P
={
E
}=
∗
tl_inv
tid
N
P
.
Proof
.
iIntros
"HP"
.
iMod
(
own_empty
(
A
:
=
prodUR
coPset_disjUR
(
gset_disjUR
positive
))
tid
)
as
"Hempty"
.
iMod
(
own_empty
(
prodUR
coPset_disjUR
(
gset_disjUR
positive
))
tid
)
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
∈
nclose
N
)).
...
...
base_logic/lib/wsat.v
View file @
eba897cc
...
...
@@ -53,7 +53,7 @@ Global Instance ownI_persistent i P : PersistentP (ownI i P).
Proof
.
rewrite
/
ownI
.
apply
_
.
Qed
.
Lemma
ownE_empty
:
True
==
∗
ownE
∅
.
Proof
.
by
rewrite
(
own_empty
(
A
:
=
coPset_disjUR
)
enabled_name
).
Qed
.
Proof
.
by
rewrite
(
own_empty
(
coPset_disjUR
)
enabled_name
).
Qed
.
Lemma
ownE_op
E1
E2
:
E1
⊥
E2
→
ownE
(
E1
∪
E2
)
⊣
⊢
ownE
E1
∗
ownE
E2
.
Proof
.
intros
.
by
rewrite
/
ownE
-
own_op
coPset_disj_union
.
Qed
.
Lemma
ownE_disjoint
E1
E2
:
ownE
E1
∗
ownE
E2
⊢
E1
⊥
E2
.
...
...
@@ -68,7 +68,7 @@ Lemma ownE_singleton_twice i : ownE {[i]} ∗ ownE {[i]} ⊢ False.
Proof
.
rewrite
ownE_disjoint
.
iIntros
(?)
;
set_solver
.
Qed
.
Lemma
ownD_empty
:
True
==
∗
ownD
∅
.
Proof
.
by
rewrite
(
own_empty
(
A
:
=
gset_disjUR
_
)
disabled_name
).
Qed
.
Proof
.
by
rewrite
(
own_empty
(
gset_disjUR
positive
)
disabled_name
).
Qed
.
Lemma
ownD_op
E1
E2
:
E1
⊥
E2
→
ownD
(
E1
∪
E2
)
⊣
⊢
ownD
E1
∗
ownD
E2
.
Proof
.
intros
.
by
rewrite
/
ownD
-
own_op
gset_disj_union
.
Qed
.
Lemma
ownD_disjoint
E1
E2
:
ownD
E1
∗
ownD
E2
⊢
E1
⊥
E2
.
...
...
@@ -126,7 +126,7 @@ Lemma ownI_alloc φ P :
wsat
∗
▷
P
==
∗
∃
i
,
■
(
φ
i
)
∗
wsat
∗
ownI
i
P
.
Proof
.
iIntros
(
Hfresh
)
"[Hw HP]"
.
iDestruct
"Hw"
as
(
I
)
"[? HI]"
.
iMod
(
own_empty
(
A
:
=
gset_disjUR
positive
)
disabled_name
)
as
"HE"
.
iMod
(
own_empty
(
gset_disjUR
positive
)
disabled_name
)
as
"HE"
.
iMod
(
own_updateP
with
"HE"
)
as
"HE"
.
{
apply
(
gset_disj_alloc_empty_updateP_strong'
(
λ
i
,
I
!!
i
=
None
∧
φ
i
)).
intros
E
.
destruct
(
Hfresh
(
E
∪
dom
_
I
))
...
...
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