@Hanna Lachnitt I simplified `is_balanced`

. Indeed, one should be able to prove `is_balanced_inter`

and `is_balanced_union`

. It should not be necessary to embed these two lemmas in the definition `is_balanced`

.

Please see my PR.

@Hanna Lachnitt I replaced the name `deutsch_jozsa`

with `jozsa`

which is shorter :slight_smile: and I made all the changes accordingly.

I just completed the proof of the lemma `is_balanced_union`

(see PR).

@Hanna Lachnitt What is the purpose of `[case_names ge 1 step]`

in `ind_from_1`

? I'm not sure since if I remove it, the rest of the code still works.

If you use the induction rule it gives you a name for the cases, i.e.

proof (induction n rule: ind_from_1)

case ge

show ?case

next

case 1

...

This is good if the induction rule is very unusual and hard to understand. E.g. if you have strange base cases or something.

I didn't used it in the code as I found it sufficiently understandable without the case name and will probably remove it. I am just working on tidying up the code a bit, a lot of it is provisional as I tried out a lot today to find the best way of defining stuff.

It's nice that you renamed the cases thanks to `[case_names ge 1 step]`

. Otherwise `case 1`

, `case 2`

and `case (3 n)`

that one sees are not very telling.

@Hanna Lachnitt What were your motivations to change `const`

?

I wanted to add an assumption to the locale jozsa that ensures that each function is either constant or balanced. For this is_const and is_balanced have to be defined before the locale specification since assumptions cannot be added to locale afterwards. However, I am still not at a point where I need to use is_const or is_balanced at all so I kept that issue for later.

Ok, I see. The assumption in the locale `jozsa`

that `f`

is either constant or balanced is fine, and even needed, since in a Deutsch's problem Bob promises Alice that he will use a fonction that is either constant or balanced.

But, given how `const`

is defined (with a parameter `n`

for the domain of `f`

) this definition and also `is_balanced`

should be in a dedicated locale with `jozsa`

as a sublocale.

I will do it.

Do you agree ?

Yes I had that thought too. I think I even wrote it in a commentary or something so I think it's a good idea

PR submitted.

Does someone have an idea how a matrix representation of the result of taking n times the tensor product of H would look like?

@Hanna Lachnitt I assume that you want the matrix representation of $H^{\otimes n}$ wrt the computational basis. For $i,j\leq 2^n$, it's given by

$H^{\otimes n}(i,j) = \frac{1}{\sqrt{2^n}} (-1)^{j.i},$

where $j.i$ denotes the **bitwise** inner product of $|j\rangle$ and $|i\rangle$.

Thanks a lot :)

@Hanna Lachnitt Two additional remarks. First, the inner product `inner_prod`

is defined in `Quantum.thy`

and denoted $\langle i|j\rangle$. Second, $|i\rangle$ (the ith element of the computational basis ) is just `unit_vec 2^n i`

.

@Hanna Lachnitt It makes sense to introduce the abbreviation $i.j$ for $\langle {\text unit\_vec}\;2^n\;i|{\text unit\_vec}\;2^n\;j\rangle$ if you plan to use it heavily.

@Hanna Lachnitt I plan to work on your theory. What is the next thing I should tackle ?

I am still trying to understand the matrix representation of $H^{\otimes n}$. I would be happy if you could explain it to me again. $\langle unit\_vec ~2^n~ i| unit\_vec~ 2^n~ j \rangle$ is 1 if i=j and 0 otw. right? But e.g. for n=1, i.e. just the usual Hadamard gate the element at position i=0 and j=0 should be positive not negative. I found a solution for which I convert decimals into binaries which is not a nice thing to express the gate with.

Besides that I was sometimes unsure about design choices, I made comments in the code in that case. I finished everything up to the last application of the $H^{\oplus n}$ gate (and of course the measurement following after that). I might need to restructure some things though depending on this last bit (regarding the $n\ge 1$ issue outside of the locale).

I am still trying to understand the matrix representation of $H^{\otimes n}$. I would be happy if you could explain it to me again. $\langle unit\_vec ~2^n~ i| unit\_vec~ 2^n~ j \rangle$ is 1 if i=j and 0 otw. right?

correct

But e.g. for n=1, i.e. just the usual Hadamard gate the element at position i=0 and j=0 should be positive not negative.

The formula is correct, but $j.i$ is the bitwise inner product of $|i\rangle$ and $|j\rangle$.

So, it's not the `inner_prod`

in `Quantum.thy`

. I will edit my previous post.

For instance, the bitwise inner product of $|00\rangle$ with itself is $0$, not $1$.

Then, I guess this is what I have done so far :( Convert i and j into binary numbers, pad them with 0's (depending on the way you define them) and multiply them bitwise. This makes everything very hard to prove. I really hoped that there was a better way.

Given $0 \leq i<2^n$, we need its binary representation, then we will be able to define the bitwise inner product of any two unit vectors of dimension $2^n$.

@Hanna Lachnitt Does it seem reasonable ? After that , everything should be easy to prove. I will write a theory `Binary_Nat.thy`

and push it into my master branch for you to use it. Is it ok ?

@Anthony Bordg I already did that but in a rather specific way. It would probably be good to have it more general so I would be glad if you could do that.

@Anthony Bordg did you already start? My approach seems to be rather inefficient, the proof that $H^{\oplus n}$ equals this new representation takes forever and is rather ugly. I basically just converted the decimals with the usual method (divide and mod by 2). The output is a nat list containing 0's and 1's. Then, I wrote another function, taking two of these lists and add 1 to the result if both lists have a 1 at the same entry. Is there a better way?

Anthony Bordg did you already start?

Yes, I started but it's not ready yet. :working_on_it:

`Binary_Nat.thy`

(see my master branch) is almost completely done, but one `sorry`

remains inside the last proof (the proof of `bin_rep_eq`

). The step is quite obvious, since the terms in the sum cancel except the first and the last ones, but I have a hard time making it clear to Isabelle. To help I think one needs to use `of_nat`

, but even so the proof remains problematic.

Do you have any suggestion to help Isabelle ?

Is there a way to separate the sum `\<Sum>i<n. m mod 2^(n-i) - m mod 2^(n-1-i)`

into the difference of two sums?

We will then obtain `\<Sum>i<n. m mod 2^(n-i) - \<Sum>i<n. m mod 2^(n-1-i)`

. Then we can take out the first and last terms, giving `\<Sum>i\<in>{1..<n}. m mod 2^(n-i) - \<Sum>i\<in>{0..<n-1}. m mod 2^(n-1-i)`

. These two sums should cancel out by a lemma `sum_diff`

.

I will try it.

Also the `sum_diff`

is the lemma in `Basics.thy`

, and importing the theory will cause some proofs in `Binary_Nat.thy`

to fail, but they can easily be fixed.

@Yijun He By the way I realize that `sum_diff`

it's a misnomer , it should be called something like `sum_of_index_diff`

. I will fix the name.

@Yijun He The relevant lemma is `sum_subtractf`

in `Groups_Big.thy`

.

But now the definition for the bitwise inner product I build upon bin_rep and all proofs built on that are not working anymore. Is there no other solution? It is a nat list after all. Adding $m \ge 0$ does not instantly help but I will try to adapt the proofs in another way to the new def of bin_rep :)

