minimum of finite set

Stream: general

[Reid Barton]

I have a finset of rationals which I know is nonempty. How do I find its minimum element?

[Mario Carneiro]

I forget if there is a max operation on finsets, but you can fold with max

[Sean Leather]

I have a finset of rationals which I know is nonempty. How do I find its minimum element?

@Reid Barton See https://github.com/spl/tts/blob/master/src/data/finset/fresh.lean#L121-L154

I'd like to see something like this with max and min in mathlib. I haven't proposed it because I wasn't sure it was worth it, but, since you are also looking for it, perhaps it is.

[Sean Leather]

@Reid Barton Is this something (after replacing max with min) that would be useful to you? I can work on it next.

import data.finset

namespace finset
variables {α : Type*} [decidable_linear_order α]

def max (a : α) : finset α → α :=
  fold _root_.max a id

@[simp]
theorem max_empty {a : α} : max a (∅ : finset α) = a :=
  by simp [max]

@[simp]
theorem max_insert {a b : α} {s : finset α} (h : a ∉ s)
: max b (insert a s) = _root_.max a (max b s) :=
  by simp [max, fold_insert h]

@[simp]
theorem max_singleton {a b : α} : max b {a} = _root_.max a b :=
  by simp [max]

theorem le_max_left (a : α) (s : finset α) : a ≤ max a s :=
  finset.induction_on s
    (by rw max_empty)
    (λ b s (hnm : b ∉ s) (ih : a ≤ max a s),
     by rw max_insert hnm; exact le_trans ih (le_max_right b (max a s)))

theorem le_max_of_mem {a b : α} {s : finset α} (h : a ≤ b) : a ∈ s → a ≤ max b s :=
  finset.induction_on s
    (λ _, by simp only [max_empty, h])
    (λ c s (hnm : c ∉ s) (ih : a ∈ s → a ≤ max b s) (hins : a ∈ insert c s),
     begin
       rw max_insert hnm,
       cases mem_insert.mp hins,
       case or.inl : p { simp only [p, _root_.le_max_left] },
       case or.inr : p { exact le_trans (ih p) (le_max_right c (max b s)) }
     end)

end finset

[Patrick Massot]

What's this {a} syntax in max b {a}?

[Sean Leather]

It's notation for a singleton.

[Sean Leather]

Actually, to correct myself, {a} is a singleton, but the notation comes from init/core.lean, I think:

/- Type class used to implement the notation { a ∈ c | p a } -/
class has_sep (α : out_param $ Type u) (γ : Type v) :=
(sep : (α → Prop) → γ → γ)

[Patrick Massot]

Oh

[Patrick Massot]

I was confused, I thought it was an implicit parameter right of colon

[Patrick Massot]

The theorem even has "singleton" in its name...

[Sean Leather]

Hmm, maybe it's not from has_sep. I thought I knew, but I don't know anymore.

[Sean Leather]

Ah, right, it's this one:

/- Type classes has_emptyc and has_insert are
   used to implement polymorphic notation for collections.
   Example: {a, b, c}. -/
class has_emptyc   (α : Type u) := (emptyc : α)
class has_insert   (α : out_param $ Type u) (γ : Type v) := (insert : α → γ → γ)

[Sean Leather]

So, if your type has has_emptyc and has_insert instances, you can use the {..., ...} notation.

[Sean Leather]

I agree that it can be confusing.

[Patrick Massot]

It's my fault, I wasn't paying enough attention. I shouldn't be watching Zulip while grading Sage notebooks (@William Stein when will we get auto-grading Sage notebooks so that we can focus on understanding Lean code?).

[Sean Leather]

I don't think it's a great idea to overload {...} in this way, even if it isn't ambiguous to the parser. But it is notationally short, which makes it convenient.

[Patrick Massot]

And it's the maths notations, so it should win over any other interpretation

[Sean Leather]

True, but it doesn't see as much usage as implicit parameters, and it would be better to reserve short notation for things you type/read a lot.

