Theory No_Cloning

```(*
Authors:

Anthony Bordg, University of Cambridge, apdb3@cam.ac.uk;
Yijun He, University of Cambridge, yh403@cam.ac.uk
*)

section ‹The No-Cloning Theorem›

theory No_Cloning
imports
Quantum
Tensor
begin

subsection ‹The Cauchy-Schwarz Inequality›

lemma inner_prod_expand:
assumes "dim_vec a = dim_vec b" and "dim_vec a = dim_vec c" and "dim_vec a = dim_vec d"
shows "⟨a + b|c + d⟩ = ⟨a|c⟩ + ⟨a|d⟩ + ⟨b|c⟩ + ⟨b|d⟩"
apply (simp add: inner_prod_def)
using assms sum.cong by (simp add: sum.distrib algebra_simps)

lemma inner_prod_distrib_left:
assumes "dim_vec a = dim_vec b"
shows "⟨c ⋅⇩v a|b⟩ = cnj(c) * ⟨a|b⟩"
using assms inner_prod_def by (simp add: algebra_simps mult_hom.hom_sum)

lemma inner_prod_distrib_right:
assumes "dim_vec a = dim_vec b"
shows "⟨a|c ⋅⇩v b⟩ = c * ⟨a|b⟩"
using assms by (simp add: algebra_simps mult_hom.hom_sum)

lemma cauchy_schwarz_ineq:
assumes "dim_vec v = dim_vec w"
shows "(cmod(⟨v|w⟩))⇧2 ≤ Re (⟨v|v⟩ * ⟨w|w⟩)"
proof (cases "⟨v|v⟩ = 0")
case c0:True
then have "⋀i. i < dim_vec v ⟹ v \$ i = 0"
by(metis index_zero_vec(1) inner_prod_with_itself_nonneg_reals_non0)
then have "(cmod(⟨v|w⟩))⇧2 = 0" by (simp add: assms inner_prod_def)
moreover have "Re (⟨v|v⟩ * ⟨w|w⟩) = 0" by (simp add: c0)
ultimately show ?thesis by simp
next
case c1:False
have "dim_vec w = dim_vec (- ⟨v|w⟩ / ⟨v|v⟩ ⋅⇩v v)" by (simp add: assms)
then have "⟨w + -⟨v|w⟩/⟨v|v⟩ ⋅⇩v v|w + -⟨v|w⟩/⟨v|v⟩ ⋅⇩v v⟩ = ⟨w|w⟩ + ⟨w|-⟨v|w⟩/⟨v|v⟩ ⋅⇩v v⟩ +
⟨-⟨v|w⟩/⟨v|v⟩ ⋅⇩v v|w⟩ + ⟨-⟨v|w⟩/⟨v|v⟩ ⋅⇩v v|-⟨v|w⟩/⟨v|v⟩ ⋅⇩v v⟩"
using inner_prod_expand[of "w" "-⟨v|w⟩/⟨v|v⟩ ⋅⇩v v" "w" "-⟨v|w⟩/⟨v|v⟩ ⋅⇩v v"] by auto
moreover have "⟨w|-⟨v|w⟩/⟨v|v⟩ ⋅⇩v v⟩ = -⟨v|w⟩/⟨v|v⟩ * ⟨w|v⟩"
using assms inner_prod_distrib_right[of "w" "v" "-⟨v|w⟩/⟨v|v⟩"] by simp
moreover have "⟨-⟨v|w⟩/⟨v|v⟩ ⋅⇩v v|w⟩ = cnj(-⟨v|w⟩/⟨v|v⟩) * ⟨v|w⟩"
using assms inner_prod_distrib_left[of "v" "w" "-⟨v|w⟩/⟨v|v⟩"] by simp
moreover have "⟨-⟨v|w⟩/⟨v|v⟩ ⋅⇩v v|-⟨v|w⟩/⟨v|v⟩ ⋅⇩v v⟩ = cnj(-⟨v|w⟩/⟨v|v⟩) * (-⟨v|w⟩/⟨v|v⟩) * ⟨v|v⟩"
using inner_prod_distrib_left[of "v" "-⟨v|w⟩/⟨v|v⟩ ⋅⇩v v" "-⟨v|w⟩/⟨v|v⟩"]
inner_prod_distrib_right[of "v" "v" "-⟨v|w⟩/⟨v|v⟩"] by simp
ultimately have "⟨w + -⟨v|w⟩/⟨v|v⟩ ⋅⇩v v|w + -⟨v|w⟩/⟨v|v⟩ ⋅⇩v v⟩ = ⟨w|w⟩ -  cmod(⟨v|w⟩)^2 / ⟨v|v⟩"
using assms inner_prod_cnj[of "w" "v"] inner_prod_cnj[of "v" "v"] complex_norm_square by simp
moreover have "Re(⟨w + -⟨v|w⟩/⟨v|v⟩ ⋅⇩v v|w + -⟨v|w⟩/⟨v|v⟩ ⋅⇩v v⟩) ≥ 0"
using inner_prod_with_itself_Re by blast
ultimately have "Re(⟨w|w⟩) ≥ cmod(⟨v|w⟩)^2/Re(⟨v|v⟩)"
using inner_prod_with_itself_real by simp
moreover have c2:"Re(⟨v|v⟩) > 0"
using inner_prod_with_itself_Re_non0 inner_prod_with_itself_eq0 c1 by auto
ultimately have "Re(⟨w|w⟩) * Re(⟨v|v⟩) ≥ cmod(⟨v|w⟩)^2/Re(⟨v|v⟩) * Re(⟨v|v⟩)"
by (metis less_numeral_extra(3) nonzero_divide_eq_eq pos_divide_le_eq)
thus ?thesis
using inner_prod_with_itself_Im c2 by (simp add: mult.commute)
qed

lemma cauchy_schwarz_eq [simp]:
assumes "v = (l ⋅⇩v w)"
shows "(cmod(⟨v|w⟩))⇧2 = Re (⟨v|v⟩ * ⟨w|w⟩)"
proof-
have "cmod(⟨v|w⟩) = cmod(cnj(l) * ⟨w|w⟩)"
using assms inner_prod_distrib_left[of "w" "w" "l"] by simp
then have "cmod(⟨v|w⟩)^2 = cmod(l)^2 * ⟨w|w⟩ * ⟨w|w⟩"
using complex_norm_square inner_prod_cnj[of "w" "w"] by simp
moreover have "⟨v|v⟩ = cmod(l)^2 * ⟨w|w⟩"
using assms complex_norm_square inner_prod_distrib_left[of "w" "v" "l"]
inner_prod_distrib_right[of "w" "w" "l"] by simp
ultimately show ?thesis by (metis Re_complex_of_real)
qed

lemma cauchy_schwarz_col [simp]:
assumes "dim_vec v = dim_vec w" and "(cmod(⟨v|w⟩))⇧2 = Re (⟨v|v⟩ * ⟨w|w⟩)"
shows "∃l. v = (l ⋅⇩v w) ∨ w = (l ⋅⇩v v)"
proof (cases "⟨v|v⟩ = 0")
case c0:True
then have "⋀i. i < dim_vec v ⟹ v \$ i = 0"
by(metis index_zero_vec(1) inner_prod_with_itself_nonneg_reals_non0)
then have "v = 0 ⋅⇩v w" by (auto simp: assms)
then show ?thesis by auto
next
case c1:False
have f0:"dim_vec w = dim_vec (- ⟨v|w⟩ / ⟨v|v⟩ ⋅⇩v v)" by (simp add: assms(1))
then have "⟨w + -⟨v|w⟩/⟨v|v⟩ ⋅⇩v v|w + -⟨v|w⟩/⟨v|v⟩ ⋅⇩v v⟩ = ⟨w|w⟩ + ⟨w|-⟨v|w⟩/⟨v|v⟩ ⋅⇩v v⟩ +
⟨-⟨v|w⟩/⟨v|v⟩ ⋅⇩v v|w⟩ + ⟨-⟨v|w⟩/⟨v|v⟩ ⋅⇩v v|-⟨v|w⟩/⟨v|v⟩ ⋅⇩v v⟩"
using inner_prod_expand[of "w" "-⟨v|w⟩/⟨v|v⟩ ⋅⇩v v" "w" "-⟨v|w⟩/⟨v|v⟩ ⋅⇩v v"] by simp
moreover have "⟨w|-⟨v|w⟩/⟨v|v⟩ ⋅⇩v v⟩ = -⟨v|w⟩/⟨v|v⟩ * ⟨w|v⟩"
using assms(1) inner_prod_distrib_right[of "w" "v" "-⟨v|w⟩/⟨v|v⟩"] by simp
moreover have "⟨-⟨v|w⟩/⟨v|v⟩ ⋅⇩v v|w⟩ = cnj(-⟨v|w⟩/⟨v|v⟩) * ⟨v|w⟩"
using assms(1) inner_prod_distrib_left[of "v" "w" "-⟨v|w⟩/⟨v|v⟩"] by simp
moreover have "⟨-⟨v|w⟩/⟨v|v⟩ ⋅⇩v v|-⟨v|w⟩/⟨v|v⟩ ⋅⇩v v⟩ = cnj(-⟨v|w⟩/⟨v|v⟩) * (-⟨v|w⟩/⟨v|v⟩) * ⟨v|v⟩"
using inner_prod_distrib_left[of "v" "-⟨v|w⟩/⟨v|v⟩ ⋅⇩v v" "-⟨v|w⟩/⟨v|v⟩"]
inner_prod_distrib_right[of "v" "v" "-⟨v|w⟩/⟨v|v⟩"] by simp
ultimately have "⟨w + -⟨v|w⟩/⟨v|v⟩ ⋅⇩v v|w + -⟨v|w⟩/⟨v|v⟩ ⋅⇩v v⟩ = ⟨w|w⟩ -  cmod(⟨v|w⟩)^2 / ⟨v|v⟩"
using inner_prod_cnj[of "w" "v"] inner_prod_cnj[of "v" "v"] assms(1) complex_norm_square by simp
moreover have "⟨w|w⟩ = cmod(⟨v|w⟩)^2 / ⟨v|v⟩"
using assms(2) inner_prod_with_itself_real by(metis Reals_mult c1 nonzero_mult_div_cancel_left of_real_Re)
ultimately have "⟨w + -⟨v|w⟩/⟨v|v⟩ ⋅⇩v v|w + -⟨v|w⟩/⟨v|v⟩ ⋅⇩v v⟩ = 0" by simp
then have "⋀i. i<dim_vec w ⟹ (w + -⟨v|w⟩/⟨v|v⟩ ⋅⇩v v) \$ i = 0"
by (metis f0 index_add_vec(2) index_zero_vec(1) inner_prod_with_itself_nonneg_reals_non0)
then have "⋀i. i<dim_vec w ⟹ w \$ i + -⟨v|w⟩/⟨v|v⟩ * v \$ i = 0"
by (metis assms(1) f0 index_add_vec(1) index_smult_vec(1))
then have "⋀i. i<dim_vec w ⟹ w \$ i = ⟨v|w⟩/⟨v|v⟩ * v \$ i" by simp
then have "w = ⟨v|w⟩/⟨v|v⟩ ⋅⇩v v" by (auto simp add: assms(1))
thus ?thesis by auto
qed

subsection ‹The No-Cloning Theorem›

lemma eq_from_inner_prod [simp]:
assumes "dim_vec v = dim_vec w" and "⟨v|w⟩ = 1" and "⟨v|v⟩ = 1" and "⟨w|w⟩ = 1"
shows "v = w"
proof-
have "(cmod(⟨v|w⟩))⇧2 = Re (⟨v|v⟩ * ⟨w|w⟩)" by (simp add: assms)
then have f0:"∃l. v = (l ⋅⇩v w) ∨ w = (l ⋅⇩v v)" by (simp add: assms(1))
then show ?thesis
proof (cases "∃l. v = (l ⋅⇩v w)")
case True
then have "∃l. v = (l ⋅⇩v w) ∧ ⟨v|w⟩ = cnj(l) * ⟨w|w⟩"
using inner_prod_distrib_left by auto
then show ?thesis by (simp add: assms(2,4))
next
case False
then have "∃l. w = (l ⋅⇩v v) ∧ ⟨v|w⟩ = l * ⟨v|v⟩"
using f0 inner_prod_distrib_right by auto
then show ?thesis by (simp add: assms(2,3))
qed
qed

lemma hermite_cnj_of_tensor:
shows "(A ⨂ B)⇧†  = (A⇧†) ⨂ (B⇧†)"
proof
show c0:"dim_row ((A ⨂ B)⇧†) = dim_row ((A⇧†) ⨂ (B⇧†))" by simp
show c1:"dim_col ((A ⨂ B)⇧†) = dim_col ((A⇧†) ⨂ (B⇧†))" by simp
show "⋀i j. i < dim_row ((A⇧†) ⨂ (B⇧†)) ⟹ j < dim_col ((A⇧†) ⨂ (B⇧†)) ⟹
((A ⨂ B)⇧†) \$\$ (i, j) = ((A⇧†) ⨂ (B⇧†)) \$\$ (i, j)"
proof-
fix i j assume a0:"i < dim_row ((A⇧†) ⨂ (B⇧†))" and a1:"j < dim_col ((A⇧†) ⨂ (B⇧†))"
then have "(A ⨂ B)⇧† \$\$ (i, j) = cnj((A ⨂ B) \$\$ (j, i))" by (simp add: dagger_def)
also have "… = cnj(A \$\$ (j div dim_row(B), i div dim_col(B)) * B \$\$ (j mod dim_row(B), i mod dim_col(B)))"
by (metis (mono_tags, lifting) a0 a1 c1 dim_row_tensor_mat dim_col_of_dagger dim_row_of_dagger
index_tensor_mat less_nat_zero_code mult_not_zero neq0_conv)
moreover have "((A⇧†) ⨂ (B⇧†)) \$\$ (i, j) =
(A⇧†) \$\$ (i div dim_col(B), j div dim_row(B)) * (B⇧†) \$\$ (i mod dim_col(B), j mod dim_row(B))"
by (smt a0 a1 c1 dim_row_tensor_mat dim_col_of_dagger dim_row_of_dagger index_tensor_mat
less_nat_zero_code mult_eq_0_iff neq0_conv)
moreover have "(B⇧†) \$\$ (i mod dim_col(B), j mod dim_row(B)) = cnj(B \$\$ (j mod dim_row(B), i mod dim_col(B)))"
proof-
have "i mod dim_col(B) < dim_col(B)"
using a0 gr_implies_not_zero mod_div_trivial by fastforce
moreover have "j mod dim_row(B) < dim_row(B)"
using a1 gr_implies_not_zero mod_div_trivial by fastforce
ultimately show ?thesis by (simp add: dagger_def)
qed
moreover have "(A⇧†) \$\$ (i div dim_col(B), j div dim_row(B)) = cnj(A \$\$ (j div dim_row(B), i div dim_col(B)))"
proof-
have "i div dim_col(B) < dim_col(A)"
using a0 dagger_def by (simp add: less_mult_imp_div_less)
moreover have "j div dim_row(B) < dim_row(A)"
using a1 dagger_def by (simp add: less_mult_imp_div_less)
ultimately show ?thesis by (simp add: dagger_def)
qed
ultimately show "((A ⨂ B)⇧†) \$\$ (i, j) = ((A⇧†) ⨂ (B⇧†)) \$\$ (i, j)" by simp
qed
qed

locale quantum_machine =
fixes n:: nat and s:: "complex Matrix.vec" and U:: "complex Matrix.mat"
assumes dim_vec [simp]: "dim_vec s = 2^n"
and dim_col [simp]: "dim_col U = 2^n * 2^n"
and square [simp]: "square_mat U" and unitary [simp]: "unitary U"

lemma inner_prod_of_unit_vec:
fixes n i:: nat
assumes "i < n"
shows "⟨unit_vec n i| unit_vec n i⟩ = 1"
by (auto simp add: inner_prod_def unit_vec_def)
(simp add: assms sum.cong[of "{0..<n}" "{0..<n}"
"λj. cnj (if j = i then 1 else 0) * (if j = i then 1 else 0)" "λj. (if j = i then 1 else 0)"])

theorem (in quantum_machine) no_cloning:
assumes [simp]: "dim_vec v = 2^n" and [simp]: "dim_vec w = 2^n" and
cloning1: "⋀s. U * ( |v⟩ ⨂ |s⟩) = |v⟩ ⨂ |v⟩" and
cloning2: "⋀s. U * ( |w⟩ ⨂ |s⟩) = |w⟩ ⨂ |w⟩" and
"⟨v|v⟩ = 1" and "⟨w|w⟩ = 1"
shows "v = w ∨ ⟨v|w⟩ = 0"
proof-
define s:: "complex Matrix.vec" where d0:"s = unit_vec (2^n) 0"
have f0:"⟨|v⟩| ⨂ ⟨|s⟩| = (( |v⟩ ⨂ |s⟩)⇧†)"
using hermite_cnj_of_tensor[of "|v⟩" "|s⟩"] bra_def dagger_def ket_vec_def by simp
moreover have f1:"( |v⟩ ⨂ |v⟩)⇧† * ( |w⟩ ⨂ |w⟩) = (⟨|v⟩| ⨂ ⟨|s⟩| ) * ( |w⟩ ⨂ |s⟩)"
proof-
have "(U * ( |v⟩ ⨂ |s⟩))⇧† = (⟨|v⟩| ⨂ ⟨|s⟩| ) * (U⇧†)"
using dagger_of_prod[of "U" "|v⟩ ⨂ |s⟩"] f0 d0 by (simp add: ket_vec_def)
then have "(U * ( |v⟩ ⨂ |s⟩))⇧† * U * ( |w⟩ ⨂ |s⟩) = (⟨|v⟩| ⨂ ⟨|s⟩| ) * (U⇧†) * U * ( |w⟩ ⨂ |s⟩)" by simp
moreover have "(U * ( |v⟩ ⨂ |s⟩))⇧† * U * ( |w⟩ ⨂ |s⟩) = (( |v⟩ ⨂ |v⟩)⇧†) * ( |w⟩ ⨂ |w⟩)"
using assms(2-4) d0 unit_vec_def by (smt Matrix.dim_vec assoc_mult_mat carrier_mat_triv dim_row_mat(1)
dim_row_tensor_mat dim_col_of_dagger index_mult_mat(2) ket_vec_def square square_mat.elims(2))
moreover have "(U⇧†) * U = 1⇩m (2^n * 2^n)"
using unitary_def dim_col unitary by simp
moreover have "(⟨|v⟩| ⨂ ⟨|s⟩| ) * (U⇧†) * U = (⟨|v⟩| ⨂ ⟨|s⟩| ) * ((U⇧†) * U)"
using d0 assms(1) unit_vec_def by (smt Matrix.dim_vec assoc_mult_mat carrier_mat_triv dim_row_mat(1)
dim_row_tensor_mat f0 dim_col_of_dagger dim_row_of_dagger ket_vec_def local.dim_col)
moreover have "(⟨|v⟩| ⨂ ⟨|s⟩| ) * 1⇩m (2^n * 2^n) = (⟨|v⟩| ⨂ ⟨|s⟩| )"
using f0 ket_vec_def d0 by simp
ultimately show ?thesis by simp
qed
then have f2:"(⟨|v⟩| * |w⟩) ⨂ (⟨|v⟩| * |w⟩) = (⟨|v⟩| * |w⟩) ⨂ (⟨|s⟩| * |s⟩)"
proof-
have "⟨|v⟩| ⨂ ⟨|v⟩| = (( |v⟩ ⨂ |v⟩)⇧†)"
using hermite_cnj_of_tensor[of "|v⟩" "|v⟩"] bra_def dagger_def ket_vec_def by simp
then show ?thesis
using f1 d0 by (simp add: bra_def mult_distr_tensor ket_vec_def)
qed
then have "⟨v|w⟩ * ⟨v|w⟩ = ⟨v|w⟩ * ⟨s|s⟩"
proof-
have "((⟨|v⟩| * |w⟩) ⨂ (⟨|v⟩| * |w⟩)) \$\$ (0,0) = ⟨v|w⟩ * ⟨v|w⟩"
using assms inner_prod_with_times_mat[of "v" "w"] by (simp add: bra_def ket_vec_def)
moreover have "((⟨|v⟩| * |w⟩) ⨂ (⟨|s⟩| * |s⟩)) \$\$ (0,0) = ⟨v|w⟩ * ⟨s|s⟩"
using inner_prod_with_times_mat[of "v" "w"] inner_prod_with_times_mat[of "s" "s"] by(simp add: bra_def ket_vec_def)
ultimately show ?thesis using f2 by auto
qed
then have "⟨v|w⟩ = 0 ∨ ⟨v|w⟩ = ⟨s|s⟩" by (simp add: mult_left_cancel)
moreover have "⟨s|s⟩ = 1" by(simp add: d0 inner_prod_of_unit_vec)
ultimately show ?thesis using assms(1,2,5,6) by auto
qed

end```