@Hanna Lachnitt Ok, I will try to help.

Thanks, I am already halfway through. I just did a new commit, maybe I should have defined bitwise_inner_product or Hn differently (I had that nat first in Hn and not in bitwise_inner_product)?

I finished except for one small lemma :)

@Hanna Lachnitt I'm currently having a look at it. The first thing which is not very clear for me is the order of the three arguments. The natural order is `bitwise_inner_product n i j`

, but with your notation it seems that the order is `bitwise_inner_product i n j`

. Is it correct ?

Yes please also see the comment I left about that. If we want to use the notation $i ⋅_n j$ the order of the argument is fixed as i n j otherwise it can easily be changed to i n j.

Since its not possible to write $i⋅_{n+1} j$, maybe this should be discarded after all anyway

Ok, after the lunch I will make a few changes. In the meantime please continue with your proofs.

I pushed the measurement outline

Thanks Hanna. I will have a look as soon as possible, but first I need to work a little bit more on the quantum Fourier transform.

I finished the Deutsch-Jozsa algorithm :tada: Except from that (optional?) proof we talked about earlier everything is done. But I still need to tidy everything up a bit.

Congrats! :tada:

Is all the type-information in `is_balanced`

needed ?

It was but actually it might not be needed anymore (or at least not that many type annotations)

Is not `ind_from_1`

a particular case of `nat_induct_at_least`

?

It might be useful though.

I would say that `Uf_mult_without_empty_summands_sum_even`

is easier to read than `Uf_mult_without_empty_summands_sum_even'`

.

I removed the braces since there are not needed.

I will change `Uf_mult_without_empty_summands_sum_even`

accordingly after you finish looking over the file

Is not

`ind_from_1`

a particular case of`nat_induct_at_least`

?

I didn't noticed that. I looked it up in the internet and there it was suggested to write a customary induction rule. It might be better to use the existing one, i.e. `nat_induct_at_least`

For `bin_rep_geq_0`

note that there is a very simple proof, namely `using assms by simp`

. Actually, this lemma is probably not even necessary.

From ` H_tensor_n_is_tensor_of_H`

one can factor out a lemma, namely `H^⇩⊗ 1 = H`

.

In `sum_every_odd_summand_is_zero`

, `A`

is an odd choice of notation for a function.

Sry I was thinking about matrix entries and A is often used to denote an arbitrary matrix. But with the degree of generality the lemma has in its final version (not much to do with matrices anymore) it is better to replace it with another notation.

For

`bin_rep_geq_0`

note that there is a very simple proof, namely`using assms by simp`

. Actually, this lemma is probably not even necessary.

Same might be the case for H_values_right_bottom and H_values

Is not

`ind_from_1`

a particular case of`nat_induct_at_least`

?I didn't noticed that. I looked it up in the internet and there it was suggested to write a customary induction rule. It might be better to use the existing one, i.e.

`nat_induct_at_least`

All the proofs using `ind_from_1`

have been rewritten with `nat_induct_at_least`

.

To help the reader or maintainer, if there are multiple assumptions then one should specify the exact subset of assumptions needed to prove a given fact. For instance, to prove the first fact in the proof of `U⇩f_mult_without_empty_summands_even`

, one should use `assms(1,2,4)`

instead of `assms`

.

In an intricate formalization one should use `show ?thesis`

whenever possible to declutter the code.

The proof `U⇩f_mult_without_empty_summands_sum_odd`

has been rewritten in the same style than `U⇩f_mult_without_empty_summands_sum_even`

.

A simpler name for `index_tensor_mat_vec2_i_smaller_row_B`

would be indeed welcome.

What about `index_tensor_mat_with_vec2`

?

From the formula it's already clear that $i < \text{dim\_row}\,B$, so one does not need to "embed" this condition into the name.

Ok, I see that a confusion would be possible with `index_tensor_mat_vec2_i_greater_row_B`

which also needs a new name.

@Hanna Lachnitt

I was thinking about that too (thats why I suggested that name in the comment), but there is also a lemma called `index_tensor_mat_vec2_i_greater_row_B`

, if you rename `index_tensor_mat_vec2_i_smaller_row_B`

to `index_tensor_mat_with_vec2`

how would you name that lemma?

Maybe we could put them together to one lemma with two goals and then name it `index_tensor_mat_with_vec2`

?

Since thematically they are closely related.

Yes maybe we could put them together to one lemma with two goals and then name it

`index_tensor_mat_with_vec2`

?

It's a possible solution.

I hesitate between `index_tensor_mat_with_vec2`

and `index_tensor_mat_with_vec2_row_cond`

. The name matters only to us, since these two lemmas are too ad hoc to be useful for someone else.

But in any case, it's worth emphasizing that `i`

and `B`

should not be into the name, since i and B are completely arbitrary, they are mere notations, one could choose `k`

and `C`

or whatever.

Since the two lemmas don't share the same assumptions, it's not easy to merge them into a single lemma.

I can simply use `index_tensor_mat_with_vec2_row_cond`

and `index_tensor_mat_with_vec2_row_cond_bis`

which are not great but not bad either.

What is the problem with:

