Skip to content
GitLab
Projects
Groups
Snippets
Help
Loading...
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in / Register
Toggle navigation
Open sidebar
Iris
Iris
Commits
6fe4e8aa
Commit
6fe4e8aa
authored
Feb 25, 2016
by
Ralf Jung
Browse files
Merge branch 'master' of gitlab.mpisws.org:FP/iriscoq
parents
b55c40d6
ad7c7b15
Pipeline
#164
passed with stage
Changes
2
Pipelines
1
Hide whitespace changes
Inline
Sidebyside
Showing
2 changed files
with
52 additions
and
60 deletions
+52
60
algebra/upred_tactics.v
algebra/upred_tactics.v
+32
32
heap_lang/wp_tactics.v
heap_lang/wp_tactics.v
+20
28
No files found.
algebra/upred_tactics.v
View file @
6fe4e8aa
...
...
@@ 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 @
6fe4e8aa
...
...
@@ 5,14 +5,6 @@ Import uPred.
(** 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
intros_revert
ltac
:
(
first
[
strip_later

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

[]
=>
idtac
...
...
@@ 23,26 +15,26 @@ 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
wp_value
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
).
Tactic
Notation
"wp_rec"
:
=
wp_rec
>
;
wp_
strip_later
.
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"
">"
:
=
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