ex_02_sumlist.v 6.28 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
(**
This exercise shows how to use representation predicates in Iris. We consider
some basic operations on linked lists. Although heap-lang is untyped, our
representation of lists intuitively corresponds to the following (rec-) type
in an ML-style language:

  list A := option (ref (A * list A))
*)
From iris.heap_lang Require Import proofmode notation.

(** A function that sums all elements of a list, defined as a heap-lang value: *)
Definition sum_list : val :=
  rec: "sum_list" "l" :=
    match: "l" with           (* A list is either... *)
      NONE => #0              (* ... the empty list *)
    | SOME "p" =>             (* ... or [SOME p], where [p] points to a pair ... *)
      let: "x" := Fst !"p" in (* ... whose first component is the head of the list *)
      let: "l" := Snd !"p" in (* ... and whose second component is the rest of the list. *)
      "x" + "sum_list" "l"
    end.

(** A function that increases all elements of a list in-place: *)
Definition inc_list : val :=
  rec: "inc_list" "n" "l" :=
    match: "l" with
      NONE => #()
    | SOME "p" =>
      let: "x" := Fst !"p" in
      let: "l" := Snd !"p" in
      "p" <- ("n" + "x", "l");;
      "inc_list" "n" "l"
    end.

(** The previous functions combined. *)
Definition sum_inc_list : val := λ: "n" "l",
  inc_list "n" "l";;
  sum_list "l".

(** A function that maps a function over all elements of a list: *)
Definition map_list : val :=
Ralf Jung's avatar
Ralf Jung committed
41
  rec: "map_list" "f" "l" :=
42 43 44 45 46 47
    match: "l" with
      NONE => #()
    | SOME "p" =>
      let: "x" := Fst !"p" in
      let: "l" := Snd !"p" in
      "p" <- ("f" "x", "l");;
Ralf Jung's avatar
Ralf Jung committed
48
      "map_list" "f" "l"
49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 158
    end.

