Zulip Chat Archive

Stream: new members

Topic: Uniqueness of binary expansions


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

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

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

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

view this post on Zulip Kevin Buzzard (Dec 15 2019 at 20:16):

i.e. write a one-sided inverse

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

view this post on Zulip Chris Hughes (Dec 15 2019 at 20:16):

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

view this post on Zulip YH (Dec 15 2019 at 20:27):

Where is finset.sum defined?

view this post on Zulip Chris Hughes (Dec 15 2019 at 20:29):

algebra.big_operators

view this post on Zulip YH (Dec 15 2019 at 20:30):

Oh found it in data.finsupp

view this post on Zulip Kevin Buzzard (Dec 15 2019 at 20:34):

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

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

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

view this post on Zulip Kevin Buzzard (Dec 15 2019 at 20:57):

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

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

view this post on Zulip YH (Dec 15 2019 at 20:58):

What is num?

view this post on Zulip Kevin Buzzard (Dec 15 2019 at 20:58):

It's in core I think

view this post on Zulip Kevin Buzzard (Dec 15 2019 at 20:59):

It's nats but defined as binary sequences

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

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

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

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

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

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

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

view this post on Zulip 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 iA2iiA,i>k2i+2k=iB,i>k2i+2k>iB,i>k2i+i=0k12iiB,i>k2i+iB,i<k2i=iB2i\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

view this post on Zulip Bhavik Mehta (Dec 15 2019 at 23:48):

This looks great, thanks!

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

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

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

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