[Sean Leather]

You pretty much only use this notation for singletons or examples.

[Sean Leather]

PR for finset.max and finset.min: https://github.com/leanprover/mathlib/pull/133

[Patrick Massot]

Nice. I will probably use it to build new normed spaces out of finitely many old ones.

[Reid Barton]

@Sean Leather I think this approach with a starting element (a) would be fine for my current application, since I have a particular element which I know belongs to the set. From a general math perspective, though, it's odd not to be able to talk about the minimum of a nonempty set, without first choosing an element of the set.

[Reid Barton]

I've been considering an approach that starts from fold1of an associative, commutative operation on a nonempty multiset, though this fold1 was quite a challenge to define.

[Reid Barton]

But fold1 seems like something one ought to have anyways.

[Reid Barton]

A friend suggested that I could just sort the list (finset.sort) and take the first element

[Sean Leather]

My thinking is that you can write different variations using max [decidable_linear_order α] : α → finset α → α. I believe this definition of max is the most general and least prescriptive since only [decidable_linear_order α] is required.

[Sean Leather]

@Johannes Hölzl suggested max [decidable_linear_order α] [inhabited α] : finset α → α, but I'm not sure if that's better (my response).

[Mario Carneiro]

It is not true that max as suggested by Johannes is the same as max_inhabited that you wrote. If s is nonempty, then max (default A) s is the max of default A and the elements of s, while Johannes's max is the max of the elements of s only. It is closer to Reid's suggested max operation, except that the nonempty constraint is replaced by a default value.

[Sean Leather]

Right. See the bottom of my response.

[Mario Carneiro]

Given johannes's max function, you could recover your max function as sean_max a s := @johannes_max A _ <a> (insert a s)

[Sean Leather]

So they are equivalent?

[Mario Carneiro]

Johannes's definition is more complicated since it requires casing on whether the list is empty

[Sean Leather]

What is the definition?

[Mario Carneiro]

there is not an easy expression for johannes_max using sean_max, you would need another quot.lift

[Mario Carneiro]

You have to start from list, define foldl1 and work your way up

[Sean Leather]

Ah, something like that.

[Mario Carneiro]

Alternatively, you could sean_max over option A

[Mario Carneiro]

where none has the appropriate interpretation as a neutral element for max

[Sean Leather]

You mean map/image some over the finset?

[Mario Carneiro]