lemma index_tensor_mat_vec2: fixes A B:: "complex Matrix.mat" and i:: "nat" assumes "i < (dim_row A) * (dim_row B)" and "0 < (dim_col A) * (dim_col B)" and "dim_row A = 2" and "dim_col A = 1" shows "i < dim_row B ⟶ (A ⨂ B) $$ (i, 0) = (A $$ (0, 0)) * (B $$ (i,0))" and "i ≥ dim_row B ⟶ (A ⨂ B) $$ (i, 0) = (A $$ (1, 0)) * (B $$ ( i -dim_row B,0))" proof- show "i < dim_row B ⟶ (A ⨂ B) $$ (i, 0) = (A $$ (0, 0)) * (B $$ (i,0))" using index_tensor_mat assms by auto next show "i ≥ dim_row B ⟶ (A ⨂ B) $$ (i, 0) = (A $$ (1, 0)) * (B $$ ( i -dim_row B,0))" proof assume a0: "i ≥ dim_row B" have "(A ⨂ B) $$ (i,0) = A $$ (i div (dim_row B), 0) * B $$ (i mod (dim_row B),0)" using assms index_tensor_mat[of A "dim_row A" "dim_col A" B "dim_row B" "dim_col B" i 0] by auto moreover have "i div (dim_row B) = 1" using assms a0 by simp then have "i mod (dim_row B) = i - (dim_row B)" by (simp add: modulo_nat_def) ultimately show "(A ⨂ B) $$ (i, 0) = (A $$ (1, 0)) * (B $$ ( i -dim_row B,0))" by (simp add: ‹i div dim_row B = 1›) qed qed

that the assumptions in the first case became stronger?

Since the first lemma is not needed it could also be deleted (although it feels nicer/more complete to have both cases) and the second could get the short name

Since the first lemma is not needed it could also be deleted (although it feels nicer/more complete to have both cases) and the second could get the short name

Do you mean the first lemma is not used ? If so, it should be deleted.

One should write `assms(1) assms(2) assms(4)`

for instance as `assms(1,2,4)`

for conciseness.

No since its proof is very easy it is not.

The abbreviations `zero`

, `one`

and the lemmas `ket_zero_is_state`

, `ket_one_is_state`

are duplicates of those in `Deutsch.thy`

. Idem with `H_on_ket_zero_is_state`

.

The lemma `ψ⇩1⇩0_values`

does not need the third assumption.

The theory does not import Deutsch.thy

The theory does not import Deutsch.thy

It does now :slight_smile:

Of course it could though. Should Grover do it too?

I feel for Deutsch and Deutsch-Jozsa it is more reasonable than for Grover

Sry for typos I am on my phone

But in any case, it's worth emphasizing that

`i`

and`B`

should not be into the name, since i and B are completely arbitrary, they are mere notations, one could choose`k`

and`C`

or whatever.

Same problem with `ψ⇩1⇩0_tensor_n`

for instance. I will simply name it `ψ⇩1⇩0_tensor`

.

The lemma `bin_rep_geq_0`

is not required.

There is a lot of places where the assumption $n\geq 1$ is not needed.

The lemma `bin_rep_index_0`

has been generalised.

A lot of parentheses can be removed to declutter the code.

In the lemma `bitwise_inner_prod_fst_el_0`

only the first assumption is required. In the same way, the third assumption in `bitwise_inner_prod_fst_el_is_1`

is not necessary.

The lemma `i_div_value_1`

is not used anywhere, I removed it.

When the same fact is proven twice for two different variables that play symmetric roles, then one can merge them into a single fact.

For instance, in `bitwise_inner_prod_fst_el_is_1`

one can replace

moreover have "k∈{0..n} ⟶ bin_rep (Suc n) i ! (k+1) = bin_rep n (i mod 2^n) ! k" for k using bin_rep_def by(metis Suc_eq_plus1 bin_rep_aux.simps(2) bin_rep_aux_neq_nil butlast.simps(2) nth_Cons_Suc) moreover have "k∈{0..n} ⟶ bin_rep (Suc n) j ! (k+1) = bin_rep n (j mod 2^n) ! k" for k using bin_rep_def by(metis Suc_eq_plus1 bin_rep_aux.simps(2) bin_rep_aux_neq_nil butlast.simps(2) nth_Cons_Suc)

with

moreover have "k∈{0..n} ⟶ bin_rep (Suc n) i ! (k+1) = bin_rep n (i mod 2^n) ! k ∧ bin_rep (Suc n) j ! (k+1) = bin_rep n (j mod 2^n) ! k" for k using bin_rep_def by(metis Suc_eq_plus1 bin_rep_aux.simps(2) bin_rep_aux_neq_nil butlast.simps(2) nth_Cons_Suc)

The declarations `declare [[show_types]]`

may be useful in the process of formalization, but they should be removed before submitting a PR.

The declarations

`declare [[show_types]]`

may be useful in the process of formalization, but they should be removed before submitting a PR.

Please see my message about that.

Note that when `i`

has type `nat`

, then the assumption `i ≥ 0`

is useless.

`for k`

being part of a statement, it should be on the same line with the statement itself.

Regarding your comment about renaming the lemma `sqrt_2_to_n_times_sqrt_2_n_plus_one`

, this lemma is really ad hoc, so the name does not matter and it won't be used outside the theory. So, what about `aux_comp`

(which stands for *auxiliary computation*) ?

Would be already much better than the current name. But aux_comp could mean anything. Maybe sqrt_2_aux_comp or something that has sqrt in its name?

Would be already much better than the current name. But aux_comp could mean anything. Maybe sqrt_2_aux_comp or something that has sqrt in its name?

Ok, `aux_comp_with_sqrt2`

sounds good.

Given the fact that it's a trivial result, it does not deserve a structured proof.

So, I have replaced

lemma sqrt_2_to_n_times_sqrt_2_n_plus_one [simp]: shows "2^n/(sqrt(2)^n * sqrt(2)^(n+1)) = 1/sqrt 2" proof(induction n) show "2^0/(sqrt(2)^0 * sqrt(2)^(0+1)) = 1/sqrt 2" by simp next fix n assume IH: "2^n/(sqrt(2)^n * sqrt(2)^(n+1)) = 1/sqrt 2" have "sqrt 2 ^ Suc n * sqrt 2 ^ (Suc n + 1) = sqrt(2)^n * sqrt(2)^(n+1) * sqrt(2)^2" by simp then have "2^Suc n /(sqrt 2 ^ Suc n * sqrt 2 ^ (Suc n + 1)) = (2 ^ n * 2) /(sqrt(2)^n * sqrt(2)^(n+1) * sqrt(2)^2)" by (metis power_Suc semiring_normalization_rules(7)) then show "2 ^ Suc n /(sqrt 2 ^ Suc n * sqrt 2 ^ (Suc n + 1)) = 1/sqrt 2" using IH by auto qed

