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
Iris
Iris
Commits
961290d2
Commit
961290d2
authored
Feb 14, 2016
by
Ralf Jung
Browse files
avoid tricky -{left,right}_id rewrites
parent
d800f42e
Changes
3
Hide whitespace changes
Inline
Side-by-side
algebra/upred.v
View file @
961290d2
...
...
@@ -615,6 +615,10 @@ Lemma sep_intro_True_l P Q R : True ⊑ P → R ⊑ Q → R ⊑ (P ★ Q).
Proof
.
by
intros
;
rewrite
-(
left_id
True
%
I
uPred_sep
R
)
;
apply
sep_mono
.
Qed
.
Lemma
sep_intro_True_r
P
Q
R
:
R
⊑
P
→
True
⊑
Q
→
R
⊑
(
P
★
Q
).
Proof
.
by
intros
;
rewrite
-(
right_id
True
%
I
uPred_sep
R
)
;
apply
sep_mono
.
Qed
.
Lemma
sep_elim_True_l
P
Q
R
:
True
⊑
P
→
(
P
★
R
)
⊑
Q
→
R
⊑
Q
.
Proof
.
by
intros
HP
;
rewrite
-
HP
left_id
.
Qed
.
Lemma
sep_elim_True_r
P
Q
R
:
True
⊑
P
→
(
R
★
P
)
⊑
Q
→
R
⊑
Q
.
Proof
.
by
intros
HP
;
rewrite
-
HP
right_id
.
Qed
.
Lemma
wand_intro_l
P
Q
R
:
(
Q
★
P
)
⊑
R
→
P
⊑
(
Q
-
★
R
).
Proof
.
rewrite
comm
;
apply
wand_intro_r
.
Qed
.
Lemma
wand_elim_r
P
Q
:
(
P
★
(
P
-
★
Q
))
⊑
Q
.
...
...
heap_lang/heap.v
View file @
961290d2
...
...
@@ -119,8 +119,10 @@ Section heap.
P
⊑
(
▷
(
∀
l
,
heap_mapsto
HeapI
γ
l
v
-
★
Q
(
LocV
l
)))
→
P
⊑
wp
E
(
Alloc
e
)
Q
.
Proof
.
intros
HN
?
Hctx
HP
.
rewrite
-(
right_id
True
%
I
(
★
)%
I
(
P
))
(
auth_empty
γ
)
pvs_frame_l
.
apply
wp_strip_pvs
.
eapply
wp_alloc_heap
with
(
σ
:
=
∅
)
;
try
eassumption
.
intros
HN
?
Hctx
HP
.
eapply
sep_elim_True_r
.
{
eapply
(
auth_empty
γ
).
}
rewrite
pvs_frame_l
.
apply
wp_strip_pvs
.
eapply
wp_alloc_heap
with
(
σ
:
=
∅
)
;
try
eassumption
.
{
eauto
with
I
.
}
rewrite
HP
comm
.
apply
sep_mono
.
-
rewrite
/
heap_own
.
f_equiv
.
apply
:
map_eq
=>
l
.
by
rewrite
lookup_fmap
!
lookup_empty
.
...
...
@@ -166,7 +168,8 @@ Section heap.
P
⊑
wp
E
(
Store
(
Loc
l
)
e
)
Q
.
Proof
.
rewrite
/
heap_ctx
/
heap_own
.
intros
Hl
Hval
HN
Hctx
HP
.
eapply
(
auth_fsa
(
heap_inv
HeapI
)
(
wp_fsa
_
)
(
λ
_:
(),
alter
(
λ
_
,
Excl
v
)
l
))
;
simpl
;
eauto
.
eapply
(
auth_fsa
(
heap_inv
HeapI
)
(
wp_fsa
_
)
(
λ
_:
(),
alter
(
λ
_
,
Excl
v
)
l
))
;
simpl
;
eauto
.
rewrite
HP
=>{
HP
Hctx
HN
}.
apply
sep_mono
;
first
done
.
apply
forall_intro
=>
hf
.
apply
wand_intro_l
.
rewrite
/
heap_inv
.
rewrite
-
assoc
.
apply
const_elim_sep_l
=>
Hv
/=.
...
...
@@ -189,12 +192,13 @@ Section heap.
+
by
rewrite
lookup_alter
/
to_heap
!
lookup_fmap
lookup_insert
Hl
/=.
+
rewrite
lookup_alter_ne
//
!
lookup_fmap
lookup_insert_ne
//.
}
rewrite
!
EQ
.
apply
sep_mono
;
last
done
.
f_equiv
.
apply
:
map_eq
=>
l'
.
move
:
(
Hv
0
%
nat
l'
).
destruct
(
decide
(
l
=
l'
))
;
simplify_map_equality
.
f_equiv
.
apply
:
map_eq
=>
l'
.
move
:
(
Hv
0
%
nat
l'
).
destruct
(
decide
(
l
=
l'
))
;
simplify_map_equality
.
-
rewrite
/
from_heap
/
to_heap
lookup_insert
lookup_omap
!
lookup_op
.
rewrite
!
lookup_fmap
lookup_insert
Hl
.
case
(
hf
!!
l'
)=>[[?||]|]
;
auto
;
contradiction
.
-
rewrite
/
from_heap
/
to_heap
lookup_insert_ne
//
!
lookup_omap
!
lookup_op
!
lookup_fmap
.
rewrite
lookup_insert_ne
//.
-
rewrite
/
from_heap
/
to_heap
lookup_insert_ne
//
!
lookup_omap
.
rewrite
!
lookup_op
!
lookup_fmap
lookup_insert_ne
//.
Qed
.
Lemma
wp_store
N
E
γ
l
v'
e
v
P
Q
:
...
...
@@ -204,7 +208,8 @@ Section heap.
P
⊑
(
heap_mapsto
HeapI
γ
l
v'
★
▷
(
heap_mapsto
HeapI
γ
l
v
-
★
Q
(
LitV
LitUnit
)))
→
P
⊑
wp
E
(
Store
(
Loc
l
)
e
)
Q
.
Proof
.
rewrite
/
heap_mapsto
=>
Hval
HN
Hctx
HP
.
eapply
wp_store_heap
;
try
eassumption
;
last
first
.
rewrite
/
heap_mapsto
=>
Hval
HN
Hctx
HP
.
eapply
wp_store_heap
;
try
eassumption
;
last
first
.
-
rewrite
HP
.
apply
sep_mono
;
first
done
.
by
rewrite
insert_singleton
.
-
by
rewrite
lookup_insert
.
Qed
.
...
...
program_logic/auth.v
View file @
961290d2
...
...
@@ -32,8 +32,8 @@ Section auth.
Lemma
auth_alloc
N
a
:
✓
a
→
φ
a
⊑
pvs
N
N
(
∃
γ
,
auth_ctx
AuthI
γ
N
φ
∧
auth_own
AuthI
γ
a
).
Proof
.
intros
Ha
.
rewrite
-(
right_id
True
%
I
(
★
)%
I
(
φ
_
))
.
rewrite
(
own_alloc
AuthI
(
Auth
(
Excl
a
)
a
)
N
)
//
;
[].
intros
Ha
.
eapply
sep_elim_True_r
.
{
by
eapply
(
own_alloc
AuthI
(
Auth
(
Excl
a
)
a
)
N
)
.
}
rewrite
pvs_frame_l
.
apply
pvs_strip_pvs
.
rewrite
sep_exist_l
.
apply
exist_elim
=>
γ
.
rewrite
-(
exist_intro
γ
).
transitivity
(
▷
auth_inv
AuthI
γ
φ
★
auth_own
AuthI
γ
a
)%
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