diff options
Diffstat (limited to 'src/Util/ZUtil.v')
| -rw-r--r-- | src/Util/ZUtil.v | 93 |
1 files changed, 93 insertions, 0 deletions
diff --git a/src/Util/ZUtil.v b/src/Util/ZUtil.v index 1a48abfd6..3ebbbece1 100644 --- a/src/Util/ZUtil.v +++ b/src/Util/ZUtil.v @@ -64,3 +64,96 @@ Proof. rewrite <- IHn. auto. Qed. + +Lemma mod_exp_0 : forall a x m, x > 0 -> m > 1 -> a mod m = 0 -> + a ^ x mod m = 0. +Proof. + intros. + replace x with (Z.of_nat (Z.to_nat x)) in * by (apply Z2Nat.id; omega). + induction (Z.to_nat x). { + simpl in *; omega. + } { + rewrite Nat2Z.inj_succ in *. + rewrite Z.pow_succ_r by omega. + rewrite Z.mul_mod by omega. + case_eq n; intros. { + subst. simpl. + rewrite Zmod_1_l by omega. + rewrite H1. + apply Zmod_0_l. + } { + subst. + rewrite IHn by (rewrite Nat2Z.inj_succ in *; omega). + rewrite H1. + auto. + } + } +Qed. + +Lemma mod_pow : forall (a m b : Z), (0 <= b) -> (m <> 0) -> + a ^ b mod m = (a mod m) ^ b mod m. +Proof. + intros; rewrite <- (Z2Nat.id b) by auto. + induction (Z.to_nat b); auto. + rewrite Nat2Z.inj_succ. + do 2 rewrite Z.pow_succ_r by apply Nat2Z.is_nonneg. + rewrite Z.mul_mod by auto. + rewrite (Z.mul_mod (a mod m) ((a mod m) ^ Z.of_nat n) m) by auto. + rewrite <- IHn by auto. + rewrite Z.mod_mod by auto. + reflexivity. +Qed. + +Ltac Zdivide_exists_mul := let k := fresh "k" in +match goal with +| [ H : (?a | ?b) |- _ ] => apply Z.mod_divide in H; try apply Zmod_divides in H; destruct H as [k H] +| [ |- (?a | ?b) ] => apply Z.mod_divide; try apply Zmod_divides +end; (omega || auto). + +Lemma divide_mul_div: forall a b c (a_nonzero : a <> 0) (c_nonzero : c <> 0), + (a | b * (a / c)) -> (c | a) -> (c | b). +Proof. + intros ? ? ? ? ? divide_a divide_c_a; do 2 Zdivide_exists_mul. + rewrite divide_c_a in divide_a. + rewrite Z_div_mul' in divide_a by auto. + replace (b * k) with (k * b) in divide_a by ring. + replace (c * k * k0) with (k * (k0 * c)) in divide_a by ring. + rewrite Z.mul_cancel_l in divide_a by (intuition; rewrite H in divide_c_a; ring_simplify in divide_a; intuition). + eapply Zdivide_intro; eauto. +Qed. + +Lemma divide2_even_iff : forall n, (2 | n) <-> Z.even n = true. +Proof. + intro; split. { + intro divide2_n. + Zdivide_exists_mul; [ | pose proof (Z.mod_pos_bound n 2); omega]. + rewrite divide2_n. + apply Z.even_mul. + } { + intro n_even. + pose proof (Zmod_even n). + rewrite n_even in H. + apply Zmod_divide; omega || auto. + } +Qed. + +Lemma prime_odd_or_2 : forall p (prime_p : prime p), p = 2 \/ Z.odd p = true. +Proof. + intros. + apply Decidable.imp_not_l; try apply Z.eq_decidable. + intros p_neq2. + pose proof (Zmod_odd p) as mod_odd. + destruct (Sumbool.sumbool_of_bool (Z.odd p)) as [? | p_not_odd]; auto. + rewrite p_not_odd in mod_odd. + apply Zmod_divides in mod_odd; try omega. + destruct mod_odd as [c c_id]. + rewrite Z.mul_comm in c_id. + apply Zdivide_intro in c_id. + apply prime_divisors in c_id; auto. + destruct c_id; [omega | destruct H; [omega | destruct H; auto]]. + pose proof (prime_ge_2 p prime_p); omega. +Qed. + +Ltac prime_bound := match goal with +| [ H : prime ?p |- _ ] => pose proof (prime_ge_2 p H); try omega +end.
\ No newline at end of file |