tree_sum.v 2.01 KB
 Robbert Krebbers committed Jun 20, 2016 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 ``````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" := `````` Robbert Krebbers committed Jul 19, 2016 24 25 26 `````` match: "t" with InjL "n" => "l" <- "n" + !"l" | InjR "tt" => "sum_loop" !(Fst "tt") "l" ;; "sum_loop" !(Snd "tt") "l" `````` Robbert Krebbers committed Jun 20, 2016 27 28 29 30 `````` end. Definition sum' : val := λ: "t", let: "l" := ref #0 in `````` Robbert Krebbers committed Jul 19, 2016 31 32 `````` sum_loop "t" "l";; !"l". `````` Robbert Krebbers committed Jun 20, 2016 33 34 35 `````` Global Opaque sum_loop sum'. `````` Robbert Krebbers committed Jul 19, 2016 36 37 ``````Lemma sum_loop_wp `{!heapG Σ} v t l (n : Z) (Φ : val → iPropG heap_lang Σ) : heap_ctx ★ l ↦ #n ★ is_tree v t `````` Robbert Krebbers committed Jun 20, 2016 38 39 40 41 `````` ★ (l ↦ #(sum t + n) -★ is_tree v t -★ Φ #()) ⊢ WP sum_loop v #l {{ Φ }}. Proof. iIntros "(#Hh & Hl & Ht & HΦ)". `````` Robbert Krebbers committed Jul 19, 2016 42 `````` iLöb (v t l n Φ) as "IH". wp_rec. wp_let. `````` Robbert Krebbers committed Jun 20, 2016 43 44 `````` destruct t as [n'|tl tr]; simpl in *. - iDestruct "Ht" as "%"; subst. `````` Robbert Krebbers committed Jun 23, 2016 45 `````` wp_match. wp_load. wp_op. wp_store. `````` Robbert Krebbers committed Jun 20, 2016 46 `````` by iApply ("HΦ" with "Hl"). `````` Robbert Krebbers committed Jul 19, 2016 47 `````` - iDestruct "Ht" as (ll lr vl vr) "(% & Hll & Htl & Hlr & Htr)"; subst. `````` Robbert Krebbers committed Jun 23, 2016 48 `````` wp_match. wp_proj. wp_load. `````` Robbert Krebbers committed Jun 20, 2016 49 50 51 52 53 54 55 56 `````` 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. `````` Robbert Krebbers committed Jul 19, 2016 57 58 ``````Lemma sum_wp `{!heapG Σ} v t Φ : heap_ctx ★ is_tree v t ★ (is_tree v t -★ Φ #(sum t)) `````` Robbert Krebbers committed Jun 20, 2016 59 60 61 62 63 64 65 66 `````` ⊢ 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.``````