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
Joshua Yanovski
iris-coq
Commits
0a44697a
Commit
0a44697a
authored
Feb 16, 2016
by
Robbert Krebbers
Browse files
wp_tactics: use wp_value afterwards instead of before.
parent
ae988e2f
Changes
2
Hide whitespace changes
Inline
Side-by-side
heap_lang/tests.v
View file @
0a44697a
...
...
@@ -69,7 +69,7 @@ Section LiftingTests.
-
wp_if
.
rewrite
(
forall_elim
(
n1
+
1
))
const_equiv
;
last
omega
.
by
rewrite
left_id
impl_elim_l
.
-
assert
(
n1
=
n2
-
1
)
as
->
by
omega
.
wp_if
.
wp_value
.
auto
with
I
.
wp_if
.
auto
with
I
.
Qed
.
Lemma
Pred_spec
n
E
Q
:
▷
Q
(
LitV
(
n
-
1
))
⊑
wp
E
(
Pred
'
n
)
%
L
Q
.
...
...
heap_lang/wp_tactics.v
View file @
0a44697a
...
...
@@ -11,49 +11,58 @@ Ltac wp_bind K :=
|
[]
=>
idtac
|
_
=>
etransitivity
;
[
|
apply
(
wp_bind
K
)];
simpl
end
.
Ltac
wp_finish
:=
let
rec
go
:=
match
goal
with
|
|-
∀
_
,
_
=>
let
H
:=
fresh
in
intro
H
;
go
;
revert
H
|
|-
_
⊑
▷
_
=>
etransitivity
;
[
|
apply
later_mono
;
go
;
reflexivity
]
|
|-
_
⊑
wp
_
_
_
=>
etransitivity
;
[
|
eapply
wp_value
;
reflexivity
];
simpl
|
_
=>
idtac
end
in
simpl
;
go
.
Tactic
Notation
"wp_value"
:=
match
goal
with
|
|-
_
⊑
wp
?
E
?
e
?
Q
=>
etransitivity
;
[
|
by
eapply
wp_value
];
simpl
|
|-
_
⊑
wp
?
E
?
e
?
Q
=>
etransitivity
;
[
|
eapply
wp_value
;
reflexivity
];
simpl
end
.
Tactic
Notation
"wp_rec"
"!"
:=
repeat
wp_value
;
match
goal
with
|
|-
_
⊑
wp
?
E
?
e
?
Q
=>
reshape_expr
e
ltac
:
(
fun
K
e
'
=>
match
eval
cbv
in
e
'
with
|
App
(
Rec
_
_
_
)
_
=>
wp_bind
K
;
etransitivity
;
[
|
by
eapply
wp_rec
];
simpl
|
App
(
Rec
_
_
_
)
_
=>
wp_bind
K
;
etransitivity
;
[
|
eapply
wp_rec
;
reflexivity
];
wp_finish
end
)
end
.
Tactic
Notation
"wp_rec"
:=
wp_rec
!
;
wp_strip_later
.
Tactic
Notation
"wp_bin_op"
"!"
:=
repeat
wp_value
;
match
goal
with
|
|-
_
⊑
wp
?
E
?
e
?
Q
=>
reshape_expr
e
ltac
:
(
fun
K
e
'
=>
match
eval
cbv
in
e
'
with
|
BinOp
LtOp
_
_
=>
wp_bind
K
;
apply
wp_lt
;
[
|
]
|
BinOp
LeOp
_
_
=>
wp_bind
K
;
apply
wp_le
;
[
|
]
|
BinOp
EqOp
_
_
=>
wp_bind
K
;
apply
wp_eq
;
[
|
]
|
BinOp
_
_
_
=>
wp_bind
K
;
etransitivity
;
[
|
by
eapply
wp_bin_op
];
simpl
|
BinOp
LtOp
_
_
=>
wp_bind
K
;
apply
wp_lt
;
wp_finish
|
BinOp
LeOp
_
_
=>
wp_bind
K
;
apply
wp_le
;
wp_finish
|
BinOp
EqOp
_
_
=>
wp_bind
K
;
apply
wp_eq
;
wp_finish
|
BinOp
_
_
_
=>
wp_bind
K
;
etransitivity
;
[
|
eapply
wp_bin_op
;
reflexivity
];
wp_finish
end
)
end
.
Tactic
Notation
"wp_bin_op"
:=
wp_bin_op
!
;
wp_strip_later
.
Tactic
Notation
"wp_un_op"
"!"
:=
repeat
wp_value
;
match
goal
with
|
|-
_
⊑
wp
?
E
?
e
?
Q
=>
reshape_expr
e
ltac
:
(
fun
K
e
'
=>
match
eval
cbv
in
e
'
with
|
UnOp
_
_
=>
wp_bind
K
;
etransitivity
;
[
|
by
eapply
wp_un_op
];
simpl
|
UnOp
_
_
=>
wp_bind
K
;
etransitivity
;
[
|
eapply
wp_un_op
;
reflexivity
];
wp_finish
end
)
end
.
Tactic
Notation
"wp_un_op"
:=
wp_un_op
!
;
wp_strip_later
.
Tactic
Notation
"wp_if"
"!"
:=
repeat
wp_value
;
try
wp_value
;
match
goal
with
|
|-
_
⊑
wp
?
E
?
e
?
Q
=>
reshape_expr
e
ltac
:
(
fun
K
e
'
=>
match
eval
cbv
in
e
'
with
|
If
_
_
_
=>
wp_bind
K
;
etransitivity
;
[
|
by
apply
wp_if_true
||
by
apply
wp_if_false
]
wp_bind
K
;
etransitivity
;
[
|
apply
wp_if_true
||
apply
wp_if_false
];
wp_finish
end
)
end
.
Tactic
Notation
"wp_if"
:=
wp_if
!
;
wp_strip_later
.
...
...
Write
Preview
Supports
Markdown
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