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 and 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Φ ≡ (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 = XΦ (id_cblinfun ⊗⇩o a)›
  by (auto simp: register_pair_apply)
lemma XΦ1_XΦ: ‹XΦ1 a = XΦ (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 = XΦ ((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 = XΦ (id_cblinfun ⊗⇩o (id_cblinfun ⊗⇩o a))›
  by (auto simp: Snd_def register_pair_apply)
lemma X_XΦ: ‹X a = XΦ (a ⊗⇩o id_cblinfun)›
  by (auto simp: register_pair_apply)
lemma Φ1_XΦ: ‹Φ1 a = XΦ (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 o⇩C⇩L 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 o⇩C⇩L 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 o⇩C⇩L 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) o⇩C⇩L 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) o⇩C⇩L 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) o⇩C⇩L 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) o⇩C⇩L O6›
  have O7: ‹O7 = Φ2 XZ o⇩C⇩L 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*) o⇩C⇩L XΦ2 Uswap o⇩C⇩L Φ (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 XΦ])
    apply (simp split del: if_split add: register_mult[of XΦ] 
                flip: complex_vector.linear_scale
                del: comp_apply)
    apply (rule arg_cong[of _ _ XΦ])
    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 o⇩C⇩L Φ (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