diff options
| -rw-r--r-- | theories/Numbers/Cyclic/ZModulo/ZModulo.v | 6 | ||||
| -rw-r--r-- | theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v | 8 | ||||
| -rw-r--r-- | theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v | 8 | ||||
| -rw-r--r-- | theories/QArith/Qreduction.v | 16 | ||||
| -rw-r--r-- | theories/ZArith/ZArith.v | 2 | ||||
| -rw-r--r-- | theories/ZArith/Zgcd_alt.v | 1 | ||||
| -rw-r--r-- | theories/ZArith/Zgcd_def.v | 21 | ||||
| -rw-r--r-- | theories/ZArith/Znumtheory.v | 472 | ||||
| -rw-r--r-- | theories/ZArith/vo.itarget | 1 |
9 files changed, 161 insertions, 374 deletions
diff --git a/theories/Numbers/Cyclic/ZModulo/ZModulo.v b/theories/Numbers/Cyclic/ZModulo/ZModulo.v index 2d9eb395a..3bdbca44a 100644 --- a/theories/Numbers/Cyclic/ZModulo/ZModulo.v +++ b/theories/Numbers/Cyclic/ZModulo/ZModulo.v @@ -465,8 +465,8 @@ Section ZModulo. Proof. intros. generalize (Zgcd_is_gcd a b); inversion_clear 1. - destruct H2; destruct H3; clear H4. - assert (H3:=Zgcd_is_pos a b). + destruct H2 as (q,H2); destruct H3 as (q',H3); clear H4. + assert (H4:=Zgcd_is_pos a b). destruct (Z_eq_dec (Zgcd a b) 0). rewrite e; generalize (Zmax_spec a b); omega. assert (0 <= q). @@ -477,7 +477,7 @@ Section ZModulo. generalize (Zmax_spec 0 b) (Zabs_spec b); omega. apply Zle_trans with a. - rewrite H1 at 2. + rewrite H2 at 2. rewrite <- (Zmult_1_l (Zgcd a b)) at 1. apply Zmult_le_compat; auto with zarith. generalize (Zmax_spec a b); omega. diff --git a/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v b/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v index 44dd2c593..6facd3c3a 100644 --- a/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v +++ b/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v @@ -421,22 +421,22 @@ Qed. Lemma gcd_divide_l : forall n m, (gcd n m | n). Proof. - intros n m. apply spec_divide. zify. apply Zgcd_divide_l. + intros n m. apply spec_divide. zify. apply Z.gcd_divide_l. Qed. Lemma gcd_divide_r : forall n m, (gcd n m | m). Proof. - intros n m. apply spec_divide. zify. apply Zgcd_divide_r. + intros n m. apply spec_divide. zify. apply Z.gcd_divide_r. Qed. Lemma gcd_greatest : forall n m p, (p|n) -> (p|m) -> (p|gcd n m). Proof. - intros n m p. rewrite !spec_divide. zify. apply Zgcd_greatest. + intros n m p. rewrite !spec_divide. zify. apply Z.gcd_greatest. Qed. Lemma gcd_nonneg : forall n m, 0 <= gcd n m. Proof. - intros. zify. apply Zgcd_nonneg. + intros. zify. apply Z.gcd_nonneg. Qed. (** Bitwise operations *) diff --git a/theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v b/theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v index 33181e32a..57277b489 100644 --- a/theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v +++ b/theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v @@ -347,22 +347,22 @@ Qed. Lemma gcd_divide_l : forall n m, (gcd n m | n). Proof. - intros n m. apply spec_divide. zify. apply Zgcd_divide_l. + intros n m. apply spec_divide. zify. apply Z.gcd_divide_l. Qed. Lemma gcd_divide_r : forall n m, (gcd n m | m). Proof. - intros n m. apply spec_divide. zify. apply Zgcd_divide_r. + intros n m. apply spec_divide. zify. apply Z.gcd_divide_r. Qed. Lemma gcd_greatest : forall n m p, (p|n) -> (p|m) -> (p|gcd n m). Proof. - intros n m p. rewrite !spec_divide. zify. apply Zgcd_greatest. + intros n m p. rewrite !spec_divide. zify. apply Z.gcd_greatest. Qed. Lemma gcd_nonneg : forall n m, 0 <= gcd n m. Proof. - intros. zify. apply Zgcd_nonneg. + intros. zify. apply Z.gcd_nonneg. Qed. (** Bitwise operations *) diff --git a/theories/QArith/Qreduction.v b/theories/QArith/Qreduction.v index 4888ce4b1..e39eca0cb 100644 --- a/theories/QArith/Qreduction.v +++ b/theories/QArith/Qreduction.v @@ -9,7 +9,7 @@ (** Normalisation functions for rational numbers. *) Require Export QArith_base. -Require Import Zgcd_def Znumtheory. +Require Import Znumtheory. (** First, a function that (tries to) build a positive back from a Z. *) @@ -83,14 +83,13 @@ Proof. exists bb; auto with zarith. intros. inversion Hg1. - destruct (H6 (g*x)). + destruct (H6 (g*x)) as (x',Hx). rewrite Hg3. destruct H2 as (xa,Hxa); exists xa; rewrite Hxa; ring. rewrite Hg4. destruct H3 as (xb,Hxb); exists xb; rewrite Hxb; ring. - exists q. - apply Zmult_reg_l with g; auto. - pattern g at 1; rewrite H7; ring. + exists x'. + apply Zmult_reg_l with g; auto. rewrite Hx at 1; ring. (* /rel_prime *) unfold rel_prime in |- *. (* rel_prime *) @@ -99,14 +98,13 @@ Proof. exists dd; auto with zarith. intros. inversion Hg'1. - destruct (H6 (g'*x)). + destruct (H6 (g'*x)) as (x',Hx). rewrite Hg'3. destruct H2 as (xc,Hxc); exists xc; rewrite Hxc; ring. rewrite Hg'4. destruct H3 as (xd,Hxd); exists xd; rewrite Hxd; ring. - exists q. - apply Zmult_reg_l with g'; auto. - pattern g' at 1; rewrite H7; ring. + exists x'. + apply Zmult_reg_l with g'; auto. rewrite Hx at 1; ring. (* /rel_prime *) assert (0<bb); [|auto with zarith]. apply Zmult_gt_0_lt_0_reg_r with g. diff --git a/theories/ZArith/ZArith.v b/theories/ZArith/ZArith.v index e532e4ad9..a935c7dac 100644 --- a/theories/ZArith/ZArith.v +++ b/theories/ZArith/ZArith.v @@ -13,7 +13,7 @@ Require Export ZArith_base. (** Extra definitions *) Require Export - Zpow_def Zsqrt_def Zlog_def Zgcd_def Zdiv_def Zdigits_def. + Zpow_def Zsqrt_def Zlog_def Zdiv_def Zdigits_def. (** Extra modules using [Omega] or [Ring]. *) diff --git a/theories/ZArith/Zgcd_alt.v b/theories/ZArith/Zgcd_alt.v index bcb9e42ae..ebf3d0246 100644 --- a/theories/ZArith/Zgcd_alt.v +++ b/theories/ZArith/Zgcd_alt.v @@ -22,7 +22,6 @@ Author: Pierre Letouzey Require Import ZArith_base. Require Import ZArithRing. Require Import Zdiv. -Require Import Zgcd_def. Require Import Znumtheory. Open Scope Z_scope. diff --git a/theories/ZArith/Zgcd_def.v b/theories/ZArith/Zgcd_def.v deleted file mode 100644 index 674f705e5..000000000 --- a/theories/ZArith/Zgcd_def.v +++ /dev/null @@ -1,21 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(************************************************************************) - -Require Import BinPos BinInt. - -Open Local Scope Z_scope. - -Notation Zgcd := Z.gcd (only parsing). -Notation Zggcd := Z.ggcd (only parsing). -Notation Zggcd_gcd := Z.ggcd_gcd (only parsing). -Notation Zggcd_correct_divisors := Z.ggcd_correct_divisors (only parsing). -Notation Zgcd_divide_l := Z.gcd_divide_l (only parsing). -Notation Zgcd_divide_r := Z.gcd_divide_r (only parsing). -Notation Zgcd_greatest := Z.gcd_greatest (only parsing). -Notation Zgcd_nonneg := Z.gcd_nonneg (only parsing). -Notation Zggcd_opp := Z.ggcd_opp (only parsing). diff --git a/theories/ZArith/Znumtheory.v b/theories/ZArith/Znumtheory.v index bbc984af1..4371707dc 100644 --- a/theories/ZArith/Znumtheory.v +++ b/theories/ZArith/Znumtheory.v @@ -10,7 +10,6 @@ Require Import ZArith_base. Require Import ZArithRing. Require Import Zcomplements. Require Import Zdiv. -Require Import Zgcd_def. Require Import Wf_nat. (** For compatibility reasons, this Open Scope isn't local as it should *) @@ -23,313 +22,170 @@ Open Scope Z_scope. - Euclid algorithm [euclid] - a relatively prime predicate [rel_prime] - a prime predicate [prime] - - properties of the efficient [Zgcd] function defined in [Zgcd_def] + - properties of the efficient [Z.gcd] function *) -(** * Divisibility *) +Notation Zgcd := Z.gcd (only parsing). +Notation Zggcd := Z.ggcd (only parsing). +Notation Zggcd_gcd := Z.ggcd_gcd (only parsing). +Notation Zggcd_correct_divisors := Z.ggcd_correct_divisors (only parsing). +Notation Zgcd_divide_l := Z.gcd_divide_l (only parsing). +Notation Zgcd_divide_r := Z.gcd_divide_r (only parsing). +Notation Zgcd_greatest := Z.gcd_greatest (only parsing). +Notation Zgcd_nonneg := Z.gcd_nonneg (only parsing). +Notation Zggcd_opp := Z.ggcd_opp (only parsing). -Inductive Zdivide (a b:Z) : Prop := - Zdivide_intro : forall q:Z, b = q * a -> Zdivide a b. +(** The former specialized inductive predicate [Zdivide] is now + a generic existential predicate. *) -(** Syntax for divisibility *) - -Notation "( a | b )" := (Zdivide a b) (at level 0) : Z_scope. +Notation Zdivide := Z.divide (only parsing). +Notation Zdivide_intro := ex_intro (only parsing). (** Results concerning divisibility*) -Lemma Zdivide_equiv : forall a b, Z.divide a b <-> Zdivide a b. -Proof. - intros a b; split; intros (c,H); now exists c. -Qed. +Notation Zdivide_refl := Z.divide_refl (only parsing). +Notation Zone_divide := Z.divide_1_l (only parsing). +Notation Zdivide_0 := Z.divide_0_r (only parsing). +Notation Zmult_divide_compat_l := Z.mul_divide_mono_l (only parsing). +Notation Zmult_divide_compat_r := Z.mul_divide_mono_r (only parsing). +Notation Zdivide_plus_r := Z.divide_add_r (only parsing). +Notation Zdivide_minus_l := Z.divide_sub_r (only parsing). +Notation Zdivide_mult_l := Z.divide_mul_l (only parsing). +Notation Zdivide_mult_r := Z.divide_mul_r (only parsing). +Notation Zdivide_factor_r := Z.divide_factor_l (only parsing). +Notation Zdivide_factor_l := Z.divide_factor_r (only parsing). -Lemma Zdivide_refl : forall a:Z, (a | a). -Proof. - intros; apply Zdivide_intro with 1; ring. -Qed. +Lemma Zdivide_opp_r a b : (a | b) -> (a | - b). +Proof. apply Z.divide_opp_r. Qed. -Lemma Zone_divide : forall a:Z, (1 | a). -Proof. - intros; apply Zdivide_intro with a; ring. -Qed. +Lemma Zdivide_opp_r_rev a b : (a | - b) -> (a | b). +Proof. apply Z.divide_opp_r. Qed. -Lemma Zdivide_0 : forall a:Z, (a | 0). -Proof. - intros; apply Zdivide_intro with 0; ring. -Qed. +Lemma Zdivide_opp_l a b : (a | b) -> (- a | b). +Proof. apply Z.divide_opp_l. Qed. -Hint Resolve Zdivide_refl Zone_divide Zdivide_0: zarith. +Lemma Zdivide_opp_l_rev a b : (- a | b) -> (a | b). +Proof. apply Z.divide_opp_l. Qed. -Lemma Zmult_divide_compat_l : forall a b c:Z, (a | b) -> (c * a | c * b). -Proof. - simple induction 1; intros; apply Zdivide_intro with q. - rewrite H0; ring. -Qed. +Theorem Zdivide_Zabs_l a b : (Z.abs a | b) -> (a | b). +Proof. apply Z.divide_abs_l. Qed. -Lemma Zmult_divide_compat_r : forall a b c:Z, (a | b) -> (a * c | b * c). -Proof. - intros a b c; rewrite (Zmult_comm a c); rewrite (Zmult_comm b c). - apply Zmult_divide_compat_l; trivial. -Qed. +Theorem Zdivide_Zabs_inv_l a b : (a | b) -> (Z.abs a | b). +Proof. apply Z.divide_abs_l. Qed. +Hint Resolve Zdivide_refl Zone_divide Zdivide_0: zarith. Hint Resolve Zmult_divide_compat_l Zmult_divide_compat_r: zarith. - -Lemma Zdivide_plus_r : forall a b c:Z, (a | b) -> (a | c) -> (a | b + c). -Proof. - simple induction 1; intros q Hq; simple induction 1; intros q' Hq'. - apply Zdivide_intro with (q + q'). - rewrite Hq; rewrite Hq'; ring. -Qed. - -Lemma Zdivide_opp_r : forall a b:Z, (a | b) -> (a | - b). -Proof. - simple induction 1; intros; apply Zdivide_intro with (- q). - rewrite H0; ring. -Qed. - -Lemma Zdivide_opp_r_rev : forall a b:Z, (a | - b) -> (a | b). -Proof. - intros; replace b with (- - b). apply Zdivide_opp_r; trivial. ring. -Qed. - -Lemma Zdivide_opp_l : forall a b:Z, (a | b) -> (- a | b). -Proof. - simple induction 1; intros; apply Zdivide_intro with (- q). - rewrite H0; ring. -Qed. - -Lemma Zdivide_opp_l_rev : forall a b:Z, (- a | b) -> (a | b). -Proof. - intros; replace a with (- - a). apply Zdivide_opp_l; trivial. ring. -Qed. - -Lemma Zdivide_minus_l : forall a b c:Z, (a | b) -> (a | c) -> (a | b - c). -Proof. - simple induction 1; intros q Hq; simple induction 1; intros q' Hq'. - apply Zdivide_intro with (q - q'). - rewrite Hq; rewrite Hq'; ring. -Qed. - -Lemma Zdivide_mult_l : forall a b c:Z, (a | b) -> (a | b * c). -Proof. - simple induction 1; intros q Hq; apply Zdivide_intro with (q * c). - rewrite Hq; ring. -Qed. - -Lemma Zdivide_mult_r : forall a b c:Z, (a | c) -> (a | b * c). -Proof. - simple induction 1; intros q Hq; apply Zdivide_intro with (q * b). - rewrite Hq; ring. -Qed. - -Lemma Zdivide_factor_r : forall a b:Z, (a | a * b). -Proof. - intros; apply Zdivide_intro with b; ring. -Qed. - -Lemma Zdivide_factor_l : forall a b:Z, (a | b * a). -Proof. - intros; apply Zdivide_intro with b; ring. -Qed. - Hint Resolve Zdivide_plus_r Zdivide_opp_r Zdivide_opp_r_rev Zdivide_opp_l Zdivide_opp_l_rev Zdivide_minus_l Zdivide_mult_l Zdivide_mult_r Zdivide_factor_r Zdivide_factor_l: zarith. (** Auxiliary result. *) -Lemma Zmult_one : forall x y:Z, x >= 0 -> x * y = 1 -> x = 1. +Lemma Zmult_one x y : x >= 0 -> x * y = 1 -> x = 1. Proof. - intros x y H H0; destruct (Zmult_1_inversion_l _ _ H0) as [Hpos| Hneg]. - assumption. - rewrite Hneg in H; simpl in H. - contradiction (Zle_not_lt 0 (-1)). - apply Zge_le; assumption. - apply Zorder.Zlt_neg_0. + Z.swap_greater. apply Z.eq_mul_1_nonneg. Qed. (** Only [1] and [-1] divide [1]. *) -Lemma Zdivide_1 : forall x:Z, (x | 1) -> x = 1 \/ x = -1. -Proof. - simple induction 1; intros. - elim (Z_lt_ge_dec 0 x); [ left | right ]. - apply Zmult_one with q; auto with zarith; rewrite H0; ring. - assert (- x = 1); auto with zarith. - apply Zmult_one with (- q); auto with zarith; rewrite H0; ring. -Qed. +Notation Zdivide_1 := Z.divide_1_r (only parsing). (** If [a] divides [b] and [b] divides [a] then [a] is [b] or [-b]. *) -Lemma Zdivide_antisym : forall a b:Z, (a | b) -> (b | a) -> a = b \/ a = - b. -Proof. - simple induction 1; intros. - inversion H1. - rewrite H0 in H2; clear H H1. - case (Z_zerop a); intro. - left; rewrite H0; rewrite e; ring. - assert (Hqq0 : q0 * q = 1). - apply Zmult_reg_l with a. - assumption. - ring_simplify. - pattern a at 2 in |- *; rewrite H2; ring. - assert (q | 1). - rewrite <- Hqq0; auto with zarith. - elim (Zdivide_1 q H); intros. - rewrite H1 in H0; left; omega. - rewrite H1 in H0; right; omega. -Qed. - -Theorem Zdivide_trans: forall a b c, (a | b) -> (b | c) -> (a | c). -Proof. - intros a b c [d H1] [e H2]; exists (d * e); auto with zarith. - rewrite H2; rewrite H1; ring. -Qed. +Notation Zdivide_antisym := Z.divide_antisym (only parsing). +Notation Zdivide_trans := Z.divide_trans (only parsing). (** If [a] divides [b] and [b<>0] then [|a| <= |b|]. *) -Lemma Zdivide_bounds : forall a b:Z, (a | b) -> b <> 0 -> Zabs a <= Zabs b. +Lemma Zdivide_bounds a b : (a | b) -> b <> 0 -> Z.abs a <= Z.abs b. Proof. - simple induction 1; intros. - assert (Zabs b = Zabs q * Zabs a). - subst; apply Zabs_Zmult. - rewrite H2. - assert (H3 := Zabs_pos q). - assert (H4 := Zabs_pos a). - assert (Zabs q * Zabs a >= 1 * Zabs a); auto with zarith. - apply Zmult_ge_compat; auto with zarith. - elim (Z_lt_ge_dec (Zabs q) 1); [ intros | auto with zarith ]. - assert (Zabs q = 0). - omega. - assert (q = 0). - rewrite <- (Zabs_Zsgn q). - rewrite H5; auto with zarith. - subst q; omega. + intros H Hb. + rewrite <- Z.divide_abs_l, <- Z.divide_abs_r in H. + apply Z.abs_pos in Hb. + now apply Z.divide_pos_le. Qed. (** [Zdivide] can be expressed using [Zmod]. *) Lemma Zmod_divide : forall a b, b<>0 -> a mod b = 0 -> (b | a). Proof. - intros a b NZ EQ. - apply Zdivide_intro with (a/b). - rewrite (Z_div_mod_eq_full a b NZ) at 1. - rewrite EQ; ring. + apply Z.mod_divide. Qed. Lemma Zdivide_mod : forall a b, (b | a) -> a mod b = 0. Proof. - intros a b (c,->); apply Z_mod_mult. + intros a b (c,->); apply Z_mod_mult. Qed. (** [Zdivide] is hence decidable *) -Lemma Zdivide_dec : forall a b:Z, {(a | b)} + {~ (a | b)}. -Proof. - intros a b; elim (Ztrichotomy_inf a 0). - (* a<0 *) - intros H; elim H; intros. - case (Z_eq_dec (b mod - a) 0). - left; apply Zdivide_opp_l_rev; apply Zmod_divide; auto with zarith. - intro H1; right; intro; elim H1; apply Zdivide_mod; auto with zarith. - (* a=0 *) - case (Z_eq_dec b 0); intro. - left; subst; auto with zarith. - right; subst; intro H0; inversion H0; omega. - (* a>0 *) - intro H; case (Z_eq_dec (b mod a) 0). - left; apply Zmod_divide; auto with zarith. - intro H1; right; intro; elim H1; apply Zdivide_mod; auto with zarith. -Qed. - -Theorem Zdivide_Zdiv_eq: forall a b : Z, - 0 < a -> (a | b) -> b = a * (b / a). +Lemma Zdivide_dec a b : {(a | b)} + {~ (a | b)}. Proof. - intros a b Hb Hc. - pattern b at 1; rewrite (Z_div_mod_eq b a); auto with zarith. - rewrite (Zdivide_mod b a); auto with zarith. -Qed. - -Theorem Zdivide_Zdiv_eq_2: forall a b c : Z, - 0 < a -> (a | b) -> (c * b)/a = c * (b / a). -Proof. - intros a b c H1 H2. - inversion H2 as [z Hz]. - rewrite Hz; rewrite Zmult_assoc. - repeat rewrite Z_div_mult; auto with zarith. -Qed. + destruct (Z.eq_dec a 0) as [Ha|Ha]. + destruct (Z.eq_dec b 0) as [Hb|Hb]. + left; subst; apply Z.divide_0_r. + right. subst. contradict Hb. now apply Z.divide_0_l. + destruct (Z.eq_dec (b mod a) 0). + left. now apply Z.mod_divide. + right. now rewrite <- Z.mod_divide. +Defined. -Theorem Zdivide_Zabs_l: forall a b, (Zabs a | b) -> (a | b). +Theorem Zdivide_Zdiv_eq a b : 0 < a -> (a | b) -> b = a * (b / a). Proof. - intros a b [x H]; subst b. - pattern (Zabs a); apply Zabs_intro. - exists (- x); ring. - exists x; ring. + intros Ha H. + rewrite (Z.div_mod b a) at 1; auto with zarith. + rewrite Zdivide_mod; auto with zarith. Qed. -Theorem Zdivide_Zabs_inv_l: forall a b, (a | b) -> (Zabs a | b). +Theorem Zdivide_Zdiv_eq_2 a b c : + 0 < a -> (a | b) -> (c * b) / a = c * (b / a). Proof. - intros a b [x H]; subst b. - pattern (Zabs a); apply Zabs_intro. - exists (- x); ring. - exists x; ring. + intros. apply Z.divide_div_mul_exact; auto with zarith. Qed. Theorem Zdivide_le: forall a b : Z, 0 <= a -> 0 < b -> (a | b) -> a <= b. Proof. - intros a b H1 H2 [q H3]; subst b. - case (Zle_lt_or_eq 0 a); auto with zarith; intros H3. - case (Zle_lt_or_eq 0 q); auto with zarith. - apply (Zmult_le_0_reg_r a); auto with zarith. - intros H4; apply Zle_trans with (1 * a); auto with zarith. - intros H4; subst q; omega. + intros. now apply Z.divide_pos_le. Qed. -Theorem Zdivide_Zdiv_lt_pos: forall a b : Z, +Theorem Zdivide_Zdiv_lt_pos a b : 1 < a -> 0 < b -> (a | b) -> 0 < b / a < b . Proof. - intros a b H1 H2 H3; split. - apply Zmult_lt_reg_r with a; auto with zarith. - rewrite (Zmult_comm (Zdiv b a)); rewrite <- Zdivide_Zdiv_eq; auto with zarith. - apply Zmult_lt_reg_r with a; auto with zarith. - repeat rewrite (fun x => Zmult_comm x a); auto with zarith. + intros H1 H2 H3; split. + apply Z.mul_pos_cancel_l with a; auto with zarith. rewrite <- Zdivide_Zdiv_eq; auto with zarith. - pattern b at 1; replace b with (1 * b); auto with zarith. - apply Zmult_lt_compat_r; auto with zarith. + now apply Z.div_lt. Qed. -Lemma Zmod_div_mod: forall n m a, 0 < n -> 0 < m -> - (n | m) -> a mod n = (a mod m) mod n. +Lemma Zmod_div_mod n m a: + 0 < n -> 0 < m -> (n | m) -> a mod n = (a mod m) mod n. Proof. - intros n m a H1 H2 H3. - pattern a at 1; rewrite (Z_div_mod_eq a m); auto with zarith. - case H3; intros q Hq; pattern m at 1; rewrite Hq. - rewrite (Zmult_comm q). - rewrite Zplus_mod; auto with zarith. - rewrite <- Zmult_assoc; rewrite Zmult_mod; auto with zarith. - rewrite Z_mod_same; try rewrite Zmult_0_l; auto with zarith. - rewrite (Zmod_small 0); auto with zarith. - rewrite Zplus_0_l; rewrite Zmod_mod; auto with zarith. + intros H1 H2 (p,Hp). + rewrite (Z.div_mod a m) at 1; auto with zarith. + rewrite Hp at 1. + rewrite Z.mul_shuffle0, Z.add_comm, Z.mod_add; auto with zarith. Qed. -Lemma Zmod_divide_minus: forall a b c : Z, 0 < b -> - a mod b = c -> (b | a - c). +Lemma Zmod_divide_minus a b c: + 0 < b -> a mod b = c -> (b | a - c). Proof. - intros a b c H H1; apply Zmod_divide; auto with zarith. + intros H H1. apply Z.mod_divide; auto with zarith. rewrite Zminus_mod; auto with zarith. - rewrite H1; pattern c at 1; rewrite <- (Zmod_small c b); auto with zarith. - rewrite Zminus_diag; apply Zmod_small; auto with zarith. - subst; apply Z_mod_lt; auto with zarith. + rewrite H1. rewrite <- (Z.mod_small c b) at 1. + rewrite Z.sub_diag, Z.mod_0_l; auto with zarith. + subst. now apply Z.mod_pos_bound. Qed. -Lemma Zdivide_mod_minus: forall a b c : Z, 0 <= c < b -> - (b | a - c) -> a mod b = c. +Lemma Zdivide_mod_minus a b c: + 0 <= c < b -> (b | a - c) -> a mod b = c. Proof. - intros a b c (H1, H2) H3; assert (0 < b); try apply Zle_lt_trans with c; auto. + intros (H1, H2) H3. + assert (0 < b) by Z.order. replace a with ((a - c) + c); auto with zarith. - rewrite Zplus_mod; auto with zarith. - rewrite (Zdivide_mod (a -c) b); try rewrite Zplus_0_l; auto with zarith. - rewrite Zmod_mod; try apply Zmod_small; 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. Qed. (** * Greatest common divisor (gcd). *) @@ -345,12 +201,12 @@ Inductive Zis_gcd (a b d:Z) : Prop := (** Trivial properties of [gcd] *) -Lemma Zis_gcd_sym : forall a b d:Z, Zis_gcd a b d -> Zis_gcd b a d. +Lemma Zis_gcd_sym : forall a b d, Zis_gcd a b d -> Zis_gcd b a d. Proof. - simple induction 1; constructor; intuition. + induction 1; constructor; intuition. Qed. -Lemma Zis_gcd_0 : forall a:Z, Zis_gcd a 0 a. +Lemma Zis_gcd_0 : forall a, Zis_gcd a 0 a. Proof. constructor; auto with zarith. Qed. @@ -365,19 +221,18 @@ Proof. constructor; auto with zarith. Qed. -Lemma Zis_gcd_minus : forall a b d:Z, Zis_gcd a (- b) d -> Zis_gcd b a d. +Lemma Zis_gcd_minus : forall a b d, Zis_gcd a (- b) d -> Zis_gcd b a d. Proof. - simple induction 1; constructor; intuition. + induction 1; constructor; intuition. Qed. -Lemma Zis_gcd_opp : forall a b d:Z, Zis_gcd a b d -> Zis_gcd b a (- d). +Lemma Zis_gcd_opp : forall a b d, Zis_gcd a b d -> Zis_gcd b a (- d). Proof. - simple induction 1; constructor; intuition. + induction 1; constructor; intuition. Qed. -Lemma Zis_gcd_0_abs : forall a:Z, Zis_gcd 0 a (Zabs a). +Lemma Zis_gcd_0_abs a : Zis_gcd 0 a (Z.abs a). Proof. - intros a. apply Zabs_ind. intros; apply Zis_gcd_sym; apply Zis_gcd_0; auto. intros; apply Zis_gcd_opp; apply Zis_gcd_0; auto. @@ -526,14 +381,15 @@ Qed. Lemma Zis_gcd_mult : forall a b c d:Z, Zis_gcd a b d -> Zis_gcd (c * a) (c * b) (c * d). Proof. - intros a b c d; simple induction 1; constructor; intuition. - elim (Zis_gcd_bezout a b d H). intros. - elim H3; intros. - elim H4; intros. - apply Zdivide_intro with (u * q + v * q0). - rewrite <- H5. + intros a b c d; simple induction 1. constructor; auto with zarith. + intros x Ha Hb. + elim (Zis_gcd_bezout a b d H). intros u v Huv. + elim Ha; intros a' Ha'. + elim Hb; intros b' Hb'. + apply Zdivide_intro with (u * a' + v * b'). + rewrite <- Huv. replace (c * (u * a + v * b)) with (u * (c * a) + v * (c * b)). - rewrite H6; rewrite H7; ring. + rewrite Ha'; rewrite Hb'; ring. ring. Qed. @@ -632,14 +488,14 @@ Proof. exists a'; auto with zarith. exists b'; auto with zarith. intros x (xa,H5) (xb,H6). - destruct (H4 (x*g)). + destruct (H4 (x*g)) as (x',Hx'). exists xa; rewrite Zmult_assoc; rewrite <- H5; auto. exists xb; rewrite Zmult_assoc; rewrite <- H6; auto. - replace g with (1*g) in H7; auto with zarith. - do 2 rewrite Zmult_assoc in H7. - generalize (Zmult_reg_r _ _ _ H2 H7); clear H7; intros. - rewrite Zmult_1_r in H7. - exists q; auto with zarith. + replace g with (1*g) in Hx'; auto with zarith. + do 2 rewrite Zmult_assoc in Hx'. + apply Zmult_reg_r in Hx'; trivial. + rewrite Zmult_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. @@ -882,83 +738,62 @@ Proof. contradict Hp; auto with zarith. Qed. -(** we now prove that Zgcd (defined in Zgcd_def) is indeed a gcd in - the sense of Zis_gcd. *) +(** we now prove that [Z.gcd] is indeed a gcd in + the sense of [Zis_gcd]. *) -Notation Zgcd_is_pos := Zgcd_nonneg (only parsing). +Notation Zgcd_is_pos := Z.gcd_nonneg (only parsing). -Lemma Zgcd_is_gcd : forall a b, Zis_gcd a b (Zgcd a b). +Lemma Zgcd_is_gcd : forall a b, Zis_gcd a b (Z.gcd a b). Proof. - constructor; intros; apply Zdivide_equiv. - apply Zgcd_divide_l. - apply Zgcd_divide_r. - apply Zgcd_greatest; now apply Zdivide_equiv. + constructor. + apply Z.gcd_divide_l. + apply Z.gcd_divide_r. + apply Z.gcd_greatest. Qed. Theorem Zgcd_spec : forall x y : Z, {z : Z | Zis_gcd x y z /\ 0 <= z}. Proof. - intros x y; exists (Zgcd x y). - split; [apply Zgcd_is_gcd | apply Zgcd_is_pos]. + intros x y; exists (Z.gcd x y). + split; [apply Zgcd_is_gcd | apply Z.gcd_nonneg]. Qed. Theorem Zdivide_Zgcd: forall p q r : Z, - (p | q) -> (p | r) -> (p | Zgcd q r). + (p | q) -> (p | r) -> (p | Z.gcd q r). Proof. - intros p q r H1 H2. - assert (H3: (Zis_gcd q r (Zgcd q r))). - apply Zgcd_is_gcd. - inversion_clear H3; auto. + intros. now apply Z.gcd_greatest. Qed. Theorem Zis_gcd_gcd: forall a b c : Z, - 0 <= c -> Zis_gcd a b c -> Zgcd a b = c. + 0 <= c -> Zis_gcd a b c -> Z.gcd a b = c. Proof. intros a b c H1 H2. case (Zis_gcd_uniqueness_apart_sign a b c (Zgcd a b)); auto. apply Zgcd_is_gcd; auto. - case Zle_lt_or_eq with (1 := H1); clear H1; intros H1; subst; auto. - intros H3; subst. - generalize (Zgcd_is_pos a b); auto with zarith. - case (Zgcd a b); simpl; auto; intros; discriminate. + Z.le_elim H1. + generalize (Z.gcd_nonneg a b); auto with zarith. + subst. now case (Z.gcd a b). Qed. -Theorem Zgcd_inv_0_l: forall x y, Zgcd x y = 0 -> x = 0. -Proof. - intros x y H. - assert (F1: Zdivide 0 x). - rewrite <- H. - generalize (Zgcd_is_gcd x y); intros HH; inversion HH; auto. - inversion F1 as [z H1]. - rewrite H1; ring. -Qed. - -Theorem Zgcd_inv_0_r: forall x y, Zgcd x y = 0 -> y = 0. -Proof. - intros x y H. - assert (F1: Zdivide 0 y). - rewrite <- H. - generalize (Zgcd_is_gcd x y); intros HH; inversion HH; auto. - inversion F1 as [z H1]. - rewrite H1; ring. -Qed. +Notation Zgcd_inv_0_l := Z.gcd_eq_0_l (only parsing). +Notation Zgcd_inv_0_r := Z.gcd_eq_0_r (only parsing). Theorem Zgcd_div_swap0 : forall a b : Z, - 0 < Zgcd a b -> + 0 < Z.gcd a b -> 0 < b -> - (a / Zgcd a b) * b = a * (b/Zgcd a b). + (a / Z.gcd a b) * b = a * (b/Z.gcd a b). Proof. intros a b Hg Hb. assert (F := Zgcd_is_gcd a b); inversion F as [F1 F2 F3]. - pattern b at 2; rewrite (Zdivide_Zdiv_eq (Zgcd a b) b); auto. + pattern b at 2; rewrite (Zdivide_Zdiv_eq (Z.gcd a b) b); auto. repeat rewrite Zmult_assoc; f_equal. rewrite Zmult_comm. rewrite <- Zdivide_Zdiv_eq; auto. Qed. Theorem Zgcd_div_swap : forall a b c : Z, - 0 < Zgcd a b -> + 0 < Z.gcd a b -> 0 < b -> - (c * a) / Zgcd a b * b = c * a * (b/Zgcd a b). + (c * a) / Z.gcd a b * b = c * a * (b/Z.gcd a b). Proof. intros a b c Hg Hb. assert (F := Zgcd_is_gcd a b); inversion F as [F1 F2 F3]. @@ -970,44 +805,21 @@ Proof. rewrite <- Zdivide_Zdiv_eq; auto. Qed. -Lemma Zgcd_comm : forall a b, Zgcd a b = Zgcd b a. -Proof. - intros. - apply Zis_gcd_gcd. - apply Zgcd_is_pos. - apply Zis_gcd_sym. - apply Zgcd_is_gcd. -Qed. - -Lemma Zgcd_ass : forall a b c, Zgcd (Zgcd a b) c = Zgcd a (Zgcd b c). -Proof. - intros. - apply Zis_gcd_gcd. - apply Zgcd_is_pos. - destruct (Zgcd_is_gcd a b). - destruct (Zgcd_is_gcd b c). - destruct (Zgcd_is_gcd a (Zgcd b c)). - constructor; eauto using Zdivide_trans. -Qed. +Notation Zgcd_comm := Z.gcd_comm (only parsing). -Lemma Zgcd_Zabs : forall a b, Zgcd (Zabs a) b = Zgcd a b. +Lemma Zgcd_ass a b c : Zgcd (Zgcd a b) c = Zgcd a (Zgcd b c). Proof. - destruct a; simpl; auto. + symmetry. apply Z.gcd_assoc. Qed. -Lemma Zgcd_0 : forall a, Zgcd a 0 = Zabs a. -Proof. - destruct a; simpl; auto. -Qed. +Notation Zgcd_Zabs := Z.gcd_abs_l (only parsing). +Notation Zgcd_0 := Z.gcd_0_r (only parsing). +Notation Zgcd_1 := Z.gcd_1_r (only parsing). -Lemma Zgcd_1 : forall a, Zgcd a 1 = 1. -Proof. - intros; apply Zis_gcd_gcd; auto with zarith; apply Zis_gcd_1. -Qed. Hint Resolve Zgcd_0 Zgcd_1 : zarith. Theorem Zgcd_1_rel_prime : forall a b, - Zgcd a b = 1 <-> rel_prime a b. + Z.gcd a b = 1 <-> rel_prime a b. Proof. unfold rel_prime; split; intro H. rewrite <- H; apply Zgcd_is_gcd. diff --git a/theories/ZArith/vo.itarget b/theories/ZArith/vo.itarget index cf0cdd7c7..7592d2fae 100644 --- a/theories/ZArith/vo.itarget +++ b/theories/ZArith/vo.itarget @@ -32,6 +32,5 @@ Zsqrt_compat.vo Zwf.vo Zsqrt_def.vo Zlog_def.vo -Zgcd_def.vo Zeuclid.vo Zdigits_def.vo
\ No newline at end of file |