Theory Preliminary_Lemmas

(*
Title: Preliminary Lemmas for Number Theoretic Transform
Author: Thomas Ammer
*)

theory Preliminary_Lemmas
 imports Berlekamp_Zassenhaus.Finite_Field 
         "HOL-Number_Theory.Number_Theory"
begin

section ‹Preliminary Lemmas›

subsection ‹A little bit of Modular Arithmetic›

text ‹An obvious lemma. Just for simplification.›

lemma two_powrs_div:
  assumes "j < (i::nat) "
  shows "((2^i) div ((2::nat)^(Suc j)))*2 =  ((2^i) div (2^j))"
proof-
  have "((2::nat)^i) div (2^(Suc j)) = 2^(i -1) div(2^ j)" using assms 
    by (smt (z3) One_nat_def add_le_cancel_left diff_Suc_Suc div_by_Suc_0 div_if less_nat_zero_code plus_1_eq_Suc power_diff_power_eq zero_neq_numeral)
  thus ?thesis 
    by (metis Suc_diff_Suc Suc_leI assms less_imp_le_nat mult.commute power_Suc power_diff_power_eq zero_neq_numeral)
qed

lemma two_powr_div:
  assumes "j < (i::nat) "
  shows "((2^i) div ((2::nat)^j)) =  2^(i-j)" 
  by (simp add: assms less_or_eq_imp_le power_diff)


text ‹
  The order of an element is the same whether we consider it as an integer or as a natural number.
›
(* TODO: Move *)
lemma ord_int: "ord (int p) (int x) = ord p x"
proof (cases "coprime p x")
  case False
  thus ?thesis
    by (auto simp: ord_def)
next
  case True
  have "(LEAST d. 0 < d  [int x ^ d = 1] (mod int p)) = ord p x"
  proof (intro Least_equality conjI)
    show "[int x ^ ord p x = 1] (mod int p)"
      using True by (metis cong_int_iff of_nat_1 of_nat_power ord_works)
    show "ord p x  y" if "0 < y  [int x ^ y = 1] (mod int p)" for y
      using that by (metis cong_int_iff int_ops(2) linorder_not_less of_nat_power ord_minimal)
  qed (use True in auto)
  thus ?thesis
    by (auto simp: ord_def)
qed

lemma not_residue_primroot_1:
  assumes "n > 2"
  shows   "¬residue_primroot n 1"
  using assms totient_gt_1[of n] by (auto simp: residue_primroot_def)

lemma residue_primroot_not_cong_1:
  assumes "residue_primroot n g" "n > 2"
  shows   "[g  1] (mod n)"
  using residue_primroot_cong not_residue_primroot_1 assms by metis  


text ‹
We want to show the existence of a generating element of $\mathbb{Z}_p$ where $p$ is prime.
\label{primroot1} ›

text ‹Non-trivial order of an element $g$ modulo $p$ in a ring  implies $g\neq1$.
Although this lemma applies to all rings, it's only intended to be used in connection with $nat$s or $int$s
›

lemma prime_not_2_order_not_1:
  assumes "prime p"
          "p > 2 "
          "ord p g > 2"
  shows   "g  1"
proof
  assume "g = 1"
  hence "ord p g = 1" unfolding ord_def
    by (simp add: Least_equality)
  then show False using assms by auto
qed

text ‹The same for modular arithmetic.›

lemma prime_not_2_order_not_1_mod:
 assumes "prime p "
         "p > 2 "
         "ord p g > 2"
 shows   "[g  1] (mod p)"
proof
  assume "[g = 1] (mod p)"
  hence "ord p g = 1" unfolding ord_def
    by(split if_split, metis assms(1) assms(2) assms(3) ord_cong prime_not_2_order_not_1)
  then show False using assms by auto
qed

text ‹
Now we formulate our lemma about generating elements in residue classes:
There is an element $g \in \mathbb{Z}_p$ such that for any $x \in \mathbb{Z}_p$ 
there is a natural $i$ such that $g^i \equiv x \; (\mod p)$.›

lemma generator_exists:
  assumes "prime (p::nat)" "p > 2"
  shows " g. [g  1] (mod p)  ( x. (0<x  x < p ) ( i. [g^i = x] (mod p)))"
