assoc.v 11.9 KB
Newer Older
1
2
3
4
5
6
7
8
9
10
11
12
13
(* Copyright (c) 2012-2013, Robbert Krebbers. *)
(* This file is distributed under the terms of the BSD license. *)
(** An implementation of finite maps and finite sets using association lists
ordered by keys. Although the lookup and insert operation are linear-time, the
main advantage of these association lists compared to search trees, is that it
has canonical representatives and thus extensional Leibniz equality. Compared
to a naive unordered association list, the merge operation (used for unions,
intersections, and difference) is also linear-time. *)
Require Import mapset.
Require Export fin_maps.

(** Because the association list is sorted using [strict lexico] instead of
[lexico], it automatically guarantees that no duplicates exist. *)
14
15
Definition assoc (K : Type) `{Lexico K, !TrichotomyT lexico,
    !StrictOrder lexico} (A : Type) : Type :=
16
  dsig (λ l : list (K * A), StronglySorted lexico (fst <$> l)).
17
18

Section assoc.
19
20
Context `{Lexico K, !StrictOrder lexico,
   x y : K, Decision (x = y), !TrichotomyT lexico}.
21

22
Infix "⊂" := lexico.
23
Notation assoc_before j l :=
24
  (Forall (lexico j) (fst <$> l)) (only parsing).
25
Notation assoc_wf l :=
26
  (StronglySorted (lexico) (fst <$> l)) (only parsing).
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46

Lemma assoc_before_transitive {A} (l : list (K * A)) i j :
  i  j  assoc_before j l  assoc_before i l.
Proof. intros. eapply Forall_impl; eauto. intros. by transitivity j. Qed.
Hint Resolve assoc_before_transitive.

Hint Extern 1 (StronglySorted _ []) => constructor.
Hint Extern 1 (StronglySorted _ (_ :: _)) => constructor.
Hint Extern 1 (Forall _ []) => constructor.
Hint Extern 1 (Forall _ (_ :: _)) => constructor.
Hint Extern 100 => progress simpl.

Ltac simplify_assoc := intros;
  repeat match goal with
  | H : Forall _ [] |- _ => clear H
  | H : Forall _ (_ :: _) |- _ => inversion_clear H
  | H : StronglySorted _ [] |- _ => clear H
  | H : StronglySorted _ (_ :: _) |- _ => inversion_clear H
  | _ => progress decompose_elem_of_list
  | _ => progress simplify_equality'
