diff options
Diffstat (limited to 'theories')
| -rw-r--r-- | theories/FSets/FMapAVL.v | 42 | ||||
| -rw-r--r-- | theories/FSets/FMapFacts.v | 2 | ||||
| -rw-r--r-- | theories/FSets/FMapIntMap.v | 55 | ||||
| -rw-r--r-- | theories/FSets/FSetAVL.v | 44 | ||||
| -rw-r--r-- | theories/FSets/FSetDecide.v | 241 | ||||
| -rw-r--r-- | theories/FSets/FSetProperties.v | 4 |
6 files changed, 140 insertions, 248 deletions
diff --git a/theories/FSets/FMapAVL.v b/theories/FSets/FMapAVL.v index a31a0fd84..f3a20eb1c 100644 --- a/theories/FSets/FMapAVL.v +++ b/theories/FSets/FMapAVL.v @@ -750,11 +750,11 @@ Proof. intuition_in. destruct s1;try contradiction;clear y. (* rewrite H_eq_2; rewrite H_eq_2 in H_eq_1; clear H_eq_2. *) - replace s2' with ((remove_min l2 x2 e2 r2)#1); [|rewrite e3; auto]. + replace s2' with ((remove_min l2 x2 e2 r2)#1) by (rewrite e3; auto). rewrite bal_in; auto. - generalize (remove_min_avl H2); rewrite e3; simpl; auto. generalize (remove_min_in y0 H2); rewrite e3; simpl; intro. rewrite H3; intuition. + generalize (remove_min_avl H2); rewrite e3; simpl; auto. Qed. Lemma merge_mapsto : forall elt (s1 s2:t elt) y e, bst s1 -> avl s1 -> bst s2 -> avl s2 -> @@ -766,10 +766,10 @@ Proof. destruct s1;try contradiction;clear y. replace s2' with ((remove_min l2 x2 e2 r2)#1); [|rewrite e3; auto]. rewrite bal_mapsto; auto; unfold create. - generalize (remove_min_avl H2); rewrite e3; simpl; auto. generalize (remove_min_mapsto y0 e H2); rewrite e3; simpl; intro. rewrite H3; intuition (try subst; auto). inversion_clear H3; intuition. + generalize (remove_min_avl H2); rewrite e3; simpl; auto. Qed. Lemma merge_bst : forall elt (s1 s2:t elt), bst s1 -> avl s1 -> bst s2 -> avl s2 -> @@ -1535,20 +1535,7 @@ simpl; auto. intuition. inversion H4. simpl; destruct a; intros. -rewrite IHl; clear IHl. -apply add_bst; auto. -apply add_avl; auto. -inversion H1; auto. -intros. -inversion_clear H1. -assert (~X.eq x k). - contradict H5. - destruct H3. - apply InA_eqA with (x,x0); eauto. -apply (H2 x). -destruct H3; exists x0; auto. -revert H4; do 2 rewrite <- In_alt; destruct 1; exists x0; auto. -eapply add_3; eauto. +rewrite IHl; clear IHl; auto using add_bst, add_avl. intuition. assert (find k0 (add k e m) = Some e0). apply find_1; auto. @@ -1565,6 +1552,17 @@ inversion_clear H1. destruct (MX.eq_dec k0 k). destruct (H2 k); eauto. right; apply add_2; auto. +inversion H1; auto. +intros. +inversion_clear H1. +assert (~X.eq x k). + contradict H5. + destruct H3. + apply InA_eqA with (x,x0); eauto. +apply (H2 x). +destruct H3; exists x0; auto. +revert H4; do 2 rewrite <- In_alt; destruct 1; exists x0; auto. +eapply add_3; eauto. Qed. Lemma anti_elements_mapsto : forall l k e, NoDupA (PX.eqk (elt:=elt'')) l -> @@ -1573,9 +1571,9 @@ Proof. intros. unfold anti_elements. rewrite anti_elements_mapsto_aux; auto; unfold empty; auto. -inversion 2. intuition. inversion H1. +inversion 2. Qed. Lemma map2_avl : forall (m: t elt)(m': t elt'), avl (map2 m m'). @@ -1612,15 +1610,11 @@ intros. case_eq (L.find x l); intros. apply find_1. apply anti_elements_bst; auto. -rewrite anti_elements_mapsto. -apply L.PX.Sort_NoDupA; auto. -apply L.find_2; auto. +rewrite anti_elements_mapsto; auto using L.PX.Sort_NoDupA, L.find_2. case_eq (find x (anti_elements l)); auto; intros. rewrite <- H0; symmetry. apply L.find_1; auto. -rewrite <- anti_elements_mapsto. -apply L.PX.Sort_NoDupA; auto. -apply find_2; auto. +rewrite <- anti_elements_mapsto; auto using L.PX.Sort_NoDupA, find_2. Qed. Lemma map2_1 : forall (m: t elt)(m': t elt')(x:key), bst m -> bst m' -> diff --git a/theories/FSets/FMapFacts.v b/theories/FSets/FMapFacts.v index 78962fd1b..993f1ae79 100644 --- a/theories/FSets/FMapFacts.v +++ b/theories/FSets/FMapFacts.v @@ -1214,7 +1214,6 @@ Module OrdProperties (M:S). constructor; auto with map. apply (@filter_sort _ eqke); auto with map; clean_eauto. rewrite (@InfA_alt _ eqke); auto with map; try (clean_eauto; fail). - apply (@filter_sort _ eqke); auto with map; clean_eauto. intros. rewrite filter_InA in H1; auto with map; destruct H1. rewrite leb_1 in H2. @@ -1224,6 +1223,7 @@ Module OrdProperties (M:S). contradict H. exists e0; apply MapsTo_1 with t0; auto. ME.order. + apply (@filter_sort _ eqke); auto with map; clean_eauto. intros. rewrite filter_InA in H1; auto with map; destruct H1. rewrite gtb_1 in H3. diff --git a/theories/FSets/FMapIntMap.v b/theories/FSets/FMapIntMap.v index 26b892885..b75968e9f 100644 --- a/theories/FSets/FMapIntMap.v +++ b/theories/FSets/FMapIntMap.v @@ -410,7 +410,7 @@ Module MapIntMap <: S with Module E:=NUsualOrderedType. Lemma mapi_2 : forall (elt elt':Type)(m: t elt)(x:key) (f:key->elt->elt'), In x (mapi f m) -> In x m. Proof. - intros elt elt' m; exact (mapi_aux_2 m (fun n => n)). + intros elt elt' m. exact (@mapi_aux_2 _ elt' m (fun n => n)). Qed. Lemma map_1 : forall (elt elt':Type)(m: t elt)(x:key)(e:elt)(f:elt->elt'), @@ -467,38 +467,37 @@ Module MapIntMap <: S with Module E:=NUsualOrderedType. intuition. inversion H2. simpl; destruct a; intros. - rewrite IHl; clear IHl. - inversion H; auto. - intros. inversion_clear H. - assert (~E.eq x k). - contradict H3. - destruct H1. - apply InA_eqA with (x,x0); eauto. - unfold eq_key, E.eq; eauto. - unfold eq_key, E.eq; congruence. - apply (H0 x). - destruct H1; exists x0; auto. - revert H2. - unfold In. - intros (e',He'). - exists e'; apply (@add_3 _ m k x e' a); unfold E.eq; auto. + rewrite IHl; clear IHl; auto. intuition. - red in H2. - rewrite add_spec in H2; auto. + red in H3. + rewrite add_spec in H3; auto. destruct (ME.eq_dec k0 k). - inversion_clear H2; subst; auto. + inversion_clear H3; subst; auto. right; apply find_2; auto. - inversion_clear H2; auto. - compute in H1; destruct H1. + inversion_clear H3; auto. + compute in H; destruct H. subst; right; apply add_1; auto. red; auto. - inversion_clear H. destruct (ME.eq_dec k0 k). unfold E.eq in *; subst. destruct (H0 k); eauto. red; eauto. right; apply add_2; unfold E.eq in *; auto. + (* proof of precondition of IHl *) + intros. + assert (~E.eq x k). + contradict H1. + destruct H. + apply InA_eqA with (x,x0); eauto. + unfold eq_key, E.eq; eauto. + unfold eq_key, E.eq; congruence. + apply (H0 x). + destruct H; exists x0; auto. + revert H3. + unfold In. + intros (e',He'). + exists e'; apply (@add_3 _ m k x e' a); unfold E.eq; auto. Qed. Lemma anti_elements_mapsto : forall (A:Type) l k e, NoDupA (eq_key (A:=A)) l -> @@ -507,10 +506,10 @@ Module MapIntMap <: S with Module E:=NUsualOrderedType. intros. unfold anti_elements. rewrite anti_elements_mapsto_aux; auto; unfold empty; auto. - inversion 2. - inversion H2. intuition. inversion H1. + inversion 2. + inversion H2. Qed. Lemma find_anti_elements : forall (A:Type)(l: list (key*A)) x, sort (@lt_key _) l -> @@ -519,15 +518,11 @@ Module MapIntMap <: S with Module E:=NUsualOrderedType. intros. case_eq (L.find x l); intros. apply find_1. - rewrite anti_elements_mapsto. - apply L.PX.Sort_NoDupA; auto. - apply L.find_2; auto. + rewrite anti_elements_mapsto; auto using L.PX.Sort_NoDupA, L.find_2. case_eq (find x (anti_elements l)); auto; intros. rewrite <- H0; symmetry. apply L.find_1; auto. - rewrite <- anti_elements_mapsto. - apply L.PX.Sort_NoDupA; auto. - apply find_2; auto. + rewrite <- anti_elements_mapsto; auto using L.PX.Sort_NoDupA, find_2. Qed. Lemma find_elements : forall (A:Type)(m: t A) x, diff --git a/theories/FSets/FSetAVL.v b/theories/FSets/FSetAVL.v index 3a08b0f4f..83dc3f1c4 100644 --- a/theories/FSets/FSetAVL.v +++ b/theories/FSets/FSetAVL.v @@ -875,9 +875,9 @@ Proof. destruct s1;try contradiction;clear y. replace s2' with ((remove_min l2 x2 r2)#1); [|rewrite e1; auto]. rewrite bal_in; auto. - generalize (remove_min_avl H2); rewrite e1; simpl; auto. generalize (remove_min_in y0 H2); rewrite e1; simpl; intro. rewrite H3 ; intuition. + generalize (remove_min_avl H2); rewrite e1; simpl; auto. Qed. Lemma merge_bst : forall s1 s2, bst s1 -> avl s1 -> bst s2 -> avl s2 -> @@ -1151,9 +1151,9 @@ Proof. inversion_clear H5. destruct s1;try contradiction;clear y; intros. rewrite (@join_in _ m s2' y H0). - generalize (remove_min_avl H2); rewrite e1; simpl; auto. generalize (remove_min_in y H2); rewrite e1; simpl. intro EQ; rewrite EQ; intuition. + generalize (remove_min_avl H2); rewrite e1; simpl; auto. Qed. Hint Resolve concat_avl concat_bst. @@ -1210,9 +1210,9 @@ Proof. (* GT *) rewrite e1 in IHp;simpl in *; inversion_clear 1; inversion_clear 1; clear H7 H6. rewrite join_in; auto. - generalize (split_avl x H5); rewrite e1; simpl; intuition. rewrite (IHp y0 H1 H5); clear e1. intuition; [ eauto | eauto | intuition_in ]. + generalize (split_avl x H5); rewrite e1; simpl; intuition. Qed. Lemma split_in_2 : forall s x y, bst s -> avl s -> @@ -1222,10 +1222,10 @@ Proof. intuition; try inversion_clear H1. (* LT *) rewrite e1 in IHp; simpl in *; inversion_clear 1; inversion_clear 1; clear H7 H6. - rewrite join_in; auto. - generalize (split_avl x H4); rewrite e1; simpl; intuition. + rewrite join_in; auto. rewrite (IHp y0 H0 H4); clear IHp e0. intuition; [ order | order | intuition_in ]. + generalize (split_avl x H4); rewrite e1; simpl; intuition. (* EQ *) simpl in *; inversion_clear 1; inversion_clear 1; clear H6 H5 e0. intuition; [ order | intuition_in; order ]. @@ -1342,13 +1342,13 @@ Proof. apply concat_bst; auto; intros y1 y2; rewrite IHi1, IHi2; intuition; order. (* In concat *) intros; rewrite concat_in; auto. - intros y1 y2; rewrite IHi1, IHi2; intuition; order. rewrite IHi1; rewrite IHi2. rewrite <- H11, <- H14, split_in_1; auto; rewrite split_in_2; auto. assert (~In x1 r) by (rewrite <- split_in_3; auto; rewrite H13; auto). intuition_in. elim H12. apply In_1 with y; auto. + intros y1 y2; rewrite IHi1, IHi2; intuition; order. Qed. Lemma inter_bst : forall s1 s2, bst s1 -> avl s1 -> bst s2 -> avl s2 -> @@ -1402,12 +1402,12 @@ Proof. apply concat_bst; auto; intros y1 y2; rewrite IHi1, IHi2; intuition; order. (* In concat *) intros; rewrite concat_in; auto. - intros y1 y2; rewrite IHi1, IHi2; intuition; order. rewrite IHi1; rewrite IHi2. rewrite <- H11, <- H14, split_in_1; auto; rewrite split_in_2; auto. rewrite split_in_3 in H13; intuition_in. elim H17. apply In_1 with x1; auto. + intros y1 y2; rewrite IHi1, IHi2; intuition; order. (* bst join *) apply join_bst; auto; intro y; [rewrite IHi1|rewrite IHi2]; intuition. (* In join *) @@ -1675,10 +1675,8 @@ Proof. induction s; simpl; intros. intuition_in. inv bst; inv avl. - rewrite IHs2; auto. - destruct (f t); auto. - rewrite IHs1; auto. - destruct (f t); auto. + rewrite IHs2 by (destruct (f t); auto). + rewrite IHs1 by (destruct (f t); auto). case_eq (f t); intros. rewrite (add_in); auto. intuition_in. @@ -1786,11 +1784,9 @@ Proof. intuition_in. destruct acc as [acct accf]; simpl in *. inv bst; inv avl. - rewrite IHs2; auto. - destruct (f t); auto. - apply partition_acc_avl_1; simpl; auto. - rewrite IHs1; auto. - destruct (f t); simpl; auto. + rewrite IHs2 by + (destruct (f t); auto; apply partition_acc_avl_1; simpl; auto). + rewrite IHs1 by (destruct (f t); simpl; auto). case_eq (f t); simpl; intros. rewrite (add_in); auto. intuition_in. @@ -1799,7 +1795,7 @@ Proof. intuition_in. rewrite (H1 _ _ H8) in H9. rewrite H in H9; discriminate. -Qed. +Qed. Lemma partition_acc_in_2 : forall s acc, avl s -> avl acc#2 -> compat_bool X.eq f -> forall x : elt, @@ -1810,11 +1806,9 @@ Proof. intuition_in. destruct acc as [acct accf]; simpl in *. inv bst; inv avl. - rewrite IHs2; auto. - destruct (f t); auto. - apply partition_acc_avl_2; simpl; auto. - rewrite IHs1; auto. - destruct (f t); simpl; auto. + rewrite IHs2 by + (destruct (f t); auto; apply partition_acc_avl_2; simpl; auto). + rewrite IHs1 by (destruct (f t); simpl; auto). case_eq (f t); simpl; intros. intuition. intuition_in. @@ -2598,10 +2592,10 @@ Module IntMake (I:Int)(X: OrderedType) <: S with Module E := X. unfold partition, filter, Equal, In; simpl ;intros H a. rewrite Raw.partition_in_2; auto. rewrite Raw.filter_in; intuition. - red; intros. - f_equal; auto. - destruct (f a); auto. + rewrite H2; auto. destruct (f a); auto. + red; intros; f_equal. + rewrite (H _ _ H0); auto. Qed. End Filter. diff --git a/theories/FSets/FSetDecide.v b/theories/FSets/FSetDecide.v index d6a92b673..1c8bac6d9 100644 --- a/theories/FSets/FSetDecide.v +++ b/theories/FSets/FSetDecide.v @@ -146,57 +146,43 @@ the above form: together. XXX: This tactic and the similar subsequent ones should - have been defined using [autorewrite]. However, there - is a bug in the order that Coq generates subgoals when - rewriting using a setoid. In order to work around this - bug, these tactics had to be written out in an explicit - way. When the bug is fixed these tactics will break!! - *) + have been defined using [autorewrite]. However, dealing + with multiples rewrite sites and side-conditions is + done more cleverly with the following explicit + analysis of goals. *) + + Ltac or_not_l_iff P Q tac := + (rewrite (or_not_l_iff_1 P Q) by tac) || + (rewrite (or_not_l_iff_2 P Q) by tac). + + Ltac or_not_r_iff P Q tac := + (rewrite (or_not_r_iff_1 P Q) by tac) || + (rewrite (or_not_r_iff_2 P Q) by tac). + + Ltac or_not_l_iff_in P Q H tac := + (rewrite (or_not_l_iff_1 P Q) in H by tac) || + (rewrite (or_not_l_iff_2 P Q) in H by tac). + + Ltac or_not_r_iff_in P Q H tac := + (rewrite (or_not_r_iff_1 P Q) in H by tac) || + (rewrite (or_not_r_iff_2 P Q) in H by tac). Tactic Notation "push" "not" "using" ident(db) := + let dec := solve_decidable using db in unfold not, iff; repeat ( match goal with - (** simplification by not_true_iff *) - | |- context [True -> False] => - rewrite not_true_iff - (** simplification by not_false_iff *) - | |- context [False -> False] => - rewrite not_false_iff - (** simplification by not_not_iff *) - | |- context [(?P -> False) -> False] => - rewrite (not_not_iff P); - [ solve_decidable using db | ] - (** simplification by contrapositive *) - | |- context [(?P -> False) -> (?Q -> False)] => - rewrite (contrapositive P Q); - [ solve_decidable using db | ] - (** simplification by or_not_l_iff_1/_2 *) - | |- context [(?P -> False) \/ ?Q] => - (rewrite (or_not_l_iff_1 P Q); - [ solve_decidable using db | ]) || - (rewrite (or_not_l_iff_2 P Q); - [ solve_decidable using db | ]) - (** simplification by or_not_r_iff_1/_2 *) - | |- context [?P \/ (?Q -> False)] => - (rewrite (or_not_r_iff_1 P Q); - [ solve_decidable using db | ]) || - (rewrite (or_not_r_iff_2 P Q); - [ solve_decidable using db | ]) - (** simplification by imp_not_l *) - | |- context [(?P -> False) -> ?Q] => - rewrite (imp_not_l P Q); - [ solve_decidable using db | ] - (** rewriting by not_or_iff *) - | |- context [?P \/ ?Q -> False] => - rewrite (not_or_iff P Q) - (** rewriting by not_and_iff *) - | |- context [?P /\ ?Q -> False] => - rewrite (not_and_iff P Q) - (** rewriting by not_imp_iff *) - | |- context [(?P -> ?Q) -> False] => - rewrite (not_imp_iff P Q); - [ solve_decidable using db | ] + | |- context [True -> False] => rewrite not_true_iff + | |- context [False -> False] => rewrite not_false_iff + | |- context [(?P -> False) -> False] => rewrite (not_not_iff P) by dec + | |- context [(?P -> False) -> (?Q -> False)] => + rewrite (contrapositive P Q) by dec + | |- context [(?P -> False) \/ ?Q] => or_not_l_iff P Q dec + | |- context [?P \/ (?Q -> False)] => or_not_r_iff P Q dec + | |- context [(?P -> False) -> ?Q] => rewrite (imp_not_l P Q) by dec + | |- context [?P \/ ?Q -> False] => rewrite (not_or_iff P Q) + | |- context [?P /\ ?Q -> False] => rewrite (not_and_iff P Q) + | |- context [(?P -> ?Q) -> False] => rewrite (not_imp_iff P Q) by dec end); fold any not. @@ -205,49 +191,24 @@ the above form: Tactic Notation "push" "not" "in" "*" "|-" "using" ident(db) := + let dec := solve_decidable using db in unfold not, iff in * |-; repeat ( match goal with - (** simplification by not_true_iff *) - | H: context [True -> False] |- _ => - rewrite not_true_iff in H - (** simplification by not_false_iff *) - | H: context [False -> False] |- _ => - rewrite not_false_iff in H - (** simplification by not_not_iff *) - | H: context [(?P -> False) -> False] |- _ => - rewrite (not_not_iff P) in H; - [ | solve_decidable using db ] - (** simplification by contrapositive *) + | H: context [True -> False] |- _ => rewrite not_true_iff in H + | H: context [False -> False] |- _ => rewrite not_false_iff in H + | H: context [(?P -> False) -> False] |- _ => + rewrite (not_not_iff P) in H by dec | H: context [(?P -> False) -> (?Q -> False)] |- _ => - rewrite (contrapositive P Q) in H; - [ | solve_decidable using db ] - (** simplification by or_not_l_iff_1/_2 *) - | H: context [(?P -> False) \/ ?Q] |- _ => - (rewrite (or_not_l_iff_1 P Q) in H; - [ | solve_decidable using db ]) || - (rewrite (or_not_l_iff_2 P Q) in H; - [ | solve_decidable using db ]) - (** simplification by or_not_r_iff_1/_2 *) - | H: context [?P \/ (?Q -> False)] |- _ => - (rewrite (or_not_r_iff_1 P Q) in H; - [ | solve_decidable using db ]) || - (rewrite (or_not_r_iff_2 P Q) in H; - [ | solve_decidable using db ]) - (** simplification by imp_not_l *) - | H: context [(?P -> False) -> ?Q] |- _ => - rewrite (imp_not_l P Q) in H; - [ | solve_decidable using db ] - (** rewriting by not_or_iff *) - | H: context [?P \/ ?Q -> False] |- _ => - rewrite (not_or_iff P Q) in H - (** rewriting by not_and_iff *) - | H: context [?P /\ ?Q -> False] |- _ => - rewrite (not_and_iff P Q) in H - (** rewriting by not_imp_iff *) - | H: context [(?P -> ?Q) -> False] |- _ => - rewrite (not_imp_iff P Q) in H; - [ | solve_decidable using db ] + rewrite (contrapositive P Q) in H by dec + | H: context [(?P -> False) \/ ?Q] |- _ => or_not_l_iff_in P Q H dec + | H: context [?P \/ (?Q -> False)] |- _ => or_not_r_iff_in P Q H dec + | H: context [(?P -> False) -> ?Q] |- _ => + rewrite (imp_not_l P Q) in H by dec + | H: context [?P \/ ?Q -> False] |- _ => rewrite (not_or_iff P Q) in H + | H: context [?P /\ ?Q -> False] |- _ => rewrite (not_and_iff P Q) in H + | H: context [(?P -> ?Q) -> False] |- _ => + rewrite (not_imp_iff P Q) in H by dec end); fold any not. @@ -272,12 +233,14 @@ the above form: (R \/ ~ (P /\ Q)) -> (~ R \/ (P /\ Q)) -> (~ P -> R) -> - (~ ((R -> P) \/ (R -> Q))) -> + (~ ((R -> P) \/ (Q -> R))) -> (~ (P /\ R)) -> (~ (P -> R)) -> True. Proof. - intros. push not in *. tauto. + intros. push not in *. + (* note that ~(R->P) remains (since R isnt decidable) *) + tauto. Qed. (** [pull not using db] will pull as many negations as @@ -289,53 +252,24 @@ the above form: the hypotheses and goal together. *) Tactic Notation "pull" "not" "using" ident(db) := + let dec := solve_decidable using db in unfold not, iff; repeat ( match goal with - (** simplification by not_true_iff *) - | |- context [True -> False] => - rewrite not_true_iff - (** simplification by not_false_iff *) - | |- context [False -> False] => - rewrite not_false_iff - (** simplification by not_not_iff *) - | |- context [(?P -> False) -> False] => - rewrite (not_not_iff P); - [ solve_decidable using db | ] - (** simplification by contrapositive *) + | |- context [True -> False] => rewrite not_true_iff + | |- context [False -> False] => rewrite not_false_iff + | |- context [(?P -> False) -> False] => rewrite (not_not_iff P) by dec | |- context [(?P -> False) -> (?Q -> False)] => - rewrite (contrapositive P Q); - [ solve_decidable using db | ] - (** simplification by or_not_l_iff_1/_2 *) - | |- context [(?P -> False) \/ ?Q] => - (rewrite (or_not_l_iff_1 P Q); - [ solve_decidable using db | ]) || - (rewrite (or_not_l_iff_2 P Q); - [ solve_decidable using db | ]) - (** simplification by or_not_r_iff_1/_2 *) - | |- context [?P \/ (?Q -> False)] => - (rewrite (or_not_r_iff_1 P Q); - [ solve_decidable using db | ]) || - (rewrite (or_not_r_iff_2 P Q); - [ solve_decidable using db | ]) - (** simplification by imp_not_l *) - | |- context [(?P -> False) -> ?Q] => - rewrite (imp_not_l P Q); - [ solve_decidable using db | ] - (** rewriting by not_or_iff *) + rewrite (contrapositive P Q) by dec + | |- context [(?P -> False) \/ ?Q] => or_not_l_iff P Q dec + | |- context [?P \/ (?Q -> False)] => or_not_r_iff P Q dec + | |- context [(?P -> False) -> ?Q] => rewrite (imp_not_l P Q) by dec | |- context [(?P -> False) /\ (?Q -> False)] => rewrite <- (not_or_iff P Q) - (** rewriting by not_and_iff *) - | |- context [?P -> ?Q -> False] => - rewrite <- (not_and_iff P Q) - (** rewriting by not_imp_iff *) - | |- context [?P /\ (?Q -> False)] => - rewrite <- (not_imp_iff P Q); - [ solve_decidable using db | ] - (** rewriting by not_imp_rev_iff *) - | |- context [(?Q -> False) /\ ?P] => - rewrite <- (not_imp_rev_iff P Q); - [ solve_decidable using db | ] + | |- context [?P -> ?Q -> False] => rewrite <- (not_and_iff P Q) + | |- context [?P /\ (?Q -> False)] => rewrite <- (not_imp_iff P Q) by dec + | |- context [(?Q -> False) /\ ?P] => + rewrite <- (not_imp_rev_iff P Q) by dec end); fold any not. @@ -344,53 +278,28 @@ the above form: Tactic Notation "pull" "not" "in" "*" "|-" "using" ident(db) := + let dec := solve_decidable using db in unfold not, iff in * |-; repeat ( match goal with - (** simplification by not_true_iff *) - | H: context [True -> False] |- _ => - rewrite not_true_iff in H - (** simplification by not_false_iff *) - | H: context [False -> False] |- _ => - rewrite not_false_iff in H - (** simplification by not_not_iff *) + | H: context [True -> False] |- _ => rewrite not_true_iff in H + | H: context [False -> False] |- _ => rewrite not_false_iff in H | H: context [(?P -> False) -> False] |- _ => - rewrite (not_not_iff P) in H; - [ | solve_decidable using db ] - (** simplification by contrapositive *) + rewrite (not_not_iff P) in H by dec | H: context [(?P -> False) -> (?Q -> False)] |- _ => - rewrite (contrapositive P Q) in H; - [ | solve_decidable using db ] - (** simplification by or_not_l_iff_1/_2 *) - | H: context [(?P -> False) \/ ?Q] |- _ => - (rewrite (or_not_l_iff_1 P Q) in H; - [ | solve_decidable using db ]) || - (rewrite (or_not_l_iff_2 P Q) in H; - [ | solve_decidable using db ]) - (** simplification by or_not_r_iff_1/_2 *) - | H: context [?P \/ (?Q -> False)] |- _ => - (rewrite (or_not_r_iff_1 P Q) in H; - [ | solve_decidable using db ]) || - (rewrite (or_not_r_iff_2 P Q) in H; - [ | solve_decidable using db ]) - (** simplification by imp_not_l *) + rewrite (contrapositive P Q) in H by dec + | H: context [(?P -> False) \/ ?Q] |- _ => or_not_l_iff_in P Q H dec + | H: context [?P \/ (?Q -> False)] |- _ => or_not_r_iff_in P Q H dec | H: context [(?P -> False) -> ?Q] |- _ => - rewrite (imp_not_l P Q) in H; - [ | solve_decidable using db ] - (** rewriting by not_or_iff *) + rewrite (imp_not_l P Q) in H by dec | H: context [(?P -> False) /\ (?Q -> False)] |- _ => - rewrite <- (not_or_iff P Q) in H - (** rewriting by not_and_iff *) - | H: context [?P -> ?Q -> False] |- _ => + rewrite <- (not_or_iff P Q) in H + | H: context [?P -> ?Q -> False] |- _ => rewrite <- (not_and_iff P Q) in H - (** rewriting by not_imp_iff *) | H: context [?P /\ (?Q -> False)] |- _ => - rewrite <- (not_imp_iff P Q) in H; - [ | solve_decidable using db ] - (** rewriting by not_imp_rev_iff *) + rewrite <- (not_imp_iff P Q) in H by dec | H: context [(?Q -> False) /\ ?P] |- _ => - rewrite <- (not_imp_rev_iff P Q) in H; - [ | solve_decidable using db ] + rewrite <- (not_imp_rev_iff P Q) in H by dec end); fold any not. @@ -415,7 +324,7 @@ the above form: (R \/ ~ (P /\ Q)) -> (~ R \/ (P /\ Q)) -> (~ P -> R) -> - (~ (R -> P) /\ ~ (R -> Q)) -> + (~ (R -> P) /\ ~ (Q -> R)) -> (~ P \/ ~ R) -> (P /\ ~ R) -> (~ R /\ P) -> diff --git a/theories/FSets/FSetProperties.v b/theories/FSets/FSetProperties.v index f3da02a83..1ea669eb8 100644 --- a/theories/FSets/FSetProperties.v +++ b/theories/FSets/FSetProperties.v @@ -859,8 +859,8 @@ Module OrdProperties (M:S). apply (@filter_sort _ E.eq); auto with set; eauto with set. constructor; auto. apply (@filter_sort _ E.eq); auto with set; eauto with set. - rewrite ME.Inf_alt; auto; intros. - apply (@filter_sort _ E.eq); auto with set; eauto with set. + rewrite ME.Inf_alt by (apply (@filter_sort _ E.eq); eauto with set). + intros. rewrite filter_InA in H1; auto; destruct H1. rewrite leb_1 in H2. rewrite <- elements_iff in H1. |