Mathlib.Data.Multiset.Fold

Multiset.fold definition

: α → Multiset α → α

Full source

/-- `fold op b s` folds a commutative associative operation `op` over
  the multiset `s`. -/
def fold : α → Multiset α → α :=
  foldr op

Folding a commutative associative operation over a multiset

Informal description

Given a commutative and associative binary operation `op` and a starting value `b`, the function `fold` applies `op` to combine all elements of a multiset `s` with `b`. More precisely, for a multiset `s` and an operation `op`, `fold op b s` computes the result of successively applying `op` to the elements of `s` starting with `b`, where the order of operations does not matter due to the commutativity and associativity of `op`.

Multiset.fold_eq_foldr theorem

(b : α) (s : Multiset α) : fold op b s = foldr op b s

Full source

theorem fold_eq_foldr (b : α) (s : Multiset α) :
    fold op b s = foldr op b s :=
  rfl

Equivalence of Multiset Fold and Right Fold for Commutative Associative Operations

Informal description

For any commutative and associative binary operation `op`, starting value `b`, and multiset `s`, the fold operation over `s` with `op` and `b` is equal to the right fold of `op` over `s` with `b`. That is, $\text{fold}\, op\, b\, s = \text{foldr}\, op\, b\, s$.

Multiset.coe_fold_r theorem

(b : α) (l : List α) : fold op b l = l.foldr op b

Full source

@[simp]
theorem coe_fold_r (b : α) (l : List α) : fold op b l = l.foldr op b :=
  rfl

Equality of Multiset Fold and List Right Fold

Informal description

For any commutative and associative binary operation $\mathrm{op}$ and starting value $b$, the fold operation over a multiset constructed from a list $l$ is equal to the right fold operation over the list $l$. That is, $\mathrm{fold}\ \mathrm{op}\ b\ l = \mathrm{foldr}\ \mathrm{op}\ b\ l$.

Multiset.coe_fold_l theorem

(b : α) (l : List α) : fold op b l = l.foldl op b

Full source

theorem coe_fold_l (b : α) (l : List α) : fold op b l = l.foldl op b :=
  (coe_foldr_swap op b l).trans <| by simp [hc.comm]

Multiset Fold Equals List Left Fold

Informal description

For any commutative and associative binary operation `op`, starting value `b`, and list `l`, the fold operation over the multiset corresponding to `l` equals the left fold of `op` over `l` starting with `b`. That is, $\text{fold}\, op\, b\, l = \text{foldl}\, op\, b\, l$.

Multiset.fold_eq_foldl theorem

(b : α) (s : Multiset α) : fold op b s = foldl op b s

Full source

theorem fold_eq_foldl (b : α) (s : Multiset α) :
    fold op b s = foldl op b s :=
  Quot.inductionOn s fun _ => coe_fold_l _ _ _

Equality of Multiset Fold and Left Fold

Informal description

For any commutative and associative binary operation $\mathrm{op}$ on a type $\alpha$, any starting value $b \in \alpha$, and any multiset $s$ of elements of $\alpha$, the fold operation over $s$ equals the left fold operation over $s$. That is, $\mathrm{fold}\, \mathrm{op}\, b\, s = \mathrm{foldl}\, \mathrm{op}\, b\, s$.

Multiset.fold_zero theorem

(b : α) : (0 : Multiset α).fold op b = b

Full source

@[simp]
theorem fold_zero (b : α) : (0 : Multiset α).fold op b = b :=
  rfl

Fold of Empty Multiset Yields Initial Value

Informal description

For any element $b$ of type $\alpha$ and the empty multiset $0$, the fold operation with starting value $b$ returns $b$, i.e., $\text{fold}\, op\, b\, 0 = b$.

Multiset.fold_cons_left theorem

: ∀ (b a : α) (s : Multiset α), (a ::ₘ s).fold op b = a * s.fold op b

Full source

@[simp]
theorem fold_cons_left : ∀ (b a : α) (s : Multiset α), (a ::ₘ s).fold op b = a * s.fold op b :=
  foldr_cons _

Left-consistency of fold over multisets: $(a \cdot s).\text{fold}~*~b = a * (s.\text{fold}~*~b)$

Informal description

For any commutative and associative binary operation $*$ on a type $\alpha$, any elements $a, b \in \alpha$, and any multiset $s$ of elements of $\alpha$, the fold operation satisfies $(a \cdot s).\text{fold}~*~b = a * (s.\text{fold}~*~b)$, where $a \cdot s$ denotes the multiset obtained by adding $a$ to $s$.

Multiset.fold_cons_right theorem

(b a : α) (s : Multiset α) : (a ::ₘ s).fold op b = s.fold op b * a

Full source

theorem fold_cons_right (b a : α) (s : Multiset α) : (a ::ₘ s).fold op b = s.fold op b * a := by
  simp [hc.comm]

Right-consistency of fold over multisets: $(a \cdot s).\text{fold}\, op\, b = (s.\text{fold}\, op\, b) * a$

Informal description

