list.v 25 KB
Newer Older
1
2
3
4
(* Copyright (c) 2012, Robbert Krebbers. *)
(* This file is distributed under the terms of the BSD license. *)
(** This file collects general purpose definitions and theorems on lists that
are not in the Coq standard library. *)
5
Require Import Omega Permutation.
Robbert Krebbers's avatar
Robbert Krebbers committed
6
7
Require Export base decidable option.

8
Arguments length {_} _.
Robbert Krebbers's avatar
Robbert Krebbers committed
9
10
11
Arguments cons {_} _ _.
Arguments app {_} _ _.

12
13
14
15
16
Arguments Forall_nil {_ _}.
Arguments Forall_cons {_ _} _ _ _ _.
Arguments Exists_nil {_ _}.
Arguments Exists_cons {_ _} _ _.

Robbert Krebbers's avatar
Robbert Krebbers committed
17
18
19
20
Arguments In {_} _ _.
Arguments NoDup_nil {_}.
Arguments Permutation {_} _ _.

21
22
23
24
25
26
27
28
29
30
31
32
33
Notation tail := tl.
Notation take := firstn.
Notation drop := skipn.
Notation foldr := fold_right.
Notation foldl := fold_left.

Arguments take {_} !_ !_ /.
Arguments drop {_} !_ !_ /.

Notation take_drop := firstn_skipn.
Notation foldr_app := fold_right_app.
Notation foldl_app := fold_left_app.

Robbert Krebbers's avatar
Robbert Krebbers committed
34
35
36
37
38
39
40
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.

41
42
(** * General definitions *)
(** Looking up elements and updating elements in a list. *)
43
Global Instance list_lookup: Lookup nat list :=
44
  fix go A (i : nat) (l : list A) {struct l} : option A :=
45
46
47
48
49
  match l with
  | [] => None
  | x :: l =>
    match i with
    | 0 => Some x
50
    | S i => @lookup _ _ go _ i l
51
52
53
54
    end
  end.

Global Instance list_alter: Alter nat list :=
55
  fix go A (f : A  A) (i : nat) (l : list A) {struct l} :=
56
57
58
59
60
  match l with
  | [] => []
  | x :: l =>
    match i with
    | 0 => f x :: l
61
    | S i => x :: @alter _ _ go _ f i l
62
63
64
    end
  end.

65
66
67
68
69
70
71
72
73
74
75
76
Global Instance list_insert: Insert nat list := λ _ i x,
  alter (λ _, x) i.

Global Instance list_delete: Delete nat list :=
  fix go A (i : nat) (l : list A) {struct l} : list A :=
  match l with
  | [] => []
  | x :: l =>
    match i with
    | 0 => l
    | S i => x :: @delete _ _ go _ i l
    end
77
78
  end.

79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
Tactic Notation "discriminate_list_equality" hyp(H) :=
  apply (f_equal length) in H;
  repeat (simpl in H || rewrite app_length in H);
  exfalso; omega.
Tactic Notation "discriminate_list_equality" :=
  repeat_on_hyps (fun H => discriminate_list_equality H).

Ltac simplify_list_equality := repeat
  match goal with
  | _ => progress simplify_equality
  | H : _ ++ _ = _ ++ _ |- _ => first
     [ apply app_inv_head in H
     | apply app_inv_tail in H ]
  | H : _ |- _ => discriminate_list_equality H
  end.
    
95
96
(** The function [option_list] converts an element of the option type into
a list. *)
97
Definition option_list {A} : option A  list A := option_rect _ (λ x, [x]) [].
98
99
100

(** The predicate [prefix_of] holds if the first list is a prefix of the second.
The predicate [suffix_of] holds if the first list is a suffix of the second. *)
101
102
103
Definition prefix_of {A} (l1 l2 : list A) : Prop :=  k, l2 = l1 ++ k.
Definition suffix_of {A} (l1 l2 : list A) : Prop :=  k, l2 = k ++ l1.

104
105
(** * General theorems *)
Section general_properties.
Robbert Krebbers's avatar
Robbert Krebbers committed
106
107
Context {A : Type}.

108
109
110
Lemma list_eq (l1 l2 : list A) : ( i, l1 !! i = l2 !! i)  l1 = l2.
Proof.
  revert l2. induction l1; intros [|??] H.
111
  * done.
112
113
  * discriminate (H 0).
  * discriminate (H 0).
114
  * f_equal. by injection (H 0). apply IHl1. intro. apply (H (S _)).
115
116
117
Qed.

Lemma list_lookup_nil i : @nil A !! i = None.
118
Proof. by destruct i. Qed.
119
Lemma list_lookup_tail (l : list A) i : tail l !! i = l !! S i.
120
Proof. by destruct l. Qed.
121
122
123
124

