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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
Theorem euclid_spec :
forall (
a b:
Z),
let (
u,
v) :=
euclid a b in
Z.gcd a b =
a*
u +
b*
v.
Proof.
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.
Lemma mod_inv_spec :
forall (
a n:
Z),
Z.gcd a n = 1 ->
(
a * (
mod_inv a n))
mod n = 1
mod n.
Proof.
Lemma divide_odd_rel_prime_2:
forall a q,
Z.odd a =
true -> (
q |
a) ->
Z.gcd q 2 = 1.
Proof.
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.
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.