list.v 12.4 KB
Newer Older
Robbert Krebbers's avatar
Robbert Krebbers committed
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
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
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
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
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
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
333
334
335
336
337
338
339
340
341
Require Import Permutation. 
Require Export base decidable option.

Arguments cons {_} _ _.
Arguments app {_} _ _.

Arguments In {_} _ _.
Arguments NoDup_nil {_}.
Arguments Permutation {_} _ _.

Notation "(::)" := cons (only parsing) : C_scope.
Notation "( x ::)" := (cons x) (only parsing) : C_scope.
Notation "(:: l )" := (λ x, cons x l) (only parsing) : C_scope.
Notation "(++)" := app (only parsing) : C_scope.
Notation "( l ++)" := (app l) (only parsing) : C_scope.
Notation "(++ k )" := (λ l, app l k) (only parsing) : C_scope.

Section list_properties.
Context {A : Type}.

Definition option_list : option A  list A := option_rect _ (λ x, [x]) [].

Lemma NoDup_singleton (x : A) : NoDup [x].
Proof. constructor. easy. constructor. Qed.
Lemma NoDup_app (l k : list A) :
  NoDup l  NoDup k  ( x, In x l  ¬In x k)  NoDup (l ++ k).
Proof.
  induction 1; simpl. easy.
  constructor. rewrite in_app_iff. firstorder. firstorder.
Qed.

Global Instance:  k : list A, Injective (=) (=) (k ++).
Proof. intros ???. apply app_inv_head. Qed.
Global Instance:  k : list A, Injective (=) (=) (++ k).
Proof. intros ???. apply app_inv_tail. Qed.

Lemma in_nil_inv (l : list A) : ( x, ¬In x l)  l = [].
Proof. destruct l. easy. now edestruct 1; constructor. Qed.
Lemma nil_length (l : list A) : length l = 0  l = [].
Proof. destruct l. easy. discriminate. Qed.
Lemma NoDup_inv_1 (x : A) (l : list A) : NoDup (x :: l)  ¬In x l.
Proof. now inversion_clear 1. Qed.
Lemma NoDup_inv_2 (x : A) (l : list A) : NoDup (x :: l)  NoDup l.
Proof. now inversion_clear 1. Qed.
Lemma Forall_inv_2 (P : A  Prop) x l : Forall P (x :: l)  Forall P l.
Proof. now inversion 1. Qed.
Lemma Exists_inv (P : A  Prop) x l : Exists P (x :: l)  P x  Exists P l.
Proof. inversion 1; intuition. Qed.

Global Instance list_eq_dec {dec :  x y : A, Decision (x = y)} :  l k : list A, Decision (l = k).
Proof. solve_decision. Qed.
Global Instance list_in_dec {dec :  x y : A, Decision (x = y)} :  x l,
  Decision (In x l) := in_dec dec.

Global Instance NoDup_dec {dec :  x y : A, Decision (x = y)} :  (l : list A), Decision (NoDup l) :=
  fix NoDup_dec l :=
  match l return Decision (NoDup l) with
  | [] => left NoDup_nil
  | x :: l =>
    match In_dec dec x l with
    | left Hin => right (λ H, NoDup_inv_1 _ _ H Hin)
    | right Hin =>
      match NoDup_dec l with
      | left H => left (NoDup_cons _ Hin H)
      | right H => right (H  NoDup_inv_2 _ _)
      end
    end
  end.

Global Instance Forall_dec (P : A  Prop) {dec :  x, Decision (P x)} :  l, Decision (Forall P l) :=
  fix go (l : list A) :=
  match l return {Forall P l} + {¬Forall P l} with
  | [] => left (Forall_nil _)
  | x :: l =>
    match dec x with
    | left Hx =>
      match go l with
      | left Hl => left (Forall_cons _ Hx Hl)
      | right Hl => right (Hl  Forall_inv_2 _ _ _)
      end
    | right Hx => right (Hx  @Forall_inv _ _ _ _)
    end
  end.

Global Instance Exists_dec (P : A  Prop) {dec :  x, Decision (P x)} :  l, Decision (Exists P l) :=
  fix go (l : list A) :=
  match l return {Exists P l} + {¬Exists P l} with
  | [] => right (proj1 (Exists_nil _))
  | x :: l =>
    match dec x with
    | left Hx => left (Exists_cons_hd _ _ _ Hx)
    | right Hx =>
      match go l with
      | left Hl => left (Exists_cons_tl _ Hl)
      | right Hl => right (or_ind Hx Hl  Exists_inv _ _ _)
      end
    end
  end.

