tree_sum.v 1.95 KB
 Jacques-Henri Jourdan committed Sep 13, 2019 1 ``````From iris.proofmode Require Export tactics. `````` Robbert Krebbers committed Jan 13, 2018 2 ``````From iris.program_logic Require Export weakestpre total_weakestpre. `````` Robbert Krebbers committed Aug 05, 2016 3 ``````From iris.heap_lang Require Export lang. `````` Robbert Krebbers committed Jun 20, 2016 4 ``````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 Jul 12, 2017 37 ``````Lemma sum_loop_wp `{!heapG Σ} v t l (n : Z) : `````` Robbert Krebbers committed Jan 13, 2018 38 `````` [[{ l ↦ #n ∗ is_tree v t }]] `````` Robbert Krebbers committed Jul 12, 2017 39 `````` sum_loop v #l `````` Robbert Krebbers committed Jan 13, 2018 40 `````` [[{ RET #(); l ↦ #(sum t + n) ∗ is_tree v t }]]. `````` Robbert Krebbers committed Jun 20, 2016 41 ``````Proof. `````` Robbert Krebbers committed Jul 12, 2017 42 `````` iIntros (Φ) "[Hl Ht] HΦ". `````` 43 `````` iInduction t as [n'|tl ? tr] "IH" forall (v l n Φ); simpl; wp_rec; wp_let. `````` Robbert Krebbers committed Jun 20, 2016 44 `````` - iDestruct "Ht" as "%"; subst. `````` Jacques-Henri Jourdan committed Oct 29, 2018 45 `````` wp_load. wp_store. `````` Robbert Krebbers committed Jul 12, 2017 46 `````` by iApply ("HΦ" with "[\$Hl]"). `````` Robbert Krebbers committed Oct 25, 2017 47 `````` - iDestruct "Ht" as (ll lr vl vr ->) "(Hll & Htl & Hlr & Htr)". `````` Jacques-Henri Jourdan committed Oct 29, 2018 48 49 `````` wp_load. wp_apply ("IH" with "Hl Htl"). iIntros "[Hl Htl]". wp_load. wp_apply ("IH1" with "Hl Htr"). iIntros "[Hl Htr]". `````` Robbert Krebbers committed Jul 12, 2017 50 `````` iApply "HΦ". iSplitL "Hl". `````` Robbert Krebbers committed Jun 20, 2016 51 52 53 54 `````` { 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 12, 2017 55 ``````Lemma sum_wp `{!heapG Σ} v t : `````` Robbert Krebbers committed Jan 13, 2018 56 `````` [[{ is_tree v t }]] sum' v [[{ RET #(sum t); is_tree v t }]]. `````` Robbert Krebbers committed Jun 20, 2016 57 ``````Proof. `````` Robbert Krebbers committed Jul 12, 2017 58 `````` iIntros (Φ) "Ht HΦ". rewrite /sum' /=. `````` Jacques-Henri Jourdan committed Oct 29, 2018 59 `````` wp_lam. wp_alloc l as "Hl". `````` Robbert Krebbers committed Jul 12, 2017 60 `````` wp_apply (sum_loop_wp with "[\$Hl \$Ht]"). `````` Robbert Krebbers committed Jun 20, 2016 61 `````` rewrite Z.add_0_r. `````` Jacques-Henri Jourdan committed Oct 29, 2018 62 `````` iIntros "[Hl Ht]". wp_load. by iApply "HΦ". `````` Robbert Krebbers committed Jun 20, 2016 63 ``Qed.``