tree_sum.v 2.05 KB
 Robbert Krebbers committed Aug 05, 2016 1 2 ``````From iris.program_logic Require Export weakestpre. From iris.heap_lang Require Export lang. `````` Robbert Krebbers committed Jun 20, 2016 3 4 ``````From iris.proofmode Require Export tactics. From iris.heap_lang Require Import proofmode notation. `````` Ralf Jung committed Jan 05, 2017 5 ``````Set Default Proof Using "Type". `````` Robbert Krebbers committed Jun 20, 2016 6 7 8 9 10 `````` Inductive tree := | leaf : Z → tree | node : tree → tree → tree. `````` Robbert Krebbers committed Aug 05, 2016 11 ``````Fixpoint is_tree `{!heapG Σ} (v : val) (t : tree) : iProp Σ := `````` Robbert Krebbers committed Jun 20, 2016 12 `````` match t with `````` Ralf Jung committed Nov 22, 2016 13 `````` | leaf n => ⌜v = InjLV #n⌝ `````` Robbert Krebbers committed Jun 20, 2016 14 15 `````` | node tl tr => ∃ (ll lr : loc) (vl vr : val), `````` Ralf Jung committed Nov 22, 2016 16 `````` ⌜v = InjRV (#ll,#lr)⌝ ∗ ll ↦ vl ∗ is_tree vl tl ∗ lr ↦ vr ∗ is_tree vr tr `````` Robbert Krebbers committed Jun 20, 2016 17 18 19 20 21 22 23 24 25 26 `````` 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 27 28 29 `````` 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 30 31 32 33 `````` end. Definition sum' : val := λ: "t", let: "l" := ref #0 in `````` Robbert Krebbers committed Jul 19, 2016 34 35 `````` sum_loop "t" "l";; !"l". `````` Robbert Krebbers committed Jun 20, 2016 36 `````` `````` Robbert Krebbers committed Aug 05, 2016 37 ``````Lemma sum_loop_wp `{!heapG Σ} v t l (n : Z) (Φ : val → iProp Σ) : `````` Robbert Krebbers committed Dec 09, 2016 38 39 `````` l ↦ #n -∗ is_tree v t -∗ (l ↦ #(sum t + n) -∗ is_tree v t -∗ Φ #()) -∗ WP sum_loop v #l {{ Φ }}. `````` Robbert Krebbers committed Jun 20, 2016 40 ``````Proof. `````` Robbert Krebbers committed Dec 09, 2016 41 `````` iIntros "Hl Ht HΦ". `````` Robbert Krebbers committed Sep 27, 2016 42 `````` iLöb as "IH" forall (v t l n Φ). 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 ``````Lemma sum_wp `{!heapG Σ} v t Φ : `````` Robbert Krebbers committed Dec 09, 2016 58 `````` is_tree v t -∗ (is_tree v t -∗ Φ #(sum t)) -∗ WP sum' v {{ Φ }}. `````` Robbert Krebbers committed Jun 20, 2016 59 ``````Proof. `````` Robbert Krebbers committed Dec 09, 2016 60 `````` iIntros "Ht HΦ". rewrite /sum' /=. `````` Robbert Krebbers committed Jun 20, 2016 61 `````` wp_let. wp_alloc l as "Hl". wp_let. `````` Robbert Krebbers committed Dec 09, 2016 62 `````` wp_apply (sum_loop_wp with "Hl Ht"). `````` Robbert Krebbers committed Jun 20, 2016 63 64 65 `````` rewrite Z.add_0_r. iIntros "Hl Ht". wp_seq. wp_load. by iApply "HΦ". Qed.``````