binary representation · quantum computing

I decided to create a dedicated topic for Binary_Rep.thy to avoid to clutter Deutsch-Jozsa.
Strangely enough if I try

using sum_subtractf[of "(λi. of_nat (m mod 2^(n-i)))" "λi. of_nat (m mod 2^(n - Suc i))" "{..<n}"]

proof (prove)
using this:
  (∑x<n. of_nat (m mod 2 ^ (n - x)) - of_nat (m mod 2 ^ (n - Suc x))) =
  (∑x<n. of_nat (m mod 2 ^ (n - x))) - (∑x<n. of_nat (m mod 2 ^ (n - Suc x)))

goal (1 subgoal):
 1. (∑i<n. of_nat (m mod 2 ^ (n - i)) - of_nat (m mod 2 ^ (n - Suc i))) =
    (∑i<n. of_nat (m mod 2 ^ (n - i))) - (∑i<n. of_nat (m mod 2 ^ (n - Suc i)))

Yijun He (Jul 15 2019 at 21:30):

Yijun He (Jul 15 2019 at 21:33):

I solved them by adding a quantifier like ⋀n m to the lemma being used. But it seems unreasonable to modify the lemma sum_subtractf in this case.

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

I tried sledgehammer_params[verbose = true] and sledgehammer_params[debug = true], but it does not help.

Hanna Lachnitt (Jul 15 2019 at 22:02):

Could it be that it has something to do with f and g having to be of the right type?
f g :: "'b ⇒'a::ab_group_add"
I had such a problem before where this was the solution and it gave similar error messages

Anthony Bordg (Jul 15 2019 at 22:48):

@Hanna Lachnitt I previously tried sum_subtractf_nat (assuming the required assumption is satisfied). It has the advantage of using f g:: "`a => nat", but Sledgehammer timed out. Now, I increased the Sledgehammer Timeout option and tried it again and metis found a proof. The only problem is that the required assumption is not satisfied, take for instance

n=m=1

and

i=0

then

1>0

Anthony Bordg (Jul 16 2019 at 16:29):

@Yijun He In Basics.thy I substituted sum_of_index_diff for sum_diff and I also generalized the type involved from complex to comm_monoid_add. I made the corresponding change in MoreTensor.thy where sum_diff was used.

Anthony Bordg (Jul 16 2019 at 20:58):

The last proof in Binary_Nat.thy has been completed. So, hopefully we are done with this theory. I will just need to tidy up the proofs.

Anthony Bordg (Jul 16 2019 at 21:34):

@Hanna Lachnitt @Yijun He
Take-home message: if you have some trouble with the type system, try to "generalize" some of the types involved.
In this case the trouble came from the fact that one wants to simultaneously see a sum as a sum of natural numbers and as a sum of integers when one regroups the terms in the sum to notice that they cancel except for the first and last ones.
So, I simply substituted bin_rep:: "nat ⇒ int ⇒ int list" for bin_rep:: "nat ⇒ nat ⇒ nat list" and added the assumption

m\geq 0

for the integer

m

in bin_rep n m whenever it was necessary.

Anthony Bordg (Jul 16 2019 at 21:39):

Anthony Bordg (Jul 17 2019 at 19:09):

I agree with @Hanna Lachnitt, it's not completely satisfactory. bin_rep n m should really be a list of natural numbers. If someone succeeds in completing the last proof bin_rep_eq while having the type

bin_rep_eq:: "nat ⇒ nat ⇒ nat list"

, he should feel free to make a PR.
However, the use of integers here does not seem to cause any particular trouble later in Deutsch_Jozsa.thy.

Hanna Lachnitt (Jul 26 2019 at 14:59):

I finally had a proper look at it and found a proof for bin_rep_eq such that
bin_rep:: "nat => nat => nat list
Is it still needed? Maybe we can discuss it on Monday :) I would prefer it conceptually (since it is a list of natural numbers) and also it should make less work when used in other theories.

Anthony Bordg (Jul 26 2019 at 15:03):

Very nice. Yes, I think it will be useful to simplify a little bit the theories that rely on it.
We should discuss it next Monday and then make the changes accordingly.

Anthony Bordg (Jul 29 2019 at 14:27):

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

Please change Deutsch_Jozsa.thy and Quantum_Fourier_Transform.thy accordingly.

Anthony Bordg (Jul 29 2019 at 14:38):

For the record, remember that it might be useful to declare the [[show_types = true]] option, then one is able to see the types of the printed outputs in the bottom window.

Stream: quantum computing

Topic: binary representation

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