Library Coqtail.Arith.Znumfacts
Informative version, derived from the stdlib
Definition prime_dec_aux_inf:
∀ p m,
{ n | 1 < n < m ∧ ¬ rel_prime n p } +
{ ∀ n, 1 < n < m → rel_prime n p }.
Proof.
intros p m.
case (Z_lt_dec 1 m); intros H1;
[ | right; intros; exfalso; omega ].
pattern m; apply natlike_rec; auto with zarith;
[ right; intros; exfalso; omega | ].
intros x Hx IH; destruct IH as [E|F].
left; destruct E as (n,((H0,H2),H3));∃ n; auto with zarith.
destruct (rel_prime_dec x p) as [Y|N].
right; 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.
left; ∃ x; split; auto with zarith.
right; intros n [HHH1 HHH2]; contradict HHH1; auto with zarith.
Defined.
Informative version, derived from the stdlib
Theorem not_prime_divide_inf:
∀ p, 1 < p → ¬ prime p → { n | 1 < n < p ∧ (n | p) }.
Proof.
intros p Hp Hp1.
case (prime_dec_aux_inf p p); intros H1.
case H1; intros n [Hn1 Hn2].
generalize (Zgcd_is_pos n p); intros Hpos.
case (Z_le_lt_eq_dec 0 (Zgcd n p)); auto with zarith; intros H3.
case (Z_le_lt_eq_dec 1 (Zgcd n p)); auto with zarith; intros H4.
∃ (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.
elim Hp1; constructor; auto.
intros n [Hn1 Hn2].
case Zle_lt_or_eq with ( 1 := Hn1 ); auto with zarith.
intros H2; subst n; red; apply Zis_gcd_intro; auto with zarith.
Defined.
Definition Z_le_lt_eq_dec x y : x ≤ y → {x < y} + {x = y}.
Proof.
Lemma Zcompare_Eq_eq : ∀ n m : Z, (n ?= m) = Eq → n = m.
Proof.
Lemma Pcompare_notEq_notEq : ∀ a b,
(Pcompare a b Lt ≠ Eq) ∧ (Pcompare a b Gt ≠ Eq).
Proof.
intros a; induction a; intros b; destruct b; split; intros E; simpl in E;
try solve [
inversion E |
auto |
eapply (proj1 (IHa _)); eauto |
eapply (proj2 (IHa _)); eauto
].
Qed.
Lemma Pcompare_Eq_eq : ∀ a b, Pcompare a b Eq = Eq → a = b.
Proof.
intros a; induction a; intros b; destruct b; intros E; simpl in E;
try solve [
inversion E |
auto |
f_equal; apply IHa; eauto
].
exfalso; eapply Pcompare_notEq_notEq; eauto.
exfalso; eapply (proj1 (Pcompare_notEq_notEq _ _)); eauto.
Defined.
intros [ | p | p ] [ | q | q] E; simpl in E;
reflexivity ||
solve [ inversion E ] ||
(f_equal; eapply Pcompare_Eq_eq; eauto).
fold (p ?= q)%positive; destruct ((p ?= q)%positive); auto || inversion E.
Defined.
pose (Zcompare_Eq_iff_eq :=
fun x y ⇒ conj (fun E : (x ?= y) = Eq ⇒ Zcompare_Eq_eq x y E)
(fun E : x = y ⇒
eq_ind_r (fun x0 ⇒ (x0 ?= y) = Eq) (Zcompare_refl y) E)).
intro H.
apply Zcompare_rec with (n := x) (m := y); intros E.
right. elim (Zcompare_Eq_iff_eq x y); auto with arith.
left. elim (Zcompare_Eq_iff_eq x y); auto with arith.
absurd (x > y); auto with arith.
Defined.
Induction on natural numbers via prime numbers and multiplication
Lemma Z_prime_rect : ∀ P : Z → Type,
((P 0) →
(P 1) →
(∀ n, prime n → P n) →
(∀ a b, P a → P b → P (a × b)) →
∀ n, 0 ≤ n → P n)%Z.
Proof.
intros P P0 P1 Pprime Psplit.
assert (Hind : ∀ (N : nat) n, 0 ≤ n → (Zabs_nat n < N)%nat → P n).
intro n ; induction n ; intros i ipos imax.
exfalso; inversion imax.
destruct (Z_le_lt_eq_dec i (Z_of_nat n)) as [|E]. zify; omega. apply IHn; zify; omega.
rewrite E in *; clear E i ipos imax.
destruct (prime_dec (Z_of_nat n)) as [Hprime | Hnprime]. apply Pprime ; assumption.
destruct n. subst; apply P0.
destruct n. subst; apply P1.
set (z := Z_of_nat (S (S n))).
assert (n_big : 1 < z) by (unfold z; zify; omega).
destruct (not_prime_divide_inf _ n_big Hnprime) as [a [[amin amax] b_eqz]].
destruct (Zdivide_inf _ _ b_eqz) as [b eqz]; clear b_eqz; rewrite eqz.
assert (Bb : 1 < b < z).
assert (1 < b) by (apply Zmult_lt_reg_r with a; omega).
split; auto.
rewrite <- (Zmult_1_r b), eqz.
apply Zmult_lt_compat_l; try omega.
assert (z = Z_of_nat (S (S n))) by auto; clearbody z.
apply Psplit; apply IHn; zify; omega.
intros n n_pos ; apply Hind with (S (Zabs_nat n)) ; auto.
Defined.
Lemma Z_prime_ind : ∀ P : Z → Prop,
((P 0) →
(P 1) →
(∀ n, prime n → P n) →
(∀ a b, P a → P b → P (a × b)) →
∀ n, 0 ≤ n → P n)%Z.
Proof.
intros; apply Z_prime_rect; auto.
Qed.
Bezout coefficients: a lot easier to use than the stdlib
Lemma bezout_inj : ∀ a b,
{u : Z & {v | u × a + v × b = Zgcd a b}}.
Proof.
intros a b.
destruct (euclid a b) as (u, v, d, E, H).
destruct (Z_le_dec 0 d) as [L|L].
∃ u; ∃ v.
rewrite (Zis_gcd_gcd _ _ _ L H).
auto.
∃ (- u); ∃ (- v).
assert (L2 : 0 ≤ - d) by omega.
rewrite (Zis_gcd_gcd _ _ _ L2).
rewrite <- E; ring.
apply Zis_gcd_opp, Zis_gcd_sym; auto.
Qed.
Lemma rel_prime_bezout : ∀ a b, rel_prime a b →
{u : Z & {v | u × a + v × b = 1}}.
Proof.
intros a b RP.
rewrite <- (proj2 (Zgcd_1_rel_prime a b)); auto.
apply bezout_inj.
Qed.
Multiplication is often injective in Z/pZ
Lemma modular_mult_inj : ∀ p n, prime p →
¬ (0 ≡ n [p]) → ∀ x y, x × n ≡ y × n [p] → x ≡ y [p].
Proof.
intros p n Pp Nn x y E.
apply eqm_minus_0, divide_eqm; notzero.
assert (D : (p | (x - y) × n)).
apply divide_eqm; notzero.
ring_simplify.
rewrite E.
red; f_equal; ring.
destruct (prime_mult _ Pp _ _ D) as [D1|D2]; auto.
exfalso; apply Nn.
symmetry; apply divide_eqm; auto.
notzero.
Qed.
Computing the modular inverse in Z_pZ
Lemma modular_inverse : ∀ p x, prime p → ~(x ≡ 0 [p]) → { y | x × y ≡ 1 [p] }.
Proof.
intros p x Pp Nd.
assert (rel_prime (x mod p) p).
apply Pp.
assert (A : p > 0) by notzero; pose proof Z_mod_lt x p A.
unfold eqm in Nd; rewrite Zmod_0_l in Nd.
omega.
destruct (rel_prime_bezout _ _ H) as (u, (v, Huv)).
∃ u.
rewrite <- Huv.
assert (REW : x mod p ≡ x [p]) by (red; rewrite Zmod_mod; auto) .
rewrite REW.
apply eqm_minus_0.
ring_simplify.
apply multiple_eqm with (- v); auto.
Qed.