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

#### 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 rws

Last updated: May 13 2021 at 05:21 UTC