natmap.v 14 KB
Newer Older
Robbert Krebbers's avatar
Robbert Krebbers committed
1
(* Copyright (c) 2012-2014, Robbert Krebbers. *)
2
(* This file is distributed under the terms of the BSD license. *)
3
4
5
6
(** 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. *)
Require Import fin_maps 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
22
23
  { exists 0. simpl. eauto. }
  destruct IH as (i&x&?); eauto using natmap_wf_inv; [|by exists (S i) x].
  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
174

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.
    + destruct i as [|i]; simplify_equality; [left|].
175
      right. rewrite Nat.add_succ_comm. by apply (IH i (S j)).
176
    + destruct i as [|i]; simplify_equality.
177
      rewrite Nat.add_succ_comm. 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. *)
258
Notation natset := (mapset (natmap unit)).
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
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
Lemma to_bools_length (X : natset) sz : length (to_bools sz X) = sz.
Proof. apply resize_length. Qed.
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.
305

306
307
(** 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 :=
308
  let (l,Hl) := m in NatMap _ (natmap_cons_canon_wf o l Hl).
309
310
311
312
313
314

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 :=
315
  let (l,Hl) := m in NatMap _ (natmap_pop_wf _ Hl).
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331

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.
332
Proof. apply natmap_eq. by destruct o, m as [[|??]]. Qed.