1
(************************************************************************)
2
(* v * The Coq Proof Assistant / The Coq Development Team *)
3
(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
4
(* \VV/ **************************************************************)
5
(* // * This file is distributed under the terms of the *)
6
(* * GNU Lesser General Public License Version 2.1 *)
7
(************************************************************************)
9
(*i $Id: List.v 10999 2008-05-27 15:55:22Z letouzey $ i*)
11
Require Import Le Gt Minus Min Bool.
13
Set Implicit Arguments.
16
(******************************************************************)
17
(** * Basics: definition of polymorphic lists and some operations *)
18
(******************************************************************)
26
Inductive list : Type :=
28
| cons : A -> list -> list.
30
Infix "::" := cons (at level 60, right associativity) : list_scope.
32
Open Scope list_scope.
35
Definition head (l:list) :=
41
Definition hd (default:A) (l:list) :=
47
Definition tail (l:list) : list :=
53
(** Length of lists *)
54
Fixpoint length (l:list) : nat :=
57
| _ :: m => S (length m)
60
(** The [In] predicate *)
61
Fixpoint In (a:A) (l:list) {struct l} : Prop :=
64
| b :: m => b = a \/ In a m
68
(** Concatenation of two lists *)
69
Fixpoint app (l m:list) {struct l} : list :=
72
| a :: l1 => a :: app l1 m
75
Infix "++" := app (right associativity, at level 60) : list_scope.
79
(** Exporting list notations and tactics *)
81
Implicit Arguments nil [A].
82
Infix "::" := cons (at level 60, right associativity) : list_scope.
83
Infix "++" := app (right associativity, at level 60) : list_scope.
85
Open Scope list_scope.
87
Delimit Scope list_scope with list.
89
Bind Scope list_scope with list.
91
Arguments Scope list [type_scope].
93
(** ** Facts about lists *)
100
(** *** Genereric facts *)
102
(** Discrimination *)
103
Theorem nil_cons : forall (x:A) (l:list A), nil <> x :: l.
105
intros; discriminate.
111
Theorem destruct_list : forall l : list A, {x:A & {tl:list A | l = x::tl}}+{l = nil}.
113
induction l as [|a tl].
115
left; exists a; exists tl; reflexivity.
118
(** *** Head and tail *)
120
Theorem head_nil : head (@nil A) = None.
125
Theorem head_cons : forall (l : list A) (x : A), head (x::l) = Some x.
127
intros; simpl; reflexivity.
131
(************************)
132
(** *** Facts about [In] *)
133
(************************)
136
(** Characterization of [In] *)
138
Theorem in_eq : forall (a:A) (l:list A), In a (a :: l).
143
Theorem in_cons : forall (a b:A) (l:list A), In b l -> In b (a :: l).
148
Theorem in_nil : forall a:A, ~ In a nil.
150
unfold not in |- *; intros a H; inversion_clear H.
153
Lemma In_split : forall x (l:list A), In x l -> exists l1, exists l2, l = l1++x::l2.
155
induction l; simpl; destruct 1.
157
exists (@nil A); exists l; auto.
158
destruct (IHl H) as (l1,(l2,H0)).
159
exists (a::l1); exists l2; simpl; f_equal; auto.
163
Theorem in_inv : forall (a b:A) (l:list A), In b (a :: l) -> a = b \/ In b l.
165
intros a b l H; inversion_clear H; auto.
168
(** Decidability of [In] *)
170
(forall x y:A, {x = y} + {x <> y}) ->
171
forall (a:A) (l:list A), {In a l} + {~ In a l}.
173
intro H; induction l as [| a0 l IHl].
175
destruct (H a0 a); simpl in |- *; auto.
176
destruct IHl; simpl in |- *; auto.
177
right; unfold not in |- *; intros [Hc1| Hc2]; auto.
181
(*************************)
182
(** *** Facts about [app] *)
183
(*************************)
185
(** Discrimination *)
186
Theorem app_cons_not_nil : forall (x y:list A) (a:A), nil <> x ++ a :: y.
189
destruct x as [| a l]; simpl in |- *; intros.
195
(** Concat with [nil] *)
197
Theorem app_nil_end : forall l:list A, l = l ++ nil.
199
induction l; simpl in |- *; auto.
200
rewrite <- IHl; auto.
203
(** [app] is associative *)
204
Theorem app_ass : forall l m n:list A, (l ++ m) ++ n = l ++ m ++ n.
206
intros. induction l; simpl in |- *; auto.
207
now_show (a :: (l ++ m) ++ n = a :: l ++ m ++ n).
208
rewrite <- IHl; auto.
210
Hint Resolve app_ass.
212
Theorem ass_app : forall l m n:list A, l ++ m ++ n = (l ++ m) ++ n.
217
(** [app] commutes with [cons] *)
218
Theorem app_comm_cons : forall (x y:list A) (a:A), a :: (x ++ y) = (a :: x) ++ y.
225
(** Facts deduced from the result of a concatenation *)
227
Theorem app_eq_nil : forall l l':list A, l ++ l' = nil -> l = nil /\ l' = nil.
229
destruct l as [| x l]; destruct l' as [| y l']; simpl in |- *; auto.
231
intros H; discriminate H.
234
Theorem app_eq_unit :
235
forall (x y:list A) (a:A),
236
x ++ y = a :: nil -> x = nil /\ y = a :: nil \/ x = a :: nil /\ y = nil.
238
destruct x as [| a l]; [ destruct y as [| a l] | destruct y as [| a0 l0] ];
240
intros a H; discriminate H.
244
generalize (app_nil_end l); intros E.
249
cut (nil = l ++ a0 :: l0); auto.
251
generalize (app_cons_not_nil _ _ _ H1); intro.
256
forall (x y:list A) (a b:A), x ++ a :: nil = y ++ b :: nil -> x = y /\ a = b.
258
induction x as [| x l IHl];
259
[ destruct y as [| a l] | destruct y as [| a l0] ];
266
generalize (app_cons_not_nil _ _ _ H0); destruct 1.
269
cut (nil = l ++ a :: nil); auto.
271
generalize (app_cons_not_nil _ _ _ H2); destruct 1.
274
destruct (IHl l0 a0 b H0).
276
rewrite <- H1; rewrite <- H2; reflexivity.
280
(** Compatibility wtih other operations *)
282
Lemma app_length : forall l l' : list A, length (l++l') = length l + length l'.
284
induction l; simpl; auto.
287
Lemma in_app_or : forall (l m:list A) (a:A), In a (l ++ m) -> In a l \/ In a m.
290
elim l; simpl in |- *; auto.
292
now_show ((a0 = a \/ In a y) \/ In a m).
295
now_show ((a0 = a \/ In a y) \/ In a m).
299
Lemma in_or_app : forall (l m:list A) (a:A), In a l \/ In a m -> In a (l ++ m).
302
elim l; simpl in |- *; intro H.
304
elim H; auto; intro H0.
306
elim H0. (* subProof completed *)
308
now_show (H = a \/ In a (y ++ m)).
311
now_show (H = a \/ In a (y ++ m)).
316
forall l l1 l2 : list A, l ++ l1 = l ++ l2 -> l1 = l2.
318
induction l; simpl; auto; injection 1; auto.
322
forall l l1 l2 : list A, l1 ++ l = l2 ++ l -> l1 = l2.
324
intros l l1 l2; revert l1 l2 l.
325
induction l1 as [ | x1 l1]; destruct l2 as [ | x2 l2];
326
simpl; auto; intros l H.
327
absurd (length (x2 :: l2 ++ l) <= length l).
328
simpl; rewrite app_length; auto with arith.
329
rewrite <- H; auto with arith.
330
absurd (length (x1 :: l1 ++ l) <= length l).
331
simpl; rewrite app_length; auto with arith.
332
rewrite H; auto with arith.
333
injection H; clear H; intros; f_equal; eauto.
338
Hint Resolve app_nil_end ass_app app_ass: datatypes v62.
339
Hint Resolve app_comm_cons app_cons_not_nil: datatypes v62.
340
Hint Immediate app_eq_nil: datatypes v62.
341
Hint Resolve app_eq_unit app_inj_tail: datatypes v62.
342
Hint Resolve in_eq in_cons in_inv in_nil in_app_or in_or_app: datatypes v62.
346
(*******************************************)
347
(** * Operations on the elements of a list *)
348
(*******************************************)
354
(*****************************)
355
(** ** Nth element of a list *)
356
(*****************************)
358
Fixpoint nth (n:nat) (l:list A) (default:A) {struct l} : A :=
361
| O, other => default
362
| S m, nil => default
363
| S m, x :: t => nth m t default
366
Fixpoint nth_ok (n:nat) (l:list A) (default:A) {struct l} : bool :=
371
| S m, x :: t => nth_ok m t default
374
Lemma nth_in_or_default :
375
forall (n:nat) (l:list A) (d:A), {In (nth n l d) l} + {nth n l d = d}.
376
(* Realizer nth_ok. Program_all. *)
378
intros n l d; generalize n; induction l; intro n0.
379
right; case n0; trivial.
380
case n0; simpl in |- *.
382
intro n1; elim (IHl n1); auto.
386
forall (n:nat) (l:list A) (d a:A),
387
In (nth n l d) l -> In (nth (S n) (a :: l) d) (a :: l).
392
Fixpoint nth_error (l:list A) (n:nat) {struct n} : Exc A :=
394
| O, x :: _ => value x
395
| S n, _ :: l => nth_error l n
399
Definition nth_default (default:A) (l:list A) (n:nat) : A :=
400
match nth_error l n with
406
forall (n:nat) (l:list A) (d:A), n < length l -> In (nth n l d) l.
409
unfold lt in |- *; induction n as [| n hn]; simpl in |- *.
410
destruct l; simpl in |- *; [ inversion 2 | auto ].
411
destruct l as [| a l hl]; simpl in |- *.
413
intros d ie; right; apply hn; auto with arith.
416
Lemma nth_overflow : forall l n d, length l <= n -> nth n l d = d.
418
induction l; destruct n; simpl; intros; auto.
420
apply IHl; auto with arith.
424
forall l n d d', n < length l -> nth n l d = nth n l d'.
426
induction l; simpl; intros; auto.
428
destruct n; simpl; auto with arith.
432
forall l l' d n, n < length l -> nth n (l++l') d = nth n l d.
439
intros; rewrite IHl; auto with arith.
443
forall l l' d n, n >= length l -> nth n (l++l') d = nth (n-length l) l' d.
454
rewrite IHl; auto with arith.
466
Hypothesis eq_dec : forall x y : A, {x = y}+{x <> y}.
468
Fixpoint remove (x : A) (l : list A){struct l} : list A :=
471
| y::tl => if (eq_dec x y) then remove x tl else y::(remove x tl)
474
Theorem remove_In : forall (l : list A) (x : A), ~ In x (remove x l).
476
induction l as [|x l]; auto.
477
intro y; simpl; destruct (eq_dec y x) as [yeqx | yneqx].
479
unfold not; intro HF; simpl in HF; destruct HF; auto.
480
apply (IHl y); assumption.
486
(******************************)
487
(** ** Last element of a list *)
488
(******************************)
490
(** [last l d] returns the last element of the list [l],
491
or the default value [d] if [l] is empty. *)
493
Fixpoint last (l:list A) (d:A) {struct l} : A :=
500
(** [removelast l] remove the last element of [l] *)
502
Fixpoint removelast (l:list A) {struct l} : list A :=
506
| a :: l => a :: removelast l
509
Lemma app_removelast_last :
510
forall l d, l<>nil -> l = removelast l ++ (last l d :: nil).
516
pattern (a0::l) at 1; rewrite IHl with d; auto; discriminate.
520
forall l, l<>nil -> { l' : (list A) & { a : A | l = l'++a::nil}}.
526
exists (@nil A); exists a; auto.
527
destruct IHl as [l' (a',H)]; try discriminate.
529
exists (a::l'); exists a'; auto.
532
Lemma removelast_app :
533
forall l l', l' <> nil -> removelast (l++l') = l ++ removelast l'.
538
assert (l++l' <> nil).
542
specialize (IHl l' H).
543
destruct (l++l'); [elim H0; auto|f_equal; auto].
547
(****************************************)
548
(** ** Counting occurences of a element *)
549
(****************************************)
551
Hypotheses eqA_dec : forall x y : A, {x = y}+{x <> y}.
553
Fixpoint count_occ (l : list A) (x : A){struct l} : nat :=
557
let n := count_occ tl x in
558
if eqA_dec y x then S n else n
561
(** Compatibility of count_occ with operations on list *)
562
Theorem count_occ_In : forall (l : list A) (x : A), In x l <-> count_occ l x > 0.
564
induction l as [|y l].
565
simpl; intros; split; [destruct 1 | apply gt_irrefl].
566
simpl. intro x; destruct (eqA_dec y x) as [Heq|Hneq].
567
rewrite Heq; intuition.
568
pose (IHl x). intuition.
571
Theorem count_occ_inv_nil : forall (l : list A), (forall x:A, count_occ l x = 0) <-> l = nil.
575
induction l as [|x l].
578
elim (O_S (count_occ l x)).
581
simpl. destruct (eqA_dec x x) as [|HF].
583
elim HF; reflexivity.
585
intro H; rewrite H; simpl; reflexivity.
588
Lemma count_occ_nil : forall (x : A), count_occ nil x = 0.
590
intro x; simpl; reflexivity.
593
Lemma count_occ_cons_eq : forall (l : list A) (x y : A), x = y -> count_occ (x::l) y = S (count_occ l y).
595
intros l x y H; simpl.
596
destruct (eqA_dec x y); [reflexivity | contradiction].
599
Lemma count_occ_cons_neq : forall (l : list A) (x y : A), x <> y -> count_occ (x::l) y = count_occ l y.
601
intros l x y H; simpl.
602
destruct (eqA_dec x y); [contradiction | reflexivity].
609
(*******************************)
610
(** * Manipulating whole lists *)
611
(*******************************)
617
(*************************)
619
(*************************)
621
Fixpoint rev (l:list A) : list A :=
624
| x :: l' => rev l' ++ x :: nil
627
Lemma distr_rev : forall x y:list A, rev (x ++ y) = rev y ++ rev x.
629
induction x as [| a l IHl].
630
destruct y as [| a l].
635
apply app_nil_end; auto.
640
apply (app_ass (rev y) (rev l) (a :: nil)).
643
Remark rev_unit : forall (l:list A) (a:A), rev (l ++ a :: nil) = a :: rev l.
646
apply (distr_rev l (a :: nil)); simpl in |- *; auto.
649
Lemma rev_involutive : forall l:list A, rev (rev l) = l.
651
induction l as [| a l IHl].
655
rewrite (rev_unit (rev l) a).
660
(** Compatibility with other operations *)
662
Lemma In_rev : forall l x, In x l <-> In x (rev l).
670
apply in_or_app; right; simpl; auto.
671
apply in_or_app; left; firstorder.
672
destruct (in_app_or _ _ _ H); firstorder.
675
Lemma rev_length : forall l, length (rev l) = length l.
677
induction l;simpl; auto.
681
elim (length l); simpl; auto.
684
Lemma rev_nth : forall l d n, n < length l ->
685
nth n (rev l) d = nth (length l - S n) l d.
691
simpl (rev (a :: l)).
692
simpl (length (a :: l) - S n).
694
rewrite <- minus_n_n; simpl.
695
rewrite <- rev_length.
696
rewrite app_nth2; auto.
697
rewrite <- minus_n_n; auto.
698
rewrite app_nth1; auto.
699
rewrite (minus_plus_simpl_l_reverse (length l) n 1).
700
replace (1 + length l) with (S (length l)); auto with arith.
701
rewrite <- minus_Sn_m; auto with arith.
702
apply IHl ; auto with arith.
703
rewrite rev_length; auto.
707
(** An alternative tail-recursive definition for reverse *)
709
Fixpoint rev_append (l l': list A) {struct l} : list A :=
712
| a::l => rev_append l (a::l')
715
Definition rev' l : list A := rev_append l nil.
717
Notation rev_acc := rev_append (only parsing).
719
Lemma rev_append_rev : forall l l', rev_acc l l' = rev l ++ l'.
721
induction l; simpl; auto; intros.
722
rewrite <- ass_app; firstorder.
725
Notation rev_acc_rev := rev_append_rev (only parsing).
727
Lemma rev_alt : forall l, rev l = rev_append l nil.
729
intros; rewrite rev_append_rev.
734
(*********************************************)
735
(** Reverse Induction Principle on Lists *)
736
(*********************************************)
738
Section Reverse_Induction.
740
Unset Implicit Arguments.
743
forall P:list A-> Prop,
745
(forall (a:A) (l:list A), P (rev l) -> P (rev (a :: l))) ->
746
forall l:list A, P (rev l).
750
Set Implicit Arguments.
753
forall P:list A -> Prop,
755
(forall (x:A) (l:list A), P l -> P (l ++ x :: nil)) -> forall l:list A, P l.
758
generalize (rev_involutive l).
759
intros E; rewrite <- E.
760
apply (rev_list_ind P).
765
apply (H0 a (rev l0)).
769
End Reverse_Induction.
773
(***********************************)
774
(** ** Lists modulo permutation *)
775
(***********************************)
779
Inductive Permutation : list A -> list A -> Prop :=
780
| perm_nil: Permutation nil nil
781
| perm_skip: forall (x:A) (l l':list A), Permutation l l' -> Permutation (cons x l) (cons x l')
782
| perm_swap: forall (x y:A) (l:list A), Permutation (cons y (cons x l)) (cons x (cons y l))
783
| perm_trans: forall (l l' l'':list A), Permutation l l' -> Permutation l' l'' -> Permutation l l''.
785
Hint Constructors Permutation.
787
(** Some facts about [Permutation] *)
789
Theorem Permutation_nil : forall (l : list A), Permutation nil l -> l = nil.
792
set (m:=@nil A) in HF; assert (m = nil); [reflexivity|idtac]; clearbody m.
793
induction HF; try elim (nil_cons (sym_eq H)); auto.
796
Theorem Permutation_nil_cons : forall (l : list A) (x : A), ~ Permutation nil (x::l).
798
unfold not; intros l x HF.
799
elim (@nil_cons A x l). apply sym_eq. exact (Permutation_nil HF).
802
(** Permutation over lists is a equivalence relation *)
804
Theorem Permutation_refl : forall l : list A, Permutation l l.
806
induction l; constructor. exact IHl.
809
Theorem Permutation_sym : forall l l' : list A, Permutation l l' -> Permutation l' l.
811
intros l l' Hperm; induction Hperm; auto.
812
apply perm_trans with (l':=l'); assumption.
815
Theorem Permutation_trans : forall l l' l'' : list A, Permutation l l' -> Permutation l' l'' -> Permutation l l''.
820
Hint Resolve Permutation_refl Permutation_sym Permutation_trans.
822
(** Compatibility with others operations on lists *)
824
Theorem Permutation_in : forall (l l' : list A) (x : A), Permutation l l' -> In x l -> In x l'.
826
intros l l' x Hperm; induction Hperm; simpl; tauto.
829
Lemma Permutation_app_tail : forall (l l' tl : list A), Permutation l l' -> Permutation (l++tl) (l'++tl).
831
intros l l' tl Hperm; induction Hperm as [|x l l'|x y l|l l' l'']; simpl; auto.
832
eapply Permutation_trans with (l':=l'++tl); trivial.
835
Lemma Permutation_app_head : forall (l tl tl' : list A), Permutation tl tl' -> Permutation (l++tl) (l++tl').
837
intros l tl tl' Hperm; induction l; [trivial | repeat rewrite <- app_comm_cons; constructor; assumption].
840
Theorem Permutation_app : forall (l m l' m' : list A), Permutation l l' -> Permutation m m' -> Permutation (l++m) (l'++m').
842
intros l m l' m' Hpermll' Hpermmm'; induction Hpermll' as [|x l l'|x y l|l l' l'']; repeat rewrite <- app_comm_cons; auto.
843
apply Permutation_trans with (l' := (x :: y :: l ++ m));
844
[idtac | repeat rewrite app_comm_cons; apply Permutation_app_head]; trivial.
845
apply Permutation_trans with (l' := (l' ++ m')); try assumption.
846
apply Permutation_app_tail; assumption.
849
Theorem Permutation_app_swap : forall (l l' : list A), Permutation (l++l') (l'++l).
851
induction l as [|x l].
852
simpl; intro l'; rewrite <- app_nil_end; trivial.
853
induction l' as [|y l'].
854
simpl; rewrite <- app_nil_end; trivial.
855
simpl; apply Permutation_trans with (l' := x :: y :: l' ++ l).
856
constructor; rewrite app_comm_cons; apply IHl.
857
apply Permutation_trans with (l' := y :: x :: l' ++ l); constructor.
858
apply Permutation_trans with (l' := x :: l ++ l'); auto.
861
Theorem Permutation_cons_app : forall (l l1 l2:list A) a,
862
Permutation l (l1 ++ l2) -> Permutation (a :: l) (l1 ++ a :: l2).
864
intros l l1; revert l.
867
intros; apply perm_skip; auto.
869
apply perm_trans with (a0::a::l1++l2).
870
apply perm_skip; auto.
871
apply perm_trans with (a::a0::l1++l2).
872
apply perm_swap; auto.
873
apply perm_skip; auto.
875
Hint Resolve Permutation_cons_app.
877
Theorem Permutation_length : forall (l l' : list A), Permutation l l' -> length l = length l'.
879
intros l l' Hperm; induction Hperm; simpl; auto.
880
apply trans_eq with (y:= (length l')); trivial.
883
Theorem Permutation_rev : forall (l : list A), Permutation l (rev l).
885
induction l as [| x l]; simpl; trivial.
886
apply Permutation_trans with (l' := (x::nil)++rev l).
888
apply Permutation_app_swap.
891
Theorem Permutation_ind_bis :
892
forall P : list A -> list A -> Prop,
893
P (@nil A) (@nil A) ->
894
(forall x l l', Permutation l l' -> P l l' -> P (x :: l) (x :: l')) ->
895
(forall x y l l', Permutation l l' -> P l l' -> P (y :: x :: l) (x :: y :: l')) ->
896
(forall l l' l'', Permutation l l' -> P l l' -> Permutation l' l'' -> P l' l'' -> P l l'') ->
897
forall l l', Permutation l l' -> P l l'.
899
intros P Hnil Hskip Hswap Htrans.
901
apply Htrans with (x::y::l); auto.
910
Ltac break_list l x l' H :=
911
destruct l as [|x l']; simpl in *;
912
injection H; intros; subst; clear H.
914
Theorem Permutation_app_inv : forall (l1 l2 l3 l4:list A) a,
915
Permutation (l1++a::l2) (l3++a::l4) -> Permutation (l1++l2) (l3 ++ l4).
918
forall a l1 l2 l3 l4, l=l1++a::l2 -> l'=l3++a::l4 -> Permutation (l1++l2) (l3++l4)).
919
cut (forall l l', Permutation l l' -> P l l').
920
intros; apply (H _ _ H0 a); auto.
921
intros; apply (Permutation_ind_bis P); unfold P; clear P; try clear H l l'; simpl; auto.
923
intros; destruct l1; simpl in *; discriminate.
925
intros x l l' H IH; intros.
926
break_list l1 b l1' H0; break_list l3 c l3' H1.
928
apply perm_trans with (l3'++c::l4); auto.
929
apply perm_trans with (l1'++a::l2); auto using Permutation_cons_app.
931
apply (IH a l1' l2 l3' l4); auto.
933
intros x y l l' Hp IH; intros.
934
break_list l1 b l1' H; break_list l3 c l3' H0.
936
break_list l3' b l3'' H.
938
apply perm_trans with (c::l3''++b::l4); auto.
939
break_list l1' c l1'' H1.
941
apply perm_trans with (b::l1''++c::l2); auto.
942
break_list l3' d l3'' H; break_list l1' e l1'' H1.
944
apply perm_trans with (e::a::l1''++l2); auto.
945
apply perm_trans with (e::l1''++a::l2); auto.
946
apply perm_trans with (d::a::l3''++l4); auto.
947
apply perm_trans with (d::l3''++a::l4); auto.
948
apply perm_trans with (e::d::l1''++l2); auto.
949
apply perm_skip; apply perm_skip.
950
apply (IH a l1'' l2 l3'' l4); auto.
953
destruct (In_split a l') as (l'1,(l'2,H6)).
954
apply (Permutation_in a H).
956
apply in_or_app; right; red; auto.
957
apply perm_trans with (l'1++l'2).
958
apply (H0 _ _ _ _ _ H3 H6).
959
apply (H2 _ _ _ _ _ H6 H4).
962
Theorem Permutation_cons_inv :
963
forall l l' a, Permutation (a::l) (a::l') -> Permutation l l'.
965
intros; exact (Permutation_app_inv (@nil _) l (@nil _) l' a H).
968
Theorem Permutation_cons_app_inv :
969
forall l l1 l2 a, Permutation (a :: l) (l1 ++ a :: l2) -> Permutation l (l1 ++ l2).
971
intros; exact (Permutation_app_inv (@nil _) l l1 l2 a H).
974
Theorem Permutation_app_inv_l :
975
forall l l1 l2, Permutation (l ++ l1) (l ++ l2) -> Permutation l1 l2.
977
induction l; simpl; auto.
980
apply Permutation_cons_inv with a; auto.
983
Theorem Permutation_app_inv_r :
984
forall l l1 l2, Permutation (l1 ++ l) (l2 ++ l) -> Permutation l1 l2.
987
intros l1 l2; do 2 rewrite <- app_nil_end; auto.
990
apply Permutation_app_inv with a; auto.
996
(***********************************)
997
(** ** Decidable equality on lists *)
998
(***********************************)
1000
Hypotheses eqA_dec : forall (x y : A), {x = y}+{x <> y}.
1003
forall l l':list A, {l = l'} + {l <> l'}.
1005
induction l as [| x l IHl]; destruct l' as [| y l'].
1007
right; apply nil_cons.
1008
right; unfold not; intro HF; apply (nil_cons (sym_eq HF)).
1009
destruct (eqA_dec x y) as [xeqy|xneqy]; destruct (IHl l') as [leql'|lneql'];
1010
try (right; unfold not; intro HF; injection HF; intros; contradiction).
1011
rewrite xeqy; rewrite leql'; left; trivial.
1018
(***************************************************)
1019
(** * Applying functions to the elements of a list *)
1020
(***************************************************)
1027
Variables A B : Type.
1028
Variable f : A -> B.
1030
Fixpoint map (l:list A) : list B :=
1033
| cons a t => cons (f a) (map t)
1037
forall (l:list A) (x:A), In x l -> In (f x) (map l).
1039
induction l as [| a l IHl]; simpl in |- *;
1041
| destruct 1; [ left; apply f_equal with (f := f); assumption | auto ] ].
1044
Lemma in_map_iff : forall l y, In y (map l) <-> exists x, f x = y /\ In x l.
1046
induction l; firstorder (subst; auto).
1049
Lemma map_length : forall l, length (map l) = length l.
1051
induction l; simpl; auto.
1054
Lemma map_nth : forall l d n,
1055
nth n (map l) (f d) = f (nth n l d).
1057
induction l; simpl map; destruct n; firstorder.
1060
Lemma map_app : forall l l',
1061
map (l++l') = (map l)++(map l').
1063
induction l; simpl; auto.
1064
intros; rewrite IHl; auto.
1067
Lemma map_rev : forall l, map (rev l) = rev (map l).
1069
induction l; simpl; auto.
1074
Hint Constructors Permutation.
1076
Lemma Permutation_map :
1077
forall l l', Permutation l l' -> Permutation (map l) (map l').
1079
induction 1; simpl; auto; eauto.
1084
Fixpoint flat_map (f:A -> list B) (l:list A) {struct l} :
1088
| cons x t => (f x)++(flat_map f t)
1091
Lemma in_flat_map : forall (f:A->list B)(l:list A)(y:B),
1092
In y (flat_map f l) <-> exists x, In x l /\ In y (f x).
1094
induction l; simpl; split; intros.
1096
destruct H as (x,(H,_)); contradiction.
1097
destruct (in_app_or _ _ _ H).
1099
destruct (IHl y) as (H1,_); destruct (H1 H0) as (x,(H2,H3)).
1102
destruct H as (x,(H0,H1)); destruct H0.
1104
right; destruct (IHl y) as (_,H2); apply H2.
1110
Lemma map_map : forall (A B C:Type)(f:A->B)(g:B->C) l,
1111
map g (map f l) = map (fun x => g (f x)) l.
1113
induction l; simpl; auto.
1118
forall (A B : Type)(f g:A->B), (forall a, f a = g a) -> forall l, map f l = map g l.
1120
induction l; simpl; auto.
1121
rewrite H; rewrite IHl; auto.
1125
(************************************)
1126
(** Left-to-right iterator on lists *)
1127
(************************************)
1129
Section Fold_Left_Recursor.
1130
Variables A B : Type.
1131
Variable f : A -> B -> A.
1133
Fixpoint fold_left (l:list B) (a0:A) {struct l} : A :=
1136
| cons b t => fold_left t (f a0 b)
1139
Lemma fold_left_app : forall (l l':list B)(i:A),
1140
fold_left (l++l') i = fold_left l' (fold_left l i).
1149
End Fold_Left_Recursor.
1151
Lemma fold_left_length :
1152
forall (A:Type)(l:list A), fold_left (fun x _ => S x) l 0 = length l.
1155
cut (forall (l:list A) n, fold_left (fun x _ => S x) l n = n + length l).
1158
induction l; simpl; auto.
1159
intros; rewrite IHl.
1160
simpl; auto with arith.
1163
(************************************)
1164
(** Right-to-left iterator on lists *)
1165
(************************************)
1167
Section Fold_Right_Recursor.
1168
Variables A B : Type.
1169
Variable f : B -> A -> A.
1172
Fixpoint fold_right (l:list B) : A :=
1175
| cons b t => f b (fold_right t)
1178
End Fold_Right_Recursor.
1180
Lemma fold_right_app : forall (A B:Type)(f:A->B->B) l l' i,
1181
fold_right f i (l++l') = fold_right f (fold_right f i l') l.
1189
Lemma fold_left_rev_right : forall (A B:Type)(f:A->B->B) l i,
1190
fold_right f i (rev l) = fold_left (fun x y => f y x) l i.
1196
rewrite fold_right_app; simpl; auto.
1199
Theorem fold_symmetric :
1200
forall (A:Type) (f:A -> A -> A),
1201
(forall x y z:A, f x (f y z) = f (f x y) z) ->
1202
(forall x y:A, f x y = f y x) ->
1203
forall (a0:A) (l:list A), fold_left f l a0 = fold_right f a0 l.
1205
destruct l as [| a l].
1210
induction l as [| a3 l IHl]; simpl in |- *.
1223
(** [(list_power x y)] is [y^x], or the set of sequences of elts of [y]
1224
indexed by elts of [x], sorted in lexicographic order. *)
1226
Fixpoint list_power (A B:Type)(l:list A) (l':list B) {struct l} :
1227
list (list (A * B)) :=
1229
| nil => cons nil nil
1231
flat_map (fun f:list (A * B) => map (fun y:B => cons (x, y) f) l')
1236
(*************************************)
1237
(** ** Boolean operations over lists *)
1238
(*************************************)
1242
Variable f : A -> bool.
1244
(** find whether a boolean function can be satisfied by an
1245
elements of the list. *)
1247
Fixpoint existsb (l:list A) {struct l}: bool :=
1250
| a::l => f a || existsb l
1253
Lemma existsb_exists :
1254
forall l, existsb l = true <-> exists x, In x l /\ f x = true.
1256
induction l; simpl; intuition.
1259
destruct (orb_prop _ _ H1); firstorder.
1265
Lemma existsb_nth : forall l n d, n < length l ->
1266
existsb l = false -> f (nth n l d) = false.
1271
destruct (orb_false_elim _ _ H0); clear H0; auto.
1273
rewrite IHl; auto with arith.
1276
(** find whether a boolean function is satisfied by
1277
all the elements of a list. *)
1279
Fixpoint forallb (l:list A) {struct l} : bool :=
1282
| a::l => f a && forallb l
1285
Lemma forallb_forall :
1286
forall l, forallb l = true <-> (forall x, In x l -> f x = true).
1288
induction l; simpl; intuition.
1289
destruct (andb_prop _ _ H1).
1291
destruct (andb_prop _ _ H1); auto.
1292
assert (forallb l = true).
1293
apply H0; intuition.
1299
Fixpoint filter (l:list A) : list A :=
1302
| x :: l => if f x then x::(filter l) else filter l
1305
Lemma filter_In : forall x l, In x (filter l) <-> In x l /\ f x = true.
1310
case_eq (f a); intros; simpl; intuition congruence.
1315
Fixpoint find (l:list A) : option A :=
1318
| x :: tl => if f x then Some x else find tl
1323
Fixpoint partition (l:list A) {struct l} : list A * list A :=
1326
| x :: tl => let (g,d) := partition tl in
1327
if f x then (x::g,d) else (g,x::d)
1335
(******************************************************)
1336
(** ** Operations on lists of pairs or lists of lists *)
1337
(******************************************************)
1340
Variables A B : Type.
1342
(** [split] derives two lists from a list of pairs *)
1344
Fixpoint split (l:list (A*B)) { struct l }: list A * list B :=
1347
| (x,y) :: tl => let (g,d) := split tl in (x::g, y::d)
1350
Lemma in_split_l : forall (l:list (A*B))(p:A*B),
1351
In p l -> In (fst p) (fst (split l)).
1353
induction l; simpl; intros; auto.
1354
destruct p; destruct a; destruct (split l); simpl in *.
1357
right; apply (IHl (a0,b) H).
1360
Lemma in_split_r : forall (l:list (A*B))(p:A*B),
1361
In p l -> In (snd p) (snd (split l)).
1363
induction l; simpl; intros; auto.
1364
destruct p; destruct a; destruct (split l); simpl in *.
1367
right; apply (IHl (a0,b) H).
1370
Lemma split_nth : forall (l:list (A*B))(n:nat)(d:A*B),
1371
nth n l d = (nth n (fst (split l)) (fst d), nth n (snd (split l)) (snd d)).
1374
destruct n; destruct d; simpl; auto.
1375
destruct n; destruct d; simpl; auto.
1376
destruct a; destruct (split l); simpl; auto.
1377
destruct a; destruct (split l); simpl in *; auto.
1381
Lemma split_length_l : forall (l:list (A*B)),
1382
length (fst (split l)) = length l.
1384
induction l; simpl; auto.
1385
destruct a; destruct (split l); simpl; auto.
1388
Lemma split_length_r : forall (l:list (A*B)),
1389
length (snd (split l)) = length l.
1391
induction l; simpl; auto.
1392
destruct a; destruct (split l); simpl; auto.
1395
(** [combine] is the opposite of [split].
1396
Lists given to [combine] are meant to be of same length.
1397
If not, [combine] stops on the shorter list *)
1399
Fixpoint combine (l : list A) (l' : list B){struct l} : list (A*B) :=
1401
| x::tl, y::tl' => (x,y)::(combine tl tl')
1405
Lemma split_combine : forall (l: list (A*B)),
1406
let (l1,l2) := split l in combine l1 l2 = l.
1411
destruct (split l); simpl in *.
1415
Lemma combine_split : forall (l:list A)(l':list B), length l = length l' ->
1416
split (combine l l') = (l,l').
1418
induction l; destruct l'; simpl; intros; auto; try discriminate.
1419
injection H; clear H; intros.
1423
Lemma in_combine_l : forall (l:list A)(l':list B)(x:A)(y:B),
1424
In (x,y) (combine l l') -> In x l.
1428
destruct l'; simpl; auto; intros.
1432
right; apply IHl with l' y; auto.
1435
Lemma in_combine_r : forall (l:list A)(l':list B)(x:A)(y:B),
1436
In (x,y) (combine l l') -> In y l'.
1439
simpl; intros; contradiction.
1440
destruct l'; simpl; auto; intros.
1443
right; apply IHl with x; auto.
1446
Lemma combine_length : forall (l:list A)(l':list B),
1447
length (combine l l') = min (length l) (length l').
1451
destruct l'; simpl; auto.
1454
Lemma combine_nth : forall (l:list A)(l':list B)(n:nat)(x:A)(y:B),
1455
length l = length l' ->
1456
nth n (combine l l') (x,y) = (nth n l x, nth n l' y).
1458
induction l; destruct l'; intros; try discriminate.
1459
destruct n; simpl; auto.
1460
destruct n; simpl in *; auto.
1463
(** [list_prod] has the same signature as [combine], but unlike
1464
[combine], it adds every possible pairs, not only those at the
1467
Fixpoint list_prod (l:list A) (l':list B) {struct l} :
1471
| cons x t => (map (fun y:B => (x, y)) l')++(list_prod t l')
1475
forall (x:A) (y:B) (l:list B),
1476
In y l -> In (x, y) (map (fun y0:B => (x, y0)) l).
1479
[ simpl in |- *; auto
1480
| simpl in |- *; destruct 1 as [H1| ];
1481
[ left; rewrite H1; trivial | right; auto ] ].
1485
forall (l:list A) (l':list B) (x:A) (y:B),
1486
In x l -> In y l' -> In (x, y) (list_prod l l').
1489
[ simpl in |- *; tauto
1490
| simpl in |- *; intros; apply in_or_app; destruct H;
1491
[ left; rewrite H; apply in_prod_aux; assumption | right; auto ] ].
1495
forall (l:list A)(l':list B)(x:A)(y:B),
1496
In (x,y) (list_prod l l') <-> In x l /\ In y l'.
1498
split; [ | intros; apply in_prod; intuition ].
1499
induction l; simpl; intros.
1501
destruct (in_app_or _ _ _ H); clear H.
1502
destruct (in_map_iff (fun y : B => (a, y)) l' (x,y)) as (H1,_).
1503
destruct (H1 H0) as (z,(H2,H3)); clear H0 H1.
1504
injection H2; clear H2; intros; subst; intuition.
1508
Lemma prod_length : forall (l:list A)(l':list B),
1509
length (list_prod l l') = (length l) * (length l').
1511
induction l; simpl; auto.
1523
(***************************************)
1524
(** * Miscelenous operations on lists *)
1525
(***************************************)
1529
(******************************)
1530
(** ** Length order of lists *)
1531
(******************************)
1533
Section length_order.
1536
Definition lel (l m:list A) := length l <= length m.
1539
Variables l m n : list A.
1541
Lemma lel_refl : lel l l.
1543
unfold lel in |- *; auto with arith.
1546
Lemma lel_trans : lel l m -> lel m n -> lel l n.
1548
unfold lel in |- *; intros.
1549
now_show (length l <= length n).
1550
apply le_trans with (length m); auto with arith.
1553
Lemma lel_cons_cons : lel l m -> lel (a :: l) (b :: m).
1555
unfold lel in |- *; simpl in |- *; auto with arith.
1558
Lemma lel_cons : lel l m -> lel l (b :: m).
1560
unfold lel in |- *; simpl in |- *; auto with arith.
1563
Lemma lel_tail : lel (a :: l) (b :: m) -> lel l m.
1565
unfold lel in |- *; simpl in |- *; auto with arith.
1568
Lemma lel_nil : forall l':list A, lel l' nil -> nil = l'.
1570
intro l'; elim l'; auto with arith.
1572
now_show (nil = a' :: y).
1573
absurd (S (length y) <= 0); auto with arith.
1577
Hint Resolve lel_refl lel_cons_cons lel_cons lel_nil lel_nil nil_cons:
1581
(******************************)
1582
(** ** Set inclusion on list *)
1583
(******************************)
1589
Definition incl (l m:list A) := forall a:A, In a l -> In a m.
1592
Lemma incl_refl : forall l:list A, incl l l.
1596
Hint Resolve incl_refl.
1598
Lemma incl_tl : forall (a:A) (l m:list A), incl l m -> incl l (a :: m).
1600
auto with datatypes.
1602
Hint Immediate incl_tl.
1604
Lemma incl_tran : forall l m n:list A, incl l m -> incl m n -> incl l n.
1609
Lemma incl_appl : forall l m n:list A, incl l n -> incl l (n ++ m).
1611
auto with datatypes.
1613
Hint Immediate incl_appl.
1615
Lemma incl_appr : forall l m n:list A, incl l n -> incl l (m ++ n).
1617
auto with datatypes.
1619
Hint Immediate incl_appr.
1622
forall (a:A) (l m:list A), In a m -> incl l m -> incl (a :: l) m.
1624
unfold incl in |- *; simpl in |- *; intros a l m H H0 a0 H1.
1627
now_show (a = a0 -> In a0 m).
1628
elim H1; auto; intro H2.
1629
now_show (a = a0 -> In a0 m).
1630
elim H2; auto. (* solves subgoal *)
1631
now_show (In a0 l -> In a0 m).
1634
Hint Resolve incl_cons.
1636
Lemma incl_app : forall l m n:list A, incl l n -> incl m n -> incl (l ++ m) n.
1638
unfold incl in |- *; simpl in |- *; intros l m n H H0 a H1.
1640
elim (in_app_or _ _ _ H1); auto.
1642
Hint Resolve incl_app.
1646
Hint Resolve incl_refl incl_tl incl_tran incl_appl incl_appr incl_cons
1647
incl_app: datatypes v62.
1650
(**************************************)
1651
(** * Cutting a list at some position *)
1652
(**************************************)
1658
Fixpoint firstn (n:nat)(l:list A) {struct n} : list A :=
1661
| S n => match l with
1663
| a::l => a::(firstn n l)
1667
Fixpoint skipn (n:nat)(l:list A) { struct n } : list A :=
1670
| S n => match l with
1676
Lemma firstn_skipn : forall n l, firstn n l ++ skipn n l = l.
1680
destruct l; simpl; auto.
1684
Lemma firstn_length : forall n l, length (firstn n l) = min n (length l).
1686
induction n; destruct l; simpl; auto.
1689
Lemma removelast_firstn : forall n l, n < length l ->
1690
removelast (firstn (S n) l) = firstn n l.
1692
induction n; destruct l.
1698
change (firstn (S (S n)) (a::l)) with ((a::nil)++firstn (S n) l).
1699
change (firstn (S n) (a::l)) with (a::firstn n l).
1700
rewrite removelast_app.
1701
rewrite IHn; auto with arith.
1703
clear IHn; destruct l; simpl in *; try discriminate.
1708
Lemma firstn_removelast : forall n l, n < length l ->
1709
firstn n (removelast l) = firstn n l.
1711
induction n; destruct l.
1717
change (removelast (a :: l)) with (removelast ((a::nil)++l)).
1718
rewrite removelast_app.
1719
simpl; f_equal; auto with arith.
1720
intro H0; rewrite H0 in H; inversion_clear H; inversion_clear H1.
1726
(********************************)
1727
(** ** Lists without redundancy *)
1728
(********************************)
1734
Inductive NoDup : list A -> Prop :=
1735
| NoDup_nil : NoDup nil
1736
| NoDup_cons : forall x l, ~ In x l -> NoDup l -> NoDup (x::l).
1738
Lemma NoDup_remove_1 : forall l l' a, NoDup (l++a::l') -> NoDup (l++l').
1741
inversion_clear 1; auto.
1745
apply in_or_app; destruct (in_app_or _ _ _ H0); simpl; tauto.
1746
apply IHl with a0; auto.
1749
Lemma NoDup_remove_2 : forall l l' a, NoDup (l++a::l') -> ~In a (l++l').
1752
inversion_clear 1; auto.
1757
apply in_or_app; right; red; auto.
1758
destruct (IHl _ _ H1); auto.
1761
Lemma NoDup_Permutation : forall l l',
1762
NoDup l -> NoDup l' -> (forall x, In x l <-> In x l') -> Permutation l l'.
1765
destruct l'; simpl; intros.
1767
destruct (H1 a) as (_,H2); destruct H2; auto.
1769
destruct (In_split a l') as (l'1,(l'2,H2)).
1770
destruct (H1 a) as (H2,H3); simpl in *; auto.
1772
apply Permutation_cons_app.
1775
apply NoDup_remove_1 with a; auto.
1776
intro x; split; intros.
1777
assert (In x (l'1++a::l'2)).
1778
destruct (H1 x); simpl in *; auto.
1779
apply in_or_app; destruct (in_app_or _ _ _ H4); auto.
1781
subst x; destruct H2; auto.
1782
assert (In x (l'1++a::l'2)).
1783
apply in_or_app; destruct (in_app_or _ _ _ H); simpl; auto.
1784
destruct (H1 x) as (_,H5); destruct H5; auto.
1786
destruct (NoDup_remove_2 _ _ _ H0 H).
1792
(***********************************)
1793
(** ** Sequence of natural numbers *)
1794
(***********************************)
1798
(** [seq] computes the sequence of [len] contiguous integers
1799
that starts at [start]. For instance, [seq 2 3] is [2::3::4::nil]. *)
1801
Fixpoint seq (start len:nat) {struct len} : list nat :=
1804
| S len => start :: seq (S start) len
1807
Lemma seq_length : forall len start, length (seq start len) = len.
1809
induction len; simpl; auto.
1812
Lemma seq_nth : forall len start n d,
1813
n < len -> nth n (seq start len) d = start+n.
1815
induction len; intros.
1820
rewrite IHlen;simpl; auto with arith.
1823
Lemma seq_shift : forall len start,
1824
map S (seq start len) = seq (S start) len.
1826
induction len; simpl; auto.
1836
(** * Exporting hints and tactics *)
1840
rev_involutive (* rev (rev l) = l *)
1841
rev_unit (* rev (l ++ a :: nil) = a :: rev l *)
1842
map_nth (* nth n (map f l) (f d) = f (nth n l d) *)
1843
map_length (* length (map f l) = length l *)
1844
seq_length (* length (seq start len) = len *)
1845
app_length (* length (l ++ l') = length l + length l' *)
1846
rev_length (* length (rev l) = length l *)
1850
app_nil_end (* l = l ++ nil *)
1853
Ltac simpl_list := autorewrite with list.
1854
Ltac ssimpl_list := autorewrite with list using simpl.
added
removed
theories/Lists/List.v
