@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 wrt the computational basis. For , it's given by
where denotes the bitwise inner product of and .
Thanks a lot :)
@Hanna Lachnitt Two additional remarks. First, the inner product inner_prod
is defined in Quantum.thy
and denoted . Second, (the ith element of the computational basis ) is just unit_vec 2^n i
.
@Hanna Lachnitt It makes sense to introduce the abbreviation for 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 . I would be happy if you could explain it to me again. 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 gate (and of course the measurement following after that). I might need to restructure some things though depending on this last bit (regarding the issue outside of the locale).
I am still trying to understand the matrix representation of . I would be happy if you could explain it to me again. 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 is the bitwise inner product of and .
So, it's not the inner_prod
in Quantum.thy
. I will edit my previous post.
For instance, the bitwise inner product of with itself is , not .
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 , we need its binary representation, then we will be able to define the bitwise inner product of any two unit vectors of dimension .
@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 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 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 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 , 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 ofnat_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, namelyusing 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 ofnat_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 , 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
andB
should not be into the name, since i and B are completely arbitrary, they are mere notations, one could choosek
andC
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 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 aboutprob_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 inQuantum.thy
. One should replaceprob_fst_qubits_0
withprob0_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 can be writen as or
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: Oct 13 2024 at 01:36 UTC