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
Jonas Kastberg
iris
Commits
f716d0dc
Commit
f716d0dc
authored
Oct 25, 2018
by
Robbert Krebbers
Browse files
A more principled set of axioms for fupd+plainly.
parent
6356ef03
Changes
4
Hide whitespace changes
Inline
Side-by-side
theories/base_logic/lib/fancy_updates.v
View file @
f716d0dc
...
...
@@ -41,17 +41,26 @@ Proof. rewrite /BiBUpdFUpd uPred_fupd_eq. by iIntros (E P) ">? [$ $] !> !>". Qed
Instance
uPred_bi_fupd_plainly
`
{
invG
Σ
}
:
BiFUpdPlainly
(
uPredSI
(
iResUR
Σ
)).
Proof
.
split
.
-
rewrite
uPred_fupd_eq
/
uPred_fupd_def
.
iIntros
(
E
P
Q
)
"HQP HQ [Hw HE]"
.
iAssert
(
◇
■
P
)%
I
as
"#>HP'"
.
{
by
iMod
(
"HQP"
with
"HQ [$]"
)
as
"(_ & _ & HP)"
.
}
-
rewrite
uPred_fupd_eq
/
uPred_fupd_def
.
iIntros
(
E
P
)
"H [Hw HE]"
.
iAssert
(
◇
■
P
)%
I
as
"#>HP"
.
{
by
iMod
(
"H"
with
"[$]"
)
as
"(_ & _ & HP)"
.
}
by
iFrame
.
-
rewrite
uPred_fupd_eq
/
uPred_fupd_def
.
iIntros
(
E
P
Q
)
"[H HQ] [Hw HE]"
.
iAssert
(
◇
■
P
)%
I
as
"#>HP"
.
{
by
iMod
(
"H"
with
"HQ [$]"
)
as
"(_ & _ & HP)"
.
}
by
iFrame
.
-
rewrite
uPred_fupd_eq
/
uPred_fupd_def
.
iIntros
(
E
P
)
"H [Hw HE]"
.
iAssert
(
▷
◇
■
P
)%
I
as
"#HP"
.
{
iNext
.
by
iMod
(
"H"
with
"[$]"
)
as
"(_ & _ & HP)"
.
}
iFrame
.
iIntros
"!> !> !>"
.
by
iMod
"HP"
.
-
rewrite
uPred_fupd_eq
/
uPred_fupd_def
.
iIntros
(
E
A
Φ
)
"HΦ [Hw HE]"
.
iAssert
(
◇
■
∀
x
:
A
,
Φ
x
)%
I
as
"#>HP"
.
{
iIntros
(
x
).
by
iMod
(
"HΦ"
with
"[$Hw $HE]"
)
as
"(_&_&?)"
.
}
by
iFrame
.
-
rewrite
uPred_fupd_eq
/
uPred_fupd_def
.
iIntros
(
p
E1
E2
P
)
"HP [Hw HE]"
.
iAssert
(
▷
?p
◇
■
P
)%
I
with
"[-]"
as
"#HP'"
;
last
by
(
rewrite
plainly_elim
;
iFrame
).
iNext
.
by
iMod
(
"HP"
with
"[$]"
)
as
"(_ & _ & HP)"
.
Qed
.
Lemma
fupd_plain_soundness
`
{
invPreG
Σ
}
E
(
P
:
iProp
Σ
)
`
{!
Plain
P
}
:
(
∀
`
{
Hinv
:
invG
Σ
},
(|={
⊤
,
E
}=>
P
)%
I
)
→
(
▷
P
)%
I
.
(
∀
`
{
Hinv
:
invG
Σ
},
(|={
⊤
,
E
}=>
P
)%
I
)
→
(
▷
P
)%
I
.
Proof
.
iIntros
(
Hfupd
).
iMod
wsat_alloc
as
(
Hinv
)
"[Hw HE]"
.
iPoseProof
(
Hfupd
Hinv
)
as
"H"
.
...
...
@@ -60,26 +69,25 @@ Proof.
Qed
.
Lemma
step_fupdN_soundness
`
{
invPreG
Σ
}
φ
n
:
(
∀
`
{
Hinv
:
invG
Σ
},
(|={
⊤
,
∅
}
▷
=>^
n
|={
⊤
,
∅
}=>
⌜
φ
⌝
:
iProp
Σ
)%
I
)
→
(
∀
`
{
Hinv
:
invG
Σ
},
(|={
⊤
,
∅
}
▷
=>^
n
|={
⊤
,
∅
}=>
⌜
φ
⌝
:
iProp
Σ
)%
I
)
→
φ
.
Proof
.
intros
Hiter
.
apply
(
soundness
(
M
:
=
iResUR
Σ
)
_
(
S
(
S
n
)))
;
simpl
.
apply
(
fupd_plain_soundness
⊤
_
).
intros
Hinv
.
iPoseProof
(
Hiter
Hinv
)
as
"H"
.
apply
(
fupd_plain_soundness
⊤
_
)
=>
Hinv
.
iPoseProof
(
Hiter
Hinv
)
as
"H"
.
clear
Hiter
.
destruct
n
as
[|
n
].
-
rewrite
//=.
iPoseProof
(
fupd_plain_strong
with
"H"
)
as
"H'"
.
do
2
iMod
"H'"
;
iModIntro
;
auto
.
-
iPoseProof
(
step_fupdN_mono
_
_
_
_
(|={
⊤
}=>
◇
⌜φ⌝
)%
I
with
"H"
)
as
"H'"
.
{
iIntros
"H"
.
iMod
(
fupd_plain_strong
with
"H"
)
;
auto
.
}
-
iApply
fupd_plainly_mask_empty
.
iMod
"H"
as
%?
;
auto
.
-
iPoseProof
(
step_fupdN_mono
_
_
_
_
(|={
⊤
}=>
⌜φ⌝
)%
I
with
"H"
)
as
"H'"
.
{
iIntros
"H"
.
by
iApply
fupd_plain_mask_empty
.
}
rewrite
-
step_fupdN_S_fupd
.
iMod
(
step_fupdN_plain
with
"H'"
)
as
"Hφ"
.
iModIntro
.
iNext
.
rewrite
-
later_laterN
laterN_later
.
iNext
.
by
do
2
iMod
"Hφ"
.
iNext
.
by
iMod
"Hφ"
.
Qed
.
Lemma
step_fupdN_soundness'
`
{
invPreG
Σ
}
φ
n
:
(
∀
`
{
Hinv
:
invG
Σ
},
(|={
⊤
,
∅
}
▷
=>^
n
⌜
φ
⌝
:
iProp
Σ
)%
I
)
→
(
∀
`
{
Hinv
:
invG
Σ
},
(|={
⊤
,
∅
}
▷
=>^
n
⌜
φ
⌝
:
iProp
Σ
)%
I
)
→
φ
.
Proof
.
iIntros
(
Hiter
).
eapply
(
step_fupdN_soundness
_
n
).
...
...
theories/bi/monpred.v
View file @
f716d0dc
...
...
@@ -956,11 +956,17 @@ Proof. move => [] /(_ i). rewrite /Plain monPred_at_plainly bi.forall_elim //. Q
Global
Instance
monPred_bi_fupd_plainly
`
{
BiFUpdPlainly
PROP
}
:
BiFUpdPlainly
monPredSI
.
Proof
.
split
;
rewrite
monPred_fupd_eq
;
unseal
.
-
intros
E
P
Q
.
split
=>/=
i
.
do
3
f_equiv
.
rewrite
monPred_at_plainly
(
bi
.
forall_elim
_
)
fupd_plainly_weak
//=.
-
intros
p
E1
E2
P
;
split
=>/=
i
;
specialize
(
later_fupd_plainly
p
)
=>
HFP
.
destruct
p
;
simpl
;
[
unseal
|
]
;
rewrite
monPred_at_plainly
(
bi
.
forall_elim
_
)
;
apply
HFP
.
split
;
rewrite
!
monPred_fupd_eq
;
try
unseal
.
-
intros
E
P
.
split
=>/=
i
.
by
rewrite
monPred_at_plainly
(
bi
.
forall_elim
i
)
fupd_plainly_mask_empty
.
-
intros
E
P
R
.
split
=>/=
i
.
rewrite
(
bi
.
forall_elim
i
)
bi
.
pure_True
//
bi
.
True_impl
.
by
rewrite
monPred_at_plainly
(
bi
.
forall_elim
i
)
fupd_plainly_keep_l
.
-
intros
E
P
.
split
=>/=
i
.
by
rewrite
monPred_at_plainly
(
bi
.
forall_elim
i
)
fupd_plainly_later
.
-
intros
E
A
Φ
.
split
=>/=
i
.
rewrite
-
fupd_plainly_forall_2
.
apply
bi
.
forall_mono
=>
x
.
by
rewrite
monPred_at_plainly
(
bi
.
forall_elim
i
).
Qed
.
Global
Instance
plainly_objective
`
{
BiPlainly
PROP
}
P
:
Objective
(
■
P
).
...
...
theories/bi/updates.v
View file @
f716d0dc
...
...
@@ -54,7 +54,7 @@ Record BiFUpdMixin (PROP : sbi) `(FUpd PROP) := {
bi_fupd_mixin_fupd_trans
E1
E2
E3
(
P
:
PROP
)
:
(|={
E1
,
E2
}=>
|={
E2
,
E3
}=>
P
)
⊢
|={
E1
,
E3
}=>
P
;
bi_fupd_mixin_fupd_mask_frame_r'
E1
E2
Ef
(
P
:
PROP
)
:
E1
##
Ef
→
(|={
E1
,
E2
}=>
⌜
E2
##
Ef
⌝
→
P
)
={
E1
∪
Ef
,
E2
∪
Ef
}=
∗
P
;
bi_fupd_mixin_fupd_frame_r
E1
E2
(
P
Q
:
PROP
)
:
(|={
E1
,
E2
}=>
P
)
∗
Q
={
E1
,
E2
}=
∗
P
∗
Q
;
bi_fupd_mixin_fupd_frame_r
E1
E2
(
P
R
:
PROP
)
:
(|={
E1
,
E2
}=>
P
)
∗
R
={
E1
,
E2
}=
∗
P
∗
R
;
}.
Class
BiBUpd
(
PROP
:
bi
)
:
=
{
...
...
@@ -80,10 +80,14 @@ Class BiBUpdPlainly (PROP : sbi) `{!BiBUpd PROP, !BiPlainly PROP} :=
Hint
Mode
BiBUpdPlainly
!
-
-
:
typeclass_instances
.
Class
BiFUpdPlainly
(
PROP
:
sbi
)
`
{!
BiFUpd
PROP
,
!
BiPlainly
PROP
}
:
=
{
fupd_plainly_weak
E
(
P
Q
:
PROP
)
:
(
Q
={
E
}=
∗
■
P
)
-
∗
Q
={
E
}=
∗
Q
∗
P
;
later_fupd_plainly
p
E1
E2
(
P
:
PROP
)
:
(
▷
?p
|={
E1
,
E2
}=>
■
P
)
={
E1
}=
∗
▷
?p
◇
P
;
fupd_plainly_mask_empty
E
(
P
:
PROP
)
:
(|={
E
,
∅
}=>
■
P
)
⊢
|={
E
}=>
P
;
fupd_plainly_keep_l
E
(
P
R
:
PROP
)
:
(
R
={
E
}=
∗
■
P
)
∗
R
⊢
|={
E
}=>
P
∗
R
;
fupd_plainly_later
E
(
P
:
PROP
)
:
(
▷
|={
E
}=>
■
P
)
⊢
|={
E
}=>
▷
◇
P
;
fupd_plainly_forall_2
E
{
A
}
(
Φ
:
A
→
PROP
)
:
(
∀
x
,
|={
E
}=>
■
Φ
x
)
⊢
|={
E
}=>
∀
x
,
Φ
x
}.
Hint
Mode
BiBUpdFUpd
!
-
-
:
typeclass_instances
.
...
...
@@ -120,7 +124,7 @@ Section fupd_laws.
Lemma
fupd_mask_frame_r'
E1
E2
Ef
(
P
:
PROP
)
:
E1
##
Ef
→
(|={
E1
,
E2
}=>
⌜
E2
##
Ef
⌝
→
P
)
={
E1
∪
Ef
,
E2
∪
Ef
}=
∗
P
.
Proof
.
eapply
bi_fupd_mixin_fupd_mask_frame_r'
,
bi_fupd_mixin
.
Qed
.
Lemma
fupd_frame_r
E1
E2
(
P
Q
:
PROP
)
:
(|={
E1
,
E2
}=>
P
)
∗
Q
={
E1
,
E2
}=
∗
P
∗
Q
.
Lemma
fupd_frame_r
E1
E2
(
P
R
:
PROP
)
:
(|={
E1
,
E2
}=>
P
)
∗
R
={
E1
,
E2
}=
∗
P
∗
R
.
Proof
.
eapply
bi_fupd_mixin_fupd_frame_r
,
bi_fupd_mixin
.
Qed
.
End
fupd_laws
.
...
...
@@ -196,8 +200,8 @@ Section fupd_derived.
Lemma
fupd_except_0
E1
E2
P
:
(|={
E1
,
E2
}=>
◇
P
)
={
E1
,
E2
}=
∗
P
.
Proof
.
by
rewrite
{
1
}(
fupd_intro
E2
P
)
except_0_fupd
fupd_trans
.
Qed
.
Lemma
fupd_frame_l
E1
E2
P
Q
:
(
P
∗
|={
E1
,
E2
}=>
Q
)
={
E1
,
E2
}=
∗
P
∗
Q
.
Proof
.
rewrite
!(
comm
_
P
)
;
apply
fupd_frame_r
.
Qed
.
Lemma
fupd_frame_l
E1
E2
R
Q
:
(
R
∗
|={
E1
,
E2
}=>
Q
)
={
E1
,
E2
}=
∗
R
∗
Q
.
Proof
.
rewrite
!(
comm
_
R
)
;
apply
fupd_frame_r
.
Qed
.
Lemma
fupd_wand_l
E1
E2
P
Q
:
(
P
-
∗
Q
)
∗
(|={
E1
,
E2
}=>
P
)
={
E1
,
E2
}=
∗
Q
.
Proof
.
by
rewrite
fupd_frame_l
wand_elim_l
.
Qed
.
Lemma
fupd_wand_r
E1
E2
P
Q
:
(|={
E1
,
E2
}=>
P
)
∗
(
P
-
∗
Q
)
={
E1
,
E2
}=
∗
Q
.
...
...
@@ -239,8 +243,7 @@ Section fupd_derived.
Proof
.
intros
?.
rewrite
(
fupd_mask_frame_r
_
_
(
E
∖
E1
))
;
last
set_solver
.
rewrite
fupd_trans
.
assert
(
E
=
E1
∪
E
∖
E1
)
as
<-
;
last
done
.
apply
union_difference_L
.
done
.
by
replace
(
E1
∪
E
∖
E1
)
with
E
by
(
by
apply
union_difference_L
).
Qed
.
(* A variant of [fupd_mask_frame] that works well for accessors: Tailored to
elliminate updates of the form [|={E1,E1∖E2}=> Q] and provides a way to
...
...
@@ -335,8 +338,7 @@ Section fupd_derived.
by
apply
later_mono
,
fupd_mono
.
Qed
.
Lemma
step_fupd_fupd
E
P
:
(|={
E
,
∅
}
▷
=>
P
)
⊣
⊢
(|={
E
,
∅
}
▷
=>
|={
E
}=>
P
).
Lemma
step_fupd_fupd
E
E'
P
:
(|={
E
,
E'
}
▷
=>
P
)
⊣
⊢
(|={
E
,
E'
}
▷
=>
|={
E
}=>
P
).
Proof
.
apply
(
anti_symm
(
⊢
)).
-
by
rewrite
-
fupd_intro
.
...
...
@@ -366,55 +368,89 @@ Section fupd_derived.
Section
fupd_plainly_derived
.
Context
`
{
BiPlainly
PROP
,
!
BiFUpdPlainly
PROP
}.
Lemma
fupd_plain_weak
E
P
Q
`
{!
Plain
P
}
:
(
Q
={
E
}=
∗
P
)
-
∗
Q
={
E
}=
∗
Q
∗
P
.
Proof
.
by
rewrite
{
1
}(
plain
P
)
fupd_plainly_weak
.
Qed
.
Lemma
fupd_plainly_mask
E
E'
P
:
(|={
E
,
E'
}=>
■
P
)
⊢
|={
E
}=>
P
.
Proof
.
rewrite
-(
fupd_plainly_mask_empty
).
apply
fupd_elim
,
(
fupd_mask_weaken
_
_
_
).
set_solver
.
Qed
.
Lemma
fupd_plainly_elim
E
P
:
■
P
={
E
}=
∗
P
.
Proof
.
by
rewrite
(
fupd_intro
E
(
■
P
)%
I
)
fupd_plainly_mask
.
Qed
.
Lemma
later_fupd_plain
p
E1
E2
P
`
{!
Plain
P
}
:
(
▷
?p
|={
E1
,
E2
}=>
P
)
={
E1
}=
∗
▷
?p
◇
P
.
Proof
.
by
rewrite
{
1
}(
plain
P
)
later_fupd_plainly
.
Qed
.
Lemma
fupd_plainly_keep_r
E
P
R
:
R
∗
(
R
={
E
}=
∗
■
P
)
⊢
|={
E
}=>
R
∗
P
.
Proof
.
by
rewrite
!(
comm
_
R
)
fupd_plainly_keep_l
.
Qed
.
Lemma
fupd_plain_strong
E1
E2
P
`
{!
Plain
P
}
:
(|={
E1
,
E2
}=>
P
)
={
E1
}=
∗
◇
P
.
Proof
.
by
apply
(
later_fupd_plain
false
).
Qed
.
Lemma
fupd_plain_mask_empty
E
P
`
{!
Plain
P
}
:
(|={
E
,
∅
}=>
P
)
⊢
|={
E
}=>
P
.
Proof
.
by
rewrite
{
1
}(
plain
P
)
fupd_plainly_mask_empty
.
Qed
.
Lemma
fupd_plain_mask
E
E'
P
`
{!
Plain
P
}
:
(|={
E
,
E'
}=>
P
)
⊢
|={
E
}=>
P
.
Proof
.
by
rewrite
{
1
}(
plain
P
)
fupd_plainly_mask
.
Qed
.
Lemma
fupd_plain'
E1
E2
E2'
P
Q
`
{!
Plain
P
}
:
E1
⊆
E2
→
(
Q
={
E1
,
E2'
}=
∗
P
)
-
∗
(|={
E1
,
E2
}=>
Q
)
={
E1
}=
∗
(|={
E1
,
E2
}=>
Q
)
∗
P
.
Lemma
fupd_plain_keep_l
E
P
R
`
{!
Plain
P
}
:
(
R
={
E
}=
∗
P
)
∗
R
⊢
|={
E
}=>
P
∗
R
.
Proof
.
by
rewrite
{
1
}(
plain
P
)
fupd_plainly_keep_l
.
Qed
.
Lemma
fupd_plain_keep_r
E
P
R
`
{!
Plain
P
}
:
R
∗
(
R
={
E
}=
∗
P
)
⊢
|={
E
}=>
R
∗
P
.
Proof
.
by
rewrite
{
1
}(
plain
P
)
fupd_plainly_keep_r
.
Qed
.
Lemma
fupd_plain_later
E
P
`
{!
Plain
P
}
:
(
▷
|={
E
}=>
P
)
⊢
|={
E
}=>
▷
◇
P
.
Proof
.
by
rewrite
{
1
}(
plain
P
)
fupd_plainly_later
.
Qed
.
Lemma
fupd_plain_forall_2
E
{
A
}
(
Φ
:
A
→
PROP
)
`
{!
∀
x
,
Plain
(
Φ
x
)}
:
(
∀
x
,
|={
E
}=>
Φ
x
)
⊢
|={
E
}=>
∀
x
,
Φ
x
.
Proof
.
intros
(
E3
&->&
HE
)%
subseteq_disjoint_union_L
.
apply
wand_intro_l
.
rewrite
fupd_frame_r
.
rewrite
fupd_plain_strong
fupd_except_0
fupd_plain_weak
wand_elim_r
.
rewrite
(
fupd_mask_mono
E1
(
E1
∪
E3
))
;
last
by
set_solver
+.
rewrite
fupd_trans
-(
fupd_trans
E1
(
E1
∪
E3
)
E1
).
apply
fupd_mono
.
rewrite
-
fupd_frame_r
.
apply
sep_mono
;
auto
.
apply
fupd_intro_mask
;
set_solver
+.
rewrite
-
fupd_plainly_forall_2
.
apply
forall_mono
=>
x
.
by
rewrite
{
1
}(
plain
(
Φ
_
)).
Qed
.
Lemma
fupd_plain
E1
E2
P
Q
`
{
!
Plain
P
}
:
E1
⊆
E2
→
(
Q
-
∗
P
)
-
∗
(|={
E1
,
E2
}=>
Q
)
={
E1
}=
∗
(|={
E1
,
E2
}=>
Q
)
∗
P
.
Lemma
fupd_plain
ly_laterN
E
n
P
`
{
HP
:
!
Plain
P
}
:
(
▷
^
n
|={
E
}=>
P
)
⊢
|={
E
}=>
▷
^
n
◇
P
.
Proof
.
intros
HE
.
rewrite
-(
fupd_plain'
_
_
E1
)
//.
apply
wand_intro_l
.
by
rewrite
wand_elim_r
-
fupd_intro
.
revert
P
HP
.
induction
n
as
[|
n
IH
]=>
P
?
/=.
-
by
rewrite
-
except_0_intro
.
-
rewrite
-!
later_laterN
!
laterN_later
.
rewrite
fupd_plain_later
.
by
rewrite
IH
except_0_later
.
Qed
.
Lemma
step_fupd_plain
E
P
`
{!
Plain
P
}
:
(|={
E
,
∅
}
▷
=>
P
)
={
E
}=
∗
▷
◇
P
.
Lemma
fupd_plain_forall
E1
E2
{
A
}
(
Φ
:
A
→
PROP
)
`
{!
∀
x
,
Plain
(
Φ
x
)}
:
E2
⊆
E1
→
(|={
E1
,
E2
}=>
∀
x
,
Φ
x
)
⊣
⊢
(
∀
x
,
|={
E1
,
E2
}=>
Φ
x
).
Proof
.
specialize
(
later_fupd_plain
true
∅
E
P
)
=>
//=
->.
rewrite
fupd_trans
fupd_plain_strong
.
apply
fupd_mono
,
except_0_later
.
intros
.
apply
(
anti_symm
_
).
{
apply
forall_intro
=>
x
.
by
rewrite
(
forall_elim
x
).
}
trans
(
∀
x
,
|={
E1
}=>
Φ
x
)%
I
.
{
apply
forall_mono
=>
x
.
by
rewrite
fupd_plain_mask
.
}
rewrite
fupd_plain_forall_2
.
apply
fupd_elim
.
rewrite
{
1
}(
plain
(
∀
x
,
Φ
x
))
(
fupd_mask_weaken
E1
E2
(
■
_
)%
I
)
//.
apply
fupd_elim
.
by
rewrite
fupd_plainly_elim
.
Qed
.
Lemma
fupd_plain_forall'
E
{
A
}
(
Φ
:
A
→
PROP
)
`
{!
∀
x
,
Plain
(
Φ
x
)}
:
(|={
E
}=>
∀
x
,
Φ
x
)
⊣
⊢
(
∀
x
,
|={
E
}=>
Φ
x
).
Proof
.
by
apply
fupd_plain_forall
.
Qed
.
Lemma
step_fupdN_plain
E
n
P
`
{!
Plain
P
}
:
(|={
E
,
∅
}
▷
=>^
n
P
)
={
E
}=
∗
▷
^
n
◇
P
.
Lemma
step_fupd_plain
E
E'
P
`
{!
Plain
P
}
:
(|={
E
,
E'
}
▷
=>
P
)
={
E
}=
∗
▷
◇
P
.
Proof
.
rewrite
-(
fupd_plain_mask
_
E'
(
▷
◇
P
)%
I
).
apply
fupd_elim
.
by
rewrite
fupd_plain_mask
-
fupd_plain_later
.
Qed
.
Lemma
step_fupdN_plain
E
E'
n
P
`
{!
Plain
P
}
:
(|={
E
,
E'
}
▷
=>^
n
P
)
={
E
}=
∗
▷
^
n
◇
P
.
Proof
.
induction
n
as
[|
n
IH
].
-
rewrite
-
fupd_intro
.
apply
except_0_intro
.
-
rewrite
Nat_iter_S
step_fupd_fupd
IH
?
fupd_trans
step_fupd_plain
.
apply
fupd_mono
.
destruct
n
;
simpl
.
-
by
rewrite
-
fupd_intro
-
except_0_intro
.
-
rewrite
Nat_iter_S
step_fupd_fupd
IH
!
fupd_trans
step_fupd_plain
.
apply
fupd_mono
.
destruct
n
as
[|
n
]
;
simpl
.
*
by
rewrite
except_0_idemp
.
*
by
rewrite
except_0_later
.
Qed
.
End
fupd_plainly_derived
.
Lemma
step_fupd_plain_forall
E1
E2
{
A
}
(
Φ
:
A
→
PROP
)
`
{!
∀
x
,
Plain
(
Φ
x
)}
:
E2
⊆
E1
→
(|={
E1
,
E2
}
▷
=>
∀
x
,
Φ
x
)
⊣
⊢
(
∀
x
,
|={
E1
,
E2
}
▷
=>
Φ
x
).
Proof
.
intros
.
apply
(
anti_symm
_
).
{
apply
forall_intro
=>
x
.
by
rewrite
(
forall_elim
x
).
}
trans
(
∀
x
,
|={
E1
}=>
▷
◇
Φ
x
)%
I
.
{
apply
forall_mono
=>
x
.
by
rewrite
step_fupd_plain
.
}
rewrite
-
fupd_plain_forall'
.
apply
fupd_elim
.
rewrite
-(
fupd_except_0
E2
E1
)
-
step_fupd_intro
//.
by
rewrite
-
later_forall
-
except_0_forall
.
Qed
.
End
fupd_plainly_derived
.
End
fupd_derived
.
theories/program_logic/adequacy.v
View file @
f716d0dc
...
...
@@ -44,7 +44,7 @@ Notation wptp s t := ([∗ list] ef ∈ t, WP ef @ s; ⊤ {{ _, True }})%I.
Lemma
wp_step
s
E
e1
σ
1
κ
κ
s
e2
σ
2
efs
Φ
:
prim_step
e1
σ
1
κ
e2
σ
2
efs
→
state_interp
σ
1
(
κ
++
κ
s
)
∗
WP
e1
@
s
;
E
{{
Φ
}}
={
E
,
∅
}
▷
=
∗
(
state_interp
σ
2
κ
s
∗
WP
e2
@
s
;
E
{{
Φ
}}
∗
wptp
s
efs
).
={
E
,
∅
}
▷
=
∗
(
state_interp
σ
2
κ
s
∗
WP
e2
@
s
;
E
{{
Φ
}}
∗
wptp
s
efs
).
Proof
.
rewrite
{
1
}
wp_unfold
/
wp_pre
.
iIntros
(?)
"[Hσ H]"
.
rewrite
(
val_stuck
e1
σ
1
κ
e2
σ
2
efs
)
//.
...
...
@@ -57,7 +57,7 @@ Lemma wptp_step s e1 t1 t2 κ κs σ1 σ2 Φ :
step
(
e1
::
t1
,
σ
1
)
κ
(
t2
,
σ
2
)
→
state_interp
σ
1
(
κ
++
κ
s
)
∗
WP
e1
@
s
;
⊤
{{
Φ
}}
∗
wptp
s
t1
==
∗
∃
e2
t2'
,
⌜
t2
=
e2
::
t2'
⌝
∗
|={
⊤
,
∅
}
▷
=>
(
state_interp
σ
2
κ
s
∗
WP
e2
@
s
;
⊤
{{
Φ
}}
∗
wptp
s
t2'
).
⌜
t2
=
e2
::
t2'
⌝
∗
|={
⊤
,
∅
}
▷
=>
(
state_interp
σ
2
κ
s
∗
WP
e2
@
s
;
⊤
{{
Φ
}}
∗
wptp
s
t2'
).
Proof
.
iIntros
(
Hstep
)
"(HW & He & Ht)"
.
destruct
Hstep
as
[
e1'
σ
1
'
e2'
σ
2
'
efs
[|?
t1'
]
t2'
??
Hstep
]
;
simplify_eq
/=.
...
...
@@ -71,7 +71,7 @@ Qed.
Lemma
wptp_steps
s
n
e1
t1
κ
s
κ
s'
t2
σ
1
σ
2
Φ
:
nsteps
n
(
e1
::
t1
,
σ
1
)
κ
s
(
t2
,
σ
2
)
→
state_interp
σ
1
(
κ
s
++
κ
s'
)
∗
WP
e1
@
s
;
⊤
{{
Φ
}}
∗
wptp
s
t1
⊢
|={
⊤
,
∅
}
▷
=>^
n
(
∃
e2
t2'
,
|={
⊤
,
∅
}
▷
=>^
n
(
∃
e2
t2'
,
⌜
t2
=
e2
::
t2'
⌝
∗
state_interp
σ
2
κ
s'
∗
WP
e2
@
s
;
⊤
{{
Φ
}}
∗
wptp
s
t2'
).
Proof
.
revert
e1
t1
κ
s
κ
s'
t2
σ
1
σ
2
;
simpl
;
induction
n
as
[|
n
IH
]=>
e1
t1
κ
s
κ
s'
t2
σ
1
σ
2
/=.
...
...
@@ -88,15 +88,15 @@ Lemma wptp_result s n e1 t1 κs κs' v2 t2 σ1 σ2 φ :
state_interp
σ
1
(
κ
s
++
κ
s'
)
∗
WP
e1
@
s
;
⊤
{{
v
,
∀
σ
,
state_interp
σ
κ
s'
={
⊤
,
∅
}=
∗
⌜φ
v
σ⌝
}}
∗
wptp
s
t1
⊢
|={
⊤
,
∅
}
▷
=>^(
S
n
)
⌜φ
v2
σ
2
⌝
.
|={
⊤
,
∅
}
▷
=>^(
S
n
)
⌜φ
v2
σ
2
⌝
.
Proof
.
intros
.
rewrite
Nat_iter_S_r
wptp_steps
//.
apply
step_fupdN_mono
.
iDestruct
1
as
(
e2
t2'
?)
"(Hσ & H & _)"
;
simplify_eq
.
iMod
(
wp_value_inv'
with
"H"
)
as
"H"
.
iMod
(
later_
fupd_plain
false
⊤
∅
(
⌜φ
v2
σ
2
⌝
)
%
I
with
"[H Hσ]"
)
as
">#%"
.
{
rewrite
//=.
by
iMod
(
"H"
with
"Hσ"
)
as
"$"
.
}
iApply
(
step_fupd_
mask_mono
∅
_
_
∅
)
;
aut
o
.
iMod
(
fupd_plain
_mask_empty
_
⌜φ
v2
σ
2
⌝
%
I
with
"[H Hσ]"
)
as
%?
.
{
by
iMod
(
"H"
with
"Hσ"
)
as
"$"
.
}
by
iApply
step_fupd_
intr
o
.
Qed
.
Lemma
wp_safe
E
e
σ
κ
s
Φ
:
...
...
@@ -105,8 +105,8 @@ Proof.
rewrite
wp_unfold
/
wp_pre
.
iIntros
"Hσ H"
.
destruct
(
to_val
e
)
as
[
v
|]
eqn
:
?.
{
iApply
(
step_fupd_mask_mono
∅
_
_
∅
)
;
eauto
.
set_solver
.
}
iMod
(
later_
fupd_plain
false
E
∅
(
⌜
reducible
e
σ⌝
)
%
I
with
"[H Hσ]"
)
as
">#%"
.
{
rewrite
//=.
by
iMod
(
"H"
$!
σ
[]
κ
s
with
"Hσ"
)
as
"($&H)"
.
}
iMod
(
fupd_plain
_mask_empty
_
⌜
reducible
e
σ⌝
%
I
with
"[H Hσ]"
)
as
%?
.
{
by
iMod
(
"H"
$!
σ
[]
κ
s
with
"Hσ"
)
as
"($&H)"
.
}
iApply
step_fupd_intro
;
first
by
set_solver
+.
iIntros
"!> !%"
.
by
right
.
Qed
.
...
...
@@ -114,7 +114,7 @@ Qed.
Lemma
wptp_safe
n
e1
κ
s
κ
s'
e2
t1
t2
σ
1
σ
2
Φ
:
nsteps
n
(
e1
::
t1
,
σ
1
)
κ
s
(
t2
,
σ
2
)
→
e2
∈
t2
→
state_interp
σ
1
(
κ
s
++
κ
s'
)
∗
WP
e1
{{
Φ
}}
∗
wptp
NotStuck
t1
⊢
|={
⊤
,
∅
}
▷
=>^(
S
n
)
⌜
is_Some
(
to_val
e2
)
∨
reducible
e2
σ
2
⌝
.
⊢
|={
⊤
,
∅
}
▷
=>^(
S
n
)
⌜
is_Some
(
to_val
e2
)
∨
reducible
e2
σ
2
⌝
.
Proof
.
intros
?
He2
.
rewrite
Nat_iter_S_r
wptp_steps
//.
apply
step_fupdN_mono
.
...
...
@@ -126,14 +126,14 @@ Qed.
Lemma
wptp_invariance
s
n
e1
κ
s
κ
s'
e2
t1
t2
σ
1
σ
2
φ
Φ
:
nsteps
n
(
e1
::
t1
,
σ
1
)
κ
s
(
t2
,
σ
2
)
→
(
state_interp
σ
2
κ
s'
={
⊤
,
∅
}=
∗
⌜φ⌝
)
∗
state_interp
σ
1
(
κ
s
++
κ
s'
)
∗
WP
e1
@
s
;
⊤
{{
Φ
}}
∗
wptp
s
t1
⊢
|={
⊤
,
∅
}
▷
=>^(
S
n
)
|={
⊤
,
∅
}=>
⌜φ⌝
.
(
state_interp
σ
2
κ
s'
={
⊤
,
∅
}=
∗
⌜φ⌝
)
∗
state_interp
σ
1
(
κ
s
++
κ
s'
)
∗
WP
e1
@
s
;
⊤
{{
Φ
}}
∗
wptp
s
t1
⊢
|={
⊤
,
∅
}
▷
=>^(
S
n
)
|={
⊤
,
∅
}=>
⌜φ⌝
.
Proof
.
intros
?.
rewrite
Nat_iter_S_r
wptp_steps
//
step_fupdN_frame_l
.
apply
step_fupdN_mono
.
iIntros
"[Hback H]"
;
iDestruct
"H"
as
(
e2'
t2'
->)
"[Hσ _]"
.
iSpecialize
(
"Hback"
with
"Hσ"
).
iApply
(
step_fupd_mask_mono
∅
_
_
∅
)
;
auto
.
iSpecialize
(
"Hback"
with
"Hσ"
).
by
iApply
step_fupd_intro
.
Qed
.
End
adequacy
.
...
...
@@ -146,15 +146,13 @@ Theorem wp_strong_adequacy Σ Λ `{invPreG Σ} s e σ φ :
Proof
.
intros
Hwp
;
split
.
-
intros
t2
σ
2
v2
[
n
[
κ
s
?]]%
erased_steps_nsteps
.
eapply
(
step_fupdN_soundness'
_
(
S
(
S
n
))).
iIntros
(
Hinv
).
eapply
(
step_fupdN_soundness'
_
(
S
(
S
n
)))=>
Hinv
.
rewrite
Nat_iter_S
.
iMod
Hwp
as
(
Istate
)
"[HI Hwp]"
.
iApply
(
step_fupd_mask_mono
∅
_
_
∅
)
;
auto
.
iModIntro
.
iNext
;
iModIntro
.
iApply
(@
wptp_result
_
_
(
IrisG
_
_
_
Hinv
Istate
)
_
_
_
_
_
[])
;
eauto
with
iFrame
.
-
destruct
s
;
last
done
.
intros
t2
σ
2 e2
_
[
n
[
κ
s
?]]%
erased_steps_nsteps
?.
eapply
(
step_fupdN_soundness'
_
(
S
(
S
n
))).
iIntros
(
Hinv
).
eapply
(
step_fupdN_soundness'
_
(
S
(
S
n
)))=>
Hinv
.
rewrite
Nat_iter_S
.
iMod
Hwp
as
(
Istate
)
"[HI Hwp]"
.
iApply
(
step_fupd_mask_mono
∅
_
_
∅
)
;
auto
.
...
...
@@ -184,11 +182,10 @@ Theorem wp_invariance Σ Λ `{invPreG Σ} s e σ1 t2 σ2 φ :
φ
.
Proof
.
intros
Hwp
[
n
[
κ
s
?]]%
erased_steps_nsteps
.
eapply
(
step_fupdN_soundness
_
(
S
(
S
n
))).
iIntros
(
Hinv
).
eapply
(
step_fupdN_soundness
_
(
S
(
S
n
)))=>
Hinv
.
rewrite
Nat_iter_S
.
iMod
(
Hwp
Hinv
κ
s
[])
as
(
Istate
)
"(HIstate & Hwp & Hclose)"
.
iApply
(
step_fupd_
mask_mono
∅
_
_
∅
)
;
auto
.
iApply
step_fupd_
intro
;
first
done
.
iApply
(@
wptp_invariance
_
_
(
IrisG
_
_
_
Hinv
Istate
))
;
eauto
with
iFrame
.
Qed
.
...
...
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