Zulip Chat Archive

Stream: Is there code for X?

Topic: can assume n is minimal


Filippo A. E. Nuccio (Jan 16 2021 at 18:59):

I am proving a lemma where I construct a list of n elements (a multiset, actually) satisfying a certain property, and I want to assume that n is "minimal", in the sense that no subset of my multiset satisfies it. I ended up proving the following

lemma can_assume_min (p : multiset α  Prop) (s₀ : multiset α) (H : p s₀) :
   s  s₀,  p s   ( a  s, ¬ p (s.erase a)) :=

but since this is quite ubiquitous a strategy, I suspect that it must already be in mathlib, so I am double-checking before proposing a PR.

Damiano Testa (Jan 17 2021 at 09:39):

Could I suggest 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.

Filippo A. E. Nuccio (Jan 17 2021 at 09:41):

Good point! I have actually created the PR #5783 and you can directly comment it there, so that it will appear to other reviewers.

Filippo A. E. Nuccio (Jan 17 2021 at 09:41):

I will certainly modify it, at any rate.

Chris Hughes (Jan 18 2021 at 07:41):

I think you can use well_founded.min with a proof that the subset relation on multisets is well founded. To prove well foundedness, you can use the fact that it implies the size decreases, so measure_wf is what you need.

Filippo A. E. Nuccio (Jan 18 2021 at 15:36):

Thanks! I also came up with the idea that existence of min could be useful, but I had no idea on how to implement this. I will give it a try!


Last updated: Dec 20 2023 at 11:08 UTC