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
Jonas Kastberg
iris
Commits
0ad1d2bd
Commit
0ad1d2bd
authored
Sep 07, 2017
by
Robbert Krebbers
Browse files
Options
Browse Files
Download
Email Patches
Plain Diff
Rename `PersistentP` → `Persistent` and `TimelessP` → `Timeless`.
parent
c311eeca
Changes
28
Hide whitespace changes
Inline
Side-by-side
Showing
28 changed files
with
176 additions
and
177 deletions
+176
-177
theories/base_logic/big_op.v
theories/base_logic/big_op.v
+21
-21
theories/base_logic/derived.v
theories/base_logic/derived.v
+74
-75
theories/base_logic/lib/auth.v
theories/base_logic/lib/auth.v
+3
-3
theories/base_logic/lib/boxes.v
theories/base_logic/lib/boxes.v
+1
-1
theories/base_logic/lib/cancelable_invariants.v
theories/base_logic/lib/cancelable_invariants.v
+2
-2
theories/base_logic/lib/core.v
theories/base_logic/lib/core.v
+3
-3
theories/base_logic/lib/counter_examples.v
theories/base_logic/lib/counter_examples.v
+4
-4
theories/base_logic/lib/fancy_updates_from_vs.v
theories/base_logic/lib/fancy_updates_from_vs.v
+2
-2
theories/base_logic/lib/fractional.v
theories/base_logic/lib/fractional.v
+1
-1
theories/base_logic/lib/gen_heap.v
theories/base_logic/lib/gen_heap.v
+1
-1
theories/base_logic/lib/invariants.v
theories/base_logic/lib/invariants.v
+2
-2
theories/base_logic/lib/na_invariants.v
theories/base_logic/lib/na_invariants.v
+2
-2
theories/base_logic/lib/own.v
theories/base_logic/lib/own.v
+2
-2
theories/base_logic/lib/saved_prop.v
theories/base_logic/lib/saved_prop.v
+1
-1
theories/base_logic/lib/sts.v
theories/base_logic/lib/sts.v
+3
-3
theories/base_logic/lib/viewshifts.v
theories/base_logic/lib/viewshifts.v
+1
-1
theories/base_logic/lib/wsat.v
theories/base_logic/lib/wsat.v
+1
-1
theories/heap_lang/lib/counter.v
theories/heap_lang/lib/counter.v
+1
-1
theories/heap_lang/lib/lock.v
theories/heap_lang/lib/lock.v
+2
-2
theories/heap_lang/lib/spin_lock.v
theories/heap_lang/lib/spin_lock.v
+2
-2
theories/heap_lang/lib/ticket_lock.v
theories/heap_lang/lib/ticket_lock.v
+2
-2
theories/program_logic/ownp.v
theories/program_logic/ownp.v
+1
-1
theories/proofmode/class_instances.v
theories/proofmode/class_instances.v
+15
-15
theories/proofmode/classes.v
theories/proofmode/classes.v
+5
-5
theories/proofmode/coq_tactics.v
theories/proofmode/coq_tactics.v
+13
-13
theories/proofmode/tactics.v
theories/proofmode/tactics.v
+7
-7
theories/tests/ipm_paper.v
theories/tests/ipm_paper.v
+1
-1
theories/tests/proofmode.v
theories/tests/proofmode.v
+3
-3
No files found.
theories/base_logic/big_op.v
View file @
0ad1d2bd
...
...
@@ -126,7 +126,7 @@ Section list.
Proof
.
apply
(
big_opL_commute
_
).
Qed
.
Lemma
big_sepL_forall
Φ
l
:
(
∀
k
x
,
Persistent
P
(
Φ
k
x
))
→
(
∀
k
x
,
Persistent
(
Φ
k
x
))
→
([
∗
list
]
k
↦
x
∈
l
,
Φ
k
x
)
⊣
⊢
(
∀
k
x
,
⌜
l
!!
k
=
Some
x
⌝
→
Φ
k
x
).
Proof
.
intros
H
Φ
.
apply
(
anti_symm
_
).
...
...
@@ -150,23 +150,23 @@ Section list.
Qed
.
Global
Instance
big_sepL_nil_persistent
Φ
:
Persistent
P
([
∗
list
]
k
↦
x
∈
[],
Φ
k
x
).
Persistent
([
∗
list
]
k
↦
x
∈
[],
Φ
k
x
).
Proof
.
simpl
;
apply
_
.
Qed
.
Global
Instance
big_sepL_persistent
Φ
l
:
(
∀
k
x
,
Persistent
P
(
Φ
k
x
))
→
Persistent
P
([
∗
list
]
k
↦
x
∈
l
,
Φ
k
x
).
(
∀
k
x
,
Persistent
(
Φ
k
x
))
→
Persistent
([
∗
list
]
k
↦
x
∈
l
,
Φ
k
x
).
Proof
.
revert
Φ
.
induction
l
as
[|
x
l
IH
]=>
Φ
?
/=
;
apply
_
.
Qed
.
Global
Instance
big_sepL_persistent_id
Ps
:
TCForall
Persistent
P
Ps
→
Persistent
P
([
∗
]
Ps
).
TCForall
Persistent
Ps
→
Persistent
([
∗
]
Ps
).
Proof
.
induction
1
;
simpl
;
apply
_
.
Qed
.
Global
Instance
big_sepL_nil_timeless
Φ
:
Timeless
P
([
∗
list
]
k
↦
x
∈
[],
Φ
k
x
).
Timeless
([
∗
list
]
k
↦
x
∈
[],
Φ
k
x
).
Proof
.
simpl
;
apply
_
.
Qed
.
Global
Instance
big_sepL_timeless
Φ
l
:
(
∀
k
x
,
Timeless
P
(
Φ
k
x
))
→
Timeless
P
([
∗
list
]
k
↦
x
∈
l
,
Φ
k
x
).
(
∀
k
x
,
Timeless
(
Φ
k
x
))
→
Timeless
([
∗
list
]
k
↦
x
∈
l
,
Φ
k
x
).
Proof
.
revert
Φ
.
induction
l
as
[|
x
l
IH
]=>
Φ
?
/=
;
apply
_
.
Qed
.
Global
Instance
big_sepL_timeless_id
Ps
:
TCForall
Timeless
P
Ps
→
Timeless
P
([
∗
]
Ps
).
TCForall
Timeless
Ps
→
Timeless
([
∗
]
Ps
).
Proof
.
induction
1
;
simpl
;
apply
_
.
Qed
.
End
list
.
...
...
@@ -316,7 +316,7 @@ Section gmap.
Proof
.
apply
(
big_opM_commute
_
).
Qed
.
Lemma
big_sepM_forall
Φ
m
:
(
∀
k
x
,
Persistent
P
(
Φ
k
x
))
→
(
∀
k
x
,
Persistent
(
Φ
k
x
))
→
([
∗
map
]
k
↦
x
∈
m
,
Φ
k
x
)
⊣
⊢
(
∀
k
x
,
⌜
m
!!
k
=
Some
x
⌝
→
Φ
k
x
).
Proof
.
intros
.
apply
(
anti_symm
_
).
...
...
@@ -343,16 +343,16 @@ Section gmap.
Qed
.
Global
Instance
big_sepM_empty_persistent
Φ
:
Persistent
P
([
∗
map
]
k
↦
x
∈
∅
,
Φ
k
x
).
Persistent
([
∗
map
]
k
↦
x
∈
∅
,
Φ
k
x
).
Proof
.
rewrite
/
big_opM
map_to_list_empty
.
apply
_
.
Qed
.
Global
Instance
big_sepM_persistent
Φ
m
:
(
∀
k
x
,
Persistent
P
(
Φ
k
x
))
→
Persistent
P
([
∗
map
]
k
↦
x
∈
m
,
Φ
k
x
).
(
∀
k
x
,
Persistent
(
Φ
k
x
))
→
Persistent
([
∗
map
]
k
↦
x
∈
m
,
Φ
k
x
).
Proof
.
intros
.
apply
big_sepL_persistent
=>
_
[??]
;
apply
_
.
Qed
.
Global
Instance
big_sepM_nil_timeless
Φ
:
Timeless
P
([
∗
map
]
k
↦
x
∈
∅
,
Φ
k
x
).
Timeless
([
∗
map
]
k
↦
x
∈
∅
,
Φ
k
x
).
Proof
.
rewrite
/
big_opM
map_to_list_empty
.
apply
_
.
Qed
.
Global
Instance
big_sepM_timeless
Φ
m
:
(
∀
k
x
,
Timeless
P
(
Φ
k
x
))
→
Timeless
P
([
∗
map
]
k
↦
x
∈
m
,
Φ
k
x
).
(
∀
k
x
,
Timeless
(
Φ
k
x
))
→
Timeless
([
∗
map
]
k
↦
x
∈
m
,
Φ
k
x
).
Proof
.
intros
.
apply
big_sepL_timeless
=>
_
[??]
;
apply
_
.
Qed
.
End
gmap
.
...
...
@@ -468,7 +468,7 @@ Section gset.
Proof
.
apply
(
big_opS_commute
_
).
Qed
.
Lemma
big_sepS_forall
Φ
X
:
(
∀
x
,
Persistent
P
(
Φ
x
))
→
([
∗
set
]
x
∈
X
,
Φ
x
)
⊣
⊢
(
∀
x
,
⌜
x
∈
X
⌝
→
Φ
x
).
(
∀
x
,
Persistent
(
Φ
x
))
→
([
∗
set
]
x
∈
X
,
Φ
x
)
⊣
⊢
(
∀
x
,
⌜
x
∈
X
⌝
→
Φ
x
).
Proof
.
intros
.
apply
(
anti_symm
_
).
{
apply
forall_intro
=>
x
.
...
...
@@ -490,15 +490,15 @@ Section gset.
by
rewrite
-
always_wand_impl
always_elim
wand_elim_l
.
Qed
.
Global
Instance
big_sepS_empty_persistent
Φ
:
Persistent
P
([
∗
set
]
x
∈
∅
,
Φ
x
).
Global
Instance
big_sepS_empty_persistent
Φ
:
Persistent
([
∗
set
]
x
∈
∅
,
Φ
x
).
Proof
.
rewrite
/
big_opS
elements_empty
.
apply
_
.
Qed
.
Global
Instance
big_sepS_persistent
Φ
X
:
(
∀
x
,
Persistent
P
(
Φ
x
))
→
Persistent
P
([
∗
set
]
x
∈
X
,
Φ
x
).
(
∀
x
,
Persistent
(
Φ
x
))
→
Persistent
([
∗
set
]
x
∈
X
,
Φ
x
).
Proof
.
rewrite
/
big_opS
.
apply
_
.
Qed
.
Global
Instance
big_sepS_nil_timeless
Φ
:
Timeless
P
([
∗
set
]
x
∈
∅
,
Φ
x
).
Global
Instance
big_sepS_nil_timeless
Φ
:
Timeless
([
∗
set
]
x
∈
∅
,
Φ
x
).
Proof
.
rewrite
/
big_opS
elements_empty
.
apply
_
.
Qed
.
Global
Instance
big_sepS_timeless
Φ
X
:
(
∀
x
,
Timeless
P
(
Φ
x
))
→
Timeless
P
([
∗
set
]
x
∈
X
,
Φ
x
).
(
∀
x
,
Timeless
(
Φ
x
))
→
Timeless
([
∗
set
]
x
∈
X
,
Φ
x
).
Proof
.
rewrite
/
big_opS
.
apply
_
.
Qed
.
End
gset
.
...
...
@@ -578,15 +578,15 @@ Section gmultiset.
□
?q
([
∗
mset
]
y
∈
X
,
Φ
y
)
⊣
⊢
([
∗
mset
]
y
∈
X
,
□
?q
Φ
y
).
Proof
.
apply
(
big_opMS_commute
_
).
Qed
.
Global
Instance
big_sepMS_empty_persistent
Φ
:
Persistent
P
([
∗
mset
]
x
∈
∅
,
Φ
x
).
Global
Instance
big_sepMS_empty_persistent
Φ
:
Persistent
([
∗
mset
]
x
∈
∅
,
Φ
x
).
Proof
.
rewrite
/
big_opMS
gmultiset_elements_empty
.
apply
_
.
Qed
.
Global
Instance
big_sepMS_persistent
Φ
X
:
(
∀
x
,
Persistent
P
(
Φ
x
))
→
Persistent
P
([
∗
mset
]
x
∈
X
,
Φ
x
).
(
∀
x
,
Persistent
(
Φ
x
))
→
Persistent
([
∗
mset
]
x
∈
X
,
Φ
x
).
Proof
.
rewrite
/
big_opMS
.
apply
_
.
Qed
.
Global
Instance
big_sepMS_nil_timeless
Φ
:
Timeless
P
([
∗
mset
]
x
∈
∅
,
Φ
x
).
Global
Instance
big_sepMS_nil_timeless
Φ
:
Timeless
([
∗
mset
]
x
∈
∅
,
Φ
x
).
Proof
.
rewrite
/
big_opMS
gmultiset_elements_empty
.
apply
_
.
Qed
.
Global
Instance
big_sepMS_timeless
Φ
X
:
(
∀
x
,
Timeless
P
(
Φ
x
))
→
Timeless
P
([
∗
mset
]
x
∈
X
,
Φ
x
).
(
∀
x
,
Timeless
(
Φ
x
))
→
Timeless
([
∗
mset
]
x
∈
X
,
Φ
x
).
Proof
.
rewrite
/
big_opMS
.
apply
_
.
Qed
.
End
gmultiset
.
End
big_op
.
...
...
theories/base_logic/derived.v
View file @
0ad1d2bd
...
...
@@ -29,15 +29,15 @@ Notation "◇ P" := (uPred_except_0 P)
Instance
:
Params
(@
uPred_except_0
)
1
.
Typeclasses
Opaque
uPred_except_0
.
Class
Timeless
P
{
M
}
(
P
:
uPred
M
)
:
=
timelessP
:
▷
P
⊢
◇
P
.
Class
Timeless
{
M
}
(
P
:
uPred
M
)
:
=
timelessP
:
▷
P
⊢
◇
P
.
Arguments
timelessP
{
_
}
_
{
_
}.
Hint
Mode
Timeless
P
+
!
:
typeclass_instances
.
Instance
:
Params
(@
Timeless
P
)
1
.
Hint
Mode
Timeless
+
!
:
typeclass_instances
.
Instance
:
Params
(@
Timeless
)
1
.
Class
Persistent
P
{
M
}
(
P
:
uPred
M
)
:
=
persistent
P
:
P
⊢
□
P
.
Arguments
persistent
P
{
_
}
_
{
_
}.
Hint
Mode
Persistent
P
+
!
:
typeclass_instances
.
Instance
:
Params
(@
Persistent
P
)
1
.
Class
Persistent
{
M
}
(
P
:
uPred
M
)
:
=
persistent
:
P
⊢
□
P
.
Arguments
persistent
{
_
}
_
{
_
}.
Hint
Mode
Persistent
+
!
:
typeclass_instances
.
Instance
:
Params
(@
Persistent
)
1
.
Module
uPred
.
Section
derived
.
...
...
@@ -794,33 +794,32 @@ Proof.
by
rewrite
-
bupd_intro
-
or_intro_l
.
Qed
.
(* Discrete instances *)
Global
Instance
TimelessP_proper
:
Proper
((
≡
)
==>
iff
)
(@
TimelessP
M
).
Global
Instance
Timeless_proper
:
Proper
((
≡
)
==>
iff
)
(@
Timeless
M
).
Proof
.
solve_proper
.
Qed
.
Global
Instance
pure_timeless
φ
:
Timeless
P
(
⌜φ⌝
:
uPred
M
)%
I
.
Global
Instance
pure_timeless
φ
:
Timeless
(
⌜φ⌝
:
uPred
M
)%
I
.
Proof
.
rewrite
/
Timeless
P
pure_alt
later_exist_false
.
by
setoid_rewrite
later_True
.
rewrite
/
Timeless
pure_alt
later_exist_false
.
by
setoid_rewrite
later_True
.
Qed
.
Global
Instance
valid_timeless
{
A
:
cmraT
}
`
{
CmraDiscrete
A
}
(
a
:
A
)
:
Timeless
P
(
✓
a
:
uPred
M
)%
I
.
Proof
.
rewrite
/
Timeless
P
!
discrete_valid
.
apply
(
timelessP
_
).
Qed
.
Global
Instance
and_timeless
P
Q
:
Timeless
P
P
→
Timeless
P
Q
→
Timeless
P
(
P
∧
Q
).
Proof
.
intros
;
rewrite
/
Timeless
P
except_0_and
later_and
;
auto
.
Qed
.
Global
Instance
or_timeless
P
Q
:
Timeless
P
P
→
Timeless
P
Q
→
Timeless
P
(
P
∨
Q
).
Proof
.
intros
;
rewrite
/
Timeless
P
except_0_or
later_or
;
auto
.
Qed
.
Global
Instance
impl_timeless
P
Q
:
Timeless
P
Q
→
Timeless
P
(
P
→
Q
).
Proof
.
rewrite
/
Timeless
P
=>
HQ
.
rewrite
later_false_excluded_middle
.
Timeless
(
✓
a
:
uPred
M
)%
I
.
Proof
.
rewrite
/
Timeless
!
discrete_valid
.
apply
(
timelessP
_
).
Qed
.
Global
Instance
and_timeless
P
Q
:
Timeless
P
→
Timeless
Q
→
Timeless
(
P
∧
Q
).
Proof
.
intros
;
rewrite
/
Timeless
except_0_and
later_and
;
auto
.
Qed
.
Global
Instance
or_timeless
P
Q
:
Timeless
P
→
Timeless
Q
→
Timeless
(
P
∨
Q
).
Proof
.
intros
;
rewrite
/
Timeless
except_0_or
later_or
;
auto
.
Qed
.
Global
Instance
impl_timeless
P
Q
:
Timeless
Q
→
Timeless
(
P
→
Q
).
Proof
.
rewrite
/
Timeless
=>
HQ
.
rewrite
later_false_excluded_middle
.
apply
or_mono
,
impl_intro_l
;
first
done
.
rewrite
-{
2
}(
l
ö
b
Q
)
;
apply
impl_intro_l
.
rewrite
HQ
/
uPred_except_0
!
and_or_r
.
apply
or_elim
;
last
auto
.
by
rewrite
assoc
(
comm
_
_
P
)
-
assoc
!
impl_elim_r
.
Qed
.
Global
Instance
sep_timeless
P
Q
:
Timeless
P
P
→
Timeless
P
Q
→
Timeless
P
(
P
∗
Q
).
Proof
.
intros
;
rewrite
/
Timeless
P
except_0_sep
later_sep
;
auto
.
Qed
.
Global
Instance
wand_timeless
P
Q
:
Timeless
P
Q
→
Timeless
P
(
P
-
∗
Q
).
Global
Instance
sep_timeless
P
Q
:
Timeless
P
→
Timeless
Q
→
Timeless
(
P
∗
Q
).
Proof
.
intros
;
rewrite
/
Timeless
except_0_sep
later_sep
;
auto
.
Qed
.
Global
Instance
wand_timeless
P
Q
:
Timeless
Q
→
Timeless
(
P
-
∗
Q
).
Proof
.
rewrite
/
Timeless
P
=>
HQ
.
rewrite
later_false_excluded_middle
.
rewrite
/
Timeless
=>
HQ
.
rewrite
later_false_excluded_middle
.
apply
or_mono
,
wand_intro_l
;
first
done
.
rewrite
-{
2
}(
l
ö
b
Q
)
;
apply
impl_intro_l
.
rewrite
HQ
/
uPred_except_0
!
and_or_r
.
apply
or_elim
;
last
auto
.
...
...
@@ -828,113 +827,113 @@ Proof.
by
rewrite
assoc
(
comm
_
_
P
)
-
assoc
-
always_and_sep_l'
impl_elim_r
wand_elim_r
.
Qed
.
Global
Instance
forall_timeless
{
A
}
(
Ψ
:
A
→
uPred
M
)
:
(
∀
x
,
Timeless
P
(
Ψ
x
))
→
Timeless
P
(
∀
x
,
Ψ
x
).
(
∀
x
,
Timeless
(
Ψ
x
))
→
Timeless
(
∀
x
,
Ψ
x
).
Proof
.
rewrite
/
Timeless
P
=>
HQ
.
rewrite
later_false_excluded_middle
.
rewrite
/
Timeless
=>
HQ
.
rewrite
later_false_excluded_middle
.
apply
or_mono
;
first
done
.
apply
forall_intro
=>
x
.
rewrite
-(
l
ö
b
(
Ψ
x
))
;
apply
impl_intro_l
.
rewrite
HQ
/
uPred_except_0
!
and_or_r
.
apply
or_elim
;
last
auto
.
by
rewrite
impl_elim_r
(
forall_elim
x
).
Qed
.
Global
Instance
exist_timeless
{
A
}
(
Ψ
:
A
→
uPred
M
)
:
(
∀
x
,
Timeless
P
(
Ψ
x
))
→
Timeless
P
(
∃
x
,
Ψ
x
).
(
∀
x
,
Timeless
(
Ψ
x
))
→
Timeless
(
∃
x
,
Ψ
x
).
Proof
.
rewrite
/
Timeless
P
=>
?.
rewrite
later_exist_false
.
apply
or_elim
.
rewrite
/
Timeless
=>
?.
rewrite
later_exist_false
.
apply
or_elim
.
-
rewrite
/
uPred_except_0
;
auto
.
-
apply
exist_elim
=>
x
.
rewrite
-(
exist_intro
x
)
;
auto
.
Qed
.
Global
Instance
always_timeless
P
:
Timeless
P
P
→
Timeless
P
(
□
P
).
Proof
.
intros
;
rewrite
/
Timeless
P
except_0_always
-
always_later
;
auto
.
Qed
.
Global
Instance
always_if_timeless
p
P
:
Timeless
P
P
→
Timeless
P
(
□
?p
P
).
Global
Instance
always_timeless
P
:
Timeless
P
→
Timeless
(
□
P
).
Proof
.
intros
;
rewrite
/
Timeless
except_0_always
-
always_later
;
auto
.
Qed
.
Global
Instance
always_if_timeless
p
P
:
Timeless
P
→
Timeless
(
□
?p
P
).
Proof
.
destruct
p
;
apply
_
.
Qed
.
Global
Instance
eq_timeless
{
A
:
ofeT
}
(
a
b
:
A
)
:
Discrete
a
→
Timeless
P
(
a
≡
b
:
uPred
M
)%
I
.
Proof
.
intros
.
rewrite
/
Timeless
P
!
discrete_eq
.
apply
(
timelessP
_
).
Qed
.
Global
Instance
ownM_timeless
(
a
:
M
)
:
Discrete
a
→
Timeless
P
(
uPred_ownM
a
).
Discrete
a
→
Timeless
(
a
≡
b
:
uPred
M
)%
I
.
Proof
.
intros
.
rewrite
/
Timeless
!
discrete_eq
.
apply
(
timelessP
_
).
Qed
.
Global
Instance
ownM_timeless
(
a
:
M
)
:
Discrete
a
→
Timeless
(
uPred_ownM
a
).
Proof
.
intros
?.
rewrite
/
Timeless
P
later_ownM
.
apply
exist_elim
=>
b
.
intros
?.
rewrite
/
Timeless
later_ownM
.
apply
exist_elim
=>
b
.
rewrite
(
timelessP
(
a
≡
b
))
(
except_0_intro
(
uPred_ownM
b
))
-
except_0_and
.
apply
except_0_mono
.
rewrite
internal_eq_sym
.
apply
(
internal_eq_rewrite
b
a
(
uPred_ownM
))
;
first
apply
_;
auto
.
Qed
.
Global
Instance
from_option_timeless
{
A
}
P
(
Ψ
:
A
→
uPred
M
)
(
mx
:
option
A
)
:
(
∀
x
,
Timeless
P
(
Ψ
x
))
→
Timeless
P
P
→
Timeless
P
(
from_option
Ψ
P
mx
).
(
∀
x
,
Timeless
(
Ψ
x
))
→
Timeless
P
→
Timeless
(
from_option
Ψ
P
mx
).
Proof
.
destruct
mx
;
apply
_
.
Qed
.
(* Derived lemmas for persistence *)
Global
Instance
Persistent
P
_proper
:
Proper
((
≡
)
==>
iff
)
(@
Persistent
P
M
).
Global
Instance
Persistent_proper
:
Proper
((
≡
)
==>
iff
)
(@
Persistent
M
).
Proof
.
solve_proper
.
Qed
.
Global
Instance
limit_preserving_Persistent
P
{
A
:
ofeT
}
`
{
Cofe
A
}
(
Φ
:
A
→
uPred
M
)
:
NonExpansive
Φ
→
LimitPreserving
(
λ
x
,
Persistent
P
(
Φ
x
)).
Global
Instance
limit_preserving_Persistent
{
A
:
ofeT
}
`
{
Cofe
A
}
(
Φ
:
A
→
uPred
M
)
:
NonExpansive
Φ
→
LimitPreserving
(
λ
x
,
Persistent
(
Φ
x
)).
Proof
.
intros
.
apply
limit_preserving_entails
;
solve_proper
.
Qed
.
Lemma
always_always
P
`
{!
Persistent
P
P
}
:
□
P
⊣
⊢
P
.
Lemma
always_always
P
`
{!
Persistent
P
}
:
□
P
⊣
⊢
P
.
Proof
.
apply
(
anti_symm
(
⊢
))
;
auto
using
always_elim
.
Qed
.
Lemma
always_if_always
p
P
`
{!
Persistent
P
P
}
:
□
?p
P
⊣
⊢
P
.
Lemma
always_if_always
p
P
`
{!
Persistent
P
}
:
□
?p
P
⊣
⊢
P
.
Proof
.
destruct
p
;
simpl
;
auto
using
always_always
.
Qed
.
Lemma
always_intro
P
Q
`
{!
Persistent
P
P
}
:
(
P
⊢
Q
)
→
P
⊢
□
Q
.
Lemma
always_intro
P
Q
`
{!
Persistent
P
}
:
(
P
⊢
Q
)
→
P
⊢
□
Q
.
Proof
.
rewrite
-(
always_always
P
)
;
apply
always_intro'
.
Qed
.
Lemma
always_and_sep_l
P
Q
`
{!
Persistent
P
P
}
:
P
∧
Q
⊣
⊢
P
∗
Q
.
Lemma
always_and_sep_l
P
Q
`
{!
Persistent
P
}
:
P
∧
Q
⊣
⊢
P
∗
Q
.
Proof
.
by
rewrite
-(
always_always
P
)
always_and_sep_l'
.
Qed
.
Lemma
always_and_sep_r
P
Q
`
{!
Persistent
P
Q
}
:
P
∧
Q
⊣
⊢
P
∗
Q
.
Lemma
always_and_sep_r
P
Q
`
{!
Persistent
Q
}
:
P
∧
Q
⊣
⊢
P
∗
Q
.
Proof
.
by
rewrite
-(
always_always
Q
)
always_and_sep_r'
.
Qed
.
Lemma
always_sep_dup
P
`
{!
Persistent
P
P
}
:
P
⊣
⊢
P
∗
P
.
Lemma
always_sep_dup
P
`
{!
Persistent
P
}
:
P
⊣
⊢
P
∗
P
.
Proof
.
by
rewrite
-(
always_always
P
)
-
always_sep_dup'
.
Qed
.
Lemma
always_entails_l
P
Q
`
{!
Persistent
P
Q
}
:
(
P
⊢
Q
)
→
P
⊢
Q
∗
P
.
Lemma
always_entails_l
P
Q
`
{!
Persistent
Q
}
:
(
P
⊢
Q
)
→
P
⊢
Q
∗
P
.
Proof
.
by
rewrite
-(
always_always
Q
)
;
apply
always_entails_l'
.
Qed
.
Lemma
always_entails_r
P
Q
`
{!
Persistent
P
Q
}
:
(
P
⊢
Q
)
→
P
⊢
P
∗
Q
.
Lemma
always_entails_r
P
Q
`
{!
Persistent
Q
}
:
(
P
⊢
Q
)
→
P
⊢
P
∗
Q
.
Proof
.
by
rewrite
-(
always_always
Q
)
;
apply
always_entails_r'
.
Qed
.
Lemma
always_impl_wand
P
`
{!
Persistent
P
P
}
Q
:
(
P
→
Q
)
⊣
⊢
(
P
-
∗
Q
).
Lemma
always_impl_wand
P
`
{!
Persistent
P
}
Q
:
(
P
→
Q
)
⊣
⊢
(
P
-
∗
Q
).
Proof
.
apply
(
anti_symm
_
)
;
auto
using
impl_wand
.
apply
impl_intro_l
.
by
rewrite
always_and_sep_l
wand_elim_r
.
Qed
.
(* Persistence *)
Global
Instance
pure_persistent
φ
:
Persistent
P
(
⌜φ⌝
:
uPred
M
)%
I
.
Proof
.
by
rewrite
/
Persistent
P
always_pure
.
Qed
.
Global
Instance
pure_persistent
φ
:
Persistent
(
⌜φ⌝
:
uPred
M
)%
I
.
Proof
.
by
rewrite
/
Persistent
always_pure
.
Qed
.
Global
Instance
pure_impl_persistent
φ
Q
:
Persistent
P
Q
→
Persistent
P
(
⌜φ⌝
→
Q
)%
I
.
Persistent
Q
→
Persistent
(
⌜φ⌝
→
Q
)%
I
.
Proof
.
rewrite
/
Persistent
P
pure_impl_forall
always_forall
.
auto
using
forall_mono
.
rewrite
/
Persistent
pure_impl_forall
always_forall
.
auto
using
forall_mono
.
Qed
.
Global
Instance
pure_wand_persistent
φ
Q
:
Persistent
P
Q
→
Persistent
P
(
⌜φ⌝
-
∗
Q
)%
I
.
Persistent
Q
→
Persistent
(
⌜φ⌝
-
∗
Q
)%
I
.
Proof
.
rewrite
/
Persistent
P
-
always_impl_wand
pure_impl_forall
always_forall
.
rewrite
/
Persistent
-
always_impl_wand
pure_impl_forall
always_forall
.
auto
using
forall_mono
.
Qed
.
Global
Instance
always_persistent
P
:
Persistent
P
(
□
P
).
Global
Instance
always_persistent
P
:
Persistent
(
□
P
).
Proof
.
by
intros
;
apply
always_intro'
.
Qed
.
Global
Instance
and_persistent
P
Q
:
Persistent
P
P
→
Persistent
P
Q
→
Persistent
P
(
P
∧
Q
).
Proof
.
by
intros
;
rewrite
/
Persistent
P
always_and
;
apply
and_mono
.
Qed
.
Persistent
P
→
Persistent
Q
→
Persistent
(
P
∧
Q
).
Proof
.
by
intros
;
rewrite
/
Persistent
always_and
;
apply
and_mono
.
Qed
.
Global
Instance
or_persistent
P
Q
:
Persistent
P
P
→
Persistent
P
Q
→
Persistent
P
(
P
∨
Q
).
Proof
.
by
intros
;
rewrite
/
Persistent
P
always_or
;
apply
or_mono
.
Qed
.
Persistent
P
→
Persistent
Q
→
Persistent
(
P
∨
Q
).
Proof
.
by
intros
;
rewrite
/
Persistent
always_or
;
apply
or_mono
.
Qed
.
Global
Instance
sep_persistent
P
Q
:
Persistent
P
P
→
Persistent
P
Q
→
Persistent
P
(
P
∗
Q
).
Proof
.
by
intros
;
rewrite
/
Persistent
P
always_sep
;
apply
sep_mono
.
Qed
.
Persistent
P
→
Persistent
Q
→
Persistent
(
P
∗
Q
).
Proof
.
by
intros
;
rewrite
/
Persistent
always_sep
;
apply
sep_mono
.
Qed
.
Global
Instance
forall_persistent
{
A
}
(
Ψ
:
A
→
uPred
M
)
:
(
∀
x
,
Persistent
P
(
Ψ
x
))
→
Persistent
P
(
∀
x
,
Ψ
x
).
Proof
.
by
intros
;
rewrite
/
Persistent
P
always_forall
;
apply
forall_mono
.
Qed
.
(
∀
x
,
Persistent
(
Ψ
x
))
→
Persistent
(
∀
x
,
Ψ
x
).
Proof
.
by
intros
;
rewrite
/
Persistent
always_forall
;
apply
forall_mono
.
Qed
.
Global
Instance
exist_persistent
{
A
}
(
Ψ
:
A
→
uPred
M
)
:
(
∀
x
,
Persistent
P
(
Ψ
x
))
→
Persistent
P
(
∃
x
,
Ψ
x
).
Proof
.
by
intros
;
rewrite
/
Persistent
P
always_exist
;
apply
exist_mono
.
Qed
.
(
∀
x
,
Persistent
(
Ψ
x
))
→
Persistent
(
∃
x
,
Ψ
x
).
Proof
.
by
intros
;
rewrite
/
Persistent
always_exist
;
apply
exist_mono
.
Qed
.
Global
Instance
internal_eq_persistent
{
A
:
ofeT
}
(
a
b
:
A
)
:
Persistent
P
(
a
≡
b
:
uPred
M
)%
I
.
Proof
.
by
intros
;
rewrite
/
Persistent
P
always_internal_eq
.
Qed
.
Persistent
(
a
≡
b
:
uPred
M
)%
I
.
Proof
.
by
intros
;
rewrite
/
Persistent
always_internal_eq
.
Qed
.
Global
Instance
cmra_valid_persistent
{
A
:
cmraT
}
(
a
:
A
)
:
Persistent
P
(
✓
a
:
uPred
M
)%
I
.
Proof
.
by
intros
;
rewrite
/
Persistent
P
always_cmra_valid
.
Qed
.
Global
Instance
later_persistent
P
:
Persistent
P
P
→
Persistent
P
(
▷
P
).
Proof
.
by
intros
;
rewrite
/
Persistent
P
always_later
;
apply
later_mono
.
Qed
.
Global
Instance
laterN_persistent
n
P
:
Persistent
P
P
→
Persistent
P
(
▷
^
n
P
).
Persistent
(
✓
a
:
uPred
M
)%
I
.
Proof
.
by
intros
;
rewrite
/
Persistent
always_cmra_valid
.
Qed
.
Global
Instance
later_persistent
P
:
Persistent
P
→
Persistent
(
▷
P
).
Proof
.
by
intros
;
rewrite
/
Persistent
always_later
;
apply
later_mono
.
Qed
.
Global
Instance
laterN_persistent
n
P
:
Persistent
P
→
Persistent
(
▷
^
n
P
).
Proof
.
induction
n
;
apply
_
.
Qed
.
Global
Instance
ownM_persistent
:
CoreId
a
→
Persistent
P
(@
uPred_ownM
M
a
).
Proof
.
intros
.
by
rewrite
/
Persistent
P
always_ownM
.
Qed
.
Global
Instance
ownM_persistent
:
CoreId
a
→
Persistent
(@
uPred_ownM
M
a
).
Proof
.
intros
.
by
rewrite
/
Persistent
always_ownM
.
Qed
.
Global
Instance
from_option_persistent
{
A
}
P
(
Ψ
:
A
→
uPred
M
)
(
mx
:
option
A
)
:
(
∀
x
,
Persistent
P
(
Ψ
x
))
→
Persistent
P
P
→
Persistent
P
(
from_option
Ψ
P
mx
).
(
∀
x
,
Persistent
(
Ψ
x
))
→
Persistent
P
→
Persistent
(
from_option
Ψ
P
mx
).
Proof
.
destruct
mx
;
apply
_
.
Qed
.
(* For big ops *)
...
...
theories/base_logic/lib/auth.v
View file @
0ad1d2bd
...
...
@@ -30,9 +30,9 @@ Section definitions.
Proof
.
solve_proper
.
Qed
.
Global
Instance
auth_own_proper
:
Proper
((
≡
)
==>
(
⊣
⊢
))
auth_own
.
Proof
.
solve_proper
.
Qed
.
Global
Instance
auth_own_timeless
a
:
Timeless
P
(
auth_own
a
).
Global
Instance
auth_own_timeless
a
:
Timeless
(
auth_own
a
).
Proof
.
apply
_
.
Qed
.
Global
Instance
auth_own_core_id
a
:
CoreId
a
→
Persistent
P
(
auth_own
a
).
Global
Instance
auth_own_core_id
a
:
CoreId
a
→
Persistent
(
auth_own
a
).
Proof
.
apply
_
.
Qed
.
Global
Instance
auth_inv_ne
n
:
...
...
@@ -51,7 +51,7 @@ Section definitions.
Proper
(
pointwise_relation
T
(
≡
)
==>
pointwise_relation
T
(
⊣
⊢
)
==>
(
⊣
⊢
))
(
auth_ctx
N
).
Proof
.
solve_proper
.
Qed
.
Global
Instance
auth_ctx_persistent
N
f
φ
:
Persistent
P
(
auth_ctx
N
f
φ
).
Global
Instance
auth_ctx_persistent
N
f
φ
:
Persistent
(
auth_ctx
N
f
φ
).
Proof
.
apply
_
.
Qed
.
End
definitions
.
...
...
theories/base_logic/lib/boxes.v
View file @
0ad1d2bd
...
...
@@ -65,7 +65,7 @@ Proof. solve_contractive. Qed.
Global
Instance
slice_proper
γ
:
Proper
((
≡
)
==>
(
≡
))
(
slice
N
γ
).
Proof
.
apply
ne_proper
,
_
.
Qed
.
Global
Instance
slice_persistent
γ
P
:
Persistent
P
(
slice
N
γ
P
).
Global
Instance
slice_persistent
γ
P
:
Persistent
(
slice
N
γ
P
).
Proof
.
apply
_
.
Qed
.
Global
Instance
box_contractive
f
:
Contractive
(
box
N
f
).
...
...
theories/base_logic/lib/cancelable_invariants.v
View file @
0ad1d2bd
...
...
@@ -24,7 +24,7 @@ Instance: Params (@cinv) 5.
Section
proofs
.
Context
`
{
invG
Σ
,
cinvG
Σ
}.
Global
Instance
cinv_own_timeless
γ
p
:
Timeless
P
(
cinv_own
γ
p
).
Global
Instance
cinv_own_timeless
γ
p
:
Timeless
(
cinv_own
γ
p
).
Proof
.
rewrite
/
cinv_own
;
apply
_
.
Qed
.
Global
Instance
cinv_contractive
N
γ
:
Contractive
(
cinv
N
γ
).
...
...
@@ -34,7 +34,7 @@ Section proofs.
Global
Instance
cinv_proper
N
γ
:
Proper
((
≡
)
==>
(
≡
))
(
cinv
N
γ
).
Proof
.
exact
:
ne_proper
.
Qed
.
Global
Instance
cinv_persistent
N
γ
P
:
Persistent
P
(
cinv
N
γ
P
).
Global
Instance
cinv_persistent
N
γ
P
:
Persistent
(
cinv
N
γ
P
).
Proof
.
rewrite
/
cinv
;
apply
_
.
Qed
.
Global
Instance
cinv_own_fractionnal
γ
:
Fractional
(
cinv_own
γ
).
...
...
theories/base_logic/lib/core.v
View file @
0ad1d2bd
...
...
@@ -15,7 +15,7 @@ Import uPred.
*)
Definition
coreP
{
M
:
ucmraT
}
(
P
:
uPred
M
)
:
uPred
M
:
=
(
∀
`
(!
Persistent
P
Q
),
⌜
P
⊢
Q
⌝
→
Q
)%
I
.
(
∀
`
(!
Persistent
Q
),
⌜
P
⊢
Q
⌝
→
Q
)%
I
.
Instance
:
Params
(@
coreP
)
1
.
Typeclasses
Opaque
coreP
.
...
...
@@ -26,7 +26,7 @@ Section core.
Lemma
coreP_intro
P
:
P
-
∗
coreP
P
.
Proof
.
rewrite
/
coreP
.
iIntros
"HP"
.
by
iIntros
(
Q
HQ
->).
Qed
.
Global
Instance
coreP_persistent
P
:
Persistent
P
(
coreP
P
).
Global
Instance
coreP_persistent
P
:
Persistent
(
coreP
P
).
Proof
.
rewrite
/
coreP
.
apply
_
.
Qed
.
Global
Instance
coreP_mono
:
Proper
((
⊢
)
==>
(
⊢
))
(@
coreP
M
).
...
...
@@ -38,7 +38,7 @@ Section core.
Global
Instance
coreP_proper
:
Proper
((
⊣
⊢
)
==>
(
⊣
⊢
))
(@
coreP
M
).
Proof
.
intros
P
Q
.
rewrite
!
equiv_spec
=>-[??].
by
split
;
apply
coreP_mono
.
Qed
.
Lemma
coreP_elim
P
:
Persistent
P
P
→
coreP
P
-
∗
P
.
Lemma
coreP_elim
P
:
Persistent
P
→
coreP
P
-
∗
P
.
Proof
.
rewrite
/
coreP
.
iIntros
(?)
"HCP"
.
unshelve
iApply
(
"HCP"
$!
P
)
;
auto
.
Qed
.
Lemma
coreP_wand
P
Q
:
...
...
theories/base_logic/lib/counter_examples.v
View file @
0ad1d2bd
...
...
@@ -12,7 +12,7 @@ Module savedprop. Section savedprop.
(** Saved Propositions and the update modality *)
Context
(
sprop
:
Type
)
(
saved
:
sprop
→
iProp
→
iProp
).
Hypothesis
sprop_persistent
:
∀
i
P
,
Persistent
P
(
saved
i
P
).
Hypothesis
sprop_persistent
:
∀
i
P
,
Persistent
(
saved
i
P
).
Hypothesis
sprop_alloc_dep
:
∀
(
P
:
sprop
→
iProp
),
(|==>
(
∃
i
,
saved
i
(
P
i
)))%
I
.
Hypothesis
sprop_agree
:
∀
i
P
Q
,
saved
i
P
∧
saved
i
Q
⊢
□
(
P
↔
Q
).
...
...
@@ -69,7 +69,7 @@ Module inv. Section inv.
(** We have invariants *)
Context
(
name
:
Type
)
(
inv
:
name
→
iProp
→
iProp
).
Hypothesis
inv_persistent
:
∀
i
P
,
Persistent
P
(
inv
i
P
).
Hypothesis
inv_persistent
:
∀
i
P
,
Persistent
(
inv
i
P
).
Hypothesis
inv_alloc
:
∀
P
,
P
⊢
fupd
M1
(
∃
i
,
inv
i
P
).
Hypothesis
inv_open
:
∀
i
P
Q
R
,
(
P
∗
Q
⊢
fupd
M0
(
P
∗
R
))
→
(
inv
i
P
∗
Q
⊢
fupd
M1
R
).
...
...
@@ -132,7 +132,7 @@ Module inv. Section inv.
(** Now to the actual counterexample. We start with a weird form of saved propositions. *)
Definition
saved
(
γ
:
gname
)
(
P
:
iProp
)
:
iProp
:
=
∃
i
,
inv
i
(
start
γ
∨
(
finished
γ
∗
□
P
)).
Global
Instance
saved_persistent
γ
P
:
Persistent
P
(
saved
γ
P
)
:
=
_
.
Global
Instance
saved_persistent
γ
P
:
Persistent
(
saved
γ
P
)
:
=
_
.
Lemma
saved_alloc
(
P
:
gname
→
iProp
)
:
fupd
M1
(
∃
γ
,
saved
γ
(
P
γ
)).
Proof
.
...
...
@@ -165,7 +165,7 @@ Module inv. Section inv.
(** And now we tie a bad knot. *)
Notation
"¬ P"
:
=
(
□
(
P
-
∗
fupd
M1
False
))%
I
:
uPred_scope
.
Definition
A
i
:
iProp
:
=
∃
P
,
¬
P
∗
saved
i
P
.
Global
Instance
A_persistent
i
:
Persistent
P
(
A
i
)
:
=
_
.
Global
Instance
A_persistent
i
:
Persistent
(
A
i
)
:
=
_
.
Lemma
A_alloc
:
fupd
M1
(
∃
i
,
saved
i
(
A
i
)).
Proof
.
by
apply
saved_alloc
.
Qed
.
...
...
theories/base_logic/lib/fancy_updates_from_vs.v
View file @
0ad1d2bd
...
...
@@ -13,7 +13,7 @@ Notation "P ={ E1 , E2 }=> Q" := (vs E1 E2 P Q)
format
"P ={ E1 , E2 }=> Q"
)
:
uPred_scope
.
Context
(
vs_ne
:
∀
E1
E2
,
NonExpansive2
(
vs
E1
E2
)).
Context
(
vs_persistent
:
∀
E1
E2
P
Q
,
Persistent
P
(
P
={
E1
,
E2
}=>
Q
)).
Context
(
vs_persistent
:
∀
E1
E2
P
Q
,
Persistent
(
P
={
E1
,
E2
}=>
Q
)).
Context
(
vs_impl
:
∀
E
P
Q
,
□
(
P
→
Q
)
⊢
P
={
E
,
E
}=>
Q
).
Context
(
vs_transitive
:
∀
E1
E2
E3
P
Q
R
,
...
...
@@ -24,7 +24,7 @@ Context (vs_frame_r : ∀ E1 E2 P Q R, (P ={E1,E2}=> Q) ⊢ P ∗ R ={E1,E2}=> Q
Context
(
vs_exists
:
∀
{
A
}
E1
E2
(
Φ
:
A
→
uPred
M
)
Q
,
(
∀
x
,
Φ
x
={
E1
,
E2
}=>
Q
)
⊢
(
∃
x
,
Φ
x
)
={
E1
,
E2
}=>
Q
).
Context
(
vs_persistent_intro_r
:
∀
E1
E2
P
Q
R
,
Persistent
P
R
→
Persistent
R
→
(
R
-
∗
(
P
={
E1
,
E2
}=>
Q
))
⊢
P
∗
R
={
E1
,
E2
}=>
Q
).
Definition
fupd
(
E1
E2
:
coPset
)
(
P
:
uPred
M
)
:
uPred
M
:
=
...
...
theories/base_logic/lib/fractional.v
View file @
0ad1d2bd
...
...
@@ -50,7 +50,7 @@ Section fractional.
(** Fractional and logical connectives *)
Global
Instance
persistent_fractional
P
:
Persistent
P
P
→
Fractional
(
λ
_
,
P
).
Persistent
P
→
Fractional
(
λ
_
,
P
).
Proof
.
intros
HP
q
q'
.
by
apply
uPred
.
always_sep_dup
.
Qed
.
Global
Instance
fractional_sep
Φ
Ψ
:
...
...
theories/base_logic/lib/gen_heap.v
View file @
0ad1d2bd
...
...
@@ -82,7 +82,7 @@ Section gen_heap.
Implicit
Types
v
:
V
.
(** General properties of mapsto *)
Global
Instance
mapsto_timeless
l
q
v
:
Timeless
P
(
l
↦
{
q
}
v
).
Global
Instance
mapsto_timeless
l
q
v
:
Timeless
(
l
↦
{
q
}
v
).
Proof
.
rewrite
mapsto_eq
/
mapsto_def
.
apply
_
.
Qed
.
Global
Instance
mapsto_fractional
l
v
:
Fractional
(
λ
q
,
l
↦
{
q
}
v
)%
I
.