with

lemma aux_comp_with_sqrt2: shows "(sqrt 2)^n * (sqrt 2)^n = 2^n" by (smt power_mult_distrib real_sqrt_mult_self) lemma aux_comp_with_sqrt2_bis [simp]: shows "2^n/(sqrt(2)^n * sqrt(2)^(n+1)) = 1/sqrt 2" using aux_comp_with_sqrt2 by (simp add: mult.left_commute)

Note that smt proofs are fine, see Gerwin's answer.

One can read

lemma sum_n_summands_one_or_minus: fixes F:: "nat ⇒ nat" (*I renamed this because f suggested that it was jozsa's f function but it might also be f(k)+1*) and A::"nat set" assumes "finite A" shows "(∑ k ∈ A. (-1)^(F(k))) ≤ card A " and "(∑ k ∈ A. (-1)^(F(k))) ≥ -card A "

, but it's better to stick to mathematical practice and choose `g`

instead if `f`

is not available for the reason you mentioned. Usually, capitals are not used for functions.

@Hanna Lachnitt

Note that smt proofs are fine, see Gerwin's answer.

Good to know that it changed. There might be other proofs with can be shortened by smt I replaced some of the smts with structured proofs because of the entry in the style guide about it.

but it's better to stick to mathematical practice and choose g instead if f is not available for the reason you mentioned.

Usually, capitals are not used for functions.

Great thanks that fully answers my question. I think I choose F to resemble f(k) (since the function is only used for f(k) and f(k)+1)

In the same spirit, I have replaced

lemma sum_n_summands_one_or_minus: fixes g:: "nat ⇒ nat" and A:: "nat set" assumes "finite A" shows "(∑k∈A. (-1)^(g k)) ≤ card A" and "(∑k∈A. (-1)^(g k)) ≥ -card A" proof- have f0: "k ∈ A⟶ (-(1::int))^(g(k)) = 1 ∨ (-(1::int))^(g(k)) = -1" for k::nat by (metis neg_one_even_power neg_one_odd_power) (*This was proposed by sledgehammer(with different variables) I added it to avoid smt. Should it stay? If yes it might be possible to replace second smt*) obtain G :: "int ⇒ (nat ⇒ int) ⇒ nat set ⇒ nat" where "∀A F i. sum F A ≤ int (card A) * i ∨ ¬ F (G i F A) ≤ i ∧ G i F A ∈ A" by (meson sum_bounded_above) then show "(∑ k::nat ∈ A. (-1)^(F(k))) ≤ card A " using f0 by (metis (no_types) mult.right_neutral negative_zle of_nat_1 order_refl) next have "k ∈ A⟶ (-(1::nat))^(F(k)) = 1 ∨ (-(1::nat))^(F(k)) = -1" for k by (metis int_ops(2) neg_one_even_power neg_one_odd_power) then show "(∑ k ∈ A. (-1)^(F(k))) ≥ -card A " using assms by (smt card_eq_sum of_nat_1 of_nat_sum sum_mono sum_negf) qed

with

lemma aux_ineq_with_card: fixes g:: "nat ⇒ nat" and A:: "nat set" assumes "finite A" shows "(∑k∈A. (-1)^(g k)) ≤ card A" and "(∑k∈A. (-1)^(g k)) ≥ -card A" apply (smt assms neg_one_even_power neg_one_odd_power card_eq_sum of_nat_1 of_nat_sum sum_mono) apply (smt assms neg_one_even_power neg_one_odd_power card_eq_sum of_nat_1 of_nat_sum sum_mono sum_negf).

Note the change in the name. One does not need to find a clever name. Indeed, since these proofs are somewhat handled automatically, nobody will use it in another formalization, they will just run Sledgehammer instead.

`const_has_max_value`

was renamed `aux_comp_with_cmod`

.

`cmod_smaller_n`

was renamed `cmod_less`

. The former name had the problem already pointed out about arbitrary notations that should not find their way into names. Also, note that there are well established conventions in Isabelle/HOL, in particular *less* in names is common for a statement involving `<`

.

The following example in `Deutsch-Jozsa.thy`

is a good case study:

lemma sum_divide_distrib_cmod: fixes n:: nat and g:: "nat ⇒ int" and a:: real shows "(cmod(complex_of_real(∑k<n. g k / a)))⇧2 = (cmod (∑k<n. g k) / a)⇧2" proof- have "(complex_of_real(∑k::nat<n. (g k) / a)) = (∑k::nat<n. (g k) / a)" by blast then have "(cmod(complex_of_real(∑k::nat<n. (g k) / a)))⇧2 = (cmod((∑k::nat<n. (g k) / a)))⇧2" by blast moreover have "(∑k::nat<n. (g k) / a) = (∑k::nat<n. (g k))/ a" by (simp add: sum_divide_distrib) ultimately show "(cmod(complex_of_real(∑k::nat<n. (g k) / a)))⇧2 = (cmod (∑k::nat<n. (g k)) / a)⇧2" by (metis norm_of_real of_real_of_int_eq power2_abs power_divide) qed

Actually, if one runs Sledgehammer, then it finds a proof, namely

by (metis cmod_square_real of_int_sum of_real_of_int_eq power_divide sum_divide_distrib)

which is perfectly fine, since the result being trivial one does not want a structured proof in that case. Also, since the proof is handled automatically, there is no need for a clever name, instead of reusing this lemma in the future people will prove it again (automatically, for free). Hence, one does not run out of clever names and avoid a headache with the choice of the name.

It simply becomes

lemma aux_comp_sum_divide_cmod: fixes n:: nat and g:: "nat ⇒ int" and a:: real shows "(cmod(complex_of_real(∑k<n. g k / a)))⇧2 = (cmod (∑k<n. g k) / a)⇧2" by (metis cmod_square_real of_int_sum of_real_of_int_eq power_divide sum_divide_distrib)

and the prefix *aux_comp* is a way to signal the thoughts above.

@Hanna Lachnitt

`add_limits_max_value`

is useless, one can simply run `by simp`

instead where this lemma is used.

For a reason already explained the name `prob_first_n_qubits_0`

is not satisfying. What about `prob_fst_qubits_0`

?

But is in general reasonable to use such a definition?

Why does the prefix `meas`

appear in `meas_fst_n_qubits_zero_remaining_indices`

while there is no measure in the statement of this lemma ?

Something like `indices_with_fst_qubits_0`

might be better.

But is in general reasonable to use such a definition?

I'm going to investigate this question.

`indices_with_fst_qubits_0`

is fine. The meas appears since the lemma shows what the remaining indices are in the case that the first n qubits are measured and are all 0.

*tensor_n* appears a lot in names, for instance in `hadamard_gate_tensor_n_times_ψ⇩2_is_ψ⇩3`

, with the usual problem.

*iter_tensor* is a good alternative (iter stands for iterated), for instance it gives `hadamard_gate_iter_tensor_times_ψ⇩2_is_ψ⇩3`

, or even better in that case `iter_tensor_of_H_times_ψ⇩2_is_ψ⇩3`

.

H is fine here, since given the context it's meaningful in itself and there is absolutely no ambiguity that it stands for the Hadamard gate.

But is in general reasonable to use such a definition?

I'm going to investigate this question.

In the second comment below `text ‹Measurement›`

it's written that `prob_fst_qubits_0 n v`

is equal to

∏i∈{0..n} . prob0 (n+1) v i)

