Theory Teleport

section Quantum teleportation

theory Teleport
  imports 
    QHoare
    Real_Impl.Real_Impl
    "HOL-Library.Code_Target_Numeral"
    Finite_Tensor_Product_Matrices
    "HOL-Library.Word"
begin

hide_const (open) Finite_Cartesian_Product.vec
hide_type (open) Finite_Cartesian_Product.vec
hide_const (open) Finite_Cartesian_Product.mat
hide_const (open) Finite_Cartesian_Product.row
hide_const (open) Finite_Cartesian_Product.column
no_notation Group.mult (infixl "ı" 70)
no_notation Order.top ("ı")
unbundle no_vec_syntax
unbundle no_inner_syntax


locale teleport_locale = qhoare "TYPE('mem::finite)" +
  fixes X :: "bit update  'mem::finite update"
    and Φ :: "(bit*bit) update  'mem update"
    and A :: "'atype::finite update  'mem update"
    and B :: "'btype::finite update  'mem update"
  assumes compat[register]: "mutually compatible (X,Φ,A,B)"
begin

abbreviation "Φ1  Φ  Fst"
abbreviation "Φ2  Φ  Snd"
abbreviation "XΦ2  (X;Φ2)"
abbreviation "XΦ1  (X;Φ1)"
abbreviation "  (X;Φ)"
abbreviation "XAB  ((X;A); B)"
abbreviation "AB  (A;B)"
abbreviation "Φ2AB  ((Φ o Snd; A); B)"

definition "teleport a b = [
    apply CNOT XΦ1,
    apply hadamard X,
    ifthen Φ1 a,
    ifthen X b, 
    apply (if a=1 then pauliX else id_cblinfun) Φ2,
    apply (if b=1 then pauliZ else id_cblinfun) Φ2
  ]"


lemma Φ_XΦ: Φ a =  (id_cblinfun o a)
  by (auto simp: register_pair_apply)
lemma XΦ1_XΦ: XΦ1 a =  (assoc (a o id_cblinfun))
  apply (subst pair_o_assoc[unfolded o_def, of X Φ1 Φ2, simplified, THEN fun_cong])
  by (auto simp: register_pair_apply)
lemma XΦ2_XΦ: XΦ2 a =  ((id r swap) (assoc (a o id_cblinfun)))
  apply (subst pair_o_tensor[unfolded o_def, THEN fun_cong], simp, simp, simp)
  apply (subst (2) register_Fst_register_Snd[symmetric, of Φ], simp)
  using [[simproc del: compatibility_warn]]
  apply (subst pair_o_swap[unfolded o_def], simp)
  apply (subst pair_o_assoc[unfolded o_def, THEN fun_cong], simp, simp, simp)
  by (auto simp: register_pair_apply)
lemma Φ2_XΦ: Φ2 a =  (id_cblinfun o (id_cblinfun o a))
  by (auto simp: Snd_def register_pair_apply)
lemma X_XΦ: X a =  (a o id_cblinfun)
  by (auto simp: register_pair_apply)
lemma Φ1_XΦ: Φ1 a =  (id_cblinfun o (a o id_cblinfun))
  by (auto simp: Fst_def register_pair_apply)
lemmas to_XΦ = Φ_XΦ XΦ1_XΦ XΦ2_XΦ Φ2_XΦ X_XΦ Φ1_XΦ

lemma X_XΦ1: X a = XΦ1 (a o id_cblinfun)
  by (auto simp: register_pair_apply)
lemmas to_XΦ1 = X_XΦ1

