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