Uniqueness of binary expansions

Stream: new members

[Bhavik Mehta]

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]

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]

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]

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]

i.e. write a one-sided inverse

[Chris Hughes]

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]

Also, I would use finset nat not finset (fin n)

[YH]

Where is finset.sum defined?

[Chris Hughes]

algebra.big_operators

[YH]

Oh found it in data.finsupp

[Kevin Buzzard]

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

[YH]

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]

I think I'd be tempted to do this with num not nat

[Kevin Buzzard]

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

[YH]

What is num?

[Kevin Buzzard]

It's in core I think

[Kevin Buzzard]

It's nats but defined as binary sequences

[Kevin Buzzard]

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

[Chris Hughes]

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]

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]

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]

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]

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

[Bhavik Mehta]

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]

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]

This looks great, thanks!

[Chris Hughes]

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]

rcases lt_trichotomy i a with hia|rfl|hai,

By the way, I love this rfl trick!

[Kevin Buzzard]

rcases can lead to some pretty cool code :-) You can do similar things with rfl and rintro.

[Bhavik Mehta]

Yeah I'm just playing with that stuff... rcases/rintro with rfl is so much nicer than rcases/rintro and then tons of rws