From fb2e6501516184a03fbc475921c20499f87d3aac Mon Sep 17 00:00:00 2001 From: letouzey Date: Fri, 5 Nov 2010 18:27:39 +0000 Subject: Numbers: axiomatization, properties and implementations of gcd - For nat, we create a brand-new gcd function, structural in the sense of Coq, even if it's Euclid algorithm. Cool... - We re-organize the Zgcd that was in Znumtheory, create out of it files Pgcd, Ngcd_def, Zgcd_def. Proofs of correctness are revised in order to be much simpler (no omega, no advanced lemmas of Znumtheory, etc). - Abstract Properties NZGcd / ZGcd / NGcd could still be completed, for the moment they contain up to Gauss thm. We could add stuff about (relative) primality, relationship between gcd and div,mod, or stuff about parity, etc etc. - Znumtheory remains as it was, apart for Zgcd and correctness proofs gone elsewhere. We could later take advantage of ZGcd in it. Someday, we'll have to switch from the current Zdivide inductive, to Zdivide' via exists. To be continued... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13623 85f007b7-540e-0410-9357-904b9bb8a0f7 --- theories/Numbers/Integer/Abstract/ZAxioms.v | 8 +- theories/Numbers/Integer/Abstract/ZGcd.v | 276 ++++++++++++++++++++++++ theories/Numbers/Integer/Abstract/ZProperties.v | 4 +- 3 files changed, 282 insertions(+), 6 deletions(-) create mode 100644 theories/Numbers/Integer/Abstract/ZGcd.v (limited to 'theories/Numbers/Integer/Abstract') diff --git a/theories/Numbers/Integer/Abstract/ZAxioms.v b/theories/Numbers/Integer/Abstract/ZAxioms.v index 47286c729e..754c0b3d19 100644 --- a/theories/Numbers/Integer/Abstract/ZAxioms.v +++ b/theories/Numbers/Integer/Abstract/ZAxioms.v @@ -9,7 +9,7 @@ (************************************************************************) Require Export NZAxioms. -Require Import NZPow NZSqrt NZLog. +Require Import NZPow NZSqrt NZLog NZGcd. (** We obtain integers by postulating that successor of predecessor is identity. *) @@ -70,16 +70,16 @@ Module Type Parity (Import Z : ZAxiomsMiniSig'). Axiom odd_spec : forall n, odd n = true <-> Odd n. End Parity. -(** For pow sqrt log2, the NZ axiomatizations are enough. *) +(** For pow sqrt log2 gcd, the NZ axiomatizations are enough. *) (** Let's group everything *) Module Type ZAxiomsSig := ZAxiomsMiniSig <+ HasCompare <+ HasAbs <+ HasSgn <+ Parity - <+ NZPow.NZPow <+ NZSqrt.NZSqrt <+ NZLog.NZLog2. + <+ NZPow.NZPow <+ NZSqrt.NZSqrt <+ NZLog.NZLog2 <+ NZGcd.NZGcd. Module Type ZAxiomsSig' := ZAxiomsMiniSig' <+ HasCompare <+ HasAbs <+ HasSgn <+ Parity - <+ NZPow.NZPow' <+ NZSqrt.NZSqrt' <+ NZLog.NZLog2. + <+ NZPow.NZPow' <+ NZSqrt.NZSqrt' <+ NZLog.NZLog2 <+ NZGcd.NZGcd'. (** Division is left apart, since many different flavours are available *) diff --git a/theories/Numbers/Integer/Abstract/ZGcd.v b/theories/Numbers/Integer/Abstract/ZGcd.v new file mode 100644 index 0000000000..d58d1f1e27 --- /dev/null +++ b/theories/Numbers/Integer/Abstract/ZGcd.v @@ -0,0 +1,276 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* (n | m). +Proof. + intros n m. split; intros (p,Hp); exists (-p); rewrite <- Hp. + now rewrite mul_opp_l, mul_opp_r. + now rewrite mul_opp_opp. +Qed. + +Lemma divide_opp_r : forall n m, (n | -m) <-> (n | m). +Proof. + intros n m. split; intros (p,Hp); exists (-p). + now rewrite mul_opp_r, Hp, opp_involutive. + now rewrite <- Hp, mul_opp_r. +Qed. + +Lemma divide_abs_l : forall n m, (abs n | m) <-> (n | m). +Proof. + intros n m. destruct (abs_eq_or_opp n) as [H|H]; rewrite H. + easy. apply divide_opp_l. +Qed. + +Lemma divide_abs_r : forall n m, (n | abs m) <-> (n | m). +Proof. + intros n m. destruct (abs_eq_or_opp m) as [H|H]; rewrite H. + easy. apply divide_opp_r. +Qed. + +Lemma divide_1_r_abs : forall n, (n | 1) -> abs n == 1. +Proof. + intros n Hn. apply divide_1_r_nonneg. apply abs_nonneg. + now apply divide_abs_l. +Qed. + +Lemma divide_1_r : forall n, (n | 1) -> n==1 \/ n==-(1). +Proof. + intros n (m,Hm). now apply eq_mul_1 with m. +Qed. + +Lemma divide_antisym_abs : forall n m, + (n | m) -> (m | n) -> abs n == abs m. +Proof. + intros. apply divide_antisym_nonneg; try apply abs_nonneg. + now apply divide_abs_l, divide_abs_r. + now apply divide_abs_l, divide_abs_r. +Qed. + +Lemma divide_antisym : forall n m, + (n | m) -> (m | n) -> n == m \/ n == -m. +Proof. + intros. now apply abs_eq_cases, divide_antisym_abs. +Qed. + +Lemma divide_sub_r : forall n m p, (n | m) -> (n | p) -> (n | m - p). +Proof. + intros n m p H H'. rewrite <- add_opp_r. + apply divide_add_r; trivial. now apply divide_opp_r. +Qed. + +Lemma divide_add_cancel_r : forall n m p, (n | m) -> (n | m + p) -> (n | p). +Proof. + intros n m p H H'. rewrite <- (add_simpl_l m p). now apply divide_sub_r. +Qed. + +(** Properties of gcd *) + +Lemma gcd_opp_l : forall n m, gcd (-n) m == gcd n m. +Proof. + intros. apply gcd_unique_alt; try apply gcd_nonneg. + intros. rewrite divide_opp_r. apply gcd_divide_iff. +Qed. + +Lemma gcd_opp_r : forall n m, gcd n (-m) == gcd n m. +Proof. + intros. now rewrite gcd_comm, gcd_opp_l, gcd_comm. +Qed. + +Lemma gcd_abs_l : forall n m, gcd (abs n) m == gcd n m. +Proof. + intros. destruct (abs_eq_or_opp n) as [H|H]; rewrite H. + easy. apply gcd_opp_l. +Qed. + +Lemma gcd_abs_r : forall n m, gcd n (abs m) == gcd n m. +Proof. + intros. now rewrite gcd_comm, gcd_abs_l, gcd_comm. +Qed. + +Lemma gcd_0_l : forall n, gcd 0 n == abs n. +Proof. + intros. rewrite <- gcd_abs_r. apply gcd_0_l_nonneg, abs_nonneg. +Qed. + +Lemma gcd_0_r : forall n, gcd n 0 == abs n. +Proof. + intros. now rewrite gcd_comm, gcd_0_l. +Qed. + +Lemma gcd_diag : forall n, gcd n n == abs n. +Proof. + intros. rewrite <- gcd_abs_l, <- gcd_abs_r. + apply gcd_diag_nonneg, abs_nonneg. +Qed. + +Lemma gcd_add_mult_diag_r : forall n m p, gcd n (m+p*n) == gcd n m. +Proof. + intros. apply gcd_unique_alt; try apply gcd_nonneg. + intros. rewrite gcd_divide_iff. split; intros (U,V); split; trivial. + apply divide_add_r; trivial. now apply divide_mul_r. + apply divide_add_cancel_r with (p*n); trivial. + now apply divide_mul_r. now rewrite add_comm. +Qed. + +Lemma gcd_add_diag_r : forall n m, gcd n (m+n) == gcd n m. +Proof. + intros n m. rewrite <- (mul_1_l n) at 2. apply gcd_add_mult_diag_r. +Qed. + +Lemma gcd_sub_diag_r : forall n m, gcd n (m-n) == gcd n m. +Proof. + intros n m. rewrite <- (mul_1_l n) at 2. + rewrite <- add_opp_r, <- mul_opp_l. apply gcd_add_mult_diag_r. +Qed. + +Definition Bezout n m p := exists a, exists b, a*n + b*m == p. + +Instance Bezout_wd : Proper (eq==>eq==>eq==>iff) Bezout. +Proof. + unfold Bezout. intros x x' Hx y y' Hy z z' Hz. + setoid_rewrite Hx. setoid_rewrite Hy. now setoid_rewrite Hz. +Qed. + +Lemma bezout_1_gcd : forall n m, Bezout n m 1 -> gcd n m == 1. +Proof. + intros n m (q & r & H). + apply gcd_unique; trivial using divide_1_l, le_0_1. + intros p Hn Hm. + rewrite <- H. apply divide_add_r; now apply divide_mul_r. +Qed. + +Lemma gcd_bezout : forall n m p, gcd n m == p -> Bezout n m p. +Proof. + (* First, a version restricted to natural numbers *) + assert (aux : forall n, 0<=n -> forall m, 0<=m -> Bezout n m (gcd n m)). + intros n Hn; pattern n. + apply strong_right_induction with (z:=0); trivial. + unfold Bezout. solve_predicate_wd. + clear n Hn. intros n Hn IHn. + apply le_lteq in Hn; destruct Hn as [Hn|Hn]. + intros m Hm; pattern m. + apply strong_right_induction with (z:=0); trivial. + unfold Bezout. solve_predicate_wd. + clear m Hm. intros m Hm IHm. + destruct (lt_trichotomy n m) as [LT|[EQ|LT]]. + (* n < m *) + destruct (IHm (m-n)) as (a & b & EQ). + apply sub_nonneg; order. + now apply lt_sub_pos. + exists (a-b). exists b. + rewrite gcd_sub_diag_r in EQ. rewrite <- EQ. + rewrite mul_sub_distr_r, mul_sub_distr_l. + now rewrite add_sub_assoc, add_sub_swap. + (* n = m *) + rewrite EQ. rewrite gcd_diag_nonneg; trivial. + exists 1. exists 0. now nzsimpl. + (* m < n *) + destruct (IHn m Hm LT n) as (a & b & EQ). order. + exists b. exists a. now rewrite gcd_comm, <- EQ, add_comm. + (* n = 0 *) + intros m Hm. rewrite <- Hn, gcd_0_l_nonneg; trivial. + exists 0. exists 1. now nzsimpl. + (* Then we relax the positivity condition on n *) + assert (aux' : forall n m, 0<=m -> Bezout n m (gcd n m)). + intros n m Hm. + destruct (le_ge_cases 0 n). now apply aux. + assert (Hn' : 0 <= -n) by now apply opp_nonneg_nonpos. + destruct (aux (-n) Hn' m Hm) as (a & b & EQ). + exists (-a). exists b. now rewrite <- gcd_opp_l, <- EQ, mul_opp_r, mul_opp_l. + (* And finally we do the same for m *) + intros n m p Hp. rewrite <- Hp; clear Hp. + destruct (le_ge_cases 0 m). now apply aux'. + assert (Hm' : 0 <= -m) by now apply opp_nonneg_nonpos. + destruct (aux' n (-m) Hm') as (a & b & EQ). + exists a. exists (-b). now rewrite <- gcd_opp_r, <- EQ, mul_opp_r, mul_opp_l. +Qed. + +Lemma gcd_mul_mono_l : + forall n m p, gcd (p * n) (p * m) == abs p * gcd n m. +Proof. + intros n m p. + apply gcd_unique. + apply mul_nonneg_nonneg; trivial using gcd_nonneg, abs_nonneg. + destruct (gcd_divide_l n m) as (q,Hq). + rewrite <- Hq at 2. rewrite <- (abs_sgn p) at 2. + rewrite mul_shuffle1. apply divide_factor_l. + destruct (gcd_divide_r n m) as (q,Hq). + rewrite <- Hq at 2. rewrite <- (abs_sgn p) at 2. + rewrite mul_shuffle1. apply divide_factor_l. + intros q H H'. + destruct (gcd_bezout n m (gcd n m) (eq_refl _)) as (a & b & EQ). + rewrite <- EQ, <- sgn_abs, mul_add_distr_l. apply divide_add_r. + rewrite mul_shuffle2. now apply divide_mul_l. + rewrite mul_shuffle2. now apply divide_mul_l. +Qed. + +Lemma gcd_mul_mono_l_nonneg : + forall n m p, 0<=p -> gcd (p*n) (p*m) == p * gcd n m. +Proof. + intros. rewrite <- (abs_eq p) at 3; trivial. apply gcd_mul_mono_l. +Qed. + +Lemma gcd_mul_mono_r : + forall n m p, gcd (n * p) (m * p) == gcd n m * abs p. +Proof. + intros n m p. now rewrite !(mul_comm _ p), gcd_mul_mono_l, mul_comm. +Qed. + +Lemma gcd_mul_mono_r_nonneg : + forall n m p, 0<=p -> gcd (n*p) (m*p) == gcd n m * p. +Proof. + intros. rewrite <- (abs_eq p) at 3; trivial. apply gcd_mul_mono_r. +Qed. + +Lemma gauss : forall n m p, (n | m * p) -> gcd n m == 1 -> (n | p). +Proof. + intros n m p H G. + destruct (gcd_bezout n m 1 G) as (a & b & EQ). + rewrite <- (mul_1_l p), <- EQ, mul_add_distr_r. + apply divide_add_r. rewrite mul_shuffle0. apply divide_factor_r. + rewrite <- mul_assoc. now apply divide_mul_r. +Qed. + +Lemma divide_mul_split : forall n m p, n ~= 0 -> (n | m * p) -> + exists q, exists r, n == q*r /\ (q | m) /\ (r | p). +Proof. + intros n m p Hn H. + assert (G := gcd_nonneg n m). + apply le_lteq in G; destruct G as [G|G]. + destruct (gcd_divide_l n m) as (q,Hq). + exists (gcd n m). exists q. + split. easy. + split. apply gcd_divide_r. + destruct (gcd_divide_r n m) as (r,Hr). + rewrite <- Hr in H. rewrite <- Hq in H at 1. + rewrite <- mul_assoc in H. apply mul_divide_cancel_l in H; [|order]. + apply gauss with r; trivial. + apply mul_cancel_l with (gcd n m); [order|]. + rewrite mul_1_r. + rewrite <- gcd_mul_mono_l_nonneg, Hq, Hr; order. + symmetry in G. apply gcd_eq_0 in G. destruct G as (Hn',_); order. +Qed. + +(** TODO : relation between gcd and division and modulo *) + +(** TODO : more about rel_prime (i.e. gcd == 1), about prime ... *) + +End ZGcdProp. diff --git a/theories/Numbers/Integer/Abstract/ZProperties.v b/theories/Numbers/Integer/Abstract/ZProperties.v index d2e9626737..6fbf0f23db 100644 --- a/theories/Numbers/Integer/Abstract/ZProperties.v +++ b/theories/Numbers/Integer/Abstract/ZProperties.v @@ -6,10 +6,10 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -Require Export ZAxioms ZMaxMin ZSgnAbs ZParity ZPow. +Require Export ZAxioms ZMaxMin ZSgnAbs ZParity ZPow ZGcd. (** This functor summarizes all known facts about Z. *) Module Type ZProp (Z:ZAxiomsSig) := ZMaxMinProp Z <+ ZSgnAbsProp Z <+ ZParityProp Z <+ ZPowProp Z - <+ NZSqrt.NZSqrtProp Z Z <+ NZLog.NZLog2Prop Z Z Z. + <+ NZSqrt.NZSqrtProp Z Z <+ NZLog.NZLog2Prop Z Z Z <+ ZGcdProp Z. -- cgit v1.2.3