Zulip Chat Archive

Stream: mathlib4

Topic: Natural map from Fin n -> Bool to Fin(2^n)

Wrenna Robson (Jul 18 2023 at 08:31):

(Moving on somewhat from what turned out to be a cul-de-sac: do we already happen to have the natural map from Fin n -> Bool to Fin(2^n)? I'd quite like to use it...)

Eric Wieser (Jul 18 2023 at 08:32):

(I linked to the Fin 2 version of that above)

Wrenna Robson (Jul 18 2023 at 08:35):

(Apologies - can you possibly post it again?)

Eric Wieser (Jul 18 2023 at 08:36):

docs#finFunctionFinEquiv

Wrenna Robson (Jul 18 2023 at 08:37):

Thanks.

Wrenna Robson (Jul 18 2023 at 08:37):

I think that means I should use Fin 2 for my context.

Kyle Miller (Jul 18 2023 at 08:39):

If you want Bool, you can use finTwoEquiv along with that as well as this:

example (α β : Type _) (h : α ≃ β) : (γ → α) ≃ (γ → β) := Equiv.arrowCongr (Equiv.refl _) h

Kyle Miller (Jul 18 2023 at 08:40):

example : (Fin n → Bool) ≃ Fin (2 ^ n) :=
  (Equiv.arrowCongr (Equiv.refl _) finTwoEquiv).symm.trans finFunctionFinEquiv

Wrenna Robson (Jul 18 2023 at 08:43):

I may as well be plain about my context:

import Mathlib.Data.Fin.Basic
import Mathlib.Algebra.Ring.BooleanRing
import Mathlib.Data.Nat.Dist
import Mathlib.Data.Matrix.Notation

def ControlBits (m : Nat) := Fin (2*m + 1) → (Fin m → Bool) → Bool
def ControlBitsOriginal (m : Nat) := Fin ((2*m + 1)*2^m) → Bool

section ControlBits
def foldFin {m : ℕ} (i : Fin (2*m + 1)) : Fin (m + 1) :=
⟨m - (Nat.dist i m), lt_of_le_of_lt (Nat.sub_le _ _) (Nat.lt_succ_self _)⟩

def controlBitsToPerm {m : ℕ} (c : ControlBits m) (i : Fin (2*m + 1)) :
(Fin (m + 1) → Bool) → (Fin (m + 1) → Bool) :=
fun k => Function.update k (foldFin i) ((k (foldFin i)) + (c i (k ∘ (Fin.succAbove (foldFin i)))))

lemma controlBitsToPermInvolutive {m : ℕ} (c : ControlBits m) (i : Fin (2*m + 1)) :
Function.Involutive (controlBitsToPerm c i) := sorry

end ControlBits

Wrenna Robson (Jul 18 2023 at 08:45):

So originally this was a way of defining a permutation on Fin(2^(m+1)) via a member of Fin ((2*m + 1)*2^m) → Bool. It turns out to be much nicer to express that using the Fin k -> Bool form for things.

Wrenna Robson (Jul 18 2023 at 08:46):

Though somewhat hard to write down terms of type of ControlBits m.

Eric Wieser (Jul 18 2023 at 08:59):

Wrenna Robson said:

(Moving on somewhat from what turned out to be a cul-de-sac: ...)

I think it's best to split the thread at this message

Wrenna Robson (Jul 18 2023 at 09:23):

Agreed; this is a distraction.

Wrenna Robson (Jul 18 2023 at 09:24):

It should probably change stream as well but I don't have the rights to do that I think.

Notification Bot (Jul 19 2023 at 15:08):

14 messages were moved here from #mathlib4 > Proposed refactor of Bitvec by Alex Keizer.

Last updated: Feb 28 2026 at 14:05 UTC