Skip to content
GitLab
Projects
Groups
Snippets
/
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in / Register
Toggle navigation
Menu
Open sidebar
Iris
Actris
Commits
595edcf5
Commit
595edcf5
authored
Jun 27, 2019
by
Robbert Krebbers
Browse files
Tweak.
parent
513d2cd7
Changes
1
Hide whitespace changes
Inline
Side-by-side
theories/examples/list_sort_instances.v
View file @
595edcf5
...
...
@@ -4,45 +4,42 @@ From iris.heap_lang Require Import proofmode notation.
From
osiris
.
utils
Require
Import
list
.
From
osiris
.
examples
Require
Import
list_sort
.
Definition
cmpZ
:
val
:
=
λ
:
"x"
"y"
,
"x"
≤
"y"
.
Section
list_sort_instances
.
Context
`
{!
heapG
Σ
,
!
proto_chanG
Σ
}
(
N
:
namespace
).
(* Example: Sort of integers *)
Definition
IZ
(
x
:
Z
)
(
v
:
val
)
:
iProp
Σ
:
=
⌜
∃
w
,
v
=
LitV
$
LitInt
w
∧
x
=
w
⌝
%
I
.
Definition
compareZ
:
val
:
=
λ
:
"x"
"y"
,
"x"
≤
"y"
.
Definition
IZ
(
x
:
Z
)
(
v
:
val
)
:
iProp
Σ
:
=
⌜
v
=
#
x
⌝
%
I
.
Lemma
c
o
mp
are
Z_spec
:
cmp_spec
IZ
(
≤
)
c
o
mp
are
Z
.
Lemma
cmpZ_spec
:
cmp_spec
IZ
(
≤
)
cmpZ
.
Proof
.
iIntros
(
x
x'
v
v'
Φ
)
"!>"
.
iIntros
([[
w
[->
->]]
[
w'
[->
->]]])
"HΦ"
.
wp_lam
.
wp_pures
.
iApply
"HΦ"
.
eauto
10
with
iFrame
.
rewrite
/
IZ
.
iIntros
(
x
x'
v
v'
Φ
[->
->])
"!> HΦ"
.
wp_lam
.
wp_pures
.
by
iApply
"HΦ"
.
Qed
.
Local
Arguments
val_encode
_
_
!
_
/.
Lemma
list_sort_client_le_spec
l
(
xs
:
list
Z
)
:
{{{
l
↦
val_encode
xs
}}}
list_sort_client
c
o
mp
are
Z
#
l
list_sort_client
cmpZ
#
l
{{{
ys
,
RET
#()
;
⌜
Sorted
(
≤
)
ys
⌝
∗
⌜
ys
≡
ₚ
xs
⌝
∗
l
↦
val_encode
ys
}}}.
Proof
.
assert
(
∀
zs
:
list
Z
,
val_encode
zs
=
val_encode
(
LitV
∘
LitInt
<$>
zs
))
as
Henc
.
{
intros
zs
.
induction
zs
;
f_equal
/=
;
auto
with
f_equal
.
}
iIntros
(
Φ
)
"Hl HΦ"
.
iApply
(
list_sort_client_spec
N
IZ
(
≤
)
_
_
(
LitV
∘
LitInt
<$>
xs
)
xs
with
"[] [Hl] [HΦ]"
).
{
iApply
c
o
mp
are
Z_spec
.
}
{
iApply
cmpZ_spec
.
}
{
rewrite
-
Henc
.
iFrame
"Hl"
.
iInduction
xs
as
[|
x
xs
]
"IH"
;
csimpl
;
first
by
iFrame
.
iFrame
"IH"
.
by
iExists
x
.
}
by
iFrame
"IH"
.
}
iIntros
"!>"
(
ys
ws
)
"(?&?&?&HI)"
.
iAssert
⌜
ws
=
(
LitV
∘
LitInt
)
<$>
ys
⌝
%
I
with
"[HI]"
as
%->.
{
iInduction
ys
as
[|
y
ys
]
"IH"
forall
(
ws
)
;
destruct
ws
as
[|
w
ws
]
;
csimpl
;
try
done
.
iDestruct
"HI"
as
"[
HI1
HI2]"
;
iDestruct
"HI1"
as
%(?&->&->)
.
iDestruct
"HI"
as
"[
->
HI2]"
.
by
iDestruct
(
"IH"
with
"HI2"
)
as
%->.
}
rewrite
-
Henc
.
iApply
(
"HΦ"
$!
ys
with
"[$]"
).
Qed
.
End
list_sort_instances
.
Write
Preview
Supports
Markdown
0%
Try again
or
attach a new 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