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
Tej Chajed
iris
Commits
ad7c7b15
Commit
ad7c7b15
authored
Feb 25, 2016
by
Robbert Krebbers
Browse files
Make identation more consistent in upred/wp tactics.
parent
a39b10c9
Changes
2
Hide whitespace changes
Inline
Sidebyside
algebra/upred_tactics.v
View file @
ad7c7b15
...
...
@@ 151,19 +151,19 @@ Tactic Notation "ecancel" open_constr(Ps) :=
Will turn this goal into P ⊑ Q and strip ▷ in P below ★, ∧, ∨. *)
Ltac
strip_later
:
=
let
rec
strip
:
=
lazymatch
goal
with


(
_
★
_
)
⊑
▷
_
=>
etrans
;
last
(
eapply
equiv_entails_sym
,
later_sep
)
;
apply
sep_mono
;
strip


(
_
∧
_
)
⊑
▷
_
=>
etrans
;
last
(
eapply
equiv_entails_sym
,
later_and
)
;
apply
sep_mono
;
strip


(
_
∨
_
)
⊑
▷
_
=>
etrans
;
last
(
eapply
equiv_entails_sym
,
later_or
)
;
apply
sep_mono
;
strip


▷
_
⊑
▷
_
=>
apply
later_mono
;
reflexivity


_
⊑
▷
_
=>
apply
later_intro
;
reflexivity
end
lazymatch
goal
with


(
_
★
_
)
⊑
▷
_
=>
etrans
;
last
(
eapply
equiv_entails_sym
,
later_sep
)
;
apply
sep_mono
;
strip


(
_
∧
_
)
⊑
▷
_
=>
etrans
;
last
(
eapply
equiv_entails_sym
,
later_and
)
;
apply
sep_mono
;
strip


(
_
∨
_
)
⊑
▷
_
=>
etrans
;
last
(
eapply
equiv_entails_sym
,
later_or
)
;
apply
sep_mono
;
strip


▷
_
⊑
▷
_
=>
apply
later_mono
;
reflexivity


_
⊑
▷
_
=>
apply
later_intro
;
reflexivity
end
in
let
rec
shape_Q
:
=
lazymatch
goal
with


_
⊑
(
_
★
_
)
=>
...
...
@@ 190,13 +190,14 @@ Ltac strip_later :=
(* TODO: this name may be a big too general *)
Ltac
revert_all
:
=
lazymatch
goal
with


∀
_
,
_
=>
let
H
:
=
fresh
in
intro
H
;
revert_all
;
(* TODO: Really, we should distinguish based on whether this is a
dependent function type or not. Right now, we distinguish based
on the sort of the argument, which is suboptimal. *)
first
[
apply
(
const_intro_impl
_
_
_
H
)
;
clear
H

revert
H
;
apply
forall_elim'
]


?C
⊑
_
=>
apply
impl_entails


∀
_
,
_
=>
let
H
:
=
fresh
in
intro
H
;
revert_all
;
(* TODO: Really, we should distinguish based on whether this is a
dependent function type or not. Right now, we distinguish based
on the sort of the argument, which is suboptimal. *)
first
[
apply
(
const_intro_impl
_
_
_
H
)
;
clear
H

revert
H
;
apply
forall_elim'
]


_
⊑
_
=>
apply
impl_entails
end
.
(** This starts on a goal of the form ∀ ..., ?0... → ?1 ⊑ ?2.
...
...
@@ 217,16 +218,15 @@ Ltac löb tac :=
(* Now introduce again all the things that we reverted, and at the bottom,
do the work *)
let
rec
go
:
=
lazymatch
goal
with


_
⊑
(
∀
_
,
_
)
=>
apply
forall_intro
;
let
H
:
=
fresh
in
intro
H
;
go
;
revert
H


_
⊑
(
■
_
→
_
)
=>
apply
impl_intro_l
,
const_elim_l
;
let
H
:
=
fresh
in
intro
H
;
go
;
revert
H
(* This is the "bottom" of the goal, where we see the impl introduced
by uPred_revert_all as well as the ▷ from löb_strong and the □ we added. *)


▷
□
?R
⊑
(
?L
→
_
)
=>
apply
impl_intro_l
;
trans
(
L
★
▷
□
R
)%
I
;
first
(
eapply
equiv_entails
,
always_and_sep_r
,
_;
reflexivity
)
;
tac
end
lazymatch
goal
with


_
⊑
(
∀
_
,
_
)
=>
apply
forall_intro
;
let
H
:
=
fresh
in
intro
H
;
go
;
revert
H


_
⊑
(
■
_
→
_
)
=>
apply
impl_intro_l
,
const_elim_l
;
let
H
:
=
fresh
in
intro
H
;
go
;
revert
H
(* This is the "bottom" of the goal, where we see the impl introduced
by uPred_revert_all as well as the ▷ from löb_strong and the □ we added. *)


▷
□
?R
⊑
(
?L
→
_
)
=>
apply
impl_intro_l
;
trans
(
L
★
▷
□
R
)%
I
;
[
eapply
equiv_entails
,
always_and_sep_r
,
_;
reflexivity

tac
]
end
in
go
.
heap_lang/wp_tactics.v
View file @
ad7c7b15
...
...
@@ 15,25 +15,25 @@ Ltac wp_finish :=
match
goal
with


_
⊑
▷
_
=>
etrans
;
[
apply
later_mono
;
go
;
reflexivity
]


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

_
⊑
wp
_
_
_
=>
simpl

_
=>
fail
end
)
etrans
;
[
eapply
wp_value_pvs
;
reflexivity
]
;
(* sometimes, we will have to do a final view shift, so only apply
pvs_intro if we obtain a consecutive wp *)
try
(
eapply
pvs_intro
;
match
goal
with

_
⊑
wp
_
_
_
=>
simpl

_
=>
fail
end
)

_
=>
idtac
end
in
simpl
;
intros_revert
go
.
Tactic
Notation
"wp_rec"
">"
:
=
l
ö
b
ltac
:
(
(* Find the redex and apply wp_rec *)
idtac
;
(* <https://coq.inria.fr/bugs/show_bug.cgi?id=4584>
*)
lazymatch
goal
with


_
⊑
wp
?E
?e
?Q
=>
reshape_expr
e
ltac
:
(
fun
K
e'
=>
match
eval
cbv
in
e'
with

App
(
Rec
_
_
_
)
_
=>
wp_bind
K
;
etrans
;
[
eapply
wp_rec
;
reflexivity
]
;
wp_finish
end
)
end
).
l
ö
b
ltac
:
(
(* Find the redex and apply wp_rec
*)
idtac
;
(* <https://coq.inria.fr/bugs/show_bug.cgi?id=4584> *)
lazymatch
goal
with


_
⊑
wp
?E
?e
?Q
=>
reshape_expr
e
ltac
:
(
fun
K
e'
=>
match
eval
cbv
in
e'
with

App
(
Rec
_
_
_
)
_
=>
wp_bind
K
;
etrans
;
[
eapply
wp_rec
;
reflexivity
]
;
wp_finish
end
)
end
).
Tactic
Notation
"wp_rec"
:
=
wp_rec
>
;
try
strip_later
.
Tactic
Notation
"wp_lam"
">"
:
=
...
...
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