finset.sup'

Stream: Is there code for X?

[Scott Morrison]

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]

There's a recent open PR for this

[Scott Morrison]

I better go review it! :-)

[Scott Morrison]

#7087

[Scott Morrison]

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

[Scott Morrison]

[Eric Wieser]

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]

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

[Scott Morrison]

@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]

I have a terrible proof of the above...

[Ruben Van de Velde]

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]

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

[Eric Wieser]

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]

But this feels silly, because

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

[Eric Wieser]

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

[Ruben Van de Velde]

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]

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]

No, go for it

[Bhavik Mehta]

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]

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]

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]

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]

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]

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

[Eric Wieser]

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

[Alistair Tucker]

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]

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

[Alistair Tucker]

You probably went down the is_total route because...

Maybe something about having bot? I'll check later

[Eric Wieser]

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

[Eric Wieser]

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

[Eric Wieser]

Oh you're right, bot is indeed the issue

[Eric Wieser]

Which was needed for sup, but not sup'

[Eric Wieser]

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]

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]

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]

@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]

I'm no longer sure

[Mario Carneiro]

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

[Eric Wieser]

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]

A total semilattice is a lattice

[Mario Carneiro]

in fact it is a linear order

[Mario Carneiro]

Maybe we need linear_order_bot?

[Eric Wieser]

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

[Mario Carneiro]

how many theorems need this combo?

[Eric Wieser]

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]

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

[Mario Carneiro]

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

[Eric Wieser]

I haven't searched mathlib-wide

[Mario Carneiro]

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

[Mario Carneiro]

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]

Doesn't the dependency make it less expensive?