From 084c2f8ad9e6fb4e2a1928d09e93ef1815b268ca Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ya=C3=ABl=20Dillies?= Date: Sat, 7 Dec 2024 07:52:21 +0000 Subject: [PATCH] chore: don't import algebra in `Data.Multiset.Basic` --- Mathlib.lean | 1 + .../Algebra/BigOperators/Group/Multiset.lean | 3 +- .../BigOperators/GroupWithZero/Action.lean | 2 +- Mathlib/Algebra/Order/Group/Multiset.lean | 177 ++++ Mathlib/Data/Multiset/Basic.lean | 904 ++++++++---------- Mathlib/Data/Multiset/OrderedMonoid.lean | 2 +- Mathlib/Data/Multiset/Range.lean | 2 +- Mathlib/Data/Sym/Basic.lean | 6 +- 8 files changed, 598 insertions(+), 499 deletions(-) create mode 100644 Mathlib/Algebra/Order/Group/Multiset.lean diff --git a/Mathlib.lean b/Mathlib.lean index 9269de2ed24fa8..0ee5365dc0d704 100644 --- a/Mathlib.lean +++ b/Mathlib.lean @@ -671,6 +671,7 @@ import Mathlib.Algebra.Order.Group.Instances import Mathlib.Algebra.Order.Group.Int import Mathlib.Algebra.Order.Group.Lattice import Mathlib.Algebra.Order.Group.MinMax +import Mathlib.Algebra.Order.Group.Multiset import Mathlib.Algebra.Order.Group.Nat import Mathlib.Algebra.Order.Group.Opposite import Mathlib.Algebra.Order.Group.OrderIso diff --git a/Mathlib/Algebra/BigOperators/Group/Multiset.lean b/Mathlib/Algebra/BigOperators/Group/Multiset.lean index a0bb921c056e3a..17b4f3c33d7678 100644 --- a/Mathlib/Algebra/BigOperators/Group/Multiset.lean +++ b/Mathlib/Algebra/BigOperators/Group/Multiset.lean @@ -5,7 +5,8 @@ Authors: Mario Carneiro -/ import Mathlib.Algebra.BigOperators.Group.List import Mathlib.Algebra.Group.Prod -import Mathlib.Data.Multiset.Basic +import Mathlib.Algebra.Order.Group.Multiset +import Mathlib.Algebra.Order.Sub.Unbundled.Basic /-! # Sums and products over multisets diff --git a/Mathlib/Algebra/BigOperators/GroupWithZero/Action.lean b/Mathlib/Algebra/BigOperators/GroupWithZero/Action.lean index 6f377d4ff77be1..12833504924063 100644 --- a/Mathlib/Algebra/BigOperators/GroupWithZero/Action.lean +++ b/Mathlib/Algebra/BigOperators/GroupWithZero/Action.lean @@ -6,7 +6,7 @@ Authors: Yury Kudryashov import Mathlib.Algebra.BigOperators.Group.Finset import Mathlib.Algebra.GroupWithZero.Action.Defs import Mathlib.Data.Finset.Basic -import Mathlib.Data.Multiset.Basic +import Mathlib.Algebra.Order.Group.Multiset import Mathlib.Algebra.BigOperators.Finprod /-! diff --git a/Mathlib/Algebra/Order/Group/Multiset.lean b/Mathlib/Algebra/Order/Group/Multiset.lean new file mode 100644 index 00000000000000..18154cf1b463d4 --- /dev/null +++ b/Mathlib/Algebra/Order/Group/Multiset.lean @@ -0,0 +1,177 @@ +/- +Copyright (c) 2015 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Mario Carneiro +-/ +import Mathlib.Algebra.Group.Hom.Defs +import Mathlib.Algebra.Group.Nat.Basic +import Mathlib.Algebra.Order.Monoid.Unbundled.ExistsOfLE +import Mathlib.Algebra.Order.Sub.Defs +import Mathlib.Data.Multiset.Basic + +/-! +# Multisets form an ordered monoid + +This file contains the ordered monoid instance on multisets, and lemmas related to it. + +See note [foundational algebra order theory]. +-/ + +open List Nat + +variable {α β : Type*} + +namespace Multiset + +/-! ### Additive monoid -/ + +instance instAddLeftMono : AddLeftMono (Multiset α) where elim _s _t _u := Multiset.add_le_add_left + +instance instAddLeftReflectLE : AddLeftReflectLE (Multiset α) where + elim _s _t _u := Multiset.le_of_add_le_add_left + +instance instAddCancelCommMonoid : AddCancelCommMonoid (Multiset α) where + add_comm := Multiset.add_comm + add_assoc := Multiset.add_assoc + zero_add := Multiset.zero_add + add_zero := Multiset.add_zero + add_left_cancel _ _ _ := Multiset.add_right_inj.1 + nsmul := nsmulRec + +lemma mem_of_mem_nsmul {a : α} {s : Multiset α} {n : ℕ} (h : a ∈ n • s) : a ∈ s := by + induction' n with n ih + · rw [zero_nsmul] at h + exact absurd h (not_mem_zero _) + · rw [succ_nsmul, mem_add] at h + exact h.elim ih id + +@[simp] +lemma mem_nsmul {a : α} {s : Multiset α} {n : ℕ} : a ∈ n • s ↔ n ≠ 0 ∧ a ∈ s := by + refine ⟨fun ha ↦ ⟨?_, mem_of_mem_nsmul ha⟩, fun h ↦ ?_⟩ + · rintro rfl + simp [zero_nsmul] at ha + obtain ⟨n, rfl⟩ := exists_eq_succ_of_ne_zero h.1 + rw [succ_nsmul, mem_add] + exact Or.inr h.2 + +lemma mem_nsmul_of_ne_zero {a : α} {s : Multiset α} {n : ℕ} (h0 : n ≠ 0) : a ∈ n • s ↔ a ∈ s := by + simp [*] + +lemma nsmul_cons {s : Multiset α} (n : ℕ) (a : α) : + n • (a ::ₘ s) = n • ({a} : Multiset α) + n • s := by + rw [← singleton_add, nsmul_add] + +/-! ### Cardinality -/ + +/-- `Multiset.card` bundled as a group hom. -/ +@[simps] +def cardHom : Multiset α →+ ℕ where + toFun := card + map_zero' := card_zero + map_add' := card_add + +lemma card_nsmul (s : Multiset α) (n : ℕ) : card (n • s) = n * card s := cardHom.map_nsmul .. + +/-! ### `Multiset.replicate` -/ + +/-- `Multiset.replicate` as an `AddMonoidHom`. -/ +@[simps] +def replicateAddMonoidHom (a : α) : ℕ →+ Multiset α where + toFun n := replicate n a + map_zero' := replicate_zero a + map_add' _ _ := replicate_add _ _ a + +lemma nsmul_replicate {a : α} (n m : ℕ) : n • replicate m a = replicate (n * m) a := + ((replicateAddMonoidHom a).map_nsmul _ _).symm + +lemma nsmul_singleton (a : α) (n) : n • ({a} : Multiset α) = replicate n a := by + rw [← replicate_one, nsmul_replicate, mul_one] + +/-! ### `Multiset.map` -/ + +/-- `Multiset.map` as an `AddMonoidHom`. -/ +@[simps] +def mapAddMonoidHom (f : α → β) : Multiset α →+ Multiset β where + toFun := map f + map_zero' := map_zero _ + map_add' := map_add _ + +@[simp] +lemma coe_mapAddMonoidHom (f : α → β) : (mapAddMonoidHom f : Multiset α → Multiset β) = map f := rfl + +lemma map_nsmul (f : α → β) (n : ℕ) (s) : map f (n • s) = n • map f s := + (mapAddMonoidHom f).map_nsmul _ _ + +/-! ### Subtraction -/ + +section +variable [DecidableEq α] + +instance : OrderedSub (Multiset α) where tsub_le_iff_right _n _m _k := Multiset.sub_le_iff_le_add + +instance : ExistsAddOfLE (Multiset α) where + exists_add_of_le h := leInductionOn h fun s ↦ + let ⟨l, p⟩ := s.exists_perm_append; ⟨l, Quot.sound p⟩ + +end + +/-! ### `Multiset.filter` -/ + +section +variable (p : α → Prop) [DecidablePred p] + +lemma filter_nsmul (s : Multiset α) (n : ℕ) : filter p (n • s) = n • filter p s := by + refine s.induction_on ?_ ?_ + · simp only [filter_zero, nsmul_zero] + · intro a ha ih + rw [nsmul_cons, filter_add, ih, filter_cons, nsmul_add] + congr + split_ifs with hp <;> + · simp only [filter_eq_self, nsmul_zero, filter_eq_nil] + intro b hb + rwa [mem_singleton.mp (mem_of_mem_nsmul hb)] + +/-! ### countP -/ + +@[simp] +lemma countP_nsmul (s) (n : ℕ) : countP p (n • s) = n * countP p s := by + induction n <;> simp [*, succ_nsmul, succ_mul, zero_nsmul] + +/-- `countP p`, the number of elements of a multiset satisfying `p`, promoted to an +`AddMonoidHom`. -/ +def countPAddMonoidHom : Multiset α →+ ℕ where + toFun := countP p + map_zero' := countP_zero _ + map_add' := countP_add _ + +@[simp] lemma coe_countPAddMonoidHom : (countPAddMonoidHom p : Multiset α → ℕ) = countP p := rfl + +end + +/-! ### Multiplicity of an element -/ + +section +variable [DecidableEq α] {s : Multiset α} + +/-- `count a`, the multiplicity of `a` in a multiset, promoted to an `AddMonoidHom`. -/ +def countAddMonoidHom (a : α) : Multiset α →+ ℕ := + countPAddMonoidHom (a = ·) + +@[simp] +lemma coe_countAddMonoidHom (a : α) : (countAddMonoidHom a : Multiset α → ℕ) = count a := rfl + +@[simp] +lemma count_nsmul (a : α) (n s) : count a (n • s) = n * count a s := by + induction n <;> simp [*, succ_nsmul, succ_mul, zero_nsmul] + +end + +-- TODO: This should be `addMonoidHom_ext` +@[ext] +lemma addHom_ext [AddZeroClass β] ⦃f g : Multiset α →+ β⦄ (h : ∀ x, f {x} = g {x}) : f = g := by + ext s + induction' s using Multiset.induction_on with a s ih + · simp only [_root_.map_zero] + · simp only [← singleton_add, _root_.map_add, ih, h] + +end Multiset diff --git a/Mathlib/Data/Multiset/Basic.lean b/Mathlib/Data/Multiset/Basic.lean index 4dd4d674499624..e96627d610e0f2 100644 --- a/Mathlib/Data/Multiset/Basic.lean +++ b/Mathlib/Data/Multiset/Basic.lean @@ -3,24 +3,34 @@ Copyright (c) 2015 Microsoft Corporation. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Mario Carneiro -/ -import Mathlib.Algebra.Group.Hom.Defs -import Mathlib.Algebra.Group.Nat.Basic -import Mathlib.Algebra.Order.Sub.Unbundled.Basic +import Mathlib.Data.List.Count import Mathlib.Data.List.Perm.Basic import Mathlib.Data.List.Perm.Lattice import Mathlib.Data.List.Perm.Subperm import Mathlib.Data.Set.List import Mathlib.Order.Hom.Basic +import Mathlib.Order.MinMax /-! # Multisets -These are implemented as the quotient of a list by permutations. + +Multisets are finite sets with duplicates allowed. They are implemented here as the quotient of +lists by permutation. This gives them computational content. + ## Notation -We define the global infix notation `::ₘ` for `Multiset.cons`. + +* `0`: The empty multiset. +* `{a}`: The multiset containing a single occurrence of `a`. +* `a ::ₘ s`: The multiset containing one more occurrence of `a` than `s`. +* `s + t`: The multiset containing for each `a` the sum of the occurrences of `a` in `s` and `t`. +* `s - t`: The multiset containing for each `a` the difference of the occurrences of `a` in `s` and + `t`. +* `s ∪ t`: The multiset containing for each `a` the max of the occurrences of `a` in `s` and `t`. +* `s ∩ t`: The multiset containing for each `a` the min of the occurrences of `a` in `s` and `t`. -/ --- No bundled ordered algebra should be required -assert_not_exists OrderedCommMonoid +-- No algebra should be required +assert_not_exists Monoid universe v @@ -572,6 +582,8 @@ end /-! ### Additive monoid -/ +section add +variable {s t u : Multiset α} /-- The sum of two multisets is the lift of the list append operation. This adds the multiplicities of each element, @@ -591,28 +603,33 @@ theorem coe_add (s t : List α) : (s + t : Multiset α) = (s ++ t : List α) := theorem singleton_add (a : α) (s : Multiset α) : {a} + s = a ::ₘ s := rfl -private theorem add_le_add_iff_left' {s t u : Multiset α} : s + t ≤ s + u ↔ t ≤ u := +protected lemma add_le_add_iff_left : s + t ≤ s + u ↔ t ≤ u := Quotient.inductionOn₃ s t u fun _ _ _ => subperm_append_left _ -instance : AddLeftMono (Multiset α) := - ⟨fun _s _t _u => add_le_add_iff_left'.2⟩ +protected lemma add_le_add_iff_right : s + u ≤ t + u ↔ s ≤ t := + Quotient.inductionOn₃ s t u fun _ _ _ => subperm_append_right _ + +protected alias ⟨le_of_add_le_add_left, add_le_add_left⟩ := Multiset.add_le_add_iff_left +protected alias ⟨le_of_add_le_add_right, add_le_add_right⟩ := Multiset.add_le_add_iff_right -instance : AddLeftReflectLE (Multiset α) := - ⟨fun _s _t _u => add_le_add_iff_left'.1⟩ +protected lemma add_comm (s t : Multiset α) : s + t = t + s := + Quotient.inductionOn₂ s t fun _ _ ↦ Quot.sound perm_append_comm -instance instAddCommMonoid : AddCancelCommMonoid (Multiset α) where - add_comm := fun s t => Quotient.inductionOn₂ s t fun _ _ => Quot.sound perm_append_comm - add_assoc := fun s₁ s₂ s₃ => - Quotient.inductionOn₃ s₁ s₂ s₃ fun l₁ l₂ l₃ => congr_arg _ <| append_assoc l₁ l₂ l₃ - zero_add := fun s => Quot.inductionOn s fun _ => rfl - add_zero := fun s => Quotient.inductionOn s fun l => congr_arg _ <| append_nil l - add_left_cancel := fun _ _ _ h => - le_antisymm (Multiset.add_le_add_iff_left'.mp h.le) (Multiset.add_le_add_iff_left'.mp h.ge) - nsmul := nsmulRec +protected lemma add_assoc (s t u : Multiset α) : s + t + u = s + (t + u) := + Quotient.inductionOn₃ s t u fun _ _ _ ↦ congr_arg _ <| append_assoc .. -theorem le_add_right (s t : Multiset α) : s ≤ s + t := by simpa using add_le_add_left (zero_le t) s +@[simp, nolint simpNF] -- We want to use this lemma earlier than `zero_add` +protected lemma zero_add (s : Multiset α) : 0 + s = s := Quotient.inductionOn s fun _ ↦ rfl -theorem le_add_left (s t : Multiset α) : s ≤ t + s := by simpa using add_le_add_right (zero_le t) s +@[simp, nolint simpNF] -- We want to use this lemma earlier than `add_zero` +protected lemma add_zero (s : Multiset α) : s + 0 = s := + Quotient.inductionOn s fun l ↦ congr_arg _ <| append_nil l + +lemma le_add_right (s t : Multiset α) : s ≤ s + t := by + simpa using Multiset.add_le_add_left (zero_le t) + +lemma le_add_left (s t : Multiset α) : s ≤ t + s := by + simpa using Multiset.add_le_add_right (zero_le t) lemma subset_add_left {s t : Multiset α} : s ⊆ s + t := subset_of_le <| le_add_right s t @@ -627,48 +644,24 @@ theorem le_iff_exists_add {s t : Multiset α} : s ≤ t ↔ ∃ u, t = s + u := @[simp] theorem cons_add (a : α) (s t : Multiset α) : a ::ₘ s + t = a ::ₘ (s + t) := by - rw [← singleton_add, ← singleton_add, add_assoc] + rw [← singleton_add, ← singleton_add, Multiset.add_assoc] @[simp] theorem add_cons (a : α) (s t : Multiset α) : s + a ::ₘ t = a ::ₘ (s + t) := by - rw [add_comm, cons_add, add_comm] + rw [Multiset.add_comm, cons_add, Multiset.add_comm] @[simp] theorem mem_add {a : α} {s t : Multiset α} : a ∈ s + t ↔ a ∈ s ∨ a ∈ t := Quotient.inductionOn₂ s t fun _l₁ _l₂ => mem_append -theorem mem_of_mem_nsmul {a : α} {s : Multiset α} {n : ℕ} (h : a ∈ n • s) : a ∈ s := by - induction' n with n ih - · rw [zero_nsmul] at h - exact absurd h (not_mem_zero _) - · rw [succ_nsmul, mem_add] at h - exact h.elim ih id - -@[simp] -theorem mem_nsmul {a : α} {s : Multiset α} {n : ℕ} : a ∈ n • s ↔ n ≠ 0 ∧ a ∈ s := by - refine ⟨fun ha ↦ ⟨?_, mem_of_mem_nsmul ha⟩, fun h => ?_⟩ - · rintro rfl - simp [zero_nsmul] at ha - obtain ⟨n, rfl⟩ := exists_eq_succ_of_ne_zero h.1 - rw [succ_nsmul, mem_add] - exact Or.inr h.2 - -lemma mem_nsmul_of_ne_zero {a : α} {s : Multiset α} {n : ℕ} (h0 : n ≠ 0) : a ∈ n • s ↔ a ∈ s := by - simp [*] - -theorem nsmul_cons {s : Multiset α} (n : ℕ) (a : α) : - n • (a ::ₘ s) = n • ({a} : Multiset α) + n • s := by - rw [← singleton_add, nsmul_add] +end add /-! ### Cardinality -/ /-- The cardinality of a multiset is the sum of the multiplicities of all its elements, or simply the length of the underlying list. -/ -def card : Multiset α →+ ℕ where - toFun s := (Quot.liftOn s length) fun _l₁ _l₂ => Perm.length_eq - map_zero' := rfl - map_add' s t := Quotient.inductionOn₂ s t length_append +def card : Multiset α → ℕ := Quot.lift length fun _l₁ _l₂ => Perm.length_eq @[simp] theorem coe_card (l : List α) : card (l : Multiset α) = length l := @@ -682,17 +675,9 @@ theorem length_toList (s : Multiset α) : s.toList.length = card s := by theorem card_zero : @card α 0 = 0 := rfl +@[simp] theorem card_add (s t : Multiset α) : card (s + t) = card s + card t := - card.map_add s t - -/-- `Multiset.card` bundled as a group hom. -/ -@[simps] -def cardHom : Multiset α →+ ℕ where - toFun := card - map_zero' := card_zero - map_add' := card_add - -lemma card_nsmul (s : Multiset α) (n : ℕ) : card (n • s) = n * card s := cardHom.map_nsmul .. + Quotient.inductionOn₂ s t length_append @[simp] theorem card_cons (a : α) (s : Multiset α) : card (a ::ₘ s) = card s + 1 := @@ -700,7 +685,7 @@ theorem card_cons (a : α) (s : Multiset α) : card (a ::ₘ s) = card s + 1 := @[simp] theorem card_singleton (a : α) : card ({a} : Multiset α) = 1 := by - simp only [← cons_zero, card_zero, eq_self_iff_true, zero_add, card_cons] + simp only [← cons_zero, card_zero, eq_self_iff_true, Multiset.zero_add, card_cons] theorem card_pair (a b : α) : card {a, b} = 2 := by rw [insert_eq_cons, card_cons, card_singleton] @@ -824,13 +809,6 @@ theorem coe_replicate (n : ℕ) (a : α) : (List.replicate n a : Multiset α) = theorem replicate_add (m n : ℕ) (a : α) : replicate (m + n) a = replicate m a + replicate n a := congr_arg _ <| List.replicate_add .. -/-- `Multiset.replicate` as an `AddMonoidHom`. -/ -@[simps] -def replicateAddMonoidHom (a : α) : ℕ →+ Multiset α where - toFun := fun n => replicate n a - map_zero' := replicate_zero a - map_add' := fun _ _ => replicate_add _ _ a - theorem replicate_one (a : α) : replicate 1 a = {a} := rfl @[simp] theorem card_replicate (n) (a : α) : card (replicate n a) = n := @@ -869,12 +847,6 @@ theorem replicate_subset_singleton (n : ℕ) (a : α) : replicate n a ⊆ {a} := theorem replicate_le_coe {a : α} {n} {l : List α} : replicate n a ≤ l ↔ List.replicate n a <+ l := ⟨fun ⟨_l', p, s⟩ => perm_replicate.1 p ▸ s, Sublist.subperm⟩ -theorem nsmul_replicate {a : α} (n m : ℕ) : n • replicate m a = replicate (n * m) a := - ((replicateAddMonoidHom a).map_nsmul _ _).symm - -theorem nsmul_singleton (a : α) (n) : n • ({a} : Multiset α) = replicate n a := by - rw [← replicate_one, nsmul_replicate, mul_one] - theorem replicate_le_replicate (a : α) {k n : ℕ} : replicate k a ≤ replicate n a ↔ k ≤ n := _root_.trans (by rw [← replicate_le_coe, coe_replicate]) (List.replicate_sublist_replicate a) @@ -949,7 +921,8 @@ theorem le_cons_erase (s : Multiset α) (a : α) : s ≤ a ::ₘ s.erase a := else by rw [erase_of_not_mem h]; apply le_cons_self theorem add_singleton_eq_iff {s t : Multiset α} {a : α} : s + {a} = t ↔ a ∈ t ∧ s = t.erase a := by - rw [add_comm, singleton_add]; constructor + rw [Multiset.add_comm, singleton_add] + constructor · rintro rfl exact ⟨s.mem_cons_self a, (s.erase_cons_head a).symm⟩ · rintro ⟨h, rfl⟩ @@ -958,15 +931,15 @@ theorem add_singleton_eq_iff {s t : Multiset α} {a : α} : s + {a} = t ↔ a theorem erase_add_left_pos {a : α} {s : Multiset α} (t) : a ∈ s → (s + t).erase a = s.erase a + t := Quotient.inductionOn₂ s t fun _l₁ l₂ h => congr_arg _ <| erase_append_left l₂ h -theorem erase_add_right_pos {a : α} (s) {t : Multiset α} (h : a ∈ t) : - (s + t).erase a = s + t.erase a := by rw [add_comm, erase_add_left_pos s h, add_comm] +theorem erase_add_right_pos {a : α} (s) (h : a ∈ t) : (s + t).erase a = s + t.erase a := by + rw [Multiset.add_comm, erase_add_left_pos s h, Multiset.add_comm] theorem erase_add_right_neg {a : α} {s : Multiset α} (t) : a ∉ s → (s + t).erase a = s + t.erase a := Quotient.inductionOn₂ s t fun _l₁ l₂ h => congr_arg _ <| erase_append_right l₂ h -theorem erase_add_left_neg {a : α} (s) {t : Multiset α} (h : a ∉ t) : - (s + t).erase a = s.erase a + t := by rw [add_comm, erase_add_right_neg s h, add_comm] +theorem erase_add_left_neg {a : α} (s) (h : a ∉ t) : (s + t).erase a = s.erase a + t := by + rw [Multiset.add_comm, erase_add_right_neg s h, Multiset.add_comm] theorem erase_le (a : α) (s : Multiset α) : s.erase a ≤ s := Quot.inductionOn s fun l => (erase_sublist a l).subperm @@ -1085,20 +1058,6 @@ instance canLift (c) (p) [CanLift α β c p] : lift l to List β using hl exact ⟨l, map_coe _ _⟩ -/-- `Multiset.map` as an `AddMonoidHom`. -/ -def mapAddMonoidHom (f : α → β) : Multiset α →+ Multiset β where - toFun := map f - map_zero' := map_zero _ - map_add' := map_add _ - -@[simp] -theorem coe_mapAddMonoidHom (f : α → β) : - (mapAddMonoidHom f : Multiset α → Multiset β) = map f := - rfl - -theorem map_nsmul (f : α → β) (n : ℕ) (s) : map f (n • s) = n • map f s := - (mapAddMonoidHom f).map_nsmul _ _ - @[simp] theorem mem_map {f : α → β} {b : β} {s : Multiset α} : b ∈ map f s ↔ ∃ a, a ∈ s ∧ f a = b := Quot.inductionOn s fun _l => List.mem_map @@ -1451,263 +1410,6 @@ instance decidableDexistsMultiset {p : ∀ a ∈ m, Prop} [_hp : ∀ (a) (h : a end DecidablePiExists -/-! ### Subtraction -/ - - -section - -variable [DecidableEq α] {s t u : Multiset α} {a : α} - -/-- `s - t` is the multiset such that `count a (s - t) = count a s - count a t` for all `a` - (note that it is truncated subtraction, so it is `0` if `count a t ≥ count a s`). -/ -protected def sub (s t : Multiset α) : Multiset α := - (Quotient.liftOn₂ s t fun l₁ l₂ => (l₁.diff l₂ : Multiset α)) fun _v₁ _v₂ _w₁ _w₂ p₁ p₂ => - Quot.sound <| p₁.diff p₂ - -instance : Sub (Multiset α) := - ⟨Multiset.sub⟩ - -@[simp] -theorem coe_sub (s t : List α) : (s - t : Multiset α) = (s.diff t : List α) := - rfl - -/-- This is a special case of `tsub_zero`, which should be used instead of this. - This is needed to prove `OrderedSub (Multiset α)`. -/ -protected theorem sub_zero (s : Multiset α) : s - 0 = s := - Quot.inductionOn s fun _l => rfl - -@[simp] -theorem sub_cons (a : α) (s t : Multiset α) : s - a ::ₘ t = s.erase a - t := - Quotient.inductionOn₂ s t fun _l₁ _l₂ => congr_arg _ <| diff_cons _ _ _ - -protected theorem zero_sub (t : Multiset α) : 0 - t = 0 := - Multiset.induction_on t rfl fun a s ih => by simp [ih] - -/-- This is a special case of `tsub_le_iff_right`, which should be used instead of this. - This is needed to prove `OrderedSub (Multiset α)`. -/ -protected theorem sub_le_iff_le_add : s - t ≤ u ↔ s ≤ u + t := by - revert s - exact @(Multiset.induction_on t (by simp [Multiset.sub_zero]) fun a t IH s => by - simp [IH, erase_le_iff_le_cons]) - -protected theorem sub_le_self (s t : Multiset α) : s - t ≤ s := by - rw [Multiset.sub_le_iff_le_add] - exact le_add_right _ _ - -instance : OrderedSub (Multiset α) := - ⟨fun _n _m _k => Multiset.sub_le_iff_le_add⟩ - -instance : ExistsAddOfLE (Multiset α) where - exists_add_of_le h := leInductionOn h fun s => - let ⟨l, p⟩ := s.exists_perm_append - ⟨l, Quot.sound p⟩ - -theorem cons_sub_of_le (a : α) {s t : Multiset α} (h : t ≤ s) : a ::ₘ s - t = a ::ₘ (s - t) := by - rw [← singleton_add, ← singleton_add, add_tsub_assoc_of_le h] - -theorem sub_eq_fold_erase (s t : Multiset α) : s - t = foldl erase s t := - Quotient.inductionOn₂ s t fun l₁ l₂ => by - show ofList (l₁.diff l₂) = foldl erase l₁ l₂ - rw [diff_eq_foldl l₁ l₂] - symm - exact foldl_hom _ _ _ _ _ fun x y => rfl - -@[simp] -theorem card_sub {s t : Multiset α} (h : t ≤ s) : card (s - t) = card s - card t := - Nat.eq_sub_of_add_eq <| by rw [← card_add, tsub_add_cancel_of_le h] - -/-! ### Union -/ - - -/-- `s ∪ t` is the lattice join operation with respect to the - multiset `≤`. The multiplicity of `a` in `s ∪ t` is the maximum - of the multiplicities in `s` and `t`. -/ -def union (s t : Multiset α) : Multiset α := - s - t + t - -instance : Union (Multiset α) := - ⟨union⟩ - -theorem union_def (s t : Multiset α) : s ∪ t = s - t + t := - rfl - -theorem le_union_left (s t : Multiset α) : s ≤ s ∪ t := - le_tsub_add - -theorem le_union_right (s t : Multiset α) : t ≤ s ∪ t := - le_add_left _ _ - -theorem eq_union_left : t ≤ s → s ∪ t = s := - tsub_add_cancel_of_le - -@[gcongr] -theorem union_le_union_right (h : s ≤ t) (u) : s ∪ u ≤ t ∪ u := - add_le_add_right (tsub_le_tsub_right h _) u - -theorem union_le (h₁ : s ≤ u) (h₂ : t ≤ u) : s ∪ t ≤ u := by - rw [← eq_union_left h₂]; exact union_le_union_right h₁ t - - -@[simp] -theorem mem_union : a ∈ s ∪ t ↔ a ∈ s ∨ a ∈ t := - ⟨fun h => (mem_add.1 h).imp_left (mem_of_le <| Multiset.sub_le_self _ _), - (Or.elim · (mem_of_le <| le_union_left _ _) (mem_of_le <| le_union_right _ _))⟩ - -@[simp] -theorem map_union [DecidableEq β] {f : α → β} (finj : Function.Injective f) {s t : Multiset α} : - map f (s ∪ t) = map f s ∪ map f t := - Quotient.inductionOn₂ s t fun l₁ l₂ => - congr_arg ofList (by rw [List.map_append f, List.map_diff finj]) - -@[simp] theorem zero_union : 0 ∪ s = s := by - simp [union_def, Multiset.zero_sub] - -@[simp] theorem union_zero : s ∪ 0 = s := by - simp [union_def] - -/-! ### Intersection -/ - -/-- `s ∩ t` is the lattice meet operation with respect to the - multiset `≤`. The multiplicity of `a` in `s ∩ t` is the minimum - of the multiplicities in `s` and `t`. -/ -def inter (s t : Multiset α) : Multiset α := - Quotient.liftOn₂ s t (fun l₁ l₂ => (l₁.bagInter l₂ : Multiset α)) fun _v₁ _v₂ _w₁ _w₂ p₁ p₂ => - Quot.sound <| p₁.bagInter p₂ - -instance : Inter (Multiset α) := - ⟨inter⟩ - -@[simp] -theorem inter_zero (s : Multiset α) : s ∩ 0 = 0 := - Quot.inductionOn s fun l => congr_arg ofList l.bagInter_nil - -@[simp] -theorem zero_inter (s : Multiset α) : 0 ∩ s = 0 := - Quot.inductionOn s fun l => congr_arg ofList l.nil_bagInter - -@[simp] -theorem cons_inter_of_pos {a} (s : Multiset α) {t} : a ∈ t → (a ::ₘ s) ∩ t = a ::ₘ s ∩ t.erase a := - Quotient.inductionOn₂ s t fun _l₁ _l₂ h => congr_arg ofList <| cons_bagInter_of_pos _ h - -@[simp] -theorem cons_inter_of_neg {a} (s : Multiset α) {t} : a ∉ t → (a ::ₘ s) ∩ t = s ∩ t := - Quotient.inductionOn₂ s t fun _l₁ _l₂ h => congr_arg ofList <| cons_bagInter_of_neg _ h - -theorem inter_le_left (s t : Multiset α) : s ∩ t ≤ s := - Quotient.inductionOn₂ s t fun _l₁ _l₂ => (bagInter_sublist_left _ _).subperm - -theorem inter_le_right (s : Multiset α) : ∀ t, s ∩ t ≤ t := - Multiset.induction_on s (fun t => (zero_inter t).symm ▸ zero_le _) fun a s IH t => - if h : a ∈ t then by simpa [h] using cons_le_cons a (IH (t.erase a)) else by simp [h, IH] - -theorem le_inter (h₁ : s ≤ t) (h₂ : s ≤ u) : s ≤ t ∩ u := by - revert s u; refine @(Multiset.induction_on t ?_ fun a t IH => ?_) <;> intros s u h₁ h₂ - · simpa only [zero_inter] using h₁ - by_cases h : a ∈ u - · rw [cons_inter_of_pos _ h, ← erase_le_iff_le_cons] - exact IH (erase_le_iff_le_cons.2 h₁) (erase_le_erase _ h₂) - · rw [cons_inter_of_neg _ h] - exact IH ((le_cons_of_not_mem <| mt (mem_of_le h₂) h).1 h₁) h₂ - -@[simp] -theorem mem_inter : a ∈ s ∩ t ↔ a ∈ s ∧ a ∈ t := - ⟨fun h => ⟨mem_of_le (inter_le_left _ _) h, mem_of_le (inter_le_right _ _) h⟩, fun ⟨h₁, h₂⟩ => by - rw [← cons_erase h₁, cons_inter_of_pos _ h₂]; apply mem_cons_self⟩ - -instance : Lattice (Multiset α) := - { sup := (· ∪ ·) - sup_le := @union_le _ _ - le_sup_left := le_union_left - le_sup_right := le_union_right - inf := (· ∩ ·) - le_inf := @le_inter _ _ - inf_le_left := inter_le_left - inf_le_right := inter_le_right } - -@[simp] -theorem sup_eq_union (s t : Multiset α) : s ⊔ t = s ∪ t := - rfl - -@[simp] -theorem inf_eq_inter (s t : Multiset α) : s ⊓ t = s ∩ t := - rfl - -@[simp] -theorem le_inter_iff : s ≤ t ∩ u ↔ s ≤ t ∧ s ≤ u := - le_inf_iff - -@[simp] -theorem union_le_iff : s ∪ t ≤ u ↔ s ≤ u ∧ t ≤ u := - sup_le_iff - -theorem union_comm (s t : Multiset α) : s ∪ t = t ∪ s := sup_comm _ _ - -theorem inter_comm (s t : Multiset α) : s ∩ t = t ∩ s := inf_comm _ _ - -theorem eq_union_right (h : s ≤ t) : s ∪ t = t := by rw [union_comm, eq_union_left h] - -@[gcongr] -theorem union_le_union_left (h : s ≤ t) (u) : u ∪ s ≤ u ∪ t := - sup_le_sup_left h _ - -theorem union_le_add (s t : Multiset α) : s ∪ t ≤ s + t := - union_le (le_add_right _ _) (le_add_left _ _) - -theorem union_add_distrib (s t u : Multiset α) : s ∪ t + u = s + u ∪ (t + u) := by - simpa [(· ∪ ·), union, eq_comm, add_assoc] using - show s + u - (t + u) = s - t by rw [add_comm t, tsub_add_eq_tsub_tsub, add_tsub_cancel_right] - -theorem add_union_distrib (s t u : Multiset α) : s + (t ∪ u) = s + t ∪ (s + u) := by - rw [add_comm, union_add_distrib, add_comm s, add_comm s] - -theorem cons_union_distrib (a : α) (s t : Multiset α) : a ::ₘ (s ∪ t) = a ::ₘ s ∪ a ::ₘ t := by - simpa using add_union_distrib (a ::ₘ 0) s t - -theorem inter_add_distrib (s t u : Multiset α) : s ∩ t + u = (s + u) ∩ (t + u) := by - by_contra h - cases' - lt_iff_cons_le.1 - (lt_of_le_of_ne - (le_inter (add_le_add_right (inter_le_left s t) u) - (add_le_add_right (inter_le_right s t) u)) - h) with - a hl - rw [← cons_add] at hl - exact - not_le_of_lt (lt_cons_self (s ∩ t) a) - (le_inter (le_of_add_le_add_right (le_trans hl (inter_le_left _ _))) - (le_of_add_le_add_right (le_trans hl (inter_le_right _ _)))) - -theorem add_inter_distrib (s t u : Multiset α) : s + t ∩ u = (s + t) ∩ (s + u) := by - rw [add_comm, inter_add_distrib, add_comm s, add_comm s] - -theorem cons_inter_distrib (a : α) (s t : Multiset α) : a ::ₘ s ∩ t = (a ::ₘ s) ∩ (a ::ₘ t) := by - simp - -theorem union_add_inter (s t : Multiset α) : s ∪ t + s ∩ t = s + t := by - apply _root_.le_antisymm - · rw [union_add_distrib] - refine union_le (add_le_add_left (inter_le_right _ _) _) ?_ - rw [add_comm] - exact add_le_add_right (inter_le_left _ _) _ - · rw [add_comm, add_inter_distrib] - refine le_inter (add_le_add_right (le_union_right _ _) _) ?_ - rw [add_comm] - exact add_le_add_right (le_union_left _ _) _ - -theorem sub_add_inter (s t : Multiset α) : s - t + s ∩ t = s := by - rw [inter_comm] - revert s; refine Multiset.induction_on t (by simp) fun a t IH s => ?_ - by_cases h : a ∈ s - · rw [cons_inter_of_pos _ h, sub_cons, add_cons, IH, cons_erase h] - · rw [cons_inter_of_neg _ h, sub_cons, erase_of_not_mem h, IH] - -theorem sub_inter (s t : Multiset α) : s - s ∩ t = s - t := - add_right_cancel (b := s ∩ t) <| by - rw [sub_add_inter s t, tsub_add_cancel_of_le (inter_le_left s t)] - -end - /-! ### `Multiset.filter` -/ @@ -1794,57 +1496,14 @@ theorem filter_cons {a : α} (s : Multiset α) : filter p (a ::ₘ s) = (if p a then {a} else 0) + filter p s := by split_ifs with h · rw [filter_cons_of_pos _ h, singleton_add] - · rw [filter_cons_of_neg _ h, zero_add] + · rw [filter_cons_of_neg _ h, Multiset.zero_add] theorem filter_singleton {a : α} (p : α → Prop) [DecidablePred p] : filter p {a} = if p a then {a} else ∅ := by - simp only [singleton, filter_cons, filter_zero, add_zero, empty_eq_zero] - -theorem filter_nsmul (s : Multiset α) (n : ℕ) : filter p (n • s) = n • filter p s := by - refine s.induction_on ?_ ?_ - · simp only [filter_zero, nsmul_zero] - · intro a ha ih - rw [nsmul_cons, filter_add, ih, filter_cons, nsmul_add] - congr - split_ifs with hp <;> - · simp only [filter_eq_self, nsmul_zero, filter_eq_nil] - intro b hb - rwa [mem_singleton.mp (mem_of_mem_nsmul hb)] + simp only [singleton, filter_cons, filter_zero, Multiset.add_zero, empty_eq_zero] variable (p) -@[simp] -theorem filter_sub [DecidableEq α] (s t : Multiset α) : - filter p (s - t) = filter p s - filter p t := by - revert s; refine Multiset.induction_on t (by simp) fun a t IH s => ?_ - rw [sub_cons, IH] - by_cases h : p a - · rw [filter_cons_of_pos _ h, sub_cons] - congr - by_cases m : a ∈ s - · rw [← cons_inj_right a, ← filter_cons_of_pos _ h, cons_erase (mem_filter_of_mem m h), - cons_erase m] - · rw [erase_of_not_mem m, erase_of_not_mem (mt mem_of_mem_filter m)] - · rw [filter_cons_of_neg _ h] - by_cases m : a ∈ s - · rw [(by rw [filter_cons_of_neg _ h] : filter p (erase s a) = filter p (a ::ₘ erase s a)), - cons_erase m] - · rw [erase_of_not_mem m] - -@[simp] -theorem filter_union [DecidableEq α] (s t : Multiset α) : - filter p (s ∪ t) = filter p s ∪ filter p t := by simp [(· ∪ ·), union] - -@[simp] -theorem filter_inter [DecidableEq α] (s t : Multiset α) : - filter p (s ∩ t) = filter p s ∩ filter p t := - le_antisymm - (le_inter (filter_le_filter _ <| inter_le_left _ _) - (filter_le_filter _ <| inter_le_right _ _)) <| - le_filter.2 - ⟨inf_le_inf (filter_le _ _) (filter_le _ _), fun _a h => - of_mem_filter (mem_of_le (inter_le_left _ _) h)⟩ - @[simp] theorem filter_filter (q) [DecidablePred q] (s : Multiset α) : filter p (filter q s) = filter (fun a => p a ∧ q a) s := @@ -1859,7 +1518,7 @@ theorem filter_add_filter (q) [DecidablePred q] (s : Multiset α) : theorem filter_add_not (s : Multiset α) : filter p s + filter (fun a => ¬p a) s = s := by rw [filter_add_filter, filter_eq_self.2, filter_eq_nil.2] - · simp only [add_zero] + · simp only [Multiset.add_zero] · simp [Decidable.em, -Bool.not_eq_true, -not_and, not_and_or, or_comm] · simp only [Bool.not_eq_true, decide_eq_true_eq, Bool.eq_false_or_eq_true, decide_true, implies_true, Decidable.em] @@ -1969,13 +1628,9 @@ theorem filterMap_le_filterMap (f : α → Option β) {s t : Multiset α} (h : s def countP (s : Multiset α) : ℕ := Quot.liftOn s (List.countP p) fun _l₁ _l₂ => Perm.countP_eq (p ·) -@[simp] -theorem coe_countP (l : List α) : countP p l = l.countP p := - rfl +@[simp] lemma coe_countP (l : List α) : countP p l = l.countP p := rfl -@[simp] -theorem countP_zero : countP p 0 = 0 := - rfl +@[simp] lemma countP_zero : countP p 0 = 0 := rfl variable {p} @@ -2002,29 +1657,9 @@ theorem countP_le_card (s) : countP p s ≤ card s := theorem countP_add (s t) : countP p (s + t) = countP p s + countP p t := by simp [countP_eq_card_filter] -@[simp] -theorem countP_nsmul (s) (n : ℕ) : countP p (n • s) = n * countP p s := by - induction n <;> simp [*, succ_nsmul, succ_mul, zero_nsmul] - theorem card_eq_countP_add_countP (s) : card s = countP p s + countP (fun x => ¬p x) s := Quot.inductionOn s fun l => by simp [l.length_eq_countP_add_countP p] -/-- `countP p`, the number of elements of a multiset satisfying `p`, promoted to an -`AddMonoidHom`. -/ -def countPAddMonoidHom : Multiset α →+ ℕ where - toFun := countP p - map_zero' := countP_zero _ - map_add' := countP_add _ - -@[simp] -theorem coe_countPAddMonoidHom : (countPAddMonoidHom p : Multiset α → ℕ) = countP p := - rfl - -@[simp] -theorem countP_sub [DecidableEq α] {s t : Multiset α} (h : t ≤ s) : - countP p (s - t) = countP p s - countP p t := by - simp [countP_eq_card_filter, h, filter_le_filter] - @[gcongr] theorem countP_le_of_le {s t} (h : s ≤ t) : countP p s ≤ countP p t := by simpa [countP_eq_card_filter] using card_le_card (filter_le_filter p h) @@ -2052,7 +1687,7 @@ theorem countP_map (f : α → β) (s : Multiset α) (p : β → Prop) [Decidabl refine Multiset.induction_on s ?_ fun a t IH => ?_ · rw [map_zero, countP_zero, filter_zero, card_zero] · rw [map_cons, countP_cons, IH, filter_cons, card_add, apply_ite card, card_zero, card_singleton, - add_comm] + Nat.add_comm] -- Porting note: `Lean.Internal.coeM` forces us to type-ascript `{a // a ∈ s}` lemma countP_attach (s : Multiset α) : s.attach.countP (fun a : {a // a ∈ s} ↦ p a) = s.countP p := @@ -2103,7 +1738,7 @@ end section -variable [DecidableEq α] {s : Multiset α} +variable [DecidableEq α] {s t u : Multiset α} /-- `count a s` is the multiplicity of `a` in `s`. -/ def count (a : α) : Multiset α → ℕ := @@ -2144,24 +1779,12 @@ theorem count_singleton_self (a : α) : count a ({a} : Multiset α) = 1 := count_eq_one_of_mem (nodup_singleton a) <| mem_singleton_self a theorem count_singleton (a b : α) : count a ({b} : Multiset α) = if a = b then 1 else 0 := by - simp only [count_cons, ← cons_zero, count_zero, zero_add] + simp only [count_cons, ← cons_zero, count_zero, Nat.zero_add] @[simp] theorem count_add (a : α) : ∀ s t, count a (s + t) = count a s + count a t := countP_add _ -/-- `count a`, the multiplicity of `a` in a multiset, promoted to an `AddMonoidHom`. -/ -def countAddMonoidHom (a : α) : Multiset α →+ ℕ := - countPAddMonoidHom (a = ·) - -@[simp] -theorem coe_countAddMonoidHom {a : α} : (countAddMonoidHom a : Multiset α → ℕ) = count a := - rfl - -@[simp] -theorem count_nsmul (a : α) (n s) : count a (n • s) = n * count a s := by - induction n <;> simp [*, succ_nsmul, succ_mul, zero_nsmul] - @[simp] lemma count_attach (a : {x // x ∈ s}) : s.attach.count a = s.count ↑a := Eq.trans (countP_congr rfl fun _ _ => by simp [Subtype.ext_iff]) <| countP_attach _ _ @@ -2203,23 +1826,6 @@ theorem count_erase_of_ne {a b : α} (ab : a ≠ b) (s : Multiset α) : Quotient.inductionOn s fun l => by convert List.count_erase_of_ne ab l <;> rw [← coe_count] <;> simp -@[simp] -theorem count_sub (a : α) (s t : Multiset α) : count a (s - t) = count a s - count a t := by - revert s; refine Multiset.induction_on t (by simp) fun b t IH s => ?_ - rw [sub_cons, IH] - rcases Decidable.eq_or_ne a b with rfl | ab - · rw [count_erase_self, count_cons_self, Nat.sub_sub, add_comm] - · rw [count_erase_of_ne ab, count_cons_of_ne ab] - -@[simp] -theorem count_union (a : α) (s t : Multiset α) : count a (s ∪ t) = max (count a s) (count a t) := by - simp [(· ∪ ·), union, Nat.sub_add_eq_max] - -@[simp] -theorem count_inter (a : α) (s t : Multiset α) : count a (s ∩ t) = min (count a s) (count a t) := by - apply @Nat.add_left_cancel (count a (s - t)) - rw [← count_add, sub_add_inter, count_sub, Nat.sub_add_min_cancel] - theorem le_count_iff_replicate_le {a : α} {s : Multiset α} {n : ℕ} : n ≤ count a s ↔ replicate n a ≤ s := Quot.inductionOn s fun _l => by @@ -2257,20 +1863,8 @@ theorem ext' {s t : Multiset α} : (∀ a, count a s = count a t) → s = t := lemma count_injective : Injective fun (s : Multiset α) a ↦ s.count a := fun _s _t hst ↦ ext' <| congr_fun hst -@[simp] -theorem coe_inter (s t : List α) : (s ∩ t : Multiset α) = (s.bagInter t : List α) := by ext; simp - theorem le_iff_count {s t : Multiset α} : s ≤ t ↔ ∀ a, count a s ≤ count a t := - ⟨fun h a => count_le_of_le a h, fun al => by - rw [← (ext.2 fun a => by simp [max_eq_right (al a)] : s ∪ t = t)]; apply le_union_left⟩ - -instance : DistribLattice (Multiset α) := - { le_sup_inf := fun s t u => - le_of_eq <| - Eq.symm <| - ext.2 fun a => by - simp only [max_min_distrib_left, Multiset.count_inter, Multiset.sup_eq_union, - Multiset.count_union, Multiset.inf_eq_inter] } + Quotient.inductionOn₂ s t fun _ _ ↦ by simp [subperm_iff_count] theorem count_map {α β : Type*} (f : α → β) (s : Multiset α) [DecidableEq β] (b : β) : count b (map f s) = card (s.filter fun a => b = f a) := by @@ -2297,11 +1891,6 @@ theorem count_map_eq_count' [DecidableEq β] (f : α → β) (s : Multiset α) ( rw [hf hkx] at hks contradiction -@[simp] -theorem sub_filter_eq_filter_not (p) [DecidablePred p] (s : Multiset α) : - s - s.filter p = s.filter (fun a ↦ ¬ p a) := by - ext a; by_cases h : p a <;> simp [h] - theorem filter_eq' (s : Multiset α) (b : α) : s.filter (· = b) = replicate (count b s) b := Quotient.inductionOn s fun l => by simp only [quot_mk_to_coe, filter_coe, mem_coe, coe_count] @@ -2310,6 +1899,353 @@ theorem filter_eq' (s : Multiset α) (b : α) : s.filter (· = b) = replicate (c theorem filter_eq (s : Multiset α) (b : α) : s.filter (Eq b) = replicate (count b s) b := by simp_rw [← filter_eq', eq_comm] +theorem erase_attach_map_val (s : Multiset α) (x : {x // x ∈ s}) : + (s.attach.erase x).map (↑) = s.erase x := by + rw [Multiset.map_erase _ val_injective, attach_map_val] + +theorem erase_attach_map (s : Multiset α) (f : α → β) (x : {x // x ∈ s}) : + (s.attach.erase x).map (fun j : {x // x ∈ s} ↦ f j) = (s.erase x).map f := by + simp only [← Function.comp_apply (f := f)] + rw [← map_map, erase_attach_map_val] + +omit [DecidableEq α] in +protected lemma add_left_inj : s + u = t + u ↔ s = t := by classical simp [Multiset.ext] + +omit [DecidableEq α] in +protected lemma add_right_inj : s + t = s + u ↔ t = u := by classical simp [Multiset.ext] + +end + +/-! ### Subtraction -/ + +section sub +variable [DecidableEq α] {s t u : Multiset α} {a : α} + +/-- `s - t` is the multiset such that `count a (s - t) = count a s - count a t` for all `a` + (note that it is truncated subtraction, so it is `0` if `count a t ≥ count a s`). -/ +protected def sub (s t : Multiset α) : Multiset α := + (Quotient.liftOn₂ s t fun l₁ l₂ => (l₁.diff l₂ : Multiset α)) fun _v₁ _v₂ _w₁ _w₂ p₁ p₂ => + Quot.sound <| p₁.diff p₂ + +instance : Sub (Multiset α) := + ⟨Multiset.sub⟩ + +@[simp] +theorem coe_sub (s t : List α) : (s - t : Multiset α) = (s.diff t : List α) := + rfl + +/-- This is a special case of `tsub_zero`, which should be used instead of this. + This is needed to prove `OrderedSub (Multiset α)`. -/ +@[simp, nolint simpNF] -- We want to use this lemma earlier than the lemma simp can prove it with +protected theorem sub_zero (s : Multiset α) : s - 0 = s := + Quot.inductionOn s fun _l => rfl + +@[simp] +theorem sub_cons (a : α) (s t : Multiset α) : s - a ::ₘ t = s.erase a - t := + Quotient.inductionOn₂ s t fun _l₁ _l₂ => congr_arg _ <| diff_cons _ _ _ + +protected theorem zero_sub (t : Multiset α) : 0 - t = 0 := + Multiset.induction_on t rfl fun a s ih => by simp [ih] + +@[simp] +theorem countP_sub {s t : Multiset α} : + t ≤ s → ∀ (p : α → Prop) [DecidablePred p], countP p (s - t) = countP p s - countP p t := + Quotient.inductionOn₂ s t fun _l₁ _l₂ hl _ _ ↦ List.countP_diff hl _ + +@[simp] +theorem count_sub (a : α) (s t : Multiset α) : count a (s - t) = count a s - count a t := + Quotient.inductionOn₂ s t <| by simp [List.count_diff] + +/-- This is a special case of `tsub_le_iff_right`, which should be used instead of this. +This is needed to prove `OrderedSub (Multiset α)`. -/ +protected theorem sub_le_iff_le_add : s - t ≤ u ↔ s ≤ u + t := by + revert s + exact @(Multiset.induction_on t (by simp [Multiset.sub_zero]) fun a t IH s => by + simp [IH, erase_le_iff_le_cons]) + +/-- This is a special case of `tsub_le_iff_left`, which should be used instead of this. -/ +protected lemma sub_le_iff_le_add' : s - t ≤ u ↔ s ≤ t + u := by + rw [Multiset.sub_le_iff_le_add, Multiset.add_comm] + +protected theorem sub_le_self (s t : Multiset α) : s - t ≤ s := by + rw [Multiset.sub_le_iff_le_add] + exact le_add_right _ _ + +protected lemma add_sub_assoc (hut : u ≤ t) : s + t - u = s + (t - u) := by + ext a; simp [Nat.add_sub_assoc <| count_le_of_le _ hut] + +protected lemma add_sub_cancel (hts : t ≤ s) : s - t + t = s := by + ext a; simp [Nat.sub_add_cancel <| count_le_of_le _ hts] + +protected lemma sub_add_cancel (hts : t ≤ s) : s - t + t = s := by + ext a; simp [Nat.sub_add_cancel <| count_le_of_le _ hts] + +protected lemma sub_add_eq_sub_sub : s - (t + u) = s - t - u := by ext; simp [Nat.sub_add_eq] + +protected lemma le_sub_add : s ≤ s - t + t := Multiset.sub_le_iff_le_add.1 le_rfl +protected lemma le_add_sub : s ≤ t + (s - t) := Multiset.sub_le_iff_le_add'.1 le_rfl + +protected lemma sub_le_sub_right (hst : s ≤ t) : s - u ≤ t - u := + Multiset.sub_le_iff_le_add'.mpr <| hst.trans Multiset.le_add_sub + +protected lemma add_sub_cancel_right : s + t - t = s := by ext a; simp + +protected lemma eq_sub_of_add_eq (hstu : s + t = u) : s = u - t := by + rw [← hstu, Multiset.add_sub_cancel_right] + +@[simp] +theorem filter_sub (p : α → Prop) [DecidablePred p] (s t : Multiset α) : + filter p (s - t) = filter p s - filter p t := by + revert s; refine Multiset.induction_on t (by simp) fun a t IH s => ?_ + rw [sub_cons, IH] + by_cases h : p a + · rw [filter_cons_of_pos _ h, sub_cons] + congr + by_cases m : a ∈ s + · rw [← cons_inj_right a, ← filter_cons_of_pos _ h, cons_erase (mem_filter_of_mem m h), + cons_erase m] + · rw [erase_of_not_mem m, erase_of_not_mem (mt mem_of_mem_filter m)] + · rw [filter_cons_of_neg _ h] + by_cases m : a ∈ s + · rw [(by rw [filter_cons_of_neg _ h] : filter p (erase s a) = filter p (a ::ₘ erase s a)), + cons_erase m] + · rw [erase_of_not_mem m] + +@[simp] +theorem sub_filter_eq_filter_not (p) [DecidablePred p] (s : Multiset α) : + s - s.filter p = s.filter fun a ↦ ¬ p a := by + rw [← filter_add_not p s] + ext a; by_cases h : p a <;> simp [h] + +theorem cons_sub_of_le (a : α) {s t : Multiset α} (h : t ≤ s) : a ::ₘ s - t = a ::ₘ (s - t) := by + rw [← singleton_add, ← singleton_add, Multiset.add_sub_assoc h] + +theorem sub_eq_fold_erase (s t : Multiset α) : s - t = foldl erase s t := + Quotient.inductionOn₂ s t fun l₁ l₂ => by + show ofList (l₁.diff l₂) = foldl erase l₁ l₂ + rw [diff_eq_foldl l₁ l₂] + symm + exact foldl_hom _ _ _ _ _ fun x y => rfl + +@[simp] +theorem card_sub {s t : Multiset α} (h : t ≤ s) : card (s - t) = card s - card t := + Nat.eq_sub_of_add_eq <| by rw [← card_add, Multiset.sub_add_cancel h] + +/-! ### Union -/ + +/-- `s ∪ t` is the lattice join operation with respect to the + multiset `≤`. The multiplicity of `a` in `s ∪ t` is the maximum + of the multiplicities in `s` and `t`. -/ +def union (s t : Multiset α) : Multiset α := + s - t + t + +instance : Union (Multiset α) := + ⟨union⟩ + +theorem union_def (s t : Multiset α) : s ∪ t = s - t + t := + rfl + +theorem le_union_left (s t : Multiset α) : s ≤ s ∪ t := Multiset.le_sub_add +theorem le_union_right (s t : Multiset α) : t ≤ s ∪ t := le_add_left _ _ + +theorem eq_union_left : t ≤ s → s ∪ t = s := Multiset.sub_add_cancel + +@[gcongr] +theorem union_le_union_right (h : s ≤ t) (u) : s ∪ u ≤ t ∪ u := + Multiset.add_le_add_right (Multiset.sub_le_sub_right h) + +theorem union_le (h₁ : s ≤ u) (h₂ : t ≤ u) : s ∪ t ≤ u := by + rw [← eq_union_left h₂]; exact union_le_union_right h₁ t + +@[simp] +theorem mem_union : a ∈ s ∪ t ↔ a ∈ s ∨ a ∈ t := + ⟨fun h => (mem_add.1 h).imp_left (mem_of_le <| Multiset.sub_le_self _ _), + (Or.elim · (mem_of_le <| le_union_left _ _) (mem_of_le <| le_union_right _ _))⟩ + +@[simp] +theorem map_union [DecidableEq β] {f : α → β} (finj : Function.Injective f) {s t : Multiset α} : + map f (s ∪ t) = map f s ∪ map f t := + Quotient.inductionOn₂ s t fun l₁ l₂ => + congr_arg ofList (by rw [List.map_append f, List.map_diff finj]) + +@[simp] theorem zero_union : 0 ∪ s = s := by + simp [union_def, Multiset.zero_sub] + +@[simp] theorem union_zero : s ∪ 0 = s := by + simp [union_def] + +@[simp] +theorem count_union (a : α) (s t : Multiset α) : count a (s ∪ t) = max (count a s) (count a t) := by + simp [(· ∪ ·), union, Nat.sub_add_eq_max] + +@[simp] +lemma filter_union (p : α → Prop) [DecidablePred p] (s t : Multiset α) : + filter p (s ∪ t) = filter p s ∪ filter p t := by simp [(· ∪ ·), union] + +/-! ### Intersection -/ + +/-- `s ∩ t` is the lattice meet operation with respect to the + multiset `≤`. The multiplicity of `a` in `s ∩ t` is the minimum + of the multiplicities in `s` and `t`. -/ +def inter (s t : Multiset α) : Multiset α := + Quotient.liftOn₂ s t (fun l₁ l₂ => (l₁.bagInter l₂ : Multiset α)) fun _v₁ _v₂ _w₁ _w₂ p₁ p₂ => + Quot.sound <| p₁.bagInter p₂ + +instance : Inter (Multiset α) := + ⟨inter⟩ + +@[simp] +theorem inter_zero (s : Multiset α) : s ∩ 0 = 0 := + Quot.inductionOn s fun l => congr_arg ofList l.bagInter_nil + +@[simp] +theorem zero_inter (s : Multiset α) : 0 ∩ s = 0 := + Quot.inductionOn s fun l => congr_arg ofList l.nil_bagInter + +@[simp] +theorem cons_inter_of_pos {a} (s : Multiset α) {t} : a ∈ t → (a ::ₘ s) ∩ t = a ::ₘ s ∩ t.erase a := + Quotient.inductionOn₂ s t fun _l₁ _l₂ h => congr_arg ofList <| cons_bagInter_of_pos _ h + +@[simp] +theorem cons_inter_of_neg {a} (s : Multiset α) {t} : a ∉ t → (a ::ₘ s) ∩ t = s ∩ t := + Quotient.inductionOn₂ s t fun _l₁ _l₂ h => congr_arg ofList <| cons_bagInter_of_neg _ h + +theorem inter_le_left (s t : Multiset α) : s ∩ t ≤ s := + Quotient.inductionOn₂ s t fun _l₁ _l₂ => (bagInter_sublist_left _ _).subperm + +theorem inter_le_right (s : Multiset α) : ∀ t, s ∩ t ≤ t := + Multiset.induction_on s (fun t => (zero_inter t).symm ▸ zero_le _) fun a s IH t => + if h : a ∈ t then by simpa [h] using cons_le_cons a (IH (t.erase a)) else by simp [h, IH] + +theorem le_inter (h₁ : s ≤ t) (h₂ : s ≤ u) : s ≤ t ∩ u := by + revert s u; refine @(Multiset.induction_on t ?_ fun a t IH => ?_) <;> intros s u h₁ h₂ + · simpa only [zero_inter] using h₁ + by_cases h : a ∈ u + · rw [cons_inter_of_pos _ h, ← erase_le_iff_le_cons] + exact IH (erase_le_iff_le_cons.2 h₁) (erase_le_erase _ h₂) + · rw [cons_inter_of_neg _ h] + exact IH ((le_cons_of_not_mem <| mt (mem_of_le h₂) h).1 h₁) h₂ + +@[simp] +theorem mem_inter : a ∈ s ∩ t ↔ a ∈ s ∧ a ∈ t := + ⟨fun h => ⟨mem_of_le (inter_le_left _ _) h, mem_of_le (inter_le_right _ _) h⟩, fun ⟨h₁, h₂⟩ => by + rw [← cons_erase h₁, cons_inter_of_pos _ h₂]; apply mem_cons_self⟩ + +instance instLattice : Lattice (Multiset α) where + sup := (· ∪ ·) + sup_le := @union_le _ _ + le_sup_left := le_union_left + le_sup_right := le_union_right + inf := (· ∩ ·) + le_inf := @le_inter _ _ + inf_le_left := inter_le_left + inf_le_right := inter_le_right + +@[simp] +theorem sup_eq_union (s t : Multiset α) : s ⊔ t = s ∪ t := + rfl + +@[simp] +theorem inf_eq_inter (s t : Multiset α) : s ⊓ t = s ∩ t := + rfl + +@[simp] +theorem le_inter_iff : s ≤ t ∩ u ↔ s ≤ t ∧ s ≤ u := + le_inf_iff + +@[simp] +theorem union_le_iff : s ∪ t ≤ u ↔ s ≤ u ∧ t ≤ u := + sup_le_iff + +theorem union_comm (s t : Multiset α) : s ∪ t = t ∪ s := sup_comm _ _ + +theorem inter_comm (s t : Multiset α) : s ∩ t = t ∩ s := inf_comm _ _ + +theorem eq_union_right (h : s ≤ t) : s ∪ t = t := by rw [union_comm, eq_union_left h] + +@[gcongr] +theorem union_le_union_left (h : s ≤ t) (u) : u ∪ s ≤ u ∪ t := + sup_le_sup_left h _ + +theorem union_le_add (s t : Multiset α) : s ∪ t ≤ s + t := + union_le (le_add_right _ _) (le_add_left _ _) + +theorem union_add_distrib (s t u : Multiset α) : s ∪ t + u = s + u ∪ (t + u) := by + simpa [(· ∪ ·), union, eq_comm, Multiset.add_assoc, Multiset.add_left_inj] using + show s + u - (t + u) = s - t by + rw [t.add_comm, Multiset.sub_add_eq_sub_sub, Multiset.add_sub_cancel_right] + +theorem add_union_distrib (s t u : Multiset α) : s + (t ∪ u) = s + t ∪ (s + u) := by + rw [Multiset.add_comm, union_add_distrib, s.add_comm, s.add_comm] + +theorem cons_union_distrib (a : α) (s t : Multiset α) : a ::ₘ (s ∪ t) = a ::ₘ s ∪ a ::ₘ t := by + simpa using add_union_distrib (a ::ₘ 0) s t + +theorem inter_add_distrib (s t u : Multiset α) : s ∩ t + u = (s + u) ∩ (t + u) := by + by_contra h + cases' + lt_iff_cons_le.1 + (lt_of_le_of_ne + (le_inter (Multiset.add_le_add_right (inter_le_left s t)) + (Multiset.add_le_add_right (inter_le_right s t))) + h) with + a hl + rw [← cons_add] at hl + exact + not_le_of_lt (lt_cons_self (s ∩ t) a) + (le_inter (Multiset.le_of_add_le_add_right (le_trans hl (inter_le_left _ _))) + (Multiset.le_of_add_le_add_right (le_trans hl (inter_le_right _ _)))) + +theorem add_inter_distrib (s t u : Multiset α) : s + t ∩ u = (s + t) ∩ (s + u) := by + rw [Multiset.add_comm, inter_add_distrib, s.add_comm, s.add_comm] + +theorem cons_inter_distrib (a : α) (s t : Multiset α) : a ::ₘ s ∩ t = (a ::ₘ s) ∩ (a ::ₘ t) := by + simp + +theorem union_add_inter (s t : Multiset α) : s ∪ t + s ∩ t = s + t := by + apply _root_.le_antisymm + · rw [union_add_distrib] + refine union_le (Multiset.add_le_add_left (inter_le_right _ _)) ?_ + rw [Multiset.add_comm] + exact Multiset.add_le_add_right (inter_le_left _ _) + · rw [Multiset.add_comm, add_inter_distrib] + refine le_inter (Multiset.add_le_add_right (le_union_right _ _)) ?_ + rw [Multiset.add_comm] + exact Multiset.add_le_add_right (le_union_left _ _) + +theorem sub_add_inter (s t : Multiset α) : s - t + s ∩ t = s := by + rw [inter_comm] + revert s; refine Multiset.induction_on t (by simp) fun a t IH s => ?_ + by_cases h : a ∈ s + · rw [cons_inter_of_pos _ h, sub_cons, add_cons, IH, cons_erase h] + · rw [cons_inter_of_neg _ h, sub_cons, erase_of_not_mem h, IH] + +theorem sub_inter (s t : Multiset α) : s - s ∩ t = s - t := + (Multiset.eq_sub_of_add_eq <| sub_add_inter ..).symm + +@[simp] +theorem count_inter (a : α) (s t : Multiset α) : count a (s ∩ t) = min (count a s) (count a t) := by + apply @Nat.add_left_cancel (count a (s - t)) + rw [← count_add, sub_add_inter, count_sub, Nat.sub_add_min_cancel] + +@[simp] +lemma coe_inter (s t : List α) : (s ∩ t : Multiset α) = (s.bagInter t : List α) := by ext; simp + +instance instDistribLattice : DistribLattice (Multiset α) where + le_sup_inf s t u := ge_of_eq <| ext.2 fun a ↦ by + simp only [max_min_distrib_left, Multiset.count_inter, Multiset.sup_eq_union, + Multiset.count_union, Multiset.inf_eq_inter] + +@[simp] +theorem filter_inter (p : α → Prop) [DecidablePred p] (s t : Multiset α) : + filter p (s ∩ t) = filter p s ∩ filter p t := + le_antisymm + (le_inter (filter_le_filter _ <| inter_le_left _ _) + (filter_le_filter _ <| inter_le_right _ _)) <| + le_filter.2 + ⟨inf_le_inf (filter_le _ _) (filter_le _ _), fun _a h => + of_mem_filter (mem_of_le (inter_le_left _ _) h)⟩ + @[simp] theorem replicate_inter (n : ℕ) (x : α) (s : Multiset α) : replicate n x ∩ s = replicate (min n (s.count x)) x := by @@ -2324,23 +2260,7 @@ theorem inter_replicate (s : Multiset α) (n : ℕ) (x : α) : s ∩ replicate n x = replicate (min (s.count x) n) x := by rw [inter_comm, replicate_inter, min_comm] -theorem erase_attach_map_val (s : Multiset α) (x : {x // x ∈ s}) : - (s.attach.erase x).map (↑) = s.erase x := by - rw [Multiset.map_erase _ val_injective, attach_map_val] - -theorem erase_attach_map (s : Multiset α) (f : α → β) (x : {x // x ∈ s}) : - (s.attach.erase x).map (fun j : {x // x ∈ s} ↦ f j) = (s.erase x).map f := by - simp only [← Function.comp_apply (f := f)] - rw [← map_map, erase_attach_map_val] - -end - -@[ext] -theorem addHom_ext [AddZeroClass β] ⦃f g : Multiset α →+ β⦄ (h : ∀ x, f {x} = g {x}) : f = g := by - ext s - induction' s using Multiset.induction_on with a s ih - · simp only [_root_.map_zero] - · simp only [← singleton_add, _root_.map_add, ih, h] +end sub section Embedding @@ -2696,7 +2616,7 @@ lemma add_eq_union_left_of_le [DecidableEq α] {s t u : Multiset α} (h : t ≤ rw [← add_eq_union_iff_disjoint] refine ⟨fun h0 ↦ ?_, ?_⟩ · rw [and_iff_right_of_imp] - · exact (le_of_add_le_add_left <| h0.trans_le <| union_le_add u t).antisymm h + · exact (Multiset.le_of_add_le_add_left <| h0.trans_le <| union_le_add u t).antisymm h · rintro rfl exact h0 · rintro ⟨h0, rfl⟩ @@ -2794,4 +2714,4 @@ theorem coe_subsingletonEquiv [Subsingleton α] : end Multiset -set_option linter.style.longFile 2900 +set_option linter.style.longFile 2800 diff --git a/Mathlib/Data/Multiset/OrderedMonoid.lean b/Mathlib/Data/Multiset/OrderedMonoid.lean index bf40bc0b213eb0..a674512d9f22c6 100644 --- a/Mathlib/Data/Multiset/OrderedMonoid.lean +++ b/Mathlib/Data/Multiset/OrderedMonoid.lean @@ -3,7 +3,7 @@ Copyright (c) 2015 Microsoft Corporation. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Mario Carneiro -/ -import Mathlib.Data.Multiset.Basic +import Mathlib.Algebra.Order.Group.Multiset import Mathlib.Algebra.Order.Monoid.Canonical.Defs /-! diff --git a/Mathlib/Data/Multiset/Range.lean b/Mathlib/Data/Multiset/Range.lean index 7f1b911b0f826b..82be6f025e6de9 100644 --- a/Mathlib/Data/Multiset/Range.lean +++ b/Mathlib/Data/Multiset/Range.lean @@ -3,7 +3,7 @@ Copyright (c) 2015 Microsoft Corporation. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Mario Carneiro -/ -import Mathlib.Data.Multiset.Basic +import Mathlib.Algebra.Order.Group.Multiset /-! # `Multiset.range n` gives `{0, 1, ..., n-1}` as a multiset. -/ diff --git a/Mathlib/Data/Sym/Basic.lean b/Mathlib/Data/Sym/Basic.lean index 32aca18c1b5c4d..b4f7c2d2cce650 100644 --- a/Mathlib/Data/Sym/Basic.lean +++ b/Mathlib/Data/Sym/Basic.lean @@ -3,7 +3,7 @@ Copyright (c) 2020 Kyle Miller. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Kyle Miller -/ -import Mathlib.Data.Multiset.Basic +import Mathlib.Algebra.Order.Group.Multiset import Mathlib.Data.Vector.Basic import Mathlib.Data.Setoid.Basic import Mathlib.Tactic.ApplyFun @@ -385,7 +385,7 @@ def equivCongr (e : α ≃ β) : Sym α n ≃ Sym β n where /-- "Attach" a proof that `a ∈ s` to each element `a` in `s` to produce an element of the symmetric power on `{x // x ∈ s}`. -/ def attach (s : Sym α n) : Sym { x // x ∈ s } n := - ⟨s.val.attach, by (conv_rhs => rw [← s.2, ← Multiset.card_attach]); rfl⟩ + ⟨s.val.attach, by (conv_rhs => rw [← s.2, ← Multiset.card_attach])⟩ @[simp] theorem attach_mk {m : Multiset α} {hc : Multiset.card m = n} : @@ -441,7 +441,7 @@ theorem mem_cast (h : n = m) : a ∈ Sym.cast h s ↔ a ∈ s := /-- Append a pair of `Sym` terms. -/ def append (s : Sym α n) (s' : Sym α n') : Sym α (n + n') := - ⟨s.1 + s'.1, by rw [map_add, s.2, s'.2]⟩ + ⟨s.1 + s'.1, by rw [Multiset.card_add, s.2, s'.2]⟩ @[simp] theorem append_inj_right (s : Sym α n) {t t' : Sym α n'} : s.append t = s.append t' ↔ t = t' :=