diff options
| author |  letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2007-11-06 02:18:53 +0000 |
|---|---|---|
| committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2007-11-06 02:18:53 +0000 |
| commit | b3f67a99cf1013343d99f7cf8036bbabb566dce0 (patch) | |
| tree | a19daf9cb9479563eb41e4f976551a8ae9e3aa49 /theories/Ints/Z | |
| parent | a17428b39d80a7da6dae16951be2b73eb0c7c4f5 (diff) | |
Integration of theories/Ints/Z/* in ZArith and large cleanup and extension of Zdiv
Some details:
- ZAux.v is the only file left in Ints/Z. The few elements that remain in it
are rather specific or compatibility oriented. Others parts and files have
been either deleted when unused or pushed into some place of ZArith.
- Ints/List/ is removed since it was not needed anymore
- Ints/Tactic.v disappear: some of its tactic were unused, some already in
Tactics.v (case_eq, f_equal instead of eq_tac), and the nice contradict
has been added to Tactics.v
- Znumtheory inherits lots of results about Zdivide, rel_prime, prime, Zgcd, ...
- A new file Zpow_facts inherits lots of results about Zpower. Placing them
into Zpower would have been difficult with respect to compatibility
(import of ring)
- A few things added to Zmax, Zabs, Znat, Zsqrt, Zeven, Zorder
- Adequate adaptations to Ints/num/* (mainly renaming of lemmas)
Now, concerning Zdiv, the behavior when dividing by a negative number is now
fully proved. When this was possible, existing lemmas has been extended,
either from strictly positive to non-zero divisor, or even to arbitrary
divisor (especially when playing with Zmod). These extended lemmas are named
with the suffix _full, whereas the original restrictive lemmas are retained
for compatibility. Several lemmas now have shorter proofs (based on unicity
lemmas). Lemmas are now more or less organized by themes (division and order,
division and usual operations, etc). Three possible choices of spec for
divisions on negative numbers are presented: this Zdiv, the ocaml approach
and the remainder-always-positive approach. The ugly behavior of Zopp
with the current choice of Zdiv/Zmod is now fully covered. A embryo of
division "a la Ocaml" is given: Odiv and Omod.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10291 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/Ints/Z')
| -rw-r--r-- | theories/Ints/Z/IntsZmisc.v | 185 | ||||
| -rw-r--r-- | theories/Ints/Z/Pmod.v | 565 | ||||
| -rw-r--r-- | theories/Ints/Z/Ppow.v | 39 | ||||
| -rw-r--r-- | theories/Ints/Z/ZAux.v | 1367 | ||||
| -rw-r--r-- | theories/Ints/Z/ZDivModAux.v | 479 | ||||
| -rw-r--r-- | theories/Ints/Z/ZPowerAux.v | 203 | ||||
| -rw-r--r-- | theories/Ints/Z/ZSum.v | 321 |
7 files changed, 148 insertions, 3011 deletions
diff --git a/theories/Ints/Z/IntsZmisc.v b/theories/Ints/Z/IntsZmisc.v deleted file mode 100644 index e4dee2d4f..000000000 --- a/theories/Ints/Z/IntsZmisc.v +++ /dev/null @@ -1,185 +0,0 @@ - -(*************************************************************) -(* This file is distributed under the terms of the *) -(* GNU Lesser General Public License Version 2.1 *) -(*************************************************************) -(* Benjamin.Gregoire@inria.fr Laurent.Thery@inria.fr *) -(*************************************************************) - -Require Export ZArith. -Open Local Scope Z_scope. - -Coercion Zpos : positive >-> Z. -Coercion Z_of_N : N >-> Z. - -Lemma Zpos_plus : forall p q, Zpos (p + q) = p + q. -Proof. intros;trivial. Qed. - -Lemma Zpos_mult : forall p q, Zpos (p * q) = p * q. -Proof. intros;trivial. Qed. - -Lemma Zpos_xI_add : forall p, Zpos (xI p) = Zpos p + Zpos p + Zpos 1. -Proof. intros p;rewrite Zpos_xI;ring. Qed. - -Lemma Zpos_xO_add : forall p, Zpos (xO p) = Zpos p + Zpos p. -Proof. intros p;rewrite Zpos_xO;ring. Qed. - -Lemma Psucc_Zplus : forall p, Zpos (Psucc p) = p + 1. -Proof. intros p;rewrite Zpos_succ_morphism;unfold Zsucc;trivial. Qed. - -Hint Rewrite Zpos_xI_add Zpos_xO_add Pplus_carry_spec - Psucc_Zplus Zpos_plus : zmisc. - -Lemma Zlt_0_pos : forall p, 0 < Zpos p. -Proof. unfold Zlt;trivial. Qed. - - -Lemma Pminus_mask_carry_spec : forall p q, - Pminus_mask_carry p q = Pminus_mask p (Psucc q). -Proof. - intros p q;generalize q p;clear q p. - induction q;destruct p;simpl;try rewrite IHq;trivial. - destruct p;trivial. destruct p;trivial. -Qed. - -Hint Rewrite Pminus_mask_carry_spec : zmisc. - -Ltac zsimpl := autorewrite with zmisc. -Ltac CaseEq t := generalize (refl_equal t);pattern t at -1;case t. -Ltac generalizeclear H := generalize H;clear H. - -Lemma Pminus_mask_spec : - forall p q, - match Pminus_mask p q with - | IsNul => Zpos p = Zpos q - | IsPos k => Zpos p = q + k - | IsNeq => p < q - end. -Proof with zsimpl;auto with zarith. - induction p;destruct q;simpl;zsimpl; - match goal with - | [|- context [(Pminus_mask ?p1 ?q1)]] => - assert (H1 := IHp q1);destruct (Pminus_mask p1 q1) - | _ => idtac - end;simpl ... - inversion H1 ... inversion H1 ... - rewrite Psucc_Zplus in H1 ... - clear IHp;induction p;simpl ... - rewrite IHp;destruct (Pdouble_minus_one p) ... - assert (H:= Zlt_0_pos q) ... assert (H:= Zlt_0_pos q) ... -Qed. - -Definition PminusN x y := - match Pminus_mask x y with - | IsPos k => Npos k - | _ => N0 - end. - -Lemma PminusN_le : forall x y:positive, x <= y -> Z_of_N (PminusN y x) = y - x. -Proof. - intros x y Hle;unfold PminusN. - assert (H := Pminus_mask_spec y x);destruct (Pminus_mask y x). - rewrite H;unfold Z_of_N;auto with zarith. - rewrite H;unfold Z_of_N;auto with zarith. - elimtype False;omega. -Qed. - -Lemma Ppred_Zminus : forall p, 1< Zpos p -> (p-1)%Z = Ppred p. -Proof. destruct p;simpl;trivial. intros;elimtype False;omega. Qed. - - -Open Local Scope positive_scope. - -Delimit Scope P_scope with P. -Open Local Scope P_scope. - -Definition is_lt (n m : positive) := - match (n ?= m) Eq with - | Lt => true - | _ => false - end. -Infix "?<" := is_lt (at level 70, no associativity) : P_scope. - -Lemma is_lt_spec : forall n m, if n ?< m then (n < m)%Z else (m <= n)%Z. -Proof. - intros n m; unfold is_lt, Zlt, Zle, Zcompare. - rewrite (ZC4 m n);destruct ((n ?= m) Eq);trivial;try (intro;discriminate). -Qed. - -Definition is_eq a b := - match (a ?= b) Eq with - | Eq => true - | _ => false - end. -Infix "?=" := is_eq (at level 70, no associativity) : P_scope. - -Lemma is_eq_refl : forall n, n ?= n = true. -Proof. intros n;unfold is_eq;rewrite Pcompare_refl;trivial. Qed. - -Lemma is_eq_eq : forall n m, n ?= m = true -> n = m. -Proof. - unfold is_eq;intros n m H; apply Pcompare_Eq_eq; - destruct ((n ?= m)%positive Eq);trivial;try discriminate. -Qed. - -Lemma is_eq_spec_pos : forall n m, if n ?= m then n = m else m <> n. -Proof. - intros n m; CaseEq (n ?= m);intro H. - rewrite (is_eq_eq _ _ H);trivial. - intro H1;rewrite H1 in H;rewrite is_eq_refl in H;discriminate H. -Qed. - -Lemma is_eq_spec : forall n m, if n ?= m then Zpos n = m else Zpos m <> n. -Proof. - intros n m; CaseEq (n ?= m);intro H. - rewrite (is_eq_eq _ _ H);trivial. - intro H1;inversion H1. - rewrite H2 in H;rewrite is_eq_refl in H;discriminate H. -Qed. - -Definition is_Eq a b := - match a, b with - | N0, N0 => true - | Npos a', Npos b' => a' ?= b' - | _, _ => false - end. - -Lemma is_Eq_spec : - forall n m, if is_Eq n m then Z_of_N n = m else Z_of_N m <> n. -Proof. - destruct n;destruct m;simpl;trivial;try (intro;discriminate). - apply is_eq_spec. -Qed. - -(* [times x y] return [x * y], a litle bit more efficiant *) -Fixpoint times (x y : positive) {struct y} : positive := - match x, y with - | xH, _ => y - | _, xH => x - | xO x', xO y' => xO (xO (times x' y')) - | xO x', xI y' => xO (x' + xO (times x' y')) - | xI x', xO y' => xO (y' + xO (times x' y')) - | xI x', xI y' => xI (x' + y' + xO (times x' y')) - end. - -Infix "*" := times : P_scope. - -Lemma times_Zmult : forall p q, Zpos (p * q)%P = (p * q)%Z. -Proof. - intros p q;generalize q p;clear p q. - induction q;destruct p; unfold times; try fold (times p q); - autorewrite with zmisc; try rewrite IHq; ring. -Qed. - -Fixpoint square (x:positive) : positive := - match x with - | xH => xH - | xO x => xO (xO (square x)) - | xI x => xI (xO (square x + x)) - end. - -Lemma square_Zmult : forall x, Zpos (square x) = (x * x) %Z. -Proof. - induction x as [x IHx|x IHx |];unfold square;try (fold (square x)); - autorewrite with zmisc; try rewrite IHx; ring. -Qed. diff --git a/theories/Ints/Z/Pmod.v b/theories/Ints/Z/Pmod.v deleted file mode 100644 index 1ea08b4fa..000000000 --- a/theories/Ints/Z/Pmod.v +++ /dev/null @@ -1,565 +0,0 @@ - -(*************************************************************) -(* This file is distributed under the terms of the *) -(* GNU Lesser General Public License Version 2.1 *) -(*************************************************************) -(* Benjamin.Gregoire@inria.fr Laurent.Thery@inria.fr *) -(*************************************************************) - -Require Import IntsZmisc. -Open Local Scope P_scope. - -(* [div_eucl a b] return [(q,r)] such that a = q*b + r *) -Fixpoint div_eucl (a b : positive) {struct a} : N * N := - match a with - | xH => if 1 ?< b then (0%N, 1%N) else (1%N, 0%N) - | xO a' => - let (q, r) := div_eucl a' b in - match q, r with - | N0, N0 => (0%N, 0%N) (* n'arrive jamais *) - | N0, Npos r => - if (xO r) ?< b then (0%N, Npos (xO r)) - else (1%N,PminusN (xO r) b) - | Npos q, N0 => (Npos (xO q), 0%N) - | Npos q, Npos r => - if (xO r) ?< b then (Npos (xO q), Npos (xO r)) - else (Npos (xI q),PminusN (xO r) b) - end - | xI a' => - let (q, r) := div_eucl a' b in - match q, r with - | N0, N0 => (0%N, 0%N) (* Impossible *) - | N0, Npos r => - if (xI r) ?< b then (0%N, Npos (xI r)) - else (1%N,PminusN (xI r) b) - | Npos q, N0 => if 1 ?< b then (Npos (xO q), 1%N) else (Npos (xI q), 0%N) - | Npos q, Npos r => - if (xI r) ?< b then (Npos (xO q), Npos (xI r)) - else (Npos (xI q),PminusN (xI r) b) - end - end. -Infix "/" := div_eucl : P_scope. - -Open Scope Z_scope. -Opaque Zmult. -Lemma div_eucl_spec : forall a b, - Zpos a = fst (a/b)%P * b + snd (a/b)%P - /\ snd (a/b)%P < b. -Proof with zsimpl;try apply Zlt_0_pos;try ((ring;fail) || omega). - intros a b;generalize a;clear a;induction a;simpl;zsimpl; - try (case IHa;clear IHa;repeat rewrite Zmult_0_l;zsimpl;intros H1 H2; - try rewrite H1; destruct (a/b)%P as [q r]; - destruct q as [|q];destruct r as [|r];simpl in *; - generalize H1 H2;clear H1 H2);repeat rewrite Zmult_0_l; - repeat rewrite Zplus_0_r; - zsimpl;simpl;intros; - match goal with - | [H : Zpos _ = 0 |- _] => discriminate H - | [|- context [ ?xx ?< b ]] => - assert (H3 := is_lt_spec xx b);destruct (xx ?< b) - | _ => idtac - end;simpl;try assert(H4 := Zlt_0_pos r);split;repeat rewrite Zplus_0_r; - try (generalize H3;zsimpl;intros); - try (rewrite PminusN_le;trivial) ... - assert (Zpos b = 1) ... rewrite H ... - assert (H4 := Zlt_0_pos b); assert (Zpos b = 1) ... -Qed. -Transparent Zmult. - -(******** Definition du modulo ************) - -(* [mod a b] return [a] modulo [b] *) -Fixpoint Pmod (a b : positive) {struct a} : N := - match a with - | xH => if 1 ?< b then 1%N else 0%N - | xO a' => - let r := Pmod a' b in - match r with - | N0 => 0%N - | Npos r' => - if (xO r') ?< b then Npos (xO r') - else PminusN (xO r') b - end - | xI a' => - let r := Pmod a' b in - match r with - | N0 => if 1 ?< b then 1%N else 0%N - | Npos r' => - if (xI r') ?< b then Npos (xI r') - else PminusN (xI r') b - end - end. - -Infix "mod" := Pmod (at level 40, no associativity) : P_scope. -Open Local Scope P_scope. - -Lemma Pmod_div_eucl : forall a b, a mod b = snd (a/b). -Proof with auto. - intros a b;generalize a;clear a;induction a;simpl; - try (rewrite IHa; - assert (H1 := div_eucl_spec a b); destruct (a/b) as [q r]; - destruct q as [|q];destruct r as [|r];simpl in *; - match goal with - | [|- context [ ?xx ?< b ]] => - assert (H2 := is_lt_spec xx b);destruct (xx ?< b) - | _ => idtac - end;simpl) ... - destruct H1 as [H3 H4];discriminate H3. - destruct (1 ?< b);simpl ... -Qed. - -Lemma mod1: forall a, a mod 1 = 0%N. -Proof. induction a;simpl;try rewrite IHa;trivial. Qed. - -Lemma mod_a_a_0 : forall a, a mod a = N0. -Proof. - intros a;generalize (div_eucl_spec a a);rewrite <- Pmod_div_eucl. - destruct (fst (a / a));unfold Z_of_N at 1. - rewrite Zmult_0_l;intros (H1,H2);elimtype False;omega. - assert (a<=p*a). - pattern (Zpos a) at 1;rewrite <- (Zmult_1_l a). - assert (H1:= Zlt_0_pos p);assert (H2:= Zle_0_pos a); - apply Zmult_le_compat;trivial;try omega. - destruct (a mod a)%P;auto with zarith. - unfold Z_of_N;assert (H1:= Zlt_0_pos p0);intros (H2,H3);elimtype False;omega. -Qed. - -Lemma mod_le_2r : forall (a b r: positive) (q:N), - Zpos a = b*q + r -> b <= a -> r < b -> 2*r <= a. -Proof. - intros a b r q H0 H1 H2. - assert (H3:=Zlt_0_pos a). assert (H4:=Zlt_0_pos b). assert (H5:=Zlt_0_pos r). - destruct q as [|q]. rewrite Zmult_0_r in H0. elimtype False;omega. - assert (H6:=Zlt_0_pos q). unfold Z_of_N in H0. - assert (Zpos r = a - b*q). omega. - simpl;zsimpl. pattern r at 2;rewrite H. - assert (b <= b * q). - pattern (Zpos b) at 1;rewrite <- (Zmult_1_r b). - apply Zmult_le_compat;try omega. - apply Zle_trans with (a - b * q + b). omega. - apply Zle_trans with (a - b + b);omega. -Qed. - -Lemma mod_lt : forall a b r, a mod b = Npos r -> r < b. -Proof. - intros a b r H;generalize (div_eucl_spec a b);rewrite <- Pmod_div_eucl; - rewrite H;simpl;intros (H1,H2);omega. -Qed. - -Lemma mod_le : forall a b r, a mod b = Npos r -> r <= b. -Proof. intros a b r H;assert (H1:= mod_lt _ _ _ H);omega. Qed. - -Lemma mod_le_a : forall a b r, a mod b = r -> r <= a. -Proof. - intros a b r H;generalize (div_eucl_spec a b);rewrite <- Pmod_div_eucl; - rewrite H;simpl;intros (H1,H2). - assert (0 <= fst (a / b) * b). - destruct (fst (a / b));simpl;auto with zarith. - auto with zarith. -Qed. - -Lemma lt_mod : forall a b, Zpos a < Zpos b -> (a mod b)%P = Npos a. -Proof. - intros a b H; rewrite Pmod_div_eucl. case (div_eucl_spec a b). - assert (0 <= snd(a/b)). destruct (snd(a/b));simpl;auto with zarith. - destruct (fst (a/b)). - unfold Z_of_N at 1;rewrite Zmult_0_l;rewrite Zplus_0_l. - destruct (snd (a/b));simpl; intros H1 H2;inversion H1;trivial. - unfold Z_of_N at 1;assert (b <= p*b). - pattern (Zpos b) at 1; rewrite <- (Zmult_1_l (Zpos b)). - assert (H1 := Zlt_0_pos p);apply Zmult_le_compat;try omega. - apply Zle_0_pos. - intros;elimtype False;omega. -Qed. - -Fixpoint gcd_log2 (a b c:positive) {struct c}: option positive := - match a mod b with - | N0 => Some b - | Npos r => - match b mod r, c with - | N0, _ => Some r - | Npos r', xH => None - | Npos r', xO c' => gcd_log2 r r' c' - | Npos r', xI c' => gcd_log2 r r' c' - end - end. - -Fixpoint egcd_log2 (a b c:positive) {struct c}: - option (Z * Z * positive) := - match a/b with - | (_, N0) => Some (0, 1, b) - | (q, Npos r) => - match b/r, c with - | (_, N0), _ => Some (1, -q, r) - | (q', Npos r'), xH => None - | (q', Npos r'), xO c' => - match egcd_log2 r r' c' with - None => None - | Some (u', v', w') => - let u := u' - v' * q' in - Some (u, v' - q * u, w') - end - | (q', Npos r'), xI c' => - match egcd_log2 r r' c' with - None => None - | Some (u', v', w') => - let u := u' - v' * q' in - Some (u, v' - q * u, w') - end - end - end. - -Lemma egcd_gcd_log2: forall c a b, - match egcd_log2 a b c, gcd_log2 a b c with - None, None => True - | Some (u,v,r), Some r' => r = r' - | _, _ => False - end. -induction c; simpl; auto; try - (intros a b; generalize (Pmod_div_eucl a b); case (a/b); simpl; - intros q r1 H; subst; case (a mod b); auto; - intros r; generalize (Pmod_div_eucl b r); case (b/r); simpl; - intros q' r1 H; subst; case (b mod r); auto; - intros r'; generalize (IHc r r'); case egcd_log2; auto; - intros ((p1,p2),p3); case gcd_log2; auto). -Qed. - -Ltac rw l := - match l with - | (?r, ?r1) => - match type of r with - True => rewrite <- r1 - | _ => rw r; rw r1 - end - | ?r => rewrite r - end. - -Lemma egcd_log2_ok: forall c a b, - match egcd_log2 a b c with - None => True - | Some (u,v,r) => u * a + v * b = r - end. -induction c; simpl; auto; - intros a b; generalize (div_eucl_spec a b); case (a/b); - simpl fst; simpl snd; intros q r1; case r1; try (intros; ring); - simpl; intros r (Hr1, Hr2); clear r1; - generalize (div_eucl_spec b r); case (b/r); - simpl fst; simpl snd; intros q' r1; case r1; - try (intros; rewrite Hr1; ring); - simpl; intros r' (Hr'1, Hr'2); clear r1; auto; - generalize (IHc r r'); case egcd_log2; auto; - intros ((u',v'),w'); case gcd_log2; auto; intros; - rw ((I, H), Hr1, Hr'1); ring. -Qed. - - -Fixpoint log2 (a:positive) : positive := - match a with - | xH => xH - | xO a => Psucc (log2 a) - | xI a => Psucc (log2 a) - end. - -Lemma gcd_log2_1: forall a c, gcd_log2 a xH c = Some xH. -Proof. destruct c;simpl;try rewrite mod1;trivial. Qed. - -Lemma log2_Zle :forall a b, Zpos a <= Zpos b -> log2 a <= log2 b. -Proof with zsimpl;try omega. - induction a;destruct b;zsimpl;intros;simpl ... - assert (log2 a <= log2 b) ... apply IHa ... - assert (log2 a <= log2 b) ... apply IHa ... - assert (H1 := Zlt_0_pos a);elimtype False;omega. - assert (log2 a <= log2 b) ... apply IHa ... - assert (log2 a <= log2 b) ... apply IHa ... - assert (H1 := Zlt_0_pos a);elimtype False;omega. - assert (H1 := Zlt_0_pos (log2 b)) ... - assert (H1 := Zlt_0_pos (log2 b)) ... -Qed. - -Lemma log2_1_inv : forall a, Zpos (log2 a) = 1 -> a = xH. -Proof. - destruct a;simpl;zsimpl;intros;trivial. - assert (H1:= Zlt_0_pos (log2 a));elimtype False;omega. - assert (H1:= Zlt_0_pos (log2 a));elimtype False;omega. -Qed. - -Lemma mod_log2 : - forall a b r:positive, a mod b = Npos r -> b <= a -> log2 r + 1 <= log2 a. -Proof. - intros; cut (log2 (xO r) <= log2 a). simpl;zsimpl;trivial. - apply log2_Zle. - replace (Zpos (xO r)) with (2 * r)%Z;trivial. - generalize (div_eucl_spec a b);rewrite <- Pmod_div_eucl;rewrite H. - rewrite Zmult_comm;intros [H1 H2];apply mod_le_2r with b (fst (a/b));trivial. -Qed. - -Lemma gcd_log2_None_aux : - forall c a b, Zpos b <= Zpos a -> log2 b <= log2 c -> - gcd_log2 a b c <> None. -Proof. - induction c;simpl;intros; - (CaseEq (a mod b);[intros Heq|intros r Heq];try (intro;discriminate)); - (CaseEq (b mod r);[intros Heq'|intros r' Heq'];try (intro;discriminate)). - apply IHc. apply mod_le with b;trivial. - generalize H0 (mod_log2 _ _ _ Heq' (mod_le _ _ _ Heq));zsimpl;intros;omega. - apply IHc. apply mod_le with b;trivial. - generalize H0 (mod_log2 _ _ _ Heq' (mod_le _ _ _ Heq));zsimpl;intros;omega. - assert (Zpos (log2 b) = 1). - assert (H1 := Zlt_0_pos (log2 b));omega. - rewrite (log2_1_inv _ H1) in Heq;rewrite mod1 in Heq;discriminate Heq. -Qed. - -Lemma gcd_log2_None : forall a b, Zpos b <= Zpos a -> gcd_log2 a b b <> None. -Proof. intros;apply gcd_log2_None_aux;auto with zarith. Qed. - -Lemma gcd_log2_Zle : - forall c1 c2 a b, log2 c1 <= log2 c2 -> - gcd_log2 a b c1 <> None -> gcd_log2 a b c2 = gcd_log2 a b c1. -Proof with zsimpl;trivial;try omega. - induction c1;destruct c2;simpl;intros; - (destruct (a mod b) as [|r];[idtac | destruct (b mod r)]) ... - apply IHc1;trivial. generalize H;zsimpl;intros;omega. - apply IHc1;trivial. generalize H;zsimpl;intros;omega. - elim H;destruct (log2 c1);trivial. - apply IHc1;trivial. generalize H;zsimpl;intros;omega. - apply IHc1;trivial. generalize H;zsimpl;intros;omega. - elim H;destruct (log2 c1);trivial. - elim H0;trivial. elim H0;trivial. -Qed. - -Lemma gcd_log2_Zle_log : - forall a b c, log2 b <= log2 c -> Zpos b <= Zpos a -> - gcd_log2 a b c = gcd_log2 a b b. -Proof. - intros a b c H1 H2; apply gcd_log2_Zle; trivial. - apply gcd_log2_None; trivial. -Qed. - -Lemma gcd_log2_mod0 : - forall a b c, a mod b = N0 -> gcd_log2 a b c = Some b. -Proof. intros a b c H;destruct c;simpl;rewrite H;trivial. Qed. - - -Require Import Zwf. - -Lemma Zwf_pos : well_founded (fun x y => Zpos x < Zpos y). -Proof. - unfold well_founded. - assert (forall x a ,x = Zpos a -> Acc (fun x y : positive => x < y) a). - intros x;assert (Hacc := Zwf_well_founded 0 x);induction Hacc;intros;subst x. - constructor;intros. apply H0 with (Zpos y);trivial. - split;auto with zarith. - intros a;apply H with (Zpos a);trivial. -Qed. - -Opaque Pmod. -Lemma gcd_log2_mod : forall a b, Zpos b <= Zpos a -> - forall r, a mod b = Npos r -> gcd_log2 a b b = gcd_log2 b r r. -Proof. - intros a b;generalize a;clear a; assert (Hacc := Zwf_pos b). - induction Hacc; intros a Hle r Hmod. - rename x into b. destruct b;simpl;rewrite Hmod. - CaseEq (xI b mod r)%P;intros. rewrite gcd_log2_mod0;trivial. - assert (H2 := mod_le _ _ _ H1);assert (H3 := mod_lt _ _ _ Hmod); - assert (H4 := mod_le _ _ _ Hmod). - rewrite (gcd_log2_Zle_log r p b);trivial. - symmetry;apply H0;trivial. - generalize (mod_log2 _ _ _ H1 H4);simpl;zsimpl;intros;omega. - CaseEq (xO b mod r)%P;intros. rewrite gcd_log2_mod0;trivial. - assert (H2 := mod_le _ _ _ H1);assert (H3 := mod_lt _ _ _ Hmod); - assert (H4 := mod_le _ _ _ Hmod). - rewrite (gcd_log2_Zle_log r p b);trivial. - symmetry;apply H0;trivial. - generalize (mod_log2 _ _ _ H1 H4);simpl;zsimpl;intros;omega. - rewrite mod1 in Hmod;discriminate Hmod. -Qed. - -Lemma gcd_log2_xO_Zle : - forall a b, Zpos b <= Zpos a -> gcd_log2 a b (xO b) = gcd_log2 a b b. -Proof. - intros a b Hle;apply gcd_log2_Zle. - simpl;zsimpl;auto with zarith. - apply gcd_log2_None_aux;auto with zarith. -Qed. - -Lemma gcd_log2_xO_Zlt : - forall a b, Zpos a < Zpos b -> gcd_log2 a b (xO b) = gcd_log2 b a a. -Proof. - intros a b H;simpl. assert (Hlt := Zlt_0_pos a). - assert (H0 := lt_mod _ _ H). - rewrite H0;simpl. - CaseEq (b mod a)%P;intros;simpl. - symmetry;apply gcd_log2_mod0;trivial. - assert (H2 := mod_lt _ _ _ H1). - rewrite (gcd_log2_Zle_log a p b);auto with zarith. - symmetry;apply gcd_log2_mod;auto with zarith. - apply log2_Zle. - replace (Zpos p) with (Z_of_N (Npos p));trivial. - apply mod_le_a with a;trivial. -Qed. - -Lemma gcd_log2_x0 : forall a b, gcd_log2 a b (xO b) <> None. -Proof. - intros;simpl;CaseEq (a mod b)%P;intros. intro;discriminate. - CaseEq (b mod p)%P;intros. intro;discriminate. - assert (H1 := mod_le_a _ _ _ H0). unfold Z_of_N in H1. - assert (H2 := mod_le _ _ _ H0). - apply gcd_log2_None_aux. trivial. - apply log2_Zle. trivial. -Qed. - -Lemma egcd_log2_x0 : forall a b, egcd_log2 a b (xO b) <> None. -Proof. -intros a b H; generalize (egcd_gcd_log2 (xO b) a b) (gcd_log2_x0 a b); - rw H; case gcd_log2; auto. -Qed. - -Definition gcd a b := - match gcd_log2 a b (xO b) with - | Some p => p - | None => (* can not appear *) 1%positive - end. - -Definition egcd a b := - match egcd_log2 a b (xO b) with - | Some p => p - | None => (* can not appear *) (1,1,1%positive) - end. - - -Lemma gcd_mod0 : forall a b, (a mod b)%P = N0 -> gcd a b = b. -Proof. - intros a b H;unfold gcd. - pattern (gcd_log2 a b (xO b)) at 1; - rewrite (gcd_log2_mod0 _ _ (xO b) H);trivial. -Qed. - -Lemma gcd1 : forall a, gcd a xH = xH. -Proof. intros a;rewrite gcd_mod0;[trivial|apply mod1]. Qed. - -Lemma gcd_mod : forall a b r, (a mod b)%P = Npos r -> - gcd a b = gcd b r. -Proof. - intros a b r H;unfold gcd. - assert (log2 r <= log2 (xO r)). simpl;zsimpl;omega. - assert (H1 := mod_lt _ _ _ H). - pattern (gcd_log2 b r (xO r)) at 1; rewrite gcd_log2_Zle_log;auto with zarith. - destruct (Z_lt_le_dec a b). - pattern (gcd_log2 a b (xO b)) at 1; rewrite gcd_log2_xO_Zlt;trivial. - rewrite (lt_mod _ _ z) in H;inversion H. - assert (r <= b). omega. - generalize (gcd_log2_None _ _ H2). - destruct (gcd_log2 b r r);intros;trivial. - assert (log2 b <= log2 (xO b)). simpl;zsimpl;omega. - pattern (gcd_log2 a b (xO b)) at 1; rewrite gcd_log2_Zle_log;auto with zarith. - pattern (gcd_log2 a b b) at 1;rewrite (gcd_log2_mod _ _ z _ H). - assert (r <= b). omega. - generalize (gcd_log2_None _ _ H3). - destruct (gcd_log2 b r r);intros;trivial. -Qed. - -Require Import ZArith. -Require Import Znumtheory. - -Hint Rewrite Zpos_mult times_Zmult square_Zmult Psucc_Zplus: zmisc. - -Ltac mauto := - trivial;autorewrite with zmisc;trivial;auto with zarith. - -Lemma gcd_Zis_gcd : forall a b:positive, (Zis_gcd b a (gcd b a)%P). -Proof with mauto. - intros a;assert (Hacc := Zwf_pos a);induction Hacc;rename x into a;intros. - generalize (div_eucl_spec b a)... - rewrite <- (Pmod_div_eucl b a). - CaseEq (b mod a)%P;[intros Heq|intros r Heq]; intros (H1,H2). - simpl in H1;rewrite Zplus_0_r in H1. - rewrite (gcd_mod0 _ _ Heq). - constructor;mauto. - apply Zdivide_intro with (fst (b/a)%P);trivial. - rewrite (gcd_mod _ _ _ Heq). - rewrite H1;apply Zis_gcd_sym. - rewrite Zmult_comm;apply Zis_gcd_for_euclid2;simpl in *. - apply Zis_gcd_sym;auto. -Qed. - -Lemma egcd_Zis_gcd : forall a b:positive, - let (uv,w) := egcd a b in - let (u,v) := uv in - u * a + v * b = w /\ (Zis_gcd b a w). -Proof with mauto. - intros a b; unfold egcd. - generalize (egcd_log2_ok (xO b) a b) (egcd_gcd_log2 (xO b) a b) - (egcd_log2_x0 a b) (gcd_Zis_gcd b a); unfold egcd, gcd. - case egcd_log2; try (intros ((u,v),w)); case gcd_log2; - try (intros; match goal with H: False |- _ => case H end); - try (intros _ _ H1; case H1; auto; fail). - intros; subst; split; try apply Zis_gcd_sym; auto. -Qed. - -Definition Zgcd a b := - match a, b with - | Z0, _ => b - | _, Z0 => a - | Zpos a, Zneg b => Zpos (gcd a b) - | Zneg a, Zpos b => Zpos (gcd a b) - | Zpos a, Zpos b => Zpos (gcd a b) - | Zneg a, Zneg b => Zpos (gcd a b) - end. - - -Lemma Zgcd_is_gcd : forall x y, Zis_gcd x y (Zgcd x y). -Proof. - destruct x;destruct y;simpl. - apply Zis_gcd_0. - apply Zis_gcd_sym;apply Zis_gcd_0. - apply Zis_gcd_sym;apply Zis_gcd_0. - apply Zis_gcd_0. - apply gcd_Zis_gcd. - apply Zis_gcd_sym;apply Zis_gcd_minus;simpl;apply gcd_Zis_gcd. - apply Zis_gcd_0. - apply Zis_gcd_minus;simpl;apply Zis_gcd_sym;apply gcd_Zis_gcd. - apply Zis_gcd_minus;apply Zis_gcd_minus;simpl;apply gcd_Zis_gcd. -Qed. - -Definition Zegcd a b := - match a, b with - | Z0, Z0 => (0,0,0) - | Zpos _, Z0 => (1,0,a) - | Zneg _, Z0 => (-1,0,-a) - | Z0, Zpos _ => (0,1,b) - | Z0, Zneg _ => (0,-1,-b) - | Zpos a, Zneg b => - match egcd a b with (u,v,w) => (u,-v, Zpos w) end - | Zneg a, Zpos b => - match egcd a b with (u,v,w) => (-u,v, Zpos w) end - | Zpos a, Zpos b => - match egcd a b with (u,v,w) => (u,v, Zpos w) end - | Zneg a, Zneg b => - match egcd a b with (u,v,w) => (-u,-v, Zpos w) end - end. - -Lemma Zegcd_is_egcd : forall x y, - match Zegcd x y with - (u,v,w) => u * x + v * y = w /\ Zis_gcd x y w /\ 0 <= w - end. -Proof. - assert (zx0: forall x, Zneg x = -x). - simpl; auto. - assert (zx1: forall x, -(-x) = x). - intro x; case x; simpl; auto. - destruct x;destruct y;simpl; try (split; [idtac|split]); - auto; try (red; simpl; intros; discriminate); - try (rewrite zx0; apply Zis_gcd_minus; try rewrite zx1; auto; - apply Zis_gcd_minus; try rewrite zx1; simpl; auto); - try apply Zis_gcd_0; try (apply Zis_gcd_sym;apply Zis_gcd_0); - generalize (egcd_Zis_gcd p p0); case egcd; intros (u,v,w) (H1, H2); - split; repeat rewrite zx0; try (rewrite <- H1; ring); auto; - (split; [idtac | red; intros; discriminate]). - apply Zis_gcd_sym; auto. - apply Zis_gcd_sym; apply Zis_gcd_minus; rw zx1; - apply Zis_gcd_sym; auto. - apply Zis_gcd_minus; rw zx1; auto. - apply Zis_gcd_minus; rw zx1; auto. - apply Zis_gcd_minus; rw zx1; auto. - apply Zis_gcd_sym; auto. -Qed. diff --git a/theories/Ints/Z/Ppow.v b/theories/Ints/Z/Ppow.v deleted file mode 100644 index b4e4ca5ef..000000000 --- a/theories/Ints/Z/Ppow.v +++ /dev/null @@ -1,39 +0,0 @@ -Require Import ZArith. -Require Import ZAux. - -Open Scope Z_scope. - -Fixpoint Ppow a z {struct z}:= - match z with - xH => a - | xO z1 => let v := Ppow a z1 in (Pmult v v) - | xI z1 => let v := Ppow a z1 in (Pmult a (Pmult v v)) - end. - -Theorem Ppow_correct: forall a z, - Zpos (Ppow a z) = (Zpos a) ^ (Zpos z). -intros a z; elim z; simpl Ppow; auto; - try (intros z1 Hrec; repeat rewrite Zpos_mult_morphism; rewrite Hrec). - rewrite Zpos_xI; rewrite Zpower_exp; auto with zarith. - rewrite Zpower_exp_1; rewrite (Zmult_comm 2); - try rewrite Zpower_mult; auto with zarith. - change 2 with (1 + 1); rewrite Zpower_exp; auto with zarith. - rewrite Zpower_exp_1; rewrite Zmult_comm; auto. - apply Zle_ge; auto with zarith. - rewrite Zpos_xO; rewrite (Zmult_comm 2); - rewrite Zpower_mult; auto with zarith. - change 2 with (1 + 1); rewrite Zpower_exp; auto with zarith. - rewrite Zpower_exp_1; auto. - rewrite Zpower_exp_1; auto. -Qed. - -Theorem Ppow_plus: forall a z1 z2, - Ppow a (z1 + z2) = ((Ppow a z1) * (Ppow a z2))%positive. -intros a z1 z2. - assert (tmp: forall x y, Zpos x = Zpos y -> x = y). - intros x y H; injection H; auto. - apply tmp. - rewrite Zpos_mult_morphism; repeat rewrite Ppow_correct. - rewrite Zpos_plus_distr; rewrite Zpower_exp; auto; red; simpl; - intros; discriminate. -Qed. diff --git a/theories/Ints/Z/ZAux.v b/theories/Ints/Z/ZAux.v index 83337ee50..8e4b1d64f 100644 --- a/theories/Ints/Z/ZAux.v +++ b/theories/Ints/Z/ZAux.v @@ -15,8 +15,13 @@ Require Import ArithRing. Require Export ZArith. Require Export Znumtheory. -Require Export Tactic. -(* Require Import MOmega. *) +Require Export Zpow_facts. + +(* *** Nota Bene *** + All results that were general enough has been moved in ZArith. + Only remain here specialized lemmas and compatibility elements. + (P.L. 5/11/2007). +*) Open Local Scope Z_scope. @@ -35,51 +40,18 @@ Hint Extern 2 (Zlt _ _) => | H: _ < ?p |- _ <= ?p => apply Zle_lt_trans with (2 := H) end). + +Hint Resolve Zlt_gt Zle_ge Z_div_pos: zarith. + (************************************** Properties of order and product **************************************) -Theorem Zmult_interval: forall p q, 0 < p * q -> 1 < p -> 0 < q < p * q. -intros p q H1 H2; assert (0 < q). -case (Zle_or_lt q 0); auto; intros H3; contradict H1; apply Zle_not_lt. -rewrite <- (Zmult_0_r p). -apply Zmult_le_compat_l; auto with zarith. -split; auto. -pattern q at 1; rewrite <- (Zmult_1_l q). -apply Zmult_lt_compat_r; auto with zarith. -Qed. - -Theorem Zmult_lt_compat: forall n m p q : Z, 0 < n <= p -> 0 < m < q -> n * m < p * q. -intros n m p q (H1, H2) (H3, H4). -apply Zle_lt_trans with (p * m). -apply Zmult_le_compat_r; auto with zarith. -apply Zmult_lt_compat_l; auto with zarith. -Qed. - -Theorem Zle_square_mult: forall a b, 0 <= a <= b -> a * a <= b * b. -intros a b (H1, H2); apply Zle_trans with (a * b); auto with zarith. -Qed. - -Theorem Zlt_square_mult: forall a b, 0 <= a < b -> a * a < b * b. -intros a b (H1, H2); apply Zle_lt_trans with (a * b); auto with zarith. -apply Zmult_lt_compat_r; auto with zarith. -Qed. - -Theorem Zlt_square_mult_inv: forall a b, 0 <= a -> 0 <= b -> a * a < b * b -> a < b. -intros a b H1 H2 H3; case (Zle_or_lt b a); auto; intros H4; apply Zmult_lt_reg_r with a; - contradict H3; apply Zle_not_lt; apply Zle_square_mult; auto. -Qed. - - -Theorem Zpower_2: forall x, x^2 = x * x. -intros; ring. -Qed. - Theorem beta_lex: forall a b c d beta, a * beta + b <= c * beta + d -> 0 <= b < beta -> 0 <= d < beta -> a <= c. -Proof. + Proof. intros a b c d beta H1 (H3, H4) (H5, H6). assert (a - c < 1); auto with zarith. apply Zmult_lt_reg_r with beta; auto with zarith. @@ -175,1203 +147,161 @@ Theorem mult_add_ineq3: forall x y c cross beta, apply Zle_trans with (1*beta+cross);auto with zarith. Qed. - -(************************************** - Properties of Z_nat - **************************************) - -Theorem inj_eq_inv: forall (n m : nat), Z_of_nat n = Z_of_nat m -> n = m. -intros n m H1; case (le_or_lt n m); auto with arith. -intros H2; case (le_lt_or_eq _ _ H2); auto; intros H3. -contradict H1; auto with zarith. -intros H2; contradict H1; auto with zarith. -Qed. - -Theorem inj_le_inv: forall (n m : nat), Z_of_nat n <= Z_of_nat m-> (n <= m)%nat. -intros n m H1; case (le_or_lt n m); auto with arith. -intros H2; contradict H1; auto with zarith. -Qed. - -Theorem Z_of_nat_Zabs_nat: - forall (z : Z), 0 <= z -> Z_of_nat (Zabs_nat z) = z. -intros z; case z; simpl; auto with zarith. -intros; apply sym_equal; apply Zpos_eq_Z_of_nat_o_nat_of_P; auto. -intros p H1; contradict H1; simpl; auto with zarith. -Qed. - -(************************************** - Properties of Zabs -**************************************) - -Theorem Zabs_square: forall a, a * a = Zabs a * Zabs a. -intros a; rewrite <- Zabs_Zmult; apply sym_equal; apply Zabs_eq; - auto with zarith. -case (Zle_or_lt 0%Z a); auto with zarith. -intros Ha; replace (a * a) with (- a * - a); auto with zarith. -ring. -Qed. - -(************************************** - Properties of Zabs_nat -**************************************) - -Theorem Z_of_nat_abs_le: - forall x y, x <= y -> x + Z_of_nat (Zabs_nat (y - x)) = y. -intros x y Hx1. -rewrite Z_of_nat_Zabs_nat; auto with zarith. -Qed. - -Theorem Zabs_nat_Zsucc: - forall p, 0 <= p -> Zabs_nat (Zsucc p) = S (Zabs_nat p). -intros p Hp. -apply inj_eq_inv. -rewrite inj_S; (repeat rewrite Z_of_nat_Zabs_nat); auto with zarith. -Qed. - -Theorem Zabs_nat_Z_of_nat: forall n, Zabs_nat (Z_of_nat n) = n. -intros n1; apply inj_eq_inv; rewrite Z_of_nat_Zabs_nat; auto with zarith. -Qed. - - -(************************************** - Properties Zsqrt_plain -**************************************) - -Theorem Zsqrt_plain_is_pos: forall n, 0 <= n -> 0 <= Zsqrt_plain n. -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; 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. - -Theorem Zsqrt_square_id: forall a, 0 <= a -> Zsqrt_plain (a * a) = a. -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; 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; apply Zle_not_lt; auto with zarith. -apply Zmult_le_compat; auto with zarith. -Qed. - -Theorem Zsqrt_le: - forall p q, 0 <= p <= q -> Zsqrt_plain p <= Zsqrt_plain q. -intros p q [H1 H2]; case Zle_lt_or_eq with ( 1 := H2 ); clear H2; intros H2. -2: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. +Hint Rewrite Zmult_1_r Zmult_0_r Zmult_1_l Zmult_0_l Zplus_0_l Zplus_0_r Zminus_0_r: rm10. (************************************** - Properties Zpower + Properties of Zdiv and Zmod **************************************) -Theorem Zpower_1: forall a, 0 <= a -> 1 ^ a = 1. -intros a Ha; pattern a; apply natlike_ind; auto with zarith. -intros x Hx Hx1; unfold Zsucc. -rewrite Zpower_exp; auto with zarith. -rewrite Hx1; simpl; auto. -Qed. - -Theorem Zpower_exp_0: forall a, a ^ 0 = 1. -simpl; unfold Zpower_pos; simpl; auto with zarith. -Qed. - -Theorem Zpower_exp_1: forall a, a ^ 1 = a. -simpl; unfold Zpower_pos; simpl; auto with zarith. -Qed. - -Theorem Zpower_Zabs: forall a b, Zabs (a ^ b) = (Zabs a) ^ b. -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. -eq_tac; 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. -intros p n H. -unfold Zsucc; rewrite Zpower_exp; auto with zarith. -rewrite Zpower_exp_1; apply Zmult_comm. -Qed. - -Theorem Zpower_mult: forall p q r, 0 <= q -> 0 <= r -> p ^ (q * r) = (p ^ q) ^ r. -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_exp_1; try rewrite <- Zpower_exp; try eq_tac; auto with zarith. -ring. -apply Zle_ge; replace 0 with (0 * r1); try apply Zmult_le_compat_r; auto. -Qed. - -Theorem Zpower_lt_0: forall a b: Z, 0 < a -> 0 <= b-> 0 < a ^b. -intros a b; case b; auto with zarith. -simpl; intros; auto with zarith. -2: intros p H H1; case H1; auto. -intros p H1 H; generalize H; pattern (Zpos p); apply natlike_ind; auto. -intros; case a; compute; auto. -intros p1 H2 H3 _; unfold Zsucc; rewrite Zpower_exp; simpl; auto with zarith. -apply Zmult_lt_O_compat; auto with zarith. -generalize H1; case a; compute; intros; auto; discriminate. -Qed. - -Theorem Zpower_le_monotone: forall a b c: Z, 0 < a -> 0 <= b <= c -> a ^ b <= a ^ c. -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_lt_0; auto with zarith. -apply Zlt_le_weak; apply Zpower_lt_0; auto with zarith. -Qed. - -Theorem Zpower_lt_monotone: forall a b c: Z, 1 < a -> 0 <= b < c -> a ^ b < a ^ c. -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_lt_0; auto with zarith. -assert (0 < a ^ (c - b)); auto with zarith. -apply Zpower_lt_0; auto with zarith. -apply Zlt_le_trans with (a ^1); auto with zarith. -rewrite Zpower_exp_1; auto with zarith. -apply Zpower_le_monotone; auto with zarith. -Qed. +Theorem Zmod_le_first: forall a b, 0 <= a -> 0 < b -> 0 <= a mod b <= a. + Proof. + intros a b H H1;case (Z_mod_lt a b);auto with zarith;intros H2 H3;split;auto. + case (Zle_or_lt b a); intros H4; auto with zarith. + rewrite Zmod_small; auto with zarith. + Qed. -Theorem Zpower_nat_Zpower: forall p q, 0 <= q -> p ^ q = Zpower_nat p (Zabs_nat q). -intros p1 q1; case q1; simpl. -intros _; exact (refl_equal _). -intros p2 _; apply Zpower_pos_nat. -intros p2 H1; case H1; auto. -Qed. -Theorem Zgt_pow_1 : forall n m : Z, 0 < n -> 1 < m -> 1 < m ^ n. -Proof. -intros n m H1 H2. -replace 1 with (m ^ 0) by apply Zpower_exp_0. -apply Zpower_lt_monotone; auto with zarith. -Qed. + Theorem Zmod_distr: forall a b r t, 0 <= a <= b -> 0 <= r -> 0 <= t < 2 ^a -> + (2 ^a * r + t) mod (2 ^ b) = (2 ^a * r) mod (2 ^ b) + t. + Proof. + intros a b r t (H1, H2) H3 (H4, H5). + assert (t < 2 ^ b). + apply Zlt_le_trans with (1:= H5); auto with zarith. + apply Zpower_le_monotone; auto with zarith. + rewrite Zplus_mod; auto with zarith. + rewrite Zmod_small with (a := t); auto with zarith. + apply Zmod_small; auto with zarith. + split; auto with zarith. + assert (0 <= 2 ^a * r); auto with zarith. + apply Zplus_le_0_compat; auto with zarith. + match goal with |- context [?X mod ?Y] => case (Z_mod_lt X Y) end; + auto with zarith. + pattern (2 ^ b) at 2; replace (2 ^ b) with ((2 ^ b - 2 ^a) + 2 ^ a); + try ring. + apply Zplus_le_lt_compat; auto with zarith. + replace b with ((b - a) + a); try ring. + rewrite Zpower_exp; auto with zarith. + pattern (2 ^a) at 4; rewrite <- (Zmult_1_l (2 ^a)); + try rewrite <- Zmult_minus_distr_r. + rewrite (Zmult_comm (2 ^(b - a))); rewrite Zmult_mod_distr_l; + auto with zarith. + rewrite (Zmult_comm (2 ^a)); apply Zmult_le_compat_r; auto with zarith. + match goal with |- context [?X mod ?Y] => case (Z_mod_lt X Y) end; + auto with zarith. + Qed. -(************************************** - Properties Zmod -**************************************) - -Theorem Zmod_mult: - forall a b n, 0 < n -> (a * b) mod n = ((a mod n) * (b mod n)) mod n. -intros a b n H. -pattern a at 1; rewrite (Z_div_mod_eq a n); auto with zarith. -pattern b at 1; rewrite (Z_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) + - (((n * (a / n)) * (b / n) + (b mod n) * (a / n)) + (a mod n) * (b / n)) * - n); auto with zarith. -apply Z_mod_plus; auto with zarith. -ring. -Qed. + Theorem Zmod_shift_r: + forall a b r t, 0 <= a <= b -> 0 <= r -> 0 <= t < 2 ^a -> + (r * 2 ^a + t) mod (2 ^ b) = (r * 2 ^a) mod (2 ^ b) + t. + Proof. + intros a b r t (H1, H2) H3 (H4, H5). + assert (t < 2 ^ b). + apply Zlt_le_trans with (1:= H5); auto with zarith. + apply Zpower_le_monotone; auto with zarith. + rewrite Zplus_mod; auto with zarith. + rewrite Zmod_small with (a := t); auto with zarith. + apply Zmod_small; auto with zarith. + split; auto with zarith. + assert (0 <= 2 ^a * r); auto with zarith. + apply Zplus_le_0_compat; auto with zarith. + match goal with |- context [?X mod ?Y] => case (Z_mod_lt X Y) end; + auto with zarith. + pattern (2 ^ b) at 2;replace (2 ^ b) with ((2 ^ b - 2 ^a) + 2 ^ a); try ring. + apply Zplus_le_lt_compat; auto with zarith. + replace b with ((b - a) + a); try ring. + rewrite Zpower_exp; auto with zarith. + pattern (2 ^a) at 4; rewrite <- (Zmult_1_l (2 ^a)); + try rewrite <- Zmult_minus_distr_r. + repeat rewrite (fun x => Zmult_comm x (2 ^ a)); rewrite Zmult_mod_distr_l; + auto with zarith. + apply Zmult_le_compat_l; auto with zarith. + match goal with |- context [?X mod ?Y] => case (Z_mod_lt X Y) end; + auto with zarith. + Qed. -Theorem Zmod_plus: - forall a b n, 0 < n -> (a + b) mod n = (a mod n + b mod n) mod n. -intros a b n H. -pattern a at 1; rewrite (Z_div_mod_eq a n); auto with zarith. -pattern b at 1; rewrite (Z_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); auto with zarith. -apply Z_mod_plus; auto with zarith. -ring. -Qed. + Theorem Zdiv_shift_r: + forall a b r t, 0 <= a <= b -> 0 <= r -> 0 <= t < 2 ^a -> + (r * 2 ^a + t) / (2 ^ b) = (r * 2 ^a) / (2 ^ b). + Proof. + intros a b r t (H1, H2) H3 (H4, H5). + assert (Eq: t < 2 ^ b); auto with zarith. + apply Zlt_le_trans with (1 := H5); auto with zarith. + apply Zpower_le_monotone; auto with zarith. + pattern (r * 2 ^ a) at 1; rewrite Z_div_mod_eq with (b := 2 ^ b); + auto with zarith. + rewrite <- Zplus_assoc. + rewrite <- Zmod_shift_r; auto with zarith. + rewrite (Zmult_comm (2 ^ b)); rewrite Z_div_plus_full_l; auto with zarith. + rewrite (fun x y => @Zdiv_small (x mod y)); auto with zarith. + match goal with |- context [?X mod ?Y] => case (Z_mod_lt X Y) end; + auto with zarith. + Qed. + + + Lemma shift_unshift_mod : forall n p a, + 0 <= a < 2^n -> + 0 <= p <= n -> + a * 2^p = a / 2^(n - p) * 2^n + (a*2^p) mod 2^n. + Proof. + intros n p a H1 H2. + pattern (a*2^p) at 1;replace (a*2^p) with + (a*2^p/2^n * 2^n + a*2^p mod 2^n). + 2:symmetry;rewrite (Zmult_comm (a*2^p/2^n));apply Z_div_mod_eq. + replace (a * 2 ^ p / 2 ^ n) with (a / 2 ^ (n - p));trivial. + replace (2^n) with (2^(n-p)*2^p). + symmetry;apply Zdiv_mult_cancel_r. + destruct H1;trivial. + cut (0 < 2^p); auto with zarith. + rewrite <- Zpower_exp. + replace (n-p+p) with n;trivial. ring. + omega. omega. + apply Zlt_gt. apply Zpower_gt_0;auto with zarith. + Qed. -Theorem Zmod_mod: forall a n, 0 < n -> (a mod n) mod n = a mod n. -intros a n H. -pattern a at 2; rewrite (Z_div_mod_eq a n); auto with zarith. -rewrite Zplus_comm; rewrite Zmult_comm. -apply sym_equal; apply Z_mod_plus; auto with zarith. -Qed. + Lemma div_le_0 : forall p x, 0 <= x -> 0 <= x / 2 ^ p. + Proof. + intros p x Hle;destruct (Z_le_gt_dec 0 p). + apply Zdiv_le_lower_bound;auto with zarith. + replace (2^p) with 0. + destruct x;compute;intro;discriminate. + destruct p;trivial;discriminate z. + Qed. -Theorem Zmod_def_small: forall a n, 0 <= a < n -> a mod n = a. -intros a n [H1 H2]; unfold Zmod. -generalize (Z_div_mod a n); case (Zdiv_eucl a n). -intros q r H3; case H3; clear H3; auto with zarith. -auto with zarith. -intros H4 [H5 H6]. -case (Zle_or_lt q (- 1)); intros H7. -contradict H1; apply Zlt_not_le. -subst a. -apply Zle_lt_trans with (n * - 1 + r); auto with zarith. -case (Zle_lt_or_eq 0 q); auto with zarith; intros H8. -contradict H2; apply Zle_not_lt. -apply Zle_trans with (n * 1 + r); auto with zarith. -rewrite H4; auto with zarith. -subst a; subst q; auto with zarith. -Qed. - -Theorem Zmod_minus: forall a b n, 0 < n -> (a - b) mod n = (a mod n - b mod n) mod n. -intros a b n H; 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 Zmod_plus; auto with zarith. -rewrite Zmod_mult; auto with zarith. -rewrite (fun x y => Zmod_plus x ((-1) * y)); auto with zarith. -rewrite Zmod_mult; auto with zarith. -rewrite (fun x => Zmod_mult x (b mod n)); auto with zarith. -repeat rewrite Zmod_mod; auto. -Qed. - -Theorem Zmod_Zpower: forall p q n, 0 < n -> (p ^ q) mod n = ((p mod n) ^ q) mod n. -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_exp_1; auto with zarith. -rewrite (fun x => (Zmod_mult x p)); try rewrite Rec; auto. -rewrite (fun x y => (Zmod_mult (x ^y))); try eq_tac; auto. -eq_tac; auto; apply sym_equal; apply Zmod_mod; auto with zarith. -generalize H1; case q; simpl; auto. -intros; discriminate. -Qed. - -Theorem Zmod_le: forall a n, 0 < n -> 0 <= a -> (Zmod a n) <= a. -intros a n H1 H2; case (Zle_or_lt n a); intros H3. -case (Z_mod_lt a n); auto with zarith. -rewrite Zmod_def_small; auto with zarith. -Qed. - -Lemma Zplus_mod_idemp_l: forall a b n, 0 < n -> (a mod n + b) mod n = (a + b) mod n. -Proof. -intros. rewrite Zmod_plus; auto. -rewrite Zmod_mod; auto. -symmetry; apply Zmod_plus; auto. -Qed. - -Lemma Zplus_mod_idemp_r: forall a b n, 0 < n -> (b + a mod n) mod n = (b + a) mod n. -Proof. -intros a b n H; repeat rewrite (Zplus_comm b). -apply Zplus_mod_idemp_l; auto. -Qed. - -Lemma Zminus_mod_idemp_l: forall a b n, 0 < n -> (a mod n - b) mod n = (a - b) mod n. -Proof. -intros. rewrite Zmod_minus; auto. -rewrite Zmod_mod; auto. -symmetry; apply Zmod_minus; auto. -Qed. - -Lemma Zminus_mod_idemp_r: forall a b n, 0 < n -> (a - b mod n) mod n = (a - b) mod n. -Proof. -intros. rewrite Zmod_minus; auto. -rewrite Zmod_mod; auto. -symmetry; apply Zmod_minus; auto. -Qed. - -Lemma Zmult_mod_idemp_l: forall a b n, 0 < n -> (a mod n * b) mod n = (a * b) mod n. -Proof. -intros; rewrite Zmod_mult; auto. -rewrite Zmod_mod; auto. -symmetry; apply Zmod_mult; auto. -Qed. - -Lemma Zmult_mod_idemp_r: forall a b n, 0 < n -> (b * (a mod n)) mod n = (b * a) mod n. -Proof. -intros a b n H; repeat rewrite (Zmult_comm b). -apply Zmult_mod_idemp_l; auto. -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 Zmod_plus; auto. -rewrite <- Zmult_assoc; rewrite Zmod_mult; auto. -rewrite Z_mod_same; try rewrite Zmult_0_l; auto with zarith. -rewrite (Zmod_def_small 0); auto with zarith. -rewrite Zplus_0_l; rewrite Zmod_mod; auto with zarith. -Qed. - -(** A better way to compute Zpower mod **) - -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. - -Theorem Zpow_mod_pos_Zpower_pos_correct: forall a m n, 0 < n -> Zpow_mod_pos a m n = (Zpower_pos a m) mod n. -intros a m; elim m; simpl; auto. -intros p Rec n H1; rewrite xI_succ_xO; rewrite Pplus_one_succ_r; rewrite <- Pplus_diag; auto. -repeat rewrite Zpower_pos_is_exp; auto. -repeat rewrite Rec; auto. -replace (Zpower_pos a 1) with a; auto. -2: unfold Zpower_pos; simpl; auto with zarith. -repeat rewrite (fun x => (Zmod_mult x a)); auto. -rewrite (Zmod_mult (Zpower_pos a p)); auto. -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 (Zmod_mult (Zpower_pos a p)); auto. -case (Zpower_pos a p mod n); auto. -unfold Zpower_pos; simpl; rewrite Zmult_1_r; auto with zarith. -Qed. - -Definition Zpow_mod a m n := match m with 0 => 1 | Zpos p1 => Zpow_mod_pos a p1 n | Zneg p1 => 0 end. - -Theorem Zpow_mod_Zpower_correct: forall a m n, 1 < n -> 0 <= m -> Zpow_mod a m n = (a ^ m) mod n. -intros a m n; case m; simpl. -intros; apply sym_equal; apply Zmod_def_small; auto with zarith. -intros; apply Zpow_mod_pos_Zpower_pos_correct; auto with zarith. -intros p H H1; case H1; auto. -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. - -Theorem Zmod_POS_correct: forall a b, Zmod_POS a b = (snd (Zdiv_eucl_POS a b)). -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. - -Definition Zmodd 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 Zmodd_correct: forall a b, Zmodd a b = Zmod a b. -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. - -(************************************** - Properties of Zdivide -**************************************) - -Theorem 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 Zmod_minus; auto. - rewrite H1; pattern c at 1; rewrite <- (Zmod_def_small c b); auto with zarith. - rewrite Zminus_diag; apply Zmod_def_small; auto with zarith. - subst; apply Z_mod_lt; auto with zarith. -Qed. - -Theorem 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 Zmod_plus; auto with zarith. - rewrite (Zdivide_mod (a -c) b); try rewrite Zplus_0_l; auto with zarith. - rewrite Zmod_mod; try apply Zmod_def_small; auto with zarith. -Qed. - -Theorem Zmod_closeby_eq: forall a b n, 0 <= a -> 0 <= b < n -> a - b < n -> a mod n = b -> a = b. -Proof. - intros a b n H H1 H2 H3. - case (Zle_or_lt 0 (a - b)); intros H4. - case Zle_lt_or_eq with (1 := H4); clear H4; intros H4; auto with zarith. - absurd_hyp H2; auto. - apply Zle_not_lt; apply Zdivide_le; auto with zarith. - apply Zmod_divide_minus; auto with zarith. - rewrite <- (Zmod_def_small a n); try split; auto with zarith. -Qed. - -Theorem 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_exp_1 p); rewrite <- Zpower_exp; try eq_tac; auto with zarith. -Qed. - - -(************************************** - Properties of Zis_gcd -**************************************) - -(* P.L. : See Numtheory.v *) + Lemma div_lt : forall p x y, 0 <= x < y -> x / 2^p < y. + Proof. + intros p x y H;destruct (Z_le_gt_dec 0 p). + apply Zdiv_lt_upper_bound;auto with zarith. + apply Zlt_le_trans with y;auto with zarith. + rewrite <- (Zmult_1_r y);apply Zmult_le_compat;auto with zarith. + assert (0 < 2^p);auto with zarith. + replace (2^p) with 0. + destruct x;change (0<y);auto with zarith. + destruct p;trivial;discriminate z. + Qed. -(************************************** - Properties rel_prime -**************************************) - -Theorem rel_prime_sym: forall a b, rel_prime a b -> rel_prime b a. -intros a b H; auto with zarith. -red; apply Zis_gcd_sym; auto with zarith. -Qed. - -Theorem rel_prime_le_prime: - forall a p, prime p -> 1 <= a < p -> rel_prime a p. -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. + Theorem Zgcd_div_pos a b: + (0 < b)%Z -> (0 < Zgcd a b)%Z -> (0 < b / Zgcd a b)%Z. + Proof. + intros a b Ha Hg. + case (Zle_lt_or_eq 0 (b/Zgcd a b)); auto. + apply Z_div_pos; auto with zarith. + intros H; generalize Ha. + pattern b at 1; rewrite (Zdivide_Zdiv_eq (Zgcd a b) b); auto. + rewrite <- H; auto with zarith. + assert (F := (Zgcd_is_gcd a b)); inversion F; auto. + Qed. -Definition rel_prime_dec: - forall a b, ({ rel_prime a b }) + ({ ~ rel_prime a b }). -intros a b; case (Z_eq_dec (Zgcd a b) 1); intros H1. -left; red. -rewrite <- H1; apply Zgcd_is_gcd. -right; contradict H1. -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. +(* For compatibility of scripts, weaker version of some lemmas of Zdiv *) -Theorem rel_prime_mod_rev: forall p q, 0 < q -> rel_prime (p mod q) q -> rel_prime p q. -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 rel_prime_div: forall p q r, rel_prime p q -> (r | p) -> rel_prime r q. -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. -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. -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. -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 Zrel_prime_neq_mod_0: forall a b, 1 < b -> rel_prime a b -> a mod b <> 0. +Lemma Zlt0_not_eq : forall n, 0<n -> n<>0. Proof. -intros a b H H1 H2. -case (not_rel_prime_0 _ H). -rewrite <- H2. -apply rel_prime_mod; auto with zarith. -Qed. - -Theorem rel_prime_Zpower_r: forall i p q, 0 < i -> rel_prime p q -> rel_prime p (q^i). -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_exp_0; apply rel_prime_sym; apply rel_prime_1. -Qed. - - -(************************************** - Properties prime -**************************************) - -Theorem not_prime_0: ~ prime 0. -intros H1; case (prime_divisors _ H1 2); auto with zarith. -Qed. - - -Theorem not_prime_1: ~ prime 1. -intros H1; absurd (1 < 1); auto with zarith. -inversion H1; auto. -Qed. - -Theorem prime_2: prime 2. -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. -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_le_2: forall p, prime p -> 2 <= p. -intros p Hp; inversion Hp; auto with zarith. -Qed. - -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 }). -intros p m. -case (Z_lt_dec 1 m); intros H1. -apply natlike_rec - with - ( P := - fun m => - ({ forall (n : Z), 1 < n < m -> rel_prime n p }) + - ({ exists n : Z , 1 < n < m /\ ~ rel_prime n p }) ); auto with zarith. -left; intros n [HH1 HH2]; contradict HH2; auto with zarith. -intros x Hx Rec; case Rec. -intros P1; case (rel_prime_dec x p); intros P2. -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. -intros tmp; right; case tmp; intros n [HH1 HH2]; exists n; auto with zarith. -left; intros n [HH1 HH2]; contradict H1; auto with zarith. -Defined. - -Theorem not_prime_divide: - forall p, 1 < p -> ~ prime p -> exists n, 1 < n < p /\ (n | p) . -intros p Hp Hp1. -case (prime_dec_aux p p); intros H1. -case Hp1; apply prime_intro; 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. -Defined. - -Definition prime_dec: forall p, ({ prime p }) + ({ ~ prime p }). -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 prime_def: - forall p, 1 < p -> (forall n, 1 < n < p -> ~ (n | p)) -> prime p. -intros p H1 H2. -apply prime_intro; auto. -intros n H3. -red; apply Zis_gcd_intro; auto with zarith. -intros x H4 H5. -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 (H2 (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. -cut (Zdivide (Zabs x) p). -intros [q Hq]; subst p; rewrite <- H6; auto with zarith. -apply Zdivide_Zabs_inv_l; auto. -Qed. - -Theorem prime_inv_def: forall p n, prime p -> 1 < n < p -> ~ (n | p). -intros p n H1 H2 H3. -absurd (rel_prime n p); auto. -unfold rel_prime; intros H4. -case (Zis_gcd_unique n p n 1); auto with zarith. -apply Zis_gcd_intro; auto with zarith. -inversion H1; auto with zarith. -Qed. - -Theorem square_not_prime: forall a, ~ prime (a * a). -intros a; rewrite (Zabs_square a). -case (Zle_lt_or_eq 0 (Zabs a)); auto with zarith; intros Hza1. -case (Zle_lt_or_eq 1 (Zabs a)); auto with zarith; intros Hza2. -intros Ha; case (prime_inv_def (Zabs a * Zabs a) (Zabs a)); auto. -split; auto. -pattern (Zabs a) at 1; replace (Zabs a) with (1 * Zabs a); auto with zarith. -apply Zmult_lt_compat_r; auto with zarith. -exists (Zabs a); auto. -rewrite <- Hza2; simpl; apply not_prime_1. -rewrite <- Hza1; simpl; apply not_prime_0. Qed. -Theorem prime_divide_prime_eq: - forall p1 p2, prime p1 -> prime p2 -> Zdivide p1 p2 -> p1 = p2. -intros p1 p2 Hp1 Hp2 Hp3. -assert (Ha: 1 < p1). -inversion Hp1; auto. -assert (Ha1: 1 < p2). -inversion Hp2; auto. -case (Zle_lt_or_eq p1 p2); auto with zarith. -apply Zdivide_le; auto with zarith. -intros Hp4. -case (prime_inv_def p2 p1); auto with zarith. -Qed. - -Theorem Zdivide_div_prime_le_square: forall x, 1 < x -> ~prime x -> exists p, prime p /\ (p | x) /\ p * p <= x. -intros x Hx; generalize Hx; pattern x; apply Z_lt_induction; auto with zarith. -clear x Hx; intros x Rec H H1. -case (not_prime_divide x); auto. -intros x1 ((H2, H3), H4); case (prime_dec x1); intros H5. -case (Zle_or_lt (x1 * x1) x); intros H6. -exists x1; auto. -case H4; clear H4; intros x2 H4; subst. -assert (Hx2: x2 <= x1). -case (Zle_or_lt x2 x1); auto; intros H8; contradict H6; apply Zle_not_lt. -apply Zmult_le_compat_r; auto with zarith. -case (prime_dec x2); intros H7. -exists x2; repeat (split; auto with zarith). -apply Zmult_le_compat_l; auto with zarith. -apply Zle_trans with 2%Z; try apply prime_le_2; auto with zarith. -case (Zle_or_lt 0 x2); intros H8. -case Zle_lt_or_eq with (1 := H8); auto with zarith; clear H8; intros H8; subst; auto with zarith. -case (Zle_lt_or_eq 1 x2); auto with zarith; clear H8; intros H8; subst; auto with zarith. -case (Rec x2); try split; auto with zarith. -intros x3 (H9, (H10, H11)). -exists x3; repeat (split; auto with zarith). -contradict H; apply Zle_not_lt; auto with zarith. -apply Zle_trans with (0 * x1); auto with zarith. -case (Rec x1); try split; auto with zarith. -intros x3 (H9, (H10, H11)). -exists x3; repeat (split; auto with zarith). -apply Zdivide_trans with x1; auto with zarith. -Qed. - -Theorem prime_div_prime: forall p q, prime p -> prime q -> (p | q) -> p = q. -intros p q H H1 H2; -assert (Hp: 0 < p); try apply Zlt_le_trans with 2; try apply prime_le_2; auto with zarith. -assert (Hq: 0 < q); try apply Zlt_le_trans with 2; try apply prime_le_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; apply not_prime_1. -contradict Hp; auto with zarith. -Qed. - -Theorem prime_div_Zpower_prime: forall n p q, 0 <= n -> prime p -> prime q -> (p | q ^ n) -> p = q. -intros n p q Hp Hq; generalize p q Hq; pattern n; apply natlike_ind; auto; clear n p q Hp Hq. -intros p q Hp Hq; rewrite Zpower_exp_0. -intros (r, H); subst. -case (Zmult_interval p r); auto; try rewrite Zmult_comm. -rewrite <- H; auto with zarith. -apply Zlt_le_trans with 2; try apply prime_le_2; auto with zarith. -rewrite <- H; intros H1 H2; contradict H2; auto with zarith. -intros n1 H Rec p q Hp Hq; try rewrite Zpower_Zsucc; auto with zarith; intros H1. -case prime_mult with (2 := H1); auto. -intros H2; apply prime_div_prime; auto. -Qed. - -Theorem rel_prime_Zpower: forall i j p q, 0 <= i -> 0 <= j -> rel_prime p q -> rel_prime (p^i) (q^j). -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_exp_0; 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_exp_0; apply rel_prime_sym; apply rel_prime_1. -Qed. - -Theorem prime_induction: forall (P: Z -> Prop), P 0 -> P 1 -> (forall p q, prime p -> P q -> P (p * q)) -> forall p, 0 <= p -> P p. -intros P H H1 H2 p Hp. -generalize Hp; pattern p; apply Z_lt_induction; auto; clear p Hp. -intros p Rec Hp. -case Zle_lt_or_eq with (1 := Hp); clear Hp; intros Hp; subst; auto. -case (Zle_lt_or_eq 1 p); auto with zarith; clear Hp; intros Hp; subst; auto. -case (prime_dec p); intros H3. -rewrite <- (Zmult_1_r p); apply H2; auto. - case (Zdivide_div_prime_le_square p); auto. -intros q (Hq1, ((q2, Hq2), Hq3)); subst. -case (Zmult_interval q q2). -rewrite Zmult_comm; apply Zlt_trans with 1; auto with zarith. -apply Zlt_le_trans with 2; auto with zarith; apply prime_le_2; auto. -intros H4 H5; rewrite Zmult_comm; apply H2; auto. -apply Rec; try split; auto with zarith. -rewrite Zmult_comm; auto. -Qed. - -Theorem div_power_max: forall p q, 1 < p -> 0 < q -> exists n, 0 <= n /\ (p ^n | q) /\ ~(p ^(1 + n) | q). -intros p q H1 H2; generalize H2; pattern q; apply Z_lt_induction; auto with zarith; clear q H2. -intros q Rec H2. -case (Zdivide_dec p q); intros H3. -case (Zdivide_Zdiv_lt_pos p q); auto with zarith; intros H4 H5. -case (Rec (Zdiv q p)); auto with zarith. -intros n (Ha1, (Ha2, Ha3)); exists (n + 1); split; auto with zarith; split. -case Ha2; intros q1 Hq; exists q1. -rewrite Zpower_exp; try rewrite Zpower_exp_1; auto with zarith. -rewrite Zmult_assoc; rewrite <- Hq. -rewrite Zmult_comm; apply Zdivide_Zdiv_eq; auto with zarith. -intros (q1, Hu); case Ha3; exists q1. -apply Zmult_reg_r with p; auto with zarith. -rewrite (Zmult_comm (q / p)); rewrite <- Zdivide_Zdiv_eq; auto with zarith. -apply trans_equal with (1 := Hu); repeat rewrite Zpower_exp; try rewrite Zpower_exp_1; auto with zarith. -ring. -exists 0; repeat split; try rewrite Zpower_exp_1; try rewrite Zpower_exp_0; auto with zarith. -Qed. - -Theorem prime_divide_Zpower_Zdiv: forall m a p i, 0 <= i -> prime p -> (m | a) -> ~(m | (a/p)) -> (p^i | a) -> (p^i | m). -intros m a p i Hi Hp (k, Hk) H (l, Hl); subst. -case (Zle_lt_or_eq 0 i); auto with arith; intros Hi1; subst. -assert (Hp0: 0 < p). -apply Zlt_le_trans with 2; auto with zarith; apply prime_le_2; auto. -case (Zdivide_dec p k); intros H1. -case H1; intros k' H2; subst. -case H; replace (k' * p * m) with ((k' * m) * p); try ring; rewrite Z_div_mult; auto with zarith. -apply Gauss with k. -exists l; rewrite Hl; ring. -apply rel_prime_sym; apply rel_prime_Zpower_r; auto. -apply rel_prime_sym; apply prime_rel_prime; auto. -rewrite Zpower_exp_0; apply Zone_divide. -Qed. - - -Theorem Zdivide_Zpower: forall n m, 0 < n -> (forall p i, prime p -> 0 < i -> (p^i | n) -> (p^i | m)) -> (n | m). -intros n m Hn; generalize m Hn; pattern n; apply prime_induction; auto with zarith; clear n m Hn. -intros m H1; contradict H1; auto with zarith. -intros p q H Rec m H1 H2. -assert (H3: (p | m)). -rewrite <- (Zpower_exp_1 p); apply H2; auto with zarith; rewrite Zpower_exp_1; apply Zdivide_factor_r. -case (Zmult_interval p q); auto. -apply Zlt_le_trans with 2; auto with zarith; apply prime_le_2; auto. -case H3; intros k Hk; subst. -intros Hq Hq1. -rewrite (Zmult_comm k); apply Zmult_divide_compat_l. -apply Rec; auto. -intros p1 i Hp1 Hp2 Hp3. -case (Z_eq_dec p p1); intros Hpp1; subst. -case (H2 p1 (Zsucc i)); auto with zarith. -rewrite Zpower_Zsucc; try apply Zmult_divide_compat_l; auto with zarith. -intros q2 Hq2; exists q2. -apply Zmult_reg_r with p1. -contradict H; subst; apply not_prime_0. -rewrite Hq2; rewrite Zpower_Zsucc; try ring; auto with zarith. -apply Gauss with p. -rewrite Zmult_comm; apply H2; auto. -apply Zdivide_trans with (1:= Hp3). -apply Zdivide_factor_l. -apply rel_prime_sym; apply rel_prime_Zpower_r; auto. -apply prime_rel_prime; auto. -contradict Hpp1; apply prime_divide_prime_eq; auto. -Qed. - -Theorem divide_prime_divide: - forall a n m, 0 < a -> (n | m) -> (a | m) -> - (forall p, prime p -> (p | a) -> ~(n | (m/p))) -> - (a | n). -intros a n m Ha Hnm Ham Hp. -apply Zdivide_Zpower; auto. -intros p i H1 H2 H3. -apply prime_divide_Zpower_Zdiv with m; auto with zarith. -apply Hp; auto; apply Zdivide_trans with (2 := H3); auto. -apply Zpower_divide; auto. -apply Zdivide_trans with (1 := H3); auto. -Qed. - -Theorem prime_div_induction: - forall (P: Z -> Prop) n, - 0 < n -> - (P 1) -> - (forall p i, prime p -> 0 <= i -> (p^i | n) -> P (p^i)) -> - (forall p q, rel_prime p q -> P p -> P q -> P (p * q)) -> - forall m, 0 <= m -> (m | n) -> P m. -intros P n P1 Hn H H1 m Hm. -generalize Hm; pattern m; apply Z_lt_induction; auto; clear m Hm. -intros m Rec Hm H2. -case (prime_dec m); intros Hm1. -rewrite <- Zpower_exp_1; apply H; auto with zarith. -rewrite Zpower_exp_1; auto. -case Zle_lt_or_eq with (1 := Hm); clear Hm; intros Hm; subst. -2: contradict P1; case H2; intros; subst; auto with zarith. -case (Zle_lt_or_eq 1 m); auto with zarith; clear Hm; intros Hm; subst; auto. -case Zdivide_div_prime_le_square with m; auto. -intros p (Hp1, (Hp2, Hp3)). -case (div_power_max p m); auto with zarith. -generalize (prime_le_2 p Hp1); auto with zarith. -intros i (Hi, (Hi1, Hi2)). -case Zle_lt_or_eq with (1 := Hi); clear Hi; intros Hi. -assert (Hpi: 0 < p ^ i). -apply Zpower_lt_0; auto with zarith. -apply Zlt_le_trans with 2; try apply prime_le_2; auto with zarith. -rewrite (Z_div_exact_2 m (p ^ i)); auto with zarith. -apply H1; auto with zarith. -apply rel_prime_sym; apply rel_prime_Zpower_r; auto. -apply rel_prime_sym. -apply prime_rel_prime; auto. -contradict Hi2. -case Hi1; intros; subst. -rewrite Z_div_mult in Hi2; auto with zarith. -case Hi2; intros q0 Hq0; subst. -exists q0; rewrite Zpower_exp; try rewrite Zpower_exp_1; auto with zarith. -apply H; auto with zarith. -apply Zdivide_trans with (1 := Hi1); auto. -apply Rec; auto with zarith. -split; auto with zarith. -apply Zge_le; apply Z_div_ge0; auto with zarith. -apply Z_div_lt; auto with zarith. -apply Zle_ge; apply Zle_trans with p. -apply prime_le_2; auto. -pattern p at 1; rewrite <- Zpower_exp_1; apply Zpower_le_monotone; auto with zarith. -apply Zlt_le_trans with 2; try apply prime_le_2; auto with zarith. -apply Zge_le; apply Z_div_ge0; auto with zarith. -apply Zdivide_trans with (2 := H2); auto. -exists (p ^ i); apply Z_div_exact_2; auto with zarith. -apply Zdivide_mod; auto with zarith. -apply Zdivide_mod; auto with zarith. -case Hi2; rewrite <- Hi; rewrite Zplus_0_r; rewrite Zpower_exp_1; auto. -Qed. - -(************************************** - A tail recursive way of compute a^n -**************************************) - -Fixpoint Zpower_tr_aux (z1 z2: Z) (n: nat) {struct n}: Z := - match n with O => z1 | (S n1) => Zpower_tr_aux (z2 * z1) z2 n1 end. - -Theorem Zpower_tr_aux_correct: -forall z1 z2 n p, z1 = Zpower_nat z2 p -> Zpower_tr_aux z1 z2 n = Zpower_nat z2 (p + n). -intros z1 z2 n; generalize z1; elim n; clear z1 n; simpl; auto. -intros z1 p; rewrite plus_0_r; auto. -intros n1 Rec z1 p H1. -rewrite Rec with (p:= S p). -rewrite <- plus_n_Sm; simpl; auto. -pattern z2 at 1; replace z2 with (Zpower_nat z2 1). -rewrite H1; rewrite <- Zpower_nat_is_exp; simpl; auto. -unfold Zpower_nat; simpl; rewrite Zmult_1_r; auto. -Qed. - -Definition Zpower_nat_tr := Zpower_tr_aux 1. - -Theorem Zpower_nat_tr_correct: -forall z n, Zpower_nat_tr z n = Zpower_nat z n. -intros z n; unfold Zpower_nat_tr. -rewrite Zpower_tr_aux_correct with (p := 0%nat); auto. -Qed. - - -(************************************** - Definition of Zsquare -**************************************) - -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. - -Theorem Psquare_correct: (forall p, Psquare p = p * p)%positive. -intros p; elim p; simpl; auto. -intros p1 Rec; rewrite Rec. -eq_tac. -apply trans_equal with (xO p1 + xO (p1 * p1) )%positive; auto. -rewrite (Pplus_comm (xO p1)); auto. -rewrite Pmult_xI_permute_r; rewrite Pplus_assoc. -eq_tac; auto. -apply sym_equal; apply Pplus_diag. -intros p1 Rec; rewrite Rec; simpl; auto. -eq_tac; auto. -apply sym_equal; apply Pmult_xO_permute_r. -Qed. - -Definition Zsquare p := -match p with Z0 => Z0 | Zpos p => Zpos (Psquare p) | Zneg p => Zpos (Psquare p) end. - -Theorem Zsquare_correct: forall p, Zsquare p = p * p. -intro p; case p; simpl; auto; intros p1; rewrite Psquare_correct; auto. -Qed. - -(************************************** - Some properties of Zpower -**************************************) - -Theorem prime_power_2: forall x n, 0 <= n -> prime x -> (x | 2 ^ n) -> x = 2. -intros x n H Hx; pattern n; apply natlike_ind; auto; clear n H. -rewrite Zpower_exp_0. -intros H1; absurd (x <= 1). -apply Zlt_not_le; apply Zlt_le_trans with 2%Z; auto with zarith. -apply prime_le_2; auto. -apply Zdivide_le; auto with zarith. -apply Zle_trans with 2%Z; try apply prime_le_2; auto with zarith. -intros n1 H H1. -unfold Zsucc; rewrite Zpower_exp; try rewrite Zpower_exp_1; auto with zarith. -intros H2; case prime_mult with (2 := H2); auto. -intros H3; case (Zle_lt_or_eq x 2); auto. -apply Zdivide_le; auto with zarith. -apply Zle_trans with 2%Z; try apply prime_le_2; auto with zarith. -intros H4; contradict H4; apply Zle_not_lt. -apply prime_le_2; auto with zarith. -Qed. - -Theorem Zdivide_power_2: forall x n, 0 <= n -> 0 <= x -> (x | 2 ^ n) -> exists q, x = 2 ^ q. -intros x n Hn H; generalize n H Hn; pattern x; apply Z_lt_induction; auto; clear x n H Hn. -intros x Rec n H Hn H1. -case Zle_lt_or_eq with (1 := H); auto; clear H; intros H; subst. -case (Zle_lt_or_eq 1 x); auto with zarith; clear H; intros H; subst. -case (prime_dec x); intros H2. -exists 1; simpl; apply prime_power_2 with n; auto. -case not_prime_divide with (2 := H2); auto. -intros p1 ((H3, H4), (q1, Hq1)); subst. -case (Rec p1) with n; auto with zarith. -apply Zdivide_trans with (2 := H1); exists q1; auto with zarith. -intros r1 Hr1. -case (Rec q1) with 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 H; auto with zarith. -apply Zmult_le_0_reg_r with p1; auto with zarith. -apply Zdivide_trans with (2 := H1); exists p1; auto with zarith. -intros r2 Hr2; exists (r2 + r1); subst. -apply sym_equal; apply Zpower_exp. -generalize H; case r2; simpl; auto with zarith. -intros; red; simpl; intros; discriminate. -generalize H; case r1; simpl; auto with zarith. -intros; red; simpl; intros; discriminate. -exists 0; simpl; auto. -case H1; intros q1; try rewrite Zmult_0_r; intros H2. -absurd (0 < 0); auto with zarith. -pattern 0 at 2; rewrite <- H2; auto with zarith. -apply Zpower_lt_0; auto with zarith. -Qed. - - -(************************************** - Some properties of Zodd and Zeven -**************************************) - -Theorem Zeven_ex: forall p, Zeven p -> exists q, p = 2 * q. -intros p; case p; simpl; auto. -intros _; exists 0; auto. -intros p1; case p1; try ((intros H; case H; fail) || intros z H; case H; fail). -intros p2 _; exists (Zpos p2); auto. -intros p1; case p1; try ((intros H; case H; fail) || intros z H; case H; fail). -intros p2 _; exists (Zneg p2); auto. -Qed. - -Theorem Zodd_ex: forall p, Zodd p -> exists q, p = 2 * q + 1. -intros p HH; case (Zle_or_lt 0 p); intros HH1. -exists (Zdiv2 p); apply Zodd_div2; auto with zarith. -exists ((Zdiv2 p) - 1); pattern p at 1; rewrite Zodd_div2_neg; auto with zarith. -Qed. - -Theorem Zeven_2p: forall p, Zeven (2 * p). -intros p; case p; simpl; auto. -Qed. - -Theorem Zodd_2p_plus_1: forall p, Zodd (2 * p + 1). -intros p; case p; simpl; auto. -intros p1; case p1; simpl; auto. -Qed. - -Theorem Zeven_plus_Zodd_Zodd: forall z1 z2, Zeven z1 -> Zodd z2 -> Zodd (z1 + z2). -intros z1 z2 HH1 HH2; case Zeven_ex with (1 := HH1); intros x HH3; try rewrite HH3; auto. -case Zodd_ex with (1 := HH2); intros y HH4; try rewrite HH4; auto. -replace (2 * x + (2 * y + 1)) with (2 * (x + y) + 1); try apply Zodd_2p_plus_1; auto with zarith. -Qed. - -Theorem Zeven_plus_Zeven_Zeven: forall z1 z2, Zeven z1 -> Zeven z2 -> Zeven (z1 + z2). -intros z1 z2 HH1 HH2; case Zeven_ex with (1 := HH1); intros x HH3; try rewrite HH3; auto. -case Zeven_ex with (1 := HH2); intros y HH4; try rewrite HH4; auto. -replace (2 * x + 2 * y) with (2 * (x + y)); try apply Zeven_2p; auto with zarith. -Qed. - -Theorem Zodd_plus_Zeven_Zodd: forall z1 z2, Zodd z1 -> Zeven z2 -> Zodd (z1 + z2). -intros z1 z2 HH1 HH2; rewrite Zplus_comm; apply Zeven_plus_Zodd_Zodd; auto. -Qed. - -Theorem Zodd_plus_Zodd_Zeven: forall z1 z2, Zodd z1 -> Zodd z2 -> Zeven (z1 + z2). -intros z1 z2 HH1 HH2; case Zodd_ex with (1 := HH1); intros x HH3; try rewrite HH3; auto. -case Zodd_ex with (1 := HH2); intros y HH4; try rewrite HH4; auto. -replace ((2 * x + 1) + (2 * y + 1)) with (2 * (x + y + 1)); try apply Zeven_2p; try ring. -Qed. - -Theorem Zeven_mult_Zeven_l: forall z1 z2, Zeven z1 -> Zeven (z1 * z2). -intros z1 z2 HH1; case Zeven_ex with (1 := HH1); intros x HH3; try rewrite HH3; auto. -replace (2 * x * z2) with (2 * (x * z2)); try apply Zeven_2p; auto with zarith. -Qed. - -Theorem Zeven_mult_Zeven_r: forall z1 z2, Zeven z2 -> Zeven (z1 * z2). -intros z1 z2 HH1; case Zeven_ex with (1 := HH1); intros x HH3; try rewrite HH3; auto. -replace (z1 * (2 * x)) with (2 * (x * z1)); try apply Zeven_2p; try ring. -Qed. - -Theorem Zodd_mult_Zodd_Zodd: forall z1 z2, Zodd z1 -> Zodd z2 -> Zodd (z1 * z2). -intros z1 z2 HH1 HH2; case Zodd_ex with (1 := HH1); intros x HH3; try rewrite HH3; auto. -case Zodd_ex with (1 := HH2); intros y HH4; try rewrite HH4; auto. -replace ((2 * x + 1) * (2 * y + 1)) with (2 * (2 * x * y + x + y) + 1); try apply Zodd_2p_plus_1; try ring. -Qed. - -Definition Zmult_lt_0_compat := Zmult_lt_O_compat. - -Hint Rewrite Zmult_1_r Zmult_0_r Zmult_1_l Zmult_0_l Zplus_0_l Zplus_0_r Zminus_0_r: rm10. -Hint Rewrite Zmult_plus_distr_r Zmult_plus_distr_l Zmult_minus_distr_r Zmult_minus_distr_l: distr. - -Theorem Zmult_lt_compat_bis: - forall n m p q : Z, 0 <= n < p -> 0 <= m < q -> n * m < p * q. -intros n m p q (H1, H2) (H3,H4). -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; autorewrite with rm10; apply Zmult_lt_0_compat; auto with zarith. -rewrite <- H5; autorewrite with rm10; apply Zmult_lt_0_compat; auto with zarith. -Qed. - - -Theorem nat_of_P_xO: - forall p, nat_of_P (xO p) = (2 * nat_of_P p)%nat. -intros p; unfold nat_of_P; simpl; rewrite Pmult_nat_2_mult_2_permute; auto with arith. -Qed. - -Theorem nat_of_P_xI: - forall p, nat_of_P (xI p) = (2 * nat_of_P p + 1)%nat. -intros p; unfold nat_of_P; simpl; rewrite Pmult_nat_2_mult_2_permute; auto with arith. -ring. -Qed. - -Theorem nat_of_P_xH: nat_of_P xH = 1%nat. -trivial. -Qed. - -Hint Rewrite - nat_of_P_xO nat_of_P_xI nat_of_P_xH - nat_of_P_succ_morphism - nat_of_P_plus_carry_morphism - nat_of_P_plus_morphism - nat_of_P_mult_morphism - nat_of_P_minus_morphism: pos_morph. - -Ltac pos_tac := - match goal with |- ?X = ?Y => - assert (tmp: Zpos X = Zpos Y); - [idtac; repeat rewrite Zpos_eq_Z_of_nat_o_nat_of_P; eq_tac | injection tmp; auto] - end; autorewrite with pos_morph. - -(************************************** - Bounded induction -**************************************) +Definition Zdiv_mult_cancel_r a b c H := Zdiv.Zdiv_mult_cancel_r a b c (Zlt0_not_eq _ H). +Definition Zdiv_mult_cancel_l a b c H := Zdiv.Zdiv_mult_cancel_r a b c (Zlt0_not_eq _ H). +Definition Z_div_plus_l a b c H := Zdiv.Z_div_plus_full_l a b c (Zlt0_not_eq _ H). Theorem Zbounded_induction : (forall Q : Z -> Prop, forall b : Z, @@ -1392,4 +322,3 @@ right; auto with zarith. unfold Q' in *; intros n H1 H2. destruct (H n H1) as [[H3 H4] | H3]. assumption. apply Zle_not_lt in H3. false_hyp H2 H3. Qed. - diff --git a/theories/Ints/Z/ZDivModAux.v b/theories/Ints/Z/ZDivModAux.v deleted file mode 100644 index 127d3cefa..000000000 --- a/theories/Ints/Z/ZDivModAux.v +++ /dev/null @@ -1,479 +0,0 @@ - -(*************************************************************) -(* This file is distributed under the terms of the *) -(* GNU Lesser General Public License Version 2.1 *) -(*************************************************************) -(* Benjamin.Gregoire@inria.fr Laurent.Thery@inria.fr *) -(*************************************************************) - -(********************************************************************** - ZDivModAux.v - - Auxillary functions & Theorems for Zdiv and Zmod - **********************************************************************) - -Require Export ZArith. -Require Export Znumtheory. -Require Export Tactic. -Require Import ZAux. -Require Import ZPowerAux. - -Open Local Scope Z_scope. - -Hint Extern 2 (Zle _ _) => - (match goal with - |- Zpos _ <= Zpos _ => exact (refl_equal _) - | H: _ <= ?p |- _ <= ?p => apply Zle_trans with (2 := H) - | H: _ < ?p |- _ <= ?p => - apply Zlt_le_weak; apply Zle_lt_trans with (2 := H) - end). - -Hint Extern 2 (Zlt _ _) => - (match goal with - |- Zpos _ < Zpos _ => exact (refl_equal _) -| H: _ <= ?p |- _ <= ?p => apply Zlt_le_trans with (2 := H) -| H: _ < ?p |- _ <= ?p => apply Zle_lt_trans with (2 := H) - end). - -Hint Resolve Zlt_gt Zle_ge: zarith. - -(************************************** - Properties Zmod -**************************************) - - Theorem Zmod_mult: - forall a b n, 0 < n -> (a * b) mod n = ((a mod n) * (b mod n)) mod n. - Proof. - intros a b n H. - pattern a at 1; rewrite (Z_div_mod_eq a n); auto with zarith. - pattern b at 1; rewrite (Z_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) + - (((n*(a/n)) * (b/n) + (b mod n)*(a / n)) + (a mod n) * (b / n)) * n); - auto with zarith. - apply Z_mod_plus; auto with zarith. - ring. - Qed. - - Theorem Zmod_plus: - forall a b n, 0 < n -> (a + b) mod n = (a mod n + b mod n) mod n. - Proof. - intros a b n H. - pattern a at 1; rewrite (Z_div_mod_eq a n); auto with zarith. - pattern b at 1; rewrite (Z_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); auto with zarith. - apply Z_mod_plus; auto with zarith. - ring. - Qed. - - Theorem Zmod_mod: forall a n, 0 < n -> (a mod n) mod n = a mod n. - Proof. - intros a n H. - pattern a at 2; rewrite (Z_div_mod_eq a n); auto with zarith. - rewrite Zplus_comm; rewrite Zmult_comm. - apply sym_equal; apply Z_mod_plus; auto with zarith. - Qed. - - Theorem Zmod_def_small: forall a n, 0 <= a < n -> a mod n = a. - Proof. - intros a n [H1 H2]; unfold Zmod. - generalize (Z_div_mod a n); case (Zdiv_eucl a n). - intros q r H3; case H3; clear H3; auto with zarith. - intros H4 [H5 H6]. - case (Zle_or_lt q (- 1)); intros H7. - contradict H1; apply Zlt_not_le. - subst a. - apply Zle_lt_trans with (n * - 1 + r); auto with zarith. - case (Zle_lt_or_eq 0 q); auto with zarith; intros H8. - contradict H2; apply Zle_not_lt. - apply Zle_trans with (n * 1 + r); auto with zarith. - rewrite H4; auto with zarith. - subst a; subst q; auto with zarith. - Qed. - - Theorem Zmod_minus: - forall a b n, 0 < n -> (a - b) mod n = (a mod n - b mod n) mod n. - Proof. - intros a b n H; 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 Zmod_plus; auto with zarith. - rewrite Zmod_mult; auto with zarith. - rewrite (fun x y => Zmod_plus x ((-1) * y)); auto with zarith. - rewrite Zmod_mult; auto with zarith. - rewrite (fun x => Zmod_mult x (b mod n)); auto with zarith. - repeat rewrite Zmod_mod; auto. - Qed. - - Theorem Zmod_le: forall a n, 0 < n -> 0 <= a -> (Zmod a n) <= a. - Proof. - intros a n H1 H2; case (Zle_or_lt n a); intros H3. - case (Z_mod_lt a n); auto with zarith. - rewrite Zmod_def_small; auto with zarith. - Qed. - - Theorem Zmod_le_first: forall a b, 0 <= a -> 0 < b -> 0 <= a mod b <= a. - Proof. - intros a b H H1;case (Z_mod_lt a b);auto with zarith;intros H2 H3;split;auto. - case (Zle_or_lt b a); intros H4; auto with zarith. - rewrite Zmod_def_small; auto with zarith. - Qed. - - -(************************************** - Properties of Zdivide -**************************************) - - Theorem Zdiv_pos: forall a b, 0 < b -> 0 <= a -> 0 <= a / b. - Proof. - intros; apply Zge_le; apply Z_div_ge0; auto with zarith. - Qed. - Hint Resolve Zdiv_pos: zarith. - - 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. - 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 Zmod_mult; case (Zmod_le_first ((c mod b) * (a mod b)) b); - auto with zarith. - apply Zmult_le_compat_r; auto with zarith. - case (Zmod_le_first 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. - - Theorem Zdiv_unique: - forall n d q r, 0 < d -> ( 0 <= r < d ) -> n = d * q + r -> q = n / d. - Proof. - intros n d q r H H0 H1. - assert (H2: n = d * (n / d) + n mod d). - apply Z_div_mod_eq; auto with zarith. - assert (H3: 0 <= n mod d < d ). - apply Z_mod_lt; auto with zarith. - case (Ztrichotomy q (n / d)); auto. - intros H4. - absurd (n < n); auto with zarith. - pattern n at 1; rewrite H1; rewrite H2. - apply Zlt_le_trans with (d * (q + 1)); auto with zarith. - rewrite Zmult_plus_distr_r; auto with zarith. - apply Zle_trans with (d * (n / d)); auto with zarith. - intros tmp; case tmp; auto; intros H4; clear tmp. - absurd (n < n); auto with zarith. - pattern n at 2; rewrite H1; rewrite H2. - apply Zlt_le_trans with (d * (n / d + 1)); auto with zarith. - rewrite Zmult_plus_distr_r; auto with zarith. - apply Zle_trans with (d * q); auto with zarith. - Qed. - - Theorem Zmod_unique: - forall n d q r, 0 < d -> ( 0 <= r < d ) -> n = d * q + r -> r = n mod d. - Proof. - intros n d q r H H0 H1. - assert (H2: n = d * (n / d) + n mod d). - apply Z_div_mod_eq; auto with zarith. - rewrite (Zdiv_unique n d q r) in H1; auto. - apply (Zplus_reg_l (d * (n / d))); auto with zarith. - Qed. - - Theorem Zmod_Zmult_compat_l: forall a b c, - 0 < b -> 0 < c -> c * a mod (c * b) = c * (a mod b). - Proof. - intros a b c H2 H3. - pattern a at 1; rewrite (Z_div_mod_eq a b); auto with zarith. - rewrite Zplus_comm; rewrite Zmult_plus_distr_r. - rewrite Zmult_assoc; rewrite (Zmult_comm (c * b)). - rewrite Z_mod_plus; auto with zarith. - apply Zmod_def_small; split; auto with zarith. - apply Zmult_le_0_compat; auto with zarith. - destruct (Z_mod_lt a b);auto with zarith. - apply Zmult_lt_compat_l; auto with zarith. - destruct (Z_mod_lt a b);auto with zarith. - Qed. - - Theorem Zdiv_Zmult_compat_l: - forall a b c, 0 <= a -> 0 < b -> 0 < c -> c * a / (c * b) = a / b. - Proof. - intros a b c H1 H2 H3; case (Z_mod_lt a b); auto with zarith; intros H4 H5. - apply Zdiv_unique with (a mod b); auto with zarith. - apply Zmult_reg_l with c; auto with zarith. - rewrite Zmult_plus_distr_r; rewrite <- Zmod_Zmult_compat_l; auto with zarith. - rewrite Zmult_assoc; apply Z_div_mod_eq; auto with zarith. - Qed. - - Theorem Zdiv_0_l: forall a, 0 / a = 0. - Proof. - intros a; case a; auto. - Qed. - - Theorem Zdiv_0_r: forall a, a / 0 = 0. - Proof. - intros a; case a; auto. - Qed. - - Theorem Zmod_0_l: forall a, 0 mod a = 0. - Proof. - intros a; case a; auto. - Qed. - - Theorem Zmod_0_r: forall a, a mod 0 = 0. - Proof. - intros a; case a; auto. - Qed. - - 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. - - Theorem Zmult_mod_distr_l: - forall a b c, 0 < a -> 0 < c -> (a * b) mod (a * c) = a * (b mod c). - Proof. - intros a b c H Hc. - apply sym_equal; apply Zmod_unique with (b / c); auto with zarith. - apply Zmult_lt_0_compat; auto. - case (Z_mod_lt b c); auto with zarith; intros; split; auto with zarith. - apply Zmult_lt_compat_l; auto. - rewrite <- Zmult_assoc; rewrite <- Zmult_plus_distr_r. - rewrite <- Z_div_mod_eq; auto with zarith. - Qed. - - - Theorem Zmod_distr: forall a b r t, 0 <= a <= b -> 0 <= r -> 0 <= t < 2 ^a -> - (2 ^a * r + t) mod (2 ^ b) = (2 ^a * r) mod (2 ^ b) + t. - Proof. - intros a b r t (H1, H2) H3 (H4, H5). - assert (t < 2 ^ b). - apply Zlt_le_trans with (1:= H5); auto with zarith. - apply Zpower_le_monotone; auto with zarith. - rewrite Zmod_plus; auto with zarith. - rewrite Zmod_def_small with (a := t); auto with zarith. - apply Zmod_def_small; auto with zarith. - split; auto with zarith. - assert (0 <= 2 ^a * r); auto with zarith. - apply Zplus_le_0_compat; auto with zarith. - match goal with |- context [?X mod ?Y] => case (Z_mod_lt X Y) end; - auto with zarith. - pattern (2 ^ b) at 2; replace (2 ^ b) with ((2 ^ b - 2 ^a) + 2 ^ a); - try ring. - apply Zplus_le_lt_compat; auto with zarith. - replace b with ((b - a) + a); try ring. - rewrite Zpower_exp; auto with zarith. - pattern (2 ^a) at 4; rewrite <- (Zmult_1_l (2 ^a)); - try rewrite <- Zmult_minus_distr_r. - rewrite (Zmult_comm (2 ^(b - a))); rewrite Zmult_mod_distr_l; - auto with zarith. - rewrite (Zmult_comm (2 ^a)); apply Zmult_le_compat_r; auto with zarith. - match goal with |- context [?X mod ?Y] => case (Z_mod_lt X Y) end; - auto with zarith. - Qed. - - Theorem Zmult_mod_distr_r: - forall a b c : Z, 0 < a -> 0 < c -> (b * a) mod (c * a) = (b mod c) * a. - Proof. - intros; repeat rewrite (fun x => (Zmult_comm x a)). - apply Zmult_mod_distr_l; auto. - Qed. - - Theorem Z_div_plus_l: forall a b c : Z, 0 < b -> (a * b + c) / b = a + c / b. - Proof. - intros a b c H; rewrite Zplus_comm; rewrite Z_div_plus; - try apply Zplus_comm; auto with zarith. - Qed. - - Theorem Zmod_shift_r: - forall a b r t, 0 <= a <= b -> 0 <= r -> 0 <= t < 2 ^a -> - (r * 2 ^a + t) mod (2 ^ b) = (r * 2 ^a) mod (2 ^ b) + t. - Proof. - intros a b r t (H1, H2) H3 (H4, H5). - assert (t < 2 ^ b). - apply Zlt_le_trans with (1:= H5); auto with zarith. - apply Zpower_le_monotone; auto with zarith. - rewrite Zmod_plus; auto with zarith. - rewrite Zmod_def_small with (a := t); auto with zarith. - apply Zmod_def_small; auto with zarith. - split; auto with zarith. - assert (0 <= 2 ^a * r); auto with zarith. - apply Zplus_le_0_compat; auto with zarith. - match goal with |- context [?X mod ?Y] => case (Z_mod_lt X Y) end; - auto with zarith. - pattern (2 ^ b) at 2;replace (2 ^ b) with ((2 ^ b - 2 ^a) + 2 ^ a); try ring. - apply Zplus_le_lt_compat; auto with zarith. - replace b with ((b - a) + a); try ring. - rewrite Zpower_exp; auto with zarith. - pattern (2 ^a) at 4; rewrite <- (Zmult_1_l (2 ^a)); - try rewrite <- Zmult_minus_distr_r. - repeat rewrite (fun x => Zmult_comm x (2 ^ a)); rewrite Zmult_mod_distr_l; - auto with zarith. - apply Zmult_le_compat_l; auto with zarith. - match goal with |- context [?X mod ?Y] => case (Z_mod_lt X Y) end; - auto with zarith. - Qed. - - Theorem Zdiv_lt_0: forall a b, 0 <= a < b -> a / b = 0. - intros a b H; apply sym_equal; apply Zdiv_unique with a; auto with zarith. - Qed. - - Theorem Zmod_mult_0: forall a b, 0 < b -> (a * b) mod b = 0. - Proof. - intros a b H; rewrite <- (Zplus_0_l (a * b)); rewrite Z_mod_plus; - auto with zarith. - Qed. - - Theorem Zdiv_shift_r: - forall a b r t, 0 <= a <= b -> 0 <= r -> 0 <= t < 2 ^a -> - (r * 2 ^a + t) / (2 ^ b) = (r * 2 ^a) / (2 ^ b). - Proof. - intros a b r t (H1, H2) H3 (H4, H5). - assert (Eq: t < 2 ^ b); auto with zarith. - apply Zlt_le_trans with (1 := H5); auto with zarith. - apply Zpower_le_monotone; auto with zarith. - pattern (r * 2 ^ a) at 1; rewrite Z_div_mod_eq with (b := 2 ^ b); - auto with zarith. - rewrite <- Zplus_assoc. - rewrite <- Zmod_shift_r; auto with zarith. - rewrite (Zmult_comm (2 ^ b)); rewrite Z_div_plus_l; auto with zarith. - rewrite (fun x y => @Zdiv_lt_0 (x mod y)); auto with zarith. - match goal with |- context [?X mod ?Y] => case (Z_mod_lt X Y) end; - auto with zarith. - Qed. - - - Theorem Zpos_minus: - forall a b, Zpos a < Zpos b -> Zpos (b- a) = Zpos b - Zpos a. - Proof. - intros a b H. - repeat rewrite Zpos_eq_Z_of_nat_o_nat_of_P; autorewrite with pos_morph; - auto with zarith. - rewrite inj_minus1; auto with zarith. - match goal with |- (?X <= ?Y)%nat => - case (le_or_lt X Y); auto; intro tmp; absurd (Z_of_nat X < Z_of_nat Y); - try apply Zle_not_lt; auto with zarith - end. - repeat rewrite <- Zpos_eq_Z_of_nat_o_nat_of_P; auto with zarith. - generalize (Zlt_gt _ _ H); auto. - Qed. - - Theorem Zdiv_Zmult_compat_r: - forall a b c : Z, 0 <= a -> 0 < b -> 0 < c -> a * c / (b * c) = a / b. - Proof. - intros a b c H H1 H2; repeat rewrite (fun x => Zmult_comm x c); - apply Zdiv_Zmult_compat_l; auto. - Qed. - - - Lemma shift_unshift_mod : forall n p a, - 0 <= a < 2^n -> - 0 <= p <= n -> - a * 2^p = a / 2^(n - p) * 2^n + (a*2^p) mod 2^n. - Proof. - intros n p a H1 H2. - pattern (a*2^p) at 1;replace (a*2^p) with - (a*2^p/2^n * 2^n + a*2^p mod 2^n). - 2:symmetry;rewrite (Zmult_comm (a*2^p/2^n));apply Z_div_mod_eq. - replace (a * 2 ^ p / 2 ^ n) with (a / 2 ^ (n - p));trivial. - replace (2^n) with (2^(n-p)*2^p). - symmetry;apply Zdiv_Zmult_compat_r. - destruct H1;trivial. - apply Zpower_lt_0;auto with zarith. - apply Zpower_lt_0;auto with zarith. - rewrite <- Zpower_exp. - replace (n-p+p) with n;trivial. ring. - omega. omega. - apply Zlt_gt. apply Zpower_lt_0;auto with zarith. - Qed. - - Lemma Zdiv_Zdiv : forall a b c, 0 < b -> 0 < c -> (a/b)/c = a / (b*c). - Proof. - intros a b c H H0. - pattern a at 2;rewrite (Z_div_mod_eq a b);auto with zarith. - pattern (a/b) at 2;rewrite (Z_div_mod_eq (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));try ring. - rewrite Z_div_plus_l;auto with zarith. - rewrite (Zdiv_lt_0 (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. - apply Zmult_lt_0_compat;auto with zarith. - Qed. - - Lemma div_le_0 : forall p x, 0 <= x -> 0 <= x / 2 ^ p. - Proof. - intros p x Hle;destruct (Z_le_gt_dec 0 p). - apply Zdiv_le_lower_bound;auto with zarith. - replace (2^p) with 0. - destruct x;compute;intro;discriminate. - destruct p;trivial;discriminate z. - Qed. - - Lemma div_lt : forall p x y, 0 <= x < y -> x / 2^p < y. - Proof. - intros p x y H;destruct (Z_le_gt_dec 0 p). - apply Zdiv_lt_upper_bound;auto with zarith. - apply Zlt_le_trans with y;auto with zarith. - rewrite <- (Zmult_1_r y);apply Zmult_le_compat;auto with zarith. - assert (0 < 2^p);auto with zarith. - replace (2^p) with 0. - destruct x;change (0<y);auto with zarith. - destruct p;trivial;discriminate z. - Qed. - - - Theorem Zgcd_div_pos a b: - (0 < b)%Z -> (0 < Zgcd a b)%Z -> (0 < b / Zgcd a b)%Z. - intros a b Ha Hg. - case (Zle_lt_or_eq 0 (b/Zgcd a b)); auto. - apply Zdiv_pos; auto with zarith. - intros H; generalize Ha. - pattern b at 1; rewrite (Zdivide_Zdiv_eq (Zgcd a b) b); auto. - rewrite <- H; auto with zarith. - assert (F := (Zgcd_is_gcd a b)); inversion F; auto. - Qed. - diff --git a/theories/Ints/Z/ZPowerAux.v b/theories/Ints/Z/ZPowerAux.v deleted file mode 100644 index 151b9a73a..000000000 --- a/theories/Ints/Z/ZPowerAux.v +++ /dev/null @@ -1,203 +0,0 @@ - -(*************************************************************) -(* This file is distributed under the terms of the *) -(* GNU Lesser General Public License Version 2.1 *) -(*************************************************************) -(* Benjamin.Gregoire@inria.fr Laurent.Thery@inria.fr *) -(*************************************************************) - -(********************************************************************** - - - ZPowerAux.v Auxillary functions & Theorems for Zpower - **********************************************************************) - -Require Export ZArith. -Require Export Znumtheory. -Require Export Tactic. - -Open Local Scope Z_scope. - -Hint Extern 2 (Zle _ _) => - (match goal with - |- Zpos _ <= Zpos _ => exact (refl_equal _) -| H: _ <= ?p |- _ <= ?p => apply Zle_trans with (2 := H) -| H: _ < ?p |- _ <= ?p => apply Zlt_le_weak; apply Zle_lt_trans with (2 := H) - end). - -Hint Extern 2 (Zlt _ _) => - (match goal with - |- Zpos _ < Zpos _ => exact (refl_equal _) -| H: _ <= ?p |- _ <= ?p => apply Zlt_le_trans with (2 := H) -| H: _ < ?p |- _ <= ?p => apply Zle_lt_trans with (2 := H) - end). - -Hint Resolve Zlt_gt Zle_ge: zarith. - -(************************************** - Properties Zpower -**************************************) - -Theorem Zpower_1: forall a, 0 <= a -> 1 ^ a = 1. -intros a Ha; pattern a; apply natlike_ind; auto with zarith. -intros x Hx Hx1; unfold Zsucc. -rewrite Zpower_exp; auto with zarith. -rewrite Hx1; simpl; auto. -Qed. - -Theorem Zpower_exp_0: forall a, a ^ 0 = 1. -simpl; unfold Zpower_pos; simpl; auto with zarith. -Qed. - -Theorem Zpower_exp_1: forall a, a ^ 1 = a. -simpl; unfold Zpower_pos; simpl; auto with zarith. -Qed. - -Theorem Zpower_Zabs: forall a b, Zabs (a ^ b) = (Zabs a) ^ b. -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. -eq_tac; 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. -intros p n H. -unfold Zsucc; rewrite Zpower_exp; auto with zarith. -rewrite Zpower_exp_1; apply Zmult_comm. -Qed. - -Theorem Zpower_mult: forall p q r, 0 <= q -> 0 <= r -> p ^ (q * r) = (p ^ q) ^ - r. -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_exp_1; try rewrite <- Zpower_exp; try eq_tac; -auto with zarith. -ring. -Qed. - -Theorem Zpower_lt_0: forall a b: Z, 0 < a -> 0 <= b-> 0 < a ^b. -intros a b; case b; auto with zarith. -simpl; intros; auto with zarith. -2: intros p H H1; case H1; auto. -intros p H1 H; generalize H; pattern (Zpos p); apply natlike_ind; auto. -intros; case a; compute; auto. -intros p1 H2 H3 _; unfold Zsucc; rewrite Zpower_exp; simpl; auto with zarith. -apply Zmult_lt_O_compat; auto with zarith. -generalize H1; case a; compute; intros; auto; discriminate. -Qed. - -Theorem Zpower_le_monotone: forall a b c: Z, 0 < a -> 0 <= b <= c -> a ^ b <= a ^ c. -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_lt_0; auto with zarith. -apply Zlt_le_weak; apply Zpower_lt_0; auto with zarith. -Qed. - - -Theorem Zpower_le_0: forall a b: Z, 0 <= a -> 0 <= a ^b. -intros a b; case b; 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. -intros p1 H2 H3 _; unfold Zsucc; rewrite Zpower_exp; simpl; auto with zarith. -apply Zmult_le_0_compat; auto with zarith. -generalize H1; case a; compute; intros; auto; discriminate. -Qed. - -Hint Resolve Zpower_le_0 Zpower_lt_0: zarith. - -Theorem Zpower_prod: forall p q r, 0 <= q -> 0 <= r -> (p * q) ^ r = p ^ r * q ^ r. -intros p q r H1 H2; generalize H2; pattern r; apply natlike_ind; auto. -intros r1 H3 H4 H5. -unfold Zsucc; rewrite Zpower_exp; auto with zarith. -rewrite H4; repeat (rewrite Zpower_exp_1 || rewrite Zpower_exp); auto with zarith; ring. -Qed. - -Theorem Zpower_le_monotone_exp: forall a b c: Z, 0 <= c -> 0 <= a <= b -> a ^ c <= b ^ c. -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_exp_1. -apply Zle_trans with (a ^x * b); auto with zarith. -Qed. - -Theorem Zpower_lt_monotone: forall a b c: Z, 1 < a -> 0 <= b < c -> a ^ b < a ^ - c. -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. -assert (0 < a ^ (c - b)); auto with zarith. -apply Zlt_le_trans with (a ^1); auto with zarith. -rewrite Zpower_exp_1; auto with zarith. -apply Zpower_le_monotone; 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_monotone_exp;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_le_monotone2: - forall a b c: Z, 0 < a -> b <= c -> a ^ b <= a ^ c. -intros a b c H H2. -destruct (Z_le_gt_dec 0 b). -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. -replace (a^b) with 0. -destruct (Z_le_gt_dec 0 c). -destruct (Zle_lt_or_eq _ _ z0). -apply Zlt_le_weak;apply Zpower_lt_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 Zpower2_lt_lin: forall n, - 0 <= n -> n < 2 ^ n. -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_exp_1. - 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. -intros; apply Zlt_le_weak. -apply Zpower2_lt_lin; auto. -Qed. diff --git a/theories/Ints/Z/ZSum.v b/theories/Ints/Z/ZSum.v deleted file mode 100644 index bcde7386c..000000000 --- a/theories/Ints/Z/ZSum.v +++ /dev/null @@ -1,321 +0,0 @@ - -(*************************************************************) -(* This file is distributed under the terms of the *) -(* GNU Lesser General Public License Version 2.1 *) -(*************************************************************) -(* Benjamin.Gregoire@inria.fr Laurent.Thery@inria.fr *) -(*************************************************************) - -(*********************************************************************** - Summation.v from Z to Z - *********************************************************************) -Require Import Arith. -Require Import ArithRing. -Require Import ListAux. -Require Import ZArith. -Require Import ZAux. -Require Import Iterator. -Require Import ZProgression. - - -Open Scope Z_scope. -(* Iterated Sum *) - -Definition Zsum := - fun n m f => - if Zle_bool n m - then iter 0 f Zplus (progression Zsucc n (Zabs_nat ((1 + m) - n))) - else iter 0 f Zplus (progression Zpred n (Zabs_nat ((1 + n) - m))). -Hint Unfold Zsum . - -Lemma Zsum_nn: forall n f, Zsum n n f = f n. -intros n f; unfold Zsum; rewrite Zle_bool_refl. -replace ((1 + n) - n) with 1; auto with zarith. -simpl; ring. -Qed. - -Theorem permutation_rev: forall (A:Set) (l : list A), permutation (rev l) l. -intros a l; elim l; simpl; auto. -intros a1 l1 Hl1. -apply permutation_trans with (cons a1 (rev l1)); auto. -change (permutation (rev l1 ++ (a1 :: nil)) (app (cons a1 nil) (rev l1))); auto. -Qed. - -Lemma Zsum_swap: forall (n m : Z) (f : Z -> Z), Zsum n m f = Zsum m n f. -intros n m f; unfold Zsum. -generalize (Zle_cases n m) (Zle_cases m n); case (Zle_bool n m); - case (Zle_bool m n); auto with arith. -intros; replace n with m; auto with zarith. -3:intros H1 H2; contradict H2; auto with zarith. -intros H1 H2; apply iter_permutation; auto with zarith. -apply permutation_trans - with (rev (progression Zsucc n (Zabs_nat ((1 + m) - n)))). -apply permutation_sym; apply permutation_rev. -rewrite Zprogression_opp; auto with zarith. -replace (n + Z_of_nat (pred (Zabs_nat ((1 + m) - n)))) with m; auto. -replace (Zabs_nat ((1 + m) - n)) with (S (Zabs_nat (m - n))); auto with zarith. -simpl. -rewrite Z_of_nat_Zabs_nat; auto with zarith. -replace ((1 + m) - n) with (1 + (m - n)); auto with zarith. -cut (0 <= m - n); auto with zarith; unfold Zabs_nat. -case (m - n); auto with zarith. -intros p; case p; simpl; auto with zarith. -intros p1 Hp1; rewrite nat_of_P_xO; rewrite nat_of_P_xI; - rewrite nat_of_P_succ_morphism. -simpl; repeat rewrite plus_0_r. -repeat rewrite <- plus_n_Sm; simpl; auto. -intros p H3; contradict H3; auto with zarith. -intros H1 H2; apply iter_permutation; auto with zarith. -apply permutation_trans - with (rev (progression Zsucc m (Zabs_nat ((1 + n) - m)))). -rewrite Zprogression_opp; auto with zarith. -replace (m + Z_of_nat (pred (Zabs_nat ((1 + n) - m)))) with n; auto. -replace (Zabs_nat ((1 + n) - m)) with (S (Zabs_nat (n - m))); auto with zarith. -simpl. -rewrite Z_of_nat_Zabs_nat; auto with zarith. -replace ((1 + n) - m) with (1 + (n - m)); auto with zarith. -cut (0 <= n - m); auto with zarith; unfold Zabs_nat. -case (n - m); auto with zarith. -intros p; case p; simpl; auto with zarith. -intros p1 Hp1; rewrite nat_of_P_xO; rewrite nat_of_P_xI; - rewrite nat_of_P_succ_morphism. -simpl; repeat rewrite plus_0_r. -repeat rewrite <- plus_n_Sm; simpl; auto. -intros p H3; contradict H3; auto with zarith. -apply permutation_rev. -Qed. - -Lemma Zsum_split_up: - forall (n m p : Z) (f : Z -> Z), - ( n <= m < p ) -> Zsum n p f = Zsum n m f + Zsum (m + 1) p f. -intros n m p f [H H0]. -case (Zle_lt_or_eq _ _ H); clear H; intros H. -unfold Zsum; (repeat rewrite Zle_imp_le_bool); auto with zarith. -assert (H1: n < p). -apply Zlt_trans with ( 1 := H ); auto with zarith. -assert (H2: m < 1 + p). -apply Zlt_trans with ( 1 := H0 ); auto with zarith. -assert (H3: n < 1 + m). -apply Zlt_trans with ( 1 := H ); auto with zarith. -assert (H4: n < 1 + p). -apply Zlt_trans with ( 1 := H1 ); auto with zarith. -replace (Zabs_nat ((1 + p) - (m + 1))) - with (minus (Zabs_nat ((1 + p) - n)) (Zabs_nat ((1 + m) - n))). -apply iter_progression_app; auto with zarith. -apply inj_le_inv. -(repeat rewrite Z_of_nat_Zabs_nat); auto with zarith. -rewrite next_n_Z; auto with zarith. -rewrite Z_of_nat_Zabs_nat; auto with zarith. -apply inj_eq_inv; auto with zarith. -rewrite inj_minus1; auto with zarith. -(repeat rewrite Z_of_nat_Zabs_nat); auto with zarith. -apply inj_le_inv. -(repeat rewrite Z_of_nat_Zabs_nat); auto with zarith. -subst m. -rewrite Zsum_nn; auto with zarith. -unfold Zsum; generalize (Zle_cases n p); generalize (Zle_cases (n + 1) p); - case (Zle_bool n p); case (Zle_bool (n + 1) p); auto with zarith. -intros H1 H2. -replace (Zabs_nat ((1 + p) - n)) with (S (Zabs_nat (p - n))); auto with zarith. -replace (n + 1) with (Zsucc n); auto with zarith. -replace ((1 + p) - Zsucc n) with (p - n); auto with zarith. -apply inj_eq_inv; auto with zarith. -rewrite inj_S; (repeat rewrite Z_of_nat_Zabs_nat); auto with zarith. -Qed. - -Lemma Zsum_S_left: - forall (n m : Z) (f : Z -> Z), n < m -> Zsum n m f = f n + Zsum (n + 1) m f. -intros n m f H; rewrite (Zsum_split_up n n m f); auto with zarith. -rewrite Zsum_nn; auto with zarith. -Qed. - -Lemma Zsum_S_right: - forall (n m : Z) (f : Z -> Z), - n <= m -> Zsum n (m + 1) f = Zsum n m f + f (m + 1). -intros n m f H; rewrite (Zsum_split_up n m (m + 1) f); auto with zarith. -rewrite Zsum_nn; auto with zarith. -Qed. - -Lemma Zsum_split_down: - forall (n m p : Z) (f : Z -> Z), - ( p < m <= n ) -> Zsum n p f = Zsum n m f + Zsum (m - 1) p f. -intros n m p f [H H0]. -case (Zle_lt_or_eq p (m - 1)); auto with zarith; intros H1. -pattern m at 1; replace m with ((m - 1) + 1); auto with zarith. -repeat rewrite (Zsum_swap n). -rewrite (Zsum_swap (m - 1)). -rewrite Zplus_comm. -apply Zsum_split_up; auto with zarith. -subst p. -repeat rewrite (Zsum_swap n). -rewrite Zsum_nn. -unfold Zsum; (repeat rewrite Zle_imp_le_bool); auto with zarith. -replace (Zabs_nat ((1 + n) - (m - 1))) with (S (Zabs_nat (n - (m - 1)))). -rewrite Zplus_comm. -replace (Zabs_nat ((1 + n) - m)) with (Zabs_nat (n - (m - 1))); auto with zarith. -pattern m at 4; replace m with (Zsucc (m - 1)); auto with zarith. -apply f_equal with ( f := Zabs_nat ); auto with zarith. -apply inj_eq_inv; auto with zarith. -rewrite inj_S. -(repeat rewrite Z_of_nat_Zabs_nat); auto with zarith. -Qed. - - -Lemma Zsum_ext: - forall (n m : Z) (f g : Z -> Z), - n <= m -> - (forall (x : Z), ( n <= x <= m ) -> f x = g x) -> Zsum n m f = Zsum n m g. -intros n m f g HH H. -unfold Zsum; auto. -unfold Zsum; (repeat rewrite Zle_imp_le_bool); auto with zarith. -apply iter_ext; auto with zarith. -intros a H1; apply H; auto; split. -apply Zprogression_le_init with ( 1 := H1 ). -cut (a < Zsucc m); auto with zarith. -replace (Zsucc m) with (n + Z_of_nat (Zabs_nat ((1 + m) - n))); auto with zarith. -apply Zprogression_le_end; auto with zarith. -rewrite Z_of_nat_Zabs_nat; auto with zarith. -Qed. - -Lemma Zsum_add: - forall (n m : Z) (f g : Z -> Z), - Zsum n m f + Zsum n m g = Zsum n m (fun (i : Z) => f i + g i). -intros n m f g; unfold Zsum; case (Zle_bool n m); apply iter_comp; - auto with zarith. -Qed. - -Lemma Zsum_times: - forall n m x f, x * Zsum n m f = Zsum n m (fun i=> x * f i). -intros n m x f. -unfold Zsum. case (Zle_bool n m); intros; apply iter_comp_const with (k := (fun y : Z => x * y)); auto with zarith. -Qed. - -Lemma inv_Zsum: - forall (P : Z -> Prop) (n m : Z) (f : Z -> Z), - n <= m -> - P 0 -> - (forall (a b : Z), P a -> P b -> P (a + b)) -> - (forall (x : Z), ( n <= x <= m ) -> P (f x)) -> P (Zsum n m f). -intros P n m f HH H H0 H1. -unfold Zsum; rewrite Zle_imp_le_bool; auto with zarith; apply iter_inv; auto. -intros x H3; apply H1; auto; split. -apply Zprogression_le_init with ( 1 := H3 ). -cut (x < Zsucc m); auto with zarith. -replace (Zsucc m) with (n + Z_of_nat (Zabs_nat ((1 + m) - n))); auto with zarith. -apply Zprogression_le_end; auto with zarith. -rewrite Z_of_nat_Zabs_nat; auto with zarith. -Qed. - - -Lemma Zsum_pred: - forall (n m : Z) (f : Z -> Z), - Zsum n m f = Zsum (n + 1) (m + 1) (fun (i : Z) => f (Zpred i)). -intros n m f. -unfold Zsum. -generalize (Zle_cases n m); generalize (Zle_cases (n + 1) (m + 1)); - case (Zle_bool n m); case (Zle_bool (n + 1) (m + 1)); auto with zarith. -replace ((1 + (m + 1)) - (n + 1)) with ((1 + m) - n); auto with zarith. -intros H1 H2; cut (exists c , c = Zabs_nat ((1 + m) - n) ). -intros [c H3]; rewrite <- H3. -generalize n; elim c; auto with zarith; clear H1 H2 H3 c n. -intros c H n; simpl; eq_tac; auto with zarith. -eq_tac; unfold Zpred; auto with zarith. -replace (Zsucc (n + 1)) with (Zsucc n + 1); auto with zarith. -exists (Zabs_nat ((1 + m) - n)); auto. -replace ((1 + (n + 1)) - (m + 1)) with ((1 + n) - m); auto with zarith. -intros H1 H2; cut (exists c , c = Zabs_nat ((1 + n) - m) ). -intros [c H3]; rewrite <- H3. -generalize n; elim c; auto with zarith; clear H1 H2 H3 c n. -intros c H n; simpl; (eq_tac; auto with zarith). -eq_tac; unfold Zpred; auto with zarith. -replace (Zpred (n + 1)) with (Zpred n + 1); auto with zarith. -unfold Zpred; auto with zarith. -exists (Zabs_nat ((1 + n) - m)); auto. -Qed. - -Theorem Zsum_c: - forall (c p q : Z), p <= q -> Zsum p q (fun x => c) = ((1 + q) - p) * c. -intros c p q Hq; unfold Zsum. -rewrite Zle_imp_le_bool; auto with zarith. -pattern ((1 + q) - p) at 2; rewrite <- Z_of_nat_Zabs_nat; auto with zarith. -cut (exists r , r = Zabs_nat ((1 + q) - p) ); - [intros [r H1]; rewrite <- H1 | exists (Zabs_nat ((1 + q) - p))]; auto. -generalize p; elim r; auto with zarith. -intros n H p0; replace (Z_of_nat (S n)) with (Z_of_nat n + 1); auto with zarith. -simpl; rewrite H; ring. -rewrite inj_S; auto with zarith. -Qed. - -Theorem Zsum_Zsum_f: - forall (i j k l : Z) (f : Z -> Z -> Z), - i <= j -> - k < l -> - Zsum i j (fun x => Zsum k (l + 1) (fun y => f x y)) = - Zsum i j (fun x => Zsum k l (fun y => f x y) + f x (l + 1)). -intros; apply Zsum_ext; intros; auto with zarith. -rewrite Zsum_S_right; auto with zarith. -Qed. - -Theorem Zsum_com: - forall (i j k l : Z) (f : Z -> Z -> Z), - Zsum i j (fun x => Zsum k l (fun y => f x y)) = - Zsum k l (fun y => Zsum i j (fun x => f x y)). -intros; unfold Zsum; case (Zle_bool i j); case (Zle_bool k l); apply iter_com; - auto with zarith. -Qed. - -Theorem Zsum_le: - forall (n m : Z) (f g : Z -> Z), - n <= m -> - (forall (x : Z), ( n <= x <= m ) -> (f x <= g x )) -> - (Zsum n m f <= Zsum n m g ). -intros n m f g Hl H. -unfold Zsum; rewrite Zle_imp_le_bool; auto with zarith. -unfold Zsum; - cut - (forall x, - In x (progression Zsucc n (Zabs_nat ((1 + m) - n))) -> ( f x <= g x )). -elim (progression Zsucc n (Zabs_nat ((1 + m) - n))); simpl; auto with zarith. -intros x H1; apply H; split. -apply Zprogression_le_init with ( 1 := H1 ); auto. -cut (x < m + 1); auto with zarith. -replace (m + 1) with (n + Z_of_nat (Zabs_nat ((1 + m) - n))); auto with zarith. -apply Zprogression_le_end; auto with zarith. -rewrite Z_of_nat_Zabs_nat; auto with zarith. -Qed. - -Theorem iter_le: -forall (f g: Z -> Z) l, (forall a, In a l -> f a <= g a) -> - iter 0 f Zplus l <= iter 0 g Zplus l. -intros f g l; elim l; simpl; auto with zarith. -Qed. - -Theorem Zsum_lt: - forall n m f g, - (forall x, n <= x -> x <= m -> f x <= g x) -> - (exists x, n <= x /\ x <= m /\ f x < g x) -> - Zsum n m f < Zsum n m g. -intros n m f g H (d, (Hd1, (Hd2, Hd3))); unfold Zsum; rewrite Zle_imp_le_bool; auto with zarith. -cut (In d (progression Zsucc n (Zabs_nat (1 + m - n)))). -cut (forall x, In x (progression Zsucc n (Zabs_nat (1 + m - n)))-> f x <= g x). -elim (progression Zsucc n (Zabs_nat (1 + m - n))); simpl; auto with zarith. -intros a l Rec H0 [H1 | H1]; subst; auto. -apply Zle_lt_trans with (f d + iter 0 g Zplus l); auto with zarith. -apply Zplus_le_compat_l. -apply iter_le; auto. -apply Zlt_le_trans with (f a + iter 0 g Zplus l); auto with zarith. -intros x H1; apply H. -apply Zprogression_le_init with ( 1 := H1 ); auto. -cut (x < m + 1); auto with zarith. -replace (m + 1) with (n + Z_of_nat (Zabs_nat ((1 + m) - n))); auto with zarith. -apply Zprogression_le_end with ( 1 := H1 ); auto with arith. -rewrite Z_of_nat_Zabs_nat; auto with zarith. -apply in_Zprogression. -rewrite Z_of_nat_Zabs_nat; auto with zarith. -Qed. - -Theorem Zsum_minus: - forall n m f g, Zsum n m f - Zsum n m g = Zsum n m (fun x => f x - g x). -intros n m f g; apply trans_equal with (Zsum n m f + (-1) * Zsum n m g); auto with zarith. -rewrite Zsum_times; rewrite Zsum_add; auto with zarith. -Qed. |