natmap.v 15.3 KB
Newer Older
Robbert Krebbers's avatar
Robbert Krebbers committed
1
(* Copyright (c) 2012-2015, Robbert Krebbers. *)
2
(* This file is distributed under the terms of the BSD license. *)
3
4
5
(** This files implements a type [natmap A] of finite maps whose keys range
over Coq's data type of unary natural numbers [nat]. The implementation equips
a list with a proof of canonicity. *)
6
Require Import prelude.fin_maps prelude.mapset.
7
8
9

Notation natmap_raw A := (list (option A)).
Definition natmap_wf {A} (l : natmap_raw A) :=
10
  match last l with None => True | Some x => is_Some x end.
11
12
13
Instance natmap_wf_pi {A} (l : natmap_raw A) : ProofIrrel (natmap_wf l).
Proof. unfold natmap_wf. case_match; apply _. Qed.

14
Lemma natmap_wf_inv {A} (o : option A) (l : natmap_raw A) :
15
16
17
18
19
  natmap_wf (o :: l)  natmap_wf l.
Proof. by destruct l. Qed.
Lemma natmap_wf_lookup {A} (l : natmap_raw A) :
  natmap_wf l  l  []   i x, mjoin (l !! i) = Some x.
Proof.
20
  intros Hwf Hl. induction l as [|[x|] l IH]; simpl; [done| |].
21
  { exists 0. simpl. eauto. }
22
  destruct IH as (i&x&?); eauto using natmap_wf_inv; [|by exists (S i), x].
23
  intros ->. by destruct Hwf.
24
25
Qed.

26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
Record natmap (A : Type) : Type := NatMap {
  natmap_car : natmap_raw A;
  natmap_prf : natmap_wf natmap_car
}.
Arguments NatMap {_} _ _.
Arguments natmap_car {_} _.
Arguments natmap_prf {_} _.
Lemma natmap_eq {A} (m1 m2 : natmap A) :
  m1 = m2  natmap_car m1 = natmap_car m2.
Proof.
  split; [by intros ->|intros]; destruct m1 as [t1 ?], m2 as [t2 ?].
  simplify_equality'; f_equal; apply proof_irrel.
