Module ModularInverse

Computation of a modular inverse, using the extended Euclidean algorithm

Require Import Coqlib.
Require Import Coq.Program.Wf.

Extended Euclidean algorithm, as a function, with proof of termination and rewriting lemma

Program Fixpoint euclid_aux (a b r u v r' u' v': Z) { measure (Z.to_nat (Z.abs r')) } :=
  if zeq r' 0 then (r, u, v)
  else euclid_aux a b r' u' v' (r - (r/r')*r') (u - (r/r')*u') (v - (r/r')*v')
  .

Next Obligation.

  rewrite <- !Zmod_eq_full; try omega.
  apply Z2Nat.inj_lt.
  - apply Z.abs_nonneg.
  - apply Z.abs_nonneg.
  - destruct r'.
    + exfalso. apply H.
      reflexivity.
    + pose proof Pos2Z.is_pos p as Hpos.
      pose proof Z_mod_lt r (Z.pos p) as Hmod.
      destruct (r mod Z.pos p); simpl.
      * omega.
      * omega.
      * pose proof Pos2Z.neg_is_neg p0 as Hneg.
        omega.
    + pose proof Pos2Z.is_pos p as Hpos.
      pose proof Pos2Z.neg_is_neg p as Hneg.
       apply Z_mod_neg with r (Z.neg p) in Hneg.
      destruct (r mod Z.neg p); simpl.
      * omega.
      * omega.
      * destruct Hneg.
        replace (Z.neg p0) with (- Z.pos p0) in H0 by auto.
        replace (Z.neg p) with (- Z.pos p) in H0 by auto.
        omega.
Qed.

Definition euclid (a b: Z) :=
  match euclid_aux a b (Z.abs a) (Z.sgn a) 0 (Z.abs b) 0 (Z.sgn b) with
    (_, u, v) => (u, v)
  end.

Lemma rewrite_euclid_aux: forall a b r u v r' u' v',
    euclid_aux a b r u v r' u' v' =
    if zeq r' 0 then (r, u, v)
    else euclid_aux a b r' u' v' (r - (r/r')*r') (u - (r/r')*u') (v - (r/r')*v').

Proof.

  intros. simpl.
  unfold euclid_aux at 1.
  unfold euclid_aux_func.
  repeat rewrite WfExtensionality.fix_sub_eq_ext.
  simpl. fold euclid_aux_func. unfold euclid_aux.
  destruct r'; try reflexivity.
Qed.

Extended Euclidean algorithm, as a relation

Inductive euclid_aux_R : Z -> Z -> Z -> Z -> Z -> Z -> Z -> Z -> Z -> Z -> Z -> Prop :=
  | euclid0 : forall a b r u v u' v',
      euclid_aux_R a b r u v 0 u' v' r u v
  | euclidIter : forall a b r u v r' u' v' r'' u'' v'',
      r' <> 0 ->
      euclid_aux_R a b r' u' v' (r - (r/r')*r') (u - (r/r')*u') (v - (r/r')*v') r'' u'' v'' ->
      euclid_aux_R a b r u v r' u' v' r'' u'' v''.

Equivalence between euclid_aux euclid_aux_R

Theorem pair_eq : forall X Y (x y: X*Y),
x = y -> fst x = fst y /\ snd x = snd y.

Proof.

intros.
split; subst; reflexivity.
Qed.

Theorem triple_eq : forall X Y Z (x1 x2: X) (y1 y2: Y) (z1 z2: Z),
(x1, y1, z1) = (x2, y2, z2) ->
x1 = x2 /\ y1 = y2 /\ z1 = z2.

Proof.

  intros.
  apply pair_eq in H. simpl in H. destruct H.
  apply pair_eq in H. simpl in H. destruct H.
  auto.
Qed.

Lemma euclid_aux_R__euclid_aux : forall a b r u v r' u' v' r'' u'' v'',
euclid_aux_R a b r u v r' u' v' r'' u'' v'' ->
euclid_aux a b r u v r' u' v' = (r'', u'', v'').

