Skip to content
GitLab
Menu
Projects
Groups
Snippets
Loading...
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in / Register
Toggle navigation
Menu
Open sidebar
PierreMarie Pédrot
Iris
Commits
faf2018e
Commit
faf2018e
authored
Feb 20, 2016
by
Ralf Jung
Browse files
make u_strip_later more clever; also use it for wp_strip_later
parent
6428df91
Changes
2
Hide whitespace changes
Inline
Sidebyside
heap_lang/tests.v
View file @
faf2018e
...
...
@@ 61,7 +61,7 @@ Section LiftingTests.
Lemma
Pred_spec
n
E
Φ
:
▷
Φ
(
LitV
(
n

1
))
⊑

Pred
'
n
@
E
{{
Φ
}}.
Proof
.
wp_lam
>
;
apply
later_mono
;
wp_op
=>
?
;
wp_if
.
wp_lam
.
wp_op
=>
?
;
wp_if
.

wp_op
.
wp_op
.
(* TODO: Can we use the wp tactic again here? It seems that the tactic fails if there
are goals being generated. That should not be the case. *)
...
...
heap_lang/wp_tactics.v
View file @
faf2018e
From
heap_lang
Require
Export
tactics
substitution
.
Import
uPred
.
(* TODO: The next
6
tactics are not wpspecific at all. They should move elsewhere. *)
(* TODO: The next
5
tactics are not wpspecific at all. They should move elsewhere. *)
Ltac
revert_intros
tac
:
=
lazymatch
goal
with


∀
_
,
_
=>
let
H
:
=
fresh
in
intro
H
;
revert_intros
tac
;
revert
H


_
=>
tac
end
.
Ltac
wp_strip_later
:
=
let
rec
go
:
=
lazymatch
goal
with


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


_
⊑
▷
_
=>
apply
later_intro


_
⊑
_
=>
reflexivity
end
in
revert_intros
ltac
:
(
etrans
;
[
go
]).
(** Assumes a goal of the shape P ⊑ ▷ Q.
Will get rid of ▷ in P below ★, ∧ and ∨. *)
(** Assumes a goal of the shape P ⊑ ▷ Q. Alterantively, if Q
is built of ★, ∧, ∨ with ▷ in all branches; that will work, too.
Will turn this goal into P ⊑ Q and strip ▷ in P below ★, ∧, ∨. *)
Ltac
u_strip_later
:
=
let
rec
strip
:
=
match
goal
with
lazy
match
goal
with


(
_
★
_
)
⊑
▷
_
=>
etrans
;
last
(
eapply
equiv_spec
,
later_sep
)
;
apply
sep_mono
;
strip
...
...
@@ 34,7 +27,25 @@ Ltac u_strip_later :=


▷
_
⊑
▷
_
=>
apply
later_mono
;
reflexivity


_
⊑
▷
_
=>
apply
later_intro
;
reflexivity
end
in
etrans
;
last
eapply
later_mono
;
first
solve
[
strip
].
in
let
rec
shape_Q
:
=
lazymatch
goal
with


_
⊑
(
_
★
_
)
=>
(* Force the later on the LHS to be toplevel, matching laters
below ★ on the RHS *)
etrans
;
first
(
apply
equiv_spec
;
symmetry
;
apply
later_sep
;
reflexivity
)
;
(* Match the arm recursively *)
apply
sep_mono
;
shape_Q


_
⊑
(
_
∧
_
)
=>
etrans
;
first
(
apply
equiv_spec
;
symmetry
;
apply
later_and
;
reflexivity
)
;
apply
sep_mono
;
shape_Q


_
⊑
(
_
∨
_
)
=>
etrans
;
first
(
apply
equiv_spec
;
symmetry
;
apply
later_or
;
reflexivity
)
;
apply
sep_mono
;
shape_Q


_
⊑
▷
_
=>
apply
later_mono
;
reflexivity
(* We fail if we don't find laters in all branches. *)
end
in
revert_intros
ltac
:
(
etrans
;
[
shape_Q
]
;
etrans
;
last
eapply
later_mono
;
first
solve
[
strip
]).
(* ssreflectlocks the part after the ⊑ *)
(* FIXME: I tried doing a lazymatch to only apply the tactic if the goal has shape ⊑,
...
...
@@ 47,28 +58,31 @@ Ltac u_lock_goal := revert_intros ltac:(apply uPred_lock_conclusion).
Ltac
u_revert_all
:
=
lazymatch
goal
with


∀
_
,
_
=>
let
H
:
=
fresh
in
intro
H
;
u_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'
]
(* 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
⊑
_
=>
trans
(
True
★
C
)%
I
;
first
(
rewrite
[(
True
★
C
)%
I
]
left_id
;
reflexivity
)
;
apply
wand_elim_l'
first
(
rewrite
[(
True
★
C
)%
I
]
left_id
;
reflexivity
)
;
apply
wand_elim_l'
end
.
(** This starts on a goal of the form ∀ ..., ?0... → ?1 ⊑ ?2.
It applies löb where all the Coq assumptions have been turned into logical
assumptions, then moves all the Coq assumptions back out to the context,
applies [tac] on the goal (now of the form _ ⊑ _), and then reverts the Coq
assumption so that we end up with the same shape as where we started. *)
applies [tac ()] on the goal (now of the form _ ⊑ _), and then reverts the
Coq assumption so that we end up with the same shape as where we started.
[tac] is a thunk because I found no other way to prevent Coq from expandig
matches too early.*)
Ltac
u_l
ö
b
tac
:
=
u_lock_goal
;
u_revert_all
;
(* We now have a goal for the form True ⊑ P, with the "original" conclusion
being locked. *)
apply
l
ö
b_strong
;
etransitivity
;
first
(
apply
equiv_spec
;
symmetry
;
apply
(
left_id
_
_
_
)
;
reflexivity
)
;
(* Now introduce again all the things that we reverted, and at the bottom, do the work *)
(* 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
;
...
...
@@ 76,13 +90,21 @@ Ltac u_löb tac :=


_
⊑
(
■
_
→
_
)
=>
apply
impl_intro_l
,
const_elim_l
;
let
H
:
=
fresh
in
intro
H
;
go
;
revert
H


▷
?R
⊑
(
?L

★
locked
_
)
=>
apply
wand_intro_l
;
(* TODO: Do sth. more robust than rewriting. *)
trans
(
▷
L
★
▷
R
)%
I
;
first
(
apply
sep_mono_l
,
later_intro
;
reflexivity
)
;
trans
(
▷
(
L
★
R
))%
I
;
first
(
apply
equiv_spec
,
later_sep
;
reflexivity
)
;
unlock
;
tac
unlock
;
tac
()
end
in
go
.
(** wpspecific 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
revert_intros
ltac
:
(
first
[
u_strip_later

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

[]
=>
idtac
...
...
@@ 101,16 +123,16 @@ Ltac wp_finish :=

_
=>
idtac
end
in
simpl
;
revert_intros
go
.
Tactic
Notation
"wp_rec"
:
=
u_l
ö
b
ltac
:
(
(* Find the redex and apply wp_rec *)
match
goal
with
Tactic
Notation
"wp_rec"
">"
:
=
u_l
ö
b
ltac
:
(
fun
_
=>
(* Find the redex and apply wp_rec *)
lazy
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
;
etrans
;
[
eapply
wp_rec
;
reflexivity
]
;
wp_finish
end
)
end
;
apply
later_mono
)
.
end
).
Tactic
Notation
"wp_rec"
:
=
wp_rec
>
;
wp_strip_later
.
Tactic
Notation
"wp_lam"
">"
:
=
match
goal
with
...
...
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