list.v 72.3 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. *)
Robbert Krebbers's avatar
Robbert Krebbers committed
5

6 7
Require Import Permutation.
Require Export base decidable option numbers.
Robbert Krebbers's avatar
Robbert Krebbers committed
8

9
Arguments length {_} _.
Robbert Krebbers's avatar
Robbert Krebbers committed
10 11 12
Arguments cons {_} _ _.
Arguments app {_} _ _.
Arguments Permutation {_} _ _.
13
Arguments Forall_cons {_} _ _ _ _ _.
Robbert Krebbers's avatar
Robbert Krebbers committed
14

Robbert Krebbers's avatar
Robbert Krebbers committed
15 16 17
Notation Forall_nil_2 := Forall_nil.
Notation Forall_cons_2 := Forall_cons.

18 19 20
Notation tail := tl.
Notation take := firstn.
Notation drop := skipn.
21
Notation take_drop := firstn_skipn.
22 23 24
Arguments take {_} !_ !_ /.
Arguments drop {_} !_ !_ /.

Robbert Krebbers's avatar
Robbert Krebbers committed
25 26 27 28 29 30 31
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.

32
(** * General definitions *)
Robbert Krebbers's avatar
Robbert Krebbers committed
33 34
(** Looking up, updating, and deleting elements of a list. *)
Instance list_lookup {A} : Lookup nat A (list A) :=
35
  fix go (i : nat) (l : list A) {struct l} : option A :=
36 37 38 39 40
  match l with
  | [] => None
  | x :: l =>
    match i with
    | 0 => Some x
41
    | S i => @lookup _ _ _ go i l
42 43
    end
  end.
Robbert Krebbers's avatar
Robbert Krebbers committed
44
Instance list_alter {A} (f : A  A) : AlterD nat A (list A) f :=
45
  fix go (i : nat) (l : list A) {struct l} :=
46 47 48 49 50
  match l with
  | [] => []
  | x :: l =>
    match i with
    | 0 => f x :: l
51
    | S i => x :: @alter _ _ _ f go i l
52 53
    end
  end.
54 55
Instance list_delete {A} : Delete nat (list A) :=
  fix go (i : nat) (l : list A) {struct l} : list A :=
56 57 58 59 60
  match l with
  | [] => []
  | x :: l =>
    match i with
    | 0 => l
61
    | S i => x :: @delete _ _ go i l
62
    end
63
  end.
Robbert Krebbers's avatar
Robbert Krebbers committed
64
Instance list_insert {A} : Insert nat A (list A) := λ i x,
65
  alter (λ _, x) i.
66

Robbert Krebbers's avatar
Robbert Krebbers committed
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
(** The function [option_list] converts an element of the option type into
a list. *)
Definition option_list {A} : option A  list A := option_rect _ (λ x, [x]) [].

(** The function [filter P l] returns the list of elements of [l] that
satisfies [P]. The order remains unchanged. *)
Instance list_filter {A} : Filter A (list A) :=
  fix go P _ l :=
  match l with
  | [] => []
  | x :: l =>
     if decide (P x)
     then x :: @filter _ _ (@go) _ _ l
     else @filter _ _ (@go) _ _ l
  end.

(** The function [replicate n x] generates a list with length [n] of elements
with value [x]. *)
Fixpoint replicate {A} (n : nat) (x : A) : list A :=
  match n with
  | 0 => []
  | S n => x :: replicate n x
  end.

(** The function [reverse l] returns the elements of [l] in reverse order. *)
Definition reverse {A} (l : list A) : list A := rev_append l [].

(** The function [resize n y l] takes the first [n] elements of [l] in case
[length l ≤ n], and otherwise appends elements with value [x] to [l] to obtain
a list of length [n]. *)
Fixpoint resize {A} (n : nat) (y : A) (l : list A) : list A :=
  match l with
  | [] => replicate n y
  | x :: l =>
    match n with
    | 0 => []
    | S n => x :: resize n y l
    end
  end.
Arguments resize {_} !_ _ !_.

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

(** * Tactics on lists *)
Lemma cons_inv {A} (l1 l2 : list A) x1 x2 :
  x1 :: l1 = x2 :: l2  x1 = x2  l1 = l2.
Proof. by injection 1. Qed.

(** The tactic [discriminate_list_equality] discharges goals containing
invalid list equalities as an assumption. *)
120 121 122
Tactic Notation "discriminate_list_equality" hyp(H) :=
  apply (f_equal length) in H;
  repeat (simpl in H || rewrite app_length in H);
123
  exfalso; lia.
124 125 126
Tactic Notation "discriminate_list_equality" :=
  repeat_on_hyps (fun H => discriminate_list_equality H).

Robbert Krebbers's avatar
Robbert Krebbers committed
127 128
(** The tactic [simplify_list_equality] simplifies assumptions involving
equalities on lists. *)
129 130
Ltac simplify_list_equality := repeat
  match goal with
