Selecting list entries by a mask

Cslib.Complexity.maskSelect l w keeps the entries of l at the positions where the bit string w is true. Masks describe exactly the sublists of l, and therefore, up to order, exactly the sub-multisets of l; this makes them polynomially long certificates for problems that ask for a sub-multiset of the input numbers, such as subset sum, partition and knapsack. Unlike Cslib.Complexity.selectDistinct, which selects each distinct entry at most once and so selects sets, a repeated entry may be selected repeatedly.

Main definitions

• Cslib.Complexity.maskSelect.

Main results

• Cslib.Complexity.maskSelect_sublist, Cslib.Complexity.exists_maskSelect_eq: masks select exactly the sublists.
• Cslib.Complexity.exists_le_coe_iff_exists_sublist: sub-multisets are sublists up to order.
• Cslib.Complexity.exists_le_iff_exists_maskSelect: a property of sub-multisets holds for one of them exactly when it holds for the selection of some mask of any length at least the length of the list.
• Cslib.Complexity.maskSelect_eq_map_filter_range: the selection as the entries at the selected indices.
• Cslib.Complexity.sum_maskSelect: the sum of the selected numbers is the scalar product with the mask.

def Cslib.Complexity.maskSelect {α : Type u_1} (l : List α) (w : List Bool) : List α

The entries of l at the positions where w is true; positions beyond the end of w are not selected. Repeated entries may be selected repeatedly, so masks select sub-multisets; for sets, Cslib.Complexity.selectDistinct selects each entry at most once.

@[simp]

theorem Cslib.Complexity.maskSelect_nil {α : Type u_1} (w : List Bool) : maskSelect [] w = []

theorem Cslib.Complexity.maskSelect_cons {α : Type u_1} (a : α) (l : List α) (w : List Bool) : maskSelect (a :: l) w = (if w.headD false = true then [a] else []) ++ maskSelect l w.tail

theorem Cslib.Complexity.maskSelect_sublist {α : Type u_1} (l : List α) (w : List Bool) : (maskSelect l w).Sublist l

A mask selects a sublist.

theorem Cslib.Complexity.exists_maskSelect_eq {α : Type u_1} {s l : List α} (h : s.Sublist l) : ∃ (w : List Bool), w.length = l.length ∧ maskSelect l w = s

Every sublist is selected by a mask as long as the list.

theorem Cslib.Complexity.maskSelect_append_replicate_false {α : Type u_1} (l : List α) (w : List Bool) (k : ℕ) : maskSelect l (w ++ List.replicate k false) = maskSelect l w

Unselected positions beyond the list do not change the selection.

theorem Cslib.Complexity.maskSelect_eq_map_filter_range {α : Type u_1} (l : List α) (w : List Bool) (d : α) : maskSelect l w = List.map (fun (x : ℕ) => l.getD x d) (List.filter (fun (i : ℕ) => w.getD i false) (List.range l.length))

The selection of a mask is the list of entries at the selected indices.

theorem Cslib.Complexity.sum_maskSelect (a : List ℕ) (w : List Bool) : (maskSelect a w).sum = ∑ j ∈ Finset.range a.length, a.getD j 0 * (w.getD j false).toNat

The numbers selected by a mask sum to the scalar product with the mask.

theorem Cslib.Complexity.exists_le_coe_iff_exists_sublist {α : Type u_1} {l : List α} (P : Multiset α → Prop) : (∃ s ≤ ↑l, P s) ↔ ∃ (s : List α), s.Sublist l ∧ P ↑s

The sub-multisets of a list are the sublists, up to order.

theorem Cslib.Complexity.exists_le_iff_exists_maskSelect {α : Type u_1} {l : List α} {n : ℕ} (hn : l.length ≤ n) (P : Multiset α → Prop) : (∃ s ≤ ↑l, P s) ↔ ∃ (w : List Bool), w.length = n ∧ P ↑(maskSelect l w)

A property of sub-multisets of l holds for one of them exactly when it holds for the selection of a mask of length n, for any n at least the length of l.