diff options
| -rw-r--r-- | doc/changelog/10-standard-library/13986-clean-List-imports.rst | 4 | ||||
| -rw-r--r-- | theories/Lists/List.v | 210 | ||||
| -rw-r--r-- | theories/MSets/MSetGenTree.v | 1 |
3 files changed, 108 insertions, 107 deletions
diff --git a/doc/changelog/10-standard-library/13986-clean-List-imports.rst b/doc/changelog/10-standard-library/13986-clean-List-imports.rst new file mode 100644 index 0000000000..02e7b9cc97 --- /dev/null +++ b/doc/changelog/10-standard-library/13986-clean-List-imports.rst @@ -0,0 +1,4 @@ +- **Removed:** + from ``List.v`` deprecated/unexpected dependencies ``Setoid``, ``Le``, ``Gt``, ``Minus``, ``Lt`` + (`#13986 <https://github.com/coq/coq/pull/13986>`_, + by Andrej Dudenhefner). diff --git a/theories/Lists/List.v b/theories/Lists/List.v index dbc79f090b..2a5eb2db39 100644 --- a/theories/Lists/List.v +++ b/theories/Lists/List.v @@ -8,8 +8,7 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) -Require Setoid. -Require Import PeanoNat Le Gt Minus Bool Lt. +Require Import PeanoNat Bool. Set Implicit Arguments. (* Set Universe Polymorphism. *) @@ -264,15 +263,13 @@ Section Facts. forall l l1 l2 : list A, l1 ++ l = l2 ++ l -> l1 = l2. Proof. intros l l1 l2; revert l1 l2 l. - intro l1; induction l1 as [ | x1 l1]; intro l2; destruct l2 as [ | x2 l2]; - simpl; auto; intros l H. - absurd (length (x2 :: l2 ++ l) <= length l). - simpl; rewrite app_length; auto with arith. - rewrite <- H; auto with arith. - absurd (length (x1 :: l1 ++ l) <= length l). - simpl; rewrite app_length; auto with arith. - rewrite H; auto with arith. - injection H as [= H H0]; f_equal; eauto. + intro l1; induction l1 as [ | x1 l1]; intro l2; destruct l2 as [ | x2 l2]. + - now intros. + - intros l Hl. apply (f_equal (@length A)) in Hl. + now rewrite ?app_length, Nat.add_cancel_r in Hl. + - intros l Hl. apply (f_equal (@length A)) in Hl. + now rewrite ?app_length, Nat.add_cancel_r in Hl. + - intros l [=H1 H2 %IHl1]. now subst. Qed. Lemma app_inv_tail_iff: @@ -472,7 +469,7 @@ Section Elts. - destruct l; simpl; [ inversion 2 | auto ]. - destruct l; simpl. * inversion 2. - * intros d ie; right; apply hn; auto with arith. + * intros d ie; right; apply hn. now apply Nat.succ_le_mono. Qed. Lemma In_nth l x d : In x l -> @@ -481,9 +478,9 @@ Section Elts. induction l as [|a l IH]. - easy. - intros [H|H]. - * subst; exists 0; simpl; auto with arith. + * subst; exists 0; simpl; auto using Nat.lt_0_succ. * destruct (IH H) as (n & Hn & Hn'). - exists (S n); simpl; auto with arith. + apply Nat.succ_lt_mono in Hn. now exists (S n). Qed. Lemma nth_overflow : forall l n d, length l <= n -> nth n l d = d. @@ -491,7 +488,7 @@ Section Elts. intro l; induction l as [|? ? IHl]; intro n; destruct n; simpl; intros d H; auto. - inversion H. - - apply IHl; auto with arith. + - apply IHl. now apply Nat.succ_le_mono. Qed. Lemma nth_indep : @@ -499,7 +496,8 @@ Section Elts. Proof. intro l; induction l. - inversion 1. - - intros [|n] d d'; simpl; auto with arith. + - intros [|n] d d'; [intros; reflexivity|]. + intros H. apply IHl. now apply Nat.succ_lt_mono. Qed. Lemma app_nth1 : @@ -507,7 +505,8 @@ Section Elts. Proof. intro l; induction l. - inversion 1. - - intros l' d [|n]; simpl; auto with arith. + - intros l' d [|n]; simpl; [intros; reflexivity|]. + intros H. apply IHl. now apply Nat.succ_lt_mono. Qed. Lemma app_nth2 : @@ -515,15 +514,15 @@ Section Elts. Proof. intro l; induction l as [|? ? IHl]; intros l' d [|n]; auto. - inversion 1. - - intros; simpl; rewrite IHl; auto with arith. + - intros; simpl; rewrite IHl; [reflexivity|now apply Nat.succ_le_mono]. Qed. Lemma app_nth2_plus : forall l l' d n, nth (length l + n) (l ++ l') d = nth n l' d. Proof. intros. - rewrite app_nth2, minus_plus; trivial. - auto with arith. + rewrite app_nth2, Nat.add_comm, Nat.add_sub; trivial. + now apply Nat.le_add_r. Qed. Lemma nth_middle : forall l l' a d, @@ -540,7 +539,7 @@ Section Elts. 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. + - destruct (IH l) as (l1 & l2 & Hl & Hl1); [now apply Nat.succ_lt_mono|]. exists (a::l1); exists l2; simpl; split; now f_equal. Qed. @@ -557,7 +556,7 @@ Section Elts. rewrite Hnth; f_equal. + apply IHl with d d'; [ now inversion Hlen | ]. intros n Hlen'; apply (Hnth (S n)). - now simpl; apply lt_n_S. + now apply (Nat.succ_lt_mono n (length l)). + simpl; apply Nat.lt_0_succ. Qed. @@ -575,18 +574,18 @@ Section Elts. induction l as [|a l IH]. - easy. - intros [H|H]. - * subst; exists 0; simpl; auto with arith. + * subst; now exists 0. * destruct (IH H) as (n,Hn). - exists (S n); simpl; auto with arith. + now exists (S n). Qed. Lemma nth_error_None l n : nth_error l n = None <-> length l <= n. Proof. revert n. induction l as [|? ? IHl]; intro n; destruct n; simpl. - split; auto. - - split; auto with arith. - - split; now auto with arith. - - rewrite IHl; split; auto with arith. + - now split; intros; [apply Nat.le_0_l|]. + - now split; [|intros ? %Nat.nle_succ_0]. + - now rewrite IHl, Nat.succ_le_mono. Qed. Lemma nth_error_Some l n : nth_error l n <> None <-> n < length l. @@ -594,8 +593,8 @@ Section Elts. revert n. induction l as [|? ? IHl]; intro n; 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. + - now split; intros; [apply Nat.lt_0_succ|]. + - now rewrite IHl, Nat.succ_lt_mono. Qed. Lemma nth_error_split l n a : nth_error l n = Some a -> @@ -613,7 +612,7 @@ Section Elts. Proof. revert l. induction n as [|n IHn]; intros [|a l] H; auto; try solve [inversion H]. - simpl in *. apply IHn. auto with arith. + simpl in *. apply IHn. now apply Nat.succ_lt_mono. Qed. Lemma nth_error_app2 l l' n : length l <= n -> @@ -621,7 +620,7 @@ Section Elts. Proof. revert l. induction n as [|n IHn]; intros [|a l] H; auto; try solve [inversion H]. - simpl in *. apply IHn. auto with arith. + simpl in *. apply IHn. now apply Nat.succ_le_mono. Qed. (** Results directly relating [nth] and [nth_error] *) @@ -841,8 +840,9 @@ Section Elts. Theorem count_occ_In l x : In x l <-> count_occ l x > 0. Proof. induction l as [|y l IHl]; simpl. - - split; [destruct 1 | apply gt_irrefl]. + - split; [destruct 1 | apply Nat.nlt_0_r]. - destruct eq_dec as [->|Hneq]; rewrite IHl; intuition. + now apply Nat.lt_0_succ. Qed. Theorem count_occ_not_In l x : ~ In x l <-> count_occ l x = 0. @@ -990,26 +990,22 @@ 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. intro l; induction l as [|a l IHl]. - intros d n H; inversion H. - intros ? n H. - simpl in H. - simpl (rev (a :: l)). - simpl (length (a :: l) - S n). - inversion H. - rewrite <- minus_n_n; simpl. - rewrite <- rev_length. - rewrite app_nth2; auto. - rewrite <- minus_n_n; auto. - rewrite app_nth1; auto. - rewrite (minus_plus_simpl_l_reverse (length l) n 1). - replace (1 + length l) with (S (length l)); auto with arith. - rewrite <- minus_Sn_m; auto with arith. - apply IHl ; auto with arith. - rewrite rev_length; auto. + - intros d n H; inversion H. + - intros ? n H. simpl in H. + inversion H. + + rewrite Nat.sub_diag; simpl. + rewrite <- rev_length. + rewrite app_nth2; auto. + now rewrite Nat.sub_diag. + + simpl. rewrite app_nth1; [|now rewrite rev_length]. + rewrite IHl; [|eassumption]. + destruct (length l); [exfalso; now apply (Nat.nlt_0_r n)|]. + rewrite (Nat.sub_succ_l n); [reflexivity|]. + now apply Nat.succ_le_mono. Qed. @@ -1360,7 +1356,7 @@ Proof. + inversion Hlen. + now rewrite nth_overflow; destruct n. - destruct n; simpl; [ reflexivity | apply IHln ]. - destruct Hlen; [ left; apply lt_S_n | right ]; assumption. + destruct Hlen; [ left; apply Nat.succ_lt_mono | right ]; assumption. Qed. @@ -1396,8 +1392,7 @@ Proof. intros A l. enough (H : forall n, fold_left (fun x _ => S x) l n = n + length l) by exact (H 0). induction l as [|? ? IHl]; simpl; auto. - intros; rewrite IHl. - simpl; auto with arith. + now intros; rewrite IHl, Nat.add_succ_r. Qed. (************************************) @@ -1502,7 +1497,7 @@ End Fold_Right_Recursor. simpl; intros n ? ? H0. destruct (orb_false_elim _ _ H0); clear H0; auto. destruct n ; auto. - rewrite IHl; auto with arith. + rewrite IHl; auto. now apply Nat.succ_lt_mono. Qed. Lemma existsb_app : forall l1 l2, @@ -1938,37 +1933,35 @@ Section length_order. Lemma lel_refl : lel l l. Proof. - unfold lel; auto with arith. + now apply Nat.le_refl. Qed. Lemma lel_trans : lel l m -> lel m n -> lel l n. Proof. unfold lel; intros. now_show (length l <= length n). - apply le_trans with (length m); auto with arith. + now apply Nat.le_trans with (length m). Qed. Lemma lel_cons_cons : lel l m -> lel (a :: l) (b :: m). Proof. - unfold lel; simpl; auto with arith. + now intros ? %Nat.succ_le_mono. Qed. Lemma lel_cons : lel l m -> lel l (b :: m). Proof. - unfold lel; simpl; auto with arith. + intros. now apply Nat.le_le_succ_r. Qed. Lemma lel_tail : lel (a :: l) (b :: m) -> lel l m. Proof. - unfold lel; simpl; auto with arith. + intros. now apply Nat.succ_le_mono. Qed. Lemma lel_nil : forall l':list A, lel l' nil -> nil = l'. Proof. - intro l'; elim l'; auto with arith. - intros a' y H H0. - now_show (nil = a' :: y). - absurd (S (length y) <= 0); auto with arith. + intro l'; elim l'; [now intros|]. + now intros a' y H H0 %Nat.nle_succ_0. Qed. End length_order. @@ -2143,7 +2136,7 @@ Section Cutting. rewrite (length_zero_iff_nil l) in H1. subst. now simpl. - intro l; destruct l as [|x xs]; simpl. * now reflexivity. - * simpl. intro H. apply Peano.le_S_n in H. f_equal. apply iHk, H. + * simpl. intro H. f_equal. apply iHk. now apply Nat.succ_le_mono. Qed. Lemma firstn_O l: firstn 0 l = []. @@ -2152,17 +2145,17 @@ Section Cutting. Lemma firstn_le_length n: forall l:list A, length (firstn n l) <= n. Proof. induction n as [|k iHk]; simpl; [auto | intro l; destruct l as [|x xs]; simpl]. - - auto with arith. - - apply Peano.le_n_S, iHk. + - now apply Nat.le_0_l. + - now rewrite <- Nat.succ_le_mono. Qed. Lemma firstn_length_le: forall l:list A, forall n:nat, n <= length l -> length (firstn n l) = n. Proof. intro l; induction l as [|x xs Hrec]. - - simpl. intros n H. apply le_n_0_eq in H. rewrite <- H. now simpl. + - simpl. intros n H. apply Nat.le_0_r in H. now subst. - intro n; destruct n as [|n]. * now simpl. - * simpl. intro H. apply le_S_n in H. now rewrite (Hrec n H). + * simpl. intro H. f_equal. apply Hrec. now apply Nat.succ_le_mono. Qed. Lemma firstn_app n: @@ -2171,7 +2164,7 @@ Section Cutting. 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. + * reflexivity. * rewrite <- app_comm_cons. simpl. f_equal. apply iHk. Qed. @@ -2180,13 +2173,13 @@ Section Cutting. 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. + rewrite firstn_app. rewrite Nat.sub_diag. 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. + * simpl. rewrite app_nil_r. apply firstn_all2. now apply Nat.le_add_r. * rewrite firstn_app. assert (H0 : (length l1 + S k - length l1) = S k). - auto with arith. - rewrite H0, firstn_all2; [reflexivity | auto with arith]. + now rewrite Nat.add_comm, Nat.add_sub. + rewrite H0, firstn_all2; [reflexivity | now apply Nat.le_add_r]. Qed. Lemma firstn_firstn: @@ -2287,11 +2280,7 @@ Section Cutting. destruct (Nat.le_ge_cases (length (rev l)) x) as [L | L]. - rewrite skipn_all2; [apply Nat.sub_0_le in L | trivial]. now rewrite L, Nat.sub_0_r, skipn_all. - - replace (length (rev l) - (length (rev l) - x)) - with (length (rev l) + x - length (rev l)). - rewrite minus_plus. reflexivity. - rewrite <- (Nat.sub_add _ _ L) at 2. - now rewrite <-!(Nat.add_comm x), <-minus_plus_simpl_l_reverse. + - f_equal. now apply Nat.eq_sym, Nat.add_sub_eq_l, Nat.sub_add. Qed. Lemma removelast_firstn : forall n l, n < length l -> @@ -2306,7 +2295,7 @@ Section Cutting. change (firstn (S (S n)) (a::l)) with ((a::nil)++firstn (S n) l). change (firstn (S n) (a::l)) with (a::firstn n l). rewrite removelast_app. - rewrite IHn; auto with arith. + rewrite IHn; [reflexivity|now apply Nat.succ_le_mono]. clear IHn; destruct l; simpl in *; try discriminate. inversion_clear H as [|? H1]. @@ -2331,7 +2320,7 @@ Section Cutting. simpl in H. change (removelast (a :: l)) with (removelast ((a::nil)++l)). rewrite removelast_app. - simpl; f_equal; auto with arith. + simpl; f_equal. apply IHn. now apply Nat.succ_lt_mono. intro H0; rewrite H0 in H; inversion_clear H as [|? H1]; inversion_clear H1. Qed. @@ -2423,7 +2412,7 @@ Section Add. Lemma Add_length a l l' : Add a l l' -> length l' = S (length l). Proof. - induction 1; simpl; auto with arith. + induction 1; simpl; now auto. Qed. Lemma Add_inv a l : In a l -> exists l', Add a l' l. @@ -2602,13 +2591,13 @@ Section ReDun. - 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. } + * f_equal. now apply IH;[apply Nat.succ_lt_mono|]. } { induction l as [|a l IHl]; 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. + specialize (H 0 (S n)). simpl in H. now discriminate H; [apply Nat.lt_0_succ|]. * apply IHl. - intros i j Hi E. apply eq_add_S, H; simpl; auto with arith. } + intros i j Hi %Nat.succ_lt_mono E. now apply eq_add_S, H. } Qed. Lemma NoDup_nth l d : @@ -2620,14 +2609,17 @@ Section ReDun. { 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. } + * elim Hal. subst a. now apply nth_In, Nat.succ_lt_mono. + * elim Hal. subst a. now apply nth_In, Nat.succ_lt_mono. + * f_equal. apply IH; [| |assumption]; now apply Nat.succ_lt_mono. } { induction l as [|a l IHl]; 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. + specialize (H 0 (S n)). simpl in H. + apply Nat.succ_lt_mono in Hn. + discriminate H; eauto using Nat.lt_0_succ. * apply IHl. - intros i j Hi Hj E. apply eq_add_S, H; simpl; auto with arith. } + intros i j Hi %Nat.succ_lt_mono Hj %Nat.succ_lt_mono E. + now apply eq_add_S, H. } Qed. (** Having [NoDup] hypotheses bring more precise facts about [incl]. *) @@ -2636,7 +2628,7 @@ Section ReDun. 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. now apply Nat.le_0_l. - 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. @@ -2653,7 +2645,7 @@ Section ReDun. 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). + * apply Nat.succ_le_mono. now rewrite <- (Add_length AD). * now apply incl_Add_inv with a l'. Qed. @@ -2728,9 +2720,8 @@ Section NatSeq. intro len; induction len as [|len IHlen]; intros start n d H. inversion H. simpl seq. - destruct n; simpl. - auto with arith. - rewrite IHlen;simpl; auto with arith. + destruct n; simpl. now rewrite Nat.add_0_r. + now rewrite IHlen; [rewrite Nat.add_succ_r|apply Nat.succ_lt_mono]. Qed. Lemma seq_shift : forall len start, @@ -2738,25 +2729,29 @@ Section NatSeq. Proof. intro len; induction len as [|len IHlen]; simpl; auto. intros. - rewrite IHlen. - auto with arith. + now rewrite IHlen. Qed. Lemma in_seq len start n : In n (seq start len) <-> start <= n < start+len. Proof. - revert start. induction len as [|len IHlen]; 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. + revert start. induction len as [|len IHlen]; simpl; intros start. + - rewrite <- plus_n_O. split;[easy|]. + intros (H,H'). apply (Nat.lt_irrefl start). + eapply Nat.le_lt_trans; eassumption. + - rewrite IHlen, <- plus_n_Sm; simpl; split. + + intros [H|H]; subst; intuition. + * apply -> Nat.succ_le_mono. apply Nat.le_add_r. + * now apply Nat.lt_le_incl. + + intros (H,H'). inversion H. + * now left. + * right. subst. now split; [apply -> Nat.succ_le_mono|]. 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). + rewrite in_seq. intros (H,_). now apply (Nat.lt_irrefl start). Qed. Lemma seq_app : forall len1 len2 start, @@ -3428,11 +3423,12 @@ Qed. Lemma list_max_le : forall l n, list_max l <= n <-> Forall (fun k => k <= n) l. Proof. -intro l; induction l as [|a l IHl]; simpl; intros n; split; intros H; intuition. -- apply Nat.max_lub_iff in H. - now constructor; [ | apply IHl ]. -- inversion_clear H as [ | ? ? Hle HF ]. - apply IHl in HF; apply Nat.max_lub; assumption. + intro l; induction l as [|a l IHl]; simpl; intros n; split. + - now intros. + - intros. now apply Nat.le_0_l. + - intros [? ?] %Nat.max_lub_iff. now constructor; [|apply IHl]. + - intros H. apply Nat.max_lub_iff. + constructor; [exact (Forall_inv H)|apply IHl; exact (Forall_inv_tail H)]. Qed. Lemma list_max_lt : forall l n, l <> nil -> diff --git a/theories/MSets/MSetGenTree.v b/theories/MSets/MSetGenTree.v index 37d20bffad..c1928fef8d 100644 --- a/theories/MSets/MSetGenTree.v +++ b/theories/MSets/MSetGenTree.v @@ -30,6 +30,7 @@ *) Require Import FunInd Orders OrdersFacts MSetInterface PeanoNat. +Require Arith. (* contains deprecated dependencies *) Local Open Scope list_scope. Local Open Scope lazy_bool_scope. |