Support subsets of list-represented bit strings

Views word : List Bool as its support subset {i : Fin n | ofList n word i = true} via Cslib.BitString.ofList, padding short lists with false and ignoring indices ≥ n.

Main definitions

• Cslib.BitString.supportOfList: support subset {i : Fin n | ofList n word i = true}.

Main results

• Cslib.BitString.mem_supportOfList, Cslib.BitString.supportOfList_ofFn_decide, Cslib.BitString.ofFn_decide_mem_supportOfList, Cslib.BitString.supportOfList_injective_of_length, Cslib.BitString.card_supportOfList_of_length: membership, round-trips, injectivity, and card.

def Cslib.BitString.supportOfList (n : ℕ) (word : List Bool) : Finset (Fin n)

Convert a Boolean indicator list to its support subset in Fin n via BitString.ofList.

@[simp]

theorem Cslib.BitString.mem_supportOfList {n : ℕ} {word : List Bool} {i : Fin n} : i ∈ supportOfList n word ↔ word.getD (↑i) false = true

Coordinate i : Fin n lies in supportOfList n word iff word.getD i.val false = true.

@[simp]

theorem Cslib.BitString.supportOfList_ofFn_decide {n : ℕ} (S : Finset (Fin n)) : supportOfList n (List.ofFn fun (i : Fin n) => decide (i ∈ S)) = S

Round-trip from S : Finset (Fin n) through List.ofFn (fun i => decide (i ∈ S)).

theorem Cslib.BitString.ofFn_decide_mem_supportOfList {n : ℕ} {word : List Bool} (hw : word.length = n) : (List.ofFn fun (i : Fin n) => decide (i ∈ supportOfList n word)) = word

On words of length n, List.ofFn (fun i => decide (i ∈ supportOfList n word)) is word.

theorem Cslib.BitString.supportOfList_injective_of_length {n : ℕ} {w₁ w₂ : List Bool} (hw₁ : w₁.length = n) (hw₂ : w₂.length = n) (heq : supportOfList n w₁ = supportOfList n w₂) : w₁ = w₂

On words of exact length n, supportOfList n is injective.

theorem Cslib.BitString.card_supportOfList_of_length {n : ℕ} {word : List Bool} (hw : word.length = n) : (supportOfList n word).card = List.count true word

On words of exact length n, #(supportOfList n word) = word.count true.