@Yijun He I'm going to work on the `sorry`

you temporarily left.

@Yijun He There might be a problem with the first `sorry`

in `qft_no_swap_of_unit_vec`

. Maybe some additional assumptions are needed. Please see the attached file with my comments.

Quantum_Fourier_Transform_draft.thy

Yes I also found it, and I just pushed a fix to my fork

I also have a question about induction: how can I impose a restriction to the induction variable? For example, I want to induct in the range 0 <= m <= n-1, but using "proof (induction m)" stops me from using the assumption "m<n" in case (Suc m), since m is already specified in this case

@Yijun He The fastest method to get an answer to your question is to ask Larry before he leaves his office at 5pm! :running:

It seems that he is not in his office today :sweat:

@Yijun He OK, I had no luck with the documentation. For an induction on $m$ with the specified range, in the case `Suc m`

you should be able to use $m < n-1$, not $m<n$, so Isabelle is right. Can you ask the mailing list (Distribution & Support) ?

I found a way to use the assumption just now, but it looks a bit messy: I added "m>n or..." to the induction hypothesis of qft_no_swap_of_unit_vec, which allows me to trivially say "m > n ==> (Suc m) > n" when m is greater than n.

@Yijun He `ind_from_1`

and its use in `pow_tensor_dim_row`

by @Hanna Lachnitt in her theory Deutsch_Jozsa.thy might be a source of inspiration wrt the problem we discuss earlier.

@Yijun He I'm going to take care of the simplification of `uniq_select_index`

.

@Yijun He In `uniq_select_index`

I'm thinking about refactoring the statement `⋀a. (a∈{..<n+1} ⟹ i mod (2^a) = j mod (2^a))`

under the appropriate assumptions. Do you think it might be a useful lemma on its own ?

I am not sure about that

That statement requires the assumption that `⋀a. (a∈{..<n} ⟹ select_index n a i = select_index n a j)`

, which seems too specific

Ok, in that case I don't see a way to shorten the proof by refactoring or changing its structure. But at least I can try to clean the proof of `⋀a. (a∈{..<n+1} ⟹ i mod (2^a) = j mod (2^a))`

which seems the longest step.

OK, thanks!

On the other hand, it's true that `⋀a. (a∈{..<n} ⟹ select_index n a i = select_index n a j)`

is specific, but refactoring may be the first step towards putting all this fancy stuff about `select_index`

into a dedicated theory, or even into a specific section of the `Basics`

theory.

That might be a better solution, as it is indeed a basic/intuitive result of number theory/modular arithmetic

Of course, in that case we can directly put the whole proof `uniq_select_index `

somewhere else, but I still feel the proof is too long. Also, somewhere else we might have burried some lemmas related to `select_index`

inside proofs. In that case, refactoring and then putting that stuff in a dedicated place is the way to go.

@Yijun He Inside the syntax `case (Suc a)`

you can't write `a + 1`

, but everywhere else in the proof note that you can and should write `a + 1`

, since we do not want the code to feel alien for any ordinary mathematician.

I am not sure why, but sometimes `auto`

might fail when I change `Suc k`

to `k+1`

(and sometimes it works properly).

In that specific case I had no trouble with auto. :slight_smile:

OK, I will change it to `k + 1`

whenever possible.

I did it for `uniq_select_index`

.

So, keep `Suc k`

if for whatever reason you have some trouble and write `k + 1`

whenever possible.

@Yijun He I cleaned the proof of `uniq_select_index`

(please see my PR). From that proof I factored out two lemmas `mod_pow_2_eq`

and `select_index_eq_to_mod_eq`

. It's unlikely that `select_index_eq_to_mod_eq`

will be useful in the future, but I believe `mod_pow_2_eq`

may be useful. Also, the whole thing is now much more legible than previously.

