Quantum.thy · quantum computing · Zulip Chat Archive

One should remove the condition state n v in prob0 and prob1. The if/then/else structure here is useless. Of course, the condition state n v should be listed among the assumptions in the subsequent lemmas whenever needed, but in the definition itself it's useless.
@Hanna Lachnitt @Yijun He

Hanna Lachnitt (Aug 13 2019 at 14:47):

That would be good it gave me some problems in Deutsch-Jozsa

Hanna Lachnitt (Aug 13 2019 at 14:49):

Also could we maybe use k instead of j in the def of select_index?

Anthony Bordg (Aug 13 2019 at 14:56):

That would be good it gave me some problems in Deutsch-Jozsa

This is what I have in mind actually.

Anthony Bordg (Aug 13 2019 at 15:05):

prob0 and prob1 have been simplify and Quantum.thy has been updated on GitHub.

Anthony Bordg (Aug 15 2019 at 10:41):

What about moving everything related to measurement from Quantum.thy to a dedicated theory Measurement.thy ?
@Yijun He @Hanna Lachnitt

Hanna Lachnitt (Aug 15 2019 at 10:51):

I would totally opt for that.

Yijun He (Aug 15 2019 at 10:56):

I also agree with that.

Anthony Bordg (Aug 20 2019 at 15:46):

Ok, but to avoid a loop (Measurement.thy importing Quantum.thy and Quantum.thy importing Measurement.thy) I would need to put the definition of Bell states and everything related to them in Measurement.thy or in a dedicated theory Bell.thy.
@Hanna Lachnitt @Yijun He

Hanna Lachnitt (Aug 20 2019 at 15:53):

Hmm... both does not sound perfect. Why don't you want to leave the definitions of the Bell states in Quantum.thy and move their measurement in Measurement.thy? Is it because facts about the Bell states would be scattered then or does it have another reason?

Anthony Bordg (Aug 20 2019 at 15:59):

Hmm... both does not sound perfect. Why don't you want to leave the definitions of the Bell states in Quantum.thy and move their measurement in Measurement.thy? Is it because facts about the Bell states would be scattered then or does it have another reason?

Yes, it would be scattered, but actually I think it's fine and probably the best solution.

Anthony Bordg (Oct 01 2019 at 09:30):

@Yijun He In Quantum.thy one proves that a unitary matrix is length-preserving. It would be nice to add the converse implication, namely that a length-preserving matrix is unitary. The proof is not difficult. We could mention this result in the section 2 of the article.

Anthony Bordg (Oct 01 2019 at 10:55):

@Yijun He
I should probably rename hermite_cnj with dagger for conciseness.

Hanna Lachnitt (Oct 01 2019 at 12:13):

I would also like to move this lemma into Quantum.thy if thats fine for you.

lemma cpx_mat_transpose_prod:
  fixes M N::"complex Matrix.mat"
  assumes "dim_col M = dim_row N"
  shows "(M * N)⇧t = N⇧t * (M⇧t)"
proof
  fix i j::nat
  assume a0: "i < dim_row (N⇧t * (M⇧t))" and a1: "j < dim_col (N⇧t * (M⇧t))"
  then have "(M * N)⇧t $$ (i,j) = (M * N) $$ (j,i)" by auto
  also have "... = (∑k<dim_row M⇧t.  M $$ (j,k) * N $$ (k,i))"
    using assms a0 a1 by auto
  also have "... = (∑k<dim_row M⇧t. N $$ (k,i) * M $$ (j,k))"
   by (simp add: semiring_normalization_rules(7))
  also have "... = (∑k<dim_row M⇧t. ((N⇧t) $$ (i,k)) * (M⇧t) $$ (k,j))"
    using assms a0 a1 by auto
  finally show "((M * N)⇧t) $$ (i,j) = (N⇧t * (M⇧t)) $$ (i,j)"
    using assms a0 a1 by auto
next
  show "dim_row ((M * N)⇧t) = dim_row (N⇧t * (M⇧t))" by auto
next
  show "dim_col ((M * N)⇧t) = dim_col (N⇧t * (M⇧t))" by auto
qed

I need it for the quantum fourier transform, but it fits into Quantum.thy much better. I can also make a pull request for this if you want to.

Hanna Lachnitt (Oct 01 2019 at 12:29):

And also this

lemma cpx_mat_hermite_cnj_prod:
  fixes M N::"complex Matrix.mat"
  assumes "dim_col M = dim_row N"
  shows "(M * N)⇧† = N⇧† * (M⇧†)"
proof-
  have "(M * N)⇧† = ((M * N)⇧⋆)⇧t" by auto
  also have "... = ((M⇧⋆) * (N⇧⋆))⇧t" using assms cpx_mat_cnj_prod by auto
  also have "... = (N⇧⋆)⇧t * ((M⇧⋆)⇧t)"
    by (metis assms cpx_mat_transpose_prod cnj_transpose hermite_cnj_dim_col hermite_cnj_dim_row index_transpose_mat(2) index_transpose_mat(3))
  finally show "(M * N)⇧† = N⇧† * (M⇧†)" by auto
qed

Anthony Bordg (Oct 01 2019 at 14:22):

I would also like to move this lemma into Quantum.thy if thats fine for you.

@Hanna Lachnitt sure, please open a PR with your lemmas.
But first you may need to update your branch due to the recent changes I made in the master branch.

Yijun He (Oct 02 2019 at 01:21):

Yijun He In Quantum.thy one proves that a unitary matrix is length-preserving. It would be nice to add the converse implication, namely that a length-preserving matrix is unitary. The proof is not difficult. We could mention this result in the section 2 of the article.

@Anthony Bordg I will work on the lemma today and add it to the pull request.

Hanna Lachnitt (Oct 02 2019 at 12:28):

Pull request is open :) I added another lemma about the product of two gates.

Yijun He (Oct 04 2019 at 10:14):

@Anthony Bordg I have finished the proof and updated the pull request, but the proof seems too complicated. I will try to clean it up tonight.

Anthony Bordg (Oct 04 2019 at 11:05):

Anthony Bordg I have finished the proof and updated the pull request, but the proof seems too complicated. I will try to clean it up tonight.

@Yijun He Great!
One could use the following result:

$\lVert M|\psi\rangle\rVert^2 = \langle \psi|M^{\dagger}M|\psi\rangle\;.$

Then use

$(M^{\dagger}M)_{ii}= \langle e_i|M^{\dagger}M|e_i\rangle$

and the assumption that $M$ is length-preserving to prove that the diagonal elements of $M^{\dagger}M$ are $1$ .
The result

$\lVert M|\psi\rangle\rVert^2 = \langle \psi|M^{\dagger}M|\psi\rangle$

can easily be formalized using cpx_vec_length_inner_prod and bra_mat_on_vec.

Yijun He (Oct 04 2019 at 13:38):

I finished cleaning up just now.

Last updated: Nov 02 2025 at 20:20 UTC

Stream: quantum computing

Topic: Quantum.thy

Anthony Bordg (Aug 13 2019 at 14:45):