diff options
Diffstat (limited to 'theories')
| -rw-r--r-- | theories/Compat/Coq810.v | 2 | ||||
| -rw-r--r-- | theories/Compat/Coq811.v | 11 | ||||
| -rw-r--r-- | theories/FSets/FMapAVL.v | 57 | ||||
| -rw-r--r-- | theories/FSets/FMapFacts.v | 24 | ||||
| -rw-r--r-- | theories/FSets/FMapFullAVL.v | 4 | ||||
| -rw-r--r-- | theories/FSets/FMapList.v | 53 | ||||
| -rw-r--r-- | theories/FSets/FMapPositive.v | 4 | ||||
| -rw-r--r-- | theories/FSets/FSetBridge.v | 10 | ||||
| -rw-r--r-- | theories/FSets/FSetEqProperties.v | 28 | ||||
| -rw-r--r-- | theories/FSets/FSetProperties.v | 8 | ||||
| -rw-r--r-- | theories/Logic/ClassicalFacts.v | 33 | ||||
| -rw-r--r-- | theories/QArith/QArith_base.v | 65 | ||||
| -rw-r--r-- | theories/QArith/Qreduction.v | 14 | ||||
| -rw-r--r-- | theories/QArith/Qround.v | 7 | ||||
| -rw-r--r-- | theories/Reals/Rtrigo1.v | 1 | ||||
| -rw-r--r-- | theories/Structures/OrderedType.v | 135 | ||||
| -rw-r--r-- | theories/Structures/OrderedTypeEx.v | 17 | ||||
| -rw-r--r-- | theories/ZArith/ZArith.v | 1 | ||||
| -rw-r--r-- | theories/ZArith/Zcomplements.v | 34 | ||||
| -rw-r--r-- | theories/ZArith/Zdiv.v | 73 | ||||
| -rw-r--r-- | theories/ZArith/Znumtheory.v | 336 | ||||
| -rw-r--r-- | theories/ZArith/Zpow_facts.v | 2 | ||||
| -rw-r--r-- | theories/ZArith/Zpower.v | 47 |
23 files changed, 580 insertions, 386 deletions
diff --git a/theories/Compat/Coq810.v b/theories/Compat/Coq810.v index d24af2186f..c611d356ce 100644 --- a/theories/Compat/Coq810.v +++ b/theories/Compat/Coq810.v @@ -9,3 +9,5 @@ (************************************************************************) (** Compatibility file for making Coq act similar to Coq v8.10 *) + +Require Export Coq.Compat.Coq811. diff --git a/theories/Compat/Coq811.v b/theories/Compat/Coq811.v new file mode 100644 index 0000000000..4a9a041d4e --- /dev/null +++ b/theories/Compat/Coq811.v @@ -0,0 +1,11 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +(** Compatibility file for making Coq act similar to Coq v8.11 *) diff --git a/theories/FSets/FMapAVL.v b/theories/FSets/FMapAVL.v index 8627ff7353..ea4062d9fe 100644 --- a/theories/FSets/FMapAVL.v +++ b/theories/FSets/FMapAVL.v @@ -593,14 +593,14 @@ Qed. Lemma MapsTo_1 : forall m x y e, X.eq x y -> MapsTo x e m -> MapsTo y e m. Proof. - induction m; simpl; intuition_in; eauto. + induction m; simpl; intuition_in; eauto with ordered_type. Qed. Hint Immediate MapsTo_1 : core. Lemma In_1 : forall m x y, X.eq x y -> In x m -> In y m. Proof. - intros m x y; induction m; simpl; intuition_in; eauto. + intros m x y; induction m; simpl; intuition_in; eauto with ordered_type. Qed. Lemma In_node_iff : @@ -671,7 +671,7 @@ Qed. Lemma lt_tree_trans : forall x y, X.lt x y -> forall m, lt_tree x m -> lt_tree y m. Proof. - eauto. + eauto with ordered_type. Qed. Lemma gt_tree_not_in : @@ -683,7 +683,7 @@ Qed. Lemma gt_tree_trans : forall x y, X.lt y x -> forall m, gt_tree x m -> gt_tree y m. Proof. - eauto. + eauto with ordered_type. Qed. Hint Resolve lt_tree_not_in lt_tree_trans gt_tree_not_in gt_tree_trans : core. @@ -707,7 +707,7 @@ Qed. Lemma is_empty_1 : forall m, Empty m -> is_empty m = true. Proof. destruct m as [|r x e l h]; simpl; auto. - intro H; elim (H x e); auto. + intro H; elim (H x e); auto with ordered_type. Qed. Lemma is_empty_2 : forall m, is_empty m = true -> Empty m. @@ -732,7 +732,7 @@ Lemma find_1 : forall m x e, bst m -> MapsTo x e m -> find x m = Some e. Proof. intros m x; functional induction (find x m); auto; intros; clearf; inv bst; intuition_in; simpl; auto; - try solve [order | absurd (X.lt x y); eauto | absurd (X.lt y x); eauto]. + try solve [order | absurd (X.lt x y); eauto with ordered_type | absurd (X.lt y x); eauto with ordered_type]. Qed. Lemma find_2 : forall m x e, find x m = Some e -> MapsTo x e m. @@ -832,8 +832,8 @@ Lemma bal_bst : forall l x e r, bst l -> bst r -> Proof. intros l x e r; functional induction (bal l x e r); intros; clearf; inv bst; repeat apply create_bst; auto; unfold create; try constructor; - (apply lt_tree_node || apply gt_tree_node); auto; - (eapply lt_tree_trans || eapply gt_tree_trans); eauto. + (apply lt_tree_node || apply gt_tree_node); auto with ordered_type; + (eapply lt_tree_trans || eapply gt_tree_trans); eauto with ordered_type. Qed. Hint Resolve bal_bst : core. @@ -865,7 +865,7 @@ Lemma add_in : forall m x y e, Proof. intros m x y e; functional induction (add x e m); auto; intros; try (rewrite bal_in, IHt); intuition_in. - apply In_1 with x; auto. + apply In_1 with x; auto with ordered_type. Qed. Lemma add_bst : forall m x e, bst m -> bst (add x e m). @@ -874,14 +874,14 @@ Proof. inv bst; try apply bal_bst; auto; intro z; rewrite add_in; intuition. apply MX.eq_lt with x; auto. - apply MX.lt_eq with x; auto. + apply MX.lt_eq with x; auto with ordered_type. Qed. Hint Resolve add_bst : core. Lemma add_1 : forall m x y e, X.eq x y -> MapsTo y e (add x e m). Proof. intros m x y e; functional induction (add x e m); - intros; inv bst; try rewrite bal_mapsto; unfold create; eauto. + intros; inv bst; try rewrite bal_mapsto; unfold create; eauto with ordered_type. Qed. Lemma add_2 : forall m x y e e', ~X.eq x y -> @@ -912,7 +912,7 @@ Proof. intros; rewrite find_mapsto_equiv; auto. split; eauto using add_2, add_3. destruct X.compare; try (apply H0; order). - auto using find_1, add_1. + auto using find_1, add_1 with ordered_type. Qed. (** * Extraction of minimum binding *) @@ -971,7 +971,7 @@ Proof. generalize (remove_min_in ll lx ld lr _x m#1). rewrite e0; simpl; intros. rewrite (bal_in l' x d r y) in H. - assert (In m#1 (Node ll lx ld lr _x)) by (rewrite H4; auto); clear H4. + assert (In m#1 (Node ll lx ld lr _x)) by (rewrite H4; auto with ordered_type); clear H4. assert (X.lt m#1 x) by order. decompose [or] H; order. Qed. @@ -1050,7 +1050,7 @@ Proof. (* EQ *) inv bst; clear e0. rewrite merge_in; intuition; [ order | order | intuition_in ]. - elim H4; eauto. + elim H4; eauto with ordered_type. (* GT *) inv bst; clear e0. rewrite bal_in; auto. @@ -1069,7 +1069,7 @@ Proof. destruct H; eauto. (* EQ *) inv bst. - apply merge_bst; eauto. + apply merge_bst; eauto with ordered_type. (* GT *) inv bst. apply bal_bst; auto. @@ -1124,8 +1124,8 @@ Lemma join_bst : forall l x d r, bst l -> bst r -> Proof. join_tac; auto; try (simpl; auto; fail); inv bst; apply bal_bst; auto; clear Hrl Hlr; intro; intros; rewrite join_in in *. - intuition; [ apply MX.lt_eq with x | ]; eauto. - intuition; [ apply MX.eq_lt with x | ]; eauto. + intuition; [ apply MX.lt_eq with x | ]; eauto with ordered_type. + intuition; [ apply MX.eq_lt with x | ]; eauto with ordered_type. Qed. Hint Resolve join_bst : core. @@ -1135,8 +1135,8 @@ Lemma join_find : forall l x d r y, Proof. join_tac; auto; inv bst; simpl (join (Leaf elt)); - try (assert (X.lt lx x) by auto); - try (assert (X.lt x rx) by auto); + try (assert (X.lt lx x) by auto with ordered_type); + try (assert (X.lt x rx) by auto with ordered_type); rewrite ?add_find, ?bal_find; auto. simpl; destruct X.compare; auto. @@ -1260,7 +1260,7 @@ Proof. change (bst (m2',xd)#1). rewrite <-e1; eauto. intros y Hy. apply H1; auto. - rewrite remove_min_in, e1; simpl; auto. + rewrite remove_min_in, e1; simpl; auto with ordered_type. change (gt_tree (m2',xd)#2#1 (m2',xd)#1). rewrite <-e1; eauto. Qed. Hint Resolve concat_bst : core. @@ -1283,9 +1283,9 @@ Proof. simpl; destruct X.compare as [Hlt| |Hlt]; simpl; auto. destruct (find y m2'); auto. symmetry; rewrite not_find_iff; auto; intro. - apply (MX.lt_not_gt Hlt); apply H1; auto; rewrite H3; auto. + apply (MX.lt_not_gt Hlt); apply H1; auto; rewrite H3; auto with ordered_type. - intros z Hz; apply H1; auto; rewrite H3; auto. + intros z Hz; apply H1; auto; rewrite H3; auto with ordered_type. Qed. @@ -1338,12 +1338,12 @@ Proof. apply InA_InfA with (eqA:=eqke); auto with *. intros (y',e') H6. destruct (elements_aux_mapsto r acc y' e'); intuition. red; simpl; eauto. - red; simpl; eauto. - intros. + red; simpl; eauto with ordered_type. + intros x e0 y0 H H6. inversion_clear H. destruct H7; simpl in *. order. - destruct (elements_aux_mapsto r acc x e0); intuition eauto. + destruct (elements_aux_mapsto r acc x e0); intuition eauto with ordered_type. Qed. Lemma elements_sort : forall s : t elt, bst s -> sort ltk (elements s). @@ -1363,7 +1363,8 @@ Lemma elements_aux_cardinal : Proof. simple induction m; simpl; intuition. rewrite <- H; simpl. - rewrite <- H0; omega. + rewrite <- H0, Nat.add_succ_r, (Nat.add_comm (cardinal t)), Nat.add_assoc. + reflexivity. Qed. Lemma elements_cardinal : forall (m:t elt), cardinal m = length (elements m). @@ -1567,7 +1568,7 @@ Lemma mapi_1 : forall (m: tree elt)(x:key)(e:elt), MapsTo x e m -> exists y, X.eq y x /\ MapsTo x (f y e) (mapi f m). Proof. induction m; simpl; inversion_clear 1; auto. -exists k; auto. +exists k; auto with ordered_type. destruct (IHm1 _ _ H0). exists x0; intuition. destruct (IHm2 _ _ H0). @@ -2072,7 +2073,7 @@ Module IntMake_ord (I:Int)(X: OrderedType)(D : OrderedType) <: X.eq x1 x2 -> D.eq d1 d2 -> Cmp c l1 l2 -> Cmp c ((x1,d1)::l1) ((x2,d2)::l2). Proof. - destruct c; simpl; intros; P.MX.elim_comp; auto. + destruct c; simpl; intros; P.MX.elim_comp; auto with ordered_type. Qed. Hint Resolve cons_Cmp : core. diff --git a/theories/FSets/FMapFacts.v b/theories/FSets/FMapFacts.v index 1a531542cc..758f9d41b0 100644 --- a/theories/FSets/FMapFacts.v +++ b/theories/FSets/FMapFacts.v @@ -1822,7 +1822,7 @@ Module OrdProperties (M:S). destruct (gtb (x,e) (a,e')); destruct (gtb (x,e) (b,e'')); auto. unfold O.ltk in *; simpl in *; intros. symmetry; rewrite H2. - apply ME.eq_lt with a; auto. + apply ME.eq_lt with a; auto with ordered_type. rewrite <- H1; auto. unfold O.ltk in *; simpl in *; intros. rewrite H1. @@ -1869,7 +1869,7 @@ Module OrdProperties (M:S). rewrite <- elements_mapsto_iff in H1. assert (~E.eq x t0). contradict H. - exists e0; apply MapsTo_1 with t0; auto. + exists e0; apply MapsTo_1 with t0; auto with ordered_type. ME.order. apply (@filter_sort _ eqke); auto with *; clean_eauto. intros. @@ -1888,9 +1888,9 @@ Module OrdProperties (M:S). find_mapsto_iff, (H0 t0), <- find_mapsto_iff, add_mapsto_iff by (auto with *). unfold O.eqke, O.ltk; simpl. - destruct (E.compare t0 x); intuition; try fold (~E.eq x t0); auto. + destruct (E.compare t0 x); intuition; try fold (~E.eq x t0); auto with ordered_type. - elim H; exists e0; apply MapsTo_1 with t0; auto. - - fold (~E.lt t0 x); auto. + - fold (~E.lt t0 x); auto with ordered_type. Qed. Lemma elements_Add_Above : forall m m' x e, @@ -1905,7 +1905,7 @@ Module OrdProperties (M:S). destruct x0; destruct y. rewrite <- elements_mapsto_iff in H1. unfold O.eqke, O.ltk in *; simpl in *; destruct H3. - apply ME.lt_eq with x; auto. + apply ME.lt_eq with x; auto with ordered_type. apply H; firstorder. inversion H3. red; intros a; destruct a. @@ -1991,7 +1991,7 @@ Module OrdProperties (M:S). injection H as [= -> ->]. inversion_clear H1. red in H; simpl in *; intuition. - elim H0; eauto. + elim H0; eauto with ordered_type. inversion H. change (max_elt_aux (p::l) = Some (x,e)) in H. generalize (IHl x e H); clear IHl; intros IHl. @@ -2007,9 +2007,9 @@ Module OrdProperties (M:S). inversion_clear H2. inversion_clear H5. red in H2; simpl in H2; ME.order. - eapply IHl; eauto. + eapply IHl; eauto with ordered_type. econstructor; eauto. - red; eauto. + red; eauto with ordered_type. inversion H2; auto. Qed. @@ -2022,7 +2022,7 @@ Module OrdProperties (M:S). induction (elements m). simpl; try discriminate. destruct a; destruct l; simpl in *. - injection H; intros; subst; constructor; red; auto. + injection H; intros; subst; constructor; red; auto with ordered_type. constructor 2; auto. Qed. @@ -2069,7 +2069,7 @@ Module OrdProperties (M:S). destruct (elements m). simpl; try discriminate. destruct p; simpl in *. - injection H; intros; subst; constructor; red; auto. + injection H; intros; subst; constructor; red; auto with ordered_type. Qed. Lemma min_elt_Empty : @@ -2106,7 +2106,7 @@ Module OrdProperties (M:S). apply IHn. assert (S n = S (cardinal (remove k m))). rewrite Heqn. - eapply cardinal_2; eauto with map. + eapply cardinal_2; eauto with map ordered_type. inversion H1; auto. eapply max_elt_Above; eauto. @@ -2133,7 +2133,7 @@ Module OrdProperties (M:S). apply IHn. assert (S n = S (cardinal (remove k m))). rewrite Heqn. - eapply cardinal_2; eauto with map. + eapply cardinal_2; eauto with map ordered_type. inversion H1; auto. eapply min_elt_Below; eauto. diff --git a/theories/FSets/FMapFullAVL.v b/theories/FSets/FMapFullAVL.v index 8ca9401a06..fa553d9fce 100644 --- a/theories/FSets/FMapFullAVL.v +++ b/theories/FSets/FMapFullAVL.v @@ -68,7 +68,7 @@ Hint Constructors avl : core. Lemma height_non_negative : forall (s : t elt), avl s -> height s >= 0. Proof. - induction s; simpl; intros; auto with zarith. + induction s; simpl; intros. now apply Z.le_ge. inv avl; intuition; omega_max. Qed. @@ -712,7 +712,7 @@ Module IntMake_ord (I:Int)(X: OrderedType)(D : OrderedType) <: X.eq x1 x2 -> D.eq d1 d2 -> Cmp c l1 l2 -> Cmp c ((x1,d1)::l1) ((x2,d2)::l2). Proof. - destruct c; simpl; intros; MX.elim_comp; auto. + destruct c; simpl; intros; MX.elim_comp; auto with ordered_type. Qed. Hint Resolve cons_Cmp : core. diff --git a/theories/FSets/FMapList.v b/theories/FSets/FMapList.v index b21d809059..cad528644a 100644 --- a/theories/FSets/FMapList.v +++ b/theories/FSets/FMapList.v @@ -68,7 +68,7 @@ Proof. intros m. case m;auto. intros (k,e) l inlist. - absurd (InA eqke (k, e) ((k, e) :: l));auto. + absurd (InA eqke (k, e) ((k, e) :: l)); auto with ordered_type. Qed. Lemma is_empty_2 : forall m, is_empty m = true -> Empty m. @@ -106,14 +106,14 @@ Proof. elim (sort_inv sorted);auto. elim (In_inv belong1);auto. intro abs. - absurd (X.eq x k');auto. + absurd (X.eq x k'); auto with ordered_type. Qed. Lemma mem_2 : forall m (Hm:Sort m) x, mem x m = true -> In x m. Proof. intros m Hm x; generalize Hm; clear Hm; unfold PX.In,PX.MapsTo. functional induction (mem x m); intros sorted hyp;try ((inversion hyp);fail). - exists _x; auto. + exists _x; auto with ordered_type. induction IHb; auto. exists x0; auto. inversion_clear sorted; auto. @@ -135,7 +135,7 @@ Function find (k:key) (s: t elt) {struct s} : option elt := Lemma find_2 : forall m x e, find x m = Some e -> MapsTo x e m. Proof. intros m x. unfold PX.MapsTo. - functional induction (find x m);simpl;intros e' eqfind; inversion eqfind; auto. + functional induction (find x m);simpl;intros e' eqfind; inversion eqfind; auto with ordered_type. Qed. Lemma find_1 : forall m (Hm:Sort m) x e, MapsTo x e m -> find x m = Some e. @@ -174,7 +174,7 @@ Lemma add_1 : forall m x y e, X.eq x y -> MapsTo y e (add x e m). Proof. intros m x y e; generalize y; clear y. unfold PX.MapsTo. - functional induction (add x e m);simpl;auto. + functional induction (add x e m);simpl;auto with ordered_type. Qed. Lemma add_2 : forall m x y e e', @@ -195,12 +195,12 @@ Qed. Lemma add_3 : forall m x y e e', ~ X.eq x y -> MapsTo y e (add x e' m) -> MapsTo y e m. -Proof. +Proof with auto with ordered_type. intros m x y e e'. generalize y e; clear y e; unfold PX.MapsTo. functional induction (add x e' m);simpl; intros. - apply (In_inv_3 H0); compute; auto. - apply (In_inv_3 H0); compute; auto. - constructor 2; apply (In_inv_3 H0); compute; auto. + apply (In_inv_3 H0)... + apply (In_inv_3 H0)... + constructor 2; apply (In_inv_3 H0)... inversion_clear H0; auto. Qed. @@ -254,7 +254,7 @@ Proof. clear e0;inversion_clear Hm. apply Sort_Inf_NotIn with x0; auto. - apply Inf_eq with (k',x0);auto; compute; apply X.eq_trans with x; auto. + apply Inf_eq with (k',x0);auto; compute; apply X.eq_trans with x; auto with ordered_type. clear e0;inversion_clear Hm. assert (notin:~ In y (remove x l)) by auto. @@ -374,13 +374,13 @@ Definition Equivb cmp m m' := Lemma equal_1 : forall m (Hm:Sort m) m' (Hm': Sort m') cmp, Equivb cmp m m' -> equal cmp m m' = true. -Proof. +Proof with auto with ordered_type. intros m Hm m' Hm' cmp; generalize Hm Hm'; clear Hm Hm'. functional induction (equal cmp m m'); simpl; subst;auto; unfold Equivb; intuition; subst. match goal with H: X.compare _ _ = _ |- _ => clear H end. assert (cmp_e_e':cmp e e' = true). - apply H1 with x; auto. + apply H1 with x... rewrite cmp_e_e'; simpl. apply IHb; auto. inversion_clear Hm; auto. @@ -388,7 +388,7 @@ Proof. unfold Equivb; intuition. destruct (H0 k). assert (In k ((x,e) ::l)). - destruct H as (e'', hyp); exists e''; auto. + destruct H as (e'', hyp); exists e''... destruct (In_inv (H2 H4)); auto. inversion_clear Hm. elim (Sort_Inf_NotIn H6 H7). @@ -396,20 +396,20 @@ Proof. apply MapsTo_eq with k; auto; order. destruct (H0 k). assert (In k ((x',e') ::l')). - destruct H as (e'', hyp); exists e''; auto. + destruct H as (e'', hyp); exists e''... destruct (In_inv (H3 H4)); auto. inversion_clear Hm'. elim (Sort_Inf_NotIn H6 H7). destruct H as (e'', hyp); exists e''; auto. apply MapsTo_eq with k; auto; order. - apply H1 with k; destruct (X.eq_dec x k); auto. + apply H1 with k; destruct (X.eq_dec x k)... destruct (X.compare x x') as [Hlt|Heq|Hlt]; try contradiction; clear y. destruct (H0 x). assert (In x ((x',e')::l')). apply H; auto. - exists e; auto. + exists e... destruct (In_inv H3). order. inversion_clear Hm'. @@ -420,7 +420,7 @@ Proof. destruct (H0 x'). assert (In x' ((x,e)::l)). apply H2; auto. - exists e'; auto. + exists e'... destruct (In_inv H3). order. inversion_clear Hm. @@ -434,13 +434,13 @@ Proof. clear H1;destruct p as (k,e). destruct (H0 k). destruct H1. - exists e; auto. + exists e... inversion H1. destruct p as (x,e). destruct (H0 x). destruct H. - exists e; auto. + exists e... inversion H. destruct p;destruct p0;contradiction. @@ -449,7 +449,7 @@ Qed. Lemma equal_2 : forall m (Hm:Sort m) m' (Hm:Sort m') cmp, equal cmp m m' = true -> Equivb cmp m m'. -Proof. +Proof with auto with ordered_type. intros m Hm m' Hm' cmp; generalize Hm Hm'; clear Hm Hm'. functional induction (equal cmp m m'); simpl; subst;auto; unfold Equivb; intuition; try discriminate; subst; @@ -464,16 +464,16 @@ Proof. exists e'; constructor; split; trivial; apply X.eq_trans with x; auto. destruct (H k). destruct (H9 H8) as (e'',hyp). - exists e''; auto. + exists e''... inversion_clear Hm;inversion_clear Hm'. destruct (andb_prop _ _ H); clear H. destruct (IHb H1 H3 H6). destruct (In_inv H0). - exists e; constructor; split; trivial; apply X.eq_trans with x'; auto. + exists e; constructor; split; trivial; apply X.eq_trans with x'... destruct (H k). destruct (H10 H8) as (e'',hyp). - exists e''; auto. + exists e''... inversion_clear Hm;inversion_clear Hm'. destruct (andb_prop _ _ H); clear H. @@ -615,7 +615,8 @@ Proof. inversion_clear 1. exists x'. destruct H0; simpl in *. - split; auto. + split. + auto with ordered_type. constructor 1. unfold eqke in *; simpl in *; intuition congruence. destruct IHm as (y, hyp); auto. @@ -946,7 +947,7 @@ Proof. destruct (IHm0 H0) as (_,H4); apply H4; auto. case_eq (find x m0); intros; auto. assert (eqk (elt:=oee') (k,(oo,oo')) (x,(oo,oo'))). - red; auto. + red; auto with ordered_type. destruct (Sort_Inf_NotIn H0 (Inf_eq (eqk_sym H5) H1)). exists p; apply find_2; auto. (* k < x *) @@ -1315,7 +1316,7 @@ Proof. apply (IHm1 H0 (Build_slist H5)); intuition. Qed. -Ltac cmp_solve := unfold eq, lt; simpl; try Raw.MX.elim_comp; auto. +Ltac cmp_solve := unfold eq, lt; simpl; try Raw.MX.elim_comp; auto with ordered_type. Definition compare : forall m1 m2, Compare lt eq m1 m2. Proof. diff --git a/theories/FSets/FMapPositive.v b/theories/FSets/FMapPositive.v index e5133f66b2..342a51b39b 100644 --- a/theories/FSets/FMapPositive.v +++ b/theories/FSets/FMapPositive.v @@ -476,8 +476,8 @@ Module PositiveMap <: S with Module E:=PositiveOrderedTypeBits. unfold elements. intros m; set (p:=1); clearbody p; revert m p. induction m; simpl; auto; intros. - rewrite (IHm1 (append p 2)), (IHm2 (append p 3)); auto. - destruct o; rewrite app_length; simpl; omega. + rewrite (IHm1 (append p 2)), (IHm2 (append p 3)). + destruct o; rewrite app_length; simpl; auto. Qed. End CompcertSpec. diff --git a/theories/FSets/FSetBridge.v b/theories/FSets/FSetBridge.v index 6e08c38a49..f0b31e6986 100644 --- a/theories/FSets/FSetBridge.v +++ b/theories/FSets/FSetBridge.v @@ -63,11 +63,11 @@ Module DepOfNodep (Import M: S) <: Sdep with Module E := M.E. {s' : t | forall y : elt, In y s' <-> ~ E.eq x y /\ In y s}. Proof. intros; exists (remove x s); intuition. - absurd (In x (remove x s)); auto with set. - apply In_1 with y; auto. + absurd (In x (remove x s)); auto with set ordered_type. + apply In_1 with y; auto with ordered_type. elim (E.eq_dec x y); intros; auto. - absurd (In x (remove x s)); auto with set. - apply In_1 with y; auto. + absurd (In x (remove x s)); auto with set ordered_type. + apply In_1 with y; auto with ordered_type. eauto with set. Qed. @@ -470,7 +470,7 @@ Module NodepOfDep (M: Sdep) <: S with Module E := M.E. Hint Resolve elements_3 : core. Lemma elements_3w : forall s : t, NoDupA E.eq (elements s). - Proof. auto. Qed. + Proof. auto with ordered_type. Qed. Definition min_elt (s : t) : option elt := match min_elt s with diff --git a/theories/FSets/FSetEqProperties.v b/theories/FSets/FSetEqProperties.v index da504259f5..1983c6caa1 100644 --- a/theories/FSets/FSetEqProperties.v +++ b/theories/FSets/FSetEqProperties.v @@ -17,7 +17,7 @@ [mem x s=true] instead of [In x s], [equal s s'=true] instead of [Equal s s'], etc. *) -Require Import FSetProperties Zerob Sumbool Omega DecidableTypeEx. +Require Import FSetProperties Zerob Sumbool DecidableTypeEx. Module WEqProperties_fun (Import E:DecidableType)(M:WSfun E). Module Import MP := WProperties_fun E M. @@ -847,11 +847,16 @@ Proof. unfold sum. intros f g Hf Hg. assert (fc : compat_opL (fun x:elt =>plus (f x))). red; auto with fset. -assert (ft : transposeL (fun x:elt =>plus (f x))). red; intros; omega. +assert (ft : transposeL (fun x:elt =>plus (f x))). red; intros x y z. + rewrite !PeanoNat.Nat.add_assoc, (PeanoNat.Nat.add_comm (f x) (f y)); reflexivity. assert (gc : compat_opL (fun x:elt => plus (g x))). red; auto with fset. -assert (gt : transposeL (fun x:elt =>plus (g x))). red; intros; omega. +assert (gt : transposeL (fun x:elt =>plus (g x))). red; intros x y z. + rewrite !PeanoNat.Nat.add_assoc, (PeanoNat.Nat.add_comm (g x) (g y)); reflexivity. assert (fgc : compat_opL (fun x:elt =>plus ((f x)+(g x)))). repeat red; auto. -assert (fgt : transposeL (fun x:elt=>plus ((f x)+(g x)))). red; intros; omega. +assert (fgt : transposeL (fun x:elt=>plus ((f x)+(g x)))). red; intros x y z. + set (u := (f x + g x)); set (v := (f y + g y)). + rewrite !PeanoNat.Nat.add_assoc, (PeanoNat.Nat.add_comm u). + reflexivity. assert (st : Equivalence (@Logic.eq nat)) by (split; congruence). intros s;pattern s; apply set_rec. intros. @@ -859,7 +864,10 @@ rewrite <- (fold_equal _ _ st _ fc ft 0 _ _ H). rewrite <- (fold_equal _ _ st _ gc gt 0 _ _ H). rewrite <- (fold_equal _ _ st _ fgc fgt 0 _ _ H); auto. intros; do 3 (rewrite (fold_add _ _ st);auto). -rewrite H0;simpl;omega. +rewrite H0;simpl. +rewrite <- !(PeanoNat.Nat.add_assoc (f x)); f_equal. +rewrite !PeanoNat.Nat.add_assoc. f_equal. +apply PeanoNat.Nat.add_comm. do 3 rewrite fold_empty;auto. Qed. @@ -872,7 +880,11 @@ assert (cc : compat_opL (fun x => plus (if f x then 1 else 0))). repeat red; intros. rewrite (Hf _ _ H); auto. assert (ct : transposeL (fun x => plus (if f x then 1 else 0))). - red; intros; omega. + red; intros. + set (a := if f x then _ else _). + rewrite PeanoNat.Nat.add_comm. + rewrite <- !PeanoNat.Nat.add_assoc. f_equal. + apply PeanoNat.Nat.add_comm. intros s;pattern s; apply set_rec. intros. change elt with E.t. @@ -921,9 +933,11 @@ Lemma sum_compat : forall f g, Proper (E.eq==>Logic.eq) f -> Proper (E.eq==>Logic.eq) g -> forall s, (forall x, In x s -> f x=g x) -> sum f s=sum g s. intros. -unfold sum; apply (fold_compat _ (@Logic.eq nat)); auto with *. +unfold sum; apply (fold_compat _ (@Logic.eq nat)); auto with fset. intros x x' Hx y y' Hy. rewrite Hx, Hy; auto. +intros x y z; rewrite !PeanoNat.Nat.add_assoc; f_equal; apply PeanoNat.Nat.add_comm. intros x x' Hx y y' Hy. rewrite Hx, Hy; auto. +intros x y z; rewrite !PeanoNat.Nat.add_assoc; f_equal; apply PeanoNat.Nat.add_comm. Qed. End Sum. diff --git a/theories/FSets/FSetProperties.v b/theories/FSets/FSetProperties.v index c6b2e0a09d..e500debc73 100644 --- a/theories/FSets/FSetProperties.v +++ b/theories/FSets/FSetProperties.v @@ -939,7 +939,7 @@ Module OrdProperties (M:S). generalize (gtb_1 x a)(gtb_1 x b); destruct (gtb x a); destruct (gtb x b); auto. intros. symmetry; rewrite H1. - apply ME.eq_lt with a; auto. + apply ME.eq_lt with a; auto with ordered_type. rewrite <- H0; auto. intros. rewrite H0. @@ -1013,7 +1013,7 @@ Module OrdProperties (M:S). intros. inversion_clear H2. rewrite <- elements_iff in H1. - apply ME.lt_eq with x; auto. + apply ME.lt_eq with x; auto with ordered_type. inversion H3. red; intros a. rewrite InA_app_iff, InA_cons, InA_nil by auto with *. @@ -1052,7 +1052,7 @@ Module OrdProperties (M:S). apply X0 with (remove e s) e; auto with set. apply IHn. assert (S n = S (cardinal (remove e s))). - rewrite Heqn; apply cardinal_2 with e; auto with set. + rewrite Heqn; apply cardinal_2 with e; auto with set ordered_type. inversion H0; auto. red; intros. rewrite remove_iff in H0; destruct H0. @@ -1073,7 +1073,7 @@ Module OrdProperties (M:S). apply X0 with (remove e s) e; auto with set. apply IHn. assert (S n = S (cardinal (remove e s))). - rewrite Heqn; apply cardinal_2 with e; auto with set. + rewrite Heqn; apply cardinal_2 with e; auto with set ordered_type. inversion H0; auto. red; intros. rewrite remove_iff in H0; destruct H0. diff --git a/theories/Logic/ClassicalFacts.v b/theories/Logic/ClassicalFacts.v index 2a9e15ab37..8538b54c08 100644 --- a/theories/Logic/ClassicalFacts.v +++ b/theories/Logic/ClassicalFacts.v @@ -29,7 +29,7 @@ Table of contents: 3. Weak classical axioms -3.1. Weak excluded middle +3.1. Weak excluded middle and classical de Morgan law 3.2. Gödel-Dummett axiom and right distributivity of implication over disjunction @@ -514,7 +514,7 @@ End Weak_proof_irrelevance_CCI. (** * Weak classical axioms *) (** We show the following increasing in the strength of axioms: - - weak excluded-middle + - weak excluded-middle and classical De Morgan's law - right distributivity of implication over disjunction and Gödel-Dummett axiom - independence of general premises and drinker's paradox - excluded-middle @@ -523,11 +523,15 @@ End Weak_proof_irrelevance_CCI. (** ** Weak excluded-middle *) (** The weak classical logic based on [~~A \/ ~A] is referred to with - name KC in [[ChagrovZakharyaschev97]] + name KC in [[ChagrovZakharyaschev97]]. See [[SorbiTerwijn11]] for + a short survey. [[ChagrovZakharyaschev97]] Alexander Chagrov and Michael Zakharyaschev, "Modal Logic", Clarendon Press, 1997. -*) + + [[SorbiTerwijn11]] Andrea Sorbi and Sebastiaan A. Terwijn, + "Generalizations of the weak law of the excluded-middle", Notre + Dame J. Formal Logic, vol 56(2), pp 321-331, 2015. *) Definition weak_excluded_middle := forall A:Prop, ~~A \/ ~A. @@ -539,16 +543,21 @@ Definition weak_excluded_middle := Definition weak_generalized_excluded_middle := forall A B:Prop, ((A -> B) -> B) \/ (A -> B). +(** Classical De Morgan's law *) + +Definition classical_de_morgan_law := + forall A B:Prop, ~(A /\ B) -> ~A \/ ~B. + (** ** Gödel-Dummett axiom *) (** [(A->B) \/ (B->A)] is studied in [[Dummett59]] and is based on [[Gödel33]]. [[Dummett59]] Michael A. E. Dummett. "A Propositional Calculus - with a Denumerable Matrix", In the Journal of Symbolic Logic, Vol - 24 No. 2(1959), pp 97-103. + with a Denumerable Matrix", In the Journal of Symbolic Logic, vol + 24(2), pp 97-103, 1959. [[Gödel33]] Kurt Gödel. "Zum intuitionistischen Aussagenkalkül", - Ergeb. Math. Koll. 4 (1933), pp. 34-38. + Ergeb. Math. Koll. 4, pp. 34-38, 1933. *) Definition GodelDummett := forall A B:Prop, (A -> B) \/ (B -> A). @@ -590,6 +599,16 @@ Proof. right; intro HA; apply (HAnotA HA HA). Qed. +(** The weak excluded middle is equivalent to the classical De Morgan's law *) + +Lemma weak_excluded_middle_iff_classical_de_morgan_law : + weak_excluded_middle <-> classical_de_morgan_law. +Proof. + split; [intro WEM|intro CDML]; intros A *. + - destruct (WEM A); tauto. + - destruct (CDML A (~A)); tauto. +Qed. + (** ** Independence of general premises and drinker's paradox *) (** Independence of general premises is the unconstrained, non diff --git a/theories/QArith/QArith_base.v b/theories/QArith/QArith_base.v index b60feb9256..54d35cded2 100644 --- a/theories/QArith/QArith_base.v +++ b/theories/QArith/QArith_base.v @@ -79,7 +79,7 @@ Notation "x <= y <= z" := (x<=y/\y<=z) : Q_scope. Lemma inject_Z_injective (a b: Z): inject_Z a == inject_Z b <-> a = b. Proof. - unfold Qeq. simpl. omega. + unfold Qeq; simpl; rewrite !Z.mul_1_r; reflexivity. Qed. (** Another approach : using Qcompare for defining order relations. *) @@ -599,9 +599,7 @@ Proof. Qed. Lemma Qle_antisym x y : x<=y -> y<=x -> x==y. -Proof. - unfold Qle, Qeq; auto with zarith. -Qed. +Proof. apply Z.le_antisymm. Qed. Lemma Qle_trans : forall x y z, x<=y -> y<=z -> x<=z. Proof. @@ -618,14 +616,10 @@ Qed. Hint Resolve Qle_trans : qarith. Lemma Qlt_irrefl x : ~x<x. -Proof. - unfold Qlt. auto with zarith. -Qed. +Proof. apply Z.lt_irrefl. Qed. Lemma Qlt_not_eq x y : x<y -> ~ x==y. -Proof. - unfold Qlt, Qeq; auto with zarith. -Qed. +Proof. apply Z.lt_neq. Qed. Lemma Zle_Qle (x y: Z): (x <= y)%Z = (inject_Z x <= inject_Z y). Proof. @@ -647,9 +641,7 @@ Proof. Qed. Lemma Qlt_le_weak x y : x<y -> x<=y. -Proof. - unfold Qle, Qlt; auto with zarith. -Qed. +Proof. apply Z.lt_le_incl. Qed. Lemma Qle_lt_trans : forall x y z, x<=y -> y<z -> x<z. Proof. @@ -684,25 +676,17 @@ Qed. (** [x<y] iff [~(y<=x)] *) -Lemma Qnot_lt_le : forall x y, ~ x<y -> y<=x. -Proof. - unfold Qle, Qlt; auto with zarith. -Qed. +Lemma Qnot_lt_le x y : ~ x < y -> y <= x. +Proof. apply Z.nlt_ge. Qed. -Lemma Qnot_le_lt : forall x y, ~ x<=y -> y<x. -Proof. - unfold Qle, Qlt; auto with zarith. -Qed. +Lemma Qnot_le_lt x y : ~ x <= y -> y < x. +Proof. apply Z.nle_gt. Qed. -Lemma Qlt_not_le : forall x y, x<y -> ~ y<=x. -Proof. - unfold Qle, Qlt; auto with zarith. -Qed. +Lemma Qlt_not_le x y : x < y -> ~ y <= x. +Proof. apply Z.lt_nge. Qed. -Lemma Qle_not_lt : forall x y, x<=y -> ~ y<x. -Proof. - unfold Qle, Qlt; auto with zarith. -Qed. +Lemma Qle_not_lt x y : x <= y -> ~ y < x. +Proof. apply Z.le_ngt. Qed. Lemma Qle_lt_or_eq : forall x y, x<=y -> x<y \/ x==y. Proof. @@ -746,21 +730,24 @@ Defined. Lemma Qopp_le_compat : forall p q, p<=q -> -q <= -p. Proof. intros (a1,a2) (b1,b2); unfold Qle, Qlt; simpl. - rewrite !Z.mul_opp_l. omega. + now rewrite !Z.mul_opp_l, <- Z.opp_le_mono. Qed. + Hint Resolve Qopp_le_compat : qarith. Lemma Qle_minus_iff : forall p q, p <= q <-> 0 <= q+-p. Proof. intros (x1,x2) (y1,y2); unfold Qle; simpl. - rewrite Z.mul_opp_l. omega. + rewrite Z.mul_1_r, Z.mul_opp_l, <- Z.le_sub_le_add_r, Z.opp_involutive. + reflexivity. Qed. Lemma Qlt_minus_iff : forall p q, p < q <-> 0 < q+-p. Proof. intros (x1,x2) (y1,y2); unfold Qlt; simpl. - rewrite Z.mul_opp_l. omega. + rewrite Z.mul_1_r, Z.mul_opp_l, <- Z.lt_sub_lt_add_r, Z.opp_involutive. + reflexivity. Qed. Lemma Qplus_le_compat : @@ -831,9 +818,11 @@ Lemma Qmult_le_compat_r : forall x y z, x <= y -> 0 <= z -> x*z <= y*z. Proof. intros (a1,a2) (b1,b2) (c1,c2); unfold Qle, Qlt; simpl. Open Scope Z_scope. + rewrite Z.mul_1_r. intros; simpl_mult. rewrite Z.mul_shuffle1, (Z.mul_shuffle1 b1). - apply Z.mul_le_mono_nonneg_r; auto with zarith. + apply Z.mul_le_mono_nonneg_r; auto. + now apply Z.mul_nonneg_nonneg. Close Scope Z_scope. Qed. @@ -843,9 +832,10 @@ Proof. Open Scope Z_scope. simpl_mult. rewrite Z.mul_shuffle1, (Z.mul_shuffle1 b1). + rewrite Z.mul_1_r. intros LT LE. apply Z.mul_le_mono_pos_r in LE; trivial. - apply Z.mul_pos_pos; [omega|easy]. + apply Z.mul_pos_pos; easy. Close Scope Z_scope. Qed. @@ -866,10 +856,11 @@ Lemma Qmult_lt_compat_r : forall x y z, 0 < z -> x < y -> x*z < y*z. Proof. intros (a1,a2) (b1,b2) (c1,c2); unfold Qle, Qlt; simpl. Open Scope Z_scope. + rewrite Z.mul_1_r. intros; simpl_mult. rewrite Z.mul_shuffle1, (Z.mul_shuffle1 b1). apply Z.mul_lt_mono_pos_r; auto with zarith. - apply Z.mul_pos_pos; [omega|reflexivity]. + apply Z.mul_pos_pos; easy. Close Scope Z_scope. Qed. @@ -880,8 +871,9 @@ Proof. unfold Qle, Qlt; simpl. simpl_mult. rewrite Z.mul_shuffle1, (Z.mul_shuffle1 b1). + rewrite Z.mul_1_r. intro LT. rewrite <- Z.mul_lt_mono_pos_r. reflexivity. - apply Z.mul_pos_pos; [omega|reflexivity]. + now apply Z.mul_pos_pos. Close Scope Z_scope. Qed. @@ -896,6 +888,7 @@ Proof. intros a b Ha Hb. unfold Qle in *. simpl in *. +rewrite Z.mul_1_r in *. auto with *. Qed. diff --git a/theories/QArith/Qreduction.v b/theories/QArith/Qreduction.v index 78cd549ce6..e314f64028 100644 --- a/theories/QArith/Qreduction.v +++ b/theories/QArith/Qreduction.v @@ -35,7 +35,7 @@ Proof. rewrite <- Hg in LE; clear Hg. assert (0 <> g) by (intro; subst; discriminate). rewrite Z2Pos.id. ring. - rewrite <- (Z.mul_pos_cancel_l g); [now rewrite <- Hd | omega]. + now rewrite <- (Z.mul_pos_cancel_l g); [ rewrite <- Hd | apply Z.le_neq ]. Close Scope Z_scope. Qed. @@ -60,8 +60,8 @@ Proof. - congruence. - (*rel_prime*) constructor. - * exists aa; auto with zarith. - * exists bb; auto with zarith. + * exists aa; auto using Z.mul_1_r. + * exists bb; auto using Z.mul_1_r. * intros x Ha Hb. destruct Hg1 as (Hg11,Hg12,Hg13). destruct (Hg13 (g*x)) as (x',Hx). @@ -73,8 +73,8 @@ Proof. apply Z.mul_reg_l with g; auto. rewrite Hx at 1; ring. - (* rel_prime *) constructor. - * exists cc; auto with zarith. - * exists dd; auto with zarith. + * exists cc; auto using Z.mul_1_r. + * exists dd; auto using Z.mul_1_r. * intros x Hc Hd. inversion Hg'1 as (Hg'11,Hg'12,Hg'13). destruct (Hg'13 (g'*x)) as (x',Hx). @@ -85,9 +85,9 @@ Proof. exists x'. apply Z.mul_reg_l with g'; auto. rewrite Hx at 1; ring. - apply Z.lt_gt. - rewrite <- (Z.mul_pos_cancel_l g); [now rewrite <- Hg4 | omega]. + rewrite <- (Z.mul_pos_cancel_l g); [ now rewrite <- Hg4 | apply Z.le_neq; intuition ]. - apply Z.lt_gt. - rewrite <- (Z.mul_pos_cancel_l g'); [now rewrite <- Hg'4 | omega]. + rewrite <- (Z.mul_pos_cancel_l g'); [now rewrite <- Hg'4 | apply Z.le_neq; intuition ]. - apply Z.mul_reg_l with (g*g'). * rewrite Z.mul_eq_0. now destruct 1. * rewrite Z.mul_shuffle1, <- Hg3, <- Hg'4. diff --git a/theories/QArith/Qround.v b/theories/QArith/Qround.v index af5c471d5d..8d68038582 100644 --- a/theories/QArith/Qround.v +++ b/theories/QArith/Qround.v @@ -13,7 +13,8 @@ Require Import QArith. Lemma Qopp_lt_compat: forall p q : Q, p < q -> - q < - p. Proof. intros (a1,a2) (b1,b2); unfold Qle, Qlt; simpl. -rewrite !Z.mul_opp_l; omega. +rewrite !Z.mul_opp_l. +apply Z.opp_lt_mono. Qed. Hint Resolve Qopp_lt_compat : qarith. @@ -38,7 +39,7 @@ intros z. unfold Qceiling. simpl. rewrite Zdiv_1_r. -auto with *. +apply Z.opp_involutive. Qed. Lemma Qfloor_le : forall x, Qfloor x <= x. @@ -119,7 +120,7 @@ Lemma Qceiling_resp_le : forall x y, x <= y -> (Qceiling x <= Qceiling y)%Z. Proof. intros x y Hxy. unfold Qceiling. -cut (Qfloor (-y) <= Qfloor (-x))%Z; auto with *. +rewrite <- Z.opp_le_mono; auto with qarith. Qed. Hint Resolve Qceiling_resp_le : qarith. diff --git a/theories/Reals/Rtrigo1.v b/theories/Reals/Rtrigo1.v index a760a0af6a..0df1442f46 100644 --- a/theories/Reals/Rtrigo1.v +++ b/theories/Reals/Rtrigo1.v @@ -18,6 +18,7 @@ Require Export Cos_rel. Require Export Cos_plus. Require Import ZArith_base. Require Import Zcomplements. +Import Omega. Require Import Lra. Require Import Ranalysis1. Require Import Rsqrt_def. diff --git a/theories/Structures/OrderedType.v b/theories/Structures/OrderedType.v index 566dd31a9e..a411c5e54e 100644 --- a/theories/Structures/OrderedType.v +++ b/theories/Structures/OrderedType.v @@ -26,6 +26,8 @@ Arguments LT [X lt eq x y] _. Arguments EQ [X lt eq x y] _. Arguments GT [X lt eq x y] _. +Create HintDb ordered_type. + Module Type MiniOrderedType. Parameter Inline t : Type. @@ -42,8 +44,8 @@ Module Type MiniOrderedType. Parameter compare : forall x y : t, Compare lt eq x y. - Hint Immediate eq_sym : core. - Hint Resolve eq_refl eq_trans lt_not_eq lt_trans : core. + Hint Immediate eq_sym : ordered_type. + Hint Resolve eq_refl eq_trans lt_not_eq lt_trans : ordered_type. End MiniOrderedType. @@ -60,9 +62,9 @@ Module MOT_to_OT (Import O : MiniOrderedType) <: OrderedType. Include O. Definition eq_dec : forall x y : t, {eq x y} + {~ eq x y}. - Proof. - intros; elim (compare x y); intro H; [ right | left | right ]; auto. - assert (~ eq y x); auto. + Proof with auto with ordered_type. + intros; elim (compare x y); intro H; [ right | left | right ]... + assert (~ eq y x)... Defined. End MOT_to_OT. @@ -79,31 +81,30 @@ Module OrderedTypeFacts (Import O: OrderedType). Lemma lt_antirefl : forall x, ~ lt x x. Proof. - intros; intro; absurd (eq x x); auto. + intros; intro; absurd (eq x x); auto with ordered_type. Qed. Instance lt_strorder : StrictOrder lt. Proof. split; [ exact lt_antirefl | exact lt_trans]. Qed. Lemma lt_eq : forall x y z, lt x y -> eq y z -> lt x z. - Proof. + Proof with auto with ordered_type. intros; destruct (compare x z) as [Hlt|Heq|Hlt]; auto. - elim (lt_not_eq H); apply eq_trans with z; auto. - elim (lt_not_eq (lt_trans Hlt H)); auto. + elim (lt_not_eq H); apply eq_trans with z... + elim (lt_not_eq (lt_trans Hlt H))... Qed. Lemma eq_lt : forall x y z, eq x y -> lt y z -> lt x z. - Proof. + Proof with auto with ordered_type. intros; destruct (compare x z) as [Hlt|Heq|Hlt]; auto. - elim (lt_not_eq H0); apply eq_trans with x; auto. - elim (lt_not_eq (lt_trans H0 Hlt)); auto. + elim (lt_not_eq H0); apply eq_trans with x... + elim (lt_not_eq (lt_trans H0 Hlt))... Qed. Instance lt_compat : Proper (eq==>eq==>iff) lt. - Proof. apply proper_sym_impl_iff_2; auto with *. intros x x' Hx y y' Hy H. - apply eq_lt with x; auto. + apply eq_lt with x; auto with ordered_type. apply lt_eq with y; auto. Qed. @@ -143,9 +144,9 @@ Module OrderedTypeFacts (Import O: OrderedType). Lemma eq_not_gt x y : eq x y -> ~ lt y x. Proof. order. Qed. Lemma lt_not_gt x y : lt x y -> ~ lt y x. Proof. order. Qed. - Hint Resolve gt_not_eq eq_not_lt : core. - Hint Immediate eq_lt lt_eq le_eq eq_le neq_eq eq_neq : core. - Hint Resolve eq_not_gt lt_antirefl lt_not_gt : core. + Hint Resolve gt_not_eq eq_not_lt : ordered_type. + Hint Immediate eq_lt lt_eq le_eq eq_le neq_eq eq_neq : ordered_type. + Hint Resolve eq_not_gt lt_antirefl lt_not_gt : ordered_type. Lemma elim_compare_eq : forall x y : t, @@ -197,7 +198,7 @@ Module OrderedTypeFacts (Import O: OrderedType). Lemma lt_dec : forall x y : t, {lt x y} + {~ lt x y}. Proof. - intros; elim (compare x y); [ left | right | right ]; auto. + intros; elim (compare x y); [ left | right | right ]; auto with ordered_type. Defined. Definition eqb x y : bool := if eq_dec x y then true else false. @@ -247,8 +248,8 @@ Proof. exact (SortA_NoDupA eq_equiv lt_strorder lt_compat). Qed. End ForNotations. -Hint Resolve ListIn_In Sort_NoDup Inf_lt : core. -Hint Immediate In_eq Inf_lt : core. +Hint Resolve ListIn_In Sort_NoDup Inf_lt : ordered_type. +Hint Immediate In_eq Inf_lt : ordered_type. End OrderedTypeFacts. @@ -266,8 +267,8 @@ Module KeyOrderedType(O:OrderedType). eq (fst p) (fst p') /\ (snd p) = (snd p'). Definition ltk (p p':key*elt) := lt (fst p) (fst p'). - Hint Unfold eqk eqke ltk : core. - Hint Extern 2 (eqke ?a ?b) => split : core. + Hint Unfold eqk eqke ltk : ordered_type. + Hint Extern 2 (eqke ?a ?b) => split : ordered_type. (* eqke is stricter than eqk *) @@ -283,35 +284,35 @@ Module KeyOrderedType(O:OrderedType). Lemma ltk_right_l : forall x k e e', ltk (k,e) x -> ltk (k,e') x. Proof. auto. Qed. - Hint Immediate ltk_right_r ltk_right_l : core. + Hint Immediate ltk_right_r ltk_right_l : ordered_type. (* eqk, eqke are equalities, ltk is a strict order *) Lemma eqk_refl : forall e, eqk e e. - Proof. auto. Qed. + Proof. auto with ordered_type. Qed. Lemma eqke_refl : forall e, eqke e e. - Proof. auto. Qed. + Proof. auto with ordered_type. Qed. Lemma eqk_sym : forall e e', eqk e e' -> eqk e' e. - Proof. auto. Qed. + Proof. auto with ordered_type. Qed. Lemma eqke_sym : forall e e', eqke e e' -> eqke e' e. Proof. unfold eqke; intuition. Qed. Lemma eqk_trans : forall e e' e'', eqk e e' -> eqk e' e'' -> eqk e e''. - Proof. eauto. Qed. + Proof. eauto with ordered_type. Qed. Lemma eqke_trans : forall e e' e'', eqke e e' -> eqke e' e'' -> eqke e e''. Proof. - unfold eqke; intuition; [ eauto | congruence ]. + unfold eqke; intuition; [ eauto with ordered_type | congruence ]. Qed. Lemma ltk_trans : forall e e' e'', ltk e e' -> ltk e' e'' -> ltk e e''. - Proof. eauto. Qed. + Proof. eauto with ordered_type. Qed. Lemma ltk_not_eqk : forall e e', ltk e e' -> ~ eqk e e'. - Proof. unfold eqk, ltk; auto. Qed. + Proof. unfold eqk, ltk; auto with ordered_type. Qed. Lemma ltk_not_eqke : forall e e', ltk e e' -> ~eqke e e'. Proof. @@ -319,18 +320,18 @@ Module KeyOrderedType(O:OrderedType). exact (lt_not_eq H H1). Qed. - Hint Resolve eqk_trans eqke_trans eqk_refl eqke_refl : core. - Hint Resolve ltk_trans ltk_not_eqk ltk_not_eqke : core. - Hint Immediate eqk_sym eqke_sym : core. + Hint Resolve eqk_trans eqke_trans eqk_refl eqke_refl : ordered_type. + Hint Resolve ltk_trans ltk_not_eqk ltk_not_eqke : ordered_type. + Hint Immediate eqk_sym eqke_sym : ordered_type. Global Instance eqk_equiv : Equivalence eqk. - Proof. constructor; eauto. Qed. + Proof. constructor; eauto with ordered_type. Qed. Global Instance eqke_equiv : Equivalence eqke. - Proof. split; eauto. Qed. + Proof. split; eauto with ordered_type. Qed. Global Instance ltk_strorder : StrictOrder ltk. - Proof. constructor; eauto. intros x; apply (irreflexivity (x:=fst x)). Qed. + Proof. constructor; eauto with ordered_type. intros x; apply (irreflexivity (x:=fst x)). Qed. Global Instance ltk_compat : Proper (eqk==>eqk==>iff) ltk. Proof. @@ -348,45 +349,45 @@ Module KeyOrderedType(O:OrderedType). Lemma eqk_not_ltk : forall x x', eqk x x' -> ~ltk x x'. Proof. - unfold eqk, ltk; simpl; auto. + unfold eqk, ltk; simpl; auto with ordered_type. Qed. Lemma ltk_eqk : forall e e' e'', ltk e e' -> eqk e' e'' -> ltk e e''. - Proof. eauto. Qed. + Proof. eauto with ordered_type. Qed. Lemma eqk_ltk : forall e e' e'', eqk e e' -> ltk e' e'' -> ltk e e''. Proof. intros (k,e) (k',e') (k'',e''). - unfold ltk, eqk; simpl; eauto. + unfold ltk, eqk; simpl; eauto with ordered_type. Qed. - Hint Resolve eqk_not_ltk : core. - Hint Immediate ltk_eqk eqk_ltk : core. + Hint Resolve eqk_not_ltk : ordered_type. + Hint Immediate ltk_eqk eqk_ltk : ordered_type. Lemma InA_eqke_eqk : forall x m, InA eqke x m -> InA eqk x m. Proof. unfold eqke; induction 1; intuition. Qed. - Hint Resolve InA_eqke_eqk : core. + Hint Resolve InA_eqke_eqk : ordered_type. Definition MapsTo (k:key)(e:elt):= InA eqke (k,e). Definition In k m := exists e:elt, MapsTo k e m. Notation Sort := (sort ltk). Notation Inf := (lelistA ltk). - Hint Unfold MapsTo In : core. + Hint Unfold MapsTo In : ordered_type. (* An alternative formulation for [In k l] is [exists e, InA eqk (k,e) l] *) Lemma In_alt : forall k l, In k l <-> exists e, InA eqk (k,e) l. - Proof. + Proof with auto with ordered_type. firstorder. - exists x; auto. + exists x... induction H. - destruct y. - exists e; auto. + destruct y. + exists e... destruct IHInA as [e H0]. - exists e; auto. + exists e... Qed. Lemma MapsTo_eq : forall l x y e, eq x y -> MapsTo x e l -> MapsTo y e l. @@ -405,8 +406,8 @@ Module KeyOrderedType(O:OrderedType). Lemma Inf_lt : forall l x x', ltk x x' -> Inf x' l -> Inf x l. Proof. exact (InfA_ltA ltk_strorder). Qed. - Hint Immediate Inf_eq : core. - Hint Resolve Inf_lt : core. + Hint Immediate Inf_eq : ordered_type. + Hint Resolve Inf_lt : ordered_type. Lemma Sort_Inf_In : forall l p q, Sort l -> Inf q l -> InA eqk p l -> ltk q p. @@ -420,8 +421,8 @@ Module KeyOrderedType(O:OrderedType). intros; red; intros. destruct H1 as [e' H2]. elim (@ltk_not_eqk (k,e) (k,e')). - eapply Sort_Inf_In; eauto. - red; simpl; auto. + eapply Sort_Inf_In; eauto with ordered_type. + red; simpl; auto with ordered_type. Qed. Lemma Sort_NoDupA: forall l, Sort l -> NoDupA eqk l. @@ -437,7 +438,7 @@ Module KeyOrderedType(O:OrderedType). Lemma Sort_In_cons_2 : forall l e e', Sort (e::l) -> InA eqk e' (e::l) -> ltk e e' \/ eqk e e'. Proof. - inversion_clear 2; auto. + inversion_clear 2; auto with ordered_type. left; apply Sort_In_cons_1 with l; auto. Qed. @@ -451,7 +452,7 @@ Module KeyOrderedType(O:OrderedType). Lemma In_inv : forall k k' e l, In k ((k',e) :: l) -> eq k k' \/ In k l. Proof. inversion 1. - inversion_clear H0; eauto. + inversion_clear H0; eauto with ordered_type. destruct H1; simpl in *; intuition. Qed. @@ -469,19 +470,19 @@ Module KeyOrderedType(O:OrderedType). End Elt. - Hint Unfold eqk eqke ltk : core. - Hint Extern 2 (eqke ?a ?b) => split : core. - Hint Resolve eqk_trans eqke_trans eqk_refl eqke_refl : core. - Hint Resolve ltk_trans ltk_not_eqk ltk_not_eqke : core. - Hint Immediate eqk_sym eqke_sym : core. - Hint Resolve eqk_not_ltk : core. - Hint Immediate ltk_eqk eqk_ltk : core. - Hint Resolve InA_eqke_eqk : core. - Hint Unfold MapsTo In : core. - Hint Immediate Inf_eq : core. - Hint Resolve Inf_lt : core. - Hint Resolve Sort_Inf_NotIn : core. - Hint Resolve In_inv_2 In_inv_3 : core. + Hint Unfold eqk eqke ltk : ordered_type. + Hint Extern 2 (eqke ?a ?b) => split : ordered_type. + Hint Resolve eqk_trans eqke_trans eqk_refl eqke_refl : ordered_type. + Hint Resolve ltk_trans ltk_not_eqk ltk_not_eqke : ordered_type. + Hint Immediate eqk_sym eqke_sym : ordered_type. + Hint Resolve eqk_not_ltk : ordered_type. + Hint Immediate ltk_eqk eqk_ltk : ordered_type. + Hint Resolve InA_eqke_eqk : ordered_type. + Hint Unfold MapsTo In : ordered_type. + Hint Immediate Inf_eq : ordered_type. + Hint Resolve Inf_lt : ordered_type. + Hint Resolve Sort_Inf_NotIn : ordered_type. + Hint Resolve In_inv_2 In_inv_3 : ordered_type. End KeyOrderedType. diff --git a/theories/Structures/OrderedTypeEx.v b/theories/Structures/OrderedTypeEx.v index 9b99fa5de4..cc216b21f8 100644 --- a/theories/Structures/OrderedTypeEx.v +++ b/theories/Structures/OrderedTypeEx.v @@ -12,7 +12,6 @@ Require Import OrderedType. Require Import ZArith. Require Import PeanoNat. Require Import Ascii String. -Require Import Omega. Require Import NArith Ndec. Require Import Compare_dec. @@ -55,7 +54,7 @@ Module Nat_as_OT <: UsualOrderedType. Proof. unfold lt; intros; apply lt_trans with y; auto. Qed. Lemma lt_not_eq : forall x y : t, lt x y -> ~ eq x y. - Proof. unfold lt, eq; intros; omega. Qed. + Proof. unfold lt, eq; intros ? ? LT ->; revert LT; apply Nat.lt_irrefl. Qed. Definition compare x y : Compare lt eq x y. Proof. @@ -85,10 +84,10 @@ Module Z_as_OT <: UsualOrderedType. Definition lt (x y:Z) := (x<y). Lemma lt_trans : forall x y z, x<y -> y<z -> x<z. - Proof. intros; omega. Qed. + Proof. exact Z.lt_trans. Qed. Lemma lt_not_eq : forall x y, x<y -> ~ x=y. - Proof. intros; omega. Qed. + Proof. intros x y LT ->; revert LT; apply Z.lt_irrefl. Qed. Definition compare x y : Compare lt eq x y. Proof. @@ -178,7 +177,7 @@ Module PairOrderedType(O1 O2:OrderedType) <: OrderedType. Lemma eq_refl : forall x : t, eq x x. Proof. - intros (x1,x2); red; simpl; auto. + intros (x1,x2); red; simpl; auto with ordered_type. Qed. Lemma eq_sym : forall x y : t, eq x y -> eq y x. @@ -188,16 +187,16 @@ Module PairOrderedType(O1 O2:OrderedType) <: OrderedType. Lemma eq_trans : forall x y z : t, eq x y -> eq y z -> eq x z. Proof. - intros (x1,x2) (y1,y2) (z1,z2); unfold eq; simpl; intuition eauto. + intros (x1,x2) (y1,y2) (z1,z2); unfold eq; simpl; intuition eauto with ordered_type. Qed. Lemma lt_trans : forall x y z : t, lt x y -> lt y z -> lt x z. Proof. intros (x1,x2) (y1,y2) (z1,z2); unfold eq, lt; simpl; intuition. - left; eauto. + left; eauto with ordered_type. left; eapply MO1.lt_eq; eauto. left; eapply MO1.eq_lt; eauto. - right; split; eauto. + right; split; eauto with ordered_type. Qed. Lemma lt_not_eq : forall x y : t, lt x y -> ~ eq x y. @@ -214,7 +213,7 @@ Module PairOrderedType(O1 O2:OrderedType) <: OrderedType. destruct (O2.compare x2 y2). apply LT; unfold lt; auto. apply EQ; unfold eq; auto. - apply GT; unfold lt; auto. + apply GT; unfold lt; auto with ordered_type. apply GT; unfold lt; auto. Defined. diff --git a/theories/ZArith/ZArith.v b/theories/ZArith/ZArith.v index b0744caa7b..38f9336f1b 100644 --- a/theories/ZArith/ZArith.v +++ b/theories/ZArith/ZArith.v @@ -18,6 +18,7 @@ Require Export Zpow_def. (** Extra modules using [Omega] or [Ring]. *) +Require Export Omega. Require Export Zcomplements. Require Export Zpower. Require Export Zdiv. diff --git a/theories/ZArith/Zcomplements.v b/theories/ZArith/Zcomplements.v index 73c8ec11c6..0be6f8c8de 100644 --- a/theories/ZArith/Zcomplements.v +++ b/theories/ZArith/Zcomplements.v @@ -10,7 +10,6 @@ Require Import ZArithRing. Require Import ZArith_base. -Require Export Omega. Require Import Wf_nat. Local Open Scope Z_scope. @@ -40,10 +39,19 @@ Proof. reflexivity. Qed. Lemma floor_ok : forall p:positive, floor p <= Zpos p < 2 * floor p. Proof. - unfold floor. induction p; simpl. - - rewrite !Pos2Z.inj_xI, (Pos2Z.inj_xO (xO _)), Pos2Z.inj_xO. omega. - - rewrite (Pos2Z.inj_xO (xO _)), (Pos2Z.inj_xO p), Pos2Z.inj_xO. omega. - - omega. + unfold floor. induction p as [p [IH1p IH2p]|p [IH1p IH2]|]; simpl. + - rewrite !Pos2Z.inj_xI, (Pos2Z.inj_xO (xO _)), Pos2Z.inj_xO. + split. + + apply Z.le_trans with (2 * Z.pos p); auto with zarith. + rewrite <- (Z.add_0_r (2 * Z.pos p)) at 1; auto with zarith. + + apply Z.lt_le_trans with (2 * (Z.pos p + 1)). + * rewrite Z.mul_add_distr_l, Z.mul_1_r. + apply Zplus_lt_compat_l; red; auto with zarith. + * apply Z.mul_le_mono_nonneg_l; auto with zarith. + rewrite Z.add_1_r; apply Zlt_le_succ; auto. + - rewrite (Pos2Z.inj_xO (xO _)), (Pos2Z.inj_xO p), Pos2Z.inj_xO. + split; auto with zarith. + - split; auto with zarith; red; auto. Qed. (**********************************************************************) @@ -64,9 +72,10 @@ Proof. - rewrite Z.abs_eq; auto; intros. destruct (H (Z.abs m)); auto with zarith. destruct (Zabs_dec m) as [-> | ->]; trivial. - - rewrite Z.abs_neq, Z.opp_involutive; auto with zarith; intros. - destruct (H (Z.abs m)); auto with zarith. - destruct (Zabs_dec m) as [-> | ->]; trivial. + - rewrite Z.abs_neq, Z.opp_involutive; intros. + + destruct (H (Z.abs m)); auto with zarith. + destruct (Zabs_dec m) as [-> | ->]; trivial. + + apply Z.opp_le_mono; rewrite Z.opp_involutive; auto. Qed. Theorem Z_lt_abs_induction : @@ -84,9 +93,10 @@ Proof. - rewrite Z.abs_eq; auto; intros. elim (H (Z.abs m)); intros; auto with zarith. elim (Zabs_dec m); intro eq; rewrite eq; trivial. - - rewrite Z.abs_neq, Z.opp_involutive; auto with zarith; intros. - destruct (H (Z.abs m)); auto with zarith. - destruct (Zabs_dec m) as [-> | ->]; trivial. + - rewrite Z.abs_neq, Z.opp_involutive; intros. + + destruct (H (Z.abs m)); auto with zarith. + destruct (Zabs_dec m) as [-> | ->]; trivial. + + apply Z.opp_le_mono; rewrite Z.opp_involutive; auto. Qed. (** To do case analysis over the sign of [z] *) @@ -129,7 +139,7 @@ Section Zlength_properties. clear l. induction l. auto with zarith. intros. simpl length; simpl Zlength_aux. - rewrite IHl, Nat2Z.inj_succ; auto with zarith. + rewrite IHl, Nat2Z.inj_succ, Z.add_succ_comm; auto. unfold Zlength. now rewrite H. Qed. diff --git a/theories/ZArith/Zdiv.v b/theories/ZArith/Zdiv.v index 78df9941c9..2aaab3e50e 100644 --- a/theories/ZArith/Zdiv.v +++ b/theories/ZArith/Zdiv.v @@ -14,7 +14,7 @@ (** Initial Contribution by Claude Marché and Xavier Urbain *) Require Export ZArith_base. -Require Import Zbool Omega ZArithRing Zcomplements Setoid Morphisms. +Require Import Zbool ZArithRing Zcomplements Setoid Morphisms. Local Open Scope Z_scope. (** The definition of the division is now in [BinIntDef], the initial @@ -67,7 +67,12 @@ Definition Remainder_alt r b := Z.abs r < Z.abs b /\ Z.sgn r <> - Z.sgn b. Lemma Remainder_equiv : forall r b, Remainder r b <-> Remainder_alt r b. Proof. - intros; unfold Remainder, Remainder_alt; omega with *. + unfold Remainder, Remainder_alt. + intros [ | r | r ] [ | b | b ]; intuition try easy. + - now apply Z.opp_lt_mono. + - right; split. + + now apply Z.opp_lt_mono. + + apply Pos2Z.neg_is_nonpos. Qed. Hint Unfold Remainder : core. @@ -104,7 +109,7 @@ Proof (Z.mod_neg_bound a b). Lemma Z_div_mod_eq a b : b > 0 -> a = b*(a/b) + (a mod b). Proof. - intros Hb; apply Z.div_mod; auto with zarith. + intros Hb; apply Z.div_mod; now intros ->. Qed. Lemma Zmod_eq_full a b : b<>0 -> a mod b = a - (a/b)*b. @@ -224,18 +229,25 @@ Proof Z.div_mul. (* Division of positive numbers is positive. *) Lemma Z_div_pos: forall a b, b > 0 -> 0 <= a -> 0 <= a/b. -Proof. intros. apply Z.div_pos; auto with zarith. Qed. +Proof. intros. apply Z.div_pos; auto using Z.gt_lt. Qed. Lemma Z_div_ge0: forall a b, b > 0 -> a >= 0 -> a/b >=0. Proof. - intros; generalize (Z_div_pos a b H); auto with zarith. + intros; apply Z.le_ge, Z_div_pos; auto using Z.ge_le. Qed. (** As soon as the divisor is greater or equal than 2, the division is strictly decreasing. *) Lemma Z_div_lt : forall a b:Z, b >= 2 -> a > 0 -> a/b < a. -Proof. intros. apply Z.div_lt; auto with zarith. Qed. +Proof. + intros a b b_ge_2 a_gt_0. + apply Z.div_lt. + - apply Z.gt_lt; exact a_gt_0. + - apply (Z.lt_le_trans _ 2). + + reflexivity. + + apply Z.ge_le; exact b_ge_2. +Qed. (** A division of a small number by a bigger one yields zero. *) @@ -250,17 +262,17 @@ Proof Z.mod_small. (** [Z.ge] is compatible with a positive division. *) Lemma Z_div_ge : forall a b c:Z, c > 0 -> a >= b -> a/c >= b/c. -Proof. intros. apply Z.le_ge. apply Z.div_le_mono; auto with zarith. Qed. +Proof. intros. apply Z.le_ge. apply Z.div_le_mono; auto using Z.gt_lt, Z.ge_le. Qed. (** Same, with [Z.le]. *) Lemma Z_div_le : forall a b c:Z, c > 0 -> a <= b -> a/c <= b/c. -Proof. intros. apply Z.div_le_mono; auto with zarith. Qed. +Proof. intros. apply Z.div_le_mono; auto using Z.gt_lt. Qed. (** With our choice of division, rounding of (a/b) is always done toward bottom: *) Lemma Z_mult_div_ge : forall a b:Z, b > 0 -> b*(a/b) <= a. -Proof. intros. apply Z.mul_div_le; auto with zarith. Qed. +Proof. intros. apply Z.mul_div_le; auto using Z.gt_lt. Qed. Lemma Z_mult_div_ge_neg : forall a b:Z, b < 0 -> b*(a/b) >= a. Proof. intros. apply Z.le_ge. apply Z.mul_div_ge; auto with zarith. Qed. @@ -296,14 +308,18 @@ Proof. intros a b q; rewrite Z.mul_comm; apply Z.div_le_lower_bound. Qed. Lemma Zdiv_le_compat_l: forall p q r, 0 <= p -> 0 < q < r -> p / r <= p / q. -Proof. intros; apply Z.div_le_compat_l; auto with zarith. Qed. +Proof. intros; apply Z.div_le_compat_l; intuition auto using Z.lt_le_incl. Qed. Theorem Zdiv_sgn: forall a b, 0 <= Z.sgn (a/b) * Z.sgn a * Z.sgn b. Proof. destruct a as [ |a|a]; destruct b as [ |b|b]; simpl; auto with zarith; generalize (Z.div_pos (Zpos a) (Zpos b)); unfold Z.div, Z.div_eucl; - destruct Z.pos_div_eucl as (q,r); destruct r; omega with *. + destruct Z.pos_div_eucl as (q,r); destruct r; + rewrite ?Z.mul_1_r, <-?Z.opp_eq_mul_m1, ?Z.sgn_opp, ?Z.opp_involutive; + match goal with [|- (_ -> _ -> ?P) -> _] => + intros HH; assert (HH1 : P); auto with zarith + end; apply Z.sgn_nonneg; auto with zarith. Qed. (** * Relations between usual operations and Z.modulo and Z.div *) @@ -346,14 +362,14 @@ Proof. intros. zero_or_not b. apply Z.div_opp_l_z; auto. Qed. Lemma Z_div_nz_opp_full : forall a b:Z, a mod b <> 0 -> (-a)/b = -(a/b)-1. -Proof. intros a b. zero_or_not b. intros; rewrite Z.div_opp_l_nz; auto. Qed. +Proof. intros a b. zero_or_not b. easy. intros; rewrite Z.div_opp_l_nz; auto. Qed. Lemma Z_div_zero_opp_r : forall a b:Z, a mod b = 0 -> a/(-b) = -(a/b). Proof. intros. zero_or_not b. apply Z.div_opp_r_z; auto. Qed. Lemma Z_div_nz_opp_r : forall a b:Z, a mod b <> 0 -> a/(-b) = -(a/b)-1. -Proof. intros a b. zero_or_not b. intros; rewrite Z.div_opp_r_nz; auto. Qed. +Proof. intros a b. zero_or_not b. easy. intros; rewrite Z.div_opp_r_nz; auto. Qed. (** Cancellations. *) @@ -372,14 +388,16 @@ Lemma Zmult_mod_distr_l: forall a b c, (c*a) mod (c*b) = c * (a mod b). Proof. intros. zero_or_not c. rewrite (Z.mul_comm c b); zero_or_not b. - rewrite (Z.mul_comm b c). apply Z.mul_mod_distr_l; auto. + + now rewrite Z.mul_0_r. + + rewrite (Z.mul_comm b c). apply Z.mul_mod_distr_l; auto. Qed. Lemma Zmult_mod_distr_r: forall a b c, (a*c) mod (b*c) = (a mod b) * c. Proof. intros. zero_or_not b. rewrite (Z.mul_comm b c); zero_or_not c. - rewrite (Z.mul_comm c b). apply Z.mul_mod_distr_r; auto. + + now rewrite Z.mul_0_r. + + rewrite (Z.mul_comm c b). apply Z.mul_mod_distr_r; auto. Qed. (** Operations modulo. *) @@ -456,7 +474,7 @@ Proof. unfold eqm; auto. Qed. Lemma eqm_trans : forall a b c, a == b -> b == c -> a == c. -Proof. unfold eqm; eauto with *. Qed. +Proof. now unfold eqm; intros a b c ->. Qed. Instance eqm_setoid : Equivalence eqm. Proof. @@ -501,7 +519,8 @@ End EqualityModulo. Lemma Zdiv_Zdiv : forall a b c, 0<=b -> 0<=c -> (a/b)/c = a/(b*c). Proof. intros. zero_or_not b. rewrite Z.mul_comm. zero_or_not c. - rewrite Z.mul_comm. apply Z.div_div; auto with zarith. + rewrite Z.mul_comm. apply Z.div_div; auto. + apply Z.le_neq; auto. Qed. (** Unfortunately, the previous result isn't always true on negative numbers. @@ -519,7 +538,10 @@ Qed. Theorem Zdiv_mult_le: forall a b c, 0<=a -> 0<=b -> 0<=c -> c*(a/b) <= (c*a)/b. Proof. - intros. zero_or_not b. apply Z.div_mul_le; auto with zarith. Qed. + intros. zero_or_not b. now rewrite Z.mul_0_r. + apply Z.div_mul_le; auto. + apply Z.le_neq; auto. +Qed. (** Z.modulo is related to divisibility (see more in Znumtheory) *) @@ -566,17 +588,17 @@ Qed. Lemma Z_div_same : forall a, a > 0 -> a/a = 1. Proof. - intros; apply Z_div_same_full; auto with zarith. + now intros; apply Z_div_same_full; intros ->. Qed. Lemma Z_div_plus : forall a b c:Z, c > 0 -> (a + b * c) / c = a / c + b. Proof. - intros; apply Z_div_plus_full; auto with zarith. + now intros; apply Z_div_plus_full; intros ->. Qed. Lemma Z_div_mult : forall a b:Z, b > 0 -> (a*b)/b = a. Proof. - intros; apply Z_div_mult_full; auto with zarith. + now intros; apply Z_div_mult_full; intros ->. Qed. Lemma Z_mod_plus : forall a b c:Z, c > 0 -> (a + b * c) mod c = a mod c. @@ -591,7 +613,7 @@ Qed. Lemma Z_div_exact_2 : forall a b:Z, b > 0 -> a mod b = 0 -> a = b*(a/b). Proof. - intros; apply Z_div_exact_full_2; auto with zarith. + now intros; apply Z_div_exact_full_2; auto; intros ->. Qed. Lemma Z_mod_zero_opp : forall a b:Z, b > 0 -> a mod b = 0 -> (-a) mod b = 0. @@ -673,14 +695,15 @@ Theorem Zdiv_eucl_extended : Proof. intros b Hb a. destruct (Z_le_gt_dec 0 b) as [Hb'|Hb']. - - assert (Hb'' : b > 0) by omega. + - assert (Hb'' : b > 0) by (apply Z.lt_gt, Z.le_neq; auto). rewrite Z.abs_eq; [ apply Zdiv_eucl_exist; assumption | assumption ]. - - assert (Hb'' : - b > 0) by omega. + - assert (Hb'' : - b > 0). + { now apply Z.lt_gt, Z.opp_lt_mono; rewrite Z.opp_involutive; apply Z.gt_lt. } destruct (Zdiv_eucl_exist Hb'' a) as ((q,r),[]). exists (- q, r). split. + rewrite <- Z.mul_opp_comm; assumption. - + rewrite Z.abs_neq; [ assumption | omega ]. + + rewrite Z.abs_neq; [ assumption | apply Z.lt_le_incl, Z.gt_lt; auto ]. Qed. Arguments Zdiv_eucl_extended : default implicits. diff --git a/theories/ZArith/Znumtheory.v b/theories/ZArith/Znumtheory.v index 5d1a13ff6c..01365135c5 100644 --- a/theories/ZArith/Znumtheory.v +++ b/theories/ZArith/Znumtheory.v @@ -117,17 +117,23 @@ Proof. right. now rewrite <- Z.mod_divide. Defined. +Lemma Z_lt_neq {x y: Z} : x < y -> y <> x. +Proof. auto using Z.lt_neq, Z.neq_sym. Qed. + Theorem Zdivide_Zdiv_eq a b : 0 < a -> (a | b) -> b = a * (b / a). Proof. intros Ha H. - rewrite (Z.div_mod b a) at 1; auto with zarith. - rewrite Zdivide_mod; auto with zarith. + rewrite (Z.div_mod b a) at 1. + + rewrite Zdivide_mod; auto with zarith. + + auto using Z_lt_neq. Qed. Theorem Zdivide_Zdiv_eq_2 a b c : 0 < a -> (a | b) -> (c * b) / a = c * (b / a). Proof. - intros. apply Z.divide_div_mul_exact; auto with zarith. + intros. apply Z.divide_div_mul_exact. + + now apply Z_lt_neq. + + auto with zarith. Qed. Theorem Zdivide_le: forall a b : Z, @@ -139,28 +145,30 @@ Qed. Theorem Zdivide_Zdiv_lt_pos a b : 1 < a -> 0 < b -> (a | b) -> 0 < b / a < b . Proof. - intros H1 H2 H3; split. - apply Z.mul_pos_cancel_l with a; auto with zarith. - rewrite <- Zdivide_Zdiv_eq; auto with zarith. - now apply Z.div_lt. + intros H1 H2 H3. + assert (0 < a) by (now transitivity 1). + split. + + apply Z.mul_pos_cancel_l with a; auto. + rewrite <- Zdivide_Zdiv_eq; auto. + + now apply Z.div_lt. Qed. Lemma Zmod_div_mod n m a: 0 < n -> 0 < m -> (n | m) -> a mod n = (a mod m) mod n. -Proof. +Proof with auto using Z_lt_neq. intros H1 H2 (p,Hp). - rewrite (Z.div_mod a m) at 1; auto with zarith. + rewrite (Z.div_mod a m) at 1... rewrite Hp at 1. - rewrite Z.mul_shuffle0, Z.add_comm, Z.mod_add; auto with zarith. + rewrite Z.mul_shuffle0, Z.add_comm, Z.mod_add... Qed. Lemma Zmod_divide_minus a b c: 0 < b -> a mod b = c -> (b | a - c). -Proof. - intros H H1. apply Z.mod_divide; auto with zarith. - rewrite Zminus_mod; auto with zarith. +Proof with auto using Z_lt_neq. + intros H H1. apply Z.mod_divide... + rewrite Zminus_mod. rewrite H1. rewrite <- (Z.mod_small c b) at 1. - rewrite Z.sub_diag, Z.mod_0_l; auto with zarith. + rewrite Z.sub_diag, Z.mod_0_l... subst. now apply Z.mod_pos_bound. Qed. @@ -169,10 +177,11 @@ Lemma Zdivide_mod_minus a b c: Proof. intros (H1, H2) H3. assert (0 < b) by Z.order. - replace a with ((a - c) + c); auto with zarith. - rewrite Z.add_mod; auto with zarith. - rewrite (Zdivide_mod (a-c) b); try rewrite Z.add_0_l; auto with zarith. - rewrite Z.mod_mod; try apply Zmod_small; auto with zarith. + assert (b <> 0) by now apply Z_lt_neq. + replace a with ((a - c) + c) by ring. + rewrite Z.add_mod; auto. + rewrite (Zdivide_mod (a-c) b); try rewrite Z.add_0_l; auto. + rewrite Z.mod_mod; try apply Zmod_small; auto. Qed. (** * Greatest common divisor (gcd). *) @@ -300,8 +309,9 @@ Section extended_euclid_algorithm. set (q := u3 / x) in *. assert (Hq : 0 <= u3 - q * x < x). replace (u3 - q * x) with (u3 mod x). - apply Z_mod_lt; omega. - assert (xpos : x > 0). omega. + apply Z_mod_lt. + apply Z.lt_gt, Z.le_neq; auto. + assert (xpos : x > 0) by (apply Z.lt_gt, Z.le_neq; auto). generalize (Z_div_mod_eq u3 x xpos). unfold q. intro eq; pattern u3 at 2; rewrite eq; ring. @@ -325,11 +335,13 @@ Section extended_euclid_algorithm. intros; apply euclid_rec with (u1 := 1) (u2 := 0) (u3 := a) (v1 := 0) (v2 := 1) (v3 := b); - auto with zarith; ring. + auto; ring. intros; apply euclid_rec with (u1 := 1) (u2 := 0) (u3 := a) (v1 := 0) (v2 := -1) (v3 := - b); - auto with zarith; try ring. + auto; try ring. + now apply Z.opp_nonneg_nonpos, Z.lt_le_incl, Z.gt_lt. + auto with zarith. Qed. End extended_euclid_algorithm. @@ -433,22 +445,24 @@ Lemma rel_prime_cross_prod : rel_prime a b -> rel_prime c d -> b > 0 -> d > 0 -> a * d = b * c -> a = c /\ b = d. Proof. - intros a b c d; intros. + intros a b c d; intros H H0 H1 H2 H3. elim (Z.divide_antisym b d). - split; auto with zarith. - rewrite H4 in H3. - rewrite Z.mul_comm in H3. - apply Z.mul_reg_l with d; auto with zarith. - intros; omega. - apply Gauss with a. - rewrite H3. - auto with zarith. - red; auto with zarith. - apply Gauss with c. - rewrite Z.mul_comm. - rewrite <- H3. - auto with zarith. - red; auto with zarith. + - split; auto with zarith. + rewrite H4 in H3. + rewrite Z.mul_comm in H3. + apply Z.mul_reg_l with d; auto. + contradict H2; rewrite H2; discriminate. + - intros H4; contradict H1; rewrite H4. + apply Zgt_asym, Z.lt_gt, Z.opp_lt_mono. + now rewrite Z.opp_involutive; apply Z.gt_lt. + - apply Gauss with a. + + rewrite H3; auto with zarith. + + now apply Zis_gcd_sym. + - apply Gauss with c. + + rewrite Z.mul_comm. + rewrite <- H3. + auto with zarith. + + now apply Zis_gcd_sym. Qed. (** After factorization by a gcd, the original numbers are relatively prime. *) @@ -457,32 +471,35 @@ Lemma Zis_gcd_rel_prime : forall a b g:Z, b > 0 -> g >= 0 -> Zis_gcd a b g -> rel_prime (a / g) (b / g). Proof. - intros a b g; intros. - assert (g <> 0). - intro. - elim H1; intros. - elim H4; intros. - rewrite H2 in H6; subst b; omega. + intros a b g; intros H H0 H1. + assert (H2 : g <> 0) by + (intro; + elim H1; intros; + elim H4; intros; + rewrite H2 in H6; subst b; + contradict H; rewrite Z.mul_0_r; discriminate). + assert (H3 : g > 0) by + (apply Z.lt_gt, Z.le_neq; split; try apply Z.ge_le; auto). unfold rel_prime. - destruct H1. - destruct H1 as (a',H1). - destruct H3 as (b',H3). + destruct H1 as [Ha Hb Hab]. + destruct Ha as [a' Ha']. + destruct Hb as [b' Hb']. replace (a/g) with a'; - [|rewrite H1; rewrite Z_div_mult; auto with zarith]. + [|rewrite Ha'; rewrite Z_div_mult; auto with zarith]. replace (b/g) with b'; - [|rewrite H3; rewrite Z_div_mult; auto with zarith]. + [|rewrite Hb'; rewrite Z_div_mult; auto with zarith]. constructor. - exists a'; auto with zarith. - exists b'; auto with zarith. - intros x (xa,H5) (xb,H6). - destruct (H4 (x*g)) as (x',Hx'). - exists xa; rewrite Z.mul_assoc; rewrite <- H5; auto. - exists xb; rewrite Z.mul_assoc; rewrite <- H6; auto. - replace g with (1*g) in Hx'; auto with zarith. - do 2 rewrite Z.mul_assoc in Hx'. - apply Z.mul_reg_r in Hx'; trivial. - rewrite Z.mul_1_r in Hx'. - exists x'; auto with zarith. + - exists a'; rewrite ?Z.mul_1_r; auto with zarith. + - exists b'; rewrite ?Z.mul_1_r; auto with zarith. + - intros x (xa,H5) (xb,H6). + destruct (Hab (x*g)) as (x',Hx'). + exists xa; rewrite Z.mul_assoc; rewrite <- H5; auto. + exists xb; rewrite Z.mul_assoc; rewrite <- H6; auto. + replace g with (1*g) in Hx'; auto with zarith. + do 2 rewrite Z.mul_assoc in Hx'. + apply Z.mul_reg_r in Hx'; trivial. + rewrite Z.mul_1_r in Hx'. + exists x'; auto with zarith. Qed. Theorem rel_prime_sym: forall a b, rel_prime a b -> rel_prime b a. @@ -504,18 +521,18 @@ Qed. Theorem rel_prime_1: forall n, rel_prime 1 n. Proof. intros n; red; apply Zis_gcd_intro; auto. - exists 1; auto with zarith. - exists n; auto with zarith. + exists 1; reflexivity. + exists n; rewrite Z.mul_1_r; reflexivity. Qed. Theorem not_rel_prime_0: forall n, 1 < n -> ~ rel_prime 0 n. Proof. intros n H H1; absurd (n = 1 \/ n = -1). - intros [H2 | H2]; subst; contradict H; auto with zarith. + intros [H2 | H2]; subst; contradict H; discriminate. case (Zis_gcd_unique 0 n n 1); auto. apply Zis_gcd_intro; auto. - exists 0; auto with zarith. - exists 1; auto with zarith. + exists 0; reflexivity. + exists 1; rewrite Z.mul_1_l; reflexivity. Qed. Theorem rel_prime_mod: forall p q, 0 < q -> @@ -528,15 +545,16 @@ Proof. apply bezout_rel_prime. apply Bezout_intro with q1 (r1 + q1 * (p / q)). rewrite <- H2. - pattern p at 3; rewrite (Z_div_mod_eq p q); try ring; auto with zarith. + pattern p at 3; rewrite (Z_div_mod_eq p q); try ring. + now apply Z.lt_gt. Qed. Theorem rel_prime_mod_rev: forall p q, 0 < q -> rel_prime (p mod q) q -> rel_prime p q. Proof. intros p q H H0. - rewrite (Z_div_mod_eq p q); auto with zarith; red. - apply Zis_gcd_sym; apply Zis_gcd_for_euclid2; auto with zarith. + rewrite (Z_div_mod_eq p q) by now apply Z.lt_gt. red. + apply Zis_gcd_sym; apply Zis_gcd_for_euclid2; auto. Qed. Theorem Zrel_prime_neq_mod_0: forall a b, 1 < b -> rel_prime a b -> a mod b <> 0. @@ -544,7 +562,8 @@ Proof. intros a b H H1 H2. case (not_rel_prime_0 _ H). rewrite <- H2. - apply rel_prime_mod; auto with zarith. + apply rel_prime_mod; auto. + now transitivity 1. Qed. (** * Primality *) @@ -563,25 +582,56 @@ Proof. assert (a = - p \/ - p < a < -1 \/ a = -1 \/ a = 0 \/ a = 1 \/ 1 < a < p \/ a = p). { assert (Z.abs a <= Z.abs p) as H2. - apply Zdivide_bounds; [ assumption | omega ]. + apply Zdivide_bounds; [ assumption | now intros -> ]. revert H2. pattern (Z.abs a); apply Zabs_ind; pattern (Z.abs p); apply Zabs_ind; - intros; omega. } + intros H2 H3 H4. + - destruct (Zle_lt_or_eq _ _ H4) as [H5 | H5]; try intuition. + destruct (Zle_lt_or_eq _ _ (Z.ge_le _ _ H3)) as [H6 | H6]; try intuition. + destruct (Zle_lt_or_eq _ _ (Zlt_le_succ _ _ H6)) as [H7 | H7]; intuition. + - contradict H2; apply Zlt_not_le; apply Z.lt_trans with (2 := H); red; auto. + - destruct (Zle_lt_or_eq _ _ H4) as [H5 | H5]. + + destruct (Zle_lt_or_eq _ _ H3) as [H6 | H6]; try intuition. + assert (H7 : a <= Z.pred 0) by (apply Z.lt_le_pred; auto). + destruct (Zle_lt_or_eq _ _ H7) as [H8 | H8]; intuition. + assert (- p < a < -1); try intuition. + now apply Z.opp_lt_mono; rewrite Z.opp_involutive. + + now left; rewrite <- H5, Z.opp_involutive. + - contradict H2. + apply Zlt_not_le; apply Z.lt_trans with (2 := H); red; auto. + } intuition idtac. (* -p < a < -1 *) - - absurd (rel_prime (- a) p); intuition. - inversion H2. - assert (- a | - a) by auto with zarith. - assert (- a | p) by auto with zarith. - apply H7, Z.divide_1_r in H8; intuition. + - absurd (rel_prime (- a) p). + + intros [H1p H2p H3p]. + assert (- a | - a) by auto with zarith. + assert (- a | p) by auto with zarith. + apply H3p, Z.divide_1_r in H5; auto with zarith. + destruct H5. + * contradict H4; rewrite <- (Z.opp_involutive a), H5 . + apply Z.lt_irrefl. + * contradict H4; rewrite <- (Z.opp_involutive a), H5 . + discriminate. + + apply H0; split. + * now apply Z.opp_le_mono; rewrite Z.opp_involutive; apply Z.lt_le_incl. + * now apply Z.opp_lt_mono; rewrite Z.opp_involutive. (* a = 0 *) - - inversion H1. subst a; omega. + - contradict H. + replace p with 0; try discriminate. + now apply sym_equal, Z.divide_0_l; rewrite <-H2. (* 1 < a < p *) - - absurd (rel_prime a p); intuition. - inversion H2. - assert (a | a) by auto with zarith. - assert (a | p) by auto with zarith. - apply H7, Z.divide_1_r in H8; intuition. + - absurd (rel_prime a p). + + intros [H1p H2p H3p]. + assert (a | a) by auto with zarith. + assert (a | p) by auto with zarith. + apply H3p, Z.divide_1_r in H5; auto with zarith. + destruct H5. + * contradict H3; rewrite <- (Z.opp_involutive a), H5 . + apply Z.lt_irrefl. + * contradict H3; rewrite <- (Z.opp_involutive a), H5 . + discriminate. + + apply H0; split; auto. + now apply Z.lt_le_incl. Qed. (** A prime number is relatively prime with any number it does not divide *) @@ -605,12 +655,17 @@ Proof. intros a p Hp [H1 H2]. apply rel_prime_sym; apply prime_rel_prime; auto. intros [q Hq]; subst a. - case (Z.le_gt_cases q 0); intros Hl. - absurd (q * p <= 0 * p); auto with zarith. - absurd (1 * p <= q * p); auto with zarith. + destruct Hp as [H3 H4]. + contradict H2; apply Zle_not_lt. + rewrite <- (Z.mul_1_l p) at 1. + apply Zmult_le_compat_r. + - apply (Zlt_le_succ 0). + apply Zmult_lt_0_reg_r with p. + + apply Z.le_succ_l, Z.lt_le_incl; auto. + + now apply Z.le_succ_l. + - apply Z.lt_le_incl, Z.le_succ_l, Z.lt_le_incl; auto. Qed. - (** If a prime [p] divides [ab] then it divides either [a] or [b] *) Lemma prime_mult : @@ -623,38 +678,44 @@ Qed. Lemma not_prime_0: ~ prime 0. Proof. - intros H1; case (prime_divisors _ H1 2); auto with zarith. + intros H1; case (prime_divisors _ H1 2); auto with zarith; intuition; discriminate. Qed. Lemma not_prime_1: ~ prime 1. Proof. - intros H1; absurd (1 < 1); auto with zarith. + intros H1; absurd (1 < 1). discriminate. inversion H1; auto. Qed. Lemma prime_2: prime 2. Proof. - apply prime_intro; auto with zarith. - intros n (H,H'); Z.le_elim H; auto with zarith. - - contradict H'; auto with zarith. - - subst n. constructor; auto with zarith. + apply prime_intro. + - red; auto. + - intros n (H,H'); Z.le_elim H; auto with zarith. + + contradict H'; auto with zarith. + now apply Zle_not_lt, (Zlt_le_succ 1). + + subst n. constructor; auto with zarith. Qed. Theorem prime_3: prime 3. Proof. apply prime_intro; auto with zarith. - intros n (H,H'); Z.le_elim H; auto with zarith. - - replace n with 2 by omega. - constructor; auto with zarith. - intros x (q,Hq) (q',Hq'). - exists (q' - q). ring_simplify. now rewrite <- Hq, <- Hq'. - - replace n with 1 by trivial. - constructor; auto with zarith. + - red; auto. + - intros n (H,H'); Z.le_elim H; auto with zarith. + + replace n with 2. + * constructor; auto with zarith. + intros x (q,Hq) (q',Hq'). + exists (q' - q). ring_simplify. now rewrite <- Hq, <- Hq'. + * apply Z.le_antisymm. + ++ now apply (Zlt_le_succ 1). + ++ now apply (Z.lt_le_pred _ 3). + + replace n with 1 by trivial. + constructor; auto with zarith. Qed. Theorem prime_ge_2 p : prime p -> 2 <= p. Proof. - intros (Hp,_); auto with zarith. + now intros (Hp,_); apply (Zlt_le_succ 1). Qed. Definition prime' p := 1<p /\ (forall n, 1<n<p -> ~ (n|p)). @@ -675,17 +736,24 @@ Proof. assert (Hx := Z.abs_nonneg x). set (y:=Z.abs x) in *; clearbody y; clear x; rename y into x. destruct (Z_0_1_more x Hx) as [->|[->|Hx']]. - + exfalso. apply Z.divide_0_l in Hxn. omega. + + exfalso. apply Z.divide_0_l in Hxn. + absurd (1 <= n). + * rewrite Hxn; red; auto. + * intuition. + now exists 1. + elim (H x); auto. split; trivial. - apply Z.le_lt_trans with n; auto with zarith. + apply Z.le_lt_trans with n; try intuition. apply Z.divide_pos_le; auto with zarith. + apply Z.lt_le_trans with (2 := H0); red; auto. - (* prime' -> prime *) constructor; trivial. intros n Hn Hnp. - case (Zis_gcd_unique n p n 1); auto with zarith. - constructor; auto with zarith. - apply H; auto with zarith. + case (Zis_gcd_unique n p n 1). + + constructor; auto with zarith. + + apply H; auto with zarith. + now intuition; apply Z.lt_le_incl. + + intros H1; intuition; subst n; discriminate. + + intros H1; intuition; subst n; discriminate. Qed. Theorem square_not_prime: forall a, ~ prime (a * a). @@ -698,7 +766,9 @@ Proof. assert (H' : 1 < a) by now apply (Z.square_lt_simpl_nonneg 1). apply (Ha' a). + split; trivial. - rewrite <- (Z.mul_1_l a) at 1. apply Z.mul_lt_mono_pos_r; omega. + rewrite <- (Z.mul_1_l a) at 1. + apply Z.mul_lt_mono_pos_r; auto. + apply Z.lt_trans with (2 := H'); red; auto. + exists a; auto. Qed. @@ -709,10 +779,11 @@ Proof. assert (Hp: 0 < p); try apply Z.lt_le_trans with 2; try apply prime_ge_2; auto with zarith. assert (Hq: 0 < q); try apply Z.lt_le_trans with 2; try apply prime_ge_2; auto with zarith. case prime_divisors with (2 := H2); auto. - intros H4; contradict Hp; subst; auto with zarith. - intros [H4| [H4 | H4]]; subst; auto. - contradict H; auto; apply not_prime_1. - contradict Hp; auto with zarith. + - intros H4; contradict Hp; subst; discriminate. + - intros [H4| [H4 | H4]]; subst; auto. + + contradict H; auto; apply not_prime_1. + + contradict Hp; apply Zle_not_lt, (Z.opp_le_mono _ 0). + now rewrite Z.opp_involutive; apply Z.lt_le_incl. Qed. (** we now prove that [Z.gcd] is indeed a gcd in @@ -748,6 +819,9 @@ Proof. apply Zgcd_is_gcd; auto. Z.le_elim H1. - generalize (Z.gcd_nonneg a b); auto with zarith. + intros H3 H4; contradict H3. + rewrite <- (Z.opp_involutive (Z.gcd a b)), <- H4. + now apply Zlt_not_le, Z.opp_lt_mono; rewrite Z.opp_involutive. - subst. now case (Z.gcd a b). Qed. @@ -801,7 +875,8 @@ Proof. case (Zis_gcd_unique a b (Z.gcd a b) 1); auto. apply Zgcd_is_gcd. intros H2; absurd (0 <= Z.gcd a b); auto with zarith. - generalize (Z.gcd_nonneg a b); auto with zarith. + - rewrite H2; red; auto. + - generalize (Z.gcd_nonneg a b); auto with zarith. Qed. Definition rel_prime_dec: forall a b, @@ -819,18 +894,25 @@ Definition prime_dec_aux: Proof. intros p m. case (Z_lt_dec 1 m); intros H1; - [ | left; intros; exfalso; omega ]. + [ | left; intros; exfalso; + contradict H1; apply Z.lt_trans with n; intuition]. pattern m; apply natlike_rec; auto with zarith. - left; intros; exfalso; omega. - intros x Hx IH; destruct IH as [F|E]. - destruct (rel_prime_dec x p) as [Y|N]. - left; intros n [HH1 HH2]. - rewrite Z.lt_succ_r in HH2. - Z.le_elim HH2; subst; auto with zarith. - - case (Z_lt_dec 1 x); intros HH1. - * right; exists x; split; auto with zarith. - * left; intros n [HHH1 HHH2]; contradict HHH1; auto with zarith. - - right; destruct E as (n,((H0,H2),H3)); exists n; auto with zarith. + - left; intros; exfalso. + absurd (1 < 0); try discriminate. + apply Z.lt_trans with n; intuition. + - intros x Hx IH; destruct IH as [F|E]. + + destruct (rel_prime_dec x p) as [Y|N]. + * left; intros n [HH1 HH2]. + rewrite Z.lt_succ_r in HH2. + Z.le_elim HH2; subst; auto with zarith. + * case (Z_lt_dec 1 x); intros HH1. + -- right; exists x; split; auto with zarith. + -- left; intros n [HHH1 HHH2]; contradict HHH1; auto with zarith. + apply Zle_not_lt; apply Z.le_trans with x. + ++ now apply Zlt_succ_le. + ++ now apply Znot_gt_le; contradict HH1; apply Z.gt_lt. + + right; destruct E as (n,((H0,H2),H3)); exists n; auto with zarith. + - apply Z.le_trans with (2 := Z.lt_le_incl _ _ H1); discriminate. Defined. Definition prime_dec: forall p, { prime p }+{ ~ prime p }. @@ -842,6 +924,7 @@ Proof. constructor; auto with zarith. * right; intros H3; inversion_clear H3 as [Hp1 Hp2]. case H2; intros n [Hn1 Hn2]; case Hn2; auto with zarith. + now apply Hp2; intuition; apply Z.lt_le_incl. + right; intros H3; inversion_clear H3 as [Hp1 Hp2]; case H1; auto. Defined. @@ -856,10 +939,15 @@ Proof. subst n; constructor; auto with zarith. - case H1; intros n (Hn1,Hn2). destruct (Z_0_1_more _ (Z.gcd_nonneg n p)) as [H|[H|H]]. - + exfalso. apply Z.gcd_eq_0_l in H. omega. + + exfalso. apply Z.gcd_eq_0_l in H. + absurd (1 < n). + * rewrite H; discriminate. + * now intuition. + elim Hn2. red. rewrite <- H. apply Zgcd_is_gcd. + exists (Z.gcd n p); split; [ split; auto | apply Z.gcd_divide_r ]. apply Z.le_lt_trans with n; auto with zarith. - apply Z.divide_pos_le; auto with zarith. - apply Z.gcd_divide_l. + * apply Z.divide_pos_le; auto with zarith. + -- apply Z.lt_trans with 1; intuition. + -- apply Z.gcd_divide_l. + * intuition. Qed. diff --git a/theories/ZArith/Zpow_facts.v b/theories/ZArith/Zpow_facts.v index 66e246616f..e65eb7cdc7 100644 --- a/theories/ZArith/Zpow_facts.v +++ b/theories/ZArith/Zpow_facts.v @@ -8,7 +8,7 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) -Require Import ZArith_base ZArithRing Zcomplements Zdiv Znumtheory. +Require Import ZArith_base ZArithRing Omega Zcomplements Zdiv Znumtheory. Require Export Zpower. Local Open Scope Z_scope. diff --git a/theories/ZArith/Zpower.v b/theories/ZArith/Zpower.v index f80d075b67..da8a9402dd 100644 --- a/theories/ZArith/Zpower.v +++ b/theories/ZArith/Zpower.v @@ -8,7 +8,7 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) -Require Import Wf_nat ZArith_base Omega Zcomplements. +Require Import Wf_nat ZArith_base Zcomplements. Require Export Zpow_def. Local Open Scope Z_scope. @@ -220,7 +220,8 @@ Section Powers_of_2. Lemma two_p_pred x : 0 <= x -> two_p (Z.pred x) < two_p x. Proof. - rewrite !two_p_equiv. intros. apply Z.pow_lt_mono_r; auto with zarith. + rewrite !two_p_equiv. intros. apply Z.pow_lt_mono_r; auto using Z.lt_pred_l. + reflexivity. Qed. End Powers_of_2. @@ -265,17 +266,45 @@ Section power_div_with_rest. let '(q,r,d) := Pos.iter Zdiv_rest_aux (x, 0, 1) p in x = q * d + r /\ 0 <= r < d. Proof. - apply Pos.iter_invariant; [|omega]. - intros ((q,r),d) (H,H'). unfold Zdiv_rest_aux. - destruct q as [ |[q|q| ]|[q|q| ]]; try omega. + apply Pos.iter_invariant; [|rewrite Z.mul_1_r, Z.add_0_r; repeat split; auto; discriminate]. + intros ((q,r),d) (H,(H1',H2')). unfold Zdiv_rest_aux. + assert (H1 : 0 < d) by now apply Z.le_lt_trans with (1 := H1'). + assert (H2 : 0 <= d + r) by now apply Z.add_nonneg_nonneg; auto; apply Z.lt_le_incl. + assert (H3 : d + r < 2 * d) + by now rewrite <-Z.add_diag; apply Zplus_lt_compat_l. + assert (H4 : r < 2 * d) by now + apply Z.lt_le_trans with (1 * d); [ + rewrite Z.mul_1_l; auto | + apply Zmult_le_compat_r; try discriminate; + now apply Z.lt_le_incl]. + destruct q as [ |[q|q| ]|[q|q| ]]. + - repeat split; auto. - rewrite Pos2Z.inj_xI, Z.mul_add_distr_r in H. - rewrite Z.mul_shuffle3, Z.mul_assoc. omega. + rewrite Z.mul_shuffle3, Z.mul_assoc. + rewrite Z.mul_1_l in H; rewrite Z.add_assoc. + repeat split; auto with zarith. - rewrite Pos2Z.inj_xO in H. - rewrite Z.mul_shuffle3, Z.mul_assoc. omega. + rewrite Z.mul_shuffle3, Z.mul_assoc. + repeat split; auto. + - rewrite Z.mul_1_l in H; repeat split; auto. - rewrite Pos2Z.neg_xI, Z.mul_sub_distr_r in H. - rewrite Z.mul_sub_distr_r, Z.mul_shuffle3, Z.mul_assoc. omega. + rewrite Z.mul_sub_distr_r, Z.mul_shuffle3, Z.mul_assoc. + repeat split; auto. + rewrite !Z.mul_1_l, H, Z.add_assoc. + apply f_equal2 with (f := Z.add); auto. + rewrite <- Z.sub_sub_distr, <- !Z.add_diag, Z.add_simpl_r. + now rewrite Z.mul_1_l. - rewrite Pos2Z.neg_xO in H. - rewrite Z.mul_shuffle3, Z.mul_assoc. omega. + rewrite Z.mul_shuffle3, Z.mul_assoc. + repeat split; auto. + - repeat split; auto. + rewrite H, (Z.mul_opp_l 1), Z.mul_1_l, Z.add_assoc. + apply f_equal2 with (f := Z.add); auto. + rewrite Z.add_comm, <- Z.add_diag. + rewrite Z.mul_add_distr_l. + replace (-1 * d) with (-d). + + now rewrite Z.add_assoc, Z.add_opp_diag_r . + + now rewrite (Z.mul_opp_l 1), <-(Z.mul_opp_l 1). Qed. (** Old-style rich specification by proof of existence *) |