Skip to content
GitLab
Menu
Projects
Groups
Snippets
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in / Register
Toggle navigation
Menu
Open sidebar
Iris
Fairis
Commits
09e52924
Commit
09e52924
authored
Feb 25, 2016
by
Robbert Krebbers
Browse files
Remove obsolete tactic wp_strip_later.
parent
2ee38008
Changes
1
Show whitespace changes
Inline
Sidebyside
heap_lang/wp_tactics.v
View file @
09e52924
...
...
@@ 5,14 +5,6 @@ Import uPred.
(
**
wp

specific
helper
tactics
*
)
(
*
First
try
to
productively
strip
off
laters
;
if
that
fails
,
at
least
cosmetically
get
rid
of
laters
in
the
conclusion
.
*
)
Ltac
wp_strip_later
:=
let
rec
go
:=
lazymatch
goal
with


_
⊑
(
_
★
_
)
=>
apply
sep_mono
;
go


_
⊑
▷
_
=>
apply
later_intro


_
⊑
_
=>
reflexivity
end
in
intros_revert
ltac
:
(
first
[
strip_later

etrans
;
[

go
]
]
).
Ltac
wp_bind
K
:=
lazymatch
eval
hnf
in
K
with

[]
=>
idtac
...
...
@@ 25,7 +17,7 @@ Ltac wp_finish :=


_
⊑
wp
_
_
_
=>
etrans
;
[

eapply
wp_value_pvs
;
reflexivity
];
(
*
sometimes
,
we
will
have
to
do
a
final
view
shift
,
so
only
apply
wp_value
if
we
obtain
a
consecutive
wp
*
)
pvs_intro
if
we
obtain
a
consecutive
wp
*
)
try
(
eapply
pvs_intro
;
match
goal
with

_
⊑
wp
_
_
_
=>
simpl

_
=>
fail
end
)

_
=>
idtac
...
...
@@ 42,7 +34,7 @@ Tactic Notation "wp_rec" ">" :=
wp_finish
end
)
end
).
Tactic
Notation
"wp_rec"
:=
wp_rec
>
;
wp_
strip_later
.
Tactic
Notation
"wp_rec"
:=
wp_rec
>
;
try
strip_later
.
Tactic
Notation
"wp_lam"
">"
:=
match
goal
with
...
...
@@ 52,7 +44,7 @@ Tactic Notation "wp_lam" ">" :=
wp_bind
K
;
etrans
;
[

eapply
wp_lam
;
reflexivity
];
wp_finish
end
)
end
.
Tactic
Notation
"wp_lam"
:=
wp_lam
>
;
wp_
strip_later
.
Tactic
Notation
"wp_lam"
:=
wp_lam
>
;
try
strip_later
.
Tactic
Notation
"wp_let"
">"
:=
wp_lam
>
.
Tactic
Notation
"wp_let"
:=
wp_lam
.
...
...
@@ 72,7 +64,7 @@ Tactic Notation "wp_op" ">" :=
wp_bind
K
;
etrans
;
[

eapply
wp_un_op
;
reflexivity
];
wp_finish
end
)
end
.
Tactic
Notation
"wp_op"
:=
wp_op
>
;
wp_
strip_later
.
Tactic
Notation
"wp_op"
:=
wp_op
>
;
try
strip_later
.
Tactic
Notation
"wp_if"
">"
:=
match
goal
with
...
...
@@ 83,7 +75,7 @@ Tactic Notation "wp_if" ">" :=
etrans
;
[

apply
wp_if_true

apply
wp_if_false
];
wp_finish
end
)
end
.
Tactic
Notation
"wp_if"
:=
wp_if
>
;
wp_
strip_later
.
Tactic
Notation
"wp_if"
:=
wp_if
>
;
try
strip_later
.
Tactic
Notation
"wp_focus"
open_constr
(
efoc
)
:=
match
goal
with
...
...
@@ 95,7 +87,7 @@ Tactic Notation "wp" ">" tactic(tac) :=
match
goal
with


_
⊑
wp
?
E
?
e
?
Q
=>
reshape_expr
e
ltac
:
(
fun
K
e
'
=>
wp_bind
K
;
tac
)
end
.
Tactic
Notation
"wp"
tactic
(
tac
)
:=
(
wp
>
tac
);
[
wp_
strip_later

..].
Tactic
Notation
"wp"
tactic
(
tac
)
:=
(
wp
>
tac
);
[
try
strip_later

..].
(
*
In
case
the
precondition
does
not
match
.
TODO:
Have
one
tactic
unifying
wp
and
ewp
.
*
)
...
...
Write
Preview
Markdown
is supported
0%
Try again
or
attach a new file
.
Attach a 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