# Zulip Chat Archive

## Stream: new members

### Topic: Uniqueness of binary expansions

#### Bhavik Mehta (Dec 15 2019 at 18:58):

Any suggestions on how to prove this function is injective?

def binary (A : finset (fin n)) : ℕ := A.sum (λ x, pow 2 x.val)

#### Kevin Buzzard (Dec 15 2019 at 20:12):

My instinct would be to do the proofs with a function taking values in int not nat, because subtraction will be involved, and then deduce the nat version from the int version.

#### Kevin Buzzard (Dec 15 2019 at 20:14):

As for proving it, the 2-adic method would be to find the smallest index i where two different finsets differ and then show that the difference was not a multiple of 2^i and hence can't be zero. The real method would be to find the largest index where they differ and then show that the difference has to be positive and hence non-zero.

#### Kevin Buzzard (Dec 15 2019 at 20:15):

Maybe another idea would be to define binary expansions of a nat (which might be there already) and prove that i is in A iff the i'th digit is 1.

#### Kevin Buzzard (Dec 15 2019 at 20:16):

i.e. write a one-sided inverse

#### Chris Hughes (Dec 15 2019 at 20:16):

I don't think this will ever be a short proof. Probably there should be some theory of base-n expansions. You'll probably have to write the left inverse to this function and prove it's a left inverse.

#### Chris Hughes (Dec 15 2019 at 20:16):

Also, I would use `finset nat`

not `finset (fin n)`

#### YH (Dec 15 2019 at 20:27):

Where is `finset.sum`

defined?

#### Chris Hughes (Dec 15 2019 at 20:29):

`algebra.big_operators`

#### YH (Dec 15 2019 at 20:30):

Oh found it in `data.finsupp`

#### Kevin Buzzard (Dec 15 2019 at 20:34):

If you use finset nat you can prove an explicit equiv between that and nat

#### YH (Dec 15 2019 at 20:46):

I guess we can just write an inverse like

import data.finset data.finsupp open finset set def binary (A : finset ℕ) : ℕ := A.sum (λ x, pow 2 x) def binary_reverse : ℕ → finset ℕ | 0 := ∅ | (n+1) := let A := binary_reverse n in

$A ∪ {k} \backslash \{0,1,..., k-1\}$ where $k$ is the smallest natural number not in $ℕ$ (now I need to learn how to write this in Lean...)

#### Kevin Buzzard (Dec 15 2019 at 20:57):

I think I'd be tempted to do this with `num`

not nat

#### Kevin Buzzard (Dec 15 2019 at 20:58):

This work must have been done already in essence, when proving nat and num are the same

#### YH (Dec 15 2019 at 20:58):

What is `num`

?

#### Kevin Buzzard (Dec 15 2019 at 20:58):

It's in core I think

#### Kevin Buzzard (Dec 15 2019 at 20:59):

It's nats but defined as binary sequences

#### Kevin Buzzard (Dec 15 2019 at 21:00):

I'm on phone right now, but try importing data.num.basic of it exists, and then #check num and right click

#### Chris Hughes (Dec 15 2019 at 21:00):

Here's a start. There's a bunch of sorries, and I do have a habit of leaving false sorries.

import data.nat.modeq data.fin algebra.big_operators data.nat.parity variable {n : ℕ} open function nat finset def binary (A : finset ℕ) : ℕ := A.sum (λ x, pow 2 x) def ith_bit (n i : ℕ) := n / 2 ^ i % 2 lemma ith_bit_binary (A : finset ℕ) : ∀ i, i ∈ A ↔ ¬ even (binary A / 2 ^ i) := finset.induction_on A (by simp [binary, ith_bit]) (λ a s has ih i, begin dsimp [binary, ith_bit] at *, rw [sum_insert has, mem_insert, nat.add_div, if_neg], rcases lt_trichotomy i a with hia|rfl|hai, { have : even (2^a / 2^i), from sorry, simp [*, ne_of_lt hia, ih] with parity_simps }, { simp [nat.div_self (nat.pow_pos (show 2 > 0, from dec_trivial) _), nat.mod_self] with parity_simps, finish }, { have : 2^a / 2^i = 2^a, from sorry, simp [ne_of_gt hai, this, ih] with parity_simps, by_cases a = 0, simp * at *, sorry, simp * }, sorry, sorry, end)

#### YH (Dec 15 2019 at 21:03):

I'm on phone right now, but try importing data.num.basic of it exists, and then #check num and right click

I see. I think this problem is essentially the same as proving `nat`

and `num`

are the same?

#### Bhavik Mehta (Dec 15 2019 at 21:34):

Also, I would use

`finset nat`

not`finset (fin n)`

I usually would, but this is in the context of a lot of other stuff, where I need `finset (fin n)`

. I'd be happy to prove it for `finset nat`

instead and convert from that to this result

#### Bhavik Mehta (Dec 15 2019 at 21:36):

Here's a start. There's a bunch of sorries, and I do have a habit of leaving false sorries.

def ith_bit (n i : ℕ) := n / 2 ^ i % 2

There's `test_bit`

, by the way - perhaps that would be nicer

#### Chris Hughes (Dec 15 2019 at 21:51):

Almost certainly better. It shouldn't be too hard to prove given the lemmas in the file.

#### Bhavik Mehta (Dec 15 2019 at 23:27):

Here's a start. There's a bunch of sorries, and I do have a habit of leaving false sorries.

have : 2^a / 2^i = 2^a, from sorry,

I'm fairly sure this sorry is false - the only assumption on `i`

here is that `a < i`

, so `2^a / 2^i`

is zero

#### Mario Carneiro (Dec 15 2019 at 23:47):

I think the easiest way to prove this one is as follows: Suppose `binary A = binary B`

, and `A != B`

. Then there exists a largest `k`

where they differ; suppose that it is in `A`

. Then $\sum_{i\in A} 2^i\ge \sum_{i\in A,i>k} 2^i+2^k = \sum_{i\in B,i>k} 2^i+2^k >\sum_{i\in B,i>k} 2^i+\sum_{i=0}^{k-1}2^i\ge \sum_{i\in B,i>k} 2^i+\sum_{i\in B, i<k}2^i=\sum_{i\in B} 2^i$

#### Bhavik Mehta (Dec 15 2019 at 23:48):

This looks great, thanks!

#### Chris Hughes (Dec 16 2019 at 02:51):

Here's a start. There's a bunch of sorries, and I do have a habit of leaving false sorries.

have : 2^a / 2^i = 2^a, from sorry,I'm fairly sure this sorry is false - the only assumption on

`i`

here is that`a < i`

, so`2^a / 2^i`

is zero

Yes it's false, I got `mod`

and `div`

confused. It should be equal to zero, in which case the proof is a little easier.

#### Bhavik Mehta (Dec 17 2019 at 21:41):

rcases lt_trichotomy i a with hia|rfl|hai,

By the way, I love this `rfl`

trick!

#### Kevin Buzzard (Dec 17 2019 at 21:49):

`rcases`

can lead to some pretty cool code :-) You can do similar things with `rfl`

and `rintro`

.

#### Bhavik Mehta (Dec 17 2019 at 21:51):

Yeah I'm just playing with that stuff... `rcases/rintro`

with `rfl`

is so much nicer than `rcases/rintro`

and then tons of `rw`

s

Last updated: May 13 2021 at 05:21 UTC