# 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Φ ≡ (X;Φ)"
abbreviation "XAB ≡ ((X;A); B)"
abbreviation "AB ≡ (A;B)"
abbreviation "Φ2AB ≡ ((Φ o Snd; A); B)"

definition "teleport a b = [
apply CNOT XΦ1,
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)›

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 (subst swap_registers[where R=XAB and S=Φ])

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
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)
also have ‹… ≤ XΦ2 Uswap *⇩S XAB (selfbutter ψ) *⇩S ⊤›
also have ‹… = (XΦ2;AB) (Uswap ⊗⇩o id_cblinfun) *⇩S (XΦ2;AB)
((swap ⊗⇩r id) (assoc' (id_cblinfun ⊗⇩o assoc (selfbutter ψ)))) *⇩S ⊤›
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)
also have ‹… ≤ Φ2AB =⇩q ψ›
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
```