Definition prefix_of (l1 l2 : list A) : Prop :=  k, l2 = l1 ++ k.
Definition suffix_of (l1 l2 : list A) : Prop :=  k, l2 = k ++ l1.

Global Instance: PreOrder prefix_of.
Proof.
  split.
   intros ?. eexists []. now rewrite app_nil_r.
  intros ??? [k1 ?] [k2 ?]. exists (k1 ++ k2). subst. now rewrite app_assoc.
Qed.

Lemma prefix_of_nil l : prefix_of [] l.
Proof. now exists l. Qed.
Lemma prefix_of_nil_not x l : ¬prefix_of (x :: l) [].
Proof. intros [k E]. discriminate. Qed.
Lemma prefix_of_cons x y l1 l2 : x = y  prefix_of l1 l2  prefix_of (x :: l1) (y :: l2).
Proof. intros ? [k E]. exists k. now subst. Qed.
Lemma prefix_of_cons_inv_1 x y l1 l2 : prefix_of (x :: l1) (y :: l2)  x = y.
Proof. intros [k E]. now injection E. Qed.
Lemma prefix_of_cons_inv_2 x y l1 l2 : prefix_of (x :: l1) (y :: l2)  prefix_of l1 l2.
Proof. intros [k E]. exists k. now injection E. Qed.

Lemma prefix_of_app_l l1 l2 l3 : prefix_of (l1 ++ l3) l2  prefix_of l1 l2.
Proof. intros [k ?]. red. exists (l3 ++ k). subst. now rewrite <-app_assoc. Qed.
Lemma prefix_of_app_r l1 l2 l3 : prefix_of l1 l2  prefix_of l1 (l2 ++ l3).
Proof. intros [k ?]. exists (k ++ l3). subst. now rewrite app_assoc. Qed.

Global Instance prefix_of_dec `{ x y : A, Decision (x = y)} :  l1 l2, Decision (prefix_of l1 l2) :=
  fix prefix_of_dec l1 l2 :=
  match l1, l2 return { prefix_of l1 l2 } + { ¬prefix_of l1 l2 } with
  | [], _ => left (prefix_of_nil _)
  | _, [] => right (prefix_of_nil_not _ _)
  | x :: l1, y :: l2 =>
    match decide_rel (=) x y with
    | left Exy =>
      match prefix_of_dec l1 l2 with
      | left Hl1l2 => left (prefix_of_cons _ _ _ _ Exy Hl1l2)
      | right Hl1l2 => right (Hl1l2  prefix_of_cons_inv_2 _ _ _ _)
      end
    | right Exy => right (Exy  prefix_of_cons_inv_1 _ _ _ _)
    end
  end.

Global Instance: PreOrder suffix_of.
Proof.
  split.
   intros ?. now eexists [].
  intros ??? [k1 ?] [k2 ?]. exists (k2 ++ k1). subst. now rewrite app_assoc.
Qed.

Lemma prefix_suffix_rev l1 l2 : prefix_of l1 l2  suffix_of (rev l1) (rev l2).
Proof.
  split; intros [k E]; exists (rev k).
   now rewrite E, rev_app_distr.
  now rewrite <-(rev_involutive l2), E, rev_app_distr, rev_involutive.
Qed.
Lemma suffix_prefix_rev l1 l2 : suffix_of l1 l2  prefix_of (rev l1) (rev l2).
Proof. now rewrite prefix_suffix_rev, !rev_involutive. Qed.

Lemma suffix_of_nil l : suffix_of [] l.
Proof. exists l. now rewrite app_nil_r. Qed.
Lemma suffix_of_nil_not x l : ¬suffix_of (x :: l) [].
Proof. intros [[] ?]; discriminate. Qed.
Lemma suffix_of_cons x y l1 l2 : x = y  suffix_of l1 l2  suffix_of (l1 ++ [x]) (l2 ++ [y]).
Proof. intros ? [k E]. exists k. subst. now rewrite app_assoc. Qed.
Lemma suffix_of_snoc_inv_1 x y l1 l2 : suffix_of (l1 ++ [x]) (l2 ++ [y])  x = y.
Proof. rewrite suffix_prefix_rev, !rev_unit. now apply prefix_of_cons_inv_1. Qed.
Lemma suffix_of_snoc_inv_2 x y l1 l2 : suffix_of (l1 ++ [x]) (l2 ++ [y])  suffix_of l1 l2.
Proof. rewrite !suffix_prefix_rev, !rev_unit. now apply prefix_of_cons_inv_2. Qed.

Lemma suffix_of_cons_l l1 l2 x : suffix_of (x :: l1) l2  suffix_of l1 l2.
Proof. intros [k ?]. exists (k ++ [x]). subst. now rewrite <-app_assoc. Qed.
Lemma suffix_of_app_l l1 l2 l3 : suffix_of (l3 ++ l1) l2  suffix_of l1 l2.
Proof. intros [k ?]. exists (k ++ l3). subst. now rewrite <-app_assoc. Qed.
Lemma suffix_of_cons_r l1 l2 x : suffix_of l1 l2  suffix_of l1 (x :: l2).
Proof. intros [k ?]. exists (x :: k). now subst. Qed.
Lemma suffix_of_app_r l1 l2 l3 : suffix_of l1 l2  suffix_of l1 (l3 ++ l2).
Proof. intros [k ?]. exists (l3 ++ k). subst. now rewrite app_assoc. Qed.

Lemma suffix_of_cons_inv l1 l2 x y : 
  suffix_of (x :: l1) (y :: l2)  x :: l1 = y :: l2  suffix_of (x :: l1) l2.
Proof.
  intros [[|? k] E].
   now left.
  right. simplify_eqs. now apply suffix_of_app_r.
Qed.
Lemma suffix_of_cons_not x l : ¬suffix_of (x :: l) l.
Proof.
  intros [k E]. change ([] ++ l = k ++ [x] ++ l) in E.
  rewrite app_assoc in E. apply app_inv_tail in E.
  destruct k; simplify_eqs.
Qed.

Global Program Instance suffix_of_dec `{ x y : A, Decision (x = y)} l1 l2 : Decision (suffix_of l1 l2) :=
  match decide_rel prefix_of (rev_append l1 []) (rev_append l2 []) with
  | left Hpre => left _
  | right Hpre => right _
  end.
