Theory Approximate_Model_Counting.RandomXORHashFamily

section ‹Random XOR hash family›

text ‹This section defines a hash family based on random XORs and proves
  that this hash family is 3-universal. ›

theory RandomXORHashFamily imports
  RandomXOR
begin

lemma finite_dom:
  assumes "finite V"
  shows "finite {w :: 'a ⇀ bool. dom w = V}"
proof -
  have *: "{w :: 'a ⇀ bool. dom w = V} =
    {w. dom w = V ∧ ran w ⊆ {True,False}}"
    by auto
  show ?thesis unfolding *
    apply (intro finite_set_of_finite_maps)
    using assms by auto
qed

lemma xor_hash_eq_dom:
  assumes "xor_hash ω xors = α"
  shows "dom xors = dom α"
  using assms unfolding xor_hash_def
  by auto

lemma prob_random_xors_xor_hash_indicat_real:
  assumes V: "finite V"
  shows"
  measure_pmf.prob (random_xors V n)
    {xors. xor_hash ω xors = α} =
     indicat_real {α::nat ⇀ bool. dom α = {0..<n}} α /
     real (card {α::nat ⇀ bool. dom α = {0..<n}})"
proof -
  have *: "{α::nat ⇀ bool. dom α = {0..<n}} =
     {α. dom α = {0..<n} ∧ ran α ⊆ {True, False}}"
    by auto
  have **: "card {α::nat ⇀ bool. dom α = {0..<n}} = 2^n"
    unfolding *
    apply (subst card_dom_ran)
    by (auto simp add: numerals(2))
  have "dom α = {..<n} ∨ dom α ≠ {..<n}"
    by auto
  moreover {
    assume "dom α = {..<n}"
    from prob_random_xors_xor_hash[OF V this]
    have ?thesis
      unfolding **
      by (simp add: ‹dom α = {..<n}› atLeast0LessThan)
  }
  moreover {
    assume *:"dom α ≠ {..<n}"
    then have "x ∈ set_pmf (random_xors V n) ⟹
         α ≠ xor_hash ω x" for x
      by (metis (mono_tags, lifting) V mem_Collect_eq random_xors_set_pmf xor_hash_eq_dom)
    then have "measure_pmf.prob (random_xors V n)
     {xors. xor_hash ω xors = α} = 0"
      apply (intro measure_pmf.measure_exclude[where A = "set_pmf ((random_xors V n))"])
      by (auto simp add: Sigma_Algebra.measure_def emeasure_pmf xor_hash_eq_dom)
    then have ?thesis
      by (simp add: * atLeast0LessThan)
  }
  ultimately show ?thesis
    by auto
qed

lemma xor_hash_family_uniform:
  assumes V: "finite V"
  assumes "dom ω = V"
  shows "prob_space.uniform_on
         (random_xors V n)
         (xor_hash i) {α. dom α = {0..<n}}"
  apply (intro measure_pmf.uniform_onI[where p = "random_xors V n"])
  subgoal by clarsimp
  subgoal  using finite_dom by blast
  using prob_random_xors_xor_hash_indicat_real[OF V]
  by (auto intro!: exI[where x = "(λi. if i < n then Some True else None)"] split:if_splits)

lemma random_xors_xor_hash_pair_indicat:
  assumes V: "finite V"
  assumes ω: "dom ω = V"
  assumes ω': "dom ω' = V"
  assumes neq: "ω ≠ ω'"
  shows "
  measure_pmf.prob (random_xors V n)
    {xors.
      xor_hash ω xors = α ∧ xor_hash ω' xors = α'} =
  (measure_pmf.prob (random_xors V n)
    {xors.
      xor_hash ω xors = α} *
   measure_pmf.prob (random_xors V n)
    {xors.
      xor_hash ω' xors = α'})"
