Zulip Chat Archive

Stream: Is there code for X?

Topic: finset.sup'


view this post on Zulip Scott Morrison (Apr 12 2021 at 05:39):

No one has finset.sup' (for nonempty finsets, but only requiring semilattice_sup rather than semilattice_sup_bot) up their sleeves, do they? It seems like an obvious omission, but I'm not so keen to go fill it in right now. :-)

view this post on Zulip Eric Wieser (Apr 12 2021 at 05:43):

There's a recent open PR for this

view this post on Zulip Scott Morrison (Apr 12 2021 at 05:44):

I better go review it! :-)

view this post on Zulip Scott Morrison (Apr 12 2021 at 05:45):

#7087

view this post on Zulip Scott Morrison (Apr 12 2021 at 05:49):

It already looks in great shape. (Thanks, @Alistair Tucker, for having exactly what I wanted ready. :-)

view this post on Zulip Scott Morrison (Apr 12 2021 at 05:51):

:merge:

view this post on Zulip Eric Wieser (Apr 12 2021 at 06:11):

That PR raises an omission in our naming guide, with finset.of_sup_of_forall - how should lemmas be named when their conclusion is p (f x), where p is an argument passed to the lemma?

view this post on Zulip Mario Carneiro (Apr 12 2021 at 06:39):

That theorem actually looks like an induction principle. I would call it sup_induction or something like that

view this post on Zulip Scott Morrison (Apr 12 2021 at 09:08):

@Alistair Tucker, I'm finding I need

@[simp] lemma lt_sup'_iff [is_total α ()] (a : α) : a < s.sup' H f  ( b  s, a < f b) :=

Any chance you want to do the le version, and the inf' analogues?

view this post on Zulip Scott Morrison (Apr 12 2021 at 09:09):

I have a terrible proof of the above...

view this post on Zulip Ruben Van de Velde (Apr 12 2021 at 09:45):

How do you feel about this?

import data.finset
variables {α β : Type*} [semilattice_sup α]
open finset

lemma sup_of_mem {s : finset β} (f : β  α) {b : β} (h : b  s) :
   (a : α), s.sup (coe  f : β  with_bot α) = a := sorry

def finset.sup' (s : finset β) (H : s.nonempty) (f : β  α) : α :=
option.get $ let b, hb := H in option.is_some_iff_exists.2 (sup_of_mem f hb)

variables {s : finset β} (H : s.nonempty) (f : β  α)

lemma sup'_le {a : α} (hs :  b  s, f b  a) : s.sup' H f  a := sorry
@[simp] lemma sup'_le_iff {a : α} : s.sup' H f  a   b  s, f b  a := sorry

@[simp] lemma not_lt' [is_total α ()] {a b : α} : ¬ a < b  b  a :=
begin
  split; intro h,
  { cases total_of () a b with h1 h1,
    { rw h1.lt_or_eq.resolve_left h },
    { exact h1 } },
  { cases total_of () a b with h1 h1,
    { rw le_antisymm h h1, apply lt_irrefl },
    { exact not_lt_of_le h } },
end

@[simp] lemma lt_sup'_iff [is_total α ()] (a : α) (s : finset β) (H : s.nonempty) (f : β  α) :
  a < s.sup' H f  ( b  s, a < f b) :=
