Deutsch-Jozsa · quantum computing

@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.

Anthony Bordg (Jul 04 2019 at 11:53):

@Hanna Lachnitt I replaced the name deutsch_jozsa with jozsa which is shorter :slight_smile: and I made all the changes accordingly.

Anthony Bordg (Jul 05 2019 at 20:33):

Anthony Bordg (Jul 05 2019 at 21:37):

@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.

Hanna Lachnitt (Jul 05 2019 at 21:43):

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.

Anthony Bordg (Jul 05 2019 at 21:50):

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.

Anthony Bordg (Jul 09 2019 at 09:36):

Hanna Lachnitt (Jul 09 2019 at 09:40):

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.

Anthony Bordg (Jul 09 2019 at 09:54):

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.

Anthony Bordg (Jul 09 2019 at 09:58):

Hanna Lachnitt (Jul 09 2019 at 10:06):

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

Anthony Bordg (Jul 09 2019 at 10:35):

Hanna Lachnitt (Jul 10 2019 at 10:59):

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

Anthony Bordg (Jul 10 2019 at 17:16):

@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

where

j.i

denotes the bitwise inner product of

|j\rangle

and

|i\rangle

Hanna Lachnitt (Jul 10 2019 at 17:27):

Anthony Bordg (Jul 10 2019 at 18:03):

@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.

Anthony Bordg (Jul 10 2019 at 20:04):

@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.

Anthony Bordg (Jul 11 2019 at 08:42):

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

Hanna Lachnitt (Jul 11 2019 at 08:45):

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.

Hanna Lachnitt (Jul 11 2019 at 08:47):

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).

Anthony Bordg (Jul 11 2019 at 09:05):

The formula is correct, but

j.i

is the bitwise inner product of

|i\rangle

and

|j\rangle

Anthony Bordg (Jul 11 2019 at 09:27):

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

Hanna Lachnitt (Jul 11 2019 at 09:32):

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.

Anthony Bordg (Jul 11 2019 at 09:43):

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

Anthony Bordg (Jul 11 2019 at 10:25):

@Hanna Lachnitt Does it seem reasonable ? After that , everything should be easy to prove. I will write a theory Binary_Nat.thyand push it into my master branch for you to use it. Is it ok ?

Hanna Lachnitt (Jul 11 2019 at 10:30):

@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.

Hanna Lachnitt (Jul 11 2019 at 14:22):

@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 (Jul 11 2019 at 15:11):

Anthony Bordg (Jul 15 2019 at 11:36):

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 ?

Yijun He (Jul 15 2019 at 11:50):

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?

Yijun He (Jul 15 2019 at 11:54):

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.

Anthony Bordg (Jul 15 2019 at 12:09):

Yijun He (Jul 15 2019 at 12:11):

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.

Anthony Bordg (Jul 15 2019 at 21:01):

@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.

Anthony Bordg (Jul 15 2019 at 21:04):

Hanna Lachnitt (Jul 17 2019 at 09:08):

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 :)

Anthony Bordg (Jul 17 2019 at 10:05):

Hanna Lachnitt (Jul 17 2019 at 10:13):

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)?

Hanna Lachnitt (Jul 17 2019 at 11:00):

Anthony Bordg (Jul 17 2019 at 11:08):

@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 ?

Hanna Lachnitt (Jul 17 2019 at 11:16):

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.

Hanna Lachnitt (Jul 17 2019 at 11:19):

Since its not possible to write

i⋅_{n+1} j

, maybe this should be discarded after all anyway

Anthony Bordg (Jul 17 2019 at 11:20):

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

Hanna Lachnitt (Jul 22 2019 at 11:43):

Anthony Bordg (Jul 22 2019 at 14:22):

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.

Hanna Lachnitt (Jul 25 2019 at 09:48):

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.

Anthony Bordg (Jul 25 2019 at 09:50):

Anthony Bordg (Aug 02 2019 at 10:36):

Hanna Lachnitt (Aug 02 2019 at 10:40):

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

Anthony Bordg (Aug 02 2019 at 10:56):

Anthony Bordg (Aug 02 2019 at 11:18):

Anthony Bordg (Aug 02 2019 at 11:48):

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.

Hanna Lachnitt (Aug 02 2019 at 12:15):

I will change Uf_mult_without_empty_summands_sum_even accordingly after you finish looking over the file

Hanna Lachnitt (Aug 02 2019 at 12:16):

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

Anthony Bordg (Aug 02 2019 at 17:11):

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.

Anthony Bordg (Aug 02 2019 at 17:58):

From H_tensor_n_is_tensor_of_H one can factor out a lemma, namely H^⇩⊗ 1 = H.

Anthony Bordg (Aug 03 2019 at 10:26):

In sum_every_odd_summand_is_zero, A is an odd choice of notation for a function.

Hanna Lachnitt (Aug 03 2019 at 11:29):

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.

Hanna Lachnitt (Aug 03 2019 at 11:31):

Anthony Bordg (Aug 03 2019 at 11:34):

All the proofs using ind_from_1 have been rewritten with nat_induct_at_least.

Anthony Bordg (Aug 03 2019 at 14:20):

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.

Anthony Bordg (Aug 03 2019 at 14:28):

In an intricate formalization one should use show ?thesis whenever possible to declutter the code.

Anthony Bordg (Aug 03 2019 at 15:01):

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.

Anthony Bordg (Aug 03 2019 at 16:38):

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

Hanna Lachnitt (Aug 03 2019 at 16:44):

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?

Hanna Lachnitt (Aug 03 2019 at 16:45):

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

Hanna Lachnitt (Aug 03 2019 at 16:46):

