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
Rodolphe Lepigre
Iris
Commits
7453ecb0
Commit
7453ecb0
authored
Nov 29, 2017
by
Robbert Krebbers
Browse files
Rename `wp_simpl` → `wp_expr_simpl` to emphasize that it only simplifies the expression part.
parent
af9bfce4
Changes
1
Hide whitespace changes
Inline
Side-by-side
theories/heap_lang/proofmode.v
View file @
7453ecb0
...
...
@@ -5,17 +5,17 @@ From iris.heap_lang Require Export tactics lifting.
Set
Default
Proof
Using
"Type"
.
Import
uPred
.
Lemma
tac_wp_
simp
l
`
{
heapG
Σ
}
Δ
E
Φ
e
e'
:
Lemma
tac_wp_
expr_eva
l
`
{
heapG
Σ
}
Δ
E
Φ
e
e'
:
e
=
e'
→
envs_entails
Δ
(
WP
e'
@
E
{{
Φ
}})
→
envs_entails
Δ
(
WP
e
@
E
{{
Φ
}}).
Proof
.
by
intros
->.
Qed
.
Ltac
wp_eval
t
:
=
Ltac
wp_
expr_
eval
t
:
=
try
iStartProof
;
try
(
eapply
tac_wp_
simp
l
;
[
t
;
reflexivity
|]).
try
(
eapply
tac_wp_
expr_eva
l
;
[
t
;
reflexivity
|]).
Ltac
wp_simpl
:
=
wp_eval
simpl
.
Ltac
wp_simpl_subst
:
=
wp_eval
simpl_subst
.
Ltac
wp_
expr_
simpl
:
=
wp_
expr_
eval
simpl
.
Ltac
wp_
expr_
simpl_subst
:
=
wp_
expr_
eval
simpl_subst
.
Lemma
tac_wp_pure
`
{
heapG
Σ
}
Δ
Δ
'
E
e1
e2
φ
Φ
:
PureExec
φ
e1
e2
→
...
...
@@ -46,7 +46,7 @@ Tactic Notation "wp_pure" open_constr(efoc) :=
[
apply
_
(* PureExec *)
|
try
fast_done
(* The pure condition for PureExec *)
|
apply
_
(* IntoLaters *)
|
wp_simpl_subst
;
try
wp_value_head
(* new goal *)
|
wp_
expr_
simpl_subst
;
try
wp_value_head
(* new goal *)
])
||
fail
"wp_pure: cannot find"
efoc
"in"
e
"or"
efoc
"is not a reduct"
|
_
=>
fail
"wp_pure: not a 'wp'"
...
...
@@ -168,7 +168,7 @@ Tactic Notation "wp_apply" open_constr(lem) :=
lazymatch
goal
with
|
|-
envs_entails
_
(
wp
?E
?e
?Q
)
=>
reshape_expr
e
ltac
:
(
fun
K
e'
=>
wp_bind_core
K
;
iApplyHyp
H
;
try
iNext
;
wp_simpl
)
||
wp_bind_core
K
;
iApplyHyp
H
;
try
iNext
;
wp_
expr_
simpl
)
||
lazymatch
iTypeOf
H
with
|
Some
(
_
,
?P
)
=>
fail
"wp_apply: cannot apply"
P
end
...
...
@@ -187,7 +187,7 @@ Tactic Notation "wp_alloc" ident(l) "as" constr(H) :=
|
first
[
intros
l
|
fail
1
"wp_alloc:"
l
"not fresh"
]
;
eexists
;
split
;
[
env_cbv
;
reflexivity
||
fail
"wp_alloc:"
H
"not fresh"
|
wp_simpl
;
try
wp_value_head
]]
|
wp_
expr_
simpl
;
try
wp_value_head
]]
|
_
=>
fail
"wp_alloc: not a 'wp'"
end
.
...
...
@@ -204,7 +204,7 @@ Tactic Notation "wp_load" :=
[
apply
_
|
let
l
:
=
match
goal
with
|-
_
=
Some
(
_
,
(
?l
↦
{
_
}
_
)%
I
)
=>
l
end
in
iAssumptionCore
||
fail
"wp_load: cannot find"
l
"↦ ?"
|
wp_simpl
;
try
wp_value_head
]
|
wp_
expr_
simpl
;
try
wp_value_head
]
|
_
=>
fail
"wp_load: not a 'wp'"
end
.
...
...
@@ -220,7 +220,7 @@ Tactic Notation "wp_store" :=
|
let
l
:
=
match
goal
with
|-
_
=
Some
(
_
,
(
?l
↦
{
_
}
_
)%
I
)
=>
l
end
in
iAssumptionCore
||
fail
"wp_store: cannot find"
l
"↦ ?"
|
env_cbv
;
reflexivity
|
wp_simpl
;
try
first
[
wp_pure
(
Seq
(
Lit
LitUnit
)
_
)|
wp_value_head
]]
|
wp_
expr_
simpl
;
try
first
[
wp_pure
(
Seq
(
Lit
LitUnit
)
_
)|
wp_value_head
]]
|
_
=>
fail
"wp_store: not a 'wp'"
end
.
...
...
@@ -236,7 +236,7 @@ Tactic Notation "wp_cas_fail" :=
|
let
l
:
=
match
goal
with
|-
_
=
Some
(
_
,
(
?l
↦
{
_
}
_
)%
I
)
=>
l
end
in
iAssumptionCore
||
fail
"wp_cas_fail: cannot find"
l
"↦ ?"
|
try
congruence
|
wp_simpl
;
try
wp_value_head
]
|
wp_
expr_
simpl
;
try
wp_value_head
]
|
_
=>
fail
"wp_cas_fail: not a 'wp'"
end
.
...
...
@@ -253,6 +253,6 @@ Tactic Notation "wp_cas_suc" :=
iAssumptionCore
||
fail
"wp_cas_suc: cannot find"
l
"↦ ?"
|
try
congruence
|
env_cbv
;
reflexivity
|
wp_simpl
;
try
wp_value_head
]
|
wp_
expr_
simpl
;
try
wp_value_head
]
|
_
=>
fail
"wp_cas_suc: not a 'wp'"
end
.
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