Zulip Chat Archive

Stream: new members

Topic: finset.max'


view this post on Zulip 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)?

view this post on Zulip Alistair Tucker (Aug 06 2020 at 13:09):

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

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip Alistair Tucker (Aug 11 2020 at 01:17):

To give you the second from the first automatically

view this post on Zulip Jalex Stark (Aug 11 2020 at 08:35):

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

view this post on Zulip Alistair Tucker (Aug 11 2020 at 10:47):

(deleted)

view this post on Zulip Alistair Tucker (Aug 11 2020 at 10:50):

(deleted)


Last updated: May 13 2021 at 06:15 UTC