diff options
Diffstat (limited to 'theories/Lists')
| -rw-r--r-- | theories/Lists/List.v | 1202 | ||||
| -rw-r--r-- | theories/Lists/ListSet.v | 53 | ||||
| -rw-r--r-- | theories/Lists/ListTactics.v | 48 | ||||
| -rw-r--r-- | theories/Lists/MonoList.v | 269 | ||||
| -rw-r--r-- | theories/Lists/SetoidList.v | 929 | ||||
| -rw-r--r-- | theories/Lists/StreamMemo.v | 48 | ||||
| -rw-r--r-- | theories/Lists/Streams.v | 8 | ||||
| -rw-r--r-- | theories/Lists/TheoryList.v | 50 | ||||
| -rwxr-xr-x | theories/Lists/intro.tex | 3 | ||||
| -rw-r--r-- | theories/Lists/vo.itarget | 7 |
10 files changed, 1174 insertions, 1443 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 *) diff --git a/theories/Lists/ListSet.v b/theories/Lists/ListSet.v index 021a64c1..20c9e7e8 100644 --- a/theories/Lists/ListSet.v +++ b/theories/Lists/ListSet.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: ListSet.v 10616 2008-03-04 17:33:35Z letouzey $ i*) +(*i $Id$ i*) (** A Library for finite sets, implemented as lists *) @@ -27,7 +27,7 @@ Section first_definitions. Definition empty_set : set := nil. - Fixpoint set_add (a:A) (x:set) {struct x} : set := + Fixpoint set_add (a:A) (x:set) : set := match x with | nil => a :: nil | a1 :: x1 => @@ -38,7 +38,7 @@ Section first_definitions. end. - Fixpoint set_mem (a:A) (x:set) {struct x} : bool := + Fixpoint set_mem (a:A) (x:set) : bool := match x with | nil => false | a1 :: x1 => @@ -47,9 +47,9 @@ Section first_definitions. | right _ => set_mem a x1 end end. - + (** If [a] belongs to [x], removes [a] from [x]. If not, does nothing *) - Fixpoint set_remove (a:A) (x:set) {struct x} : set := + Fixpoint set_remove (a:A) (x:set) : set := match x with | nil => empty_set | a1 :: x1 => @@ -67,20 +67,20 @@ Section first_definitions. if set_mem a1 y then a1 :: set_inter x1 y else set_inter x1 y end. - Fixpoint set_union (x y:set) {struct y} : set := + Fixpoint set_union (x y:set) : set := match y with | nil => x | a1 :: y1 => set_add a1 (set_union x y1) end. - + (** returns the set of all els of [x] that does not belong to [y] *) - Fixpoint set_diff (x y:set) {struct x} : set := + Fixpoint set_diff (x y:set) : set := match x with | nil => nil | a1 :: x1 => if set_mem a1 y then set_diff x1 y else set_add a1 (set_diff x1 y) end. - + Definition set_In : A -> set -> Prop := In (A:=A). @@ -123,7 +123,7 @@ Section first_definitions. case H3; auto. Qed. - + Lemma set_mem_correct1 : forall (a:A) (x:set), set_mem a x = true -> set_In a x. Proof. @@ -191,11 +191,11 @@ Section first_definitions. Lemma set_add_intro : forall (a b:A) (x:set), a = b \/ set_In a x -> set_In a (set_add b x). - + Proof. intros a b x [H1| H2]; auto with datatypes. Qed. - + Lemma set_add_elim : forall (a b:A) (x:set), set_In a (set_add b x) -> a = b \/ set_In a x. @@ -225,7 +225,7 @@ Section first_definitions. simple induction x; simpl in |- *. discriminate. intros; elim (Aeq_dec a a0); intros; discriminate. - Qed. + Qed. Lemma set_union_intro1 : @@ -289,7 +289,7 @@ Section first_definitions. elim (set_mem a y); simpl in |- *; intros. auto with datatypes. absurd (set_In a y); auto with datatypes. - elim (set_mem a0 y); [ right; auto with datatypes | auto with datatypes ]. + elim (set_mem a0 y); [ right; auto with datatypes | auto with datatypes ]. Qed. Lemma set_inter_elim1 : @@ -324,7 +324,7 @@ Section first_definitions. set_In a (set_inter x y) -> set_In a x /\ set_In a y. Proof. eauto with datatypes. - Qed. + Qed. Lemma set_diff_intro : forall (a:A) (x y:set), @@ -354,7 +354,7 @@ Section first_definitions. forall (a:A) (x y:set), set_In a (set_diff x y) -> ~ set_In a y. intros a x y; elim x; simpl in |- *. intros; contradiction. - intros a0 l Hrec. + intros a0 l Hrec. apply set_mem_ind2; auto. intros H1 H2; case (set_add_elim _ _ _ H2); intros; auto. rewrite H; trivial. @@ -373,24 +373,23 @@ End first_definitions. Section other_definitions. - Variables A B : Type. - - Definition set_prod : set A -> set B -> set (A * B) := - list_prod (A:=A) (B:=B). + Definition set_prod : forall {A B:Type}, set A -> set B -> set (A * B) := + list_prod. (** [B^A], set of applications from [A] to [B] *) - Definition set_power : set A -> set B -> set (set (A * B)) := - list_power (A:=A) (B:=B). + Definition set_power : forall {A B:Type}, set A -> set B -> set (set (A * B)) := + list_power. - Definition set_map : (A -> B) -> set A -> set B := map (A:=A) (B:=B). - - Definition set_fold_left : (B -> A -> B) -> set A -> B -> B := + Definition set_fold_left {A B:Type} : (B -> A -> B) -> set A -> B -> B := fold_left (A:=B) (B:=A). - Definition set_fold_right (f:A -> B -> B) (x:set A) + Definition set_fold_right {A B:Type} (f:A -> B -> B) (x:set A) (b:B) : B := fold_right f b x. - + Definition set_map {A B:Type} (Aeq_dec : forall x y:B, {x = y} + {x <> y}) + (f : A -> B) (x : set A) : set B := + set_fold_right (fun a => set_add Aeq_dec (f a)) x (empty_set B). + End other_definitions. Unset Implicit Arguments. diff --git a/theories/Lists/ListTactics.v b/theories/Lists/ListTactics.v index 515ed138..0a21a9e2 100644 --- a/theories/Lists/ListTactics.v +++ b/theories/Lists/ListTactics.v @@ -6,40 +6,44 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: ListTactics.v 9427 2006-12-11 18:46:35Z bgregoir $ i*) +(*i $Id$ i*) Require Import BinPos. Require Import List. Ltac list_fold_right fcons fnil l := match l with - | (cons ?x ?tl) => fcons x ltac:(list_fold_right fcons fnil tl) + | ?x :: ?tl => fcons x ltac:(list_fold_right fcons fnil tl) | nil => fnil end. +(* A variant of list_fold_right, to prevent the match of list_fold_right + from catching errors raised by fcons. *) Ltac lazy_list_fold_right fcons fnil l := - match l with - | (cons ?x ?tl) => - let cont := lazy_list_fold_right fcons fnil in - fcons x cont tl - | nil => fnil - end. + let f := + match l with + | ?x :: ?tl => + fun _ => + fcons x ltac:(fun _ => lazy_list_fold_right fcons fnil tl) + | nil => fun _ => fnil() + end in + f(). Ltac list_fold_left fcons fnil l := match l with - | (cons ?x ?tl) => list_fold_left fcons ltac:(fcons x fnil) tl + | ?x :: ?tl => list_fold_left fcons ltac:(fcons x fnil) tl | nil => fnil end. Ltac list_iter f l := match l with - | (cons ?x ?tl) => f x; list_iter f tl + | ?x :: ?tl => f x; list_iter f tl | nil => idtac end. Ltac list_iter_gen seq f l := match l with - | (cons ?x ?tl) => + | ?x :: ?tl => let t1 _ := f x in let t2 _ := list_iter_gen seq f tl in seq t1 t2 @@ -48,30 +52,30 @@ Ltac list_iter_gen seq f l := Ltac AddFvTail a l := match l with - | nil => constr:(cons a l) - | (cons a _) => l - | (cons ?x ?l) => let l' := AddFvTail a l in constr:(cons x l') + | nil => constr:(a::nil) + | a :: _ => l + | ?x :: ?l => let l' := AddFvTail a l in constr:(x::l') end. Ltac Find_at a l := let rec find n l := match l with - | nil => fail 100 "anomaly: Find_at" - | (cons a _) => eval compute in n - | (cons _ ?l) => find (Psucc n) l + | nil => fail 100 "anomaly: Find_at" + | a :: _ => eval compute in n + | _ :: ?l => find (Psucc n) l end in find 1%positive l. Ltac check_is_list t := match t with - | cons _ ?l => check_is_list l - | nil => idtac - | _ => fail 100 "anomaly: failed to build a canonical list" + | _ :: ?l => check_is_list l + | nil => idtac + | _ => fail 100 "anomaly: failed to build a canonical list" end. Ltac check_fv l := check_is_list l; - match type of l with + match type of l with | list _ => idtac - | _ => fail 100 "anomaly: built an ill-typed list" + | _ => fail 100 "anomaly: built an ill-typed list" end. diff --git a/theories/Lists/MonoList.v b/theories/Lists/MonoList.v deleted file mode 100644 index aa2b74dd..00000000 --- a/theories/Lists/MonoList.v +++ /dev/null @@ -1,269 +0,0 @@ -(************************************************************************) -(* 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: MonoList.v 8642 2006-03-17 10:09:02Z notin $ i*) - -(** THIS IS A OLD CONTRIB. IT IS NO LONGER MAINTAINED ***) - -Require Import Le. - -Parameter List_Dom : Set. -Definition A := List_Dom. - -Inductive list : Set := - | nil : list - | cons : A -> list -> list. - -Fixpoint app (l m:list) {struct l} : list := - match l return list with - | nil => m - | cons a l1 => cons a (app l1 m) - end. - - -Lemma app_nil_end : forall l:list, l = app l nil. -Proof. - intro l; elim l; simpl in |- *; auto. - simple induction 1; auto. -Qed. -Hint Resolve app_nil_end: list v62. - -Lemma app_ass : forall l m n:list, app (app l m) n = app l (app m n). -Proof. - intros l m n; elim l; simpl in |- *; auto with list. - simple induction 1; auto with list. -Qed. -Hint Resolve app_ass: list v62. - -Lemma ass_app : forall l m n:list, app l (app m n) = app (app l m) n. -Proof. - auto with list. -Qed. -Hint Resolve ass_app: list v62. - -Definition tail (l:list) : list := - match l return list with - | cons _ m => m - | _ => nil - end. - - -Lemma nil_cons : forall (a:A) (m:list), nil <> cons a m. - intros; discriminate. -Qed. - -(****************************************) -(* Length of lists *) -(****************************************) - -Fixpoint length (l:list) : nat := - match l return nat with - | cons _ m => S (length m) - | _ => 0 - end. - -(******************************) -(* Length order of lists *) -(******************************) - -Section length_order. -Definition lel (l m:list) := length l <= length m. - -Hint Unfold lel: list. - -Variables a b : A. -Variables l m n : list. - -Lemma lel_refl : lel l l. -Proof. - unfold lel in |- *; auto with list. -Qed. - -Lemma lel_trans : lel l m -> lel m n -> lel l n. -Proof. - unfold lel in |- *; intros. - apply le_trans with (length m); auto with list. -Qed. - -Lemma lel_cons_cons : lel l m -> lel (cons a l) (cons b m). -Proof. - unfold lel in |- *; simpl in |- *; auto with list arith. -Qed. - -Lemma lel_cons : lel l m -> lel l (cons b m). -Proof. - unfold lel in |- *; simpl in |- *; auto with list arith. -Qed. - -Lemma lel_tail : lel (cons a l) (cons b m) -> lel l m. -Proof. - unfold lel in |- *; simpl in |- *; auto with list arith. -Qed. - -Lemma lel_nil : forall l':list, lel l' nil -> nil = l'. -Proof. - intro l'; elim l'; auto with list arith. - intros a' y H H0. - (* <list>nil=(cons a' y) - ============================ - H0 : (lel (cons a' y) nil) - H : (lel y nil)->(<list>nil=y) - y : list - a' : A - l' : list *) - absurd (S (length y) <= 0); auto with list arith. -Qed. -End length_order. - -Hint Resolve lel_refl lel_cons_cons lel_cons lel_nil lel_nil nil_cons: list - v62. - -Fixpoint In (a:A) (l:list) {struct l} : Prop := - match l with - | nil => False - | cons b m => b = a \/ In a m - end. - -Lemma in_eq : forall (a:A) (l:list), In a (cons a l). -Proof. - simpl in |- *; auto with list. -Qed. -Hint Resolve in_eq: list v62. - -Lemma in_cons : forall (a b:A) (l:list), In b l -> In b (cons a l). -Proof. - simpl in |- *; auto with list. -Qed. -Hint Resolve in_cons: list v62. - -Lemma in_app_or : forall (l m:list) (a:A), In a (app l m) -> In a l \/ In a m. -Proof. - intros l m a. - elim l; simpl in |- *; auto with list. - intros a0 y H H0. - (* ((<A>a0=a)\/(In a y))\/(In a m) - ============================ - H0 : (<A>a0=a)\/(In a (app y m)) - H : (In a (app y m))->((In a y)\/(In a m)) - y : list - a0 : A - a : A - m : list - l : list *) - elim H0; auto with list. - intro H1. - (* ((<A>a0=a)\/(In a y))\/(In a m) - ============================ - H1 : (In a (app y m)) *) - elim (H H1); auto with list. -Qed. -Hint Immediate in_app_or: list v62. - -Lemma in_or_app : forall (l m:list) (a:A), In a l \/ In a m -> In a (app l m). -Proof. - intros l m a. - elim l; simpl in |- *; intro H. - (* 1 (In a m) - ============================ - H : False\/(In a m) - a : A - m : list - l : list *) - elim H; auto with list; intro H0. - (* (In a m) - ============================ - H0 : False *) - elim H0. (* subProof completed *) - intros y H0 H1. - (* 2 (<A>H=a)\/(In a (app y m)) - ============================ - H1 : ((<A>H=a)\/(In a y))\/(In a m) - H0 : ((In a y)\/(In a m))->(In a (app y m)) - y : list *) - elim H1; auto 4 with list. - intro H2. - (* (<A>H=a)\/(In a (app y m)) - ============================ - H2 : (<A>H=a)\/(In a y) *) - elim H2; auto with list. -Qed. -Hint Resolve in_or_app: list v62. - -Definition incl (l m:list) := forall a:A, In a l -> In a m. - -Hint Unfold incl: list v62. - -Lemma incl_refl : forall l:list, incl l l. -Proof. - auto with list. -Qed. -Hint Resolve incl_refl: list v62. - -Lemma incl_tl : forall (a:A) (l m:list), incl l m -> incl l (cons a m). -Proof. - auto with list. -Qed. -Hint Immediate incl_tl: list v62. - -Lemma incl_tran : forall l m n:list, incl l m -> incl m n -> incl l n. -Proof. - auto with list. -Qed. - -Lemma incl_appl : forall l m n:list, incl l n -> incl l (app n m). -Proof. - auto with list. -Qed. -Hint Immediate incl_appl: list v62. - -Lemma incl_appr : forall l m n:list, incl l n -> incl l (app m n). -Proof. - auto with list. -Qed. -Hint Immediate incl_appr: list v62. - -Lemma incl_cons : - forall (a:A) (l m:list), In a m -> incl l m -> incl (cons a l) m. -Proof. - unfold incl in |- *; simpl in |- *; intros a l m H H0 a0 H1. - (* (In a0 m) - ============================ - H1 : (<A>a=a0)\/(In a0 l) - a0 : A - H0 : (a:A)(In a l)->(In a m) - H : (In a m) - m : list - l : list - a : A *) - elim H1. - (* 1 (<A>a=a0)->(In a0 m) *) - elim H1; auto with list; intro H2. - (* (<A>a=a0)->(In a0 m) - ============================ - H2 : <A>a=a0 *) - elim H2; auto with list. (* solves subgoal *) - (* 2 (In a0 l)->(In a0 m) *) - auto with list. -Qed. -Hint Resolve incl_cons: list v62. - -Lemma incl_app : forall l m n:list, incl l n -> incl m n -> incl (app l m) n. -Proof. - unfold incl in |- *; simpl in |- *; intros l m n H H0 a H1. - (* (In a n) - ============================ - H1 : (In a (app l m)) - a : A - H0 : (a:A)(In a m)->(In a n) - H : (a:A)(In a l)->(In a n) - n : list - m : list - l : list *) - elim (in_app_or l m a); auto with list. -Qed. -Hint Resolve incl_app: list v62.
\ No newline at end of file diff --git a/theories/Lists/SetoidList.v b/theories/Lists/SetoidList.v index 2592abb5..d42e71e5 100644 --- a/theories/Lists/SetoidList.v +++ b/theories/Lists/SetoidList.v @@ -6,23 +6,23 @@ (* * GNU Lesser General Public License Version 2.1 *) (***********************************************************************) -(* $Id: SetoidList.v 11800 2009-01-18 18:34:15Z msozeau $ *) +(* $Id$ *) Require Export List. Require Export Sorting. -Require Export Setoid. +Require Export Setoid Basics Morphisms. Set Implicit Arguments. Unset Strict Implicit. -(** * Logical relations over lists with respect to a setoid equality - or ordering. *) +(** * Logical relations over lists with respect to a setoid equality + or ordering. *) -(** This can be seen as a complement of predicate [lelistA] and [sort] +(** This can be seen as a complement of predicate [lelistA] and [sort] found in [Sorting]. *) Section Type_with_equality. Variable A : Type. -Variable eqA : A -> A -> Prop. +Variable eqA : A -> A -> Prop. (** Being in a list modulo an equality relation over type [A]. *) @@ -32,27 +32,28 @@ Inductive InA (x : A) : list A -> Prop := Hint Constructors InA. +(** TODO: it would be nice to have a generic definition instead + of the previous one. Having [InA = Exists eqA] raises too + many compatibility issues. For now, we only state the equivalence: *) + +Lemma InA_altdef : forall x l, InA x l <-> Exists (eqA x) l. +Proof. split; induction 1; auto. Qed. + Lemma InA_cons : forall x y l, InA x (y::l) <-> eqA x y \/ InA x l. Proof. - intuition. - inversion H; auto. + intuition. invlist InA; auto. Qed. Lemma InA_nil : forall x, InA x nil <-> False. Proof. - intuition. - inversion H. + intuition. invlist InA. Qed. (** 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. +Proof. + intros; rewrite InA_altdef, Exists_exists; firstorder. Qed. (** A list without redundancy modulo the equality over [A]. *) @@ -63,8 +64,22 @@ Inductive NoDupA : list A -> Prop := Hint Constructors NoDupA. +(** An alternative definition of [NoDupA] based on [ForallOrdPairs] *) + +Lemma NoDupA_altdef : forall l, + NoDupA l <-> ForallOrdPairs (complement eqA) l. +Proof. + split; induction 1; constructor; auto. + rewrite Forall_forall. intros b Hb. + intro Eq; elim H. rewrite InA_alt. exists b; auto. + rewrite InA_alt; intros (a' & Haa' & Ha'). + rewrite Forall_forall in H. exact (H a' Ha' Haa'). +Qed. + + (** lists with same elements modulo [eqA] *) +Definition inclA l l' := forall x, InA x l -> InA x l'. Definition equivlistA l l' := forall x, InA x l <-> InA x l'. (** lists with same elements modulo [eqA] at the same place *) @@ -76,48 +91,78 @@ Inductive eqlistA : list A -> list A -> Prop := Hint Constructors eqlistA. -(** Compatibility of a boolean function with respect to an equality. *) +(** We could also have written [eqlistA = Forall2 eqA]. *) -Definition compat_bool (f : A->bool) := forall x y, eqA x y -> f x = f y. +Lemma eqlistA_altdef : forall l l', eqlistA l l' <-> Forall2 eqA l l'. +Proof. split; induction 1; auto. Qed. -(** Compatibility of a function upon natural numbers. *) +(** Results concerning lists modulo [eqA] *) -Definition compat_nat (f : A->nat) := forall x y, eqA x y -> f x = f y. +Hypothesis eqA_equiv : Equivalence eqA. -(** Compatibility of a predicate with respect to an equality. *) +Hint Resolve (@Equivalence_Reflexive _ _ eqA_equiv). +Hint Resolve (@Equivalence_Transitive _ _ eqA_equiv). +Hint Immediate (@Equivalence_Symmetric _ _ eqA_equiv). -Definition compat_P (P : A->Prop) := forall x y, eqA x y -> P x -> P y. +Ltac inv := invlist InA; invlist sort; invlist lelistA; invlist NoDupA. -(** Results concerning lists modulo [eqA] *) +(** First, the two notions [equivlistA] and [eqlistA] are indeed equivlances *) -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. +Global Instance equivlist_equiv : Equivalence equivlistA. +Proof. + firstorder. +Qed. + +Global Instance eqlistA_equiv : Equivalence eqlistA. +Proof. + constructor; red. + induction x; auto. + induction 1; auto. + intros x y z H; revert z; induction H; auto. + inversion 1; subst; auto. invlist eqlistA; eauto with *. +Qed. + +(** Moreover, [eqlistA] implies [equivlistA]. A reverse result + will be proved later for sorted list without duplicates. *) + +Global Instance eqlistA_equivlistA : subrelation eqlistA equivlistA. +Proof. + intros x x' H. induction H. + intuition. + red; intros. + rewrite 2 InA_cons. + rewrite (IHeqlistA x0), H; intuition. +Qed. + +(** InA is compatible with eqA (for its first arg) and with + equivlistA (and hence eqlistA) for its second arg *) + +Global Instance InA_compat : Proper (eqA==>equivlistA==>iff) InA. +Proof. + intros x x' Hxx' l l' Hll'. rewrite (Hll' x). + rewrite 2 InA_alt; firstorder. +Qed. -Hint Resolve eqA_refl eqA_trans. -Hint Immediate eqA_sym. +(** For compatibility, an immediate consequence of [InA_compat] *) 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. +Proof. + intros l x y H H'. rewrite <- H; auto. 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. + simple induction l; simpl; intuition. + subst; auto. Qed. Hint Resolve In_InA. -Lemma InA_split : forall l x, InA x l -> - exists l1, exists y, exists l2, +Lemma InA_split : forall l x, InA x l -> + exists l1, exists y, exists l2, eqA x y /\ l = l1++y::l2. Proof. -induction l; inversion_clear 1. +induction l; intros; inv. exists (@nil A); exists a; exists l; auto. destruct (IHl x H0) as (l1,(y,(l2,(H1,H2)))). exists (a::l1); exists y; exists l2; auto. @@ -128,7 +173,7 @@ 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. + inv; auto. elim (IHl1 l2 x H0); auto. Qed. @@ -144,7 +189,7 @@ Proof. apply in_or_app; auto. Qed. -Lemma InA_rev : forall p m, +Lemma InA_rev : forall p m, InA p (rev m) <-> InA p m. Proof. intros; do 2 rewrite InA_alt. @@ -153,107 +198,16 @@ Proof. rewrite <- In_rev; auto. Qed. -(** 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). - -Hint Constructors lelistA sort. - -Lemma InfA_ltA : - forall l x y, ltA x y -> InfA y l -> InfA x l. -Proof. - destruct l; 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 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 NoDupA. -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) -> +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. +inv. constructor. rewrite InA_alt; intros (y,(H4,H5)). destruct (in_app_or _ _ _ H5). @@ -274,35 +228,36 @@ Proof. induction l. simpl; auto. simpl; intros. -inversion_clear H. +inv. apply NoDupA_app; auto. constructor; auto. -intro H2; inversion H2. +intro; inv. intros x. rewrite InA_alt. intros (x1,(H2,H3)). -inversion_clear 1. +intro; inv. destruct H0. -apply InA_eqA with x1; eauto. +rewrite <- H4, H2. apply In_InA. rewrite In_rev; auto. -inversion H4. Qed. Lemma NoDupA_split : forall l l' x, NoDupA (l++x::l') -> NoDupA (l++l'). Proof. - induction l; simpl in *; inversion_clear 1; auto. + induction l; simpl in *; intros; inv; auto. constructor; eauto. contradict H0. - rewrite InA_app_iff in *; rewrite InA_cons; intuition. + rewrite InA_app_iff in *. + rewrite InA_cons. + intuition. Qed. Lemma NoDupA_swap : forall l l' x, NoDupA (l++x::l') -> NoDupA (x::l++l'). Proof. - induction l; simpl in *; inversion_clear 1; auto. + induction l; simpl in *; intros; inv; auto. constructor; eauto. assert (H2:=IHl _ _ H1). - inversion_clear H2. + inv. rewrite InA_cons. red; destruct 1. apply H0. @@ -314,287 +269,130 @@ Proof. eapply NoDupA_split; eauto. Qed. -End NoDupA. - -(** Some results about [eqlistA] *) - -Section EqlistA. - -Lemma eqlistA_length : forall l l', eqlistA l l' -> length l = length l'. -Proof. -induction 1; auto; simpl; congruence. -Qed. - -Lemma eqlistA_app : forall l1 l1' l2 l2', - eqlistA l1 l1' -> eqlistA l2 l2' -> eqlistA (l1++l2) (l1'++l2'). -Proof. -intros l1 l1' l2 l2' H; revert l2 l2'; induction H; simpl; auto. -Qed. - -Lemma eqlistA_rev_app : forall l1 l1', - eqlistA l1 l1' -> forall l2 l2', eqlistA l2 l2' -> - eqlistA ((rev l1)++l2) ((rev l1')++l2'). -Proof. -induction 1; auto. -simpl; intros. -do 2 rewrite app_ass; simpl; auto. -Qed. - -Lemma eqlistA_rev : forall l1 l1', - eqlistA l1 l1' -> eqlistA (rev l1) (rev l1'). -Proof. -intros. -rewrite (app_nil_end (rev l1)). -rewrite (app_nil_end (rev l1')). -apply eqlistA_rev_app; auto. -Qed. - -Lemma SortA_equivlistA_eqlistA : forall l l', - SortA l -> SortA l' -> equivlistA l l' -> eqlistA l l'. -Proof. -induction l; destruct l'; simpl; intros; auto. -destruct (H1 a); assert (H4 : InA a nil) by auto; inversion H4. -destruct (H1 a); assert (H4 : InA a nil) by auto; inversion H4. -inversion_clear H; inversion_clear H0. -assert (forall y, InA y l -> ltA a y). -intros; eapply SortA_InfA_InA with (l:=l); eauto. -assert (forall y, InA y l' -> ltA a0 y). -intros; eapply SortA_InfA_InA with (l:=l'); eauto. -clear H3 H4. -assert (eqA a a0). - destruct (H1 a). - destruct (H1 a0). - assert (InA a (a0::l')) by auto. - inversion_clear H8; auto. - assert (InA a0 (a::l)) by auto. - inversion_clear H8; auto. - elim (@ltA_not_eqA a a); auto. - apply ltA_trans with a0; auto. -constructor; auto. -apply IHl; auto. -split; intros. -destruct (H1 x). -assert (H8 : InA x (a0::l')) by auto; inversion_clear H8; auto. -elim (@ltA_not_eqA a x); eauto. -destruct (H1 x). -assert (H8 : InA x (a::l)) by auto; inversion_clear H8; auto. -elim (@ltA_not_eqA a0 x); eauto. -Qed. - -End EqlistA. - -(** A few things about [filter] *) - -Section Filter. - -Lemma filter_sort : forall f l, SortA l -> SortA (List.filter f l). +Lemma equivlistA_NoDupA_split : forall l l1 l2 x y, eqA x y -> + NoDupA (x::l) -> NoDupA (l1++y::l2) -> + equivlistA (x::l) (l1++y::l2) -> equivlistA l (l1++l2). Proof. -induction l; simpl; auto. -inversion_clear 1; auto. -destruct (f a); auto. -constructor; auto. -apply In_InfA; auto. -intros. -rewrite filter_In in H; destruct H. -eapply SortA_InfA_InA; eauto. + intros; intro a. + generalize (H2 a). + rewrite !InA_app_iff, !InA_cons. + inv. + assert (SW:=NoDupA_swap H1). inv. + rewrite InA_app_iff in H0. + split; intros. + assert (~eqA a x) by (contradict H3; rewrite <- H3; auto). + assert (~eqA a y) by (rewrite <- H; auto). + tauto. + assert (OR : eqA a x \/ InA a l) by intuition. clear H6. + destruct OR as [EQN|INA]; auto. + elim H0. + rewrite <-H,<-EQN; auto. Qed. -Lemma filter_InA : forall f, (compat_bool f) -> - forall l x, InA x (List.filter f l) <-> InA x l /\ f x = true. -Proof. -intros; do 2 rewrite InA_alt; intuition. -destruct H0 as (y,(H0,H1)); rewrite filter_In in H1; exists y; intuition. -destruct H0 as (y,(H0,H1)); rewrite filter_In in H1; intuition. - rewrite (H _ _ H0); auto. -destruct H1 as (y,(H0,H1)); exists y; rewrite filter_In; intuition. - rewrite <- (H _ _ H0); auto. -Qed. +End NoDupA. -Lemma filter_split : - forall f, (forall x y, f x = true -> f y = false -> ltA x y) -> - forall l, SortA l -> l = filter f l ++ filter (fun x=>negb (f x)) l. -Proof. -induction l; simpl; intros; auto. -inversion_clear H0. -pattern l at 1; rewrite IHl; auto. -case_eq (f a); simpl; intros; auto. -assert (forall e, In e l -> f e = false). - intros. - assert (H4:=SortA_InfA_InA H1 H2 (In_InA H3)). - case_eq (f e); simpl; intros; auto. - elim (@ltA_not_eqA e e); auto. - apply ltA_trans with a; eauto. -replace (List.filter f l) with (@nil A); auto. -generalize H3; clear; induction l; simpl; auto. -case_eq (f a); auto; intros. -rewrite H3 in H; auto; try discriminate. -Qed. -End Filter. Section Fold. Variable B:Type. Variable eqB:B->B->Prop. - -(** Compatibility of a two-argument function with respect to two equalities. *) -Definition compat_op (f : A -> B -> B) := - forall (x x' : A) (y y' : B), eqA x x' -> eqB y y' -> eqB (f x y) (f x' y'). - -(** Two-argument functions that allow to reorder their arguments. *) -Definition transpose (f : A -> B -> B) := - forall (x y : A) (z : B), eqB (f x (f y z)) (f y (f x z)). - -(** A version of transpose with restriction on where it should hold *) -Definition transpose_restr (R : A -> A -> Prop)(f : A -> B -> B) := - forall (x y : A) (z : B), R x y -> eqB (f x (f y z)) (f y (f x z)). - Variable st:Equivalence eqB. Variable f:A->B->B. Variable i:B. -Variable Comp:compat_op f. +Variable Comp:Proper (eqA==>eqB==>eqB) f. -Lemma fold_right_eqlistA : - forall s s', eqlistA s s' -> +Lemma fold_right_eqlistA : + forall s s', eqlistA s s' -> eqB (fold_right f i s) (fold_right f i s'). Proof. -induction 1; simpl; auto. -reflexivity. -Qed. - -Lemma equivlistA_NoDupA_split : forall l l1 l2 x y, eqA x y -> - NoDupA (x::l) -> NoDupA (l1++y::l2) -> - equivlistA (x::l) (l1++y::l2) -> equivlistA l (l1++l2). -Proof. - intros; intro a. - generalize (H2 a). - repeat rewrite InA_app_iff. - do 2 rewrite InA_cons. - inversion_clear H0. - assert (SW:=NoDupA_swap H1). - inversion_clear SW. - rewrite InA_app_iff in H0. - split; intros. - assert (~eqA a x). - contradict H3; apply InA_eqA with a; auto. - assert (~eqA a y). - contradict H8; eauto. - intuition. - assert (eqA a x \/ InA a l) by intuition. - destruct H8; auto. - elim H0. - destruct H7; [left|right]; eapply InA_eqA; eauto. +induction 1; simpl; auto with relations. +apply Comp; auto. Qed. -(** [ForallList2] : specifies that a certain binary predicate should - always hold when inspecting two different elements of the list. *) - -Inductive ForallList2 (R : A -> A -> Prop) : list A -> Prop := - | ForallNil : ForallList2 R nil - | ForallCons : forall a l, - (forall b, In b l -> R a b) -> - ForallList2 R l -> ForallList2 R (a::l). -Hint Constructors ForallList2. +(** Fold with restricted [transpose] hypothesis. *) -(** [NoDupA] can be written in terms of [ForallList2] *) - -Lemma ForallList2_NoDupA : forall l, - ForallList2 (fun a b => ~eqA a b) l <-> NoDupA l. -Proof. - induction l; split; intros; auto. - inversion_clear H. constructor; [ | rewrite <- IHl; auto ]. - rewrite InA_alt; intros (a',(Haa',Ha')). - exact (H0 a' Ha' Haa'). - inversion_clear H. constructor; [ | rewrite IHl; auto ]. - intros b Hb. - contradict H0. - rewrite InA_alt; exists b; auto. -Qed. +Section Fold_With_Restriction. +Variable R : A -> A -> Prop. +Hypothesis R_sym : Symmetric R. +Hypothesis R_compat : Proper (eqA==>eqA==>iff) R. -Lemma ForallList2_impl : forall (R R':A->A->Prop), - (forall a b, R a b -> R' a b) -> - forall l, ForallList2 R l -> ForallList2 R' l. -Proof. - induction 2; auto. -Qed. -(** The following definition is easier to use than [ForallList2]. *) +(* -Definition ForallList2_alt (R:A->A->Prop) l := - forall a b, InA a l -> InA b l -> ~eqA a b -> R a b. +(** [ForallOrdPairs R] is compatible with [equivlistA] over the + lists without duplicates, as long as the relation [R] + is symmetric and compatible with [eqA]. To prove this fact, + we use an auxiliary notion: "forall distinct pairs, ...". +*) -Section Restriction. -Variable R : A -> A -> Prop. +Definition ForallNeqPairs := + ForallPairs (fun a b => ~eqA a b -> R a b). -(** [ForallList2] and [ForallList2_alt] are related, but no completely +(** [ForallOrdPairs] and [ForallNeqPairs] are related, but not completely equivalent. For proving one implication, we need to know that the list has no duplicated elements... *) -Lemma ForallList2_equiv1 : forall l, NoDupA l -> - ForallList2_alt R l -> ForallList2 R l. +Lemma ForallNeqPairs_ForallOrdPairs : forall l, NoDupA l -> + ForallNeqPairs l -> ForallOrdPairs R l. Proof. induction l; auto. - constructor. intros b Hb. - inversion_clear H. - apply H0; auto. - contradict H1. - apply InA_eqA with b; auto. + constructor. inv. + rewrite Forall_forall; intros b Hb. + apply H0; simpl; auto. + contradict H1; rewrite H1; auto. apply IHl. - inversion_clear H; auto. + inv; auto. intros b c Hb Hc Hneq. - apply H0; auto. + apply H0; simpl; auto. Qed. (** ... and for proving the other implication, we need to be able - to reverse and adapt relation [R] modulo [eqA]. *) - -Hypothesis R_sym : forall a b, R a b -> R b a. -Hypothesis R_compat : forall a, compat_P (R a). + to reverse relation [R]. *) -Lemma ForallList2_equiv2 : forall l, - ForallList2 R l -> ForallList2_alt R l. +Lemma ForallOrdPairs_ForallNeqPairs : forall l, + ForallOrdPairs R l -> ForallNeqPairs l. Proof. - induction l. - intros _. red. intros a b Ha. inversion Ha. - inversion_clear 1 as [|? ? H_R Hl]. - intros b c Hb Hc Hneq. - inversion_clear Hb; inversion_clear Hc. - (* b,c = a : impossible *) - elim Hneq; eauto. - (* b = a, c in l *) - rewrite InA_alt in H0; destruct H0 as (d,(Hcd,Hd)). - apply R_compat with d; auto. - apply R_sym; apply R_compat with a; auto. - (* b in l, c = a *) - rewrite InA_alt in H; destruct H as (d,(Hcd,Hd)). - apply R_compat with a; auto. - apply R_sym; apply R_compat with d; auto. - (* b,c in l *) - apply (IHl Hl); auto. + intros l Hl x y Hx Hy N. + destruct (ForallOrdPairs_In Hl x y Hx Hy) as [H|[H|H]]. + subst; elim N; auto. + assumption. + apply R_sym; assumption. Qed. -Lemma ForallList2_equiv : forall l, NoDupA l -> - (ForallList2 R l <-> ForallList2_alt R l). -Proof. -split; [apply ForallList2_equiv2|apply ForallList2_equiv1]; auto. -Qed. +*) + +(** Compatibility of [ForallOrdPairs] with respect to [inclA]. *) -Lemma ForallList2_equivlistA : forall l l', NoDupA l' -> - equivlistA l l' -> ForallList2 R l -> ForallList2 R l'. +Lemma ForallOrdPairs_inclA : forall l l', + NoDupA l' -> inclA l' l -> ForallOrdPairs R l -> ForallOrdPairs R l'. Proof. -intros. -apply ForallList2_equiv1; auto. -intros a b Ha Hb Hneq. -red in H0; rewrite <- H0 in Ha,Hb. -revert a b Ha Hb Hneq. -change (ForallList2_alt R l). -apply ForallList2_equiv2; auto. +induction l' as [|x l' IH]. +constructor. +intros ND Incl FOP. apply FOP_cons; inv; unfold inclA in *; auto. +rewrite Forall_forall; intros y Hy. +assert (Ix : InA x (x::l')) by (rewrite InA_cons; auto). + apply Incl in Ix. rewrite InA_alt in Ix. destruct Ix as (x' & Hxx' & Hx'). +assert (Iy : InA y (x::l')) by (apply In_InA; simpl; auto). + apply Incl in Iy. rewrite InA_alt in Iy. destruct Iy as (y' & Hyy' & Hy'). +rewrite Hxx', Hyy'. +destruct (ForallOrdPairs_In FOP x' y' Hx' Hy') as [E|[?|?]]; auto. +absurd (InA x l'); auto. rewrite Hxx', E, <- Hyy'; auto. Qed. + +(** Two-argument functions that allow to reorder their arguments. *) +Definition transpose (f : A -> B -> B) := + forall (x y : A) (z : B), eqB (f x (f y z)) (f y (f x z)). + +(** A version of transpose with restriction on where it should hold *) +Definition transpose_restr (R : A -> A -> Prop)(f : A -> B -> B) := + forall (x y : A) (z : B), R x y -> eqB (f x (f y z)) (f y (f x z)). + Variable TraR :transpose_restr R f. Lemma fold_right_commutes_restr : - forall s1 s2 x, ForallList2 R (s1++x::s2) -> + forall s1 s2 x, ForallOrdPairs R (s1++x::s2) -> eqB (fold_right f i (s1++x::s2)) (f x (fold_right f i (s1++s2))). Proof. induction s1; simpl; auto; intros. @@ -602,15 +400,15 @@ reflexivity. transitivity (f a (f x (fold_right f i (s1++s2)))). apply Comp; auto. apply IHs1. -inversion_clear H; auto. +invlist ForallOrdPairs; auto. apply TraR. -inversion_clear H. -apply H0. +invlist ForallOrdPairs; auto. +rewrite Forall_forall in H0; apply H0. apply in_or_app; simpl; auto. Qed. Lemma fold_right_equivlistA_restr : - forall s s', NoDupA s -> NoDupA s' -> ForallList2 R s -> + forall s s', NoDupA s -> NoDupA s' -> ForallOrdPairs R s -> equivlistA s s' -> eqB (fold_right f i s) (fold_right f i s'). Proof. simple induction s. @@ -618,35 +416,35 @@ Proof. intros; reflexivity. unfold equivlistA; intros. destruct (H2 a). - assert (X : InA a nil); auto; inversion X. + assert (InA a nil) by auto; inv. intros x l Hrec s' N N' F E; simpl in *. - assert (InA x s'). - rewrite <- (E x); auto. + assert (InA x s') by (rewrite <- (E x); auto). destruct (InA_split H) as (s1,(y,(s2,(H1,H2)))). subst s'. transitivity (f x (fold_right f i (s1++s2))). apply Comp; auto. apply Hrec; auto. - inversion_clear N; auto. + inv; auto. eapply NoDupA_split; eauto. - inversion_clear F; auto. + invlist ForallOrdPairs; auto. eapply equivlistA_NoDupA_split; eauto. transitivity (f y (fold_right f i (s1++s2))). apply Comp; auto. reflexivity. symmetry; apply fold_right_commutes_restr. - apply ForallList2_equivlistA with (x::l); auto. + apply ForallOrdPairs_inclA with (x::l); auto. + red; intros; rewrite E; auto. Qed. Lemma fold_right_add_restr : - forall s' s x, NoDupA s -> NoDupA s' -> ForallList2 R s' -> ~ InA x s -> + forall s' s x, NoDupA s -> NoDupA s' -> ForallOrdPairs R s' -> ~ InA x s -> equivlistA s' (x::s) -> eqB (fold_right f i s') (f x (fold_right f i s)). Proof. intros; apply (@fold_right_equivlistA_restr s' (x::s)); auto. Qed. -End Restriction. +End Fold_With_Restriction. -(** we know state similar results, but without restriction on transpose. *) +(** we now state similar results, but without restriction on transpose. *) Variable Tra :transpose f. @@ -656,6 +454,7 @@ Proof. induction s1; simpl; auto; intros. reflexivity. transitivity (f a (f x (fold_right f i (s1++s2)))); auto. +apply Comp; auto. Qed. Lemma fold_right_equivlistA : @@ -663,8 +462,8 @@ Lemma fold_right_equivlistA : equivlistA s s' -> eqB (fold_right f i s) (fold_right f i s'). Proof. intros; apply fold_right_equivlistA_restr with (R:=fun _ _ => True); - try red; auto. -apply ForallList2_equiv1; try red; auto. + repeat red; auto. +apply ForallPairs_ForallOrdPairs; try red; auto. Qed. Lemma fold_right_add : @@ -674,6 +473,8 @@ Proof. intros; apply (@fold_right_equivlistA s' (x::s)); auto. Qed. +End Fold. + Section Remove. Hypothesis eqA_dec : forall x y : A, {eqA x y}+{~(eqA x y)}. @@ -682,15 +483,15 @@ Lemma InA_dec : forall x l, { InA x l } + { ~ InA x l }. Proof. induction l. right; auto. -red; inversion 1. +intro; inv. destruct (eqA_dec x a). left; auto. destruct IHl. left; auto. -right; red; inversion_clear 1; contradiction. -Qed. +right; intro; inv; contradiction. +Defined. -Fixpoint removeA (x : A) (l : list A){struct l} : list A := +Fixpoint removeA (x : A) (l : list A) : list A := match l with | nil => nil | y::tl => if (eqA_dec x y) then removeA x tl else y::(removeA x tl) @@ -708,21 +509,21 @@ 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. +intro; inv. +destruct 1; inv. 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. +inv; auto. +destruct H0; transitivity a; auto. split. -inversion_clear 1. +intro; inv. split; auto. contradict n. -apply eqA_trans with y; auto. +transitivity y; auto. rewrite (IHl x y) in H0; destruct H0; auto. -destruct 1; inversion_clear H; auto. -constructor 2; rewrite IHl; auto. +destruct 1; inv; auto. +right; rewrite IHl; auto. Qed. Lemma removeA_NoDupA : @@ -730,17 +531,17 @@ Lemma removeA_NoDupA : Proof. simple induction s; simpl; intros. auto. -inversion_clear H0. -destruct (eqA_dec x a); simpl; auto. +inv. +destruct (eqA_dec x a); simpl; auto. constructor; auto. rewrite removeA_InA. intuition. -Qed. +Qed. -Lemma removeA_equivlistA : forall l l' x, +Lemma removeA_equivlistA : forall l l' x, ~InA x l -> equivlistA (x :: l) l' -> equivlistA l (removeA x l'). -Proof. -unfold equivlistA; intros. +Proof. +unfold equivlistA; intros. rewrite removeA_InA. split; intros. rewrite <- H0; split; auto. @@ -748,64 +549,306 @@ contradict H. apply InA_eqA with x0; auto. rewrite <- (H0 x0) in H1. destruct H1. -inversion_clear H1; auto. +inv; auto. elim H2; auto. Qed. End Remove. -End Fold. + +(** Results concerning lists modulo [eqA] and [ltA] *) + +Variable ltA : A -> A -> Prop. +Hypothesis ltA_strorder : StrictOrder ltA. +Hypothesis ltA_compat : Proper (eqA==>eqA==>iff) ltA. + +Hint Resolve (@StrictOrder_Transitive _ _ ltA_strorder). + +Notation InfA:=(lelistA ltA). +Notation SortA:=(sort ltA). + +Hint Constructors lelistA sort. + +Lemma InfA_ltA : + forall l x y, ltA x y -> InfA y l -> InfA x l. +Proof. + destruct l; constructor. inv; eauto. +Qed. + +Global Instance InfA_compat : Proper (eqA==>eqlistA==>iff) InfA. +Proof. + intros x x' Hxx' l l' Hll'. + inversion_clear Hll'. + intuition. + split; intro; inv; constructor. + rewrite <- Hxx', <- H; auto. + rewrite Hxx', H; auto. +Qed. + +(** For compatibility, can be deduced from [InfA_compat] *) +Lemma InfA_eqA : + forall l x y, eqA x y -> InfA y l -> InfA x l. +Proof. + intros l x y H; rewrite H; auto. +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. inv. + intros. inv. + setoid_replace x with a; auto. + eauto. +Qed. + +Lemma In_InfA : + forall l x, (forall y, In y l -> ltA x y) -> InfA x l. +Proof. + simple induction l; simpl; 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; 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 InfA_app : forall l1 l2 a, InfA a l1 -> InfA a l2 -> InfA a (l1++l2). +Proof. + induction l1; simpl; auto. + intros; inv; 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. + inv. + constructor; auto. + apply InfA_app; auto. + destruct l2; auto. +Qed. + +Lemma SortA_NoDupA : forall l, SortA l -> NoDupA l. +Proof. + simple induction l; auto. + intros x l' H H0. + inv. + constructor; auto. + intro. + apply (StrictOrder_Irreflexive x). + eapply SortA_InfA_InA; eauto. +Qed. + + +(** Some results about [eqlistA] *) + +Section EqlistA. + +Lemma eqlistA_length : forall l l', eqlistA l l' -> length l = length l'. +Proof. +induction 1; auto; simpl; congruence. +Qed. + +Global Instance app_eqlistA_compat : + Proper (eqlistA==>eqlistA==>eqlistA) (@app A). +Proof. + repeat red; induction 1; simpl; auto. +Qed. + +(** For compatibility, can be deduced from app_eqlistA_compat **) +Lemma eqlistA_app : forall l1 l1' l2 l2', + eqlistA l1 l1' -> eqlistA l2 l2' -> eqlistA (l1++l2) (l1'++l2'). +Proof. +intros l1 l1' l2 l2' H H'; rewrite H, H'; reflexivity. +Qed. + +Lemma eqlistA_rev_app : forall l1 l1', + eqlistA l1 l1' -> forall l2 l2', eqlistA l2 l2' -> + eqlistA ((rev l1)++l2) ((rev l1')++l2'). +Proof. +induction 1; auto. +simpl; intros. +do 2 rewrite app_ass; simpl; auto. +Qed. + +Global Instance rev_eqlistA_compat : Proper (eqlistA==>eqlistA) (@rev A). +Proof. +repeat red. intros. +rewrite (app_nil_end (rev x)), (app_nil_end (rev y)). +apply eqlistA_rev_app; auto. +Qed. + +Lemma eqlistA_rev : forall l1 l1', + eqlistA l1 l1' -> eqlistA (rev l1) (rev l1'). +Proof. +apply rev_eqlistA_compat. +Qed. + +Lemma SortA_equivlistA_eqlistA : forall l l', + SortA l -> SortA l' -> equivlistA l l' -> eqlistA l l'. +Proof. +induction l; destruct l'; simpl; intros; auto. +destruct (H1 a); assert (InA a nil) by auto; inv. +destruct (H1 a); assert (InA a nil) by auto; inv. +inv. +assert (forall y, InA y l -> ltA a y). +intros; eapply SortA_InfA_InA with (l:=l); eauto. +assert (forall y, InA y l' -> ltA a0 y). +intros; eapply SortA_InfA_InA with (l:=l'); eauto. +clear H3 H4. +assert (eqA a a0). + destruct (H1 a). + destruct (H1 a0). + assert (InA a (a0::l')) by auto. inv; auto. + assert (InA a0 (a::l)) by auto. inv; auto. + elim (StrictOrder_Irreflexive a); eauto. +constructor; auto. +apply IHl; auto. +split; intros. +destruct (H1 x). +assert (InA x (a0::l')) by auto. inv; auto. +rewrite H9,<-H3 in H4. elim (StrictOrder_Irreflexive a); eauto. +destruct (H1 x). +assert (InA x (a::l)) by auto. inv; auto. +rewrite H9,H3 in H4. elim (StrictOrder_Irreflexive a0); eauto. +Qed. + +End EqlistA. + +(** A few things about [filter] *) + +Section Filter. + +Lemma filter_sort : forall f l, SortA l -> SortA (List.filter f l). +Proof. +induction l; simpl; auto. +intros; inv; auto. +destruct (f a); auto. +constructor; auto. +apply In_InfA; auto. +intros. +rewrite filter_In in H; destruct H. +eapply SortA_InfA_InA; eauto. +Qed. + +Implicit Arguments eq [ [A] ]. + +Lemma filter_InA : forall f, Proper (eqA==>eq) f -> + forall l x, InA x (List.filter f l) <-> InA x l /\ f x = true. +Proof. +clear ltA ltA_compat ltA_strorder. +intros; do 2 rewrite InA_alt; intuition. +destruct H0 as (y,(H0,H1)); rewrite filter_In in H1; exists y; intuition. +destruct H0 as (y,(H0,H1)); rewrite filter_In in H1; intuition. + rewrite (H _ _ H0); auto. +destruct H1 as (y,(H0,H1)); exists y; rewrite filter_In; intuition. + rewrite <- (H _ _ H0); auto. +Qed. + +Lemma filter_split : + forall f, (forall x y, f x = true -> f y = false -> ltA x y) -> + forall l, SortA l -> l = filter f l ++ filter (fun x=>negb (f x)) l. +Proof. +induction l; simpl; intros; auto. +inv. +rewrite IHl at 1; auto. +case_eq (f a); simpl; intros; auto. +assert (forall e, In e l -> f e = false). + intros. + assert (H4:=SortA_InfA_InA H1 H2 (In_InA H3)). + case_eq (f e); simpl; intros; auto. + elim (StrictOrder_Irreflexive e). + transitivity a; auto. +replace (List.filter f l) with (@nil A); auto. +generalize H3; clear; induction l; simpl; auto. +case_eq (f a); auto; intros. +rewrite H3 in H; auto; try discriminate. +Qed. + +End Filter. End Type_with_equality. -Hint Unfold compat_bool compat_nat compat_P. -Hint Constructors InA NoDupA sort lelistA eqlistA. -Section Find. -Variable A B : Type. -Variable eqA : A -> A -> Prop. -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 Constructors InA eqlistA NoDupA sort lelistA. + +Section Find. + +Variable A B : Type. +Variable eqA : A -> A -> Prop. +Hypothesis eqA_equiv : Equivalence eqA. Hypothesis eqA_dec : forall x y : A, {eqA x y}+{~(eqA x y)}. -Fixpoint findA (f : A -> bool) (l:list (A*B)) : option B := - match l with - | nil => None +Fixpoint findA (f : A -> bool) (l:list (A*B)) : option B := + match l with + | nil => None | (a,b)::l => if f a then Some b else findA f l end. -Lemma findA_NoDupA : - forall l a b, - NoDupA (fun p p' => eqA (fst p) (fst p')) l -> +Lemma findA_NoDupA : + forall l a b, + NoDupA (fun p p' => eqA (fst p) (fst p')) l -> (InA (fun p p' => eqA (fst p) (fst p') /\ snd p = snd p') (a,b) l <-> findA (fun a' => if eqA_dec a a' then true else false) l = Some b). Proof. -induction l; simpl; intros. +set (eqk := fun p p' : A*B => eqA (fst p) (fst p')). +set (eqke := fun p p' : A*B => eqA (fst p) (fst p') /\ snd p = snd p'). +induction l; intros; simpl. split; intros; try discriminate. -inversion H0. +invlist InA. destruct a as (a',b'); rename a0 into a. -inversion_clear H. +invlist NoDupA. split; intros. -inversion_clear H. -simpl in *; destruct H2; subst b'. +invlist InA. +compute in H2; destruct H2. subst b'. destruct (eqA_dec a a'); intuition. destruct (eqA_dec a a'); simpl. -destruct H0. -generalize e H2 eqA_trans eqA_sym; clear. +contradict H0. +revert e H2; clear - eqA_equiv. induction l. -inversion 2. -inversion_clear 2; intros; auto. +intros; invlist InA. +intros; invlist InA; auto. destruct a0. compute in H; destruct H. subst b. -constructor 1; auto. -simpl. -apply eqA_trans with a; auto. +left; auto. +compute. +transitivity a; auto. symmetry; auto. rewrite <- IHl; auto. destruct (eqA_dec a a'); simpl in *. -inversion H; clear H; intros; subst b'; auto. -constructor 2. -rewrite IHl; auto. +left; split; simpl; congruence. +right. rewrite IHl; auto. Qed. -End Find. +End Find. + + +(** Compatibility aliases. [Proper] is rather to be used directly now.*) + +Definition compat_bool {A} (eqA:A->A->Prop)(f:A->bool) := + Proper (eqA==>Logic.eq) f. + +Definition compat_nat {A} (eqA:A->A->Prop)(f:A->nat) := + Proper (eqA==>Logic.eq) f. + +Definition compat_P {A} (eqA:A->A->Prop)(P:A->Prop) := + Proper (eqA==>impl) P. + +Definition compat_op {A B} (eqA:A->A->Prop)(eqB:B->B->Prop)(f:A->B->B) := + Proper (eqA==>eqB==>eqB) f. + diff --git a/theories/Lists/StreamMemo.v b/theories/Lists/StreamMemo.v index bdbe0ecc..d906cfa4 100644 --- a/theories/Lists/StreamMemo.v +++ b/theories/Lists/StreamMemo.v @@ -11,8 +11,8 @@ Require Import Streams. (** * Memoization *) -(** Successive outputs of a given function [f] are stored in - a stream in order to avoid duplicated computations. *) +(** Successive outputs of a given function [f] are stored in + a stream in order to avoid duplicated computations. *) Section MemoFunction. @@ -24,8 +24,8 @@ CoFixpoint memo_make (n:nat) : Stream A := Cons (f n) (memo_make (S n)). Definition memo_list := memo_make 0. Fixpoint memo_get (n:nat) (l:Stream A) : A := - match n with - | O => hd l + match n with + | O => hd l | S n1 => memo_get n1 (tl l) end. @@ -49,7 +49,7 @@ Variable g: A -> A. Hypothesis Hg_correct: forall n, f (S n) = g (f n). CoFixpoint imemo_make (fn:A) : Stream A := - let fn1 := g fn in + let fn1 := g fn in Cons fn1 (imemo_make fn1). Definition imemo_list := let f0 := f 0 in @@ -68,7 +68,7 @@ Qed. End MemoFunction. -(** For a dependent function, the previous solution is +(** For a dependent function, the previous solution is reused thanks to a temporarly hiding of the dependency in a "container" [memo_val]. *) @@ -80,7 +80,7 @@ Variable f: forall n, A n. Inductive memo_val: Type := memo_mval: forall n, A n -> memo_val. -Fixpoint is_eq (n m : nat) {struct n}: {n = m} + {True} := +Fixpoint is_eq (n m : nat) : {n = m} + {True} := match n, m return {n = m} + {True} with | 0, 0 =>left True (refl_equal 0) | 0, S m1 => right (0 = S m1) I @@ -88,7 +88,7 @@ Fixpoint is_eq (n m : nat) {struct n}: {n = m} + {True} := | S n1, S m1 => match is_eq n1 m1 with | left H => left True (f_equal S H) - | right _ => right (S n1 = S m1) I + | right _ => right (S n1 = S m1) I end end. @@ -97,7 +97,7 @@ match v with | memo_mval m x => match is_eq n m with | left H => - match H in (@eq _ _ y) return (A y -> A n) with + match H in (eq _ y) return (A y -> A n) with | refl_equal => fun v1 : A n => v1 end | right _ => fun _ : A m => f n @@ -134,7 +134,7 @@ Variable g: forall n, A n -> A (S n). Hypothesis Hg_correct: forall n, f (S n) = g n (f n). -Let mg v := match v with +Let mg v := match v with memo_mval n1 v1 => memo_mval (S n1) (g n1 v1) end. Definition dimemo_list := imemo_list _ mf mg. @@ -166,13 +166,13 @@ End DependentMemoFunction. Require Import ZArith. Open Scope Z_scope. -Fixpoint tfact (n: nat) := - match n with - | O => 1 - | S n1 => Z_of_nat n * tfact n1 +Fixpoint tfact (n: nat) := + match n with + | O => 1 + | S n1 => Z_of_nat n * tfact n1 end. -Definition lfact_list := +Definition lfact_list := dimemo_list _ tfact (fun n z => (Z_of_nat (S n) * z)). Definition lfact n := dmemo_get _ tfact n lfact_list. @@ -183,18 +183,18 @@ intros n; unfold lfact, lfact_list. rewrite dimemo_get_correct; auto. Qed. -Fixpoint nop p := +Fixpoint nop p := match p with - | xH => 0 - | xI p1 => nop p1 - | xO p1 => nop p1 + | xH => 0 + | xI p1 => nop p1 + | xO p1 => nop p1 end. -Fixpoint test z := +Fixpoint test z := match z with - | Z0 => 0 - | Zpos p1 => nop p1 - | Zneg p1 => nop p1 + | Z0 => 0 + | Zpos p1 => nop p1 + | Zneg p1 => nop p1 end. Time Eval vm_compute in test (lfact 2000). @@ -202,4 +202,4 @@ Time Eval vm_compute in test (lfact 2000). Time Eval vm_compute in test (lfact 1500). Time Eval vm_compute in (lfact 1500). *) - + diff --git a/theories/Lists/Streams.v b/theories/Lists/Streams.v index 49990502..3fa053b7 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 9967 2007-07-11 15:25:03Z roconnor $ i*) +(*i $Id$ i*) Set Implicit Arguments. @@ -29,7 +29,7 @@ Definition tl (x:Stream) := match x with end. -Fixpoint Str_nth_tl (n:nat) (s:Stream) {struct n} : Stream := +Fixpoint Str_nth_tl (n:nat) (s:Stream) : Stream := match n with | O => s | S m => Str_nth_tl m (tl s) @@ -41,7 +41,7 @@ Definition Str_nth (n:nat) (s:Stream) : A := hd (Str_nth_tl n s). Lemma unfold_Stream : forall x:Stream, x = match x with | Cons a s => Cons a s - end. + end. Proof. intro x. case x. @@ -223,7 +223,7 @@ Variable f: A -> B -> C. CoFixpoint zipWith (a:Stream A) (b:Stream B) : Stream C := Cons (f (hd a) (hd b)) (zipWith (tl a) (tl b)). -Lemma Str_nth_tl_zipWith : forall n (a:Stream A) (b:Stream B), +Lemma Str_nth_tl_zipWith : forall n (a:Stream A) (b:Stream B), Str_nth_tl n (zipWith a b)= zipWith (Str_nth_tl n a) (Str_nth_tl n b). Proof. induction n. diff --git a/theories/Lists/TheoryList.v b/theories/Lists/TheoryList.v index 2bfb70fe..7ed9c519 100644 --- a/theories/Lists/TheoryList.v +++ b/theories/Lists/TheoryList.v @@ -6,12 +6,16 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: TheoryList.v 8866 2006-05-28 16:21:04Z herbelin $ i*) +(*i $Id$ i*) (** Some programs and results about lists following CAML Manual *) Require Export List. Set Implicit Arguments. + +Local Notation "[ ]" := nil (at level 0). +Local Notation "[ a ; .. ; b ]" := (a :: .. (b :: []) ..) (at level 0). + Section Lists. Variable A : Type. @@ -23,11 +27,13 @@ Variable A : Type. Definition Isnil (l:list A) : Prop := nil = l. Lemma Isnil_nil : Isnil nil. +Proof. red in |- *; auto. Qed. Hint Resolve Isnil_nil. Lemma not_Isnil_cons : forall (a:A) (l:list A), ~ Isnil (a :: l). +Proof. unfold Isnil in |- *. intros; discriminate. Qed. @@ -35,6 +41,7 @@ Qed. Hint Resolve Isnil_nil not_Isnil_cons. Lemma Isnil_dec : forall l:list A, {Isnil l} + {~ Isnil l}. +Proof. intro l; case l; auto. (* Realizer (fun l => match l with @@ -50,6 +57,7 @@ Qed. Lemma Uncons : forall l:list A, {a : A & {m : list A | a :: m = l}} + {Isnil l}. +Proof. intro l; case l. auto. intros a m; intros; left; exists a; exists m; reflexivity. @@ -67,6 +75,7 @@ Qed. Lemma Hd : forall l:list A, {a : A | exists m : list A, a :: m = l} + {Isnil l}. +Proof. intro l; case l. auto. intros a m; intros; left; exists a; exists m; reflexivity. @@ -81,6 +90,7 @@ Qed. Lemma Tl : forall l:list A, {m : list A | (exists a : A, a :: m = l) \/ Isnil l /\ Isnil m}. +Proof. intro l; case l. exists (nil (A:=A)); auto. intros a m; intros; exists m; left; exists a; reflexivity. @@ -97,7 +107,7 @@ Qed. (****************************************) (* length is defined in List *) -Fixpoint Length_l (l:list A) (n:nat) {struct l} : nat := +Fixpoint Length_l (l:list A) (n:nat) : nat := match l with | nil => n | _ :: m => Length_l m (S n) @@ -105,6 +115,7 @@ Fixpoint Length_l (l:list A) (n:nat) {struct l} : nat := (* A tail recursive version *) Lemma Length_l_pf : forall (l:list A) (n:nat), {m : nat | n + length l = m}. +Proof. induction l as [| a m lrec]. intro n; exists n; simpl in |- *; auto. intro n; elim (lrec (S n)); simpl in |- *; intros. @@ -115,6 +126,7 @@ Realizer Length_l. Qed. Lemma Length : forall l:list A, {m : nat | length l = m}. +Proof. intro l. apply (Length_l_pf l 0). (* Realizer (fun l -> Length_l_pf l O). @@ -139,14 +151,9 @@ elim l; intros; elim H; auto. Qed. -Inductive AllS (P:A -> Prop) : list A -> Prop := - | allS_nil : AllS P nil - | allS_cons : forall (a:A) (l:list A), P a -> AllS P l -> AllS P (a :: l). -Hint Resolve allS_nil allS_cons. - Hypothesis eqA_dec : forall a b:A, {a = b} + {a <> b}. -Fixpoint mem (a:A) (l:list A) {struct l} : bool := +Fixpoint mem (a:A) (l:list A) : bool := match l with | nil => false | b :: m => if eqA_dec a b then true else mem a m @@ -154,7 +161,7 @@ Fixpoint mem (a:A) (l:list A) {struct l} : bool := Hint Unfold In. Lemma Mem : forall (a:A) (l:list A), {In a l} + {AllS (fun b:A => b <> a) l}. -intros a l. +Proof. induction l. auto. elim (eqA_dec a a0). @@ -188,20 +195,23 @@ Hint Resolve fst_nth_O fst_nth_S. Lemma fst_nth_nth : forall (l:list A) (n:nat) (a:A), fst_nth_spec l n a -> nth_spec l n a. +Proof. induction 1; auto. Qed. Hint Immediate fst_nth_nth. Lemma nth_lt_O : forall (l:list A) (n:nat) (a:A), nth_spec l n a -> 0 < n. +Proof. induction 1; auto. Qed. Lemma nth_le_length : forall (l:list A) (n:nat) (a:A), nth_spec l n a -> n <= length l. +Proof. induction 1; simpl in |- *; auto with arith. Qed. -Fixpoint Nth_func (l:list A) (n:nat) {struct l} : Exc A := +Fixpoint Nth_func (l:list A) (n:nat) : Exc A := match l, n with | a :: _, S O => value a | _ :: l', S (S p) => Nth_func l' (S p) @@ -211,6 +221,7 @@ Fixpoint Nth_func (l:list A) (n:nat) {struct l} : Exc A := Lemma Nth : forall (l:list A) (n:nat), {a : A | nth_spec l n a} + {n = 0 \/ length l < n}. +Proof. induction l as [| a l IHl]. intro n; case n; simpl in |- *; auto with arith. intro n; destruct n as [| [| n1]]; simpl in |- *; auto. @@ -227,6 +238,7 @@ Qed. Lemma Item : forall (l:list A) (n:nat), {a : A | nth_spec l (S n) a} + {length l <= n}. +Proof. intros l n; case (Nth l (S n)); intro. case s; intro a; left; exists a; auto. right; case o; intro. @@ -237,7 +249,7 @@ Qed. Require Import Minus. Require Import DecBool. -Fixpoint index_p (a:A) (l:list A) {struct l} : nat -> Exc nat := +Fixpoint index_p (a:A) (l:list A) : nat -> Exc nat := match l with | nil => fun p => error | b :: m => fun p => ifdec (eqA_dec a b) (value p) (index_p a m (S p)) @@ -246,6 +258,7 @@ Fixpoint index_p (a:A) (l:list A) {struct l} : nat -> Exc nat := Lemma Index_p : forall (a:A) (l:list A) (p:nat), {n : nat | fst_nth_spec l (S n - p) a} + {AllS (fun b:A => a <> b) l}. +Proof. induction l as [| b m irec]. auto. intro p. @@ -264,6 +277,7 @@ Lemma Index : forall (a:A) (l:list A), {n : nat | fst_nth_spec l n a} + {AllS (fun b:A => a <> b) l}. +Proof. intros a l; case (Index_p a l 1); auto. intros [n P]; left; exists n; auto. rewrite (minus_n_O n); trivial. @@ -287,20 +301,24 @@ Definition InR_inv (l:list A) := end. Lemma InR_INV : forall l:list A, InR l -> InR_inv l. +Proof. induction 1; simpl in |- *; auto. Qed. Lemma InR_cons_inv : forall (a:A) (l:list A), InR (a :: l) -> R a \/ InR l. +Proof. intros a l H; exact (InR_INV H). Qed. Lemma InR_or_app : forall l m:list A, InR l \/ InR m -> InR (l ++ m). +Proof. intros l m [| ]. induction 1; simpl in |- *; auto. intro. induction l; simpl in |- *; auto. Qed. Lemma InR_app_or : forall l m:list A, InR (l ++ m) -> InR l \/ InR m. +Proof. intros l m; elim l; simpl in |- *; auto. intros b l' Hrec IAc; elim (InR_cons_inv IAc); auto. intros; elim Hrec; auto. @@ -315,6 +333,7 @@ Fixpoint find (l:list A) : Exc A := end. Lemma Find : forall l:list A, {a : A | In a l & R a} + {AllS P l}. +Proof. induction l as [| a m [[b H1 H2]| H]]; auto. left; exists b; auto. destruct (RS_dec a). @@ -342,6 +361,7 @@ Fixpoint try_find (l:list A) : Exc B := Lemma Try_find : forall l:list A, {c : B | exists2 a : A, In a l & T a c} + {AllS P l}. +Proof. induction l as [| a m [[b H1]| H]]. auto. left; exists b; destruct H1 as [a' H2 H3]; exists a'; auto. @@ -349,7 +369,7 @@ destruct (TS_dec a) as [[c H1]| ]. left; exists c. exists a; auto. auto. -(* +(* Realizer try_find. *) Qed. @@ -359,7 +379,7 @@ End Find_sec. Section Assoc_sec. Variable B : Type. -Fixpoint assoc (a:A) (l:list (A * B)) {struct l} : +Fixpoint assoc (a:A) (l:list (A * B)) : Exc B := match l with | nil => error @@ -383,6 +403,7 @@ Hint Resolve allS_assoc_nil allS_assoc_cons. Lemma Assoc : forall (a:A) (l:list (A * B)), B + {AllS_assoc (fun a':A => a <> a') l}. +Proof. induction l as [| [a' b] m assrec]. auto. destruct (eqA_dec a a'). left; exact b. @@ -398,6 +419,5 @@ End Assoc_sec. End Lists. -Hint Resolve Isnil_nil not_Isnil_cons in_hd in_tl in_cons allS_nil allS_cons: - datatypes. +Hint Resolve Isnil_nil not_Isnil_cons in_hd in_tl in_cons : datatypes. Hint Immediate fst_nth_nth: datatypes. diff --git a/theories/Lists/intro.tex b/theories/Lists/intro.tex index c45f8803..0051e2c2 100755 --- a/theories/Lists/intro.tex +++ b/theories/Lists/intro.tex @@ -21,7 +21,4 @@ This library includes the following files: 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} diff --git a/theories/Lists/vo.itarget b/theories/Lists/vo.itarget new file mode 100644 index 00000000..d2a31367 --- /dev/null +++ b/theories/Lists/vo.itarget @@ -0,0 +1,7 @@ +ListSet.vo +ListTactics.vo +List.vo +SetoidList.vo +StreamMemo.vo +Streams.vo +TheoryList.vo |