diff options
Diffstat (limited to 'theories/Lists')
| -rw-r--r-- | theories/Lists/List.v | 361 | ||||
| -rw-r--r-- | theories/Lists/SetoidList.v | 225 |
2 files changed, 376 insertions, 210 deletions
diff --git a/theories/Lists/List.v b/theories/Lists/List.v index d6277b3bb5..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. @@ -877,6 +877,36 @@ Section Elts. intros H. simpl. now destruct (eq_dec x y). Qed. + Lemma count_occ_app l1 l2 x : + count_occ (l1 ++ l2) x = count_occ l1 x + count_occ l2 x. + Proof. + induction l1 as [ | h l1 IHl1]; cbn; auto. + now destruct (eq_dec h x); [ rewrite IHl1 | ]. + Qed. + + Lemma count_occ_elt_eq l1 l2 x y : x = y -> + count_occ (l1 ++ x :: l2) y = S (count_occ (l1 ++ l2) y). + Proof. + intros ->. + rewrite ? count_occ_app; cbn. + destruct (eq_dec y y) as [Heq | Hneq]; + [ apply Nat.add_succ_r | now contradiction Hneq ]. + Qed. + + Lemma count_occ_elt_neq l1 l2 x y : x <> y -> + count_occ (l1 ++ x :: l2) y = count_occ (l1 ++ l2) y. + Proof. + intros Hxy. + rewrite ? count_occ_app; cbn. + now destruct (eq_dec x y) as [Heq | Hneq]; [ contradiction Hxy | ]. + Qed. + + Lemma count_occ_bound x l : count_occ l x <= length l. + Proof. + induction l as [|h l]; cbn; auto. + destruct (eq_dec h x); [ apply (proj1 (Nat.succ_le_mono _ _)) | ]; intuition. + Qed. + End Elts. (*******************************) @@ -960,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. @@ -1138,10 +1164,18 @@ Section Map. intro l; induction l; simpl map; intros d n; destruct n; firstorder. Qed. + Lemma nth_error_map : forall n l, + nth_error (map l) n = option_map f (nth_error l n). + Proof. + intro n. induction n as [|n IHn]; intro l. + - now destruct l. + - destruct l as [|? l]; [reflexivity|exact (IHn l)]. + Qed. + Lemma map_nth_error : forall n l d, nth_error l n = Some d -> nth_error (map l) n = Some (f d). Proof. - intro n; induction n; intros [ | ] ? Heq; simpl in *; inversion Heq; auto. + intros n l d H. now rewrite nth_error_map, H. Qed. Lemma map_app : forall l l', @@ -1322,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. @@ -1358,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. (************************************) @@ -1464,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, @@ -1900,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. @@ -2105,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 = []. @@ -2114,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: @@ -2133,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. @@ -2142,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: @@ -2249,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 -> @@ -2268,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]. @@ -2293,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. @@ -2385,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. @@ -2564,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 : @@ -2582,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]. *) @@ -2598,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. @@ -2615,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. @@ -2690,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, @@ -2700,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, @@ -3021,6 +3054,53 @@ Hint Constructors Exists : core. #[global] Hint Constructors Forall : core. +Lemma Exists_map A B (f : A -> B) P l : + Exists P (map f l) <-> Exists (fun x => P (f x)) l. +Proof. + induction l as [|a l IHl]. + - cbn. now rewrite Exists_nil. + - cbn. now rewrite ?Exists_cons, IHl. +Qed. + +Lemma Exists_concat A P (ls : list (list A)) : + Exists P (concat ls) <-> Exists (Exists P) ls. +Proof. + induction ls as [|l ls IHls]. + - cbn. now rewrite Exists_nil. + - cbn. now rewrite Exists_app, Exists_cons, IHls. +Qed. + +Lemma Exists_flat_map A B P ls (f : A -> list B) : + Exists P (flat_map f ls) <-> Exists (fun d => Exists P (f d)) ls. +Proof. + now rewrite flat_map_concat_map, Exists_concat, Exists_map. +Qed. + +Lemma Forall_map A B (f : A -> B) P l : + Forall P (map f l) <-> Forall (fun x => P (f x)) l. +Proof. + induction l as [|a l IHl]. + - constructor; intros; now constructor. + - constructor; intro H; + (constructor; [exact (Forall_inv H) | apply IHl; exact (Forall_inv_tail H)]). +Qed. + +Lemma Forall_concat A P (ls : list (list A)) : + Forall P (concat ls) <-> Forall (Forall P) ls. +Proof. + induction ls as [|l ls IHls]. + - constructor; intros; now constructor. + - cbn. rewrite Forall_app. constructor; intro H. + + constructor; [exact (proj1 H) | apply IHls; exact (proj2 H)]. + + constructor; [exact (Forall_inv H) | apply IHls; exact (Forall_inv_tail H)]. +Qed. + +Lemma Forall_flat_map A B P ls (f : A -> list B) : + Forall P (flat_map f ls) <-> Forall (fun d => Forall P (f d)) ls. +Proof. + now rewrite flat_map_concat_map, Forall_concat, Forall_map. +Qed. + Lemma exists_Forall A B : forall (P : A -> B -> Prop) l, (exists k, Forall (P k) l) -> Forall (fun x => exists k, P k x) l. Proof. @@ -3242,6 +3322,70 @@ Section Repeat. now rewrite (IHl HF') at 1. Qed. + Hypothesis decA : forall x y : A, {x = y}+{x <> y}. + + Lemma count_occ_repeat_eq x y n : x = y -> count_occ decA (repeat y n) x = n. + Proof. + intros ->. + induction n; cbn; auto. + destruct (decA y y); auto. + exfalso; intuition. + Qed. + + Lemma count_occ_repeat_neq x y n : x <> y -> count_occ decA (repeat y n) x = 0. + Proof. + intros Hneq. + induction n; cbn; auto. + destruct (decA y x); auto. + exfalso; intuition. + Qed. + + Lemma count_occ_unique x l : count_occ decA l x = length l -> l = repeat x (length l). + Proof. + induction l as [|h l]; cbn; intros Hocc; auto. + destruct (decA h x). + - f_equal; intuition. + - assert (Hb := count_occ_bound decA x l). + rewrite Hocc in Hb. + exfalso; apply (Nat.nle_succ_diag_l _ Hb). + Qed. + + Lemma count_occ_repeat_excl x l : + (forall y, y <> x -> count_occ decA l y = 0) -> l = repeat x (length l). + Proof. + intros Hocc. + apply Forall_eq_repeat, Forall_forall; intros z Hin. + destruct (decA z x) as [Heq|Hneq]; auto. + apply Hocc, count_occ_not_In in Hneq; intuition. + Qed. + + Lemma count_occ_sgt l x : l = x :: nil <-> + count_occ decA l x = 1 /\ forall y, y <> x -> count_occ decA l y = 0. + Proof. + split. + - intros ->; cbn; split; intros; destruct decA; subst; intuition. + - intros [Heq Hneq]. + apply count_occ_repeat_excl in Hneq. + rewrite Hneq, count_occ_repeat_eq in Heq; trivial. + now rewrite Heq in Hneq. + Qed. + + Lemma nth_repeat a m n : + nth n (repeat a m) a = a. + Proof. + revert n. induction m as [|m IHm]. + - now intros [|n]. + - intros [|n]; [reflexivity|exact (IHm n)]. + Qed. + + Lemma nth_error_repeat a m n : + n < m -> nth_error (repeat a m) n = Some a. + Proof. + intro Hnm. rewrite (nth_error_nth' _ a). + - now rewrite nth_repeat. + - now rewrite repeat_length. + Qed. + End Repeat. Lemma repeat_to_concat A n (a:A) : @@ -3279,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/Lists/SetoidList.v b/theories/Lists/SetoidList.v index 826815410a..69b158a87e 100644 --- a/theories/Lists/SetoidList.v +++ b/theories/Lists/SetoidList.v @@ -71,7 +71,7 @@ Hint Constructors NoDupA : core. Lemma NoDupA_altdef : forall l, NoDupA l <-> ForallOrdPairs (complement eqA) l. Proof. - split; induction 1; constructor; auto. + split; induction 1 as [|a l H rest]; 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'). @@ -85,7 +85,7 @@ Definition inclA l l' := forall x, InA x l -> InA x l'. Definition equivlistA l l' := forall x, InA x l <-> InA x l'. Lemma incl_nil l : inclA nil l. -Proof. intro. intros. inversion H. Qed. +Proof. intros a H. inversion H. Qed. #[local] Hint Resolve incl_nil : list. @@ -128,7 +128,7 @@ Qed. Global Instance eqlistA_equiv : Equivalence eqlistA. Proof. constructor; red. - induction x; auto. + intros x; induction x; auto. induction 1; auto. intros x y z H; revert z; induction H; auto. inversion 1; subst; auto. invlist eqlistA; eauto with *. @@ -138,9 +138,9 @@ Qed. Global Instance eqlistA_equivlistA : subrelation eqlistA equivlistA. Proof. - intros x x' H. induction H. + intros x x' H. induction H as [|? ? ? ? H ? IHeqlistA]. intuition. - red; intros. + red; intros x0. rewrite 2 InA_cons. rewrite (IHeqlistA x0), H; intuition. Qed. @@ -165,7 +165,7 @@ Hint Immediate InA_eqA : core. Lemma In_InA : forall l x, In x l -> InA x l. Proof. - simple induction l; simpl; intuition. + intros l; induction l; simpl; intuition. subst; auto. Qed. #[local] @@ -174,8 +174,9 @@ Hint Resolve In_InA : core. Lemma InA_split : forall l x, InA x l -> exists l1 y l2, eqA x y /\ l = l1++y::l2. Proof. -induction l; intros; inv. +intros l; induction l as [|a l IHl]; intros x H; inv. exists (@nil A); exists a; exists l; auto. +match goal with H' : InA x l |- _ => rename H' into H0 end. destruct (IHl x H0) as (l1,(y,(l2,(H1,H2)))). exists (a::l1); exists y; exists l2; auto. split; simpl; f_equal; auto. @@ -184,9 +185,10 @@ Qed. Lemma InA_app : forall l1 l2 x, InA x (l1 ++ l2) -> InA x l1 \/ InA x l2. Proof. - induction l1; simpl in *; intuition. + intros l1; induction l1 as [|a l1 IHl1]; simpl in *; intuition. inv; auto. - elim (IHl1 l2 x H0); auto. + match goal with H0' : InA _ (l1 ++ _) |- _ => rename H0' into H0 end. + elim (IHl1 _ _ H0); auto. Qed. Lemma InA_app_iff : forall l1 l2 x, @@ -194,7 +196,7 @@ Lemma InA_app_iff : forall l1 l2 x, Proof. split. apply InA_app. - destruct 1; generalize H; do 2 rewrite InA_alt. + destruct 1 as [H|H]; generalize H; do 2 rewrite InA_alt. destruct 1 as (y,(H1,H2)); exists y; split; auto. apply in_or_app; auto. destruct 1 as (y,(H1,H2)); exists y; split; auto. @@ -240,11 +242,12 @@ 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. +intros l; induction l as [|a l IHl]; simpl; auto; intros l' H H0 H1. inv. constructor. rewrite InA_alt; intros (y,(H4,H5)). destruct (in_app_or _ _ _ H5). +match goal with H2' : ~ InA a l |- _ => rename H2' into H2 end. elim H2. rewrite InA_alt. exists y; auto. @@ -253,13 +256,13 @@ auto. rewrite InA_alt. exists y; auto. apply IHl; auto. -intros. +intros x ? ?. apply (H1 x); auto. Qed. Lemma NoDupA_rev : forall l, NoDupA l -> NoDupA (rev l). Proof. -induction l. +intros l; induction l. simpl; auto. simpl; intros. inv. @@ -270,17 +273,17 @@ intros x. rewrite InA_alt. intros (x1,(H2,H3)). intro; inv. -destruct H0. -rewrite <- H4, H2. +match goal with H0 : ~ InA _ _ |- _ => destruct H0 end. +match goal with H4 : eqA x ?x' |- InA ?x' _ => rewrite <- H4, H2 end. apply In_InA. rewrite In_rev; auto. Qed. Lemma NoDupA_split : forall l l' x, NoDupA (l++x::l') -> NoDupA (l++l'). Proof. - induction l; simpl in *; intros; inv; auto. + intros l; induction l; simpl in *; intros; inv; auto. constructor; eauto. - contradict H0. + match goal with H0 : ~ InA _ _ |- _ => contradict H0 end. rewrite InA_app_iff in *. rewrite InA_cons. intuition. @@ -288,17 +291,17 @@ Qed. Lemma NoDupA_swap : forall l l' x, NoDupA (l++x::l') -> NoDupA (x::l++l'). Proof. - induction l; simpl in *; intros; inv; auto. + intros l; induction l as [|a l IHl]; simpl in *; intros l' x H; inv; auto. constructor; eauto. - assert (H2:=IHl _ _ H1). + match goal with H1 : NoDupA (l ++ x :: l') |- _ => assert (H2:=IHl _ _ H1) end. inv. rewrite InA_cons. red; destruct 1. - apply H0. + match goal with H0 : ~ InA a (l ++ x :: l') |- _ => apply H0 end. rewrite InA_app_iff in *; rewrite InA_cons; auto. - apply H; auto. + auto. constructor. - contradict H0. + match goal with H0 : ~ InA a (l ++ x :: l') |- _ => contradict H0 end. rewrite InA_app_iff in *; rewrite InA_cons; intuition. eapply NoDupA_split; eauto. Qed. @@ -356,19 +359,21 @@ Lemma equivlistA_NoDupA_split 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. + intros H H0 H1 H2; intro a. generalize (H2 a). rewrite !InA_app_iff, !InA_cons. inv. assert (SW:=NoDupA_swap H1). inv. - rewrite InA_app_iff in H0. + rewrite InA_app_iff in *. split; intros. - assert (~eqA a x) by (contradict H3; rewrite <- H3; auto). + match goal with H3 : ~ InA x l |- _ => + assert (~eqA a x) by (contradict H3; rewrite <- H3; auto) + end. assert (~eqA a y) by (rewrite <- H; auto). tauto. - assert (OR : eqA a x \/ InA a l) by intuition. clear H6. + assert (OR : eqA a x \/ InA a l) by intuition. destruct OR as [EQN|INA]; auto. - elim H0. + match goal with H0 : ~ (InA y l1 \/ InA y l2) |- _ => elim H0 end. rewrite <-H,<-EQN; auto. Qed. @@ -448,7 +453,7 @@ Qed. Lemma ForallOrdPairs_inclA : forall l l', NoDupA l' -> inclA l' l -> ForallOrdPairs R l -> ForallOrdPairs R l'. Proof. -induction l' as [|x l' IH]. +intros l l'. 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. @@ -476,7 +481,7 @@ Lemma fold_right_commutes_restr : 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. +intros s1; induction s1 as [|a s1 IHs1]; simpl; auto; intros s2 x H. reflexivity. transitivity (f a (f x (fold_right f i (s1++s2)))). apply Comp; auto. @@ -484,7 +489,9 @@ apply IHs1. invlist ForallOrdPairs; auto. apply TraR. invlist ForallOrdPairs; auto. -rewrite Forall_forall in H0; apply H0. +match goal with H0 : Forall (R a) (s1 ++ x :: s2) |- R a x => + rewrite Forall_forall in H0; apply H0 +end. apply in_or_app; simpl; auto. Qed. @@ -492,14 +499,14 @@ Lemma fold_right_equivlistA_restr : 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. - destruct s'; simpl. + intros s; induction s as [|x l Hrec]. + intros s'; destruct s' as [|a s']; simpl. intros; reflexivity. - unfold equivlistA; intros. + unfold equivlistA; intros H H0 H1 H2. destruct (H2 a). assert (InA a nil) by auto; inv. - intros x l Hrec s' N N' F E; simpl in *. - assert (InA x s') by (rewrite <- (E x); auto). + intros s' N N' F E; simpl in *. + assert (InA x s') as H 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))). @@ -520,7 +527,7 @@ Lemma fold_right_add_restr : 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. + intros s' s x **; apply (@fold_right_equivlistA_restr s' (x::s)); auto. Qed. End Fold_With_Restriction. @@ -532,7 +539,7 @@ Variable Tra :transpose f. Lemma fold_right_commutes : forall s1 s2 x, eqB (fold_right f i (s1++x::s2)) (f x (fold_right f i (s1++s2))). Proof. -induction s1; simpl; auto; intros. +intros s1; induction s1 as [|a s1 IHs1]; simpl; auto; intros s2 x. reflexivity. transitivity (f a (f x (fold_right f i (s1++s2)))); auto. apply Comp; auto. @@ -542,7 +549,7 @@ Lemma fold_right_equivlistA : forall s s', NoDupA s -> NoDupA s' -> 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); +intros; apply (fold_right_equivlistA_restr (R:=fun _ _ => True)); repeat red; auto. apply ForallPairs_ForallOrdPairs; try red; auto. Qed. @@ -551,7 +558,7 @@ Lemma fold_right_add : forall s' s x, NoDupA s -> NoDupA 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 s' (x::s)); auto. + intros s' s x **; apply (@fold_right_equivlistA s' (x::s)); auto. Qed. End Fold. @@ -571,7 +578,7 @@ Lemma fold_right_eqlistA2 : eqB (fold_right f i s) (fold_right f j s'). Proof. intros s. - induction s;intros. + induction s as [|a s IHs];intros s' i j heqij heqss'. - inversion heqss'. subst. simpl. @@ -604,7 +611,7 @@ 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. +intros s1; induction s1 as [|a s1 IHs1]; simpl; auto; intros s2 x i j heqij ?. - apply Comp. + destruct eqA_equiv. apply Equivalence_Reflexive. + eapply fold_right_eqlistA2. @@ -617,7 +624,9 @@ induction s1; simpl; auto; intros. invlist ForallOrdPairs; auto. apply TraR. invlist ForallOrdPairs; auto. - rewrite Forall_forall in H0; apply H0. + match goal with H0 : Forall (R a) (s1 ++ x :: s2) |- _ => + rewrite Forall_forall in H0; apply H0 + end. apply in_or_app; simpl; auto. reflexivity. Qed. @@ -628,14 +637,14 @@ Lemma fold_right_equivlistA_restr2 : equivlistA s s' -> eqB i j -> eqB (fold_right f i s) (fold_right f j s'). Proof. - simple induction s. - destruct s'; simpl. + intros s; induction s as [|x l Hrec]. + intros s'; destruct s' as [|a s']; simpl. intros. assumption. - unfold equivlistA; intros. + unfold equivlistA; intros ? ? H H0 H1 H2 **. destruct (H2 a). assert (InA a nil) by auto; inv. - intros x l Hrec s' i j N N' F E eqij; simpl in *. - assert (InA x s') by (rewrite <- (E x); auto). + intros s' i j N N' F E eqij; simpl in *. + assert (InA x s') as H 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))). @@ -663,7 +672,7 @@ 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. + intros s' s i j x **; apply (@fold_right_equivlistA_restr2 s' (x::s) i j); auto. Qed. End Fold2_With_Restriction. @@ -674,7 +683,7 @@ 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. + intros s1; induction s1 as [|a s1 IHs1];simpl;intros s2 i x x' H. - apply Comp;auto. reflexivity. - transitivity (f a (f x' (fold_right f i (s1++s2)))); auto. @@ -688,7 +697,7 @@ Lemma fold_right_equivlistA2 : 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); +intros; apply (fold_right_equivlistA_restr2 (R:=fun _ _ => True)); repeat red; auto. apply ForallPairs_ForallOrdPairs; try red; auto. Qed. @@ -697,9 +706,9 @@ 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. + intros s' s i j x **. replace (f x (fold_right f j s)) with (fold_right f j (x::s)) by auto. - eapply fold_right_equivlistA2;auto. + eapply fold_right_equivlistA2;auto. Qed. End Fold2. @@ -710,7 +719,7 @@ Hypothesis eqA_dec : forall x y : A, {eqA x y}+{~(eqA x y)}. Lemma InA_dec : forall x l, { InA x l } + { ~ InA x l }. Proof. -induction l. +intros x l; induction l as [|a l IHl]. right; auto. intro; inv. destruct (eqA_dec x a). @@ -729,28 +738,30 @@ Fixpoint removeA (x : A) (l : list A) : list A := Lemma removeA_filter : forall x l, removeA x l = filter (fun y => if eqA_dec x y then false else true) l. Proof. -induction l; simpl; auto. +intros x l; induction l as [|a l IHl]; simpl; auto. destruct (eqA_dec x a); auto. rewrite IHl; auto. Qed. Lemma removeA_InA : forall l x y, InA y (removeA x l) <-> InA y l /\ ~eqA x y. Proof. -induction l; simpl; auto. -split. +intros l; induction l as [|a l IHl]; simpl; auto. +intros x y; split. intro; inv. destruct 1; inv. -intros. +intros x y. destruct (eqA_dec x a) as [Heq|Hnot]; simpl; auto. rewrite IHl; split; destruct 1; split; auto. inv; auto. -destruct H0; transitivity a; auto. +match goal with H0 : ~ eqA x y |- _ => destruct H0 end; transitivity a; auto. split. intro; inv. split; auto. contradict Hnot. transitivity y; auto. -rewrite (IHl x y) in H0; destruct H0; auto. +match goal with H0 : InA y (removeA x l) |- _ => + rewrite (IHl x y) in H0; destruct H0; auto +end. destruct 1; inv; auto. right; rewrite IHl; auto. Qed. @@ -758,7 +769,7 @@ Qed. Lemma removeA_NoDupA : forall s x, NoDupA s -> NoDupA (removeA x s). Proof. -simple induction s; simpl; intros. +intros s; induction s as [|a s IHs]; simpl; intros x ?. auto. inv. destruct (eqA_dec x a); simpl; auto. @@ -770,16 +781,16 @@ Qed. Lemma removeA_equivlistA : forall l l' x, ~InA x l -> equivlistA (x :: l) l' -> equivlistA l (removeA x l'). Proof. -unfold equivlistA; intros. +unfold equivlistA; intros l l' x H H0 x0. rewrite removeA_InA. -split; intros. +split; intros H1. rewrite <- H0; split; auto. contradict H. apply InA_eqA with x0; auto. rewrite <- (H0 x0) in H1. destruct H1. inv; auto. -elim H2; auto. +match goal with H2 : ~ eqA x x0 |- _ => elim H2; auto end. Qed. End Remove. @@ -806,7 +817,7 @@ Hint Constructors lelistA sort : core. Lemma InfA_ltA : forall l x y, ltA x y -> InfA y l -> InfA x l. Proof. - destruct l; constructor. inv; eauto. + intros l; destruct l; constructor. inv; eauto. Qed. Global Instance InfA_compat : Proper (eqA==>eqlistA==>iff) InfA. @@ -815,8 +826,8 @@ Proof using eqA_equiv ltA_compat. (* and not ltA_strorder *) inversion_clear Hll'. intuition. split; intro; inv; constructor. - rewrite <- Hxx', <- H; auto. - rewrite Hxx', H; auto. + match goal with H : eqA _ _ |- _ => rewrite <- Hxx', <- H; auto end. + match goal with H : eqA _ _ |- _ => rewrite Hxx', H; auto end. Qed. (** For compatibility, can be deduced from [InfA_compat] *) @@ -830,9 +841,9 @@ Hint Immediate InfA_ltA InfA_eqA : core. 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. + intros l; induction l as [|a l IHl]. + intros x a **. inv. + intros x a0 **. inv. setoid_replace x with a; auto. eauto. Qed. @@ -840,13 +851,13 @@ 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. + intros l; 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. + intros l; induction l; simpl; intros; constructor; auto. Qed. (* In fact, this may be used as an alternative definition for InfA: *) @@ -861,7 +872,7 @@ Qed. Lemma InfA_app : forall l1 l2 a, InfA a l1 -> InfA a l2 -> InfA a (l1++l2). Proof. - induction l1; simpl; auto. + intros l1; induction l1; simpl; auto. intros; inv; auto. Qed. @@ -870,7 +881,7 @@ Lemma SortA_app : (forall x y, InA x l1 -> InA y l2 -> ltA x y) -> SortA (l1 ++ l2). Proof. - induction l1; simpl in *; intuition. + intros l1; induction l1; intros l2; simpl in *; intuition. inv. constructor; auto. apply InfA_app; auto. @@ -879,8 +890,8 @@ Qed. Lemma SortA_NoDupA : forall l, SortA l -> NoDupA l. Proof. - simple induction l; auto. - intros x l' H H0. + intros l; induction l as [|x l' H]; auto. + intros H0. inv. constructor; auto. intro. @@ -922,7 +933,7 @@ Qed. Global Instance rev_eqlistA_compat : Proper (eqlistA==>eqlistA) (@rev A). Proof. -repeat red. intros. +repeat red. intros x y ?. rewrite <- (app_nil_r (rev x)), <- (app_nil_r (rev y)). apply eqlistA_rev_app; auto. Qed. @@ -936,15 +947,15 @@ 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. +intros l; induction l as [|a l IHl]; intros l'; destruct l' as [|a0 l']; simpl; intros H H0 H1; auto. +destruct (H1 a0); assert (InA a0 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. +intros; eapply (SortA_InfA_InA (l:=l)); eauto. assert (forall y, InA y l' -> ltA a0 y). -intros; eapply SortA_InfA_InA with (l:=l'); eauto. -clear H3 H4. +intros; eapply (SortA_InfA_InA (l:=l')); eauto. +do 2 match goal with H : InfA _ _ |- _ => clear H end. assert (eqA a a0). destruct (H1 a). destruct (H1 a0). @@ -953,13 +964,19 @@ assert (eqA a a0). elim (StrictOrder_Irreflexive a); eauto. constructor; auto. apply IHl; auto. -split; intros. +intros x; split; intros. destruct (H1 x). assert (InA x (a0::l')) by auto. inv; auto. -rewrite H9,<-H3 in H4. elim (StrictOrder_Irreflexive a); eauto. +match goal with H3 : eqA a a0, H4 : InA x l, H9 : eqA x a0 |- InA x l' => + rewrite H9,<-H3 in H4 +end. +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. +match goal with H3 : eqA a a0, H4 : InA x l', H9 : eqA x a |- InA x l => + rewrite H9,H3 in H4 +end. +elim (StrictOrder_Irreflexive a0); eauto. Qed. End EqlistA. @@ -970,12 +987,12 @@ Section Filter. Lemma filter_sort : forall f l, SortA l -> SortA (List.filter f l). Proof. -induction l; simpl; auto. +intros f l; induction l as [|a l IHl]; simpl; auto. intros; inv; auto. destruct (f a); auto. constructor; auto. apply In_InfA; auto. -intros. +intros y H. rewrite filter_In in H; destruct H. eapply SortA_InfA_InA; eauto. Qed. @@ -984,12 +1001,14 @@ 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. +(* Unset Mangle Names. *) 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. +intros f H l x; do 2 rewrite InA_alt; intuition; + match goal with Hex' : exists _, _ |- _ => rename Hex' into Hex end. +destruct Hex as (y,(H0,H1)); rewrite filter_In in H1; exists y; intuition. +destruct Hex 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. +destruct Hex as (y,(H0,H1)); exists y; rewrite filter_In; intuition. rewrite <- (H _ _ H0); auto. Qed. @@ -997,19 +1016,20 @@ 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. +intros f H l; induction l as [|a l IHl]; simpl; intros H0; auto. inv. +match goal with H1' : SortA l, H2' : InfA a l |- _ => rename H1' into H1, H2' into H2 end. rewrite IHl at 1; auto. case_eq (f a); simpl; intros; auto. -assert (forall e, In e l -> f e = false). - intros. +assert (forall e, In e l -> f e = false) as H3. + intros e H3. 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. +generalize H3; clear; induction l as [|a l IHl]; simpl; auto. +case_eq (f a); auto; intros H H3. rewrite H3 in H; auto; try discriminate. Qed. @@ -1043,23 +1063,24 @@ Lemma findA_NoDupA : Proof. 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. +intros l; induction l as [|a l IHl]; intros a0 b H; simpl. +split; intros H0; try discriminate. invlist InA. destruct a as (a',b'); rename a0 into a. invlist NoDupA. split; intros. invlist InA. -compute in H2; destruct H2. subst b'. +match goal with H2 : eqke (a, b) (a', b') |- _ => compute in H2; destruct H2 end. +subst b'. destruct (eqA_dec a a'); intuition. destruct (eqA_dec a a') as [HeqA|]; simpl. -contradict H0. -revert HeqA H2; clear - eqA_equiv. +match goal with H0 : ~ InA eqk (a', b') l |- _ => contradict H0 end. +match goal with H2 : InA eqke (a, b) l |- _ => revert HeqA H2; clear - eqA_equiv end. induction l. intros; invlist InA. intros; invlist InA; auto. -destruct a0. -compute in H; destruct H. +match goal with |- InA eqk _ (?p :: _) => destruct p as [a0 b0] end. +match goal with H : eqke (a, b) (a0, b0) |- _ => compute in H; destruct H end. subst b. left; auto. compute. |