# Zulip Chat Archive

## 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 of`finset.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

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

(deleted)

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

(deleted)

Last updated: May 13 2021 at 06:15 UTC