tree_sum.v 1.95 KB
Newer Older
1
From iris.program_logic Require Export weakestpre total_weakestpre.
2
From iris.heap_lang Require Export lang.
3 4
From iris.proofmode Require Export tactics.
From iris.heap_lang Require Import proofmode notation.
5
Set Default Proof Using "Type".
6 7 8 9 10

Inductive tree :=
  | leaf : Z  tree
  | node : tree  tree  tree.

11
Fixpoint is_tree `{!heapG Σ} (v : val) (t : tree) : iProp Σ :=
12
  match t with
Ralf Jung's avatar
Ralf Jung committed
13
  | leaf n => v = InjLV #n
14 15
  | node tl tr =>
      (ll lr : loc) (vl vr : val),
Ralf Jung's avatar
Ralf Jung committed
16
       v = InjRV (#ll,#lr)  ll  vl  is_tree vl tl  lr  vr  is_tree vr tr
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" :=
27 28 29
    match: "t" with
      InjL "n" => "l" <- "n" + !"l"
    | InjR "tt" => "sum_loop" !(Fst "tt") "l" ;; "sum_loop" !(Snd "tt") "l"
30 31 32 33
    end.

Definition sum' : val := λ: "t",
  let: "l" := ref #0 in
34 35
  sum_loop "t" "l";;
  !"l".
36

37
Lemma sum_loop_wp `{!heapG Σ} v t l (n : Z) :
38
  [[{ l  #n  is_tree v t }]]
39
    sum_loop v #l
40
  [[{ RET #(); l  #(sum t + n)  is_tree v t }]].
41
Proof.
42
  iIntros (Φ) "[Hl Ht] HΦ".
43
  iInduction t as [n'|tl ? tr] "IH" forall (v l n Φ); simpl; wp_rec; wp_let.
44
  - iDestruct "Ht" as "%"; subst.
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
45
    wp_load. wp_store.
46
    by iApply ("HΦ" with "[$Hl]").
47
  - iDestruct "Ht" as (ll lr vl vr ->) "(Hll & Htl & Hlr & Htr)".
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
48 49
    wp_load. wp_apply ("IH" with "Hl Htl"). iIntros "[Hl Htl]".
    wp_load. wp_apply ("IH1" with "Hl Htr"). iIntros "[Hl Htr]".
50
    iApply "HΦ". iSplitL "Hl".
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.

55
Lemma sum_wp `{!heapG Σ} v t :
56
  [[{ is_tree v t }]] sum' v [[{ RET #(sum t); is_tree v t }]].
57
Proof.
58
  iIntros (Φ) "Ht HΦ". rewrite /sum' /=.
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
59
  wp_lam. wp_alloc l as "Hl".
60
  wp_apply (sum_loop_wp with "[$Hl $Ht]").
61
  rewrite Z.add_0_r.
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
62
  iIntros "[Hl Ht]". wp_load. by iApply "HΦ".
63
Qed.