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⟩))⇧² ≤ 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⟩))⇧² = 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⟩))⇧² = 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⟩))⇧² = 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⟩))⇧² = 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 (verit) 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 (verit) 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 (verit) 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