Zulip Chat Archive

Stream: Is there code for X?

Topic: finset.sup'


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. :-)

Eric Wieser (Apr 12 2021 at 05:43):

There's a recent open PR for this

Scott Morrison (Apr 12 2021 at 05:44):

I better go review it! :-)

Scott Morrison (Apr 12 2021 at 05:45):

#7087

Scott Morrison (Apr 12 2021 at 05:49):

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

Scott Morrison (Apr 12 2021 at 05:51):

:merge:

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?

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

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?

Scott Morrison (Apr 12 2021 at 09:09):

I have a terrible proof of the above...

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

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 α]?

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 α) } _ _

Eric Wieser (Apr 12 2021 at 09:59):

But this feels silly, because

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

Eric Wieser (Apr 12 2021 at 10:00):

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

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

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!

Ruben Van de Velde (Apr 12 2021 at 11:21):

No, go for it

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

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

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

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

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.

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

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

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.

Alistair Tucker (Apr 12 2021 at 16:54):

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

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

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

Eric Wieser (Apr 12 2021 at 16:58):

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

Eric Wieser (Apr 12 2021 at 17:04):

Oh you're right, bot is indeed the issue

Eric Wieser (Apr 12 2021 at 17:05):

Which was needed for sup, but not sup'

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?

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?

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.

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.

Eric Wieser (Apr 13 2021 at 07:21):

I'm no longer sure

Mario Carneiro (Apr 13 2021 at 07:23):

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

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

Mario Carneiro (Apr 13 2021 at 07:24):

A total semilattice is a lattice

Mario Carneiro (Apr 13 2021 at 07:24):

in fact it is a linear order

Mario Carneiro (Apr 13 2021 at 07:25):

Maybe we need linear_order_bot?

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

Mario Carneiro (Apr 13 2021 at 07:26):

how many theorems need this combo?

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

Eric Wieser (Apr 13 2021 at 07:27):

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

Mario Carneiro (Apr 13 2021 at 07:27):

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

Eric Wieser (Apr 13 2021 at 07:28):

I haven't searched mathlib-wide

Mario Carneiro (Apr 13 2021 at 07:28):

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

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

Eric Wieser (Apr 13 2021 at 07:44):

Doesn't the dependency make it less expensive?


Last updated: Dec 20 2023 at 11:08 UTC