and that would give you both the partial max function and the inhabited max function (Johannes's max)

[Mario Carneiro]

Any semigroup operation extends to a monoid if you add a neutral element

[Mario Carneiro]

That means that you can take a semigroup operation like max and extend it to option_max : option A -> option A -> option A that is a monoid operation

[Mario Carneiro]

and then you can finset.prod over this

[Mario Carneiro]

This is essentially the same as adjoining a -inf element to the set

[Sean Leather]

Can you not finset.image some?

[Mario Carneiro]

That would be the input to the fold, yes

[Sean Leather]

Right, okay.

[Mario Carneiro]

The nice thing about this approach is that it naturally handles partiality, you don't need the inhabited thing; but it's easy to implement the inhabited version using option.iget

[Sean Leather]

Personally, I'm not a big fan of inhabited. I haven't found a need for it in anything I've done, and I feel like, if you need an inhabited type, why not use option in the first place?

[Sean Leather]

But I'm happy to see some version of finset.max and finset.min go into mathlib, so I don't feel that strongly about which one... as long as it works with nat. :simple_smile:

[Mario Carneiro]

I have a similar antipathy to inhabited, it's a somewhat lazy way to totalize functions like division on nonempty domains.

[Mario Carneiro]

Arguments in favor would say that composing them is a lot cleaner than the monad stuff

[Mario Carneiro]

i.e. (x + 2) / (y + 2 / z) is easier to read than do a <- 2 / z, (x + 2) / (y + a) or some such

[Mario Carneiro]

The best situation is if you are literally working in a sup_bot semilattice, in which case you don't have to cheat and get a proper function

[Johannes Hölzl]

Working on sup_bot_semilattice is indeed very nice, e.g. https://github.com/johoelzl/mason-stother/blob/master/Sup_fin.lean But we don't have a lot of ordered types having this structure, I guess nat, fin, and ennreal.

[Johannes Hölzl]

I prefer the inhabited version over option. With inhabited you get not only a nicer syntax, but a lot of cases etc can be easily done in the proofs, while for option we are often forced to do it on the term itself.

[Sean Leather]

Just thinking about it a little more... It seems like there are two goals here: one for a max with no requirements other than decidable_linear_order (me) and one for a max that does not need the extra a : α (Johannes and Reid). In the latter case, which is more useful: an inhabited α predicate or a non-empty predicate (e.g. s ≠ ∅ or ∃ a : α, a ∈ s)? I'm guessing the non-empty predicate is more useful because inhabited α doesn't tell you anything about the finset itself, and if you use the inhabited α version and want to know that you are not getting the inhabited.default, you need to know if the finset is empty anyway.

[Johannes Hölzl]

It is the other way round, the inhabited α is more useful from a user perspective. We don't need to give max more information than necessary. For max it is enough to show that α is inhabited, it is not necessary to show that s is inhabited (from which at least nonempty α follows). It is very annoying when the user always needs to provide a prove that s is not empty, this is exactly what I want to avoid.
After all, we are in a theorem prover! Carrying around this information explicitly is not necessary, as usually we can show it in a proof.

[Reid Barton]

My only worry about inhabited is that as, on the one hand, it is not a Prop, and on the other hand, we may not always have a canonical inhabited instance at hand and need to construct one from the knowledge that s is nonempty, we might end up in a situation where Lean thinks max s depends on the choice of inhabited instance, even though we know it doesn't really.

[Reid Barton]

On the other hand, taking a nonempty α instance would make max noncomputable, which is maybe sort of okay for a theorem prover but not very attractive for programming use.

[Reid Barton]

(As it turns out, the theorem I really need has the conclusion ∃x ∈ s, ∀y ∈ s, f y ≤ f x, and for this, we need s to be nonempty anyways.)

[Reid Barton]

The advantage of s ≠ ∅ here is that it is a Prop, but also sufficient to define max computably

[Reid Barton]

I'm kind of tempted to make s ≠ ∅ into a type class argument, actually, but maybe that is going too far?

[Johannes Hölzl]

Of course a theorem like s ≠ ∅ -> ∃x ∈ s, ∀y ∈ s, f y ≤ f x is a nice fit for max with such an assumption. I'm worried about complicated constructions, where you have an elaborate proof that s is not empty. Putting s ≠ ∅ in a type class argument makes also some constructions very unpleasent, like using finset.filter

[Reid Barton]

Maybe the version returning option is most flexible then. If you want the version that uses inhabited, you can apply option.iget.

[Sean Leather]

@Reid Barton Are you referring to max [decidable_linear_order α] : finset α → option α. that returns none for an empty finset and some a for a non-empty finset? That would be fine with me.

[Reid Barton]

Yes. Or more generally, fold1 f : finset α → option α for an associative and commutative operation f.

[Sean Leather]

For those not following along on GitHub, leanprove/mathlib#133 has been updated with new versions of the definitions under discussion:

finset.max [decidable_linear_order α] : finset α → option α
finset.min [decidable_linear_order α] : finset α → option α

I think this proposal is better than the original. Thanks to everyone for the discussion and collaboration. Feedback welcome.

[Patrick Massot]

So, how do we use this new toy? Say I want to talk about the function "max of coordinates on ℝ^n", assuming n is a British natural number, so I get a well defined function from ℝ^n to ℝ

[Patrick Massot]

I can't even find the lemma saying the image of finset is a finset

[Johannes Hölzl]

Its already in the type of finset.image.
To do what you want: λx, (univ.image (λn, x n)).max.iget