Lemma list_lookup_Some_In (l : list A) i x : l !! i = Some x  In x l.
Proof.
  revert i. induction l; intros [|i] ?;
125
    simpl; simplify_equality; constructor (solve [eauto]).
126
127
128
129
130
Qed.

Lemma list_lookup_In_Some (l : list A) x : In x l   i, l !! i = Some x.
Proof.
  induction l; destruct 1; subst.
131
132
  * by exists 0.
  * destruct IHl as [i ?]; auto. by exists (S i).
133
134
135
136
Qed.
Lemma list_lookup_In (l : list A) x : In x l   i, l !! i = Some x.
Proof. firstorder eauto using list_lookup_Some_In, list_lookup_In_Some. Qed.

137
Lemma list_lookup_middle (l1 l2 : list A) (x : A) :
138
  (l1 ++ x :: l2) !! length l1 = Some x.
139
Proof. by induction l1; simpl. Qed.
140
141
142
143

Lemma list_lookup_lt_length (l : list A) i : is_Some (l !! i)  i < length l.
Proof.
  revert i. induction l.
144
145
  * split; by inversion 1.
  * intros [|?]; simpl.
146
    + split; auto with arith.
147
    + by rewrite <-NPeano.Nat.succ_lt_mono.
148
149
150
Qed.
Lemma list_lookup_weaken (l l' : list A) i x :
  l !! i = Some x  (l ++ l') !! i = Some x.
151
152
153
154
155
156
157
158
159
Proof. revert i. induction l. done. by intros []. Qed.

Lemma take_lookup i j (l : list A) :
  j < i  take i l !! j = l !! j.
Proof.
  revert i j. induction l; intros [|i] j ?; trivial.
  * by destruct (le_Sn_0 j).
  * destruct j; simpl; auto with arith.
Qed.
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
Lemma take_lookup_le i j (l : list A) :
  i  j  take i l !! j = None.
Proof.
  revert i j. induction l; intros [|i] [|j] ?; trivial.
  * by destruct (le_Sn_0 i).
  * simpl; auto with arith.
Qed.

Lemma drop_lookup i j (l : list A) :
  drop i l !! j = l !! (i + j).
Proof. revert i j. induction l; intros [|i] ?; simpl; auto. Qed.

Lemma list_lookup_alter (f : A  A) i l : alter f i l !! i = f <$> l !! i.
Proof. revert i. induction l. done. intros [|i]. done. apply (IHl i). Qed.
Lemma list_lookup_alter_ne (f : A  A) i j l :
  i  j  alter f i l !! j = l !! j.
Proof.
  revert i j. induction l; [done|].
  intros [|i] [|j] ?; try done. apply (IHl i). congruence.
Qed.

Lemma take_alter (f : A  A) i j l :
  i  j  take i (alter f j l) = take i l.
Proof.
  intros. apply list_eq. intros jj. destruct (le_lt_dec i jj).
  * by rewrite !take_lookup_le.
  * by rewrite !take_lookup, !list_lookup_alter_ne by omega.
Qed.
Lemma take_insert i j (x : A) l :
  i  j  take i (<[j:=x]>l) = take i l.
Proof take_alter _ _ _ _.

Lemma drop_alter (f : A  A) i j l :
  j < i  drop i (alter f j l) = drop i l.
Proof.
  intros. apply list_eq. intros jj.
  by rewrite !drop_lookup, !list_lookup_alter_ne by omega.
Qed.
Lemma drop_insert i j (x : A) l :
  j < i  drop i (<[j:=x]>l) = drop i l.
Proof drop_alter _ _ _ _.

Lemma foldr_permutation {B} (f : A  B  B) (b : B) :
204
  ( a1 a2 b, f a1 (f a2 b) = f a2 (f a1 b)) 
205
  Proper (Permutation ==> (=)) (foldr f b).
206
207
Proof. intro. induction 1; simpl; congruence. Qed.

208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
Lemma Forall_cons_inv (P : A  Prop) x l :
  Forall P (x :: l)  P x  Forall P l.
Proof. by inversion_clear 1. Qed.

Lemma Forall_app (P : A  Prop) l1 l2 :
  Forall P (l1 ++ l2)  Forall P l1  Forall P l2.
Proof.
  split.
   induction l1; inversion 1; intuition.
  intros [H ?]. induction H; simpl; intuition.
Qed.

Lemma Forall_true (P : A  Prop) l :
  ( x, P x)  Forall P l.
Proof. induction l; auto. Qed.
223
224
225
Lemma Forall_impl (P Q : A  Prop) l :
  Forall P l  ( x, P x  Q x)  Forall Q l.
Proof. induction 1; auto. Qed.
226
227
228
229
230
231
Lemma Forall_delete (P : A  Prop) l i :
  Forall P l  Forall P (delete i l).
Proof.
  intros H. revert i.
  by induction H; intros [|i]; try constructor.
Qed.
232
233
234
235
236
237
238
239
240
241

Lemma Forall2_length {B} (P : A  B  Prop) l1 l2 :
  Forall2 P l1 l2  length l1 = length l2.
Proof. induction 1; simpl; auto. Qed.

Lemma Forall2_impl {B} (P Q : A  B  Prop) l1 l2 :
  Forall2 P l1 l2  ( x y, P x y  Q x y)  Forall2 Q l1 l2.
Proof. induction 1; auto. Qed.

Lemma Forall2_unique {B} (P : A  B  Prop) l k1 k2 :
242
243
244
245
246
247
248
  Forall2 P l k1 
  Forall2 P l k2 
  ( x y1 y2, P x y1  P x y2  y1 = y2) 
  k1 = k2.
Proof.
  intros H. revert k2. induction H; inversion_clear 1; intros; f_equal; eauto.
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
249
250

Lemma NoDup_singleton (x : A) : NoDup [x].
251
Proof. constructor. intros []. constructor. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
252
253
254
Lemma NoDup_app (l k : list A) :
  NoDup l  NoDup k  ( x, In x l  ¬In x k)  NoDup (l ++ k).
Proof.
255
  induction 1; simpl.
256
257
  * done.
  * constructor; rewrite ?in_app_iff; firstorder.
Robbert Krebbers's avatar
Robbert Krebbers committed
258
259
260
261
262
263
264
265
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 = [].
266
Proof. destruct l. done. by edestruct 1; constructor. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
267
Lemma nil_length (l : list A) : length l = 0  l = [].
268
Proof. by destruct l. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
269
Lemma NoDup_inv_1 (x : A) (l : list A) : NoDup (x :: l)  ¬In x l.
270
Proof. by inversion_clear 1. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
271
Lemma NoDup_inv_2 (x : A) (l : list A) : NoDup (x :: l)  NoDup l.
272
Proof. by inversion_clear 1. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
273
Lemma Forall_inv_2 (P : A  Prop) x l : Forall P (x :: l)  Forall P l.
274
Proof. by inversion 1. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
275
Lemma Exists_inv (P : A  Prop) x l : Exists P (x :: l)  P x  Exists P l.
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
Proof. inversion 1; intuition trivial. Qed.

Definition reverse (l : list A) : list A := rev_append l [].

Lemma reverse_nill : reverse [] = [].
Proof. done. Qed.
Lemma reverse_cons x l : reverse (x :: l) = reverse l ++ [x].
Proof. unfold reverse. by rewrite <-!rev_alt. Qed.
Lemma reverse_snoc x l : reverse (l ++ [x]) = x :: reverse l.
Proof. unfold reverse. by rewrite <-!rev_alt, rev_unit. Qed.
Lemma reverse_app l1 l2 : reverse (l1 ++ l2) = reverse l2 ++ reverse l1.
Proof. unfold reverse. rewrite <-!rev_alt. apply rev_app_distr. Qed.
Lemma reverse_length l : length (reverse l) = length l.
Proof. unfold reverse. rewrite <-!rev_alt. apply rev_length. Qed.
Lemma reverse_involutive l : reverse (reverse l) = l.
Proof. unfold reverse. rewrite <-!rev_alt. apply rev_involutive. Qed. 
Robbert Krebbers's avatar
Robbert Krebbers committed
292

293
294
Global Instance list_eq_dec {dec :  x y : A, Decision (x = y)} :  l k,
  Decision (l = k) := list_eq_dec dec.
295
Global Instance In_dec {dec :  x y : A, Decision (x = y)} :  x l,
Robbert Krebbers's avatar
Robbert Krebbers committed
296
297
  Decision (In x l) := in_dec dec.

298
299
Global Instance NoDup_dec {dec :  x y : A, Decision (x = y)} :
     (l : list A), Decision (NoDup l) :=
Robbert Krebbers's avatar
Robbert Krebbers committed
300
301
302
303
  fix NoDup_dec l :=
  match l return Decision (NoDup l) with
  | [] => left NoDup_nil
  | x :: l =>
304
    match In_dec x l with
Robbert Krebbers's avatar
Robbert Krebbers committed
305
306
307
308
309
310
311
312
313
    | 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.

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
Section Forall_Exists.
Context (P : A  Prop).

Lemma Exists_not_Forall l : Exists (not  P) l  ¬Forall P l.
Proof. induction 1; inversion_clear 1; contradiction. Qed.

Lemma Forall_not_Exists l : Forall (not  P) l  ¬Exists P l.
Proof. induction 1; inversion_clear 1; contradiction. Qed.

Context {dec :  x, Decision (P x)}.

Fixpoint Forall_Exists_dec l : {Forall P l} + {Exists (not  P) l}.
Proof.
 refine (
  match l with
  | [] => left _
  | x :: l => cast_if_and (dec x) (Forall_Exists_dec l)
  end); clear Forall_Exists_dec; abstract intuition.
Defined.

Lemma not_Forall_Exists l : ¬Forall P l  Exists (not  P) l.
Proof. intro. destruct (Forall_Exists_dec l); intuition. Qed.

Global Instance Forall_dec l : Decision (Forall P l) :=
  match Forall_Exists_dec l with
  | left H => left H
  | right H => right (Exists_not_Forall _ H)
Robbert Krebbers's avatar
Robbert Krebbers committed
341
342
  end.

343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
Fixpoint Exists_Forall_dec l : {Exists P l} + {Forall (not  P) l}.
Proof.
 refine (
  match l with
  | [] => right _
  | x :: l => cast_if_or (dec x) (Exists_Forall_dec l)
  end); clear Exists_Forall_dec; abstract intuition.
Defined.

Lemma not_Exists_Forall l : ¬Exists P l  Forall (not  P) l.
Proof. intro. destruct (Exists_Forall_dec l); intuition. Qed.

Global Instance Exists_dec l : Decision (Exists P l) :=
  match Exists_Forall_dec l with
  | left H => left H
  | right H => right (Forall_not_Exists _ H)
Robbert Krebbers's avatar
Robbert Krebbers committed
359
  end.
360
End Forall_Exists.
361
362
363
364
365
End general_properties.

(** * Theorems on the prefix and suffix predicates *)
Section prefix_postfix.
Context {A : Type}.
Robbert Krebbers's avatar
Robbert Krebbers committed
366

367
Global Instance: PreOrder (@prefix_of A).
Robbert Krebbers's avatar
Robbert Krebbers committed
368
369
Proof.
  split.
370
371
372
  * intros ?. eexists []. by rewrite app_nil_r.
  * intros ??? [k1 ?] [k2 ?].
    exists (k1 ++ k2). subst. by rewrite app_assoc.
Robbert Krebbers's avatar
Robbert Krebbers committed
373
374
Qed.

375
Lemma prefix_of_nil (l : list A) : prefix_of [] l.
376
Proof. by exists l. Qed.
377
Lemma prefix_of_nil_not x (l : list A) : ¬prefix_of (x :: l) [].
378
Proof. by intros [k E]. Qed.
379
380
Lemma prefix_of_cons x y (l1 l2 : list A) :
  x = y  prefix_of l1 l2  prefix_of (x :: l1) (y :: l2).
381
Proof. intros ? [k E]. exists k. by subst. Qed.
382
383
Lemma prefix_of_cons_inv_1 x y (l1 l2 : list A) :
  prefix_of (x :: l1) (y :: l2)  x = y.
384
Proof. intros [k E]. by injection E. Qed.
385
386
Lemma prefix_of_cons_inv_2 x y (l1 l2 : list A) :
  prefix_of (x :: l1) (y :: l2)  prefix_of l1 l2.
387
Proof. intros [k E]. exists k. by injection E. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
388

389
390
Lemma prefix_of_app_l (l1 l2 l3 : list A) :
  prefix_of (l1 ++ l3) l2  prefix_of l1 l2.
391
Proof. intros [k ?]. red. exists (l3 ++ k). subst. by rewrite <-app_assoc. Qed.
392
393
Lemma prefix_of_app_r (l1 l2 l3 : list A) :
  prefix_of l1 l2  prefix_of l1 (l2 ++ l3).
394
Proof. intros [k ?]. exists (k ++ l3). subst. by rewrite app_assoc. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
395

396
397
Global Instance prefix_of_dec `{ x y : A, Decision (x = y)} :
     l1 l2, Decision (prefix_of l1 l2) :=
Robbert Krebbers's avatar
Robbert Krebbers committed
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
  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.

413
Global Instance: PreOrder (@suffix_of A).
Robbert Krebbers's avatar
Robbert Krebbers committed
414
415
Proof.
  split.
416
  * intros ?. by eexists [].
417
  * intros ??? [k1 ?] [k2 ?].
418
    exists (k2 ++ k1). subst. by rewrite app_assoc.
Robbert Krebbers's avatar
Robbert Krebbers committed
419
420
Qed.

421
422
Lemma prefix_suffix_reverse (l1 l2 : list A) :
  prefix_of l1 l2  suffix_of (reverse l1) (reverse l2).
Robbert Krebbers's avatar
Robbert Krebbers committed
423
Proof.
424
425
426
  split; intros [k E]; exists (reverse k).
  * by rewrite E, reverse_app.
  * by rewrite <-(reverse_involutive l2), E, reverse_app, reverse_involutive.
Robbert Krebbers's avatar
Robbert Krebbers committed
427
Qed.
428
429
430
Lemma suffix_prefix_reverse (l1 l2 : list A) :
  suffix_of l1 l2  prefix_of (reverse l1) (reverse l2).
Proof. by rewrite prefix_suffix_reverse, !reverse_involutive. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
431

432
Lemma suffix_of_nil (l : list A) : suffix_of [] l.
433
434
435
436
437
438
439
440
441
442
Proof. exists l. by rewrite app_nil_r. Qed.
Lemma suffix_of_nil_inv (l : list A) : suffix_of l []  l = [].
Proof. by intros [[|?] ?]; simplify_list_equality. Qed.
Lemma suffix_of_cons_nil_inv x (l : list A) : ¬suffix_of (x :: l) [].
Proof. by intros [[] ?]. Qed.

Lemma suffix_of_app (l1 l2 k : list A) :
  suffix_of l1 l2  suffix_of (l1 ++ k) (l2 ++ k).
Proof. intros [k' E]. exists k'. subst. by rewrite app_assoc. Qed.

443
444
Lemma suffix_of_snoc_inv_1 x y (l1 l2 : list A) :
  suffix_of (l1 ++ [x]) (l2 ++ [y])  x = y.
445
Proof.
446
447
  rewrite suffix_prefix_reverse, !reverse_snoc.
  by apply prefix_of_cons_inv_1.
448
Qed.
449
450
Lemma suffix_of_snoc_inv_2 x y (l1 l2 : list A) :
  suffix_of (l1 ++ [x]) (l2 ++ [y])  suffix_of l1 l2.
451
Proof.
452
453
  rewrite !suffix_prefix_reverse, !reverse_snoc.
  by apply prefix_of_cons_inv_2.
454
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
455

456
457
Lemma suffix_of_cons_l (l1 l2 : list A) x :
  suffix_of (x :: l1) l2  suffix_of l1 l2.
458
Proof. intros [k ?]. exists (k ++ [x]). subst. by rewrite <-app_assoc. Qed.
459
460
Lemma suffix_of_app_l (l1 l2 l3 : list A) :
  suffix_of (l3 ++ l1) l2  suffix_of l1 l2.
461
Proof. intros [k ?]. exists (k ++ l3). subst. by rewrite <-app_assoc. Qed.
462
463
Lemma suffix_of_cons_r (l1 l2 : list A) x :
  suffix_of l1 l2  suffix_of l1 (x :: l2).
464
Proof. intros [k ?]. exists (x :: k). by subst. Qed.
465
466
Lemma suffix_of_app_r (l1 l2 l3 : list A) :
  suffix_of l1 l2  suffix_of l1 (l3 ++ l2).
467
Proof. intros [k ?]. exists (l3 ++ k). subst. by rewrite app_assoc. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
468

469
Lemma suffix_of_cons_inv (l1 l2 : list A) x y :
470
471
  suffix_of (x :: l1) (y :: l2) 
    x :: l1 = y :: l2  suffix_of (x :: l1) l2.
Robbert Krebbers's avatar
Robbert Krebbers committed
472
473
Proof.
  intros [[|? k] E].
474
475
  * by left.
  * right. simplify_equality. by apply suffix_of_app_r.
Robbert Krebbers's avatar
Robbert Krebbers committed
476
Qed.
477

478
Lemma suffix_of_cons_not x (l : list A) : ¬suffix_of (x :: l) l.
479
Proof. intros [??]. discriminate_list_equality. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
480

481
482
483
484
485
486
Global Instance suffix_of_dec `{ x y : A, Decision (x = y)} (l1 l2 : list A) :
  Decision (suffix_of l1 l2).
Proof.
  refine (cast_if (decide_rel prefix_of (reverse l1) (reverse l2)));
   abstract (by rewrite suffix_prefix_reverse).
Defined.
487
End prefix_postfix.
Robbert Krebbers's avatar
Robbert Krebbers committed
488

489
490
(** The [simplify_suffix_of] removes [suffix_of] hypotheses that are
tautologies, and simplifies [suffix_of] hypotheses involving [(::)] and
491
[(++)]. *)
Robbert Krebbers's avatar
Robbert Krebbers committed
492
493
Ltac simplify_suffix_of := repeat
  match goal with
494
495
496
  | H : suffix_of (_ :: _) _ |- _ =>
    destruct (suffix_of_cons_not _ _ H)
  | H : suffix_of (_ :: _) [] |- _ =>
497
    apply suffix_of_nil_inv in H
498
499
  | H : suffix_of (_ :: _) (_ :: _) |- _ =>
    destruct (suffix_of_cons_inv _ _ _ _ H); clear H
Robbert Krebbers's avatar
Robbert Krebbers committed
500
501
502
  | H : suffix_of ?x ?x |- _ => clear H
  | H : suffix_of ?x (_ :: ?x) |- _ => clear H
  | H : suffix_of ?x (_ ++ ?x) |- _ => clear H
503
  | _ => progress simplify_equality
Robbert Krebbers's avatar
Robbert Krebbers committed
504
505
  end.

506
(** The [solve_suffix_of] tries to solve goals involving [suffix_of]. It uses
507
508
509
[simplify_suffix_of] to simplify hypotheses and tries to solve [suffix_of]
conclusions. This tactic either fails or proves the goal. *)
Ltac solve_suffix_of := solve [intuition (repeat
510
  match goal with
511
512
  | _ => done
  | _ => progress simplify_suffix_of
513
514
  | |- suffix_of [] _ => apply suffix_of_nil
  | |- suffix_of _ _ => reflexivity
515
516
517
518
  | |- suffix_of _ (_ :: _) => apply suffix_of_cons_r
  | |- suffix_of _ (_ ++ _) => apply suffix_of_app_r
  | H : suffix_of _ _  False |- _ => destruct H
  end)].
519
520
Hint Extern 0 (PropHolds (suffix_of _ _)) =>
  unfold PropHolds; solve_suffix_of : typeclass_instances.
Robbert Krebbers's avatar
Robbert Krebbers committed
521

522
(** * Monadic operations *)
523
524
Global Instance list_fmap {A B} (f : A  B) : FMap list f :=
  fix go (l : list A) :=
Robbert Krebbers's avatar
Robbert Krebbers committed
525
526
  match l with
  | [] => []
527
  | x :: l => f x :: @fmap _ _ _ f go l
Robbert Krebbers's avatar
Robbert Krebbers committed
528
  end.
529
530
Global Instance list_join {A} : MJoin list :=
  fix go (l : list (list A)) : list A :=
Robbert Krebbers's avatar
Robbert Krebbers committed
531
532
  match l with
  | [] =>  []
533
  | x :: l => x ++ @mjoin _ _ go l
Robbert Krebbers's avatar
Robbert Krebbers committed
534
  end.
535
536
Global Instance list_bind {A B} (f : A  list B) : MBind list f := λ l,
  mjoin (f <$> l).
Robbert Krebbers's avatar
Robbert Krebbers committed
537

538
539
Section list_fmap.
  Context {A B : Type} (f : A  B).
Robbert Krebbers's avatar
Robbert Krebbers committed
540

541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
  Global Instance: Injective (=) (=) f  Injective (=) (=) (fmap f).
  Proof.
    intros ? l1. induction l1 as [|x l1 IH].
    * by intros [|??].
    * intros [|??]; [done |]; simpl; intros; simplify_equality.
      by f_equal; [apply (injective f) | auto].
  Qed.
  Lemma fmap_app l1 l2 : f <$> l1 ++ l2 = (f <$> l1) ++ (f <$> l2).
  Proof. induction l1; simpl; by f_equal. Qed.
  Lemma fmap_cons_inv y l k :
    f <$> l = y :: k   x l', y = f x  l = x :: l'.
  Proof. intros. destruct l; simpl; simplify_equality; eauto. Qed.
  Lemma fmap_app_inv l k1 k2 :
    f <$> l = k1 ++ k2   l1 l2, k1 = f <$> l1  k2 = f <$> l2  l = l1 ++ l2.
  Proof.
    revert l. induction k1 as [|y k1 IH]; simpl.
    * intros l ?. by eexists [], l.
    * intros [|x l] ?; simpl; simplify_equality.
      destruct (IH l) as [l1 [l2 [? [??]]]]; subst; [done |].
      by exists (x :: l1) l2.
  Qed.
562

563
  Lemma fmap_length l : length (f <$> l) = length l.
564
565
566
567
568
569
  Proof. induction l; simpl; by f_equal. Qed.
  Lemma fmap_reverse l : f <$> reverse l = reverse (f <$> l).
  Proof.
    induction l; simpl; [done |].
    by rewrite !reverse_cons, fmap_app, IHl.
  Qed.
570
571

  Lemma list_lookup_fmap l i : (f <$> l) !! i = f <$> (l !! i).
572
  Proof. revert i. induction l; by intros [|]. Qed.
573
574
575
576

  Lemma in_fmap_1 l x : In x l  In (f x) (f <$> l).
  Proof. induction l; destruct 1; subst; constructor (solve [auto]). Qed.
  Lemma in_fmap_1_alt l x y : In x l  y = f x  In y (f <$> l).
577
  Proof. intros. subst. by apply in_fmap_1. Qed.
578
579
580
  Lemma in_fmap_2 l x : In x (f <$> l)   y, x = f y  In y l.
  Proof.
    induction l as [|y l]; destruct 1; subst.
581
582
    * exists y; by intuition.
    * destruct IHl as [y' [??]]. done. exists y'; intuition.
583
584
  Qed.
  Lemma in_fmap l x : In x (f <$> l)   y, x = f y  In y l.
Robbert Krebbers's avatar
Robbert Krebbers committed
585
  Proof.
586
587
588
    split.
    * apply in_fmap_2.
    * intros [? [??]]. eauto using in_fmap_1_alt.
Robbert Krebbers's avatar
Robbert Krebbers committed
589
  Qed.
590
591
592
593

  Lemma Forall_fmap (l : list A) (P : B  Prop) :
    Forall (P  f) l  Forall P (f <$> l).
  Proof. induction l; split; inversion_clear 1; constructor; firstorder auto. Qed.
594
595
End list_fmap.

596
597
598
599
600
601
602
603
604
605
Ltac simplify_list_fmap_equality := repeat
  match goal with
  | _ => progress simplify_equality
  | H : _ <$> _ = _ :: _ |- _ =>
    apply fmap_cons_inv in H; destruct H as [? [? [??]]]
  | H : _ :: _ = _ <$> _ |- _ => symmetry in H
  | H : _ <$> _ = _ ++ _ |- _ =>
    apply fmap_app_inv in H; destruct H as [? [? [? [??]]]]
  | H : _ ++ _ = _ <$> _ |- _ => symmetry in H
  end.
606

607
608
609
(** * Indexed folds and maps *)
(** We define stronger variants of map and fold that also take the index of the
element into account. *)
610
611
612
613
614
615
616
Definition imap_go {A B} (f : nat  A  B) : nat  list A  list B :=
  fix go (n : nat) (l : list A) :=
  match l with
  | [] => []
  | x :: l => f n x :: go (S n) l
  end.
Definition imap {A B} (f : nat  A  B) : list A  list B := imap_go f 0.
Robbert Krebbers's avatar
Robbert Krebbers committed
617

618
Definition ifoldr {A B} (f : nat  B  A  A)
619
    (a : nat  A) : nat  list B  A :=
620
621
622
623
624
  fix go (n : nat) (l : list B) : A :=
  match l with
  | nil => a n
  | b :: l => f n b (go (S n) l)
  end.
Robbert Krebbers's avatar
Robbert Krebbers committed
625

626
Lemma ifoldr_app {A B} (f : nat  B  A  A) (a : nat  A)
627
    (l1 l2 : list B) n :
628
  ifoldr f a n (l1 ++ l2) = ifoldr f (λ n, ifoldr f a n l2) n l1.
629
630
631
Proof.
  revert n a. induction l1 as [| b l1 IH ]; intros; simpl; f_equal; auto.
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
632

633
634
635
(** * Lists of the same length *)
(** The [same_length] view allows convenient induction over two lists with the
same length. *)
636
637
Section same_length.
  Context {A B : Type}.
Robbert Krebbers's avatar
Robbert Krebbers committed
638

639
640
641
642
643
644
645
  Inductive same_length : list A  list B  Prop :=
    | same_length_nil : same_length [] []
    | same_length_cons x y l k :
      same_length l k  same_length (x :: l) (y :: k).

  Lemma same_length_length l k :
    same_length l k  length l = length k.
Robbert Krebbers's avatar
Robbert Krebbers committed
646
  Proof.
647
648
649
650
    split.
    * induction 1; simpl; auto.
    * revert k. induction l; intros [|??]; try discriminate;
      constructor; auto with arith.
Robbert Krebbers's avatar
Robbert Krebbers committed
651
652
  Qed.

653
654
  Lemma same_length_lookup l k i :
    same_length l k  is_Some (l !! i)  is_Some (k !! i).
Robbert Krebbers's avatar
Robbert Krebbers committed
655
  Proof.
656
657
    rewrite same_length_length.
    setoid_rewrite list_lookup_lt_length.
658
    intros E. by rewrite E.
Robbert Krebbers's avatar
Robbert Krebbers committed
659
  Qed.
660
661
662
663
664

  Lemma Forall2_app_inv (P : A  B  Prop) l1 l2 k1 k2 :
    same_length l1 k1 
    Forall2 P (l1 ++ l2) (k1 ++ k2)  Forall2 P l2 k2.
  Proof. induction 1. done. inversion 1; subst; auto. Qed.
665
End same_length.
Robbert Krebbers's avatar
Robbert Krebbers committed
666

667
668
669
Instance:  A, Reflexive (@same_length A A).
Proof. intros A l. induction l; try constructor; auto. Qed.

670
(** * Zipping lists *)
671
672
673
674
675
676
677
678
Definition zip_with {A B C} (f : A  B  C) : list A  list B  list C :=
  fix go l1 l2 :=
  match l1, l2 with
  | x1 :: l1, x2 :: l2 => f x1 x2 :: go l1 l2
  | _ , _ => []
  end.

Notation zip := (zip_with pair).
Robbert Krebbers's avatar
Robbert Krebbers committed
679

680
681
682
683
684
685
686
687
688
689
690
691
692
693
Section zip.
  Context {A B : Type}.

  Lemma zip_fst_le (l1 : list A) (l2 : list B) :
    length l1  length l2  fst <$> zip l1 l2 = l1.
  Proof.
    revert l2.
    induction l1; intros [|??] ?; simpl; f_equal; auto with arith.
    edestruct Le.le_Sn_0; eauto.
  Qed.
  Lemma zip_fst (l1 : list A) (l2 : list B) :
    same_length l1 l2  fst <$> zip l1 l2 = l1.
  Proof.
    rewrite same_length_length. intros H.
694
    apply zip_fst_le. by rewrite H.
695
696
697
698
699
700
701
702
703
704
705
706
707
  Qed.

  Lemma zip_snd_le (l1 : list A) (l2 : list B) :
    length l2  length l1  snd <$> zip l1 l2 = l2.
  Proof.
    revert l2.
    induction l1; intros [|??] ?; simpl; f_equal; auto with arith.
    edestruct Le.le_Sn_0; eauto.
  Qed.
  Lemma zip_snd (l1 : list A) (l2 : list B) :
    same_length l1 l2  snd <$> zip l1 l2 = l2.
  Proof.
    rewrite same_length_length. intros H.
708
    apply zip_snd_le. by rewrite H.
709
710
  Qed.
End zip.
711
712
713
714
715
716
717
718
719
720
721
722
723
724
725
726
727
728
729
730
731
732
733
734
735
736
737
738
739
740
741
742
743
744
745
746
747
748
749
750
751
752
753
754
755
756
757
758
759
760
761
762
763
764

Definition zipped_map {A B} (f : list A  list A  A  B) :
    list A  list A  list B :=
  fix go l k :=
  match k with
  | [] => []
  | x :: k => f l k x :: go (x :: l) k
  end.

Lemma In_zipped_map {A B} (f : list A  list A  A  B) l k x :
  In x (zipped_map f l k) 
     k' k'' y, k = k' ++ [y] ++ k''  x = f (reverse k' ++ l) k'' y.
Proof.
  split.
  * revert l. induction k as [|z k IH]; [done | intros l [?|?]]; subst.
    + by eexists [], k, z.
    + destruct (IH (z :: l)) as [k' [k'' [y [??]]]]; [done |]; subst.
      eexists (z :: k'), k'', y. split; [done |].
      by rewrite reverse_cons, <-app_assoc.
  * intros [k' [k'' [y [??]]]]; subst.
    revert l. induction k' as [|z k' IH]; intros l.
    + by left.
    + right. by rewrite reverse_cons, <-!app_assoc.
Qed.

Section zipped_list_ind.
  Context {A} (P : list A  list A  Prop).
  Context (Pnil :  l, P l []).
  Context (Pcons :  l k x, P (x :: l) k  P l (x :: k)).

  Fixpoint zipped_list_ind l k : P l k :=
    match k with
    | [] => Pnil _
    | x :: k => Pcons _ _ _ (zipped_list_ind (x :: l) k)
    end.
End zipped_list_ind.

Inductive zipped_Forall {A} (P : list A  list A  A  Prop) :
    list A  list A  Prop :=
  | zipped_Forall_nil l : zipped_Forall P l []
  | zipped_Forall_cons l k x :
     P l k x 
     zipped_Forall P (x :: l) k 
     zipped_Forall P l (x :: k).
Arguments zipped_Forall_nil {_ _} _.
Arguments zipped_Forall_cons {_ _} _ _ _ _ _.

Lemma zipped_Forall_app {A} (P : list A  list A  A  Prop) l k k' :
  zipped_Forall P l (k ++ k')  zipped_Forall P (reverse k ++ l) k'.
Proof.
  revert l. induction k as [|x k IH]; simpl; [done |].
  inversion_clear 1. rewrite reverse_cons, <-app_assoc.
  by apply IH.
Qed.