lemma XAB_to_XΦ2_AB: XAB a = (XΦ2;AB) ((swap r id) (assoc' (id_cblinfun o assoc a)))
  by (simp add: pair_o_tensor[unfolded o_def, THEN fun_cong] register_pair_apply
      pair_o_swap[unfolded o_def, THEN fun_cong]
      pair_o_assoc'[unfolded o_def, THEN fun_cong]
      pair_o_assoc[unfolded o_def, THEN fun_cong])

lemma XΦ2_to_XΦ2_AB: XΦ2 a = (XΦ2;AB) (a o id_cblinfun)
  by (simp add: register_pair_apply)

schematic_goal Φ2AB_to_XΦ2_AB: "Φ2AB a = (XΦ2;AB) ?b"
  apply (subst pair_o_assoc'[unfolded o_def, THEN fun_cong])
     apply simp_all[3]
  apply (subst register_pair_apply[where a=id_cblinfun])
   apply simp_all[2]
  apply (subst pair_o_assoc[unfolded o_def, THEN fun_cong])
     apply simp_all[3]
  by simp

lemmas to_XΦ2_AB = XAB_to_XΦ2_AB XΦ2_to_XΦ2_AB Φ2AB_to_XΦ2_AB

lemma teleport:
  assumes [simp]: "norm ψ = 1"
  shows "hoare (XAB =q ψ  Φ =q β00) (teleport a b) (Φ2AB =q ψ)"
proof -
  define XZ :: bit update where "XZ = (if a=1 then (if b=1 then pauliZ oCL pauliX else pauliX) else (if b=1 then pauliZ else id_cblinfun))"

  define pre where "pre = XAB =q ψ"

  define O1 where "O1 = Φ (selfbutter β00)"
  have (XAB =q ψ  Φ =q β00) = O1 *S pre
    unfolding pre_def O1_def EQ_def
    apply (subst compatible_proj_intersect[where R=XAB and S=Φ])
       apply (simp_all add: butterfly_is_Proj)
    apply (subst swap_registers[where R=XAB and S=Φ])
    by (simp_all add: cblinfun_assoc_left(2))

  also
  define O2 where "O2 = XΦ1 CNOT oCL O1"
  have hoare (O1 *S pre) [apply CNOT XΦ1] (O2 *S pre)
    apply (rule hoare_apply) by (simp add: O2_def cblinfun_assoc_left(2))

  also
  define O3 where O3 = X hadamard oCL O2
  have hoare (O2 *S pre) [apply hadamard X] (O3 *S pre)
    apply (rule hoare_apply) by (simp add: O3_def cblinfun_assoc_left(2))

  also
  define O4 where O4 = Φ1 (selfbutterket a) oCL O3
  have hoare (O3 *S pre) [ifthen Φ1 a] (O4 *S pre)
    apply (rule hoare_ifthen) by (simp add: O4_def cblinfun_assoc_left(2))

  also
  define O5 where O5 = X (selfbutterket b) oCL O4
  have hoare (O4 *S pre) [ifthen X b] (O5 *S pre)
    apply (rule hoare_ifthen) by (simp add: O5_def cblinfun_assoc_left(2))

  also
  define O6 where O6 = Φ2 (if a=1 then pauliX else id_cblinfun) oCL O5
  have hoare (O5 *S pre) [apply (if a=1 then pauliX else id_cblinfun) (Φ  Snd)] (O6 *S pre)
    apply (rule hoare_apply) by (auto simp add: O6_def cblinfun_assoc_left(2))

  also
  define O7 where O7 = Φ2 (if b = 1 then pauliZ else id_cblinfun) oCL O6
  have O7: O7 = Φ2 XZ oCL O5
    by (auto simp add: O6_def O7_def XZ_def register_mult lift_cblinfun_comp[OF register_mult])
  have hoare (O6 *S pre) [apply (if b=1 then pauliZ else id_cblinfun) (Φ  Snd)] (O7 *S pre)
    apply (rule hoare_apply) 
    by (auto simp add: O7_def cblinfun_assoc_left(2))

  finally have hoare: hoare (XAB =q ψ  Φ =q β00) (teleport a b) (O7 *S pre)
    by (auto simp add: teleport_def comp_def)

  have O5': "O5 = (1/2) *C Φ2 (XZ*) oCL XΦ2 Uswap oCL Φ (butterfly (ket a s ket b) β00)"
    unfolding O7 O5_def O4_def O3_def O2_def O1_def 
    apply (simp split del: if_split only: to_XΦ register_mult[of ])
    apply (simp split del: if_split add: register_mult[of ] 
                flip: complex_vector.linear_scale
                del: comp_apply)
    apply (rule arg_cong[of _ _ ])
    apply (rule cblinfun_eq_mat_of_cblinfunI)
    apply (simp add: assoc_ell2_sandwich mat_of_cblinfun_tensor_op XZ_def
                     butterfly_def mat_of_cblinfun_compose mat_of_cblinfun_vector_to_cblinfun
                     mat_of_cblinfun_adj vec_of_basis_enum_ket mat_of_cblinfun_id
                     swap_sandwich[abs_def] mat_of_cblinfun_scaleR mat_of_cblinfun_scaleC
                     id_tensor_sandwich vec_of_basis_enum_tensor_state mat_of_cblinfun_cblinfun_apply
                     mat_of_cblinfun_sandwich)
    by normalization

  have [simp]: "unitary XZ"
    unfolding unitary_def unfolding XZ_def apply auto
     apply (metis cblinfun_assoc_left(1) pauliXX pauliZZ cblinfun_compose_id_left)
    by (metis cblinfun_assoc_left(1) pauliXX pauliZZ cblinfun_compose_id_left)

  have O7': "O7 = (1/2) *C XΦ2 Uswap oCL Φ (butterfly (ket a s ket b) β00)"
    unfolding O7 O5'
    by (simp add: cblinfun_compose_assoc[symmetric] register_mult[of Φ2] del: comp_apply)

  have "O7 *S pre = XΦ2 Uswap *S XAB (selfbutter ψ) *S Φ (butterfly (ket (a, b)) β00) *S "
    apply (simp add: O7' pre_def EQ_def cblinfun_compose_image)
    apply (subst lift_cblinfun_comp[OF swap_registers[where R=Φ and S=XAB]], simp)
    by (simp add: cblinfun_assoc_left(2))
  also have   XΦ2 Uswap *S XAB (selfbutter ψ) *S 
    by (simp add: cblinfun_image_mono)
  also have  = (XΦ2;AB) (Uswap o id_cblinfun) *S (XΦ2;AB)
                      ((swap r id) (assoc' (id_cblinfun o assoc (selfbutter ψ)))) *S 
    by (simp add: to_XΦ2_AB)
  also have  = Φ2AB (selfbutter ψ) *S XΦ2 Uswap *S 
    apply (simp add: swap_sandwich sandwich_grow_left to_XΦ2_AB   
        cblinfun_compose_image[symmetric] register_mult)
    by (simp add: sandwich_def cblinfun_compose_assoc[symmetric] comp_tensor_op tensor_op_adjoint)
  also have   Φ2AB =q ψ
    by (simp add: EQ_def cblinfun_image_mono)
  finally have O7 *S pre  Φ2AB =q ψ
    by simp

  with hoare
  show ?thesis
    by (meson basic_trans_rules(31) hoare_def less_eq_ccsubspace.rep_eq)
qed

end


locale concrete_teleport_vars begin

type_synonym a_state = "64 word"
type_synonym b_state = "1000000 word"
type_synonym mem = "a_state * bit * bit * b_state * bit"
type_synonym 'a var = 'a update  mem update

definition A :: "a_state var" where A a = a o id_cblinfun o id_cblinfun o id_cblinfun o id_cblinfun
definition X :: bit var where X a = id_cblinfun o a o id_cblinfun o id_cblinfun o id_cblinfun
definition Φ1 :: bit var where Φ1 a = id_cblinfun o id_cblinfun o a o id_cblinfun o id_cblinfun
definition B :: b_state var where B a = id_cblinfun o id_cblinfun o id_cblinfun o a o id_cblinfun
definition Φ2 :: bit var where Φ2 a = id_cblinfun o id_cblinfun o id_cblinfun o id_cblinfun o a

end


interpretation teleport_concrete:
  concrete_teleport_vars +
  teleport_locale concrete_teleport_vars.X
                  (concrete_teleport_vars.Φ1; concrete_teleport_vars.Φ2)
                  concrete_teleport_vars.A
                  concrete_teleport_vars.B
  apply standard
  using [[simproc del: compatibility_warn]]
  by (auto simp: concrete_teleport_vars.X_def[abs_def]
                 concrete_teleport_vars.Φ1_def[abs_def]
                 concrete_teleport_vars.Φ2_def[abs_def]
                 concrete_teleport_vars.A_def[abs_def]
                 concrete_teleport_vars.B_def[abs_def]
           intro!: compatible3' compatible3)

thm teleport
thm teleport_def

end