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
8cf16088
Commit
8cf16088
authored
Feb 20, 2016
by
Ralf Jung
Browse files
get rid of the unnecessary locking; the wand gives us enough structure in the goal
parent
ed12ea1c
Changes
2
Hide whitespace changes
Inline
Sidebyside
algebra/upred.v
View file @
8cf16088
...
...
@@ 217,10 +217,6 @@ Notation "✓ x" := (uPred_valid x) (at level 20) : uPred_scope.
Definition
uPred_iff
{
M
}
(
P
Q
:
uPred
M
)
:
uPred
M
:
=
((
P
→
Q
)
∧
(
Q
→
P
))%
I
.
Infix
"↔"
:
=
uPred_iff
:
uPred_scope
.
Lemma
uPred_lock_conclusion
{
M
}
(
P
Q
:
uPred
M
)
:
P
⊑
locked
Q
→
P
⊑
Q
.
Proof
.
by
rewrite

lock
.
Qed
.
Class
TimelessP
{
M
}
(
P
:
uPred
M
)
:
=
timelessP
:
▷
P
⊑
(
P
∨
▷
False
).
Arguments
timelessP
{
_
}
_
{
_
}
_
_
_
_
.
Class
AlwaysStable
{
M
}
(
P
:
uPred
M
)
:
=
always_stable
:
P
⊑
□
P
.
...
...
heap_lang/wp_tactics.v
View file @
8cf16088
From
heap_lang
Require
Export
tactics
substitution
.
Import
uPred
.
(* TODO: The next
5
tactics are not wpspecific at all. They should move elsewhere. *)
(* TODO: The next
few
tactics are not wpspecific at all. They should move elsewhere. *)
Ltac
revert_intros
tac
:
=
lazymatch
goal
with
...
...
@@ 47,9 +47,6 @@ Ltac u_strip_later :=
in
revert_intros
ltac
:
(
etrans
;
[
shape_Q
]
;
etrans
;
last
eapply
later_mono
;
first
solve
[
strip
]).
(* ssreflectlocks the part after the ⊑ *)
Ltac
u_lock_goal
:
=
revert_intros
ltac
:
(
apply
uPred_lock_conclusion
).
(** Transforms a goal of the form ∀ ..., ?0... → ?1 ⊑ ?2
into True ⊑ ∀..., ■?0... → ?1 ★ ?2, applies tac, and
the moves all the assumptions back. *)
...
...
@@ 72,7 +69,7 @@ Ltac u_revert_all :=
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. *)
Ltac
u_l
ö
b
tac
:
=
u_lock_goal
;
u_revert_all
;
u_revert_all
;
(* We now have a goal for the form True ⊑ P, with the "original" conclusion
being locked. *)
apply
l
ö
b_strong
;
etransitivity
;
...
...
@@ 86,8 +83,8 @@ Ltac u_löb tac :=


_
⊑
(
■
_
→
_
)
=>
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 wand introduced
by u_revert_all
and the lock,
as well as the ▷ from löb_strong. *)


▷
_
⊑
(
_

★
locked
_
)
=>
apply
wand_intro_l
;
unlock
;
tac
by u_revert_all as well as the ▷ from löb_strong. *)


▷
_
⊑
(
_

★
_
)
=>
apply
wand_intro_l
;
tac
end
in
go
.
...
...
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