Documentation

Complexity.Foundations.Data.List.SelectDistinct

Selecting distinct list entries by a mask #

Cslib.Complexity.selectDistinct l w keeps the entry at position i of l when bit i of w is true and i is the first occurrence of that entry in l. Missing bits are false, and bits beyond the length of l are ignored. Unlike Cslib.Complexity.maskSelect, which keeps every selected position and so selects sub-multisets, a repeated entry is selected at most once, so the selection is duplicate-free (nodup_selectDistinct) and describes a set. Selecting with a full mask of true bits lists the distinct entries of l in the order of their first occurrences (mem_selectDistinct_replicate, length_selectDistinct_replicate).

Main definitions #

Main results #

source
def Cslib.Complexity.selectDistinct {γ : Type u_1} [DecidableEq γ] (l : List γ) (w : List Bool) :
List γ

The distinct entries of l selected by the mask w: position i of l is kept when bit i of w is true and i is the first occurrence of its entry in l. Missing bits are false, and bits beyond the length of l are ignored. Unlike Cslib.Complexity.maskSelect, which keeps every selected position and so selects sub-multisets, a repeated entry is selected at most once, so the selection describes a set.

Instances For
    source
    theorem Cslib.Complexity.mem_selectDistinct {γ : Type u_1} [DecidableEq γ] {l : List γ} {w : List Bool} {v : γ} :
    v ∈ selectDistinct l w ↔ v ∈ l ∧ w.getD (List.idxOf v l) false = true

    An entry v belongs to selectDistinct l w iff v ∈ l and the mask bit at the first occurrence l.idxOf v is true.

    source
    theorem Cslib.Complexity.nodup_selectDistinct {γ : Type u_1} [DecidableEq γ] (l : List γ) (w : List Bool) :
    (selectDistinct l w).Nodup

    selectDistinct l w contains no duplicate entries.

    source
    theorem Cslib.Complexity.mem_selectDistinct_replicate {γ : Type u_1} [DecidableEq γ] {l : List γ} {v : γ} :
    v ∈ selectDistinct l (List.replicate l.length true) ↔ v ∈ l

    The full mask selects every entry of l, at its first occurrence.

    source
    theorem Cslib.Complexity.length_selectDistinct_replicate {γ : Type u_1} [DecidableEq γ] (l : List γ) :
    (selectDistinct l (List.replicate l.length true)).length = l.toFinset.card

    The full mask selects as many entries as l has distinct entries.