For any commutative and associative binary operation $*$ on a type $\alpha$, any elements $a, b \in \alpha$, and any multiset $s$ of elements of $\alpha$, the fold operation satisfies $(a \cdot s).\text{fold}\, op\, b = (s.\text{fold}\, op\, b) * a$, where $a \cdot s$ denotes the multiset obtained by adding $a$ to $s$.

Multiset.fold_cons'_right theorem

(b a : α) (s : Multiset α) : (a ::ₘ s).fold op b = s.fold op (b * a)

Full source

theorem fold_cons'_right (b a : α) (s : Multiset α) : (a ::ₘ s).fold op b = s.fold op (b * a) := by
  rw [fold_eq_foldl, foldl_cons, ← fold_eq_foldl]

Right-consistency of fold with shifted accumulator: $(a \cdot s).\mathrm{fold}\, \mathrm{op}\, b = s.\mathrm{fold}\, \mathrm{op}\, (b * a)$

Informal description

For any commutative and associative binary operation $\mathrm{op}$ on a type $\alpha$, any elements $a, b \in \alpha$, and any multiset $s$ of elements of $\alpha$, the fold operation satisfies $(a \cdot s).\mathrm{fold}\, \mathrm{op}\, b = s.\mathrm{fold}\, \mathrm{op}\, (b * a)$, where $a \cdot s$ denotes the multiset obtained by adding $a$ to $s$.

Multiset.fold_cons'_left theorem

(b a : α) (s : Multiset α) : (a ::ₘ s).fold op b = s.fold op (a * b)

Full source