Next Obligation. apply suffix_prefix_rev. now rewrite !rev_alt. Qed.
Next Obligation. intro. destruct Hpre. rewrite <-!rev_alt. now apply suffix_prefix_rev. Qed.
End list_properties.

Hint Resolve suffix_of_nil suffix_of_cons_r suffix_of_app_r : list.
Hint Extern 0 (prefix_of _ _) => reflexivity : list.
Hint Extern 0 (suffix_of _ _) => reflexivity: list.
Hint Extern 0 (PropHolds (suffix_of _ _)) => red; auto with list : typeclass_instances.

Ltac simplify_suffix_of := repeat
  match goal with
  | H : suffix_of (_ :: _) _ |- _ => destruct (suffix_of_cons_not _ _ H); clear H
  | H : suffix_of (_ :: _) [] |- _ => destruct (suffix_of_nil_not _ _ H); clear H
  | H : suffix_of (_ :: _) (_ :: _) |- _ => destruct (suffix_of_cons_inv _ _ _ _ H); clear H
  | H : suffix_of ?x ?x |- _ => clear H
  | H : suffix_of ?x (_ :: ?x) |- _ => clear H
  | H : suffix_of ?x (_ ++ ?x) |- _ => clear H
  | _ => progress simplify_eqs
  end.

Global Instance list_lookup: Lookup nat list :=
  fix list_lookup A (i : nat) (l : list A) {struct l} : option A :=
  match l with
  | [] => None
  | x :: l =>
    match i with
    | 0 => Some x
    | S i => @lookup _ _ list_lookup _ i l
    end
  end.
Local Arguments lookup _ _ _ _ _ !_ /.

Global Instance list_alter: Alter nat list :=
  fix list_alter A (f : A  A) (i : nat) (l : list A) {struct l} :=
  match l with
  | [] => []
  | x :: l =>
    match i with
    | 0 => f x :: l
    | S i => x :: @alter _ _ list_alter _ f i l
    end
  end.

Lemma list_eq {A} (l1 l2 : list A) : ( i, l1 !! i = l2 !! i)  l1 = l2.
Proof.
  revert l2. induction l1; intros [|??] H.
     easy.
    discriminate (H 0).
   discriminate (H 0).
  f_equal. now injection (H 0). apply IHl1. intro. apply (H (S _)).
