diff options
Diffstat (limited to 'theories/Lists/List.v')
| -rwxr-xr-x | theories/Lists/List.v | 655 |
1 files changed, 655 insertions, 0 deletions
diff --git a/theories/Lists/List.v b/theories/Lists/List.v new file mode 100755 index 00000000..c3f65d67 --- /dev/null +++ b/theories/Lists/List.v @@ -0,0 +1,655 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * 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. + + +Section Lists. + +Variable A : Set. + +Set Implicit Arguments. + +Inductive list : Set := + | nil : list + | cons : A -> list -> list. + +Infix "::" := cons (at level 60, right associativity) : list_scope. + +Open Scope list_scope. + +(*************************) +(** Discrimination *) +(*************************) + +Lemma nil_cons : forall (a:A) (m:list), nil <> a :: m. +Proof. + intros; discriminate. +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 *) +(*************************) + +Definition head (l:list) := + match l with + | nil => error + | x :: _ => value x + end. + +Definition tail (l:list) : list := + 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. + +(******************************) +(** Length order of lists *) +(******************************) + +Section length_order. +Definition lel (l m:list) := length l <= length m. + +Variables a b : A. +Variables l m n : list. + +Lemma lel_refl : lel l l. +Proof. + unfold lel in |- *; auto with arith. +Qed. + +Lemma lel_trans : lel l m -> lel m n -> lel l n. +Proof. + unfold lel in |- *; 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. +Qed. + +Lemma lel_cons : lel l m -> lel l (b :: m). +Proof. + unfold lel in |- *; simpl in |- *; auto with arith. +Qed. + +Lemma lel_tail : lel (a :: l) (b :: m) -> lel l m. +Proof. + unfold lel in |- *; simpl in |- *; auto with arith. +Qed. + +Lemma lel_nil : forall l':list, lel l' nil -> nil = l'. +Proof. + intro l'; elim l'; auto with arith. + intros a' y H H0. + now_show (nil = a' :: y). + absurd (S (length y) <= 0); auto with arith. +Qed. +End length_order. + +Hint Resolve lel_refl lel_cons_cons lel_cons lel_nil lel_nil nil_cons. + +(*********************************) +(** The [In] predicate *) +(*********************************) + +Fixpoint In (a:A) (l:list) {struct l} : Prop := + match l with + | nil => False + | b :: m => b = a \/ In a m + end. + +Lemma in_eq : forall (a:A) (l:list), In a (a :: l). +Proof. + simpl in |- *; auto. +Qed. +Hint Resolve in_eq. + +Lemma in_cons : forall (a b:A) (l:list), In b l -> In b (a :: l). +Proof. + simpl in |- *; auto. +Qed. +Hint Resolve in_cons. + +Lemma in_nil : forall a:A, ~ In a nil. +Proof. + unfold not in |- *; intros a H; inversion_clear H. +Qed. + + +Lemma in_inv : forall (a b:A) (l:list), In b (a :: l) -> a = b \/ In b l. +Proof. + intros a b l H; inversion_clear H; auto. +Qed. + +Lemma In_dec : + (forall x y:A, {x = y} + {x <> y}) -> + forall (a:A) (l:list), {In a l} + {~ In a l}. + +Proof. + 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. +Qed. + +Lemma in_app_or : forall (l m:list) (a:A), In a (l ++ m) -> In a l \/ In a m. +Proof. + intros l m a. + elim l; simpl in |- *; auto. + intros a0 y H H0. + now_show ((a0 = a \/ In a y) \/ In a m). + elim H0; auto. + intro H1. + now_show ((a0 = a \/ In a y) \/ In a m). + elim (H H1); auto. +Qed. +Hint Immediate in_app_or. + +Lemma in_or_app : forall (l m:list) (a:A), In a l \/ In a m -> In a (l ++ m). +Proof. + intros l m a. + elim l; simpl in |- *; intro H. + now_show (In a m). + elim H; auto; intro H0. + now_show (In a m). + elim H0. (* subProof completed *) + intros y H0 H1. + now_show (H = a \/ In a (y ++ m)). + elim H1; auto 4. + intro H2. + now_show (H = a \/ In a (y ++ m)). + elim H2; auto. +Qed. +Hint Resolve in_or_app. + +(***************************) +(** Set inclusion on list *) +(***************************) + +Definition incl (l m:list) := forall a:A, In a l -> In a m. +Hint Unfold incl. + +Lemma incl_refl : forall l:list, incl l l. +Proof. + auto. +Qed. +Hint Resolve incl_refl. + +Lemma incl_tl : forall (a:A) (l m:list), incl l m -> incl l (a :: m). +Proof. + auto. +Qed. +Hint Immediate incl_tl. + +Lemma incl_tran : forall l m n:list, incl l m -> incl m n -> incl l n. +Proof. + auto. +Qed. + +Lemma incl_appl : forall l m n:list, incl l n -> incl l (n ++ m). +Proof. + auto. +Qed. +Hint Immediate incl_appl. + +Lemma incl_appr : forall l m n:list, incl l n -> incl l (m ++ n). +Proof. + auto. +Qed. +Hint Immediate incl_appr. + +Lemma incl_cons : + forall (a:A) (l m:list), In a m -> incl l m -> incl (a :: l) m. +Proof. + unfold incl in |- *; simpl in |- *; intros a l m H H0 a0 H1. + now_show (In a0 m). + elim H1. + now_show (a = a0 -> In a0 m). + elim H1; auto; intro H2. + now_show (a = a0 -> In a0 m). + elim H2; auto. (* solves subgoal *) + now_show (In a0 l -> In a0 m). + auto. +Qed. +Hint Resolve incl_cons. + +Lemma incl_app : forall l m n:list, incl l n -> incl m n -> incl (l ++ m) n. +Proof. + unfold incl in |- *; simpl in |- *; intros l m n H H0 a H1. + now_show (In a n). + elim (in_app_or _ _ _ H1); auto. +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 *) +(********************************) + + +Lemma list_eq_dec : + (forall x y:A, {x = y} + {x <> y}) -> forall x y:list, {x = y} + {x <> y}. +Proof. + induction x as [| a l IHl]; destruct y as [| a0 l0]; auto. + destruct (H a a0) as [e| e]. + destruct (IHl l0) as [e'| e']. + left; rewrite e; rewrite e'; trivial. + right; red in |- *; intro. + apply e'; injection H0; trivial. + right; red in |- *; intro. + apply e; injection H0; trivial. +Qed. + +(*************************) +(** Reverse *) +(*************************) + +Fixpoint rev (l:list) : list := + match l with + | nil => nil + | x :: l' => rev l' ++ x :: nil + end. + +Lemma distr_rev : forall x y:list, rev (x ++ y) = rev y ++ rev x. +Proof. + induction x as [| a l IHl]. + destruct y as [| a l]. + simpl in |- *. + auto. + + simpl in |- *. + apply app_nil_end; auto. + + intro y. + simpl in |- *. + rewrite (IHl y). + apply (app_ass (rev y) (rev l) (a :: nil)). +Qed. + +Remark rev_unit : forall (l:list) (a:A), rev (l ++ a :: nil) = a :: rev l. +Proof. + intros. + apply (distr_rev l (a :: nil)); simpl in |- *; auto. +Qed. + +Lemma rev_involutive : forall l:list, rev (rev l) = l. +Proof. + induction l as [| a l IHl]. + simpl in |- *; auto. + + simpl in |- *. + rewrite (rev_unit (rev l) a). + rewrite IHl; auto. +Qed. + +(*********************************************) +(** Reverse Induction Principle on Lists *) +(*********************************************) + +Section Reverse_Induction. + +Unset Implicit Arguments. + +Remark rev_list_ind : + forall P:list -> Prop, + P nil -> + (forall (a:A) (l:list), P (rev l) -> P (rev (a :: l))) -> + forall l:list, P (rev l). +Proof. + induction l; auto. +Qed. +Set Implicit Arguments. + +Lemma rev_ind : + forall P:list -> Prop, + P nil -> + (forall (x:A) (l:list), P l -> P (l ++ x :: nil)) -> forall l:list, P l. +Proof. + intros. + generalize (rev_involutive l). + intros E; rewrite <- E. + apply (rev_list_ind P). + auto. + + simpl in |- *. + intros. + apply (H0 a (rev l0)). + auto. +Qed. + +End Reverse_Induction. + +End Lists. + +Implicit Arguments nil [A]. + +Hint Resolve nil_cons app_nil_end ass_app app_ass: 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 lel_refl lel_cons_cons lel_cons lel_nil lel_nil nil_cons: + datatypes v62. +Hint Resolve in_eq in_cons in_inv in_nil in_app_or in_or_app: datatypes v62. +Hint Resolve incl_refl incl_tl incl_tran incl_appl incl_appr incl_cons + incl_app: datatypes v62. + +Section Functions_on_lists. + +(****************************************************************) +(** Some generic functions on lists and basic functions of them *) +(****************************************************************) + +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). +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} : + list B := + match l with + | nil => nil + | cons x t => app (f x) (flat_map f t) + end. + +Fixpoint list_prod (A B:Set) (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') + end. + +Lemma in_prod_aux : + forall (A B:Set) (x:A) (y:B) (l:list B), + In y l -> In (x, y) (map (fun y0:B => (x, y0)) l). +Proof. + induction l; + [ simpl in |- *; auto + | simpl in |- *; destruct 1 as [H1| ]; + [ left; rewrite H1; trivial | right; auto ] ]. +Qed. + +Lemma in_prod : + forall (A B:Set) (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; + [ simpl in |- *; tauto + | simpl in |- *; intros; apply in_or_app; destruct H; + [ left; rewrite H; apply in_prod_aux; assumption | right; auto ] ]. +Qed. + +(** [(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} : + list (list (A * B)) := + match l with + | nil => cons nil nil + | cons x t => + flat_map (fun f:list (A * B) => map (fun y:B => cons (x, y) f) l') + (list_power t l') + end. + +(************************************) +(** Left-to-right iterator on lists *) +(************************************) + +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. +End Fold_Left_Recursor. + +(************************************) +(** Right-to-left iterator on lists *) +(************************************) + +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. + +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) -> + (forall x y:A, f x y = f y x) -> + forall (a0:A) (l:list A), fold_left f l a0 = fold_right f a0 l. +Proof. +destruct l as [| a l]. +reflexivity. +simpl in |- *. +rewrite <- H0. +generalize a0 a. +induction l as [| a3 l IHl]; simpl in |- *. +trivial. +intros. +rewrite H. +rewrite (H0 a2). +rewrite <- (H a1). +rewrite (H0 a1). +rewrite IHl. +reflexivity. +Qed. + +End Functions_on_lists. + + +(** Exporting list notations *) + +Infix "::" := cons (at level 60, right associativity) : list_scope. + +Infix "++" := app (right associativity, at level 60) : list_scope. + +Open Scope list_scope. + +(** Declare Scope list_scope with key list *) +Delimit Scope list_scope with list. + +Bind Scope list_scope with list. |