Computation of a modular inverse, unsing a fast method
Require Import Coqlib.
Lemma succ_pred_double :
forall x,
Pos.succ (
Pos.pred_double x) =
Pos.mul 2
x.
Proof.
intros x.
induction x.
- reflexivity.
- simpl. rewrite IHx. reflexivity.
- reflexivity.
Qed.
Lemma div2_2x_1 :
forall x,
Z.div2 (2*
x + 1) =
x.
Proof.
Lemma a_plus_b_squared :
forall a b,
(
a +
b) * (
a +
b) =
a*
a +
a*
b*2 +
b*
b.
Proof.
Fast Bézout algorithm and specification
Fixpoint fast_bezout (
a:
Z) (
n:
nat) :
Z *
Z :=
match n with
|
O => (1, -
Z.div2 a)
|
S n' =>
let (
u,
v) :=
fast_bezout a n'
in
(
a*
u*
u +
u*(2 ^ (2 ^ (
Z.of_nat n')))*
v*2,
v*
v)
end.
Theorem fast_bezout_spec :
forall (
a:
Z) (
n:
nat),
Z.odd a =
true ->
let (
u,
v) := (
fast_bezout a n)
in
a *
u + (2 ^ (2 ^
Z.of_nat n)) *
v = 1.
Proof.
Fast modular inverse and specification
Definition fast_mod_inv (
a:
Z) (
n:
nat) :
Z :=
fst (
fast_bezout a n)
mod (2 ^ (2 ^
Z.of_nat n)).
Theorem fast_mod_inv_spec :
forall (
a:
Z) (
n:
nat),
Z.odd a =
true ->
((
a *
fast_mod_inv a n)
mod (2 ^ (2 ^
Z.of_nat n))) = 1.
Proof.
Fast identity insertion and specification
Definition fast_identity (
a b:
Z) (
n:
nat) :=
fun x =>
let c := (
fast_mod_inv a n)
in
let d := -
b *
c in
(
a*
x +
b) *
c +
d.
Theorem fast_identity_spec :
forall (
a b:
Z) (
n:
nat) (
x:
Z),
Z.odd a =
true ->
(
fast_identity a b n)
x mod (2 ^ (2 ^
Z.of_nat n)) =
x mod (2 ^ (2 ^
Z.of_nat n)).
Proof.