Section proof.
Context `{!heapG Σ}.

(** Representation predicate in separation logic for a list of integers [l]: *)
Fixpoint is_list (l : list Z) (v : val) : iProp Σ :=
  match l with
  | [] =>  v = NONEV 
  | x :: l' =>  (p : loc),  v = SOMEV #p  
                  v' : val, p  (#x, v')  is_list l' v'
  end%I.

(**
In order to give a specification of [sum_list] we relate its result to the
sum defined as a pure Coq function.
*)
Definition sum_list_coq (l : list Z) : Z :=
  fold_right Z.add 0 l.

(**
The proof of the recursive function [sum_list] requires some form of recursion.
We can either do the induction over the list [l], or use the Löb induction
principle, given by the step-indexed nature of Iris. *)

(** The proof using induction over [l]: *)
Lemma sum_list_spec_induction l v :
  {{{ is_list l v }}} sum_list v {{{ RET #(sum_list_coq l); is_list l v }}}.
Proof.
  iIntros (Φ) "Hl Post".
  iInduction l as [|x l] "IH" forall (v Φ); simpl.
  (**
  Note that the option type is in fact encoded using sum types.
  Hence, [NONE] is syntactic sugar for [InjL #()] (or [InjLV #()]
  for values), and [SOME x] is syntactic sugar for [InjR x].
  *)
  - iDestruct "Hl" as %->.
    wp_rec.
    wp_match.
    iApply "Post". iPureIntro. reflexivity.
  - iDestruct "Hl" as (p) "[-> Hl]". iDestruct "Hl" as (v) "[Hp Hl]".
    wp_rec.
    wp_match.
    wp_load. wp_proj. wp_let.
    wp_load. wp_proj. wp_let.
    wp_apply ("IH" with "Hl"). iIntros "Hl". wp_op.
    iApply "Post".
    iExists p. iSplitR; [done|].
    iExists v. iSplitR "Hl"; [iApply "Hp"|iApply "Hl"].
Qed.

(** The proof using Löb induction. The parts which are in common with
[sum_list_spec_induction] are shortened using automation. *)
Lemma sum_list_spec_löb l v :
  {{{ is_list l v }}} sum_list v {{{ RET #(sum_list_coq l); is_list l v }}}.
Proof.
  iIntros (Φ) "Hl Post".
  iLöb as "IH" forall (l v Φ). destruct l as [|x l]; simpl; wp_rec.
  - iDestruct "Hl" as %->. wp_match. by iApply "Post".
  - iDestruct "Hl" as (p -> v) "[Hp Hl]". wp_match.
    do 2 (wp_load; wp_proj; wp_let).
    wp_apply ("IH" with "Hl"). iIntros "Hl". wp_op.
    iApply "Post". eauto with iFrame.
Qed.

(** *Exercise*: Do the proof of [inc_list] yourself. Use ordinary induction. *)
Lemma inc_list_spec_induction n l v :
  {{{ is_list l v }}}
    inc_list #n v
  {{{ RET #(); is_list (map (Z.add n) l) v }}}.
Proof.
  iIntros (Φ) "Hl Post".
  iInduction l as [|x l] "IH" forall (v Φ); simpl.
  - iDestruct "Hl" as %->.
    wp_rec. wp_let. wp_match.
    by iApply "Post".
  - iDestruct "Hl" as (p) "[-> Hl] /=". iDestruct "Hl" as (v) "[Hp Hl]".
    wp_rec. wp_let.
    wp_match.
    wp_load. wp_proj. wp_let.
    wp_load. wp_proj. wp_let.
    wp_op. wp_store.
    wp_apply ("IH" with "Hl"). iIntros "Hl".
    iApply "Post".
    iExists p. iSplitR; [done|].
    iExists v. iSplitR "Hl"; [iApply "Hp"|iApply "Hl"].
Qed.

(** *Exercise*: Now do the proof again using Löb induction. *)
Lemma inc_list_spec_löb n l v :
  {{{ is_list l v }}}
    inc_list #n v
  {{{ RET #(); is_list (map (Z.add n) l) v }}}.
Proof.
  iIntros (Φ) "Hl Post".
  iLöb as "IH" forall (l v Φ). destruct l as [|x l]; simpl; wp_rec; wp_let.
  - iDestruct "Hl" as %->. wp_match. by iApply "Post".
  - iDestruct "Hl" as (p -> v) "[Hp Hl] /=". wp_match.
    do 2 (wp_load; wp_proj; wp_let). wp_op. wp_store.
    wp_apply ("IH" with "Hl"). iIntros "Hl".
    iApply "Post". eauto with iFrame.
Qed.

(** *Exercise*: Do the proof of [sum_inc_list] by making use of the lemmas of
[sum_list] and [inc_list] we just proved. Make use of [wp_apply]. *)
Lemma sum_inc_list_spec n l v :
  {{{ is_list l v }}}
    sum_inc_list #n v
  {{{ RET #(sum_list_coq (map (Z.add n) l)); is_list (map (Z.add n) l) v }}}.
Proof.
159
  iIntros (Φ) "Hl Post". wp_lam. wp_let.
160 161 162 163 164 165 166 167 168 169 170 171 172 173 174 175 176 177 178 179 180 181
  wp_apply (inc_list_spec_induction with "Hl"); iIntros "Hl /="; wp_seq.
  wp_apply (sum_list_spec_induction with "Hl"); auto.
Qed.

(** *Optional exercise*: Prove the following spec of [map_list] which makes use
of a nested Texan triple, This spec is rather weak, as it requires [f] to be
pure, if you like, you can try to make it more general. *)
Lemma map_list_spec_induction (f : val) (f_coq : Z  Z) l v :
  ( n, {{{ True }}} f #n {{{ RET #(f_coq n); True }}}) -
  {{{ is_list l v }}} map_list f v {{{ RET #(); is_list (map f_coq l) v }}}.
Proof.
  iIntros "#Hf" (Φ) "!# Hl Post".
  iLöb as "IH" forall (l v Φ). destruct l as [|x l]; simpl; wp_rec; wp_let.
  - iDestruct "Hl" as %->. wp_match. by iApply "Post".
  - iDestruct "Hl" as (p -> v) "[Hp Hl] /=". wp_match.
    do 2 (wp_load; wp_proj; wp_let).
    wp_apply ("Hf" with "[//]"); iIntros "_ /=".
    wp_store.
    wp_apply ("IH" with "Hl"). iIntros "Hl".
    iApply "Post". eauto with iFrame.
Qed.
End proof.