diff options
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 | 1372 | ||||
| -rw-r--r-- | theories/Ints/Z/ZDivModAux.v | 452 | ||||
| -rw-r--r-- | theories/Ints/Z/ZPowerAux.v | 183 | ||||
| -rw-r--r-- | theories/Ints/Z/ZSum.v | 321 | ||||
| -rw-r--r-- | theories/Ints/Z/Zmod.v | 94 |
8 files changed, 3211 insertions, 0 deletions
diff --git a/theories/Ints/Z/IntsZmisc.v b/theories/Ints/Z/IntsZmisc.v new file mode 100644 index 0000000000..6fcaaa6e9f --- /dev/null +++ b/theories/Ints/Z/IntsZmisc.v @@ -0,0 +1,185 @@ + +(*************************************************************) +(* 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 else m <= n. +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 new file mode 100644 index 0000000000..1ea08b4fab --- /dev/null +++ b/theories/Ints/Z/Pmod.v @@ -0,0 +1,565 @@ + +(*************************************************************) +(* 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 new file mode 100644 index 0000000000..b4e4ca5ef0 --- /dev/null +++ b/theories/Ints/Z/Ppow.v @@ -0,0 +1,39 @@ +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 new file mode 100644 index 0000000000..73fdbd1281 --- /dev/null +++ b/theories/Ints/Z/ZAux.v @@ -0,0 +1,1372 @@ + +(*************************************************************) +(* 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 *) +(*************************************************************) + +(********************************************************************** + Aux.v + + Auxillary functions & Theorems + **********************************************************************) + +Require Import ArithRing. +Require Export ZArith. +Require Export Znumtheory. +Require Export Tactic. +(* Require Import MOmega. *) + + +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). + +(************************************** + 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. + 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. + apply Zle_lt_trans with (d - b); auto with zarith. + rewrite Zmult_minus_distr_r; auto with zarith. + Qed. + + Theorem beta_lex_inv: forall a b c d beta, + a < c -> 0 <= b < beta -> + 0 <= d < beta -> + a * beta + b < c * beta + d. + Proof. + intros a b c d beta H1 (H3, H4) (H5, H6). + case (Zle_or_lt (c * beta + d) (a * beta + b)); auto with zarith. + intros H7; contradict H1;apply Zle_not_lt;apply beta_lex with (1 := H7);auto. + Qed. + + Lemma beta_mult : forall h l beta, + 0 <= h < beta -> 0 <= l < beta -> 0 <= h*beta+l < beta^2. + Proof. + intros h l beta H1 H2;split. auto with zarith. + rewrite <- (Zplus_0_r (beta^2)); rewrite Zpower_2; + apply beta_lex_inv;auto with zarith. + Qed. + + Lemma Zmult_lt_b : + forall b x y, 0 <= x < b -> 0 <= y < b -> 0 <= x * y <= b^2 - 2*b + 1. + Proof. + intros b x y (Hx1,Hx2) (Hy1,Hy2);split;auto with zarith. + apply Zle_trans with ((b-1)*(b-1)). + apply Zmult_le_compat;auto with zarith. + apply Zeq_le;ring. + Qed. + + Lemma sum_mul_carry : forall xh xl yh yl wc cc beta, + 1 < beta -> + 0 <= wc < beta -> + 0 <= xh < beta -> + 0 <= xl < beta -> + 0 <= yh < beta -> + 0 <= yl < beta -> + 0 <= cc < beta^2 -> + wc*beta^2 + cc = xh*yl + xl*yh -> + 0 <= wc <= 1. + Proof. + intros xh xl yh yl wc cc beta U H1 H2 H3 H4 H5 H6 H7. + assert (H8 := Zmult_lt_b beta xh yl H2 H5). + assert (H9 := Zmult_lt_b beta xl yh H3 H4). + split;auto with zarith. + apply beta_lex with (cc) (beta^2 - 2) (beta^2); auto with zarith. + Qed. + + Theorem mult_add_ineq: forall x y cross beta, + 0 <= x < beta -> + 0 <= y < beta -> + 0 <= cross < beta -> + 0 <= x * y + cross < beta^2. + Proof. + intros x y cross beta HH HH1 HH2. + split; auto with zarith. + apply Zle_lt_trans with ((beta-1)*(beta-1)+(beta-1)); auto with zarith. + apply Zplus_le_compat; auto with zarith. + apply Zmult_le_compat; auto with zarith. + repeat (rewrite Zmult_minus_distr_l || rewrite Zmult_minus_distr_r); + rewrite Zpower_2; auto with zarith. + Qed. + + Theorem mult_add_ineq2: forall x y c cross beta, + 0 <= x < beta -> + 0 <= y < beta -> + 0 <= c*beta + cross <= 2*beta - 2 -> + 0 <= x * y + (c*beta + cross) < beta^2. + Proof. + intros x y c cross beta HH HH1 HH2. + split; auto with zarith. + apply Zle_lt_trans with ((beta-1)*(beta-1)+(2*beta-2));auto with zarith. + apply Zplus_le_compat; auto with zarith. + apply Zmult_le_compat; auto with zarith. + repeat (rewrite Zmult_minus_distr_l || rewrite Zmult_minus_distr_r); + rewrite Zpower_2; auto with zarith. + Qed. + +Theorem mult_add_ineq3: forall x y c cross beta, + 0 <= x < beta -> + 0 <= y < beta -> + 0 <= cross <= beta - 2 -> + 0 <= c <= 1 -> + 0 <= x * y + (c*beta + cross) < beta^2. + Proof. + intros x y c cross beta HH HH1 HH2 HH3. + apply mult_add_ineq2;auto with zarith. + split;auto with zarith. + 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. + + +(************************************** + 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. +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 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. + + +(************************************** + 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_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 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. + +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. + +(** 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 Zdivide_trans: forall a b c, (a | b) -> (b | c) -> (a | c). +intros a b c [d H1] [e H2]; exists (d * e)%Z; auto with zarith. +rewrite H2; rewrite H1; ring. +Qed. + +Theorem Zdivide_Zabs_l: forall a b, (Zabs a | b) -> (a | b). +intros a b [x H]; subst b. +pattern (Zabs a); apply Zabs_intro. +exists (- x); ring. +exists x; ring. +Qed. + +Theorem Zdivide_Zabs_inv_l: forall a b, (a | b) -> (Zabs a | b). +intros a b [x H]; subst b. +pattern (Zabs a); apply Zabs_intro. +exists (- x); ring. +exists x; ring. +Qed. + +Theorem Zdivide_le: forall a b, 0 <= a -> 0 < b -> (a | b) -> a <= b. +intros a b H1 H2 [q H3]; subst b. +case (Zle_lt_or_eq 0 a); auto with zarith; intros H3. +case (Zle_lt_or_eq 0 q); auto with zarith. +apply (Zmult_le_0_reg_r a); auto with zarith. +intros H4; apply Zle_trans with (1 * a); auto with zarith. +intros H4; subst q; contradict H2; auto with zarith. +Qed. + +Theorem Zdivide_Zdiv_eq: forall a b, 0 < a -> (a | b) -> b = a * (b / a). +intros a b Hb Hc. +pattern b at 1; rewrite (Z_div_mod_eq b a); auto with zarith. +rewrite (Zdivide_mod b a); auto with zarith. +Qed. + +Theorem Zdivide_Zdiv_lt_pos: + forall a b, 1 < a -> 0 < b -> (a | b) -> 0 < b / a < b . +intros a b H1 H2 H3; split. +apply Zmult_lt_reg_r with a; auto with zarith. +rewrite (Zmult_comm (Zdiv b a)); rewrite <- Zdivide_Zdiv_eq; auto with zarith. +apply Zmult_lt_reg_r with a; auto with zarith. +(repeat rewrite (fun x => Zmult_comm x a)); auto with zarith. +rewrite <- Zdivide_Zdiv_eq; auto with zarith. +pattern b at 1; replace b with (1 * b); auto with zarith. +apply Zmult_lt_compat_r; auto with zarith. +Qed. + +Theorem Zmod_divide_minus: forall a b c, 0 < b -> a mod b = c -> (b | a - c). +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, 0 <= c < b -> (b | a -c) -> (a mod b) = c. +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. +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. +contradict H2; 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). +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 +**************************************) + +Theorem Zis_gcd_unique: + forall (a b c d : Z), Zis_gcd a b c -> Zis_gcd b a d -> c = d \/ c = (- d). +intros a b c d H1 H2. +inversion_clear H1 as [Hc1 Hc2 Hc3]. +inversion_clear H2 as [Hd1 Hd2 Hd3]. +assert (H3: Zdivide c d); auto. +assert (H4: Zdivide d c); auto. +apply Zdivide_antisym; auto. +Qed. + + +Theorem Zis_gcd_gcd: forall a b c, 0 <= c -> Zis_gcd a b c -> Zgcd a b = c. +intros a b c H1 H2. +case (Zis_gcd_uniqueness_apart_sign a b c (Zgcd a b)); auto. +apply Zgcd_is_gcd; auto. +case Zle_lt_or_eq with (1 := H1); clear H1; intros H1; subst; auto. +intros H3; subst; contradict H1. +apply Zle_not_lt; generalize (Zgcd_is_pos a b); auto with zarith. +case (Zgcd a b); simpl; auto; intros; discriminate. +Qed. + + +Theorem Zdivide_Zgcd: forall p q r, (p | q) -> (p | r) -> (p | Zgcd q r). +intros p q r H1 H2. +assert (H3: (Zis_gcd q r (Zgcd q r))). +apply Zgcd_is_gcd. +inversion_clear H3; auto. +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. + +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. +apply Zis_gcd_sym; auto. +intros H2; absurd (0 <= Zgcd a b); auto with zarith. +generalize (Zgcd_is_pos a b); 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 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. +apply Zis_gcd_sym; auto. +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 prime2: 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 prime3: 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. + + diff --git a/theories/Ints/Z/ZDivModAux.v b/theories/Ints/Z/ZDivModAux.v new file mode 100644 index 0000000000..d07b92d80e --- /dev/null +++ b/theories/Ints/Z/ZDivModAux.v @@ -0,0 +1,452 @@ + +(*************************************************************) +(* 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: forall a, 0 < a -> 0 / a = 0. + Proof. + intros a H;apply sym_equal;apply Zdiv_unique with (r := 0); auto with zarith. + 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. + diff --git a/theories/Ints/Z/ZPowerAux.v b/theories/Ints/Z/ZPowerAux.v new file mode 100644 index 0000000000..b56b52d49d --- /dev/null +++ b/theories/Ints/Z/ZPowerAux.v @@ -0,0 +1,183 @@ + +(*************************************************************) +(* 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. diff --git a/theories/Ints/Z/ZSum.v b/theories/Ints/Z/ZSum.v new file mode 100644 index 0000000000..bcde7386c3 --- /dev/null +++ b/theories/Ints/Z/ZSum.v @@ -0,0 +1,321 @@ + +(*************************************************************) +(* 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. diff --git a/theories/Ints/Z/Zmod.v b/theories/Ints/Z/Zmod.v new file mode 100644 index 0000000000..dffa795322 --- /dev/null +++ b/theories/Ints/Z/Zmod.v @@ -0,0 +1,94 @@ +Require Import ZArith. +Require Import ZAux. + +Set Implicit Arguments. + +Open Scope Z_scope. + +Lemma rel_prime_mod: forall a b, 1 < b -> + rel_prime a b -> a mod b <> 0. +Proof. +intros a b H H1 H2. +case (not_rel_prime_0 _ H). +rewrite <- H2. +apply rel_prime_mod; auto with zarith. +Qed. + +Lemma Zmodpl: forall a b n, 0 < n -> + (a mod n + b) mod n = (a + b) mod n. +Proof. +intros a b n H. +rewrite Zmod_plus; auto. +rewrite Zmod_mod; auto. +apply sym_equal; apply Zmod_plus; auto. +Qed. + +Lemma Zmodpr: 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 Zmodpl; auto. +Qed. + +Lemma Zmodml: forall a b n, 0 < n -> + (a mod n * b) mod n = (a * b) mod n. +Proof. +intros a b n H. +rewrite Zmod_mult; auto. +rewrite Zmod_mod; auto. +apply sym_equal; apply Zmod_mult; auto. +Qed. + +Lemma Zmodmr: 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 Zmodml; auto. +Qed. + + +Ltac is_ok t := + match t with + | (?x mod _ + ?y mod _) mod _ => constr:false + | (?x mod _ * (?y mod _)) mod _ => constr:false + | ?x mod _ => x + end. + +Ltac rmod t := + match t with + (?x + ?y) mod _ => + match (is_ok x) with + | false => rmod x + | ?x1 => match (is_ok y) with + |false => rmod y + | ?y1 => + rewrite <- (Zmod_plus x1 y1) + |false => rmod y + end + end + | (?x * ?y) mod _ => + match (is_ok x) with + | false => rmod x + | ?x1 => match (is_ok y) with + |false => rmod y + | ?y1 => rewrite <- (Zmod_mult x1 y1) + end + | false => rmod x + end + end. + + +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. + |