diff options
Diffstat (limited to 'theories/Lists/List.v')
| -rw-r--r-- | theories/Lists/List.v | 1202 |
1 files changed, 566 insertions, 636 deletions
diff --git a/theories/Lists/List.v b/theories/Lists/List.v index c015854e..f42dc7fa 100644 --- a/theories/Lists/List.v +++ b/theories/Lists/List.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: List.v 12446 2009-10-29 21:43:06Z glondu $ i*) +(*i $Id$ i*) Require Import Le Gt Minus Min Bool. @@ -17,78 +17,47 @@ Set Implicit Arguments. (** * Basics: definition of polymorphic lists and some operations *) (******************************************************************) -(** ** Definitions *) +(** The definition of [list] is now in [Init/Datatypes], + as well as the definitions of [length] and [app] *) + +Open Scope list_scope. Section Lists. Variable A : Type. - Inductive list : Type := - | nil : list - | cons : A -> list -> list. - - Infix "::" := cons (at level 60, right associativity) : list_scope. + (** Head and tail *) - Open Scope list_scope. + Definition hd (default:A) (l:list A) := + match l with + | nil => default + | x :: _ => x + end. - (** Head and tail *) - Definition head (l:list) := + Definition hd_error (l:list A) := match l with | nil => error | x :: _ => value x end. - Definition hd (default:A) (l:list) := - match l with - | nil => default - | x :: _ => x - end. - - Definition tail (l:list) : list := + Definition tl (l:list A) := match l with | nil => nil | a :: m => m end. - (** Length of lists *) - Fixpoint length (l:list) : nat := - match l with - | nil => 0 - | _ :: m => S (length m) - end. - (** The [In] predicate *) - Fixpoint In (a:A) (l:list) {struct l} : Prop := + Fixpoint In (a:A) (l:list A) : Prop := match l with | nil => False | b :: m => b = a \/ In a m end. - - (** Concatenation of two lists *) - 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. - End Lists. -(** Exporting list notations and tactics *) - -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. - -Arguments Scope list [type_scope]. +(* Keep these notations local to prevent conflicting notations *) +Local Notation "[ ]" := nil : list_scope. +Local Notation "[ a ; .. ; b ]" := (a :: .. (b :: []) ..) : list_scope. (** ** Facts about lists *) @@ -100,164 +69,172 @@ Section Facts. (** *** Genereric facts *) (** Discrimination *) - Theorem nil_cons : forall (x:A) (l:list A), nil <> x :: l. - Proof. + Theorem nil_cons : forall (x:A) (l:list A), [] <> x :: l. + Proof. intros; discriminate. Qed. (** Destruction *) - Theorem destruct_list : forall l : list A, {x:A & {tl:list A | l = x::tl}}+{l = nil}. + Theorem destruct_list : forall l : list A, {x:A & {tl:list A | l = x::tl}}+{l = []}. Proof. - induction l as [|a tl]. + induction l as [|a tail]. right; reflexivity. - left; exists a; exists tl; reflexivity. + left; exists a, tail; reflexivity. Qed. - + (** *** Head and tail *) - - Theorem head_nil : head (@nil A) = None. + + Theorem hd_error_nil : hd_error (@nil A) = None. Proof. simpl; reflexivity. Qed. - Theorem head_cons : forall (l : list A) (x : A), head (x::l) = Some x. + Theorem hd_error_cons : forall (l : list A) (x : A), hd_error (x::l) = Some x. Proof. intros; simpl; reflexivity. Qed. (************************) - (** *** Facts about [In] *) + (** *** Facts about [In] *) (************************) (** Characterization of [In] *) - + Theorem in_eq : forall (a:A) (l:list A), In a (a :: l). - Proof. - simpl in |- *; auto. + Proof. + simpl; auto. Qed. - + Theorem in_cons : forall (a b:A) (l:list A), In b l -> In b (a :: l). - Proof. - simpl in |- *; auto. + Proof. + simpl; auto. Qed. - Theorem in_nil : forall a:A, ~ In a nil. + Theorem in_nil : forall a:A, ~ In a []. Proof. - unfold not in |- *; intros a H; inversion_clear H. + unfold not; intros a H; inversion_clear H. Qed. - Lemma In_split : forall x (l:list A), In x l -> exists l1, exists l2, l = l1++x::l2. + Theorem in_split : forall x (l:list A), In x l -> exists l1, exists l2, l = l1++x::l2. Proof. induction l; simpl; destruct 1. subst a; auto. - exists (@nil A); exists l; auto. + exists [], l; auto. destruct (IHl H) as (l1,(l2,H0)). - exists (a::l1); exists l2; simpl; f_equal; auto. + exists (a::l1), l2; simpl; f_equal; auto. Qed. (** Inversion *) - Theorem in_inv : forall (a b:A) (l:list A), In b (a :: l) -> a = b \/ In b l. + Lemma in_inv : forall (a b:A) (l:list A), In b (a :: l) -> a = b \/ In b l. Proof. intros a b l H; inversion_clear H; auto. Qed. (** Decidability of [In] *) - Theorem In_dec : + Theorem in_dec : (forall x y:A, {x = y} + {x <> y}) -> forall (a:A) (l:list A), {In a l} + {~ In a l}. Proof. intro H; induction l as [| a0 l IHl]. right; apply in_nil. - destruct (H a0 a); simpl in |- *; auto. - destruct IHl; simpl in |- *; auto. - right; unfold not in |- *; intros [Hc1| Hc2]; auto. + destruct (H a0 a); simpl; auto. + destruct IHl; simpl; auto. + right; unfold not; intros [Hc1| Hc2]; auto. Defined. - (*************************) + (**************************) (** *** Facts about [app] *) - (*************************) + (**************************) (** Discrimination *) - Theorem app_cons_not_nil : forall (x y:list A) (a:A), nil <> x ++ a :: y. + Theorem app_cons_not_nil : forall (x y:list A) (a:A), [] <> x ++ a :: y. Proof. - unfold not in |- *. - destruct x as [| a l]; simpl in |- *; intros. + unfold not. + destruct x as [| a l]; simpl; intros. discriminate H. discriminate H. Qed. (** Concat with [nil] *) + Theorem app_nil_l : forall l:list A, [] ++ l = l. + Proof. + reflexivity. + Qed. - Theorem app_nil_end : forall l:list A, l = l ++ nil. - Proof. - induction l; simpl in |- *; auto. - rewrite <- IHl; auto. + Theorem app_nil_r : forall l:list A, l ++ [] = l. + Proof. + induction l; simpl; f_equal; auto. Qed. + (* begin hide *) + (* Deprecated *) + Theorem app_nil_end : forall (l:list A), l = l ++ []. + Proof. symmetry; apply app_nil_r. Qed. + (* end hide *) + (** [app] is associative *) - Theorem app_ass : forall l m n:list A, (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. + Theorem app_assoc : forall l m n:list A, l ++ m ++ n = (l ++ m) ++ n. + Proof. + intros l m n; induction l; simpl; f_equal; auto. Qed. - Hint Resolve app_ass. - Theorem ass_app : forall l m n:list A, l ++ m ++ n = (l ++ m) ++ n. - Proof. - auto using app_ass. + (* begin hide *) + (* Deprecated *) + Theorem app_assoc_reverse : forall l m n:list A, (l ++ m) ++ n = l ++ m ++ n. + Proof. + auto using app_assoc. Qed. + Hint Resolve app_assoc_reverse. + (* end hide *) - (** [app] commutes with [cons] *) + (** [app] commutes with [cons] *) Theorem app_comm_cons : forall (x y:list A) (a:A), a :: (x ++ y) = (a :: x) ++ y. Proof. auto. Qed. + (** Facts deduced from the result of a concatenation *) - - (** Facts deduced from the result of a concatenation *) - - Theorem app_eq_nil : forall l l':list A, l ++ l' = nil -> l = nil /\ l' = nil. + Theorem app_eq_nil : forall l l':list A, l ++ l' = [] -> l = [] /\ l' = []. Proof. - destruct l as [| x l]; destruct l' as [| y l']; simpl in |- *; auto. + destruct l as [| x l]; destruct l' as [| y l']; simpl; auto. intro; discriminate. intros H; discriminate H. Qed. Theorem app_eq_unit : forall (x y:list A) (a:A), - x ++ y = a :: nil -> x = nil /\ y = a :: nil \/ x = a :: nil /\ y = nil. + x ++ y = [a] -> x = [] /\ y = [a] \/ x = [a] /\ y = []. Proof. destruct x as [| a l]; [ destruct y as [| a l] | destruct y as [| a0 l0] ]; - simpl in |- *. + simpl. intros a H; discriminate H. left; split; auto. right; split; auto. generalize H. - generalize (app_nil_end l); intros E. - rewrite <- E; auto. + generalize (app_nil_r l); intros E. + rewrite -> E; auto. intros. injection H. intro. - cut (nil = l ++ a0 :: l0); auto. + cut ([] = l ++ a0 :: l0); auto. intro. generalize (app_cons_not_nil _ _ _ H1); intro. elim H2. Qed. Lemma app_inj_tail : - forall (x y:list A) (a b:A), x ++ a :: nil = y ++ b :: nil -> x = y /\ a = b. + forall (x y:list A) (a b:A), x ++ [a] = y ++ [b] -> x = y /\ a = b. Proof. induction x as [| x l IHl]; - [ destruct y as [| a l] | destruct y as [| a l0] ]; - simpl in |- *; auto. + [ destruct y as [| a l] | destruct y as [| a l0] ]; + simpl; auto. intros a b H. injection H. auto. @@ -266,12 +243,12 @@ Section Facts. generalize (app_cons_not_nil _ _ _ H0); destruct 1. intros a b H. injection H; intros. - cut (nil = l ++ a :: nil); auto. + cut ([] = l ++ [a]); auto. intro. generalize (app_cons_not_nil _ _ _ H2); destruct 1. intros a0 b H. injection H; intros. - destruct (IHl l0 a0 b H0). + destruct (IHl l0 a0 b H0). split; auto. rewrite <- H1; rewrite <- H2; reflexivity. Qed. @@ -285,9 +262,9 @@ Section Facts. Qed. Lemma in_app_or : forall (l m:list A) (a:A), In a (l ++ m) -> In a l \/ In a m. - Proof. + Proof. intros l m a. - elim l; simpl in |- *; auto. + elim l; simpl; auto. intros a0 y H H0. now_show ((a0 = a \/ In a y) \/ In a m). elim H0; auto. @@ -297,9 +274,9 @@ Section Facts. Qed. Lemma in_or_app : forall (l m:list A) (a:A), In a l \/ In a m -> In a (l ++ m). - Proof. + Proof. intros l m a. - elim l; simpl in |- *; intro H. + elim l; simpl; intro H. now_show (In a m). elim H; auto; intro H0. now_show (In a m). @@ -311,18 +288,23 @@ Section Facts. now_show (H = a \/ In a (y ++ m)). elim H2; auto. Qed. - + + Lemma in_app_iff : forall l l' (a:A), In a (l++l') <-> In a l \/ In a l'. + Proof. + split; auto using in_app_or, in_or_app. + Qed. + Lemma app_inv_head: - forall l l1 l2 : list A, l ++ l1 = l ++ l2 -> l1 = l2. + forall l l1 l2 : list A, l ++ l1 = l ++ l2 -> l1 = l2. Proof. induction l; simpl; auto; injection 1; auto. Qed. - + Lemma app_inv_tail: - forall l l1 l2 : list A, l1 ++ l = l2 ++ l -> l1 = l2. + forall l l1 l2 : list A, l1 ++ l = l2 ++ l -> l1 = l2. Proof. intros l l1 l2; revert l1 l2 l. - induction l1 as [ | x1 l1]; destruct l2 as [ | x2 l2]; + induction l1 as [ | x1 l1]; destruct l2 as [ | x2 l2]; simpl; auto; intros l H. absurd (length (x2 :: l2 ++ l) <= length l). simpl; rewrite app_length; auto with arith. @@ -335,10 +317,10 @@ Section Facts. End Facts. -Hint Resolve app_nil_end ass_app app_ass: datatypes v62. +Hint Resolve app_assoc app_assoc_reverse: datatypes v62. Hint Resolve app_comm_cons app_cons_not_nil: datatypes v62. Hint Immediate app_eq_nil: datatypes v62. -Hint Resolve app_eq_unit app_inj_tail: datatypes v62. +Hint Resolve app_eq_unit app_inj_tail: datatypes v62. Hint Resolve in_eq in_cons in_inv in_nil in_app_or in_or_app: datatypes v62. @@ -359,7 +341,7 @@ Section Elts. match n, l with | O, x :: l' => x | O, other => default - | S m, nil => default + | S m, [] => default | S m, x :: t => nth m t default end. @@ -367,26 +349,26 @@ Section Elts. match n, l with | O, x :: l' => true | O, other => false - | S m, nil => false + | S m, [] => false | S m, x :: t => nth_ok m t default end. Lemma nth_in_or_default : forall (n:nat) (l:list A) (d:A), {In (nth n l d) l} + {nth n l d = d}. (* Realizer nth_ok. Program_all. *) - Proof. + Proof. intros n l d; generalize n; induction l; intro n0. right; case n0; trivial. - case n0; simpl in |- *. + case n0; simpl. auto. - intro n1; elim (IHl n1); auto. + intro n1; elim (IHl n1); auto. Qed. Lemma nth_S_cons : forall (n:nat) (l:list A) (d a:A), In (nth n l d) l -> In (nth (S n) (a :: l) d) (a :: l). - Proof. - simpl in |- *; auto. + Proof. + simpl; auto. Qed. Fixpoint nth_error (l:list A) (n:nat) {struct n} : Exc A := @@ -402,13 +384,19 @@ Section Elts. | None => default end. + Lemma nth_default_eq : + forall n l (d:A), nth_default d l n = nth n l d. + Proof. + unfold nth_default; induction n; intros [ | ] ?; simpl; auto. + Qed. + Lemma nth_In : forall (n:nat) (l:list A) (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 |- *. + unfold lt; induction n as [| n hn]; simpl. + destruct l; simpl; [ inversion 2 | auto ]. + destruct l as [| a l hl]; simpl. inversion 2. intros d ie; right; apply hn; auto with arith. Qed. @@ -420,7 +408,7 @@ Section Elts. apply IHl; auto with arith. Qed. - Lemma nth_indep : + 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. @@ -428,7 +416,7 @@ Section Elts. destruct n; simpl; auto with arith. Qed. - Lemma app_nth1 : + Lemma app_nth1 : forall l l' d n, n < length l -> nth n (l++l') d = nth n l d. Proof. induction l. @@ -439,7 +427,7 @@ Section Elts. intros; rewrite IHl; auto with arith. Qed. - Lemma app_nth2 : + 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. @@ -461,53 +449,49 @@ Section Elts. (** ** Remove *) (*****************) - Section Remove. + Hypothesis eq_dec : forall x y : A, {x = y}+{x <> y}. - 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. - - Theorem remove_In : forall (l : list A) (x : A), ~ In x (remove x l). - Proof. - induction l as [|x l]; auto. - intro y; simpl; destruct (eq_dec y x) as [yeqx | yneqx]. - apply IHl. - unfold not; intro HF; simpl in HF; destruct HF; auto. - apply (IHl y); assumption. - Qed. - - End Remove. + Fixpoint remove (x : A) (l : list A) : list A := + match l with + | [] => [] + | y::tl => if (eq_dec x y) then remove x tl else y::(remove x tl) + end. + + Theorem remove_In : forall (l : list A) (x : A), ~ In x (remove x l). + Proof. + induction l as [|x l]; auto. + intro y; simpl; destruct (eq_dec y x) as [yeqx | yneqx]. + apply IHl. + unfold not; intro HF; simpl in HF; destruct HF; auto. + apply (IHl y); assumption. + Qed. (******************************) (** ** Last element of a list *) (******************************) - (** [last l d] returns the last element of the list [l], + (** [last l d] returns the last element 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 + Fixpoint last (l:list A) (d:A) : A := + match l with + | [] => d + | [a] => 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 + Fixpoint removelast (l:list A) : list A := + match l with + | [] => [] + | [a] => [] | a :: l => a :: removelast l end. - - Lemma app_removelast_last : - forall l d, l<>nil -> l = removelast l ++ (last l d :: nil). + + Lemma app_removelast_last : + forall l d, l <> [] -> l = removelast l ++ [last l d]. Proof. induction l. destruct 1; auto. @@ -515,27 +499,27 @@ Section Elts. 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. + + Lemma exists_last : + forall l, l <> [] -> { l' : (list A) & { a : A | l = l' ++ [a]}}. + Proof. induction l. destruct 1; auto. intros _. destruct l. - exists (@nil A); exists a; auto. + exists [], a; auto. destruct IHl as [l' (a',H)]; try discriminate. rewrite H. - exists (a::l'); exists a'; auto. + exists (a::l'), a'; auto. Qed. - Lemma removelast_app : - forall l l', l' <> nil -> removelast (l++l') = l ++ removelast l'. + Lemma removelast_app : + forall l l', l' <> [] -> removelast (l++l') = l ++ removelast l'. Proof. induction l. simpl; auto. simpl; intros. - assert (l++l' <> nil). + assert (l++l' <> []). destruct l. simpl; auto. simpl; discriminate. @@ -543,32 +527,30 @@ Section Elts. destruct (l++l'); [elim H0; auto|f_equal; auto]. Qed. - + (****************************************) (** ** Counting occurences of a element *) (****************************************) - Hypotheses eqA_dec : forall x y : A, {x = y}+{x <> y}. - - Fixpoint count_occ (l : list A) (x : A){struct l} : nat := - match l with - | nil => 0 - | y :: tl => - let n := count_occ tl x in - if eqA_dec y x then S n else n + Fixpoint count_occ (l : list A) (x : A) : nat := + match l with + | [] => 0 + | y :: tl => + let n := count_occ tl x in + if eq_dec y x then S n else n end. - + (** Compatibility of count_occ with operations on list *) Theorem count_occ_In : forall (l : list A) (x : A), In x l <-> count_occ l x > 0. Proof. induction l as [|y l]. simpl; intros; split; [destruct 1 | apply gt_irrefl]. - simpl. intro x; destruct (eqA_dec y x) as [Heq|Hneq]. - rewrite Heq; intuition. + simpl. intro x; destruct (eq_dec y x) as [Heq|Hneq]. + rewrite Heq; intuition. pose (IHl x). intuition. Qed. - - Theorem count_occ_inv_nil : forall (l : list A), (forall x:A, count_occ l x = 0) <-> l = nil. + + Theorem count_occ_inv_nil : forall (l : list A), (forall x:A, count_occ l x = 0) <-> l = []. Proof. split. (* Case -> *) @@ -578,14 +560,14 @@ Section Elts. elim (O_S (count_occ l x)). apply sym_eq. generalize (H x). - simpl. destruct (eqA_dec x x) as [|HF]. + simpl. destruct (eq_dec x x) as [|HF]. trivial. elim HF; reflexivity. (* Case <- *) intro H; rewrite H; simpl; reflexivity. Qed. - - Lemma count_occ_nil : forall (x : A), count_occ nil x = 0. + + Lemma count_occ_nil : forall (x : A), count_occ [] x = 0. Proof. intro x; simpl; reflexivity. Qed. @@ -593,13 +575,13 @@ Section Elts. Lemma count_occ_cons_eq : forall (l : list A) (x y : A), x = y -> count_occ (x::l) y = S (count_occ l y). Proof. intros l x y H; simpl. - destruct (eqA_dec x y); [reflexivity | contradiction]. + destruct (eq_dec x y); [reflexivity | contradiction]. Qed. - + Lemma count_occ_cons_neq : forall (l : list A) (x y : A), x <> y -> count_occ (x::l) y = count_occ l y. Proof. intros l x y H; simpl. - destruct (eqA_dec x y); [contradiction | reflexivity]. + destruct (eq_dec x y); [contradiction | reflexivity]. Qed. End Elts. @@ -620,38 +602,38 @@ Section ListOps. Fixpoint rev (l:list A) : list A := match l with - | nil => nil - | x :: l' => rev l' ++ x :: nil + | [] => [] + | x :: l' => rev l' ++ [x] end. - Lemma distr_rev : forall x y:list A, rev (x ++ y) = rev y ++ rev x. + Lemma rev_app_distr : forall x y:list A, rev (x ++ y) = rev y ++ rev x. Proof. induction x as [| a l IHl]. destruct y as [| a l]. - simpl in |- *. + simpl. auto. - simpl in |- *. - apply app_nil_end; auto. + simpl. + rewrite app_nil_r; auto. intro y. - simpl in |- *. + simpl. rewrite (IHl y). - apply (app_ass (rev y) (rev l) (a :: nil)). + rewrite app_assoc; trivial. Qed. - Remark rev_unit : forall (l:list A) (a:A), rev (l ++ a :: nil) = a :: rev l. + Remark rev_unit : forall (l:list A) (a:A), rev (l ++ [a]) = a :: rev l. Proof. intros. - apply (distr_rev l (a :: nil)); simpl in |- *; auto. + apply (rev_app_distr l [a]); simpl; auto. Qed. Lemma rev_involutive : forall l:list A, rev (rev l) = l. Proof. induction l as [| a l IHl]. - simpl in |- *; auto. + simpl; auto. - simpl in |- *. + simpl. rewrite (rev_unit (rev l) a). rewrite IHl; auto. Qed. @@ -659,7 +641,7 @@ Section ListOps. (** Compatibility with other operations *) - Lemma In_rev : forall l x, In x l <-> In x (rev l). + Lemma in_rev : forall l x, In x l <-> In x (rev l). Proof. induction l. simpl; intuition. @@ -681,7 +663,7 @@ Section ListOps. elim (length l); simpl; auto. Qed. - Lemma rev_nth : forall l d n, n < length l -> + 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. @@ -704,309 +686,77 @@ Section ListOps. Qed. - (** An alternative tail-recursive definition for reverse *) + (** An alternative tail-recursive definition for reverse *) - Fixpoint rev_append (l l': list A) {struct l} : list A := - match l with - | nil => l' + Fixpoint rev_append (l l': list A) : list A := + match l with + | [] => l' | a::l => rev_append l (a::l') end. - Definition rev' l : list A := rev_append l nil. - - Notation rev_acc := rev_append (only parsing). + Definition rev' l : list A := rev_append l []. - Lemma rev_append_rev : forall l l', rev_acc l l' = rev l ++ l'. + Lemma rev_append_rev : forall l l', rev_append l l' = rev l ++ l'. Proof. induction l; simpl; auto; intros. - rewrite <- ass_app; firstorder. + rewrite <- app_assoc; firstorder. Qed. - Notation rev_acc_rev := rev_append_rev (only parsing). - - Lemma rev_alt : forall l, rev l = rev_append l nil. + Lemma rev_alt : forall l, rev l = rev_append l []. Proof. intros; rewrite rev_append_rev. - apply app_nil_end. + rewrite app_nil_r; trivial. Qed. (*********************************************) (** Reverse Induction Principle on Lists *) (*********************************************) - + Section Reverse_Induction. - - Unset Implicit Arguments. - + Lemma rev_list_ind : forall P:list A-> Prop, - P nil -> + P [] -> (forall (a:A) (l:list A), P (rev l) -> P (rev (a :: l))) -> forall l:list A, P (rev l). Proof. induction l; auto. Qed. - Set Implicit Arguments. - + Theorem rev_ind : forall P:list A -> Prop, - P nil -> - (forall (x:A) (l:list A), P l -> P (l ++ x :: nil)) -> forall l:list A, P l. + P [] -> + (forall (x:A) (l:list A), P l -> P (l ++ [x])) -> forall l:list A, P l. Proof. intros. generalize (rev_involutive l). intros E; rewrite <- E. apply (rev_list_ind P). auto. - - simpl in |- *. + + simpl. intros. apply (H0 a (rev l0)). auto. Qed. - - End Reverse_Induction. - - - - (***********************************) - (** ** Lists modulo permutation *) - (***********************************) - - Section Permutation. - - Inductive Permutation : list A -> list A -> Prop := - | perm_nil: Permutation nil nil - | perm_skip: forall (x:A) (l l':list A), Permutation l l' -> Permutation (cons x l) (cons x l') - | perm_swap: forall (x y:A) (l:list A), Permutation (cons y (cons x l)) (cons x (cons y l)) - | perm_trans: forall (l l' l'':list A), Permutation l l' -> Permutation l' l'' -> Permutation l l''. - - Hint Constructors Permutation. - - (** Some facts about [Permutation] *) - - Theorem Permutation_nil : forall (l : list A), Permutation nil l -> l = nil. - Proof. - intros l HF. - set (m:=@nil A) in HF; assert (m = nil); [reflexivity|idtac]; clearbody m. - induction HF; try elim (nil_cons (sym_eq H)); auto. - Qed. - - Theorem Permutation_nil_cons : forall (l : list A) (x : A), ~ Permutation nil (x::l). - Proof. - unfold not; intros l x HF. - elim (@nil_cons A x l). apply sym_eq. exact (Permutation_nil HF). - Qed. - - (** Permutation over lists is a equivalence relation *) - - Theorem Permutation_refl : forall l : list A, Permutation l l. - Proof. - induction l; constructor. exact IHl. - Qed. - - Theorem Permutation_sym : forall l l' : list A, Permutation l l' -> Permutation l' l. - Proof. - intros l l' Hperm; induction Hperm; auto. - apply perm_trans with (l':=l'); assumption. - Qed. - - Theorem Permutation_trans : forall l l' l'' : list A, Permutation l l' -> Permutation l' l'' -> Permutation l l''. - Proof. - exact perm_trans. - Qed. - - Hint Resolve Permutation_refl Permutation_sym Permutation_trans. - - (** Compatibility with others operations on lists *) - - Theorem Permutation_in : forall (l l' : list A) (x : A), Permutation l l' -> In x l -> In x l'. - Proof. - intros l l' x Hperm; induction Hperm; simpl; tauto. - Qed. - - Lemma Permutation_app_tail : forall (l l' tl : list A), Permutation l l' -> Permutation (l++tl) (l'++tl). - Proof. - intros l l' tl Hperm; induction Hperm as [|x l l'|x y l|l l' l'']; simpl; auto. - eapply Permutation_trans with (l':=l'++tl); trivial. - Qed. - - Lemma Permutation_app_head : forall (l tl tl' : list A), Permutation tl tl' -> Permutation (l++tl) (l++tl'). - Proof. - intros l tl tl' Hperm; induction l; [trivial | repeat rewrite <- app_comm_cons; constructor; assumption]. - Qed. - - Theorem Permutation_app : forall (l m l' m' : list A), Permutation l l' -> Permutation m m' -> Permutation (l++m) (l'++m'). - Proof. - 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. - apply Permutation_trans with (l' := (x :: y :: l ++ m)); - [idtac | repeat rewrite app_comm_cons; apply Permutation_app_head]; trivial. - apply Permutation_trans with (l' := (l' ++ m')); try assumption. - apply Permutation_app_tail; assumption. - Qed. - - Theorem Permutation_app_swap : forall (l l' : list A), Permutation (l++l') (l'++l). - Proof. - induction l as [|x l]. - simpl; intro l'; rewrite <- app_nil_end; trivial. - induction l' as [|y l']. - simpl; rewrite <- app_nil_end; trivial. - simpl; apply Permutation_trans with (l' := x :: y :: l' ++ l). - constructor; rewrite app_comm_cons; apply IHl. - apply Permutation_trans with (l' := y :: x :: l' ++ l); constructor. - apply Permutation_trans with (l' := x :: l ++ l'); auto. - Qed. - - Theorem Permutation_cons_app : forall (l l1 l2:list A) a, - Permutation l (l1 ++ l2) -> Permutation (a :: l) (l1 ++ a :: l2). - Proof. - intros l l1; revert l. - induction l1. - simpl. - intros; apply perm_skip; auto. - simpl; intros. - apply perm_trans with (a0::a::l1++l2). - apply perm_skip; auto. - apply perm_trans with (a::a0::l1++l2). - apply perm_swap; auto. - apply perm_skip; auto. - Qed. - Hint Resolve Permutation_cons_app. - - Theorem Permutation_length : forall (l l' : list A), Permutation l l' -> length l = length l'. - Proof. - intros l l' Hperm; induction Hperm; simpl; auto. - apply trans_eq with (y:= (length l')); trivial. - Qed. - - Theorem Permutation_rev : forall (l : list A), Permutation l (rev l). - Proof. - induction l as [| x l]; simpl; trivial. - apply Permutation_trans with (l' := (x::nil)++rev l). - simpl; auto. - apply Permutation_app_swap. - Qed. - - Theorem Permutation_ind_bis : - forall P : list A -> list A -> Prop, - P (@nil A) (@nil A) -> - (forall x l l', Permutation l l' -> P l l' -> P (x :: l) (x :: l')) -> - (forall x y l l', Permutation l l' -> P l l' -> P (y :: x :: l) (x :: y :: l')) -> - (forall l l' l'', Permutation l l' -> P l l' -> Permutation l' l'' -> P l' l'' -> P l l'') -> - forall l l', Permutation l l' -> P l l'. - Proof. - intros P Hnil Hskip Hswap Htrans. - induction 1; auto. - apply Htrans with (x::y::l); auto. - apply Hswap; auto. - induction l; auto. - apply Hskip; auto. - apply Hskip; auto. - induction l; auto. - eauto. - Qed. - - Ltac break_list l x l' H := - destruct l as [|x l']; simpl in *; - injection H; intros; subst; clear H. - - Theorem Permutation_app_inv : forall (l1 l2 l3 l4:list A) a, - Permutation (l1++a::l2) (l3++a::l4) -> Permutation (l1++l2) (l3 ++ l4). - Proof. - set (P:=fun l l' => - forall a l1 l2 l3 l4, l=l1++a::l2 -> l'=l3++a::l4 -> Permutation (l1++l2) (l3++l4)). - cut (forall l l', Permutation l l' -> P l l'). - intros; apply (H _ _ H0 a); auto. - intros; apply (Permutation_ind_bis P); unfold P; clear P; try clear H l l'; simpl; auto. - (* nil *) - intros; destruct l1; simpl in *; discriminate. - (* skip *) - intros x l l' H IH; intros. - break_list l1 b l1' H0; break_list l3 c l3' H1. - auto. - apply perm_trans with (l3'++c::l4); auto. - apply perm_trans with (l1'++a::l2); auto using Permutation_cons_app. - apply perm_skip. - apply (IH a l1' l2 l3' l4); auto. - (* contradict *) - intros x y l l' Hp IH; intros. - break_list l1 b l1' H; break_list l3 c l3' H0. - auto. - break_list l3' b l3'' H. - auto. - apply perm_trans with (c::l3''++b::l4); auto. - break_list l1' c l1'' H1. - auto. - apply perm_trans with (b::l1''++c::l2); auto. - break_list l3' d l3'' H; break_list l1' e l1'' H1. - auto. - apply perm_trans with (e::a::l1''++l2); auto. - apply perm_trans with (e::l1''++a::l2); auto. - apply perm_trans with (d::a::l3''++l4); auto. - apply perm_trans with (d::l3''++a::l4); auto. - apply perm_trans with (e::d::l1''++l2); auto. - apply perm_skip; apply perm_skip. - apply (IH a l1'' l2 l3'' l4); auto. - (*trans*) - intros. - destruct (In_split a l') as (l'1,(l'2,H6)). - apply (Permutation_in a H). - subst l. - apply in_or_app; right; red; auto. - apply perm_trans with (l'1++l'2). - apply (H0 _ _ _ _ _ H3 H6). - apply (H2 _ _ _ _ _ H6 H4). - Qed. - - Theorem Permutation_cons_inv : - forall l l' a, Permutation (a::l) (a::l') -> Permutation l l'. - Proof. - intros; exact (Permutation_app_inv (@nil _) l (@nil _) l' a H). - Qed. - - Theorem Permutation_cons_app_inv : - forall l l1 l2 a, Permutation (a :: l) (l1 ++ a :: l2) -> Permutation l (l1 ++ l2). - Proof. - intros; exact (Permutation_app_inv (@nil _) l l1 l2 a H). - Qed. - - Theorem Permutation_app_inv_l : - forall l l1 l2, Permutation (l ++ l1) (l ++ l2) -> Permutation l1 l2. - Proof. - induction l; simpl; auto. - intros. - apply IHl. - apply Permutation_cons_inv with a; auto. - Qed. - - Theorem Permutation_app_inv_r : - forall l l1 l2, Permutation (l1 ++ l) (l2 ++ l) -> Permutation l1 l2. - Proof. - induction l. - intros l1 l2; do 2 rewrite <- app_nil_end; auto. - intros. - apply IHl. - apply Permutation_app_inv with a; auto. - Qed. - - End Permutation. + End Reverse_Induction. (***********************************) (** ** Decidable equality on lists *) (***********************************) - Hypotheses eqA_dec : forall (x y : A), {x = y}+{x <> y}. + Hypothesis eq_dec : forall (x y : A), {x = y}+{x <> y}. Lemma list_eq_dec : forall l l':list A, {l = l'} + {l <> l'}. Proof. induction l as [| x l IHl]; destruct l' as [| y l']. left; trivial. - right; apply nil_cons. + right; apply nil_cons. right; unfold not; intro HF; apply (nil_cons (sym_eq HF)). - destruct (eqA_dec x y) as [xeqy|xneqy]; destruct (IHl l') as [leql'|lneql']; + destruct (eq_dec x y) as [xeqy|xneqy]; destruct (IHl l') as [leql'|lneql']; try (right; unfold not; intro HF; injection HF; intros; contradiction). rewrite xeqy; rewrite leql'; left; trivial. Qed. @@ -1026,21 +776,19 @@ End ListOps. Section Map. Variables A B : Type. 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. - + Lemma in_map : 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 ] ]. + Proof. + induction l; firstorder (subst; auto). Qed. - + 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). @@ -1051,45 +799,48 @@ Section Map. induction l; simpl; auto. Qed. - Lemma map_nth : forall l d n, + 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', + + Lemma map_nth_error : forall n l d, + nth_error l n = Some d -> nth_error (map l) n = Some (f d). + Proof. + induction n; intros [ | ] ? Heq; simpl in *; inversion Heq; auto. + Qed. + + Lemma map_app : forall l l', map (l++l') = (map l)++(map l'). - Proof. + Proof. induction l; simpl; auto. intros; rewrite IHl; auto. Qed. - + Lemma map_rev : forall l, map (rev l) = rev (map l). - Proof. + Proof. induction l; simpl; auto. rewrite map_app. rewrite IHl; auto. Qed. - Hint Constructors Permutation. - - Lemma Permutation_map : - forall l l', Permutation l l' -> Permutation (map l) (map l'). - Proof. - induction 1; simpl; auto; eauto. + Lemma map_eq_nil : forall l, map l = [] -> l = []. + Proof. + destruct l; simpl; reflexivity || discriminate. Qed. (** [flat_map] *) Definition flat_map (f:A -> list B) := - fix flat_map (l:list A) {struct l} : list B := + fix flat_map (l:list A) : list B := match l with | nil => nil | cons x t => (f x)++(flat_map t) end. - + 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). + In y (flat_map f l) <-> exists x, In x l /\ In y (f x). Proof. induction l; simpl; split; intros. contradiction. @@ -1105,16 +856,22 @@ Section Map. exists x; auto. Qed. -End Map. +End Map. + +Lemma map_id : forall (A :Type) (l : list A), + map (fun x => x) l = l. +Proof. + induction l; simpl; auto; rewrite IHl; auto. +Qed. -Lemma map_map : forall (A B C:Type)(f:A->B)(g:B->C) l, +Lemma map_map : forall (A B C:Type)(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 : +Lemma map_ext : forall (A B : Type)(f g:A->B), (forall a, f a = g a) -> forall l, map f l = map g l. Proof. induction l; simpl; auto. @@ -1129,17 +886,17 @@ Qed. Section Fold_Left_Recursor. Variables A B : Type. Variable f : A -> B -> A. - - Fixpoint fold_left (l:list B) (a0:A) {struct l} : A := + + Fixpoint fold_left (l:list B) (a0:A) : 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), + + 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. + induction l. simpl; auto. intros. simpl. @@ -1148,7 +905,7 @@ Section Fold_Left_Recursor. End Fold_Left_Recursor. -Lemma fold_left_length : +Lemma fold_left_length : forall (A:Type)(l:list A), fold_left (fun x _ => S x) l 0 = length l. Proof. intro A. @@ -1168,7 +925,7 @@ Section Fold_Right_Recursor. Variables A B : Type. Variable f : B -> A -> A. Variable a0 : A. - + Fixpoint fold_right (l:list B) : A := match l with | nil => a0 @@ -1177,7 +934,7 @@ Section Fold_Right_Recursor. End Fold_Right_Recursor. - Lemma fold_right_app : forall (A B:Type)(f:A->B->B) l l' i, + Lemma fold_right_app : forall (A B:Type)(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. @@ -1186,7 +943,7 @@ End Fold_Right_Recursor. f_equal; auto. Qed. - Lemma fold_left_rev_right : forall (A B:Type)(f:A->B->B) l i, + Lemma fold_left_rev_right : forall (A B:Type)(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. @@ -1204,10 +961,10 @@ End Fold_Right_Recursor. Proof. destruct l as [| a l]. reflexivity. - simpl in |- *. + simpl. rewrite <- H0. generalize a0 a. - induction l as [| a3 l IHl]; simpl in |- *. + induction l as [| a3 l IHl]; simpl. trivial. intros. rewrite H. @@ -1223,7 +980,7 @@ End Fold_Right_Recursor. (** [(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:Type)(l:list A) (l':list B) {struct l} : + Fixpoint list_power (A B:Type)(l:list A) (l':list B) : list (list (A * B)) := match l with | nil => cons nil nil @@ -1237,20 +994,20 @@ End Fold_Right_Recursor. (** ** Boolean operations over lists *) (*************************************) - Section Bool. + Section Bool. Variable A : Type. Variable f : A -> bool. - (** find whether a boolean function can be satisfied by an + (** 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 + Fixpoint existsb (l:list A) : bool := + match l with | nil => false | a::l => f a || existsb l end. - Lemma existsb_exists : + Lemma existsb_exists : forall l, existsb l = true <-> exists x, In x l /\ f x = true. Proof. induction l; simpl; intuition. @@ -1269,20 +1026,28 @@ End Fold_Right_Recursor. inversion 1. simpl; intros. destruct (orb_false_elim _ _ H0); clear H0; auto. - destruct n ; auto. + destruct n ; auto. rewrite IHl; auto with arith. Qed. - (** find whether a boolean function is satisfied by + Lemma existsb_app : forall l1 l2, + existsb (l1++l2) = existsb l1 || existsb l2. + Proof. + induction l1; intros l2; simpl. + solve[auto]. + case (f a); simpl; solve[auto]. + 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 + Fixpoint forallb (l:list A) : bool := + match l with | nil => true | a::l => f a && forallb l end. - Lemma forallb_forall : + Lemma forallb_forall : forall l, forallb l = true <-> (forall x, In x l -> f x = true). Proof. induction l; simpl; intuition. @@ -1291,13 +1056,20 @@ End Fold_Right_Recursor. destruct (andb_prop _ _ H1); auto. assert (forallb l = true). apply H0; intuition. - rewrite H1; auto. + rewrite H1; auto. Qed. + Lemma forallb_app : + forall l1 l2, forallb (l1++l2) = forallb l1 && forallb l2. + Proof. + induction l1; simpl. + solve[auto]. + case (f a); simpl; solve[auto]. + Qed. (** [filter] *) - Fixpoint filter (l:list A) : list A := - match l with + 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. @@ -1320,10 +1092,10 @@ End Fold_Right_Recursor. (** [partition] *) - Fixpoint partition (l:list A) {struct l} : list A * list A := + Fixpoint partition (l:list A) : list A * list A := match l with | nil => (nil, nil) - | x :: tl => let (g,d) := partition tl in + | x :: tl => let (g,d) := partition tl in if f x then (x::g,d) else (g,x::d) end. @@ -1338,17 +1110,17 @@ End Fold_Right_Recursor. Section ListPairs. Variables A B : Type. - + (** [split] derives two lists from a list of pairs *) - Fixpoint split (l:list (A*B)) { struct l }: list A * list B := + 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. - Lemma in_split_l : forall (l:list (A*B))(p:A*B), - In p l -> In (fst p) (fst (split l)). + 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 *. @@ -1357,8 +1129,8 @@ End Fold_Right_Recursor. 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)). + 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 *. @@ -1367,7 +1139,7 @@ End Fold_Right_Recursor. right; apply (IHl (a0,b) H). Qed. - Lemma split_nth : forall (l:list (A*B))(n:nat)(d:A*B), + 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. @@ -1379,40 +1151,40 @@ End Fold_Right_Recursor. Qed. Lemma split_length_l : forall (l:list (A*B)), - length (fst (split l)) = length l. + length (fst (split l)) = length l. Proof. induction l; simpl; auto. destruct a; destruct (split l); simpl; auto. Qed. Lemma split_length_r : forall (l:list (A*B)), - length (snd (split l)) = length l. + 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. + (** [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) := + Fixpoint combine (l : list A) (l' : list B) : 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)), + 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 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' -> + 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. @@ -1420,19 +1192,19 @@ End Fold_Right_Recursor. rewrite IHl; auto. Qed. - Lemma in_combine_l : forall (l:list A)(l':list B)(x:A)(y:B), + 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. + 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), + 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. @@ -1443,7 +1215,7 @@ End Fold_Right_Recursor. right; apply IHl with x; auto. Qed. - Lemma combine_length : forall (l:list A)(l':list B), + Lemma combine_length : forall (l:list A)(l':list B), length (combine l l') = min (length l) (length l'). Proof. induction l. @@ -1451,8 +1223,8 @@ End Fold_Right_Recursor. 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' -> + 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. @@ -1461,10 +1233,10 @@ End Fold_Right_Recursor. Qed. (** [list_prod] has the same signature as [combine], but unlike - [combine], it adds every possible pairs, not only those at the + [combine], it adds every possible pairs, not only those at the same position. *) - Fixpoint list_prod (l:list A) (l':list B) {struct l} : + Fixpoint list_prod (l:list A) (l':list B) : list (A * B) := match l with | nil => nil @@ -1474,25 +1246,25 @@ End Fold_Right_Recursor. Lemma in_prod_aux : forall (x:A) (y:B) (l:list B), In y l -> In (x, y) (map (fun y0:B => (x, y0)) l). - Proof. + Proof. induction l; - [ simpl in |- *; auto - | simpl in |- *; destruct 1 as [H1| ]; + [ simpl; auto + | simpl; destruct 1 as [H1| ]; [ left; rewrite H1; trivial | right; auto ] ]. Qed. Lemma in_prod : 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. + Proof. induction l; - [ simpl in |- *; tauto - | simpl in |- *; intros; apply in_or_app; destruct H; + [ simpl; tauto + | simpl; intros; apply in_or_app; destruct H; [ 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), + 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 ]. @@ -1503,9 +1275,9 @@ End Fold_Right_Recursor. destruct (H1 H0) as (z,(H2,H3)); clear H0 H1. injection H2; clear H2; intros; subst; intuition. intuition. - Qed. + Qed. - Lemma prod_length : forall (l:list A)(l':list B), + Lemma prod_length : forall (l:list A)(l':list B), length (list_prod l l') = (length l) * (length l'). Proof. induction l; simpl; auto. @@ -1520,9 +1292,9 @@ End Fold_Right_Recursor. -(***************************************) -(** * Miscelenous operations on lists *) -(***************************************) +(*****************************************) +(** * Miscellaneous operations on lists *) +(*****************************************) @@ -1539,34 +1311,34 @@ Section length_order. Variables l m n : list A. Lemma lel_refl : lel l l. - Proof. - unfold lel in |- *; auto with arith. + Proof. + unfold lel; auto with arith. Qed. Lemma lel_trans : lel l m -> lel m n -> lel l n. - Proof. - unfold lel in |- *; intros. + Proof. + unfold lel; intros. now_show (length l <= length n). apply le_trans with (length m); auto with arith. Qed. Lemma lel_cons_cons : lel l m -> lel (a :: l) (b :: m). - Proof. - unfold lel in |- *; simpl in |- *; auto with arith. + Proof. + unfold lel; simpl; auto with arith. Qed. Lemma lel_cons : lel l m -> lel l (b :: m). - Proof. - unfold lel in |- *; simpl in |- *; auto with arith. + Proof. + unfold lel; simpl; auto with arith. Qed. Lemma lel_tail : lel (a :: l) (b :: m) -> lel l m. - Proof. - unfold lel in |- *; simpl in |- *; auto with arith. + Proof. + unfold lel; simpl; auto with arith. Qed. Lemma lel_nil : forall l':list A, lel l' nil -> nil = l'. - Proof. + Proof. intro l'; elim l'; auto with arith. intros a' y H H0. now_show (nil = a' :: y). @@ -1588,40 +1360,40 @@ Section SetIncl. Definition incl (l m:list A) := forall a:A, In a l -> In a m. Hint Unfold incl. - + Lemma incl_refl : forall l:list A, incl l l. - Proof. + Proof. auto. Qed. Hint Resolve incl_refl. - + Lemma incl_tl : forall (a:A) (l m:list A), incl l m -> incl l (a :: m). - Proof. + Proof. auto with datatypes. Qed. Hint Immediate incl_tl. Lemma incl_tran : forall l m n:list A, incl l m -> incl m n -> incl l n. - Proof. + Proof. auto. Qed. - + Lemma incl_appl : forall l m n:list A, incl l n -> incl l (n ++ m). - Proof. + Proof. auto with datatypes. Qed. Hint Immediate incl_appl. - + Lemma incl_appr : forall l m n:list A, incl l n -> incl l (m ++ n). - Proof. + Proof. auto with datatypes. Qed. Hint Immediate incl_appr. - + Lemma incl_cons : forall (a:A) (l m:list A), In a m -> incl l m -> incl (a :: l) m. - Proof. - unfold incl in |- *; simpl in |- *; intros a l m H H0 a0 H1. + Proof. + unfold incl; simpl; intros a l m H H0 a0 H1. now_show (In a0 m). elim H1. now_show (a = a0 -> In a0 m). @@ -1632,15 +1404,15 @@ Section SetIncl. auto. Qed. Hint Resolve incl_cons. - + Lemma incl_app : forall l m n:list A, incl l n -> incl m n -> incl (l ++ m) n. - Proof. - unfold incl in |- *; simpl in |- *; intros l m n H H0 a H1. + Proof. + unfold incl; simpl; intros l m n H H0 a H1. now_show (In a n). elim (in_app_or _ _ _ H1); auto. Qed. Hint Resolve incl_app. - + End SetIncl. Hint Resolve incl_refl incl_tl incl_tran incl_appl incl_appr incl_cons @@ -1655,24 +1427,24 @@ Section Cutting. Variable A : Type. - Fixpoint firstn (n:nat)(l:list A) {struct n} : list A := - match n with - | 0 => nil - | S n => match l with - | nil => nil + Fixpoint firstn (n:nat)(l:list A) : 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 + + Fixpoint skipn (n:nat)(l:list A) : 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. @@ -1686,7 +1458,7 @@ Section Cutting. induction n; destruct l; simpl; auto. Qed. - Lemma removelast_firstn : forall n l, n < length l -> + Lemma removelast_firstn : forall n l, n < length l -> removelast (firstn (S n) l) = firstn n l. Proof. induction n; destruct l. @@ -1699,13 +1471,13 @@ Section Cutting. change (firstn (S n) (a::l)) with (a::firstn n l). rewrite removelast_app. rewrite IHn; auto with arith. - + clear IHn; destruct l; simpl in *; try discriminate. inversion_clear H. inversion_clear H0. Qed. - Lemma firstn_removelast : forall n l, n < length l -> + Lemma firstn_removelast : forall n l, n < length l -> firstn n (removelast l) = firstn n l. Proof. induction n; destruct l. @@ -1730,10 +1502,10 @@ End Cutting. Section ReDun. Variable A : Type. - - Inductive NoDup : list A -> Prop := - | NoDup_nil : NoDup nil - | NoDup_cons : forall x l, ~ In x l -> NoDup l -> NoDup (x::l). + + Inductive NoDup : list A -> Prop := + | NoDup_nil : NoDup nil + | NoDup_cons : forall x l, ~ In x l -> NoDup l -> NoDup (x::l). Lemma NoDup_remove_1 : forall l l' a, NoDup (l++a::l') -> NoDup (l++l'). Proof. @@ -1758,34 +1530,6 @@ Section ReDun. destruct (IHl _ _ H1); auto. Qed. - Lemma NoDup_Permutation : forall l l', - NoDup l -> NoDup l' -> (forall x, In x l <-> In x l') -> Permutation l l'. - Proof. - induction l. - destruct l'; simpl; intros. - apply perm_nil. - destruct (H1 a) as (_,H2); destruct H2; auto. - intros. - destruct (In_split a l') as (l'1,(l'2,H2)). - destruct (H1 a) as (H2,H3); simpl in *; auto. - subst l'. - apply Permutation_cons_app. - inversion_clear H. - apply IHl; auto. - apply NoDup_remove_1 with a; auto. - intro x; split; intros. - assert (In x (l'1++a::l'2)). - destruct (H1 x); simpl in *; auto. - apply in_or_app; destruct (in_app_or _ _ _ H4); auto. - destruct H5; auto. - subst x; destruct H2; auto. - assert (In x (l'1++a::l'2)). - apply in_or_app; destruct (in_app_or _ _ _ H); simpl; auto. - destruct (H1 x) as (_,H5); destruct H5; auto. - subst x. - destruct (NoDup_remove_2 _ _ _ H0 H). - Qed. - End ReDun. @@ -1795,21 +1539,21 @@ End ReDun. Section NatSeq. - (** [seq] computes the sequence of [len] contiguous integers + (** [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 + + Fixpoint seq (start len:nat) : list nat := + match len with | 0 => nil | S len => start :: seq (S start) len - end. - + 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, + + Lemma seq_nth : forall len start n d, n < len -> nth n (seq start len) d = start+n. Proof. induction len; intros. @@ -1822,7 +1566,7 @@ Section NatSeq. Lemma seq_shift : forall len start, map S (seq start len) = seq (S start) len. - Proof. + Proof. induction len; simpl; auto. intros. rewrite IHlen. @@ -1832,11 +1576,172 @@ Section NatSeq. End NatSeq. +(** * Existential and universal predicates over lists *) + +Inductive Exists {A} (P:A->Prop) : list A -> Prop := + | Exists_cons_hd : forall x l, P x -> Exists P (x::l) + | Exists_cons_tl : forall x l, Exists P l -> Exists P (x::l). +Hint Constructors Exists. + +Lemma Exists_exists : forall A P (l:list A), + Exists P l <-> (exists x, In x l /\ P x). +Proof. +split. +induction 1; firstorder. +induction l; firstorder; subst; auto. +Qed. + +Lemma Exists_nil : forall A (P:A->Prop), Exists P nil <-> False. +Proof. split; inversion 1. Qed. + +Lemma Exists_cons : forall A (P:A->Prop) x l, + Exists P (x::l) <-> P x \/ Exists P l. +Proof. split; inversion 1; auto. Qed. + + +Inductive Forall {A} (P:A->Prop) : list A -> Prop := + | Forall_nil : Forall P nil + | Forall_cons : forall x l, P x -> Forall P l -> Forall P (x::l). +Hint Constructors Forall. - (** * Exporting hints and tactics *) +Lemma Forall_forall : forall A P (l:list A), + Forall P l <-> (forall x, In x l -> P x). +Proof. +split. +induction 1; firstorder; subst; auto. +induction l; firstorder. +Qed. + +Lemma Forall_inv : forall A P (a:A) l, Forall P (a :: l) -> P a. +Proof. +intros; inversion H; trivial. +Defined. + +Lemma Forall_rect : forall A (P:A->Prop) (Q : list A -> Type), + Q [] -> (forall b l, P b -> Q (b :: l)) -> forall l, Forall P l -> Q l. +Proof. +intros A P Q H H'; induction l; intro; [|eapply H', Forall_inv]; eassumption. +Defined. + +Lemma Forall_impl : forall A (P Q : A -> Prop), (forall a, P a -> Q a) -> + forall l, Forall P l -> Forall Q l. +Proof. + intros A P Q Himp l H. + induction H; firstorder. +Qed. +(** [Forall2]: stating that elements of two lists are pairwise related. *) -Hint Rewrite +Inductive Forall2 A B (R:A->B->Prop) : list A -> list B -> Prop := + | Forall2_nil : Forall2 R [] [] + | Forall2_cons : forall x y l l', + R x y -> Forall2 R l l' -> Forall2 R (x::l) (y::l'). +Hint Constructors Forall2. + +Theorem Forall2_refl : forall A B (R:A->B->Prop), Forall2 R [] []. +Proof. exact Forall2_nil. Qed. + +Theorem Forall2_app_inv_l : forall A B (R:A->B->Prop) l1 l2 l', + Forall2 R (l1 ++ l2) l' -> + exists l1', exists l2', Forall2 R l1 l1' /\ Forall2 R l2 l2' /\ l' = l1' ++ l2'. +Proof. + induction l1; intros. + exists [], l'; auto. + simpl in H; inversion H; subst; clear H. + apply IHl1 in H4 as (l1' & l2' & Hl1 & Hl2 & ->). + exists (y::l1'), l2'; simpl; auto. +Qed. + +Theorem Forall2_app_inv_r : forall A B (R:A->B->Prop) l1' l2' l, + Forall2 R l (l1' ++ l2') -> + exists l1, exists l2, Forall2 R l1 l1' /\ Forall2 R l2 l2' /\ l = l1 ++ l2. +Proof. + induction l1'; intros. + exists [], l; auto. + simpl in H; inversion H; subst; clear H. + apply IHl1' in H4 as (l1 & l2 & Hl1 & Hl2 & ->). + exists (x::l1), l2; simpl; auto. +Qed. + +Theorem Forall2_app : forall A B (R:A->B->Prop) l1 l2 l1' l2', + Forall2 R l1 l1' -> Forall2 R l2 l2' -> Forall2 R (l1 ++ l2) (l1' ++ l2'). +Proof. + intros. induction l1 in l1', H, H0 |- *; inversion H; subst; simpl; auto. +Qed. + +(** [ForallPairs] : specifies that a certain relation should + always hold when inspecting all possible pairs of elements of a list. *) + +Definition ForallPairs A (R : A -> A -> Prop) l := + forall a b, In a l -> In b l -> R a b. + +(** [ForallOrdPairs] : we still check a relation over all pairs + of elements of a list, but now the order of elements matters. *) + +Inductive ForallOrdPairs A (R : A -> A -> Prop) : list A -> Prop := + | FOP_nil : ForallOrdPairs R nil + | FOP_cons : forall a l, + Forall (R a) l -> ForallOrdPairs R l -> ForallOrdPairs R (a::l). +Hint Constructors ForallOrdPairs. + +Lemma ForallOrdPairs_In : forall A (R:A->A->Prop) l, + ForallOrdPairs R l -> + forall x y, In x l -> In y l -> x=y \/ R x y \/ R y x. +Proof. + induction 1. + inversion 1. + simpl; destruct 1; destruct 1; repeat subst; auto. + right; left. apply -> Forall_forall; eauto. + right; right. apply -> Forall_forall; eauto. +Qed. + + +(** [ForallPairs] implies [ForallOrdPairs]. The reverse implication is true + only when [R] is symmetric and reflexive. *) + +Lemma ForallPairs_ForallOrdPairs : forall A (R:A->A->Prop) l, + ForallPairs R l -> ForallOrdPairs R l. +Proof. + induction l; auto. intros H. + constructor. + apply <- Forall_forall. intros; apply H; simpl; auto. + apply IHl. red; intros; apply H; simpl; auto. +Qed. + +Lemma ForallOrdPairs_ForallPairs : forall A (R:A->A->Prop), + (forall x, R x x) -> + (forall x y, R x y -> R y x) -> + forall l, ForallOrdPairs R l -> ForallPairs R l. +Proof. + intros A R Refl Sym l Hl x y Hx Hy. + destruct (ForallOrdPairs_In Hl _ _ Hx Hy); subst; intuition. +Qed. + +(** * Inversion of predicates over lists based on head symbol *) + +Ltac is_list_constr c := + match c with + | nil => idtac + | (_::_) => idtac + | _ => fail + end. + +Ltac invlist f := + match goal with + | H:f ?l |- _ => is_list_constr l; inversion_clear H; invlist f + | H:f _ ?l |- _ => is_list_constr l; inversion_clear H; invlist f + | H:f _ _ ?l |- _ => is_list_constr l; inversion_clear H; invlist f + | H:f _ _ _ ?l |- _ => is_list_constr l; inversion_clear H; invlist f + | H:f _ _ _ _ ?l |- _ => is_list_constr l; inversion_clear H; invlist f + | _ => idtac + end. + + + +(** * Exporting hints and tactics *) + + +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) *) @@ -1844,11 +1749,36 @@ Hint Rewrite 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 *) + app_nil_r (* l ++ nil = l *) : list. Ltac simpl_list := autorewrite with list. Ltac ssimpl_list := autorewrite with list using simpl. + +(* begin hide *) +(* Compatibility notations after the migration of [list] to [Datatypes] *) +Notation list := list (only parsing). +Notation list_rect := list_rect (only parsing). +Notation list_rec := list_rec (only parsing). +Notation list_ind := list_ind (only parsing). +Notation nil := nil (only parsing). +Notation cons := cons (only parsing). +Notation length := length (only parsing). +Notation app := app (only parsing). +(* Compatibility Names *) +Notation tail := tl (only parsing). +Notation head := hd_error (only parsing). +Notation head_nil := hd_error_nil (only parsing). +Notation head_cons := hd_error_cons (only parsing). +Notation ass_app := app_assoc (only parsing). +Notation app_ass := app_assoc_reverse (only parsing). +Notation In_split := in_split (only parsing). +Notation In_rev := in_rev (only parsing). +Notation In_dec := in_dec (only parsing). +Notation distr_rev := rev_app_distr (only parsing). +Notation rev_acc := rev_append (only parsing). +Notation rev_acc_rev := rev_append_rev (only parsing). +Notation AllS := Forall (only parsing). (* was formerly in TheoryList *) + +Hint Resolve app_nil_end : datatypes v62. +(* end hide *) |