theorem fold_cons'_left (b a : α) (s : Multiset α) : (a ::ₘ s).fold op b = s.fold op (a * b) := by
  rw [fold_cons'_right, hc.comm]

Left-consistency of fold with shifted accumulator: $(a \cdot s).\text{fold}\, *\, b = s.\text{fold}\, *\, (a * b)$

Informal description

For any commutative and associative binary operation $*$ on a type $\alpha$, any elements $a, b \in \alpha$, and any multiset $s$ of elements of $\alpha$, the fold operation satisfies $(a \cdot s).\text{fold}\, *\, b = s.\text{fold}\, *\, (a * b)$, where $a \cdot s$ denotes the multiset obtained by adding $a$ to $s$.

Multiset.fold_add theorem

 (b₁ b₂ : α) (s₁ s₂ : Multiset α) : (s₁ + s₂).fold op (b₁ * b₂) = s₁.fold op b₁ * s₂.fold op b₂

Full source

theorem fold_add (b₁ b₂ : α) (s₁ s₂ : Multiset α) :
    (s₁ + s₂).fold op (b₁ * b₂) = s₁.fold op b₁ * s₂.fold op b₂ :=
  Multiset.induction_on s₂
    (by rw [Multiset.add_zero, fold_zero, ← fold_cons'_right, ← fold_cons_right op])
    (fun a b h => by rw [fold_cons_left, add_cons, fold_cons_left, h, ← ha.assoc, hc.comm a,
      ha.assoc])

Additivity of Fold over Multiset Union: $\text{fold}(*, b_1 * b_2, s_1 + s_2) = \text{fold}(*, b_1, s_1) * \text{fold}(*, b_2, s_2)$

Informal description

Let $*$ be a commutative and associative binary operation on a type $\alpha$. For any elements $b_1, b_2 \in \alpha$ and any multisets $s_1, s_2$ of elements of $\alpha$, the fold of the combined multiset $s_1 + s_2$ with initial value $b_1 * b_2$ is equal to the product of the folds of $s_1$ and $s_2$ with initial values $b_1$ and $b_2$ respectively. That is, \[ (s_1 + s_2).\text{fold}\, *\, (b_1 * b_2) = (s_1.\text{fold}\, *\, b_1) * (s_2.\text{fold}\, *\, b_2). \]

Multiset.fold_singleton theorem

(b a : α) : ({ a } : Multiset α).fold op b = a * b

Full source

theorem fold_singleton (b a : α) : ({a} : Multiset α).fold op b = a * b :=
  foldr_singleton _ _ _

Fold of Singleton Multiset: $\text{fold}(*, b, \{a\}) = a * b$

Informal description

For any elements $b$ and $a$ in a type $\alpha$ equipped with a commutative and associative binary operation $*$, the fold of the singleton multiset $\{a\}$ with initial value $b$ is equal to $a * b$. That is, $\text{fold}(*, b, \{a\}) = a * b$.

Multiset.fold_distrib theorem

 {f g : β → α} (u₁ u₂ : α) (s : Multiset β) :
  (s.map fun x => f x * g x).fold op (u₁ * u₂) = (s.map f).fold op u₁ * (s.map g).fold op u₂

Full source

theorem fold_distrib {f g : β → α} (u₁ u₂ : α) (s : Multiset β) :
    (s.map fun x => f x * g x).fold op (u₁ * u₂) = (s.map f).fold op u₁ * (s.map g).fold op u₂ :=
  Multiset.induction_on s (by simp) (fun a b h => by
    rw [map_cons, fold_cons_left, h, map_cons, fold_cons_left, map_cons,
      fold_cons_right, ha.assoc, ← ha.assoc (g a), hc.comm (g a),
      ha.assoc, hc.comm (g a), ha.assoc])

Distributivity of Fold over Function Composition: $\text{fold}(*, u_1 * u_2, \text{map}(f * g, s)) = \text{fold}(*, u_1, \text{map}(f, s)) * \text{fold}(*, u_2, \text{map}(g, s))$

Informal description

Let $*$ be a commutative and associative binary operation on a type $\alpha$, and let $f, g : \beta \to \alpha$ be functions. For any elements $u_1, u_2 \in \alpha$ and any multiset $s$ of elements of $\beta$, the following equality holds: \[ \left(s \mathbin{\text{map}} (x \mapsto f(x) * g(x))\right).\text{fold}~*~(u_1 * u_2) = (s \mathbin{\text{map}} f).\text{fold}~*~u_1 * (s \mathbin{\text{map}} g).\text{fold}~*~u_2. \]

Multiset.fold_hom theorem

 {op' : β → β → β} [Std.Commutative op'] [Std.Associative op'] {m : α → β} (hm : ∀ x y, m (op x y) = op' (m x) (m y))
  (b : α) (s : Multiset α) : (s.map m).fold op' (m b) = m (s.fold op b)

Full source

theorem fold_hom {op' : β → β → β} [Std.Commutative op'] [Std.Associative op'] {m : α → β}
    (hm : ∀ x y, m (op x y) = op' (m x) (m y)) (b : α) (s : Multiset α) :
    (s.map m).fold op' (m b) = m (s.fold op b) :=
  Multiset.induction_on s (by simp) (by simp +contextual [hm])

Homomorphism Property of Multiset Fold: $m(\text{fold}~*~b~s) = \text{fold}~*'~m(b)~(\text{map}~m~s)$

Informal description

Let $*$ and $*'$ be commutative and associative binary operations on types $\alpha$ and $\beta$ respectively, and let $m : \alpha \to \beta$ be a homomorphism satisfying $m(x * y) = m(x) *' m(y)$ for all $x, y \in \alpha$. Then for any starting value $b \in \alpha$ and any multiset $s$ of elements of $\alpha$, the fold of the image of $s$ under $m$ with operation $*'$ and starting value $m(b)$ equals the image under $m$ of the fold of $s$ with operation $*$ and starting value $b$. That is, $$(\text{map } m \ s).\text{fold}~*'~m(b) = m(s.\text{fold}~*~b).$$

Multiset.fold_union_inter theorem

 [DecidableEq α] (s₁ s₂ : Multiset α) (b₁ b₂ : α) :
  ((s₁ ∪ s₂).fold op b₁ * (s₁ ∩ s₂).fold op b₂) = s₁.fold op b₁ * s₂.fold op b₂

Full source

theorem fold_union_inter [DecidableEq α] (s₁ s₂ : Multiset α) (b₁ b₂ : α) :
    ((s₁ ∪ s₂).fold op b₁ * (s₁ ∩ s₂).fold op b₂) = s₁.fold op b₁ * s₂.fold op b₂ := by
  rw [← fold_add op, union_add_inter, fold_add op]

Fold Identity for Union and Intersection of Multisets: $\text{fold}(*, b_1, s_1 \cup s_2) * \text{fold}(*, b_2, s_1 \cap s_2) = \text{fold}(*, b_1, s_1) * \text{fold}(*, b_2, s_2)$

Informal description

Let $*$ be a commutative and associative binary operation on a type $\alpha$ with decidable equality. For any multisets $s_1, s_2$ of elements of $\alpha$ and any elements $b_1, b_2 \in \alpha$, the following equality holds: \[ (s_1 \cup s_2).\text{fold}\, *\, b_1 * (s_1 \cap s_2).\text{fold}\, *\, b_2 = s_1.\text{fold}\, *\, b_1 * s_2.\text{fold}\, *\, b_2. \]

Multiset.fold_dedup_idem theorem

[DecidableEq α] [hi : Std.IdempotentOp op] (s : Multiset α) (b : α) : (dedup s).fold op b = s.fold op b

Full source

@[simp]
theorem fold_dedup_idem [DecidableEq α] [hi : Std.IdempotentOp op] (s : Multiset α) (b : α) :
    (dedup s).fold op b = s.fold op b :=
  Multiset.induction_on s (by simp) fun a s IH => by
    by_cases h : a ∈ s <;> simp [IH, h]
    show fold op b s = op a (fold op b s)
    rw [← cons_erase h, fold_cons_left, ← ha.assoc, hi.idempotent]

Fold Invariance under Deduplication for Idempotent Operations

Informal description

For a type $\alpha$ with decidable equality and an idempotent binary operation $*$ on $\alpha$, the fold operation over a multiset $s$ with starting value $b$ is equal to the fold operation over the deduplicated version of $s$ with the same starting value. That is, $(\text{dedup } s).\text{fold}~*~b = s.\text{fold}~*~b$.