diff options
Diffstat (limited to 'theories/Lists/List.v')
| -rw-r--r--[-rwxr-xr-x] | theories/Lists/List.v | 1000 |
1 files changed, 818 insertions, 182 deletions
diff --git a/theories/Lists/List.v b/theories/Lists/List.v index c3f65d67..ad91a350 100755..100644 --- a/theories/Lists/List.v +++ b/theories/Lists/List.v @@ -6,10 +6,9 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: List.v,v 1.9.2.1 2004/07/16 19:31:05 herbelin Exp $ i*) - -Require Import Le. +(*i $Id: List.v 8686 2006-04-06 13:25:10Z letouzey $ i*) +Require Import Le Minus Min Bool. Section Lists. @@ -25,6 +24,8 @@ Infix "::" := cons (at level 60, right associativity) : list_scope. Open Scope list_scope. +Ltac now_show c := change c in |- *. + (*************************) (** Discrimination *) (*************************) @@ -35,108 +36,6 @@ Proof. Qed. (*************************) -(** Concatenation *) -(*************************) - -Fixpoint app (l m:list) {struct l} : list := - match l with - | nil => m - | a :: l1 => a :: app l1 m - end. - -Infix "++" := app (right associativity, at level 60) : list_scope. - -Lemma app_nil_end : forall l:list, l = l ++ nil. -Proof. - induction l; simpl in |- *; auto. - rewrite <- IHl; auto. -Qed. -Hint Resolve app_nil_end. - -Ltac now_show c := change c in |- *. - -Lemma app_ass : forall l m n:list, (l ++ m) ++ n = l ++ m ++ n. -Proof. - intros. induction l; simpl in |- *; auto. - now_show (a :: (l ++ m) ++ n = a :: l ++ m ++ n). - rewrite <- IHl; auto. -Qed. -Hint Resolve app_ass. - -Lemma ass_app : forall l m n:list, l ++ m ++ n = (l ++ m) ++ n. -Proof. - auto. -Qed. -Hint Resolve ass_app. - -Lemma app_comm_cons : forall (x y:list) (a:A), a :: x ++ y = (a :: x) ++ y. -Proof. - auto. -Qed. - -Lemma app_eq_nil : forall x y:list, x ++ y = nil -> x = nil /\ y = nil. -Proof. - destruct x as [| a l]; [ destruct y as [| a l] | destruct y as [| a0 l0] ]; - simpl in |- *; auto. - intros H; discriminate H. - intros; discriminate H. -Qed. - -Lemma app_cons_not_nil : forall (x y:list) (a:A), nil <> x ++ a :: y. -Proof. -unfold not in |- *. - destruct x as [| a l]; simpl in |- *; intros. - discriminate H. - discriminate H. -Qed. - -Lemma app_eq_unit : - forall (x y:list) (a:A), - x ++ y = a :: nil -> x = nil /\ y = a :: nil \/ x = a :: nil /\ y = nil. - -Proof. - destruct x as [| a l]; [ destruct y as [| a l] | destruct y as [| a0 l0] ]; - simpl in |- *. - intros a H; discriminate H. - left; split; auto. - right; split; auto. - generalize H. - generalize (app_nil_end l); intros E. - rewrite <- E; auto. - intros. - injection H. - intro. - cut (nil = l ++ a0 :: l0); auto. - intro. - generalize (app_cons_not_nil _ _ _ H1); intro. - elim H2. -Qed. - -Lemma app_inj_tail : - forall (x y:list) (a b:A), x ++ a :: nil = y ++ b :: nil -> x = y /\ a = b. -Proof. - induction x as [| x l IHl]; - [ destruct y as [| a l] | destruct y as [| a l0] ]; - simpl in |- *; auto. - intros a b H. - injection H. - auto. - intros a0 b H. - injection H; intros. - generalize (app_cons_not_nil _ _ _ H0); destruct 1. - intros a b H. - injection H; intros. - cut (nil = l ++ a :: nil); auto. - intro. - generalize (app_cons_not_nil _ _ _ H2); destruct 1. - intros a0 b H. - injection H; intros. - destruct (IHl l0 a0 b H0). - split; auto. - rewrite <- H1; rewrite <- H2; reflexivity. -Qed. - -(*************************) (** Head and tail *) (*************************) @@ -253,6 +152,189 @@ Proof. destruct (H a0 a); simpl in |- *; auto. destruct IHl; simpl in |- *; auto. right; unfold not in |- *; intros [Hc1| Hc2]; auto. +Defined. + +(**************************) +(** Nth element of a list *) +(**************************) + +Fixpoint nth (n:nat) (l:list) (default:A) {struct l} : A := + match n, l with + | O, x :: l' => x + | O, other => default + | S m, nil => default + | S m, x :: t => nth m t default + end. + +Fixpoint nth_ok (n:nat) (l:list) (default:A) {struct l} : bool := + match n, l with + | O, x :: l' => true + | O, other => false + | S m, nil => false + | S m, x :: t => nth_ok m t default + end. + +Lemma nth_in_or_default : + forall (n:nat) (l:list) (d:A), {In (nth n l d) l} + {nth n l d = d}. +(* Realizer nth_ok. Program_all. *) +Proof. + intros n l d; generalize n; induction l; intro n0. + right; case n0; trivial. + case n0; simpl in |- *. + auto. + intro n1; elim (IHl n1); auto. +Qed. + +Lemma nth_S_cons : + forall (n:nat) (l:list) (d a:A), + In (nth n l d) l -> In (nth (S n) (a :: l) d) (a :: l). +Proof. + simpl in |- *; auto. +Qed. + +Fixpoint nth_error (l:list) (n:nat) {struct n} : Exc A := + match n, l with + | O, x :: _ => value x + | S n, _ :: l => nth_error l n + | _, _ => error + end. + +Definition nth_default (default:A) (l:list) (n:nat) : A := + match nth_error l n with + | Some x => x + | None => default + end. + +Lemma nth_In : + forall (n:nat) (l:list) (d:A), n < length l -> In (nth n l d) l. + +Proof. +unfold lt in |- *; induction n as [| n hn]; simpl in |- *. +destruct l; simpl in |- *; [ inversion 2 | auto ]. +destruct l as [| a l hl]; simpl in |- *. +inversion 2. +intros d ie; right; apply hn; auto with arith. +Qed. + +Lemma nth_overflow : forall l n d, length l <= n -> nth n l d = d. +Proof. +induction l; destruct n; simpl; intros; auto. +inversion H. +apply IHl; auto with arith. +Qed. + +Lemma nth_indep : + forall l n d d', n < length l -> nth n l d = nth n l d'. +Proof. +induction l; simpl; intros; auto. +inversion H. +destruct n; simpl; auto with arith. +Qed. + + +(*************************) +(** Concatenation *) +(*************************) + +Fixpoint app (l m:list) {struct l} : list := + match l with + | nil => m + | a :: l1 => a :: app l1 m + end. + +Infix "++" := app (right associativity, at level 60) : list_scope. + +Lemma app_nil_end : forall l:list, l = l ++ nil. +Proof. + induction l; simpl in |- *; auto. + rewrite <- IHl; auto. +Qed. +Hint Resolve app_nil_end. + +Lemma app_ass : forall l m n:list, (l ++ m) ++ n = l ++ m ++ n. +Proof. + intros. induction l; simpl in |- *; auto. + now_show (a :: (l ++ m) ++ n = a :: l ++ m ++ n). + rewrite <- IHl; auto. +Qed. +Hint Resolve app_ass. + +Lemma ass_app : forall l m n:list, l ++ m ++ n = (l ++ m) ++ n. +Proof. + auto. +Qed. +Hint Resolve ass_app. + +Lemma app_comm_cons : forall (x y:list) (a:A), a :: x ++ y = (a :: x) ++ y. +Proof. + auto. +Qed. + +Lemma app_eq_nil : forall x y:list, x ++ y = nil -> x = nil /\ y = nil. +Proof. + destruct x as [| a l]; [ destruct y as [| a l] | destruct y as [| a0 l0] ]; + simpl in |- *; auto. + intros H; discriminate H. + intros; discriminate H. +Qed. + +Lemma app_cons_not_nil : forall (x y:list) (a:A), nil <> x ++ a :: y. +Proof. +unfold not in |- *. + destruct x as [| a l]; simpl in |- *; intros. + discriminate H. + discriminate H. +Qed. + +Lemma app_eq_unit : + forall (x y:list) (a:A), + x ++ y = a :: nil -> x = nil /\ y = a :: nil \/ x = a :: nil /\ y = nil. + +Proof. + destruct x as [| a l]; [ destruct y as [| a l] | destruct y as [| a0 l0] ]; + simpl in |- *. + intros a H; discriminate H. + left; split; auto. + right; split; auto. + generalize H. + generalize (app_nil_end l); intros E. + rewrite <- E; auto. + intros. + injection H. + intro. + cut (nil = l ++ a0 :: l0); auto. + intro. + generalize (app_cons_not_nil _ _ _ H1); intro. + elim H2. +Qed. + +Lemma app_inj_tail : + forall (x y:list) (a b:A), x ++ a :: nil = y ++ b :: nil -> x = y /\ a = b. +Proof. + induction x as [| x l IHl]; + [ destruct y as [| a l] | destruct y as [| a l0] ]; + simpl in |- *; auto. + intros a b H. + injection H. + auto. + intros a0 b H. + injection H; intros. + generalize (app_cons_not_nil _ _ _ H0); destruct 1. + intros a b H. + injection H; intros. + cut (nil = l ++ a :: nil); auto. + intro. + generalize (app_cons_not_nil _ _ _ H2); destruct 1. + intros a0 b H. + injection H; intros. + destruct (IHl l0 a0 b H0). + split; auto. + rewrite <- H1; rewrite <- H2; reflexivity. +Qed. + +Lemma app_length : forall l l', length (l++l') = length l + length l'. +Proof. +induction l; simpl; auto. Qed. Lemma in_app_or : forall (l m:list) (a:A), In a (l ++ m) -> In a l \/ In a m. @@ -285,6 +367,33 @@ Proof. Qed. Hint Resolve in_or_app. +Lemma app_nth1 : + forall l l' d n, n < length l -> nth n (l++l') d = nth n l d. +Proof. +induction l. +intros. +inversion H. +intros l' d n. +case n; simpl; auto. +intros; rewrite IHl; auto with arith. +Qed. + +Lemma app_nth2 : + forall l l' d n, n >= length l -> nth n (l++l') d = nth (n-length l) l' d. +Proof. +induction l. +intros. +simpl. +destruct n; auto. +intros l' d n. +case n; simpl; auto. +intros. +inversion H. +intros. +rewrite IHl; auto with arith. +Qed. + + (***************************) (** Set inclusion on list *) (***************************) @@ -344,67 +453,7 @@ Proof. Qed. Hint Resolve incl_app. -(**************************) -(** Nth element of a list *) -(**************************) - -Fixpoint nth (n:nat) (l:list) (default:A) {struct l} : A := - match n, l with - | O, x :: l' => x - | O, other => default - | S m, nil => default - | S m, x :: t => nth m t default - end. - -Fixpoint nth_ok (n:nat) (l:list) (default:A) {struct l} : bool := - match n, l with - | O, x :: l' => true - | O, other => false - | S m, nil => false - | S m, x :: t => nth_ok m t default - end. - -Lemma nth_in_or_default : - forall (n:nat) (l:list) (d:A), {In (nth n l d) l} + {nth n l d = d}. -(* Realizer nth_ok. Program_all. *) -Proof. - intros n l d; generalize n; induction l; intro n0. - right; case n0; trivial. - case n0; simpl in |- *. - auto. - intro n1; elim (IHl n1); auto. -Qed. - -Lemma nth_S_cons : - forall (n:nat) (l:list) (d a:A), - In (nth n l d) l -> In (nth (S n) (a :: l) d) (a :: l). -Proof. - simpl in |- *; auto. -Qed. -Fixpoint nth_error (l:list) (n:nat) {struct n} : Exc A := - match n, l with - | O, x :: _ => value x - | S n, _ :: l => nth_error l n - | _, _ => error - end. - -Definition nth_default (default:A) (l:list) (n:nat) : A := - match nth_error l n with - | Some x => x - | None => default - end. - -Lemma nth_In : - forall (n:nat) (l:list) (d:A), n < length l -> In (nth n l d) l. - -Proof. -unfold lt in |- *; induction n as [| n hn]; simpl in |- *. -destruct l; simpl in |- *; [ inversion 2 | auto ]. -destruct l as [| a l hl]; simpl in |- *. -inversion 2. -intros d ie; right; apply hn; auto with arith. -Qed. (********************************) (** Decidable equality on lists *) @@ -466,6 +515,72 @@ Proof. rewrite IHl; auto. Qed. +Lemma In_rev : forall l x, In x l <-> In x (rev l). +Proof. +induction l. +simpl; intuition. +intros. +simpl. +intuition. +subst. +apply in_or_app; right; simpl; auto. +apply in_or_app; left; firstorder. +destruct (in_app_or _ _ _ H); firstorder. +Qed. + +Lemma rev_length : forall l, length (rev l) = length l. +Proof. +induction l;simpl; auto. +rewrite app_length. +rewrite IHl. +simpl. +elim (length l); simpl; auto. +Qed. + +Lemma rev_nth : forall l d n, n < length l -> + nth n (rev l) d = nth (length l - S n) l d. +Proof. +induction l. +intros; inversion H. +intros. +simpl in H. +simpl (rev (a :: l)). +simpl (length (a :: l) - S n). +inversion H. +rewrite <- minus_n_n; simpl. +rewrite <- rev_length. +rewrite app_nth2; auto. +rewrite <- minus_n_n; auto. +rewrite app_nth1; auto. +rewrite (minus_plus_simpl_l_reverse (length l) n 1). +replace (1 + length l) with (S (length l)); auto with arith. +rewrite <- minus_Sn_m; auto with arith; simpl. +apply IHl; auto. +rewrite rev_length; auto. +Qed. + +(****************************************************) +(** An alternative tail-recursive definition for reverse *) +(****************************************************) + +Fixpoint rev_acc (l l': list) {struct l} : list := + match l with + | nil => l' + | a::l => rev_acc l (a::l') + end. + +Lemma rev_acc_rev : forall l l', rev_acc l l' = rev l ++ l'. +Proof. +induction l; simpl; auto; intros. +rewrite <- ass_app; firstorder. +Qed. + +Lemma rev_alt : forall l, rev l = rev_acc l nil. +Proof. +intros; rewrite rev_acc_rev. +apply app_nil_end. +Qed. + (*********************************************) (** Reverse Induction Principle on Lists *) (*********************************************) @@ -503,9 +618,119 @@ Qed. End Reverse_Induction. +(***************************) +(** Last elements of a list *) +(***************************) + +(** [last l d] returns the last elements of the list [l], + or the default value [d] if [l] is empty. *) + +Fixpoint last (l:list)(d:A) {struct l} : A := + match l with + | nil => d + | a :: nil => a + | a :: l => last l d + end. + +(** [removelast l] remove the last element of [l] *) + +Fixpoint removelast (l:list) {struct l} : list := + match l with + | nil => nil + | a :: nil => nil + | a :: l => a :: removelast l + end. + +Lemma app_removelast_last : + forall l d, l<>nil -> l = removelast l ++ (last l d :: nil). +Proof. +induction l. +destruct 1; auto. +intros d _. +destruct l; auto. +pattern (a0::l) at 1; rewrite IHl with d; auto; discriminate. +Qed. + +Lemma exists_last : + forall l, l<>nil -> { l' : list & { a : A | l = l'++a::nil}}. +Proof. +induction l. +destruct 1; auto. +intros _. +destruct l. +exists nil; exists a; auto. +destruct IHl as [l' (a',H)]; try discriminate. +rewrite H. +exists (a::l'); exists a'; auto. +Qed. + +(********************************) +(* Cutting a list at some position *) +(********************************) + +Fixpoint firstn (n:nat)(l:list) {struct n} : list := + match n with + | 0 => nil + | S n => match l with + | nil => nil + | a::l => a::(firstn n l) + end + end. + +Fixpoint skipn (n:nat)(l:list) { struct n } : list := + match n with + | 0 => l + | S n => match l with + | nil => nil + | a::l => skipn n l + end + end. + +Lemma firstn_skipn : forall n l, firstn n l ++ skipn n l = l. +Proof. +induction n. +simpl; auto. +destruct l; simpl; auto. +f_equal; auto. +Qed. + +(**************) +(** Remove *) +(**************) + +Section Remove. + +Hypothesis eq_dec : forall x y : A, {x = y}+{x <> y}. + +Fixpoint remove (x : A) (l : list){struct l} : list := + match l with + | nil => nil + | y::tl => if (eq_dec x y) then remove x tl else y::(remove x tl) + end. + +End Remove. + +(***************************) +(** List without redundancy *) +(***************************) + +Inductive NoDup : list -> Prop := + | NoDup_nil : NoDup nil + | NoDup_cons : forall x l, ~ In x l -> NoDup l -> NoDup (x::l). + End Lists. +(** Exporting list notations and hints *) + Implicit Arguments nil [A]. +Infix "::" := cons (at level 60, right associativity) : list_scope. +Infix "++" := app (right associativity, at level 60) : list_scope. + +Open Scope list_scope. + +Delimit Scope list_scope with list. + +Bind Scope list_scope with list. Hint Resolve nil_cons app_nil_end ass_app app_ass: datatypes v62. Hint Resolve app_comm_cons app_cons_not_nil: datatypes v62. @@ -523,40 +748,241 @@ Section Functions_on_lists. (** Some generic functions on lists and basic functions of them *) (****************************************************************) +(*********) +(** Map *) +(*********) + Section Map. Variables A B : Set. Variable f : A -> B. + Fixpoint map (l:list A) : list B := match l with | nil => nil | cons a t => cons (f a) (map t) end. -End Map. Lemma in_map : - forall (A B:Set) (f:A -> B) (l:list A) (x:A), In x l -> In (f x) (map f l). + forall (l:list A) (x:A), In x l -> In (f x) (map l). Proof. induction l as [| a l IHl]; simpl in |- *; [ auto | destruct 1; [ left; apply f_equal with (f := f); assumption | auto ] ]. Qed. -Fixpoint flat_map (A B:Set) (f:A -> list B) (l:list A) {struct l} : +Lemma in_map_iff : forall l y, In y (map l) <-> exists x, f x = y /\ In x l. +Proof. +induction l; firstorder (subst; auto). +Qed. + +Lemma map_length : forall l, length (map l) = length l. +Proof. +induction l; simpl; auto. +Qed. + +Lemma map_nth : forall l d n, + nth n (map l) (f d) = f (nth n l d). +Proof. +induction l; simpl map; destruct n; firstorder. +Qed. + +Lemma map_app : forall l l', + map (l++l') = (map l)++(map l'). +Proof. +induction l; simpl; auto. +intros; rewrite IHl; auto. +Qed. + +Lemma map_rev : forall l, map (rev l) = rev (map l). +Proof. +induction l; simpl; auto. +rewrite map_app. +rewrite IHl; auto. +Qed. + +End Map. + +Lemma map_map : forall (A B C:Set)(f:A->B)(g:B->C) l, + map g (map f l) = map (fun x => g (f x)) l. +Proof. +induction l; simpl; auto. +rewrite IHl; auto. +Qed. + +Lemma map_ext : + forall (A B : Set)(f g:A->B), (forall a, f a = g a) -> forall l, map f l = map g l. +Proof. +induction l; simpl; auto. +rewrite H; rewrite IHl; auto. +Qed. + +(********************************************) +(** Operations on lists of pairs or lists of lists *) +(********************************************) + +Section ListPairs. +Variable A B : Set. + +(** [split] derives two lists from a list of pairs *) + +Fixpoint split (l:list (A*B)) { struct l }: list A * list B := + match l with + | nil => (nil, nil) + | (x,y) :: tl => let (g,d) := split tl in (x::g, y::d) + end. + +Lemma in_split_l : forall (l:list (A*B))(p:A*B), + In p l -> In (fst p) (fst (split l)). +Proof. +induction l; simpl; intros; auto. +destruct p; destruct a; destruct (split l); simpl in *. +destruct H. +injection H; auto. +right; apply (IHl (a0,b) H). +Qed. + +Lemma in_split_r : forall (l:list (A*B))(p:A*B), + In p l -> In (snd p) (snd (split l)). +Proof. +induction l; simpl; intros; auto. +destruct p; destruct a; destruct (split l); simpl in *. +destruct H. +injection H; auto. +right; apply (IHl (a0,b) H). +Qed. + +Lemma split_nth : forall (l:list (A*B))(n:nat)(d:A*B), + nth n l d = (nth n (fst (split l)) (fst d), nth n (snd (split l)) (snd d)). +Proof. +induction l. +destruct n; destruct d; simpl; auto. +destruct n; destruct d; simpl; auto. +destruct a; destruct (split l); simpl; auto. +destruct a; destruct (split l); simpl in *; auto. +rewrite IHl; simpl; auto. +Qed. + +Lemma split_lenght_l : forall (l:list (A*B)), + length (fst (split l)) = length l. +Proof. +induction l; simpl; auto. +destruct a; destruct (split l); simpl; auto. +Qed. + +Lemma split_lenght_r : forall (l:list (A*B)), + length (snd (split l)) = length l. +Proof. +induction l; simpl; auto. +destruct a; destruct (split l); simpl; auto. +Qed. + +(** [combine] is the opposite of [split]. + Lists given to [combine] are meant to be of same length. + If not, [combine] stops on the shorter list *) + +Fixpoint combine (l : list A) (l' : list B){struct l} : list (A*B) := + match l,l' with + | x::tl, y::tl' => (x,y)::(combine tl tl') + | _, _ => nil + end. + +Lemma split_combine : forall (l: list (A*B)), + let (l1,l2) := split l in combine l1 l2 = l. +Proof. +induction l. +simpl; auto. +destruct a; simpl. +destruct (split l); simpl in *. +f_equal; auto. +Qed. + +Lemma combine_split : forall (l:list A)(l':list B), length l = length l' -> + split (combine l l') = (l,l'). +Proof. +induction l; destruct l'; simpl; intros; auto; try discriminate. +injection H; clear H; intros. +rewrite IHl; auto. +Qed. + +Lemma in_combine_l : forall (l:list A)(l':list B)(x:A)(y:B), + In (x,y) (combine l l') -> In x l. +Proof. +induction l. +simpl; auto. +destruct l'; simpl; auto; intros. +contradiction. +destruct H. +injection H; auto. +right; apply IHl with l' y; auto. +Qed. + +Lemma in_combine_r : forall (l:list A)(l':list B)(x:A)(y:B), + In (x,y) (combine l l') -> In y l'. +Proof. +induction l. +simpl; intros; contradiction. +destruct l'; simpl; auto; intros. +destruct H. +injection H; auto. +right; apply IHl with x; auto. +Qed. + +Lemma combine_length : forall (l:list A)(l':list B), + length (combine l l') = min (length l) (length l'). +Proof. +induction l. +simpl; auto. +destruct l'; simpl; auto. +Qed. + +Lemma combine_nth : forall (l:list A)(l':list B)(n:nat)(x:A)(y:B), + length l = length l' -> + nth n (combine l l') (x,y) = (nth n l x, nth n l' y). +Proof. +induction l; destruct l'; intros; try discriminate. +destruct n; simpl; auto. +destruct n; simpl in *; auto. +Qed. + +(** [flat_map] *) + +Fixpoint flat_map (f:A -> list B) (l:list A) {struct l} : list B := match l with | nil => nil - | cons x t => app (f x) (flat_map f t) + | cons x t => (f x)++(flat_map f t) end. -Fixpoint list_prod (A B:Set) (l:list A) (l':list B) {struct l} : +Lemma in_flat_map : forall (f:A->list B)(l:list A)(y:B), + In y (flat_map f l) <-> exists x, In x l /\ In y (f x). +Proof. +induction l; simpl; split; intros. +contradiction. +destruct H as (x,(H,_)); contradiction. +destruct (in_app_or _ _ _ H). +exists a; auto. +destruct (IHl y) as (H1,_); destruct (H1 H0) as (x,(H2,H3)). +exists x; auto. +apply in_or_app. +destruct H as (x,(H0,H1)); destruct H0. +subst; auto. +right; destruct (IHl y) as (_,H2); apply H2. +exists x; auto. +Qed. + +(** [list_prod] has the same signature as [combine], but unlike + [combine], it adds every possible pairs, not only those at the + same position. *) + +Fixpoint list_prod (l:list A) (l':list B) {struct l} : list (A * B) := match l with | nil => nil - | cons x t => app (map (fun y:B => (x, y)) l') (list_prod t l') + | cons x t => (map (fun y:B => (x, y)) l')++(list_prod t l') end. Lemma in_prod_aux : - forall (A B:Set) (x:A) (y:B) (l:list B), + forall (x:A) (y:B) (l:list B), In y l -> In (x, y) (map (fun y0:B => (x, y0)) l). Proof. induction l; @@ -566,7 +992,7 @@ Proof. Qed. Lemma in_prod : - forall (A B:Set) (l:list A) (l':list B) (x:A) (y:B), + forall (l:list A) (l':list B) (x:A) (y:B), In x l -> In y l' -> In (x, y) (list_prod l l'). Proof. induction l; @@ -575,10 +1001,36 @@ Proof. [ left; rewrite H; apply in_prod_aux; assumption | right; auto ] ]. Qed. +Lemma in_prod_iff : + forall (l:list A)(l':list B)(x:A)(y:B), + In (x,y) (list_prod l l') <-> In x l /\ In y l'. +Proof. +split; [ | intros; apply in_prod; intuition ]. +induction l; simpl; intros. +intuition. +destruct (in_app_or _ _ _ H); clear H. +destruct (in_map_iff (fun y : B => (a, y)) l' (x,y)) as (H1,_). +destruct (H1 H0) as (z,(H2,H3)); clear H0 H1. +injection H2; clear H2; intros; subst; intuition. +intuition. +Qed. + +Lemma prod_length : forall (l:list A)(l':list B), + length (list_prod l l') = (length l) * (length l'). +Proof. +induction l; simpl; auto. +intros. +rewrite app_length. +rewrite map_length. +auto. +Qed. + +End ListPairs. + (** [(list_power x y)] is [y^x], or the set of sequences of elts of [y] indexed by elts of [x], sorted in lexicographic order. *) -Fixpoint list_power (A B:Set) (l:list A) (l':list B) {struct l} : +Fixpoint list_power (A B:Set)(l:list A) (l':list B) {struct l} : list (list (A * B)) := match l with | nil => cons nil nil @@ -594,13 +1046,37 @@ Fixpoint list_power (A B:Set) (l:list A) (l':list B) {struct l} : Section Fold_Left_Recursor. Variables A B : Set. Variable f : A -> B -> A. + Fixpoint fold_left (l:list B) (a0:A) {struct l} : A := match l with | nil => a0 | cons b t => fold_left t (f a0 b) end. + +Lemma fold_left_app : forall (l l':list B)(i:A), + fold_left (l++l') i = fold_left l' (fold_left l i). +Proof. +induction l. +simpl; auto. +intros. +simpl. +auto. +Qed. + End Fold_Left_Recursor. +Lemma fold_left_length : + forall (A:Set)(l:list A), fold_left (fun x _ => S x) l 0 = length l. +Proof. +intro A. +cut (forall (l:list A) n, fold_left (fun x _ => S x) l n = n + length l). +intros. +exact (H l 0). +induction l; simpl; auto. +intros; rewrite IHl. +simpl; auto with arith. +Qed. + (************************************) (** Right-to-left iterator on lists *) (************************************) @@ -609,13 +1085,34 @@ Section Fold_Right_Recursor. Variables A B : Set. Variable f : B -> A -> A. Variable a0 : A. + Fixpoint fold_right (l:list B) : A := match l with | nil => a0 | cons b t => f b (fold_right t) end. + End Fold_Right_Recursor. +Lemma fold_right_app : forall (A B:Set)(f:A->B->B) l l' i, + fold_right f i (l++l') = fold_right f (fold_right f i l') l. +Proof. +induction l. +simpl; auto. +simpl; intros. +f_equal; auto. +Qed. + +Lemma fold_left_rev_right : forall (A B:Set)(f:A->B->B) l i, + fold_right f i (rev l) = fold_left (fun x y => f y x) l i. +Proof. +induction l. +simpl; auto. +intros. +simpl. +rewrite fold_right_app; simpl; auto. +Qed. + Theorem fold_symmetric : forall (A:Set) (f:A -> A -> A), (forall x y z:A, f x (f y z) = f (f x y) z) -> @@ -638,18 +1135,157 @@ rewrite IHl. reflexivity. Qed. -End Functions_on_lists. +(********************************) +(** Boolean operations over lists *) +(********************************) +Section Bool. +Variable A : Set. +Variable f : A -> bool. -(** Exporting list notations *) +(** find whether a boolean function can be satisfied by an + elements of the list. *) -Infix "::" := cons (at level 60, right associativity) : list_scope. +Fixpoint existsb (l:list A) {struct l}: bool := + match l with + | nil => false + | a::l => f a || existsb l + end. -Infix "++" := app (right associativity, at level 60) : list_scope. +Lemma existsb_exists : + forall l, existsb l = true <-> exists x, In x l /\ f x = true. +Proof. +induction l; simpl; intuition. +inversion H. +firstorder. +destruct (orb_prop _ _ H1); firstorder. +firstorder. +subst. +rewrite H2; auto. +Qed. -Open Scope list_scope. +Lemma existsb_nth : forall l n d, n < length l -> + existsb l = false -> f (nth n l d) = false. +Proof. +induction l. +inversion 1. +simpl; intros. +destruct (orb_false_elim _ _ H0); clear H0; auto. +destruct n ; auto. +rewrite IHl; auto with arith. +Qed. -(** Declare Scope list_scope with key list *) -Delimit Scope list_scope with list. +(** find whether a boolean function is satisfied by + all the elements of a list. *) -Bind Scope list_scope with list. +Fixpoint forallb (l:list A) {struct l} : bool := + match l with + | nil => true + | a::l => f a && forallb l + end. + +Lemma forallb_forall : + forall l, forallb l = true <-> (forall x, In x l -> f x = true). +Proof. +induction l; simpl; intuition. +destruct (andb_prop _ _ H1). +congruence. +destruct (andb_prop _ _ H1); auto. +assert (forallb l = true). +apply H0; intuition. +rewrite H1; auto. +Qed. + +(** [filter] *) + +Fixpoint filter (l:list A) : list A := + match l with + | nil => nil + | x :: l => if f x then x::(filter l) else filter l + end. + +Lemma filter_In : forall x l, In x (filter l) <-> In x l /\ f x = true. +Proof. +induction l; simpl. +intuition. +intros. +case_eq (f a); intros; simpl; intuition congruence. +Qed. + +(** [find] *) + +Fixpoint find (l:list A) : option A := + match l with + | nil => None + | x :: tl => if f x then Some x else find tl + end. + +(** [partition] *) + +Fixpoint partition (l:list A) {struct l} : list A * list A := + match l with + | nil => (nil, nil) + | x :: tl => let (g,d) := partition tl in + if f x then (x::g,d) else (g,x::d) + end. + +End Bool. + + +(*********************************) +(** Sequence of natural numbers *) +(*********************************) + +(** [seq] computes the sequence of [len] contiguous integers + that starts at [start]. For instance, [seq 2 3] is [2::3::4::nil]. *) + +Fixpoint seq (start len:nat) {struct len} : list nat := + match len with + | 0 => nil + | S len => start :: seq (S start) len + end. + +Lemma seq_length : forall len start, length (seq start len) = len. +Proof. +induction len; simpl; auto. +Qed. + +Lemma seq_nth : forall len start n d, + n < len -> nth n (seq start len) d = start+n. +Proof. +induction len; intros. +inversion H. +simpl seq. +destruct n; simpl. +auto with arith. +rewrite IHlen;simpl; auto with arith. +Qed. + +Lemma seq_shift : forall len start, + map S (seq start len) = seq (S start) len. +Proof. +induction len; simpl; auto. +intros. +rewrite IHlen. +auto with arith. +Qed. + +End Functions_on_lists. + + +Hint Rewrite + rev_involutive (* rev (rev l) = l *) + rev_unit (* rev (l ++ a :: nil) = a :: rev l *) + map_nth (* nth n (map f l) (f d) = f (nth n l d) *) + map_length (* length (map f l) = length l *) + seq_length (* length (seq start len) = len *) + app_length (* length (l ++ l') = length l + length l' *) + rev_length (* length (rev l) = length l *) + : list. + +Hint Rewrite <- + app_nil_end (* l = l ++ nil *) + : list. + +Ltac simpl_list := autorewrite with list. +Ltac ssimpl_list := autorewrite with list using simpl. |