Theory CryptHOL_ext

theory CryptHOL_ext

imports CryptHOL.Cyclic_Group_SPMF "HOL-Computational_Algebra.Polynomial" 
  Berlekamp_Zassenhaus.Finite_Field Polynomial_Interpolation.Polynomial_Interpolation

begin

section ‹Extensions to CryptHOL›

text ‹Here we collect a handful of lemmas about CryptHOL games, that we use in our proofs.
These lemmas are particularly useful to resort asserts (assert\_spmf) within games and to prove 
so-called bridging steps i.e. subtle differences in games, as they allow to ``peel off layers''
of a game.›

lemma ennreal_spmf: "ennreal (spmf game1 True) ≤ ennreal (spmf game2 True) ⟹ 
  spmf game1 True ≤ spmf game2 True"
  by simp

lemma unpack_bind_spmf: "X = X' ⟹ bind_spmf X Y = bind_spmf X' Y"
  by simp

lemma unpack_bind_spmf': "Y = Y' ⟹ bind_spmf X Y = bind_spmf X Y'"
  by simp

lemma unpack_bind_spmf_fun: "X = X' ⟹ bind_spmf X (λy. f y) = bind_spmf X' (λy. f y)"
  by (fact CryptHOL_ext.unpack_bind_spmf)

lemma unpack_try_spmf: "X = X' ⟹ TRY X ELSE Y = TRY X' ELSE Y"
  by simp

lemma unpack_try_spmf': "Y = Y' ⟹ TRY X ELSE Y = TRY X ELSE Y'"
  by simp

lemma spmf_eqI': "X = X' ⟹ spmf X Y = spmf X' Y"
  by simp

subsection ‹SPMF True›

lemma return_spmf_assert: "TRY return_spmf X ELSE return_spmf False = 
  TRY bind_spmf (assert_spmf X) (λ_. return_spmf True) ELSE return_spmf False"
  by (simp add: try_bind_assert_spmf)

lemma bind_spmf_independent_return_spmf: 
  "lossless_spmf x ⟹ bind_spmf x (λx. return_spmf y) = return_spmf y"
  by (simp add: bind_eq_return_spmf)
  
lemma bind_spmf_le:
  "(⋀x. spmf (f x) True ≤ spmf (f' x) True) ⟹ spmf (bind_spmf p f) True ≤ spmf (bind_spmf p f') True"
  apply (simp add: spmf_bind integral_measure_spmf)
  apply (rule integral_mono)
    apply (rule integrableI_bounded)
     apply simp
    apply (smt (verit, del_insts) ennreal_less_top ennreal_spmf_bind infinity_ennreal_def nn_integral_cong pmf_nonneg real_norm_def)
   apply (rule integrableI_bounded)
    apply simp
   apply (smt (verit, del_insts) ennreal_less_top ennreal_spmf_bind infinity_ennreal_def nn_integral_cong pmf_nonneg real_norm_def)
  apply simp
  done

lemma try_spmf_eq:
  assumes "spmf x True = spmf x' True"
  shows "spmf (TRY x ELSE return_spmf False) True = spmf (TRY x' ELSE return_spmf False) True"
  apply (simp add: spmf_try_spmf)
  apply (rule assms)
  done
  
lemma try_spmf_le:
  assumes "spmf x True ≤ spmf x' True"
  shows "spmf (TRY x ELSE return_spmf False) True ≤ spmf (TRY x' ELSE return_spmf False) True"
  apply (rule ennreal_spmf)
  apply (simp add: spmf_try_spmf)
  apply (rule assms)
  done

lemma try_spmf_true_else_false_le: "spmf (TRY X ELSE return_spmf False) True ≤ spmf X True"   
  by (simp add: spmf_try_spmf)

lemma del_assert: "spmf (bind_spmf (assert_spmf X) (λ_ . Y)) True ≤ spmf Y True"
  apply (rule ennreal_spmf)
  apply (simp add: spmf_try_spmf ennreal_spmf_bind)
  apply (simp add: mult_left_le measure_spmf.emeasure_space_le_1)
  done

