summaryrefslogtreecommitdiff
path: root/theories/ZArith
diff options
context:
space:
mode:
authorGravatar Samuel Mimram <smimram@debian.org>2008-07-25 15:12:53 +0200
committerGravatar Samuel Mimram <smimram@debian.org>2008-07-25 15:12:53 +0200
commita0cfa4f118023d35b767a999d5a2ac4b082857b4 (patch)
treedabcac548e299fee1da464c93b3dba98484f45b1 /theories/ZArith
parent2281410e38ef99d025ea77194585a9bc019fdaa9 (diff)
Imported Upstream version 8.2~beta3+dfsgupstream/8.2.beta3+dfsg
Diffstat (limited to 'theories/ZArith')
-rw-r--r--theories/ZArith/BinInt.v208
-rw-r--r--theories/ZArith/Int.v47
-rw-r--r--theories/ZArith/ZArith_dec.v2
-rw-r--r--theories/ZArith/ZOdiv.v953
-rw-r--r--theories/ZArith/ZOdiv_def.v136
-rw-r--r--theories/ZArith/Zabs.v129
-rw-r--r--theories/ZArith/Zbool.v16
-rw-r--r--theories/ZArith/Zcomplements.v8
-rw-r--r--theories/ZArith/Zdiv.v1068
-rw-r--r--theories/ZArith/Zeven.v130
-rw-r--r--theories/ZArith/Zgcd_alt.v317
-rw-r--r--theories/ZArith/Zmax.v60
-rw-r--r--theories/ZArith/Zmin.v20
-rw-r--r--theories/ZArith/Zmisc.v29
-rw-r--r--theories/ZArith/Znat.v207
-rw-r--r--theories/ZArith/Znumtheory.v750
-rw-r--r--theories/ZArith/Zorder.v32
-rw-r--r--theories/ZArith/Zpow_facts.v465
-rw-r--r--theories/ZArith/Zpower.v126
-rw-r--r--theories/ZArith/Zsqrt.v53
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.
+
+