Stream: quantum computing

Topic: binary representation


view this post on Zulip Anthony Bordg (Jul 15 2019 at 21:17):

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}"]

then in the bottom window I got

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

but Sledgehammer is unable to conclude. Am I missing something ?

view this post on Zulip Yijun He (Jul 15 2019 at 21:30):

I am not sure about that, but I have encountered similar situations.

view this post on Zulip 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.

view this post on Zulip Anthony Bordg (Jul 15 2019 at 21:45):

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

view this post on Zulip 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

view this post on Zulip 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=1n=m=1 and i=0i=0 then 1>01>0.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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 m0m\geq 0 for the integer mm in bin_rep n m whenever it was necessary.

view this post on Zulip Anthony Bordg (Jul 16 2019 at 21:39):

@Yijun He Your strategy for the proof was the right one.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Anthony Bordg (Jul 29 2019 at 14:27):

Now, thanks to @Hanna Lachnitt we have a satisfying Binary_Nat theory.

view this post on Zulip Anthony Bordg (Jul 29 2019 at 14:29):

Please change Deutsch_Jozsa.thy and Quantum_Fourier_Transform.thy accordingly.

view this post on Zulip Anthony Bordg (Jul 29 2019 at 14:38):

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 m0m\geq 0 for the integer mm in bin_rep n m whenever it was necessary.

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.


Last updated: Oct 01 2022 at 10:26 UTC