47
  | _ => match goal with |- context [?o = _] => by destruct o end
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
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
  end;
  repeat first
  [ progress simplify_order
  | progress autorewrite with assoc in *; simplify_equality'
  | destruct (trichotomyT lexico) as [[?|?]|?]; simplify_equality' ];
  eauto 9.

Fixpoint assoc_lookup_raw {A} (i : K) (l : list (K * A)) : option A :=
  match l with
  | [] => None
  | (j,x) :: l =>
    match trichotomyT lexico i j with
    | (**i i ⊂ j *) inleft (left _) => None
    | (**i i = j *) inleft (right _) => Some x
    | (**i j ⊂ i *) inright _ => assoc_lookup_raw i l
    end
  end.
Global Instance assoc_lookup {A} : Lookup K A (assoc K A) := λ k m,
  assoc_lookup_raw k (`m).

Lemma assoc_lookup_before {A} (l : list (K * A)) i :
  assoc_before i l  assoc_lookup_raw i l = None.
Proof. induction l as [|[??]]; simplify_assoc. Qed.
Hint Rewrite @assoc_lookup_before using (by eauto) : assoc.

Lemma assoc_eq {A} (l1 l2 : list (K * A)) :
  assoc_wf l1  assoc_wf l2 
  ( i, assoc_lookup_raw i l1 = assoc_lookup_raw i l2)  l1 = l2.
Proof.
  revert l2. induction l1 as [|[i x] l1 IH]; intros [|[j y] l2]; intros ?? E.
  { done. }
  { specialize (E j); simplify_assoc; by repeat constructor. }
  { specialize (E i); simplify_assoc; by repeat constructor. }
  pose proof (E i); pose proof (E j); simplify_assoc.
  f_equal. apply IH; auto. intros i'. specialize (E i'); simplify_assoc.
Qed.
Definition assoc_empty_wf {A} : assoc_wf (@nil (K * A)).
Proof. constructor. Qed.
Global Instance assoc_empty {A} : Empty (assoc K A) := dexist _ assoc_empty_wf.

Definition assoc_cons {A} (i : K) (o : option A) (l : list (K * A)) :
  list (K * A) := match o with None => l | Some z => (i,z) :: l end.
Lemma assoc_cons_before {A} (l : list (K * A)) i j o :
  assoc_before i l  i  j  assoc_before i (assoc_cons j o l).
Proof. destruct o; simplify_assoc. Qed.
Lemma assoc_cons_wf {A} (l : list (K * A)) i o :
  assoc_wf l  assoc_before i l  assoc_wf (assoc_cons i o l).
Proof. destruct o; simplify_assoc. Qed.
Hint Resolve assoc_cons_before assoc_cons_wf.
Lemma assoc_lookup_cons {A} (l : list (K * A)) i o :
  assoc_before i l  assoc_lookup_raw i (assoc_cons i o l) = o.
Proof. destruct o; simplify_assoc. Qed.
Lemma assoc_lookup_cons_lt {A} (l : list (K * A)) i j o :
  i  j  assoc_before i l  assoc_lookup_raw i (assoc_cons j o l) = None.
Proof. destruct o; simplify_assoc. Qed.
Lemma assoc_lookup_cons_gt {A} (l : list (K * A)) i j o :
  j  i  assoc_lookup_raw i (assoc_cons j o l) = assoc_lookup_raw i l.
Proof. destruct o; simplify_assoc. Qed.
Hint Rewrite @assoc_lookup_cons @assoc_lookup_cons_lt
  @assoc_lookup_cons_gt using (by eauto 8) : assoc.

Fixpoint assoc_alter_raw {A} (f : option A  option A)
    (i : K) (l : list (K * A)) : list (K * A) :=
  match l with
  | [] => assoc_cons i (f None) []
  | (j,x) :: l =>
    match trichotomyT lexico i j with
    | (**i i ⊂ j *) inleft (left _) => assoc_cons i (f None) ((j,x) :: l)
    | (**i i = j *) inleft (right _) => assoc_cons j (f (Some x)) l
    | (**i j ⊂ i *) inright _ => (j,x) :: assoc_alter_raw f i l
    end
  end.
Lemma assoc_alter_wf {A} (f : option A  option A) i l :
  assoc_wf l  assoc_wf (assoc_alter_raw f i l).
Proof.
  revert l. assert ( j l,
    j  i  assoc_before j l  assoc_before j (assoc_alter_raw f i l)).
  { intros j l. induction l as [|[??]]; simplify_assoc. }
  intros l. induction l as [|[??]]; simplify_assoc.
Qed.
Global Instance assoc_alter {A} : PartialAlter K A (assoc K A) := λ f i m,
  dexist _ (assoc_alter_wf f i _ (proj2_dsig m)).

Lemma assoc_lookup_raw_alter {A} f (l : list (K * A)) i :
  assoc_wf l 
  assoc_lookup_raw i (assoc_alter_raw f i l) = f (assoc_lookup_raw i l).
Proof. induction l as [|[??]]; simplify_assoc. Qed.
Lemma assoc_lookup_raw_alter_ne {A} f (l : list (K * A)) i j :
  assoc_wf l  i  j 
  assoc_lookup_raw j (assoc_alter_raw f i l) = assoc_lookup_raw j l.
Proof.
  induction l as [|[??]]; simplify_assoc; unfold assoc_cons;
    destruct (f _); simplify_assoc.
Qed.
Lemma assoc_fmap_wf {A B} (f : A  B) (l : list (K * A)) :
143
  assoc_wf l  assoc_wf (prod_map id f <$> l).
144
145
146
147
148
149
150
Proof.
  intros. by rewrite <-list_fmap_compose,
    (list_fmap_ext _ fst l l) by (done; by intros []).
Qed.
Global Program Instance assoc_fmap: FMap (assoc K) := λ A B f m,
  dexist _ (assoc_fmap_wf f _ (proj2_dsig m)).
Lemma assoc_lookup_fmap {A B} (f : A  B) (l : list (K * A)) i :
151
  assoc_lookup_raw i (prod_map id f <$> l) = fmap f (assoc_lookup_raw i l).
152
153
Proof. induction l as [|[??]]; simplify_assoc. Qed.

154
Fixpoint assoc_omap_raw {A B} (f : A  option B)
155
156
157
    (l : list (K * A)) : list (K * B) :=
  match l with
  | [] => []
158
  | (i,x) :: l => assoc_cons i (f x) (assoc_omap_raw f l)
159
  end.
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
Lemma assoc_omap_raw_before {A B} (f : A  option B) l j :
  assoc_before j l  assoc_before j (assoc_omap_raw f l).
Proof. induction l as [|[??]]; simplify_assoc. Qed.
Hint Resolve assoc_omap_raw_before.
Lemma assoc_omap_wf {A B} (f : A  option B) l :
  assoc_wf l  assoc_wf (assoc_omap_raw f l).
Proof. induction l as [|[??]]; simplify_assoc. Qed.
Hint Resolve assoc_omap_wf.
Global Instance assoc_omap: OMap (assoc K) := λ A B f m,
  dexist _ (assoc_omap_wf f _ (proj2_dsig m)).
Lemma assoc_omap_spec {A B} (f : A  option B) l i :
  assoc_wf l 
  assoc_lookup_raw i (assoc_omap_raw f l) = assoc_lookup_raw i l = f.
Proof. intros. induction l as [|[??]]; simplify_assoc. Qed.
Hint Rewrite @assoc_omap_spec using (by eauto) : assoc.

176
177
178
179
Fixpoint assoc_merge_raw {A B C} (f : option A  option B  option C)
    (l : list (K * A)) : list (K * B)  list (K * C) :=
  fix go (k : list (K * B)) :=
  match l, k with
180
181
  | [], _ => assoc_omap_raw (f None  Some) k
  | _, [] => assoc_omap_raw (flip f None  Some) l
182
183
184
185
186
187
188
189
190
191
192
  | (i,x) :: l, (j,y) :: k =>
    match trichotomyT lexico i j with
    | (**i i ⊂ j *) inleft (left _) =>
      assoc_cons i (f (Some x) None) (assoc_merge_raw f l ((j,y) :: k))
    | (**i i = j *) inleft (right _) =>
      assoc_cons i (f (Some x) (Some y)) (assoc_merge_raw f l k)
    | (**i j ⊂ i *) inright _ =>
      assoc_cons j (f None (Some y)) (go k)
    end
  end.
Section assoc_merge_raw.
193
  Context {A B C} (f : option A  option B  option C).
194
  Lemma assoc_merge_nil_l k :
195
    assoc_merge_raw f [] k = assoc_omap_raw (f None  Some) k.
196
197
  Proof. by destruct k. Qed.
  Lemma assoc_merge_nil_r l :
198
    assoc_merge_raw f l [] = assoc_omap_raw (flip f None  Some) l.
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
  Proof. by destruct l as [|[??]]. Qed.
  Lemma assoc_merge_cons i x j y l k :
    assoc_merge_raw f ((i,x) :: l) ((j,y) :: k) =
      match trichotomyT lexico i j with
      | (**i i ⊂ j *) inleft (left _) =>
        assoc_cons i (f (Some x) None) (assoc_merge_raw f l ((j,y) :: k))
      | (**i i = j *) inleft (right _) =>
        assoc_cons i (f (Some x) (Some y)) (assoc_merge_raw f l k)
      | (**i j ⊂ i *) inright _ =>
        assoc_cons j (f None (Some y)) (assoc_merge_raw f ((i,x) :: l) k)
      end.
  Proof. done. Qed.
End assoc_merge_raw.
Arguments assoc_merge_raw _ _ _ _ _ _ : simpl never.
Hint Rewrite @assoc_merge_nil_l @assoc_merge_nil_r @assoc_merge_cons : assoc.
Lemma assoc_merge_before {A B C} (f : option A  option B  option C) l1 l2 j :
  assoc_before j l1  assoc_before j l2 
  assoc_before j (assoc_merge_raw f l1 l2).
Proof.
  revert l2. induction l1 as [|[??] l1 IH];
    intros l2; induction l2 as [|[??] l2 IH2]; simplify_assoc.
Qed.
Hint Resolve assoc_merge_before.
Lemma assoc_merge_wf {A B C} (f : option A  option B  option C) l1 l2 :
  assoc_wf l1  assoc_wf l2  assoc_wf (assoc_merge_raw f l1 l2).
Proof.
225
  revert l2. induction l1 as [|[i x] l1 IH];
226
227
228
    intros l2; induction l2 as [|[j y] l2 IH2]; simplify_assoc.
Qed.
Global Instance assoc_merge: Merge (assoc K) := λ A B C f m1 m2,
229
  dexist _ (assoc_merge_wf f _ _ (proj2_dsig m1) (proj2_dsig m2)).
230
231
232
233
234
235
236
237
238
Lemma assoc_merge_spec {A B C} (f : option A  option B  option C) l1 l2 i :
  f None None = None  assoc_wf l1  assoc_wf l2 
  assoc_lookup_raw i (assoc_merge_raw f l1 l2) =
    f (assoc_lookup_raw i l1) (assoc_lookup_raw i l2).
Proof.
  intros ?. revert l2. induction l1 as [|[??] l1 IH]; intros l2;
    induction l2 as [|[??] l2 IH2]; simplify_assoc; rewrite ?IH; simplify_assoc.
Qed.

239
Global Instance assoc_to_list {A} : FinMapToList K A (assoc K A) := proj1_sig.
240
241
242
243
Lemma assoc_to_list_nodup {A} (l : list (K * A)) : assoc_wf l  NoDup l.
Proof.
  revert l. assert ( i x (l : list (K * A)), assoc_before i l  (i,x)  l).
  { intros i x l. rewrite Forall_fmap, Forall_forall. intros Hl Hi.
244
    destruct (irreflexivity (lexico) i). by apply (Hl (i,x) Hi). }
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
  induction l as [|[??]]; simplify_assoc; constructor; auto.
Qed.
Lemma assoc_to_list_elem_of {A} (l : list (K * A)) i x :
  assoc_wf l  (i,x)  l  assoc_lookup_raw i l = Some x.
Proof.
  split.
  * induction l as [|[??]]; simplify_assoc; naive_solver.
  * induction l as [|[??]]; simplify_assoc; [left| right]; eauto.
Qed.

(** * Instantiation of the finite map interface *)
Hint Extern 1 (assoc_wf _) => by apply (bool_decide_unpack _).
Global Instance: FinMap K (assoc K).
Proof.
  split.
  * intros ? [l1 ?] [l2 ?] ?. apply (sig_eq_pi _), assoc_eq; auto.
  * done.
  * intros ?? [??] ?. apply assoc_lookup_raw_alter; auto. 
  * intros ?? [??] ???. apply assoc_lookup_raw_alter_ne; auto.
  * intros ??? [??] ?. apply assoc_lookup_fmap.
  * intros ? [??]. apply assoc_to_list_nodup; auto.
  * intros ? [??] ??. apply assoc_to_list_elem_of; auto.
267
  * intros ??? [??] ?. apply assoc_omap_spec; auto.
268
269
270
271
272
273
274
  * intros ????? [??] [??] ?. apply assoc_merge_spec; auto.
Qed.
End assoc.

(** * Finite sets *)
(** We construct finite sets using the above implementation of maps. *)
Notation assoc_set K := (mapset (assoc K)).
275
276
Instance assoc_map_dom `{Lexico K, !TrichotomyT (@lexico K _),
  !StrictOrder lexico} {A} : Dom (assoc K A) (assoc_set K) := mapset_dom.
277
Instance assoc_map_dom_spec `{Lexico K} `{!TrichotomyT (@lexico K _)}
278
    `{!StrictOrder lexico,  x y : K, Decision (x = y)} :
279
  FinMapDom K (assoc K) (assoc_set K) := mapset_dom_spec.