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
Dan Frumin
iriscoq
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
wp

specific
at
all
.
They
should
move
elsewhere
.
*
)
(
*
TODO
:
The
next
few
tactics
are
not
wp

specific
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
]).
(
*
ssreflect

locks
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