llist.v 8.6 KB
Newer Older
1
2
(** This file defines an encoding of lists in the [heap_lang]
language, along with common functions such as append and split. *)
Robbert Krebbers's avatar
Robbert Krebbers committed
3
4
5
6
From iris.heap_lang Require Export proofmode notation.
From iris.heap_lang Require Import assert.

(** Immutable ML-style functional lists *)
Robbert Krebbers's avatar
Robbert Krebbers committed
7
8
9
Fixpoint llist `{heapG Σ} {A} (I : A  val  iProp Σ)
    (l : loc) (xs : list A) : iProp Σ :=
  match xs with
Robbert Krebbers's avatar
Robbert Krebbers committed
10
  | [] => l  NONEV
Robbert Krebbers's avatar
Robbert Krebbers committed
11
  | x :: xs =>  (v : val) (l' : loc), I x v  l  SOMEV (v,#l')  llist I l' xs
Robbert Krebbers's avatar
Robbert Krebbers committed
12
13
14
15
  end%I.
Arguments llist : simpl never.

Definition lnil : val := λ: <>, ref NONE.
Robbert Krebbers's avatar
Robbert Krebbers committed
16
Definition lcons : val := λ: "x" "l", "l" <- SOME ("x", ref (!"l")).
Robbert Krebbers's avatar
Robbert Krebbers committed
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
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

Definition lisnil : val := λ: "l",
  match: !"l" with
    SOME "p" => #false
  | NONE => #true
  end.

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

Definition lpop : val := λ: "l",
  match: !"l" with
    SOME "p" => "l" <- !(Snd "p");; Fst "p"
  | NONE => assert: #false
  end.

Definition llookup : val :=
  rec: "go" "l" "n" :=
    if: "n" = #0 then lhead "l" else
    match: !"l" with
      SOME "p" => "go" (Snd "p") ("n" - #1)
    | NONE => assert: #false
    end.

Definition llength : val :=
  rec: "go" "l" :=
    match: !"l" with
      NONE => #0
    | SOME "p" => #1 + "go" (Snd "p")
    end.

Definition lapp : val :=
  rec: "go" "l" "k" :=
    match: !"l" with
      NONE => "l" <- !"k"
    | SOME "p" => "go" (Snd "p") "k"
    end.
Definition lprep : val := λ: "l" "k",
  lapp "k" "l";; "l" <- !"k".

Definition lsnoc : val :=
  rec: "go" "l" "x" :=
    match: !"l" with
      NONE => "l" <- SOME ("x", ref NONE)
    | SOME "p" => "go" (Snd "p") "x"
    end.

Definition lsplit_at : val :=
  rec: "go" "l" "n" :=
    if: "n"  #0 then let: "k" := ref (! "l") in "l" <- NONE;; "k" else
    match: !"l" with
      NONE => ref NONE
    | SOME "p" => "go" (Snd "p") ("n" - #1)
    end.

Definition lsplit : val := λ: "l", lsplit_at "l" (llength "l" `quot` #2).

Section lists.
Robbert Krebbers's avatar
Robbert Krebbers committed
78
Context `{heapG Σ} {A} (I : A  val  iProp Σ).
Robbert Krebbers's avatar
Robbert Krebbers committed
79
Implicit Types i : nat.
Robbert Krebbers's avatar
Robbert Krebbers committed
80
81
82
Implicit Types xs : list A.
Implicit Types l : loc.
Local Arguments llist {_ _ _} _ _ !_ /.
Robbert Krebbers's avatar
Robbert Krebbers committed
83

84
85
86
87
88
89
90
91
92
Lemma llist_fmap {B} (J : B  val  iProp Σ) (f : A  B) l xs :
   ( x v, I x v - J (f x) v) -
  llist I l xs - llist J l (f <$> xs).
