list.v 18.7 KB
Newer Older
1 2 3 4 5
(* 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. *)
Require Import Permutation.
Robbert Krebbers's avatar
Robbert Krebbers committed
6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21
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.

22 23
(** * General definitions *)
(** Looking up elements and updating elements in a list. *)
24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45
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.

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.

46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67
(** The [simpl] tactic does not simplify [list_lookup] as it is wrapped into
an operational type class and we cannot let it unfold on a per instance basis.
Therefore we use the [simplify_list_lookup] tactic to perform these
simplifications. Bug: it does not unfold under binders. *)
Ltac simplify_list_lookup := repeat
  match goal with
  | |- context C [@nil ?A !! _] =>
    let X := (context C [@None A]) in change X
  | |- context C [(?x :: _) !! 0] =>
    let X := (context C [Some x]) in change X
  | |- context C [(_ :: ?l) !! S ?i] =>
    let X := (context C [l !! i]) in change X
  | H : context C [@nil ?A !! _] |- _ =>
    let X := (context C [@None A]) in change X in H
  | H : context C [(?x :: _) !! 0] |- _ =>
    let X := (context C [Some x]) in change X in H
  | H : context C [(_ :: ?l) !! S ?i] |- _  =>
    let X := (context C [l !! i]) in change X in H
  end.

(** The function [option_list] converts an element of the option type into
a list. *)
68
Definition option_list {A} : option A  list A := option_rect _ (λ x, [x]) [].
69 70 71

(** 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. *)
72 73 74
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.

75 76
(** * General theorems *)
Section general_properties.
Robbert Krebbers's avatar
Robbert Krebbers committed
77 78
Context {A : Type}.

