Documentation

Batteries.Data.List.Count

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 #

source
theorem List.count_singleton' {α : Type u_1} [DecidableEq α] (a b : α) :
count a [b] = if b = a then 1 else 0
source
theorem List.count_concat {α : Type u_1} [BEq α] [LawfulBEq α] (a : α) (l : List α) :
count a (l.concat a) = count a l + 1

idxToSigmaCount, sigmaCountToIdx #

source
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
Instances For
    source
    @[simp]
    theorem List.fst_idxToSigmaCount {α : Type u_1} [BEq α] [ReflBEq α] {xs : List α} {i : Fin xs.length} :
    (xs.idxToSigmaCount i).fst = xs[↑i]
    source
    @[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, ⋯⟩
    source
    @[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
    source
    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
    Instances For
      source
      @[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
      source
      @[simp]
      theorem List.sigmaCountToIdx_idxToSigmaCount {α : Type u_1} [BEq α] [ReflBEq α] {xs : List α} {i : Fin xs.length} :
      xs.sigmaCountToIdx (xs.idxToSigmaCount i) = i
      source
      theorem List.leftInverse_sigmaCountToIdx_idxToSigmaCount {α : Type u_1} [BEq α] [ReflBEq α] {xs : List α} :
      Function.LeftInverse xs.sigmaCountToIdx xs.idxToSigmaCount
      source
      theorem List.rightInverse_idxToSigmaCount_sigmaCountToIdx {α : Type u_1} [BEq α] [ReflBEq α] {xs : List α} :
      Function.RightInverse xs.idxToSigmaCount xs.sigmaCountToIdx
      source
      theorem List.injective_idxToSigmaCount {α : Type u_1} [BEq α] [ReflBEq α] {xs : List α} :
      Function.Injective xs.idxToSigmaCount
      source
      theorem List.surjective_sigmaCountToIdx {α : Type u_1} [BEq α] [ReflBEq α] {xs : List α} :
      Function.Surjective xs.sigmaCountToIdx
      source
      @[simp]
      theorem List.idxToSigmaCount_sigmaCountToIdx {α : Type u_1} [BEq α] [LawfulBEq α] {xs : List α} {xc : (x : α) × Fin (count x xs)} :
      xs.idxToSigmaCount (xs.sigmaCountToIdx xc) = xc
      source
      theorem List.leftInverse_idxToSigmaCount_sigmaCountToIdx {α : Type u_1} [BEq α] [LawfulBEq α] {xs : List α} :
      Function.LeftInverse xs.idxToSigmaCount xs.sigmaCountToIdx
      source
      theorem List.rightInverse_sigmaCountToIdx_idxToSigmaCount {α : Type u_1} [BEq α] [LawfulBEq α] {xs : List α} :
      Function.RightInverse xs.sigmaCountToIdx xs.idxToSigmaCount
      source
      theorem List.injective_sigmaCountToIdx {α : Type u_1} [BEq α] [LawfulBEq α] {xs : List α} :
      Function.Injective xs.sigmaCountToIdx
      source
      theorem List.surjective_idxToSigmaCount {α : Type u_1} [BEq α] [LawfulBEq α] {xs : List α} :
      Function.Surjective xs.idxToSigmaCount