From 5f9b04da0f3c72f4b582cd094edae721b1bc9a9e Mon Sep 17 00:00:00 2001 From: letouzey Date: Thu, 6 Apr 2006 13:25:58 +0000 Subject: versement de MoreList.v dans List.v, reorganisation, quelques nouveaux lemmes git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8687 85f007b7-540e-0410-9357-904b9bb8a0f7 --- theories/Lists/MoreList.v | 507 ---------------------------------------------- 1 file changed, 507 deletions(-) delete mode 100644 theories/Lists/MoreList.v diff --git a/theories/Lists/MoreList.v b/theories/Lists/MoreList.v deleted file mode 100644 index 113703318..000000000 --- a/theories/Lists/MoreList.v +++ /dev/null @@ -1,507 +0,0 @@ -(***********************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* 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. - -End Nth. - -Section App. - -Lemma app_length : forall l l', length (l++l') = length l + length l'. -Proof. -induction l; simpl; auto. -Qed. - -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. -rewrite <- minus_n_O; auto. -intros l' d n. -case n; simpl; auto. -intros. -inversion H. -intros. -rewrite IHl; auto with arith. -Qed. - -End App. - -Section Fold. - -Lemma fold_left_length : - forall l, fold_left (fun x _ => S x) l 0 = length l. -Proof. -cut (forall l 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. - -Lemma fold_left_app : forall (l l':list B)(f : A -> B -> A)(i:A), - fold_left f (l++l') i = fold_left f l' (fold_left f l i). -Proof. -induction l. -simpl; auto. -intros. -simpl. -auto. -Qed. - -Lemma fold_right_app : forall l l' (f:A->B->B)(i:B), - 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 l (f:A->B->B)(i:B), - 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. - -End Fold. - -Section Rev. - -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; rewrite plus_comm; 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. - -End Rev. - -Section Rev_acc. - -(** An alternative tail-recursive definition of [rev] *) - -Fixpoint rev_acc (l l': list A) {struct l} : list A := - 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. - -End Rev_acc. - -Section Seq. - -(** [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 Seq. - -Section Map. - -Variable f : A-> B. - -Lemma In_map : forall l y, In y (map f l) <-> exists x, f x = y /\ In x l. -Proof. -induction l; firstorder (subst; auto). -Qed. - -Lemma map_length : forall l, length (map f l) = length l. -Proof. -induction l; simpl; auto. -Qed. - -Lemma map_nth : forall l d n, - nth n (map f l) (f d) = f (nth n l d). -Proof. -induction l; simpl map; destruct n; firstorder. -Qed. - -Lemma map_app : forall l l', - map f (l++l') = (map f l) ++ (map f l'). -Proof. -induction l; simpl; auto. -intros; rewrite IHl; auto. -Qed. - -Lemma map_rev : forall l, map f (rev l) = rev (map f l). -Proof. -induction l; simpl; auto. -rewrite map_app. -rewrite IHl; auto. -Qed. - -Lemma map_map : forall (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 g, (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. - -End Map. - -Section SplitLast. - -(** [last l d] returns the last elements of the list [l], - or the default value [d] if [l] is empty. *) - -Fixpoint last (l:list A)(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 A) {struct l} : list A := - 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 : A | l = l'++a::nil}}. -Proof. -induction l. -destruct 1; auto. -intros _. -destruct l. -exists (@nil A); exists a; auto. -destruct IHl as [l' (a',H)]; try discriminate. -rewrite H. -exists (a::l'); exists a'; auto. -Qed. - -End SplitLast. - -Section SplitN. - -Fixpoint firstn (n:nat)(l:list A) {struct n} : list A := - 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 A) { struct n } : list A := - 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. - -End SplitN. - -Section Bool. - -Variable f : A -> bool. - -(** find whether a boolean function can be satisfied by an - elements of the list. *) - -Fixpoint existsb (l:list A) {struct l}: bool := - match l with - | nil => false - | a::l => f a || existsb l - end. - -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. - - -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. - -(** find whether a boolean function is satisfied by - all the elements of a 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. - -Fixpoint find (l:list A) : option A := - match l with - | nil => None - | x :: tl => if f x then Some x else find tl - end. - -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. - -Section Split. - -Fixpoint split (l:list (A*B)) : list A * list B := - match l with - | nil => (nil, nil) - | (x,y) :: tl => let (g,d) := split tl in (x::g, y::d) - end. - -(** [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. - -End Split. - -Section Remove. - -Hypothesis eq_dec : forall x y : A, {x = y}+{x <> y}. - -Fixpoint remove (x : A) (l : list A){struct l} : list A := - match l with - | nil => nil - | y::tl => if (eq_dec x y) then remove x tl else y::(remove x tl) - end. - -End Remove. - -Section NoDuplicates. - -(** A list without redundancy. *) - -Inductive NoDup : list A -> Prop := - | NoDup_nil : NoDup nil - | NoDup_cons : forall x l, ~ In x l -> NoDup l -> NoDup (x::l). - -End NoDuplicates. - -End MoreLists. - -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. -- cgit v1.2.3