From 6e707f4d64a33ac386ac2c0aa129514b9e135248 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 | 4 +- Mathlib/Algebra/Order/Group/Multiset.lean | 178 ++++++++++++ Mathlib/Data/Multiset/Basic.lean | 266 +++++++----------- Mathlib/Data/Multiset/OrderedMonoid.lean | 2 +- Mathlib/Data/Multiset/Range.lean | 2 +- Mathlib/Data/Sym/Basic.lean | 2 +- 8 files changed, 282 insertions(+), 176 deletions(-) create mode 100644 Mathlib/Algebra/Order/Group/Multiset.lean diff --git a/Mathlib.lean b/Mathlib.lean index 99606d29a64b3..9c97b9cd9e153 100644 --- a/Mathlib.lean +++ b/Mathlib.lean @@ -689,6 +689,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 a93afea870a07..9f83c37dae0a1 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 6f377d4ff77be..af5e65fe47cb5 100644 --- a/Mathlib/Algebra/BigOperators/GroupWithZero/Action.lean +++ b/Mathlib/Algebra/BigOperators/GroupWithZero/Action.lean @@ -3,11 +3,11 @@ Copyright (c) 2020 Yury Kudryashov. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Yury Kudryashov -/ +import Mathlib.Algebra.BigOperators.Finprod import Mathlib.Algebra.BigOperators.Group.Finset import Mathlib.Algebra.GroupWithZero.Action.Defs +import Mathlib.Algebra.Order.Group.Multiset import Mathlib.Data.Finset.Basic -import Mathlib.Data.Multiset.Basic -import Mathlib.Algebra.BigOperators.Finprod /-! # Lemmas about group actions on big operators diff --git a/Mathlib/Algebra/Order/Group/Multiset.lean b/Mathlib/Algebra/Order/Group/Multiset.lean new file mode 100644 index 0000000000000..7fb63d8cd37e0 --- /dev/null +++ b/Mathlib/Algebra/Order/Group/Multiset.lean @@ -0,0 +1,178 @@ +/- +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 + +@[simp] +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 9fec51e78b073..bb263451f18a0 100644 --- a/Mathlib/Data/Multiset/Basic.lean +++ b/Mathlib/Data/Multiset/Basic.lean @@ -3,15 +3,13 @@ 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 @@ -34,8 +32,8 @@ lists by permutation. This gives them computational content. 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 @@ -588,6 +586,7 @@ 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, @@ -607,28 +606,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 _ -instance : AddLeftReflectLE (Multiset α) := - ⟨fun _s _t _u => add_le_add_iff_left'.1⟩ +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 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_comm (s t : Multiset α) : s + t = t + s := + Quotient.inductionOn₂ s t fun _ _ ↦ Quot.sound perm_append_comm -theorem le_add_right (s t : Multiset α) : s ≤ s + t := by simpa using add_le_add_left (zero_le t) s +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_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 `zero_add` +protected lemma zero_add (s : Multiset α) : 0 + s = s := Quotient.inductionOn s fun _ ↦ rfl + +@[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 @@ -643,11 +647,11 @@ 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 := @@ -655,29 +659,6 @@ theorem mem_add {a : α} {s t : Multiset α} : a ∈ s + t ↔ a ∈ s ∨ a ∈ end add -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] - /-! ### Cardinality -/ @@ -697,18 +678,9 @@ theorem length_toList (s : Multiset α) : s.toList.length = card s := by theorem card_zero : @card α 0 = 0 := rfl -@[simp] lemma card_add (s t : Multiset α) : card (s + t) = card s + card t := - Quotient.inductionOn₂ s t length_append - -/-- `Multiset.card` bundled as a monoid hom. -/ -@[simps] -def cardHom : Multiset α →+ ℕ where - toFun := card - map_zero' := card_zero - map_add' := card_add - @[simp] -lemma card_nsmul (s : Multiset α) (n : ℕ) : card (n • s) = n * card s := cardHom.map_nsmul .. +theorem card_add (s t : Multiset α) : card (s + t) = card s + card t := + Quotient.inductionOn₂ s t length_append @[simp] theorem card_cons (a : α) (s : Multiset α) : card (a ::ₘ s) = card s + 1 := @@ -716,7 +688,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] @@ -840,13 +812,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 := @@ -885,12 +850,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) @@ -965,7 +924,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⟩ @@ -974,15 +934,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 @@ -1101,20 +1061,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 @@ -1553,22 +1499,11 @@ 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) @@ -1586,7 +1521,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] @@ -1729,24 +1664,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 - @[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) @@ -1774,7 +1694,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 := @@ -1825,7 +1745,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 α → ℕ := @@ -1866,24 +1786,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 _ _ @@ -2007,6 +1915,12 @@ lemma erase_attach_map (s : Multiset α) (f : α → β) (x : {x // x ∈ s}) : 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 -/ @@ -2055,17 +1969,35 @@ protected lemma sub_le_iff_le_add : s - t ≤ u ↔ s ≤ u + t := by exact @(Multiset.induction_on t (by simp [Multiset.sub_zero]) fun a t IH s => by simp [IH, erase_le_iff_le_cons]) -protected lemma sub_le_self (s t : Multiset α) : s - t ≤ s := by +/-- 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 _ _ -instance : OrderedSub (Multiset α) := - ⟨fun _n _m _k => Multiset.sub_le_iff_le_add⟩ +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] -instance : ExistsAddOfLE (Multiset α) where - exists_add_of_le h := leInductionOn h fun s => - let ⟨l, p⟩ := s.exists_perm_append - ⟨l, Quot.sound p⟩ +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] lemma filter_sub (p : α → Prop) [DecidablePred p] (s t : Multiset α) : @@ -2090,7 +2022,7 @@ lemma sub_filter_eq_filter_not (p : α → Prop) [DecidablePred p] (s : Multiset s - s.filter p = s.filter fun a ↦ ¬ p a := by ext a; by_cases h : p a <;> simp [h] lemma 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] + rw [← singleton_add, ← singleton_add, Multiset.add_sub_assoc h] lemma sub_eq_fold_erase (s t : Multiset α) : s - t = foldl erase s t := Quotient.inductionOn₂ s t fun l₁ l₂ => by @@ -2101,7 +2033,7 @@ lemma sub_eq_fold_erase (s t : Multiset α) : s - t = foldl erase s t := @[simp] lemma 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] + Nat.eq_sub_of_add_eq <| by rw [← card_add, Multiset.sub_add_cancel h] /-! ### Union -/ @@ -2109,17 +2041,18 @@ lemma card_sub {s t : Multiset α} (h : t ≤ s) : card (s - t) = card s - card multiplicity of `a` in `s` and `t`. This is the supremum of multisets. -/ def union (s t : Multiset α) : Multiset α := s - t + t -instance : Union (Multiset α) := ⟨union⟩ +instance : Union (Multiset α) := + ⟨union⟩ lemma union_def (s t : Multiset α) : s ∪ t = s - t + t := rfl -lemma le_union_left : s ≤ s ∪ t := le_tsub_add +lemma le_union_left : s ≤ s ∪ t := Multiset.le_sub_add lemma le_union_right : t ≤ s ∪ t := le_add_left _ _ -lemma eq_union_left : t ≤ s → s ∪ t = s := tsub_add_cancel_of_le +lemma eq_union_left : t ≤ s → s ∪ t = s := Multiset.sub_add_cancel @[gcongr] lemma union_le_union_right (h : s ≤ t) (u) : s ∪ u ≤ t ∪ u := - add_le_add_right (tsub_le_tsub_right h _) _ + Multiset.add_le_add_right <| Multiset.sub_le_sub_right h lemma union_le (h₁ : s ≤ u) (h₂ : t ≤ u) : s ∪ t ≤ u := by rw [← eq_union_left h₂]; exact union_le_union_right h₁ t @@ -2219,12 +2152,12 @@ lemma eq_union_right (h : s ≤ t) : s ∪ t = t := by rw [union_comm, eq_union_ lemma union_le_add (s t : Multiset α) : s ∪ t ≤ s + t := union_le (le_add_right ..) (le_add_left ..) lemma union_add_distrib (s t u : Multiset α) : s ∪ t + u = s + u ∪ (t + u) := by - simpa [(· ∪ ·), union, eq_comm, add_assoc, add_left_inj] using + simpa [(· ∪ ·), union, eq_comm, Multiset.add_assoc, Multiset.add_left_inj] using show s + u - (t + u) = s - t by - rw [add_comm t, tsub_add_eq_tsub_tsub, add_tsub_cancel_right] + rw [t.add_comm, Multiset.sub_add_eq_sub_sub, Multiset.add_sub_cancel_right] lemma 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] + rw [Multiset.add_comm, union_add_distrib, s.add_comm, s.add_comm] lemma cons_union_distrib (a : α) (s t : Multiset α) : a ::ₘ (s ∪ t) = a ::ₘ s ∪ a ::ₘ t := by simpa using add_union_distrib (a ::ₘ 0) s t @@ -2232,14 +2165,14 @@ lemma cons_union_distrib (a : α) (s t : Multiset α) : a ::ₘ (s ∪ t) = a :: lemma inter_add_distrib (s t u : Multiset α) : s ∩ t + u = (s + u) ∩ (t + u) := by by_contra! h obtain ⟨a, ha⟩ := lt_iff_cons_le.1 <| h.lt_of_le <| le_inter - (add_le_add_right inter_le_left _) (add_le_add_right inter_le_right _) + (Multiset.add_le_add_right inter_le_left) (Multiset.add_le_add_right inter_le_right) rw [← cons_add] at ha exact (lt_cons_self (s ∩ t) a).not_le <| le_inter - (le_of_add_le_add_right (ha.trans inter_le_left)) - (le_of_add_le_add_right (ha.trans inter_le_right)) + (Multiset.le_of_add_le_add_right (ha.trans inter_le_left)) + (Multiset.le_of_add_le_add_right (ha.trans inter_le_right)) lemma 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] + rw [Multiset.add_comm, inter_add_distrib, s.add_comm, s.add_comm] lemma cons_inter_distrib (a : α) (s t : Multiset α) : a ::ₘ s ∩ t = (a ::ₘ s) ∩ (a ::ₘ t) := by simp @@ -2247,13 +2180,13 @@ lemma cons_inter_distrib (a : α) (s t : Multiset α) : a ::ₘ s ∩ t = (a :: lemma 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 _ + 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 lemma sub_add_inter (s t : Multiset α) : s - t + s ∩ t = s := by rw [inter_comm] @@ -2263,7 +2196,7 @@ lemma sub_add_inter (s t : Multiset α) : s - t + s ∩ t = s := by · rw [cons_inter_of_neg _ h, sub_cons, erase_of_not_mem h, IH] lemma sub_inter (s t : Multiset α) : s - s ∩ t = s - t := - (eq_tsub_of_add_eq <| sub_add_inter ..).symm + (Multiset.eq_sub_of_add_eq <| sub_add_inter ..).symm @[simp] lemma count_inter (a : α) (s t : Multiset α) : count a (s ∩ t) = min (count a s) (count a t) := by @@ -2300,13 +2233,6 @@ theorem inter_replicate (s : Multiset α) (n : ℕ) (x : α) : end sub -@[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] - section Embedding @[simp] @@ -2661,7 +2587,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⟩ diff --git a/Mathlib/Data/Multiset/OrderedMonoid.lean b/Mathlib/Data/Multiset/OrderedMonoid.lean index bf40bc0b213eb..a674512d9f22c 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 7f1b911b0f826..82be6f025e6de 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 2733966c42fc7..24af84e1ec2d4 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