## Stream: new members

### Topic: finset.max'

#### Alistair Tucker (Aug 06 2020 at 13:06):

Given import data.finset and variables (α β : Type) [decidable_linear_order β] (f : α → β) (s : finset α) (h : s.nonempty)
is there an easier way to write finset.max' (s.image f) (finset.nonempty.image h f)?

#### Alistair Tucker (Aug 06 2020 at 13:09):

Could max' be defined on multiset instead? and then simply lifted to finset?

#### Floris van Doorn (Aug 07 2020 at 16:19):

is there an easier way to write finset.max' (s.image f) (finset.nonempty.image h f)?

Not really (currently), other than the shortening (s.image f).max' (h.image f).

Could max' be defined on multiset instead? and then simply lifted to finset?

That would be possible. Would that help you though?

#### Alistair Tucker (Aug 07 2020 at 21:59):

Thanks! What seemed awkward to me was having to compute the image, removing duplicates, before taking the max. If it were defined on multiset, I could write something like (s.1.map f).max' (mem_map_of_mem' f h) and avoid that step.

For my purposes it would also be handy to have this work for semilattice_sup rather than decidable_linear_order. So I have been playing with defining a sup' which is to sup as max' is to max.

namespace multiset
section sup'
variables {α β : Type*} [semilattice_sup α]

theorem sup_of_mem {s : multiset α} {a : α} (h : a ∈ s) :
∃ b, @sup (with_bot α) _ (s.map some) = some b :=
(@le_sup (with_bot α) _ _ _ (mem_map_of_mem some h) a rfl).imp (λ b, Exists.fst)

def sup' (s : multiset α) (H : ∃ a : α, a ∈ s) : α :=
@option.get α (s.map some : multiset (with_bot α)).sup $let ⟨a, ha⟩ := H in let ⟨b, hb⟩ := sup_of_mem ha in by simp [hb] lemma mem_map_of_mem' {s : multiset β} (f : β → α) (H : ∃ b, b ∈ s) : ∃ a : α, a ∈ s.map f := let ⟨b, hb⟩ := H in ⟨f b, multiset.mem_map_of_mem f hb⟩ end sup' end multiset  Now I have a choice. I could define finset.sup' using multiset.sup' like this: namespace finset section sup' variables {α β : Type*} [semilattice_sup α] def sup' (s : finset β) (H : s.nonempty) (f : β → α) : α := (s.1.map f).sup' (multiset.mem_map_of_mem' f H) lemma sup'_def (s : finset β) (H : s.nonempty) (f : β → α) : s.sup' H f = (s.1.map f).sup' (multiset.mem_map_of_mem' f H) := rfl end sup' section max_min variables {α β : Type*} [decidable_linear_order α] theorem max'_eq_sup' (s : finset α) (H : s.nonempty) : s.max' H = s.1.sup' H := rfl end max_min end finset  or I could define it using finset.sup like this: namespace finset section sup' variables {α β : Type*} [semilattice_sup α] theorem sup_of_mem {s : finset β} (f : β → α) {b : β} (h : b ∈ s) : ∃ a, @sup (with_bot α) β _ s (some ∘ f) = some a := Exists.imp (λ b, Exists.fst) (@le_sup (with_bot α) β _ s (some ∘ f) b h (f b) rfl) def sup' (s : finset β) (H : s.nonempty) (f : β → α) : α := @option.get α (sup s (some ∘ f) : with_bot α)$
let ⟨k, hk⟩ := H in
let ⟨b, hb⟩ := sup_of_mem f hk in by simp [hb]

lemma sup_def' (s : finset α) (H : s.nonempty) : s.sup' H id = s.1.sup' H :=
rfl

end sup'

section max_min
variables {α β : Type*} [decidable_linear_order α]

theorem max'_eq_sup' (s : finset α) (H : s.nonempty) : s.max' H = s.1.sup' H :=
rfl

theorem max'_eq_sup'_id (s : finset α) (H : s.nonempty) : s.max' H = s.sup' H id :=
rfl

end max_min
end finset


#### Alistair Tucker (Aug 10 2020 at 18:33):

Basically by copying and pasting from finset.max', I made a minimal API for multiset.sup' here https://github.com/leanprover-community/mathlib/compare/master...agjftucker:master#diff-38b2e2b9f83fc5c799388cc6931a902f.
It works for semilattice_sup α, unlike finset.max' which requires decidable_linear_order and, naturally, unlike multiset.sup or finset.sup which require semilattice_sup_bot. Moreover because it is in multiset rather than finset we can use map rather than image even when dealing with a function not provably injective, thus achieving the same goal without introducing a spurious computation.

#### Alistair Tucker (Aug 10 2020 at 18:35):

I claim that multiset.sup' is more general than finset.max' and also that it can act as a drop-in replacement. In my fork I have quite easily made the small number of changes required to get mathlib to typecheck with the definitions offinset.max, min, max' and min' removed. I think such a culling is at least worth thinking about because there is a lot going on in finset and often multiple ways of doing things. It hurts my head :smile: I have only adapted a fraction of the theorems from finset.max' so consider this no more than a proof of concept.

#### Jalex Stark (Aug 10 2020 at 19:34):

hmm. in your world I have to do a coercion to my finset before getting the max out of it?

#### Alistair Tucker (Aug 10 2020 at 20:31):

Well currently I think there is no coercion from finset to multiset so I have added a .1 where necessary. It's a very small overhead, but to get rid of it one could either define that coercion (I guess?) or extend sup' to finset in one of the ways I outlined above.

#### Jalex Stark (Aug 10 2020 at 22:04):

Ah, I think I understand now. You've proven theorems that are more general than the old theorems about finset.max.

#### Jalex Stark (Aug 10 2020 at 22:08):

Instead of "using multiset.sup as a drop-in replacement for finset.max", you should replace the proofs of the finset.max theorems with applications of the multiset.sup theorems.

#### Jalex Stark (Aug 10 2020 at 22:09):

one could probably write a metaprogram to generate parts of the finset API from parts of the multiset API.

#### Alistair Tucker (Aug 11 2020 at 01:04):

Then you would be left with a bunch of max definitions and theorems requiring decidable_linear_order when semilattice_sup would suffice. I thought that's what typeclass inference was for?

#### Alistair Tucker (Aug 11 2020 at 01:17):

To give you the second from the first automatically

#### Jalex Stark (Aug 11 2020 at 08:35):

You could weaken the typeclass argument for finset.max without renaming it

(deleted)

#### Alistair Tucker (Aug 11 2020 at 10:50):

(deleted)

Last updated: May 13 2021 at 06:15 UTC