feat(multiset/basic): add lemma exists_minimal_subset

[faenuccio]

Add lemma can_assume_minimal showing that if a property p holds for some multiset, that it is possible to find a
multiset which has minimal cardinality satisfying it.

---

[adomani]

In line with the thread https://leanprover.zulipchat.com/#narrow/stream/217875-Is-there.20code.20for.20X.3F/topic/can.20assume.20n.20is.20minimal, would you mind minimizing over all nonempty subsets? For instance, if your property is "having odd cardinality", I would probably expect a singleton, rather than a subset of odd cardinality.

Thanks!

[kmill]

@adomani If you want a nonempty subset, couldn't you use the statement as-is but then make sure to add an s.nonempty clause into the predicate p? Otherwise you'd be excluding applications where the empty subset might be the minimal subset.

[faenuccio]

@kmill @adomani Well, indeed, as I tried to implement adomani's request, I realized that the best option seems (to me) to add two lemmas, one for the case where the empty set is allowed and one when it is not. It is on progress, hence I have changed the label to WIP

[adomani]

You are right: I had in mind of minimizing over all proper subsets, not the nonempty ones! Thus, the statement would return the empty set, if it satisfies p, since the empty set has no proper subsets. Sorry about my mistake!

[kmill]

I think this statement is not as strong as you'd like it to be. What if p s is that s.card is odd? Then s₀ would satisfy the conclusion since you can't remove a single element to make the multiset smaller while having it satisfy p.

Here's a stronger statement that you could use to prove yours:

lemma exists_minimal_subset [decidable_eq α] (p : multiset α → Prop) [decidable_pred p]
  (s₀ : multiset α) (H : p s₀) : ∃ s ≤ s₀, p s ∧ (∀ s' ≤ s, p s' → s' = s) :=
begin
  refine multiset.strong_induction_on s₀ (λ s₀ ih H, _) H,
  by_cases h : ∃ s < s₀, p s,
  { rcases h with ⟨s₁, hs₁, ps₁⟩,
    specialize ih s₁ hs₁ ps₁,
    rcases ih with ⟨s, hsle, hs⟩,
    use ⟨s, le_of_lt (lt_of_le_of_lt hsle hs₁), hs⟩, },
  { push_neg at h,
    use [s₀, rfl.ge, H],
    intros s' hs' ps',
    cases lt_or_eq_of_le hs' with hs'' hs'',
    { exact (h _ hs'' ps').elim, },
    { exact hs'', }, },
end

[kmill]

lemma exists_minimal_subset' [decidable_eq α] (p : multiset α → Prop) [decidable_pred p]
  (s₀ : multiset α) (H : p s₀) : ∃ s ≤ s₀, p s ∧ (∀ a ∈ s, ¬p (s.erase a)) :=
begin
  rcases exists_minimal_subset p s₀ H with ⟨s, hsle, ps, hs⟩,
  use [s, hsle, ps],
  intros a ha perase,
  have : s.erase a < s := erase_lt.mpr ha,
  rw hs (s.erase a) (erase_le a s) perase at this,
  exact lt_irrefl _ this,
end

[faenuccio]

Very good point! I'll study your suggestions, but just to understand better: have you commited any change, or are you proposing that I incorporate both exists_minimal_subset and exists_minimal_subset' in a new commit? Also, as far as I understand, the current version of my lemma can_assume_min would become obsolete, is that right?

[kmill]

I haven't committed anything -- I'm just giving these to you, and you can use them however you like.

It seems to me that exists_minimal_subset is the more useful one, and if you need a statement like exists_minimal_subset', you should instead have a lemma that if you have a minimal subset for which a predicate is true, then it's not true for any erasure:

/- not sure what to call this -/
lemma not_erase_of_minimal [decidable_eq α] (s : multiset α) (p : multiset α → Prop)
  (h : ∀ s' ≤ s, p s' → s' = s) (a : α) (ha : a ∈ s) : ¬p (s.erase a) :=
begin
  intro perase,
  have : s.erase a < s  := erase_lt.mpr ha,
  rw h _ (erase_le a s) perase at this,
  exact lt_irrefl _ this,
end

(Note: for exists_minimal_subset it turns out you can remove all the decidability constraints.)

[faenuccio]

Ok, thanks so much. I'll work on this and turn the label back to awaiting-review once done and commited.

[adomani]

In case you do not mind assuming classical facts, below is a short proof of exists_minimal_subset.

-- I could not find this in mathlib, but it seems like it could be there...
lemma nat.well_ordered_of_exists {s : set ℕ} [decidable_pred (λ w, w ∈ s)] (ex : ∃ w : ℕ, w ∈ s) :
  ∃ n ∈ s, ∀ m ∈ s, n ≤ m :=
⟨nat.find ex, nat.find_spec ex, λ m, nat.find_min' ex⟩

lemma exists_minimal_subset {p : multiset α → Prop} {s₀ : multiset α} (H : p s₀)
  [decidable_pred (λ w, w ∈ {i | ∃ u, u ≤ s₀ ∧ p u ∧ u.card = i})] :
  ∃ s ≤ s₀, p s ∧ (∀ s' ≤ s, p s' → s' = s) :=
begin
  obtain ⟨n, ⟨sm, sm0, ps, sc⟩, F⟩ := nat.well_ordered_of_exists
    (⟨_, _, le_rfl, H, rfl⟩ : ∃ w : ℕ, w ∈ { i | ∃ u, u ≤ s₀ ∧ p u ∧ u.card = i }),
  exact ⟨sm, sm0, ps, λ t tsm pt, eq_of_le_of_card_le tsm
    (by {rw sc, exact F _ ⟨t, le_trans tsm sm0, pt, rfl⟩})⟩,
end

Note that, if you do not want to get into the decidable stuff, you can write open_locale classical at the beginning of your file and all these decidable issues go away.

If I understand this correctly, the proof above uses classical, since it finds a subset of minimum cardinality by going through subsets of ℕ. Kyle's proof stays on multiset: I think that multisets already have all the decidable stuff inbuilt. For me, this is the reason why working with multisets and finsets is hard, without classical.

[bryangingechen]

@faenuccio I put this to "awaiting-author" for now since there's still a sorry left, but is this still waiting for comments from @adomani ?

[faenuccio]

I have even converted this to a draft since I will not be able to work on this for some time. I realise I do not know how to bring it back to life as a normal PR, but this is not urgent.

[bryangingechen]

@faenuccio Thanks for the update! If I recall correctly, there's a link to change draft PRs back to normal PRs at the top right, near where the list of assigned reviewers is.