(assuming that v is a state of an n+1-qubits system). But, actually it's equal to

something more complicated involving `post_meas0`

. It's certainly the origin of the trouble.

Also, one should prove it for any state v, not only for jozsa_algo, since the proof will be more general and actually simpler.

Otherwise, this approach is perfectly reasonable.

@Hanna Lachnitt

Great there might be a generalized version in the comment below. It could solve the issue but actually I think I considered that and increased n in the counterpart as well :/ It might be just a remnant of a proof attempt in the comment.

`not_const_cannot_have_max_value1`

was renamed `max_value_of_not_const_less`

.

Great there might be a generalized version in the comment below. It could solve the issue but actually I think I considered that and increased n in the counterpart as well :/ It might be just a remnant of a proof attempt in the comment.

I'm trying to complete the proof.

@Hanna Lachnitt

I simplified `prob_fst_qubits_0`

as well by removing the condition `state (n+1) v`

.

For a reason already explained the name

`prob_first_n_qubits_0`

is not satisfying. What about`prob_fst_qubits_0`

?

I did not realize until this evening that the notations introduced in `Deutsch-Jozsa`

are not coherent with the ones in `Quantum.thy`

. One should replace `prob_fst_qubits_0`

with `prob0_fst_qubits`

.

@Hanna Lachnitt

When you wrote `text ‹General lemmata needed for the probability proofs›`

, do you mean general lemmata to compute probabilities ?

@Hanna Lachnitt

Yes, they concern the probability that the first n qubits are 0.

I did not realize until this evening that the notations introduced in

`Deutsch-Jozsa`

are not coherent with the ones in`Quantum.thy`

. One should replace`prob_fst_qubits_0`

with`prob0_fst_qubits`

.

Hanna Lachnitt

Yes thats fine. I put the 0 in the name to match the notation in Quantum, but put it in the end because I didn't wanted it to sound as if its only about one qubit from the fst n ones. But it gets pretty clear from the name

It's picky but often after the command `using`

there is useless stuff that could be removed. It's confusing if one tries to read the proofs to understand them, since there is a lot of useless stuff.

One example:

have "k < 2^n⟶((1 div 2) ⋅⇘n⇙ k) = 0" for k::nat using bitwise_inner_prod_with_zero by simp

instead of

have "k < 2^n⟶((1 div 2) ⋅⇘n⇙ k) = 0" for k::nat using bin_rep_def bin_rep_aux_def bitwise_inner_prod_def bitwise_inner_prod_with_zero by simp

A second example:

moreover have "(cmod(jozsa_algo $$ (1,0)))⇧2 = (cmod (∑k<(2::nat)^n. (-1)^(f k+ 1 + ((1 div 2) ⋅⇘n⇙ k))/(sqrt(2)^n * sqrt(2)^(n+1))))⇧2" using ψ⇩3_dim by auto

instead of

moreover have "(cmod(jozsa_algo $$ (1,0)))⇧2 = (cmod (∑k<(2::nat)^n. (-1)^(f k+ 1 + ((1 div 2) ⋅⇘n⇙ k))/(sqrt(2)^n * sqrt(2)^(n+1))))⇧2" using jozsa_algo_result const_def assms ψ⇩3_values ψ⇩3_dim by auto

Please clean your proofs when you are done and get rid of useless definitions and lemmas after `using`

.

@Hanna Lachnitt

It's even more picky, but sometimes there is an irregular use of white spaces. For example, one finds `∑k < 2^n`

or `∑k<2^n`

or `∑ k < 2 ^ n`

.

If LaTeX is so pleasing to the eye, it's due in part to standardized spaces.

For example, I find

shows "∀A B. A∩B={}∧ A∪B=C⟶(∑k::nat ∈ C. g k) = (∑ k::nat ∈ A. g k) + (∑ k::nat ∈ B. g k)"

less pleasing than

shows "∀A B. A ∩ B = {} ∧ A ∪ B = C ⟶ (∑k∈C. g k) = (∑k∈A. g k) + (∑k∈B. g k)"

Another example:

and "jozsa_algo_eval = 0 ⟷ is_balanced "

there is no white space after the first quotation mark but there is one before the second.

Note that instead of writing `∀x∈{i::nat. i < 2^n}. g x = 0`

one can write `∀x< 2^n. g x = 0`

.

Regarding your comment about possibly generalizing the lemmas involving `f k`

and `f k + 1`

, we could indeed write one general lemma and see the current lemmas as two different instances, but I'm not sure it's worth the trouble.

@Hanna Lachnitt

I managed to prove the following lemma:

