Library Coqtail.Arith.Znumfacts

Require Import ZArith Omega Znumtheory.
Require Import Natsets MyNat Ztools Zeqm.

Number theory : factorisation, computation of Bezout coefficients and modular inverse



Informative version, derived from the stdlib

Definition prime_dec_aux_inf:
   p m,
    { n | 1 < n < m ¬ rel_prime n p } +
    { n, 1 < n < mrel_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) = Eqn = 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 = Eqa = 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 yconj (fun E : (x ?= y) = EqZcompare_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 : ZType,
  ((P 0) →
  (P 1) →
  ( n, prime nP n) →
  ( a b, P aP bP (a × b)) →
     n, 0 nP n)%Z.
Proof.
  intros P P0 P1 Pprime Psplit.
  assert (Hind : (N : nat) n, 0 n → (Zabs_nat n < N)%natP 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 : ZProp,
  ((P 0) →
  (P 1) →
  ( n, prime nP n) →
  ( a b, P aP bP (a × b)) →
     n, 0 nP 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.