diff options
Diffstat (limited to 'theories/Lists/SetoidList.v')
| -rw-r--r-- | theories/Lists/SetoidList.v | 225 |
1 files changed, 123 insertions, 102 deletions
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. |