lemma prob0_fst_qubits_eq: (* To move in Measurement.thy *) fixes n:: nat shows "prob0_fst_qubits n v = (cmod(v $$ (0,0)))⇧2 + (cmod(v $$ (1,0)))⇧2" proof- have "prob0_fst_qubits n v = (∑j∈{k| k::nat. (k<2^(n+1)) ∧ (∀i∈{0..<n}. ¬ select_index (n+1) i k)}. (cmod(v $$ (j,0)))⇧2)" using prob0_fst_qubits_def by simp moreover have "… = (∑j∈{0,1}. (cmod(v $$ (j,0)))⇧2)" using prob0_fst_qubits_index by simp finally show ?thesis by simp qed

The prerequisites are as follow:

lemma select_index_div_2: (* To move in Measurement.thy *) fixes n i j::"nat" assumes "i < 2^(n+1)" and "j<n" shows "select_index n j (i div 2) = select_index (n+1) j i" proof- have "2^(n-Suc j) ≤ i div 2 mod 2^(n-j) ⟹ 2^(n-j) ≤ i mod 2^(n+1-j)" proof- define a::nat where a0:"a = i div 2 mod 2^(n-j)" assume "2^(n-Suc j) ≤ a" then have "2*a + i mod 2 ≥ 2^(n-(Suc j)+1)" by simp then have f0:"2*a + i mod 2 ≥ 2^(n-j)" by (metis Suc_diff_Suc Suc_eq_plus1 assms(2)) have "a < 2^(n-j)" using a0 by simp then have "2*a + i mod 2 < 2*2^(n-j)" by linarith then have "2*a + i mod 2 < 2^(n-j+1)" by simp then have f1:"2*a + i mod 2 < 2^(n+1-j)" by (metis Nat.add_diff_assoc2 Suc_leD Suc_leI assms(2)) have "i = 2*(a + 2^(n-j)*(i div 2 div 2^(n-j))) + i mod 2" using a0 by simp then have "i = 2*a + i mod 2 + 2^(n-j+1)*(i div 2 div 2^(n-j))" by simp then have "i = 2*a + i mod 2 + 2^(n+1-j)*(i div 2 div 2^(n-j))" by (metis Nat.add_diff_assoc2 Suc_leD Suc_leI assms(2)) then have "i mod 2^(n+1-j) = 2*a + i mod 2" using f1 by (metis mod_if mod_mult_self2) then show "2^(n-j) ≤ i mod 2^(n+1-j)" using f0 by simp qed moreover have "2^(n-j) ≤ i mod 2^(n+1-j) ⟹ 2^(n-Suc j) ≤ i div 2 mod 2^(n-j)" proof- define a::nat where a0:"a = i div 2 mod 2^(n-j)" assume a1:"2^(n-j) ≤ i mod 2^(n+1-j)" have f0:"2^(n-j) = 2^(n-Suc j+1)" by (metis Suc_diff_Suc Suc_eq_plus1 assms(2)) have "a < 2^(n-j)" using a0 by simp then have "2*a + i mod 2 < 2*2^(n-j)" by linarith then have "2*a + i mod 2 < 2^(n-j+1)" by simp then have f1:"2*a + i mod 2 < 2^(n+1-j)" by (metis Nat.add_diff_assoc2 Suc_leD Suc_leI assms(2)) have "i = 2*(a + 2^(n-j)*(i div 2 div 2^(n-j))) + i mod 2" using a0 by simp then have "i = 2*a + i mod 2 + 2^(n-j+1)*(i div 2 div 2^(n-j))" by simp then have "i = 2*a + i mod 2 + 2^(n+1-j)*(i div 2 div 2^(n-j))" by (metis Nat.add_diff_assoc2 Suc_leD Suc_leI assms(2)) then have "i mod 2^(n+1-j) = 2*a + i mod 2" using f1 by (metis mod_if mod_mult_self2) then have "2*a + i mod 2 ≥ 2^(n-j)" using a1 by simp then have "(2*a + i mod 2) div 2 ≥ (2^(n-j)) div 2" using div_le_mono by blast then show "2^(n-Suc j) ≤ a" by (simp add: f0) qed ultimately show ?thesis using select_index_def assms by auto qed lemma select_index_suc_even: (* To move in Measurement.thy *) fixes n k i:: nat assumes "k < 2^n" and "select_index n i k" shows "select_index (Suc n) i (2*k)" proof- have "select_index n i k = select_index n i (2*k div 2)" by simp moreover have "… = select_index (Suc n) i (2*k)" proof- have "i < n" using assms(2) select_index_def by (metis (no_types, hide_lams) Suc_eq_plus1 assms(1) calculation diff_diff_left diff_le_self diff_self_eq_0 div_by_1 le_0_eq le_eq_less_or_eq less_imp_diff_less mod_div_trivial mult.left_neutral mult_eq_0_iff mult_le_mono1 not_less plus_1_eq_Suc power_0 semiring_normalization_rules(7)) thus ?thesis using select_index_div_2 assms(1) select_index_def by(metis Suc_1 Suc_eq_plus1 Suc_mult_less_cancel1 power_Suc) qed ultimately show "select_index (Suc n) i (2*k)" using assms(2) by simp qed lemma select_index_suc_odd: fixes n k i:: nat assumes "k ≤ 2^n -1" and "select_index n i k" shows "select_index (Suc n) i (2*k+1)" proof- have "((2*k+1) mod 2^(Suc n - i) ≥ 2^(n - i)) = (((2*k+1) div 2) mod 2^(n - i) ≥ 2^(n-1-i))" proof- have "2*k+1 < 2^(n + 1)" using assms(1) by (smt Suc_1 Suc_eq_plus1 Suc_le_lessD Suc_le_mono add_Suc_right distrib_left_numeral le_add_diff_inverse mult_le_mono2 nat_mult_1_right one_le_numeral one_le_power plus_1_eq_Suc power_add power_one_right) moreover have "i < n" using assms(2) select_index_def by (metis (no_types, hide_lams) add_cancel_left_left add_diff_inverse_nat diff_le_self div_by_1 le_antisym less_le_trans less_one mod_div_trivial not_le power_0) ultimately show ?thesis using select_index_div_2[of "2*k+1" "n" i] select_index_def by (metis Nat.le_diff_conv2 Suc_eq_plus1 Suc_leI assms(2) diff_Suc_1 less_imp_le less_power_add_imp_div_less one_le_numeral one_le_power power_one_right) qed moreover have "… = (k mod 2^(n - i) ≥ 2^(n-1-i))" by simp ultimately show ?thesis proof- have "i ≤ Suc n -1" using assms(2) select_index_def by auto moreover have "2*k+1 ≤ 2^(Suc n)-1" using assms(1) by (smt Suc_diff_1 Suc_eq_plus1 add_diff_cancel_right' diff_Suc_diff_eq2 diff_diff_left diff_is_0_eq diff_mult_distrib2 le_add2 mult_2 mult_Suc_right plus_1_eq_Suc pos2 power_Suc zero_less_power) ultimately show ?thesis using select_index_def by (metis ‹(2 ^ (n - 1 - i) ≤ (2 * k + 1) div 2 mod 2 ^ (n - i)) = (2 ^ (n - 1 - i) ≤ k mod 2 ^ (n - i))› ‹(2 ^ (n - i) ≤ (2 * k + 1) mod 2 ^ (Suc n - i)) = (2 ^ (n - 1 - i) ≤ (2 * k + 1) div 2 mod 2 ^ (n - i))› assms(2) diff_Suc_1) qed qed lemma aux_range: fixes k:: nat assumes "k < 2^(Suc n + 1)" and "k ≥ 2" shows "k = 2 ∨ k = 3 ∨ (∃l. l≥2 ∧ l≤2^(n+1)-1 ∧ (k = 2*l ∨ k = 2*l + 1))" proof(rule disjCI) assume "¬ (k = 3 ∨ (∃l≥2. l ≤ 2^(n + 1) - 1 ∧ (k = 2 * l ∨ k = 2 * l + 1)))" have "k > 3 ⟶ (∃l≥2. l ≤ 2^(n + 1) - 1 ∧ (k = 2 * l ∨ k = 2 * l + 1))" proof assume asm:"k > 3" have "even k ∨ odd k" by simp then obtain l where "k = 2*l ∨ k = 2*l+1" by (meson evenE oddE) moreover have "l ≥ 2" using asm calculation by linarith moreover have "l ≤ 2^(n+1) - 1" using assms(1) by (metis Suc_diff_1 Suc_eq_plus1 calculation(1) dvd_triv_left even_Suc_div_two less_Suc_eq_le less_power_add_imp_div_less nonzero_mult_div_cancel_left pos2 power_one_right zero_less_power zero_neq_numeral) ultimately show "∃l≥2. l ≤ 2^(n + 1) - 1 ∧ (k = 2 * l ∨ k = 2 * l + 1)" by auto qed then have "k ≤ 2" using ‹¬ (k = 3 ∨ (∃l≥2. l ≤ 2 ^ (n + 1) - 1 ∧ (k = 2 * l ∨ k = 2 * l + 1)))› less_Suc_eq_le by auto thus "k = 2" using assms(2) by simp qed lemma select_index_with_1: (* To move in Measurement.thy *) fixes n:: nat assumes "n ≥ 1" shows "∀k. k < 2^(n+1) ⟶ k ≥ 2 ⟶ (∃i<n. select_index (n+1) i k)" using assms proof(rule nat_induct_at_least) show "∀k< 2^(1+1). 2 ≤ k ⟶ (∃i<1. select_index (1+1) i k)" proof- have "select_index 2 0 2 = True" using select_index_def by simp moreover have "select_index 2 0 3" using select_index_def by simp ultimately show ?thesis by (metis Suc_leI add_Suc_shift le_eq_less_or_eq mult_2 not_less one_add_one one_plus_numeral plus_1_eq_Suc power.simps(2) power_one_right semiring_norm(3) zero_less_one_class.zero_less_one) qed next show "⋀n. 1 ≤ n ⟹ ∀k < 2^(n+1). 2 ≤ k ⟶ (∃i<n. select_index (n+1) i k) ⟹ ∀k < 2^(Suc n + 1). 2 ≤ k ⟶ (∃i<Suc n. select_index (Suc n +1) i k)" proof- fix n:: nat assume asm:"n ≥ 1" and IH:"∀k < 2^(n+1). 2 ≤ k ⟶ (∃i<n. select_index (n+1) i k)" have "select_index (Suc n + 1) n 2" proof- have "select_index (Suc n) n 1" using select_index_def by(smt Suc_1 Suc_diff_Suc Suc_lessI add_diff_cancel_right' diff_Suc_1 diff_commute diff_zero le_eq_less_or_eq less_Suc_eq_le nat.simps(3) nat_power_eq_Suc_0_iff one_mod_two_eq_one plus_1_eq_Suc power_one_right zero_less_power) thus ?thesis using select_index_suc_even by (metis Suc_eq_plus1 less_numeral_extra(4) mult_2 not_less_less_Suc_eq one_add_one one_less_power zero_less_Suc) qed moreover have "select_index (Suc n + 1) n 3" proof- have "select_index (Suc n) n 1" using select_index_def by(smt Suc_1 Suc_diff_Suc Suc_lessI add_diff_cancel_right' diff_Suc_1 diff_commute diff_zero le_eq_less_or_eq less_Suc_eq_le nat.simps(3) nat_power_eq_Suc_0_iff one_mod_two_eq_one plus_1_eq_Suc power_one_right zero_less_power) thus ?thesis using select_index_suc_odd by (metis One_nat_def Suc_eq_plus1 mult_2 numeral_3_eq_3 select_index_def) qed moreover have "∃i<Suc n. select_index (Suc n +1) i (2*k)" if "k ≥ 2" and "k ≤ 2^(n + 1)-1" for k:: nat proof- obtain i where "i<n" and "select_index (n+1) i k" using IH by(metis One_nat_def Suc_diff_Suc ‹2 ≤ k› ‹k ≤ 2 ^ (n + 1) - 1› diff_zero le_imp_less_Suc pos2 zero_less_power) then have "select_index (Suc n +1) i (2*k)" using select_index_suc_even by (metis One_nat_def Suc_diff_Suc add.commute diff_zero le_imp_less_Suc plus_1_eq_Suc pos2 that(2) zero_less_power) thus ?thesis using ‹i < n› less_SucI by blast qed moreover have "∃i<Suc n. select_index (Suc n +1) i (2*k +1)" if "k ≥ 2" and "k ≤ 2^(n + 1)-1" for k:: nat proof- obtain i where "i<n" and "select_index (n+1) i k" using IH by(metis One_nat_def Suc_diff_Suc ‹2 ≤ k› ‹k ≤ 2 ^ (n + 1) - 1› diff_zero le_imp_less_Suc pos2 zero_less_power) then have "select_index (Suc n +1) i (2*k+1)" using select_index_suc_odd that(2) by simp thus ?thesis using ‹i < n› less_SucI by blast qed ultimately show "∀k< 2^(Suc n + 1). 2 ≤ k ⟶ (∃i<Suc n. select_index (Suc n +1) i k)" using aux_range by (metis lessI) qed qed

and

lemma prob0_fst_qubits_index: (* To move in Measurement.thy *) fixes n:: nat and v:: "complex Matrix.mat" shows "{k| k::nat. (k<2^(n+1)) ∧ (∀i∈{0..<n}. ¬ select_index (n+1) i k)} = {0,1}" proof(induct n) case 0 show "{k |k. k < 2^(0+1) ∧ (∀i∈{0..<0}. ¬ select_index (0+1) i k)} = {0,1}" by auto next case (Suc n) show "⋀n. {k |k. k < 2^(n+1) ∧ (∀i∈{0..<n}. ¬ select_index (n+1) i k)} = {0,1} ⟹ {k |k. k < 2^(Suc n + 1) ∧ (∀i∈{0..<Suc n}. ¬ select_index (Suc n + 1) i k)} = {0, 1}" proof- fix n assume IH: "{k |k. k < 2^(n+1) ∧ (∀i∈{0..<n}. ¬ select_index (n+1) i k)} = {0,1}" then have "{0,1} ⊆ {k |k. k < 2^(Suc n + 1) ∧ (∀i∈{0..<Suc n}. ¬ select_index (Suc n + 1) i k)}" proof- have "k < 2^(n+1) ⟶ k < 2^(Suc n + 1)" for k::nat by simp moreover have "(∀i∈{0..<n}. ¬ select_index (n+1) i 0) ∧ (∀i∈{0..<n}. ¬ select_index (n+1) i 1)" using IH by auto then have "(∀i∈{0..<n}. ¬ select_index (Suc n +1) i 0) ∧ (∀i∈{0..<n}. ¬ select_index (Suc n +1) i 1)" using select_index_suc_odd[of 0 "n+1"] Suc_eq_plus1 by (smt One_nat_def Suc_1 add_Suc_shift add_diff_cancel_right' atLeastLessThan_iff diff_diff_cancel le_eq_less_or_eq less_Suc_eq linorder_not_le mod_less nat_power_eq_Suc_0_iff select_index_def zero_less_power) moreover have "select_index (Suc n + 1) n 0 = False" using select_index_def by simp moreover have "select_index (Suc n + 1) n 1 = False" using select_index_def by simp ultimately show ?thesis by (smt One_nat_def Suc_1 Suc_eq_plus1 Suc_lessI atLeast0_lessThan_Suc empty_iff insertE mem_Collect_eq nat.simps(1) nat_power_eq_Suc_0_iff pos2 subsetI zero_less_power) qed moreover have "{k |k. k < 2^(Suc n + 1) ∧ (∀i∈{0..<Suc n}. ¬ select_index (Suc n + 1) i k)} ⊆ {0,1}" proof- have "∀k<2^(Suc n +1). k ≥ 2 ⟶ (∃i<Suc n. ¬ select_index (Suc n +1) i k = False)" using select_index_with_1[of "Suc n"] by (metis Suc_eq_plus1 add.commute le_add1) thus ?thesis by auto qed ultimately show "{k |k. k<2^(Suc n + 1) ∧ (∀i∈{0..<Suc n}. ¬ select_index (Suc n +1) i k)} = {0,1}" by auto qed qed

Now, one can introduce the following, more general, machinery:

(* Below in iter_post_meas0, the firt argument n corresponds to the number of qubits of the system , and the second argument m corresponds to the number of qubits that have been measured. *) primrec iter_post_meas0:: "nat ⇒ nat ⇒ complex Matrix.mat ⇒ complex Matrix.mat" where (* To move in Quantum.thy or better in a new file Measurement.thy *) "iter_post_meas0 n 0 v = v" | "iter_post_meas0 n (Suc m) v = post_meas0 n (iter_post_meas0 n m v) m" (* iter_prob0 outputs the probability that successive measurements of the first m qubits give m zeros. *) definition iter_prob0:: "nat ⇒ nat ⇒ complex Matrix.mat ⇒ real" where (* idem *) "iter_prob0 n m v = (∏i∈{k|k::nat. k ≤ m-1}. prob0 n (iter_post_meas0 n i v) i)"

But, it remains elusive to prove the following lemma:

lemma iter_prob0_eq: (* To do *) fixes n:: nat and v:: "complex Matrix.mat" assumes "n ≥ 1" shows "iter_prob0 (Suc n) n v = prob0_fst_qubits n v" sorry

@Hanna Lachnitt @Yijun He

I will try to prove it tomorrow :)

Note that instead of writing

`∀x∈{i::nat. i < 2^n}. g x = 0`

one can write`∀x< 2^n. g x = 0`

.

This also applies to iter_prob0, where $i\in \{k|k::nat. k\le m-1\}$ can be writen as $i\le m-1$ or $i < m$

Further clean-up would be possible, especially more comments, but for now it's enough.

It only remains to move a few things in different theories.

@Hanna Lachnitt Do you plan to use the bitwise inner product in another formalization ? If so, It should be moved to Quantum.thy.

If we want to do Simon's algorithm at some point (period finding) it would be useful. But right now I don't see any other application.

Maybe it will also be useful for the QFT ?

If you agree, I will move it in Quantum.thy.

I got rid of all the things related to measurements. They are now part of `Measurement.thy`

.

Maybe it will also be useful for the QFT ?

If you agree, I will move it in Quantum.thy.

I moved your contribution on the bitwise inner product and the associated lemmas in a dedicated subsection of `Quantum.thy`

.

Thanks could you add me as an author please?

Thanks could you add me as an author please?

It's already done. In front of the subsection on the bitwise inner product, which was imported from `Deutsch-Jozsa.thy`

to `Quantum.thy`

, I added immediately a comment with the authorship of this subsection.

Thanks a lot :)

Last updated: Dec 07 2023 at 16:21 UTC