proof-
  obtain g where g_prim_root:"residue_primroot p g" 
    using assms prime_gt_1_nat prime_primitive_root_exists
    by (metis One_nat_def)
  have g_not_1: "[g  1] (mod p)"
    using residue_primroot_not_cong_1 assms g_prim_root by blast

  have "i. [g ^ i = x] (mod p)" if x_bounds: "x > 0" "x < p" for x
  proof -
    have 1:"coprime p x" 
      using assms prime_nat_iff'' x_bounds by blast
    have 2:"ord p g = p-1"
      by (metis assms(1) g_prim_root residue_primroot_def totient_prime)
    hence bij: "bij_betw (λi. g ^ i mod p) {..<totient p} (totatives p)"
      using residue_primroot_is_generator[of p g] totatives_def[of p] 
          1 totient_def[of p] assms g_prim_root prime_gt_1_nat by blast
    have 3:"x mod p  totatives p" 
      by (simp add: "1" coprime_commute in_totatives_iff order_le_less x_bounds)
    have " {..<totient p}  {}" 
      by (metis assms(1) lessThan_empty_iff prime_nat_iff'' totient_0_iff)
   then obtain i where "g^i mod p = x mod p" 
      using bij_betw_inv[of "(λi. g ^ i mod p)" "{..<totient p}" "(totatives p)"] 
      3 bij 
      by (metis (no_types, lifting) bij_betw_iff_bijections)
   then show ?thesis
     using cong_def by blast
  qed
  thus ?thesis
    using g_prim_root g_not_1 by auto
qed

subsection ‹General Lemmas in a Finite Field›

text ‹
\label{primroot2}
We make certain assumptions:
From now on, we will calculate in a finite field which is the ring of integers modulo a prime $p$.
Let $n$ be the length of vectors to be transformed. 
By Dirichlet's theorem on arithmetic progressions we can
 assume that there is a natural number $k$ and a prime $p$ with $p = k\cdot n + 1$.
In order to avoid some special cases and even contradictions, 
we additionally assume that $p \geq 3$ and $n \geq 2$. 
›

text ‹\label{prelim}›
locale preliminary = 
  fixes
       a_type::"('a::prime_card) itself" 
   and p::nat
   and n::nat 
   and k::nat
 assumes
       p_def: "p= CARD('a)" and p_lst3: "p > 2"  and p_fact: "p = k*n +1"
   and n_lst2: "n  2" 
begin

lemma exp_rule: "((c::('a) mod_ring) * d )^e= (c^e) * (d^e)" 
  by (simp add: power_mult_distrib)

lemma " y. x  0  (x::(('a) mod_ring)) *  y = 1" 
  by (metis dvd_field_iff unit_dvdE)

lemma test: "prime p" 
  by (simp add: p_def prime_card)

lemma k_bound: "k > 0" 
  using p_fact prime_nat_iff'' test by force

text ‹We show some homomorphisms.›

