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 = 1m (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| ) * 1m (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