Theory Compressed_Oracle_Is_RO

section ‹‹Compressed_Oracle_Is_RO› -- Equivalence of compressed oracle and regular random oracle›

theory Compressed_Oracle_Is_RO imports
    Registers.Pure_States
    CO_Operations
begin

lemma swap_function_oracle_measure_generic:
  fixes standard_query
  fixes X :: ‹'x update ⇒ 'mem update› and Y :: ‹'y::ab_group_add update ⇒ 'mem update›
  assumes std_query_Some: ‹⋀H x y z. H x = Some z ⟹ standard_query *⇩V (ket (x,y,H)) = ket (x, y + z, H)› (* e.g. standard_query_ket_full_Some *)
  assumes [register]: ‹compatible X Y›
  shows ‹(Fst o X; (Fst o Y; Snd)) standard_query o⇩C⇩L Snd (proj (ket (Some o h)))
            = Fst ((X;Y) (function_oracle h)) o⇩C⇩L Snd (proj (ket (Some o h)))›
proof -
  note [[simproc del: Laws_Quantum.compatibility_warn]]
  let ?goal = ?thesis
  have [register]: ‹register (Fst o X; (Fst o Y; Snd :: _ ⇒ ('mem × ('x ⇀ 'y)) update))›
    by simp
  from register_decomposition[OF this]
  have ‹let 'd::type = register_decomposition_basis (Fst o X; (Fst o Y; Snd :: _ ⇒ ('mem × ('x ⇀ 'y)) update)) in ?thesis›
  proof with_type_mp
    case with_type_mp
    then obtain U :: ‹(('x × 'y × ('x ⇒ 'y option)) × 'd) ell2 ⇒⇩C⇩L ('mem × ('x ⇒ 'y option)) ell2› 
      where ‹unitary U› and unwrap: ‹(Fst ∘ X;(Fst ∘ Y;Snd)) θ = sandwich U *⇩V (θ ⊗⇩o id_cblinfun)› for θ
      by blast
    have unwrap_Snd: ‹Snd a = sandwich U *⇩V ((id_cblinfun ⊗⇩o (id_cblinfun ⊗⇩o a)) ⊗⇩o id_cblinfun)› for a
      apply (rewrite at Snd to ‹(Fst ∘ X;(Fst ∘ Y;Snd)) o Snd o Snd› DEADID.rel_mono_strong)
       apply (simp add: register_pair_Snd)
      by (simp add: unwrap Snd_def)
    have unwrap_Fst_XY: ‹(Fst o (X;Y)) a = sandwich U *⇩V assoc (a ⊗⇩o id_cblinfun) ⊗⇩o id_cblinfun›
      for a
      apply (rewrite at ‹Fst o (X;Y)› to ‹(Fst ∘ X;(Fst ∘ Y;Snd)) o assoc o Fst› DEADID.rel_mono_strong)
       apply (simp add: register_pair_Fst register_comp_pair)
      by (simp add: only: o_apply unwrap Fst_def)

    have ‹standard_query ⊗⇩o id_cblinfun o⇩C⇩L
          (id_cblinfun ⊗⇩o id_cblinfun ⊗⇩o proj (ket (Some ∘ h))) ⊗⇩o id_cblinfun =
          assoc (function_oracle h ⊗⇩o id_cblinfun) ⊗⇩o id_cblinfun o⇩C⇩L
          (id_cblinfun ⊗⇩o id_cblinfun ⊗⇩o proj (ket (Some ∘ h))) ⊗⇩o id_cblinfun›
      by (auto intro!: equal_ket
          simp: tensor_op_ket tensor_ell2_ket proj_ket_x_y_ofbool std_query_Some assoc_ell2_sandwich
          sandwich_apply function_oracle_apply)
    then show ?goal
      by (auto intro!: arg_cong[where f=‹sandwich U›]
          simp add: unwrap unwrap_Snd unwrap_Fst_XY[unfolded o_def] sandwich_arg_compose ‹unitary U›)
  qed
  from this[cancel_with_type]
  show ?goal
    by -
qed


lemma standard_query_for_fixed_func_generic:
  fixes standard_query
  fixes X :: ‹'x update ⇒ 'mem update› and Y :: ‹'y::ab_group_add update ⇒ 'mem update›
  assumes ‹⋀H x y z. H x = Some z ⟹ standard_query *⇩V (ket (x,y,H)) = ket (x, y + z, H)› (* e.g. standard_query_ket_full_Some *)
  assumes ‹compatible X Y›
  shows ‹(Fst o X; (Fst o Y; Snd)) standard_query *⇩V (ψ ⊗⇩s ket (Some ∘ h))
            = Fst ((X;Y) (function_oracle h)) *⇩V (ψ ⊗⇩s ket (Some ∘ h))›
proof -
  have ‹(Fst o X; (Fst o Y; Snd)) standard_query *⇩V (ψ ⊗⇩s ket (Some ∘ h))
      = (Fst o X; (Fst o Y; Snd)) standard_query *⇩V Snd (proj (ket (Some o h))) *⇩V (ψ ⊗⇩s ket (Some ∘ h))›
    by (simp add: proj_ket_x_y_ofbool)
  also have ‹… = Fst ((X;Y) (function_oracle h)) *⇩V Snd (proj (ket (Some o h))) *⇩V (ψ ⊗⇩s ket (Some ∘ h))›
    apply (subst cblinfun_apply_cblinfun_compose[symmetric])+
    by (simp_all add: assms swap_function_oracle_measure_generic)
  also have ‹… = Fst ((X;Y) (function_oracle h)) *⇩V (ψ ⊗⇩s ket (Some ∘ h))›
    by (simp add: Proj_fixes_image ccspan.rep_eq complex_vector.span_base flip: cblinfun_apply_cblinfun_compose)
  finally show ?thesis
    by -
qed





end