begin
  suffices : ¬(a < s.sup' H f)  ¬( b  s, a < f b),
  { have := not_congr this,
    rwa [not_not, not_not] at this },
  push_neg,
  simp_rw [not_lt', sup'_le_iff H f]
end

view this post on Zulip Eric Wieser (Apr 12 2021 at 09:50):

Why doesn't docs#not_lt work for you there? Do we have examples where [is_total α (≤)] but not [linear_order α]?

view this post on Zulip Eric Wieser (Apr 12 2021 at 09:58):

not_lt' golfs slightly to:

@[simp] lemma not_lt' [semilattice_sup α] [is_total α ()] {a b : α} : ¬ a < b  b  a :=
@not_lt _ {
  le_total := is_total.total,
  decidable_le := classical.dec_rel _,
  decidable_eq := classical.dec_eq _,
  decidable_lt := classical.dec_rel _,
  ..(infer_instance : partial_order α) } _ _

view this post on Zulip Eric Wieser (Apr 12 2021 at 09:59):

But this feels silly, because

example {α} [linear_order α] : semilattice_sup α := infer_instance

view this post on Zulip Eric Wieser (Apr 12 2021 at 10:00):

So I think is_total is probably a wrong turn in @Scott Morrison's requested statement

view this post on Zulip Ruben Van de Velde (Apr 12 2021 at 10:17):

It's nicer with linear_order, definitely.

@[simp] lemma lt_sup'_iff [linear_order α] (a : α) (s : finset β) (H : s.nonempty) (f : β  α) :
  a < s.sup' H f  ( b  s, a < f b) :=
begin
  split; { contrapose!, rw sup'_le_iff H f, exact id }
end

Even better if contrapose handled iffs

view this post on Zulip Scott Morrison (Apr 12 2021 at 11:17):

Thanks @Ruben Van de Velde, that's nice! I can roll this, and the variations, into an upcoming PR, unless you feel like getting to them first!

view this post on Zulip Ruben Van de Velde (Apr 12 2021 at 11:21):

No, go for it

view this post on Zulip Bhavik Mehta (Apr 12 2021 at 11:36):

Eric Wieser said:

Why doesn't docs#not_lt work for you there? Do we have examples where [is_total α (≤)] but not [linear_order α]?

I don't know if we have examples in mathlib yet but it's not hard to come up with examples in maths - Peter mentioned one a couple of days ago: consider the order given by inv_image where the target is a linear order, then the new order is a total preorder but it's not antisymmetric

view this post on Zulip Eric Wieser (Apr 12 2021 at 12:37):

In the example above there was already a [semilattice_sup α] assumption - but I see I didn't make it clear in that question

view this post on Zulip Alistair Tucker (Apr 12 2021 at 15:12):

Following the pattern in the rest of the file, one would first prove that

lemma lt_sup_iff [is_total α ()] {a : α} : a < s.sup f  ( b  s, a < f b)

(It should be in there anyway for completeness.) Then it's pretty straightforward to do a version for sup'.

lemma lt_sup'_iff [is_total α ()] {a : α} : a < s.sup' H f  ( b  s, a < f b) :=
begin
  rw [with_bot.coe_lt_coe, coe_sup', lt_sup_iff],
  exact bex_congr (λ b hb, with_bot.coe_lt_coe),
end

view this post on Zulip Alistair Tucker (Apr 12 2021 at 15:13):

There was some reason why I had to go down the is_total route rather than linear_order but I can't remember right now

view this post on Zulip Alistair Tucker (Apr 12 2021 at 15:21):

I would probably have proved lt_sup_iff by induction like so

lemma lt_sup_iff [is_total α ()] {a : α} : a < s.sup f   b  s, a < f b :=
begin
  split,
  { intro h,
    induction s using finset.cons_induction with b s hb ih,
    { exact false.elim (not_lt_bot h), },
    { rw [sup_cons, _root_.lt_sup_iff] at h,
      cases h,
      { exact b, mem_cons.2 (or.inl rfl), h⟩, },
      { rcases ih h with c, hc, hlt⟩,
        exact c, mem_cons.2 (or.inr hc), hlt⟩, }, }, },
  { rintro b, hb, hlt⟩,
    exact lt_of_lt_of_le hlt (le_sup hb), },
end

But maybe Ruben's proof points to a better way... let me check.

view this post on Zulip Eric Wieser (Apr 12 2021 at 16:23):

You probably went down the is_total route because [linear_order α] [semilattice_sup α] introduced two different has_les

view this post on Zulip Eric Wieser (Apr 12 2021 at 16:25):

But [linear_order α] by itself induces a semilattice_sup α anyway, so there's no need for both

view this post on Zulip Alistair Tucker (Apr 12 2021 at 16:53):

I've made a branch for this. Based on Ruben's proof although it turns out there is such a thing as as_linear_order which makes it considerably shorter. @Ruben Van de Velde or @Eric Wieser would either of you like to make changes and/or a PR? I suppose Scott will be asleep atm.

view this post on Zulip Alistair Tucker (Apr 12 2021 at 16:54):

Oops https://github.com/leanprover-community/mathlib/tree/lt_sup_iff

view this post on Zulip Alistair Tucker (Apr 12 2021 at 16:56):

You probably went down the is_total route because...

Maybe something about having bot? I'll check later

view this post on Zulip Eric Wieser (Apr 12 2021 at 16:58):

I'd missed that your last PR already added the is_total arguments - I'll play with removing them

view this post on Zulip Eric Wieser (Apr 12 2021 at 16:58):

Do we have those arguments on lemmas about docs#finset.max'?

view this post on Zulip Eric Wieser (Apr 12 2021 at 17:04):

Oh you're right, bot is indeed the issue

view this post on Zulip Eric Wieser (Apr 12 2021 at 17:05):

Which was needed for sup, but not sup'

view this post on Zulip Eric Wieser (Apr 12 2021 at 17:11):

But sup is still a mess for similar reasons. Perhaps we should have a linear_order_bot and linear_order_top class, to sit between docs#linear_order and docs#complete_linear_order?

view this post on Zulip Kevin Buzzard (Apr 12 2021 at 18:36):

When I was a lad back in 2017, there was just lattice, semilattice_sup_bot, semilattice_inf_top, conditionally_complete_lattice, and then complete_lattice. Then people wanted semilattice_sup_top and semilattice_inf_bot, and now we're getting variants with total orders. Similarly we now seem to have monoids with 0, add_monoids with 1 and so on. My impression is that given any subset of the set of all notation coming up in the topological hierarchy, sooner or later someone will want an object which has all of the subset but nothing else, because their favourite mathematical object has precisely this subset but not the rest. The same is happening in the algebraic heirarchy -- all this distrib_mul_action stuff is what you get with + and * but no 0 or 1, for example, with added heterogeneous issues thrown in. People seem really reluctant to pull off everything into pieces, because then complete_lattice would extend has_bot, has_top, has_sup, has_Sup, has_inf, has_Inf and then there would be a gazillion Props on top. But my impression is that this is somehow the way we're moving. Is there some more principled way of doing this stuff rather than just inventing 2^N new typeclasses?

view this post on Zulip Eric Wieser (Apr 12 2021 at 20:45):

I believe that the defs in core around src#is_total was an attempt at such a principled approach - there seems to be an @[algebra] attribute for some feature that I can only assume never materialized.

view this post on Zulip Alistair Tucker (Apr 13 2021 at 07:19):

@Eric Wieser So should we regard is_total as a great thing or as an outdated piece of junk? You don't seem to approve of it but for example a version of exists_mem_eq_sup written for [semilattice_sup_bot α] [is_total α (≤)] instead of [complete_linear_order α ] would resolve the problem with that cropped up in this thread https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/strict.20instance.20requirement.

view this post on Zulip Eric Wieser (Apr 13 2021 at 07:21):

I'm no longer sure

view this post on Zulip Mario Carneiro (Apr 13 2021 at 07:23):

It's useful when working with general relations that aren't the le on the type

view this post on Zulip Eric Wieser (Apr 13 2021 at 07:23):

If is_total (\le) is a good thing, then we should change as many lemmas as possible to use it instead of linear_order

view this post on Zulip Mario Carneiro (Apr 13 2021 at 07:24):

A total semilattice is a lattice

view this post on Zulip Mario Carneiro (Apr 13 2021 at 07:24):

in fact it is a linear order

view this post on Zulip Mario Carneiro (Apr 13 2021 at 07:25):

Maybe we need linear_order_bot?

view this post on Zulip Eric Wieser (Apr 13 2021 at 07:26):

Either we need that, or we need to switch to using is_total as a mixing for totality

view this post on Zulip Mario Carneiro (Apr 13 2021 at 07:26):

how many theorems need this combo?

view this post on Zulip Eric Wieser (Apr 13 2021 at 07:27):

Currently we're in a middle ground where we have to switch between the two and end up reproving things like not_lt_iff as happened up thread

view this post on Zulip Eric Wieser (Apr 13 2021 at 07:27):

I think I found 2 within finset.lattice, and another two for the top version

view this post on Zulip Mario Carneiro (Apr 13 2021 at 07:27):

if it's only those then I guess the is_total mixin is fine

view this post on Zulip Eric Wieser (Apr 13 2021 at 07:28):

I haven't searched mathlib-wide

view this post on Zulip Mario Carneiro (Apr 13 2021 at 07:28):

That's okay, you can just convert lemmas when you find them / need them

view this post on Zulip Mario Carneiro (Apr 13 2021 at 07:29):

Looking is_total up is more expensive since it's two typeclass searches with one dependent on the other, so I don't think we want to use too many mixins

view this post on Zulip Eric Wieser (Apr 13 2021 at 07:44):

Doesn't the dependency make it less expensive?


Last updated: May 17 2021 at 16:26 UTC