Qed.
Global Instance natmap_eq_dec `{ x y : A, Decision (x = y)}
    (m1 m2 : natmap A) : Decision (m1 = m2) :=
  match decide (natmap_car m1 = natmap_car m2) with
  | left H => left (proj2 (natmap_eq m1 m2) H)
  | right H => right (H  proj1 (natmap_eq m1 m2))
  end.
45

46
47
48
Instance natmap_empty {A} : Empty (natmap A) := NatMap [] I.
Instance natmap_lookup {A} : Lookup nat A (natmap A) := λ i m,
  let (l,_) := m in mjoin (l !! i).
49
50

Fixpoint natmap_singleton_raw {A} (i : nat) (x : A) : natmap_raw A :=
51
  match i with 0 => [Some x]| S i => None :: natmap_singleton_raw i x end.
52
53
Lemma natmap_singleton_wf {A} (i : nat) (x : A) :
  natmap_wf (natmap_singleton_raw i x).
54
Proof. unfold natmap_wf. induction i as [|[]]; simplify_equality'; eauto. Qed.
55
56
57
58
59
60
61
62
63
Lemma natmap_lookup_singleton_raw {A} (i : nat) (x : A) :
  mjoin (natmap_singleton_raw i x !! i) = Some x.
Proof. induction i; simpl; auto. Qed.
Lemma natmap_lookup_singleton_raw_ne {A} (i j : nat) (x : A) :
  i  j  mjoin (natmap_singleton_raw i x !! j) = None.
Proof. revert j; induction i; intros [|?]; simpl; auto with congruence. Qed.
Hint Rewrite @natmap_lookup_singleton_raw : natmap.

Definition natmap_cons_canon {A} (o : option A) (l : natmap_raw A) :=
64
  match o, l with None, [] => [] | _, _ => o :: l end.
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
Lemma natmap_cons_canon_wf {A} (o : option A) (l : natmap_raw A) :
  natmap_wf l  natmap_wf (natmap_cons_canon o l).
Proof. unfold natmap_wf, last. destruct o, l; simpl; eauto. Qed.
Lemma natmap_cons_canon_O {A} (o : option A) (l : natmap_raw A) :
  mjoin (natmap_cons_canon o l !! 0) = o.
Proof. by destruct o, l. Qed.
Lemma natmap_cons_canon_S {A} (o : option A) (l : natmap_raw A) i :
  natmap_cons_canon o l !! S i = l !! i.
Proof. by destruct o, l. Qed.
Hint Rewrite @natmap_cons_canon_O @natmap_cons_canon_S : natmap.

Definition natmap_alter_raw {A} (f : option A  option A) :
    nat  natmap_raw A  natmap_raw A :=
  fix go i l {struct l} :=
  match l with
  | [] =>
     match f None with
82
     | Some x => natmap_singleton_raw i x | None => []
83
84
85
     end
  | o :: l =>
     match i with
86
     | 0 => natmap_cons_canon (f o) l | S i => natmap_cons_canon o (go i l)
87
88
89
90
91
92
93
94
95
     end
  end.
Lemma natmap_alter_wf {A} (f : option A  option A) i l :
  natmap_wf l  natmap_wf (natmap_alter_raw f i l).
Proof.
  revert i. induction l; [intro | intros [|?]]; simpl; repeat case_match;
    eauto using natmap_singleton_wf, natmap_cons_canon_wf, natmap_wf_inv.
Qed.
Instance natmap_alter {A} : PartialAlter nat A (natmap A) := λ f i m,
96
  let (l,Hl) := m in NatMap _ (natmap_alter_wf f i l Hl).
97
98
99
100
101
102
103
104
105
106
107
108
109
110
Lemma natmap_lookup_alter_raw {A} (f : option A  option A) i l :
  mjoin (natmap_alter_raw f i l !! i) = f (mjoin (l !! i)).
Proof.
  revert i. induction l; intros [|?]; simpl; repeat case_match; simpl;
    autorewrite with natmap; auto.
Qed.
Lemma natmap_lookup_alter_raw_ne {A} (f : option A  option A) i j l :
  i  j  mjoin (natmap_alter_raw f i l !! j) = mjoin (l !! j).
Proof.
  revert i j. induction l; intros [|?] [|?] ?; simpl;
    repeat case_match; simpl; autorewrite with natmap; auto with congruence.
  rewrite natmap_lookup_singleton_raw_ne; congruence.
Qed.

111
Definition natmap_omap_raw {A B} (f : A  option B) :
112
113
    natmap_raw A  natmap_raw B :=
  fix go l :=
114
115
116
  match l with [] => [] | o :: l => natmap_cons_canon (o = f) (go l) end.
Lemma natmap_omap_raw_wf {A B} (f : A  option B) l :
  natmap_wf l  natmap_wf (natmap_omap_raw f l).
117
Proof. induction l; simpl; eauto using natmap_cons_canon_wf, natmap_wf_inv. Qed.
118
119
Lemma natmap_lookup_omap_raw {A B} (f : A  option B) l i :
  mjoin (natmap_omap_raw f l !! i) = mjoin (l !! i) = f.
120
121
122
Proof.
  revert i. induction l; intros [|?]; simpl; autorewrite with natmap; auto.
Qed.
123
Hint Rewrite @natmap_lookup_omap_raw : natmap.
124
125
Global Instance natmap_omap: OMap natmap := λ A B f m,
  let (l,Hl) := m in NatMap _ (natmap_omap_raw_wf f _ Hl).
126
127
128
129
130

Definition natmap_merge_raw {A B C} (f : option A  option B  option C) :
    natmap_raw A  natmap_raw B  natmap_raw C :=
  fix go l1 l2 :=
  match l1, l2 with
131
132
  | [], l2 => natmap_omap_raw (f None  Some) l2
  | l1, [] => natmap_omap_raw (flip f None  Some) l1
133
134
135
136
137
138
  | o1 :: l1, o2 :: l2 => natmap_cons_canon (f o1 o2) (go l1 l2)
  end.
Lemma natmap_merge_wf {A B C} (f : option A  option B  option C) l1 l2 :
  natmap_wf l1  natmap_wf l2  natmap_wf (natmap_merge_raw f l1 l2).
Proof.
  revert l2. induction l1; intros [|??]; simpl;
139
    eauto using natmap_omap_raw_wf, natmap_cons_canon_wf, natmap_wf_inv.
140
Qed.
141
142
Lemma natmap_lookup_merge_raw {A B C} (f : option A  option B  option C)
    l1 l2 i : f None None = None 
143
144
145
  mjoin (natmap_merge_raw f l1 l2 !! i) = f (mjoin (l1 !! i)) (mjoin (l2 !! i)).
Proof.
  intros. revert i l2. induction l1; intros [|?] [|??]; simpl;
146
147
    autorewrite with natmap; auto;
    match goal with |- context [?o = _] => by destruct o end.
148
149
Qed.
Instance natmap_merge: Merge natmap := λ A B C f m1 m2,
150
  let (l1, Hl1) := m1 in let (l2, Hl2) := m2 in
151
  NatMap (natmap_merge_raw f l1 l2) (natmap_merge_wf _ _ _ Hl1 Hl2).
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173

Fixpoint natmap_to_list_raw {A} (i : nat) (l : natmap_raw A) : list (nat * A) :=
  match l with
  | [] => []
  | None :: l => natmap_to_list_raw (S i) l
  | Some x :: l => (i,x) :: natmap_to_list_raw (S i) l
  end.
Lemma natmap_elem_of_to_list_raw_aux {A} j (l : natmap_raw A) i x :
  (i,x)  natmap_to_list_raw j l   i', i = i' + j  mjoin (l !! i') = Some x.
Proof.
  split.
  * revert j. induction l as [|[y|] l IH]; intros j; simpl.
    + by rewrite elem_of_nil.
    + rewrite elem_of_cons. intros [?|?]; simplify_equality.
      - by exists 0.
      - destruct (IH (S j)) as (i'&?&?); auto.
        exists (S i'); simpl; auto with lia.
    + intros. destruct (IH (S j)) as (i'&?&?); auto.
      exists (S i'); simpl; auto with lia.
  * intros (i'&?&Hi'). subst. revert i' j Hi'.
    induction l as [|[y|] l IH]; intros i j ?; simpl.
    + done.
174
175
176
177
    + destruct i as [|i]; simplify_equality'; [left|].
      right. rewrite <-Nat.add_succ_r. by apply (IH i (S j)).
    + destruct i as [|i]; simplify_equality'.
      rewrite <-Nat.add_succ_r. by apply (IH i (S j)).
178
179
180
181
Qed.
Lemma natmap_elem_of_to_list_raw {A} (l : natmap_raw A) i x :
  (i,x)  natmap_to_list_raw 0 l  mjoin (l !! i) = Some x.
Proof.
182
183
  rewrite natmap_elem_of_to_list_raw_aux. setoid_rewrite Nat.add_0_r.
  naive_solver.
184
185
186
187
188
189
190
191
Qed.
Lemma natmap_to_list_raw_nodup {A} i (l : natmap_raw A) :
  NoDup (natmap_to_list_raw i l).
Proof.
  revert i. induction l as [|[?|] ? IH]; simpl; try constructor; auto.
  rewrite natmap_elem_of_to_list_raw_aux. intros (?&?&?). lia.
Qed.
Instance natmap_to_list {A} : FinMapToList nat A (natmap A) := λ m,
192
  let (l,_) := m in natmap_to_list_raw 0 l.
193
194
195
196
197
198

Definition natmap_map_raw {A B} (f : A  B) : natmap_raw A  natmap_raw B :=
  fmap (fmap f).
Lemma natmap_map_wf {A B} (f : A  B) l :
  natmap_wf l  natmap_wf (natmap_map_raw f l).
Proof.
199
200
  unfold natmap_map_raw, natmap_wf. rewrite fmap_last.
  destruct (last l). by apply fmap_is_Some. done.
201
202
203
Qed.
Lemma natmap_lookup_map_raw {A B} (f : A  B) i l :
  mjoin (natmap_map_raw f l !! i) = f <$> mjoin (l !! i).
204
205
206
Proof.
  unfold natmap_map_raw. rewrite list_lookup_fmap. by destruct (l !! i).
Qed.
207
Instance natmap_map: FMap natmap := λ A B f m,
208
  let (l,Hl) := m in NatMap (natmap_map_raw f l) (natmap_map_wf _ _ Hl).
209
210
211
212
213

Instance: FinMap nat natmap.
Proof.
  split.
  * unfold lookup, natmap_lookup. intros A [l1 Hl1] [l2 Hl2] E.
214
    apply natmap_eq. revert l2 Hl1 Hl2 E. simpl.
215
216
217
    induction l1 as [|[x|] l1 IH]; intros [|[y|] l2] Hl1 Hl2 E; simpl in *.
    + done.
    + by specialize (E 0).
218
    + destruct (natmap_wf_lookup (None :: l2)) as (i&?&?); auto with congruence.
219
220
221
222
    + by specialize (E 0).
    + f_equal. apply (E 0). apply IH; eauto using natmap_wf_inv.
      intros i. apply (E (S i)).
    + by specialize (E 0).
223
    + destruct (natmap_wf_lookup (None :: l1)) as (i&?&?); auto with congruence.
224
    + by specialize (E 0).
225
    + f_equal. apply IH; eauto using natmap_wf_inv. intros i. apply (E (S i)).
226
227
228
229
230
231
  * done.
  * intros ?? [??] ?. apply natmap_lookup_alter_raw.
  * intros ?? [??] ??. apply natmap_lookup_alter_raw_ne.
  * intros ??? [??] ?. apply natmap_lookup_map_raw.
  * intros ? [??]. by apply natmap_to_list_raw_nodup.
  * intros ? [??] ??. by apply natmap_elem_of_to_list_raw.
232
  * intros ??? [??] ?. by apply natmap_lookup_omap_raw.
233
234
  * intros ????? [??] [??] ?. by apply natmap_lookup_merge_raw.
Qed.
235

236
237
238
239
240
241
242
243
244
245
Fixpoint strip_Nones {A} (l : list (option A)) : list (option A) :=
  match l with None :: l => strip_Nones l | _ => l end.

Lemma list_to_natmap_wf {A} (l : list (option A)) :
  natmap_wf (reverse (strip_Nones (reverse l))).
Proof.
  unfold natmap_wf. rewrite last_reverse.
  induction (reverse l) as [|[]]; simpl; eauto.
Qed.
Definition list_to_natmap {A} (l : list (option A)) : natmap A :=
246
  NatMap (reverse (strip_Nones (reverse l))) (list_to_natmap_wf l).
247
248
249
250
251
252
253
254
255
Lemma list_to_natmap_spec {A} (l : list (option A)) i :
  list_to_natmap l !! i = mjoin (l !! i).
Proof.
  unfold lookup at 1, natmap_lookup, list_to_natmap; simpl.
  rewrite <-(reverse_involutive l) at 2. revert i.
  induction (reverse l) as [|[x|] l' IH]; intros i; simpl; auto.
  rewrite reverse_cons, IH. clear IH. revert i.
  induction (reverse l'); intros [|?]; simpl; auto.
Qed.
256

257
(** Finally, we can construct sets of [nat]s satisfying extensional equality. *)
Robbert Krebbers's avatar
Robbert Krebbers committed
258
Notation natset := (mapset natmap).
259
260
261
Instance natmap_dom {A} : Dom (natmap A) natset := mapset_dom.
Instance: FinMapDom nat natmap natset := mapset_dom_spec.

262
263
(* Fixpoint avoids this definition from being unfolded *)
Fixpoint of_bools (βs : list bool) : natset :=
264
265
266
267
268
  let f (β : bool) := if β then Some () else None in
  Mapset $ list_to_natmap $ f <$> βs.
Definition to_bools (sz : nat) (X : natset) : list bool :=
  let f (mu : option ()) := match mu with Some _ => true | None => false end in
  resize sz false $ f <$> natmap_car (mapset_car X).
269
270

Lemma of_bools_unfold βs :
271
272
  let f (β : bool) := if β then Some () else None in
  of_bools βs = Mapset $ list_to_natmap $ f <$> βs.
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
Proof. by destruct βs. Qed.
Lemma elem_of_of_bools βs i : i  of_bools βs  βs !! i = Some true.
Proof.
  rewrite of_bools_unfold; unfold elem_of, mapset_elem_of; simpl.
  rewrite list_to_natmap_spec, list_lookup_fmap.
  destruct (βs !! i) as [[]|]; compute; intuition congruence.
Qed.
Lemma of_bools_union βs1 βs2 :
  length βs1 = length βs2 
  of_bools (βs1 ||* βs2) = of_bools βs1  of_bools βs2.
Proof.
  rewrite <-Forall2_same_length; intros Hβs.
  apply elem_of_equiv_L. intros i. rewrite elem_of_union, !elem_of_of_bools.
  revert i. induction Hβs as [|[] []]; intros [|?]; naive_solver.
Qed.
288
289
Lemma to_bools_length (X : natset) sz : length (to_bools sz X) = sz.
Proof. apply resize_length. Qed.
290
291
Lemma lookup_to_bools_ge sz X i : sz  i  to_bools sz X !! i = None.
Proof. by apply lookup_resize_old. Qed.
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
Lemma lookup_to_bools sz X i β :
  i < sz  to_bools sz X !! i = Some β  (i  X  β = true).
Proof.
  unfold to_bools, elem_of, mapset_elem_of, lookup at 2, natmap_lookup; simpl.
  intros. destruct (mapset_car X) as [l ?]; simpl.
  destruct (l !! i) as [mu|] eqn:Hmu; simpl.
  { rewrite lookup_resize, list_lookup_fmap, Hmu
      by (rewrite ?fmap_length; eauto using lookup_lt_Some).
    destruct mu as [[]|], β; simpl; intuition congruence. }
  rewrite lookup_resize_new by (rewrite ?fmap_length;
    eauto using lookup_ge_None_1); destruct β; intuition congruence.
Qed.
Lemma lookup_to_bools_true sz X i :
  i < sz  to_bools sz X !! i = Some true  i  X.
Proof. intros. rewrite lookup_to_bools by done. intuition. Qed.
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
Lemma lookup_to_bools_false sz X i :
  i < sz  to_bools sz X !! i = Some false  i  X.
Proof. intros. rewrite lookup_to_bools by done. naive_solver. Qed.
Lemma to_bools_union sz X1 X2 :
  to_bools sz (X1  X2) = to_bools sz X1 ||* to_bools sz X2.
Proof.
  apply list_eq; intros i; rewrite lookup_zip_with.
  destruct (decide (i < sz)); [|by rewrite !lookup_to_bools_ge by lia].
  apply option_eq; intros β.
  rewrite lookup_to_bools, elem_of_union by done; intros.
  destruct (decide (i  X1)), (decide (i  X2)); repeat first
    [ rewrite (λ X H, proj2 (lookup_to_bools_true sz X i H)) by done
    | rewrite (λ X H, proj2 (lookup_to_bools_false sz X i H)) by done];
    destruct β; naive_solver.
Qed.
Lemma to_of_bools βs sz : to_bools sz (of_bools βs) = resize sz false βs.
Proof.
  apply list_eq; intros i. destruct (decide (i < sz));
    [|by rewrite lookup_to_bools_ge, lookup_resize_old by lia].
  apply option_eq; intros β.
  rewrite lookup_to_bools, elem_of_of_bools by done.
  destruct (decide (i < length βs)).
  { rewrite lookup_resize by done.
    destruct (lookup_lt_is_Some_2 βs i) as [[]]; destruct β; naive_solver. }
  rewrite lookup_resize_new, lookup_ge_None_2 by lia. destruct β; naive_solver.
Qed.
333

334
335
(** A [natmap A] forms a stack with elements of type [A] and possible holes *)
Definition natmap_push {A} (o : option A) (m : natmap A) : natmap A :=
336
  let (l,Hl) := m in NatMap _ (natmap_cons_canon_wf o l Hl).
337
338
339
340
341
342

Definition natmap_pop_raw {A} (l : natmap_raw A) : natmap_raw A := tail l.
Lemma natmap_pop_wf {A} (l : natmap_raw A) :
  natmap_wf l  natmap_wf (natmap_pop_raw l).
Proof. destruct l; simpl; eauto using natmap_wf_inv. Qed.
Definition natmap_pop {A} (m : natmap A) : natmap A :=
343
  let (l,Hl) := m in NatMap _ (natmap_pop_wf _ Hl).
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359

Lemma lookup_natmap_push_O {A} o (m : natmap A) : natmap_push o m !! 0 = o.
Proof. by destruct o, m as [[|??]]. Qed.
Lemma lookup_natmap_push_S {A} o (m : natmap A) i :
  natmap_push o m !! S i = m !! i.
Proof. by destruct o, m as [[|??]]. Qed.
Lemma lookup_natmap_pop {A} (m : natmap A) i : natmap_pop m !! i = m !! S i.
Proof. by destruct m as [[|??]]. Qed.
Lemma natmap_push_pop {A} (m : natmap A) :
  natmap_push (m !! 0) (natmap_pop m) = m.
Proof.
  apply map_eq. intros i. destruct i.
  * by rewrite lookup_natmap_push_O.
  * by rewrite lookup_natmap_push_S, lookup_natmap_pop.
Qed.
Lemma natmap_pop_push {A} o (m : natmap A) : natmap_pop (natmap_push o m) = m.
360
Proof. apply natmap_eq. by destruct o, m as [[|??]]. Qed.