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
Iris
Fairis
Commits
df7a0a33
Commit
df7a0a33
authored
Feb 16, 2016
by
Ralf Jung
Browse files
Merge branch 'master' of gitlab.mpisws.org:FP/iriscoq
parents
1ee007f8
cd509c3f
Changes
2
Hide whitespace changes
Inline
Sidebyside
heap_lang/tests.v
View file @
df7a0a33
...
@@ 67,7 +67,7 @@ Section LiftingTests.
...
@@ 67,7 +67,7 @@ Section LiftingTests.
wp_rec
.
wp_bin_op
.
wp_rec
.
wp_bin_op
=>
?
;
wp_if
.
wp_rec
.
wp_bin_op
.
wp_rec
.
wp_bin_op
=>
?
;
wp_if
.

rewrite
(
forall_elim
(
n1
+
1
))
const_equiv
;
last
omega
.

rewrite
(
forall_elim
(
n1
+
1
))
const_equiv
;
last
omega
.
by
rewrite
left_id
impl_elim_l
.
by
rewrite
left_id
impl_elim_l
.

assert
(
n1
=
n2

1
)
as
>
by
omega
;
auto
with
I
.

wp_value
.
assert
(
n1
=
n2

1
)
as
>
by
omega
;
auto
with
I
.
Qed
.
Qed
.
Lemma
Pred_spec
n
E
Q
:
▷
Q
(
LitV
(
n

1
))
⊑
wp
E
(
Pred
'
n
)
%
L
Q
.
Lemma
Pred_spec
n
E
Q
:
▷
Q
(
LitV
(
n

1
))
⊑
wp
E
(
Pred
'
n
)
%
L
Q
.
...
...
heap_lang/wp_tactics.v
View file @
df7a0a33
...
@@ 16,7 +16,11 @@ Ltac wp_finish :=
...
@@ 16,7 +16,11 @@ Ltac wp_finish :=
match
goal
with
match
goal
with


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


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


_
⊑
▷
_
=>
etransitivity
;
[

apply
later_mono
;
go
;
reflexivity
]


_
⊑
▷
_
=>
etransitivity
;
[

apply
later_mono
;
go
;
reflexivity
]


_
⊑
wp
_
_
_
=>
etransitivity
;
[

eapply
wp_value
;
reflexivity
];
simpl


_
⊑
wp
_
_
_
=>
etransitivity
;
[

eapply
wp_value
;
reflexivity
];
(
*
sometimes
,
we
will
have
to
do
a
final
view
shift
,
so
only
apply
wp_value
if
we
obtain
a
consecutive
wp
*
)
match
goal
with

_
⊑
wp
_
_
_
=>
simpl

_
=>
fail
end

_
=>
idtac

_
=>
idtac
end
in
simpl
;
go
.
end
in
simpl
;
go
.
...
@@ 55,7 +59,6 @@ Tactic Notation "wp_un_op" ">" :=
...
@@ 55,7 +59,6 @@ Tactic Notation "wp_un_op" ">" :=
end
.
end
.
Tactic
Notation
"wp_un_op"
:=
wp_un_op
>
;
wp_strip_later
.
Tactic
Notation
"wp_un_op"
:=
wp_un_op
>
;
wp_strip_later
.
Tactic
Notation
"wp_if"
">"
:=
Tactic
Notation
"wp_if"
">"
:=
try
wp_value
;
match
goal
with
match
goal
with


_
⊑
wp
?
E
?
e
?
Q
=>
reshape_expr
e
ltac
:
(
fun
K
e
'
=>


_
⊑
wp
?
E
?
e
?
Q
=>
reshape_expr
e
ltac
:
(
fun
K
e
'
=>
match
eval
cbv
in
e
'
with
match
eval
cbv
in
e
'
with
...
...
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