tree_sum.v 2.05 KB
Newer Older
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42
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Φ)".
43
  iLöb {v t l n Φ} as "IH". wp_rec; wp_let.
44 45
  destruct t as [n'|tl tr]; simpl in *.
  - iDestruct "Ht" as "%"; subst.
46
    wp_match. wp_load. wp_op. wp_store.
47 48
    by iApply ("HΦ" with "Hl").
  - iDestruct "Ht" as {ll lr vl vr} "(% & Hll & Htl & Hlr & Htr)"; subst.
49
    wp_match. wp_proj. wp_load.
50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67
    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.