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
Marianna Rapoport
iris-coq
Commits
fa9b9d1b
Commit
fa9b9d1b
authored
Feb 09, 2016
by
Ralf Jung
Browse files
fix viewshifts.v
parent
99f6e537
Changes
1
Hide whitespace changes
Inline
Side-by-side
program_logic/viewshifts.v
View file @
fa9b9d1b
...
...
@@ -87,7 +87,7 @@ Qed.
Lemma
vs_mask_frame'
E
Ef
P
Q
:
Ef
∩
E
=
∅
→
P
>{
E
}>
Q
⊑
P
>{
E
∪
Ef
}>
Q
.
Proof
.
intros
;
apply
vs_mask_frame
;
solve_elem_of
.
Qed
.
Lemma
vs_open
i
P
:
ownI
i
P
>{{[
i
]},
∅
}>
▷
P
.
Proof
.
intros
;
apply
vs_alt
,
pvs_open
.
Qed
.
Proof
.
intros
;
apply
vs_alt
,
pvs_open
I
.
Qed
.
Lemma
vs_open'
E
i
P
:
i
∉
E
→
ownI
i
P
>{{[
i
]}
∪
E
,
E
}>
▷
P
.
Proof
.
...
...
@@ -96,7 +96,7 @@ Proof.
Qed
.
Lemma
vs_close
i
P
:
(
ownI
i
P
∧
▷
P
)
>{
∅
,{[
i
]}}>
True
.
Proof
.
intros
;
apply
vs_alt
,
pvs_close
.
Qed
.
Proof
.
intros
;
apply
vs_alt
,
pvs_close
I
.
Qed
.
Lemma
vs_close'
E
i
P
:
i
∉
E
→
(
ownI
i
P
∧
▷
P
)
>{
E
,{[
i
]}
∪
E
}>
True
.
Proof
.
...
...
@@ -116,6 +116,6 @@ Proof. by intros; apply vs_alt, pvs_ownG_updateP_empty. Qed.
Lemma
vs_update
E
m
m'
:
m
~~>
m'
→
ownG
m
>{
E
}>
ownG
m'
.
Proof
.
by
intros
;
apply
vs_alt
,
pvs_ownG_update
.
Qed
.
Lemma
vs_alloc
E
P
:
¬
set_finite
E
→
▷
P
>{
E
}>
(
∃
i
,
■
(
i
∈
E
)
∧
ownI
i
P
).
Proof
.
by
intros
;
apply
vs_alt
,
pvs_alloc
.
Qed
.
Proof
.
by
intros
;
apply
vs_alt
,
pvs_alloc
I
.
Qed
.
End
vs
.
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