Vector from finset of indices

Stream: new members

[George Tillisch]

Hi, it's my first time posting but I often come here to read the discussions, so thanks to everyone who answers questions on here!

I'm having trouble defining the inverse of a function that sends binary words (which are defined in the same way as vectors in TPIL) to a set of nonzero indices. Here's a MWE:

import tactic

inductive bit : Type
| O : bit
| I  : bit

inductive binary_word : ℕ → Type
| nil {} : binary_word nat.zero
| cons {n : ℕ} (b : bit) (bw : binary_word n) : binary_word (nat.succ n)

namespace binary_word
open bit
local notation h :: t := cons h t

def indices (n : ℕ) : finset ℕ := finset.erase (finset.range (n + 1)) 0

def bw_to_nonzero_indices : Π {n : ℕ}, binary_word n → finset ℕ
| 0 nil       := ∅
| n (O :: tl) := bw_to_nonzero_indices tl
| n (I :: tl) := insert n (bw_to_nonzero_indices tl)

def nonzero_indices_to_bw : Π (n : ℕ), finset ℕ → binary_word n
| 0     s := nil
| (n+1) s :=
  if (n + 1) ∈ s then
    (I :: nonzero_indices_to_bw n s)
  else
    (O :: nonzero_indices_to_bw n s)

lemma bw_to_nonzero_indices_inv_nonzero_indices_to_bw (n : ℕ) (s : finset ℕ) (h : s ⊆ indices n) :
  bw_to_nonzero_indices (nonzero_indices_to_bw n s) = s :=
sorry

end binary_word

Does anyone have a suggestion for how I could define nonzero_indices_to_bw? The current definition doesn't really work for this proof.

[Alistair Tucker]

Hi! Normally someone here would made intelligent comment already but you must have slipped through the net. For what it's worth here are some of my (not quite so intelligent) thoughts...

First of all I'm not a big fan of your definition of indices. It's not particularly easy to work with. As evidence I provide these two proofs which would surely have been much more easier to do for simple inequalities.

lemma a {n : ℕ} {s : finset ℕ} : s ⊆ indices (n + 1) → s.erase (n + 1) ⊆ indices n :=
begin
  intros h i hi,
  dunfold indices at *,
  specialize h (finset.mem_of_mem_erase hi),
  rw finset.mem_erase at *,
  split,
  { exact h.1, },
  { rw finset.mem_range,
    refine lt_of_le_of_ne _ hi.1,
    { rw ← finset.mem_range_succ_iff,
      exact h.2, }, },
end

lemma b {n : ℕ} {s : finset ℕ} : s ⊆ indices (n + 1) → n + 1 ∉ s → s ⊆ indices n :=
begin
  intros h h' i hi,
  dunfold indices at *,
  specialize h hi,
  rw finset.mem_erase at *,
  split,
  { exact h.1, },
  { rw finset.mem_range,
    apply lt_of_le_of_ne,
    { rw ← finset.mem_range_succ_iff,
      exact h.2, },
    { intro h,
      rw h at hi,
      exact h' hi, } },
end

[Alistair Tucker]

Then since you ask specifically about nonzero_indices_to_bw, I would suggest the following slight change.

def nonzero_indices_to_bw : Π (n : ℕ), finset ℕ → binary_word n
| 0     s := nil
| (n+1) s :=
  if (n + 1) ∈ s then
    (I :: nonzero_indices_to_bw n (s.erase (n + 1)))
  else
    (O :: nonzero_indices_to_bw n s)

With that I have been able to prove your lemma by

lemma bw_to_nonzero_indices_inv_nonzero_indices_to_bw (n : ℕ) (s : finset ℕ) (h : s ⊆ indices n) :
  bw_to_nonzero_indices (nonzero_indices_to_bw n s) = s :=
begin
  revert s,
  induction n with n ih,
  { intros s h,
    change ∅ = s,
    symmetry,
    rwa ← finset.subset_empty, },
  { intros t h,
    dunfold nonzero_indices_to_bw,
    split_ifs with h',
    { specialize ih (t.erase (n + 1)) (a h),
      dunfold bw_to_nonzero_indices,
      conv_rhs { rw [← finset.insert_erase h', ← ih], }, },
    { exact ih t (b h h'), }, },
end

[Kevin Buzzard]

I think it would be a lot easier to just work with lists

[George Tillisch]

Thank you @Alistair Tucker , you've shown me some great new tactics there! I did have a go with a definition that used erase but I put an empty set in the base case and it didn't work.

I agree with you @Kevin Buzzard , this is definitely a bodge. I ended up with this definition because I was trying to prove the hamming bound, so I wanted to prove that there are $\binom{n}{m}$ binary words at a given distance from another binary word. I looked around but it seems that counting arguments aren't very easy to formalise. I found finset.card_powerset_len in mathlib so I thought a good strategy would be to translate the statement into one about sets. That's also the reason I defined indices as a set, so I can take (indices n).powerset and prove finset.image (λ v : BW n, bw_to_nonzero_indices v) finset.univ = (indices n).powerset. There is probably a more straightforward approach that doesn't involve finsets.

[Yakov Pechersky]

You can make it a statement about list.length

[Yakov Pechersky]

Or number of times you have to do list.update_nth