Theory ApproxMCAnalysis
section ‹ ApproxMC definition and analysis ›
text ‹
This section puts together preceding results to formalize the
PAC guarantee of ApproxMC.
›
theory ApproxMCAnalysis imports
ApproxMCCoreAnalysis
RandomXORHashFamily
Median_Method.Median
begin
lemma replicate_pmf_Pi_pmf:
assumes "distinct ls"
shows "replicate_pmf (length ls) P =
map_pmf (λf. map f ls)
(Pi_pmf (set ls) def (λ_. P))"
using assms
proof (induction ls)
case Nil
then show ?case
by auto
next
case (Cons x xs)
then show ?case
by (auto intro!: bind_pmf_cong simp add: Pi_pmf_insert' map_bind_pmf bind_map_pmf)
qed
lemma replicate_pmf_Pi_pmf':
assumes "finite V"
shows "replicate_pmf (card V) P =
map_pmf (λf. map f (sorted_list_of_set V))
(Pi_pmf V def (λ_. P))"
proof -
have *:"card V = length (sorted_list_of_set V)"
using assms by auto
show ?thesis
unfolding *
apply (subst replicate_pmf_Pi_pmf)
using assms by auto
qed
definition map_of_default::"('a × 'b) list ⇒ 'b ⇒ 'a ⇒ 'b"
where "map_of_default ls def =
(let m = map_of ls in
(λx. case m x of None ⇒ def | Some v ⇒ v))"
lemma Pi_pmf_replicate_pmf:
assumes "finite V"
shows
"(Pi_pmf V def (λ_. p)) =
map_pmf (λbs.
map_of_default (zip (sorted_list_of_set V) bs) def)
(replicate_pmf (card V) p)"
proof -
show ?thesis
apply (subst replicate_pmf_Pi_pmf'[OF assms, where def="def"])
unfolding map_pmf_comp
apply (intro map_pmf_idI[symmetric])
unfolding map_of_default_def Let_def fun_eq_iff map_of_zip_map
by (smt (verit, del_insts) assms option.case(1) option.case(2) pmf_Pi pmf_eq_0_set_pmf sorted_list_of_set.set_sorted_key_list_of_set)
qed
lemma proj_inter_neutral:
assumes "⋀w. w ∈ B ⟷ restr S w ∈ C"
shows "proj S (A ∩ B) = proj S A ∩ C"
unfolding ApproxMCCore.proj_def
using assms by auto
text ‹
An abstract spec of ApproxMC for any Boolean theory.
This locale must be instantiated with a theory implementing the two
the functions below (and satisfying the assumption linking them).
›
locale ApproxMC =
fixes sols :: "'fml ⇒ ('a ⇒ bool) set"
fixes enc_xor :: "'a set × bool ⇒ 'fml ⇒ 'fml"
assumes sols_enc_xor:
"⋀F xor. finite (fst xor) ⟹
sols (enc_xor xor F) =
sols F ∩ {ω. satisfies_xor xor {x. ω x}}"
begin
definition compute_thresh :: "real ⇒ nat"
where "compute_thresh ε =
nat ⌈1 + 9.84 * (1 + ε / (1 + ε)) * (1 + 1 / ε)^2⌉"
definition fix_t :: "real ⇒ nat"
where "fix_t δ =
nat ⌈ln (1 / δ) /(2 * (0.5-0.36)^2)⌉"
definition raw_median_bound :: "real ⇒ nat ⇒ real"
where "raw_median_bound α t =
(∑i = 0..t div 2.
(t choose i) * (1 / 2 + α) ^ i * (1 / 2 - α) ^ (t - i))"
definition compute_t :: "real ⇒ nat ⇒ nat"
where "compute_t δ n =
(if raw_median_bound 0.14 n < δ then n
else fix_t δ)"
definition size_xor ::"
'fml ⇒ 'a set ⇒
(nat ⇒ ('a set × bool) option) ⇒
nat ⇒ nat"
where "size_xor F S xorsf i = (
let xors = map (the ∘ xorsf) [0..<i] in
let Fenc = fold enc_xor xors F in
card (proj S (sols Fenc))
)"
definition check_xor ::"
'fml ⇒ 'a set ⇒
nat ⇒
(nat ⇒ ('a set × bool) option) ⇒
nat ⇒ bool"
where "check_xor F S thresh xorsf i =
(size_xor F S xorsf i < thresh)"
definition approxcore_xors :: "
'fml ⇒ 'a set ⇒
nat ⇒
(nat ⇒ ('a set × bool) option) ⇒
nat"
where "
approxcore_xors F S thresh xorsf =
(case List.find
(check_xor F S thresh xorsf) [1..<card S] of
None ⇒ 2 ^ card S
| Some m ⇒
(2 ^ m * size_xor F S xorsf m))"
definition approxmccore :: "'fml ⇒ 'a set ⇒ nat ⇒ nat pmf"
where "approxmccore F S thresh =
map_pmf (approxcore_xors F S thresh) (random_xors S (card S - 1))"
definition approxmc :: "'fml ⇒ 'a set ⇒ real ⇒ real ⇒ nat ⇒ nat pmf"
where "approxmc F S ε δ n = (
let thresh = compute_thresh ε in
if card (proj S (sols F)) < thresh then
return_pmf (card (proj S (sols F)))
else
let t = compute_t δ n in
map_pmf (median t)
(prod_pmf {0..<t::nat} (λi. approxmccore F S thresh))
)"
lemma median_commute:
assumes "t ≥ 1"
shows "(real ∘ median t) = (λw::nat ⇒ nat. median t (real ∘ w))"
proof -
have "real (median t x) = median t (real ∘ x)" for x
using assms by (intro median_commute_mono) (simp_all add:incseq_def)
thus ?thesis by auto
qed
lemma median_default:
shows "median t y = median t (λx. if x < t then y x else def)"
by (intro median_cong) auto
definition default_α::"'a set ⇒ nat assg"
where "default_α S i = (if i < card S - 1 then Some True else None)"
lemma dom_default_α:
"dom (default_α S) = {0..<card S -1}"
by (auto simp add:default_α_def split: if_splits)
lemma compute_thresh_bound_4:
assumes "ε > 0"
shows"4 < compute_thresh ε"
proof -
have 1: "(1 + ε / (1 + ε)) > 1"
using assms
by simp
have 2: "(1 + 1 / ε)^2 > 1"
using assms by simp
define a where "a = (1 + ε / (1 + ε)) * (1 + 1 / ε)⇧2"
have "a > 1" unfolding a_def
using 1 2
using less_1_mult by blast
then have "(984 / 10⇧2) * a ≥ 4"
by auto
thus ?thesis
unfolding compute_thresh_def
by (smt (verit) a_def arith_special(2) arithmetic_simps(1) more_arith_simps(11) nat_less_real_le numeral_Bit0 of_nat_numeral real_nat_ceiling_ge)
qed
lemma satisfies_xor_with_domain:
assumes "fst x ⊆ S"
shows "satisfies_xor x {x. w x} ⟷
satisfies_xor x ({x. w x} ∩ S)"
using assms
apply (cases x)
by (simp add: Int_assoc inf.absorb_iff2)
lemma approxcore_xors_eq:
assumes thresh:
"thresh = compute_thresh ε"
"thresh ≤ card (proj S (sols F))"
assumes ε: "ε > (0::real)" "ε ≤ 1"
assumes S: "finite S"
shows "measure_pmf.prob (random_xors S (card S - 1))
{xors. real (approxcore_xors F S thresh xors) ∈
{real (card (proj S (sols F))) / (1 + ε)..
(1 + ε) * real (card (proj S (sols F)))}} ≥ 0.64"
proof -
have "ApproxMCCore (sols F) S ε (default_α S) thresh"
apply unfold_locales
subgoal using dom_default_α by simp
subgoal using ε by simp
subgoal using thresh assms(3) compute_thresh_bound_4 by blast
using thresh S by auto
then interpret amc: ApproxMCCore "sols F" _ _ "(default_α S)" .
have "
m < card S ⟹
{0..<m} ⊆ dom xors ⟹
(⋀i. i < m ⟹ fst (the (xors i)) ⊆ S) ⟹
(proj S
(sols (fold enc_xor (map (the ∘ xors) [0..<m]) F))) =
proj S (sols F) ∩
{w. hslice m (λω. xor_hash ω xors) w =
aslice m (default_α S)}" for m xors
proof (induction m)
case 0
then show ?case
unfolding hslice_def aslice_def
by auto
next
case (Suc m)
have m: "m ∈ dom xors"
by (meson Set.basic_monos(7) Suc(3) atLeastLessThan_iff le0 lessI)
have sp: "fst (the (xors m)) ⊆ S"
by (simp add: Suc(4))
then obtain xor where x: "xors m = Some xor"
using m by blast
have eq: "{w. xor_hash w xors m = Some True} =
{ω. satisfies_xor xor {x. ω x = Some True}}"
unfolding xor_hash_def
by (clarsimp simp add: x)
have neut: "⋀w.
w ∈ {ω. satisfies_xor xor {x. ω x}} ⟷
restr S w ∈ {ω. satisfies_xor xor {x. ω x = Some True}}"
using sp unfolding restr_def
by (smt (verit, ccfv_SIG) Collect_cong Int_def mem_Collect_eq option.sel satisfies_xor_with_domain x)
have lhs: "
proj S
(sols (fold enc_xor (map (the ∘ xors) [0..<Suc m]) F)) =
proj S (sols (fold enc_xor (map (the ∘ xors) [0..<m]) F)) ∩
{w. xor_hash w xors m = Some True}"
apply clarsimp
apply (subst sols_enc_xor)
subgoal using assms(5) rev_finite_subset sp by blast
apply (subst proj_inter_neutral)
using eq neut x by auto
have rhs1:" hslice (Suc m) (λω. xor_hash ω xors) w = aslice (Suc m) (default_α S) ⟹
hslice m (λω. xor_hash ω xors) w = aslice m (default_α S)" for w
unfolding hslice_def aslice_def fun_eq_iff
by (auto simp add:lessThan_Suc restrict_map_def split: if_splits)
have rhs2:"hslice (Suc m) (λω. xor_hash ω xors) w = aslice (Suc m) (default_α S) ⟹
xor_hash w xors m = Some True" for w
unfolding hslice_def aslice_def fun_eq_iff
apply (clarsimp simp add:lessThan_Suc restrict_map_def )
by (metis default_α_def domIff m xor_hash_eq_dom)
have rhs3: "hslice m (λω. xor_hash ω xors) w = aslice m (default_α S) ⟹
xor_hash w xors m = Some True ⟹
hslice (Suc m) (λω. xor_hash ω xors) w = aslice (Suc m) (default_α S)" for w
unfolding hslice_def aslice_def fun_eq_iff
apply (clarsimp simp add:lessThan_Suc restrict_map_def )
by (metis One_nat_def Suc.prems(1) Suc_lessD Suc_less_eq Suc_pred default_α_def gr_zeroI zero_less_diff)
have rhs: "{w. hslice (Suc m) (λω. xor_hash ω xors) w = aslice (Suc m) (default_α S)} =
{w. hslice m (λω. xor_hash ω xors) w = aslice m (default_α S)} ∩
{w. xor_hash w xors m = Some True}"
by (auto simp add: rhs1 rhs2 rhs3)
have ih: "proj S (sols (fold enc_xor (map (the ∘ xors) [0..<m]) F)) =
proj S (sols F) ∩
{w. hslice m (λω. xor_hash ω xors) w = aslice m (default_α S)}"
apply (intro Suc(1))
using Suc(2) Suc_lessD apply blast
using Suc(3) atLeast0_lessThan_Suc apply blast
using Suc(4) less_SucI by blast
show ?case
unfolding lhs rhs
by (simp add: Int_ac(1) ih)
qed
then have *: "
m < card S ⟹
{0..<m} ⊆ dom xors ⟹
(⋀i. i < m ⟹ fst (the (xors i)) ⊆ S) ⟹
size_xor F S xors m =
amc.card_slice (λω. xor_hash ω xors) m" for m xors
unfolding size_xor_def amc.card_slice_def
by auto
have **: "
{0..<card S - 1} ⊆ dom xors ⟹
(⋀i. i < card S - 1 ⟹ fst (the (xors i)) ⊆ S) ⟹
find (check_xor F S thresh xors) [1..<card S] =
find (λi. (λω. xor_hash ω xors) ∈ amc.T i) [1..<card S]" for xors
apply (intro find_cong)
unfolding check_xor_def amc.T_def
subgoal by simp
apply (subst *)
subgoal by clarsimp
subgoal by (clarsimp simp add: domIff subset_iff)
by auto
have rw: "
{0..<card S - 1} ⊆ dom xors ⟹
(⋀i. i < card S - 1 ⟹ fst (the (xors i)) ⊆ S) ⟹
approxcore_xors F S thresh xors =
(λ(a,b). a*b) (amc.approxcore (λω. xor_hash ω xors))" for xors
apply (subst amc.approxcore_def)
unfolding approxcore_xors_def
apply (subst **)
subgoal by clarsimp
subgoal by clarsimp
apply (clarsimp split: option.split)
apply (subst *)
subgoal by (auto simp add: find_Some_iff domIff subset_iff)
subgoal by (auto simp add: find_Some_iff domIff subset_iff)
subgoal
using ‹⋀x2. ⟦{0..<card S - Suc 0} ⊆ dom xors; ⋀i. i < card S - Suc 0 ⟹ fst (the (xors i)) ⊆ S; find (λi. (λω. xor_hash ω xors) ∈ amc.T i) [Suc 0..<card S] = Some x2⟧ ⟹ x2 < card S› by auto
by auto
from xor_hash_family_2_universal[OF S]
have univ:"prob_space.k_universal (measure_pmf (random_xors S (card S - 1))) 2
xor_hash {α. dom α = S} {α. dom α = {0..<card S - 1}}" .
have "measure_pmf.prob
(map_pmf (λs w. xor_hash w s) (random_xors S (card S - 1)))
amc.approxcore_fail ≤ 0.36"
apply (intro amc.analysis_3[OF _ _ univ])
apply (smt (verit, ccfv_SIG) Groups.mult_ac(3) amc.pivot_def assms(1) compute_thresh_def more_arith_simps(11) real_nat_ceiling_ge)
using S finite_random_xors_set_pmf apply blast
using ε by auto
then have b: "measure_pmf.prob
(random_xors S (card S - 1))
{xors.
(real ((λ(a,b). a*b) (amc.approxcore (λω. xor_hash ω xors))))
∉
{real (card (proj S (sols F))) / (1 + ε)..
(1 + ε) * real (card (proj S (sols F)))}} ≤ 0.36"
unfolding amc.approxcore_fail_def
by (auto simp add: case_prod_unfold Let_def)
have 1: "x ∈ set_pmf (random_xors S (card S - Suc 0)) ⟹
{0..<card S - 1} ⊆ dom x" for x
by (auto simp add:random_xors_set_pmf[OF S])
have 2: "x ∈ set_pmf (random_xors S (card S - Suc 0)) ⟹
(∀i. i < card S - 1 ⟶ fst (the (x i)) ⊆ S)" for x
proof -
assume x: "x ∈ set_pmf (random_xors S (card S - Suc 0))"
moreover {
fix i
assume i: "i < card S - 1"
from random_xors_set_pmf[OF S]
have xx: "dom x = {..<(card S - Suc 0)}" "ran x ⊆ Pow S × UNIV"
using x by auto
obtain xi where xi: "x i = Some xi"
using xx i apply clarsimp
by (metis atLeast0LessThan atLeastLessThan_iff bot_nat_0.extremum domIff option.exhaust surj_pair)
then have "fst xi ⊆ S" using xx(2)
unfolding ran_def apply (clarsimp simp add: subset_iff)
by (metis prod.collapse)
then have "fst (the (x i)) ⊆ S" by (simp add: xi)
}
thus "(∀i. i < card S - 1 ⟶ fst (the (x i)) ⊆ S)" by auto
qed
have "measure_pmf.prob (random_xors S (card S - 1))
{xors. real (approxcore_xors F S thresh xors) ∈
{real (card (proj S (sols F))) / (1 + ε)..
(1 + ε) * real (card (proj S (sols F)))}} =
measure_pmf.prob
(random_xors S (card S - 1))
{xors.
(real ((λ(a,b). a*b) (amc.approxcore (λω. xor_hash ω xors))))
∈
{real (card (proj S (sols F))) / (1 + ε)..
(1 + ε) * real (card (proj S (sols F)))}}"
apply (intro measure_pmf.measure_pmf_eq[where p = "(random_xors S (card S - 1))"])
subgoal by auto
apply clarsimp
apply (frule 1)
apply (drule 2)
apply (frule rw)
by auto
moreover have "... =
1 - measure_pmf.prob
(random_xors S (card S - 1))
{xors.
(real ((λ(a,b). a*b) (amc.approxcore (λω. xor_hash ω xors))))
∉
{real (card (proj S (sols F))) / (1 + ε)..
(1 + ε) * real (card (proj S (sols F)))}}"
apply (subst measure_pmf.prob_compl[symmetric])
by (auto intro!: measure_pmf.measure_pmf_eq)
moreover have "... ≥ 0.64"
using b
by auto
ultimately show ?thesis by auto
qed
lemma compute_t_ge1:
assumes "0 < δ" "δ < 1"
shows"compute_t δ n ≥ 1"
proof -
have "ln (1 / δ) > 0"
by (simp add: assms)
then have fix_t: "1 ≤ fix_t δ"
unfolding fix_t_def
by (simp add: Suc_leI)
show ?thesis
unfolding compute_t_def
using fix_t
apply (cases n)
unfolding raw_median_bound_def
using assms by auto
qed
lemma success_arith_bound:
assumes "s ≤ (f ::nat)"
assumes "p ≤ (1::real)" "q ≤ p" "1 /2 ≤ q"
shows "p ^ s * (1 - p) ^ f ≤ q ^ s * (1 - q) ^ f"
proof -
have ple: "p * (1-p) ≤ q * (1-q)"
using assms(2-4)
by (sos "(((A<0 * R<1) + ((R<1 * (R<1 * [p + ~1*q]^2)) + ((A<=1 * (A<=2 * R<1)) * (R<2 * [1]^2)))))")
have feq:"f = (f-s)+s"
using Nat.le_imp_diff_is_add assms(1) by blast
then have "(1-p)^f = (1-p)^s * (1-p)^(f-s)"
by (metis add.commute power_add)
then have "p ^ s * (1 - p) ^ f =
(p * (1-p)) ^ s * (1 - p) ^ (f-s)"
by (simp add: power_mult_distrib)
moreover have "... ≤
(q * (1-q)) ^ s * (1 - p) ^ (f-s)"
by (smt (verit) assms(1) assms(2) assms(3) assms(4) diff_self_eq_0 divide_nonneg_nonneg mult_nonneg_nonneg mult_right_mono order_le_less ple power_0 power_eq_0_iff power_mono zero_less_diff zero_less_power)
moreover have "... ≤
(q * (1-q)) ^ s * (1 - q) ^ (f-s)"
by (smt (verit, ccfv_SIG) assms(2) assms(3) assms(4) divide_eq_0_iff divide_nonneg_nonneg mult_left_mono mult_pos_pos power_mono zero_less_power)
moreover have "... = q ^ s * (1 - q) ^ f"
by (smt (verit) feq mult.assoc mult.commute power_add power_mult_distrib)
ultimately show ?thesis by auto
qed
lemma prob_binomial_pmf_upto_mono:
assumes "1/2 ≤ q" "q ≤ p" "p ≤ 1"
shows "
measure_pmf.prob (binomial_pmf n p) {..n div 2} ≤
measure_pmf.prob (binomial_pmf n q) {..n div 2}"
proof -
have i: "i ≤ n div 2 ⟹
p ^ i * (1 - p) ^ (n - i) ≤ q ^ i * (1 - q) ^ (n - i)" for i
using assms by(auto intro!: success_arith_bound)
show ?thesis
apply (subst prob_binomial_pmf_upto)
subgoal using assms by auto
subgoal using assms by auto
apply (subst prob_binomial_pmf_upto)
subgoal using assms by auto
subgoal using assms by auto
by (auto intro!: sum_mono simp add: i ab_semigroup_mult_class.mult_ac(1) mult_left_mono)
qed
theorem approxmc_sound:
assumes δ: "δ > 0" "δ < 1"
assumes ε: "ε > 0" "ε ≤ 1"
assumes S: "finite S"
shows "measure_pmf.prob (approxmc F S ε δ n)
{c. real c ∈
{real (card (proj S (sols F))) / (1 + ε)..
(1 + ε) * real (card (proj S (sols F)))}}
≥ 1 - δ"
proof -
define thresh where "thresh = compute_thresh ε"
define t where "t = compute_t δ n"
then have t1: "1 ≤ t"
using compute_t_ge1[OF δ] by auto
have "card (proj S (sols F)) < thresh ∨
card (proj S (sols F)) ≥ thresh" by auto
moreover {
assume "card (proj S (sols F)) < thresh"
then have "approxmc F S ε δ n =
return_pmf (card (proj S (sols F)))"
unfolding approxmc_def Let_def thresh_def
by auto
then have "?thesis"
unfolding indicator_def of_bool_def
using assms ε
by (auto simp add: mult_le_cancel_left1 mult_le_cancel_right1 divide_le_eq)
}
moreover {
assume a: "card (proj S (sols F)) ≥ thresh"
define Xf where "Xf = (λ(i::nat) xs.
approxcore_xors F S thresh (xs i))"
then have *: "approxmc F S ε δ n =
map_pmf (median t)
(prod_pmf {0..<t} (λi. approxmccore F S thresh))"
using a
unfolding approxmc_def Let_def thresh_def t_def
by auto
have **: "map_pmf (real ∘ median t)
(Pi_pmf {0..<t} (approxcore_xors F S thresh undefined)
(λi. approxmccore F S thresh)) =
map_pmf (λω. median t (λi. real (Xf i ω)))
(prod_pmf {0..<t} (λi. random_xors S (card S - 1)))"
apply (subst median_commute)
subgoal using t1 by simp
unfolding approxmccore_def
apply (subst Pi_pmf_map)
unfolding Xf_def by (auto simp add: pmf.map_comp o_def)
define α where "α = (0.14 ::real)"
then have α: "α > 0" by auto
have indep:"prob_space.indep_vars
(measure_pmf
(prod_pmf {0..<t} (λi. random_xors S (card S - 1))))
(λ_. borel) (λx xa. real (Xf x xa)) {0..<t}"
unfolding Xf_def
apply (intro indep_vars_restrict_intro')
by (auto simp add: restrict_dfl_def)
have d: "δ ∈ {0<..<1}" using δ by auto
from approxcore_xors_eq[OF thresh_def a ε S]
have b1: "1 / 2 + α ≤
measure_pmf.prob (random_xors S (card S - 1))
{xors.
real (approxcore_xors F S thresh xors)
∈ {real (card (proj S (sols F))) /
(1 + ε)..(1 + ε) * real (card (proj S (sols F)))}}"
unfolding α_def by auto
then have b2: "i < t ⟹
1 / 2 + α ≤
measure_pmf.prob
(prod_pmf {0..<t}
(λi. random_xors S (card S - 1)))
{ω ∈ space
(measure_pmf
(prod_pmf {0..<t}
(λi. random_xors S (card S - 1)))).
real (Xf i ω)
∈ {real (card (proj S (sols F))) /(1 + ε)..
(1 + ε) *real (card (proj S (sols F)))}}" for i
unfolding Xf_def apply clarsimp
apply (subst prob_prod_pmf_slice)
by auto
have ***: "1 - δ
≤ measure_pmf.prob (prod_pmf {0..<t} (λi. random_xors S (card S - 1)))
{ω.
median t (λi. real (Xf i ω))
∈ {real (card (proj S (sols F))) /
(1 + ε)..(1 + ε) * real (card (proj S (sols F)))}}"
proof -
have "t = fix_t δ ∨ t = n ∧ raw_median_bound α n < δ"
unfolding t_def compute_t_def α_def by auto
moreover {
assume "t = fix_t δ"
then have tb:"- ln δ / (2 * α⇧2) ≤ real t"
unfolding fix_t_def α_def
apply clarsimp
by (metis assms(1) divide_minus_left inverse_eq_divide ln_inverse real_nat_ceiling_ge)
from measure_pmf.median_bound_1[OF α d indep tb]
have ?thesis using b2 by auto
}
moreover {
assume *: "t = n" "raw_median_bound α n < δ"
have s: "1 / 2 - α = 1 - (1 /2 + α)"
by auto
have d1: "0 < t" using t1 by linarith
have d2: "1 / 2 + α ≥ 0" using α by auto
have d3: "interval{x..y::real}" for x y
unfolding interval_def by auto
from prob_space.median_bound_raw[OF _ d1 d2 d3 indep b2]
have "1 -
measure_pmf.prob (binomial_pmf t (1 / 2 + α)) {..t div 2}
≤ measure_pmf.prob
(prod_pmf {0..<t}
(λi. random_xors S (card S - 1)))
{ω.
median t (λi. real (Xf i ω))
∈ {real (card (proj S (sols F))) /
(1 + ε)..(1 + ε) * real (card (proj S (sols F)))}}"
by (auto simp add: prob_space_measure_pmf)
moreover have "measure_pmf.prob (binomial_pmf t (1 / 2 + α)) {..t div 2} ≤ δ"
by (smt (verit, ccfv_SIG) * b1 d2 measure_pmf.prob_le_1 prob_binomial_pmf_upto raw_median_bound_def s sum.cong)
ultimately have ?thesis by auto
}
ultimately show ?thesis by auto
qed
have "measure_pmf.prob (approxmc F S ε δ n)
{c. real c
∈ {real (card (proj S (sols F))) /
(1 + ε)..(1 + ε) * real (card (proj S (sols F)))}} =
measure_pmf.prob (map_pmf (real ∘ median t)
(prod_pmf {0..<t}
(λi. approxmccore F S thresh)))
{c. c ∈ {real (card (proj S (sols F))) /
(1 + ε)..(1 + ε) * real (card (proj S (sols F)))}}"
using * by auto
moreover have "... =
measure_pmf.prob (map_pmf (real ∘ median t)
(map_pmf (λf x. if x ∈ {0..<t} then f x else undefined) (Pi_pmf {0..<t} (approxcore_xors F S thresh undefined)
(λi. approxmccore F S thresh))))
{c. c ∈ {real (card (proj S (sols F))) /
(1 + ε)..(1 + ε) * real (card (proj S (sols F)))}}"
apply (subst Pi_pmf_default_swap)
by auto
moreover have "... =
measure_pmf.prob (map_pmf (real ∘ median t)
(Pi_pmf {0..<t} (approxcore_xors F S thresh undefined)
(λi. approxmccore F S thresh)))
{c. c ∈ {real (card (proj S (sols F))) /
(1 + ε)..(1 + ε) * real (card (proj S (sols F)))}}"
by (clarsimp simp add: median_default[symmetric])
moreover have "... ≥ 1 - δ"
unfolding **
using ***
by auto
ultimately have ?thesis by auto
}
ultimately show ?thesis by auto
qed
text ‹ To simplify further analyses, we can remove the (required) upper bound on epsilon. ›
definition mk_eps :: "real ⇒ real"
where "mk_eps ε = (if ε > 1 then 1 else ε)"
definition approxmc'::"
'fml ⇒ 'a set ⇒
real ⇒ real ⇒ nat ⇒ nat pmf"
where "approxmc' F S ε δ n =
approxmc F S (mk_eps ε) δ n"
corollary approxmc'_sound:
assumes δ: "δ > 0" "δ < 1"
assumes ε: "ε > 0"
assumes S: "finite S"
shows "prob_space.prob (approxmc' F S ε δ n)
{c. real c ∈
{real (card (proj S (sols F))) / (1 + ε)..
(1 + ε) * real (card (proj S (sols F)))}}
≥ 1 - δ"
proof -
define ε' where "ε' = (if ε > 1 then 1 else ε)"
have ε': "0 < ε'" "ε' ≤ 1"
unfolding ε'_def using ε by auto
from approxmc_sound[OF δ ε' S]
have *: "prob_space.prob (approxmc F S ε' δ n)
{c. real c ∈
{real (card (proj S (sols F))) / (1 + ε')..
(1 + ε') * real (card (proj S (sols F)))}}
≥ 1 - δ" .
have **: "
{c. real c ∈
{real (card (proj S (sols F))) / (1 + ε')..
(1 + ε') * real (card (proj S (sols F)))}}
⊆
{c. real c ∈
{real (card (proj S (sols F))) / (1 + ε)..
(1 + ε) * real (card (proj S (sols F)))}}"
unfolding ε'_def
apply clarsimp
apply (rule conjI)
apply (smt (verit) field_sum_of_halves frac_less2 zero_less_divide_iff)
by (metis (no_types, opaque_lifting) add_le_cancel_left arith_special(3) dual_order.trans less_eq_real_def mult_right_mono of_nat_0_le_iff)
show ?thesis
apply (intro order.trans[OF *])
unfolding approxmc'_def ε'_def mk_eps_def
apply (intro measure_pmf.finite_measure_mono)
using **[unfolded ε'_def]
by auto
qed
text ‹ This shows we can lift all randomness to the top-level (i.e., eagerly sample it). ›
definition approxmc_map::"
'fml ⇒ 'a set ⇒
real ⇒ real ⇒ nat ⇒
(nat ⇒ nat ⇒ ('a set × bool) option) ⇒
nat"
where "approxmc_map F S ε δ n xorsFs = (
let ε = mk_eps ε in
let thresh = compute_thresh ε in
if card (proj S (sols F)) < thresh then
card (proj S (sols F))
else
let t = compute_t δ n in
median t (approxcore_xors F S thresh ∘ xorsFs))"
lemma approxmc_map_eq:
shows "
map_pmf (approxmc_map F S ε δ n)
(Pi_pmf {0..<compute_t δ n} def
(λi. random_xors S (card S - 1))) =
approxmc' F S ε δ n"
proof -
define def' where "def' = approxcore_xors F S (compute_thresh (mk_eps ε)) def"
have *: "
map_pmf (median (compute_t δ n))
(prod_pmf {0..<compute_t δ n}
(λi. map_pmf
(approxcore_xors F S
(compute_thresh (mk_eps ε)))
(random_xors S (card S - Suc 0)))) =
map_pmf (median (compute_t δ n))
(Pi_pmf {0..<compute_t δ n} def'
(λi. map_pmf
(approxcore_xors F S
(compute_thresh (mk_eps ε)))
(random_xors S (card S - Suc 0))))"
apply (subst Pi_pmf_default_swap[symmetric, where dflt ="undefined", where dflt'="def'"])
by (auto simp add: map_pmf_comp median_default[symmetric])
show ?thesis
unfolding approxmc'_def approxmc_map_def approxmc_def Let_def approxmccore_def
using def'_def
by (auto simp add: map_pmf_comp Pi_pmf_map[of _ _ def] *)
qed
end
end