Proof.

  intros.
  induction H.
  - subst. auto.
  - rewrite rewrite_euclid_aux.
    rewrite zeq_false.
    + auto.
    + auto.
Qed.

Lemma euclid_aux__euclid_aux_R__pos : forall r',
    0 <= r' -> forall a b r u v u' v' r'' u'' v'',
    euclid_aux a b r u v r' u' v' = (r'', u'', v'') ->
    euclid_aux_R a b r u v r' u' v' r'' u'' v''.

Proof.

  intros r'0 POS0.
  pattern r'0.
  apply Zlt_0_ind; auto.
  intros r' IND POS.
  intros.

  rewrite rewrite_euclid_aux in H. simpl in H.
  destruct (zeq r' 0).
  - apply triple_eq in H.
    destruct H as [Hr [Hu Hv]]. subst.
    apply euclid0; auto.
  - apply euclidIter; auto.
    apply IND.
    rewrite <- Zmod_eq_full; auto.
    apply Z_mod_lt; try omega.
    apply H.
Qed.

Lemma euclid_aux__euclid_aux_R__neg : forall r',
    r' <= 0 -> forall a b r u v u' v' r'' u'' v'',
    euclid_aux a b r u v r' u' v' = (r'', u'', v'') ->
    euclid_aux_R a b r u v r' u' v' r'' u'' v''.

Proof.

  intros r'0 POS0.
  remember (-r'0) as rr.
  assert(H0: r'0 = -rr) by omega.
  rewrite H0.
  pattern rr.
  apply Zlt_0_ind; try omega.
  intros r' IND POS.
  intros.

  rewrite rewrite_euclid_aux in H. simpl in H.
  destruct (zeq (-r') 0).
  - apply triple_eq in H.
    destruct H as [Hr [Hu Hv]]. subst.
    rewrite e.
    apply euclid0; auto.
  - apply euclidIter; try omega.
    rewrite <- Zmod_eq_full; try omega.
    rewrite <- Zmod_eq_full in H; try omega.
    destruct (zeq (r mod r') 0).
    + rewrite Z_mod_zero_opp_r; auto.
      replace 0 with (- 0) by auto.
      apply IND; try omega.
      rewrite Z_mod_zero_opp_r in H; auto.
    + rewrite Z_mod_nz_opp_r; auto.
      replace (r mod r' - r') with (- (r' - r mod r')) by omega.
      apply IND; try omega.
      pose proof Z_mod_lt r r'. omega.
      replace (- (r' - r mod r')) with (r mod r' - r') by omega.
      rewrite <- Z_mod_nz_opp_r; auto.
Qed.

Lemma euclid_aux__euclid_aux_R : forall a b r u v r' u' v' r'' u'' v'',
euclid_aux a b r u v r' u' v' = (r'', u'', v'') ->
euclid_aux_R a b r u v r' u' v' r'' u'' v''.

Proof.

  intros.
  destruct r'.
  - apply euclid_aux__euclid_aux_R__pos.
    + try omega.
    + auto.
  - apply euclid_aux__euclid_aux_R__pos.
    + apply Zle_0_pos.
    + auto.
  - apply euclid_aux__euclid_aux_R__neg.
    + pose proof Zlt_neg_0 p. omega.
    + auto.
Qed.

Theorem euclid_aux__iff__euclid_aux_R : forall a b r u v r' u' v' r'' u'' v'',
euclid_aux a b r u v r' u' v' = (r'', u'', v'') <->
euclid_aux_R a b r u v r' u' v' r'' u'' v''.

Proof.

  intros.
  split.
  - apply euclid_aux__euclid_aux_R.
  - apply euclid_aux_R__euclid_aux.
Qed.

Specification of the extended Euclidean algorithm

Lemma euclid_aux_spec_bezout_rec : forall (a b r u v r' u' v' r'' u'' v'': Z),
    euclid_aux a b r u v r' u' v' = (r'', u'', v'') ->
    r = a*u + b*v ->
    r' = a*u' + b*v' ->
    r'' = a*u'' + b*v''.

Proof.

  intros a b r u v r' u' v' r'' u'' v''.
  intros E.
  apply euclid_aux__iff__euclid_aux_R in E.
  induction E.
  - intros. subst. auto.
  - intros Hr Hr'.
    apply IHE.
    + apply Hr'.
    + rewrite !Z.mul_sub_distr_l.
      assert(H2: forall x y z w, x - y + (z - w) = x + z - (y + w)) by (intros; omega).
      rewrite H2.
      assert(H3: forall x y z, x * (y * z) = y * (x * z)).
      { intros. rewrite !Z.mul_assoc. f_equal. apply Z.mul_comm. }
      rewrite (H3 a).
      rewrite (H3 b).
      rewrite <- Z.mul_add_distr_l.
      rewrite <- Hr, <- Hr'.
      reflexivity.
Qed.

Lemma euclid_aux_spec_bezout : forall (a b r u v: Z),
euclid_aux a b (Z.abs a) (Z.sgn a) 0 (Z.abs b) 0 (Z.sgn b) = (r, u, v) ->
r = a*u + b*v.

Proof.

  intros.
  apply euclid_aux_spec_bezout_rec with (Z.abs a) (Z.sgn a) 0 (Z.abs b) 0 (Z.sgn b).
  - auto.
  - rewrite Z.sgn_abs. omega.
  - rewrite Z.sgn_abs. omega.
Qed.

Lemma euclid_aux_spec_gcd : forall (a b r u v r' u' v' r'' u'' v'': Z),
euclid_aux a b r u v r' u' v' = (r'', u'', v'') ->
Z.gcd r r' = (Z.abs r'').

Proof.

  intros a b r u v r' u' v' r'' u'' v''.
  intros E.
  apply euclid_aux__iff__euclid_aux_R in E.
  induction E.
  - subst.
    apply Z.gcd_0_r.
  - rewrite <- IHE.
    rewrite <- Zmod_eq_full; try omega.
    symmetry.
    rewrite Z.gcd_comm.
    rewrite Z.gcd_mod; auto.
    apply Z.gcd_comm.
Qed.

Lemma euclid_aux_spec_pos_rec : forall (a b r u v r' u' v' r'' u'' v'': Z),
    euclid_aux a b r u v r' u' v' = (r'', u'', v'') ->
    0 <= r ->
    0 <= r' ->
    0 <= r''.

Proof.

  intros a b r u v r' u' v' r'' u'' v''.
  intros E.
  apply euclid_aux__iff__euclid_aux_R in E.
  induction E.
  - subst. auto.
  - intros Hr Hr'.
    apply IHE; auto.
    rewrite <- Zmod_eq_full; auto.
    apply Z_mod_lt.
    omega.
Qed.

Lemma euclid_aux_spec_pos : forall (a b u v u' v' r'' u'' v'': Z),
euclid_aux a b (Z.abs a) u v (Z.abs b) u' v' = (r'', u'', v'') ->
0 <= r''.

Proof.

  intros.
  apply euclid_aux_spec_pos_rec in H; auto.
  apply Z.abs_nonneg.
  apply Z.abs_nonneg.
Qed.

Theorem euclid_spec : forall (a b: Z),
let (u, v) := euclid a b in
Z.gcd a b = a*u + b*v.

Proof.

  intros a b.
  destruct (euclid a b) as [u v] eqn:Heucl.
  unfold euclid in Heucl.

  destruct (euclid_aux a b (Z.abs a) (Z.sgn a) 0 (Z.abs b) 0 (Z.sgn b)) as [ru' v'] eqn:Haux.
  destruct ru' as [r' u'].


  apply euclid_aux_spec_gcd in Haux as Hgcd.
  rewrite Z.gcd_abs_l in Hgcd.
  rewrite Z.gcd_abs_r in Hgcd.

  apply euclid_aux_spec_bezout in Haux as Hbezout.

  apply euclid_aux_spec_pos in Haux as Hpos.
  apply Z.abs_eq_iff in Hpos.

  apply pair_eq in Heucl.
  simpl in Heucl.
  destruct Heucl.
  rewrite Hpos in Hgcd.

  subst.

  auto.
Qed.

Modular inverse, and specification

Definition mod_inv (a n: Z) :=
fst (euclid a n).

Lemma mod_inv_gcd_spec : forall (a n: Z),
(a * (mod_inv a n)) mod n = Z.gcd a n mod n.

Proof.

  intros a n.
  unfold mod_inv.
  pose proof euclid_spec a n as Heucl.
  destruct (euclid a n) as [u v].
  simpl.
  replace (a * u) with (Z.gcd a n + - (n * v)) by omega.
  rewrite Z.mul_comm.
  rewrite Zopp_mult_distr_l.
  apply Z_mod_plus_full.
Qed.

Lemma mod_inv_spec : forall (a n: Z),
Z.gcd a n = 1 ->
(a * (mod_inv a n)) mod n = 1 mod n.

Proof.

  intros a n.
  intros Hgcd.
  rewrite <- Hgcd.
  apply mod_inv_gcd_spec.
Qed.

Lemma divide_odd_rel_prime_2: forall a q,
Z.odd a = true -> (q | a) ->
Z.gcd q 2 = 1.

Proof.

  intros a q Hodd Hdiv.
  rewrite Zodd_mod in Hodd.
  apply Zeq_bool_eq in Hodd.

  apply Z.gcd_unique.
  - omega.
  - apply Z.divide_1_l.
  - apply Z.divide_1_l.
  - intros q2 H1 H2.
    unfold Z.divide in *.
    destruct H1 as [z1 H1].
    destruct H2 as [z2 H2].
    destruct Hdiv as [z3 Hdiv].
    rewrite H2 in Hodd.
    rewrite H1 in Hdiv.
    rewrite Hdiv in Hodd.
    rewrite Z.mul_assoc in Hodd.
    rewrite Zmult_mod_distr_r in Hodd.
    eauto.
Qed.

Lemma power_of_two_rel_prime_odd : forall (a: Z) (n: nat),
Z.odd a = true -> Z.gcd (2^(Z.of_nat n)) a = 1.

Proof.

  intros a n Hodd.

  induction n.
  - apply Z.gcd_1_l.
  - rewrite Nat2Z.inj_succ.
    rewrite Z.pow_succ_r; try omega.
    remember (2 ^ Z.of_nat n) as x.
    rewrite <- IHn.
    apply Z.gcd_unique.
    + apply Z.gcd_nonneg.
    + apply Z.divide_trans with x.
      * apply Z.gcd_divide_l.
      * unfold Z.divide. exists 2. reflexivity.
    + apply Z.gcd_divide_r.
    + intros q H1 H2.
      apply Z.gcd_greatest.
      * apply Z.gauss with 2.
        -- apply H1.
        -- apply divide_odd_rel_prime_2 with a; auto.
      * apply H2.
Qed.

Lemma mod_inv_spec_power_of_two : forall (a p: Z) ,
    Z.odd a = true ->
    0 < p ->
    (a * (mod_inv a (2^p))) mod (2^p) = 1.

Proof.

  intros a p.
  intros Hodd Hpos.
  assert(H: exists n : nat, p = Z.of_nat n).
  { apply Z_of_nat_complete. omega. }
  destruct H as [n H].
  rewrite H.
  apply power_of_two_rel_prime_odd with a n in Hodd as Hgcd.
  rewrite Z.gcd_comm in Hgcd.
  pose proof mod_inv_spec _ _ Hgcd as H2.
  rewrite H2.
  apply Z.mod_1_l.
  apply Z.pow_gt_1; omega.
Qed.