diff options
Diffstat (limited to 'theories/ZArith')
| -rw-r--r-- | theories/ZArith/BinInt.v | 208 | ||||
| -rw-r--r-- | theories/ZArith/Int.v | 47 | ||||
| -rw-r--r-- | theories/ZArith/ZArith_dec.v | 2 | ||||
| -rw-r--r-- | theories/ZArith/ZOdiv.v | 953 | ||||
| -rw-r--r-- | theories/ZArith/ZOdiv_def.v | 136 | ||||
| -rw-r--r-- | theories/ZArith/Zabs.v | 129 | ||||
| -rw-r--r-- | theories/ZArith/Zbool.v | 16 | ||||
| -rw-r--r-- | theories/ZArith/Zcomplements.v | 8 | ||||
| -rw-r--r-- | theories/ZArith/Zdiv.v | 1068 | ||||
| -rw-r--r-- | theories/ZArith/Zeven.v | 130 | ||||
| -rw-r--r-- | theories/ZArith/Zgcd_alt.v | 317 | ||||
| -rw-r--r-- | theories/ZArith/Zmax.v | 60 | ||||
| -rw-r--r-- | theories/ZArith/Zmin.v | 20 | ||||
| -rw-r--r-- | theories/ZArith/Zmisc.v | 29 | ||||
| -rw-r--r-- | theories/ZArith/Znat.v | 207 | ||||
| -rw-r--r-- | theories/ZArith/Znumtheory.v | 750 | ||||
| -rw-r--r-- | theories/ZArith/Zorder.v | 32 | ||||
| -rw-r--r-- | theories/ZArith/Zpow_facts.v | 465 | ||||
| -rw-r--r-- | theories/ZArith/Zpower.v | 126 | ||||
| -rw-r--r-- | theories/ZArith/Zsqrt.v | 53 |
20 files changed, 4191 insertions, 565 deletions
diff --git a/theories/ZArith/BinInt.v b/theories/ZArith/BinInt.v index 71e48360..1ff88604 100644 --- a/theories/ZArith/BinInt.v +++ b/theories/ZArith/BinInt.v @@ -6,10 +6,10 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: BinInt.v 9245 2006-10-17 12:53:34Z notin $ i*) +(*i $Id: BinInt.v 11015 2008-05-28 20:06:42Z herbelin $ i*) (***********************************************************) -(** Binary Integers (Pierre Crégut, CNET, Lannion, France) *) +(** Binary Integers (Pierre Crégut, CNET, Lannion, France) *) (***********************************************************) Require Export BinPos. @@ -40,43 +40,48 @@ Arguments Scope Zneg [positive_scope]. Definition Zdouble_plus_one (x:Z) := match x with | Z0 => Zpos 1 - | Zpos p => Zpos (xI p) + | Zpos p => Zpos p~1 | Zneg p => Zneg (Pdouble_minus_one p) end. Definition Zdouble_minus_one (x:Z) := match x with | Z0 => Zneg 1 - | Zneg p => Zneg (xI p) + | Zneg p => Zneg p~1 | Zpos p => Zpos (Pdouble_minus_one p) end. Definition Zdouble (x:Z) := match x with | Z0 => Z0 - | Zpos p => Zpos (xO p) - | Zneg p => Zneg (xO p) + | Zpos p => Zpos p~0 + | Zneg p => Zneg p~0 end. +Open Local Scope positive_scope. + Fixpoint ZPminus (x y:positive) {struct y} : Z := match x, y with - | xI x', xI y' => Zdouble (ZPminus x' y') - | xI x', xO y' => Zdouble_plus_one (ZPminus x' y') - | xI x', xH => Zpos (xO x') - | xO x', xI y' => Zdouble_minus_one (ZPminus x' y') - | xO x', xO y' => Zdouble (ZPminus x' y') - | xO x', xH => Zpos (Pdouble_minus_one x') - | xH, xI y' => Zneg (xO y') - | xH, xO y' => Zneg (Pdouble_minus_one y') - | xH, xH => Z0 + | p~1, q~1 => Zdouble (ZPminus p q) + | p~1, q~0 => Zdouble_plus_one (ZPminus p q) + | p~1, 1 => Zpos p~0 + | p~0, q~1 => Zdouble_minus_one (ZPminus p q) + | p~0, q~0 => Zdouble (ZPminus p q) + | p~0, 1 => Zpos (Pdouble_minus_one p) + | 1, q~1 => Zneg q~0 + | 1, q~0 => Zneg (Pdouble_minus_one q) + | 1, 1 => Z0 end. +Close Local Scope positive_scope. + (** ** Addition on integers *) Definition Zplus (x y:Z) := match x, y with | Z0, y => y - | x, Z0 => x + | Zpos x', Z0 => Zpos x' + | Zneg x', Z0 => Zneg x' | Zpos x', Zpos y' => Zpos (x' + y') | Zpos x', Zneg y' => match (x' ?= y')%positive Eq with @@ -217,6 +222,7 @@ Qed. (**********************************************************************) + (** ** Properties of opposite on binary integer numbers *) Theorem Zopp_neg : forall p:positive, - Zneg p = Zpos p. @@ -247,30 +253,6 @@ Proof. | simplify_eq H; intro E; rewrite E; trivial ]. Qed. -(*************************************************************************) -(** ** Properties of the direct definition of successor and predecessor *) - -Lemma Zpred'_succ' : forall n:Z, Zpred' (Zsucc' n) = n. -Proof. - intro x; destruct x; simpl in |- *. - reflexivity. - destruct p; simpl in |- *; try rewrite Pdouble_minus_one_o_succ_eq_xI; - reflexivity. - destruct p; simpl in |- *; try rewrite Psucc_o_double_minus_one_eq_xO; - reflexivity. -Qed. - -Lemma Zsucc'_discr : forall n:Z, n <> Zsucc' n. -Proof. - intro x; destruct x; simpl in |- *. - discriminate. - injection; apply Psucc_discr. - destruct p; simpl in |- *. - discriminate. - intro H; symmetry in H; injection H; apply double_moins_un_xO_discr. - discriminate. -Qed. - (**********************************************************************) (** ** Other properties of binary integer numbers *) @@ -313,10 +295,15 @@ Qed. Theorem Zopp_plus_distr : forall n m:Z, - (n + m) = - n + - m. Proof. intro x; destruct x as [| p| p]; intro y; destruct y as [| q| q]; - simpl in |- *; reflexivity || destruct ((p ?= q)%positive Eq); + simpl in |- *; reflexivity || destruct ((p ?= q)%positive Eq); reflexivity. Qed. +Theorem Zopp_succ : forall n:Z, Zopp (Zsucc n) = Zpred (Zopp n). +Proof. +intro; unfold Zsucc; now rewrite Zopp_plus_distr. +Qed. + (** ** opposite is inverse for addition *) Theorem Zplus_opp_r : forall n:Z, n + - n = Z0. @@ -520,11 +507,13 @@ Proof. trivial with arith. Qed. -Lemma Zplus_succ_r : forall n m:Z, Zsucc (n + m) = n + Zsucc m. +Lemma Zplus_succ_r_reverse : forall n m:Z, Zsucc (n + m) = n + Zsucc m. Proof. intros n m; unfold Zsucc in |- *; rewrite Zplus_assoc; trivial with arith. Qed. +Notation Zplus_succ_r := Zplus_succ_r_reverse (only parsing). + Lemma Zplus_succ_comm : forall n m:Z, Zsucc n + m = n + Zsucc m. Proof. unfold Zsucc in |- *; intros n m; rewrite <- Zplus_assoc; @@ -586,10 +575,10 @@ Theorem Zsucc_pred : forall n:Z, n = Zsucc (Zpred n). Proof. intros n; unfold Zsucc, Zpred in |- *; rewrite <- Zplus_assoc; simpl in |- *; rewrite Zplus_0_r; trivial with arith. -Qed. +Qed. Hint Immediate Zsucc_pred: zarith. - + Theorem Zpred_succ : forall n:Z, n = Zpred (Zsucc n). Proof. intros m; unfold Zpred, Zsucc in |- *; rewrite <- Zplus_assoc; simpl in |- *; @@ -603,7 +592,59 @@ Proof. do 2 rewrite <- Zplus_assoc; do 2 rewrite (Zplus_comm (Zpos 1)); unfold Zsucc in H; rewrite H; trivial with arith. Qed. - + +(*************************************************************************) +(** ** Properties of the direct definition of successor and predecessor *) + +Theorem Zsucc_succ' : forall n:Z, Zsucc n = Zsucc' n. +Proof. +destruct n as [| p | p]; simpl. +reflexivity. +now rewrite Pplus_one_succ_r. +now destruct p as [q | q |]. +Qed. + +Theorem Zpred_pred' : forall n:Z, Zpred n = Zpred' n. +Proof. +destruct n as [| p | p]; simpl. +reflexivity. +now destruct p as [q | q |]. +now rewrite Pplus_one_succ_r. +Qed. + +Theorem Zsucc'_inj : forall n m:Z, Zsucc' n = Zsucc' m -> n = m. +Proof. +intros n m; do 2 rewrite <- Zsucc_succ'; now apply Zsucc_inj. +Qed. + +Theorem Zsucc'_pred' : forall n:Z, Zsucc' (Zpred' n) = n. +Proof. +intro; rewrite <- Zsucc_succ'; rewrite <- Zpred_pred'; +symmetry; apply Zsucc_pred. +Qed. + +Theorem Zpred'_succ' : forall n:Z, Zpred' (Zsucc' n) = n. +Proof. +intro; apply Zsucc'_inj; now rewrite Zsucc'_pred'. +Qed. + +Theorem Zpred'_inj : forall n m:Z, Zpred' n = Zpred' m -> n = m. +Proof. +intros n m H. +rewrite <- (Zsucc'_pred' n); rewrite <- (Zsucc'_pred' m); now rewrite H. +Qed. + +Theorem Zsucc'_discr : forall n:Z, n <> Zsucc' n. +Proof. + intro x; destruct x; simpl in |- *. + discriminate. + injection; apply Psucc_discr. + destruct p; simpl in |- *. + discriminate. + intro H; symmetry in H; injection H; apply double_moins_un_xO_discr. + discriminate. +Qed. + (** Misc properties, usually redundant or non natural *) Lemma Zsucc_eq_compat : forall n m:Z, n = m -> Zsucc n = Zsucc m. @@ -645,6 +686,22 @@ Qed. (** ** Relating [minus] with [plus] and [Zsucc] *) +Lemma Zminus_plus_distr : forall n m p:Z, n - (m + p) = n - m - p. +Proof. +intros; unfold Zminus; rewrite Zopp_plus_distr; apply Zplus_assoc. +Qed. + +Lemma Zminus_succ_l : forall n m:Z, Zsucc (n - m) = Zsucc n - m. +Proof. + intros n m; unfold Zminus, Zsucc in |- *; rewrite (Zplus_comm n (- m)); + rewrite <- Zplus_assoc; apply Zplus_comm. +Qed. + +Lemma Zminus_succ_r : forall n m:Z, n - (Zsucc m) = Zpred (n - m). +Proof. +intros; unfold Zsucc; now rewrite Zminus_plus_distr. +Qed. + Lemma Zplus_minus_eq : forall n m p:Z, n = m + p -> p = n - m. Proof. intros n m p H; unfold Zminus in |- *; apply (Zplus_reg_l m); @@ -665,12 +722,6 @@ Proof. apply Zplus_0_r. Qed. -Lemma Zminus_succ_l : forall n m:Z, Zsucc (n - m) = Zsucc n - m. -Proof. - intros n m; unfold Zminus, Zsucc in |- *; rewrite (Zplus_comm n (- m)); - rewrite <- Zplus_assoc; apply Zplus_comm. -Qed. - Lemma Zminus_plus_simpl_l : forall n m p:Z, p + n - (p + m) = n - m. Proof. intros n m p; unfold Zminus in |- *; rewrite Zopp_plus_distr; @@ -696,6 +747,16 @@ Proof. reflexivity. Qed. +Lemma Zpos_minus_morphism : forall a b:positive, Pcompare a b Eq = Lt -> + Zpos (b-a) = Zpos b - Zpos a. +Proof. + intros. + simpl. + change Eq with (CompOpp Eq). + rewrite <- Pcompare_antisym. + rewrite H; simpl; auto. +Qed. + (** ** Misc redundant properties *) Lemma Zeq_minus : forall n m:Z, n = m -> n - m = Z0. @@ -805,6 +866,19 @@ Proof. reflexivity). Qed. +(** ** Multiplication and Doubling *) + +Lemma Zdouble_mult : forall z, Zdouble z = (Zpos 2) * z. +Proof. + reflexivity. +Qed. + +Lemma Zdouble_plus_one_mult : forall z, + Zdouble_plus_one z = (Zpos 2) * z + (Zpos 1). +Proof. + destruct z; simpl; auto with zarith. +Qed. + (** ** Multiplication and Opposite *) Theorem Zopp_mult_distr_l : forall n m:Z, - (n * m) = - n * m. @@ -967,22 +1041,37 @@ Qed. (**********************************************************************) (** * Relating binary positive numbers and binary integers *) -Lemma Zpos_xI : forall p:positive, Zpos (xI p) = Zpos 2 * Zpos p + Zpos 1. +Lemma Zpos_eq : forall p q:positive, p = q -> Zpos p = Zpos q. +Proof. + intros; f_equal; auto. +Qed. + +Lemma Zpos_eq_rev : forall p q:positive, Zpos p = Zpos q -> p = q. +Proof. + inversion 1; auto. +Qed. + +Lemma Zpos_eq_iff : forall p q:positive, p = q <-> Zpos p = Zpos q. +Proof. + split; [apply Zpos_eq|apply Zpos_eq_rev]. +Qed. + +Lemma Zpos_xI : forall p:positive, Zpos p~1 = Zpos 2 * Zpos p + Zpos 1. Proof. intro; apply refl_equal. Qed. -Lemma Zpos_xO : forall p:positive, Zpos (xO p) = Zpos 2 * Zpos p. +Lemma Zpos_xO : forall p:positive, Zpos p~0 = Zpos 2 * Zpos p. Proof. intro; apply refl_equal. Qed. -Lemma Zneg_xI : forall p:positive, Zneg (xI p) = Zpos 2 * Zneg p - Zpos 1. +Lemma Zneg_xI : forall p:positive, Zneg p~1 = Zpos 2 * Zneg p - Zpos 1. Proof. intro; apply refl_equal. Qed. -Lemma Zneg_xO : forall p:positive, Zneg (xO p) = Zpos 2 * Zneg p. +Lemma Zneg_xO : forall p:positive, Zneg p~0 = Zpos 2 * Zneg p. Proof. reflexivity. Qed. @@ -1057,7 +1146,8 @@ Definition Zabs_N (z:Z) := | Zneg p => Npos p end. -Definition Z_of_N (x:N) := match x with - | N0 => Z0 - | Npos p => Zpos p - end. +Definition Z_of_N (x:N) := + match x with + | N0 => Z0 + | Npos p => Zpos p + end. diff --git a/theories/ZArith/Int.v b/theories/ZArith/Int.v index 3cee9190..fcb44d6f 100644 --- a/theories/ZArith/Int.v +++ b/theories/ZArith/Int.v @@ -7,11 +7,11 @@ (***********************************************************************) (* Finite sets library. - * Authors: Pierre Letouzey and Jean-Christophe Filliâtre - * Institution: LRI, CNRS UMR 8623 - Université Paris Sud + * Authors: Pierre Letouzey and Jean-Christophe Filliâtre + * Institution: LRI, CNRS UMR 8623 - Université Paris Sud * 91405 Orsay, France *) -(* $Id: Int.v 9319 2006-10-30 12:41:21Z barras $ *) +(* $Id: Int.v 10739 2008-04-01 14:45:20Z herbelin $ *) (** An axiomatization of integers. *) @@ -352,46 +352,15 @@ Module MoreInt (I:Int). Ltac i2z_refl := i2z_gen; match goal with |- ?t => - let e := p2ep t - in - (change (ep2p e); - apply norm_ep_correct2; - simpl) + let e := p2ep t in + change (ep2p e); apply norm_ep_correct2; simpl end. - Ltac iauto := i2z_refl; auto. - Ltac iomega := i2z_refl; intros; romega. - - Open Scope Z_scope. - - Lemma max_spec : forall (x y:Z), - x >= y /\ Zmax x y = x \/ - x < y /\ Zmax x y = y. - Proof. - intros; unfold Zmax, Zlt, Zge. - destruct (Zcompare x y); [ left | right | left ]; split; auto; discriminate. - Qed. - - Ltac omega_max_genspec x y := - generalize (max_spec x y); - (let z := fresh "z" in let Hz := fresh "Hz" in - set (z:=Zmax x y); clearbody z). - - Ltac omega_max_loop := - match goal with - (* hack: we don't want [i2z (height ...)] to be reduced by romega later... *) - | |- context [ i2z (?f ?x) ] => - let i := fresh "i2z" in (set (i:=i2z (f x)); clearbody i); omega_max_loop - | |- context [ Zmax ?x ?y ] => omega_max_genspec x y; omega_max_loop - | _ => intros - end. - - Ltac omega_max := i2z_refl; omega_max_loop; try romega. + (* i2z_refl can be replaced below by (simpl in *; i2z). + The reflexive version improves compilation of AVL files by about 15% *) - Ltac false_omega := i2z_refl; intros; romega. - Ltac false_omega_max := elimtype False; omega_max. + Ltac omega_max := i2z_refl; romega with Z. - Open Scope Int_scope. End MoreInt. diff --git a/theories/ZArith/ZArith_dec.v b/theories/ZArith/ZArith_dec.v index 7febbf6a..b831afee 100644 --- a/theories/ZArith/ZArith_dec.v +++ b/theories/ZArith/ZArith_dec.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: ZArith_dec.v 9958 2007-07-06 22:47:40Z letouzey $ i*) +(*i $Id: ZArith_dec.v 9759 2007-04-12 17:46:54Z notin $ i*) Require Import Sumbool. diff --git a/theories/ZArith/ZOdiv.v b/theories/ZArith/ZOdiv.v new file mode 100644 index 00000000..03e061f2 --- /dev/null +++ b/theories/ZArith/ZOdiv.v @@ -0,0 +1,953 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + + +Require Import BinPos BinNat Nnat ZArith_base ROmega ZArithRing. +Require Export ZOdiv_def. +Require Zdiv. + +Open Scope Z_scope. + +(** This file provides results about the Round-Toward-Zero Euclidean + division [ZOdiv_eucl], whose projections are [ZOdiv] and [ZOmod]. + Definition of this division can be found in file [ZOdiv_def]. + + This division and the one defined in Zdiv agree only on positive + numbers. Otherwise, Zdiv performs Round-Toward-Bottom. + + The current approach is compatible with the division of usual + programming languages such as Ocaml. In addition, it has nicer + properties with respect to opposite and other usual operations. +*) + +(** Since ZOdiv and Zdiv are not meant to be used concurrently, + we reuse the same notation. *) + +Infix "/" := ZOdiv : Z_scope. +Infix "mod" := ZOmod (at level 40, no associativity) : Z_scope. + +Infix "/" := Ndiv : N_scope. +Infix "mod" := Nmod (at level 40, no associativity) : N_scope. + +(** Auxiliary results on the ad-hoc comparison [NPgeb]. *) + +Lemma NPgeb_Zge : forall (n:N)(p:positive), + NPgeb n p = true -> Z_of_N n >= Zpos p. +Proof. + destruct n as [|n]; simpl; intros. + discriminate. + red; simpl; destruct Pcompare; now auto. +Qed. + +Lemma NPgeb_Zlt : forall (n:N)(p:positive), + NPgeb n p = false -> Z_of_N n < Zpos p. +Proof. + destruct n as [|n]; simpl; intros. + red; auto. + red; simpl; destruct Pcompare; now auto. +Qed. + +(** * Relation between division on N and on Z. *) + +Lemma Ndiv_Z0div : forall a b:N, + Z_of_N (a/b) = (Z_of_N a / Z_of_N b). +Proof. + intros. + destruct a; destruct b; simpl; auto. + unfold Ndiv, ZOdiv; simpl; destruct Pdiv_eucl; auto. +Qed. + +Lemma Nmod_Z0mod : forall a b:N, + Z_of_N (a mod b) = (Z_of_N a) mod (Z_of_N b). +Proof. + intros. + destruct a; destruct b; simpl; auto. + unfold Nmod, ZOmod; simpl; destruct Pdiv_eucl; auto. +Qed. + +(** * Characterization of this euclidean division. *) + +(** First, the usual equation [a=q*b+r]. Notice that [a mod 0] + has been chosen to be [a], so this equation holds even for [b=0]. +*) + +Theorem N_div_mod_eq : forall a b, + a = (b * (Ndiv a b) + (Nmod a b))%N. +Proof. + intros; generalize (Ndiv_eucl_correct a b). + unfold Ndiv, Nmod; destruct Ndiv_eucl; simpl. + intro H; rewrite H; rewrite Nmult_comm; auto. +Qed. + +Theorem ZO_div_mod_eq : forall a b, + a = b * (ZOdiv a b) + (ZOmod a b). +Proof. + intros; generalize (ZOdiv_eucl_correct a b). + unfold ZOdiv, ZOmod; destruct ZOdiv_eucl; simpl. + intro H; rewrite H; rewrite Zmult_comm; auto. +Qed. + +(** Then, the inequalities constraining the remainder. *) + +Theorem Pdiv_eucl_remainder : forall a b:positive, + Z_of_N (snd (Pdiv_eucl a b)) < Zpos b. +Proof. + induction a; cbv beta iota delta [Pdiv_eucl]; fold Pdiv_eucl; cbv zeta. + intros b; generalize (IHa b); case Pdiv_eucl. + intros q1 r1 Hr1; simpl in Hr1. + case_eq (NPgeb (2*r1+1) b); intros; unfold snd. + romega with *. + apply NPgeb_Zlt; auto. + intros b; generalize (IHa b); case Pdiv_eucl. + intros q1 r1 Hr1; simpl in Hr1. + case_eq (NPgeb (2*r1) b); intros; unfold snd. + romega with *. + apply NPgeb_Zlt; auto. + destruct b; simpl; romega with *. +Qed. + +Theorem Nmod_lt : forall (a b:N), b<>0%N -> + (a mod b < b)%N. +Proof. + destruct b as [ |b]; intro H; try solve [elim H;auto]. + destruct a as [ |a]; try solve [compute;auto]; unfold Nmod, Ndiv_eucl. + generalize (Pdiv_eucl_remainder a b); destruct Pdiv_eucl; simpl. + romega with *. +Qed. + +(** The remainder is bounded by the divisor, in term of absolute values *) + +Theorem ZOmod_lt : forall a b:Z, b<>0 -> + Zabs (a mod b) < Zabs b. +Proof. + destruct b as [ |b|b]; intro H; try solve [elim H;auto]; + destruct a as [ |a|a]; try solve [compute;auto]; unfold ZOmod, ZOdiv_eucl; + generalize (Pdiv_eucl_remainder a b); destruct Pdiv_eucl; simpl; + try rewrite Zabs_Zopp; rewrite Zabs_eq; auto; apply Z_of_N_le_0. +Qed. + +(** The sign of the remainder is the one of [a]. Due to the possible + nullity of [a], a general result is to be stated in the following form: +*) + +Theorem ZOmod_sgn : forall a b:Z, + 0 <= Zsgn (a mod b) * Zsgn a. +Proof. + destruct b as [ |b|b]; destruct a as [ |a|a]; simpl; auto with zarith; + unfold ZOmod, ZOdiv_eucl; destruct Pdiv_eucl; + simpl; destruct n0; simpl; auto with zarith. +Qed. + +(** This can also be said in a simplier way: *) + +Theorem Zsgn_pos_iff : forall z, 0 <= Zsgn z <-> 0 <= z. +Proof. + destruct z; simpl; intuition auto with zarith. +Qed. + +Theorem ZOmod_sgn2 : forall a b:Z, + 0 <= (a mod b) * a. +Proof. + intros; rewrite <-Zsgn_pos_iff, Zsgn_Zmult; apply ZOmod_sgn. +Qed. + +(** Reformulation of [ZOdiv_lt] and [ZOmod_sgn] in 2 + then 4 particular cases. *) + +Theorem ZOmod_lt_pos : forall a b:Z, 0<=a -> b<>0 -> + 0 <= a mod b < Zabs b. +Proof. + intros. + assert (0 <= a mod b). + generalize (ZOmod_sgn a b). + destruct (Zle_lt_or_eq 0 a H). + rewrite <- Zsgn_pos in H1; rewrite H1; romega with *. + subst a; simpl; auto. + generalize (ZOmod_lt a b H0); romega with *. +Qed. + +Theorem ZOmod_lt_neg : forall a b:Z, a<=0 -> b<>0 -> + -Zabs b < a mod b <= 0. +Proof. + intros. + assert (a mod b <= 0). + generalize (ZOmod_sgn a b). + destruct (Zle_lt_or_eq a 0 H). + rewrite <- Zsgn_neg in H1; rewrite H1; romega with *. + subst a; simpl; auto. + generalize (ZOmod_lt a b H0); romega with *. +Qed. + +Theorem ZOmod_lt_pos_pos : forall a b:Z, 0<=a -> 0<b -> 0 <= a mod b < b. +Proof. + intros; generalize (ZOmod_lt_pos a b); romega with *. +Qed. + +Theorem ZOmod_lt_pos_neg : forall a b:Z, 0<=a -> b<0 -> 0 <= a mod b < -b. +Proof. + intros; generalize (ZOmod_lt_pos a b); romega with *. +Qed. + +Theorem ZOmod_lt_neg_pos : forall a b:Z, a<=0 -> 0<b -> -b < a mod b <= 0. +Proof. + intros; generalize (ZOmod_lt_neg a b); romega with *. +Qed. + +Theorem ZOmod_lt_neg_neg : forall a b:Z, a<=0 -> b<0 -> b < a mod b <= 0. +Proof. + intros; generalize (ZOmod_lt_neg a b); romega with *. +Qed. + +(** * Division and Opposite *) + +(* The precise equalities that are invalid with "historic" Zdiv. *) + +Theorem ZOdiv_opp_l : forall a b:Z, (-a)/b = -(a/b). +Proof. + destruct a; destruct b; simpl; auto; + unfold ZOdiv, ZOdiv_eucl; destruct Pdiv_eucl; simpl; auto with zarith. +Qed. + +Theorem ZOdiv_opp_r : forall a b:Z, a/(-b) = -(a/b). +Proof. + destruct a; destruct b; simpl; auto; + unfold ZOdiv, ZOdiv_eucl; destruct Pdiv_eucl; simpl; auto with zarith. +Qed. + +Theorem ZOmod_opp_l : forall a b:Z, (-a) mod b = -(a mod b). +Proof. + destruct a; destruct b; simpl; auto; + unfold ZOmod, ZOdiv_eucl; destruct Pdiv_eucl; simpl; auto with zarith. +Qed. + +Theorem ZOmod_opp_r : forall a b:Z, a mod (-b) = a mod b. +Proof. + destruct a; destruct b; simpl; auto; + unfold ZOmod, ZOdiv_eucl; destruct Pdiv_eucl; simpl; auto with zarith. +Qed. + +Theorem ZOdiv_opp_opp : forall a b:Z, (-a)/(-b) = a/b. +Proof. + destruct a; destruct b; simpl; auto; + unfold ZOdiv, ZOdiv_eucl; destruct Pdiv_eucl; simpl; auto with zarith. +Qed. + +Theorem ZOmod_opp_opp : forall a b:Z, (-a) mod (-b) = -(a mod b). +Proof. + destruct a; destruct b; simpl; auto; + unfold ZOmod, ZOdiv_eucl; destruct Pdiv_eucl; simpl; auto with zarith. +Qed. + +(** * Unicity results *) + +Definition Remainder a b r := + (0 <= a /\ 0 <= r < Zabs b) \/ (a <= 0 /\ -Zabs b < r <= 0). + +Definition Remainder_alt a b r := + Zabs r < Zabs b /\ 0 <= r * a. + +Lemma Remainder_equiv : forall a b r, + Remainder a b r <-> Remainder_alt a b r. +Proof. + unfold Remainder, Remainder_alt; intuition. + romega with *. + romega with *. + rewrite <-(Zmult_opp_opp). + apply Zmult_le_0_compat; romega. + assert (0 <= Zsgn r * Zsgn a) by (rewrite <-Zsgn_Zmult, Zsgn_pos_iff; auto). + destruct r; simpl Zsgn in *; romega with *. +Qed. + +Theorem ZOdiv_mod_unique_full: + forall a b q r, Remainder a b r -> + a = b*q + r -> q = a/b /\ r = a mod b. +Proof. + destruct 1 as [(H,H0)|(H,H0)]; intros. + apply Zdiv.Zdiv_mod_unique with b; auto. + apply ZOmod_lt_pos; auto. + romega with *. + rewrite <- H1; apply ZO_div_mod_eq. + + rewrite <- (Zopp_involutive a). + rewrite ZOdiv_opp_l, ZOmod_opp_l. + generalize (Zdiv.Zdiv_mod_unique b (-q) (-a/b) (-r) (-a mod b)). + generalize (ZOmod_lt_pos (-a) b). + rewrite <-ZO_div_mod_eq, <-Zopp_mult_distr_r, <-Zopp_plus_distr, <-H1. + romega with *. +Qed. + +Theorem ZOdiv_unique_full: + forall a b q r, Remainder a b r -> + a = b*q + r -> q = a/b. +Proof. + intros; destruct (ZOdiv_mod_unique_full a b q r); auto. +Qed. + +Theorem ZOdiv_unique: + forall a b q r, 0 <= a -> 0 <= r < b -> + a = b*q + r -> q = a/b. +Proof. + intros; eapply ZOdiv_unique_full; eauto. + red; romega with *. +Qed. + +Theorem ZOmod_unique_full: + forall a b q r, Remainder a b r -> + a = b*q + r -> r = a mod b. +Proof. + intros; destruct (ZOdiv_mod_unique_full a b q r); auto. +Qed. + +Theorem ZOmod_unique: + forall a b q r, 0 <= a -> 0 <= r < b -> + a = b*q + r -> r = a mod b. +Proof. + intros; eapply ZOmod_unique_full; eauto. + red; romega with *. +Qed. + +(** * Basic values of divisions and modulo. *) + +Lemma ZOmod_0_l: forall a, 0 mod a = 0. +Proof. + destruct a; simpl; auto. +Qed. + +Lemma ZOmod_0_r: forall a, a mod 0 = a. +Proof. + destruct a; simpl; auto. +Qed. + +Lemma ZOdiv_0_l: forall a, 0/a = 0. +Proof. + destruct a; simpl; auto. +Qed. + +Lemma ZOdiv_0_r: forall a, a/0 = 0. +Proof. + destruct a; simpl; auto. +Qed. + +Lemma ZOmod_1_r: forall a, a mod 1 = 0. +Proof. + intros; symmetry; apply ZOmod_unique_full with a; auto with zarith. + rewrite Remainder_equiv; red; simpl; auto with zarith. +Qed. + +Lemma ZOdiv_1_r: forall a, a/1 = a. +Proof. + intros; symmetry; apply ZOdiv_unique_full with 0; auto with zarith. + rewrite Remainder_equiv; red; simpl; auto with zarith. +Qed. + +Hint Resolve ZOmod_0_l ZOmod_0_r ZOdiv_0_l ZOdiv_0_r ZOdiv_1_r ZOmod_1_r + : zarith. + +Lemma ZOdiv_1_l: forall a, 1 < a -> 1/a = 0. +Proof. + intros; symmetry; apply ZOdiv_unique with 1; auto with zarith. +Qed. + +Lemma ZOmod_1_l: forall a, 1 < a -> 1 mod a = 1. +Proof. + intros; symmetry; apply ZOmod_unique with 0; auto with zarith. +Qed. + +Lemma ZO_div_same : forall a:Z, a<>0 -> a/a = 1. +Proof. + intros; symmetry; apply ZOdiv_unique_full with 0; auto with *. + rewrite Remainder_equiv; red; simpl; romega with *. +Qed. + +Lemma ZO_mod_same : forall a, a mod a = 0. +Proof. + destruct a; intros; symmetry. + compute; auto. + apply ZOmod_unique with 1; auto with *; romega with *. + apply ZOmod_unique_full with 1; auto with *; red; romega with *. +Qed. + +Lemma ZO_mod_mult : forall a b, (a*b) mod b = 0. +Proof. + intros a b; destruct (Z_eq_dec b 0) as [Hb|Hb]. + subst; simpl; rewrite ZOmod_0_r; auto with zarith. + symmetry; apply ZOmod_unique_full with a; [ red; romega with * | ring ]. +Qed. + +Lemma ZO_div_mult : forall a b:Z, b <> 0 -> (a*b)/b = a. +Proof. + intros; symmetry; apply ZOdiv_unique_full with 0; auto with zarith; + [ red; romega with * | ring]. +Qed. + +(** * Order results about ZOmod and ZOdiv *) + +(* Division of positive numbers is positive. *) + +Lemma ZO_div_pos: forall a b, 0 <= a -> 0 <= b -> 0 <= a/b. +Proof. + intros. + destruct (Zle_lt_or_eq 0 b H0). + assert (H2:=ZOmod_lt_pos_pos a b H H1). + rewrite (ZO_div_mod_eq a b) in H. + destruct (Z_lt_le_dec (a/b) 0); auto. + assert (b*(a/b) <= -b). + replace (-b) with (b*-1); [ | ring]. + apply Zmult_le_compat_l; auto with zarith. + romega. + subst b; rewrite ZOdiv_0_r; auto. +Qed. + +(** As soon as the divisor is greater or equal than 2, + the division is strictly decreasing. *) + +Lemma ZO_div_lt : forall a b:Z, 0 < a -> 2 <= b -> a/b < a. +Proof. + intros. + assert (Hb : 0 < b) by romega. + assert (H1 : 0 <= a/b) by (apply ZO_div_pos; auto with zarith). + assert (H2 : 0 <= a mod b < b) by (apply ZOmod_lt_pos_pos; auto with zarith). + destruct (Zle_lt_or_eq 0 (a/b) H1) as [H3|H3]; [ | rewrite <- H3; auto]. + pattern a at 2; rewrite (ZO_div_mod_eq a b). + apply Zlt_le_trans with (2*(a/b)). + romega. + apply Zle_trans with (b*(a/b)). + apply Zmult_le_compat_r; auto. + romega. +Qed. + +(** A division of a small number by a bigger one yields zero. *) + +Theorem ZOdiv_small: forall a b, 0 <= a < b -> a/b = 0. +Proof. + intros a b H; apply sym_equal; apply ZOdiv_unique with a; auto with zarith. +Qed. + +(** Same situation, in term of modulo: *) + +Theorem ZOmod_small: forall a n, 0 <= a < n -> a mod n = a. +Proof. + intros a b H; apply sym_equal; apply ZOmod_unique with 0; auto with zarith. +Qed. + +(** [Zge] is compatible with a positive division. *) + +Lemma ZO_div_monotone_pos : forall a b c:Z, 0<=c -> 0<=a<=b -> a/c <= b/c. +Proof. + intros. + destruct H0. + destruct (Zle_lt_or_eq 0 c H); + [ clear H | subst c; do 2 rewrite ZOdiv_0_r; auto]. + generalize (ZO_div_mod_eq a c). + generalize (ZOmod_lt_pos_pos a c H0 H2). + generalize (ZO_div_mod_eq b c). + generalize (ZOmod_lt_pos_pos b c (Zle_trans _ _ _ H0 H1) H2). + intros. + elim (Z_le_gt_dec (a / c) (b / c)); auto with zarith. + intro. + absurd (a - b >= 1). + omega. + replace (a-b) with (c * (a/c-b/c) + a mod c - b mod c) by + (symmetry; pattern a at 1; rewrite H5; pattern b at 1; rewrite H3; ring). + assert (c * (a / c - b / c) >= c * 1). + apply Zmult_ge_compat_l. + omega. + omega. + assert (c * 1 = c). + ring. + omega. +Qed. + +Lemma ZO_div_monotone : forall a b c, 0<=c -> a<=b -> a/c <= b/c. +Proof. + intros. + destruct (Z_le_gt_dec 0 a). + apply ZO_div_monotone_pos; auto with zarith. + destruct (Z_le_gt_dec 0 b). + apply Zle_trans with 0. + apply Zle_left_rev. + simpl. + rewrite <- ZOdiv_opp_l. + apply ZO_div_pos; auto with zarith. + apply ZO_div_pos; auto with zarith. + rewrite <-(Zopp_involutive a), (ZOdiv_opp_l (-a)). + rewrite <-(Zopp_involutive b), (ZOdiv_opp_l (-b)). + generalize (ZO_div_monotone_pos (-b) (-a) c H). + romega. +Qed. + +(** With our choice of division, rounding of (a/b) is always done toward zero: *) + +Lemma ZO_mult_div_le : forall a b:Z, 0 <= a -> 0 <= b*(a/b) <= a. +Proof. + intros a b Ha. + destruct b as [ |b|b]. + simpl; auto with zarith. + split. + apply Zmult_le_0_compat; auto with zarith. + apply ZO_div_pos; auto with zarith. + generalize (ZO_div_mod_eq a (Zpos b)) (ZOmod_lt_pos_pos a (Zpos b) Ha); romega with *. + change (Zneg b) with (-Zpos b); rewrite ZOdiv_opp_r, Zmult_opp_opp. + split. + apply Zmult_le_0_compat; auto with zarith. + apply ZO_div_pos; auto with zarith. + generalize (ZO_div_mod_eq a (Zpos b)) (ZOmod_lt_pos_pos a (Zpos b) Ha); romega with *. +Qed. + +Lemma ZO_mult_div_ge : forall a b:Z, a <= 0 -> a <= b*(a/b) <= 0. +Proof. + intros a b Ha. + destruct b as [ |b|b]. + simpl; auto with zarith. + split. + generalize (ZO_div_mod_eq a (Zpos b)) (ZOmod_lt_neg_pos a (Zpos b) Ha); romega with *. + apply Zle_left_rev; unfold Zplus. + rewrite Zopp_mult_distr_r, <-ZOdiv_opp_l. + apply Zmult_le_0_compat; auto with zarith. + apply ZO_div_pos; auto with zarith. + change (Zneg b) with (-Zpos b); rewrite ZOdiv_opp_r, Zmult_opp_opp. + split. + generalize (ZO_div_mod_eq a (Zpos b)) (ZOmod_lt_neg_pos a (Zpos b) Ha); romega with *. + apply Zle_left_rev; unfold Zplus. + rewrite Zopp_mult_distr_r, <-ZOdiv_opp_l. + apply Zmult_le_0_compat; auto with zarith. + apply ZO_div_pos; auto with zarith. +Qed. + +(** The previous inequalities between [b*(a/b)] and [a] are exact + iff the modulo is zero. *) + +Lemma ZO_div_exact_full_1 : forall a b:Z, a = b*(a/b) -> a mod b = 0. +Proof. + intros; generalize (ZO_div_mod_eq a b); romega. +Qed. + +Lemma ZO_div_exact_full_2 : forall a b:Z, a mod b = 0 -> a = b*(a/b). +Proof. + intros; generalize (ZO_div_mod_eq a b); romega. +Qed. + +(** A modulo cannot grow beyond its starting point. *) + +Theorem ZOmod_le: forall a b, 0 <= a -> 0 <= b -> a mod b <= a. +Proof. + intros a b H1 H2. + destruct (Zle_lt_or_eq _ _ H2). + case (Zle_or_lt b a); intros H3. + case (ZOmod_lt_pos_pos a b); auto with zarith. + rewrite ZOmod_small; auto with zarith. + subst; rewrite ZOmod_0_r; auto with zarith. +Qed. + +(** Some additionnal inequalities about Zdiv. *) + +Theorem ZOdiv_le_upper_bound: + forall a b q, 0 <= a -> 0 < b -> a <= q*b -> a/b <= q. +Proof. + intros a b q H1 H2 H3. + apply Zmult_le_reg_r with b; auto with zarith. + apply Zle_trans with (2 := H3). + pattern a at 2; rewrite (ZO_div_mod_eq a b); auto with zarith. + rewrite (Zmult_comm b); case (ZOmod_lt_pos_pos a b); auto with zarith. +Qed. + +Theorem ZOdiv_lt_upper_bound: + forall a b q, 0 <= a -> 0 < b -> a < q*b -> a/b < q. +Proof. + intros a b q H1 H2 H3. + apply Zmult_lt_reg_r with b; auto with zarith. + apply Zle_lt_trans with (2 := H3). + pattern a at 2; rewrite (ZO_div_mod_eq a b); auto with zarith. + rewrite (Zmult_comm b); case (ZOmod_lt_pos_pos a b); auto with zarith. +Qed. + +Theorem ZOdiv_le_lower_bound: + forall a b q, 0 <= a -> 0 < b -> q*b <= a -> q <= a/b. +Proof. + intros a b q H1 H2 H3. + assert (q < a / b + 1); auto with zarith. + apply Zmult_lt_reg_r with b; auto with zarith. + apply Zle_lt_trans with (1 := H3). + pattern a at 1; rewrite (ZO_div_mod_eq a b); auto with zarith. + rewrite Zmult_plus_distr_l; rewrite (Zmult_comm b); case (ZOmod_lt_pos_pos a b); + auto with zarith. +Qed. + +Theorem ZOdiv_sgn: forall a b, + 0 <= Zsgn (a/b) * Zsgn a * Zsgn b. +Proof. + destruct a as [ |a|a]; destruct b as [ |b|b]; simpl; auto with zarith; + unfold ZOdiv; simpl; destruct Pdiv_eucl; simpl; destruct n; simpl; auto with zarith. +Qed. + +(** * Relations between usual operations and Zmod and Zdiv *) + +(** First, a result that used to be always valid with Zdiv, + but must be restricted here. + For instance, now (9+(-5)*2) mod 2 = -1 <> 1 = 9 mod 2 *) + +Lemma ZO_mod_plus : forall a b c:Z, + 0 <= (a+b*c) * a -> + (a + b * c) mod c = a mod c. +Proof. + intros; destruct (Z_eq_dec a 0) as [Ha|Ha]. + subst; simpl; rewrite ZOmod_0_l; apply ZO_mod_mult. + intros; destruct (Z_eq_dec c 0) as [Hc|Hc]. + subst; do 2 rewrite ZOmod_0_r; romega. + symmetry; apply ZOmod_unique_full with (a/c+b); auto with zarith. + rewrite Remainder_equiv; split. + apply ZOmod_lt; auto. + apply Zmult_le_0_reg_r with (a*a); eauto. + destruct a; simpl; auto with zarith. + replace ((a mod c)*(a+b*c)*(a*a)) with (((a mod c)*a)*((a+b*c)*a)) by ring. + apply Zmult_le_0_compat; auto. + apply ZOmod_sgn2. + rewrite Zmult_plus_distr_r, Zmult_comm. + generalize (ZO_div_mod_eq a c); romega. +Qed. + +Lemma ZO_div_plus : forall a b c:Z, + 0 <= (a+b*c) * a -> c<>0 -> + (a + b * c) / c = a / c + b. +Proof. + intros; destruct (Z_eq_dec a 0) as [Ha|Ha]. + subst; simpl; apply ZO_div_mult; auto. + symmetry. + apply ZOdiv_unique_full with (a mod c); auto with zarith. + rewrite Remainder_equiv; split. + apply ZOmod_lt; auto. + apply Zmult_le_0_reg_r with (a*a); eauto. + destruct a; simpl; auto with zarith. + replace ((a mod c)*(a+b*c)*(a*a)) with (((a mod c)*a)*((a+b*c)*a)) by ring. + apply Zmult_le_0_compat; auto. + apply ZOmod_sgn2. + rewrite Zmult_plus_distr_r, Zmult_comm. + generalize (ZO_div_mod_eq a c); romega. +Qed. + +Theorem ZO_div_plus_l: forall a b c : Z, + 0 <= (a*b+c)*c -> b<>0 -> + b<>0 -> (a * b + c) / b = a + c / b. +Proof. + intros a b c; rewrite Zplus_comm; intros; rewrite ZO_div_plus; + try apply Zplus_comm; auto with zarith. +Qed. + +(** Cancellations. *) + +Lemma ZOdiv_mult_cancel_r : forall a b c:Z, + c<>0 -> (a*c)/(b*c) = a/b. +Proof. + intros a b c Hc. + destruct (Z_eq_dec b 0). + subst; simpl; do 2 rewrite ZOdiv_0_r; auto. + symmetry. + apply ZOdiv_unique_full with ((a mod b)*c); auto with zarith. + rewrite Remainder_equiv. + split. + do 2 rewrite Zabs_Zmult. + apply Zmult_lt_compat_r. + romega with *. + apply ZOmod_lt; auto. + replace ((a mod b)*c*(a*c)) with (((a mod b)*a)*(c*c)) by ring. + apply Zmult_le_0_compat. + apply ZOmod_sgn2. + destruct c; simpl; auto with zarith. + pattern a at 1; rewrite (ZO_div_mod_eq a b); ring. +Qed. + +Lemma ZOdiv_mult_cancel_l : forall a b c:Z, + c<>0 -> (c*a)/(c*b) = a/b. +Proof. + intros. + rewrite (Zmult_comm c a); rewrite (Zmult_comm c b). + apply ZOdiv_mult_cancel_r; auto. +Qed. + +Lemma ZOmult_mod_distr_l: forall a b c, + (c*a) mod (c*b) = c * (a mod b). +Proof. + intros; destruct (Z_eq_dec c 0) as [Hc|Hc]. + subst; simpl; rewrite ZOmod_0_r; auto. + destruct (Z_eq_dec b 0) as [Hb|Hb]. + subst; repeat rewrite Zmult_0_r || rewrite ZOmod_0_r; auto. + assert (c*b <> 0). + contradict Hc; eapply Zmult_integral_l; eauto. + rewrite (Zplus_minus_eq _ _ _ (ZO_div_mod_eq (c*a) (c*b))). + rewrite (Zplus_minus_eq _ _ _ (ZO_div_mod_eq a b)). + rewrite ZOdiv_mult_cancel_l; auto with zarith. + ring. +Qed. + +Lemma ZOmult_mod_distr_r: forall a b c, + (a*c) mod (b*c) = (a mod b) * c. +Proof. + intros; repeat rewrite (fun x => (Zmult_comm x c)). + apply ZOmult_mod_distr_l; auto. +Qed. + +(** Operations modulo. *) + +Theorem ZOmod_mod: forall a n, (a mod n) mod n = a mod n. +Proof. + intros. + generalize (ZOmod_sgn2 a n). + pattern a at 2 4; rewrite (ZO_div_mod_eq a n); auto with zarith. + rewrite Zplus_comm; rewrite (Zmult_comm n). + intros. + apply sym_equal; apply ZO_mod_plus; auto with zarith. + rewrite Zmult_comm; auto. +Qed. + +Theorem ZOmult_mod: forall a b n, + (a * b) mod n = ((a mod n) * (b mod n)) mod n. +Proof. + intros. + generalize (Zmult_le_0_compat _ _ (ZOmod_sgn2 a n) (ZOmod_sgn2 b n)). + pattern a at 2 3; rewrite (ZO_div_mod_eq a n); auto with zarith. + pattern b at 2 3; rewrite (ZO_div_mod_eq b n); auto with zarith. + set (A:=a mod n); set (B:=b mod n); set (A':=a/n); set (B':=b/n). + replace (A*(n*A'+A)*(B*(n*B'+B))) with (((n*A' + A) * (n*B' + B))*(A*B)) + by ring. + replace ((n*A' + A) * (n*B' + B)) + with (A*B + (A'*B+B'*A+n*A'*B')*n) by ring. + intros. + apply ZO_mod_plus; auto with zarith. +Qed. + +(** addition and modulo + + Generally speaking, unlike with Zdiv, we don't have + (a+b) mod n = (a mod n + b mod n) mod n + for any a and b. + For instance, take (8 + (-10)) mod 3 = -2 whereas + (8 mod 3 + (-10 mod 3)) mod 3 = 1. *) + +Theorem ZOplus_mod: forall a b n, + 0 <= a * b -> + (a + b) mod n = (a mod n + b mod n) mod n. +Proof. + assert (forall a b n, 0<a -> 0<b -> + (a + b) mod n = (a mod n + b mod n) mod n). + intros a b n Ha Hb. + assert (H : 0<=a+b) by (romega with * ); revert H. + pattern a at 1 2; rewrite (ZO_div_mod_eq a n); auto with zarith. + pattern b at 1 2; rewrite (ZO_div_mod_eq b n); auto with zarith. + replace ((n * (a / n) + a mod n) + (n * (b / n) + b mod n)) + with ((a mod n + b mod n) + (a / n + b / n) * n) by ring. + intros. + apply ZO_mod_plus; auto with zarith. + apply Zmult_le_0_compat; auto with zarith. + apply Zplus_le_0_compat. + apply Zmult_le_reg_r with a; auto with zarith. + simpl; apply ZOmod_sgn2; auto. + apply Zmult_le_reg_r with b; auto with zarith. + simpl; apply ZOmod_sgn2; auto. + (* general situation *) + intros a b n Hab. + destruct (Z_eq_dec a 0). + subst; simpl; symmetry; apply ZOmod_mod. + destruct (Z_eq_dec b 0). + subst; simpl; do 2 rewrite Zplus_0_r; symmetry; apply ZOmod_mod. + assert (0<a /\ 0<b \/ a<0 /\ b<0). + destruct a; destruct b; simpl in *; intuition; romega with *. + destruct H0. + apply H; intuition. + rewrite <-(Zopp_involutive a), <-(Zopp_involutive b). + rewrite <- Zopp_plus_distr; rewrite ZOmod_opp_l. + rewrite (ZOmod_opp_l (-a)),(ZOmod_opp_l (-b)). + match goal with |- _ = (-?x+-?y) mod n => + rewrite <-(Zopp_plus_distr x y), ZOmod_opp_l end. + f_equal; apply H; auto with zarith. +Qed. + +Lemma ZOplus_mod_idemp_l: forall a b n, + 0 <= a * b -> + (a mod n + b) mod n = (a + b) mod n. +Proof. + intros. + rewrite ZOplus_mod. + rewrite ZOmod_mod. + symmetry. + apply ZOplus_mod; auto. + destruct (Z_eq_dec a 0). + subst; rewrite ZOmod_0_l; auto. + destruct (Z_eq_dec b 0). + subst; rewrite Zmult_0_r; auto with zarith. + apply Zmult_le_reg_r with (a*b). + assert (a*b <> 0). + intro Hab. + rewrite (Zmult_integral_l _ _ n1 Hab) in n0; auto with zarith. + auto with zarith. + simpl. + replace (a mod n * b * (a*b)) with ((a mod n * a)*(b*b)) by ring. + apply Zmult_le_0_compat. + apply ZOmod_sgn2. + destruct b; simpl; auto with zarith. +Qed. + +Lemma ZOplus_mod_idemp_r: forall a b n, + 0 <= a*b -> + (b + a mod n) mod n = (b + a) mod n. +Proof. + intros. + rewrite Zplus_comm, (Zplus_comm b a). + apply ZOplus_mod_idemp_l; auto. +Qed. + +Lemma ZOmult_mod_idemp_l: forall a b n, (a mod n * b) mod n = (a * b) mod n. +Proof. + intros; rewrite ZOmult_mod, ZOmod_mod, <- ZOmult_mod; auto. +Qed. + +Lemma ZOmult_mod_idemp_r: forall a b n, (b * (a mod n)) mod n = (b * a) mod n. +Proof. + intros; rewrite ZOmult_mod, ZOmod_mod, <- ZOmult_mod; auto. +Qed. + +(** Unlike with Zdiv, the following result is true without restrictions. *) + +Lemma ZOdiv_ZOdiv : forall a b c, (a/b)/c = a/(b*c). +Proof. + (* particular case: a, b, c positive *) + assert (forall a b c, a>0 -> b>0 -> c>0 -> (a/b)/c = a/(b*c)). + intros a b c H H0 H1. + pattern a at 2;rewrite (ZO_div_mod_eq a b). + pattern (a/b) at 2;rewrite (ZO_div_mod_eq (a/b) c). + replace (b * (c * (a / b / c) + (a / b) mod c) + a mod b) with + ((a / b / c)*(b * c) + (b * ((a / b) mod c) + a mod b)) by ring. + assert (b*c<>0). + intro H2; + assert (H3: c <> 0) by auto with zarith; + rewrite (Zmult_integral_l _ _ H3 H2) in H0; auto with zarith. + assert (0<=a/b) by (apply (ZO_div_pos a b); auto with zarith). + assert (0<=a mod b < b) by (apply ZOmod_lt_pos_pos; auto with zarith). + assert (0<=(a/b) mod c < c) by + (apply ZOmod_lt_pos_pos; auto with zarith). + rewrite ZO_div_plus_l; auto with zarith. + rewrite (ZOdiv_small (b * ((a / b) mod c) + a mod b)). + ring. + split. + apply Zplus_le_0_compat;auto with zarith. + apply Zle_lt_trans with (b * ((a / b) mod c) + (b-1)). + apply Zplus_le_compat;auto with zarith. + apply Zle_lt_trans with (b * (c-1) + (b - 1)). + apply Zplus_le_compat;auto with zarith. + replace (b * (c - 1) + (b - 1)) with (b*c-1);try ring;auto with zarith. + repeat (apply Zmult_le_0_compat || apply Zplus_le_0_compat); auto with zarith. + apply (ZO_div_pos (a/b) c); auto with zarith. + (* b c positive, a general *) + assert (forall a b c, b>0 -> c>0 -> (a/b)/c = a/(b*c)). + intros; destruct a as [ |a|a]; try reflexivity. + apply H; auto with zarith. + change (Zneg a) with (-Zpos a); repeat rewrite ZOdiv_opp_l. + f_equal; apply H; auto with zarith. + (* c positive, a b general *) + assert (forall a b c, c>0 -> (a/b)/c = a/(b*c)). + intros; destruct b as [ |b|b]. + repeat rewrite ZOdiv_0_r; reflexivity. + apply H0; auto with zarith. + change (Zneg b) with (-Zpos b); + repeat (rewrite ZOdiv_opp_r || rewrite ZOdiv_opp_l || rewrite <- Zopp_mult_distr_l). + f_equal; apply H0; auto with zarith. + (* a b c general *) + intros; destruct c as [ |c|c]. + rewrite Zmult_0_r; repeat rewrite ZOdiv_0_r; reflexivity. + apply H1; auto with zarith. + change (Zneg c) with (-Zpos c); + rewrite <- Zopp_mult_distr_r; do 2 rewrite ZOdiv_opp_r. + f_equal; apply H1; auto with zarith. +Qed. + +(** A last inequality: *) + +Theorem ZOdiv_mult_le: + forall a b c, 0<=a -> 0<=b -> 0<=c -> c*(a/b) <= (c*a)/b. +Proof. + intros a b c Ha Hb Hc. + destruct (Zle_lt_or_eq _ _ Ha); + [ | subst; rewrite ZOdiv_0_l, Zmult_0_r, ZOdiv_0_l; auto]. + destruct (Zle_lt_or_eq _ _ Hb); + [ | subst; rewrite ZOdiv_0_r, ZOdiv_0_r, Zmult_0_r; auto]. + destruct (Zle_lt_or_eq _ _ Hc); + [ | subst; rewrite ZOdiv_0_l; auto]. + case (ZOmod_lt_pos_pos a b); auto with zarith; intros Hu1 Hu2. + case (ZOmod_lt_pos_pos c b); auto with zarith; intros Hv1 Hv2. + apply Zmult_le_reg_r with b; auto with zarith. + rewrite <- Zmult_assoc. + replace (a / b * b) with (a - a mod b). + replace (c * a / b * b) with (c * a - (c * a) mod b). + rewrite Zmult_minus_distr_l. + unfold Zminus; apply Zplus_le_compat_l. + match goal with |- - ?X <= -?Y => assert (Y <= X); auto with zarith end. + apply Zle_trans with ((c mod b) * (a mod b)); auto with zarith. + rewrite ZOmult_mod; auto with zarith. + apply (ZOmod_le ((c mod b) * (a mod b)) b); auto with zarith. + apply Zmult_le_compat_r; auto with zarith. + apply (ZOmod_le c b); auto. + pattern (c * a) at 1; rewrite (ZO_div_mod_eq (c * a) b); try ring; + auto with zarith. + pattern a at 1; rewrite (ZO_div_mod_eq a b); try ring; auto with zarith. +Qed. + +(** ZOmod is related to divisibility (see more in Znumtheory) *) + +Lemma ZOmod_divides : forall a b, + a mod b = 0 <-> exists c, a = b*c. +Proof. + split; intros. + exists (a/b). + pattern a at 1; rewrite (ZO_div_mod_eq a b). + rewrite H; auto with zarith. + destruct H as [c Hc]. + destruct (Z_eq_dec b 0). + subst b; simpl in *; subst a; auto. + symmetry. + apply ZOmod_unique_full with c; auto with zarith. + red; romega with *. +Qed. + +(** * Interaction with "historic" Zdiv *) + +(** They agree at least on positive numbers: *) + +Theorem ZOdiv_eucl_Zdiv_eucl_pos : forall a b:Z, 0 <= a -> 0 < b -> + a/b = Zdiv.Zdiv a b /\ a mod b = Zdiv.Zmod a b. +Proof. + intros. + apply Zdiv.Zdiv_mod_unique with b. + apply ZOmod_lt_pos; auto with zarith. + rewrite Zabs_eq; auto with *; apply Zdiv.Z_mod_lt; auto with *. + rewrite <- Zdiv.Z_div_mod_eq; auto with *. + symmetry; apply ZO_div_mod_eq; auto with *. +Qed. + +Theorem ZOdiv_Zdiv_pos : forall a b, 0 <= a -> 0 <= b -> + a/b = Zdiv.Zdiv a b. +Proof. + intros a b Ha Hb. + destruct (Zle_lt_or_eq _ _ Hb). + generalize (ZOdiv_eucl_Zdiv_eucl_pos a b Ha H); intuition. + subst; rewrite ZOdiv_0_r, Zdiv.Zdiv_0_r; reflexivity. +Qed. + +Theorem ZOmod_Zmod_pos : forall a b, 0 <= a -> 0 < b -> + a mod b = Zdiv.Zmod a b. +Proof. + intros a b Ha Hb; generalize (ZOdiv_eucl_Zdiv_eucl_pos a b Ha Hb); + intuition. +Qed. + +(** Modulos are null at the same places *) + +Theorem ZOmod_Zmod_zero : forall a b, b<>0 -> + (a mod b = 0 <-> Zdiv.Zmod a b = 0). +Proof. + intros. + rewrite ZOmod_divides, Zdiv.Zmod_divides; intuition. +Qed. diff --git a/theories/ZArith/ZOdiv_def.v b/theories/ZArith/ZOdiv_def.v new file mode 100644 index 00000000..2c84765e --- /dev/null +++ b/theories/ZArith/ZOdiv_def.v @@ -0,0 +1,136 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + + +Require Import BinPos BinNat Nnat ZArith_base. + +Open Scope Z_scope. + +Definition NPgeb (a:N)(b:positive) := + match a with + | N0 => false + | Npos na => match Pcompare na b Eq with Lt => false | _ => true end + end. + +Fixpoint Pdiv_eucl (a b:positive) {struct a} : N * N := + match a with + | xH => + match b with xH => (1, 0)%N | _ => (0, 1)%N end + | xO a' => + let (q, r) := Pdiv_eucl a' b in + let r' := (2 * r)%N in + if (NPgeb r' b) then (2 * q + 1, (Nminus r' (Npos b)))%N + else (2 * q, r')%N + | xI a' => + let (q, r) := Pdiv_eucl a' b in + let r' := (2 * r + 1)%N in + if (NPgeb r' b) then (2 * q + 1, (Nminus r' (Npos b)))%N + else (2 * q, r')%N + end. + +Definition ZOdiv_eucl (a b:Z) : Z * Z := + match a, b with + | Z0, _ => (Z0, Z0) + | _, Z0 => (Z0, a) + | Zpos na, Zpos nb => + let (nq, nr) := Pdiv_eucl na nb in + (Z_of_N nq, Z_of_N nr) + | Zneg na, Zpos nb => + let (nq, nr) := Pdiv_eucl na nb in + (Zopp (Z_of_N nq), Zopp (Z_of_N nr)) + | Zpos na, Zneg nb => + let (nq, nr) := Pdiv_eucl na nb in + (Zopp (Z_of_N nq), Z_of_N nr) + | Zneg na, Zneg nb => + let (nq, nr) := Pdiv_eucl na nb in + (Z_of_N nq, Zopp (Z_of_N nr)) + end. + +Definition ZOdiv a b := fst (ZOdiv_eucl a b). +Definition ZOmod a b := snd (ZOdiv_eucl a b). + + +Definition Ndiv_eucl (a b:N) : N * N := + match a, b with + | N0, _ => (N0, N0) + | _, N0 => (N0, a) + | Npos na, Npos nb => Pdiv_eucl na nb + end. + +Definition Ndiv a b := fst (Ndiv_eucl a b). +Definition Nmod a b := snd (Ndiv_eucl a b). + + +(* Proofs of specifications for these euclidean divisions. *) + +Theorem NPgeb_correct: forall (a:N)(b:positive), + if NPgeb a b then a = (Nminus a (Npos b) + Npos b)%N else True. +Proof. + destruct a; intros; simpl; auto. + generalize (Pcompare_Eq_eq p b). + case_eq (Pcompare p b Eq); intros; auto. + rewrite H0; auto. + now rewrite Pminus_mask_diag. + destruct (Pminus_mask_Gt p b H) as [d [H2 [H3 _]]]. + rewrite H2. rewrite <- H3. + simpl; f_equal; apply Pplus_comm. +Qed. + +Hint Rewrite Z_of_N_plus Z_of_N_mult Z_of_N_minus Zmult_1_l Zmult_assoc + Zmult_plus_distr_l Zmult_plus_distr_r : zdiv. +Hint Rewrite <- Zplus_assoc : zdiv. + +Theorem Pdiv_eucl_correct: forall a b, + let (q,r) := Pdiv_eucl a b in + Zpos a = Z_of_N q * Zpos b + Z_of_N r. +Proof. + induction a; cbv beta iota delta [Pdiv_eucl]; fold Pdiv_eucl; cbv zeta. + intros b; generalize (IHa b); case Pdiv_eucl. + intros q1 r1 Hq1. + generalize (NPgeb_correct (2 * r1 + 1) b); case NPgeb; intros H. + set (u := Nminus (2 * r1 + 1) (Npos b)) in * |- *. + assert (HH: Z_of_N u = (Z_of_N (2 * r1 + 1) - Zpos b)%Z). + rewrite H; autorewrite with zdiv; simpl. + rewrite Zplus_comm, Zminus_plus; trivial. + rewrite HH; autorewrite with zdiv; simpl Z_of_N. + rewrite Zpos_xI, Hq1. + autorewrite with zdiv; f_equal; rewrite Zplus_minus; trivial. + rewrite Zpos_xI, Hq1; autorewrite with zdiv; auto. + intros b; generalize (IHa b); case Pdiv_eucl. + intros q1 r1 Hq1. + generalize (NPgeb_correct (2 * r1) b); case NPgeb; intros H. + set (u := Nminus (2 * r1) (Npos b)) in * |- *. + assert (HH: Z_of_N u = (Z_of_N (2 * r1) - Zpos b)%Z). + rewrite H; autorewrite with zdiv; simpl. + rewrite Zplus_comm, Zminus_plus; trivial. + rewrite HH; autorewrite with zdiv; simpl Z_of_N. + rewrite Zpos_xO, Hq1. + autorewrite with zdiv; f_equal; rewrite Zplus_minus; trivial. + rewrite Zpos_xO, Hq1; autorewrite with zdiv; auto. + destruct b; auto. +Qed. + +Theorem ZOdiv_eucl_correct: forall a b, + let (q,r) := ZOdiv_eucl a b in a = q * b + r. +Proof. + destruct a; destruct b; simpl; auto; + generalize (Pdiv_eucl_correct p p0); case Pdiv_eucl; auto; intros; + try change (Zneg p) with (Zopp (Zpos p)); rewrite H. + destruct n; auto. + repeat (rewrite Zopp_plus_distr || rewrite Zopp_mult_distr_l); trivial. + repeat (rewrite Zopp_plus_distr || rewrite Zopp_mult_distr_r); trivial. +Qed. + +Theorem Ndiv_eucl_correct: forall a b, + let (q,r) := Ndiv_eucl a b in a = (q * b + r)%N. +Proof. + destruct a; destruct b; simpl; auto; + generalize (Pdiv_eucl_correct p p0); case Pdiv_eucl; auto; intros; + destruct n; destruct n0; simpl; simpl in H; try discriminate; + injection H; intros; subst; trivial. +Qed. diff --git a/theories/ZArith/Zabs.v b/theories/ZArith/Zabs.v index ed641358..c15493e3 100644 --- a/theories/ZArith/Zabs.v +++ b/theories/ZArith/Zabs.v @@ -5,14 +5,16 @@ (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: Zabs.v 9302 2006-10-27 21:21:17Z barras $ i*) +(*i $Id: Zabs.v 10302 2007-11-08 09:54:31Z letouzey $ i*) -(** Binary Integers (Pierre Crégut (CNET, Lannion, France) *) +(** Binary Integers (Pierre Crégut (CNET, Lannion, France) *) Require Import Arith_base. Require Import BinPos. Require Import BinInt. Require Import Zorder. +Require Import Zmax. +Require Import Znat. Require Import ZArith_dec. Open Local Scope Z_scope. @@ -63,6 +65,11 @@ Lemma Zabs_pos : forall n:Z, 0 <= Zabs n. intro x; destruct x; auto with arith; compute in |- *; intros H; inversion H. Qed. +Lemma Zabs_involutive : forall x:Z, Zabs (Zabs x) = Zabs x. +Proof. + intros; apply Zabs_eq; apply Zabs_pos. +Qed. + Theorem Zabs_eq_case : forall n m:Z, Zabs n = Zabs m -> n = m \/ n = - m. Proof. intros z1 z2; case z1; case z2; simpl in |- *; auto; @@ -70,6 +77,13 @@ Proof. (intros H2; rewrite H2); auto. Qed. +Lemma Zabs_spec : forall x:Z, + 0 <= x /\ Zabs x = x \/ + 0 > x /\ Zabs x = -x. +Proof. + intros; unfold Zabs, Zle, Zgt; destruct x; simpl; intuition discriminate. +Qed. + (** * Triangular inequality *) Hint Local Resolve Zle_neg_pos: zarith. @@ -106,25 +120,106 @@ Proof. intros z1 z2; case z1; case z2; simpl in |- *; auto. Qed. -(** * Absolute value in nat is compatible with order *) +Theorem Zabs_square : forall a, Zabs a * Zabs a = a * a. +Proof. + destruct a; simpl; auto. +Qed. + +(** * Results about absolute value in nat. *) + +Theorem inj_Zabs_nat : forall z:Z, Z_of_nat (Zabs_nat z) = Zabs z. +Proof. + destruct z; simpl; auto; symmetry; apply Zpos_eq_Z_of_nat_o_nat_of_P. +Qed. + +Theorem Zabs_nat_Z_of_nat: forall n, Zabs_nat (Z_of_nat n) = n. +Proof. + destruct n; simpl; auto. + apply nat_of_P_o_P_of_succ_nat_eq_succ. +Qed. + +Lemma Zabs_nat_mult: forall n m:Z, Zabs_nat (n*m) = (Zabs_nat n * Zabs_nat m)%nat. +Proof. + intros; apply inj_eq_rev. + rewrite inj_mult; repeat rewrite inj_Zabs_nat; apply Zabs_Zmult. +Qed. + +Lemma Zabs_nat_Zsucc: + forall p, 0 <= p -> Zabs_nat (Zsucc p) = S (Zabs_nat p). +Proof. + intros; apply inj_eq_rev. + rewrite inj_S; repeat rewrite inj_Zabs_nat, Zabs_eq; auto with zarith. +Qed. + +Lemma Zabs_nat_Zplus: + forall x y, 0<=x -> 0<=y -> Zabs_nat (x+y) = (Zabs_nat x + Zabs_nat y)%nat. +Proof. + intros; apply inj_eq_rev. + rewrite inj_plus; repeat rewrite inj_Zabs_nat, Zabs_eq; auto with zarith. + apply Zplus_le_0_compat; auto. +Qed. + +Lemma Zabs_nat_Zminus: + forall x y, 0 <= x <= y -> Zabs_nat (y - x) = (Zabs_nat y - Zabs_nat x)%nat. +Proof. + intros x y (H,H'). + assert (0 <= y) by (apply Zle_trans with x; auto). + assert (0 <= y-x) by (apply Zle_minus_le_0; auto). + apply inj_eq_rev. + rewrite inj_minus; repeat rewrite inj_Zabs_nat, Zabs_eq; auto. + rewrite Zmax_right; auto. +Qed. + +Lemma Zabs_nat_le : + forall n m:Z, 0 <= n <= m -> (Zabs_nat n <= Zabs_nat m)%nat. +Proof. + intros n m (H,H'); apply inj_le_rev. + repeat rewrite inj_Zabs_nat, Zabs_eq; auto. + apply Zle_trans with n; auto. +Qed. Lemma Zabs_nat_lt : - forall n m:Z, 0 <= n /\ n < m -> (Zabs_nat n < Zabs_nat m)%nat. + forall n m:Z, 0 <= n < m -> (Zabs_nat n < Zabs_nat m)%nat. +Proof. + intros n m (H,H'); apply inj_lt_rev. + repeat rewrite inj_Zabs_nat, Zabs_eq; auto. + apply Zlt_le_weak; apply Zle_lt_trans with n; auto. +Qed. + +(** * Some results about the sign function. *) + +Lemma Zsgn_Zmult : forall a b, Zsgn (a*b) = Zsgn a * Zsgn b. +Proof. + destruct a; destruct b; simpl; auto. +Qed. + +Lemma Zsgn_Zopp : forall a, Zsgn (-a) = - Zsgn a. Proof. - intros x y. case x; simpl in |- *. case y; simpl in |- *. + destruct a; simpl; auto. +Qed. - intro. absurd (0 < 0). compute in |- *. intro H0. discriminate H0. intuition. - intros. elim (ZL4 p). intros. rewrite H0. auto with arith. - intros. elim (ZL4 p). intros. rewrite H0. auto with arith. - - case y; simpl in |- *. - intros. absurd (Zpos p < 0). compute in |- *. intro H0. discriminate H0. intuition. - intros. change (nat_of_P p > nat_of_P p0)%nat in |- *. - apply nat_of_P_gt_Gt_compare_morphism. - elim H; auto with arith. intro. exact (ZC2 p0 p). +(** A characterization of the sign function: *) - intros. absurd (Zpos p0 < Zneg p). - compute in |- *. intro H0. discriminate H0. intuition. +Lemma Zsgn_spec : forall x:Z, + 0 < x /\ Zsgn x = 1 \/ + 0 = x /\ Zsgn x = 0 \/ + 0 > x /\ Zsgn x = -1. +Proof. + intros; unfold Zsgn, Zle, Zgt; destruct x; compute; intuition. +Qed. - intros. absurd (0 <= Zneg p). compute in |- *. auto with arith. intuition. +Lemma Zsgn_pos : forall x:Z, Zsgn x = 1 <-> 0 < x. +Proof. + destruct x; now intuition. Qed. + +Lemma Zsgn_neg : forall x:Z, Zsgn x = -1 <-> x < 0. +Proof. + destruct x; now intuition. +Qed. + +Lemma Zsgn_null : forall x:Z, Zsgn x = 0 <-> x = 0. +Proof. + destruct x; now intuition. +Qed. + diff --git a/theories/ZArith/Zbool.v b/theories/ZArith/Zbool.v index 7da91c44..34114d46 100644 --- a/theories/ZArith/Zbool.v +++ b/theories/ZArith/Zbool.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: Zbool.v 9245 2006-10-17 12:53:34Z notin $ *) +(* $Id: Zbool.v 10063 2007-08-08 14:21:03Z emakarov $ *) Require Import BinInt. Require Import Zeven. @@ -104,7 +104,7 @@ Qed. Lemma Zle_bool_imp_le : forall n m:Z, Zle_bool n m = true -> (n <= m)%Z. Proof. - unfold Zle_bool, Zle in |- *. intros x y. unfold not in |- *. + unfold Zle_bool, Zle in |- *. intros x y. unfold not in |- *. case (x ?= y)%Z; intros; discriminate. Qed. @@ -178,6 +178,18 @@ Proof. intro. apply Zle_ge. apply Zle_bool_imp_le. assumption. Qed. +Lemma Zlt_is_lt_bool : forall n m:Z, (n < m)%Z <-> Zlt_bool n m = true. +Proof. +intros n m; unfold Zlt_bool, Zlt. +destruct (n ?= m)%Z; simpl; split; now intro. +Qed. + +Lemma Zgt_is_gt_bool : forall n m:Z, (n > m)%Z <-> Zgt_bool n m = true. +Proof. +intros n m; unfold Zgt_bool, Zgt. +destruct (n ?= m)%Z; simpl; split; now intro. +Qed. + Lemma Zlt_is_le_bool : forall n m:Z, (n < m)%Z <-> Zle_bool n (m - 1) = true. Proof. diff --git a/theories/ZArith/Zcomplements.v b/theories/ZArith/Zcomplements.v index 78c8a976..c6ade934 100644 --- a/theories/ZArith/Zcomplements.v +++ b/theories/ZArith/Zcomplements.v @@ -6,11 +6,11 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: Zcomplements.v 9245 2006-10-17 12:53:34Z notin $ i*) +(*i $Id: Zcomplements.v 10617 2008-03-04 18:07:16Z letouzey $ i*) Require Import ZArithRing. Require Import ZArith_base. -Require Import Omega. +Require Export Omega. Require Import Wf_nat. Open Local Scope Z_scope. @@ -160,7 +160,7 @@ Qed. Require Import List. -Fixpoint Zlength_aux (acc:Z) (A:Set) (l:list A) {struct l} : Z := +Fixpoint Zlength_aux (acc:Z) (A:Type) (l:list A) {struct l} : Z := match l with | nil => acc | _ :: l => Zlength_aux (Zsucc acc) A l @@ -171,7 +171,7 @@ Implicit Arguments Zlength [A]. Section Zlength_properties. - Variable A : Set. + Variable A : Type. Implicit Type l : list A. diff --git a/theories/ZArith/Zdiv.v b/theories/ZArith/Zdiv.v index 31f68207..4c560c6b 100644 --- a/theories/ZArith/Zdiv.v +++ b/theories/ZArith/Zdiv.v @@ -6,9 +6,9 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: Zdiv.v 9245 2006-10-17 12:53:34Z notin $ i*) +(*i $Id: Zdiv.v 10999 2008-05-27 15:55:22Z letouzey $ i*) -(* Contribution by Claude Marché and Xavier Urbain *) +(* Contribution by Claude Marché and Xavier Urbain *) (** Euclidean Division @@ -21,6 +21,7 @@ Require Import Zbool. Require Import Omega. Require Import ZArithRing. Require Import Zcomplements. +Require Export Setoid. Open Local Scope Z_scope. (** * Definitions of Euclidian operations *) @@ -70,8 +71,21 @@ Unboxed Fixpoint Zdiv_eucl_POS (a:positive) (b:Z) {struct a} : if r = 0 then (-q,0) else (-(q+1),b+r) In other word, when b is non-zero, q is chosen to be the greatest integer - smaller or equal to a/b. And sgn(r)=sgn(b) and |r| < |b|. + smaller or equal to a/b. And sgn(r)=sgn(b) and |r| < |b| (at least when + r is not null). +*) + +(* Nota: At least two others conventions also exist for euclidean division. + They all satify the equation a=b*q+r, but differ on the choice of (q,r) + on negative numbers. + + * Ocaml uses Round-Toward-Zero division: (-a)/b = a/(-b) = -(a/b). + Hence (-a) mod b = - (a mod b) + a mod (-b) = a mod b + And: |r| < |b| and sgn(r) = sgn(a) (notice the a here instead of b). + * Another solution is to always pick a non-negative remainder: + a=b*q+r with 0 <= r < |b| *) Definition Zdiv_eucl (a b:Z) : Z * Z := @@ -96,7 +110,7 @@ Definition Zdiv_eucl (a b:Z) : Z * Z := (** Division and modulo are projections of [Zdiv_eucl] *) - + Definition Zdiv (a b:Z) : Z := let (q, _) := Zdiv_eucl a b in q. Definition Zmod (a b:Z) : Z := let (_, r) := Zdiv_eucl a b in r. @@ -108,20 +122,20 @@ Infix "mod" := Zmod (at level 40, no associativity) : Z_scope. (* Tests: -Eval Compute in `(Zdiv_eucl 7 3)`. +Eval compute in (Zdiv_eucl 7 3). -Eval Compute in `(Zdiv_eucl (-7) 3)`. +Eval compute in (Zdiv_eucl (-7) 3). -Eval Compute in `(Zdiv_eucl 7 (-3))`. +Eval compute in (Zdiv_eucl 7 (-3)). -Eval Compute in `(Zdiv_eucl (-7) (-3))`. +Eval compute in (Zdiv_eucl (-7) (-3)). *) (** * Main division theorem *) -(** First a lemma for positive *) +(** First a lemma for two positive arguments *) Lemma Z_div_mod_POS : forall b:Z, @@ -129,7 +143,8 @@ Lemma Z_div_mod_POS : forall a:positive, let (q, r) := Zdiv_eucl_POS a b in Zpos a = b * q + r /\ 0 <= r < b. Proof. -simple induction a; unfold Zdiv_eucl_POS in |- *; fold Zdiv_eucl_POS in |- *. +simple induction a; cbv beta iota delta [Zdiv_eucl_POS] in |- *; + fold Zdiv_eucl_POS in |- *; cbv zeta. intro p; case (Zdiv_eucl_POS p b); intros q r [H0 H1]. generalize (Zgt_cases b (2 * r + 1)). @@ -147,6 +162,7 @@ case (Zge_bool b 2); (intros; split; [ try ring | omega ]). omega. Qed. +(** Then the usual situation of a positive [b] and no restriction on [a] *) Theorem Z_div_mod : forall a b:Z, @@ -166,27 +182,131 @@ Proof. intros [H1 H2]. split; trivial. - replace (Zneg p0) with (- Zpos p0); [ rewrite H1; ring | trivial ]. + change (Zneg p0) with (- Zpos p0); rewrite H1; ring. intros p1 [H1 H2]. split; trivial. - replace (Zneg p0) with (- Zpos p0); [ rewrite H1; ring | trivial ]. + change (Zneg p0) with (- Zpos p0); rewrite H1; ring. generalize (Zorder.Zgt_pos_0 p1); omega. intros p1 [H1 H2]. split; trivial. - replace (Zneg p0) with (- Zpos p0); [ rewrite H1; ring | trivial ]. + change (Zneg p0) with (- Zpos p0); rewrite H1; ring. generalize (Zorder.Zlt_neg_0 p1); omega. intros; discriminate. Qed. -(** Existence theorems *) +(** For stating the fully general result, let's give a short name + to the condition on the remainder. *) -Theorem Zdiv_eucl_exist : - forall b:Z, - b > 0 -> - forall a:Z, {qr : Z * Z | let (q, r) := qr in a = b * q + r /\ 0 <= r < b}. +Definition Remainder r b := 0 <= r < b \/ b < r <= 0. + +(** Another equivalent formulation: *) + +Definition Remainder_alt r b := Zabs r < Zabs b /\ Zsgn r <> - Zsgn b. + +(* In the last formulation, [ Zsgn r <> - Zsgn b ] is less nice than saying + [ Zsgn r = Zsgn b ], but at least it works even when [r] is null. *) + +Lemma Remainder_equiv : forall r b, Remainder r b <-> Remainder_alt r b. +Proof. + intros; unfold Remainder, Remainder_alt; omega with *. +Qed. + +Hint Unfold Remainder. + +(** Now comes the fully general result about Euclidean division. *) + +Theorem Z_div_mod_full : + forall a b:Z, + b <> 0 -> let (q, r) := Zdiv_eucl a b in a = b * q + r /\ Remainder r b. +Proof. + destruct b as [|b|b]. + (* b = 0 *) + intro H; elim H; auto. + (* b > 0 *) + intros _. + assert (Zpos b > 0) by auto with zarith. + generalize (Z_div_mod a (Zpos b) H). + destruct Zdiv_eucl as (q,r); intuition; simpl; auto. + (* b < 0 *) + intros _. + assert (Zpos b > 0) by auto with zarith. + generalize (Z_div_mod a (Zpos b) H). + unfold Remainder. + destruct a as [|a|a]. + (* a = 0 *) + simpl; intuition. + (* a > 0 *) + unfold Zdiv_eucl; destruct Zdiv_eucl_POS as (q,r). + destruct r as [|r|r]; [ | | omega with *]. + rewrite <- Zmult_opp_comm; simpl Zopp; intuition. + rewrite <- Zmult_opp_comm; simpl Zopp. + rewrite Zmult_plus_distr_r; omega with *. + (* a < 0 *) + unfold Zdiv_eucl. + generalize (Z_div_mod_POS (Zpos b) H a). + destruct Zdiv_eucl_POS as (q,r). + destruct r as [|r|r]; change (Zneg b) with (-Zpos b). + rewrite Zmult_opp_comm; omega with *. + rewrite <- Zmult_opp_comm, Zmult_plus_distr_r; + repeat rewrite Zmult_opp_comm; omega. + rewrite Zmult_opp_comm; omega with *. +Qed. + +(** The same results as before, stated separately in terms of Zdiv and Zmod *) + +Lemma Z_mod_remainder : forall a b:Z, b<>0 -> Remainder (a mod b) b. +Proof. + unfold Zmod; intros a b Hb; generalize (Z_div_mod_full a b Hb); auto. + destruct Zdiv_eucl; tauto. +Qed. + +Lemma Z_mod_lt : forall a b:Z, b > 0 -> 0 <= a mod b < b. +Proof. + unfold Zmod; intros a b Hb; generalize (Z_div_mod a b Hb). + destruct Zdiv_eucl; tauto. +Qed. + +Lemma Z_mod_neg : forall a b:Z, b < 0 -> b < a mod b <= 0. +Proof. + unfold Zmod; intros a b Hb. + assert (Hb' : b<>0) by (auto with zarith). + generalize (Z_div_mod_full a b Hb'). + destruct Zdiv_eucl. + unfold Remainder; intuition. +Qed. + +Lemma Z_div_mod_eq_full : forall a b:Z, b <> 0 -> a = b*(a/b) + (a mod b). +Proof. + unfold Zdiv, Zmod; intros a b Hb; generalize (Z_div_mod_full a b Hb). + destruct Zdiv_eucl; tauto. +Qed. + +Lemma Z_div_mod_eq : forall a b:Z, b > 0 -> a = b*(a/b) + (a mod b). +Proof. + intros; apply Z_div_mod_eq_full; auto with zarith. +Qed. + +Lemma Zmod_eq_full : forall a b:Z, b<>0 -> a mod b = a - (a/b)*b. +Proof. + intros. + rewrite <- Zeq_plus_swap, Zplus_comm, Zmult_comm; symmetry. + apply Z_div_mod_eq_full; auto. +Qed. + +Lemma Zmod_eq : forall a b:Z, b>0 -> a mod b = a - (a/b)*b. +Proof. + intros. + rewrite <- Zeq_plus_swap, Zplus_comm, Zmult_comm; symmetry. + apply Z_div_mod_eq; auto. +Qed. + +(** Existence theorem *) + +Theorem Zdiv_eucl_exist : forall (b:Z)(Hb:b>0)(a:Z), + {qr : Z * Z | let (q, r) := qr in a = b * q + r /\ 0 <= r < b}. Proof. intros b Hb a. exists (Zdiv_eucl a b). @@ -195,70 +315,180 @@ Qed. Implicit Arguments Zdiv_eucl_exist. -Theorem Zdiv_eucl_extended : - forall b:Z, - b <> 0 -> - forall a:Z, - {qr : Z * Z | let (q, r) := qr in a = b * q + r /\ 0 <= r < Zabs b}. + +(** Uniqueness theorems *) + +Theorem Zdiv_mod_unique : + forall b q1 q2 r1 r2:Z, + 0 <= r1 < Zabs b -> 0 <= r2 < Zabs b -> + b*q1+r1 = b*q2+r2 -> q1=q2 /\ r1=r2. Proof. - intros b Hb a. - elim (Z_le_gt_dec 0 b); intro Hb'. - cut (b > 0); [ intro Hb'' | omega ]. - rewrite Zabs_eq; [ apply Zdiv_eucl_exist; assumption | assumption ]. - cut (- b > 0); [ intro Hb'' | omega ]. - elim (Zdiv_eucl_exist Hb'' a); intros qr. - elim qr; intros q r Hqr. - exists (- q, r). - elim Hqr; intros. - split. - rewrite <- Zmult_opp_comm; assumption. - rewrite Zabs_non_eq; [ assumption | omega ]. +intros b q1 q2 r1 r2 Hr1 Hr2 H. +destruct (Z_eq_dec q1 q2) as [Hq|Hq]. +split; trivial. +rewrite Hq in H; omega. +elim (Zlt_not_le (Zabs (r2 - r1)) (Zabs b)). +omega with *. +replace (r2-r1) with (b*(q1-q2)) by (rewrite Zmult_minus_distr_l; omega). +replace (Zabs b) with ((Zabs b)*1) by ring. +rewrite Zabs_Zmult. +apply Zmult_le_compat_l; auto with *. +omega with *. Qed. -Implicit Arguments Zdiv_eucl_extended. +Theorem Zdiv_mod_unique_2 : + forall b q1 q2 r1 r2:Z, + Remainder r1 b -> Remainder r2 b -> + b*q1+r1 = b*q2+r2 -> q1=q2 /\ r1=r2. +Proof. +unfold Remainder. +intros b q1 q2 r1 r2 Hr1 Hr2 H. +destruct (Z_eq_dec q1 q2) as [Hq|Hq]. +split; trivial. +rewrite Hq in H; omega. +elim (Zlt_not_le (Zabs (r2 - r1)) (Zabs b)). +omega with *. +replace (r2-r1) with (b*(q1-q2)) by (rewrite Zmult_minus_distr_l; omega). +replace (Zabs b) with ((Zabs b)*1) by ring. +rewrite Zabs_Zmult. +apply Zmult_le_compat_l; auto with *. +omega with *. +Qed. -(** * Auxiliary lemmas about [Zdiv] and [Zmod] *) +Theorem Zdiv_unique_full: + forall a b q r, Remainder r b -> + a = b*q + r -> q = a/b. +Proof. + intros. + assert (b <> 0) by (unfold Remainder in *; omega with *). + generalize (Z_div_mod_full a b H1). + unfold Zdiv; destruct Zdiv_eucl as (q',r'). + intros (H2,H3); rewrite H2 in H0. + destruct (Zdiv_mod_unique_2 b q q' r r'); auto. +Qed. -Lemma Z_div_mod_eq : forall a b:Z, b > 0 -> a = b * Zdiv a b + Zmod a b. +Theorem Zdiv_unique: + forall a b q r, 0 <= r < b -> + a = b*q + r -> q = a/b. Proof. - unfold Zdiv, Zmod in |- *. - intros a b Hb. - generalize (Z_div_mod a b Hb). - case Zdiv_eucl; tauto. + intros; eapply Zdiv_unique_full; eauto. Qed. -Lemma Z_mod_lt : forall a b:Z, b > 0 -> 0 <= Zmod a b < b. +Theorem Zmod_unique_full: + forall a b q r, Remainder r b -> + a = b*q + r -> r = a mod b. Proof. - unfold Zmod in |- *. - intros a b Hb. - generalize (Z_div_mod a b Hb). - case (Zdiv_eucl a b); tauto. + intros. + assert (b <> 0) by (unfold Remainder in *; omega with *). + generalize (Z_div_mod_full a b H1). + unfold Zmod; destruct Zdiv_eucl as (q',r'). + intros (H2,H3); rewrite H2 in H0. + destruct (Zdiv_mod_unique_2 b q q' r r'); auto. Qed. -Lemma Z_div_POS_ge0 : - forall (b:Z) (a:positive), let (q, _) := Zdiv_eucl_POS a b in q >= 0. +Theorem Zmod_unique: + forall a b q r, 0 <= r < b -> + a = b*q + r -> r = a mod b. Proof. - simple induction a; unfold Zdiv_eucl_POS in |- *; fold Zdiv_eucl_POS in |- *. - intro p; case (Zdiv_eucl_POS p b). - intros; case (Zgt_bool b (2 * z0 + 1)); intros; omega. - intro p; case (Zdiv_eucl_POS p b). - intros; case (Zgt_bool b (2 * z0)); intros; omega. - case (Zge_bool b 2); simpl in |- *; omega. + intros; eapply Zmod_unique_full; eauto. Qed. -Lemma Z_div_ge0 : forall a b:Z, b > 0 -> a >= 0 -> Zdiv a b >= 0. +(** * Basic values of divisions and modulo. *) + +Lemma Zmod_0_l: forall a, 0 mod a = 0. Proof. - intros a b Hb; unfold Zdiv, Zdiv_eucl in |- *; case a; simpl in |- *; intros. - case b; simpl in |- *; trivial. - generalize Hb; case b; try trivial. - auto with zarith. - intros p0 Hp0; generalize (Z_div_POS_ge0 (Zpos p0) p). - case (Zdiv_eucl_POS p (Zpos p0)); simpl in |- *; tauto. - intros; discriminate. - elim H; trivial. + destruct a; simpl; auto. +Qed. + +Lemma Zmod_0_r: forall a, a mod 0 = 0. +Proof. + destruct a; simpl; auto. +Qed. + +Lemma Zdiv_0_l: forall a, 0/a = 0. +Proof. + destruct a; simpl; auto. +Qed. + +Lemma Zdiv_0_r: forall a, a/0 = 0. +Proof. + destruct a; simpl; auto. +Qed. + +Lemma Zmod_1_r: forall a, a mod 1 = 0. +Proof. + intros; symmetry; apply Zmod_unique with a; auto with zarith. Qed. -Lemma Z_div_lt : forall a b:Z, b >= 2 -> a > 0 -> Zdiv a b < a. +Lemma Zdiv_1_r: forall a, a/1 = a. +Proof. + intros; symmetry; apply Zdiv_unique with 0; auto with zarith. +Qed. + +Hint Resolve Zmod_0_l Zmod_0_r Zdiv_0_l Zdiv_0_r Zdiv_1_r Zmod_1_r + : zarith. + +Lemma Zdiv_1_l: forall a, 1 < a -> 1/a = 0. +Proof. + intros; symmetry; apply Zdiv_unique with 1; auto with zarith. +Qed. + +Lemma Zmod_1_l: forall a, 1 < a -> 1 mod a = 1. +Proof. + intros; symmetry; apply Zmod_unique with 0; auto with zarith. +Qed. + +Lemma Z_div_same_full : forall a:Z, a<>0 -> a/a = 1. +Proof. + intros; symmetry; apply Zdiv_unique_full with 0; auto with *; red; omega. +Qed. + +Lemma Z_mod_same_full : forall a, a mod a = 0. +Proof. + destruct a; intros; symmetry. + compute; auto. + apply Zmod_unique with 1; auto with *; omega with *. + apply Zmod_unique_full with 1; auto with *; red; omega with *. +Qed. + +Lemma Z_mod_mult : forall a b, (a*b) mod b = 0. +Proof. + intros a b; destruct (Z_eq_dec b 0) as [Hb|Hb]. + subst; simpl; rewrite Zmod_0_r; auto. + symmetry; apply Zmod_unique_full with a; [ red; omega | ring ]. +Qed. + +Lemma Z_div_mult_full : forall a b:Z, b <> 0 -> (a*b)/b = a. +Proof. + intros; symmetry; apply Zdiv_unique_full with 0; auto with zarith; + [ red; omega | ring]. +Qed. + +(** * Order results about Zmod and Zdiv *) + +(* Division of positive numbers is positive. *) + +Lemma Z_div_pos: forall a b, b > 0 -> 0 <= a -> 0 <= a/b. +Proof. + intros. + rewrite (Z_div_mod_eq a b H) in H0. + assert (H1:=Z_mod_lt a b H). + destruct (Z_lt_le_dec (a/b) 0); auto. + assert (b*(a/b) <= -b). + replace (-b) with (b*-1); [ | ring]. + apply Zmult_le_compat_l; auto with zarith. + omega. +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. +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. cut (b > 0); [ intro Hb | omega ]. generalize (Z_div_mod a b Hb). @@ -271,9 +501,24 @@ Proof. auto with zarith. Qed. -(** * Other lemmas (now using the syntax for [Zdiv] and [Zmod]). *) -Lemma Z_div_ge : forall a b c:Z, c > 0 -> a >= b -> a / c >= b / c. +(** A division of a small number by a bigger one yields zero. *) + +Theorem Zdiv_small: forall a b, 0 <= a < b -> a/b = 0. +Proof. + intros a b H; apply sym_equal; apply Zdiv_unique with a; auto with zarith. +Qed. + +(** Same situation, in term of modulo: *) + +Theorem Zmod_small: forall a n, 0 <= a < n -> a mod n = a. +Proof. + intros a b H; apply sym_equal; apply Zmod_unique with 0; auto with zarith. +Qed. + +(** [Zge] 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 a b c cPos aGeb. generalize (Z_div_mod_eq a c cPos). @@ -285,13 +530,8 @@ Proof. intro. absurd (b - a >= 1). omega. - rewrite H0. - rewrite H2. - assert - (c * (b / c) + b mod c - (c * (a / c) + a mod c) = - c * (b / c - a / c) + b mod c - a mod c). - ring. - rewrite H3. + replace (b-a) with (c * (b/c-a/c) + b mod c - a mod c) by + (symmetry; pattern a at 1; rewrite H2; pattern b at 1; rewrite H0; ring). assert (c * (b / c - a / c) >= c * 1). apply Zmult_ge_compat_l. omega. @@ -301,111 +541,639 @@ Proof. omega. Qed. -Lemma Z_mod_plus : forall a b c:Z, c > 0 -> (a + b * c) mod c = a mod c. +(** Same, with [Zle]. *) + +Lemma Z_div_le : forall a b c:Z, c > 0 -> a <= b -> a/c <= b/c. Proof. - intros a b c cPos. - generalize (Z_div_mod_eq a c cPos). - generalize (Z_mod_lt a c cPos). - generalize (Z_div_mod_eq (a + b * c) c cPos). - generalize (Z_mod_lt (a + b * c) c cPos). - intros. + intros a b c H H0. + apply Zge_le. + apply Z_div_ge; auto with *. +Qed. - assert ((a + b * c) mod c - a mod c = c * (b + a / c - (a + b * c) / c)). - replace ((a + b * c) mod c) with (a + b * c - c * ((a + b * c) / c)). - replace (a mod c) with (a - c * (a / c)). - ring. - omega. - omega. - set (q := b + a / c - (a + b * c) / c) in *. - apply (Zcase_sign q); intros. - assert (c * q = 0). - rewrite H4; ring. - rewrite H5 in H3. - omega. +(** With our choice of division, rounding of (a/b) is always done toward bottom: *) - assert (c * q >= c). - pattern c at 2 in |- *; replace c with (c * 1). - apply Zmult_ge_compat_l; omega. - ring. - omega. +Lemma Z_mult_div_ge : forall a b:Z, b > 0 -> b*(a/b) <= a. +Proof. + intros a b H; generalize (Z_div_mod_eq a b H) (Z_mod_lt a b H); omega. +Qed. + +Lemma Z_mult_div_ge_neg : forall a b:Z, b < 0 -> b*(a/b) >= a. +Proof. + intros a b H. + generalize (Z_div_mod_eq_full a _ (Zlt_not_eq _ _ H)) (Z_mod_neg a _ H); omega. +Qed. + +(** The previous inequalities are exact iff the modulo is zero. *) + +Lemma Z_div_exact_full_1 : forall a b:Z, a = b*(a/b) -> a mod b = 0. +Proof. + intros; destruct (Z_eq_dec b 0) as [Hb|Hb]. + subst b; simpl in *; subst; auto. + generalize (Z_div_mod_eq_full a b Hb); omega. +Qed. + +Lemma Z_div_exact_full_2 : forall a b:Z, b <> 0 -> a mod b = 0 -> a = b*(a/b). +Proof. + intros; generalize (Z_div_mod_eq_full a b H); omega. +Qed. + +(** A modulo cannot grow beyond its starting point. *) + +Theorem Zmod_le: forall a b, 0 < b -> 0 <= a -> a mod b <= a. +Proof. + intros a b H1 H2; case (Zle_or_lt b a); intros H3. + case (Z_mod_lt a b); auto with zarith. + rewrite Zmod_small; auto with zarith. +Qed. + +(** Some additionnal inequalities about Zdiv. *) + +Theorem Zdiv_le_upper_bound: + forall a b q, 0 <= a -> 0 < b -> a <= q*b -> a/b <= q. +Proof. + intros a b q H1 H2 H3. + apply Zmult_le_reg_r with b; auto with zarith. + apply Zle_trans with (2 := H3). + pattern a at 2; rewrite (Z_div_mod_eq a b); auto with zarith. + rewrite (Zmult_comm b); case (Z_mod_lt a b); auto with zarith. +Qed. + +Theorem Zdiv_lt_upper_bound: + forall a b q, 0 <= a -> 0 < b -> a < q*b -> a/b < q. +Proof. + intros a b q H1 H2 H3. + apply Zmult_lt_reg_r with b; auto with zarith. + apply Zle_lt_trans with (2 := H3). + pattern a at 2; rewrite (Z_div_mod_eq a b); auto with zarith. + rewrite (Zmult_comm b); case (Z_mod_lt a b); auto with zarith. +Qed. + +Theorem Zdiv_le_lower_bound: + forall a b q, 0 <= a -> 0 < b -> q*b <= a -> q <= a/b. +Proof. + intros a b q H1 H2 H3. + assert (q < a / b + 1); auto with zarith. + apply Zmult_lt_reg_r with b; auto with zarith. + apply Zle_lt_trans with (1 := H3). + pattern a at 1; rewrite (Z_div_mod_eq a b); auto with zarith. + rewrite Zmult_plus_distr_l; rewrite (Zmult_comm b); case (Z_mod_lt a b); + auto with zarith. +Qed. + + +(** A division of respect opposite monotonicity for the divisor *) + +Lemma Zdiv_le_compat_l: forall p q r, 0 <= p -> 0 < q < r -> + p / r <= p / q. +Proof. + intros p q r H H1. + apply Zdiv_le_lower_bound; auto with zarith. + rewrite Zmult_comm. + pattern p at 2; rewrite (Z_div_mod_eq p r); auto with zarith. + apply Zle_trans with (r * (p / r)); auto with zarith. + apply Zmult_le_compat_r; auto with zarith. + apply Zdiv_le_lower_bound; auto with zarith. + case (Z_mod_lt p r); auto with zarith. +Qed. + +Theorem Zdiv_sgn: forall a b, + 0 <= Zsgn (a/b) * Zsgn a * Zsgn 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 Zdiv, Zdiv_eucl; + destruct Zdiv_eucl_POS as (q,r); destruct r; omega with *. +Qed. + +(** * Relations between usual operations and Zmod and Zdiv *) + +Lemma Z_mod_plus_full : forall a b c:Z, (a + b * c) mod c = a mod c. +Proof. + intros; destruct (Z_eq_dec c 0) as [Hc|Hc]. + subst; do 2 rewrite Zmod_0_r; auto. + symmetry; apply Zmod_unique_full with (a/c+b); auto with zarith. + red; generalize (Z_mod_lt a c)(Z_mod_neg a c); omega. + rewrite Zmult_plus_distr_r, Zmult_comm. + generalize (Z_div_mod_eq_full a c Hc); omega. +Qed. + +Lemma Z_div_plus_full : forall a b c:Z, c <> 0 -> (a + b * c) / c = a / c + b. +Proof. + intro; symmetry. + apply Zdiv_unique_full with (a mod c); auto with zarith. + red; generalize (Z_mod_lt a c)(Z_mod_neg a c); omega. + rewrite Zmult_plus_distr_r, Zmult_comm. + generalize (Z_div_mod_eq_full a c H); omega. +Qed. + +Theorem Z_div_plus_full_l: forall a b c : Z, b <> 0 -> (a * b + c) / b = a + c / b. +Proof. + intros a b c H; rewrite Zplus_comm; rewrite Z_div_plus_full; + try apply Zplus_comm; auto with zarith. +Qed. - assert (c * q <= - c). - replace (- c) with (c * -1). - apply Zmult_le_compat_l; omega. +(** [Zopp] and [Zdiv], [Zmod]. + Due to the choice of convention for our Euclidean division, + some of the relations about [Zopp] and divisions are rather complex. *) + +Lemma Zdiv_opp_opp : forall a b:Z, (-a)/(-b) = a/b. +Proof. + intros [|a|a] [|b|b]; try reflexivity; unfold Zdiv; simpl; + destruct (Zdiv_eucl_POS a (Zpos b)); destruct z0; try reflexivity. +Qed. + +Lemma Zmod_opp_opp : forall a b:Z, (-a) mod (-b) = - (a mod b). +Proof. + intros; destruct (Z_eq_dec b 0) as [Hb|Hb]. + subst; do 2 rewrite Zmod_0_r; auto. + intros; symmetry. + apply Zmod_unique_full with ((-a)/(-b)); auto. + generalize (Z_mod_remainder a b Hb); destruct 1; [right|left]; omega. + rewrite Zdiv_opp_opp. + pattern a at 1; rewrite (Z_div_mod_eq_full a b Hb); ring. +Qed. + +Lemma Z_mod_zero_opp_full : forall a b:Z, a mod b = 0 -> (-a) mod b = 0. +Proof. + intros; destruct (Z_eq_dec b 0) as [Hb|Hb]. + subst; rewrite Zmod_0_r; auto. + rewrite Z_div_exact_full_2 with a b; auto. + replace (- (b * (a / b))) with (0 + - (a / b) * b). + rewrite Z_mod_plus_full; auto. ring. - omega. Qed. -Lemma Z_div_plus : forall a b c:Z, c > 0 -> (a + b * c) / c = a / c + b. +Lemma Z_mod_nz_opp_full : forall a b:Z, a mod b <> 0 -> + (-a) mod b = b - (a mod b). Proof. - intros a b c cPos. - generalize (Z_div_mod_eq a c cPos). - generalize (Z_mod_lt a c cPos). - generalize (Z_div_mod_eq (a + b * c) c cPos). - generalize (Z_mod_lt (a + b * c) c cPos). intros. - apply Zmult_reg_l with c. omega. - replace (c * ((a + b * c) / c)) with (a + b * c - (a + b * c) mod c). - rewrite (Z_mod_plus a b c cPos). - pattern a at 1 in |- *; rewrite H2. - ring. - pattern (a + b * c) at 1 in |- *; rewrite H0. - ring. + assert (b<>0) by (contradict H; subst; rewrite Zmod_0_r; auto). + symmetry; apply Zmod_unique_full with (-1-a/b); auto. + generalize (Z_mod_remainder a b H0); destruct 1; [left|right]; omega. + rewrite Zmult_minus_distr_l. + pattern a at 1; rewrite (Z_div_mod_eq_full a b H0); ring. Qed. -Lemma Z_div_mult : forall a b:Z, b > 0 -> a * b / b = a. - intros; replace (a * b) with (0 + a * b); auto. - rewrite Z_div_plus; auto. +Lemma Z_mod_zero_opp_r : forall a b:Z, a mod b = 0 -> a mod (-b) = 0. +Proof. + intros. + rewrite <- (Zopp_involutive a). + rewrite Zmod_opp_opp. + rewrite Z_mod_zero_opp_full; auto. Qed. -Lemma Z_mult_div_ge : forall a b:Z, b > 0 -> b * (a / b) <= a. +Lemma Z_mod_nz_opp_r : forall a b:Z, a mod b <> 0 -> + a mod (-b) = (a mod b) - b. Proof. - intros a b bPos. - generalize (Z_div_mod_eq a _ bPos); intros. - generalize (Z_mod_lt a _ bPos); intros. - pattern a at 2 in |- *; rewrite H. - omega. + intros. + pattern a at 1; rewrite <- (Zopp_involutive a). + rewrite Zmod_opp_opp. + rewrite Z_mod_nz_opp_full; auto; omega. +Qed. + +Lemma Z_div_zero_opp_full : forall a b:Z, a mod b = 0 -> (-a)/b = -(a/b). +Proof. + intros; destruct (Z_eq_dec b 0) as [Hb|Hb]. + subst; do 2 rewrite Zdiv_0_r; auto. + symmetry; apply Zdiv_unique_full with 0; auto. + red; omega. + pattern a at 1; rewrite (Z_div_mod_eq_full a b Hb). + rewrite H; ring. Qed. -Lemma Z_mod_same : forall a:Z, a > 0 -> a mod a = 0. +Lemma Z_div_nz_opp_full : forall a b:Z, a mod b <> 0 -> + (-a)/b = -(a/b)-1. Proof. - intros a aPos. - generalize (Z_mod_plus 0 1 a aPos). - replace (0 + 1 * a) with a. intros. - rewrite H. - compute in |- *. - trivial. - ring. + assert (b<>0) by (contradict H; subst; rewrite Zmod_0_r; auto). + symmetry; apply Zdiv_unique_full with (b-a mod b); auto. + generalize (Z_mod_remainder a b H0); destruct 1; [left|right]; omega. + pattern a at 1; rewrite (Z_div_mod_eq_full a b H0); ring. +Qed. + +Lemma Z_div_zero_opp_r : forall a b:Z, a mod b = 0 -> a/(-b) = -(a/b). +Proof. + intros. + pattern a at 1; rewrite <- (Zopp_involutive a). + rewrite Zdiv_opp_opp. + rewrite Z_div_zero_opp_full; auto. +Qed. + +Lemma Z_div_nz_opp_r : forall a b:Z, a mod b <> 0 -> + a/(-b) = -(a/b)-1. +Proof. + intros. + pattern a at 1; rewrite <- (Zopp_involutive a). + rewrite Zdiv_opp_opp. + rewrite Z_div_nz_opp_full; auto; omega. +Qed. + +(** Cancellations. *) + +Lemma Zdiv_mult_cancel_r : forall a b c:Z, + c <> 0 -> (a*c)/(b*c) = a/b. +Proof. +assert (X: forall a b c, b > 0 -> c > 0 -> (a*c) / (b*c) = a / b). + intros a b c Hb Hc. + symmetry. + apply Zdiv_unique with ((a mod b)*c); auto with zarith. + destruct (Z_mod_lt a b Hb); split. + apply Zmult_le_0_compat; auto with zarith. + apply Zmult_lt_compat_r; auto with zarith. + pattern a at 1; rewrite (Z_div_mod_eq a b Hb); ring. +intros a b c Hc. +destruct (Z_dec b 0) as [Hb|Hb]. +destruct Hb as [Hb|Hb]; destruct (not_Zeq_inf _ _ Hc); auto with *. +rewrite <- (Zdiv_opp_opp a), <- (Zmult_opp_opp b), <-(Zmult_opp_opp a); + auto with *. +rewrite <- (Zdiv_opp_opp a), <- Zdiv_opp_opp, Zopp_mult_distr_l, + Zopp_mult_distr_l; auto with *. +rewrite <- Zdiv_opp_opp, Zopp_mult_distr_r, Zopp_mult_distr_r; auto with *. +rewrite Hb; simpl; do 2 rewrite Zdiv_0_r; auto. Qed. -Lemma Z_div_same : forall a:Z, a > 0 -> a / a = 1. +Lemma Zdiv_mult_cancel_l : forall a b c:Z, + c<>0 -> (c*a)/(c*b) = a/b. Proof. - intros a aPos. - generalize (Z_div_plus 0 1 a aPos). - replace (0 + 1 * a) with a. intros. - rewrite H. - compute in |- *. - trivial. + rewrite (Zmult_comm c a); rewrite (Zmult_comm c b). + apply Zdiv_mult_cancel_r; auto. +Qed. + +Lemma Zmult_mod_distr_l: forall a b c, + (c*a) mod (c*b) = c * (a mod b). +Proof. + intros; destruct (Z_eq_dec c 0) as [Hc|Hc]. + subst; simpl; rewrite Zmod_0_r; auto. + destruct (Z_eq_dec b 0) as [Hb|Hb]. + subst; repeat rewrite Zmult_0_r || rewrite Zmod_0_r; auto. + assert (c*b <> 0). + contradict Hc; eapply Zmult_integral_l; eauto. + rewrite (Zplus_minus_eq _ _ _ (Z_div_mod_eq_full (c*a) (c*b) H)). + rewrite (Zplus_minus_eq _ _ _ (Z_div_mod_eq_full a b Hb)). + rewrite Zdiv_mult_cancel_l; auto with zarith. ring. Qed. -Lemma Z_div_exact_1 : forall a b:Z, b > 0 -> a = b * (a / b) -> a mod b = 0. - intros a b Hb; generalize (Z_div_mod a b Hb); unfold Zmod, Zdiv in |- *. - case (Zdiv_eucl a b); intros q r; omega. +Lemma Zmult_mod_distr_r: forall a b c, + (a*c) mod (b*c) = (a mod b) * c. +Proof. + intros; repeat rewrite (fun x => (Zmult_comm x c)). + apply Zmult_mod_distr_l; auto. +Qed. + +(** Operations modulo. *) + +Theorem Zmod_mod: forall a n, (a mod n) mod n = a mod n. +Proof. + intros; destruct (Z_eq_dec n 0) as [Hb|Hb]. + subst; do 2 rewrite Zmod_0_r; auto. + pattern a at 2; rewrite (Z_div_mod_eq_full a n); auto with zarith. + rewrite Zplus_comm; rewrite Zmult_comm. + apply sym_equal; apply Z_mod_plus_full; auto with zarith. +Qed. + +Theorem Zmult_mod: forall a b n, + (a * b) mod n = ((a mod n) * (b mod n)) mod n. +Proof. + intros; destruct (Z_eq_dec n 0) as [Hb|Hb]. + subst; do 2 rewrite Zmod_0_r; auto. + pattern a at 1; rewrite (Z_div_mod_eq_full a n); auto with zarith. + pattern b at 1; rewrite (Z_div_mod_eq_full b n); auto with zarith. + set (A:=a mod n); set (B:=b mod n); set (A':=a/n); set (B':=b/n). + replace ((n*A' + A) * (n*B' + B)) + with (A*B + (A'*B+B'*A+n*A'*B')*n) by ring. + apply Z_mod_plus_full; auto with zarith. Qed. -Lemma Z_div_exact_2 : forall a b:Z, b > 0 -> a mod b = 0 -> a = b * (a / b). - intros a b Hb; generalize (Z_div_mod a b Hb); unfold Zmod, Zdiv in |- *. - case (Zdiv_eucl a b); intros q r; omega. +Theorem Zplus_mod: forall a b n, + (a + b) mod n = (a mod n + b mod n) mod n. +Proof. + intros; destruct (Z_eq_dec n 0) as [Hb|Hb]. + subst; do 2 rewrite Zmod_0_r; auto. + pattern a at 1; rewrite (Z_div_mod_eq_full a n); auto with zarith. + pattern b at 1; rewrite (Z_div_mod_eq_full b n); auto with zarith. + replace ((n * (a / n) + a mod n) + (n * (b / n) + b mod n)) + with ((a mod n + b mod n) + (a / n + b / n) * n) by ring. + apply Z_mod_plus_full; auto with zarith. Qed. -Lemma Z_mod_zero_opp : forall a b:Z, b > 0 -> a mod b = 0 -> - a mod b = 0. - intros a b Hb. +Theorem Zminus_mod: forall a b n, + (a - b) mod n = (a mod n - b mod n) mod n. +Proof. intros. - rewrite Z_div_exact_2 with a b; auto. - replace (- (b * (a / b))) with (0 + - (a / b) * b). - rewrite Z_mod_plus; auto. + replace (a - b) with (a + (-1) * b); auto with zarith. + replace (a mod n - b mod n) with (a mod n + (-1) * (b mod n)); auto with zarith. + rewrite Zplus_mod. + rewrite Zmult_mod. + rewrite Zplus_mod with (b:=(-1) * (b mod n)). + rewrite Zmult_mod. + rewrite Zmult_mod with (b:= b mod n). + repeat rewrite Zmod_mod; auto. +Qed. + +Lemma Zplus_mod_idemp_l: forall a b n, (a mod n + b) mod n = (a + b) mod n. +Proof. + intros; rewrite Zplus_mod, Zmod_mod, <- Zplus_mod; auto. +Qed. + +Lemma Zplus_mod_idemp_r: forall a b n, (b + a mod n) mod n = (b + a) mod n. +Proof. + intros; rewrite Zplus_mod, Zmod_mod, <- Zplus_mod; auto. +Qed. + +Lemma Zminus_mod_idemp_l: forall a b n, (a mod n - b) mod n = (a - b) mod n. +Proof. + intros; rewrite Zminus_mod, Zmod_mod, <- Zminus_mod; auto. +Qed. + +Lemma Zminus_mod_idemp_r: forall a b n, (a - b mod n) mod n = (a - b) mod n. +Proof. + intros; rewrite Zminus_mod, Zmod_mod, <- Zminus_mod; auto. +Qed. + +Lemma Zmult_mod_idemp_l: forall a b n, (a mod n * b) mod n = (a * b) mod n. +Proof. + intros; rewrite Zmult_mod, Zmod_mod, <- Zmult_mod; auto. +Qed. + +Lemma Zmult_mod_idemp_r: forall a b n, (b * (a mod n)) mod n = (b * a) mod n. +Proof. + intros; rewrite Zmult_mod, Zmod_mod, <- Zmult_mod; auto. +Qed. + +(** For a specific number n, equality modulo n is hence a nice setoid + equivalence, compatible with the usual operations. Due to restrictions + with Coq setoids, we cannot state this in a section, but it works + at least with a module. *) + +Module Type SomeNumber. + Parameter n:Z. +End SomeNumber. + +Module EqualityModulo (M:SomeNumber). + + Definition eqm a b := (a mod M.n = b mod M.n). + Infix "==" := eqm (at level 70). + + Lemma eqm_refl : forall a, a == a. + Proof. unfold eqm; auto. Qed. + + Lemma eqm_sym : forall a b, a == b -> b == a. + Proof. unfold eqm; auto. Qed. + + Lemma eqm_trans : forall a b c, a == b -> b == c -> a == c. + Proof. unfold eqm; eauto with *. Qed. + + Add Relation Z eqm + reflexivity proved by eqm_refl + symmetry proved by eqm_sym + transitivity proved by eqm_trans as eqm_setoid. + + Add Morphism Zplus : Zplus_eqm. + Proof. + unfold eqm; intros; rewrite Zplus_mod, H, H0, <- Zplus_mod; auto. + Qed. + + Add Morphism Zminus : Zminus_eqm. + Proof. + unfold eqm; intros; rewrite Zminus_mod, H, H0, <- Zminus_mod; auto. + Qed. + + Add Morphism Zmult : Zmult_eqm. + Proof. + unfold eqm; intros; rewrite Zmult_mod, H, H0, <- Zmult_mod; auto. + Qed. + + Add Morphism Zopp : Zopp_eqm. + Proof. + intros; change (-x == -y) with (0-x == 0-y). + rewrite H; red; auto. + Qed. + + Lemma Zmod_eqm : forall a, a mod M.n == a. + Proof. + unfold eqm; intros; apply Zmod_mod. + Qed. + + (* Zmod and Zdiv are not full morphisms with respect to eqm. + For instance, take n=2. Then 3 == 1 but we don't have + 1 mod 3 == 1 mod 1 nor 1/3 == 1/1. + *) + +End EqualityModulo. + +Lemma Zdiv_Zdiv : forall a b c, 0<=b -> 0<=c -> (a/b)/c = a/(b*c). +Proof. + intros a b c Hb Hc. + destruct (Zle_lt_or_eq _ _ Hb); [ | subst; rewrite Zdiv_0_r, Zdiv_0_r, Zdiv_0_l; auto]. + destruct (Zle_lt_or_eq _ _ Hc); [ | subst; rewrite Zmult_0_r, Zdiv_0_r, Zdiv_0_r; auto]. + pattern a at 2;rewrite (Z_div_mod_eq_full a b);auto with zarith. + pattern (a/b) at 2;rewrite (Z_div_mod_eq_full (a/b) c);auto with zarith. + replace (b * (c * (a / b / c) + (a / b) mod c) + a mod b) with + ((a / b / c)*(b * c) + (b * ((a / b) mod c) + a mod b)) by ring. + rewrite Z_div_plus_full_l; auto with zarith. + rewrite (Zdiv_small (b * ((a / b) mod c) + a mod b)). ring. + split. + apply Zplus_le_0_compat;auto with zarith. + apply Zmult_le_0_compat;auto with zarith. + destruct (Z_mod_lt (a/b) c);auto with zarith. + destruct (Z_mod_lt a b);auto with zarith. + apply Zle_lt_trans with (b * ((a / b) mod c) + (b-1)). + destruct (Z_mod_lt a b);auto with zarith. + apply Zle_lt_trans with (b * (c-1) + (b - 1)). + apply Zplus_le_compat;auto with zarith. + destruct (Z_mod_lt (a/b) c);auto with zarith. + replace (b * (c - 1) + (b - 1)) with (b*c-1);try ring;auto with zarith. + intro H1; + assert (H2: c <> 0) by auto with zarith; + rewrite (Zmult_integral_l _ _ H2 H1) in H; auto with zarith. +Qed. + +(** Unfortunately, the previous result isn't always true on negative numbers. + For instance: 3/(-2)/(-2) = 1 <> 0 = 3 / (-2*-2) *) + +(** A last inequality: *) + +Theorem Zdiv_mult_le: + forall a b c, 0<=a -> 0<=b -> 0<=c -> c*(a/b) <= (c*a)/b. +Proof. + intros a b c H1 H2 H3. + destruct (Zle_lt_or_eq _ _ H2); + [ | subst; rewrite Zdiv_0_r, Zdiv_0_r, Zmult_0_r; auto]. + case (Z_mod_lt a b); auto with zarith; intros Hu1 Hu2. + case (Z_mod_lt c b); auto with zarith; intros Hv1 Hv2. + apply Zmult_le_reg_r with b; auto with zarith. + rewrite <- Zmult_assoc. + replace (a / b * b) with (a - a mod b). + replace (c * a / b * b) with (c * a - (c * a) mod b). + rewrite Zmult_minus_distr_l. + unfold Zminus; apply Zplus_le_compat_l. + match goal with |- - ?X <= -?Y => assert (Y <= X); auto with zarith end. + apply Zle_trans with ((c mod b) * (a mod b)); auto with zarith. + rewrite Zmult_mod; auto with zarith. + apply (Zmod_le ((c mod b) * (a mod b)) b); auto with zarith. + apply Zmult_le_compat_r; auto with zarith. + apply (Zmod_le c b); auto. + pattern (c * a) at 1; rewrite (Z_div_mod_eq (c * a) b); try ring; + auto with zarith. + pattern a at 1; rewrite (Z_div_mod_eq a b); try ring; auto with zarith. +Qed. + +(** Zmod is related to divisibility (see more in Znumtheory) *) + +Lemma Zmod_divides : forall a b, b<>0 -> + (a mod b = 0 <-> exists c, a = b*c). +Proof. + split; intros. + exists (a/b). + pattern a at 1; rewrite (Z_div_mod_eq_full a b); auto with zarith. + destruct H0 as [c Hc]. + symmetry. + apply Zmod_unique_full with c; auto with zarith. + red; omega with *. +Qed. + +(** * Compatibility *) + +(** Weaker results kept only for compatibility *) + +Lemma Z_mod_same : forall a, a > 0 -> a mod a = 0. +Proof. + intros; apply Z_mod_same_full. +Qed. + +Lemma Z_div_same : forall a, a > 0 -> a/a = 1. +Proof. + intros; apply Z_div_same_full; auto with zarith. +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. +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. Qed. + +Lemma Z_mod_plus : forall a b c:Z, c > 0 -> (a + b * c) mod c = a mod c. +Proof. + intros; apply Z_mod_plus_full; auto with zarith. +Qed. + +Lemma Z_div_exact_1 : forall a b:Z, b > 0 -> a = b*(a/b) -> a mod b = 0. +Proof. + intros; apply Z_div_exact_full_1; auto with zarith. +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. +Qed. + +Lemma Z_mod_zero_opp : forall a b:Z, b > 0 -> a mod b = 0 -> (-a) mod b = 0. +Proof. + intros; apply Z_mod_zero_opp_full; auto with zarith. +Qed. + +(** * A direct way to compute Zmod *) + +Fixpoint Zmod_POS (a : positive) (b : Z) {struct a} : Z := + match a with + | xI a' => + let r := Zmod_POS a' b in + let r' := (2 * r + 1) in + if Zgt_bool b r' then r' else (r' - b) + | xO a' => + let r := Zmod_POS a' b in + let r' := (2 * r) in + if Zgt_bool b r' then r' else (r' - b) + | xH => if Zge_bool b 2 then 1 else 0 + end. + +Definition Zmod' a b := + match a with + | Z0 => 0 + | Zpos a' => + match b with + | Z0 => 0 + | Zpos _ => Zmod_POS a' b + | Zneg b' => + let r := Zmod_POS a' (Zpos b') in + match r with Z0 => 0 | _ => b + r end + end + | Zneg a' => + match b with + | Z0 => 0 + | Zpos _ => + let r := Zmod_POS a' b in + match r with Z0 => 0 | _ => b - r end + | Zneg b' => - (Zmod_POS a' (Zpos b')) + end + end. + + +Theorem Zmod_POS_correct: forall a b, Zmod_POS a b = (snd (Zdiv_eucl_POS a b)). +Proof. + intros a b; elim a; simpl; auto. + intros p Rec; rewrite Rec. + case (Zdiv_eucl_POS p b); intros z1 z2; simpl; auto. + match goal with |- context [Zgt_bool _ ?X] => case (Zgt_bool b X) end; auto. + intros p Rec; rewrite Rec. + case (Zdiv_eucl_POS p b); intros z1 z2; simpl; auto. + match goal with |- context [Zgt_bool _ ?X] => case (Zgt_bool b X) end; auto. + case (Zge_bool b 2); auto. +Qed. + +Theorem Zmod'_correct: forall a b, Zmod' a b = Zmod a b. +Proof. + intros a b; unfold Zmod; case a; simpl; auto. + intros p; case b; simpl; auto. + intros p1; refine (Zmod_POS_correct _ _); auto. + intros p1; rewrite Zmod_POS_correct; auto. + case (Zdiv_eucl_POS p (Zpos p1)); simpl; intros z1 z2; case z2; auto. + intros p; case b; simpl; auto. + intros p1; rewrite Zmod_POS_correct; auto. + case (Zdiv_eucl_POS p (Zpos p1)); simpl; intros z1 z2; case z2; auto. + intros p1; rewrite Zmod_POS_correct; simpl; auto. + case (Zdiv_eucl_POS p (Zpos p1)); auto. +Qed. + + +(** Another convention is possible for division by negative numbers: + * quotient is always the biggest integer smaller than or equal to a/b + * remainder is hence always positive or null. *) + +Theorem Zdiv_eucl_extended : + forall b:Z, + b <> 0 -> + forall a:Z, + {qr : Z * Z | let (q, r) := qr in a = b * q + r /\ 0 <= r < Zabs b}. +Proof. + intros b Hb a. + elim (Z_le_gt_dec 0 b); intro Hb'. + cut (b > 0); [ intro Hb'' | omega ]. + rewrite Zabs_eq; [ apply Zdiv_eucl_exist; assumption | assumption ]. + cut (- b > 0); [ intro Hb'' | omega ]. + elim (Zdiv_eucl_exist Hb'' a); intros qr. + elim qr; intros q r Hqr. + exists (- q, r). + elim Hqr; intros. + split. + rewrite <- Zmult_opp_comm; assumption. + rewrite Zabs_non_eq; [ assumption | omega ]. +Qed. + +Implicit Arguments Zdiv_eucl_extended. + +(** A third convention: Ocaml. + + See files ZOdiv_def.v and ZOdiv.v. + + Ocaml uses Round-Toward-Zero division: (-a)/b = a/(-b) = -(a/b). + Hence (-a) mod b = - (a mod b) + a mod (-b) = a mod b + And: |r| < |b| and sgn(r) = sgn(a) (notice the a here instead of b). +*) diff --git a/theories/ZArith/Zeven.v b/theories/ZArith/Zeven.v index 6fab4461..4a402c61 100644 --- a/theories/ZArith/Zeven.v +++ b/theories/ZArith/Zeven.v @@ -6,10 +6,12 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: Zeven.v 9245 2006-10-17 12:53:34Z notin $ i*) +(*i $Id: Zeven.v 10291 2007-11-06 02:18:53Z letouzey $ i*) Require Import BinInt. +Open Scope Z_scope. + (*******************************************************************) (** About parity: even and odd predicates on Z, division by 2 on Z *) @@ -135,14 +137,14 @@ Hint Unfold Zeven Zodd: zarith. Definition Zdiv2 (z:Z) := match z with - | Z0 => 0%Z - | Zpos xH => 0%Z + | Z0 => 0 + | Zpos xH => 0 | Zpos p => Zpos (Pdiv2 p) - | Zneg xH => 0%Z + | Zneg xH => 0 | Zneg p => Zneg (Pdiv2 p) end. -Lemma Zeven_div2 : forall n:Z, Zeven n -> n = (2 * Zdiv2 n)%Z. +Lemma Zeven_div2 : forall n:Z, Zeven n -> n = 2 * Zdiv2 n. Proof. intro x; destruct x. auto with arith. @@ -154,27 +156,27 @@ Proof. intros. absurd (Zeven (-1)); red in |- *; auto with arith. Qed. -Lemma Zodd_div2 : forall n:Z, (n >= 0)%Z -> Zodd n -> n = (2 * Zdiv2 n + 1)%Z. +Lemma Zodd_div2 : forall n:Z, n >= 0 -> Zodd n -> n = 2 * Zdiv2 n + 1. Proof. intro x; destruct x. intros. absurd (Zodd 0); red in |- *; auto with arith. destruct p; auto with arith. intros. absurd (Zodd (Zpos (xO p))); red in |- *; auto with arith. - intros. absurd (Zneg p >= 0)%Z; red in |- *; auto with arith. + intros. absurd (Zneg p >= 0); red in |- *; auto with arith. Qed. Lemma Zodd_div2_neg : - forall n:Z, (n <= 0)%Z -> Zodd n -> n = (2 * Zdiv2 n - 1)%Z. + forall n:Z, n <= 0 -> Zodd n -> n = 2 * Zdiv2 n - 1. Proof. intro x; destruct x. intros. absurd (Zodd 0); red in |- *; auto with arith. - intros. absurd (Zneg p >= 0)%Z; red in |- *; auto with arith. + intros. absurd (Zneg p >= 0); red in |- *; auto with arith. destruct p; auto with arith. intros. absurd (Zodd (Zneg (xO p))); red in |- *; auto with arith. Qed. Lemma Z_modulo_2 : - forall n:Z, {y : Z | n = (2 * y)%Z} + {y : Z | n = (2 * y + 1)%Z}. + forall n:Z, {y : Z | n = 2 * y} + {y : Z | n = 2 * y + 1}. Proof. intros x. elim (Zeven_odd_dec x); intro. @@ -193,7 +195,7 @@ Qed. Lemma Zsplit2 : forall n:Z, {p : Z * Z | - let (x1, x2) := p in n = (x1 + x2)%Z /\ (x1 = x2 \/ x2 = (x1 + 1)%Z)}. + let (x1, x2) := p in n = x1 + x2 /\ (x1 = x2 \/ x2 = x1 + 1)}. Proof. intros x. elim (Z_modulo_2 x); intros [y Hy]; rewrite Zmult_comm in Hy; @@ -206,3 +208,109 @@ Proof. right; reflexivity. Qed. + +Theorem Zeven_ex: forall n, Zeven n -> exists m, n = 2 * m. +Proof. + intro n; exists (Zdiv2 n); apply Zeven_div2; auto. +Qed. + +Theorem Zodd_ex: forall n, Zodd n -> exists m, n = 2 * m + 1. +Proof. + destruct n; intros. + inversion H. + exists (Zdiv2 (Zpos p)). + apply Zodd_div2; simpl; auto; compute; inversion 1. + exists (Zdiv2 (Zneg p) - 1). + unfold Zminus. + rewrite Zmult_plus_distr_r. + rewrite <- Zplus_assoc. + assert (Zneg p <= 0) by (compute; inversion 1). + exact (Zodd_div2_neg _ H0 H). +Qed. + +Theorem Zeven_2p: forall p, Zeven (2 * p). +Proof. + destruct p; simpl; auto. +Qed. + +Theorem Zodd_2p_plus_1: forall p, Zodd (2 * p + 1). +Proof. + destruct p; simpl; auto. + destruct p; simpl; auto. +Qed. + +Theorem Zeven_plus_Zodd: forall a b, + Zeven a -> Zodd b -> Zodd (a + b). +Proof. + intros a b H1 H2; case Zeven_ex with (1 := H1); intros x H3; try rewrite H3; auto. + case Zodd_ex with (1 := H2); intros y H4; try rewrite H4; auto. + replace (2 * x + (2 * y + 1)) with (2 * (x + y) + 1); try apply Zodd_2p_plus_1; auto with zarith. + rewrite Zmult_plus_distr_r, Zplus_assoc; auto. +Qed. + +Theorem Zeven_plus_Zeven: forall a b, + Zeven a -> Zeven b -> Zeven (a + b). +Proof. + intros a b H1 H2; case Zeven_ex with (1 := H1); intros x H3; try rewrite H3; auto. + case Zeven_ex with (1 := H2); intros y H4; try rewrite H4; auto. + replace (2 * x + 2 * y) with (2 * (x + y)); try apply Zeven_2p; auto with zarith. + apply Zmult_plus_distr_r; auto. +Qed. + +Theorem Zodd_plus_Zeven: forall a b, + Zodd a -> Zeven b -> Zodd (a + b). +Proof. + intros a b H1 H2; rewrite Zplus_comm; apply Zeven_plus_Zodd; auto. +Qed. + +Theorem Zodd_plus_Zodd: forall a b, + Zodd a -> Zodd b -> Zeven (a + b). +Proof. + intros a b H1 H2; case Zodd_ex with (1 := H1); intros x H3; try rewrite H3; auto. + case Zodd_ex with (1 := H2); intros y H4; try rewrite H4; auto. + replace ((2 * x + 1) + (2 * y + 1)) with (2 * (x + y + 1)); try apply Zeven_2p; auto. + (* ring part *) + do 2 rewrite Zmult_plus_distr_r; auto. + repeat rewrite <- Zplus_assoc; f_equal. + rewrite (Zplus_comm 1). + repeat rewrite <- Zplus_assoc; auto. +Qed. + +Theorem Zeven_mult_Zeven_l: forall a b, + Zeven a -> Zeven (a * b). +Proof. + intros a b H1; case Zeven_ex with (1 := H1); intros x H3; try rewrite H3; auto. + replace (2 * x * b) with (2 * (x * b)); try apply Zeven_2p; auto with zarith. + (* ring part *) + apply Zmult_assoc. +Qed. + +Theorem Zeven_mult_Zeven_r: forall a b, + Zeven b -> Zeven (a * b). +Proof. + intros a b H1; case Zeven_ex with (1 := H1); intros x H3; try rewrite H3; auto. + replace (a * (2 * x)) with (2 * (x * a)); try apply Zeven_2p; auto. + (* ring part *) + rewrite (Zmult_comm x a). + do 2 rewrite Zmult_assoc. + rewrite (Zmult_comm 2 a); auto. +Qed. + +Hint Rewrite Zmult_plus_distr_r Zmult_plus_distr_l + Zplus_assoc Zmult_1_r Zmult_1_l : Zexpand. + +Theorem Zodd_mult_Zodd: forall a b, + Zodd a -> Zodd b -> Zodd (a * b). +Proof. + intros a b H1 H2; case Zodd_ex with (1 := H1); intros x H3; try rewrite H3; auto. + case Zodd_ex with (1 := H2); intros y H4; try rewrite H4; auto. + replace ((2 * x + 1) * (2 * y + 1)) with (2 * (2 * x * y + x + y) + 1); try apply Zodd_2p_plus_1; auto. + (* ring part *) + autorewrite with Zexpand; f_equal. + repeat rewrite <- Zplus_assoc; f_equal. + repeat rewrite <- Zmult_assoc; f_equal. + repeat rewrite Zmult_assoc; f_equal; apply Zmult_comm. +Qed. + +(* for compatibility *) +Close Scope Z_scope. diff --git a/theories/ZArith/Zgcd_alt.v b/theories/ZArith/Zgcd_alt.v new file mode 100644 index 00000000..286dd710 --- /dev/null +++ b/theories/ZArith/Zgcd_alt.v @@ -0,0 +1,317 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(*i $Id: Zgcd_alt.v 10997 2008-05-27 15:16:40Z letouzey $ i*) + +(** * Zgcd_alt : an alternate version of Zgcd, based on Euler's algorithm *) + +(** +Author: Pierre Letouzey +*) + +(** The alternate [Zgcd_alt] given here used to be the main [Zgcd] + function (see file [Znumtheory]), but this main [Zgcd] is now + based on a modern binary-efficient algorithm. This earlier + version, based on Euler's algorithm of iterated modulo, is kept + here due to both its intrinsic interest and its use as reference + point when proving gcd on Int31 numbers *) + +Require Import ZArith_base. +Require Import ZArithRing. +Require Import Zdiv. +Require Import Znumtheory. + +Open Scope Z_scope. + +(** In Coq, we need to control the number of iteration of modulo. + For that, we use an explicit measure in [nat], and we prove later + that using [2*d] is enough, where [d] is the number of binary + digits of the first argument. *) + + Fixpoint Zgcdn (n:nat) : Z -> Z -> Z := fun a b => + match n with + | O => 1 (* arbitrary, since n should be big enough *) + | S n => match a with + | Z0 => Zabs b + | Zpos _ => Zgcdn n (Zmod b a) a + | Zneg a => Zgcdn n (Zmod b (Zpos a)) (Zpos a) + end + end. + + Definition Zgcd_bound (a:Z) := + match a with + | Z0 => S O + | Zpos p => let n := Psize p in (n+n)%nat + | Zneg p => let n := Psize p in (n+n)%nat + end. + + Definition Zgcd_alt a b := Zgcdn (Zgcd_bound a) a b. + + (** A first obvious fact : [Zgcd a b] is positive. *) + + Lemma Zgcdn_pos : forall n a b, + 0 <= Zgcdn n a b. + Proof. + induction n. + simpl; auto with zarith. + destruct a; simpl; intros; auto with zarith; auto. + Qed. + + Lemma Zgcd_alt_pos : forall a b, 0 <= Zgcd_alt a b. + Proof. + intros; unfold Zgcd; apply Zgcdn_pos; auto. + Qed. + + (** We now prove that Zgcd is indeed a gcd. *) + + (** 1) We prove a weaker & easier bound. *) + + Lemma Zgcdn_linear_bound : forall n a b, + Zabs a < Z_of_nat n -> Zis_gcd a b (Zgcdn n a b). + Proof. + induction n. + simpl; intros. + elimtype False; generalize (Zabs_pos a); omega. + destruct a; intros; simpl; + [ generalize (Zis_gcd_0_abs b); intuition | | ]; + unfold Zmod; + generalize (Z_div_mod b (Zpos p) (refl_equal Gt)); + destruct (Zdiv_eucl b (Zpos p)) as (q,r); + intros (H0,H1); + rewrite inj_S in H; simpl Zabs in H; + (assert (H2: Zabs r < Z_of_nat n) by + (rewrite Zabs_eq; auto with zarith)); + assert (IH:=IHn r (Zpos p) H2); clear IHn; + simpl in IH |- *; + rewrite H0. + apply Zis_gcd_for_euclid2; auto. + apply Zis_gcd_minus; apply Zis_gcd_sym. + apply Zis_gcd_for_euclid2; auto. + Qed. + + (** 2) For Euclid's algorithm, the worst-case situation corresponds + to Fibonacci numbers. Let's define them: *) + + Fixpoint fibonacci (n:nat) : Z := + match n with + | O => 1 + | S O => 1 + | S (S n as p) => fibonacci p + fibonacci n + end. + + Lemma fibonacci_pos : forall n, 0 <= fibonacci n. + Proof. + cut (forall N n, (n<N)%nat -> 0<=fibonacci n). + eauto. + induction N. + inversion 1. + intros. + destruct n. + simpl; auto with zarith. + destruct n. + simpl; auto with zarith. + change (0 <= fibonacci (S n) + fibonacci n). + generalize (IHN n) (IHN (S n)); omega. + Qed. + + Lemma fibonacci_incr : + forall n m, (n<=m)%nat -> fibonacci n <= fibonacci m. + Proof. + induction 1. + auto with zarith. + apply Zle_trans with (fibonacci m); auto. + clear. + destruct m. + simpl; auto with zarith. + change (fibonacci (S m) <= fibonacci (S m)+fibonacci m). + generalize (fibonacci_pos m); omega. + Qed. + + (** 3) We prove that fibonacci numbers are indeed worst-case: + for a given number [n], if we reach a conclusion about [gcd(a,b)] in + exactly [n+1] loops, then [fibonacci (n+1)<=a /\ fibonacci(n+2)<=b] *) + + Lemma Zgcdn_worst_is_fibonacci : forall n a b, + 0 < a < b -> + Zis_gcd a b (Zgcdn (S n) a b) -> + Zgcdn n a b <> Zgcdn (S n) a b -> + fibonacci (S n) <= a /\ + fibonacci (S (S n)) <= b. + Proof. + induction n. + simpl; intros. + destruct a; omega. + intros. + destruct a; [simpl in *; omega| | destruct H; discriminate]. + revert H1; revert H0. + set (m:=S n) in *; (assert (m=S n) by auto); clearbody m. + pattern m at 2; rewrite H0. + simpl Zgcdn. + unfold Zmod; generalize (Z_div_mod b (Zpos p) (refl_equal Gt)). + destruct (Zdiv_eucl b (Zpos p)) as (q,r). + intros (H1,H2). + destruct H2. + destruct (Zle_lt_or_eq _ _ H2). + generalize (IHn _ _ (conj H4 H3)). + intros H5 H6 H7. + replace (fibonacci (S (S m))) with (fibonacci (S m) + fibonacci m) by auto. + assert (r = Zpos p * (-q) + b) by (rewrite H1; ring). + destruct H5; auto. + pattern r at 1; rewrite H8. + apply Zis_gcd_sym. + apply Zis_gcd_for_euclid2; auto. + apply Zis_gcd_sym; auto. + split; auto. + rewrite H1. + apply Zplus_le_compat; auto. + apply Zle_trans with (Zpos p * 1); auto. + ring_simplify (Zpos p * 1); auto. + apply Zmult_le_compat_l. + destruct q. + omega. + assert (0 < Zpos p0) by (compute; auto). + omega. + assert (Zpos p * Zneg p0 < 0) by (compute; auto). + omega. + compute; intros; discriminate. + (* r=0 *) + subst r. + simpl; rewrite H0. + intros. + simpl in H4. + simpl in H5. + destruct n. + simpl in H5. + simpl. + omega. + simpl in H5. + elim H5; auto. + Qed. + + (** 3b) We reformulate the previous result in a more positive way. *) + + Lemma Zgcdn_ok_before_fibonacci : forall n a b, + 0 < a < b -> a < fibonacci (S n) -> + Zis_gcd a b (Zgcdn n a b). + Proof. + destruct a; [ destruct 1; elimtype False; omega | | destruct 1; discriminate]. + cut (forall k n b, + k = (S (nat_of_P p) - n)%nat -> + 0 < Zpos p < b -> Zpos p < fibonacci (S n) -> + Zis_gcd (Zpos p) b (Zgcdn n (Zpos p) b)). + destruct 2; eauto. + clear n; induction k. + intros. + assert (nat_of_P p < n)%nat by omega. + apply Zgcdn_linear_bound. + simpl. + generalize (inj_le _ _ H2). + rewrite inj_S. + rewrite <- Zpos_eq_Z_of_nat_o_nat_of_P; auto. + omega. + intros. + generalize (Zgcdn_worst_is_fibonacci n (Zpos p) b H0); intros. + assert (Zis_gcd (Zpos p) b (Zgcdn (S n) (Zpos p) b)). + apply IHk; auto. + omega. + replace (fibonacci (S (S n))) with (fibonacci (S n)+fibonacci n) by auto. + generalize (fibonacci_pos n); omega. + replace (Zgcdn n (Zpos p) b) with (Zgcdn (S n) (Zpos p) b); auto. + generalize (H2 H3); clear H2 H3; omega. + Qed. + + (** 4) The proposed bound leads to a fibonacci number that is big enough. *) + + Lemma Zgcd_bound_fibonacci : + forall a, 0 < a -> a < fibonacci (Zgcd_bound a). + Proof. + destruct a; [omega| | intro H; discriminate]. + intros _. + induction p; [ | | compute; auto ]; + simpl Zgcd_bound in *; + rewrite plus_comm; simpl plus; + set (n:= (Psize p+Psize p)%nat) in *; simpl; + assert (n <> O) by (unfold n; destruct p; simpl; auto). + + destruct n as [ |m]; [elim H; auto| ]. + generalize (fibonacci_pos m); rewrite Zpos_xI; omega. + + destruct n as [ |m]; [elim H; auto| ]. + generalize (fibonacci_pos m); rewrite Zpos_xO; omega. + Qed. + + (* 5) the end: we glue everything together and take care of + situations not corresponding to [0<a<b]. *) + + Lemma Zgcdn_is_gcd : + forall n a b, (Zgcd_bound a <= n)%nat -> + Zis_gcd a b (Zgcdn n a b). + Proof. + destruct a; intros. + simpl in H. + destruct n; [elimtype False; omega | ]. + simpl; generalize (Zis_gcd_0_abs b); intuition. + (*Zpos*) + generalize (Zgcd_bound_fibonacci (Zpos p)). + simpl Zgcd_bound in *. + remember (Psize p+Psize p)%nat as m. + assert (1 < m)%nat. + rewrite Heqm; destruct p; simpl; rewrite 1? plus_comm; + auto with arith. + destruct m as [ |m]; [inversion H0; auto| ]. + destruct n as [ |n]; [inversion H; auto| ]. + simpl Zgcdn. + unfold Zmod. + generalize (Z_div_mod b (Zpos p) (refl_equal Gt)). + destruct (Zdiv_eucl b (Zpos p)) as (q,r). + intros (H2,H3) H4. + rewrite H2. + apply Zis_gcd_for_euclid2. + destruct H3. + destruct (Zle_lt_or_eq _ _ H1). + apply Zgcdn_ok_before_fibonacci; auto. + apply Zlt_le_trans with (fibonacci (S m)); [ omega | apply fibonacci_incr; auto]. + subst r; simpl. + destruct m as [ |m]; [elimtype False; omega| ]. + destruct n as [ |n]; [elimtype False; omega| ]. + simpl; apply Zis_gcd_sym; apply Zis_gcd_0. + (*Zneg*) + generalize (Zgcd_bound_fibonacci (Zpos p)). + simpl Zgcd_bound in *. + remember (Psize p+Psize p)%nat as m. + assert (1 < m)%nat. + rewrite Heqm; destruct p; simpl; rewrite 1? plus_comm; + auto with arith. + destruct m as [ |m]; [inversion H0; auto| ]. + destruct n as [ |n]; [inversion H; auto| ]. + simpl Zgcdn. + unfold Zmod. + generalize (Z_div_mod b (Zpos p) (refl_equal Gt)). + destruct (Zdiv_eucl b (Zpos p)) as (q,r). + intros (H1,H2) H3. + rewrite H1. + apply Zis_gcd_minus. + apply Zis_gcd_sym. + apply Zis_gcd_for_euclid2. + destruct H2. + destruct (Zle_lt_or_eq _ _ H2). + apply Zgcdn_ok_before_fibonacci; auto. + apply Zlt_le_trans with (fibonacci (S m)); [ omega | apply fibonacci_incr; auto]. + subst r; simpl. + destruct m as [ |m]; [elimtype False; omega| ]. + destruct n as [ |n]; [elimtype False; omega| ]. + simpl; apply Zis_gcd_sym; apply Zis_gcd_0. + Qed. + + Lemma Zgcd_is_gcd : + forall a b, Zis_gcd a b (Zgcd_alt a b). + Proof. + unfold Zgcd_alt; intros; apply Zgcdn_is_gcd; auto. + Qed. + + diff --git a/theories/ZArith/Zmax.v b/theories/ZArith/Zmax.v index 8af9b891..0d6fc94a 100644 --- a/theories/ZArith/Zmax.v +++ b/theories/ZArith/Zmax.v @@ -5,7 +5,7 @@ (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: Zmax.v 9302 2006-10-27 21:21:17Z barras $ i*) +(*i $Id: Zmax.v 10291 2007-11-06 02:18:53Z letouzey $ i*) Require Import Arith_base. Require Import BinInt. @@ -38,6 +38,28 @@ Proof. destruct (n ?= m); (apply H1|| apply H2); discriminate. Qed. +Lemma Zmax_spec : forall x y:Z, + x >= y /\ Zmax x y = x \/ + x < y /\ Zmax x y = y. +Proof. + intros; unfold Zmax, Zlt, Zge. + destruct (Zcompare x y); [ left | right | left ]; split; auto; discriminate. +Qed. + +Lemma Zmax_left : forall n m:Z, n>=m -> Zmax n m = n. +Proof. + intros n m; unfold Zmax, Zge; destruct (n ?= m); auto. + intro H; elim H; auto. +Qed. + +Lemma Zmax_right : forall n m:Z, n<=m -> Zmax n m = m. +Proof. + intros n m; unfold Zmax, Zle. + generalize (Zcompare_Eq_eq n m). + destruct (n ?= m); auto. + intros _ H; elim H; auto. +Qed. + (** * Least upper bound properties of max *) Lemma Zle_max_l : forall n m:Z, n <= Zmax n m. @@ -106,3 +128,39 @@ Proof. rewrite (Zcompare_plus_compat x y n). case (x ?= y); apply Zplus_comm. Qed. + +(** * Maximum and Zpos *) + +Lemma Zpos_max : forall p q, Zpos (Pmax p q) = Zmax (Zpos p) (Zpos q). +Proof. + intros; unfold Zmax, Pmax; simpl; generalize (Pcompare_Eq_eq p q). + destruct Pcompare; auto. + intro H; rewrite H; auto. +Qed. + +Lemma Zpos_max_1 : forall p, Zmax 1 (Zpos p) = Zpos p. +Proof. + intros; unfold Zmax; simpl; destruct p; simpl; auto. +Qed. + +(** * Characterization of Pminus in term of Zminus and Zmax *) + +Lemma Zpos_minus : forall p q, Zpos (Pminus p q) = Zmax 1 (Zpos p - Zpos q). +Proof. + intros. + case_eq (Pcompare p q Eq). + intros H; rewrite (Pcompare_Eq_eq _ _ H). + rewrite Zminus_diag. + unfold Zmax; simpl. + unfold Pminus; rewrite Pminus_mask_diag; auto. + intros; rewrite Pminus_Lt; auto. + destruct (Zmax_spec 1 (Zpos p - Zpos q)) as [(H1,H2)|(H1,H2)]; auto. + elimtype False; clear H2. + assert (H1':=Zlt_trans 0 1 _ Zlt_0_1 H1). + generalize (Zlt_0_minus_lt _ _ H1'). + unfold Zlt; simpl. + rewrite (ZC2 _ _ H); intro; discriminate. + intros; simpl; rewrite H. + symmetry; apply Zpos_max_1. +Qed. + diff --git a/theories/ZArith/Zmin.v b/theories/ZArith/Zmin.v index 37d78a74..bad40a32 100644 --- a/theories/ZArith/Zmin.v +++ b/theories/ZArith/Zmin.v @@ -5,9 +5,9 @@ (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: Zmin.v 9302 2006-10-27 21:21:17Z barras $ i*) +(*i $Id: Zmin.v 10028 2007-07-18 22:38:06Z letouzey $ i*) -(** Initial version from Pierre Crégut (CNET, Lannion, France), 1996. +(** Initial version from Pierre Crégut (CNET, Lannion, France), 1996. Further extensions by the Coq development team, with suggestions from Russell O'Connor (Radbout U., Nijmegen, The Netherlands). *) @@ -43,6 +43,14 @@ Proof. intros n m P H1 H2; unfold Zmin in |- *; case (n ?= m); auto with arith. Qed. +Lemma Zmin_spec : forall x y:Z, + x <= y /\ Zmin x y = x \/ + x > y /\ Zmin x y = y. +Proof. + intros; unfold Zmin, Zle, Zgt. + destruct (Zcompare x y); [ left | left | right ]; split; auto; discriminate. +Qed. + (** * Greatest lower bound properties of min *) Lemma Zle_min_l : forall n m:Z, Zmin n m <= n. @@ -128,3 +136,11 @@ Proof. Qed. Notation Zmin_plus := Zplus_min_distr_r (only parsing). + +(** * Minimum and Zpos *) + +Lemma Zpos_min : forall p q, Zpos (Pmin p q) = Zmin (Zpos p) (Zpos q). +Proof. + intros; unfold Zmin, Pmin; simpl; destruct Pcompare; auto. +Qed. + diff --git a/theories/ZArith/Zmisc.v b/theories/ZArith/Zmisc.v index d01cada6..0634096e 100644 --- a/theories/ZArith/Zmisc.v +++ b/theories/ZArith/Zmisc.v @@ -6,8 +6,9 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: Zmisc.v 9245 2006-10-17 12:53:34Z notin $ i*) +(*i $Id: Zmisc.v 11072 2008-06-08 16:13:37Z herbelin $ i*) +Require Import Wf_nat. Require Import BinInt. Require Import Zcompare. Require Import Zorder. @@ -18,37 +19,23 @@ Open Local Scope Z_scope. (** Iterators *) (** [n]th iteration of the function [f] *) -Fixpoint iter_nat (n:nat) (A:Set) (f:A -> A) (x:A) {struct n} : A := - match n with - | O => x - | S n' => f (iter_nat n' A f x) - end. -Fixpoint iter_pos (n:positive) (A:Set) (f:A -> A) (x:A) {struct n} : A := +Fixpoint iter_pos (n:positive) (A:Type) (f:A -> A) (x:A) {struct n} : A := match n with | xH => f x | xO n' => iter_pos n' A f (iter_pos n' A f x) | xI n' => f (iter_pos n' A f (iter_pos n' A f x)) end. -Definition iter (n:Z) (A:Set) (f:A -> A) (x:A) := +Definition iter (n:Z) (A:Type) (f:A -> A) (x:A) := match n with | Z0 => x | Zpos p => iter_pos p A f x | Zneg p => x end. -Theorem iter_nat_plus : - forall (n m:nat) (A:Set) (f:A -> A) (x:A), - iter_nat (n + m) A f x = iter_nat n A f (iter_nat m A f x). -Proof. - simple induction n; - [ simpl in |- *; auto with arith - | intros; simpl in |- *; apply f_equal with (f := f); apply H ]. -Qed. - Theorem iter_nat_of_P : - forall (p:positive) (A:Set) (f:A -> A) (x:A), + forall (p:positive) (A:Type) (f:A -> A) (x:A), iter_pos p A f x = iter_nat (nat_of_P p) A f x. Proof. intro n; induction n as [p H| p H| ]; @@ -63,7 +50,7 @@ Proof. Qed. Theorem iter_pos_plus : - forall (p q:positive) (A:Set) (f:A -> A) (x:A), + forall (p q:positive) (A:Type) (f:A -> A) (x:A), iter_pos (p + q) A f x = iter_pos p A f (iter_pos q A f x). Proof. intros n m; intros. @@ -78,7 +65,7 @@ Qed. then the iterates of [f] also preserve it. *) Theorem iter_nat_invariant : - forall (n:nat) (A:Set) (f:A -> A) (Inv:A -> Prop), + forall (n:nat) (A:Type) (f:A -> A) (Inv:A -> Prop), (forall x:A, Inv x -> Inv (f x)) -> forall x:A, Inv x -> Inv (iter_nat n A f x). Proof. @@ -89,7 +76,7 @@ Proof. Qed. Theorem iter_pos_invariant : - forall (p:positive) (A:Set) (f:A -> A) (Inv:A -> Prop), + forall (p:positive) (A:Type) (f:A -> A) (Inv:A -> Prop), (forall x:A, Inv x -> Inv (f x)) -> forall x:A, Inv x -> Inv (iter_pos p A f x). Proof. diff --git a/theories/ZArith/Znat.v b/theories/ZArith/Znat.v index f0a3d47b..c5b5edc1 100644 --- a/theories/ZArith/Znat.v +++ b/theories/ZArith/Znat.v @@ -6,9 +6,9 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: Znat.v 9302 2006-10-27 21:21:17Z barras $ i*) +(*i $Id: Znat.v 10726 2008-03-28 18:15:23Z notin $ i*) -(** Binary Integers (Pierre Crégut, CNET, Lannion, France) *) +(** Binary Integers (Pierre Crégut, CNET, Lannion, France) *) Require Export Arith_base. Require Import BinPos. @@ -17,6 +17,7 @@ Require Import Zcompare. Require Import Zorder. Require Import Decidable. Require Import Peano_dec. +Require Import Min Max Zmin Zmax. Require Export Compare_dec. Open Local Scope Z_scope. @@ -26,6 +27,13 @@ Definition neq (x y:nat) := x <> y. (************************************************) (** Properties of the injection from nat into Z *) +(** Injection and successor *) + +Theorem inj_0 : Z_of_nat 0 = 0%Z. +Proof. + reflexivity. +Qed. + Theorem inj_S : forall n:nat, Z_of_nat (S n) = Zsucc (Z_of_nat n). Proof. intro y; induction y as [| n H]; @@ -33,25 +41,12 @@ Proof. | change (Zpos (Psucc (P_of_succ_nat n)) = Zsucc (Z_of_nat (S n))) in |- *; rewrite Zpos_succ_morphism; trivial with arith ]. Qed. - -Theorem inj_plus : forall n m:nat, Z_of_nat (n + m) = Z_of_nat n + Z_of_nat m. -Proof. - intro x; induction x as [| n H]; intro y; destruct y as [| m]; - [ simpl in |- *; trivial with arith - | simpl in |- *; trivial with arith - | simpl in |- *; rewrite <- plus_n_O; trivial with arith - | change (Z_of_nat (S (n + S m)) = Z_of_nat (S n) + Z_of_nat (S m)) in |- *; - rewrite inj_S; rewrite H; do 2 rewrite inj_S; rewrite Zplus_succ_l; - trivial with arith ]. -Qed. -Theorem inj_mult : forall n m:nat, Z_of_nat (n * m) = Z_of_nat n * Z_of_nat m. +(** Injection and equality. *) + +Theorem inj_eq : forall n m:nat, n = m -> Z_of_nat n = Z_of_nat m. Proof. - intro x; induction x as [| n H]; - [ simpl in |- *; trivial with arith - | intro y; rewrite inj_S; rewrite <- Zmult_succ_l_reverse; rewrite <- H; - rewrite <- inj_plus; simpl in |- *; rewrite plus_comm; - trivial with arith ]. + intros x y H; rewrite H; trivial with arith. Qed. Theorem inj_neq : forall n m:nat, neq n m -> Zne (Z_of_nat n) (Z_of_nat m). @@ -66,6 +61,24 @@ Proof. intros E; rewrite E; auto with arith ]. Qed. +Theorem inj_eq_rev : forall n m:nat, Z_of_nat n = Z_of_nat m -> n = m. +Proof. + intros x y H. + destruct (eq_nat_dec x y) as [H'|H']; auto. + elimtype False. + exact (inj_neq _ _ H' H). +Qed. + +Theorem inj_eq_iff : forall n m:nat, n=m <-> Z_of_nat n = Z_of_nat m. +Proof. + split; [apply inj_eq | apply inj_eq_rev]. +Qed. + + +(** Injection and order relations: *) + +(** One way ... *) + Theorem inj_le : forall n m:nat, (n <= m)%nat -> Z_of_nat n <= Z_of_nat m. Proof. intros x y; intros H; elim H; @@ -81,29 +94,100 @@ Proof. exact H. Qed. +Theorem inj_ge : forall n m:nat, (n >= m)%nat -> Z_of_nat n >= Z_of_nat m. +Proof. + intros x y H; apply Zle_ge; apply inj_le; apply H. +Qed. + Theorem inj_gt : forall n m:nat, (n > m)%nat -> Z_of_nat n > Z_of_nat m. Proof. intros x y H; apply Zlt_gt; apply inj_lt; exact H. Qed. -Theorem inj_ge : forall n m:nat, (n >= m)%nat -> Z_of_nat n >= Z_of_nat m. +(** The other way ... *) + +Theorem inj_le_rev : forall n m:nat, Z_of_nat n <= Z_of_nat m -> (n <= m)%nat. Proof. - intros x y H; apply Zle_ge; apply inj_le; apply H. + intros x y H. + destruct (le_lt_dec x y) as [H0|H0]; auto. + elimtype False. + assert (H1:=inj_lt _ _ H0). + red in H; red in H1. + rewrite <- Zcompare_antisym in H; rewrite H1 in H; auto. Qed. -Theorem inj_eq : forall n m:nat, n = m -> Z_of_nat n = Z_of_nat m. +Theorem inj_lt_rev : forall n m:nat, Z_of_nat n < Z_of_nat m -> (n < m)%nat. Proof. - intros x y H; rewrite H; trivial with arith. + intros x y H. + destruct (le_lt_dec y x) as [H0|H0]; auto. + elimtype False. + assert (H1:=inj_le _ _ H0). + red in H; red in H1. + rewrite <- Zcompare_antisym in H1; rewrite H in H1; auto. Qed. -Theorem intro_Z : - forall n:nat, exists y : Z, Z_of_nat n = y /\ 0 <= y * 1 + 0. +Theorem inj_ge_rev : forall n m:nat, Z_of_nat n >= Z_of_nat m -> (n >= m)%nat. Proof. - intros x; exists (Z_of_nat x); split; - [ trivial with arith - | rewrite Zmult_comm; rewrite Zmult_1_l; rewrite Zplus_0_r; - unfold Zle in |- *; elim x; intros; simpl in |- *; - discriminate ]. + intros x y H. + destruct (le_lt_dec y x) as [H0|H0]; auto. + elimtype False. + assert (H1:=inj_gt _ _ H0). + red in H; red in H1. + rewrite <- Zcompare_antisym in H; rewrite H1 in H; auto. +Qed. + +Theorem inj_gt_rev : forall n m:nat, Z_of_nat n > Z_of_nat m -> (n > m)%nat. +Proof. + intros x y H. + destruct (le_lt_dec x y) as [H0|H0]; auto. + elimtype False. + assert (H1:=inj_ge _ _ H0). + red in H; red in H1. + rewrite <- Zcompare_antisym in H1; rewrite H in H1; auto. +Qed. + +(* Both ways ... *) + +Theorem inj_le_iff : forall n m:nat, (n<=m)%nat <-> Z_of_nat n <= Z_of_nat m. +Proof. + split; [apply inj_le | apply inj_le_rev]. +Qed. + +Theorem inj_lt_iff : forall n m:nat, (n<m)%nat <-> Z_of_nat n < Z_of_nat m. +Proof. + split; [apply inj_lt | apply inj_lt_rev]. +Qed. + +Theorem inj_ge_iff : forall n m:nat, (n>=m)%nat <-> Z_of_nat n >= Z_of_nat m. +Proof. + split; [apply inj_ge | apply inj_ge_rev]. +Qed. + +Theorem inj_gt_iff : forall n m:nat, (n>m)%nat <-> Z_of_nat n > Z_of_nat m. +Proof. + split; [apply inj_gt | apply inj_gt_rev]. +Qed. + +(** Injection and usual operations *) + +Theorem inj_plus : forall n m:nat, Z_of_nat (n + m) = Z_of_nat n + Z_of_nat m. +Proof. + intro x; induction x as [| n H]; intro y; destruct y as [| m]; + [ simpl in |- *; trivial with arith + | simpl in |- *; trivial with arith + | simpl in |- *; rewrite <- plus_n_O; trivial with arith + | change (Z_of_nat (S (n + S m)) = Z_of_nat (S n) + Z_of_nat (S m)) in |- *; + rewrite inj_S; rewrite H; do 2 rewrite inj_S; rewrite Zplus_succ_l; + trivial with arith ]. +Qed. + +Theorem inj_mult : forall n m:nat, Z_of_nat (n * m) = Z_of_nat n * Z_of_nat m. +Proof. + intro x; induction x as [| n H]; + [ simpl in |- *; trivial with arith + | intro y; rewrite inj_S; rewrite <- Zmult_succ_l_reverse; rewrite <- H; + rewrite <- inj_plus; simpl in |- *; rewrite plus_comm; + trivial with arith ]. Qed. Theorem inj_minus1 : @@ -121,6 +205,46 @@ Proof. [ trivial with arith | apply gt_not_le; assumption ]. Qed. +Theorem inj_minus : forall n m:nat, + Z_of_nat (minus n m) = Zmax 0 (Z_of_nat n - Z_of_nat m). +Proof. + intros. + rewrite Zmax_comm. + unfold Zmax. + destruct (le_lt_dec m n) as [H|H]. + + rewrite (inj_minus1 _ _ H). + assert (H':=Zle_minus_le_0 _ _ (inj_le _ _ H)). + unfold Zle in H'. + rewrite <- Zcompare_antisym in H'. + destruct Zcompare; simpl in *; intuition. + + rewrite (inj_minus2 _ _ H). + assert (H':=Zplus_lt_compat_r _ _ (- Z_of_nat m) (inj_lt _ _ H)). + rewrite Zplus_opp_r in H'. + unfold Zminus; rewrite H'; auto. +Qed. + +Theorem inj_min : forall n m:nat, + Z_of_nat (min n m) = Zmin (Z_of_nat n) (Z_of_nat m). +Proof. + induction n; destruct m; try (compute; auto; fail). + simpl min. + do 3 rewrite inj_S. + rewrite <- Zsucc_min_distr; f_equal; auto. +Qed. + +Theorem inj_max : forall n m:nat, + Z_of_nat (max n m) = Zmax (Z_of_nat n) (Z_of_nat m). +Proof. + induction n; destruct m; try (compute; auto; fail). + simpl max. + do 3 rewrite inj_S. + rewrite <- Zsucc_max_distr; f_equal; auto. +Qed. + +(** Composition of injections **) + Theorem Zpos_eq_Z_of_nat_o_nat_of_P : forall p:positive, Zpos p = Z_of_nat (nat_of_P p). Proof. @@ -136,3 +260,26 @@ Proof. rewrite inj_plus; repeat rewrite <- H. rewrite Zpos_xO; simpl in |- *; rewrite Pplus_diag; reflexivity. Qed. + +(** Misc *) + +Theorem intro_Z : + forall n:nat, exists y : Z, Z_of_nat n = y /\ 0 <= y * 1 + 0. +Proof. + intros x; exists (Z_of_nat x); split; + [ trivial with arith + | rewrite Zmult_comm; rewrite Zmult_1_l; rewrite Zplus_0_r; + unfold Zle in |- *; elim x; intros; simpl in |- *; + discriminate ]. +Qed. + +Lemma Zpos_P_of_succ_nat : forall n:nat, + Zpos (P_of_succ_nat n) = Zsucc (Z_of_nat n). +Proof. + intros. + unfold Z_of_nat. + destruct n. + simpl; auto. + simpl (P_of_succ_nat (S n)). + apply Zpos_succ_morphism. +Qed. diff --git a/theories/ZArith/Znumtheory.v b/theories/ZArith/Znumtheory.v index d89ec052..e77475e0 100644 --- a/theories/ZArith/Znumtheory.v +++ b/theories/ZArith/Znumtheory.v @@ -6,13 +6,12 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: Znumtheory.v 9245 2006-10-17 12:53:34Z notin $ i*) +(*i $Id: Znumtheory.v 10295 2007-11-06 22:46:21Z letouzey $ i*) Require Import ZArith_base. Require Import ZArithRing. Require Import Zcomplements. Require Import Zdiv. -Require Import Ndigits. Require Import Wf_nat. Open Local Scope Z_scope. @@ -156,21 +155,27 @@ Qed. 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. + 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. (** If [a] divides [b] and [b<>0] then [|a| <= |b|]. *) @@ -194,6 +199,134 @@ Proof. subst q; omega. Qed. +(** [Zdivide] can be expressed using [Zmod]. *) + +Lemma Zmod_divide : forall a b:Z, b > 0 -> a mod b = 0 -> (b | a). +Proof. + intros a b H H0. + apply Zdivide_intro with (a / b). + pattern a at 1 in |- *; rewrite (Z_div_mod_eq a b H). + rewrite H0; ring. +Qed. + +Lemma Zdivide_mod : forall a b:Z, b > 0 -> (b | a) -> a mod b = 0. +Proof. + intros a b; simple destruct 2; intros; subst. + change (q * b) with (0 + q * b) in |- *. + rewrite Z_mod_plus; auto. +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). +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. + +Theorem Zdivide_Zabs_l: forall a b, (Zabs a | b) -> (a | b). +Proof. + intros a b [x H]; subst b. + pattern (Zabs a); apply Zabs_intro. + exists (- x); ring. + exists x; ring. +Qed. + +Theorem Zdivide_Zabs_inv_l: forall a b, (a | b) -> (Zabs a | b). +Proof. + intros a b [x H]; subst b. + pattern (Zabs a); apply Zabs_intro. + exists (- x); ring. + exists x; ring. +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. +Qed. + +Theorem Zdivide_Zdiv_lt_pos: forall a b : Z, + 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. + 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. +Qed. + +Lemma Zmod_div_mod: forall 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. +Qed. + +Lemma Zmod_divide_minus: forall a b c : Z, 0 < b -> + a mod b = c -> (b | a - c). +Proof. + intros a b c H H1; apply Zmod_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. +Qed. + +Lemma Zdivide_mod_minus: forall a b c : Z, 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. + 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. +Qed. + (** * Greatest common divisor (gcd). *) (** There is no unicity of the gcd; hence we define the predicate [gcd a b d] @@ -246,6 +379,18 @@ Proof. Qed. Hint Resolve Zis_gcd_sym Zis_gcd_0 Zis_gcd_minus Zis_gcd_opp: zarith. + +Theorem Zis_gcd_unique: forall a b c d : Z, + Zis_gcd a b c -> Zis_gcd a b d -> c = d \/ c = (- d). +Proof. +intros a b c d H1 H2. +inversion_clear H1 as [Hc1 Hc2 Hc3]. +inversion_clear H2 as [Hd1 Hd2 Hd3]. +assert (H3: Zdivide c d); auto. +assert (H4: Zdivide d c); auto. +apply Zdivide_antisym; auto. +Qed. + (** * Extended Euclid algorithm. *) @@ -463,6 +608,7 @@ Qed. 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. @@ -491,6 +637,68 @@ Lemma Zis_gcd_rel_prime : exists q; auto with zarith. Qed. +Theorem rel_prime_sym: forall a b, rel_prime a b -> rel_prime b a. +Proof. + intros a b H; auto with zarith. + red; apply Zis_gcd_sym; auto with zarith. +Qed. + +Theorem rel_prime_div: forall p q r, + rel_prime p q -> (r | p) -> rel_prime r q. +Proof. + intros p q r H (u, H1); subst. + inversion_clear H as [H1 H2 H3]. + red; apply Zis_gcd_intro; try apply Zone_divide. + intros x H4 H5; apply H3; auto. + apply Zdivide_mult_r; auto. +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. +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. + case (Zis_gcd_unique 0 n n 1); auto. + apply Zis_gcd_intro; auto. + exists 0; auto with zarith. + exists 1; auto with zarith. +Qed. + +Theorem rel_prime_mod: forall p q, 0 < q -> + rel_prime p q -> rel_prime (p mod q) q. +Proof. + intros p q H H0. + assert (H1: Bezout p q 1). + apply rel_prime_bezout; auto. + inversion_clear H1 as [q1 r1 H2]. + 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. +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. +Qed. + +Theorem Zrel_prime_neq_mod_0: forall a b, 1 < b -> rel_prime a b -> a mod b <> 0. +Proof. + intros a b H H1 H2. + case (not_rel_prime_0 _ H). + rewrite <- H2. + apply rel_prime_mod; auto with zarith. +Qed. + (** * Primality *) Inductive prime (p:Z) : Prop := @@ -543,42 +751,19 @@ Qed. Hint Resolve prime_rel_prime: zarith. -(** [Zdivide] can be expressed using [Zmod]. *) +(** As a consequence, a prime number is relatively prime with smaller numbers *) -Lemma Zmod_divide : forall a b:Z, b > 0 -> a mod b = 0 -> (b | a). +Theorem rel_prime_le_prime: + forall a p, prime p -> 1 <= a < p -> rel_prime a p. Proof. - intros a b H H0. - apply Zdivide_intro with (a / b). - pattern a at 1 in |- *; rewrite (Z_div_mod_eq a b H). - rewrite H0; ring. + intros a p Hp [H1 H2]. + apply rel_prime_sym; apply prime_rel_prime; auto. + intros [q Hq]; subst a. + case (Zle_or_lt q 0); intros Hl. + absurd (q * p <= 0 * p); auto with zarith. + absurd (1 * p <= q * p); auto with zarith. Qed. -Lemma Zdivide_mod : forall a b:Z, b > 0 -> (b | a) -> a mod b = 0. -Proof. - intros a b; simple destruct 2; intros; subst. - change (q * b) with (0 + q * b) in |- *. - rewrite Z_mod_plus; auto. -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. (** If a prime [p] divides [ab] then it divides either [a] or [b] *) @@ -590,6 +775,108 @@ Proof. right; apply Gauss with a; auto with zarith. Qed. +Lemma not_prime_0: ~ prime 0. +Proof. + intros H1; case (prime_divisors _ H1 2); auto with zarith. +Qed. + +Lemma not_prime_1: ~ prime 1. +Proof. + intros H1; absurd (1 < 1); auto with zarith. + inversion H1; auto. +Qed. + +Lemma prime_2: prime 2. +Proof. + apply prime_intro; auto with zarith. + intros n [H1 H2]; case Zle_lt_or_eq with ( 1 := H1 ); auto with zarith; + clear H1; intros H1. + contradict H2; auto with zarith. + subst n; red; auto with zarith. + apply Zis_gcd_intro; auto with zarith. +Qed. + +Theorem prime_3: prime 3. +Proof. + apply prime_intro; auto with zarith. + intros n [H1 H2]; case Zle_lt_or_eq with ( 1 := H1 ); auto with zarith; + clear H1; intros H1. + case (Zle_lt_or_eq 2 n); auto with zarith; clear H1; intros H1. + contradict H2; auto with zarith. + subst n; red; auto with zarith. + apply Zis_gcd_intro; auto with zarith. + intros x [q1 Hq1] [q2 Hq2]. + exists (q2 - q1). + apply trans_equal with (3 - 2); auto with zarith. + rewrite Hq1; rewrite Hq2; ring. + subst n; red; auto with zarith. + apply Zis_gcd_intro; auto with zarith. +Qed. + +Theorem prime_ge_2: forall p, prime p -> 2 <= p. +Proof. + intros p Hp; inversion Hp; auto with zarith. +Qed. + +Definition prime' p := 1<p /\ (forall n, 1<n<p -> ~ (n|p)). + +Theorem prime_alt: + forall p, prime' p <-> prime p. +Proof. + split; destruct 1; intros. + (* prime -> prime' *) + constructor; auto; intros. + red; apply Zis_gcd_intro; auto with zarith; intros. + case (Zle_lt_or_eq 0 (Zabs x)); auto with zarith; intros H6. + case (Zle_lt_or_eq 1 (Zabs x)); auto with zarith; intros H7. + case (Zle_lt_or_eq (Zabs x) p); auto with zarith. + apply Zdivide_le; auto with zarith. + apply Zdivide_Zabs_inv_l; auto. + intros H8; case (H0 (Zabs x)); auto. + apply Zdivide_Zabs_inv_l; auto. + intros H8; subst p; absurd (Zabs x <= n); auto with zarith. + apply Zdivide_le; auto with zarith. + apply Zdivide_Zabs_inv_l; auto. + rewrite H7; pattern (Zabs x); apply Zabs_intro; auto with zarith. + absurd (0%Z = p); auto with zarith. + assert (x=0) by (destruct x; simpl in *; now auto). + subst x; elim H3; intro q; rewrite Zmult_0_r; auto. + (* prime' -> prime *) + split; auto; intros. + intros H2. + case (Zis_gcd_unique n p n 1); auto with zarith. + apply Zis_gcd_intro; auto with zarith. + apply H0; auto with zarith. +Qed. + +Theorem square_not_prime: forall a, ~ prime (a * a). +Proof. + intros a Ha. + rewrite <- (Zabs_square a) in Ha. + assert (0 <= Zabs a) by auto with zarith. + set (b:=Zabs a) in *; clearbody b. + rewrite <- prime_alt in Ha; destruct Ha. + case (Zle_lt_or_eq 0 b); auto with zarith; intros Hza1; [ | subst; omega]. + case (Zle_lt_or_eq 1 b); auto with zarith; intros Hza2; [ | subst; omega]. + assert (Hza3 := Zmult_lt_compat_r 1 b b Hza1 Hza2). + rewrite Zmult_1_l in Hza3. + elim (H1 _ (conj Hza2 Hza3)). + exists b; auto. +Qed. + +Theorem prime_div_prime: forall p q, + prime p -> prime q -> (p | q) -> p = q. +Proof. + intros p q H H1 H2; + assert (Hp: 0 < p); try apply Zlt_le_trans with 2; try apply prime_ge_2; auto with zarith. + assert (Hq: 0 < q); try apply Zlt_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. +Qed. + (** We could obtain a [Zgcd] function via Euclid algorithm. But we propose here a binary version of [Zgcd], faster and executable within Coq. @@ -617,105 +904,34 @@ Fixpoint Pgcdn (n: nat) (a b : positive) { struct n } : positive := | xO a, xO b => xO (Pgcdn n a b) | a, xO b => Pgcdn n a b | xO a, b => Pgcdn n a b - | xI a', xI b' => match Pcompare a' b' Eq with - | Eq => a - | Lt => Pgcdn n (b'-a') a - | Gt => Pgcdn n (a'-b') b - end - end - end. - -Fixpoint Pggcdn (n: nat) (a b : positive) { struct n } : (positive*(positive*positive)) := - match n with - | O => (1,(a,b)) - | S n => - match a,b with - | xH, b => (1,(1,b)) - | a, xH => (1,(a,1)) - | xO a, xO b => - let (g,p) := Pggcdn n a b in - (xO g,p) - | a, xO b => - let (g,p) := Pggcdn n a b in - let (aa,bb) := p in - (g,(aa, xO bb)) - | xO a, b => - let (g,p) := Pggcdn n a b in - let (aa,bb) := p in - (g,(xO aa, bb)) - | xI a', xI b' => match Pcompare a' b' Eq with - | Eq => (a,(1,1)) - | Lt => - let (g,p) := Pggcdn n (b'-a') a in - let (ba,aa) := p in - (g,(aa, aa + xO ba)) - | Gt => - let (g,p) := Pggcdn n (a'-b') b in - let (ab,bb) := p in - (g,(bb+xO ab, bb)) - end + | xI a', xI b' => + match Pcompare a' b' Eq with + | Eq => a + | Lt => Pgcdn n (b'-a') a + | Gt => Pgcdn n (a'-b') b + end end end. Definition Pgcd (a b: positive) := Pgcdn (Psize a + Psize b)%nat a b. -Definition Pggcd (a b: positive) := Pggcdn (Psize a + Psize b)%nat a b. -Open Scope Z_scope. +Close Scope positive_scope. -Definition Zgcd (a b : Z) : Z := match a,b with - | Z0, _ => Zabs b - | _, Z0 => Zabs a - | Zpos a, Zpos b => Zpos (Pgcd a b) - | Zpos a, Zneg b => Zpos (Pgcd a b) - | Zneg a, Zpos b => Zpos (Pgcd a b) - | Zneg a, Zneg b => Zpos (Pgcd a b) - end. - -Definition Zggcd (a b : Z) : Z*(Z*Z) := match a,b with - | Z0, _ => (Zabs b,(0, Zsgn b)) - | _, Z0 => (Zabs a,(Zsgn a, 0)) - | Zpos a, Zpos b => - let (g,p) := Pggcd a b in - let (aa,bb) := p in - (Zpos g, (Zpos aa, Zpos bb)) - | Zpos a, Zneg b => - let (g,p) := Pggcd a b in - let (aa,bb) := p in - (Zpos g, (Zpos aa, Zneg bb)) - | Zneg a, Zpos b => - let (g,p) := Pggcd a b in - let (aa,bb) := p in - (Zpos g, (Zneg aa, Zpos bb)) - | Zneg a, Zneg b => - let (g,p) := Pggcd a b in - let (aa,bb) := p in - (Zpos g, (Zneg aa, Zneg bb)) - end. +Definition Zgcd (a b : Z) : Z := + match a,b with + | Z0, _ => Zabs b + | _, Z0 => Zabs a + | Zpos a, Zpos b => Zpos (Pgcd a b) + | Zpos a, Zneg b => Zpos (Pgcd a b) + | Zneg a, Zpos b => Zpos (Pgcd a b) + | Zneg a, Zneg b => Zpos (Pgcd a b) + end. Lemma Zgcd_is_pos : forall a b, 0 <= Zgcd a b. Proof. unfold Zgcd; destruct a; destruct b; auto with zarith. Qed. -Lemma Psize_monotone : forall p q, Pcompare p q Eq = Lt -> (Psize p <= Psize q)%nat. -Proof. - induction p; destruct q; simpl; auto with arith; intros; try discriminate. - intros; generalize (Pcompare_Gt_Lt _ _ H); auto with arith. - intros; destruct (Pcompare_Lt_Lt _ _ H); auto with arith; subst; auto. -Qed. - -Lemma Pminus_Zminus : forall a b, Pcompare a b Eq = Lt -> - Zpos (b-a) = Zpos b - Zpos a. -Proof. - intros. - repeat rewrite Zpos_eq_Z_of_nat_o_nat_of_P. - rewrite nat_of_P_minus_morphism. - apply inj_minus1. - apply lt_le_weak. - apply nat_of_P_lt_Lt_compare_morphism; auto. - rewrite ZC4; rewrite H; auto. -Qed. - Lemma Zis_gcd_even_odd : forall a b g, Zis_gcd (Zpos a) (Zpos (xI b)) g -> Zis_gcd (Zpos (xO a)) (Zpos (xI b)) g. Proof. @@ -758,12 +974,12 @@ Proof. assert (Psize (b-a) <= Psize b)%nat. apply Psize_monotone. change (Zpos (b-a) < Zpos b). - rewrite (Pminus_Zminus _ _ H1). + rewrite (Zpos_minus_morphism _ _ H1). assert (0 < Zpos a) by (compute; auto). omega. omega. rewrite Zpos_xO; do 2 rewrite Zpos_xI. - rewrite Pminus_Zminus; auto. + rewrite Zpos_minus_morphism; auto. omega. (* a = xI, b = xI, compare = Gt *) apply Zis_gcd_for_euclid with 1. @@ -775,13 +991,13 @@ Proof. assert (Psize (a-b) <= Psize a)%nat. apply Psize_monotone. change (Zpos (a-b) < Zpos a). - rewrite (Pminus_Zminus b a). + rewrite (Zpos_minus_morphism b a). assert (0 < Zpos b) by (compute; auto). omega. rewrite ZC4; rewrite H1; auto. omega. rewrite Zpos_xO; do 2 rewrite Zpos_xI. - rewrite Pminus_Zminus; auto. + rewrite Zpos_minus_morphism; auto. omega. rewrite ZC4; rewrite H1; auto. (* a = xI, b = xO *) @@ -840,6 +1056,230 @@ Proof. apply Pgcd_correct. 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]. +Qed. + +Theorem Zdivide_Zgcd: forall p q r : Z, + (p | q) -> (p | r) -> (p | Zgcd 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. +Qed. + +Theorem Zis_gcd_gcd: forall a b c : Z, + 0 <= c -> Zis_gcd a b c -> Zgcd 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. +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. + +Theorem Zgcd_div_swap0 : forall a b : Z, + 0 < Zgcd a b -> + 0 < b -> + (a / Zgcd a b) * b = a * (b/Zgcd 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. + 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 < b -> + (c * a) / Zgcd a b * b = c * a * (b/Zgcd a b). +Proof. + intros a b c 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. + repeat rewrite Zmult_assoc; f_equal. + rewrite Zdivide_Zdiv_eq_2; auto. + repeat rewrite <- Zmult_assoc; f_equal. + rewrite Zmult_comm. + rewrite <- Zdivide_Zdiv_eq; auto. +Qed. + +Theorem Zgcd_1_rel_prime : forall a b, + Zgcd a b = 1 <-> rel_prime a b. +Proof. + unfold rel_prime; split; intro H. + rewrite <- H; apply Zgcd_is_gcd. + case (Zis_gcd_unique a b (Zgcd a b) 1); auto. + apply Zgcd_is_gcd. + intros H2; absurd (0 <= Zgcd a b); auto with zarith. + generalize (Zgcd_is_pos a b); auto with zarith. +Qed. + +Definition rel_prime_dec: forall a b, + { rel_prime a b }+{ ~ rel_prime a b }. +Proof. + intros a b; case (Z_eq_dec (Zgcd a b) 1); intros H1. + left; apply -> Zgcd_1_rel_prime; auto. + right; contradict H1; apply <- Zgcd_1_rel_prime; auto. +Defined. + +Definition prime_dec_aux: + forall p m, + { forall n, 1 < n < m -> rel_prime n p } + + { exists n, 1 < n < m /\ ~ rel_prime n p }. +Proof. + intros p m. + case (Z_lt_dec 1 m); intros H1; + [ | left; intros; elimtype False; omega ]. + pattern m; apply natlike_rec; auto with zarith. + left; intros; elimtype False; omega. + intros x Hx IH; destruct IH as [F|E]. + destruct (rel_prime_dec x p) as [Y|N]. + left; intros n [HH1 HH2]. + case (Zgt_succ_gt_or_eq x n); auto with zarith. + intros HH3; subst x; auto. + 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. +Defined. + +Definition prime_dec: forall p, { prime p }+{ ~ prime p }. +Proof. + intros p; case (Z_lt_dec 1 p); intros H1. + case (prime_dec_aux p p); intros H2. + left; apply prime_intro; auto. + intros n [Hn1 Hn2]; case Zle_lt_or_eq with ( 1 := Hn1 ); auto. + intros HH; subst n. + red; apply Zis_gcd_intro; auto with zarith. + right; intros H3; inversion_clear H3 as [Hp1 Hp2]. + case H2; intros n [Hn1 Hn2]; case Hn2; auto with zarith. + right; intros H3; inversion_clear H3 as [Hp1 Hp2]; case H1; auto. +Defined. + +Theorem not_prime_divide: + forall p, 1 < p -> ~ prime p -> exists n, 1 < n < p /\ (n | p). +Proof. + intros p Hp Hp1. + case (prime_dec_aux p p); intros H1. + elim Hp1; constructor; auto. + intros n [Hn1 Hn2]. + case Zle_lt_or_eq with ( 1 := Hn1 ); auto with zarith. + intros H2; subst n; red; apply Zis_gcd_intro; auto with zarith. + case H1; intros n [Hn1 Hn2]. + generalize (Zgcd_is_pos n p); intros Hpos. + case (Zle_lt_or_eq 0 (Zgcd n p)); auto with zarith; intros H3. + case (Zle_lt_or_eq 1 (Zgcd n p)); auto with zarith; intros H4. + exists (Zgcd n p); split; auto. + split; auto. + apply Zle_lt_trans with n; auto with zarith. + generalize (Zgcd_is_gcd n p); intros tmp; inversion_clear tmp as [Hr1 Hr2 Hr3]. + case Hr1; intros q Hq. + case (Zle_or_lt q 0); auto with zarith; intros Ht. + absurd (n <= 0 * Zgcd n p) ; auto with zarith. + pattern n at 1; rewrite Hq; auto with zarith. + apply Zle_trans with (1 * Zgcd n p); auto with zarith. + pattern n at 2; rewrite Hq; auto with zarith. + generalize (Zgcd_is_gcd n p); intros Ht; inversion Ht; auto. + case Hn2; red. + rewrite H4; apply Zgcd_is_gcd. + generalize (Zgcd_is_gcd n p); rewrite <- H3; intros tmp; + inversion_clear tmp as [Hr1 Hr2 Hr3]. + absurd (n = 0); auto with zarith. + case Hr1; auto with zarith. +Qed. + +(** A Generalized Gcd that also computes Bezout coefficients. + The algorithm is the same as for Zgcd. *) + +Open Scope positive_scope. + +Fixpoint Pggcdn (n: nat) (a b : positive) { struct n } : (positive*(positive*positive)) := + match n with + | O => (1,(a,b)) + | S n => + match a,b with + | xH, b => (1,(1,b)) + | a, xH => (1,(a,1)) + | xO a, xO b => + let (g,p) := Pggcdn n a b in + (xO g,p) + | a, xO b => + let (g,p) := Pggcdn n a b in + let (aa,bb) := p in + (g,(aa, xO bb)) + | xO a, b => + let (g,p) := Pggcdn n a b in + let (aa,bb) := p in + (g,(xO aa, bb)) + | xI a', xI b' => + match Pcompare a' b' Eq with + | Eq => (a,(1,1)) + | Lt => + let (g,p) := Pggcdn n (b'-a') a in + let (ba,aa) := p in + (g,(aa, aa + xO ba)) + | Gt => + let (g,p) := Pggcdn n (a'-b') b in + let (ab,bb) := p in + (g,(bb+xO ab, bb)) + end + end + end. + +Definition Pggcd (a b: positive) := Pggcdn (Psize a + Psize b)%nat a b. + +Open Scope Z_scope. + +Definition Zggcd (a b : Z) : Z*(Z*Z) := + match a,b with + | Z0, _ => (Zabs b,(0, Zsgn b)) + | _, Z0 => (Zabs a,(Zsgn a, 0)) + | Zpos a, Zpos b => + let (g,p) := Pggcd a b in + let (aa,bb) := p in + (Zpos g, (Zpos aa, Zpos bb)) + | Zpos a, Zneg b => + let (g,p) := Pggcd a b in + let (aa,bb) := p in + (Zpos g, (Zpos aa, Zneg bb)) + | Zneg a, Zpos b => + let (g,p) := Pggcd a b in + let (aa,bb) := p in + (Zpos g, (Zneg aa, Zpos bb)) + | Zneg a, Zneg b => + let (g,p) := Pggcd a b in + let (aa,bb) := p in + (Zpos g, (Zneg aa, Zneg bb)) + end. + Lemma Pggcdn_gcdn : forall n a b, fst (Pggcdn n a b) = Pgcdn n a b. @@ -870,8 +1310,8 @@ Open Scope positive_scope. Lemma Pggcdn_correct_divisors : forall n a b, let (g,p) := Pggcdn n a b in - let (aa,bb):=p in - (a=g*aa) /\ (b=g*bb). + let (aa,bb):=p in + (a=g*aa) /\ (b=g*bb). Proof. induction n. simpl; auto. @@ -910,30 +1350,32 @@ Qed. Lemma Pggcd_correct_divisors : forall a b, let (g,p) := Pggcd a b in - let (aa,bb):=p in - (a=g*aa) /\ (b=g*bb). + let (aa,bb):=p in + (a=g*aa) /\ (b=g*bb). Proof. intros a b; exact (Pggcdn_correct_divisors (Psize a + Psize b)%nat a b). Qed. -Open Scope Z_scope. +Close Scope positive_scope. Lemma Zggcd_correct_divisors : forall a b, let (g,p) := Zggcd a b in - let (aa,bb):=p in - (a=g*aa) /\ (b=g*bb). + let (aa,bb):=p in + (a=g*aa) /\ (b=g*bb). Proof. destruct a; destruct b; simpl; auto; try solve [rewrite Pmult_comm; simpl; auto]; generalize (Pggcd_correct_divisors p p0); destruct (Pggcd p p0) as (g,(aa,bb)); destruct 1; subst; auto. Qed. -Theorem Zgcd_spec : forall x y : Z, {z : Z | Zis_gcd x y z /\ 0 <= z}. +Theorem Zggcd_opp: forall x y, + Zggcd (-x) y = let (p1,p) := Zggcd x y in + let (p2,p3) := p in + (p1,(-p2,p3)). Proof. - intros x y; exists (Zgcd x y). - split; [apply Zgcd_is_gcd | apply Zgcd_is_pos]. +intros [|x|x] [|y|y]; unfold Zggcd, Zopp; auto. +case Pggcd; intros p1 (p2, p3); auto. +case Pggcd; intros p1 (p2, p3); auto. +case Pggcd; intros p1 (p2, p3); auto. +case Pggcd; intros p1 (p2, p3); auto. Qed. - - - - diff --git a/theories/ZArith/Zorder.v b/theories/ZArith/Zorder.v index 47490be6..425aa83b 100644 --- a/theories/ZArith/Zorder.v +++ b/theories/ZArith/Zorder.v @@ -5,9 +5,9 @@ (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: Zorder.v 9302 2006-10-27 21:21:17Z barras $ i*) +(*i $Id: Zorder.v 10291 2007-11-06 02:18:53Z letouzey $ i*) -(** Binary Integers (Pierre Crégut (CNET, Lannion, France) *) +(** Binary Integers (Pierre Crégut (CNET, Lannion, France) *) Require Import BinPos. Require Import BinInt. @@ -549,7 +549,7 @@ Hint Immediate Zeq_le: zarith. (** Transitivity using successor *) -Lemma Zge_trans_succ : forall n m p:Z, Zsucc n > m -> m > p -> n > p. +Lemma Zgt_trans_succ : forall n m p:Z, Zsucc n > m -> m > p -> n > p. Proof. intros n m p H1 H2; apply Zle_gt_trans with (m := m); [ apply Zgt_succ_le; assumption | assumption ]. @@ -997,5 +997,31 @@ Proof. rewrite <- Zplus_assoc; rewrite Zplus_opp_l; rewrite Zplus_0_r; exact H. Qed. +Lemma Zmult_lt_compat: + forall n m p q : Z, 0 <= n < p -> 0 <= m < q -> n * m < p * q. +Proof. + intros n m p q (H1, H2) (H3,H4). + assert (0<p) by (apply Zle_lt_trans with n; auto). + assert (0<q) by (apply Zle_lt_trans with m; auto). + case Zle_lt_or_eq with (1 := H1); intros H5; auto with zarith. + case Zle_lt_or_eq with (1 := H3); intros H6; auto with zarith. + apply Zlt_trans with (n * q). + apply Zmult_lt_compat_l; auto. + apply Zmult_lt_compat_r; auto with zarith. + rewrite <- H6; rewrite Zmult_0_r; apply Zmult_lt_0_compat; auto with zarith. + rewrite <- H5; simpl; apply Zmult_lt_0_compat; auto with zarith. +Qed. + +Lemma Zmult_lt_compat2: + forall n m p q : Z, 0 < n <= p -> 0 < m < q -> n * m < p * q. +Proof. + intros n m p q (H1, H2) (H3, H4). + apply Zle_lt_trans with (p * m). + apply Zmult_le_compat_r; auto. + apply Zlt_le_weak; auto. + apply Zmult_lt_compat_l; auto. + apply Zlt_le_trans with n; auto. +Qed. + (** For compatibility *) Notation Zlt_O_minus_lt := Zlt_0_minus_lt (only parsing). diff --git a/theories/ZArith/Zpow_facts.v b/theories/ZArith/Zpow_facts.v new file mode 100644 index 00000000..3d4d235a --- /dev/null +++ b/theories/ZArith/Zpow_facts.v @@ -0,0 +1,465 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(*i $Id: Zpow_facts.v 11098 2008-06-11 09:16:22Z letouzey $ i*) + +Require Import ZArith_base. +Require Import ZArithRing. +Require Import Zcomplements. +Require Export Zpower. +Require Import Zdiv. +Require Import Znumtheory. +Open Local Scope Z_scope. + +Lemma Zpower_pos_1_r: forall x, Zpower_pos x 1 = x. +Proof. + intros x; unfold Zpower_pos; simpl; auto with zarith. +Qed. + +Lemma Zpower_pos_1_l: forall p, Zpower_pos 1 p = 1. +Proof. + induction p. + (* xI *) + rewrite xI_succ_xO, <-Pplus_diag, Pplus_one_succ_l. + repeat rewrite Zpower_pos_is_exp. + rewrite Zpower_pos_1_r, IHp; auto. + (* xO *) + rewrite <- Pplus_diag. + repeat rewrite Zpower_pos_is_exp. + rewrite IHp; auto. + (* xH *) + rewrite Zpower_pos_1_r; auto. +Qed. + +Lemma Zpower_pos_0_l: forall p, Zpower_pos 0 p = 0. +Proof. + induction p. + change (xI p) with (1 + (xO p))%positive. + rewrite Zpower_pos_is_exp, Zpower_pos_1_r; auto. + rewrite <- Pplus_diag. + rewrite Zpower_pos_is_exp, IHp; auto. + rewrite Zpower_pos_1_r; auto. +Qed. + +Lemma Zpower_pos_pos: forall x p, + 0 < x -> 0 < Zpower_pos x p. +Proof. + induction p; intros. + (* xI *) + rewrite xI_succ_xO, <-Pplus_diag, Pplus_one_succ_l. + repeat rewrite Zpower_pos_is_exp. + rewrite Zpower_pos_1_r. + repeat apply Zmult_lt_0_compat; auto. + (* xO *) + rewrite <- Pplus_diag. + repeat rewrite Zpower_pos_is_exp. + repeat apply Zmult_lt_0_compat; auto. + (* xH *) + rewrite Zpower_pos_1_r; auto. +Qed. + + +Theorem Zpower_1_r: forall z, z^1 = z. +Proof. + exact Zpower_pos_1_r. +Qed. + +Theorem Zpower_1_l: forall z, 0 <= z -> 1^z = 1. +Proof. + destruct z; simpl; auto. + intros; apply Zpower_pos_1_l. + intros; compute in H; elim H; auto. +Qed. + +Theorem Zpower_0_l: forall z, z<>0 -> 0^z = 0. +Proof. + destruct z; simpl; auto with zarith. + intros; apply Zpower_pos_0_l. +Qed. + +Theorem Zpower_0_r: forall z, z^0 = 1. +Proof. + simpl; auto. +Qed. + +Theorem Zpower_2: forall z, z^2 = z * z. +Proof. + intros; ring. +Qed. + +Theorem Zpower_gt_0: forall x y, + 0 < x -> 0 <= y -> 0 < x^y. +Proof. + destruct y; simpl; auto with zarith. + intros; apply Zpower_pos_pos; auto. + intros; compute in H0; elim H0; auto. +Qed. + +Theorem Zpower_Zabs: forall a b, Zabs (a^b) = (Zabs a)^b. +Proof. + intros a b; case (Zle_or_lt 0 b). + intros Hb; pattern b; apply natlike_ind; auto with zarith. + intros x Hx Hx1; unfold Zsucc. + (repeat rewrite Zpower_exp); auto with zarith. + rewrite Zabs_Zmult; rewrite Hx1. + f_equal; auto. + replace (a ^ 1) with a; auto. + simpl; unfold Zpower_pos; simpl; rewrite Zmult_1_r; auto. + simpl; unfold Zpower_pos; simpl; rewrite Zmult_1_r; auto. + case b; simpl; auto with zarith. + intros p Hp; discriminate. +Qed. + +Theorem Zpower_Zsucc: forall p n, 0 <= n -> p^(Zsucc n) = p * p^n. +Proof. + intros p n H. + unfold Zsucc; rewrite Zpower_exp; auto with zarith. + rewrite Zpower_1_r; apply Zmult_comm. +Qed. + +Theorem Zpower_mult: forall p q r, 0 <= q -> 0 <= r -> p^(q*r) = (p^q)^r. +Proof. + intros p q r H1 H2; generalize H2; pattern r; apply natlike_ind; auto. + intros H3; rewrite Zmult_0_r; repeat rewrite Zpower_exp_0; auto. + intros r1 H3 H4 H5. + unfold Zsucc; rewrite Zpower_exp; auto with zarith. + rewrite <- H4; try rewrite Zpower_1_r; try rewrite <- Zpower_exp; try f_equal; auto with zarith. + ring. + apply Zle_ge; replace 0 with (0 * r1); try apply Zmult_le_compat_r; auto. +Qed. + +Theorem Zpower_le_monotone: forall a b c, + 0 < a -> 0 <= b <= c -> a^b <= a^c. +Proof. + intros a b c H (H1, H2). + rewrite <- (Zmult_1_r (a ^ b)); replace c with (b + (c - b)); auto with zarith. + rewrite Zpower_exp; auto with zarith. + apply Zmult_le_compat_l; auto with zarith. + assert (0 < a ^ (c - b)); auto with zarith. + apply Zpower_gt_0; auto with zarith. + apply Zlt_le_weak; apply Zpower_gt_0; auto with zarith. +Qed. + +Theorem Zpower_lt_monotone: forall a b c, + 1 < a -> 0 <= b < c -> a^b < a^c. +Proof. + intros a b c H (H1, H2). + rewrite <- (Zmult_1_r (a ^ b)); replace c with (b + (c - b)); auto with zarith. + rewrite Zpower_exp; auto with zarith. + apply Zmult_lt_compat_l; auto with zarith. + apply Zpower_gt_0; auto with zarith. + assert (0 < a ^ (c - b)); auto with zarith. + apply Zpower_gt_0; auto with zarith. + apply Zlt_le_trans with (a ^1); auto with zarith. + rewrite Zpower_1_r; auto with zarith. + apply Zpower_le_monotone; auto with zarith. +Qed. + +Theorem Zpower_gt_1 : forall x y, + 1 < x -> 0 < y -> 1 < x^y. +Proof. + intros x y H1 H2. + replace 1 with (x ^ 0) by apply Zpower_0_r. + apply Zpower_lt_monotone; auto with zarith. +Qed. + +Theorem Zpower_ge_0: forall x y, 0 <= x -> 0 <= x^y. +Proof. + intros x y; case y; auto with zarith. + simpl ; auto with zarith. + intros p H1; assert (H: 0 <= Zpos p); auto with zarith. + generalize H; pattern (Zpos p); apply natlike_ind; auto with zarith. + intros p1 H2 H3 _; unfold Zsucc; rewrite Zpower_exp; simpl; auto with zarith. + apply Zmult_le_0_compat; auto with zarith. + generalize H1; case x; compute; intros; auto; try discriminate. +Qed. + +Theorem Zpower_le_monotone2: + forall a b c, 0 < a -> b <= c -> a^b <= a^c. +Proof. + intros a b c H H2. + destruct (Z_le_gt_dec 0 b). + apply Zpower_le_monotone; auto. + replace (a^b) with 0. + destruct (Z_le_gt_dec 0 c). + destruct (Zle_lt_or_eq _ _ z0). + apply Zlt_le_weak;apply Zpower_gt_0;trivial. + rewrite <- H0;simpl;auto with zarith. + replace (a^c) with 0. auto with zarith. + destruct c;trivial;unfold Zgt in z0;discriminate z0. + destruct b;trivial;unfold Zgt in z;discriminate z. +Qed. + +Theorem Zmult_power: forall p q r, 0 <= r -> + (p*q)^r = p^r * q^r. +Proof. + intros p q r H1; generalize H1; pattern r; apply natlike_ind; auto. + clear r H1; intros r H1 H2 H3. + unfold Zsucc; rewrite Zpower_exp; auto with zarith. + rewrite H2; repeat rewrite Zpower_exp; auto with zarith; ring. +Qed. + +Hint Resolve Zpower_ge_0 Zpower_gt_0: zarith. + +Theorem Zpower_le_monotone3: forall a b c, + 0 <= c -> 0 <= a <= b -> a^c <= b^c. +Proof. + intros a b c H (H1, H2). + generalize H; pattern c; apply natlike_ind; auto. + intros x HH HH1 _; unfold Zsucc; repeat rewrite Zpower_exp; auto with zarith. + repeat rewrite Zpower_1_r. + apply Zle_trans with (a^x * b); auto with zarith. +Qed. + +Lemma Zpower_le_monotone_inv: forall a b c, + 1 < a -> 0 < b -> a^b <= a^c -> b <= c. +Proof. + intros a b c H H0 H1. + destruct (Z_le_gt_dec b c);trivial. + assert (2 <= a^b). + apply Zle_trans with (2^b). + pattern 2 at 1;replace 2 with (2^1);trivial. + apply Zpower_le_monotone;auto with zarith. + apply Zpower_le_monotone3;auto with zarith. + assert (c > 0). + destruct (Z_le_gt_dec 0 c);trivial. + destruct (Zle_lt_or_eq _ _ z0);auto with zarith. + rewrite <- H3 in H1;simpl in H1; elimtype False;omega. + destruct c;try discriminate z0. simpl in H1. elimtype False;omega. + assert (H4 := Zpower_lt_monotone a c b H). elimtype False;omega. +Qed. + +Theorem Zpower_nat_Zpower: forall p q, 0 <= q -> + p^q = Zpower_nat p (Zabs_nat q). +Proof. + intros p1 q1; case q1; simpl. + intros _; exact (refl_equal _). + intros p2 _; apply Zpower_pos_nat. + intros p2 H1; case H1; auto. +Qed. + +Theorem Zpower2_lt_lin: forall n, 0 <= n -> n < 2^n. +Proof. + intros n; apply (natlike_ind (fun n => n < 2 ^n)); clear n. + simpl; auto with zarith. + intros n H1 H2; unfold Zsucc. + case (Zle_lt_or_eq _ _ H1); clear H1; intros H1. + apply Zle_lt_trans with (n + n); auto with zarith. + rewrite Zpower_exp; auto with zarith. + rewrite Zpower_1_r. + assert (tmp: forall p, p * 2 = p + p); intros; try ring; + rewrite tmp; auto with zarith. + subst n; simpl; unfold Zpower_pos; simpl; auto with zarith. +Qed. + +Theorem Zpower2_le_lin: forall n, 0 <= n -> n <= 2^n. +Proof. + intros; apply Zlt_le_weak; apply Zpower2_lt_lin; auto. +Qed. + +Lemma Zpower2_Psize : + forall n p, Zpos p < 2^(Z_of_nat n) <-> (Psize p <= n)%nat. +Proof. + induction n. + destruct p; split; intros H; discriminate H || inversion H. + destruct p; simpl Psize. + rewrite inj_S, Zpower_Zsucc; auto with zarith. + rewrite Zpos_xI; specialize IHn with p; omega. + rewrite inj_S, Zpower_Zsucc; auto with zarith. + rewrite Zpos_xO; specialize IHn with p; omega. + split; auto with arith. + intros _; apply Zpower_gt_1; auto with zarith. + rewrite inj_S; generalize (Zle_0_nat n); omega. +Qed. + +(** * Zpower and modulo *) + +Theorem Zpower_mod: forall p q n, 0 < n -> + (p^q) mod n = ((p mod n)^q) mod n. +Proof. + intros p q n Hn; case (Zle_or_lt 0 q); intros H1. + generalize H1; pattern q; apply natlike_ind; auto. + intros q1 Hq1 Rec _; unfold Zsucc; repeat rewrite Zpower_exp; repeat rewrite Zpower_1_r; auto with zarith. + rewrite (fun x => (Zmult_mod x p)); try rewrite Rec; auto with zarith. + rewrite (fun x y => (Zmult_mod (x ^y))); try f_equal; auto with zarith. + f_equal; auto; apply sym_equal; apply Zmod_mod; auto with zarith. + generalize H1; case q; simpl; auto. + intros; discriminate. +Qed. + +(** A direct way to compute Zpower modulo **) + +Fixpoint Zpow_mod_pos (a: Z)(m: positive)(n : Z) {struct m} : Z := + match m with + | xH => a mod n + | xO m' => + let z := Zpow_mod_pos a m' n in + match z with + | 0 => 0 + | _ => (z * z) mod n + end + | xI m' => + let z := Zpow_mod_pos a m' n in + match z with + | 0 => 0 + | _ => (z * z * a) mod n + end + end. + +Definition Zpow_mod a m n := + match m with + | 0 => 1 + | Zpos p => Zpow_mod_pos a p n + | Zneg p => 0 + end. + +Theorem Zpow_mod_pos_correct: forall a m n, 0 < n -> + Zpow_mod_pos a m n = (Zpower_pos a m) mod n. +Proof. + intros a m; elim m; simpl; auto. + intros p Rec n H1; rewrite xI_succ_xO, Pplus_one_succ_r, <-Pplus_diag; auto. + repeat rewrite Zpower_pos_is_exp; auto. + repeat rewrite Rec; auto. + rewrite Zpower_pos_1_r. + repeat rewrite (fun x => (Zmult_mod x a)); auto with zarith. + rewrite (Zmult_mod (Zpower_pos a p)); auto with zarith. + case (Zpower_pos a p mod n); auto. + intros p Rec n H1; rewrite <- Pplus_diag; auto. + repeat rewrite Zpower_pos_is_exp; auto. + repeat rewrite Rec; auto. + rewrite (Zmult_mod (Zpower_pos a p)); auto with zarith. + case (Zpower_pos a p mod n); auto. + unfold Zpower_pos; simpl; rewrite Zmult_1_r; auto with zarith. +Qed. + +Theorem Zpow_mod_correct: forall a m n, 1 < n -> 0 <= m -> + Zpow_mod a m n = (a ^ m) mod n. +Proof. + intros a m n; case m; simpl. + intros; apply sym_equal; apply Zmod_small; auto with zarith. + intros; apply Zpow_mod_pos_correct; auto with zarith. + intros p H H1; case H1; auto. +Qed. + +(* Complements about power and number theory. *) + +Lemma Zpower_divide: forall p q, 0 < q -> (p | p ^ q). +Proof. + intros p q H; exists (p ^(q - 1)). + pattern p at 3; rewrite <- (Zpower_1_r p); rewrite <- Zpower_exp; try f_equal; auto with zarith. +Qed. + +Theorem rel_prime_Zpower_r: forall i p q, 0 < i -> + rel_prime p q -> rel_prime p (q^i). +Proof. + intros i p q Hi Hpq; generalize Hi; pattern i; apply natlike_ind; auto with zarith; clear i Hi. + intros H; contradict H; auto with zarith. + intros i Hi Rec _; rewrite Zpower_Zsucc; auto. + apply rel_prime_mult; auto. + case Zle_lt_or_eq with (1 := Hi); intros Hi1; subst; auto. + rewrite Zpower_0_r; apply rel_prime_sym; apply rel_prime_1. +Qed. + +Theorem rel_prime_Zpower: forall i j p q, 0 <= i -> 0 <= j -> + rel_prime p q -> rel_prime (p^i) (q^j). +Proof. + intros i j p q Hi; generalize Hi j p q; pattern i; apply natlike_ind; auto with zarith; clear i Hi j p q. + intros _ j p q H H1; rewrite Zpower_0_r; apply rel_prime_1. + intros n Hn Rec _ j p q Hj Hpq. + rewrite Zpower_Zsucc; auto. + case Zle_lt_or_eq with (1 := Hj); intros Hj1; subst. + apply rel_prime_sym; apply rel_prime_mult; auto. + apply rel_prime_sym; apply rel_prime_Zpower_r; auto with arith. + apply rel_prime_sym; apply Rec; auto. + rewrite Zpower_0_r; apply rel_prime_sym; apply rel_prime_1. +Qed. + +Theorem prime_power_prime: forall p q n, 0 <= n -> + prime p -> prime q -> (p | q^n) -> p = q. +Proof. + intros p q n Hn Hp Hq; pattern n; apply natlike_ind; auto; clear n Hn. + rewrite Zpower_0_r; intros. + assert (2<=p) by (apply prime_ge_2; auto). + assert (p<=1) by (apply Zdivide_le; auto with zarith). + omega. + intros n1 H H1. + unfold Zsucc; rewrite Zpower_exp; try rewrite Zpower_1_r; auto with zarith. + assert (2<=p) by (apply prime_ge_2; auto). + assert (2<=q) by (apply prime_ge_2; auto). + intros H3; case prime_mult with (2 := H3); auto. + intros; apply prime_div_prime; auto. +Qed. + +Theorem Zdivide_power_2: forall x p n, 0 <= n -> 0 <= x -> prime p -> + (x | p^n) -> exists m, x = p^m. +Proof. + intros x p n Hn Hx; revert p n Hn; generalize Hx. + pattern x; apply Z_lt_induction; auto. + clear x Hx; intros x IH Hx p n Hn Hp H. + case Zle_lt_or_eq with (1 := Hx); auto; clear Hx; intros Hx; subst. + case (Zle_lt_or_eq 1 x); auto with zarith; clear Hx; intros Hx; subst. + (* x > 1 *) + case (prime_dec x); intros H2. + exists 1; rewrite Zpower_1_r; apply prime_power_prime with n; auto. + case not_prime_divide with (2 := H2); auto. + intros p1 ((H3, H4), (q1, Hq1)); subst. + case (IH p1) with p n; auto with zarith. + apply Zdivide_trans with (2 := H); exists q1; auto with zarith. + intros r1 Hr1. + case (IH q1) with p n; auto with zarith. + case (Zle_lt_or_eq 0 q1). + apply Zmult_le_0_reg_r with p1; auto with zarith. + split; auto with zarith. + pattern q1 at 1; replace q1 with (q1 * 1); auto with zarith. + apply Zmult_lt_compat_l; auto with zarith. + intros H5; subst; contradict Hx; auto with zarith. + apply Zmult_le_0_reg_r with p1; auto with zarith. + apply Zdivide_trans with (2 := H); exists p1; auto with zarith. + intros r2 Hr2; exists (r2 + r1); subst. + apply sym_equal; apply Zpower_exp. + generalize Hx; case r2; simpl; auto with zarith. + intros; red; simpl; intros; discriminate. + generalize H3; case r1; simpl; auto with zarith. + intros; red; simpl; intros; discriminate. + (* x = 1 *) + exists 0; rewrite Zpower_0_r; auto. + (* x = 0 *) + exists n; destruct H; rewrite Zmult_0_r in H; auto. +Qed. + +(** * Zsquare: a direct definition of [z^2] *) + +Fixpoint Psquare (p: positive): positive := + match p with + | xH => xH + | xO p => xO (xO (Psquare p)) + | xI p => xI (xO (Pplus (Psquare p) p)) + end. + +Definition Zsquare p := + match p with + | Z0 => Z0 + | Zpos p => Zpos (Psquare p) + | Zneg p => Zpos (Psquare p) + end. + +Theorem Psquare_correct: forall p, Psquare p = (p * p)%positive. +Proof. + induction p; simpl; auto; f_equal; rewrite IHp. + apply trans_equal with (xO p + xO (p*p))%positive; auto. + rewrite (Pplus_comm (xO p)); auto. + rewrite Pmult_xI_permute_r; rewrite Pplus_assoc. + f_equal; auto. + symmetry; apply Pplus_diag. + symmetry; apply Pmult_xO_permute_r. +Qed. + +Theorem Zsquare_correct: forall p, Zsquare p = p * p. +Proof. + intro p; case p; simpl; auto; intros p1; rewrite Psquare_correct; auto. +Qed. diff --git a/theories/ZArith/Zpower.v b/theories/ZArith/Zpower.v index c9cee31d..1912f5e1 100644 --- a/theories/ZArith/Zpower.v +++ b/theories/ZArith/Zpower.v @@ -6,89 +6,75 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: Zpower.v 9551 2007-01-29 15:13:35Z bgregoir $ i*) +(*i $Id: Zpower.v 11072 2008-06-08 16:13:37Z herbelin $ i*) +Require Import Wf_nat. Require Import ZArith_base. Require Export Zpow_def. Require Import Omega. Require Import Zcomplements. Open Local Scope Z_scope. -Section section1. +Infix "^" := Zpower : Z_scope. (** * Definition of powers over [Z]*) (** [Zpower_nat z n] is the n-th power of [z] when [n] is an unary integer (type [nat]) and [z] a signed integer (type [Z]) *) - Definition Zpower_nat (z:Z) (n:nat) := iter_nat n Z (fun x:Z => z * x) 1. - - (** [Zpower_nat_is_exp] says [Zpower_nat] is a morphism for - [plus : nat->nat] and [Zmult : Z->Z] *) - - Lemma Zpower_nat_is_exp : - forall (n m:nat) (z:Z), - Zpower_nat z (n + m) = Zpower_nat z n * Zpower_nat z m. - Proof. - intros; elim n; - [ simpl in |- *; elim (Zpower_nat z m); auto with zarith - | unfold Zpower_nat in |- *; intros; simpl in |- *; rewrite H; - apply Zmult_assoc ]. - Qed. - - (** This theorem shows that powers of unary and binary integers - are the same thing, modulo the function convert : [positive -> nat] *) - - Theorem Zpower_pos_nat : - forall (z:Z) (p:positive), Zpower_pos z p = Zpower_nat z (nat_of_P p). - Proof. - intros; unfold Zpower_pos in |- *; unfold Zpower_nat in |- *; - apply iter_nat_of_P. - Qed. - - (** Using the theorem [Zpower_pos_nat] and the lemma [Zpower_nat_is_exp] we - deduce that the function [[n:positive](Zpower_pos z n)] is a morphism - for [add : positive->positive] and [Zmult : Z->Z] *) - - Theorem Zpower_pos_is_exp : - forall (n m:positive) (z:Z), - Zpower_pos z (n + m) = Zpower_pos z n * Zpower_pos z m. - Proof. - intros. - rewrite (Zpower_pos_nat z n). - rewrite (Zpower_pos_nat z m). - rewrite (Zpower_pos_nat z (n + m)). - rewrite (nat_of_P_plus_morphism n m). - apply Zpower_nat_is_exp. - Qed. - - Infix "^" := Zpower : Z_scope. - - Hint Immediate Zpower_nat_is_exp: zarith. - Hint Immediate Zpower_pos_is_exp: zarith. - Hint Unfold Zpower_pos: zarith. - Hint Unfold Zpower_nat: zarith. - - Lemma Zpower_exp : - forall x n m:Z, n >= 0 -> m >= 0 -> x ^ (n + m) = x ^ n * x ^ m. - Proof. - destruct n; destruct m; auto with zarith. - simpl in |- *; intros; apply Zred_factor0. - simpl in |- *; auto with zarith. - intros; compute in H0; absurd (Datatypes.Lt = Datatypes.Lt); auto with zarith. - intros; compute in H0; absurd (Datatypes.Lt = Datatypes.Lt); auto with zarith. - Qed. - -End section1. - -(** Exporting notation "^" *) - -Infix "^" := Zpower : Z_scope. - -Hint Immediate Zpower_nat_is_exp: zarith. -Hint Immediate Zpower_pos_is_exp: zarith. -Hint Unfold Zpower_pos: zarith. -Hint Unfold Zpower_nat: zarith. +Definition Zpower_nat (z:Z) (n:nat) := iter_nat n Z (fun x:Z => z * x) 1. + +(** [Zpower_nat_is_exp] says [Zpower_nat] is a morphism for + [plus : nat->nat] and [Zmult : Z->Z] *) + +Lemma Zpower_nat_is_exp : + forall (n m:nat) (z:Z), + Zpower_nat z (n + m) = Zpower_nat z n * Zpower_nat z m. +Proof. + intros; elim n; + [ simpl in |- *; elim (Zpower_nat z m); auto with zarith + | unfold Zpower_nat in |- *; intros; simpl in |- *; rewrite H; + apply Zmult_assoc ]. +Qed. + +(** This theorem shows that powers of unary and binary integers + are the same thing, modulo the function convert : [positive -> nat] *) + +Lemma Zpower_pos_nat : + forall (z:Z) (p:positive), Zpower_pos z p = Zpower_nat z (nat_of_P p). +Proof. + intros; unfold Zpower_pos in |- *; unfold Zpower_nat in |- *; + apply iter_nat_of_P. +Qed. + +(** Using the theorem [Zpower_pos_nat] and the lemma [Zpower_nat_is_exp] we + deduce that the function [[n:positive](Zpower_pos z n)] is a morphism + for [add : positive->positive] and [Zmult : Z->Z] *) + +Lemma Zpower_pos_is_exp : + forall (n m:positive) (z:Z), + Zpower_pos z (n + m) = Zpower_pos z n * Zpower_pos z m. +Proof. + intros. + rewrite (Zpower_pos_nat z n). + rewrite (Zpower_pos_nat z m). + rewrite (Zpower_pos_nat z (n + m)). + rewrite (nat_of_P_plus_morphism n m). + apply Zpower_nat_is_exp. +Qed. + +Hint Immediate Zpower_nat_is_exp Zpower_pos_is_exp : zarith. +Hint Unfold Zpower_pos Zpower_nat: zarith. + +Theorem Zpower_exp : + forall x n m:Z, n >= 0 -> m >= 0 -> x ^ (n + m) = x ^ n * x ^ m. +Proof. + destruct n; destruct m; auto with zarith. + simpl; intros; apply Zred_factor0. + simpl; auto with zarith. + intros; compute in H0; elim H0; auto. + intros; compute in H; elim H; auto. +Qed. Section Powers_of_2. diff --git a/theories/ZArith/Zsqrt.v b/theories/ZArith/Zsqrt.v index 3f475a63..6ea952e6 100644 --- a/theories/ZArith/Zsqrt.v +++ b/theories/ZArith/Zsqrt.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: Zsqrt.v 9551 2007-01-29 15:13:35Z bgregoir $ *) +(* $Id: Zsqrt.v 10295 2007-11-06 22:46:21Z letouzey $ *) Require Import ZArithRing. Require Import Omega. @@ -148,6 +148,7 @@ Definition Zsqrt_plain (x:Z) : Z := end. (** A basic theorem about Zsqrt_plain *) + Theorem Zsqrt_interval : forall n:Z, 0 <= n -> @@ -162,3 +163,53 @@ Proof. intros p Hle; elim Hle; auto. Qed. +(** Positivity *) + +Theorem Zsqrt_plain_is_pos: forall n, 0 <= n -> 0 <= Zsqrt_plain n. +Proof. + intros n m; case (Zsqrt_interval n); auto with zarith. + intros H1 H2; case (Zle_or_lt 0 (Zsqrt_plain n)); auto. + intros H3; contradict H2; auto; apply Zle_not_lt. + apply Zle_trans with ( 2 := H1 ). + replace ((Zsqrt_plain n + 1) * (Zsqrt_plain n + 1)) + with (Zsqrt_plain n * Zsqrt_plain n + (2 * Zsqrt_plain n + 1)); + auto with zarith. + ring. +Qed. + +(** Direct correctness on squares. *) + +Theorem Zsqrt_square_id: forall a, 0 <= a -> Zsqrt_plain (a * a) = a. +Proof. + intros a H. + generalize (Zsqrt_plain_is_pos (a * a)); auto with zarith; intros Haa. + case (Zsqrt_interval (a * a)); auto with zarith. + intros H1 H2. + case (Zle_or_lt a (Zsqrt_plain (a * a))); intros H3; auto. + case Zle_lt_or_eq with (1:=H3); auto; clear H3; intros H3. + contradict H1; auto; apply Zlt_not_le; auto with zarith. + apply Zle_lt_trans with (a * Zsqrt_plain (a * a)); auto with zarith. + apply Zmult_lt_compat_r; auto with zarith. + contradict H2; auto; apply Zle_not_lt; auto with zarith. + apply Zmult_le_compat; auto with zarith. +Qed. + +(** [Zsqrt_plain] is increasing *) + +Theorem Zsqrt_le: + forall p q, 0 <= p <= q -> Zsqrt_plain p <= Zsqrt_plain q. +Proof. + intros p q [H1 H2]; case Zle_lt_or_eq with (1:=H2); clear H2; intros H2; + [ | subst q; auto with zarith]. + case (Zle_or_lt (Zsqrt_plain p) (Zsqrt_plain q)); auto; intros H3. + assert (Hp: (0 <= Zsqrt_plain q)). + apply Zsqrt_plain_is_pos; auto with zarith. + absurd (q <= p); auto with zarith. + apply Zle_trans with ((Zsqrt_plain q + 1) * (Zsqrt_plain q + 1)). + case (Zsqrt_interval q); auto with zarith. + apply Zle_trans with (Zsqrt_plain p * Zsqrt_plain p); auto with zarith. + apply Zmult_le_compat; auto with zarith. + case (Zsqrt_interval p); auto with zarith. +Qed. + + |