From a4c7f8bd98be2a200489325ff7c5061cf80ab4f3 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Tue, 27 Dec 2016 16:53:30 +0100 Subject: Imported Upstream version 8.6 --- theories/Lists/List.v | 117 ++++++++++++++++++++++++++++++++++++++--------- theories/Lists/ListSet.v | 109 +++++++++++++++++++++++++++++++++++++++++-- theories/Lists/Streams.v | 2 +- 3 files changed, 202 insertions(+), 26 deletions(-) (limited to 'theories/Lists') diff --git a/theories/Lists/List.v b/theories/Lists/List.v index cc7586fe..30f1dec2 100644 --- a/theories/Lists/List.v +++ b/theories/Lists/List.v @@ -7,7 +7,7 @@ (************************************************************************) Require Setoid. -Require Import PeanoNat Le Gt Minus Bool. +Require Import PeanoNat Le Gt Minus Bool Lt. Set Implicit Arguments. (* Set Universe Polymorphism. *) @@ -21,12 +21,13 @@ Set Implicit Arguments. Open Scope list_scope. -(** Standard notations for lists. +(** 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. +Notation "[ ]" := nil (format "[ ]") : list_scope. +Notation "[ x ]" := (cons x nil) : list_scope. +Notation "[ x ; y ; .. ; z ]" := (cons x (cons y .. (cons z nil) ..)) : list_scope. +Notation "[ x ; .. ; y ]" := (cons x .. (cons y nil) ..) (compat "8.4") : list_scope. End ListNotations. Import ListNotations. @@ -195,7 +196,7 @@ Section Facts. Qed. Theorem app_nil_r : forall l:list A, l ++ [] = l. - Proof. + Proof. induction l; simpl; f_equal; auto. Qed. @@ -248,8 +249,7 @@ Section Facts. generalize (app_nil_r l); intros E. rewrite -> E; auto. intros. - injection H. - intro. + injection H as H H0. assert ([] = l ++ a0 :: l0) by auto. apply app_cons_not_nil in H1 as []. Qed. @@ -335,16 +335,16 @@ Section Facts. absurd (length (x1 :: l1 ++ l) <= length l). simpl; rewrite app_length; auto with arith. rewrite H; auto with arith. - injection H; clear H; intros; f_equal; eauto. + injection H as H H0; f_equal; eauto. Qed. End Facts. -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 in_eq in_cons in_inv in_nil in_app_or in_or_app: datatypes v62. +Hint Resolve app_assoc app_assoc_reverse: datatypes. +Hint Resolve app_comm_cons app_cons_not_nil: datatypes. +Hint Immediate app_eq_nil: datatypes. +Hint Resolve app_eq_unit app_inj_tail: datatypes. +Hint Resolve in_eq in_cons in_inv in_nil in_app_or in_or_app: datatypes. @@ -518,7 +518,7 @@ Section Elts. 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. + - exists nil; exists l. now injection H as ->. - destruct (IH _ H) as (l1 & l2 & H1 & H2). exists (x::l1); exists l2; simpl; split; now f_equal. Qed. @@ -1385,9 +1385,8 @@ End Fold_Right_Recursor. 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. - injection H; clear H; intros. - rewrite IHl; auto. + induction l, l'; simpl; trivial; try discriminate. + now intros [= ->%IHl]. Qed. Lemma in_combine_l : forall (l:list A)(l':list B)(x:A)(y:B), @@ -1471,7 +1470,7 @@ End Fold_Right_Recursor. destruct (in_app_or _ _ _ H); clear H. destruct (in_map_iff (fun y : B => (a, y)) l' (x,y)) as (H1,_). destruct (H1 H0) as (z,(H2,H3)); clear H0 H1. - injection H2; clear H2; intros; subst; intuition. + injection H2 as -> ->; intuition. intuition. Qed. @@ -1545,7 +1544,7 @@ Section length_order. End length_order. Hint Resolve lel_refl lel_cons_cons lel_cons lel_nil lel_nil nil_cons: - datatypes v62. + datatypes. (******************************) @@ -1614,7 +1613,7 @@ Section SetIncl. End SetIncl. Hint Resolve incl_refl incl_tl incl_tran incl_appl incl_appr incl_cons - incl_app: datatypes v62. + incl_app: datatypes. (**************************************) @@ -1634,6 +1633,80 @@ Section Cutting. end end. + Lemma firstn_nil n: firstn n [] = []. + Proof. induction n; now simpl. Qed. + + Lemma firstn_cons n a l: firstn (S n) (a::l) = a :: (firstn n l). + Proof. now simpl. Qed. + + Lemma firstn_all l: firstn (length l) l = l. + Proof. induction l as [| ? ? H]; simpl; [reflexivity | now rewrite H]. Qed. + + Lemma firstn_all2 n: forall (l:list A), (length l) <= n -> firstn n l = l. + Proof. induction n as [|k iHk]. + - intro. inversion 1 as [H1|?]. + rewrite (length_zero_iff_nil l) in H1. subst. now simpl. + - destruct l as [|x xs]; simpl. + * now reflexivity. + * simpl. intro H. apply Peano.le_S_n in H. f_equal. apply iHk, H. + Qed. + + Lemma firstn_O l: firstn 0 l = []. + Proof. now simpl. Qed. + + Lemma firstn_le_length n: forall l:list A, length (firstn n l) <= n. + Proof. + induction n as [|k iHk]; simpl; [auto | destruct l as [|x xs]; simpl]. + - auto with arith. + - apply Peano.le_n_S, iHk. + Qed. + + Lemma firstn_length_le: forall l:list A, forall n:nat, + n <= length l -> length (firstn n l) = n. + Proof. induction l as [|x xs Hrec]. + - simpl. intros n H. apply le_n_0_eq in H. rewrite <- H. now simpl. + - destruct n. + * now simpl. + * simpl. intro H. apply le_S_n in H. now rewrite (Hrec n H). + Qed. + + Lemma firstn_app n: + forall l1 l2, + firstn n (l1 ++ l2) = (firstn n l1) ++ (firstn (n - length l1) l2). + Proof. induction n as [|k iHk]; intros l1 l2. + - now simpl. + - destruct l1 as [|x xs]. + * unfold firstn at 2, length. now rewrite 2!app_nil_l, <- minus_n_O. + * rewrite <- app_comm_cons. simpl. f_equal. apply iHk. + Qed. + + Lemma firstn_app_2 n: + forall l1 l2, + firstn ((length l1) + n) (l1 ++ l2) = l1 ++ firstn n l2. + Proof. induction n as [| k iHk];intros l1 l2. + - unfold firstn at 2. rewrite <- plus_n_O, app_nil_r. + rewrite firstn_app. rewrite <- minus_diag_reverse. + unfold firstn at 2. rewrite app_nil_r. apply firstn_all. + - destruct l2 as [|x xs]. + * simpl. rewrite app_nil_r. apply firstn_all2. auto with arith. + * rewrite firstn_app. assert (H0 : (length l1 + S k - length l1) = S k). + auto with arith. + rewrite H0, firstn_all2; [reflexivity | auto with arith]. + Qed. + + Lemma firstn_firstn: + forall l:list A, + forall i j : nat, + firstn i (firstn j l) = firstn (min i j) l. + Proof. induction l as [|x xs Hl]. + - intros. simpl. now rewrite ?firstn_nil. + - destruct i. + * intro. now simpl. + * destruct j. + + now simpl. + + simpl. f_equal. apply Hl. + Qed. + Fixpoint skipn (n:nat)(l:list A) : list A := match n with | 0 => l @@ -2292,7 +2365,7 @@ 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. +Hint Resolve app_nil_end : datatypes. (* end hide *) Section Repeat. diff --git a/theories/Lists/ListSet.v b/theories/Lists/ListSet.v index fd0464fb..655d3940 100644 --- a/theories/Lists/ListSet.v +++ b/theories/Lists/ListSet.v @@ -48,7 +48,11 @@ Section first_definitions. end end. - (** If [a] belongs to [x], removes [a] from [x]. If not, does nothing *) + (** If [a] belongs to [x], removes [a] from [x]. If not, does nothing. + Invariant: any element should occur at most once in [x], see for + instance [set_add]. We hence remove here only the first occurrence + of [a] in [x]. *) + Fixpoint set_remove (a:A) (x:set) : set := match x with | nil => empty_set @@ -227,6 +231,68 @@ Section first_definitions. intros; elim (Aeq_dec a a0); intros; discriminate. Qed. + Lemma set_add_iff a b l : In a (set_add b l) <-> a = b \/ In a l. + Proof. + split. apply set_add_elim. apply set_add_intro. + Qed. + + Lemma set_add_nodup a l : NoDup l -> NoDup (set_add a l). + Proof. + induction 1 as [|x l H H' IH]; simpl. + - constructor; [ tauto | constructor ]. + - destruct (Aeq_dec a x) as [<-|Hax]; constructor; trivial. + rewrite set_add_iff. intuition. + Qed. + + Lemma set_remove_1 (a b : A) (l : set) : + In a (set_remove b l) -> In a l. + Proof. + induction l as [|x xs Hrec]. + - intros. auto. + - simpl. destruct (Aeq_dec b x). + * tauto. + * intro H. destruct H. + + rewrite H. apply in_eq. + + apply in_cons. apply Hrec. assumption. + Qed. + + Lemma set_remove_2 (a b:A) (l : set) : + NoDup l -> In a (set_remove b l) -> a <> b. + Proof. + induction l as [|x l IH]; intro ND; simpl. + - tauto. + - inversion_clear ND. + destruct (Aeq_dec b x) as [<-|Hbx]. + + congruence. + + destruct 1; subst; auto. + Qed. + + Lemma set_remove_3 (a b : A) (l : set) : + In a l -> a <> b -> In a (set_remove b l). + Proof. + induction l as [|x xs Hrec]. + - now simpl. + - simpl. destruct (Aeq_dec b x) as [<-|Hbx]; simpl; intuition. + congruence. + Qed. + + Lemma set_remove_iff (a b : A) (l : set) : + NoDup l -> (In a (set_remove b l) <-> In a l /\ a <> b). + Proof. + split; try split. + - eapply set_remove_1; eauto. + - eapply set_remove_2; eauto. + - destruct 1; apply set_remove_3; auto. + Qed. + + Lemma set_remove_nodup a l : NoDup l -> NoDup (set_remove a l). + Proof. + induction 1 as [|x l H H' IH]; simpl. + - constructor. + - destruct (Aeq_dec a x) as [<-|Hax]; trivial. + constructor; trivial. + rewrite set_remove_iff; trivial. intuition. + Qed. Lemma set_union_intro1 : forall (a:A) (x y:set), set_In a x -> set_In a (set_union x y). @@ -264,18 +330,26 @@ Section first_definitions. tauto. Qed. + Lemma set_union_iff a l l': In a (set_union l l') <-> In a l \/ In a l'. + Proof. + split. apply set_union_elim. apply set_union_intro. + Qed. + + Lemma set_union_nodup l l' : NoDup l -> NoDup l' -> NoDup (set_union l l'). + Proof. + induction 2 as [|x' l' ? ? IH]; simpl; trivial. now apply set_add_nodup. + Qed. + Lemma set_union_emptyL : forall (a:A) (x:set), set_In a (set_union empty_set x) -> set_In a x. intros a x H; case (set_union_elim _ _ _ H); auto || contradiction. Qed. - Lemma set_union_emptyR : forall (a:A) (x:set), set_In a (set_union x empty_set) -> set_In a x. intros a x H; case (set_union_elim _ _ _ H); auto || contradiction. Qed. - Lemma set_inter_intro : forall (a:A) (x y:set), set_In a x -> set_In a y -> set_In a (set_inter x y). @@ -326,6 +400,21 @@ Section first_definitions. eauto with datatypes. Qed. + Lemma set_inter_iff a l l' : In a (set_inter l l') <-> In a l /\ In a l'. + Proof. + split. + - apply set_inter_elim. + - destruct 1. now apply set_inter_intro. + Qed. + + Lemma set_inter_nodup l l' : NoDup l -> NoDup l' -> NoDup (set_inter l l'). + Proof. + induction 1 as [|x l H H' IH]; intro Hl'; simpl. + - constructor. + - destruct (set_mem x l'); auto. + constructor; auto. rewrite set_inter_iff; tauto. + Qed. + Lemma set_diff_intro : forall (a:A) (x y:set), set_In a x -> ~ set_In a y -> set_In a (set_diff x y). @@ -360,6 +449,20 @@ Section first_definitions. rewrite H; trivial. Qed. + Lemma set_diff_iff a l l' : In a (set_diff l l') <-> In a l /\ ~In a l'. + Proof. + split. + - split; [eapply set_diff_elim1 | eapply set_diff_elim2]; eauto. + - destruct 1. now apply set_diff_intro. + Qed. + + Lemma set_diff_nodup l l' : NoDup l -> NoDup l' -> NoDup (set_diff l l'). + Proof. + induction 1 as [|x l H H' IH]; intro Hl'; simpl. + - constructor. + - destruct (set_mem x l'); auto using set_add_nodup. + Qed. + Lemma set_diff_trivial : forall (a:A) (x:set), ~ set_In a (set_diff x x). red; intros a x H. apply (set_diff_elim2 _ _ _ H). diff --git a/theories/Lists/Streams.v b/theories/Lists/Streams.v index 7ec3d250..1c302b22 100644 --- a/theories/Lists/Streams.v +++ b/theories/Lists/Streams.v @@ -51,7 +51,7 @@ Lemma tl_nth_tl : Proof. simple induction n; simpl; auto. Qed. -Hint Resolve tl_nth_tl: datatypes v62. +Hint Resolve tl_nth_tl: datatypes. Lemma Str_nth_tl_plus : forall (n m:nat) (s:Stream), -- cgit v1.2.3