Counting in lists

This file proves basic properties of List.countP and List.count, which count the number of elements of a list satisfying a predicate and equal to a given element respectively. Their definitions can be found in Batteries.Data.List.Basic.

count

theorem List.count_singleton' {α : Type u_1} [DecidableEq α] (a b : α) : count a [b] = if b = a then 1 else 0

theorem List.count_concat {α : Type u_1} [BEq α] [LawfulBEq α] (a : α) (l : List α) : count a (l.concat a) = count a l + 1

idxToSigmaCount, sigmaCountToIdx

def List.idxToSigmaCount {α : Type u_1} [BEq α] [ReflBEq α] (xs : List α) (i : Fin xs.length) : (x : α) × Fin (count x xs)

idxToSigmaCount is essentially a Fin-to-Fin wrapper for countBefore that also includes the corresponding element.

For example:

idxToSigmaCount [5, 1, 3, 2, 4, 0, 1, 4] 5 = ⟨0, 0⟩

Equations

• xs.idxToSigmaCount i = ⟨xs[↑i], ⟨List.countBefore xs[↑i] xs ↑i, ⋯⟩⟩

@[simp]

theorem List.fst_idxToSigmaCount {α : Type u_1} [BEq α] [ReflBEq α] {xs : List α} {i : Fin xs.length} : (xs.idxToSigmaCount i).fst = xs[↑i]

@[simp]

theorem List.snd_idxToSigmaCount {α : Type u_1} [BEq α] [ReflBEq α] {xs : List α} {i : Fin xs.length} : (xs.idxToSigmaCount i).snd = ⟨countBefore xs[↑i] xs ↑i, ⋯⟩

@[simp]

theorem List.coe_snd_idxToSigmaCount {α : Type u_1} [BEq α] [ReflBEq α] {xs : List α} {i : Fin xs.length} : ↑(xs.idxToSigmaCount i).snd = countBefore xs[↑i] xs ↑i

def List.sigmaCountToIdx {α : Type u_1} [BEq α] (xs : List α) (xc : (x : α) × Fin (count x xs)) : Fin xs.length

sigmaCountToIdx is a _ × Fin-to-Fin wrapper for countBefore.

For example:

sigmaCountToIdx [5, 1, 3, 2, 4, 0, 1, 4] ⟨0, 0⟩ = 5

Equations

• xs.sigmaCountToIdx xc = ⟨List.idxOfNth xc.fst xs ↑xc.snd, ⋯⟩

@[simp]

theorem List.coe_sigmaCountToIdx {α : Type u_1} [BEq α] {xs : List α} {xc : (x : α) × Fin (count x xs)} : ↑(xs.sigmaCountToIdx xc) = idxOfNth xc.fst xs ↑xc.snd

@[simp]

theorem List.sigmaCountToIdx_idxToSigmaCount {α : Type u_1} [BEq α] [ReflBEq α] {xs : List α} {i : Fin xs.length} : xs.sigmaCountToIdx (xs.idxToSigmaCount i) = i

theorem List.leftInverse_sigmaCountToIdx_idxToSigmaCount {α : Type u_1} [BEq α] [ReflBEq α] {xs : List α} : Function.LeftInverse xs.sigmaCountToIdx xs.idxToSigmaCount

theorem List.rightInverse_idxToSigmaCount_sigmaCountToIdx {α : Type u_1} [BEq α] [ReflBEq α] {xs : List α} : Function.RightInverse xs.idxToSigmaCount xs.sigmaCountToIdx

theorem List.injective_idxToSigmaCount {α : Type u_1} [BEq α] [ReflBEq α] {xs : List α} : Function.Injective xs.idxToSigmaCount

theorem List.surjective_sigmaCountToIdx {α : Type u_1} [BEq α] [ReflBEq α] {xs : List α} : Function.Surjective xs.sigmaCountToIdx

@[simp]

theorem List.idxToSigmaCount_sigmaCountToIdx {α : Type u_1} [BEq α] [LawfulBEq α] {xs : List α} {xc : (x : α) × Fin (count x xs)} : xs.idxToSigmaCount (xs.sigmaCountToIdx xc) = xc

theorem List.leftInverse_idxToSigmaCount_sigmaCountToIdx {α : Type u_1} [BEq α] [LawfulBEq α] {xs : List α} : Function.LeftInverse xs.idxToSigmaCount xs.sigmaCountToIdx

theorem List.rightInverse_sigmaCountToIdx_idxToSigmaCount {α : Type u_1} [BEq α] [LawfulBEq α] {xs : List α} : Function.RightInverse xs.sigmaCountToIdx xs.idxToSigmaCount

theorem List.injective_sigmaCountToIdx {α : Type u_1} [BEq α] [LawfulBEq α] {xs : List α} : Function.Injective xs.sigmaCountToIdx

theorem List.surjective_idxToSigmaCount {α : Type u_1} [BEq α] [LawfulBEq α] {xs : List α} : Function.Surjective xs.idxToSigmaCount