@Anthony Bordg I am currently struggling with the complicated expressions in quantum Fourier transform. In the book, the vectors are expressed as the tensor product of n qubits, but I am not sure about how to do that in Isabelle (product and sum require the operators to be `comm_monoid`

, which doesn't work for tensor product and even vector addition), and my current expressions using products and `select_index`

seems too complicated to work with. Could you give me some advice about it? Many thanks.

@Yijun He vector addition is obviously a monoid law (for any given dimension), so I would be very surprised if it's not already proven, and if it's not then we need to prove it.

For example, when I try to make a statement `"v = (∑k<n. unit_vec n k)"`

(this is incorrect, but the variable types should be correct), Isabelle gives an error message saying `No type arity Matrix.vec :: comm_monoid_add`

Can I find your draft on GitHub ? Otherwise, please send me your file.

I just pushed my updates to GitHub.

I added a test lemma `sum_of_unit_vec`

, which uses the exact statement above and should give an error message.

`unit_vec n k`

is of type `complex Matrix.vec`

. Now, if you look at the theory `Matrix.thy`

, you see the lemma `comm_monoid_vec`

, where the locale `comm_monoid`

is introduced in `Group.thy`

. But, `comm_monoid_add`

is a class introduced in `Groups.thy`

.

So, it's enough to prove `comm_monoid_add`

of the set of complex vectors of a given dimension. I will do that.

thanks!

Just to show a different approach. My solution for expressing "v = (∑k<n. unit_vec n k)" would be to go from "complex vec" to "nat ell2" using my function "vec_to_ell2". The type "nat ell2" is the complex Hilbert space of square-summable sequences of complex numbers (in particular comm_monoid). In order to return to "complex vec" from "nat ell2", I use the function "ell2_to_vec". Indeed, "unit_vec n k" goes to what I call "ket k" in "nat ell2". Finite_Dimensional_Case.thy

@Yijun He Even better, I browsed the theory `Matrix.thy`

and I discovered that one has the definition `finsum_vec`

. I think this is the definition you want to use here and the corresponding lemmas they proved to handle such sums.

`finsum_vec`

seems to work now. Many thanks!

The only thing lacking is a nice notation like $\sum$ for `finsum_vec`

, but we can introduce it as an abbreviation.

@Yijun He About the use of `Suc n`

vs `n+1`

Part 2 of the style guide (7th bullet) seems to have a point when it says that it depends on the distinction between top-level lemmas that you may want to present to people and lemmas that are used in further proofs as a convenient scaffolding in the formalization process. For the latter, normal forms are fine and may help automation.

@Yijun He This afternoon I plan to work on the proof of `qubits_tensor_prod`

. Is that ok with you ?

That would be great, thanks! Actually it still needs some assumptions on the functions f and g's. I am still working on the proof of `qft_no_swap_of_unit_vec`

.

@Yijun He done. But, for the proof the associativity of the tensor product of matrices is needed. So, I'm going to prove this associativity in `Tensor.thy`

.

@Yijun He Probably due to the changes in `Binary_Nat.thy`

your proof of `select_index_eq_bin_rep`

is broken. The bad thing: I don't get a proof without smt.

@Yijun He In `qubits_rep`

I changed `select_index n j i`

to `select_index n i j`

(and made the corresponding changes).

Indeed, in `Quantum.thy`

`select_index`

is defined as

select_index n i j ≡ (i≤n-1) ∧ (j≤2^n - 1) ∧ (j mod 2^(n-i) ≥ 2^(n-1-i)).

It's confusing to use the same letters but with a permutation.

Associativity for the tensor product of complex matrices done.

@Yijun He I made a PR in your master branch. Also, `Tensor.thy`

is up-to-date in my master branch.

Thanks! Pull request merged.

@Yijun He Please tell me which `sorry`

you want me to tackle next.

Maybe the `sorry`

in `qft_no_swap_of_unit_vec`

? Now I am not even sure whether my formulation is correct. Many thanks.

Ok, in that case I will work on the first `sorry`

in `qft_no_swap_of_unit_vec`

.

@Yijun He In the book what is the corresponding element to `qft_no_swap n m v`

?

It should be an intermediate state of the expression (5.17), where `v`

is the unit vector |j⟩.

@Yijun He We have to do some reverse engineering here if we have Shor's algorithm in mind. To what extent do we need the quantum Fourier Transform to formalize Shor's algorithm ?

Proving correctness of Shor's algorithm seems to need the correctness of inverse Quantum Fourier Transform.

Proving correctness of Shor's algorithm seems to need the correctness of inverse Quantum Fourier Transform.

@Yijun He Yes, but this is not what I meant.

As usual in mathematics we want to make our life easier, at least to start and generalize eventually. So, If we start with the quantum Fourier transform on 3 qubits for instance, to avoid a difficult and messy formalization at least at the beginning, then to what extent the nice applications of the quantum Fourier transform still make sense ?

I think quantum Fourier transform is just a faster way of computing the classical Fourier transform on qubits, so Shor's algorithm works (more slowly, but still correctly) even with the classical Fourier transform, and it doesn't depend on any nice property of the quantum one.

I think quantum Fourier transform is just a faster way of computing the classical Fourier transform on qubits, so Shor's algorithm works (more slowly, but still correctly) even with the classical Fourier transform, and it doesn't depend on any nice property of the quantum one.

Yes, you're right and actually one could say the same thing about anything in quantum computing, it's "just" a way to speed up classical algorithms. But, the fast Fourier transform is already in the AFP and we want to contribute something new. Moreover, it would be a shame to lose your nice work on the quantum Fourier transform, but to avoid to get stuck we may need, at least temporarily, to assume a fixed number of qubits, then the formalization should be more workable.

Hey :) I believe that I found a way to formalize quantum Fourier tranform without things getting so complicated in the first place. My controlled R gate is just a 4x4 matrix (as in the literature) and I use swapping to get the qubit needed in front of the unit vector (this seems to be done in practice as well). I am not entirely sure if this will avoid getting in trouble (it needs some unit vector decomposition lemmas) but I am pretty confident. @Yijun He do you feel this is a way I should pursue or do you think the current formalization is fixable? I will also have a more thoroughly look at the current file once I finish with Grover.

