## 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?

#### 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