section ‹Modular Inverses
›
theory Modular_Inverse
imports Cong
"HOL-Library.FuncSet"
begin
text ‹
The following returns the unique number $m$ such that $mn
\equiv 1
\pmod{p}$
if there
is one,
i.e.
\ if $n$
and $p$ are coprime,
and otherwise $0$
by convention.
›
definition modular_inverse
where
"modular_inverse p n = (if coprime p n then fst (bezout_coefficients n p) mod p else 0)"
lemma cong_modular_inverse1:
assumes "coprime n p"
shows "[n * modular_inverse p n = 1] (mod p)"
proof -
have "[fst (bezout_coefficients n p) * n + snd (bezout_coefficients n p) * p =
modular_inverse p n * n + 0] (mod p)
"
unfolding modular_inverse_def
using assms
by (intro cong_add cong_mult) (auto simp: Cong.cong_def coprime_commute)
also have "fst (bezout_coefficients n p) * n + snd (bezout_coefficients n p) * p = gcd n p"
by (simp add: bezout_coefficients_fst_snd)
also have "\ = 1"
using assms
by simp
finally show ?thesis
by (simp add: cong_sym mult_ac)
qed
lemma cong_modular_inverse2:
assumes "coprime n p"
shows "[modular_inverse p n * n = 1] (mod p)"
using cong_modular_inverse1[OF assms]
by (simp add: mult.commute)
lemma coprime_modular_inverse [simp, intro]:
fixes n ::
"'a :: {euclidean_ring_gcd,unique_euclidean_semiring}"
assumes "coprime n p"
shows "coprime (modular_inverse p n) p"
using cong_modular_inverse1[OF assms] assms
by (meson cong_imp_coprime cong_sym coprime_1_left coprime_mult_left_iff)
lemma modular_inverse_int_nonneg:
"p > 0 \ modular_inverse p (n :: int) \ 0"
by (simp add: modular_inverse_def)
lemma modular_inverse_int_less:
"p > 0 \ modular_inverse p (n :: int) < p"
by (simp add: modular_inverse_def)
lemma modular_inverse_int_eqI:
fixes x y :: int
assumes "y \ {0.. "[x * y = 1] (mod m)"
shows "modular_inverse m x = y"
proof -
from assms have "coprime x m"
using cong_gcd_eq by force
have "[modular_inverse m x * 1 = modular_inverse m x * (x * y)] (mod m)"
by (rule cong_sym, intro cong_mult assms cong_refl)
also have "modular_inverse m x * (x * y) = (modular_inverse m x * x) * y"
by (simp add: mult_ac)
also have "[\ = 1 * y] (mod m)"
using ‹coprime x m› by (intro cong_mult cong_refl cong_modular_inverse2)
finally have "[modular_inverse m x = y] (mod m)"
by simp
thus "modular_inverse m x = y"
using assms by (simp add: Cong.cong_def modular_inverse_def)
qed
lemma modular_inverse_1 [simp]:
assumes "m > (1 :: int)"
shows "modular_inverse m 1 = 1"
by (rule modular_inverse_int_eqI) (use assms in auto)
lemma modular_inverse_int_mult:
fixes x y :: int
assumes "coprime x m" "coprime y m" "m > 0"
shows "modular_inverse m (x * y) = (modular_inverse m y * modular_inverse m x) mod m"
proof (rule modular_inverse_int_eqI)
show "modular_inverse m y * modular_inverse m x mod m \ {0..
using assms by auto
next
have "[x * y * (modular_inverse m y * modular_inverse m x mod m) =
x * y * (modular_inverse m y * modular_inverse m x)] (mod m)"
by (intro cong_mult cong_refl) auto
also have "x * y * (modular_inverse m y * modular_inverse m x) =
(x * modular_inverse m x) * (y * modular_inverse m y)"
by (simp add: mult_ac)
also have "[\ = 1 * 1] (mod m)"
by (intro cong_mult cong_modular_inverse1 assms)
finally show "[x * y * (modular_inverse m y * modular_inverse m x mod m) = 1] (mod m)"
by simp
qed
lemma bij_betw_int_remainders_mult:
fixes a n :: int
assumes a: "coprime a n"
shows "bij_betw (\m. a * m mod n) {1..
proof -
define a' where "a' = modular_inverse n a"
have *: "a' * (a * m mod n) mod n = m \ a * m mod n \ {1..
if a: "[a * a' = 1] (mod n)" and m: "m \ {1.. for m a a' :: int
proof
have "[a' * (a * m mod n) = a' * (a * m)] (mod n)"
by (intro cong_mult cong_refl) (auto simp: Cong.cong_def)
also have "a' * (a * m) = (a * a') * m"
by (simp add: mult_ac)
also have "[(a * a') * m = 1 * m] (mod n)"
unfolding a'_def by (intro cong_mult cong_refl) (use a in auto)
finally show "a' * (a * m mod n) mod n = m"
using m by (simp add: Cong.cong_def)
next
have "coprime a n"
using a coprime_iff_invertible_int by auto
hence "\n dvd (a * m)"
using m by (simp add: coprime_commute coprime_dvd_mult_right_iff zdvd_not_zless)
hence "a * m mod n > 0"
using m order_le_less by fastforce
thus "a * m mod n \ {1..
using m by auto
qed
have "[a * a' = 1] (mod n)" "[a' * a = 1] (mod n)"
unfolding a'_def by (rule cong_modular_inverse1 cong_modular_inverse2; fact)+
from this[THEN *] show ?thesis
by (intro bij_betwI[of _ _ _ "\m. a' * m mod n"]) auto
qed
lemma mult_modular_inverse_of_not_coprime [simp]: "\coprime a m \ modular_inverse m a = 0"
by (simp add: coprime_commute modular_inverse_def)
lemma mult_modular_inverse_eq_0_iff:
fixes a :: "'a :: {unique_euclidean_semiring, euclidean_ring_gcd}"
shows "\is_unit m \ modular_inverse m a = 0 \ \coprime a m"
by (metis coprime_modular_inverse mult_modular_inverse_of_not_coprime coprime_0_left_iff)
lemma mult_modular_inverse_int_pos: "m > 1 \ coprime a m \ modular_inverse m a > (0 :: int)"
by (simp add: modular_inverse_int_nonneg mult_modular_inverse_eq_0_iff order.strict_iff_order)
lemma abs_mult_modular_inverse_int_less: "m \ 0 \ \modular_inverse m a :: int\ < \m\"
by (auto simp: modular_inverse_def intro!: abs_mod_less)
lemma modular_inverse_int_less': "m \ 0 \ (modular_inverse m a :: int) < \m\"
using abs_mult_modular_inverse_int_less[of m a] by linarith
end
