One-hot bit lists

listSingle dimension index is the bit list of length dimension whose only true coordinate is index; an index outside the dimension gives all zeros. It is the list form of a one-hot row in an explicit relation table (CSP.Table.exactlyOne) and of the basis vector Pi.single index true (listSingle_eq_ofFn_single in BitString.List.Operations).

Main definitions

• Cslib.BitString.listSingle: the one-hot list of a given length.

Main results

• Cslib.BitString.listSingle_eq_ofFn: an in-range one-hot list as List.ofFn.
• Cslib.BitString.listSingle_succ_zero, Cslib.BitString.listSingle_succ_succ: the recursive description by the first coordinate.
• Cslib.BitString.count_true_listSingle, Cslib.BitString.exists_listSingle_of_count_true: the one-hot lists of a given length are exactly the lists with one true coordinate.

def Cslib.BitString.listSingle (dimension index : ℕ) : List Bool

A coordinate mask, with all zeros when the index is outside the requested dimension.

theorem Cslib.BitString.listSingle_eq_ofFn {n : ℕ} (index : Fin n) : listSingle n ↑index = List.ofFn fun (j : Fin n) => decide (j = index)

An in-range one-hot list is the list of the indicator of its index.

theorem Cslib.BitString.listSingle_succ_zero (dimension : ℕ) : listSingle (dimension + 1) 0 = true :: List.replicate dimension false

A one-hot list at position zero starts with true.

theorem Cslib.BitString.listSingle_succ_succ (dimension index : ℕ) : listSingle (dimension + 1) (index + 1) = false :: listSingle dimension index

Shifting the selected position prepends a zero.

theorem Cslib.BitString.count_true_listSingle {dimension index : ℕ} (h : index < dimension) : List.count true (listSingle dimension index) = 1

An in-range one-hot list has precisely one true coordinate.

theorem Cslib.BitString.exists_listSingle_of_count_true {row : List Bool} (h : List.count true row = 1) : ∃ (index : ℕ), index < row.length ∧ listSingle row.length index = row

Every list with exactly one true coordinate is a one-hot list.