diff options
Diffstat (limited to 'theories/Lists')
| -rw-r--r--[-rwxr-xr-x] | theories/Lists/List.v | 1000 | ||||
| -rw-r--r-- | theories/Lists/ListSet.v | 12 | ||||
| -rw-r--r--[-rwxr-xr-x] | theories/Lists/MonoList.v | 2 | ||||
| -rw-r--r-- | theories/Lists/SetoidList.v | 300 | ||||
| -rw-r--r--[-rwxr-xr-x] | theories/Lists/Streams.v | 15 | ||||
| -rw-r--r--[-rwxr-xr-x] | theories/Lists/TheoryList.v | 2 | ||||
| -rwxr-xr-x | theories/Lists/intro.tex | 15 |
7 files changed, 1141 insertions, 205 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. diff --git a/theories/Lists/ListSet.v b/theories/Lists/ListSet.v index d5ecad9c..4e009ed5 100644 --- a/theories/Lists/ListSet.v +++ b/theories/Lists/ListSet.v @@ -6,14 +6,12 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: ListSet.v,v 1.13.2.1 2004/07/16 19:31:05 herbelin Exp $ i*) +(*i $Id: ListSet.v 6844 2005-03-16 13:09:55Z herbelin $ i*) -(** A Library for finite sets, implemented as lists - A Library with similar interface will soon be available under - the name TreeSet in the theories/Trees directory *) +(** A Library for finite sets, implemented as lists *) -(** PolyList is loaded, but not exported. - This allow to "hide" the definitions, functions and theorems of PolyList +(** List is loaded, but not exported. + This allow to "hide" the definitions, functions and theorems of List and to see only the ones of ListSet *) Require Import List. @@ -395,4 +393,4 @@ Section other_definitions. End other_definitions. -Unset Implicit Arguments.
\ No newline at end of file +Unset Implicit Arguments. diff --git a/theories/Lists/MonoList.v b/theories/Lists/MonoList.v index d639a39d..aa2b74dd 100755..100644 --- a/theories/Lists/MonoList.v +++ b/theories/Lists/MonoList.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: MonoList.v,v 1.2.2.1 2004/07/16 19:31:05 herbelin Exp $ i*) +(*i $Id: MonoList.v 8642 2006-03-17 10:09:02Z notin $ i*) (** THIS IS A OLD CONTRIB. IT IS NO LONGER MAINTAINED ***) diff --git a/theories/Lists/SetoidList.v b/theories/Lists/SetoidList.v new file mode 100644 index 00000000..811dcab4 --- /dev/null +++ b/theories/Lists/SetoidList.v @@ -0,0 +1,300 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) + +(* $Id: SetoidList.v 8686 2006-04-06 13:25:10Z letouzey $ *) + +Require Export List. +Require Export Sorting. +Require Export Setoid. +Set Implicit Arguments. +Unset Strict Implicit. + +(** * Logical relations over lists with respect to a setoid equality + or ordering. *) + +(** This can be seen as a complement of predicate [lelistA] and [sort] + found in [Sorting]. *) + +Section Type_with_equality. +Variable A : Set. +Variable eqA : A -> A -> Prop. + +(** Being in a list modulo an equality relation over type [A]. *) + +Inductive InA (x : A) : list A -> Prop := + | InA_cons_hd : forall y l, eqA x y -> InA x (y :: l) + | InA_cons_tl : forall y l, InA x l -> InA x (y :: l). + +Hint Constructors InA. + +(** An alternative definition of [InA]. *) + +Lemma InA_alt : forall x l, InA x l <-> exists y, eqA x y /\ In y l. +Proof. + induction l; intuition. + inversion H. + firstorder. + inversion H1; firstorder. + firstorder; subst; auto. +Qed. + +(** A list without redundancy modulo the equality over [A]. *) + +Inductive NoDupA : list A -> Prop := + | NoDupA_nil : NoDupA nil + | NoDupA_cons : forall x l, ~ InA x l -> NoDupA l -> NoDupA (x::l). + +Hint Constructors NoDupA. + +(** lists with same elements modulo [eqA] *) + +Definition eqlistA l l' := forall x, InA x l <-> InA x l'. + +(** Results concerning lists modulo [eqA] *) + +Hypothesis eqA_refl : forall x, eqA x x. +Hypothesis eqA_sym : forall x y, eqA x y -> eqA y x. +Hypothesis eqA_trans : forall x y z, eqA x y -> eqA y z -> eqA x z. + +Hint Resolve eqA_refl eqA_trans. +Hint Immediate eqA_sym. + +Lemma InA_eqA : forall l x y, eqA x y -> InA x l -> InA y l. +Proof. + intros s x y. + do 2 rewrite InA_alt. + intros H (z,(U,V)). + exists z; split; eauto. +Qed. +Hint Immediate InA_eqA. + +Lemma In_InA : forall l x, In x l -> InA x l. +Proof. + simple induction l; simpl in |- *; intuition. + subst; auto. +Qed. +Hint Resolve In_InA. + +(** Results concerning lists modulo [eqA] and [ltA] *) + +Variable ltA : A -> A -> Prop. + +Hypothesis ltA_trans : forall x y z, ltA x y -> ltA y z -> ltA x z. +Hypothesis ltA_not_eqA : forall x y, ltA x y -> ~ eqA x y. +Hypothesis ltA_eqA : forall x y z, ltA x y -> eqA y z -> ltA x z. +Hypothesis eqA_ltA : forall x y z, eqA x y -> ltA y z -> ltA x z. + +Hint Resolve ltA_trans. +Hint Immediate ltA_eqA eqA_ltA. + +Notation InfA:=(lelistA ltA). +Notation SortA:=(sort ltA). + +Lemma InfA_ltA : + forall l x y, ltA x y -> InfA y l -> InfA x l. +Proof. + intro s; case s; constructor; inversion_clear H0. + eapply ltA_trans; eauto. +Qed. + +Lemma InfA_eqA : + forall l x y, eqA x y -> InfA y l -> InfA x l. +Proof. + intro s; case s; constructor; inversion_clear H0; eauto. +Qed. +Hint Immediate InfA_ltA InfA_eqA. + +Lemma SortA_InfA_InA : + forall l x a, SortA l -> InfA a l -> InA x l -> ltA a x. +Proof. + simple induction l. + intros; inversion H1. + intros. + inversion_clear H0; inversion_clear H1; inversion_clear H2. + eapply ltA_eqA; eauto. + eauto. +Qed. + +Lemma In_InfA : + forall l x, (forall y, In y l -> ltA x y) -> InfA x l. +Proof. + simple induction l; simpl in |- *; intros; constructor; auto. +Qed. + +Lemma InA_InfA : + forall l x, (forall y, InA y l -> ltA x y) -> InfA x l. +Proof. + simple induction l; simpl in |- *; intros; constructor; auto. +Qed. + +(* In fact, this may be used as an alternative definition for InfA: *) + +Lemma InfA_alt : + forall l x, SortA l -> (InfA x l <-> (forall y, InA y l -> ltA x y)). +Proof. +split. +intros; eapply SortA_InfA_InA; eauto. +apply InA_InfA. +Qed. + +Lemma SortA_NoDupA : forall l, SortA l -> NoDupA l. +Proof. + simple induction l; auto. + intros x l' H H0. + inversion_clear H0. + constructor; auto. + intro. + assert (ltA x x) by eapply SortA_InfA_InA; eauto. + elim (ltA_not_eqA H3); auto. +Qed. + +Lemma NoDupA_app : forall l l', NoDupA l -> NoDupA l' -> + (forall x, InA x l -> InA x l' -> False) -> + NoDupA (l++l'). +Proof. +induction l; simpl; auto; intros. +inversion_clear H. +constructor. +rewrite InA_alt; intros (y,(H4,H5)). +destruct (in_app_or _ _ _ H5). +elim H2. +rewrite InA_alt. +exists y; auto. +apply (H1 a). +auto. +rewrite InA_alt. +exists y; auto. +apply IHl; auto. +intros. +apply (H1 x); auto. +Qed. + + +Lemma NoDupA_rev : forall l, NoDupA l -> NoDupA (rev l). +Proof. +induction l. +simpl; auto. +simpl; intros. +inversion_clear H. +apply NoDupA_app; auto. +constructor; auto. +intro H2; inversion H2. +intros x. +rewrite InA_alt. +intros (x1,(H2,H3)). +inversion_clear 1. +destruct H0. +apply InA_eqA with x1; eauto. +apply In_InA. +rewrite In_rev; auto. +inversion H4. +Qed. + + +Lemma InA_app : forall l1 l2 x, + InA x (l1 ++ l2) -> InA x l1 \/ InA x l2. +Proof. + induction l1; simpl in *; intuition. + inversion_clear H; auto. + elim (IHl1 l2 x H0); auto. +Qed. + + Hint Constructors lelistA sort. + +Lemma InfA_app : forall l1 l2 a, InfA a l1 -> InfA a l2 -> InfA a (l1++l2). +Proof. + induction l1; simpl; auto. + inversion_clear 1; auto. +Qed. + +Lemma SortA_app : + forall l1 l2, SortA l1 -> SortA l2 -> + (forall x y, InA x l1 -> InA y l2 -> ltA x y) -> + SortA (l1 ++ l2). +Proof. + induction l1; simpl in *; intuition. + inversion_clear H. + constructor; auto. + apply InfA_app; auto. + destruct l2; auto. +Qed. + +Section Remove. + +Hypothesis eqA_dec : forall x y : A, {eqA x y}+{~(eqA x y)}. + +Fixpoint removeA (x : A) (l : list A){struct l} : list A := + match l with + | nil => nil + | y::tl => if (eqA_dec x y) then removeA x tl else y::(removeA x tl) + end. + +Lemma removeA_filter : forall x l, + removeA x l = filter (fun y => if eqA_dec x y then false else true) l. +Proof. +induction l; simpl; auto. +destruct (eqA_dec x a); auto. +rewrite IHl; auto. +Qed. + +Lemma removeA_InA : forall l x y, InA y (removeA x l) <-> InA y l /\ ~eqA x y. +Proof. +induction l; simpl; auto. +split. +inversion_clear 1. +destruct 1; inversion_clear H. +intros. +destruct (eqA_dec x a); simpl; auto. +rewrite IHl; split; destruct 1; split; auto. +inversion_clear H; auto. +destruct H0; apply eqA_trans with a; auto. +split. +inversion_clear 1. +split; auto. +swap n. +apply eqA_trans with y; auto. +rewrite (IHl x y) in H0; destruct H0; auto. +destruct 1; inversion_clear H; auto. +constructor 2; rewrite IHl; auto. +Qed. + +Lemma removeA_NoDupA : + forall s x, NoDupA s -> NoDupA (removeA x s). +Proof. +simple induction s; simpl; intros. +auto. +inversion_clear H0. +destruct (eqA_dec x a); simpl; auto. +constructor; auto. +rewrite removeA_InA. +intuition. +Qed. + +Lemma removeA_eqlistA : forall l l' x, + ~InA x l -> eqlistA (x :: l) l' -> eqlistA l (removeA x l'). +Proof. +unfold eqlistA; intros. +rewrite removeA_InA. +split; intros. +rewrite <- H0; split; auto. +swap H. +apply InA_eqA with x0; auto. +rewrite <- (H0 x0) in H1. +destruct H1. +inversion_clear H1; auto. +elim H2; auto. +Qed. + +End Remove. + +End Type_with_equality. + +Hint Constructors InA. +Hint Constructors NoDupA. +Hint Constructors sort. +Hint Constructors lelistA. diff --git a/theories/Lists/Streams.v b/theories/Lists/Streams.v index 3c433ba2..7bc6a09d 100755..100644 --- a/theories/Lists/Streams.v +++ b/theories/Lists/Streams.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: Streams.v,v 1.15.2.1 2004/07/16 19:31:05 herbelin Exp $ i*) +(*i $Id: Streams.v 8642 2006-03-17 10:09:02Z notin $ i*) Set Implicit Arguments. @@ -71,9 +71,8 @@ Qed. (** Extensional Equality between two streams *) -CoInductive EqSt : Stream -> Stream -> Prop := +CoInductive EqSt (s1 s2: Stream) : Prop := eqst : - forall s1 s2:Stream, hd s1 = hd s2 -> EqSt (tl s1) (tl s2) -> EqSt s1 s2. (** A coinduction principle *) @@ -140,12 +139,12 @@ Inductive Exists : Stream -> Prop := | Further : forall x:Stream, ~ P x -> Exists (tl x) -> Exists x. i*) -Inductive Exists : Stream -> Prop := - | Here : forall x:Stream, P x -> Exists x - | Further : forall x:Stream, Exists (tl x) -> Exists x. +Inductive Exists ( x: Stream ) : Prop := + | Here : P x -> Exists x + | Further : Exists (tl x) -> Exists x. -CoInductive ForAll : Stream -> Prop := - HereAndFurther : forall x:Stream, P x -> ForAll (tl x) -> ForAll x. +CoInductive ForAll (x: Stream) : Prop := + HereAndFurther : P x -> ForAll (tl x) -> ForAll x. Section Co_Induction_ForAll. diff --git a/theories/Lists/TheoryList.v b/theories/Lists/TheoryList.v index fbeb97ce..19f97aec 100755..100644 --- a/theories/Lists/TheoryList.v +++ b/theories/Lists/TheoryList.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: TheoryList.v,v 1.15.2.1 2004/07/16 19:31:06 herbelin Exp $ i*) +(*i $Id: TheoryList.v 8642 2006-03-17 10:09:02Z notin $ i*) (** Some programs and results about lists following CAML Manual *) diff --git a/theories/Lists/intro.tex b/theories/Lists/intro.tex index 344bba59..c45f8803 100755 --- a/theories/Lists/intro.tex +++ b/theories/Lists/intro.tex @@ -4,21 +4,24 @@ This library includes the following files: \begin{itemize} -\item {\tt List.v} THIS OLD LIBRARY IS HERE ONLY FOR COMPATIBILITY - WITH OLDER VERSIONS OF COQS. THE USER SHOULD USE POLYLIST INSTEAD. - -\item {\tt PolyList.v} contains definitions of (polymorphic) lists, +\item {\tt List.v} contains definitions of (polymorphic) lists, functions on lists such as head, tail, map, append and prove some properties of these functions. Implicit arguments are used in this - library, so you should read the Referance Manual about implicit + library, so you should read the Reference Manual about implicit arguments before using it. +\item {\tt ListSet.v} contains definitions and properties of finite + sets, implemented as lists. + \item {\tt TheoryList.v} contains complementary results on lists. Here - a more theoric point of view is assumed : one extracts functions + a more theoretic point of view is assumed : one extracts functions from propositions, rather than defining functions and then prove them. \item {\tt Streams.v} defines the type of infinite lists (streams). It is a coinductive type. Basic facts are stated and proved. The streams are also polymorphic. +\item {\tt MonoList.v} THIS OLD LIBRARY IS HERE ONLY FOR COMPATIBILITY + WITH OLDER VERSIONS OF COQ. THE USER SHOULD USE {\tt List.v} INSTEAD. + \end{itemize} |