I still think the current proof is fixable, but a 4x4 controlled R gate sounds much better than the current proof. It would be great if you can help with the formalization of quantum Fourier transform.

Hey :) I believe that I found a way to formalize quantum Fourier tranform without things getting so complicated in the first place. My controlled R gate is just a 4x4 matrix (as in the literature) and I use swapping to get the qubit needed in front of the unit vector (this seems to be done in practice as well).

@Hanna Lachnitt @Yijun He It sounds promising.

Until now everything worked out, although of course there could be troubles later. I uploaded a first tentative theory in a QFT branch in my fork where I tried out my ideas. Everything is still under construction (especially some indices might be wrong). I hope I did not just do nonsense or made a stupid mistake :fear: However, I feel with this new approach proving becomes more difficult in terms of thinking about what parameters to use before proving something but the proofs themselves are rather easy now. And I feel that its well understandable for a reader especially with some explanations

The idea behind the approach is not to define a matrix R_k with takes a huge unit vector and has to select all indices of qubits i and k to extend the binary fraction as this creates complexity. Instead swap the needed qubit $|j_k\rangle$ outside of unit vector $| j_l,...,j_n \rangle$ (which is just a tensor product of single qubits, and $j_k$ corresponds to the qubit at position k). Then, apply a 4x4 CR gate to the tensor product of this two qubits i and k. Since the second qubit is left untouched by this operation it can just be swapped back afterwards. This corresponds to an application of a $R_k$ gate to qubit i.

The file is still messy but I felt it was better to involve you in the process, I will make it more readable and add further proofs, so please pull from time to time if you have a look at it. Right now I am leaving proofs which are supposed to be very easy or bound to work for later to see if the overall approach is promising.

Hey guys :) Just to keep you updated, I managed to prove calculation (5.4) from page 218 of Nielsen and Chuang. There are some easy proofs missing (including almost all gate proofs) but nothing that should cause any problems. The equivalence of (5.4) to the definition of quantum fourier transform is described as using only elementary algebra so I hope it will be doable :)

@Anthony Bordg Regarding your comment about:

subsection ‹Transformation of j into a Tensor Product of Single Qubits›

what do you thing about:

subsection ‹Transformation of the Input into a Tensor Product of Single Qubits›

Anthony Bordg Regarding your comment about:

subsection ‹Transformation of j into a Tensor Product of Single Qubits›

what do you thing about:

subsection ‹Transformation of the Input into a Tensor Product of Single Qubits›

@Hanna Lachnitt I think it's better. If I remember correctly "Mike and Ike", $|j\rangle$ is any basis state. Do you define qFt directly on an arbitrary state ? In other words is your "input" here refering to an arbitrary state ? If yes, why not simply "Transformation of a State into a Tensor Product of Single Qubits"? We could even later move this part into More_Tensor.thy.

Yes qFt takes an arbitrary basis state (actually just a natural number). Sound good, I will take that. Especially if its moved to some other theory input does not make sense. Also I wrote an introductory comment which might explain things a bit better.

As to your comment to to_list_bound:

`Also, it seems that you start counting from 1 for the position s while all the rest of the library takes the convention that we start counting from 0.`

I did this to stick closely to the literature where $j_1j_2...j_n$ are used for the binary representation of j. Actually I also did this for the $CR_i$ gates and so on. Otherwise it would be a bit confusing. While I work through the theory I will search for cases where I started to count from 0 it might be better to change them instead of changing the cases where counting starts from 1.

I have renamed the abbreviation for to_tensor_prod j⨂ with ⨂r, standing for tensor product representation since j should not appear in any names

Should the comments rather be texts?

I decided to rename qr to phase_shifted_qubit, in short psq. I am still not 100% happy with that but qr is unacceptable. If there is a better possibility I would be happy for suggestions.

Regarding your comment about `lemma transpose_of_controlled_phase_shift: (* AB: Maybe simply transpose_of_CR ? *)`

Isn't this the same thing as having H in a lemma name instead of hadamard_gate? So it would mix up notation and full name of the definition. But I would be happy to change this, shorter names would be preferable here.