Anthony Bordg (Aug 03 2019 at 16:54):

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.

Anthony Bordg (Aug 03 2019 at 16:58):

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.

Anthony Bordg (Aug 03 2019 at 17:06):

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

Anthony Bordg (Aug 03 2019 at 17:09):

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.

Hanna Lachnitt (Aug 03 2019 at 17:22):

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

Hanna Lachnitt (Aug 03 2019 at 17:27):

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

Anthony Bordg (Aug 03 2019 at 17:33):

Anthony Bordg (Aug 03 2019 at 17:35):

One should write assms(1) assms(2) assms(4) for instance as assms(1,2,4) for conciseness.

Hanna Lachnitt (Aug 03 2019 at 17:36):

Anthony Bordg (Aug 04 2019 at 09:57):

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.

Anthony Bordg (Aug 04 2019 at 10:01):

Hanna Lachnitt (Aug 04 2019 at 10:06):

Anthony Bordg (Aug 04 2019 at 10:08):

Hanna Lachnitt (Aug 04 2019 at 10:08):

Hanna Lachnitt (Aug 04 2019 at 10:09):

Anthony Bordg (Aug 04 2019 at 10:09):

Same problem with ψ⇩1⇩0_tensor_n for instance. I will simply name it ψ⇩1⇩0_tensor.

Anthony Bordg (Aug 04 2019 at 11:01):

Anthony Bordg (Aug 04 2019 at 11:07):

Anthony Bordg (Aug 04 2019 at 11:46):

Anthony Bordg (Aug 05 2019 at 10:52):

Anthony Bordg (Aug 05 2019 at 10:55):

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.

Anthony Bordg (Aug 05 2019 at 11:10):

Anthony Bordg (Aug 05 2019 at 11:50):

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)

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)

Anthony Bordg (Aug 05 2019 at 12:01):

The declarations declare [[show_types]] may be useful in the process of formalization, but they should be removed before submitting a PR.

Hanna Lachnitt (Aug 05 2019 at 12:05):

Anthony Bordg (Aug 05 2019 at 14:40):

Anthony Bordg (Aug 05 2019 at 16:03):

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

Anthony Bordg (Aug 06 2019 at 09:44):

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) ?

Hanna Lachnitt (Aug 06 2019 at 11:18):

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?

Anthony Bordg (Aug 06 2019 at 14:30):

Anthony Bordg (Aug 06 2019 at 14:57):

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

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)

Anthony Bordg (Aug 06 2019 at 15:02):

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

Hanna Lachnitt (Aug 06 2019 at 15:06):

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.

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

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)

Anthony Bordg (Aug 06 2019 at 15:32):

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

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.

Anthony Bordg (Aug 06 2019 at 15:55):

Anthony Bordg (Aug 06 2019 at 16:04):

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 <.

Anthony Bordg (Aug 06 2019 at 16:38):

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

 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

Anthony Bordg (Aug 06 2019 at 16:48):

add_limits_max_value is useless, one can simply run by simp instead where this lemma is used.

Anthony Bordg (Aug 08 2019 at 09:46):

For a reason already explained the name prob_first_n_qubits_0 is not satisfying. What about prob_fst_qubits_0 ?

Hanna Lachnitt (Aug 08 2019 at 09:53):

Anthony Bordg (Aug 08 2019 at 09:54):

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.

Anthony Bordg (Aug 08 2019 at 09:55):

Hanna Lachnitt (Aug 08 2019 at 10:20):

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.

Anthony Bordg (Aug 08 2019 at 10:32):

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.

Anthony Bordg (Aug 08 2019 at 14:39):

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

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

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.

Anthony Bordg (Aug 08 2019 at 15:54):

Anthony Bordg (Aug 08 2019 at 20:28):

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

I simplified prob_fst_qubits_0 as well by removing the condition state (n+1) v.

Anthony Bordg (Aug 13 2019 at 21:37):

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

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

When you wrote text ‹General lemmata needed for the probability proofs›, do you mean general lemmata to compute probabilities ?
@Hanna Lachnitt

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

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

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

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

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

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

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

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

Anthony Bordg (Aug 14 2019 at 14:27):

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)"

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

and "jozsa_algo_eval = 0 ⟷ is_balanced "

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

Anthony Bordg (Aug 14 2019 at 15:33):

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

Anthony Bordg (Aug 14 2019 at 18:33):

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.

Anthony Bordg (Aug 18 2019 at 17:05):

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

Anthony Bordg (Aug 18 2019 at 17:07):

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

Anthony Bordg (Aug 18 2019 at 17:08):

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

Anthony Bordg (Aug 18 2019 at 17:10):

(* 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)"

Anthony Bordg (Aug 18 2019 at 17:11):

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 (Aug 18 2019 at 21:36):

Hanna Lachnitt (Aug 19 2019 at 09:27):

This also applies to iter_prob0, where

i\in \{k|k::nat. k\le m-1\}

can be writen as

i\le m-1

i < m

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

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.

Anthony Bordg (Aug 20 2019 at 16:04):

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

Hanna Lachnitt (Aug 20 2019 at 16:07):

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.

Anthony Bordg (Aug 20 2019 at 16:21):

Maybe it will also be useful for the QFT ?
If you agree, I will move it in Quantum.thy.

Anthony Bordg (Aug 20 2019 at 17:14):

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

Anthony Bordg (Aug 20 2019 at 18:10):

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

Hanna Lachnitt (Aug 21 2019 at 14:52):

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

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.

Stream: quantum computing

Topic: Deutsch-Jozsa

Anthony Bordg (Jul 04 2019 at 11:23):