Theory Find_Zero
section ‹‹Find_Zero› – Invariant preservation for zero-finding›
theory Find_Zero
imports CO_Invariants Oracle_Programs
begin
context compressed_oracle begin
definition ‹no_zero = {(x::'x,y::'y,D::'x⇀'y). 0 ∉ ran D}›
definition ‹no_zero' = {D::'x⇀'y. 0 ∉ ran D}›
lemma no_zero_no_zero': ‹no_zero = UNIV × UNIV × no_zero'›
by (auto intro!: simp: no_zero_def no_zero'_def)
lemma ket_invariant_no_zero_no_zero': ‹ket_invariant no_zero = ⊤ ⊗⇩S ⊤ ⊗⇩S ket_invariant no_zero'›
by (auto simp: ket_invariant_tensor no_zero_no_zero' simp flip: ket_invariant_UNIV)
text ‹We show the preservation of the \<^const>‹no_zero› invariant.
We show it first with respect to the oracle \<^const>‹query›.›
lemma preserves_no_zero: ‹preserves_ket query no_zero no_zero (6 / sqrt N)›
proof -
define K where ‹K x = ket_invariant {(x,y::'y,D::'x⇀'y) | y D. Some 0 ∉ D ` (-{x})}› for x
define Kd where ‹Kd x D0 = ket_invariant {(x,y::'y,D::'x⇀'y) | y D. (∀x'≠x. D x' = D0 x')}› for x D0
have aux: ‹Some 0 ∉ D ` (- {x}) ⟹
∃xa. xa x = None ∧ Some 0 ∉ range xa ∧ (∀x'. x' ≠ x ⟶ D x' = xa x')› for D::‹'x⇀'y› and x
apply (rule exI[of _ ‹D(x:=None)›])
by force
have K: ‹K x = (SUP D0∈{D0. D0 x = None ∧ Some 0 ∉ range D0}. Kd x D0)› for x
using aux[of _ x] by (auto intro!: simp: K_def Kd_def simp flip: ket_invariant_SUP)
define Kdx where ‹Kdx x D0 x' = ket_invariant {(x::'x,y::'y,D::'x⇀'y) | y D. D x' = D0 x'}› for x D0 x'
have Kd: ‹Kd x D0 = (INF x'∈-{x}. Kdx x D0 x')› for x D0
unfolding Kd_def Kdx_def
apply (subst ket_invariant_INF[symmetric])
apply (rule arg_cong[where f=ket_invariant])
by auto
have Kdx: ‹Kdx x D0 x' = lift_invariant reg_1_3 (ket_invariant {x}) ⊓ lift_invariant (reg_3_3 o function_at x') (ket_invariant {D0 x'})› for x D0 x'
unfolding Kdx_def reg_3_3_def reg_1_3_def
apply (simp add: lift_invariant_comp)
apply (subst lift_invariant_function_at_ket_inv)
apply (subst lift_Snd_ket_inv)
apply (subst lift_Snd_ket_inv)
apply (subst lift_Fst_ket_inv)
apply (subst ket_invariant_inter)
apply (rule arg_cong[where f=ket_invariant])
by auto
show ?thesis
proof (rule inv_split_reg_query[where X=‹reg_1_3› and Y=‹reg_2_3› and H=‹reg_3_3› and K=K
and ?I1.0=‹λ_. ket_invariant (UNIV × -{Some 0})› and ?J1.0=‹λ_. ket_invariant (UNIV × -{Some 0})›])
show ‹query = (reg_1_3;(reg_2_3;reg_3_3)) query›
by (simp add: pair_Fst_Snd reg_1_3_def reg_2_3_def reg_3_3_def)
show ‹compatible reg_1_3 reg_2_3› ‹compatible reg_1_3 reg_3_3› ‹compatible reg_2_3 reg_3_3›
by simp_all
show ‹compatible_register_invariant reg_2_3 (K x)› for x
unfolding K Kd Kdx
apply (rule compatible_register_invariant_SUP, simp)
apply (rule compatible_register_invariant_INF, simp)
apply (rule compatible_register_invariant_inter, simp)
apply (rule compatible_register_invariant_compatible_register)
apply simp
apply (rule compatible_register_invariant_compatible_register)
by simp
show ‹compatible_register_invariant (reg_3_3 o function_at x) (K x)› for x
unfolding K Kd Kdx
apply (rule compatible_register_invariant_SUP, simp)
apply (rule compatible_register_invariant_INF, simp)
apply (rule compatible_register_invariant_inter, simp)
apply (rule compatible_register_invariant_compatible_register)
apply simp
apply (rule compatible_register_invariant_compatible_register)
by simp
show ‹ket_invariant no_zero
≤ (SUP x. K x ⊓
lift_invariant (reg_2_3;reg_3_3 ∘ function_at x) (ket_invariant (UNIV × - {Some 0})))›
apply (simp add: K_def lift_Fst_ket_inv reg_1_3_def reg_2_3_def ket_invariant_inter ket_invariant_SUP[symmetric]
lift_inv_prod lift_invariant_comp lift_invariant_function_at_ket_inv reg_3_3_def lift_Snd_ket_inv)
unfolding no_zero_def
by (auto simp add: ranI)
have aux: ‹⋀D::'x⇀'y. Some 0 ∉ D ` (- {x}) ⟹ D x ≠ Some 0 ⟹ 0 ∈ ran D ⟹ False› for x
by (smt (verit, del_insts) ComplI image_iff mem_Collect_eq ran_def singletonD)
show ‹K x ⊓ lift_invariant (reg_2_3;reg_3_3 ∘ function_at x) (ket_invariant (UNIV × - {Some 0}))
≤ ket_invariant no_zero› for x
by (auto intro: aux simp add: K_def lift_Fst_ket_inv reg_1_3_def reg_2_3_def ket_invariant_inter ket_invariant_SUP[symmetric]
lift_inv_prod lift_invariant_comp lift_invariant_function_at_ket_inv reg_3_3_def lift_Snd_ket_inv
no_zero_def)
show ‹orthogonal_spaces (K x) (K x')› if ‹x ≠ x'› for x x'
using that by (auto simp add: K_def)
show ‹preserves_ket query1 (UNIV × - {Some 0}) (UNIV × - {Some 0}) (6 / sqrt N)›
apply (subst asm_rl[of ‹6 / sqrt N = 6 * sqrt (1::nat) / sqrt N›], simp)
apply (rule preserve_query1_simplified)
by (auto simp add: card_le_Suc0_iff_eq)
show ‹K x ≤ lift_invariant reg_1_3 (ket_invariant {x})› for x
by (auto simp add: K_def reg_1_3_def lift_Fst_ket_inv)
show ‹6 / sqrt N ≥ 0›
by simp
qed simp
qed
text ‹Like @{thm [source] preserves_no_zero} but with respect to the oracle \<^const>‹query›.›
lemma preserves_no_zero': ‹preserves_ket query' no_zero no_zero (5 / sqrt N)›
proof -
define K where ‹K x = ket_invariant {(x,y::'y,D::'x⇀'y) | y D. Some 0 ∉ D ` (-{x})}› for x
define Kd where ‹Kd x D0 = ket_invariant {(x,y::'y,D::'x⇀'y) | y D. (∀x'≠x. D x' = D0 x')}› for x D0
have aux: ‹Some 0 ∉ D ` (- {x}) ⟹
∃xa. xa x = None ∧ Some 0 ∉ range xa ∧ (∀x'. x' ≠ x ⟶ D x' = xa x')› for D::‹'x⇀'y› and x
apply (rule exI[of _ ‹D(x:=None)›])
by force
have K: ‹K x = (SUP D0∈{D0. D0 x = None ∧ Some 0 ∉ range D0}. Kd x D0)› for x
using aux[of _ x] by (auto intro!: simp: K_def Kd_def simp flip: ket_invariant_SUP)
define Kdx where ‹Kdx x D0 x' = ket_invariant {(x::'x,y::'y,D::'x⇀'y) | y D. D x' = D0 x'}› for x D0 x'
have Kd: ‹Kd x D0 = (INF x'∈-{x}. Kdx x D0 x')› for x D0
unfolding Kd_def Kdx_def
apply (subst ket_invariant_INF[symmetric])
apply (rule arg_cong[where f=ket_invariant])
by auto
have Kdx: ‹Kdx x D0 x' = lift_invariant reg_1_3 (ket_invariant {x}) ⊓ lift_invariant (reg_3_3 o function_at x') (ket_invariant {D0 x'})› for x D0 x'
unfolding Kdx_def reg_3_3_def reg_1_3_def
apply (simp add: lift_invariant_comp)
apply (subst lift_invariant_function_at_ket_inv)
apply (subst lift_Snd_ket_inv)
apply (subst lift_Snd_ket_inv)
apply (subst lift_Fst_ket_inv)
apply (subst ket_invariant_inter)
apply (rule arg_cong[where f=ket_invariant])
by auto
show ?thesis
proof (rule inv_split_reg_query'[where X=‹reg_1_3› and Y=‹reg_2_3› and H=‹reg_3_3› and K=K
and ?I1.0=‹λ_. ket_invariant (UNIV × -{Some 0})› and ?J1.0=‹λ_. ket_invariant (UNIV × -{Some 0})›])
show ‹query' = (reg_1_3;(reg_2_3;reg_3_3)) query'›
by (simp add: pair_Fst_Snd reg_1_3_def reg_2_3_def reg_3_3_def)
show ‹compatible reg_1_3 reg_2_3› ‹compatible reg_1_3 reg_3_3› ‹compatible reg_2_3 reg_3_3›
by simp_all
show ‹compatible_register_invariant reg_2_3 (K x)› for x
unfolding K Kd Kdx
apply (rule compatible_register_invariant_SUP, simp)
apply (rule compatible_register_invariant_INF, simp)
apply (rule compatible_register_invariant_inter, simp)
apply (rule compatible_register_invariant_compatible_register)
apply simp
apply (rule compatible_register_invariant_compatible_register)
by simp
show ‹compatible_register_invariant (reg_3_3 o function_at x) (K x)› for x
unfolding K Kd Kdx
apply (rule compatible_register_invariant_SUP, simp)
apply (rule compatible_register_invariant_INF, simp)
apply (rule compatible_register_invariant_inter, simp)
apply (rule compatible_register_invariant_compatible_register)
apply simp
apply (rule compatible_register_invariant_compatible_register)
by simp
show ‹ket_invariant no_zero
≤ (SUP x. K x ⊓
lift_invariant (reg_2_3;reg_3_3 ∘ function_at x) (ket_invariant (UNIV × - {Some 0})))›
apply (simp add: K_def lift_Fst_ket_inv reg_1_3_def reg_2_3_def ket_invariant_inter ket_invariant_SUP[symmetric]
lift_inv_prod lift_invariant_comp lift_invariant_function_at_ket_inv reg_3_3_def lift_Snd_ket_inv)
unfolding no_zero_def
by (auto simp add: ranI)
have aux: ‹Some 0 ∉ D ` (- {x}) ⟹ D x ≠ Some 0 ⟹ 0 ∉ ran D› for D x
by (smt (verit, del_insts) ComplI image_iff mem_Collect_eq ran_def singletonD)
show ‹K x ⊓ lift_invariant (reg_2_3;reg_3_3 ∘ function_at x) (ket_invariant (UNIV × - {Some 0}))
≤ ket_invariant no_zero› for x
using aux[of _ x]
by (auto simp add: K_def lift_Fst_ket_inv reg_1_3_def reg_2_3_def ket_invariant_inter ket_invariant_SUP[symmetric]
lift_inv_prod lift_invariant_comp lift_invariant_function_at_ket_inv reg_3_3_def lift_Snd_ket_inv
no_zero_def)
show ‹orthogonal_spaces (K x) (K x')› if ‹x ≠ x'› for x x'
using that by (auto simp add: K_def)
show ‹preserves_ket query1' (UNIV × - {Some 0}) (UNIV × - {Some 0}) (5 / sqrt N)›
apply (subst asm_rl[of ‹5 / sqrt N = 5 * sqrt (1::nat) / sqrt N›], simp)
apply (rule preserve_query1'_simplified)
by (auto simp add: card_le_Suc0_iff_eq)
show ‹K x ≤ lift_invariant reg_1_3 (ket_invariant {x})› for x
by (auto simp add: K_def reg_1_3_def lift_Fst_ket_inv)
show ‹5 / sqrt N ≥ 0›
by simp
qed simp
qed
lemma preserves_no_zero_num: ‹preserves_ket query (no_zero ∩ num_queries q) (no_zero ∩ num_queries (q+1)) (6 / sqrt N)›
apply (subst add_0_right[of ‹6/sqrt N›, symmetric])
apply (rule preserves_intersect_ket)
apply (simp add: preserves_mono[OF preserves_no_zero])
apply (rule preserves_mono[OF preserves_num])
by auto
lemma preserves_no_zero_num': ‹preserves_ket query' (no_zero ∩ num_queries q) (no_zero ∩ num_queries (q+1)) (5 / sqrt N)›
apply (subst add_0_right[of ‹5/sqrt N›, symmetric])
apply (rule preserves_intersect_ket)
apply (simp add: preserves_mono[OF preserves_no_zero'])
apply (rule preserves_mono[OF preserves_num'])
by auto
subsection ‹Zero-finding is hard for q-query adversaries›
lemma zero_finding_is_hard:
fixes program :: ‹('mem, 'x, 'y) program›
and adv_output :: ‹'x update ⇒ 'mem update›
and initial_state
assumes [iff]: ‹valid_program program›
assumes ‹norm initial_state = 1›
assumes [register]: ‹register adv_output›
shows ‹(∑h∈UNIV. ∑x|h x = 0. measurement_probability adv_output (exec_program h program initial_state) x) / CARD('x ⇒ 'y)
≤ (5 * real (query_count program) + 11)⇧2 / N›
proof -
note [[simproc del: Laws_Quantum.compatibility_warn]]
text ‹In this game based proof, we consider three different quantum memory models:
▪ The one from the statement of the lemma, where the overall quantum state lives in \<^typ>‹'mem›,
and the adversary output register is described by \<^term>‹adv_output›, and the initial state
in \<^term>‹initial_state›. The program \<^term>‹program› assumes this memory model.
▪ The "extra output" (short XO) memory model, where there is an extra auxiliary register ‹aux› of type \<^typ>‹'y›.
The type of the memory is then \<^typ>‹'mem × 'y›. (I.e., the extra register is in addition to the content of \<^typ>‹'mem›.)
▪ The "compressed oracle" (short CO) memory model, where additionally to XO, we have an oracle register
that can holds the content of the compressed oracle (or the standard oracle).›
text ‹Since the register \<^term>‹adv_output :: _ ⇒ ('mem ell2 ⇒⇩C⇩L 'mem ell2)› is defined w.r.t. a specific memory,
we define convenience definitions for the same register as it would be accessed in the other memories:›
define adv_output_in_xo :: ‹'x update ⇒ ('mem×'y) update› where ‹adv_output_in_xo = Fst o adv_output›
define adv_output_in_co :: ‹'x update ⇒ (('mem×'y) × ('x⇀'y)) update› where ‹adv_output_in_co = Fst o adv_output_in_xo›
text ‹Analogously, we defined the ‹aux›-register and the oracle register in the applicable memories:›
define aux_in_xo :: ‹'y update ⇒ ('mem×'y) update› where ‹aux_in_xo = Snd›
define aux_in_co :: ‹'y update ⇒ (('mem×'y) × ('x⇀'y)) update› where ‹aux_in_co = Fst o aux_in_xo›
define oracle_in_co :: ‹('x⇀'y) update ⇒ (('mem×'y) × ('x⇀'y)) update› where ‹oracle_in_co = Snd›
define aao_in_co where ‹aao_in_co = (adv_output_in_co; (aux_in_co; oracle_in_co))›
have [register]: ‹compatible aux_in_co oracle_in_co›
by (simp add: adv_output_in_co_def aux_in_co_def oracle_in_co_def adv_output_in_xo_def aux_in_xo_def)
have [register]: ‹compatible adv_output_in_xo aux_in_xo›
by (simp add: adv_output_in_xo_def aux_in_xo_def)
have [register]: ‹compatible adv_output_in_co aux_in_co›
by (simp add: adv_output_in_co_def aux_in_co_def)
have [register]: ‹compatible adv_output_in_co oracle_in_co›
by (simp add: adv_output_in_co_def oracle_in_co_def)
have [register]: ‹compatible aux_in_xo Fst›
by (simp add: aux_in_xo_def)
have [register]: ‹compatible aux_in_co (Fst o Fst)›
by (simp add: aux_in_co_def)
have [register]: ‹compatible aux_in_co Snd›
by (simp add: aux_in_co_def)
have [register]: ‹register aao_in_co›
by (simp add: aao_in_co_def)
text ‹The initial states in XO/CO are like the original initial state, but with
\<^term>‹ket 0› in ‹aux› and \<^term>‹ket Map.empty› (the fully undefined function) in the oracle register.›
define initial_state_in_xo where ‹initial_state_in_xo = initial_state ⊗⇩s ket (0 :: 'y)›
define initial_state_in_co :: ‹(('mem×'y) × ('x⇀'y)) ell2› where ‹initial_state_in_co = initial_state_in_xo ⊗⇩s ket Map.empty›
text ‹We define an extended program ‹ext_program› that executes \<^term>‹program›, followed by one additional query to the oracle.
Input register is the adversary output register. Output register is the additional register ‹aux›.
Hence ‹ext_program› is only meaningful in the models XO and CO. (Our definition is for XO.)›
define ext_program where ‹ext_program = lift_program Fst program @ [QueryStep adv_output_in_xo aux_in_xo]›
have [iff]: ‹valid_program ext_program›
by (auto intro!: valid_program_lift simp add: valid_program_append adv_output_in_xo_def aux_in_xo_def ext_program_def)
text ‹We define the final states of the programs \<^term>‹program› and \<^term>‹ext_program›, in the original model, and in XO, and CO.›
define final :: ‹('x ⇒ 'y) ⇒ 'mem ell2› where ‹final h = exec_program h program initial_state› for h
define xo_ext_final :: ‹('x ⇒ 'y) ⇒ ('mem×'y) ell2› where ‹xo_ext_final h = exec_program h ext_program initial_state_in_xo› for h
define xo_final :: ‹('x ⇒ 'y) ⇒ ('mem×'y) ell2› where ‹xo_final h = exec_program h (lift_program Fst program) initial_state_in_xo› for h
define co_ext_final :: ‹(('mem×'y) × ('x⇀'y)) ell2› where ‹co_ext_final = exec_program_with query' ext_program initial_state_in_co›
define co_final :: ‹(('mem×'y) × ('x⇀'y)) ell2› where ‹co_final = exec_program_with query' (lift_program Fst program) initial_state_in_co›
have [simp]: ‹norm initial_state_in_xo = 1›
by (simp add: initial_state_in_xo_def norm_tensor_ell2 assms)
have norm_initial_state_in_co[simp]: ‹norm initial_state_in_co = 1›
by (simp add: initial_state_in_co_def norm_tensor_ell2)
have norm_co_final[simp]: ‹norm co_final ≤ 1›
unfolding co_final_def
using norm_exec_program_with valid_program_lift ‹valid_program program›
norm_query' register_Fst norm_initial_state_in_co
by smt
text ‹We derive the relationships between the various final states:›
have co_ext_final_prefinal: ‹co_ext_final = aao_in_co query' *⇩V co_final›
by (simp add: co_ext_final_def ext_program_def exec_program_with_append aao_in_co_def
flip: initial_state_in_co_def co_final_def adv_output_in_co_def aux_in_co_def oracle_in_co_def)
have xo_final_final: ‹xo_final h = final h ⊗⇩s ket 0› for h
by (simp add: xo_final_def final_def initial_state_in_xo_def exec_lift_program_Fst)
have xo_ext_final_xo_final: ‹xo_ext_final h = (adv_output_in_xo;aux_in_xo) (function_oracle h) *⇩V xo_final h› for h
by (simp add: xo_ext_final_def xo_final_def ext_program_def exec_program_def)
text ‹After executing \<^term>‹program› (in XO), the ‹aux›-register is in state \<^term>‹ket 0›:›
have xo_final_has_y0: ‹dist_inv_avg (adv_output_in_xo;aux_in_xo) (λ_. ket_invariant {(x,y). y = 0}) xo_final = 0›
proof -
have ‹dist_inv_avg aux_in_xo (λ_::'x⇒'y. ket_invariant {0}) xo_final
≤ dist_inv_avg aux_in_xo (λ_::'x⇒'y. ket_invariant {0}) (λh. initial_state_in_xo)›
unfolding xo_final_def
apply (subst dist_inv_avg_exec_compatible)
using dist_inv_avg_exec_compatible
by auto
also have ‹… = 0›
by (auto intro!: tensor_ell2_in_tensor_ccsubspace ket_in_ket_invariantI
simp add: initial_state_in_xo_def dist_inv_0_iff distance_from_inv_avg0I aux_in_xo_def lift_Snd_inv)
finally have ‹dist_inv_avg aux_in_xo (λ_. ket_invariant {0}) xo_final = 0›
by (smt (verit, ccfv_SIG) dist_inv_avg_pos)
then show ?thesis
apply (rewrite at ‹{(x, y). y = 0}› to ‹UNIV × {0}› DEADID.rel_mono_strong, blast)
apply (subst dist_inv_avg_register_rewrite)
by (simp_all add: lift_inv_prod)
qed
text ‹Same as @{thm [source] xo_final_has_y0}, but in CO:›
have co_final_has_y0: ‹dist_inv aao_in_co (ket_invariant {(x,y,D). y = 0}) co_final = 0›
proof -
have ‹dist_inv aux_in_co (ket_invariant {0}) co_final
≤ dist_inv aux_in_co (ket_invariant {0}) initial_state_in_co›
unfolding co_final_def
apply (rule dist_inv_exec'_compatible)
by simp_all
also have ‹… = 0›
by (auto intro!: tensor_ell2_in_tensor_ccsubspace ket_in_ket_invariantI
simp add: initial_state_in_co_def initial_state_in_xo_def dist_inv_0_iff
aux_in_co_def aux_in_xo_def lift_Fst_inv lift_Snd_inv lift_invariant_comp)
finally have ‹dist_inv aux_in_co (ket_invariant {0}) co_final = 0›
by (smt (verit, best) dist_inv_pos)
then show ?thesis
apply (rewrite at ‹{(x, y, D). y = 0}› to ‹UNIV × {0} × UNIV› DEADID.rel_mono_strong, blast)
apply (subst dist_inv_register_rewrite)
by (simp_all add: lift_inv_prod aao_in_co_def)
qed
define q where ‹q = query_count program›
text ‹The following term occurs a lot (it's how much the \<^term>‹no_zero› invariant is preserved after running \<^term>‹ext_program›).
So we abbreviate it as ‹d›.›
define d :: real where ‹d = (5 * q + 11) / sqrt N›
have [iff]: ‹d ≥ 0›
by (simp add: d_def)
have ‹dist_inv oracle_in_co (ket_invariant no_zero') co_ext_final ≤ 5 * (q+1) / sqrt N›
proof (unfold co_ext_final_def, rule dist_inv_induct[where g=‹λ_. 5 / sqrt N› and J=‹λ_. ket_invariant no_zero'›])
show ‹compatible oracle_in_co Fst›
using oracle_in_co_def by simp
show ‹initial_state_in_co ∈ space_as_set (lift_invariant oracle_in_co (ket_invariant no_zero'))›
by (auto intro!: tensor_ell2_in_tensor_ccsubspace
simp add: initial_state_in_co_def oracle_in_co_def lift_Snd_ket_inv
initial_state_in_xo_def tensor_ell2_ket ket_in_ket_invariantI no_zero'_def
simp flip: ket_invariant_tensor)
show ‹ket_invariant no_zero' ≤ ket_invariant no_zero'›
by simp
show ‹valid_program ext_program›
by (simp add: valid_program_lift)
show ‹preserves ((Fst ∘ X_in_xo;(Fst ∘ Y_in_xo;Snd)) query') (lift_invariant oracle_in_co (ket_invariant no_zero'))
(lift_invariant oracle_in_co (ket_invariant no_zero')) (5 / sqrt N)› if [register]: ‹compatible X_in_xo Y_in_xo› for X_in_xo Y_in_xo
proof -
from preserves_no_zero'
have ‹preserves ((Fst ∘ X_in_xo;(Fst ∘ Y_in_xo;Snd)) query')
(lift_invariant (Fst ∘ X_in_xo;(Fst ∘ Y_in_xo;Snd)) (ket_invariant no_zero))
(lift_invariant (Fst ∘ X_in_xo;(Fst ∘ Y_in_xo;Snd)) (ket_invariant no_zero))
(5 / sqrt (real N))›
unfolding N_def
apply (rule preserves_lift_invariant[THEN iffD2, rotated])
by simp
moreover have ‹lift_invariant (Fst ∘ X_in_xo;(Fst ∘ Y_in_xo;Snd)) (ket_invariant no_zero)
= lift_invariant oracle_in_co (ket_invariant no_zero')›
by (simp add: oracle_in_co_def no_zero_no_zero' lift_inv_prod)
finally show ?thesis
by -
qed
show ‹norm query' ≤ 1›
by simp
show ‹norm initial_state_in_co ≤ 1›
by simp
show ‹(∑i<query_count ext_program. 5 / sqrt N) ≤ real (5 * (q+1)) / sqrt N›
apply (simp add: query_count_lift_program ext_program_def flip: q_def)
by argo
qed
then have dist_zero: ‹dist_inv aao_in_co (ket_invariant no_zero) co_ext_final ≤ 5 * (q+1) / sqrt N›
apply (rule le_back_subst)
apply (rule dist_inv_register_rewrite)
by (auto intro!: simp: aao_in_co_def no_zero_no_zero' lift_inv_prod)
have dist_Dxy: ‹dist_inv aao_in_co (ket_invariant {(x,y,D). D x = Some y}) co_ext_final ≤ 6 / sqrt N› (is ‹?lhs ≤ _›)
unfolding co_ext_final_prefinal
apply (rule dist_inv_leq_if_preserves[THEN order_trans])
apply (subst preserves_lift_invariant)
apply (auto intro!: preserves_ket_query'_output_simple simp: register_norm)[4]
using norm_co_final
by (simp add: N_def co_final_has_y0 field_class.field_divide_inverse)
have ‹dist_inv aao_in_co
(ket_invariant {(x, y, D::'x ⇀ 'y). 0 ∉ ran D ∧ D x = Some y}) co_ext_final ≤ d› (is ‹?lhs ≤ d›)
proof -
have ‹?lhs = dist_inv aao_in_co (ket_invariant no_zero ⊓ ket_invariant {(x, y, D). D x = Some y}) co_ext_final›
apply (rule arg_cong3[where f=dist_inv])
by (auto intro!: simp: no_zero_def ket_invariant_inter)
also have ‹… ≤ sqrt ((dist_inv aao_in_co (ket_invariant no_zero) co_ext_final)⇧2
+ (dist_inv aao_in_co (ket_invariant {(x, y, D). D x = Some y}) co_ext_final)⇧2)›
apply (rule dist_inv_intersect)
by auto
also have ‹… ≤ sqrt ((5 * (q+1) / sqrt N)⇧2 + (6 / sqrt N)⇧2)›
apply (rule real_sqrt_le_mono)
apply (rule add_mono)
using dist_zero dist_Dxy
by auto
also have ‹… ≤ (5 * q + 11) / sqrt N›
apply (rule sqrt_sum_squares_le_sum[THEN order_trans])
by (auto, argo)
finally show ?thesis
by (simp add: d_def)
qed
then have ‹dist_inv aao_in_co (ket_invariant {(x, y, D::'x ⇀ 'y). y ≠ 0}) co_ext_final ≤ d›
apply (rule le_back_subst_le)
apply (rule dist_inv_mono)
by (auto intro!: ranI)
then have ‹dist_inv (adv_output_in_co; aux_in_co) (ket_invariant {(x, y). y ≠ 0}) co_ext_final ≤ d›
apply (rule le_back_subst)
apply (rule dist_inv_register_rewrite)
apply (simp, simp)
apply (rewrite at ‹{(x, y, D). y ≠ 0}›
to ‹(λ((a,b),c). (a,b,c)) ` ({(x, y) | x y. y ≠ 0} × UNIV)› DEADID.rel_mono_strong)
apply force
by (simp add: ket_invariant_image_assoc pair_o_assoc pair_o_assoc[unfolded o_def] lift_inv_prod aao_in_co_def
flip: lift_invariant_comp[unfolded o_def, THEN fun_cong])
then have ‹dist_inv_avg (adv_output_in_xo; aux_in_xo) (λh. ket_invariant {(x, y). y ≠ 0}) xo_ext_final ≤ d›
apply (rule le_back_subst)
unfolding co_ext_final_def xo_ext_final_def
apply (rewrite at ‹(adv_output_in_co;aux_in_co)› to ‹Fst o (adv_output_in_xo;aux_in_xo)› DEADID.rel_mono_strong)
apply (simp add: adv_output_in_co_def aux_in_co_def register_comp_pair)
by (simp add: initial_state_in_co_def dist_inv_exec_query'_exec_fixed)
then have ‹dist_inv_avg (adv_output_in_xo; aux_in_xo)
(λh. ket_invariant {(x, y). h x ≠ 0 ∨ y ≠ 0}) xo_final ≤ d›
apply (rule le_back_subst_le)
unfolding xo_ext_final_xo_final[abs_def]
apply (subst dist_inv_avg_apply_iff)
by (auto intro!: ext dist_inv_avg_mono simp: function_oracle_ket_invariant)
then have *: ‹dist_inv_avg (adv_output_in_xo; aux_in_xo)
(λh. ket_invariant {(x, y). h x ≠ 0}) xo_final ≤ d›
apply (rule le_back_subst_le)
apply (rule ord_le_eq_trans)
apply (rule dist_inv_avg_mono[where I=‹λh. ket_invariant {(x, y). h x ≠ 0 ∨ y ≠ 0} ⊓ ket_invariant {(x,y). y=0}›])
apply (auto simp: ket_invariant_inter)[2]
apply (rule dist_inv_avg_intersect)
apply simp_all[2]
by (fact xo_final_has_y0)
then have ‹dist_inv_avg adv_output_in_xo
(λh. ket_invariant {x. h x ≠ 0}) xo_final ≤ d›
apply (subst dist_inv_avg_register_rewrite[where R=‹(adv_output_in_xo; aux_in_xo)› and J=‹λh. ket_invariant {(x, y). h x ≠ 0}›])
apply (simp, simp)
apply (rewrite at ‹{(x, y). h x ≠ 0}› in for (h) to ‹{x. h x ≠ 0} × UNIV› DEADID.rel_mono_strong)
apply fastforce
by (simp add: lift_inv_prod)
then have ‹dist_inv_avg adv_output (λh. ket_invariant {x. h x ≠ 0}) final ≤ d›
by (simp add: xo_final_final[abs_def] adv_output_in_xo_def dist_inv_avg_Fst_tensor)
then have ‹(∑h∈UNIV. ∑x|h x = 0. measurement_probability adv_output (final h) x) / CARD('x ⇒ 'y) ≤ d⇧2›
apply (subst dist_inv_avg_measurement_probability)
apply simp
apply (rewrite at ‹- {x. h x = 0}› in ‹λh. ⌑› to ‹{x. h x ≠ 0}› DEADID.rel_mono_strong)
apply blast
by auto
also have ‹d⇧2 = (5 * q + 11)⇧2 / N›
by (simp add: d_def power2_eq_square)
finally show ?thesis
by (simp add: final_def q_def)
qed
end
end