Skip to content
Snippets Groups Projects
Commit bf42c065 authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Repair tree_sum test case and add to _CoqProject.

parent f96e229a
No related branches found
No related tags found
No related merge requests found
......@@ -106,6 +106,7 @@ tests/joining_existentials.v
tests/proofmode.v
tests/barrier_client.v
tests/list_reverse.v
tests/tree_sum.v
proofmode/coq_tactics.v
proofmode/pviewshifts.v
proofmode/environments.v
......
......@@ -21,16 +21,15 @@ Fixpoint sum (t : tree) : Z :=
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"
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".
sum_loop "t" "l";;
!"l".
Global Opaque sum_loop sum'.
......@@ -40,12 +39,12 @@ Lemma sum_loop_wp `{!heapG Σ} heapN v t l (n : Z) (Φ : val → iPropG heap_lan
WP sum_loop v #l {{ Φ }}.
Proof.
iIntros "(#Hh & Hl & Ht & HΦ)".
iLöb {v t l n Φ} as "IH". wp_rec; wp_let.
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_match. wp_load. wp_op. wp_store.
by iApply ("HΦ" with "Hl").
- iDestruct "Ht" as {ll lr vl vr} "(% & Hll & Htl & Hlr & Htr)"; subst.
- iDestruct "Ht" as (ll lr vl vr) "(% & Hll & Htl & Hlr & Htr)"; subst.
wp_match. wp_proj. wp_load.
wp_apply ("IH" with "Hl Htl"). iIntros "Hl Htl".
wp_seq. wp_proj. wp_load.
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment