Theory Finite_UNIV

theory Finite_UNIV
imports 
  "HOL-Analysis.Finite_Cartesian_Product"
  "CRYSTALS-Kyber.Kyber_spec"

begin
section ‹$R_q$ is Finite›

text ‹The module $R_q$ is finite. This can be reasoned in two steps: 
One, the set of possible coefficients of a polynomial in $R_q$ is finite since coefficients 
are in $\mathbb{z}_q$.
Two, the polynomials in $R_q$ have degree less than $n$.
Together, this implies that $R_q$ itself is a finite set.›



lemma card_UNIV_qr:
 "card (UNIV :: 'a::qr_spec qr set) = (CARD('a)) ^ (degree (qr_poly' TYPE('a)))"
proof -
  let ?q = "(CARD('a))"
  let ?n = "degree (qr_poly' TYPE('a))"
  have fin: "finite (UNIV :: 'a mod_ring set)" by simp
  then obtain f where "bij_betw f (UNIV::'a mod_ring set) {0..< ?q}"
    by (metis CARD_mod_ring ex_bij_betw_finite_nat)
  have rew:"(UNIV :: 'a qr set) = (to_qr ∘ Poly ) ` {xs :: 'a mod_ring list. length xs = ?n}"
  proof (safe, goal_cases)
    case (1 x)
    let ?xs = "coeffs (of_qr x)"
    define ys where "ys = ?xs @ replicate (?n-length ?xs) 0"
    have "length (coeffs (of_qr x)) ≤ degree (qr_poly' TYPE('a))"
    by (metis Suc_le_eq coeffs_eq_Nil deg_of_qr deg_qr_def length_coeffs_degree 
      list.size(3) zero_le)
    then have "length (coeffs (of_qr x)) + (degree (qr_poly' TYPE('a)) - length (coeffs (of_qr x))) =
      degree (qr_poly' TYPE('a))" by (subst add_diff_assoc) (auto simp add: 1)
    then have "length ys = ?n" unfolding ys_def by (auto) 
    moreover have "x = to_qr (Poly ys)" unfolding ys_def Poly_append_replicate_zero 
      Poly_coeffs to_qr_of_qr by simp
    ultimately have "∃ ys. length ys = ?n ∧ x = to_qr (Poly ys)" by blast
    then show ?case by force
  qed simp
  have "card (UNIV :: 'a qr set) = card {xs :: 'a mod_ring list. length xs = ?n}"
  proof (unfold rew, rule card_image, subst comp_inj_on_iff[symmetric], goal_cases)
    case 1
    then show ?case by (metis (mono_tags, lifting) coeff_Poly_eq inj_onI map_nth_default 
      mem_Collect_eq nat_int)
  next
    case 2
    then show ?case unfolding inj_on_def proof (safe, goal_cases)
      case (1 x xa y xb)
      moreover have "Poly xa mod qr_poly = Poly xa" using 1(1) 
        by (intro deg_mod_qr_poly) (metis coeff_Poly_eq deg_qr_pos degree_0 degree_qr_poly' 
          leading_coeff_0_iff nth_default_def)
      moreover have "Poly xb mod qr_poly = Poly xb" using 1(2)  
        by (intro deg_mod_qr_poly) (metis coeff_Poly_eq deg_qr_pos degree_0 degree_qr_poly' 
          leading_coeff_0_iff nth_default_def)
      ultimately show ?case unfolding to_qr_eq_iff  by (simp add: cong_def)
    qed
  qed
  also have "… = ?q^(?n)" using card_lists_length_eq[OF fin, of "nat ?n"] 
    by (auto)
  ultimately show ?thesis by auto
qed


lemma finite_qr [simp]:
  "finite (UNIV::'a::qr_spec qr set)" using card_UNIV_qr 
  by (metis card.infinite card_UNIV_option card_option nat.distinct(1) power_not_zero)

instantiation qr ::(qr_spec) finite
begin
instance
proof 
  show "finite (UNIV :: 'a ::qr_spec qr set)" using finite_qr by simp 
qed
end

text ‹Moreover, there are only finitely many vectors (of fixed length) over a finite types and
only finitely many matrices (of fixed dimension) over a finite type.
This yields that $R_q^k$ and $R_q^{k\times k}$ are both finite.›

lemma finite_vec: 
assumes "finite (UNIV :: 'a set)"
shows "finite (UNIV :: ('a, 'k::finite) vec set)"
proof -
  have "bij_betw vec_lambda (UNIV :: ('k ⇒ 'a) set) (UNIV :: ('a, 'k) vec set)" 
    by (metis UNIV_I bijI' vec_lambda_cases vec_lambda_inject)
  show ?thesis
  by (meson ‹bij vec_lambda› assms bij_betw_finite finite_UNIV_fun finite_class.finite_UNIV)
qed

lemma finite_mat:
assumes "finite (UNIV :: 'a set)"
shows "finite (UNIV :: (('a, 'k::finite) vec,'k) vec set)"
using finite_vec[OF finite_vec[OF assms]] by auto


lemma finite_UNIV_vec [simp]:
  "finite (UNIV:: ('a::qr_spec qr, 'k::finite) vec set)"
using finite_vec[OF finite_qr] .

lemma finite_UNIV_mat [simp]:
  "finite (UNIV:: (('a::qr_spec qr, 'k) vec, 'k::finite) vec set)"
using finite_mat[OF finite_qr] .

lemma finite_UNIV_vec_option [simp]:
  "finite (UNIV :: ('a::qr_spec qr,'k::finite option) vec set)"
by (simp add: finite_vec)

lemma finite_UNIV_mat_option [simp]:
  "finite (UNIV:: (('a::qr_spec qr, 'k::finite) vec, 'k option) vec set)"
using finite_vec[OF finite_qr] finite_vec by blast


end