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 ?

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

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.

I tried `sledgehammer_params[verbose = true]`

and `sledgehammer_params[debug = true]`

, but it does not help.

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

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

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

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.

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

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

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`

.

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.

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.

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

theory.

Please change `Deutsch_Jozsa.thy`

and `Quantum_Fourier_Transform.thy`

accordingly.

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.

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