Qed.

Lemma list_lookup_tail {A} (l : list A) i : tail l !! i = l !! S i.
Proof. now destruct l. Qed.

Global Instance list_ret: MRet list := λ A a, [a].
Global Instance list_fmap: FMap list :=
  fix go A B (f : A  B) (l : list A) :=
  match l with
  | [] => []
  | x :: l => f x :: @fmap _ go _ _ f l
  end.
Global Instance list_join: MJoin list := 
  fix go A (l : list (list A)) : list A :=
  match l with
  | [] =>  []
  | x :: l => x ++ @mjoin _ go _ l
  end.
Global Instance list_bind: MBind list := λ A B f l, mjoin (f <$> l).

Lemma list_lookup_weaken {A} (l l' : list A) i x :
  l !! i = Some x  (l ++ l') !! i = Some x.
Proof. revert i. induction l. discriminate. now intros []. Qed.

Lemma list_lookup_fmap {A B} (f : A  B) l i : (f <$> l) !! i = f <$> (l !! i).
Proof. revert i. induction l; now intros [|]. Qed.

Lemma fold_right_permutation `(f : A  B  B) (b : B) :
  ( a1 a2 b, f a1 (f a2 b) = f a2 (f a1 b))  Proper (Permutation ==> (=)) (fold_right f b).
Proof. intros Hflip. induction 1; simpl; try congruence. Qed.

(*
Section NoDupA.
  Fixpoint removeDups (l : list A) : list A :=
    match l with
    | [] => []
    | x :: l =>
      let k := removeDups l in
      if InA_dec dec x k then k else x :: k
    end.

  Lemma removeDups_NoDupA l : NoDupA R (removeDups l).
  Proof. induction l; simpl; try case InA_dec; intuition. Qed.

  Definition elem_removeDups x l : x ∈ removeDups l → x ∈ l.
  Proof.
    induction l; simpl; auto.
    case InA_dec; eauto.
    intros ? Hin. destruct (list_elem_inv _ _ _ Hin); subst; eauto.
  Qed.

  Lemma elem_InA x y l : x ∈ l → R y x → InA R y l.
  Proof. induction 1; subst; intuition. Qed.

  Lemma InA_elem x l : InA R x l → ∃ y, y ∈ l ∧ R x y.
  Proof. induction 1. eauto. destruct IHInA as [? [??]]; eauto. Qed.

  Context `{!Equivalence R}.

  Lemma in_removeDups_inv x l : x ∈ l → ∃ y, y ∈ l ∧ R x y ∧ y ∈ removeDups l.
  Proof.
    induction l as [|y l]; simpl.
     inversion 1.
    case InA_dec.
     inversion 2; subst.
      destruct (InA_elem y (removeDups l)) as [z [??]]; auto.
      exists z. intuition. right. now apply elem_removeDups.
     destruct IHl as [z [?[??]]]. auto. exists z. intuition.
    intros ? Hin. destruct (list_elem_inv _ _ _ Hin).
     subst. exists y. intuition.
    destruct IHl as [z [?[??]]]. easy. exists z. intuition.
  Qed.

  Lemma in_removeDups x l : InA R x l ↔ InA R x (removeDups l).
  Proof.
    split.
     induction 1 as [?? E|]; simpl; [rewrite E|]; case InA_dec; intuition.
    induction l; simpl; auto.
    case InA_dec. auto. inversion_clear 2; auto.
  Qed.
End NoDupA.

Lemma InA_lift_rel {A B} (R : relation A) (f : B → A) x l : InA R (f x) (f <$> l) ↔ InA (lift_rel R f) x l.
Proof. split; induction l; unfold fmap; simpl; inversion_clear 1; auto. Qed.

Lemma NoDupA_lift_rel {A B} (R : relation A) (f : B → A) l : NoDupA R (f <$> l) ↔ NoDupA (lift_rel R f) l.
Proof.
  split.
   induction l; [easy |].
   intros HnoDup. constructor.
    intro. destruct (NoDupA_inv_1 R _ _ HnoDup). now apply InA_lift_rel.
   eapply IHl, NoDupA_inv_2; eauto.
  induction 1; constructor. now rewrite InA_lift_rel. easy.
Qed.
*)