Proof.
  iIntros "#Hf Hll". iInduction xs as [|x xs] "IH" forall (l); csimpl; auto.
  iDestruct "Hll" as (v l') "(Hx & Hl & Hll)". iExists _, _. iFrame "Hl".
  iSplitL "Hx". by iApply "Hf". by iApply "IH".
Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
93
Lemma lnil_spec :
Robbert Krebbers's avatar
Robbert Krebbers committed
94
  {{{ True }}} lnil #() {{{ l, RET #l; llist I l [] }}}.
Robbert Krebbers's avatar
Robbert Krebbers committed
95
96
Proof. iIntros (Φ _) "HΦ". wp_lam. wp_alloc l. by iApply "HΦ". Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
97
98
Lemma lcons_spec l x xs v :
  {{{ llist I l xs  I x v }}} lcons v #l {{{ RET #(); llist I l (x :: xs) }}}.
Robbert Krebbers's avatar
Robbert Krebbers committed
99
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
100
  iIntros (Φ) "[Hll Hx] HΦ". wp_lam. destruct xs as [|x' xs]; simpl; wp_pures.
Robbert Krebbers's avatar
Robbert Krebbers committed
101
  - wp_load. wp_alloc k. wp_store. iApply "HΦ"; eauto with iFrame.
Robbert Krebbers's avatar
Robbert Krebbers committed
102
103
  - iDestruct "Hll" as (v' l') "(HIx' & Hl & Hll)".
    wp_load. wp_alloc k. wp_store. iApply "HΦ"; eauto 10 with iFrame.
Robbert Krebbers's avatar
Robbert Krebbers committed
104
105
Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
106
107
Lemma lisnil_spec l xs:
  {{{ llist I l xs }}}
Robbert Krebbers's avatar
Robbert Krebbers committed
108
    lisnil #l
Robbert Krebbers's avatar
Robbert Krebbers committed
109
  {{{ RET #(if xs is [] then true else false); llist I l xs }}}.
Robbert Krebbers's avatar
Robbert Krebbers committed
110
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
111
  iIntros (Φ) "Hll HΦ". wp_lam. destruct xs as [|x xs]; simpl; wp_pures.
Robbert Krebbers's avatar
Robbert Krebbers committed
112
  - wp_load; wp_pures. by iApply "HΦ".
Robbert Krebbers's avatar
Robbert Krebbers committed
113
  - iDestruct "Hll" as (v l') "(HIx & Hl & Hll)".
Robbert Krebbers's avatar
Robbert Krebbers committed
114
115
116
    wp_load; wp_pures. iApply "HΦ"; eauto with iFrame.
Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
117
118
119
120
121
(** Not the nicest spec, they leaks *)
Lemma lhead_spec_aux l x xs :
  {{{ llist I l (x :: xs) }}}
    lhead #l
  {{{ v (l' : loc), RET v; I x v  l  SOMEV (v,#l')  llist I l' xs }}}.
Robbert Krebbers's avatar
Robbert Krebbers committed
122
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
123
  iIntros (Φ) "/=". iDestruct 1 as (v l') "(HIx & Hl & Hll)". iIntros "HΦ".
Robbert Krebbers's avatar
Robbert Krebbers committed
124
125
  wp_lam. wp_load; wp_pures. iApply "HΦ"; eauto with iFrame.
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
126
127
Lemma lpop_spec_aux l l' v xs :
  {{{ l  SOMEV (v,#l')  llist I l' xs }}} lpop #l {{{ RET v; llist I l xs }}}.
Robbert Krebbers's avatar
Robbert Krebbers committed
128
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
129
130
  iIntros (Φ) "[Hl Hll] HΦ".
  wp_lam. wp_load. wp_pures. destruct xs as [|x' xs]; simpl; wp_pures.
Robbert Krebbers's avatar
Robbert Krebbers committed
131
  - wp_load. wp_store. wp_pures. iApply "HΦ"; eauto with iFrame.
Robbert Krebbers's avatar
Robbert Krebbers committed
132
  - iDestruct "Hll" as (v' l'') "(HIx' & Hl' & Hll)".
Robbert Krebbers's avatar
Robbert Krebbers committed
133
134
135
    wp_load. wp_store. wp_pures. iApply "HΦ"; eauto with iFrame.
Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
Lemma lhead_spec l x xs :
  {{{ llist I l (x :: xs) }}}
    lhead #l
  {{{ v, RET v; I x v  (I x v - llist I l (x :: xs)) }}}.
Proof.
  iIntros (Φ) "Hll HΦ". wp_apply (lhead_spec_aux with "Hll").
  iIntros (v l') "(HIx&?&?)". iApply "HΦ". iIntros "{$HIx} HIx".
  simpl; eauto with iFrame.
Qed.

Lemma lpop_spec l x xs :
  {{{ llist I l (x :: xs) }}} lpop #l {{{ v, RET v; I x v  llist I l xs }}}.
Proof.
  iIntros (Φ) "/=". iDestruct 1 as (v l') "(HIx & Hl & Hll)". iIntros "HΦ".
  wp_apply (lpop_spec_aux with "[$]"); iIntros "Hll". iApply "HΦ"; iFrame.
Qed.

Lemma llookup_spec l i xs x :
  xs !! i = Some x 
  {{{ llist I l xs }}}
    llookup #l #i
  {{{ v, RET v; I x v  (I x v - llist I l xs) }}}.
Robbert Krebbers's avatar
Robbert Krebbers committed
158
159
Proof.
  iIntros (Hi Φ) "Hll HΦ".
Robbert Krebbers's avatar
Robbert Krebbers committed
160
  iInduction xs as [|x' xs] "IH" forall (l i x Hi Φ); [done|simpl; wp_rec; wp_pures].
Robbert Krebbers's avatar
Robbert Krebbers committed
161
  destruct i as [|i]; simplify_eq/=; wp_pures.
Robbert Krebbers's avatar
Robbert Krebbers committed
162
163
164
  - wp_apply (lhead_spec with "Hll"); iIntros (v) "[HI Hll]".
    iApply "HΦ"; eauto with iFrame.
  - iDestruct "Hll" as (v l') "(HIx' & Hl' & Hll)". wp_load; wp_pures.
Robbert Krebbers's avatar
Robbert Krebbers committed
165
    rewrite Nat2Z.inj_succ Z.sub_1_r Z.pred_succ.
Robbert Krebbers's avatar
Robbert Krebbers committed
166
167
    wp_apply ("IH" with "[//] Hll"); iIntros (v') "[HIx Hll]".
    iApply "HΦ". iIntros "{$HIx} HIx". iExists v, l'. iFrame. by iApply "Hll".
Robbert Krebbers's avatar
Robbert Krebbers committed
168
169
Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
170
171
Lemma llength_spec l xs :
  {{{ llist I l xs }}} llength #l {{{ RET #(length xs); llist I l xs }}}.
Robbert Krebbers's avatar
Robbert Krebbers committed
172
173
Proof.
  iIntros (Φ) "Hll HΦ".
Robbert Krebbers's avatar
Robbert Krebbers committed
174
  iInduction xs as [|x xs] "IH" forall (l Φ); simpl; wp_rec; wp_pures.
Robbert Krebbers's avatar
Robbert Krebbers committed
175
  - wp_load; wp_pures. by iApply "HΦ".
Robbert Krebbers's avatar
Robbert Krebbers committed
176
  - iDestruct "Hll" as (v l') "(HIx & Hl' & Hll)". wp_load; wp_pures.
Robbert Krebbers's avatar
Robbert Krebbers committed
177
178
179
180
    wp_apply ("IH" with "Hll"); iIntros "Hll". wp_pures.
    rewrite (Nat2Z.inj_add 1). iApply "HΦ"; eauto with iFrame.
Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
181
182
Lemma lapp_spec l1 l2 xs1 xs2 :
  {{{ llist I l1 xs1  llist I l2 xs2 }}}
Robbert Krebbers's avatar
Robbert Krebbers committed
183
    lapp #l1 #l2
Robbert Krebbers's avatar
Robbert Krebbers committed
184
  {{{ RET #(); llist I l1 (xs1 ++ xs2)  l2  - }}}.
Robbert Krebbers's avatar
Robbert Krebbers committed
185
186
Proof.
  iIntros (Φ) "[Hll1 Hll2] HΦ".
Robbert Krebbers's avatar
Robbert Krebbers committed
187
188
  iInduction xs1 as [|x1 xs1] "IH" forall (l1 Φ); simpl; wp_rec; wp_pures.
  - wp_load. wp_pures. destruct xs2 as [|x2 xs2]; simpl; wp_pures.
Robbert Krebbers's avatar
Robbert Krebbers committed
189
    + wp_load. wp_store. iApply "HΦ". eauto with iFrame.
Robbert Krebbers's avatar
Robbert Krebbers committed
190
    + iDestruct "Hll2" as (v2 l2') "(HIx2 & Hl2 & Hll2)". wp_load. wp_store.
Robbert Krebbers's avatar
Robbert Krebbers committed
191
      iApply "HΦ". iSplitR "Hl2"; eauto 10 with iFrame.
Robbert Krebbers's avatar
Robbert Krebbers committed
192
  - iDestruct "Hll1" as (v1 l') "(HIx1 & Hl1 & Hll1)". wp_load; wp_pures.
Robbert Krebbers's avatar
Robbert Krebbers committed
193
194
195
196
    wp_apply ("IH" with "Hll1 Hll2"); iIntros "[Hll Hl2]".
    iApply "HΦ"; eauto with iFrame.
Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
197
198
Lemma lprep_spec l1 l2 xs1 xs2 :
  {{{ llist I l1 xs2  llist I l2 xs1 }}}
Robbert Krebbers's avatar
Robbert Krebbers committed
199
    lprep #l1 #l2
Robbert Krebbers's avatar
Robbert Krebbers committed
200
  {{{ RET #(); llist I l1 (xs1 ++ xs2)  l2  - }}}.
Robbert Krebbers's avatar
Robbert Krebbers committed
201
202
203
Proof.
  iIntros (Φ) "[Hll1 Hll2] HΦ". wp_lam.
  wp_apply (lapp_spec with "[$Hll2 $Hll1]"); iIntros "[Hll2 Hl1]".
Robbert Krebbers's avatar
Robbert Krebbers committed
204
  iDestruct "Hl1" as (w) "Hl1". destruct (xs1 ++ xs2) as [|x xs]; simpl; wp_pures.
Robbert Krebbers's avatar
Robbert Krebbers committed
205
  - wp_load. wp_store. iApply "HΦ"; eauto with iFrame.
Robbert Krebbers's avatar
Robbert Krebbers committed
206
  - iDestruct "Hll2" as (v l') "(HIx & Hl2 & Hll2)". wp_load. wp_store.
Robbert Krebbers's avatar
Robbert Krebbers committed
207
208
209
    iApply "HΦ"; iSplitR "Hl2"; eauto with iFrame.
Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
210
211
Lemma lsnoc_spec l xs x v :
  {{{ llist I l xs  I x v }}} lsnoc #l v {{{ RET #(); llist I l (xs ++ [x]) }}}.
Robbert Krebbers's avatar
Robbert Krebbers committed
212
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
213
214
  iIntros (Φ) "[Hll HIx] HΦ".
  iInduction xs as [|x' xs] "IH" forall (l Φ); simpl; wp_rec; wp_pures.
Robbert Krebbers's avatar
Robbert Krebbers committed
215
  - wp_load. wp_alloc k. wp_store. iApply "HΦ"; eauto with iFrame.
Robbert Krebbers's avatar
Robbert Krebbers committed
216
217
  - iDestruct "Hll" as (v' l') "(HIx' & Hl & Hll)". wp_load; wp_pures.
    wp_apply ("IH" with "Hll HIx"); iIntros "Hll". iApply "HΦ"; eauto with iFrame.
Robbert Krebbers's avatar
Robbert Krebbers committed
218
219
Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
220
221
Lemma lsplit_at_spec l xs (n : nat) :
  {{{ llist I l xs }}}
Robbert Krebbers's avatar
Robbert Krebbers committed
222
    lsplit_at #l #n
Robbert Krebbers's avatar
Robbert Krebbers committed
223
  {{{ k, RET #k; llist I l (take n xs)  llist I k (drop n xs) }}}.
Robbert Krebbers's avatar
Robbert Krebbers committed
224
225
Proof.
  iIntros (Φ) "Hll HΦ".
Robbert Krebbers's avatar
Robbert Krebbers committed
226
  iInduction xs as [|x xs] "IH" forall (l n Φ); simpl; wp_rec; wp_pures.
Robbert Krebbers's avatar
Robbert Krebbers committed
227
228
229
  - destruct n as [|n]; simpl; wp_pures.
    + wp_load. wp_alloc k. wp_store. iApply "HΦ"; iFrame.
    + wp_load. wp_alloc k. iApply "HΦ"; iFrame.
Robbert Krebbers's avatar
Robbert Krebbers committed
230
  - iDestruct "Hll" as (v l') "(HIx & Hl & Hll)". destruct n as [|n]; simpl; wp_pures.
Robbert Krebbers's avatar
Robbert Krebbers committed
231
232
233
234
235
236
    + wp_load. wp_alloc k. wp_store. iApply "HΦ"; eauto with iFrame.
    + wp_load; wp_pures. rewrite Nat2Z.inj_succ Z.sub_1_r Z.pred_succ.
      wp_apply ("IH" with "[$]"); iIntros (k) "[Hll Hlk]".
      iApply "HΦ"; eauto with iFrame.
Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
237
238
Lemma lsplit_spec l xs :
  {{{ llist I l xs }}}
Robbert Krebbers's avatar
Robbert Krebbers committed
239
    lsplit #l
Robbert Krebbers's avatar
Robbert Krebbers committed
240
  {{{ k xs1 xs2, RET #k;  xs = xs1 ++ xs2   llist I l xs1  llist I k xs2 }}}.
Robbert Krebbers's avatar
Robbert Krebbers committed
241
242
243
244
245
246
247
248
Proof.
  iIntros (Φ) "Hl HΦ". wp_lam.
  wp_apply (llength_spec with "Hl"); iIntros "Hl". wp_pures.
  rewrite Z.quot_div_nonneg; [|lia..]. rewrite -(Z2Nat_inj_div _ 2).
  wp_apply (lsplit_at_spec with "Hl"); iIntros (k) "[Hl Hk]".
  iApply "HΦ". iFrame. by rewrite take_drop.
Qed.
End lists.