proof -
  have "dom α = {..<n} ∧ dom α' = {..<n} ∨
    ¬(dom α = {..<n} ∧ dom α' = {..<n})" by auto
  moreover {
    assume *: "dom α = {..<n}" "dom α' = {..<n}"
    have "measure_pmf.prob (random_xors V n)
     {xors.
      xor_hash ω xors = α ∧ xor_hash ω' xors = α'} = 1 / 4 ^n"
      by (simp add: "*"(1) "*"(2) assms(1) assms(2) assms(3) assms(4) random_xors_xor_hash_pair)
    moreover have "
    measure_pmf.prob (random_xors V n)
      {xors.  xor_hash ω xors = α} = 1/2^n"
      by (simp add: "*"(1) assms(1) prob_random_xors_xor_hash)
    moreover have "
    measure_pmf.prob (random_xors V n)
      {xors.  xor_hash ω' xors = α'} = 1/2^n"
      by (simp add: "*"(2) assms(1) prob_random_xors_xor_hash)
    ultimately have ?thesis
      by (metis (full_types) Groups.mult_ac(2) four_x_squared power2_eq_square power_mult power_one_over verit_prod_simplify(2))
  }
  moreover {
    assume *: "dom α ≠ {..<n} ∨ dom α' ≠ {..<n}"
    then have **: "x ∈ set_pmf (random_xors V n) ⟹
         α = xor_hash ω x ⟹
         α' = xor_hash ω' x ⟹ False" for x
      by (metis (mono_tags, lifting) CollectD assms(1) random_xors_set_pmf xor_hash_eq_dom)
    have "measure_pmf.prob (random_xors V n)
    {xors.
      xor_hash ω xors = α} = 0 ∨
     measure_pmf.prob (random_xors V n)
      {xors.
        xor_hash ω' xors = α'} = 0"
      unfolding prob_random_xors_xor_hash_indicat_real[OF V]
      by (metis (full_types) * atLeast0LessThan div_0 indicator_simps(2) mem_Collect_eq)
    moreover have "
    measure_pmf.prob (random_xors V n)
    {xors.
      xor_hash ω xors = α ∧ xor_hash ω' xors = α'} = 0"
      apply (intro measure_pmf.measure_exclude[where A = "set_pmf ((random_xors V n))"])
      using ** by (auto simp add: Sigma_Algebra.measure_def emeasure_pmf)
    ultimately have ?thesis by auto
  }
  ultimately show ?thesis by auto
qed

lemma prod_3_expand:
  assumes "a ≠ b" "b ≠ c" "c ≠ a"
  shows"(∏ω∈{a, b, c}. f ω) = f a * (f b * f c)"
  using assms by auto

lemma random_xors_xor_hash_three_indicat:
  assumes V: "finite V"
  assumes ω: "dom ω = V"
  assumes ω': "dom ω' = V"
  assumes ω'': "dom ω'' = V"
  assumes neq: "ω ≠ ω'" "ω' ≠ ω''" "ω'' ≠ ω"
  shows "
  measure_pmf.prob (random_xors V n)
    {xors.
      xor_hash ω xors = α
    ∧ xor_hash ω' xors = α'
    ∧ xor_hash ω'' xors = α''} =
  (measure_pmf.prob (random_xors V n)
    {xors.
      xor_hash ω xors = α} *
   measure_pmf.prob (random_xors V n)
    {xors.
      xor_hash ω' xors = α'} *
   measure_pmf.prob (random_xors V n)
    {xors.
      xor_hash ω'' xors = α''})"
proof -
  have "dom α = {..<n} ∧ dom α' = {..<n} ∧ dom α'' = {..<n} ∨
    ¬(dom α = {..<n} ∧ dom α' = {..<n} ∧ dom α'' = {..<n})" by auto
  moreover {
    assume *: "dom α = {..<n}" "dom α' = {..<n}" "dom α'' = {..<n}"
    have 1:"measure_pmf.prob (random_xors V n)
     {xors.
      xor_hash ω xors = α ∧
      xor_hash ω' xors = α' ∧
      xor_hash ω'' xors = α''} = 1 / 8 ^n"
      apply (intro random_xors_xor_hash_three)
      using V * ω ω' ω'' neq by auto
    have 2:"
    measure_pmf.prob (random_xors V n)
      {xors.  xor_hash ω xors = α} = 1/2^n"
      by (simp add: "*"(1) assms(1) prob_random_xors_xor_hash)
    have 3:"
    measure_pmf.prob (random_xors V n)
      {xors.  xor_hash ω' xors = α'} = 1/2^n"
      by (simp add: "*"(2) assms(1) prob_random_xors_xor_hash)
    have 4: "
    measure_pmf.prob (random_xors V n)
      {xors.  xor_hash ω'' xors = α''} = 1/2^n"
      by (simp add: "*"(3) assms(1) prob_random_xors_xor_hash)
    have ?thesis
      unfolding 1 2 3 4
      by (metis (mono_tags, opaque_lifting) arith_simps(11) arith_simps(12) arith_simps(58) divide_divide_eq_left mult.right_neutral power_mult_distrib times_divide_eq_right)
  }
  moreover {
    assume *: "dom α ≠ {..<n} ∨ dom α' ≠ {..<n} ∨ dom α'' ≠ {..<n}"
    then have **: "x ∈ set_pmf (random_xors V n) ⟹
         α = xor_hash ω x ⟹
         α' = xor_hash ω' x ⟹
         α'' = xor_hash ω'' x ⟹ False" for x
      by (metis (mono_tags, lifting) CollectD assms(1) random_xors_set_pmf xor_hash_eq_dom)
    have "measure_pmf.prob (random_xors V n)
    {xors.
      xor_hash ω xors = α} = 0 ∨
     measure_pmf.prob (random_xors V n)
      {xors.
        xor_hash ω' xors = α'} = 0 ∨
     measure_pmf.prob (random_xors V n)
      {xors.
        xor_hash ω'' xors = α''} = 0"
      unfolding prob_random_xors_xor_hash_indicat_real[OF V]
      by (metis (full_types) * atLeast0LessThan div_0 indicator_simps(2) mem_Collect_eq)
    moreover have "
    measure_pmf.prob (random_xors V n)
    {xors.
      xor_hash ω xors = α ∧ xor_hash ω' xors = α' ∧ xor_hash ω'' xors = α''} = 0"
      apply (intro measure_pmf.measure_exclude[where A = "set_pmf ((random_xors V n))"])
      using ** by (auto simp add: Sigma_Algebra.measure_def emeasure_pmf)
    ultimately have ?thesis by auto
  }
  ultimately show ?thesis
    by fastforce
qed

lemma xor_hash_3_indep:
  assumes V: "finite V"
  assumes J: "card J ≤ 3" "J ⊆ {α. dom α = V}"
  shows "
    measure_pmf.prob (random_xors V n)
      {xors. ∀ω∈J. xor_hash ω xors = f ω} =
       (∏ω∈J.
          measure_pmf.prob (random_xors V n)
           {xors. xor_hash ω xors = f ω})"
proof -
  have "card J = 0 ∨ card J = 1 ∨ card J = 2 ∨ card J = 3"
    using assms by auto
  moreover {
    assume" card J = 0"
    then have "J = {}"
      by (meson assms(1) assms(3) card_eq_0_iff finite_dom finite_subset)
    then have ?thesis
      by clarsimp
  }
  moreover {
    assume "card J = 1"
    then obtain x where "J = {x}"
      using card_1_singletonE by blast
    then have ?thesis
      by auto
  }
  moreover {
    assume "card J = 2"
    then obtain ω ω' where J:"J = {ω, ω'}" and
      ω: "ω ≠ ω'" "dom ω = V" "dom ω' = V"
      unfolding card_2_iff
      using J
      by force
    have ?thesis unfolding J
      by (auto simp add: random_xors_xor_hash_pair_indicat V ω)
  }
  moreover {
    assume "card J = 3"
    then obtain ω ω' ω'' where J:"J = {ω, ω', ω''}" and
      ω: "ω ≠ ω'" "ω' ≠ ω''" "ω'' ≠ ω"
        "dom ω = V" "dom ω' = V" "dom ω'' = V"
      unfolding card_3_iff
      using J
      by force
    have ?thesis unfolding J
      by (auto simp add: random_xors_xor_hash_three_indicat V ω  prod_3_expand[OF ω(1-3)])
  }
  ultimately show ?thesis by auto
