feat(data/*/interval): finset.uIcc on concrete structures (#18838)

Calculate the size of `finset.uIcc` in `ℕ`, `ℤ`, `fin`, `prod`, `pi`, `multiset`, `finset`...




Co-authored-by: Eric Wieser <wieser.eric@gmail.com>

src/data/dfinsupp/interval.lean

@@ -140,7 +140,7 @@ end
 
 end pi
 
-section locally_finite
+section partial_order
 variables [decidable_eq ι] [Π i, decidable_eq (α i)]
 variables [Π i, partial_order (α i)] [Π i, has_zero (α i)] [Π i, locally_finite_order (α i)]
 
@@ -169,7 +169,16 @@ by rw [card_Ioc_eq_card_Icc_sub_one, card_Icc]
 lemma card_Ioo : (Ioo f g).card = ∏ i in f.support ∪ g.support, (Icc (f i) (g i)).card - 2 :=
 by rw [card_Ioo_eq_card_Icc_sub_two, card_Icc]
 
-end locally_finite
+end partial_order
+
+section lattice
+variables [decidable_eq ι] [Π i, decidable_eq (α i)] [Π i, lattice (α i)] [Π i, has_zero (α i)]
+  [Π i, locally_finite_order (α i)] (f g : Π₀ i, α i)
+
+lemma card_uIcc : (uIcc f g).card = ∏ i in f.support ∪ g.support, (uIcc (f i) (g i)).card :=
+by { rw ←support_inf_union_support_sup, exact card_Icc _ _ }
+
+end lattice
 
 section canonically_ordered
 variables [decidable_eq ι] [Π i, decidable_eq (α i)]

src/data/dfinsupp/multiset.lean

@@ -17,6 +17,8 @@ with `multiset.to_dfinsupp` the reverse equivalence.
 Note that this provides a computable alternative to `finsupp.to_multiset`.
 -/
 
+open function
+
 variables {α : Type*} {β : α → Type*}
 
 namespace dfinsupp
@@ -38,7 +40,7 @@ dfinsupp.sum_add_hom_single _ _ _
 end dfinsupp
 
 namespace multiset
-variables [decidable_eq α]
+variables [decidable_eq α] {s t : multiset α}
 
 /-- A computable version of `multiset.to_finsupp` -/
 def to_dfinsupp : multiset α →+ Π₀ a : α, ℕ :=
@@ -78,12 +80,52 @@ add_monoid_hom.to_add_equiv
 @[simp] lemma to_dfinsupp_to_multiset (s : multiset α) : s.to_dfinsupp.to_multiset = s :=
 equiv_dfinsupp.symm_apply_apply s
 
-@[simp] lemma to_dfinsupp_le_to_dfinsupp (s t : multiset α) :
-  to_dfinsupp s ≤ to_dfinsupp t ↔ s ≤ t :=
+lemma to_dfinsupp_injective : injective (to_dfinsupp : multiset α → Π₀ a, ℕ) :=
+equiv_dfinsupp.injective
+
+@[simp] lemma to_dfinsupp_inj : to_dfinsupp s = to_dfinsupp t ↔ s = t :=
+to_dfinsupp_injective.eq_iff
+
+@[simp] lemma to_dfinsupp_le_to_dfinsupp : to_dfinsupp s ≤ to_dfinsupp t ↔ s ≤ t :=
 by simp [multiset.le_iff_count, dfinsupp.le_def]
 
+@[simp] lemma to_dfinsupp_lt_to_dfinsupp : to_dfinsupp s < to_dfinsupp t ↔ s < t :=
+lt_iff_lt_of_le_iff_le' to_dfinsupp_le_to_dfinsupp to_dfinsupp_le_to_dfinsupp
+
+@[simp] lemma to_dfinsupp_inter (s t : multiset α) :
+  to_dfinsupp (s ∩ t) = s.to_dfinsupp ⊓ t.to_dfinsupp :=
+by { ext i, simp [inf_eq_min] }
+
+@[simp] lemma to_dfinsupp_union (s t : multiset α) :
+  to_dfinsupp (s ∪ t) = s.to_dfinsupp ⊔ t.to_dfinsupp :=
+by { ext i, simp [sup_eq_max] }
+
 end multiset
 
-@[simp] lemma dfinsupp.to_multiset_to_dfinsupp [decidable_eq α] (f : Π₀ a : α, ℕ) :
-  f.to_multiset.to_dfinsupp = f :=
+namespace dfinsupp
+variables [decidable_eq α] {f g : Π₀ a : α, ℕ}
+
+@[simp] lemma to_multiset_to_dfinsupp : f.to_multiset.to_dfinsupp = f :=
 multiset.equiv_dfinsupp.apply_symm_apply f
+
+lemma to_multiset_injective : injective (to_multiset : (Π₀ a, ℕ) → multiset α) :=
+multiset.equiv_dfinsupp.symm.injective
+
+@[simp] lemma to_multiset_inj : to_multiset f = to_multiset g ↔ f = g :=
+to_multiset_injective.eq_iff
+
+@[simp] lemma to_multiset_le_to_multiset : to_multiset f ≤ to_multiset g ↔ f ≤ g :=
+by simp_rw [←multiset.to_dfinsupp_le_to_dfinsupp, to_multiset_to_dfinsupp]
+
+@[simp] lemma to_multiset_lt_to_multiset : to_multiset f < to_multiset g ↔ f < g :=
+by simp_rw [←multiset.to_dfinsupp_lt_to_dfinsupp, to_multiset_to_dfinsupp]
+
+variables (f g)
+
+@[simp] lemma to_multiset_inf : to_multiset (f ⊓ g) = f.to_multiset ∩ g.to_multiset :=
+multiset.to_dfinsupp_injective $ by simp
+
+@[simp] lemma to_multiset_sup : to_multiset (f ⊔ g) = f.to_multiset ∪ g.to_multiset :=
+multiset.to_dfinsupp_injective $ by simp
+
+end dfinsupp

src/data/dfinsupp/order.lean

@@ -31,15 +31,13 @@ namespace dfinsupp
 /-! ### Order structures -/
 
 section has_zero
-variables (α) [Π i, has_zero (α i)]
+variables [Π i, has_zero (α i)]
 
 section has_le
 variables [Π i, has_le (α i)]
 
 instance : has_le (Π₀ i, α i) := ⟨λ f g, ∀ i, f i ≤ g i⟩
 
-variables {α}
-
 lemma le_def {f g : Π₀ i, α i} : f ≤ g ↔ ∀ i, f i ≤ g i := iff.rfl
 
 /-- The order on `dfinsupp`s over a partial order embeds into the order on functions -/
@@ -59,22 +57,22 @@ variables [Π i, preorder (α i)]
 instance : preorder (Π₀ i, α i) :=
 { le_refl := λ f i, le_rfl,
   le_trans := λ f g h hfg hgh i, (hfg i).trans (hgh i),
-  .. dfinsupp.has_le α }
+  .. dfinsupp.has_le }
 
 lemma coe_fn_mono : monotone (coe_fn : (Π₀ i, α i) → Π i, α i) := λ f g, le_def.1
 
 end preorder
 
 instance [Π i, partial_order (α i)] : partial_order (Π₀ i, α i) :=
 { le_antisymm := λ f g hfg hgf, ext $ λ i, (hfg i).antisymm (hgf i),
-  .. dfinsupp.preorder α}
+  .. dfinsupp.preorder }
 
 instance [Π i, semilattice_inf (α i)] : semilattice_inf (Π₀ i, α i) :=
 { inf := zip_with (λ _, (⊓)) (λ _, inf_idem),
   inf_le_left := λ f g i, by { rw zip_with_apply, exact inf_le_left },
   inf_le_right := λ f g i, by { rw zip_with_apply, exact inf_le_right },
   le_inf := λ f g h hf hg i, by { rw zip_with_apply, exact le_inf (hf i) (hg i) },
-  ..dfinsupp.partial_order α }
+  ..dfinsupp.partial_order }
 
 @[simp] lemma inf_apply [Π i, semilattice_inf (α i)] (f g : Π₀ i, α i) (i : ι) :
   (f ⊓ g) i = f i ⊓ g i :=
@@ -85,15 +83,26 @@ instance [Π i, semilattice_sup (α i)] : semilattice_sup (Π₀ i, α i) :=
   le_sup_left := λ f g i, by { rw zip_with_apply, exact le_sup_left },
   le_sup_right := λ f g i, by { rw zip_with_apply, exact le_sup_right },
   sup_le := λ f g h hf hg i, by { rw zip_with_apply, exact sup_le (hf i) (hg i) },
-  ..dfinsupp.partial_order α }
+  ..dfinsupp.partial_order }
 
 @[simp] lemma sup_apply [Π i, semilattice_sup (α i)] (f g : Π₀ i, α i) (i : ι) :
   (f ⊔ g) i = f i ⊔ g i :=
 zip_with_apply _ _ _ _ _
 
-instance lattice [Π i, lattice (α i)] : lattice (Π₀ i, α i) :=
-{ .. dfinsupp.semilattice_inf α, .. dfinsupp.semilattice_sup α }
+section lattice
+variables [Π i, lattice (α i)] (f g : Π₀ i, α i)
+
+instance lattice : lattice (Π₀ i, α i) := { ..dfinsupp.semilattice_inf, ..dfinsupp.semilattice_sup }
+
+variables [decidable_eq ι] [Π i (x : α i), decidable (x ≠ 0)]
+
+lemma support_inf_union_support_sup : (f ⊓ g).support ∪ (f ⊔ g).support = f.support ∪ g.support :=
+coe_injective $ compl_injective $ by { ext, simp [inf_eq_and_sup_eq_iff] }
+
+lemma support_sup_union_support_inf : (f ⊔ g).support ∪ (f ⊓ g).support = f.support ∪ g.support :=
+(union_comm _ _).trans $ support_inf_union_support_sup _ _
 
+end lattice
 end has_zero
 
 /-! ### Algebraic order structures -/
@@ -102,7 +111,7 @@ instance (α : ι → Type*) [Π i, ordered_add_comm_monoid (α i)] :
   ordered_add_comm_monoid (Π₀ i, α i) :=
 { add_le_add_left := λ a b h c i,
     by { rw [add_apply, add_apply], exact add_le_add_left (h i) (c i) },
-  .. dfinsupp.add_comm_monoid, .. dfinsupp.partial_order α }
+  .. dfinsupp.add_comm_monoid, .. dfinsupp.partial_order }
 
 instance (α : ι → Type*) [Π i, ordered_cancel_add_comm_monoid (α i)] :
   ordered_cancel_add_comm_monoid (Π₀ i, α i) :=

src/data/fin/interval.lean

@@ -16,6 +16,16 @@ This file proves that `fin n` is a `locally_finite_order` and calculates the car
 intervals as finsets and fintypes.
 -/
 
+namespace fin
+variables {n : ℕ} (a b : fin n)
+
+@[simp, norm_cast] lemma coe_sup : (↑(a ⊔ b) : ℕ) = a ⊔ b := rfl
+@[simp, norm_cast] lemma coe_inf : (↑(a ⊓ b) : ℕ) = a ⊓ b := rfl
+@[simp, norm_cast] lemma coe_max : (↑(max a b) : ℕ) = max a b := rfl
+@[simp, norm_cast] lemma coe_min : (↑(min a b) : ℕ) = min a b := rfl
+
+end fin
+
 open finset fin function
 
 open_locale big_operators
@@ -39,6 +49,7 @@ lemma Icc_eq_finset_subtype : Icc a b = (Icc (a : ℕ) b).fin n := rfl
 lemma Ico_eq_finset_subtype : Ico a b = (Ico (a : ℕ) b).fin n := rfl
 lemma Ioc_eq_finset_subtype : Ioc a b = (Ioc (a : ℕ) b).fin n := rfl
 lemma Ioo_eq_finset_subtype : Ioo a b = (Ioo (a : ℕ) b).fin n := rfl
+lemma uIcc_eq_finset_subtype : uIcc a b = (uIcc (a : ℕ) b).fin n := rfl
 
 @[simp] lemma map_subtype_embedding_Icc : (Icc a b).map fin.coe_embedding = Icc a b :=
 by simp [Icc_eq_finset_subtype, finset.fin, finset.map_map, Icc_filter_lt_of_lt_right]
@@ -52,6 +63,9 @@ by simp [Ioc_eq_finset_subtype, finset.fin, finset.map_map, Ioc_filter_lt_of_lt_
 @[simp] lemma map_subtype_embedding_Ioo : (Ioo a b).map fin.coe_embedding = Ioo a b :=
 by simp [Ioo_eq_finset_subtype, finset.fin, finset.map_map]
 
+@[simp] lemma map_subtype_embedding_uIcc : (uIcc a b).map coe_embedding = uIcc a b :=
+map_subtype_embedding_Icc _ _
+
 @[simp] lemma card_Icc : (Icc a b).card = b + 1 - a :=
 by rw [←nat.card_Icc, ←map_subtype_embedding_Icc, card_map]
 
@@ -64,6 +78,9 @@ by rw [←nat.card_Ioc, ←map_subtype_embedding_Ioc, card_map]
 @[simp] lemma card_Ioo : (Ioo a b).card = b - a - 1 :=
 by rw [←nat.card_Ioo, ←map_subtype_embedding_Ioo, card_map]
 
+@[simp] lemma card_uIcc : (uIcc a b).card = (b - a : ℤ).nat_abs + 1 :=
+by rw [coe_coe, coe_coe, ←nat.card_uIcc, ←map_subtype_embedding_uIcc, card_map]
+
 @[simp] lemma card_fintype_Icc : fintype.card (set.Icc a b) = b + 1 - a :=
 by rw [←card_Icc, fintype.card_of_finset]
 
@@ -76,6 +93,9 @@ by rw [←card_Ioc, fintype.card_of_finset]
 @[simp] lemma card_fintype_Ioo : fintype.card (set.Ioo a b) = b - a - 1 :=
 by rw [←card_Ioo, fintype.card_of_finset]
 
+@[simp] lemma card_fintype_uIcc : fintype.card (set.uIcc a b) = (b - a : ℤ).nat_abs + 1 :=
+by rw [←card_uIcc, fintype.card_of_finset]
+
 lemma Ici_eq_finset_subtype : Ici a = (Icc (a : ℕ) n).fin n := by { ext, simp }
 lemma Ioi_eq_finset_subtype : Ioi a = (Ioc (a : ℕ) n).fin n := by { ext, simp }
 lemma Iic_eq_finset_subtype : Iic b = (Iic (b : ℕ)).fin n := rfl

src/data/finset/locally_finite.lean

@@ -564,8 +564,11 @@ lemma Icc_subset_uIcc' : Icc b a ⊆ [a, b] := Icc_subset_Icc inf_le_right le_su
 @[simp] lemma left_mem_uIcc : a ∈ [a, b] := mem_Icc.2 ⟨inf_le_left, le_sup_left⟩
 @[simp] lemma right_mem_uIcc : b ∈ [a, b] := mem_Icc.2 ⟨inf_le_right, le_sup_right⟩
 
-lemma mem_uIcc_of_le (ha : a ≤ x) (hb : x ≤ b) : x ∈ [a, b] := Icc_subset_uIcc $ mem_Icc.2 ⟨ha, hb⟩
-lemma mem_uIcc_of_ge (hb : b ≤ x) (ha : x ≤ a) : x ∈ [a, b] := Icc_subset_uIcc' $ mem_Icc.2 ⟨hb, ha⟩
+lemma mem_uIcc_of_le (ha : a ≤ x) (hb : x ≤ b) : x ∈ [a, b] :=
+Icc_subset_uIcc $ mem_Icc.2 ⟨ha, hb⟩
+
+lemma mem_uIcc_of_ge (hb : b ≤ x) (ha : x ≤ a) : x ∈ [a, b] :=
+Icc_subset_uIcc' $ mem_Icc.2 ⟨hb, ha⟩
 
 lemma uIcc_subset_uIcc (h₁ : a₁ ∈ [a₂, b₂]) (h₂ : b₁ ∈ [a₂, b₂]) : [a₁, b₁] ⊆ [a₂, b₂] :=
 by { rw mem_uIcc at h₁ h₂, exact Icc_subset_Icc (le_inf h₁.1 h₂.1) (sup_le h₁.2 h₂.2) }
@@ -576,11 +579,15 @@ by { rw mem_Icc at ha hb, exact Icc_subset_Icc (le_inf ha.1 hb.1) (sup_le ha.2 h
 lemma uIcc_subset_uIcc_iff_mem : [a₁, b₁] ⊆ [a₂, b₂] ↔ a₁ ∈ [a₂, b₂] ∧ b₁ ∈ [a₂, b₂] :=
 ⟨λ h, ⟨h left_mem_uIcc, h right_mem_uIcc⟩, λ h, uIcc_subset_uIcc h.1 h.2⟩
 
-lemma uIcc_subset_uIcc_iff_le' : [a₁, b₁] ⊆ [a₂, b₂] ↔ a₂ ⊓ b₂ ≤ a₁ ⊓ b₁ ∧ a₁ ⊔ b₁ ≤ a₂ ⊔ b₂ :=
+lemma uIcc_subset_uIcc_iff_le' :
+  [a₁, b₁] ⊆ [a₂, b₂] ↔ a₂ ⊓ b₂ ≤ a₁ ⊓ b₁ ∧ a₁ ⊔ b₁ ≤ a₂ ⊔ b₂ :=
 Icc_subset_Icc_iff inf_le_sup
 
-lemma uIcc_subset_uIcc_right (h : x ∈ [a, b]) : [x, b] ⊆ [a, b] := uIcc_subset_uIcc h right_mem_uIcc
-lemma uIcc_subset_uIcc_left (h : x ∈ [a, b]) : [a, x] ⊆ [a, b] := uIcc_subset_uIcc left_mem_uIcc h
+lemma uIcc_subset_uIcc_right (h : x ∈ [a, b]) : [x, b] ⊆ [a, b] :=
+uIcc_subset_uIcc h right_mem_uIcc
+
+lemma uIcc_subset_uIcc_left (h : x ∈ [a, b]) : [a, x] ⊆ [a, b] :=
+uIcc_subset_uIcc left_mem_uIcc h
 
 end lattice
 

src/data/finsupp/interval.lean

@@ -106,6 +106,15 @@ by rw [card_Ioo_eq_card_Icc_sub_two, card_Icc]
 
 end partial_order
 
+section lattice
+variables [lattice α] [has_zero α] [locally_finite_order α] (f g : ι →₀ α)
+
+lemma card_uIcc [decidable_eq ι] :
+  (uIcc f g).card = ∏ i in f.support ∪ g.support, (uIcc (f i) (g i)).card :=
+by { rw ←support_inf_union_support_sup, exact card_Icc _ _ }
+
+end lattice
+
 section canonically_ordered
 variables [canonically_ordered_add_monoid α] [locally_finite_order α]
 

src/data/finsupp/order.lean

@@ -86,8 +86,18 @@ instance [semilattice_sup α] : semilattice_sup (ι →₀ α) :=
 
 @[simp] lemma sup_apply [semilattice_sup α] {i : ι} {f g : ι →₀ α} : (f ⊔ g) i = f i ⊔ g i := rfl
 
-instance lattice [lattice α] : lattice (ι →₀ α) :=
-{ .. finsupp.semilattice_inf, .. finsupp.semilattice_sup }
+instance [lattice α] : lattice (ι →₀ α) := { ..finsupp.semilattice_inf, ..finsupp.semilattice_sup }
+
+section lattice
+variables [decidable_eq ι] [lattice α] (f g : ι →₀ α)
+
+lemma support_inf_union_support_sup : (f ⊓ g).support ∪ (f ⊔ g).support = f.support ∪ g.support :=
+coe_injective $ compl_injective $ by { ext, simp [inf_eq_and_sup_eq_iff] }
+
+lemma support_sup_union_support_inf : (f ⊔ g).support ∪ (f ⊓ g).support = f.support ∪ g.support :=
+(union_comm _ _).trans $ support_inf_union_support_sup _ _
+
+end lattice
 
 end has_zero
 

src/data/int/interval.lean

@@ -92,18 +92,18 @@ lemma Ioc_eq_finset_map :
 lemma Ioo_eq_finset_map :
   Ioo a b = (finset.range (b - a - 1).to_nat).map
     (nat.cast_embedding.trans $ add_left_embedding (a + 1)) := rfl
+lemma uIcc_eq_finset_map : uIcc a b = (range (max a b + 1 - min a b).to_nat).map
+    (nat.cast_embedding.trans $ add_left_embedding $ min a b) := rfl
 
-@[simp] lemma card_Icc : (Icc a b).card = (b + 1 - a).to_nat :=
-by { change (finset.map _ _).card = _, rw [finset.card_map, finset.card_range] }
+@[simp] lemma card_Icc : (Icc a b).card = (b + 1 - a).to_nat := (card_map _).trans $ card_range _
+@[simp] lemma card_Ico : (Ico a b).card = (b - a).to_nat := (card_map _).trans $ card_range _
+@[simp] lemma card_Ioc : (Ioc a b).card = (b - a).to_nat := (card_map _).trans $ card_range _
+@[simp] lemma card_Ioo : (Ioo a b).card = (b - a - 1).to_nat := (card_map _).trans $ card_range _
 
-@[simp] lemma card_Ico : (Ico a b).card = (b - a).to_nat :=
-by { change (finset.map _ _).card = _, rw [finset.card_map, finset.card_range] }
-
-@[simp] lemma card_Ioc : (Ioc a b).card = (b - a).to_nat :=
-by { change (finset.map _ _).card = _, rw [finset.card_map, finset.card_range] }
-
-@[simp] lemma card_Ioo : (Ioo a b).card = (b - a - 1).to_nat :=
-by { change (finset.map _ _).card = _, rw [finset.card_map, finset.card_range] }
+@[simp] lemma card_uIcc : (uIcc a b).card = (b - a).nat_abs + 1 :=
+(card_map _).trans $ int.coe_nat_inj $ by rw [card_range, sup_eq_max, inf_eq_min,
+  int.to_nat_of_nonneg (sub_nonneg_of_le $ le_add_one min_le_max), int.coe_nat_add, int.coe_nat_abs,
+  add_comm, add_sub_assoc, max_sub_min_eq_abs, add_comm, int.coe_nat_one]
 
 lemma card_Icc_of_le (h : a ≤ b + 1) : ((Icc a b).card : ℤ) = b + 1 - a :=
 by rw [card_Icc, to_nat_sub_of_le h]
@@ -129,6 +129,9 @@ by rw [←card_Ioc, fintype.card_of_finset]
 @[simp] lemma card_fintype_Ioo : fintype.card (set.Ioo a b) = (b - a - 1).to_nat :=
 by rw [←card_Ioo, fintype.card_of_finset]
 
+@[simp] lemma card_fintype_uIcc : fintype.card (set.uIcc a b) = (b - a).nat_abs + 1 :=
+by rw [←card_uIcc, fintype.card_of_finset]
+
 lemma card_fintype_Icc_of_le (h : a ≤ b + 1) : (fintype.card (set.Icc a b) : ℤ) = b + 1 - a :=
 by rw [card_fintype_Icc, to_nat_sub_of_le h]