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
Simon Spies
Iris
Commits
1fc3937f
Commit
1fc3937f
authored
Jun 24, 2016
by
Robbert Krebbers
Browse files
Rename uPred_const -> uPred_pure.
This is more consistent with the proofmode, where we also call it pure.
parent
d59fa2f7
Changes
9
Hide whitespace changes
Inline
Side-by-side
algebra/upred.v
View file @
1fc3937f
...
...
@@ -123,15 +123,15 @@ Instance uPred_entails_rewrite_relation M : RewriteRelation (@uPred_entails M).
Hint
Resolve
uPred_mono
uPred_closed
:
uPred_def
.
(** logical connectives *)
Program
Definition
uPred_
const
_def
{
M
}
(
φ
:
Prop
)
:
uPred
M
:
=
Program
Definition
uPred_
pure
_def
{
M
}
(
φ
:
Prop
)
:
uPred
M
:
=
{|
uPred_holds
n
x
:
=
φ
|}.
Solve
Obligations
with
done
.
Definition
uPred_
const
_aux
:
{
x
|
x
=
@
uPred_
const
_def
}.
by
eexists
.
Qed
.
Definition
uPred_
const
{
M
}
:
=
proj1_sig
uPred_
const
_aux
M
.
Definition
uPred_
const
_eq
:
@
uPred_
const
=
@
uPred_
const
_def
:
=
proj2_sig
uPred_
const
_aux
.
Definition
uPred_
pure
_aux
:
{
x
|
x
=
@
uPred_
pure
_def
}.
by
eexists
.
Qed
.
Definition
uPred_
pure
{
M
}
:
=
proj1_sig
uPred_
pure
_aux
M
.
Definition
uPred_
pure
_eq
:
@
uPred_
pure
=
@
uPred_
pure
_def
:
=
proj2_sig
uPred_
pure
_aux
.
Instance
uPred_inhabited
M
:
Inhabited
(
uPred
M
)
:
=
populate
(
uPred_
const
True
).
Instance
uPred_inhabited
M
:
Inhabited
(
uPred
M
)
:
=
populate
(
uPred_
pure
True
).
Program
Definition
uPred_and_def
{
M
}
(
P
Q
:
uPred
M
)
:
uPred
M
:
=
{|
uPred_holds
n
x
:
=
P
n
x
∧
Q
n
x
|}.
...
...
@@ -263,12 +263,12 @@ Notation "(⊢)" := uPred_entails (only parsing) : C_scope.
Notation
"P ⊣⊢ Q"
:
=
(
equiv
(
A
:
=
uPred
_
)
P
%
I
Q
%
I
)
(
at
level
95
,
no
associativity
)
:
C_scope
.
Notation
"(⊣⊢)"
:
=
(
equiv
(
A
:
=
uPred
_
))
(
only
parsing
)
:
C_scope
.
Notation
"■ φ"
:
=
(
uPred_
const
φ
%
C
%
type
)
Notation
"■ φ"
:
=
(
uPred_
pure
φ
%
C
%
type
)
(
at
level
20
,
right
associativity
)
:
uPred_scope
.
Notation
"x = y"
:
=
(
uPred_
const
(
x
%
C
%
type
=
y
%
C
%
type
))
:
uPred_scope
.
Notation
"x ⊥ y"
:
=
(
uPred_
const
(
x
%
C
%
type
⊥
y
%
C
%
type
))
:
uPred_scope
.
Notation
"'False'"
:
=
(
uPred_
const
False
)
:
uPred_scope
.
Notation
"'True'"
:
=
(
uPred_
const
True
)
:
uPred_scope
.
Notation
"x = y"
:
=
(
uPred_
pure
(
x
%
C
%
type
=
y
%
C
%
type
))
:
uPred_scope
.
Notation
"x ⊥ y"
:
=
(
uPred_
pure
(
x
%
C
%
type
⊥
y
%
C
%
type
))
:
uPred_scope
.
Notation
"'False'"
:
=
(
uPred_
pure
False
)
:
uPred_scope
.
Notation
"'True'"
:
=
(
uPred_
pure
True
)
:
uPred_scope
.
Infix
"∧"
:
=
uPred_and
:
uPred_scope
.
Notation
"(∧)"
:
=
uPred_and
(
only
parsing
)
:
uPred_scope
.
Infix
"∨"
:
=
uPred_or
:
uPred_scope
.
...
...
@@ -308,7 +308,7 @@ Arguments persistentP {_} _ {_}.
Module
uPred
.
Definition
unseal
:
=
(
uPred_
const
_eq
,
uPred_and_eq
,
uPred_or_eq
,
uPred_impl_eq
,
uPred_forall_eq
,
(
uPred_
pure
_eq
,
uPred_and_eq
,
uPred_or_eq
,
uPred_impl_eq
,
uPred_forall_eq
,
uPred_exist_eq
,
uPred_eq_eq
,
uPred_sep_eq
,
uPred_wand_eq
,
uPred_always_eq
,
uPred_later_eq
,
uPred_ownM_eq
,
uPred_valid_eq
).
Ltac
unseal
:
=
rewrite
!
unseal
/=.
...
...
@@ -353,7 +353,7 @@ Lemma entails_equiv_r (P Q R : uPred M) : (P ⊢ Q) → (Q ⊣⊢ R) → (P ⊢
Proof
.
by
intros
?
<-.
Qed
.
(** Non-expansiveness and setoid morphisms *)
Global
Instance
const
_proper
:
Proper
(
iff
==>
(
⊣
⊢
))
(@
uPred_
const
M
).
Global
Instance
pure
_proper
:
Proper
(
iff
==>
(
⊣
⊢
))
(@
uPred_
pure
M
).
Proof
.
intros
φ
1
φ
2
H
φ
.
by
unseal
;
split
=>
-[|
n
]
?
;
try
apply
H
φ
.
Qed
.
Global
Instance
and_ne
n
:
Proper
(
dist
n
==>
dist
n
==>
dist
n
)
(@
uPred_and
M
).
Proof
.
...
...
@@ -459,9 +459,9 @@ Global Instance iff_proper :
Proper
((
⊣
⊢
)
==>
(
⊣
⊢
)
==>
(
⊣
⊢
))
(@
uPred_iff
M
)
:
=
ne_proper_2
_
.
(** Introduction and elimination rules *)
Lemma
const
_intro
φ
P
:
φ
→
P
⊢
■
φ
.
Lemma
pure
_intro
φ
P
:
φ
→
P
⊢
■
φ
.
Proof
.
by
intros
?
;
unseal
;
split
.
Qed
.
Lemma
const
_elim
φ
Q
R
:
(
Q
⊢
■
φ
)
→
(
φ
→
Q
⊢
R
)
→
Q
⊢
R
.
Lemma
pure
_elim
φ
Q
R
:
(
Q
⊢
■
φ
)
→
(
φ
→
Q
⊢
R
)
→
Q
⊢
R
.
Proof
.
unseal
;
intros
HQP
HQR
;
split
=>
n
x
??
;
apply
HQR
;
first
eapply
HQP
;
eauto
.
Qed
.
...
...
@@ -517,9 +517,9 @@ Qed.
(* Derived logical stuff *)
Lemma
False_elim
P
:
False
⊢
P
.
Proof
.
by
apply
(
const
_elim
False
).
Qed
.
Proof
.
by
apply
(
pure
_elim
False
).
Qed
.
Lemma
True_intro
P
:
P
⊢
True
.
Proof
.
by
apply
const
_intro
.
Qed
.
Proof
.
by
apply
pure
_intro
.
Qed
.
Lemma
and_elim_l'
P
Q
R
:
(
P
⊢
R
)
→
P
∧
Q
⊢
R
.
Proof
.
by
rewrite
and_elim_l
.
Qed
.
Lemma
and_elim_r'
P
Q
R
:
(
Q
⊢
R
)
→
P
∧
Q
⊢
R
.
...
...
@@ -562,8 +562,8 @@ Qed.
Lemma
equiv_iff
P
Q
:
(
P
⊣
⊢
Q
)
→
True
⊢
P
↔
Q
.
Proof
.
intros
->
;
apply
iff_refl
.
Qed
.
Lemma
const
_mono
φ
1
φ
2
:
(
φ
1
→
φ
2
)
→
■
φ
1
⊢
■
φ
2
.
Proof
.
intros
;
apply
const
_elim
with
φ
1
;
eauto
using
const
_intro
.
Qed
.
Lemma
pure
_mono
φ
1
φ
2
:
(
φ
1
→
φ
2
)
→
■
φ
1
⊢
■
φ
2
.
Proof
.
intros
;
apply
pure
_elim
with
φ
1
;
eauto
using
pure
_intro
.
Qed
.
Lemma
and_mono
P
P'
Q
Q'
:
(
P
⊢
Q
)
→
(
P'
⊢
Q'
)
→
P
∧
P'
⊢
Q
∧
Q'
.
Proof
.
auto
.
Qed
.
Lemma
and_mono_l
P
P'
Q
:
(
P
⊢
Q
)
→
P
∧
P'
⊢
Q
∧
P'
.
...
...
@@ -589,8 +589,8 @@ Qed.
Lemma
exist_mono
{
A
}
(
Φ
Ψ
:
A
→
uPred
M
)
:
(
∀
a
,
Φ
a
⊢
Ψ
a
)
→
(
∃
a
,
Φ
a
)
⊢
∃
a
,
Ψ
a
.
Proof
.
intros
H
Φ
.
apply
exist_elim
=>
a
;
rewrite
(
H
Φ
a
)
;
apply
exist_intro
.
Qed
.
Global
Instance
const
_mono'
:
Proper
(
impl
==>
(
⊢
))
(@
uPred_
const
M
).
Proof
.
intros
φ
1
φ
2
;
apply
const
_mono
.
Qed
.
Global
Instance
pure
_mono'
:
Proper
(
impl
==>
(
⊢
))
(@
uPred_
pure
M
).
Proof
.
intros
φ
1
φ
2
;
apply
pure
_mono
.
Qed
.
Global
Instance
and_mono'
:
Proper
((
⊢
)
==>
(
⊢
)
==>
(
⊢
))
(@
uPred_and
M
).
Proof
.
by
intros
P
P'
HP
Q
Q'
HQ
;
apply
and_mono
.
Qed
.
Global
Instance
and_flip_mono'
:
...
...
@@ -673,18 +673,18 @@ Proof.
rewrite
-(
comm
_
P
)
and_exist_l
.
apply
exist_proper
=>
a
.
by
rewrite
comm
.
Qed
.
Lemma
const
_intro_l
φ
Q
R
:
φ
→
(
■
φ
∧
Q
⊢
R
)
→
Q
⊢
R
.
Proof
.
intros
?
<-
;
auto
using
const
_intro
.
Qed
.
Lemma
const
_intro_r
φ
Q
R
:
φ
→
(
Q
∧
■
φ
⊢
R
)
→
Q
⊢
R
.
Proof
.
intros
?
<-
;
auto
using
const
_intro
.
Qed
.
Lemma
const
_intro_impl
φ
Q
R
:
φ
→
(
Q
⊢
■
φ
→
R
)
→
Q
⊢
R
.
Proof
.
intros
?
->.
eauto
using
const
_intro_l
,
impl_elim_r
.
Qed
.
Lemma
const
_elim_l
φ
Q
R
:
(
φ
→
Q
⊢
R
)
→
■
φ
∧
Q
⊢
R
.
Proof
.
intros
;
apply
const
_elim
with
φ
;
eauto
.
Qed
.
Lemma
const
_elim_r
φ
Q
R
:
(
φ
→
Q
⊢
R
)
→
Q
∧
■
φ
⊢
R
.
Proof
.
intros
;
apply
const
_elim
with
φ
;
eauto
.
Qed
.
Lemma
const
_equiv
(
φ
:
Prop
)
:
φ
→
■
φ
⊣
⊢
True
.
Proof
.
intros
;
apply
(
anti_symm
_
)
;
auto
using
const
_intro
.
Qed
.
Lemma
pure
_intro_l
φ
Q
R
:
φ
→
(
■
φ
∧
Q
⊢
R
)
→
Q
⊢
R
.
Proof
.
intros
?
<-
;
auto
using
pure
_intro
.
Qed
.
Lemma
pure
_intro_r
φ
Q
R
:
φ
→
(
Q
∧
■
φ
⊢
R
)
→
Q
⊢
R
.
Proof
.
intros
?
<-
;
auto
using
pure
_intro
.
Qed
.
Lemma
pure
_intro_impl
φ
Q
R
:
φ
→
(
Q
⊢
■
φ
→
R
)
→
Q
⊢
R
.
Proof
.
intros
?
->.
eauto
using
pure
_intro_l
,
impl_elim_r
.
Qed
.
Lemma
pure
_elim_l
φ
Q
R
:
(
φ
→
Q
⊢
R
)
→
■
φ
∧
Q
⊢
R
.
Proof
.
intros
;
apply
pure
_elim
with
φ
;
eauto
.
Qed
.
Lemma
pure
_elim_r
φ
Q
R
:
(
φ
→
Q
⊢
R
)
→
Q
∧
■
φ
⊢
R
.
Proof
.
intros
;
apply
pure
_elim
with
φ
;
eauto
.
Qed
.
Lemma
pure
_equiv
(
φ
:
Prop
)
:
φ
→
■
φ
⊣
⊢
True
.
Proof
.
intros
;
apply
(
anti_symm
_
)
;
auto
using
pure
_intro
.
Qed
.
Lemma
eq_refl'
{
A
:
cofeT
}
(
a
:
A
)
P
:
P
⊢
a
≡
a
.
Proof
.
rewrite
(
True_intro
P
).
apply
eq_refl
.
Qed
.
...
...
@@ -822,10 +822,10 @@ Lemma sep_and P Q : (P ★ Q) ⊢ (P ∧ Q).
Proof
.
auto
.
Qed
.
Lemma
impl_wand
P
Q
:
(
P
→
Q
)
⊢
P
-
★
Q
.
Proof
.
apply
wand_intro_r
,
impl_elim
with
P
;
auto
.
Qed
.
Lemma
const
_elim_sep_l
φ
Q
R
:
(
φ
→
Q
⊢
R
)
→
■
φ
★
Q
⊢
R
.
Proof
.
intros
;
apply
const
_elim
with
φ
;
eauto
.
Qed
.
Lemma
const
_elim_sep_r
φ
Q
R
:
(
φ
→
Q
⊢
R
)
→
Q
★
■
φ
⊢
R
.
Proof
.
intros
;
apply
const
_elim
with
φ
;
eauto
.
Qed
.
Lemma
pure
_elim_sep_l
φ
Q
R
:
(
φ
→
Q
⊢
R
)
→
■
φ
★
Q
⊢
R
.
Proof
.
intros
;
apply
pure
_elim
with
φ
;
eauto
.
Qed
.
Lemma
pure
_elim_sep_r
φ
Q
R
:
(
φ
→
Q
⊢
R
)
→
Q
★
■
φ
⊢
R
.
Proof
.
intros
;
apply
pure
_elim
with
φ
;
eauto
.
Qed
.
Global
Instance
sep_False
:
LeftAbsorb
(
⊣
⊢
)
False
%
I
(@
uPred_sep
M
).
Proof
.
intros
P
;
apply
(
anti_symm
_
)
;
auto
.
Qed
.
...
...
@@ -858,7 +858,7 @@ Lemma sep_forall_r {A} (Φ : A → uPred M) Q : (∀ a, Φ a) ★ Q ⊢ ∀ a,
Proof
.
by
apply
forall_intro
=>
a
;
rewrite
forall_elim
.
Qed
.
(* Always *)
Lemma
always_
const
φ
:
□
■
φ
⊣
⊢
■
φ
.
Lemma
always_
pure
φ
:
□
■
φ
⊣
⊢
■
φ
.
Proof
.
by
unseal
.
Qed
.
Lemma
always_elim
P
:
□
P
⊢
P
.
Proof
.
...
...
@@ -910,7 +910,7 @@ Proof.
apply
(
anti_symm
(
⊢
))
;
auto
using
always_elim
.
apply
(
eq_rewrite
a
b
(
λ
b
,
□
(
a
≡
b
))%
I
)
;
auto
.
{
intros
n
;
solve_proper
.
}
rewrite
-(
eq_refl
a
)
always_
const
;
auto
.
rewrite
-(
eq_refl
a
)
always_
pure
;
auto
.
Qed
.
Lemma
always_and_sep
P
Q
:
□
(
P
∧
Q
)
⊣
⊢
□
(
P
★
Q
).
Proof
.
apply
(
anti_symm
(
⊢
))
;
auto
using
always_and_sep_1
.
Qed
.
...
...
@@ -1098,7 +1098,7 @@ Proof.
apply
HP
,
uPred_closed
with
n
;
eauto
using
cmra_validN_le
.
Qed
.
Global
Instance
const
_timeless
φ
:
TimelessP
(
■
φ
:
uPred
M
)%
I
.
Global
Instance
pure
_timeless
φ
:
TimelessP
(
■
φ
:
uPred
M
)%
I
.
Proof
.
by
apply
timelessP_spec
;
unseal
=>
-[|
n
]
x
.
Qed
.
Global
Instance
valid_timeless
{
A
:
cmraT
}
`
{
CMRADiscrete
A
}
(
a
:
A
)
:
TimelessP
(
✓
a
:
uPred
M
)%
I
.
...
...
@@ -1141,7 +1141,7 @@ Qed.
Global
Instance
always_timeless
P
:
TimelessP
P
→
TimelessP
(
□
P
).
Proof
.
intros
?
;
rewrite
/
TimelessP
.
by
rewrite
-
always_
const
-!
always_later
-
always_or
;
apply
always_mono
.
by
rewrite
-
always_
pure
-!
always_later
-
always_or
;
apply
always_mono
.
Qed
.
Global
Instance
always_if_timeless
p
P
:
TimelessP
P
→
TimelessP
(
□
?p
P
).
Proof
.
destruct
p
;
apply
_
.
Qed
.
...
...
@@ -1157,8 +1157,8 @@ Proof.
Qed
.
(* Persistence *)
Global
Instance
const
_persistent
φ
:
PersistentP
(
■
φ
:
uPred
M
)%
I
.
Proof
.
by
rewrite
/
PersistentP
always_
const
.
Qed
.
Global
Instance
pure
_persistent
φ
:
PersistentP
(
■
φ
:
uPred
M
)%
I
.
Proof
.
by
rewrite
/
PersistentP
always_
pure
.
Qed
.
Global
Instance
always_persistent
P
:
PersistentP
(
□
P
).
Proof
.
by
intros
;
apply
always_intro'
.
Qed
.
Global
Instance
and_persistent
P
Q
:
...
...
@@ -1210,7 +1210,7 @@ Proof. by rewrite -(always_always Q); apply always_entails_r'. Qed.
End
uPred_logic
.
(* Hint DB for the logic *)
Hint
Resolve
const
_intro
.
Hint
Resolve
pure
_intro
.
Hint
Resolve
or_elim
or_intro_l'
or_intro_r'
:
I
.
Hint
Resolve
and_intro
and_elim_l'
and_elim_r'
:
I
.
Hint
Resolve
always_mono
:
I
.
...
...
algebra/upred_big_op.v
View file @
1fc3937f
...
...
@@ -223,7 +223,7 @@ Section gmap.
(
□
[
★
map
]
k
↦
x
∈
m
,
Φ
k
x
)
⊣
⊢
([
★
map
]
k
↦
x
∈
m
,
□
Φ
k
x
).
Proof
.
rewrite
/
uPred_big_sepM
.
induction
(
map_to_list
m
)
as
[|[
i
x
]
l
IH
]
;
csimpl
;
rewrite
?always_
const
//.
induction
(
map_to_list
m
)
as
[|[
i
x
]
l
IH
]
;
csimpl
;
rewrite
?always_
pure
//.
by
rewrite
always_sep
IH
.
Qed
.
...
...
@@ -237,14 +237,14 @@ Section gmap.
Proof
.
intros
.
apply
(
anti_symm
_
).
{
apply
forall_intro
=>
k
;
apply
forall_intro
=>
x
.
apply
impl_intro_l
,
const
_elim_l
=>
?
;
by
apply
big_sepM_lookup
.
}
apply
impl_intro_l
,
pure
_elim_l
=>
?
;
by
apply
big_sepM_lookup
.
}
rewrite
/
uPred_big_sepM
.
setoid_rewrite
<-
elem_of_map_to_list
.
induction
(
map_to_list
m
)
as
[|[
i
x
]
l
IH
]
;
csimpl
;
auto
.
rewrite
-
always_and_sep_l
;
apply
and_intro
.
-
rewrite
(
forall_elim
i
)
(
forall_elim
x
)
const
_equiv
;
last
by
left
.
-
rewrite
(
forall_elim
i
)
(
forall_elim
x
)
pure
_equiv
;
last
by
left
.
by
rewrite
True_impl
.
-
rewrite
-
IH
.
apply
forall_mono
=>
k
;
apply
forall_mono
=>
y
.
apply
impl_intro_l
,
const
_elim_l
=>
?.
rewrite
const
_equiv
;
last
by
right
.
apply
impl_intro_l
,
pure
_elim_l
=>
?.
rewrite
pure
_equiv
;
last
by
right
.
by
rewrite
True_impl
.
Qed
.
...
...
@@ -253,7 +253,7 @@ Section gmap.
⊢
[
★
map
]
k
↦
x
∈
m
,
Ψ
k
x
.
Proof
.
rewrite
always_and_sep_l
.
do
2
setoid_rewrite
always_forall
.
setoid_rewrite
always_impl
;
setoid_rewrite
always_
const
.
setoid_rewrite
always_impl
;
setoid_rewrite
always_
pure
.
rewrite
-
big_sepM_forall
-
big_sepM_sepM
.
apply
big_sepM_mono
;
auto
=>
k
x
?.
by
rewrite
-
always_wand_impl
always_elim
wand_elim_l
.
Qed
.
...
...
@@ -345,7 +345,7 @@ Section gset.
Lemma
big_sepS_always
Φ
X
:
□
([
★
set
]
y
∈
X
,
Φ
y
)
⊣
⊢
([
★
set
]
y
∈
X
,
□
Φ
y
).
Proof
.
rewrite
/
uPred_big_sepS
.
induction
(
elements
X
)
as
[|
x
l
IH
]
;
csimpl
;
first
by
rewrite
?always_
const
.
induction
(
elements
X
)
as
[|
x
l
IH
]
;
csimpl
;
first
by
rewrite
?always_
pure
.
by
rewrite
always_sep
IH
.
Qed
.
...
...
@@ -358,13 +358,13 @@ Section gset.
Proof
.
intros
.
apply
(
anti_symm
_
).
{
apply
forall_intro
=>
x
.
apply
impl_intro_l
,
const
_elim_l
=>
?
;
by
apply
big_sepS_elem_of
.
}
apply
impl_intro_l
,
pure
_elim_l
=>
?
;
by
apply
big_sepS_elem_of
.
}
rewrite
/
uPred_big_sepS
.
setoid_rewrite
<-
elem_of_elements
.
induction
(
elements
X
)
as
[|
x
l
IH
]
;
csimpl
;
auto
.
rewrite
-
always_and_sep_l
;
apply
and_intro
.
-
rewrite
(
forall_elim
x
)
const
_equiv
;
last
by
left
.
by
rewrite
True_impl
.
-
rewrite
(
forall_elim
x
)
pure
_equiv
;
last
by
left
.
by
rewrite
True_impl
.
-
rewrite
-
IH
.
apply
forall_mono
=>
y
.
apply
impl_intro_l
,
const
_elim_l
=>
?.
rewrite
const
_equiv
;
last
by
right
.
apply
impl_intro_l
,
pure
_elim_l
=>
?.
rewrite
pure
_equiv
;
last
by
right
.
by
rewrite
True_impl
.
Qed
.
...
...
@@ -372,7 +372,7 @@ Section gset.
□
(
∀
x
,
■
(
x
∈
X
)
→
Φ
x
→
Ψ
x
)
∧
([
★
set
]
x
∈
X
,
Φ
x
)
⊢
[
★
set
]
x
∈
X
,
Ψ
x
.
Proof
.
rewrite
always_and_sep_l
always_forall
.
setoid_rewrite
always_impl
;
setoid_rewrite
always_
const
.
setoid_rewrite
always_impl
;
setoid_rewrite
always_
pure
.
rewrite
-
big_sepS_forall
-
big_sepS_sepS
.
apply
big_sepS_mono
;
auto
=>
x
?.
by
rewrite
-
always_wand_impl
always_elim
wand_elim_l
.
Qed
.
...
...
heap_lang/heap.v
View file @
1fc3937f
...
...
@@ -136,12 +136,12 @@ Section heap.
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
.
}
{
by
rewrite
heap_mapsto_op_eq
pure
_equiv
//
left_id
.
}
rewrite
heap_mapsto_eq
-
auth_own_op
op_singleton
pair_op
dec_agree_ne
//.
apply
(
anti_symm
(
⊢
))
;
last
by
apply
const
_elim_l
.
apply
(
anti_symm
(
⊢
))
;
last
by
apply
pure
_elim_l
.
rewrite
auth_own_valid
gmap_validI
(
forall_elim
l
)
lookup_singleton
.
rewrite
option_validI
prod_validI
frac_validI
discrete_valid
.
by
apply
const
_elim_r
.
by
apply
pure
_elim_r
.
Qed
.
Lemma
heap_mapsto_op_split
l
q
v
:
l
↦
{
q
}
v
⊣
⊢
(
l
↦
{
q
/
2
}
v
★
l
↦
{
q
/
2
}
v
).
...
...
heap_lang/lib/assert.v
View file @
1fc3937f
...
...
@@ -19,5 +19,5 @@ Lemma wp_assert' {Σ} (Φ : val → iProp heap_lang Σ) e :
WP
e
{{
v
,
v
=
#
true
∧
▷
Φ
#()
}}
⊢
WP
Assert
e
{{
Φ
}}.
Proof
.
rewrite
/
Assert
.
wp_focus
e
;
apply
wp_mono
=>
v
.
apply
uPred
.
const
_elim_l
=>->.
apply
wp_assert
.
apply
uPred
.
pure
_elim_l
=>->.
apply
wp_assert
.
Qed
.
program_logic/ghost_ownership.v
View file @
1fc3937f
...
...
@@ -54,8 +54,8 @@ Proof.
eapply
pvs_ownG_updateP
,
(
iprod_singleton_updateP_empty
(
inG_id
i
))
;
first
(
eapply
alloc_updateP_strong'
,
cmra_transport_valid
,
Ha
)
;
naive_solver
.
-
apply
exist_elim
=>
m
;
apply
const
_elim_l
=>-[
γ
[
Hfresh
->]].
by
rewrite
!
own_eq
/
own_def
-(
exist_intro
γ
)
const
_equiv
//
left_id
.
-
apply
exist_elim
=>
m
;
apply
pure
_elim_l
=>-[
γ
[
Hfresh
->]].
by
rewrite
!
own_eq
/
own_def
-(
exist_intro
γ
)
pure
_equiv
//
left_id
.
Qed
.
Lemma
own_alloc
a
E
:
✓
a
→
True
={
E
}=>
∃
γ
,
own
γ
a
.
Proof
.
...
...
@@ -70,14 +70,14 @@ Proof.
-
eapply
pvs_ownG_updateP
,
iprod_singleton_updateP
;
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
|].
-
apply
exist_elim
=>
m
;
apply
pure
_elim_l
=>-[
a'
[->
HP
]].
rewrite
-(
exist_intro
a'
).
by
apply
and_intro
;
[
apply
pure
_intro
|].
Qed
.
Lemma
own_update
γ
a
a'
E
:
a
~~>
a'
→
own
γ
a
={
E
}=>
own
γ
a'
.
Proof
.
intros
;
rewrite
(
own_updateP
(
a'
=))
;
last
by
apply
cmra_update_updateP
.
by
apply
pvs_mono
,
exist_elim
=>
a''
;
apply
const
_elim_l
=>
->.
by
apply
pvs_mono
,
exist_elim
=>
a''
;
apply
pure
_elim_l
=>
->.
Qed
.
End
global
.
...
...
program_logic/lifting.v
View file @
1fc3937f
...
...
@@ -76,9 +76,9 @@ Proof.
apply
forall_intro
=>
e2'
;
apply
forall_intro
=>
σ
2
'
.
apply
forall_intro
=>
ef
;
apply
wand_intro_l
.
rewrite
always_and_sep_l
-
assoc
-
always_and_sep_l
.
apply
const
_elim_l
=>-[[
v2
Hv
]
?]
/=.
apply
pure
_elim_l
=>-[[
v2
Hv
]
?]
/=.
rewrite
-
pvs_intro
.
rewrite
(
forall_elim
v2
)
(
forall_elim
σ
2
'
)
(
forall_elim
ef
)
const
_equiv
//.
rewrite
(
forall_elim
v2
)
(
forall_elim
σ
2
'
)
(
forall_elim
ef
)
pure
_equiv
//.
rewrite
left_id
wand_elim_r
-(
wp_value
_
_
e2'
v2
)
//.
by
erewrite
of_to_val
.
Qed
.
...
...
@@ -96,7 +96,7 @@ Proof.
apply
forall_intro
=>
e2'
;
apply
forall_intro
=>
σ
2
'
;
apply
forall_intro
=>
ef'
.
apply
wand_intro_l
.
rewrite
always_and_sep_l
-
assoc
-
always_and_sep_l
to_of_val
.
apply
const
_elim_l
=>-[->
[[->]
->]]
/=.
by
rewrite
wand_elim_r
.
apply
pure
_elim_l
=>-[->
[[->]
->]]
/=.
by
rewrite
wand_elim_r
.
Qed
.
Lemma
wp_lift_pure_det_step
{
E
Φ
}
e1
e2
ef
:
...
...
@@ -108,6 +108,6 @@ Proof.
intros
.
rewrite
-(
wp_lift_pure_step
E
(
λ
e2'
ef'
,
e2
=
e2'
∧
ef
=
ef'
)
_
e1
)
//=.
apply
later_mono
,
forall_intro
=>
e'
;
apply
forall_intro
=>
ef'
.
by
apply
impl_intro_l
,
const
_elim_l
=>-[->
->].
by
apply
impl_intro_l
,
pure
_elim_l
=>-[->
->].
Qed
.
End
lifting
.
program_logic/pviewshifts.v
View file @
1fc3937f
...
...
@@ -224,7 +224,7 @@ Proof. auto using pvs_mask_frame'. Qed.
Lemma
pvs_ownG_update
E
m
m'
:
m
~~>
m'
→
ownG
m
={
E
}=>
ownG
m'
.
Proof
.
intros
;
rewrite
(
pvs_ownG_updateP
E
_
(
m'
=))
;
last
by
apply
cmra_update_updateP
.
by
apply
pvs_mono
,
uPred
.
exist_elim
=>
m''
;
apply
uPred
.
const
_elim_l
=>
->.
by
apply
pvs_mono
,
uPred
.
exist_elim
=>
m''
;
apply
uPred
.
pure
_elim_l
=>
->.
Qed
.
End
pvs
.
...
...
proofmode/coq_tactics.v
View file @
1fc3937f
...
...
@@ -117,15 +117,15 @@ Qed.
Lemma
envs_lookup_sound
Δ
i
p
P
:
envs_lookup
i
Δ
=
Some
(
p
,
P
)
→
Δ
⊢
□
?p
P
★
envs_delete
i
p
Δ
.
Proof
.
rewrite
/
envs_lookup
/
envs_delete
/
of_envs
=>?
;
apply
const
_elim_sep_l
=>
Hwf
.
rewrite
/
envs_lookup
/
envs_delete
/
of_envs
=>?
;
apply
pure
_elim_sep_l
=>
Hwf
.
destruct
Δ
as
[
Γ
p
Γ
s
],
(
Γ
p
!!
i
)
eqn
:
?
;
simplify_eq
/=.
-
rewrite
(
env_lookup_perm
Γ
p
)
//=
always_and_sep
always_sep
.
ecancel
[
□
[
∧
]
_;
□
P
;
[
★
]
_
]%
I
;
apply
const
_intro
.
ecancel
[
□
[
∧
]
_;
□
P
;
[
★
]
_
]%
I
;
apply
pure
_intro
.
destruct
Hwf
;
constructor
;
naive_solver
eauto
using
env_delete_wf
,
env_delete_fresh
.
-
destruct
(
Γ
s
!!
i
)
eqn
:
?
;
simplify_eq
/=.
rewrite
(
env_lookup_perm
Γ
s
)
//=.
ecancel
[
□
[
∧
]
_;
P
;
[
★
]
_
]%
I
;
apply
const
_intro
.
ecancel
[
□
[
∧
]
_;
P
;
[
★
]
_
]%
I
;
apply
pure
_intro
.
destruct
Hwf
;
constructor
;
naive_solver
eauto
using
env_delete_wf
,
env_delete_fresh
.
Qed
.
...
...
@@ -141,13 +141,13 @@ Qed.
Lemma
envs_lookup_split
Δ
i
p
P
:
envs_lookup
i
Δ
=
Some
(
p
,
P
)
→
Δ
⊢
□
?p
P
★
(
□
?p
P
-
★
Δ
).
Proof
.
rewrite
/
envs_lookup
/
of_envs
=>?
;
apply
const
_elim_sep_l
=>
Hwf
.
rewrite
/
envs_lookup
/
of_envs
=>?
;
apply
pure
_elim_sep_l
=>
Hwf
.
destruct
Δ
as
[
Γ
p
Γ
s
],
(
Γ
p
!!
i
)
eqn
:
?
;
simplify_eq
/=.
-
rewrite
(
env_lookup_perm
Γ
p
)
//=
always_and_sep
always_sep
.
rewrite
const
_equiv
//
left_id
.
rewrite
pure
_equiv
//
left_id
.
cancel
[
□
P
]%
I
.
apply
wand_intro_l
.
solve_sep_entails
.
-
destruct
(
Γ
s
!!
i
)
eqn
:
?
;
simplify_eq
/=.
rewrite
(
env_lookup_perm
Γ
s
)
//=.
rewrite
const
_equiv
//
left_id
.
rewrite
(
env_lookup_perm
Γ
s
)
//=.
rewrite
pure
_equiv
//
left_id
.
cancel
[
P
].
apply
wand_intro_l
.
solve_sep_entails
.
Qed
.
...
...
@@ -160,11 +160,11 @@ Proof. intros [? ->]%envs_lookup_delete_Some. by apply envs_lookup_sound'. Qed.
Lemma
envs_app_sound
Δ
Δ
'
p
Γ
:
envs_app
p
Γ
Δ
=
Some
Δ
'
→
Δ
⊢
□
?p
[
★
]
Γ
-
★
Δ
'
.
Proof
.
rewrite
/
of_envs
/
envs_app
=>
?
;
apply
const
_elim_sep_l
=>
Hwf
.
rewrite
/
of_envs
/
envs_app
=>
?
;
apply
pure
_elim_sep_l
=>
Hwf
.
destruct
Δ
as
[
Γ
p
Γ
s
],
p
;
simplify_eq
/=.
-
destruct
(
env_app
Γ
Γ
s
)
eqn
:
Happ
,
(
env_app
Γ
Γ
p
)
as
[
Γ
p'
|]
eqn
:
?
;
simplify_eq
/=.
apply
wand_intro_l
,
sep_intro_True_l
;
[
apply
const
_intro
|].
apply
wand_intro_l
,
sep_intro_True_l
;
[
apply
pure
_intro
|].
+
destruct
Hwf
;
constructor
;
simpl
;
eauto
using
env_app_wf
.
intros
j
.
apply
(
env_app_disjoint
_
_
_
j
)
in
Happ
.
naive_solver
eauto
using
env_app_fresh
.
...
...
@@ -173,7 +173,7 @@ Proof.
solve_sep_entails
.
-
destruct
(
env_app
Γ
Γ
p
)
eqn
:
Happ
,
(
env_app
Γ
Γ
s
)
as
[
Γ
s'
|]
eqn
:
?
;
simplify_eq
/=.
apply
wand_intro_l
,
sep_intro_True_l
;
[
apply
const
_intro
|].
apply
wand_intro_l
,
sep_intro_True_l
;
[
apply
pure
_intro
|].
+
destruct
Hwf
;
constructor
;
simpl
;
eauto
using
env_app_wf
.
intros
j
.
apply
(
env_app_disjoint
_
_
_
j
)
in
Happ
.
naive_solver
eauto
using
env_app_fresh
.
...
...
@@ -185,10 +185,10 @@ Lemma envs_simple_replace_sound' Δ Δ' i p Γ :
envs_delete
i
p
Δ
⊢
□
?p
[
★
]
Γ
-
★
Δ
'
.
Proof
.
rewrite
/
envs_simple_replace
/
envs_delete
/
of_envs
=>
?.
apply
const
_elim_sep_l
=>
Hwf
.
destruct
Δ
as
[
Γ
p
Γ
s
],
p
;
simplify_eq
/=.
apply
pure
_elim_sep_l
=>
Hwf
.
destruct
Δ
as
[
Γ
p
Γ
s
],
p
;
simplify_eq
/=.
-
destruct
(
env_app
Γ
Γ
s
)
eqn
:
Happ
,
(
env_replace
i
Γ
Γ
p
)
as
[
Γ
p'
|]
eqn
:
?
;
simplify_eq
/=.
apply
wand_intro_l
,
sep_intro_True_l
;
[
apply
const
_intro
|].
apply
wand_intro_l
,
sep_intro_True_l
;
[
apply
pure
_intro
|].
+
destruct
Hwf
;
constructor
;
simpl
;
eauto
using
env_replace_wf
.
intros
j
.
apply
(
env_app_disjoint
_
_
_
j
)
in
Happ
.
destruct
(
decide
(
i
=
j
))
;
try
naive_solver
eauto
using
env_replace_fresh
.
...
...
@@ -197,7 +197,7 @@ Proof.
solve_sep_entails
.
-
destruct
(
env_app
Γ
Γ
p
)
eqn
:
Happ
,
(
env_replace
i
Γ
Γ
s
)
as
[
Γ
s'
|]
eqn
:
?
;
simplify_eq
/=.
apply
wand_intro_l
,
sep_intro_True_l
;
[
apply
const
_intro
|].
apply
wand_intro_l
,
sep_intro_True_l
;
[
apply
pure
_intro
|].
+
destruct
Hwf
;
constructor
;
simpl
;
eauto
using
env_replace_wf
.
intros
j
.
apply
(
env_app_disjoint
_
_
_
j
)
in
Happ
.
destruct
(
decide
(
i
=
j
))
;
try
naive_solver
eauto
using
env_replace_fresh
.
...
...
@@ -225,19 +225,19 @@ Proof. intros. by rewrite envs_lookup_sound// envs_replace_sound'//. Qed.
Lemma
envs_split_sound
Δ
lr
js
Δ
1
Δ
2
:
envs_split
lr
js
Δ
=
Some
(
Δ
1
,
Δ
2
)
→
Δ
⊢
Δ
1
★
Δ
2
.
Proof
.
rewrite
/
envs_split
/
of_envs
=>
?
;
apply
const
_elim_sep_l
=>
Hwf
.
rewrite
/
envs_split
/
of_envs
=>
?
;
apply
pure
_elim_sep_l
=>
Hwf
.
destruct
Δ
as
[
Γ
p
Γ
s
],
(
env_split
js
_
)
as
[[
Γ
s1
Γ
s2
]|]
eqn
:
?
;
simplify_eq
/=.
rewrite
(
env_split_perm
Γ
s
)
//
big_sep_app
{
1
}
always_sep_dup'
.
destruct
lr
;
simplify_eq
/=
;
cancel
[
□
[
∧
]
Γ
p
;
□
[
∧
]
Γ
p
;
[
★
]
Γ
s1
;
[
★
]
Γ
s2
]%
I
;
destruct
Hwf
;
apply
sep_intro_True_l
;
apply
const
_intro
;
constructor
;
destruct
Hwf
;
apply
sep_intro_True_l
;
apply
pure
_intro
;
constructor
;
naive_solver
eauto
using
env_split_wf_1
,
env_split_wf_2
,
env_split_fresh_1
,
env_split_fresh_2
.
Qed
.
Lemma
envs_clear_spatial_sound
Δ
:
Δ
⊢
envs_clear_spatial
Δ
★
[
★
]
env_spatial
Δ
.
Proof
.
rewrite
/
of_envs
/
envs_clear_spatial
/=
;
apply
const
_elim_sep_l
=>
Hwf
.
rewrite
right_id
-
assoc
;
apply
sep_intro_True_l
;
[
apply
const
_intro
|
done
].
rewrite
/
of_envs
/
envs_clear_spatial
/=
;
apply
pure
_elim_sep_l
=>
Hwf
.
rewrite
right_id
-
assoc
;
apply
sep_intro_True_l
;
[
apply
pure
_intro
|
done
].
destruct
Hwf
;
constructor
;
simpl
;
auto
using
Enil_wf
.
Qed
.
...
...
@@ -270,8 +270,8 @@ Proof. intros [??] ?; constructor; eauto using env_Forall2_impl. Qed.
Global
Instance
of_envs_mono
:
Proper
(
envs_Forall2
(
⊢
)
==>
(
⊢
))
(@
of_envs
M
).
Proof
.
intros
[
Γ
p1
Γ
s1
]
[
Γ
p2
Γ
s2
]
[
Hp
Hs
]
;
unfold
of_envs
;
simpl
in
*.
apply
const
_elim_sep_l
=>
Hwf
.
apply
sep_intro_True_l
.
-
destruct
Hwf
;
apply
const
_intro
;
constructor
;
apply
pure
_elim_sep_l
=>
Hwf
.
apply
sep_intro_True_l
.
-
destruct
Hwf
;
apply
pure
_intro
;
constructor
;
naive_solver
eauto
using
env_Forall2_wf
,
env_Forall2_fresh
.
-
by
repeat
f_equiv
.
Qed
.
...
...
@@ -287,8 +287,8 @@ Proof. by constructor. Qed.
(** * Adequacy *)
Lemma
tac_adequate
P
:
(
Envs
Enil
Enil
⊢
P
)
→
True
⊢
P
.
Proof
.
intros
<-.
rewrite
/
of_envs
/=
always_
const
!
right_id
.
apply
const
_intro
;
repeat
constructor
.
intros
<-.
rewrite
/
of_envs
/=
always_
pure
!
right_id
.
apply
pure
_intro
;
repeat
constructor
.
Qed
.
(** * Basic rules *)
...
...
@@ -329,7 +329,7 @@ Proof. by rewrite -(False_elim Q). Qed.
(** * Pure *)
Class
ToPure
(
P
:
uPred
M
)
(
φ
:
Prop
)
:
=
to_pure
:
P
⊣
⊢
■
φ
.
Arguments
to_pure
:
clear
implicits
.
Global
Instance
to_pure_
const
φ
:
ToPure
(
■
φ
)
φ
.
Global
Instance
to_pure_
pure
φ
:
ToPure
(
■
φ
)
φ
.
Proof
.
done
.
Qed
.
Global
Instance
to_pure_eq
{
A
:
cofeT
}
(
a
b
:
A
)
:
Timeless
a
→
ToPure
(
a
≡
b
)
(
a
≡
b
).
...
...
@@ -338,18 +338,18 @@ Global Instance to_pure_valid `{CMRADiscrete A} (a : A) : ToPure (✓ a) (✓ a)
Proof
.
intros
;
red
.
by
rewrite
discrete_valid
.
Qed
.
Lemma
tac_pure_intro
Δ
Q
(
φ
:
Prop
)
:
ToPure
Q
φ
→
φ
→
Δ
⊢
Q
.
Proof
.
intros
->.
apply
const
_intro
.
Qed
.
Proof
.
intros
->.
apply
pure
_intro
.
Qed
.
Lemma
tac_pure
Δ
Δ
'
i
p
P
φ
Q
:
envs_lookup_delete
i
Δ
=
Some
(
p
,
P
,
Δ
'
)
→
ToPure
P
φ
→
(
φ
→
Δ
'
⊢
Q
)
→
Δ
⊢
Q
.
Proof
.
intros
??
HQ
.
rewrite
envs_lookup_delete_sound'
//
;
simpl
.
rewrite
(
to_pure
P
)
;
by
apply
const
_elim_sep_l
.
rewrite
(
to_pure
P
)
;
by
apply
pure
_elim_sep_l
.
Qed
.
Lemma
tac_pure_revert
Δ
φ
Q
:
(
Δ
⊢
■
φ
→
Q
)
→
(
φ
→
Δ
⊢
Q
).
Proof
.
intros
H
Δ
?.
by
rewrite
H
Δ
const
_equiv
//
left_id
.
Qed
.
Proof
.
intros
H
Δ
?.
by
rewrite
H
Δ
pure
_equiv
//
left_id
.
Qed
.
(** * Later *)
Class
StripLaterEnv
(
Γ
1
Γ
2
:
env
(
uPred
M
))
:
=
...
...
@@ -373,7 +373,7 @@ Lemma strip_later_env_sound Δ1 Δ2 : StripLaterEnvs Δ1 Δ2 → Δ1 ⊢ ▷ Δ2
Proof
.
intros
[
Hp
Hs
]
;
rewrite
/
of_envs
/=
!
later_sep
-
always_later
.
repeat
apply
sep_mono
;
try
apply
always_mono
.
-
rewrite
-
later_intro
;
apply
const
_mono
;
destruct
1
;
constructor
;
-
rewrite
-
later_intro
;
apply
pure
_mono
;
destruct
1
;
constructor
;
naive_solver
eauto
using
env_Forall2_wf
,
env_Forall2_fresh
.
-
induction
Hp
;
rewrite
/=
?later_and
;
auto
using
and_mono
,
later_intro
.
-
induction
Hs
;
rewrite
/=
?later_sep
;
auto
using
sep_mono
,
later_intro
.
...
...
@@ -437,7 +437,7 @@ Proof.
Qed
.
Lemma
tac_impl_intro_pure
Δ
P
φ
Q
:
ToPure
P
φ
→
(
φ
→
Δ
⊢
Q
)
→
Δ
⊢
P
→
Q
.
Proof
.
intros
.
by
apply
impl_intro_l
;
rewrite
(
to_pure
P
)
;
apply
const
_elim_l
.
<