diff options
Diffstat (limited to 'theories/Lists')
| -rw-r--r-- | theories/Lists/List.v | 1047 | ||||
| -rw-r--r-- | theories/Lists/ListDec.v | 103 | ||||
| -rw-r--r-- | theories/Lists/ListSet.v | 22 | ||||
| -rw-r--r-- | theories/Lists/ListTactics.v | 2 | ||||
| -rw-r--r-- | theories/Lists/SetoidList.v | 189 | ||||
| -rw-r--r-- | theories/Lists/SetoidPermutation.v | 3 | ||||
| -rw-r--r-- | theories/Lists/StreamMemo.v | 2 | ||||
| -rw-r--r-- | theories/Lists/Streams.v | 2 | ||||
| -rw-r--r-- | theories/Lists/vo.itarget | 1 |
9 files changed, 1087 insertions, 284 deletions
diff --git a/theories/Lists/List.v b/theories/Lists/List.v index f5a12b09..3cba090f 100644 --- a/theories/Lists/List.v +++ b/theories/Lists/List.v @@ -1,15 +1,16 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -Require Import Le Gt Minus Bool Setoid. +Require Setoid. +Require Import PeanoNat Le Gt Minus Bool. Set Implicit Arguments. - +(* Set Universe Polymorphism. *) (******************************************************************) (** * Basics: definition of polymorphic lists and some operations *) @@ -20,6 +21,16 @@ Set Implicit Arguments. Open Scope list_scope. +(** Standard notations for lists. +In a special module to avoid conflicts. *) +Module ListNotations. +Notation " [ ] " := nil (format "[ ]") : list_scope. +Notation " [ x ] " := (cons x nil) : list_scope. +Notation " [ x ; .. ; y ] " := (cons x .. (cons y nil) ..) : list_scope. +End ListNotations. + +Import ListNotations. + Section Lists. Variable A : Type. @@ -28,44 +39,31 @@ Section Lists. Definition hd (default:A) (l:list A) := match l with - | nil => default + | [] => default | x :: _ => x end. Definition hd_error (l:list A) := match l with - | nil => error + | [] => error | x :: _ => value x end. Definition tl (l:list A) := match l with - | nil => nil + | [] => nil | a :: m => m end. (** The [In] predicate *) Fixpoint In (a:A) (l:list A) : Prop := match l with - | nil => False + | [] => False | b :: m => b = a \/ In a m end. End Lists. - -(** Standard notations for lists. -In a special module to avoid conflict. *) -Module ListNotations. -Notation " [ ] " := nil : list_scope. -Notation " [ x ] " := (cons x nil) : list_scope. -Notation " [ x ; .. ; y ] " := (cons x .. (cons y nil) ..) : list_scope. -End ListNotations. - -Import ListNotations. - -(** ** Facts about lists *) - Section Facts. Variable A : Type. @@ -89,6 +87,24 @@ Section Facts. left; exists a, tail; reflexivity. Qed. + Lemma hd_error_tl_repr : forall l (a:A) r, + hd_error l = Some a /\ tl l = r <-> l = a :: r. + Proof. destruct l as [|x xs]. + - unfold hd_error, tl; intros a r. split; firstorder discriminate. + - intros. simpl. split. + * intros (H1, H2). inversion H1. rewrite H2. reflexivity. + * inversion 1. subst. auto. + Qed. + + Lemma hd_error_some_nil : forall l (a:A), hd_error l = Some a -> l <> nil. + Proof. unfold hd_error. destruct l; now discriminate. Qed. + + Theorem length_zero_iff_nil (l : list A): + length l = 0 <-> l=[]. + Proof. + split; [now destruct l | now intros ->]. + Qed. + (** *** Head and tail *) Theorem hd_error_nil : hd_error (@nil A) = None. @@ -119,6 +135,12 @@ Section Facts. simpl; auto. Qed. + Theorem not_in_cons (x a : A) (l : list A): + ~ In x (a::l) <-> x<>a /\ ~ In x l. + Proof. + simpl. intuition. + Qed. + Theorem in_nil : forall a:A, ~ In a []. Proof. unfold not; intros a H; inversion_clear H. @@ -130,7 +152,7 @@ Section Facts. subst a; auto. exists [], l; auto. destruct (IHl H) as (l1,(l2,H0)). - exists (a::l1), l2; simpl; f_equal; auto. + exists (a::l1), l2; simpl. apply f_equal. auto. Qed. (** Inversion *) @@ -173,7 +195,7 @@ Section Facts. Qed. Theorem app_nil_r : forall l:list A, l ++ [] = l. - Proof. + Proof. induction l; simpl; f_equal; auto. Qed. @@ -228,10 +250,8 @@ Section Facts. intros. injection H. intro. - cut ([] = l ++ a0 :: l0); auto. - intro. - generalize (app_cons_not_nil _ _ _ H1); intro. - elim H2. + assert ([] = l ++ a0 :: l0) by auto. + apply app_cons_not_nil in H1 as []. Qed. Lemma app_inj_tail : @@ -240,22 +260,20 @@ Section Facts. induction x as [| x l IHl]; [ destruct y as [| a l] | destruct y as [| a l0] ]; simpl; auto. - intros a b H. - injection H. - auto. - intros a0 b H. - injection H; intros. - generalize (app_cons_not_nil _ _ _ H0); destruct 1. - intros a b H. - injection H; intros. - cut ([] = 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). - split; auto. - rewrite <- H1; rewrite <- H2; reflexivity. + - intros a b H. + injection H. + auto. + - intros a0 b H. + injection H as H1 H0. + apply app_cons_not_nil in H0 as []. + - intros a b H. + injection H as H1 H0. + assert ([] = l ++ [a]) by auto. + apply app_cons_not_nil in H as []. + - intros a0 b H. + injection H as <- H0. + destruct (IHl l0 a0 b H0) as (<-,<-). + split; auto. Qed. @@ -360,13 +378,12 @@ Section Elts. 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. - intros n l d; generalize n; induction l; intro n0. - right; case n0; trivial. - case n0; simpl. - auto. - intro n1; elim (IHl n1); auto. + intros n l d; revert n; induction l. + - right; destruct n; trivial. + - intros [|n]; simpl. + * left; auto. + * destruct (IHl n); auto. Qed. Lemma nth_S_cons : @@ -395,60 +412,132 @@ Section Elts. unfold nth_default; induction n; intros [ | ] ?; simpl; auto. Qed. + (** Results about [nth] *) + Lemma nth_In : forall (n:nat) (l:list A) (d:A), n < length l -> In (nth n l d) l. - Proof. 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. + - 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. + + Lemma In_nth l x d : In x l -> + exists n, n < length l /\ nth n l d = x. + Proof. + induction l as [|a l IH]. + - easy. + - intros [H|H]. + * subst; exists 0; simpl; auto with arith. + * destruct (IH H) as (n & Hn & Hn'). + exists (S n); simpl; auto with arith. Qed. Lemma nth_overflow : forall l n d, length l <= n -> nth n l d = d. Proof. induction l; destruct n; simpl; intros; auto. - inversion H. - apply IHl; auto with arith. + - inversion H. + - apply IHl; auto with arith. Qed. Lemma nth_indep : forall l n d d', n < length l -> nth n l d = nth n l d'. Proof. - induction l; simpl; intros; auto. - inversion H. - destruct n; simpl; auto with arith. + induction l. + - inversion 1. + - intros [|n] d d'; simpl; auto with arith. Qed. Lemma app_nth1 : forall l l' d n, n < length l -> nth n (l++l') d = nth n l d. Proof. induction l. - intros. - inversion H. - intros l' d n. - case n; simpl; auto. - intros; rewrite IHl; auto with arith. + - inversion 1. + - intros l' d [|n]; simpl; auto with arith. Qed. Lemma app_nth2 : forall l l' d n, n >= length l -> nth n (l++l') d = nth (n-length l) l' d. Proof. - induction l. - intros. - simpl. - destruct n; auto. - intros l' d n. - case n; simpl; auto. - intros. - inversion H. - intros. - rewrite IHl; auto with arith. + induction l; intros l' d [|n]; auto. + - inversion 1. + - intros; simpl; rewrite IHl; auto with arith. + Qed. + + Lemma nth_split n l d : n < length l -> + exists l1, exists l2, l = l1 ++ nth n l d :: l2 /\ length l1 = n. + Proof. + revert l. + induction n as [|n IH]; intros [|a l] H; try easy. + - exists nil; exists l; now simpl. + - destruct (IH l) as (l1 & l2 & Hl & Hl1); auto with arith. + exists (a::l1); exists l2; simpl; split; now f_equal. Qed. + (** Results about [nth_error] *) + Lemma nth_error_In l n x : nth_error l n = Some x -> In x l. + Proof. + revert n. induction l as [|a l IH]; intros [|n]; simpl; try easy. + - injection 1; auto. + - eauto. + Qed. + Lemma In_nth_error l x : In x l -> exists n, nth_error l n = Some x. + Proof. + induction l as [|a l IH]. + - easy. + - intros [H|H]. + * subst; exists 0; simpl; auto with arith. + * destruct (IH H) as (n,Hn). + exists (S n); simpl; auto with arith. + Qed. + + Lemma nth_error_None l n : nth_error l n = None <-> length l <= n. + Proof. + revert n. induction l; destruct n; simpl. + - split; auto. + - split; auto with arith. + - split; now auto with arith. + - rewrite IHl; split; auto with arith. + Qed. + + Lemma nth_error_Some l n : nth_error l n <> None <-> n < length l. + Proof. + revert n. induction l; destruct n; simpl. + - split; [now destruct 1 | inversion 1]. + - split; [now destruct 1 | inversion 1]. + - split; now auto with arith. + - rewrite IHl; split; auto with arith. + Qed. + + Lemma nth_error_split l n a : nth_error l n = Some a -> + exists l1, exists l2, l = l1 ++ a :: l2 /\ length l1 = n. + Proof. + revert l. + induction n as [|n IH]; intros [|x l] H; simpl in *; try easy. + - exists nil; exists l. injection H; clear H; intros; now subst. + - destruct (IH _ H) as (l1 & l2 & H1 & H2). + exists (x::l1); exists l2; simpl; split; now f_equal. + Qed. + + Lemma nth_error_app1 l l' n : n < length l -> + nth_error (l++l') n = nth_error l n. + Proof. + revert l. + induction n; intros [|a l] H; auto; try solve [inversion H]. + simpl in *. apply IHn. auto with arith. + Qed. + + Lemma nth_error_app2 l l' n : length l <= n -> + nth_error (l++l') n = nth_error l' (n-length l). + Proof. + revert l. + induction n; intros [|a l] H; auto; try solve [inversion H]. + simpl in *. apply IHn. auto with arith. + Qed. (*****************) (** ** Remove *) @@ -541,19 +630,29 @@ Section Elts. match l with | [] => 0 | y :: tl => - let n := count_occ tl x in - if eq_dec y x then S n else n + 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 (l : list A) (x : A) : In x l <-> count_occ l x > 0. + Theorem count_occ_In l x : In x l <-> count_occ l x > 0. Proof. induction l as [|y l]; simpl. - split; [destruct 1 | apply gt_irrefl]. - destruct eq_dec as [->|Hneq]; rewrite IHl; intuition. Qed. - Theorem count_occ_inv_nil (l : list A) : + Theorem count_occ_not_In l x : ~ In x l <-> count_occ l x = 0. + Proof. + rewrite count_occ_In. unfold gt. now rewrite Nat.nlt_ge, Nat.le_0_r. + Qed. + + Lemma count_occ_nil x : count_occ [] x = 0. + Proof. + reflexivity. + Qed. + + Theorem count_occ_inv_nil l : (forall x:A, count_occ l x = 0) <-> l = []. Proof. split. @@ -563,27 +662,20 @@ Section Elts. - now intros ->. Qed. - Lemma count_occ_nil : forall (x : A), count_occ [] x = 0. - Proof. - intro x; simpl; reflexivity. - Qed. - - Lemma count_occ_cons_eq : forall (l : list A) (x y : A), x = y -> count_occ (x::l) y = S (count_occ l y). + Lemma count_occ_cons_eq l x y : + x = y -> count_occ (x::l) y = S (count_occ l y). Proof. - intros l x y H; simpl. - destruct (eq_dec x y); [reflexivity | contradiction]. + intros H. simpl. now destruct (eq_dec x y). Qed. - Lemma count_occ_cons_neq : forall (l : list A) (x y : A), x <> y -> count_occ (x::l) y = count_occ l y. + Lemma count_occ_cons_neq l x y : + x <> y -> count_occ (x::l) y = count_occ l y. Proof. - intros l x y H; simpl. - destruct (eq_dec x y); [contradiction | reflexivity]. + intros H. simpl. now destruct (eq_dec x y). Qed. End Elts. - - (*******************************) (** * Manipulating whole lists *) (*******************************) @@ -739,6 +831,33 @@ Section ListOps. End Reverse_Induction. + (*************************) + (** ** Concatenation *) + (*************************) + + Fixpoint concat (l : list (list A)) : list A := + match l with + | nil => nil + | cons x l => x ++ concat l + end. + + Lemma concat_nil : concat nil = nil. + Proof. + reflexivity. + Qed. + + Lemma concat_cons : forall x l, concat (cons x l) = x ++ concat l. + Proof. + reflexivity. + Qed. + + Lemma concat_app : forall l1 l2, concat (l1 ++ l2) = concat l1 ++ concat l2. + Proof. + intros l1; induction l1 as [|x l1 IH]; intros l2; simpl. + + reflexivity. + + rewrite IH; apply app_assoc. + Qed. + (***********************************) (** ** Decidable equality on lists *) (***********************************) @@ -759,15 +878,20 @@ End ListOps. (************) Section Map. - Variables A B : Type. + Variables (A : Type) (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) + | [] => [] + | a :: t => (f a) :: (map t) end. + Lemma map_cons (x:A)(l:list A) : map (x::l) = (f x) :: (map l). + Proof. + reflexivity. + Qed. + Lemma in_map : forall (l:list A) (x:A), In x l -> In (f x) (map l). Proof. @@ -815,6 +939,25 @@ Section Map. destruct l; simpl; reflexivity || discriminate. Qed. + (** [map] and count of occurrences *) + + Hypothesis decA: forall x1 x2 : A, {x1 = x2} + {x1 <> x2}. + Hypothesis decB: forall y1 y2 : B, {y1 = y2} + {y1 <> y2}. + Hypothesis Hfinjective: forall x1 x2: A, (f x1) = (f x2) -> x1 = x2. + + Theorem count_occ_map x l: + count_occ decA l x = count_occ decB (map l) (f x). + Proof. + revert x. induction l as [| a l' Hrec]; intro x; simpl. + - reflexivity. + - specialize (Hrec x). + destruct (decA a x) as [H1|H1], (decB (f a) (f x)) as [H2|H2]. + * rewrite Hrec. reflexivity. + * contradiction H2. rewrite H1. reflexivity. + * specialize (Hfinjective H2). contradiction H1. + * assumption. + Qed. + (** [flat_map] *) Definition flat_map (f:A -> list B) := @@ -826,7 +969,7 @@ Section Map. Lemma in_flat_map : forall (f:A->list B)(l:list A)(y:B), In y (flat_map f l) <-> exists x, In x l /\ In y (f x). - Proof. + Proof using A B. induction l; simpl; split; intros. contradiction. destruct H as (x,(H,_)); contradiction. @@ -843,6 +986,21 @@ Section Map. End Map. +Lemma flat_map_concat_map : forall A B (f : A -> list B) l, + flat_map f l = concat (map f l). +Proof. +intros A B f l; induction l as [|x l IH]; simpl. ++ reflexivity. ++ rewrite IH; reflexivity. +Qed. + +Lemma concat_map : forall A B (f : A -> B) l, map f (concat l) = concat (map (map f) l). +Proof. +intros A B f l; induction l as [|x l IH]; simpl. ++ reflexivity. ++ rewrite map_app, IH; reflexivity. +Qed. + Lemma map_id : forall (A :Type) (l : list A), map (fun x => x) l = l. Proof. @@ -869,7 +1027,7 @@ Qed. (************************************) Section Fold_Left_Recursor. - Variables A B : Type. + Variables (A : Type) (B : Type). Variable f : A -> B -> A. Fixpoint fold_left (l:list B) (a0:A) : A := @@ -893,10 +1051,8 @@ End Fold_Left_Recursor. Lemma fold_left_length : forall (A:Type)(l:list A), fold_left (fun x _ => S x) l 0 = length l. Proof. - intro A. - cut (forall (l:list A) n, fold_left (fun x _ => S x) l n = n + length l). - intros. - exact (H l 0). + intros A l. + enough (H : forall n, fold_left (fun x _ => S x) l n = n + length l) by exact (H 0). induction l; simpl; auto. intros; rewrite IHl. simpl; auto with arith. @@ -907,7 +1063,7 @@ Qed. (************************************) Section Fold_Right_Recursor. - Variables A B : Type. + Variables (A : Type) (B : Type). Variable f : B -> A -> A. Variable a0 : A. @@ -939,29 +1095,17 @@ End Fold_Right_Recursor. Qed. Theorem fold_symmetric : - forall (A:Type) (f:A -> A -> A), - (forall x y z:A, f x (f y z) = f (f x y) z) -> - (forall x y:A, f x y = f y x) -> - forall (a0:A) (l:list A), fold_left f l a0 = fold_right f a0 l. + forall (A : Type) (f : A -> A -> A), + (forall x y z : A, f x (f y z) = f (f x y) z) -> + forall (a0 : A), (forall y : A, f a0 y = f y a0) -> + forall (l : list A), fold_left f l a0 = fold_right f a0 l. Proof. - destruct l as [| a l]. - reflexivity. - simpl. - rewrite <- H0. - generalize a0 a. - induction l as [| a3 l IHl]; simpl. - trivial. - intros. - rewrite H. - rewrite (H0 a2). - rewrite <- (H a1). - rewrite (H0 a1). - rewrite IHl. - reflexivity. + intros A f assoc a0 comma0 l. + induction l as [ | a1 l ]; [ simpl; reflexivity | ]. + simpl. rewrite <- IHl. clear IHl. revert a1. induction l; [ auto | ]. + simpl. intro. rewrite <- assoc. rewrite IHl. rewrite IHl. auto. Qed. - - (** [(list_power x y)] is [y^x], or the set of sequences of elts of [y] indexed by elts of [x], sorted in lexicographic order. *) @@ -1075,6 +1219,21 @@ End Fold_Right_Recursor. | x :: tl => if f x then Some x else find tl end. + Lemma find_some l x : find l = Some x -> In x l /\ f x = true. + Proof. + induction l as [|a l IH]; simpl; [easy| ]. + case_eq (f a); intros Ha Eq. + * injection Eq as ->; auto. + * destruct (IH Eq); auto. + Qed. + + Lemma find_none l : find l = None -> forall x, In x l -> f x = false. + Proof. + induction l as [|a l IH]; simpl; [easy|]. + case_eq (f a); intros Ha Eq x IN; [easy|]. + destruct IN as [<-|IN]; auto. + Qed. + (** [partition] *) Fixpoint partition (l:list A) : list A * list A := @@ -1084,6 +1243,53 @@ End Fold_Right_Recursor. if f x then (x::g,d) else (g,x::d) end. + Theorem partition_cons1 a l l1 l2: + partition l = (l1, l2) -> + f a = true -> + partition (a::l) = (a::l1, l2). + Proof. + simpl. now intros -> ->. + Qed. + + Theorem partition_cons2 a l l1 l2: + partition l = (l1, l2) -> + f a=false -> + partition (a::l) = (l1, a::l2). + Proof. + simpl. now intros -> ->. + Qed. + + Theorem partition_length l l1 l2: + partition l = (l1, l2) -> + length l = length l1 + length l2. + Proof. + revert l1 l2. induction l as [ | a l' Hrec]; intros l1 l2. + - now intros [= <- <- ]. + - simpl. destruct (f a), (partition l') as (left, right); + intros [= <- <- ]; simpl; rewrite (Hrec left right); auto. + Qed. + + Theorem partition_inv_nil (l : list A): + partition l = ([], []) <-> l = []. + Proof. + split. + - destruct l as [|a l' _]. + * intuition. + * simpl. destruct (f a), (partition l'); now intros [= -> ->]. + - now intros ->. + Qed. + + Theorem elements_in_partition l l1 l2: + partition l = (l1, l2) -> + forall x:A, In x l <-> In x l1 \/ In x l2. + Proof. + revert l1 l2. induction l as [| a l' Hrec]; simpl; intros l1 l2 Eq x. + - injection Eq as <- <-. tauto. + - destruct (partition l') as (left, right). + specialize (Hrec left right eq_refl x). + destruct (f a); injection Eq as <- <-; simpl; tauto. + Qed. + End Bool. @@ -1094,14 +1300,14 @@ End Fold_Right_Recursor. (******************************************************) Section ListPairs. - Variables A B : Type. + Variables (A : Type) (B : Type). (** [split] derives two lists from a list of pairs *) 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) + | [] => ([], []) + | (x,y) :: tl => let (left,right) := split tl in (x::left, y::right) end. Lemma in_split_l : forall (l:list (A*B))(p:A*B), @@ -1479,6 +1685,61 @@ Section Cutting. End Cutting. +(**********************************************************************) +(** ** Predicate for List addition/removal (no need for decidability) *) +(**********************************************************************) + +Section Add. + + Variable A : Type. + + (* [Add a l l'] means that [l'] is exactly [l], with [a] added + once somewhere *) + Inductive Add (a:A) : list A -> list A -> Prop := + | Add_head l : Add a l (a::l) + | Add_cons x l l' : Add a l l' -> Add a (x::l) (x::l'). + + Lemma Add_app a l1 l2 : Add a (l1++l2) (l1++a::l2). + Proof. + induction l1; simpl; now constructor. + Qed. + + Lemma Add_split a l l' : + Add a l l' -> exists l1 l2, l = l1++l2 /\ l' = l1++a::l2. + Proof. + induction 1. + - exists nil; exists l; split; trivial. + - destruct IHAdd as (l1 & l2 & Hl & Hl'). + exists (x::l1); exists l2; split; simpl; f_equal; trivial. + Qed. + + Lemma Add_in a l l' : Add a l l' -> + forall x, In x l' <-> In x (a::l). + Proof. + induction 1; intros; simpl in *; rewrite ?IHAdd; tauto. + Qed. + + Lemma Add_length a l l' : Add a l l' -> length l' = S (length l). + Proof. + induction 1; simpl; auto with arith. + Qed. + + Lemma Add_inv a l : In a l -> exists l', Add a l' l. + Proof. + intro Ha. destruct (in_split _ _ Ha) as (l1 & l2 & ->). + exists (l1 ++ l2). apply Add_app. + Qed. + + Lemma incl_Add_inv a l u v : + ~In a l -> incl (a::l) v -> Add a u v -> incl l u. + Proof. + intros Ha H AD y Hy. + assert (Hy' : In y (a::u)). + { rewrite <- (Add_in AD). apply H; simpl; auto. } + destruct Hy'; [ subst; now elim Ha | trivial ]. + Qed. + +End Add. (********************************) (** ** Lists without redundancy *) @@ -1492,31 +1753,187 @@ Section ReDun. | 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'). + Lemma NoDup_Add a l l' : Add a l l' -> (NoDup l' <-> NoDup l /\ ~In a l). Proof. - induction l; simpl. - inversion_clear 1; auto. - inversion_clear 1. - constructor. - contradict H0. - apply in_or_app; destruct (in_app_or _ _ _ H0); simpl; tauto. - apply IHl with a0; auto. + induction 1 as [l|x l l' AD IH]. + - split; [ inversion_clear 1; now split | now constructor ]. + - split. + + inversion_clear 1. rewrite IH in *. rewrite (Add_in AD) in *. + simpl in *; split; try constructor; intuition. + + intros (N,IN). inversion_clear N. constructor. + * rewrite (Add_in AD); simpl in *; intuition. + * apply IH. split; trivial. simpl in *; intuition. Qed. - Lemma NoDup_remove_2 : forall l l' a, NoDup (l++a::l') -> ~In a (l++l'). + Lemma NoDup_remove l l' a : + NoDup (l++a::l') -> NoDup (l++l') /\ ~In a (l++l'). Proof. - induction l; simpl. - inversion_clear 1; auto. - inversion_clear 1. - contradict H0. - destruct H0. - subst a0. - apply in_or_app; right; red; auto. - destruct (IHl _ _ H1); auto. + apply NoDup_Add. apply Add_app. + Qed. + + Lemma NoDup_remove_1 l l' a : NoDup (l++a::l') -> NoDup (l++l'). + Proof. + intros. now apply NoDup_remove with a. + Qed. + + Lemma NoDup_remove_2 l l' a : NoDup (l++a::l') -> ~In a (l++l'). + Proof. + intros. now apply NoDup_remove. + Qed. + + Theorem NoDup_cons_iff a l: + NoDup (a::l) <-> ~ In a l /\ NoDup l. + Proof. + split. + + inversion_clear 1. now split. + + now constructor. + Qed. + + (** Effective computation of a list without duplicates *) + + Hypothesis decA: forall x y : A, {x = y} + {x <> y}. + + Fixpoint nodup (l : list A) : list A := + match l with + | [] => [] + | x::xs => if in_dec decA x xs then nodup xs else x::(nodup xs) + end. + + Lemma nodup_In l x : In x (nodup l) <-> In x l. + Proof. + induction l as [|a l' Hrec]; simpl. + - reflexivity. + - destruct (in_dec decA a l'); simpl; rewrite Hrec. + * intuition; now subst. + * reflexivity. + Qed. + + Lemma NoDup_nodup l: NoDup (nodup l). + Proof. + induction l as [|a l' Hrec]; simpl. + - constructor. + - destruct (in_dec decA a l'); simpl. + * assumption. + * constructor; [ now rewrite nodup_In | assumption]. + Qed. + + Lemma nodup_inv k l a : nodup k = a :: l -> ~ In a l. + Proof. + intros H. + assert (H' : NoDup (a::l)). + { rewrite <- H. apply NoDup_nodup. } + now inversion_clear H'. + Qed. + + Theorem NoDup_count_occ l: + NoDup l <-> (forall x:A, count_occ decA l x <= 1). + Proof. + induction l as [| a l' Hrec]. + - simpl; split; auto. constructor. + - rewrite NoDup_cons_iff, Hrec, (count_occ_not_In decA). clear Hrec. split. + + intros (Ha, H) x. simpl. destruct (decA a x); auto. + subst; now rewrite Ha. + + split. + * specialize (H a). rewrite count_occ_cons_eq in H; trivial. + now inversion H. + * intros x. specialize (H x). simpl in *. destruct (decA a x); auto. + now apply Nat.lt_le_incl. + Qed. + + Theorem NoDup_count_occ' l: + NoDup l <-> (forall x:A, In x l -> count_occ decA l x = 1). + Proof. + rewrite NoDup_count_occ. + setoid_rewrite (count_occ_In decA). unfold gt, lt in *. + split; intros H x; specialize (H x); + set (n := count_occ decA l x) in *; clearbody n. + (* the rest would be solved by omega if we had it here... *) + - now apply Nat.le_antisymm. + - destruct (Nat.le_gt_cases 1 n); trivial. + + rewrite H; trivial. + + now apply Nat.lt_le_incl. + Qed. + + (** Alternative characterisations of being without duplicates, + thanks to [nth_error] and [nth] *) + + Lemma NoDup_nth_error l : + NoDup l <-> + (forall i j, i<length l -> nth_error l i = nth_error l j -> i = j). + Proof. + split. + { intros H; induction H as [|a l Hal Hl IH]; intros i j Hi E. + - inversion Hi. + - destruct i, j; simpl in *; auto. + * elim Hal. eapply nth_error_In; eauto. + * elim Hal. eapply nth_error_In; eauto. + * f_equal. apply IH; auto with arith. } + { induction l as [|a l]; intros H; constructor. + * intro Ha. apply In_nth_error in Ha. destruct Ha as (n,Hn). + assert (n < length l) by (now rewrite <- nth_error_Some, Hn). + specialize (H 0 (S n)). simpl in H. discriminate H; auto with arith. + * apply IHl. + intros i j Hi E. apply eq_add_S, H; simpl; auto with arith. } + Qed. + + Lemma NoDup_nth l d : + NoDup l <-> + (forall i j, i<length l -> j<length l -> + nth i l d = nth j l d -> i = j). + Proof. + split. + { intros H; induction H as [|a l Hal Hl IH]; intros i j Hi Hj E. + - inversion Hi. + - destruct i, j; simpl in *; auto. + * elim Hal. subst a. apply nth_In; auto with arith. + * elim Hal. subst a. apply nth_In; auto with arith. + * f_equal. apply IH; auto with arith. } + { induction l as [|a l]; intros H; constructor. + * intro Ha. eapply In_nth in Ha. destruct Ha as (n & Hn & Hn'). + specialize (H 0 (S n)). simpl in H. discriminate H; eauto with arith. + * apply IHl. + intros i j Hi Hj E. apply eq_add_S, H; simpl; auto with arith. } + Qed. + + (** Having [NoDup] hypotheses bring more precise facts about [incl]. *) + + Lemma NoDup_incl_length l l' : + NoDup l -> incl l l' -> length l <= length l'. + Proof. + intros N. revert l'. induction N as [|a l Hal N IH]; simpl. + - auto with arith. + - intros l' H. + destruct (Add_inv a l') as (l'', AD). { apply H; simpl; auto. } + rewrite (Add_length AD). apply le_n_S. apply IH. + now apply incl_Add_inv with a l'. + Qed. + + Lemma NoDup_length_incl l l' : + NoDup l -> length l' <= length l -> incl l l' -> incl l' l. + Proof. + intros N. revert l'. induction N as [|a l Hal N IH]. + - destruct l'; easy. + - intros l' E H x Hx. + destruct (Add_inv a l') as (l'', AD). { apply H; simpl; auto. } + rewrite (Add_in AD) in Hx. simpl in Hx. + destruct Hx as [Hx|Hx]; [left; trivial|right]. + revert x Hx. apply (IH l''); trivial. + * apply le_S_n. now rewrite <- (Add_length AD). + * now apply incl_Add_inv with a l'. Qed. End ReDun. +(** NoDup and map *) + +(** NB: the reciprocal result holds only for injective functions, + see FinFun.v *) + +Lemma NoDup_map_inv A B (f:A->B) l : NoDup (map f l) -> NoDup l. +Proof. + induction l; simpl; inversion_clear 1; subst; constructor; auto. + intro H. now apply (in_map f) in H. +Qed. (***********************************) (** ** Sequence of natural numbers *) @@ -1558,149 +1975,252 @@ Section NatSeq. auto with arith. Qed. + Lemma in_seq len start n : + In n (seq start len) <-> start <= n < start+len. + Proof. + revert start. induction len; simpl; intros. + - rewrite <- plus_n_O. split;[easy|]. + intros (H,H'). apply (Lt.lt_irrefl _ (Lt.le_lt_trans _ _ _ H H')). + - rewrite IHlen, <- plus_n_Sm; simpl; split. + * intros [H|H]; subst; intuition auto with arith. + * intros (H,H'). destruct (Lt.le_lt_or_eq _ _ H); intuition. + Qed. + + Lemma seq_NoDup len start : NoDup (seq start len). + Proof. + revert start; induction len; simpl; constructor; trivial. + rewrite in_seq. intros (H,_). apply (Lt.lt_irrefl _ H). + Qed. + End NatSeq. +Section Exists_Forall. -(** * Existential and universal predicates over lists *) + (** * 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. + Variable A:Type. -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. + Section One_predicate. + + Variable P:A->Prop. + + Inductive Exists : list A -> Prop := + | Exists_cons_hd : forall x l, P x -> Exists (x::l) + | Exists_cons_tl : forall x l, Exists l -> Exists (x::l). -Lemma Exists_nil : forall A (P:A->Prop), Exists P nil <-> False. -Proof. split; inversion 1. Qed. + Hint Constructors Exists. -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. + Lemma Exists_exists (l:list A) : + Exists l <-> (exists x, In x l /\ P x). + Proof. + split. + - induction 1; firstorder. + - induction l; firstorder; subst; auto. + Qed. + Lemma Exists_nil : Exists nil <-> False. + Proof. split; inversion 1. Qed. + + Lemma Exists_cons x l: + Exists (x::l) <-> P x \/ Exists l. + Proof. split; inversion 1; auto. Qed. + + Lemma Exists_dec l: + (forall x:A, {P x} + { ~ P x }) -> + {Exists l} + {~ Exists l}. + Proof. + intro Pdec. induction l as [|a l' Hrec]. + - right. now rewrite Exists_nil. + - destruct Hrec as [Hl'|Hl']. + * left. now apply Exists_cons_tl. + * destruct (Pdec a) as [Ha|Ha]. + + left. now apply Exists_cons_hd. + + right. now inversion_clear 1. + 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). + Inductive Forall : list A -> Prop := + | Forall_nil : Forall nil + | Forall_cons : forall x l, P x -> Forall l -> Forall (x::l). + + Hint Constructors Forall. + + Lemma Forall_forall (l:list A): + Forall l <-> (forall x, In x l -> P x). + Proof. + split. + - induction 1; firstorder; subst; auto. + - induction l; firstorder. + Qed. + + Lemma Forall_inv : forall (a:A) l, Forall (a :: l) -> P a. + Proof. + intros; inversion H; trivial. + Qed. + + Lemma Forall_rect : forall (Q : list A -> Type), + Q [] -> (forall b l, P b -> Q (b :: l)) -> forall l, Forall l -> Q l. + Proof. + intros Q H H'; induction l; intro; [|eapply H', Forall_inv]; eassumption. + Qed. + + Lemma Forall_dec : + (forall x:A, {P x} + { ~ P x }) -> + forall l:list A, {Forall l} + {~ Forall l}. + Proof. + intro Pdec. induction l as [|a l' Hrec]. + - left. apply Forall_nil. + - destruct Hrec as [Hl'|Hl']. + + destruct (Pdec a) as [Ha|Ha]. + * left. now apply Forall_cons. + * right. now inversion_clear 1. + + right. now inversion_clear 1. + Qed. + + End One_predicate. + + Lemma Forall_Exists_neg (P:A->Prop)(l:list A) : + Forall (fun x => ~ P x) l <-> ~(Exists P l). + Proof. + rewrite Forall_forall, Exists_exists. firstorder. + Qed. + + Lemma Exists_Forall_neg (P:A->Prop)(l:list A) : + (forall x, P x \/ ~P x) -> + Exists (fun x => ~ P x) l <-> ~(Forall P l). + Proof. + intro Dec. + split. + - rewrite Forall_forall, Exists_exists; firstorder. + - intros NF. + induction l as [|a l IH]. + + destruct NF. constructor. + + destruct (Dec a) as [Ha|Ha]. + * apply Exists_cons_tl, IH. contradict NF. now constructor. + * now apply Exists_cons_hd. + Qed. + + Lemma Forall_Exists_dec (P:A->Prop) : + (forall x:A, {P x} + { ~ P x }) -> + forall l:list A, + {Forall P l} + {Exists (fun x => ~ P x) l}. + Proof. + intros Pdec l. + destruct (Forall_dec P Pdec l); [left|right]; trivial. + apply Exists_Forall_neg; trivial. + intro x. destruct (Pdec x); [now left|now right]. + Qed. + + Lemma Forall_impl : forall (P Q : A -> Prop), (forall a, P a -> Q a) -> + forall l, Forall P l -> Forall Q l. + Proof. + intros P Q H l. rewrite !Forall_forall. firstorder. + Qed. + +End Exists_Forall. + +Hint Constructors Exists. Hint Constructors Forall. -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. +Section Forall2. -Lemma Forall_inv : forall A P (a:A) l, Forall P (a :: l) -> P a. -Proof. -intros; inversion H; trivial. -Defined. + (** [Forall2]: stating that elements of two lists are pairwise related. *) -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. + Variables A B : Type. + Variable R : A -> B -> Prop. -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. + Inductive Forall2 : list A -> list B -> Prop := + | Forall2_nil : Forall2 [] [] + | Forall2_cons : forall x y l l', + R x y -> Forall2 l l' -> Forall2 (x::l) (y::l'). -(** [Forall2]: stating that elements of two lists are pairwise related. *) + Hint Constructors Forall2. -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 : Forall2 [] []. + Proof. intros; apply Forall2_nil. Qed. + + Theorem Forall2_app_inv_l : forall l1 l2 l', + Forall2 (l1 ++ l2) l' -> + exists l1' l2', Forall2 l1 l1' /\ Forall2 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_refl : forall A B (R:A->B->Prop), Forall2 R [] []. -Proof. exact Forall2_nil. Qed. + Theorem Forall2_app_inv_r : forall l1' l2' l, + Forall2 l (l1' ++ l2') -> + exists l1 l2, Forall2 l1 l1' /\ Forall2 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_inv_l : forall A B (R:A->B->Prop) l1 l2 l', - Forall2 R (l1 ++ l2) l' -> - exists l1' 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 : forall l1 l2 l1' l2', + Forall2 l1 l1' -> Forall2 l2 l2' -> Forall2 (l1 ++ l2) (l1' ++ l2'). + Proof. + intros. induction l1 in l1', H, H0 |- *; inversion H; subst; simpl; auto. + Qed. +End Forall2. -Theorem Forall2_app_inv_r : forall A B (R:A->B->Prop) l1' l2' l, - Forall2 R l (l1' ++ l2') -> - exists l1 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. +Hint Constructors Forall2. -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. +Section ForallPairs. -(** [ForallPairs] : specifies that a certain relation should + (** [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. + Variable A : Type. + Variable R : A -> A -> Prop. -(** [ForallOrdPairs] : we still check a relation over all pairs + Definition ForallPairs 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. + Inductive ForallOrdPairs : list A -> Prop := + | FOP_nil : ForallOrdPairs nil + | FOP_cons : forall a l, + Forall (R a) l -> ForallOrdPairs l -> ForallOrdPairs (a::l). -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. + Hint Constructors ForallOrdPairs. + Lemma ForallOrdPairs_In : forall l, + ForallOrdPairs 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 + (** [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 ForallPairs_ForallOrdPairs l: ForallPairs l -> ForallOrdPairs 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. + Lemma ForallOrdPairs_ForallPairs : + (forall x, R x x) -> + (forall x y, R x y -> R y x) -> + forall l, ForallOrdPairs l -> ForallPairs l. + Proof. + intros Refl Sym l Hl x y Hx Hy. + destruct (ForallOrdPairs_In Hl _ _ Hx Hy); subst; intuition. + Qed. +End ForallPairs. (** * Inversion of predicates over lists based on head symbol *) @@ -1767,3 +2287,28 @@ Notation AllS := Forall (only parsing). (* was formerly in TheoryList *) Hint Resolve app_nil_end : datatypes v62. (* end hide *) + +Section Repeat. + + Variable A : Type. + Fixpoint repeat (x : A) (n: nat ) := + match n with + | O => [] + | S k => x::(repeat x k) + end. + + Theorem repeat_length x n: + length (repeat x n) = n. + Proof. + induction n as [| k Hrec]; simpl; rewrite ?Hrec; reflexivity. + Qed. + + Theorem repeat_spec n x y: + In y (repeat x n) -> y=x. + Proof. + induction n as [|k Hrec]; simpl; destruct 1; auto. + Qed. + +End Repeat. + +(* Unset Universe Polymorphism. *) diff --git a/theories/Lists/ListDec.v b/theories/Lists/ListDec.v new file mode 100644 index 00000000..8bd2daaf --- /dev/null +++ b/theories/Lists/ListDec.v @@ -0,0 +1,103 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(** Decidability results about lists *) + +Require Import List Decidable. +Set Implicit Arguments. + +Definition decidable_eq A := forall x y:A, decidable (x=y). + +Section Dec_in_Prop. +Variables (A:Type)(dec:decidable_eq A). + +Lemma In_decidable x (l:list A) : decidable (In x l). +Proof using A dec. + induction l as [|a l IH]. + - now right. + - destruct (dec a x). + + left. now left. + + destruct IH; simpl; [left|right]; tauto. +Qed. + +Lemma incl_decidable (l l':list A) : decidable (incl l l'). +Proof using A dec. + induction l as [|a l IH]. + - left. inversion 1. + - destruct (In_decidable a l') as [IN|IN]. + + destruct IH as [IC|IC]. + * left. destruct 1; subst; auto. + * right. contradict IC. intros x H. apply IC; now right. + + right. contradict IN. apply IN; now left. +Qed. + +Lemma NoDup_decidable (l:list A) : decidable (NoDup l). +Proof using A dec. + induction l as [|a l IH]. + - left; now constructor. + - destruct (In_decidable a l). + + right. inversion_clear 1. tauto. + + destruct IH. + * left. now constructor. + * right. inversion_clear 1. tauto. +Qed. + +End Dec_in_Prop. + +Section Dec_in_Type. +Variables (A:Type)(dec : forall x y:A, {x=y}+{x<>y}). + +Definition In_dec := List.In_dec dec. (* Already in List.v *) + +Lemma incl_dec (l l':list A) : {incl l l'}+{~incl l l'}. +Proof using A dec. + induction l as [|a l IH]. + - left. inversion 1. + - destruct (In_dec a l') as [IN|IN]. + + destruct IH as [IC|IC]. + * left. destruct 1; subst; auto. + * right. contradict IC. intros x H. apply IC; now right. + + right. contradict IN. apply IN; now left. +Qed. + +Lemma NoDup_dec (l:list A) : {NoDup l}+{~NoDup l}. +Proof using A dec. + induction l as [|a l IH]. + - left; now constructor. + - destruct (In_dec a l). + + right. inversion_clear 1. tauto. + + destruct IH. + * left. now constructor. + * right. inversion_clear 1. tauto. +Qed. + +End Dec_in_Type. + +(** An extra result: thanks to decidability, a list can be purged + from redundancies. *) + +Lemma uniquify_map A B (d:decidable_eq B)(f:A->B)(l:list A) : + exists l', NoDup (map f l') /\ incl (map f l) (map f l'). +Proof. + induction l. + - exists nil. simpl. split; [now constructor | red; trivial]. + - destruct IHl as (l' & N & I). + destruct (In_decidable d (f a) (map f l')). + + exists l'; simpl; split; trivial. + intros x [Hx|Hx]. now subst. now apply I. + + exists (a::l'); simpl; split. + * now constructor. + * intros x [Hx|Hx]. subst; now left. right; now apply I. +Qed. + +Lemma uniquify A (d:decidable_eq A)(l:list A) : + exists l', NoDup l' /\ incl l l'. +Proof. + destruct (uniquify_map d id l) as (l',H). + exists l'. now rewrite !map_id in H. +Qed. diff --git a/theories/Lists/ListSet.v b/theories/Lists/ListSet.v index 37d051a3..0a0bf0de 100644 --- a/theories/Lists/ListSet.v +++ b/theories/Lists/ListSet.v @@ -1,16 +1,18 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(** A Library for finite sets, implemented as lists *) +(** A library for finite sets, implemented as lists *) -(** List is loaded, but not exported. - This allow to "hide" the definitions, functions and theorems of List - and to see only the ones of ListSet *) +(** This is a light implementation of finite sets as lists; for a more + extensive library, you might rather consider MSetWeakList.v. In + addition, if your domain is totally ordered, you might also + consider implementations of finite sets with access in logarithmic + time (e.g. MSetRBT.v which is based on red-black trees). *) Require Import List. @@ -116,7 +118,7 @@ Section first_definitions. simple induction x; simpl; intros. apply H0; red; trivial. case (Aeq_dec a a0); auto with datatypes. - intro; apply H; intros; auto. + intro Hneg; apply H; intros; auto. apply H1; red; intro. case H3; auto. Qed. @@ -147,8 +149,8 @@ Section first_definitions. simple induction x; simpl. tauto. intros a0 l; elim (Aeq_dec a a0). - intros; discriminate H0. - unfold not; intros; elim H1; auto with datatypes. + intros _ _ [=]. + unfold not; intros H H0 H1 [|]; auto with datatypes. Qed. Lemma set_mem_complete2 : @@ -157,7 +159,7 @@ Section first_definitions. simple induction x; simpl. tauto. intros a0 l; elim (Aeq_dec a a0). - intros; elim H0; auto with datatypes. + intros H H0 []; auto with datatypes. tauto. Qed. @@ -204,7 +206,7 @@ Section first_definitions. simpl; do 3 intro. elim (Aeq_dec b a0). simpl; tauto. - simpl; intros; elim H0. + simpl; intros H0 [|]. trivial with datatypes. tauto. tauto. diff --git a/theories/Lists/ListTactics.v b/theories/Lists/ListTactics.v index 64c11cd8..f19d95a9 100644 --- a/theories/Lists/ListTactics.v +++ b/theories/Lists/ListTactics.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/theories/Lists/SetoidList.v b/theories/Lists/SetoidList.v index 0fd1693e..b57c3f04 100644 --- a/theories/Lists/SetoidList.v +++ b/theories/Lists/SetoidList.v @@ -11,7 +11,7 @@ Require Export Sorted. Require Export Setoid Basics Morphisms. Set Implicit Arguments. Unset Strict Implicit. - +(* Set Universe Polymorphism. *) (** * Logical relations over lists with respect to a setoid equality or ordering. *) @@ -34,7 +34,7 @@ Hint Constructors InA. 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. +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. @@ -101,10 +101,12 @@ Proof. split; induction 1; auto. Qed. (** Results concerning lists modulo [eqA] *) Hypothesis eqA_equiv : Equivalence eqA. - -Hint Resolve (@Equivalence_Reflexive _ _ eqA_equiv). -Hint Resolve (@Equivalence_Transitive _ _ eqA_equiv). -Hint Immediate (@Equivalence_Symmetric _ _ eqA_equiv). +Definition eqarefl := (@Equivalence_Reflexive _ _ eqA_equiv). +Definition eqatrans := (@Equivalence_Transitive _ _ eqA_equiv). +Definition eqasym := (@Equivalence_Symmetric _ _ eqA_equiv). + +Hint Resolve eqarefl eqatrans. +Hint Immediate eqasym. Ltac inv := invlist InA; invlist sort; invlist lelistA; invlist NoDupA. @@ -123,7 +125,6 @@ Proof. 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. *) @@ -149,7 +150,7 @@ Qed. Lemma InA_eqA : forall l x y, eqA x y -> InA x l -> InA y l. Proof. - intros l x y H H'. rewrite <- H; auto. + intros l x y H H'. rewrite <- H. auto. Qed. Hint Immediate InA_eqA. @@ -496,7 +497,7 @@ Proof. apply Hrec; auto. inv; auto. eapply NoDupA_split; eauto. - invlist ForallOrdPairs; auto. + invlist ForallOrdPairs; auto. eapply equivlistA_NoDupA_split; eauto. transitivity (f y (fold_right f i (s1++s2))). apply Comp; auto. reflexivity. @@ -545,6 +546,155 @@ Qed. End Fold. + +Section Fold2. + +Variable B:Type. +Variable eqB:B->B->Prop. +Variable st:Equivalence eqB. +Variable f:A->B->B. +Variable Comp:Proper (eqA==>eqB==>eqB) f. + + +Lemma fold_right_eqlistA2 : + forall s s' (i j:B) (heqij: eqB i j) (heqss': eqlistA s s'), + eqB (fold_right f i s) (fold_right f j s'). +Proof. + intros s. + induction s;intros. + - inversion heqss'. + subst. + simpl. + assumption. + - inversion heqss'. + subst. + simpl. + apply Comp. + + assumption. + + apply IHs;assumption. +Qed. + +Section Fold2_With_Restriction. + +Variable R : A -> A -> Prop. +Hypothesis R_sym : Symmetric R. +Hypothesis R_compat : Proper (eqA==>eqA==>iff) R. + +(** Two-argument functions that allow to reorder their arguments. *) +Definition transpose2 (f : A -> B -> B) := + forall (x y : A) (z z': B), eqB z z' -> eqB (f x (f y z)) (f y (f x z')). + +(** A version of transpose with restriction on where it should hold *) +Definition transpose_restr2 (R : A -> A -> Prop)(f : A -> B -> B) := + forall (x y : A) (z z': B), R x y -> eqB z z' -> eqB (f x (f y z)) (f y (f x z')). + +Variable TraR :transpose_restr2 R f. + +Lemma fold_right_commutes_restr2 : + forall s1 s2 x (i j:B) (heqij: eqB i j), ForallOrdPairs R (s1++x::s2) -> + eqB (fold_right f i (s1++x::s2)) (f x (fold_right f j (s1++s2))). +Proof. +induction s1; simpl; auto; intros. +- apply Comp. + + destruct eqA_equiv. apply Equivalence_Reflexive. + + eapply fold_right_eqlistA2. + * assumption. + * reflexivity. +- transitivity (f a (f x (fold_right f j (s1++s2)))). + apply Comp; auto. + eapply IHs1. + assumption. + invlist ForallOrdPairs; auto. + apply TraR. + invlist ForallOrdPairs; auto. + rewrite Forall_forall in H0; apply H0. + apply in_or_app; simpl; auto. + reflexivity. +Qed. + +Lemma fold_right_equivlistA_restr2 : + forall s s' (i j:B) (heqij: eqB i j), + NoDupA s -> NoDupA s' -> ForallOrdPairs R s -> + eqB i j -> + equivlistA s s' -> eqB (fold_right f i s) (fold_right f j s'). +Proof. + simple induction s. + destruct s'; simpl. + intros. assumption. + unfold equivlistA; intros. + destruct (H3 a). + assert (InA a nil) by auto; inv. + intros x l Hrec s' i j heqij N N' F eqij E; simpl in *. + 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 j (s1++s2))). + - apply Comp; auto. + apply Hrec; auto. + inv; auto. + eapply NoDupA_split; eauto. + invlist ForallOrdPairs; auto. + eapply equivlistA_NoDupA_split; eauto. + - transitivity (f y (fold_right f i (s1++s2))). + + apply Comp; auto. + symmetry. + apply fold_right_eqlistA2. + * assumption. + * reflexivity. + + symmetry. + apply fold_right_commutes_restr2. + symmetry. + assumption. + apply ForallOrdPairs_inclA with (x::l); auto. + red; intros; rewrite E; auto. +Qed. + + +Lemma fold_right_add_restr2 : + forall s' s i j x, NoDupA s -> NoDupA s' -> eqB i j -> ForallOrdPairs R s' -> ~ InA x s -> + equivlistA s' (x::s) -> eqB (fold_right f i s') (f x (fold_right f j s)). +Proof. + intros; apply (@fold_right_equivlistA_restr2 s' (x::s) i j); auto. +Qed. + +End Fold2_With_Restriction. + +Variable Tra :transpose2 f. + +Lemma fold_right_commutes2 : forall s1 s2 i x x', + eqA x x' -> + eqB (fold_right f i (s1++x::s2)) (f x' (fold_right f i (s1++s2))). +Proof. + induction s1;simpl;intros. +- apply Comp;auto. + reflexivity. +- transitivity (f a (f x' (fold_right f i (s1++s2)))); auto. + + apply Comp;auto. + + apply Tra. + reflexivity. +Qed. + +Lemma fold_right_equivlistA2 : + forall s s' i j, NoDupA s -> NoDupA s' -> eqB i j -> + equivlistA s s' -> eqB (fold_right f i s) (fold_right f j s'). +Proof. +red in Tra. +intros; apply fold_right_equivlistA_restr2 with (R:=fun _ _ => True); +repeat red; auto. +apply ForallPairs_ForallOrdPairs; try red; auto. +Qed. + +Lemma fold_right_add2 : + forall s' s i j x, NoDupA s -> NoDupA s' -> eqB i j -> ~ InA x s -> + equivlistA s' (x::s) -> eqB (fold_right f i s') (f x (fold_right f j s)). +Proof. + intros. + replace (f x (fold_right f j s)) with (fold_right f j (x::s)) by auto. + eapply fold_right_equivlistA2;auto. +Qed. + +End Fold2. + Section Remove. Hypothesis eqA_dec : forall x y : A, {eqA x y}+{~(eqA x y)}. @@ -582,14 +732,14 @@ split. intro; inv. destruct 1; inv. intros. -destruct (eqA_dec x a); simpl; auto. +destruct (eqA_dec x a) as [Heq|Hnot]; simpl; auto. rewrite IHl; split; destruct 1; split; auto. inv; auto. destruct H0; transitivity a; auto. split. intro; inv. split; auto. -contradict n. +contradict Hnot. transitivity y; auto. rewrite (IHl x y) in H0; destruct H0; auto. destruct 1; inv; auto. @@ -633,7 +783,9 @@ Variable ltA : A -> A -> Prop. Hypothesis ltA_strorder : StrictOrder ltA. Hypothesis ltA_compat : Proper (eqA==>eqA==>iff) ltA. -Hint Resolve (@StrictOrder_Transitive _ _ ltA_strorder). +Let sotrans := (@StrictOrder_Transitive _ _ ltA_strorder). + +Hint Resolve sotrans. Notation InfA:=(lelistA ltA). Notation SortA:=(sort ltA). @@ -647,7 +799,7 @@ Proof. Qed. Global Instance InfA_compat : Proper (eqA==>eqlistA==>iff) InfA. -Proof. +Proof using eqA_equiv ltA_compat. (* and not ltA_strorder *) intros x x' Hxx' l l' Hll'. inversion_clear Hll'. intuition. @@ -658,7 +810,7 @@ Qed. (** For compatibility, can be deduced from [InfA_compat] *) Lemma InfA_eqA l x y : eqA x y -> InfA y l -> InfA x l. -Proof. +Proof using eqA_equiv ltA_compat. intros H; now rewrite H. Qed. Hint Immediate InfA_ltA InfA_eqA. @@ -759,7 +911,7 @@ 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)). +rewrite <- (app_nil_r (rev x)), <- (app_nil_r (rev y)). apply eqlistA_rev_app; auto. Qed. @@ -815,13 +967,12 @@ intros. rewrite filter_In in H; destruct H. eapply SortA_InfA_InA; eauto. Qed. - Arguments eq {A} x _. 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. +clear sotrans ltA ltA_strorder ltA_compat. 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. @@ -888,9 +1039,9 @@ split; intros. invlist InA. compute in H2; destruct H2. subst b'. destruct (eqA_dec a a'); intuition. -destruct (eqA_dec a a'); simpl. +destruct (eqA_dec a a') as [HeqA|]; simpl. contradict H0. -revert e H2; clear - eqA_equiv. +revert HeqA H2; clear - eqA_equiv. induction l. intros; invlist InA. intros; invlist InA; auto. diff --git a/theories/Lists/SetoidPermutation.v b/theories/Lists/SetoidPermutation.v index b0657b63..afc7c25b 100644 --- a/theories/Lists/SetoidPermutation.v +++ b/theories/Lists/SetoidPermutation.v @@ -7,6 +7,7 @@ (***********************************************************************) Require Import SetoidList. +(* Set Universe Polymorphism. *) Set Implicit Arguments. Unset Strict Implicit. @@ -88,7 +89,7 @@ Lemma PermutationA_cons_app l l₁ l₂ x : PermutationA l (l₁ ++ l₂) -> PermutationA (x :: l) (l₁ ++ x :: l₂). Proof. intros E. rewrite E. - now rewrite app_comm_cons, PermutationA_cons_append, <-app_assoc. + now rewrite app_comm_cons, (PermutationA_cons_append l₁ x), <- app_assoc. Qed. Lemma PermutationA_middle l₁ l₂ x : diff --git a/theories/Lists/StreamMemo.v b/theories/Lists/StreamMemo.v index fd5ab100..74d464c5 100644 --- a/theories/Lists/StreamMemo.v +++ b/theories/Lists/StreamMemo.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/theories/Lists/Streams.v b/theories/Lists/Streams.v index fa9b7873..cc4fb179 100644 --- a/theories/Lists/Streams.v +++ b/theories/Lists/Streams.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/theories/Lists/vo.itarget b/theories/Lists/vo.itarget index 04994f59..82dd1be8 100644 --- a/theories/Lists/vo.itarget +++ b/theories/Lists/vo.itarget @@ -1,6 +1,7 @@ ListSet.vo ListTactics.vo List.vo +ListDec.vo SetoidList.vo SetoidPermutation.vo StreamMemo.vo |