feat(data/finset/grade): Finsets and multisets are graded

src/data/finset/basic.lean

@@ -1,4 +1,4 @@
 /-
 Copyright (c) 2015 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura, Jeremy Avigad, Minchao Wu, Mario Carneiro
@@ -298,6 +298,8 @@
 @[simp] theorem val_lt_iff {s₁ s₂ : finset α} : s₁.1 < s₂.1 ↔ s₁ ⊂ s₂ :=
 and_congr val_le_iff $ not_congr val_le_iff
 
+lemma val_strict_mono : strict_mono (val : finset α → multiset α) := λ _ _, val_lt_iff.2
+
 lemma ssubset_iff_subset_ne {s t : finset α} : s ⊂ t ↔ s ⊆ t ∧ s ≠ t :=
 @lt_iff_le_and_ne _ _ s t
 
@@ -543,6 +545,10 @@
   s.nonempty → (∃ a, s = {a}) ∨ (s : set α).nontrivial :=
 λ ⟨a, ha⟩, (eq_singleton_or_nontrivial ha).imp_left $ exists.intro a
 
+lemma exists_eq_singleton_iff_nonempty_subsingleton :
+  (∃ a : α, s = {a}) ↔ s.nonempty ∧ (s : set α).subsingleton :=
+by simp_rw [←coe_eq_singleton, set.exists_eq_singleton_iff_nonempty_subsingleton]; refl
+
 instance [nonempty α] : nontrivial (finset α) :=
 ‹nonempty α›.elim $ λ a, ⟨⟨{a}, ∅, singleton_ne_empty _⟩⟩
 
@@ -573,6 +579,8 @@
 @[simp] lemma mk_cons {s : multiset α} (h : (a ::ₘ s).nodup) :
   (⟨a ::ₘ s, h⟩ : finset α) = cons a ⟨s, (nodup_cons.1 h).2⟩ (nodup_cons.1 h).1 := rfl
 
+@[simp] lemma cons_empty : cons a ∅ (not_mem_empty _) = {a} := rfl
+
 @[simp] lemma nonempty_cons (h : a ∉ s) : (cons a s h).nonempty := ⟨a, mem_cons.2 $ or.inl rfl⟩
 
 @[simp] lemma nonempty_mk {m : multiset α} {hm} : (⟨m, hm⟩ : finset α).nonempty ↔ m ≠ 0 :=
@@ -705,6 +713,8 @@
 lemma eq_of_not_mem_of_mem_insert (ha : b ∈ insert a s) (hb : b ∉ s) : b = a :=
 (mem_insert.1 ha).resolve_right hb
 
+@[simp] lemma insert_empty : insert a (∅ : finset α) = {a} := rfl
+
 @[simp] theorem cons_eq_insert (a s h) : @cons α a s h = insert a s := ext $ λ a, by simp
 
 @[simp, norm_cast] lemma coe_insert (a : α) (s : finset α) :

src/data/finset/card.lean

@@ -1,4 +1,4 @@
 /-
 Copyright (c) 2015 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura, Jeremy Avigad
@@ -205,6 +205,7 @@
 end
 
 lemma card_lt_card (h : s ⊂ t) : s.card < t.card := card_lt_of_lt $ val_lt_iff.2 h