lemma assert_imp: "(X ⟶ X') ⟹ 
  spmf (bind_spmf (assert_spmf X) (λ_ . Y)) True 
  ≤ spmf (bind_spmf (assert_spmf X') (λ_ . Y)) True"
  using del_assert by fastforce

lemma assert_ret_unit: "bind_spmf (assert_spmf x) (λx . y) = bind_spmf (assert_spmf x) (λ_ . y)"
  by presburger

lemma assert_based_eq: 
  assumes "x ⟹ y = y'"
  shows "bind_spmf (assert_spmf x) (λ_ . y)
  = bind_spmf (assert_spmf x) (λ_ . y')"
  by (auto simp add: assms assert_spmf_def)

lemma assert_commute: "bind_spmf X (λx. bind_spmf (assert_spmf Y) (λ_. Z x)) 
  = bind_spmf (assert_spmf Y) (λ_. bind_spmf X (λx. Z x))"
  by (rule bind_commute_spmf)

lemma assert_collapse: "bind_spmf (assert_spmf X) (λ_. bind_spmf (assert_spmf Y) (λ_. Z)) = 
   bind_spmf (assert_spmf (X ∧ Y)) (λ_. Z)"
  by (smt (verit) assert_spmf_simps(1,2) return_None_bind_spmf return_bind_spmf)

lemma assert_cong: " X = Y ⟹ rel_spmf (=) (assert_spmf X) (assert_spmf Y)"
  by (simp add: spmf_rel_eq)

lemma rel_spmf_bind_assert_reflI: "(Z ⟹ rel_spmf P X Y) ⟹ 
  rel_spmf P (bind_spmf (assert_spmf Z) (λ_. X)) (bind_spmf (assert_spmf Z) (λ_. Y))"
  using rel_spmf_bind_reflI by fastforce


text ‹We provide sampling of uniform random sets and lists. 
Additionally, we provide uniform sampling of polynomials over finite fields and show them equivalent 
to interpolating on a zipped list of coordinates where the evaluations are a uniformly random 
chosen list.›

subsection ‹Sample uniform set›

definition sample_uniform_set :: "nat ⇒ nat ⇒ nat set spmf"
  where "sample_uniform_set k n = spmf_of_set {x. x ⊆ {..<n} ∧ card x = k}"

lemma spmf_sample_uniform_set: "spmf (sample_uniform_set k n) x 
  = indicator {x. x ⊆ {..<n} ∧ card x = k} x / (n choose k)"
  by (simp add: n_subsets sample_uniform_set_def spmf_of_set)

lemma weight_sample_uniform_set: "weight_spmf (sample_uniform_set k n) = of_bool (k≤n)"
  apply (simp add: sample_uniform_set_def weight_spmf_of_set split: if_splits)
  apply (rule conjI)
   apply (metis card_lessThan card_mono finite_lessThan)
  using card_lessThan by blast

lemma weight_sample_uniform_set_k_0 [simp]: "weight_spmf (sample_uniform_set 0 n) = 1"
  by (auto simp add: weight_sample_uniform_set)

lemma weight_sample_uniform_set_n_0 [simp]: "weight_spmf (sample_uniform_set k 0) = of_bool (k=0)"
  by (auto simp add: weight_sample_uniform_set)

lemma weight_sample_uniform_set_k_le_n [simp]: "k≤n ⟹ weight_spmf (sample_uniform_set k n) = 1"
  by (auto simp add: weight_sample_uniform_set indicator_def gr0_conv_Suc)

lemma lossless_sample_uniform_set [simp]: "lossless_spmf (sample_uniform_set k n) ⟷ k ≤ n"
  by (auto simp add: lossless_spmf_def weight_sample_uniform_set intro: ccontr)

lemma set_spmf_sample_uniform_set [simp]: "set_spmf (sample_uniform_set k n) = {x. x ⊆ {..<n} ∧ card x = k}"
  by(simp add: sample_uniform_set_def)


subsection ‹Sample uniform list›

definition sample_uniform_list :: "nat ⇒ nat ⇒ nat list spmf"
  where "sample_uniform_list k n = spmf_of_set {x. set x ⊆ {..<n} ∧ length x = k}"

lemma spmf_sample_uniform_list: "spmf (sample_uniform_list k n) x 
  = indicator {x. set x ⊆ {..<n} ∧ length x = k} x / (n^k)"
  by (simp add: card_lists_length_eq sample_uniform_list_def spmf_of_set)

lemma weight_sample_uniform_list: "weight_spmf (sample_uniform_list k n) = of_bool (k=0 ∨ 0<n)"
proof -
  have "0 < n ⟶ (∃x. set x ⊆ {..<n} ∧ length x = k)"
  proof
    assume zero_l_n: "0 < n"
    show "∃x. set x ⊆ {..<n} ∧ length x = k"
    proof 
      let ?x = "replicate k 0"
      show "set ?x ⊆ {..<n} ∧ length ?x = k"
        using zero_l_n by fastforce
    qed
  qed
  then show ?thesis 
    by (simp add: finite_lists_length_eq sample_uniform_list_def weight_spmf_of_set)
qed
  
lemma weight_sample_uniform_list_k_0 [simp]: "weight_spmf (sample_uniform_list 0 n) = 1"
  by (auto simp add: weight_sample_uniform_list)

lemma weight_sample_uniform_list_n_0 [simp]: "weight_spmf (sample_uniform_list k 0) = of_bool (k=0)"
  by (auto simp add: weight_sample_uniform_list)

lemma weight_sample_uniform_list_k_le_n [simp]: "k<n ⟹ weight_spmf (sample_uniform_list k n) = 1"
  by (auto simp add: weight_sample_uniform_list less_iff_Suc_add)

lemma lossless_sample_uniform_list [simp]: "lossless_spmf (sample_uniform_list k n) ⟷ (k=0 ∨ 0<n)"
  by (auto simp add: lossless_spmf_def weight_sample_uniform_list intro: ccontr)

lemma set_spmf_sample_uniform_list [simp]: "set_spmf (sample_uniform_list k n) = {x. set x ⊆ {..<n} ∧ length x = k}"
  by (simp add: finite_lists_length_eq sample_uniform_list_def)

text ‹the two following lemmas are helping lemmas for Cons\_random\_list\_split›

lemma set_spmf_lhs: "set_spmf (map_spmf ((#) x) (sample_uniform_list k p)) 
             = {xs. set (tl xs) ⊆ {..<p} ∧ length xs = k+1 ∧ hd xs = x}"
proof -
  fix x
  have "set_spmf (map_spmf ((#) x) (sample_uniform_list k p)) 
    = ((#) x) ` {xs. set xs ⊆ {..<p} ∧ length xs = k}" 
    unfolding sample_uniform_list_def
    by (simp add: finite_lists_length_eq)
  also have "… = {xs. set (tl xs) ⊆ {..<p} ∧ length xs = k+1 ∧ hd xs = x}"
  proof (rule equalityI; rule subsetI)
    fix ys assume "ys ∈ (#) x ` {xs. set xs ⊆ {..<p} ∧ length xs = k}"
    then obtain zs where "zs ∈ {xs. set xs ⊆ {..<p} ∧ length xs = k}" and "ys = x # zs"
      by blast
    then show "ys ∈ {xs. set (tl xs) ⊆ {..<p} ∧ length xs = k+1 ∧ hd xs = x}"
      by simp
  next
    fix ys assume ys: "ys ∈ {xs. set (tl xs) ⊆ {..<p} ∧ length xs = k+1 ∧ hd xs = x}"
    then have facts: "set (tl ys) ⊆ {..<p}" "length ys = k+1" "hd ys = x" by simp_all
    then obtain a zs where azs: "ys = a # zs" and len_zs: "length zs = k"
      by (metis Suc_eq_plus1 Suc_length_conv)
    have "ys = x # zs" using azs facts by simp
    moreover have "zs ∈ {xs. set xs ⊆ {..<p} ∧ length xs = k}"
      using azs facts len_zs by simp
    ultimately show "ys ∈ (#) x ` {xs. set xs ⊆ {..<p} ∧ length xs = k}"
      by (metis image_eqI)
  qed
  finally show "set_spmf (map_spmf ((#) x) (sample_uniform_list k p)) 
      = {xs. set (tl xs) ⊆ {..<p} ∧ length xs = k + 1 ∧ hd xs = x}"
    .
qed

lemma set_spmf_lhs_imp_length_gr_0: "xs ∈ set_spmf (map_spmf ((#) x) (sample_uniform_list k p)) 
  ⟹ length xs > 0"
  unfolding set_spmf_lhs by force

text ‹sampling a uniform random list can be split up into prepending a uniform random element
to a one element short uniform random list. 
Intuitively: sample\_uniform\_list (k+1) = Cons (sample\_uniform) (sample\_uniform\_list k)›
lemma Cons_random_list_split: 
  assumes "p>1"
  shows "do {x ← sample_uniform p;
            map_spmf ((#) x) (sample_uniform_list k p)} = sample_uniform_list (k+1) p"
  (is "?lhs = ?rhs")
proof -
  have "∀s. spmf ?lhs s = spmf ?rhs s"
  proof 
    fix s
    have spmf_rhs: "spmf ?rhs s = indicator {x. set x ⊆ {..<p} ∧ length x = k+1} s / real p^(k+1)"
      unfolding spmf_sample_uniform_list ..
    have spmf_lhs: "spmf ?lhs s 
        = (∑x<p. ennreal (spmf (map_spmf ((#) x) (sample_uniform_list k p)) s)) 
        / of_nat (card {..<p})"
        unfolding ennreal_spmf_bind
        unfolding sample_uniform_def
        unfolding nn_integral_spmf_of_set
        ..
    show "spmf ?lhs s = spmf ?rhs s"
    proof (cases s)
      case Nil
      have "spmf ?lhs s = 0"
      proof -
        have "⋀x. spmf (map_spmf ((#) x) (sample_uniform_list k p)) s = 0"
          using set_spmf_lhs set_spmf_lhs_imp_length_gr_0 spmf_eq_0_set_spmf
          unfolding Nil 
          by fast
        then show ?thesis 
         using spmf_lhs by force
      qed
      moreover have "spmf ?rhs s = 0"
        using spmf_rhs 
        unfolding Nil
        by force
      ultimately show ?thesis by presburger
    next
      case (Cons s_hd s_tl)
      then show ?thesis
      proof (cases "s_hd<p")
        case True
        have "spmf ?lhs s
          = (indicator {x. set x ⊆ {..<p} ∧ length x = k} s_tl / (real p^(k+1)))"
        proof - 
          have spmf_is_sum: "spmf ?lhs s = 
              sum (λx. ennreal (spmf (map_spmf ((#) x) (sample_uniform_list k p)) s)) {..<p} 
              / real (card {..<p})"
                unfolding spmf_lhs
                using ennreal_of_nat_eq_real_of_nat by presburger
          also have "sum (λx. ennreal (spmf (map_spmf ((#) x) (sample_uniform_list k p)) s)) {..<p}
          = sum (λx. ennreal (spmf (map_spmf ((#) x) (sample_uniform_list k p)) s)) (({..<p}-{s_hd}) ∪ {s_hd})"
            by (simp add: True insert_absorb)
          also have "… = sum (λx. ennreal (spmf (map_spmf ((#) x) (sample_uniform_list k p)) s)) ({..<p}-{s_hd})
            + ennreal (spmf (map_spmf ((#) s_hd) (sample_uniform_list k p)) s)"
            by (metis (no_types, lifting) Un_insert_right add.commute dual_order.refl finite_nat_iff_bounded insert_Diff_single sum.insert_remove sup_bot.right_neutral)
          also have "… = ennreal (spmf (map_spmf ((#) s_hd) (sample_uniform_list k p)) s)"
          proof -
            have "⋀x. x ∈ {..<p}-{s_hd} ⟶ ennreal (spmf (map_spmf ((#) x) (sample_uniform_list k p)) s) = 0"
            proof 
              fix x 
              assume "x ∈ {..<p} - {s_hd}"
              then have "x ≠ s_hd" by blast
              then show "ennreal (spmf (map_spmf ((#) x) (sample_uniform_list k p)) s) = 0"
                using set_spmf_lhs 
                unfolding Cons 
                by (simp add: spmf_eq_0_set_spmf)
            qed
            then show ?thesis by force
          qed
          also have "… = ennreal (spmf (sample_uniform_list k p) s_tl)"
            unfolding Cons
            using spmf_map_inj
            by (simp add: spmf_map_inj')
          also have "… = indicator {x. set x ⊆ {..<p} ∧ length x = k} s_tl / (real p^k)"
            unfolding spmf_sample_uniform_list ..
          finally have "ennreal (spmf ?lhs s) = ennreal ((indicator {x. set x ⊆ {..<p} ∧ length x = k} s_tl / (real p^k))) /  ennreal (real (card {..<p}))"
            by argo
          then have "spmf ?lhs s = (indicator {x. set x ⊆ {..<p} ∧ length x = k} s_tl / (real p^k)) / (real (card {..<p}))"
            using assms(1) divide_ennreal by auto
          also have "… = (indicator {x. set x ⊆ {..<p} ∧ length x = k} s_tl / (real p^(k+1)))"
            by auto
          finally show ?thesis .
        qed

        moreover have "spmf ?rhs s
          = (indicator {x. set x ⊆ {..<p} ∧ length x = k} s_tl / (real p^(k+1)))"
        proof -
          have "(s_hd # s_tl) ∈ {x. set x ⊆ {..<p} ∧ length x = k + 1} 
          ⟷ s_tl ∈ {x. set x ⊆ {..<p} ∧ length x = k}"
            by (simp add: True)
          then show ?thesis
            unfolding spmf_sample_uniform_list Cons
            by (metis (no_types, lifting) indicator_simps(1) indicator_simps(2))
        qed
        ultimately show ?thesis by presburger
      next
        case False
        have "spmf ?lhs s = 0"
      proof -
        have "⋀x. x<p ⟶ spmf (map_spmf ((#) x) (sample_uniform_list k p)) s = 0"
          unfolding Cons 
          using set_spmf_lhs spmf_eq_0_set_spmf False
          by fastforce
        then show ?thesis
         using spmf_lhs by force
      qed
      moreover have "spmf ?rhs s = 0"
        using spmf_rhs 
        unfolding Cons
        using False
        by fastforce
      ultimately show ?thesis by presburger
      qed
    qed
  qed
  then show ?thesis
    using spmf_eqI by blast
qed

text ‹This corollary puts the last lemma in a more readable and thus workable definition.
Intuitively: sample\_uniform\_list (k+1) = Cons (sample\_uniform) (sample\_uniform\_list k)›
corollary pretty_Cons_random_list_split: 
  assumes "p>1"
  shows "sample_uniform_list (k+1) p =
    do {x ← sample_uniform p;
        xs ← (sample_uniform_list k p);
        return_spmf (x#xs)}"
  (is "?lhs = ?rhs")
proof -
  have "?rhs = do {x ← sample_uniform p;
          map_spmf ((#) x) (sample_uniform_list k p)}"
    by (simp add: map_spmf_conv_bind_spmf)
  then show ?thesis 
    using Cons_random_list_split[symmetric, OF assms]
    by presburger
qed

subsection ‹Sample uniform polynomial›

definition sample_uniform_poly :: "nat ⇒ 'a::zero poly spmf" 
  where "sample_uniform_poly t = spmf_of_set {p. degree p ≤ t}"

lemma of_int_mod_inj_on_ff: "inj_on (of_int_mod_ring ∘ int:: nat ⇒ 'e::prime_card mod_ring) {..<CARD ('e)}"
proof 
  fix x 
  fix y
  assume x: "x ∈ {..<CARD('e)}"
  assume y: "y ∈ {..<CARD('e)}"
  assume app_x_eq_y: "(of_int_mod_ring ∘ int:: nat ⇒ 'e mod_ring) x = (of_int_mod_ring ∘ int:: nat ⇒ 'e mod_ring) y"
  show "x = y"
    using x y app_x_eq_y 
    by (metis comp_apply lessThan_iff nat_int of_nat_0_le_iff of_nat_less_iff to_int_mod_ring_of_int_mod_ring)
qed

text ‹sampling a uniform random polynomial is equivalent to interpolating a polynomial from a list 
of uniform random chosen evaluations›
lemma sample_uniform_evals_is_sample_poly:
  assumes "distinct I"
  and "length I = t+1"
  shows "(sample_uniform_poly t::'e mod_ring poly spmf) = do {
      evals::('e::prime_card) mod_ring list ← map_spmf (map (of_int_mod_ring ∘ int:: nat ⇒ 'e mod_ring)) (sample_uniform_list (t+1) (CARD ('e)));
      return_spmf (lagrange_interpolation_poly (zip I evals))}"
  (is "?lhs = ?rhs")
proof -
  have "?rhs = do {
      evals ← spmf_of_set {x::'e mod_ring list. length x = t + 1};
      return_spmf (lagrange_interpolation_poly (zip I evals))}"
  proof - 
    have uni_list_set_is_card_set: "(⋃ (set ` {x::nat list. set x ⊆ {..<CARD('e)} ∧ length x = t + (1::nat)})) 
      = {..<CARD('e)}"
    proof 
      show "{..<CARD('e)} ⊆ ⋃ (set ` {x::nat list. set x ⊆ {..<CARD('e)} ∧ length x = t + (1::nat)})"
      proof 
        fix x 
        assume "x ∈ {..<CARD('e)}"
        then have "replicate (t+1) x ∈ {x::nat list. set x ⊆ {..<CARD('e)} ∧ length x = t + (1::nat)}"
          by fastforce
        then show "x ∈ ⋃ (set ` {x::nat list. set x ⊆ {..<CARD('e)} ∧ length x = t + (1::nat)})"
          by fastforce
      qed
    qed auto
    have "map_spmf (map (of_int_mod_ring ∘ int:: nat ⇒ 'e mod_ring)) (sample_uniform_list (t + 1) CARD('e))
    = spmf_of_set ((map (of_int_mod_ring ∘ int:: nat ⇒ 'e mod_ring)) ` {x. set x ⊆ {..<CARD('e)} ∧ length x = t+1})"
    (is "?map = ?set")
      unfolding sample_uniform_list_def
      apply (rule map_spmf_of_set_inj_on)
      apply (rule inj_on_mapI)
      unfolding uni_list_set_is_card_set
      by (rule of_int_mod_inj_on_ff)
    also have "(map (of_int_mod_ring ∘ int:: nat ⇒ 'e mod_ring)) ` {x. set x ⊆ {..<CARD('e)} ∧ length x = t+1} 
      = {x::'e mod_ring list. length x = t + 1}"
    proof 
      show "{x::'e mod_ring list. length x = t + (1::nat)}
        ⊆ map (of_int_mod_ring ∘ int:: nat ⇒ 'e mod_ring) ` {x::nat list. set x ⊆ {..<CARD('e)} ∧ length x = t + (1::nat)}"
      proof 
        fix x 
        assume asm: "x ∈ {x::'e mod_ring list. length x = t + (1::nat)}"
        obtain x_int where x_int : "x_int = map to_int_mod_ring x" by force
        have x_eq_map_x_int: "x = map of_int_mod_ring x_int"
          unfolding x_int 
          by (simp add: nth_equalityI)
        obtain x_nat where x_nat: "x_nat = map nat x_int" by simp
        have x_int_x_nat: "x_int = map int x_nat"
        proof -
          have "map int x_nat =  map (λi. if i≥0 then i else 0)  x_int"
            unfolding x_nat using int_nat_eq by simp
          moreover have "∀x ∈ set x_int. x≥0"
            unfolding x_int 
            using range_to_int_mod_ring
            by (metis atLeastLessThan_iff ex_map_conv rangeI)
          ultimately show ?thesis
            by (simp add: map_idI)
        qed
        have "x_nat ∈ {x::nat list. set x ⊆ {..<CARD('e)} ∧ length x = t + (1::nat)}"
          unfolding x_nat x_int
          apply (rule CollectI, rule conjI)
           apply (simp only: set_map)
           apply (rule subsetI)
           apply (metis range_to_int_mod_ring UNIV_I atLeastLessThan_iff image_iff nat_less_iff lessThan_iff)
          using asm by simp
        moreover have "x = map (of_int_mod_ring ∘ int:: nat ⇒ 'e mod_ring) x_nat"
          by (simp add: x_eq_map_x_int x_int_x_nat)
        ultimately show "x ∈ map (of_int_mod_ring ∘ int:: nat ⇒ 'e mod_ring) 
          ` {x::nat list. set x ⊆ {..<CARD('e)} ∧ length x = t + (1::nat)}"
          by blast
      qed
    qed auto
    finally show ?thesis by metis
  qed
  also have "… =  do {
      evals ← spmf_of_set {x::'e mod_ring list. length x = t + 1};
      let φ = lagrange_interpolation_poly (zip I evals);
      return_spmf φ}" unfolding Let_def ..
  also have "… = map_spmf (λevals. lagrange_interpolation_poly (zip I evals)) 
                         (spmf_of_set {x::'e mod_ring list. length x = t + 1})"
    by (simp add: map_spmf_conv_bind_spmf)
  also have "… = spmf_of_set ((λevals. lagrange_interpolation_poly (zip I evals)) ` {x::'e mod_ring list. length x = t + 1})"
  proof (rule map_spmf_of_set_inj_on)
    show "inj_on (λevals::'e mod_ring list. lagrange_interpolation_poly (zip I evals))
     {x::'e mod_ring list. length x = t + (1::nat)}"
    proof 
      fix x y
      assume x_in:"x ∈ {x::'e mod_ring list. length x = t + (1::nat)}"
      assume y_in:"y ∈ {x::'e mod_ring list. length x = t + (1::nat)}"
      assume asm: "lagrange_interpolation_poly (zip I x) = lagrange_interpolation_poly (zip I y)"
      have poly_xi: "⋀i. i<length I ⟹ poly (lagrange_interpolation_poly (zip I x)) (I!i) = x!i"
        using lagrange_interpolation_poly[of "zip I x" "lagrange_interpolation_poly (zip I x)"]
        assms(1)
        by (smt (verit, del_insts) assms(2) length_zip map_fst_zip mem_Collect_eq min_less_iff_conj nth_mem nth_zip x_in)
      have poly_y: "⋀i. i<length I ⟹ poly (lagrange_interpolation_poly (zip I y)) (I!i) = y!i"
        using lagrange_interpolation_poly[of "zip I y" "lagrange_interpolation_poly (zip I y)"]
        assms(1)
        by (smt (verit, del_insts) assms(2) length_zip map_fst_zip mem_Collect_eq min_less_iff_conj nth_mem nth_zip y_in)
      then have "⋀i. i<length I ⟹ poly (lagrange_interpolation_poly (zip I x)) (I!i) = y!i"
        using asm by presburger
      then show "x=y"
        using poly_y assms(2) x_in y_in
        by (simp add: nth_equalityI poly_xi)
    qed
  qed
  also have "… = spmf_of_set {p. degree p ≤ t}"
    (is "?map = ?set")
  proof -
    have "{p. degree p ≤ t} = (λevals::'e mod_ring list. lagrange_interpolation_poly (zip I evals)) `
      {x::'e mod_ring list. length x = t + (1::nat)}"
    proof 
      show "{p::'e mod_ring poly. degree p ≤ t}
    ⊆ (λevals::'e mod_ring list. lagrange_interpolation_poly (zip I evals)) `
       {x::'e mod_ring list. length x = t + (1::nat)}"
      proof 
        fix x 
        assume asm: "x ∈ {p::'e mod_ring poly. degree p ≤ t}"
        obtain x_evals where x_evals: "x_evals = map (λi. poly x i) I" by simp
        then have "length x_evals = t+1"
          by (simp add: assms(2))
        moreover have "x = lagrange_interpolation_poly (zip I x_evals)"
          apply (rule uniqueness_of_interpolation_point_list[of "zip I x_evals" x "lagrange_interpolation_poly (zip I x_evals)"])
              apply (simp add: assms(1) x_evals)
             apply (metis fst_eqD in_set_zip nth_map snd_eqD x_evals)
          using asm assms(2) calculation apply force
           apply (metis assms(1) assms(2) calculation lagrange_interpolation_poly map_fst_zip)
          apply (metis Suc_eq_plus1 assms(2) calculation degree_lagrange_interpolation_poly diff_Suc_1 le_refl length_zip less_Suc_eq min.absorb1 order.strict_trans1)
          done
        ultimately show "x ∈ (λevals::'e mod_ring list. lagrange_interpolation_poly (zip I evals)) `
            {x::'e mod_ring list. length x = t + (1::nat)}"
          by blast
      qed
      show "(λevals::'e mod_ring list. lagrange_interpolation_poly (zip I evals)) `
    {x::'e mod_ring list. length x = t + (1::nat)}
    ⊆ {p::'e mod_ring poly. degree p ≤ t}"
      proof 
        fix x 
        assume asm: "x ∈ (λevals::'e mod_ring list. lagrange_interpolation_poly (zip I evals)) `
            {x::'e mod_ring list. length x = t + (1::nat)}"
        then show "x ∈ {p::'e mod_ring poly. degree p ≤ t}"
          using degree_lagrange_interpolation_poly
          by (smt (verit) Nat.le_diff_conv2 One_nat_def Suc_eq_plus1 add_leE diff_Suc_1 diff_is_0_eq image_iff le_trans length_zip mem_Collect_eq min.absorb1 min.absorb2 nat_le_linear plus_1_eq_Suc zero_le)
      qed
    qed
    then show ?thesis by argo
  qed
  finally show ?thesis 
    unfolding sample_uniform_poly_def by argo
qed

end