list.v 4.86 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 43 44 45 46 47 48 49 50
From iris.heap_lang Require Export proofmode notation.
From iris.heap_lang Require Import assert.

(** Immutable ML-style functional lists *)
Fixpoint is_list (hd : val) (xs : list val) : Prop :=
  match xs with
  | [] => hd = NONEV
  | x :: xs =>  hd', hd = SOMEV (x,hd')  is_list hd' xs
  end.

Definition lnil : val := λ: <>, NONEV.
Definition lcons : val := λ: "x" "l", SOME ("x", "l").

Definition lhead : val := λ: "l",
  match: "l" with
    SOME "p" => Fst "p"
  | NONE => assert: #false
  end.
Definition ltail : val := λ: "l",
  match: "l" with
    SOME "p" => Snd "p"
  | NONE => assert: #false
  end.

Definition llookup : val :=
  rec: "go" "n" "l" :=
    if: "n" = #0 then lhead "l" else
    let: "l" := ltail "l" in "go" ("n" - #1) "l".

Definition linsert : val :=
  rec: "go" "n" "x" "l" :=
    if: "n" = #0 then let: "l" := ltail "l" in lcons "x" "l" else
    let: "k" := ltail "l" in
    let: "k" := "go" ("n" - #1) "x" "k" in
    lcons (lhead "l") "k".

Definition lreplicate : val :=
  rec: "go" "n" "x" :=
    if: "n" = #0 then lnil #() else
    let: "l" := "go" ("n" - #1) "x" in lcons "x" "l".

Definition llist_member : val :=
  rec: "go" "x" "l" :=
    match: "l" with
      NONE => #false
    | SOME "p" =>
      if: Fst "p" = "x" then #true
      else let: "l" := (Snd "p")  in "go" "x" "l"
    end.

Robbert Krebbers's avatar
Robbert Krebbers committed
51 52 53 54 55 56 57
Definition llength : val :=
  rec: "go" "l" :=
    match: "l" with
      NONE => #0
    | SOME "p" => #1 + "go" (Snd "p")
    end.

58 59 60 61 62 63 64 65 66 67
Section lists.
Context `{heapG Σ}.
Implicit Types i : nat.
Implicit Types v : val.

Lemma lnil_spec : {{{ True }}} lnil #() {{{ hd, RET hd;  is_list hd []  }}}.
Proof. iIntros (Φ _) "HΦ". wp_lam. by iApply "HΦ". Qed.

Lemma lcons_spec hd vs v :
  {{{  is_list hd vs  }}} lcons v hd {{{ hd', RET hd';  is_list hd' (v :: vs)  }}}.
68 69 70 71
Proof.
  iIntros (Φ ?) "HΦ". wp_lam. wp_pures.
  iApply "HΦ". simpl; eauto.
Qed.
72 73 74

Lemma lhead_spec hd vs v :
  {{{  is_list hd (v :: vs)  }}} lhead hd {{{ RET v; True }}}.
75
Proof. iIntros (Φ (hd'&->&?)) "HΦ". wp_lam. wp_pures. by iApply "HΦ". Qed.
76 77 78

Lemma ltail_spec hd vs v :
  {{{  is_list hd (v :: vs)  }}} ltail hd {{{ hd', RET hd';  is_list hd' vs  }}}.
79
Proof. iIntros (Φ (hd'&->&?)) "HΦ". wp_lam. wp_pures. by iApply "HΦ". Qed.
80

Robbert Krebbers's avatar
Robbert Krebbers committed
81
Lemma llookup_spec i hd vs v :
82 83 84 85 86
  vs !! i = Some v 
  {{{  is_list hd vs  }}} llookup #i hd {{{ RET v; True }}}.
Proof.
  iIntros (Hi Φ Hl) "HΦ".
  iInduction vs as [|v' vs] "IH" forall (hd i Hi Hl); destruct i as [|i]=> //; simplify_eq/=.
87 88
  { wp_lam. wp_pures. by iApply (lhead_spec with "[//]"). }
  wp_lam. wp_pures.
89 90 91 92
  wp_apply (ltail_spec with "[//]"); iIntros (hd' ?). wp_let.
  wp_op. rewrite Nat2Z.inj_succ -Z.add_1_l Z.add_simpl_l. by iApply "IH".
Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
93
Lemma linsert_spec i hd vs v :
94 95 96 97 98
  is_Some (vs !! i) 
  {{{  is_list hd vs  }}} linsert #i v hd {{{ hd', RET hd';  is_list hd' (<[i:=v]> vs)  }}}.
Proof.
  iIntros ([w Hi] Φ Hl) "HΦ".
  iInduction vs as [|v' vs] "IH" forall (hd i Hi Hl Φ); destruct i as [|i]=> //; simplify_eq/=.
99
  { wp_lam. wp_pures. wp_apply (ltail_spec with "[//]"). iIntros (hd' ?).
100
    wp_let. by iApply (lcons_spec with "[//]"). }
101
  wp_lam; wp_pures.
102 103 104 105 106 107 108 109 110 111 112 113
  wp_apply (ltail_spec with "[//]"); iIntros (hd' ?). wp_let.
  wp_op. rewrite Nat2Z.inj_succ -Z.add_1_l Z.add_simpl_l.
  wp_apply ("IH" with "[//] [//]"). iIntros (hd'' ?). wp_let.
  wp_apply (lhead_spec with "[//]"); iIntros "_".
  by wp_apply (lcons_spec with "[//]").
Qed.

Lemma llist_member_spec hd vs v :
  {{{  is_list hd vs  }}} llist_member v hd {{{ RET #(bool_decide (v  vs)); True }}}.
Proof.
  iIntros (Φ Hl) "HΦ".
  iInduction vs as [|v' vs] "IH" forall (hd Hl); simplify_eq/=.
114 115 116
  { wp_lam; wp_pures. by iApply "HΦ". }
  destruct Hl as (hd'&->&?). wp_lam; wp_pures.
  destruct (bool_decide_reflect (v' = v)) as [->|?]; wp_if.
117 118 119 120 121 122 123 124 125 126
  { rewrite (bool_decide_true (_  _ :: _)); last by left. by iApply "HΦ". }
  wp_proj. wp_let. iApply ("IH" with "[//]"). destruct (bool_decide_reflect (v  vs)).
  - by rewrite bool_decide_true; last by right.
  - by rewrite bool_decide_false ?elem_of_cons; last naive_solver.
Qed.

Lemma lreplicate_spec i v :
  {{{ True }}} lreplicate #i v {{{ hd, RET hd;  is_list hd (replicate i v)  }}}.
Proof.
  iIntros (Φ _) "HΦ". iInduction i as [|i] "IH" forall (Φ); simpl.
127
  { wp_lam; wp_pures.
128
    iApply (lnil_spec with "[//]"). iApply "HΦ". }
129 130
  wp_lam; wp_pures.
  rewrite Nat2Z.inj_succ -Z.add_1_l Z.add_simpl_l.
131 132
  wp_apply "IH"; iIntros (hd' Hl). wp_let. by iApply (lcons_spec with "[//]").
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
133 134 135 136 137 138 139 140 141 142 143

Lemma llength_spec hd vs :
  {{{  is_list hd vs  }}} llength hd {{{ RET #(length vs); True }}}.
Proof.
  iIntros (Φ Hl) "HΦ".
  iInduction vs as [|v' vs] "IH" forall (hd Hl Φ); simplify_eq/=.
  { wp_lam. wp_match. by iApply "HΦ". }
  destruct Hl as (hd'&->&?). wp_lam. wp_match. wp_proj.
  wp_apply ("IH" $! hd' with "[//]"); iIntros "_ /=". wp_op.
  rewrite (Nat2Z.inj_add 1). by iApply "HΦ".
Qed.
144
End lists.