+lemma card_strict_mono : strict_mono (card : finset α → ℕ) := λ _ _, card_lt_card
 
 lemma card_eq_of_bijective (f : ∀ i, i < n → α) (hf : ∀ a ∈ s, ∃ i, ∃ h : i < n, f i h = a)
   (hf' : ∀ i (h : i < n), f i h ∈ s) (f_inj : ∀ i j (hi : i < n)

src/data/finset/grade.lean

@@ -0,0 +1,149 @@
+/-
+Copyright (c) 2023 Yaël Dillies. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Yaël Dillies
+-/
+import data.finset.card
+import data.set.finite
+import order.atoms
+import order.grade
+
+/-!
+# Finsets and multisets form a graded order
+
+This file characterises atoms, coatoms and the covering relation in finsets and multisets. It also
+proves that they form a `ℕ`-graded order.
+-/
+
+open order
+
+variables {α : Type*}
+
+namespace multiset
+variables {s t : multiset α} {a : α}
+
+@[simp] lemma covby_cons (s : multiset α) (a : α) : s ⋖ a ::ₘ s :=
+⟨lt_cons_self _ _, λ t hst hts, (covby_succ _).2 (card_lt_of_lt hst) $
+  by simpa using card_lt_of_lt hts⟩
+
+lemma _root_.covby.exists_multiset_cons (h : s ⋖ t) : ∃ a, t = a ::ₘ s :=
+(lt_iff_cons_le.1 h.lt).imp $ λ a ha, ha.eq_of_not_gt $ h.2 $ lt_cons_self _ _
+
+lemma covby_iff : s ⋖ t ↔ ∃ a, t = a ::ₘ s :=
+⟨covby.exists_multiset_cons, by { rintro ⟨a, rfl⟩, exact covby_cons _ _ }⟩
+
+lemma _root_.covby.card_multiset (h : s ⋖ t) : s.card ⋖ t.card :=
+by { obtain ⟨a, rfl⟩ := h.exists_multiset_cons, rw card_cons, exact covby_succ _ }
+
+lemma is_atom_iff : is_atom s ↔ ∃ a, s = {a} := bot_covby_iff.symm.trans covby_iff
+
+@[simp] lemma is_atom_singleton (a : α) : is_atom ({a} : multiset α) := is_atom_iff.2 ⟨_, rfl⟩
+
+instance : grade_min_order ℕ (multiset α) :=
+{ grade := card,
+  grade_strict_mono := card_strict_mono,
+  covby_grade := λ s t, covby.card_multiset,
+  is_min_grade := λ s hs, by { rw is_min_iff_eq_bot.1 hs, exact is_min_bot } }
+
+@[simp] protected lemma grade (m : multiset α) : grade ℕ m = m.card := rfl
+
+end multiset
+
+namespace finset
+variables {s t : finset α} {a : α}
+
+/-- Finsets form an order-connected suborder of multisets. -/
+lemma ord_connected_range_val : set.ord_connected (set.range val : set $ multiset α) :=
+⟨by { rintro _ _ _ ⟨s, rfl⟩ t ht, exact ⟨⟨t, multiset.nodup_of_le ht.2 s.2⟩, rfl⟩ }⟩
+
+/-- Finsets form an order-connected suborder of sets. -/
+lemma ord_connected_range_coe : set.ord_connected (set.range (coe : finset α → set α)) :=
+⟨by { rintro _ _ _ ⟨s, rfl⟩ t ht, exact ⟨_, (s.finite_to_set.subset ht.2).coe_to_finset⟩ }⟩
+
+@[simp] lemma val_wcovby_val : s.1 ⩿ t.1 ↔ s ⩿ t :=
+ord_connected_range_val.apply_wcovby_apply_iff ⟨⟨val, val_injective⟩, λ _ _ : finset α, val_le_iff⟩
+
+@[simp] lemma val_covby_val : s.1 ⋖ t.1 ↔ s ⋖ t :=
+ord_connected_range_val.apply_covby_apply_iff ⟨⟨val, val_injective⟩, λ _ _ : finset α, val_le_iff⟩
+
+@[simp] lemma coe_wcovby_coe : (s : set α) ⩿ t ↔ s ⩿ t :=
+ord_connected_range_coe.apply_wcovby_apply_iff ⟨⟨coe, coe_injective⟩, λ _ _ : finset α, coe_subset⟩
+
+@[simp] lemma coe_covby_coe : (s : set α) ⋖ t ↔ s ⋖ t :=
+ord_connected_range_coe.apply_covby_apply_iff ⟨⟨coe, coe_injective⟩, λ _ _ : finset α, coe_subset⟩
+
+alias val_wcovby_val ↔ _ _root_.wcovby.finset_val
+alias val_covby_val ↔ _ _root_.covby.finset_val
+alias coe_wcovby_coe ↔ _ _root_.wcovby.finset_coe
+alias coe_covby_coe ↔ _ _root_.covby.finset_coe
+
+@[simp] lemma covby_cons (ha : a ∉ s) : s ⋖ s.cons a ha := by simp [←val_covby_val]
+
+lemma _root_.covby.exists_finset_cons (h : s ⋖ t) : ∃ a ∉ s, t = s.cons a ‹_› :=
+(ssubset_iff_exists_cons_subset.1 h.lt).imp₂ $ λ a ha (hst : cons a s ha ⊆ t),
+  hst.eq_of_not_ssuperset $ h.2 $ ssubset_cons _
+
+lemma covby_iff_cons : s ⋖ t ↔ ∃ a ∉ s, t = s.cons a ‹_› :=
+⟨covby.exists_finset_cons, by { rintro ⟨a, ha, rfl⟩, exact covby_cons _ }⟩
+
+lemma _root_.covby.card_finset (h : s ⋖ t) : s.card ⋖ t.card := (val_covby_val.2 h).card_multiset
+
+section decidable_eq
+variables [decidable_eq α]
+
+@[simp] lemma wcovby_insert (s : finset α) (a : α) : s ⩿ insert a s := by simp [←coe_wcovby_coe]
+@[simp] lemma erase_wcovby (s : finset α) (a : α) : s.erase a ⩿ s := by simp [←coe_wcovby_coe]
+
+lemma covby_insert (ha : a ∉ s) : s ⋖ insert a s :=
+(wcovby_insert _ _).covby_of_lt $ ssubset_insert ha
+
+@[simp] lemma erase_covby (ha : a ∈ s) : s.erase a ⋖ s := ⟨erase_ssubset ha, (erase_wcovby _ _).2⟩
+
+lemma _root_.covby.exists_finset_insert (h : s ⋖ t) : ∃ a ∉ s, t = insert a s :=
+by simpa using h.exists_finset_cons
+
+lemma _root_.covby.exists_finset_erase (h : s ⋖ t) : ∃ a ∈ t, s = t.erase a :=
+by simpa only [←coe_inj, coe_erase] using h.finset_coe.exists_set_sdiff_singleton
+
+lemma covby_iff_insert : s ⋖ t ↔ ∃ a ∉ s, t = insert a s :=
+by simp only [←coe_covby_coe, set.covby_iff_insert, ←coe_inj, coe_insert, mem_coe]
+
+lemma covby_iff_erase : s ⋖ t ↔ ∃ a ∈ t, s = t.erase a :=
+by simp only [←coe_covby_coe, set.covby_iff_sdiff_singleton, ←coe_inj, coe_erase, mem_coe]
+
+end decidable_eq
+
+@[simp] lemma is_atom_singleton (a : α) : is_atom ({a} : finset α) :=
+⟨singleton_ne_empty a, λ s, eq_empty_of_ssubset_singleton⟩
+
+protected lemma is_atom_iff : is_atom s ↔ ∃ a, s = {a} :=
+bot_covby_iff.symm.trans $ covby_iff_cons.trans $ by simp
+
+section fintype
+variables [fintype α] [decidable_eq α]
+
+@[simp] lemma is_coatom_compl_singleton (a : α) : is_coatom ({a}ᶜ : finset α) :=
+(is_atom_singleton a).compl
+
+protected lemma is_coatom_iff : is_coatom s ↔ ∃ a, s = {a}ᶜ :=
+by simp_rw [←is_atom_compl, finset.is_atom_iff, compl_eq_iff_is_compl, eq_compl_iff_is_compl]
+
+end fintype
+
+instance grade_min_order_multiset : grade_min_order (multiset α) (finset α) :=
+{ grade := val,
+  grade_strict_mono := val_strict_mono,
+  covby_grade := λ _ _, covby.finset_val,
+  is_min_grade := λ s hs, by { rw is_min_iff_eq_bot.1 hs, exact is_min_bot } }
+
+@[simp] lemma grade_multiset (s : finset α) : grade (multiset α) s = s.1 := rfl
+
+instance grade_min_order_nat : grade_min_order ℕ (finset α) :=
+{ grade := card,
+  grade_strict_mono := card_strict_mono,
+  covby_grade := λ _ _, covby.card_finset,
+  is_min_grade := λ s hs, by { rw is_min_iff_eq_bot.1 hs, exact is_min_bot } }
+
+@[simp] protected lemma grade (s : finset α) : grade ℕ s = s.card := rfl
+
+end finset

src/data/list/basic.lean

@@ -1,4 +1,4 @@
 /-
 Copyright (c) 2014 Parikshit Khanna. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Parikshit Khanna, Jeremy Avigad, Leonardo de Moura, Floris van Doorn, Mario Carneiro
@@ -1066,6 +1066,9 @@
 @[simp] theorem sublist_nil_iff_eq_nil {l : list α} : l <+ [] ↔ l = [] :=
 ⟨eq_nil_of_sublist_nil, λ H, H ▸ sublist.refl _⟩
 
+@[simp] lemma sublist_singleton {l : list α} {a : α} : l <+ [a] ↔ l = [] ∨ l = [a] :=
+by split; rintro (_ | _); simp [*] at *
+
 @[simp] theorem replicate_sublist_replicate (a : α) {m n} :
   replicate m a <+ replicate n a ↔ m ≤ n :=
 ⟨λ h, by simpa only [length_replicate] using h.length_le,

src/data/list/perm.lean

@@ -1,4 +1,4 @@
 /-
 Copyright (c) 2015 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura, Jeremy Avigad, Mario Carneiro
@@ -27,7 +27,7 @@
 universes uu vv
 
 namespace list
-variables {α : Type uu} {β : Type vv} {l₁ l₂ : list α}
+variables {α : Type uu} {β : Type vv} {l l₁ l₂ : list α} {a : α}
 
 /-- `perm l₁ l₂` or `l₁ ~ l₂` asserts that `l₁` and `l₂` are permutations
   of each other. This is defined by induction using pairwise swaps. -/
@@ -386,6 +386,28 @@
   let ⟨l, p⟩ := sublist.exists_perm_append s in
   ⟨l, p.cons a⟩
 
+lemma subperm_iff : l₁ <+~ l₂ ↔ ∃ l ~ l₂, l₁ <+ l :=
+begin
+  refine ⟨_, λ ⟨l, h₁, h₂⟩, h₂.subperm.trans h₁.subperm⟩,
+  rintro ⟨l, h₁, h₂⟩,
+  obtain ⟨l', h₂⟩ := h₂.exists_perm_append,
+  exact ⟨l₁ ++ l', (h₂.trans (h₁.append_right _)).symm, (prefix_append _ _).sublist⟩,
+end
+
+@[simp] lemma singleton_subperm_iff : [a] <+~ l ↔ a ∈ l :=
+⟨λ ⟨s, hla, h⟩, by rwa [perm_singleton.1 hla, singleton_sublist] at h,
+ λ h, ⟨[a], perm.refl _, singleton_sublist.2 h⟩⟩
+
+@[simp] lemma subperm_singleton_iff : l <+~ [a] ↔ l = [] ∨ l = [a] :=
+begin
+  split,
+  { rw subperm_iff,
+    rintro ⟨s, hla, h⟩,
+    rwa [perm_singleton.mp hla, sublist_singleton] at h },
+  { rintro (rfl | rfl),
+    exacts [nil_subperm, subperm.refl _] }
+end
+
 theorem perm.countp_eq (p : α → Prop) [decidable_pred p]
   {l₁ l₂ : list α} (s : l₁ ~ l₂) : countp p l₁ = countp p l₂ :=
 by rw [countp_eq_length_filter, countp_eq_length_filter];
@@ -785,10 +807,6 @@
 instance decidable_subperm : decidable_rel ((<+~) : list α → list α → Prop) :=
 λ l₁ l₂, decidable_of_iff _ list.subperm_ext_iff.symm
 
-@[simp] lemma subperm_singleton_iff {α} {l : list α} {a : α} : [a] <+~ l ↔ a ∈ l :=
-⟨λ ⟨s, hla, h⟩, by rwa [perm_singleton.mp hla, singleton_sublist] at h,
- λ h, ⟨[a], perm.refl _, singleton_sublist.mpr h⟩⟩
-
 lemma subperm.cons_left {l₁ l₂ : list α} (h : l₁ <+~ l₂)
   (x : α) (hx : count x l₁ < count x l₂) :
   x :: l₁ <+~ l₂  :=

src/data/multiset/basic.lean

@@ -1,4 +1,4 @@
 /-
 Copyright (c) 2015 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mario Carneiro
@@ -252,6 +252,7 @@
 /-! ### `multiset.subset` -/
 
 section subset
+variables {s : multiset α} {a : α}
 
 /-- `s ⊆ t` is the lift of the list subset relation. It means that any
   element with nonzero multiplicity in `s` has nonzero multiplicity in `t`,
@@ -261,8 +262,9 @@
 
 instance : has_subset (multiset α) := ⟨multiset.subset⟩
 instance : has_ssubset (multiset α) := ⟨λ s t, s ⊆ t ∧ ¬ t ⊆ s⟩
+instance : is_nonstrict_strict_order (multiset α) (⊆) (⊂) := ⟨λ _ _, iff.rfl⟩
 
-@[simp] theorem coe_subset {l₁ l₂ : list α} : (l₁ : multiset α) ⊆ l₂ ↔ l₁ ⊆ l₂ := iff.rfl
+@[simp, norm_cast] theorem coe_subset {l₁ l₂ : list α} : (l₁ : multiset α) ⊆ l₂ ↔ l₁ ⊆ l₂ := iff.rfl
 
 @[simp] theorem subset.refl (s : multiset α) : s ⊆ s := λ a h, h
 
@@ -290,9 +292,13 @@
 theorem eq_zero_of_subset_zero {s : multiset α} (h : s ⊆ 0) : s = 0 :=
 eq_zero_of_forall_not_mem h
 
-theorem subset_zero {s : multiset α} : s ⊆ 0 ↔ s = 0 :=
+@[simp] theorem subset_zero : s ⊆ 0 ↔ s = 0 :=
 ⟨eq_zero_of_subset_zero, λ xeq, xeq.symm ▸ subset.refl 0⟩
 
+@[simp] lemma zero_ssubset : 0 ⊂ s ↔ s ≠ 0 := by simp [ssubset_iff_subset_not_subset]
+
+@[simp] lemma singleton_subset : {a} ⊆ s ↔ a ∈ s := by simp [subset_iff]
+
 lemma induction_on' {p : multiset α → Prop} (S : multiset α)
   (h₁ : p 0) (h₂ : ∀ {a s}, a ∈ S → s ⊆ S → p s → p (insert a s)) : p S :=
 @multiset.induction_on α (λ T, T ⊆ S → p T) S (λ _, h₁) (λ a s hps hs,
@@ -390,6 +396,11 @@
 
 lemma cons_le_cons (a : α) : s ≤ t → a ::ₘ s ≤ a ::ₘ t := (cons_le_cons_iff a).2
 
+@[simp] lemma cons_lt_cons_iff : a ::ₘ s < a ::ₘ t ↔ s < t :=
+lt_iff_lt_of_le_iff_le' (cons_le_cons_iff _) (cons_le_cons_iff _)
+
+lemma cons_lt_cons (a : α) (h : s < t) : a ::ₘ s < a ::ₘ t := cons_lt_cons_iff.2 h
+
 lemma le_cons_of_not_mem (m : a ∉ s) : s ≤ a ::ₘ t ↔ s ≤ t :=
 begin
   refine ⟨_, λ h, le_trans h $ le_cons_self _ _⟩,
@@ -409,6 +420,27 @@
 ⟨λ h, mem_of_le h (mem_singleton_self _),
  λ h, let ⟨t, e⟩ := exists_cons_of_mem h in e.symm ▸ cons_le_cons _ (zero_le _)⟩
 
+@[simp] lemma le_singleton : s ≤ {a} ↔ s = 0 ∨ s = {a} :=
+quot.induction_on s $ λ l, by simp only [cons_zero, ←coe_singleton, quot_mk_to_coe'', coe_le,
+  coe_eq_zero, coe_eq_coe, list.perm_singleton, list.subperm_singleton_iff]
+
+@[simp] lemma lt_singleton : s < {a} ↔ s = 0 :=
+begin
+  simp only [lt_iff_le_and_ne, le_singleton, or_and_distrib_right, ne.def, and_not_self, or_false,
+    and_iff_left_iff_imp],
+  rintro rfl,
+  exact (singleton_ne_zero _).symm,
+end
+
+@[simp] lemma ssubset_singleton_iff : s ⊂ {a} ↔ s = 0 :=
+begin
+  refine ⟨λ hs, eq_zero_of_subset_zero $ λ b hb, hs.2 _, _⟩,
+  { obtain rfl := mem_singleton.1 (hs.1 hb),
+    rwa singleton_subset },
+  { rintro rfl,
+    simp }
+end
+
 end
 
 /-! ### Additive monoid -/
@@ -542,6 +574,8 @@
 theorem card_lt_of_lt {s t : multiset α} (h : s < t) : card s < card t :=
 lt_of_not_ge $ λ h₂, ne_of_lt h $ eq_of_le_of_card_le (le_of_lt h) h₂
 
+lemma card_strict_mono : strict_mono (card : multiset α → ℕ) := λ _ _, card_lt_of_lt
+
 theorem lt_iff_cons_le {s t : multiset α} : s < t ↔ ∃ a, a ::ₘ s ≤ t :=
 ⟨quotient.induction_on₂ s t $ λ l₁ l₂ h,
   subperm.exists_of_length_lt (le_of_lt h) (card_lt_of_lt h),

src/data/set/basic.lean

@@ -1,4 +1,4 @@
 /-
 Copyright (c) 2014 Jeremy Avigad. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Jeremy Avigad, Leonardo de Moura
@@ -976,6 +976,9 @@
 
 lemma subset_diff : s ⊆ t \ u ↔ s ⊆ t ∧ disjoint s u := le_iff_subset.symm.trans le_sdiff
 
+lemma ssubset_iff_sdiff_singleton : s ⊂ t ↔ ∃ a ∈ t, s ⊆ t \ {a} :=
+by simp [ssubset_iff_insert, subset_diff, insert_subset, and_comm, and.left_comm]
+
 lemma inter_diff_distrib_left (s t u : set α) : s ∩ (t \ u) = (s ∩ t) \ (s ∩ u) :=
 inf_sdiff_distrib_left _ _ _
 

src/logic/lemmas.lean

@@ -1,4 +1,4 @@
 /-
 Copyright (c) 2022 Yaël Dillies. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Yaël Dillies
@@ -31,6 +31,9 @@
 alias ne_of_eq_of_ne ← eq.trans_ne
 alias ne_of_ne_of_eq ← ne.trans_eq
 
+alias Exists₂.imp ← Exists.imp₂
+alias Exists₃.imp ← Exists.imp₃
+
 variables {α : Sort*} {p q r : Prop} [decidable p] [decidable q] {a b c : α}
 
 lemma dite_dite_distrib_left {a : p → α} {b : ¬ p → q → α} {c : ¬ p → ¬ q → α} :