qed

lemma xor_hash_3_wise_indep:
  assumes "finite V"
  shows "prob_space.k_wise_indep_vars
     (random_xors V n) 3
     (λ_. Universal_Hash_Families_More_Independent_Families.discrete) xor_hash
     {α. dom α = V}"
  apply (subst prob_space.k_wise_indep_vars_def)
  by (auto intro!: measure_pmf.indep_vars_pmf xor_hash_3_indep simp add: measure_pmf.prob_space_axioms assms card_mono dual_order.trans)

theorem xor_hash_family_3_universal:
  assumes "finite V"
  shows"prob_space.k_universal
    (random_xors V n) 3 xor_hash
    {α::'a ⇀ bool. dom α = V}
    {α::nat ⇀ bool. dom α = {0..<n}}"
  apply (subst prob_space.k_universal_def)
  subgoal by (clarsimp simp add: measure_pmf.prob_space_axioms )
  using xor_hash_3_wise_indep assms xor_hash_family_uniform assms by blast

corollary xor_hash_family_2_universal:
  assumes "finite V"
  shows"prob_space.k_universal
    (random_xors V n) 2 xor_hash
    {α::'a ⇀ bool. dom α = V}
    {α::nat ⇀ bool. dom α = {0..<n}}"
  using assms
  by (auto intro!: prob_space.k_universal_mono[OF _ _ xor_hash_family_3_universal] measure_pmf.prob_space_axioms)

end