lemma homomorphism_add: "(of_int_mod_ring x)+(of_int_mod_ring y) = 
              ((of_int_mod_ring  (x+y)) ::(('a::prime_card) mod_ring))"
  by (metis of_int_hom.hom_add of_int_of_int_mod_ring)

lemma homomorphism_mul_on_ring: "(of_int_mod_ring x)*(of_int_mod_ring y) =  
              ((of_int_mod_ring  (x*y)) ::(('a::prime_card) mod_ring))"
  by (metis of_int_mult of_int_of_int_mod_ring)

lemma exp_homo:"(of_int_mod_ring (x^i)) = ((of_int_mod_ring x)^i ::(('a::prime_card) mod_ring))"
  by (induction i) (metis of_int_of_int_mod_ring of_int_power)+

lemma mod_homo: "((of_int_mod_ring x)::(('a::prime_card) mod_ring)) = of_int_mod_ring (x mod p)"
  using p_def unfolding of_int_mod_ring_def by simp

lemma int_exp_hom: "int x ^i = int (x^i)" 
  by simp

lemma coprime_nat_int: "coprime (int p) (to_int_mod_ring pr)  coprime p (nat(to_int_mod_ring pr))"
  unfolding coprime_def to_int_mod_ring_def 
  by (smt (z3) Rep_mod_ring atLeastLessThan_iff dvd_trans int_dvd_int_iff int_nat_eq int_ops(2) prime_divisor_exists prime_nat_int_transfer primes_dvd_imp_eq test to_int_mod_ring.rep_eq to_int_mod_ring_def)

lemma nat_int_mod:"[nat (to_int_mod_ring pr) ^ d = 1] (mod p) = 
                           [ (to_int_mod_ring pr) ^ d = 1] (mod (int p)) "
  unfolding to_int_mod_ring_def 
  by (metis Rep_mod_ring atLeastLessThan_iff cong_int_iff int_exp_hom int_nat_eq int_ops(2) to_int_mod_ring.rep_eq to_int_mod_ring_def)

text ‹Order of $p$ doesn't change when interpreting it as an integer.›

lemma ord_lift: "ord (int p) (to_int_mod_ring pr) = ord p (nat (to_int_mod_ring pr))"
proof -
  have "to_int_mod_ring pr = int (nat (to_int_mod_ring pr))"
    by (metis Rep_mod_ring atLeastLessThan_iff int_nat_eq to_int_mod_ring.rep_eq)
  thus ?thesis
    using ord_int by metis
qed

text ‹A primitive root has order $p-1$.›

lemma primroot_ord: "residue_primroot p g  ord p g = p -1" 
  by (simp add: residue_primroot_def test totient_prime)

text ‹If $x^l = 1$ in $\mathbb{Z}_p$, then $l$ is an upper bound for the order of $x$ in $\mathbb{Z}_ p$.›

lemma ord_max:
  assumes "l  0" "(x :: (('a::prime_card) mod_ring))^l = 1"
  shows " ord p (to_int_mod_ring x)  l"
proof-
  have "[(to_int_mod_ring x)^l = 1] (mod p)" 
    by (metis assms(2) cong_def exp_homo of_int_mod_ring.rep_eq of_int_mod_ring_to_int_mod_ring one_mod_card_int one_mod_ring.rep_eq p_def)
  thus ?thesis unfolding ord_def using assms 
    by (smt (z3) Least_le less_imp_le_nat not_gr0)
qed

subsection ‹Existence of $n$-th Roots of Unity in the Finite Field›

text ‹
\label{primroot3}
We obtain an element in the finite field such that
its reinterpretation as a $nat$ will be a primitive root in the residue class modulo $p$.
The difference between residue classes, their representatives in the Integers and elements 
of the finite field is notable. When conducting informal proofs, this distinction
 is usually blurred, but Isabelle enforces the explicit conversion between those structures.
›

lemma primroot_ex:
  obtains primroot::"('a::prime_card) mod_ring" where 
    "primroot^(p-1) = 1"
    "primroot  1"
    "residue_primroot p (nat (to_int_mod_ring primroot))"
proof-
  obtain g where g_Def: "residue_primroot p g  g  1" 
    using prime_nat_iff' prime_primitive_root_exists test 
    by (metis bigger_prime euler_theorem ord_1_right power_one_right prime_nat_iff'' residue_primroot.cases residue_primroot_cong)
  hence "[g  1] (mod p)" using prime_not_2_order_not_1_mod[of p g]
    by (metis One_nat_def p_lst3 less_numeral_extra(4) ord_eq_Suc_0_iff residue_primroot.cases totient_gt_1)
  hence "[g^(p-1) = 1] (mod p)" using g_Def
    by (metis coprime_commute euler_theorem residue_primroot_def test totient_prime)
  moreover hence "int (g ^ (p - 1)) mod int p = (1::int)" 
    by (metis cong_def int_ops(2) mod_less of_nat_mod prime_gt_1_nat test)
  moreover hence "of_int_mod_ring (int (g ^ (p - 1)) mod int p) = 
                      ((of_int_mod_ring 1) ::(('a::prime_card) mod_ring))" by simp
  ultimately have "(of_int_mod_ring (g^(p-1))) = (1 ::(('a::prime_card) mod_ring))" 
    using mod_homo[of "g^(p-1)"]  by (metis exp_homo power_0)
  hence "((of_int_mod_ring g)^(p-1) ::(('a::prime_card) mod_ring)) = 1" 
    using exp_homo[of "int g" "p-1"] by simp
  moreover 
  have "((of_int_mod_ring g) ::(('a::prime_card) mod_ring))  1" 
  proof
    assume "((of_int_mod_ring g) ::(('a::prime_card) mod_ring)) = 1"
    hence "[int g = 1] (mod p)" using p_def unfolding of_int_mod_ring_def 
      by (metis of_int_mod_ring (int g) = 1 cong_def of_int_mod_ring.rep_eq one_mod_card_int one_mod_ring.rep_eq)
    hence "[g=1] (mod p)"
      by (metis cong_int_iff int_ops(2))
    thus False 
      using [g  1] (mod p) by auto
  qed
  moreover have residue_primroot p (g mod p)
    using g_Def by simp
  then have residue_primroot p (nat (to_int_mod_ring (of_int_mod_ring (int g) :: 'a mod_ring)))
    by (transfer fixing: p) (simp add: p_def nat_mod_distrib)
  ultimately show thesis ..
qed

text ‹From this, we obtain an $n$-th root of unity $\omega$ in the finite 
field of characteristic $p$.
 Note that in this step we will use the assumption $p = k \cdot n +1$ 
from locale $preliminary$: The $k$-th power of a primitive 
root $pr$ modulo $p$ will have the property $(pr^k)^n \equiv 1 \mod p$.
›

lemma omega_properties_ex: 
  obtains ω ::"(('a::prime_card) mod_ring)" 
  where  "ω^n = 1" 
         "ω  1"  
         " m. ω^m = 1  m0  m  n"
proof-
  obtain pr::"(('a::prime_card) mod_ring)" where a: "pr^(p-1) = 1 " and b: "pr  1"
              and c: "residue_primroot p (nat( to_int_mod_ring pr))"
    using primroot_ex by blast
  moreover hence "(pr^k)^n =1" 
    by (simp add: p_fact power_mult)
  moreover have "pr^k  1"
  proof
    assume " pr ^ k = 1"
    hence "(to_int_mod_ring pr)^k mod p = 1"
      by (metis exp_homo of_int_mod_ring.rep_eq of_int_mod_ring_to_int_mod_ring one_mod_ring.rep_eq p_def)
    hence "ord p (to_int_mod_ring pr)  k"
      by (simp add: pr ^ k = 1 k_bound ord_max)
    hence "ord p (nat (to_int_mod_ring pr))  k" 
      by (metis ord_lift)
    also have "ord p (nat (to_int_mod_ring pr)) = p - 1"
      using c primroot_ord[of "(nat (to_int_mod_ring pr))"] by blast
    also have " = k * n"
      using p_fact by simp
    finally have "n  1"
      using k_bound by simp
    thus False
      using n_lst2 by linarith
  qed
  moreover have " m. (pr^k)^m = 1  m0  m  n"
  proof(rule ccontr)
    assume  "¬ (m. (pr ^ k) ^ m = 1  m0  n  m) "
    then obtain m where "(pr^k)^m = 1   m0  m < n" by force
    hence "ord p (to_int_mod_ring pr)  k * m" using ord_max[of "k*m" pr]
      by (metis calculation(5) mult_is_0 power_mult) 
    moreover have "ord p (nat (to_int_mod_ring pr)) = p-1" using c primroot_ord ord_lift by simp
    ultimately show False 
      by (metis (pr ^ k) ^ m = 1  m  0  m < n add_diff_cancel_right' nat_0_less_mult_iff nat_mult_le_cancel_disj not_less ord_lift p_def p_fact prime_card prime_gt_1_nat zero_less_diff)
  qed
    ultimately show ?thesis
    using that by simp
qed

text ‹We define an $n$-th root of unity $\omega$ for $NTT$.›
theorem omega_exists: " ω ::(('a::prime_card) mod_ring) .
                              ω^n = 1  ω  1  ( m. ω^m = 1  m0  m  n)"
  using omega_properties_ex by metis

definition "(omega::(('a::prime_card) mod_ring)) = 
       (SOME ω . (ω^n = 1  ω  1 ( m. ω^m = 1  m0  m  n)))"

lemma omega_properties: "omega^n = 1" "omega  1" 
  "( m. omega^m = 1  m0  m  n)"
  unfolding omega_def using omega_exists 
  by (smt (verit, best) verit_sko_ex')+

text ‹We define the multiplicative inverse $\mu$ of $\omega$.›

definition "mu = omega ^ (n - 1)"

lemma mu_properties: "mu * omega = 1" "mu  1" 
proof -
  have "omega ^ (n - 1) * omega = omega ^ Suc (n - 1)"
    by simp
  also have "Suc (n - 1) = n"
    using n_lst2 by simp
  also have "omega ^ n = 1"
    using omega_properties(1) by auto
  finally show "mu * omega = 1"
    by (simp add: mu_def)
next
  show "mu  1"
    using omega_properties n_lst2 by (auto simp: mu_def)
qed

subsection ‹Some Lemmas on Sums›
text ‹\label{sums}›

text ‹The following lemmas concern sums over a finite field. 
 Most of the propositions are intuitive.›

lemma sum_in: "(i=0..<(x::nat). f i * (y ::('a mod_ring))) = (i=0..<x. f i )* (y) "
  by(induction x) (auto simp add: algebra_simps)

lemma sum_eq: "( i. i < x  f i = g i)
                     (i=0..<(x::nat). f i) = (i=0..<x. g i) " 
  by(induction x) (auto simp add: algebra_simps)

lemma sum_diff_in: "(i=0..<(x::nat). (f i)::('a mod_ring)) - (i=0..<x. g i) = 
                    (i=0..<x. f i - g i)"
 by(induction x) (auto simp add: algebra_simps)

lemma sum_swap: "(i=0..<(x::nat). j=0..<(y::nat). f i j) = 
                 (j=0..<(y::nat). i=0..<(x::nat). f i j ) "
  using Groups_Big.comm_monoid_add_class.sum.swap by fast

lemma sum_const: "(i=0..<(x::nat). (c::('a::prime_card) mod_ring)) = (of_int_mod_ring x) * c" 
  by(induction x, simp add: algebra_simps,  simp add: algebra_simps)
    (metis distrib_left mult.right_neutral of_int_of_int_mod_ring of_int_of_nat_eq of_nat_Suc)

lemma sum_split: "(r1::nat) < r2  (l = 0..<r1. ((f l)::(('a::prime_card) mod_ring))) 
                                         +(l = r1..<r2. f l) = (l = 0..<r2. f l)" 
  by (meson less_or_eq_imp_le sum.atLeastLessThan_concat zero_le)

lemma sum_index_shift: "(l = (a::nat)..< b. f(l+c)) = (l = (a+c)..< (b+c). f l )"
  by(induction a arbitrary: b c) (metis sum.shift_bounds_nat_ivl)+

text ‹One may sum over even and odd indices independently.
The lemma statement was taken from a formalization of FFT~\parencite{FFT-AFP}. 
We give an alternative proof adapted to the finite field $\mathbb{Z}_p$. 
›

lemma sum_splice:
  "(i::nat = 0..<2*nn. f i) = (i = 0..<nn. f (2*i)) + (i = 0..<nn. f (2*i+1))"
proof(induction nn)
  case (Suc n)
  have "(i::nat = 0..<2*(n+1). f i)  = (i::nat = 0..<(2*n). f i) + f(2*n+1) + f (2*n)" 
    by( simp add: algebra_simps)
  also have " = (i::nat = 0..<n. f (2*i)) + (i::nat = 0..<n. f (2*i+1)) + f(2*n+1) + f (2*n)"
    using Suc by simp
  also have " = (i::nat = 0..<(Suc n). f (2*i)) + (i::nat = 0..<(Suc n). f (2*i+1))"
   by( simp add: algebra_simps)
  finally show ?case by simp
qed simp

lemma sum_even_odd_split: "even (a::nat)  (j=0..<(a div 2). f (2*j))+ (j=0..<(a div 2). f (2*j+1)) =  (j=0..<a. f j)"
  by (induction a, simp)(metis even_two_times_div_two sum_splice)

lemma sum_splice_other_way_round: " (j=(0::nat)..<i. f (2*j)) + (j=0..<i. f (2*j+1)) = 
        (j=(0::nat)..<2*i. f j )"
by (metis sum_splice)

lemma sum_neg_in: "- (j = 0..<l. (f j)::('a mod_ring)) =  (j = 0..<l. - f j) " 
  by (simp add: sum_negf)

subsection ‹Geometric Sums›

text ‹\label{geosum}›

text ‹This lemma will be important for proving properties on $\mathsf{NTT}$. At first, an informal proof sketch:
\begin{align*}
(1-x) \cdot \sum \limits _{l = 0} ^ {r-1} x^l 
&= \sum \limits _{l = 0} ^ {r-1} x^l  - x \cdot \sum \limits _{l = 0} ^{r-1} x^l \\ 
&= \sum \limits _{l = 0} ^ {r-1} x^l  - \sum \limits _{l = 1} ^{r} x^l \\ 
& = 1 - x^r
\end{align*}

The same lemma for integers can be found in~\parencite{Dirichlet_Series-AFP}.
 Our version is adapted to finite fields.
›

lemma geo_sum: 
  assumes "x  1"
  shows "(1-x)*(l = 0..<r. (x::('a mod_ring))^l) = (1-x^r)"
proof-
  have 0:"x * (l = 0..<r. x^l) = (l = 0..<r. x^(Suc l))" using sum_in[of "λ l. x^l" x r] 
    by(simp add: algebra_simps)
  have 1:"(l = 0..<r. x^l) - (l = 0..<r. x^(Suc l)) = (l = 0..<r. x^l - x^(Suc l))" 
    by(rule sum_diff_in)
  have 2: "(l = 0..<r. x^l - x^(Suc l)) = 1 - x^r"
    by(induction r) simp+
  thus ?thesis
    by (simp add: lessThan_atLeast0 one_diff_power_eq)
qed 

lemmas sum_rules = sum_in sum_eq sum_diff_in sum_swap sum_const sum_split sum_index_shift

end
end