finset.max'

Stream: new members

[Alistair Tucker]

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]

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

[Floris van Doorn]

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]

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]

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]

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]

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

[Alistair Tucker]

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]

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

[Jalex Stark]

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]

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

[Alistair Tucker]

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]

To give you the second from the first automatically

[Jalex Stark]

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

[Alistair Tucker]

(deleted)

[Alistair Tucker]

(deleted)