79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95
Lemma list_eq (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_nil i : @nil A !! i = None.
Proof. now destruct i. Qed.
Lemma list_lookup_tail (l : list A) i : tail l !! i = l !! S i.
Proof. now destruct l. Qed.

Lemma list_lookup_Some_In (l : list A) i x : l !! i = Some x  In x l.
Proof.
  revert i. induction l; intros [|i] ?;
96
    simplify_list_lookup; simplify_equality; constructor (solve [eauto]).
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
Qed.

Lemma list_lookup_In_Some (l : list A) x : In x l   i, l !! i = Some x.
Proof.
  induction l; destruct 1; subst.
  * now exists 0.
  * destruct IHl as [i ?]; auto. now exists (S i).
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.

Lemma list_lookup_app_length (l1 l2 : list A) (x : A) :
  (l1 ++ x :: l2) !! length l1 = Some x.
Proof. induction l1; simpl; now simplify_list_lookup. Qed.

Lemma list_lookup_lt_length (l : list A) i : is_Some (l !! i)  i < length l.
Proof.
  revert i. induction l.
  * split; now inversion 1.
  * intros [|?]; simplify_list_lookup; simpl.
    + split; auto with arith.
    + now rewrite <-NPeano.Nat.succ_lt_mono.
Qed.
Lemma list_lookup_weaken (l l' : list A) i x :
  l !! i = Some x  (l ++ l') !! i = Some x.
Proof. revert i. induction l. discriminate. now intros []. Qed.

124 125 126 127 128
Lemma fold_right_permutation {B} (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. intro. induction 1; simpl; congruence. Qed.

129 130 131 132 133 134 135 136 137 138 139 140 141
Lemma Forall_impl (P Q : A  Prop) l :
  Forall P l  ( x, P x  Q x)  Forall Q l.
Proof. induction 1; auto. Qed.

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 :
142 143 144 145 146 147 148
  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
149 150 151 152 153 154

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.
155 156 157
  induction 1; simpl.
  * easy.
  * constructor. rewrite in_app_iff. firstorder. firstorder.
Robbert Krebbers's avatar
Robbert Krebbers committed
158 159 160 161 162 163 164 165 166 167 168 169 170 171 172 173 174 175 176 177
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.

178 179
Global Instance list_eq_dec {dec :  x y : A, Decision (x = y)} :  l k,
  Decision (l = k) := list_eq_dec dec.
Robbert Krebbers's avatar
Robbert Krebbers committed
180 181 182
Global Instance list_in_dec {dec :  x y : A, Decision (x = y)} :  x l,
  Decision (In x l) := in_dec dec.

183 184
Global Instance NoDup_dec {dec :  x y : A, Decision (x = y)} :
     (l : list A), Decision (NoDup l) :=
Robbert Krebbers's avatar
Robbert Krebbers committed
185 186 187 188 189 190 191 192 193 194 195 196 197 198
  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.

199 200
Global Instance Forall_dec (P : A  Prop) {dec :  x, Decision (P x)} :
     l, Decision (Forall P l) :=
Robbert Krebbers's avatar
Robbert Krebbers committed
201 202 203 204 205 206 207 208 209 210 211 212 213 214
  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.

215 216
Global Instance Exists_dec (P : A  Prop) {dec :  x, Decision (P x)} :
     l, Decision (Exists P l) :=
Robbert Krebbers's avatar
Robbert Krebbers committed
217 218 219 220 221 222 223 224 225 226 227 228 229
  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.
230 231 232 233 234
End general_properties.

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

236
Global Instance: PreOrder (@prefix_of A).
Robbert Krebbers's avatar
Robbert Krebbers committed
237 238 239 240 241 242
Proof.
  split.
   intros ?. eexists []. now rewrite app_nil_r.
  intros ??? [k1 ?] [k2 ?]. exists (k1 ++ k2). subst. now rewrite app_assoc.
Qed.

243
Lemma prefix_of_nil (l : list A) : prefix_of [] l.
Robbert Krebbers's avatar
Robbert Krebbers committed
244
Proof. now exists l. Qed.
245
Lemma prefix_of_nil_not x (l : list A) : ¬prefix_of (x :: l) [].
Robbert Krebbers's avatar
Robbert Krebbers committed
246
Proof. intros [k E]. discriminate. Qed.
247 248
Lemma prefix_of_cons x y (l1 l2 : list A) :
  x = y  prefix_of l1 l2  prefix_of (x :: l1) (y :: l2).
Robbert Krebbers's avatar
Robbert Krebbers committed
249
Proof. intros ? [k E]. exists k. now subst. Qed.
250 251
Lemma prefix_of_cons_inv_1 x y (l1 l2 : list A) :
  prefix_of (x :: l1) (y :: l2)  x = y.
Robbert Krebbers's avatar
Robbert Krebbers committed
252
Proof. intros [k E]. now injection E. Qed.
253 254
Lemma prefix_of_cons_inv_2 x y (l1 l2 : list A) :
  prefix_of (x :: l1) (y :: l2)  prefix_of l1 l2.
Robbert Krebbers's avatar
Robbert Krebbers committed
255 256
Proof. intros [k E]. exists k. now injection E. Qed.

257 258
Lemma prefix_of_app_l (l1 l2 l3 : list A) :
  prefix_of (l1 ++ l3) l2  prefix_of l1 l2.
Robbert Krebbers's avatar
Robbert Krebbers committed
259
Proof. intros [k ?]. red. exists (l3 ++ k). subst. now rewrite <-app_assoc. Qed.
260 261
Lemma prefix_of_app_r (l1 l2 l3 : list A) :
  prefix_of l1 l2  prefix_of l1 (l2 ++ l3).
Robbert Krebbers's avatar
Robbert Krebbers committed
262 263
Proof. intros [k ?]. exists (k ++ l3). subst. now rewrite app_assoc. Qed.

264 265
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
266 267 268 269 270 271 272 273 274 275 276 277 278 279 280
  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.

281
Global Instance: PreOrder (@suffix_of A).
Robbert Krebbers's avatar
Robbert Krebbers committed
282 283
Proof.
  split.
284 285 286
  * intros ?. now eexists [].
  * intros ??? [k1 ?] [k2 ?].
    exists (k2 ++ k1). subst. now rewrite app_assoc.
Robbert Krebbers's avatar
Robbert Krebbers committed
287 288
Qed.

289 290
Lemma prefix_suffix_rev (l1 l2 : list A) :
  prefix_of l1 l2  suffix_of (rev l1) (rev l2).
Robbert Krebbers's avatar
Robbert Krebbers committed
291 292
Proof.
  split; intros [k E]; exists (rev k).
293 294
  * now rewrite E, rev_app_distr.
  * now rewrite <-(rev_involutive l2), E, rev_app_distr, rev_involutive.
Robbert Krebbers's avatar
Robbert Krebbers committed
295
Qed.
296 297
Lemma suffix_prefix_rev (l1 l2 : list A) :
  suffix_of l1 l2  prefix_of (rev l1) (rev l2).
Robbert Krebbers's avatar
Robbert Krebbers committed
298 299
Proof. now rewrite prefix_suffix_rev, !rev_involutive. Qed.

300
Lemma suffix_of_nil (l : list A) : suffix_of [] l.
Robbert Krebbers's avatar
Robbert Krebbers committed
301
Proof. exists l. now rewrite app_nil_r. Qed.
302
Lemma suffix_of_nil_not x (l : list A) : ¬suffix_of (x :: l) [].
Robbert Krebbers's avatar
Robbert Krebbers committed
303
Proof. intros [[] ?]; discriminate. Qed.
304 305
Lemma suffix_of_cons x y (l1 l2 : list A) :
  x = y  suffix_of l1 l2  suffix_of (l1 ++ [x]) (l2 ++ [y]).
Robbert Krebbers's avatar
Robbert Krebbers committed
306
Proof. intros ? [k E]. exists k. subst. now rewrite app_assoc. Qed.
307 308
Lemma suffix_of_snoc_inv_1 x y (l1 l2 : list A) :
  suffix_of (l1 ++ [x]) (l2 ++ [y])  x = y.
309 310 311
Proof.
  rewrite suffix_prefix_rev, !rev_unit. now apply prefix_of_cons_inv_1.
Qed.
312 313
Lemma suffix_of_snoc_inv_2 x y (l1 l2 : list A) :
  suffix_of (l1 ++ [x]) (l2 ++ [y])  suffix_of l1 l2.
314 315 316
Proof.
  rewrite !suffix_prefix_rev, !rev_unit. now apply prefix_of_cons_inv_2.
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
317

318 319
Lemma suffix_of_cons_l (l1 l2 : list A) x :
  suffix_of (x :: l1) l2  suffix_of l1 l2.
Robbert Krebbers's avatar
Robbert Krebbers committed
320
Proof. intros [k ?]. exists (k ++ [x]). subst. now rewrite <-app_assoc. Qed.
321 322
Lemma suffix_of_app_l (l1 l2 l3 : list A) :
  suffix_of (l3 ++ l1) l2  suffix_of l1 l2.
Robbert Krebbers's avatar
Robbert Krebbers committed
323
Proof. intros [k ?]. exists (k ++ l3). subst. now rewrite <-app_assoc. Qed.
324 325
Lemma suffix_of_cons_r (l1 l2 : list A) x :
  suffix_of l1 l2  suffix_of l1 (x :: l2).
Robbert Krebbers's avatar
Robbert Krebbers committed
326
Proof. intros [k ?]. exists (x :: k). now subst. Qed.
327 328
Lemma suffix_of_app_r (l1 l2 l3 : list A) :
  suffix_of l1 l2  suffix_of l1 (l3 ++ l2).
Robbert Krebbers's avatar
Robbert Krebbers committed
329 330
Proof. intros [k ?]. exists (l3 ++ k). subst. now rewrite app_assoc. Qed.

331
Lemma suffix_of_cons_inv (l1 l2 : list A) x y :
Robbert Krebbers's avatar
Robbert Krebbers committed
332 333 334 335
  suffix_of (x :: l1) (y :: l2)  x :: l1 = y :: l2  suffix_of (x :: l1) l2.
Proof.
  intros [[|? k] E].
   now left.
336
  right. simplify_equality. now apply suffix_of_app_r.
Robbert Krebbers's avatar
Robbert Krebbers committed
337
Qed.
338
Lemma suffix_of_cons_not x (l : list A) : ¬suffix_of (x :: l) l.
Robbert Krebbers's avatar
Robbert Krebbers committed
339 340 341
Proof.
  intros [k E]. change ([] ++ l = k ++ [x] ++ l) in E.
  rewrite app_assoc in E. apply app_inv_tail in E.
342
  destruct k; simplify_equality.
Robbert Krebbers's avatar
Robbert Krebbers committed
343 344
Qed.

345 346
Global Program Instance suffix_of_dec `{ x y : A, Decision (x = y)} l1 l2 :
    Decision (suffix_of l1 l2) :=
Robbert Krebbers's avatar
Robbert Krebbers committed
347 348 349 350 351
  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.
352 353
Next Obligation.
  intro. destruct Hpre. rewrite <-!rev_alt.
354 355
  now apply suffix_prefix_rev.
Qed.
356
End prefix_postfix.
Robbert Krebbers's avatar
Robbert Krebbers committed
357

358 359 360
(** The [simplify_suffix_of] removes [suffix_of] assumptions that are
tautologies, and simplifies [suffix_of] assumptions involving [(::)] and
[(++)]. *)
Robbert Krebbers's avatar
Robbert Krebbers committed
361 362
Ltac simplify_suffix_of := repeat
  match goal with
363 364 365 366
  | H : suffix_of (_ :: _) _ |- _ =>
    destruct (suffix_of_cons_not _ _ H)
  | H : suffix_of (_ :: _) [] |- _ =>
    destruct (suffix_of_nil_not _ _ H)
367 368
  | H : suffix_of (_ :: _) (_ :: _) |- _ =>
    destruct (suffix_of_cons_inv _ _ _ _ H); clear H
Robbert Krebbers's avatar
Robbert Krebbers committed
369 370 371
  | H : suffix_of ?x ?x |- _ => clear H
  | H : suffix_of ?x (_ :: ?x) |- _ => clear H
  | H : suffix_of ?x (_ ++ ?x) |- _ => clear H
372
  | _ => progress simplify_equality
Robbert Krebbers's avatar
Robbert Krebbers committed
373 374
  end.

375 376 377 378 379 380
(** The [solve_suffix_of] tries to solve goals involving [suffix_of]. It uses
[simplify_suffix_of] to simplify assumptions, tries to solve [suffix_of]
conclusions, and adds transitive consequences of assumptions to the context. 
This tactic either fails or proves the goal. *)
Ltac solve_suffix_of :=
  let rec go :=
381
  match goal with
382 383 384 385 386 387 388
  | _ => progress simplify_suffix_of; go
  | |- suffix_of [] _ => apply suffix_of_nil
  | |- suffix_of _ _ => reflexivity
  | |- suffix_of _ _ => solve [auto]
  | |- suffix_of _ (_ :: _) => apply suffix_of_cons_r; go
  | |- suffix_of _ (_ ++ _) => apply suffix_of_app_r; go
  | H : ¬suffix_of _ _ |- _ => destruct H; go
389 390
  | H1 : suffix_of ?x ?y, H2 : suffix_of ?y ?z |- _ =>
     match goal with
391
     | _ : suffix_of x z |- _ => fail 1
392
     | _ => assert (suffix_of x z) by (transitivity y; assumption);
393
            clear H1; clear H2; go (**i clear to avoid loops *)
394
     end
395 396 397
  end in go.
Hint Extern 0 (PropHolds (suffix_of _ _)) =>
  unfold PropHolds; solve_suffix_of : typeclass_instances.
Robbert Krebbers's avatar
Robbert Krebbers committed
398

399
(** * Monadic operations *)
Robbert Krebbers's avatar
Robbert Krebbers committed
400 401 402 403 404 405 406
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.
407
Global Instance list_join: MJoin list :=
Robbert Krebbers's avatar
Robbert Krebbers committed
408 409 410 411 412 413 414
  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).

415 416
Section list_fmap.
  Context {A B : Type} (f : A  B).
Robbert Krebbers's avatar
Robbert Krebbers committed
417

418 419
  Local Arguments fmap _ _ _ _ _ !_ /.

420 421 422 423 424 425 426 427 428 429 430 431 432 433 434 435 436
  Lemma fmap_length l : length (f <$> l) = length l.
  Proof. induction l; simpl; auto. Qed.

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

  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).
  Proof. intros. subst. now apply in_fmap_1. Qed.
  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.
    * exists y; now intuition.
    * destruct IHl as [y' [??]]. easy. exists y'; now intuition.
  Qed.
  Lemma in_fmap l x : In x (f <$> l)   y, x = f y  In y l.
Robbert Krebbers's avatar
Robbert Krebbers committed
437
  Proof.
438 439 440
    split.
    * apply in_fmap_2.
    * intros [? [??]]. eauto using in_fmap_1_alt.
Robbert Krebbers's avatar
Robbert Krebbers committed
441
  Qed.
442 443 444 445 446 447 448 449 450
End list_fmap.

Lemma Forall_fst {A B} (l : list (A * B)) (P : A  Prop) :
  Forall (P  fst) l  Forall P (fst <$> l).
Proof. induction l; split; inversion 1; subst; constructor; firstorder auto. Qed.
Lemma Forall_snd {A B} (l : list (A * B)) (P : B  Prop) :
  Forall (P  snd) l  Forall P (snd <$> l).
Proof. induction l; split; inversion 1; subst; constructor; firstorder auto. Qed.

451 452 453
(** * Indexed folds and maps *)
(** We define stronger variants of map and fold that also take the index of the
element into account. *)
454 455 456 457 458 459 460
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
461

462 463
Definition ifold_right {A B} (f : nat  B  A  A)
    (a : nat  A) : nat  list B  A :=
464 465 466 467 468
  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
469

470 471
Lemma ifold_right_app {A B} (f : nat  B  A  A) (a : nat  A)
    (l1 l2 : list B) n :
472
  ifold_right f a n (l1 ++ l2) = ifold_right f (λ n, ifold_right f a n l2) n l1.
473 474 475
Proof.
  revert n a. induction l1 as [| b l1 IH ]; intros; simpl; f_equal; auto.
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
476

477 478 479
(** * Lists of the same length *)
(** The [same_length] view allows convenient induction over two lists with the
same length. *)
480 481
Section same_length.
  Context {A B : Type}.
Robbert Krebbers's avatar
Robbert Krebbers committed
482

483 484 485 486 487 488 489
  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
490
  Proof.
491 492 493 494
    split.
    * induction 1; simpl; auto.
    * revert k. induction l; intros [|??]; try discriminate;
      constructor; auto with arith.
Robbert Krebbers's avatar
Robbert Krebbers committed
495 496
  Qed.

497 498
  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
499
  Proof.
500 501 502
    rewrite same_length_length.
    setoid_rewrite list_lookup_lt_length.
    intros E. now rewrite E.
Robbert Krebbers's avatar
Robbert Krebbers committed
503
  Qed.
504
End same_length.
Robbert Krebbers's avatar
Robbert Krebbers committed
505

506 507 508
(** * Zipping lists *)
(** Since we prefer Haskell style naming, we rename the standard library's
implementation [combine] into [zip] using a notation. *)
509
Notation zip := combine.
Robbert Krebbers's avatar
Robbert Krebbers committed
510

511 512 513
Section zip.
  Context {A B : Type}.

514 515
  Local Arguments fmap _ _ _ _ _ !_ /.

516 517 518 519 520 521 522 523 524 525 526 527 528 529 530 531 532 533 534 535 536 537 538 539 540 541 542 543
  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.
    apply zip_fst_le. now rewrite H.
  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.
    apply zip_snd_le. now rewrite H.
  Qed.
End zip.