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
Rice Wine
Iris
Commits
7e19e1e7
Commit
7e19e1e7
authored
Jun 21, 2016
by
Jacques-Henri Jourdan
Browse files
Merge branch 'master' of gitlab.mpi-sws.org:FP/iris-coq
parents
119562b9
75db3853
Changes
1
Hide whitespace changes
Inline
Side-by-side
tests/tree_sum.v
0 → 100644
View file @
7e19e1e7
From
iris
.
proofmode
Require
Export
tactics
.
From
iris
.
heap_lang
Require
Import
proofmode
notation
.
Inductive
tree
:
=
|
leaf
:
Z
→
tree
|
node
:
tree
→
tree
→
tree
.
Fixpoint
is_tree
`
{!
heapG
Σ
}
(
v
:
val
)
(
t
:
tree
)
:
iPropG
heap_lang
Σ
:
=
match
t
with
|
leaf
n
=>
v
=
InjLV
#
n
|
node
tl
tr
=>
∃
(
ll
lr
:
loc
)
(
vl
vr
:
val
),
v
=
InjRV
(#
ll
,#
lr
)
★
ll
↦
vl
★
is_tree
vl
tl
★
lr
↦
vr
★
is_tree
vr
tr
end
%
I
.
Fixpoint
sum
(
t
:
tree
)
:
Z
:
=
match
t
with
|
leaf
n
=>
n
|
node
tl
tr
=>
sum
tl
+
sum
tr
end
.
Definition
sum_loop
:
val
:
=
rec
:
"sum_loop"
"t"
"l"
:
=
match
:
'
"t"
with
InjL
"n"
=>
'
"l"
<-
'
"n"
+
!
'
"l"
|
InjR
"tt"
=>
'
"sum_loop"
!(
Fst
'
"tt"
)
'
"l"
;;
'
"sum_loop"
!(
Snd
'
"tt"
)
'
"l"
end
.
Definition
sum'
:
val
:
=
λ
:
"t"
,
let
:
"l"
:
=
ref
#
0
in
^
sum_loop
'
"t"
'
"l"
;;
!
'
"l"
.
Global
Opaque
sum_loop
sum'
.
Lemma
sum_loop_wp
`
{!
heapG
Σ
}
heapN
v
t
l
(
n
:
Z
)
(
Φ
:
val
→
iPropG
heap_lang
Σ
)
:
heap_ctx
heapN
★
l
↦
#
n
★
is_tree
v
t
★
(
l
↦
#(
sum
t
+
n
)
-
★
is_tree
v
t
-
★
Φ
#())
⊢
WP
sum_loop
v
#
l
{{
Φ
}}.
Proof
.
iIntros
"(#Hh & Hl & Ht & HΦ)"
.
iL
ö
b
{
v
t
l
n
Φ
}
as
"IH"
.
wp_rec
.
wp_let
.
destruct
t
as
[
n'
|
tl
tr
]
;
simpl
in
*.
-
iDestruct
"Ht"
as
"%"
;
subst
.
wp_case
.
wp_let
.
wp_load
.
wp_op
.
wp_store
.
by
iApply
(
"HΦ"
with
"Hl"
).
-
iDestruct
"Ht"
as
{
ll
lr
vl
vr
}
"(% & Hll & Htl & Hlr & Htr)"
;
subst
.
wp_case
.
wp_let
.
wp_proj
.
wp_load
.
wp_apply
(
"IH"
with
"Hl Htl"
).
iIntros
"Hl Htl"
.
wp_seq
.
wp_proj
.
wp_load
.
wp_apply
(
"IH"
with
"Hl Htr"
).
iIntros
"Hl Htr"
.
iApply
(
"HΦ"
with
"[Hl]"
).
{
by
replace
(
sum
tl
+
sum
tr
+
n
)
with
(
sum
tr
+
(
sum
tl
+
n
))
by
omega
.
}
iExists
ll
,
lr
,
vl
,
vr
.
by
iFrame
.
Qed
.
Lemma
sum_wp
`
{!
heapG
Σ
}
heapN
v
t
Φ
:
heap_ctx
heapN
★
is_tree
v
t
★
(
is_tree
v
t
-
★
Φ
#(
sum
t
))
⊢
WP
sum'
v
{{
Φ
}}.
Proof
.
iIntros
"(#Hh & Ht & HΦ)"
.
rewrite
/
sum'
.
wp_let
.
wp_alloc
l
as
"Hl"
.
wp_let
.
wp_apply
sum_loop_wp
;
iFrame
"Hh Ht Hl"
.
rewrite
Z
.
add_0_r
.
iIntros
"Hl Ht"
.
wp_seq
.
wp_load
.
by
iApply
"HΦ"
.
Qed
.
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