I also tried to change the definition qr/phase_shifted_qubit into an abbreviation. But then it got so slow that I had to set everything back. Might be just my laptop though, its not very powerful.

Regarding your comment about

`lemma transpose_of_controlled_phase_shift: (* AB: Maybe simply transpose_of_CR ? *)`

Isn't this the same thing as having H in a lemma name instead of hadamard_gate? So it would mix up notation and full name of the definition. But I would be happy to change this, shorter names would be preferable here.

There are two things we should absolutely avoid. First, variables in names. Second, notations in names if those notations are not standard. However, using very standard notations, like H or cR, in names is fine.

Great, then I will change this, its much better readable.

Should the comments rather be texts?

At some point we should replace the source comments with text blocks, but it's unimportant at that stage. They are more fundamental things we need first to take care

Yes of course. I just replaced some of the latex code in the comments with the built-in code for readability, e.g. $|j_1,j_2,...,j_n\rangle$ with $|j_1,j_2,...,j_n\rangle$ but if they are replaced with text at some point I would not do that.

@Hanna Lachnitt There is something still confusing in the first comment. In your example, what's the link between $j=11$ and $|01011\rangle$ ? Do you mean $|00011\rangle$ instead ?

01011 is the binary representation of 11. I used the notation as it is introduced in the book of Nielsen and Chuang. To make it clearer I could add that $|j_1j_2...j_n\rangle$ = $|01011\rangle$ where $j = j_1*2^{n-1}+...+j_n*2^0$ which is simply written as $j=j_1...j_n$ in the book (the notation is a bit untidy).

Indeed if one writes $|j\rangle$ what is meant is always j in binary representation (its really untidy), never something like 000j. Otherwise how would you encode e.g. 3 if 11 is $|00011\rangle$?

I realize now that I maybe should take another number as example that does contain a digit beyond 1, e.g. 12. This might make it clearer and avoid confusion between binary and decimal representation.

01011 is the binary representation of 11. I used the notation as it is introduced in the book of Nielsen and Chuang. To make it clearer I could add that $|j_1j_2...j_n\rangle$ = $|01011\rangle$ where $j = j_1*2^{n-1}+...+j_n*2^0$ which is simply written as $j=j_1...j_n$ in the book (the notation is a bit untidy).

Oh I see, it's eleven, not the binary representation 11 (namely 3)! Maybe it's better to use 9 or 12 to avoid any confusion.

`pow_tensor_list_one`

looks a bit cumbersome:

lemma pow_tensor_list_one [simp]: assumes "xs = []" shows "(pr (Cons x xs) 1) = x" by (simp add: assms)

It could simply be:

lemma pow_tensor_length_1: fixes X:: "complex Matrix.mat" shows "(pr [X] 1) = X" by simp

@Hanna Lachnitt I made a new PR.

Thanks for your PR, there seems to be still some confusion left about the binary representation. If j is a natural number strictly smaller than 2^m then the binary representation in this setting has length m, i.e. $j=j_1j_2...j_m$ and not length n.

I put m instead of n for some reasons (I used a locale in the first versions and needed another variable for inductions) but I wonder now if m should not be renamed to n since you would usually use j and n.

`pow_tensor_list_one`

looks a bit cumbersome:

Thanks! I only used Cons because of our talk about when to use (Suc n) instead of (n+1) and this is not a lemma that is for people to look at it. I removed the type annotation (fixes X:: "complex Matrix.mat") however, since it was done nowhere else.

double post

`pow_tensor_list_one`

looks a bit cumbersome:Thanks! I only used Cons because of our talk about when to use (Suc n) instead of (n+1) and this is not a lemma that is for people to look at it. I removed the type annotation (fixes X:: "complex Matrix.mat") however, since it was done nowhere else.

Formal proofs is a tricky business. A rule has exceptions, but there is the spirit of the rule. Regarding canonical forms, sometimes they will help, in particular in involved proofs, but here the proof is trivial. So, here canonical forms only make the statement less legible.

I put m instead of n for some reasons (I used a locale in the first versions and needed another variable for inductions) but I wonder now if m should not be renamed to n since you would usually use j and n.

Yes, it would be better to use n for the number of qubits to be consistent across the library. To be consistent would help the readers and the maintainers.

Also, why use the variable k to denote a length when one can use l ?

On another issue, should j also be replaced by j_dec or jd? Otherwise it is a bit cumbersome if j appears inside of a matrix, e.g.

` (Matrix.mat 2 1 (λ(i,j). if i=0 then (1::complex)/sqrt(2) else (exp (complex_of_real (2*pi)*𝗂*(bin_frac (s-1) (t-1) n jd)))*1/sqrt(2)))" `

I am currently working towards replacing m by n and k with l if its used for a length

Last updated: Sep 25 2022 at 23:25 UTC