Robbert Krebbers's avatar
Robbert Krebbers committed
131 132 133
  | H : _ :: _ = _ :: _ |- _ =>
     apply cons_inv in H; destruct H
     (* to circumvent bug #2939 in some situations *)
134
  | H : _ ++ _ = _ ++ _ |- _ => first
Robbert Krebbers's avatar
Robbert Krebbers committed
135 136
     [ apply app_inj_tail in H; destruct H
     | apply app_inv_head in H
137
     | apply app_inv_tail in H ]
Robbert Krebbers's avatar
Robbert Krebbers committed
138 139 140
  | H : [?x] !! ?i = Some ?y |- _ =>
     destruct i; [change (Some x = Some y) in H|discriminate]
  | _ => progress simplify_equality
141 142
  | H : _ |- _ => discriminate_list_equality H
  end.
143

144 145
(** * General theorems *)
Section general_properties.
Robbert Krebbers's avatar
Robbert Krebbers committed
146 147
Context {A : Type}.

Robbert Krebbers's avatar
Robbert Krebbers committed
148 149 150 151
Global Instance:  x : A, Injective (=) (=) (x ::).
Proof. by injection 1. Qed.
Global Instance:  l : list A, Injective (=) (=) (:: l).
Proof. by injection 1. Qed.
152 153 154 155 156
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.

Robbert Krebbers's avatar
Robbert Krebbers committed
157 158 159 160 161
Lemma app_inj (l1 k1 l2 k2 : list A) :
  length l1 = length k1 
  l1 ++ l2 = k1 ++ k2  l1 = k1  l2 = k2.
Proof. revert k1. induction l1; intros [|??]; naive_solver. Qed.

162 163 164
Lemma list_eq (l1 l2 : list A) : ( i, l1 !! i = l2 !! i)  l1 = l2.
Proof.
  revert l2. induction l1; intros [|??] H.
165
  * done.
166 167
  * discriminate (H 0).
  * discriminate (H 0).
168 169
  * f_equal; [by injection (H 0) |].
    apply IHl1. intro. apply (H (S _)).
170
Qed.
171 172
Lemma list_eq_nil (l : list A) : ( i, l !! i = None)  l = nil.
Proof. intros. by apply list_eq. Qed.
173

174 175
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
176 177 178 179 180 181 182 183
Definition list_singleton_dec (l : list A) : { x | l = [x] } + { length l  1 }.
Proof.
 by refine (
  match l with
  | [x] => inleft (x  _)
  | _ => inright _
  end).
Defined.
184 185 186 187 188 189

Lemma nil_or_length_pos (l : list A) : l = []  length l  0.
Proof. destruct l; simpl; auto with lia. Qed.
Lemma nil_length (l : list A) : length l = 0  l = [].
Proof. by destruct l. Qed.
Lemma lookup_nil i : @nil A !! i = None.
190
Proof. by destruct i. Qed.
191
Lemma lookup_tail (l : list A) i : tail l !! i = l !! S i.
192
Proof. by destruct l. Qed.
193

194 195
Lemma lookup_lt_length (l : list A) i :
  is_Some (l !! i)  i < length l.
196
Proof.
197 198 199 200 201
  revert i. induction l.
  * split; by inversion 1.
  * intros [|?]; simpl.
    + split; eauto with arith.
    + by rewrite <-NPeano.Nat.succ_lt_mono.
202
Qed.
203 204 205 206 207 208 209 210 211 212 213 214 215 216 217 218 219 220 221 222
Lemma lookup_lt_length_1 (l : list A) i :
  is_Some (l !! i)  i < length l.
Proof. apply lookup_lt_length. Qed.
Lemma lookup_lt_length_alt (l : list A) i x :
  l !! i = Some x  i < length l.
Proof. intros Hl. by rewrite <-lookup_lt_length, Hl. Qed.
Lemma lookup_lt_length_2 (l : list A) i :
  i < length l  is_Some (l !! i).
Proof. apply lookup_lt_length. Qed.

Lemma lookup_ge_length (l : list A) i :
  l !! i = None  length l  i.
Proof. rewrite eq_None_not_Some, lookup_lt_length. lia. Qed.
Lemma lookup_ge_length_1 (l : list A) i :
  l !! i = None  length l  i.
Proof. by rewrite lookup_ge_length. Qed.
Lemma lookup_ge_length_2 (l : list A) i :
  length l  i  l !! i = None.
Proof. by rewrite lookup_ge_length. Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
223 224 225 226 227 228 229 230 231 232 233 234 235
Lemma list_eq_length_eq (l1 l2 : list A) :
  length l2 = length l1 
  ( i x y, l1 !! i = Some x  l2 !! i = Some y  x = y) 
  l1 = l2.
Proof.
  intros Hlength Hlookup. apply list_eq. intros i.
  destruct (l2 !! i) as [x|] eqn:E.
  * feed inversion (lookup_lt_length_2 l1 i) as [y].
    { pose proof (lookup_lt_length_alt l2 i x E). lia. }
    f_equal. eauto.
  * rewrite lookup_ge_length in E |- *. lia.
Qed.

236 237 238 239 240 241 242 243 244 245 246
Lemma lookup_app_l (l1 l2 : list A) i :
  i < length l1 
  (l1 ++ l2) !! i = l1 !! i.
Proof. revert i. induction l1; intros [|?]; simpl; auto with lia. Qed.
Lemma lookup_app_l_Some (l1 l2 : list A) i x :
  l1 !! i = Some x 
  (l1 ++ l2) !! i = Some x.
Proof. intros. rewrite lookup_app_l; eauto using lookup_lt_length_alt. Qed.

Lemma lookup_app_r (l1 l2 : list A) i :
  (l1 ++ l2) !! (length l1 + i) = l2 !! i.
247
Proof.
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
  revert i.
  induction l1; intros [|i]; simpl in *; simplify_equality; auto.
Qed.
Lemma lookup_app_r_alt (l1 l2 : list A) i :
  length l1  i 
  (l1 ++ l2) !! i = l2 !! (i - length l1).
Proof.
  intros. assert (i = length l1 + (i - length l1)) as Hi by lia.
  rewrite Hi at 1. by apply lookup_app_r.
Qed.
Lemma lookup_app_r_Some (l1 l2 : list A) i x :
  l2 !! i = Some x 
  (l1 ++ l2) !! (length l1 + i) = Some x.
Proof. by rewrite lookup_app_r. Qed.
Lemma lookup_app_r_Some_alt (l1 l2 : list A) i x :
  length l1  i 
  l2 !! (i - length l1) = Some x 
  (l1 ++ l2) !! i = Some x.
Proof. intro. by rewrite lookup_app_r_alt. Qed.

Lemma lookup_app_inv (l1 l2 : list A) i x :
  (l1 ++ l2) !! i = Some x 
  l1 !! i = Some x  l2 !! (i - length l1) = Some x.
Proof.
  revert i.
  induction l1; intros [|i] ?; simpl in *; simplify_equality; auto.
274 275
Qed.

276
Lemma list_lookup_middle (l1 l2 : list A) (x : A) :
277
  (l1 ++ x :: l2) !! length l1 = Some x.
278
Proof. by induction l1; simpl. Qed.
279

280 281 282 283 284 285 286 287 288
Lemma alter_length (f : A  A) l i :
  length (alter f i l) = length l.
Proof. revert i. induction l; intros [|?]; simpl; auto with lia. Qed.
Lemma insert_length (l : list A) i x :
  length (<[i:=x]>l) = length l.
Proof. apply alter_length. Qed.

Lemma list_lookup_alter (f : A  A) l i :
  alter f i l !! i = f <$> l !! i.
289
Proof. revert i. induction l. done. intros [|i]. done. apply (IHl i). Qed.
290
Lemma list_lookup_alter_ne (f : A  A) l i j :
291 292 293 294 295
  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.
296 297 298 299 300 301 302 303 304 305 306 307
Lemma list_lookup_insert (l : list A) i x :
  i < length l 
  <[i:=x]>l !! i = Some x.
Proof.
  intros Hi. unfold insert, list_insert.
  rewrite list_lookup_alter.
  by feed inversion (lookup_lt_length_2 l i).
Qed.
Lemma list_lookup_insert_ne (l : list A) i j x :
  i  j  <[i:=x]>l !! j = l !! j.
Proof. apply list_lookup_alter_ne. Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
308 309 310 311 312 313 314 315 316 317 318
Lemma list_lookup_other (l : list A) i x :
  length l  1 
  l !! i = Some x 
   j y, j  i  l !! j = Some y.
Proof.
  intros Hl Hi.
  destruct i; destruct l as [|x0 [|x1 l]]; simpl in *; simplify_equality.
  * by exists 1 x1.
  * by exists 0 x0.
Qed.

319 320 321 322 323 324 325 326 327 328 329 330 331 332 333 334 335 336 337 338
Lemma alter_app_l (f : A  A) (l1 l2 : list A) i :
  i < length l1 
  alter f i (l1 ++ l2) = alter f i l1 ++ l2.
Proof.
  revert i.
  induction l1; intros [|?] ?; simpl in *; f_equal; auto with lia.
Qed.
Lemma alter_app_r (f : A  A) (l1 l2 : list A) i :
  alter f (length l1 + i) (l1 ++ l2) = l1 ++ alter f i l2.
Proof.
  revert i.
  induction l1; intros [|?]; simpl in *; f_equal; auto.
Qed.
Lemma alter_app_r_alt (f : A  A) (l1 l2 : list A) i :
  length l1  i 
  alter f i (l1 ++ l2) = l1 ++ alter f (i - length l1) l2.
Proof.
  intros. assert (i = length l1 + (i - length l1)) as Hi by lia.
  rewrite Hi at 1. by apply alter_app_r.
Qed.
339

340 341 342 343 344 345 346 347 348 349 350 351 352 353 354
Lemma insert_app_l (l1 l2 : list A) i x :
  i < length l1 
  <[i:=x]>(l1 ++ l2) = <[i:=x]>l1 ++ l2.
Proof. apply alter_app_l. Qed.
Lemma insert_app_r (l1 l2 : list A) i x :
  <[length l1 + i:=x]>(l1 ++ l2) = l1 ++ <[i:=x]>l2.
Proof. apply alter_app_r. Qed.
Lemma insert_app_r_alt (l1 l2 : list A) i x :
  length l1  i 
  <[i:=x]>(l1 ++ l2) = l1 ++ <[i - length l1:=x]>l2.
Proof. apply alter_app_r_alt. Qed.

Lemma insert_consecutive_length (l : list A) i k :
  length (insert_consecutive i k l) = length l.
Proof. revert i. by induction k; intros; simpl; rewrite ?insert_length. Qed.
355

356 357 358 359 360 361
Lemma not_elem_of_nil (x : A) : x  [].
Proof. by inversion 1. Qed.
Lemma elem_of_nil (x : A) : x  []  False.
Proof. intuition. by destruct (not_elem_of_nil x). Qed.
Lemma elem_of_nil_inv (l : list A) : ( x, x  l)  l = [].
Proof. destruct l. done. by edestruct 1; constructor. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
362
Lemma elem_of_cons (l : list A) x y :
363
  x  y :: l  x = y  x  l.
364 365
Proof.
  split.
366 367
  * inversion 1; subst. by left. by right.
  * intros [?|?]; subst. by left. by right.
368
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
369 370 371 372
Lemma not_elem_of_cons (l : list A) x y :
  x  y :: l  x  y  x  l.
Proof. rewrite elem_of_cons. tauto. Qed.
Lemma elem_of_app (l1 l2 : list A) x :
373
  x  l1 ++ l2  x  l1  x  l2.
374
Proof.
375 376 377 378
  induction l1.
  * split; [by right|]. intros [Hx|]; [|done].
    by destruct (elem_of_nil x).
  * simpl. rewrite !elem_of_cons, IHl1. tauto.
379
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
380 381 382 383
Lemma not_elem_of_app (l1 l2 : list A) x :
  x  l1 ++ l2  x  l1  x  l2.
Proof. rewrite elem_of_app. tauto. Qed.

384 385
Lemma elem_of_list_singleton (x y : A) : x  [y]  x = y.
Proof. rewrite elem_of_cons, elem_of_nil. tauto. Qed.
386

387 388 389
Global Instance elem_of_list_permutation_proper (x : A) :
  Proper (Permutation ==> iff) (x ).
Proof. induction 1; rewrite ?elem_of_nil, ?elem_of_cons; intuition. Qed.
390

Robbert Krebbers's avatar
Robbert Krebbers committed
391
Lemma elem_of_list_split (l : list A) x :
392 393 394 395 396 397
  x  l   l1 l2, l = l1 ++ x :: l2.
Proof.
  induction 1 as [x l|x y l ? [l1 [l2 ?]]].
  * by eexists [], l.
  * subst. by exists (y :: l1) l2.
Qed.
398

399 400 401 402 403 404 405 406 407 408 409 410 411 412 413 414 415 416 417 418 419 420 421 422 423 424
Global Instance elem_of_list_dec {dec :  x y : A, Decision (x = y)} :
   (x : A) l, Decision (x  l).
Proof.
 intros x. refine (
  fix go l :=
  match l return Decision (x  l) with
  | [] => right (not_elem_of_nil _)
  | y :: l => cast_if_or (decide_rel (=) x y) (go l)
  end); clear go dec; subst; try (by constructor); by inversion 1.
Defined.

Lemma elem_of_list_lookup_1 (l : list A) x :
  x  l   i, l !! i = Some x.
Proof.
  induction 1 as [|???? IH].
  * by exists 0.
  * destruct IH as [i ?]; auto. by exists (S i).
Qed.
Lemma elem_of_list_lookup_2 (l : list A) i x :
  l !! i = Some x  x  l.
Proof.
  revert i. induction l; intros [|i] ?;
    simpl; simplify_equality; constructor; eauto.
Qed.
Lemma elem_of_list_lookup (l : list A) x :
  x  l   i, l !! i = Some x.
425
Proof.
426 427
  firstorder eauto using
    elem_of_list_lookup_1, elem_of_list_lookup_2.
428
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
429

430 431 432 433 434 435 436 437
Lemma NoDup_nil : NoDup (@nil A)  True.
Proof. split; constructor. Qed.
Lemma NoDup_cons (x : A) l : NoDup (x :: l)  x  l  NoDup l.
Proof. split. by inversion 1. intros [??]. by constructor. Qed.
Lemma NoDup_cons_11 (x : A) l : NoDup (x :: l)  x  l.
Proof. rewrite NoDup_cons. by intros [??]. Qed.
Lemma NoDup_cons_12 (x : A) l : NoDup (x :: l)  NoDup l.
Proof. rewrite NoDup_cons. by intros [??]. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
438
Lemma NoDup_singleton (x : A) : NoDup [x].
439 440
Proof. constructor. apply not_elem_of_nil. constructor. Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
441
Lemma NoDup_app (l k : list A) :
442
  NoDup (l ++ k)  NoDup l  ( x, x  l  x  k)  NoDup k.
Robbert Krebbers's avatar
Robbert Krebbers committed
443
Proof.
444 445 446 447 448 449
  induction l; simpl.
  * rewrite NoDup_nil.
    setoid_rewrite elem_of_nil. naive_solver.
  * rewrite !NoDup_cons.
    setoid_rewrite elem_of_cons. setoid_rewrite elem_of_app.
    naive_solver.
Robbert Krebbers's avatar
Robbert Krebbers committed
450 451
Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
452
Global Instance NoDup_proper:
453 454 455 456 457 458 459 460
  Proper (Permutation ==> iff) (@NoDup A).
Proof.
  induction 1 as [|x l k Hlk IH | |].
  * by rewrite !NoDup_nil.
  * by rewrite !NoDup_cons, IH, Hlk.
  * rewrite !NoDup_cons, !elem_of_cons. intuition.
  * intuition.
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
461

462 463 464 465 466 467 468 469
Lemma NoDup_Permutation (l k : list A) :
  NoDup l  NoDup k  ( x, x  l  x  k)  Permutation l k.
Proof.
  intros Hl. revert k. induction Hl as [|x l Hin ? IH].
  * intros k _ Hk.
    rewrite (elem_of_nil_inv k); [done |].
    intros x. rewrite <-Hk, elem_of_nil. intros [].
  * intros k Hk Hlk.
Robbert Krebbers's avatar
Robbert Krebbers committed
470
    destruct (elem_of_list_split k x) as [l1 [l2 ?]]; subst.
471 472 473 474 475 476 477 478
    { rewrite <-Hlk. by constructor. }
    rewrite <-Permutation_middle, NoDup_cons in Hk.
    destruct Hk as [??].
    apply Permutation_cons_app, IH; [done |].
    intros y. specialize (Hlk y).
    rewrite <-Permutation_middle, !elem_of_cons in Hlk.
    naive_solver.
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
479

480 481
Global Instance NoDup_dec {dec :  x y : A, Decision (x = y)} :
     (l : list A), Decision (NoDup l) :=
Robbert Krebbers's avatar
Robbert Krebbers committed
482 483
  fix NoDup_dec l :=
  match l return Decision (NoDup l) with
484
  | [] => left NoDup_nil_2
Robbert Krebbers's avatar
Robbert Krebbers committed
485
  | x :: l =>
486 487
    match decide_rel () x l with
    | left Hin => right (λ H, NoDup_cons_11 _ _ H Hin)
Robbert Krebbers's avatar
Robbert Krebbers committed
488 489
    | right Hin =>
      match NoDup_dec l with
490 491
      | left H => left (NoDup_cons_2 _ _ Hin H)
      | right H => right (H  NoDup_cons_12 _ _)
Robbert Krebbers's avatar
Robbert Krebbers committed
492 493 494 495
      end
    end
  end.

496 497
Section remove_dups.
  Context `{! x y : A, Decision (x = y)}.
498

499 500 501 502 503 504
  Fixpoint remove_dups (l : list A) : list A :=
    match l with
    | [] => []
    | x :: l =>
      if decide_rel () x l then remove_dups l else x :: remove_dups l
    end.
505

506 507 508 509 510 511
  Lemma elem_of_remove_dups l x :
    x  remove_dups l  x  l.
  Proof.
    split; induction l; simpl; repeat case_decide;
      rewrite ?elem_of_cons; intuition (simplify_equality; auto).
  Qed.
512

513 514 515 516 517 518
  Lemma remove_dups_nodup l : NoDup (remove_dups l).
  Proof.
    induction l; simpl; repeat case_decide; try constructor; auto.
    by rewrite elem_of_remove_dups.
  Qed.
End remove_dups.
519

Robbert Krebbers's avatar
Robbert Krebbers committed
520 521 522 523 524 525 526 527 528 529 530 531 532
Lemma elem_of_list_filter `{ x : A, Decision (P x)} l x :
  x  filter P l  P x  x  l.
Proof.
  unfold filter. induction l; simpl; repeat case_decide;
     rewrite ?elem_of_nil, ?elem_of_cons; naive_solver.
Qed.
Lemma filter_nodup P `{ x : A, Decision (P x)} l :
  NoDup l  NoDup (filter P l).
Proof.
  unfold filter. induction 1; simpl; repeat case_decide;
    rewrite ?NoDup_nil, ?NoDup_cons, ?elem_of_list_filter; tauto.
Qed.

533 534 535 536 537 538 539 540 541 542 543 544 545 546
Lemma reverse_nil : reverse [] = @nil A.
Proof. done. Qed.
Lemma reverse_cons (l : list A) x : reverse (x :: l) = reverse l ++ [x].
Proof. unfold reverse. by rewrite <-!rev_alt. Qed.
Lemma reverse_snoc (l : list A) x : reverse (l ++ [x]) = x :: reverse l.
Proof. unfold reverse. by rewrite <-!rev_alt, rev_unit. Qed.
Lemma reverse_app (l1 l2 : list A) :
  reverse (l1 ++ l2) = reverse l2 ++ reverse l1.
Proof. unfold reverse. rewrite <-!rev_alt. apply rev_app_distr. Qed.
Lemma reverse_length (l : list A) : length (reverse l) = length l.
Proof. unfold reverse. rewrite <-!rev_alt. apply rev_length. Qed.
Lemma reverse_involutive (l : list A) : reverse (reverse l) = l.
Proof. unfold reverse. rewrite <-!rev_alt. apply rev_involutive. Qed. 

Robbert Krebbers's avatar
Robbert Krebbers committed
547 548 549 550 551 552 553 554 555 556 557 558 559 560 561 562 563 564 565 566 567 568 569 570 571 572 573 574 575 576 577 578 579 580 581 582 583 584 585 586 587 588 589 590 591 592 593 594 595 596 597 598 599 600 601 602 603 604 605 606 607 608 609 610 611 612 613 614 615 616 617 618 619 620 621 622 623 624 625 626 627 628 629 630 631 632 633 634 635 636 637 638 639 640 641 642 643 644 645 646 647 648 649 650 651 652 653
Lemma take_nil n :
  take n (@nil A) = [].
Proof. by destruct n. Qed.
Lemma take_app (l k : list A) :
  take (length l) (l ++ k) = l.
Proof. induction l; simpl; f_equal; auto. Qed.
Lemma take_app_alt (l k : list A) n :
  n = length l 
  take n (l ++ k) = l.
Proof. intros Hn. by rewrite Hn, take_app. Qed.
Lemma take_app_le (l k : list A) n :
  n  length l 
  take n (l ++ k) = take n l.
Proof.
  revert n;
  induction l; intros [|?] ?; simpl in *; f_equal; auto with lia.
Qed.
Lemma take_app_ge (l k : list A) n :
  length l  n 
  take n (l ++ k) = l ++ take (n - length l) k.
Proof.
  revert n;
  induction l; intros [|?] ?; simpl in *; f_equal; auto with lia.
Qed.
Lemma take_ge (l : list A) n :
  length l  n 
  take n l = l.
Proof.
  revert n.
  induction l; intros [|?] ?; simpl in *; f_equal; auto with lia.
Qed.

Lemma take_take (l : list A) n m :
  take n (take m l) = take (min n m) l.
Proof. revert n m. induction l; intros [|?] [|?]; simpl; f_equal; auto. Qed.
Lemma take_idempotent (l : list A) n :
  take n (take n l) = take n l.
Proof. by rewrite take_take, Min.min_idempotent. Qed.

Lemma take_length (l : list A) n :
  length (take n l) = min n (length l).
Proof. revert n. induction l; intros [|?]; simpl; f_equal; done. Qed.
Lemma take_length_alt (l : list A) n :
  n  length l 
  length (take n l) = n.
Proof. rewrite take_length. apply Min.min_l. Qed.

Lemma lookup_take (l : list A) n i :
  i < n  take n l !! i = l !! i.
Proof.
  revert n i. induction l; intros [|n] i ?; trivial.
  * auto with lia.
  * destruct i; simpl; auto with arith.
Qed.
Lemma lookup_take_ge (l : list A) n i :
  n  i  take n l !! i = None.
Proof.
  revert n i.
  induction l; intros [|?] [|?] ?; simpl; auto with lia.
Qed.
Lemma take_alter (f : A  A) l n i :
  n  i  take n (alter f i l) = take n l.
Proof.
  intros. apply list_eq. intros j. destruct (le_lt_dec n j).
  * by rewrite !lookup_take_ge.
  * by rewrite !lookup_take, !list_lookup_alter_ne by lia.
Qed.
Lemma take_insert (l : list A) n i x :
  n  i  take n (<[i:=x]>l) = take n l.
Proof take_alter _ _ _ _.

Lemma drop_nil n :
  drop n (@nil A) = [].
Proof. by destruct n. Qed.
Lemma drop_app (l k : list A) :
  drop (length l) (l ++ k) = k.
Proof. induction l; simpl; f_equal; auto. Qed.
Lemma drop_app_alt (l k : list A) n :
  n = length l 
  drop n (l ++ k) = k.
Proof. intros Hn. by rewrite Hn, drop_app. Qed.
Lemma drop_length (l : list A) n :
  length (drop n l) = length l - n.
Proof.
  revert n. by induction l; intros [|i]; simpl; f_equal.
Qed.
Lemma drop_all (l : list A) :
  drop (length l) l = [].
Proof. induction l; simpl; auto. Qed.
Lemma drop_all_alt (l : list A) n :
  n = length l 
  drop n l = [].
Proof. intros. subst. by rewrite drop_all. Qed.

Lemma lookup_drop (l : list A) n i :
  drop n l !! i = l !! (n + i).
Proof. revert n i. induction l; intros [|i] ?; simpl; auto. Qed.
Lemma drop_alter (f : A  A) l n i  :
  i < n  drop n (alter f i l) = drop n l.
Proof.
  intros. apply list_eq. intros j.
  by rewrite !lookup_drop, !list_lookup_alter_ne by lia.
Qed.
Lemma drop_insert (l : list A) n i x :
  i < n  drop n (<[i:=x]>l) = drop n l.
Proof drop_alter _ _ _ _.

654 655 656 657 658
Lemma replicate_length n (x : A) : length (replicate n x) = n.
Proof. induction n; simpl; auto. Qed.
Lemma lookup_replicate n (x : A) i :
  i < n 
  replicate n x !! i = Some x.
659
Proof.
660 661 662 663 664 665 666 667 668
  revert i.
  induction n; intros [|?]; naive_solver auto with lia.
Qed.
Lemma lookup_replicate_inv n (x y : A) i :
  replicate n x !! i = Some y  y = x  i < n.
Proof.
  revert i.
  induction n; intros [|?]; naive_solver auto with lia.
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
669 670 671 672 673 674 675 676 677 678 679 680 681 682 683 684 685 686 687 688 689 690 691 692 693 694 695 696 697 698 699 700 701 702 703 704 705 706 707 708 709 710 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 765 766 767 768 769 770 771 772 773 774 775 776 777 778 779 780 781 782 783 784 785 786 787 788 789 790 791 792 793 794 795 796 797 798 799 800 801 802 803 804 805 806 807 808 809 810 811 812 813 814 815 816 817
Lemma replicate_plus n m (x : A) :
  replicate (n + m) x = replicate n x ++ replicate m x.
Proof. induction n; simpl; f_equal; auto. Qed.

Lemma take_replicate n m (x : A) :
  take n (replicate m x) = replicate (min n m) x.
Proof. revert m. by induction n; intros [|?]; simpl; f_equal. Qed.
Lemma take_replicate_plus n m (x : A) :
  take n (replicate (n + m) x) = replicate n x.
Proof. by rewrite take_replicate, min_l by lia. Qed.
Lemma drop_replicate n m (x : A) :
  drop n (replicate m x) = replicate (m - n) x.
Proof. revert m. by induction n; intros [|?]; simpl; f_equal. Qed.
Lemma drop_replicate_plus n m (x : A) :
  drop n (replicate (n + m) x) = replicate m x.
Proof. rewrite drop_replicate. f_equal. lia. Qed.

Lemma resize_spec (l : list A) n x :
  resize n x l = take n l ++ replicate (n - length l) x.
Proof.
  revert n.
  induction l; intros [|?]; simpl; f_equal; auto.
Qed.
Lemma resize_0 (l : list A) x :
  resize 0 x l = [].
Proof. by destruct l. Qed.
Lemma resize_nil n (x : A) :
  resize n x [] = replicate n x.
Proof. rewrite resize_spec. rewrite take_nil. simpl. f_equal. lia. Qed.
Lemma resize_ge (l : list A) n x :
  length l  n 
  resize n x l = l ++ replicate (n - length l) x.
Proof. intros. by rewrite resize_spec, take_ge. Qed.
Lemma resize_le (l : list A) n x :
  n  length l 
  resize n x l = take n l.
Proof.
  intros. rewrite resize_spec, (proj2 (NPeano.Nat.sub_0_le _ _)) by done.
  simpl. by rewrite app_nil_r.
Qed.

Lemma resize_all (l : list A) x :
  resize (length l) x l = l.
Proof. intros. by rewrite resize_le, take_ge. Qed.
Lemma resize_all_alt (l : list A) n x :
  n = length l 
  resize n x l = l.
Proof. intros. subst. by rewrite resize_all. Qed.

Lemma resize_plus (l : list A) n m x :
  resize (n + m) x l = resize n x l ++ resize m x (drop n l).
Proof.
  revert n m.
  induction l; intros [|?] [|?]; simpl; f_equal; auto.
  * by rewrite plus_0_r, app_nil_r.
  * by rewrite replicate_plus.
Qed.
Lemma resize_plus_eq (l : list A) n m x :
  length l = n 
  resize (n + m) x l = l ++ replicate m x.
Proof.
  intros. subst.
  by rewrite resize_plus, resize_all, drop_all, resize_nil.
Qed.

Lemma resize_app_le (l1 l2 : list A) n x :
  n  length l1 
  resize n x (l1 ++ l2) = resize n x l1.
Proof.
  intros.
  by rewrite !resize_le, take_app_le by (rewrite ?app_length; lia).
Qed.
Lemma resize_app_ge (l1 l2 : list A) n x :
  length l1  n 
  resize n x (l1 ++ l2) = l1 ++ resize (n - length l1) x l2.
Proof.
  intros.
  rewrite !resize_spec, take_app_ge, app_assoc by done.
  do 2 f_equal. rewrite app_length. lia.
Qed.

Lemma resize_length (l : list A) n x : length (resize n x l) = n.
Proof.
  rewrite resize_spec, app_length, replicate_length, take_length. lia.
Qed.
Lemma resize_replicate (x : A) n m :
  resize n x (replicate m x) = replicate n x.
Proof. revert m. induction n; intros [|?]; simpl; f_equal; auto. Qed.

Lemma resize_resize (l : list A) n m x :
  n  m 
  resize n x (resize m x l) = resize n x l.
Proof.
  revert n m. induction l; simpl.
  * intros. by rewrite !resize_nil, resize_replicate.
  * intros [|?] [|?] ?; simpl; f_equal; auto with lia.
Qed.
Lemma resize_idempotent (l : list A) n x :
  resize n x (resize n x l) = resize n x l.
Proof. by rewrite resize_resize. Qed.

Lemma resize_take_le (l : list A) n m x :
  n  m 
  resize n x (take m l) = resize n x l.
Proof.
  revert n m.
  induction l; intros [|?] [|?] ?; simpl; f_equal; auto with lia.
Qed.
Lemma resize_take_eq (l : list A) n x :
  resize n x (take n l) = resize n x l.
Proof. by rewrite resize_take_le. Qed.

Lemma take_resize (l : list A) n m x :
  take n (resize m x l) = resize (min n m) x l.
Proof.
  revert n m.
  induction l; intros [|?] [|?]; simpl; f_equal; auto using take_replicate.
Qed.
Lemma take_resize_le (l : list A) n m x :
  n  m 
  take n (resize m x l) = resize n x l.
Proof. intros. by rewrite take_resize, Min.min_l. Qed.
Lemma take_resize_eq (l : list A) n x :
  take n (resize n x l) = resize n x l.
Proof. intros. by rewrite take_resize, Min.min_l. Qed.
Lemma take_length_resize (l : list A) n x :
  length l  n 
  take (length l) (resize n x l) = l.
Proof. intros. by rewrite take_resize_le, resize_all. Qed.
Lemma take_length_resize_alt (l : list A) n m x :
  m = length l 
  m  n 
  take m (resize n x l) = l.
Proof. intros. subst. by apply take_length_resize. Qed.
Lemma take_resize_plus (l : list A) n m x :
  take n (resize (n + m) x l) = resize n x l.
Proof. by rewrite take_resize, min_l by lia. Qed.

Lemma drop_resize_le (l : list A) n m x :
  n  m 
  drop n (resize m x l) = resize (m - n) x (drop n l).
Proof.
  revert n m. induction l; simpl.
  * intros. by rewrite drop_nil, !resize_nil, drop_replicate.
  * intros [|?] [|?] ?; simpl; try case_match; auto with lia.
Qed.
Lemma drop_resize_plus (l : list A) n m x :
  drop n (resize (n + m) x l) = resize m x (drop n l).
Proof. rewrite drop_resize_le by lia. f_equal. lia. Qed.
818

819 820
Section Forall_Exists.
  Context (P : A  Prop).
821

822 823 824 825 826 827 828 829 830 831
  Lemma Forall_forall l :
    Forall P l   x, x  l  P x.
  Proof.
    split.
    * induction 1; inversion 1; subst; auto.
    * intros Hin. induction l; constructor.
      + apply Hin. constructor.
      + apply IHl. intros ??. apply Hin. by constructor.
  Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
832 833 834 835 836 837 838 839
  Lemma Forall_nil : Forall P []  True.
  Proof. done. Qed.
  Lemma Forall_cons_1 x l : Forall P (x :: l)  P x  Forall P l.
  Proof. by inversion 1. Qed.
  Lemma Forall_cons x l : Forall P (x :: l)  P x  Forall P l.
  Proof. split. by inversion 1. intros [??]. by constructor. Qed.
  Lemma Forall_singleton x : Forall P [x]  P x.
  Proof. rewrite Forall_cons, Forall_nil; tauto. Qed.
840 841 842 843 844 845 846 847 848 849 850
  Lemma Forall_app 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 l : ( x, P x)  Forall P l.
  Proof. induction l; auto. Qed.
  Lemma Forall_impl l (Q : A  Prop) :
    Forall P l  ( x, P x  Q x)  Forall Q l.
  Proof. intros H ?. induction H; auto. Defined.
Robbert Krebbers's avatar
Robbert Krebbers committed
851

852 853 854 855 856 857 858 859 860 861 862 863
  Lemma Forall_delete l i : Forall P l  Forall P (delete i l).
  Proof.
    intros H. revert i.
    by induction H; intros [|i]; try constructor.
  Qed.
  Lemma Forall_lookup l :
    Forall P l   i x, l !! i = Some x  P x.
  Proof.
    rewrite Forall_forall.
    setoid_rewrite elem_of_list_lookup.
    naive_solver.
  Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
864 865 866
  Lemma Forall_lookup_1 l i x :
    Forall P l  l !! i = Some x  P x.
  Proof. rewrite Forall_lookup. eauto. Qed.
867 868 869 870 871 872 873 874
  Lemma Forall_alter f l i :
    Forall P l 
    ( x, l !! i = Some x  P x  P (f x)) 
    Forall P (alter f i l).
  Proof.
    intros Hl. revert i.
    induction Hl; simpl; intros [|i]; constructor; auto.
  Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
875

Robbert Krebbers's avatar
Robbert Krebbers committed
876 877 878 879 880 881 882
  Lemma Forall_replicate n x :
    P x  Forall P (replicate n x).
  Proof. induction n; simpl; constructor; auto. Qed.
  Lemma Forall_replicate_eq n (x : A) :
    Forall (=x) (replicate n x).
  Proof. induction n; simpl; constructor; auto. Qed.

883 884 885 886 887 888 889 890 891 892 893 894 895 896 897 898 899 900 901 902 903
  Lemma Exists_exists l :
    Exists P l   x, x  l  P x.
  Proof.
    split.
    * induction 1 as [x|y ?? IH].
      + exists x. split. constructor. done.
      + destruct IH as [x [??]]. exists x. split. by constructor. done. 
    * intros [x [Hin ?]]. induction l.
      + by destruct (not_elem_of_nil x).
      + inversion Hin; subst. by left. right; auto.
  Qed.
  Lemma Exists_inv x l : Exists P (x :: l)  P x  Exists P l.
  Proof. inversion 1; intuition trivial. Qed.
  Lemma Exists_app l1 l2 : Exists P (l1 ++ l2)  Exists P l1  Exists P l2.
  Proof.
    split.
    * induction l1; inversion 1; intuition.
    * intros [H|H].
      + induction H; simpl; intuition.
      + induction l1; simpl; intuition. 
  Qed.
904

905 906 907 908
  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.
909

910 911 912 913 914 915 916 917 918 919 920 921 922 923 924 925 926 927 928 929 930 931 932 933 934 935 936 937 938 939 940 941 942 943 944 945 946
  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)
    end.

  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)
    end.
947
End Forall_Exists.
Robbert Krebbers's avatar
Robbert Krebbers committed
948
End general_properties.
949 950

Section Forall2.
Robbert Krebbers's avatar
Robbert Krebbers committed
951 952 953 954 955 956 957 958 959 960 961 962 963 964 965 966 967 968 969 970 971 972 973 974 975 976 977 978 979 980
  Context {A B} (P : A  B  Prop).

  Lemma Forall2_nil_inv_l k :
    Forall2 P [] k  k = [].
  Proof. by inversion 1. Qed.
  Lemma Forall2_nil_inv_r k :
    Forall2 P k []  k = [].
  Proof. by inversion 1. Qed.

  Lemma Forall2_cons_inv l1 l2 x1 x2 :
    Forall2 P (x1 :: l1) (x2 :: l2)  P x1 x2  Forall2 P l1 l2.
  Proof. by inversion 1. Qed.
  Lemma Forall2_cons_inv_l l1 k x1 :
    Forall2 P (x1 :: l1) k   x2 l2,
      P x1 x2  Forall2 P l1 l2  k = x2 :: l2.
  Proof. inversion 1; subst; eauto. Qed.
  Lemma Forall2_cons_inv_r k l2 x2 :
    Forall2 P k (x2 :: l2)   x1 l1,
      P x1 x2  Forall2 P l1 l2  k = x1 :: l1.
  Proof. inversion 1; subst; eauto. Qed.
  Lemma Forall2_cons_nil_inv l1 x1 :
    Forall2 P (x1 :: l1) []  False.
  Proof. by inversion 1. Qed.
  Lemma Forall2_nil_cons_inv l2 x2 :
    Forall2 P [] (x2 :: l2)  False.
  Proof. by inversion 1. Qed.

  Lemma Forall2_flip l1 l2 :
    Forall2 P l1 l2  Forall2 (flip P) l2 l1.
  Proof. split; induction 1; constructor; auto. Qed.
981 982 983 984

  Lemma Forall2_length l1 l2 :
    Forall2 P l1 l2  length l1 = length l2.
  Proof. induction 1; simpl; auto. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
985

986 987
  Lemma Forall2_impl (Q : A  B  Prop) l1 l2 :
    Forall2 P l1 l2  ( x y, P x y  Q x y)  Forall2 Q l1 l2.
Robbert Krebbers's avatar
Robbert Krebbers committed
988
  Proof. intros H ?. induction H; auto. Defined.
989 990 991 992 993 994 995 996 997 998 999

  Lemma Forall2_unique l k1 k2 :
    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
1000
  Lemma Forall2_Forall_l (Q : A  Prop) l k :
1001 1002 1003
    Forall2 P l k 
    Forall (λ y,  x, P x y  Q x) k 
    Forall Q l.
Robbert Krebbers's avatar
Robbert Krebbers committed
1004 1005
  Proof. induction 1; inversion_clear 1; eauto. Qed.
  Lemma Forall2_Forall_r (Q : B  Prop) l k :
1006 1007 1008
    Forall2 P l k 
    Forall (λ x,  y, P x y  Q y) l 
    Forall Q k.
Robbert Krebbers's avatar
Robbert Krebbers committed
1009 1010 1011 1012 1013 1014 1015 1016 1017 1018 1019 1020 1021 1022 1023 1024 1025 1026 1027 1028 1029 1030 1031 1032 1033 1034 1035 1036 1037 1038 1039 1040 1041 1042 1043 1044 1045 1046 1047 1048 1049 1050 1051 1052 1053 1054 1055 1056 1057 1058 1059 1060 1061 1062 1063 1064 1065 1066 1067 1068 1069 1070 1071 1072 1073 1074 1075 1076 1077 1078 1079 1080 1081 1082 1083 1084 1085 1086 1087 1088 1089 1090 1091 1092 1093 1094 1095 1096 1097 1098 1099 1100 1101 1102 1103 1104 1105 1106 1107 1108 1109 1110 1111 1112 1113 1114 1115 1116 1117 1118 1119 1120 1121 1122 1123 1124 1125 1126 1127 1128 1129 1130 1131 1132 1133 1134 1135 1136 1137 1138 1139 1140 1141 1142 1143 1144 1145 1146 1147 1148 1149 1150 1151 1152 1153 1154 1155 1156 1157 1158 1159 1160 1161
  Proof. induction 1; inversion_clear 1; eauto. Qed.

  Lemma Forall2_lookup l1 l2 i x y :
    Forall2 P l1 l2 
      l1 !! i = Some x  l2 !! i = Some y  P x y.
  Proof.
    intros H. revert i. induction H.
    * discriminate.
    * intros [|?] ??; simpl in *; simplify_equality; eauto.
  Qed.
  Lemma Forall2_lookup_l l1 l2 i x :
    Forall2 P l1 l2  l1 !! i = Some x   y,
      l2 !! i = Some y  P x y.
  Proof.
    intros H. revert i. induction H.
    * discriminate.
    * intros [|?] ?; simpl in *; simplify_equality; eauto.
  Qed.
  Lemma Forall2_lookup_r l1 l2 i y :
    Forall2 P l1 l2  l2 !! i = Some y   x,
      l1 !! i = Some x  P x y.
  Proof.
    intros H. revert i. induction H.
    * discriminate.
    * intros [|?] ?; simpl in *; simplify_equality; eauto.
  Qed.

  Lemma Forall2_alter_l f l1 l2 i :
    Forall2 P l1 l2 
    ( x1 x2,
      l1 !! i = Some x1  l2 !! i = Some x2  P x1 x2  P (f x1) x2) 
    Forall2 P (alter f i l1) l2.
  Proof.
    intros Hl. revert i.
    induction Hl; simpl; intros [|i]; constructor; auto.
  Qed.
  Lemma Forall2_alter_r f l1 l2 i :
    Forall2 P l1 l2 
    ( x1 x2,
      l1 !! i = Some x1  l2 !! i = Some x2  P x1 x2  P x1 (f x2)) 
    Forall2 P l1 (alter f i l2).
  Proof.
    intros Hl. revert i.
    induction Hl; simpl; intros [|i]; constructor; auto.
  Qed.
  Lemma Forall2_alter f g l1 l2 i :
    Forall2 P l1 l2 
    ( x1 x2,
      l1 !! i = Some x1  l2 !! i = Some x2  P x1 x2  P (f x1) (g x2)) 
    Forall2 P (alter f i l1) (alter g i l2).
  Proof.
    intros Hl. revert i.
    induction Hl; simpl; intros [|i]; constructor; auto.
  Qed.

  Lemma Forall2_replicate_l l n x :
    Forall (P x) l 
    length l = n 
    Forall2 P (replicate n x) l.
  Proof.
    intros Hl. revert n.
    induction Hl; intros [|?] ?; simplify_equality; constructor; auto.
  Qed.
  Lemma Forall2_replicate_r l n x :
    Forall (flip P x) l 
    length l = n 
    Forall2 P l (replicate n x).
  Proof.
    intros Hl. revert n.
    induction Hl; intros [|?] ?; simplify_equality; constructor; auto.
  Qed.
  Lemma Forall2_replicate n x1 x2 :
    P x1 x2 
    Forall2 P (replicate n x1) (replicate n x2).
  Proof. induction n; simpl; constructor; auto. Qed.

  Lemma Forall2_take l1 l2 n :
    Forall2 P l1 l2 
    Forall2 P (take n l1) (take n l2).
  Proof.
    intros Hl1l2. revert n.
    induction Hl1l2; intros [|?]; simpl; auto.
  Qed.
  Lemma Forall2_drop l1 l2 n :
    Forall2 P l1 l2 
    Forall2 P (drop n l1) (drop n l2).
  Proof.
    intros Hl1l2. revert n.
    induction Hl1l2; intros [|?]; simpl; auto.
  Qed.
  Lemma Forall2_resize l1 l2 x1 x2 n :
    P x1 x2 
    Forall2 P l1 l2 
    Forall2 P (resize n x1 l1) (resize n x2 l2).
  Proof.
    intros. rewrite !resize_spec, (Forall2_length l1 l2) by done.
    auto using Forall2_app, Forall2_take, Forall2_replicate.
  Qed.

  Lemma Forall2_resize_ge_l l1 l2 x1 x2 n m :
    ( x, P x x2) 
    n  m 
    Forall2 P (resize n x1 l1) l2 
    Forall2 P (resize m x1 l1) (resize m x2 l2).
  Proof.
    intros. assert (n = length l2).
    { by rewrite <-(Forall2_length (resize n x1 l1) l2), resize_length. }
    rewrite (le_plus_minus n m) by done. subst.
    rewrite !resize_plus, resize_all, drop_all, resize_nil.
    apply Forall2_app; [done |].
    apply Forall2_replicate_r; [| by rewrite resize_length].
    by apply Forall_true.
  Qed.
  Lemma Forall2_resize_ge_r l1 l2 x1 x2 n m :
    ( x3, P x1 x3) 
    n  m 
    Forall2 P l1 (resize n x2 l2) 
    Forall2 P (resize m x1 l1) (resize m x2 l2).
  Proof.
    intros. assert (n = length l1).
    { by rewrite (Forall2_length l1 (resize n x2 l2)), resize_length. }
    rewrite (le_plus_minus n m) by done. subst.
    rewrite !resize_plus, resize_all, drop_all, resize_nil.
    apply Forall2_app; [done |].
    apply Forall2_replicate_l; [| by rewrite resize_length].
    by apply Forall_true.
  Qed.

  Lemma Forall2_trans {C} (Q : B  C  Prop) (R : A  C  Prop) l1 l2 l3 :
    ( x1 x2 x3, P x1 x2  Q x2 x3  R x1 x3) 
    Forall2 P l1 l2 
    Forall2 Q l2 l3 
    Forall2 R l1 l3.
  Proof.
    intros ? Hl1l2. revert l3.
    induction Hl1l2; inversion_clear 1; eauto.
  Qed.

  Lemma Forall2_Forall (Q : A  A  Prop) l :
    Forall (λ x, Q x x) l  Forall2 Q l l.
  Proof. induction 1; constructor; auto. Qed.

  Global Instance Forall2_dec `{ x1 x2, Decision (P x1 x2)} :
     l1 l2, Decision (Forall2 P l1 l2).
  Proof.
   refine (
    fix go l1 l2 : Decision (Forall2 P l1 l2) :=
    match l1, l2 with
    | [], [] => left _
    | x1 :: l1, x2 :: l2 => cast_if_and (decide (P x1 x2)) (go l1 l2)
    | _, _ => right _
    end); clear go; abstract first [by constructor<