Zulip Chat Archive

Stream: new members

Topic: strict instance requirement


view this post on Zulip Pontus Sundqvist (Mar 24 2021 at 19:51):

I'm trying to use finset.exists_mem_eq_sup when β is nat but it wants a [complete_linear_order β]. And I'm guessing nat isn't a complete_linear_order? But when I rewrite the theorem with nat and without requiring [complete_linear_order ℕ], with the exact same proof, then the theorem compiles. I'm also finding it hard to figure out which instances are actually being used in the proof.

Am I missing something or are the requirements on the theorem too strict?

view this post on Zulip Kevin Buzzard (Mar 24 2021 at 19:52):

you're missing a #mwe so we can all figure out the details of what you're talking about.

view this post on Zulip Kevin Buzzard (Mar 24 2021 at 19:53):

I agree that nat isn't a complete linear order, because an arbitrary collection of naturals might not have a (finite) sup.

view this post on Zulip Kevin Buzzard (Mar 24 2021 at 19:54):

PS you can just do docs#finset.exists_mem_eq_sup to save you having to cut and paste the full URL.

view this post on Zulip Kevin Buzzard (Mar 24 2021 at 19:57):

import data.finset.lattice

namespace finset

open order_dual multiset

universes u_1 u_2 u_3
variables {α : Type u_1} {β : Type u_2} {γ : Type u_3}

lemma exists_mem_eq_sup' (s : finset α) (h : s.nonempty) (f : α  ) :
   a, a  s  s.sup f = f a :=
begin
  classical,
  induction s using finset.induction_on with x xs hxm ih,
  { exact (not_nonempty_empty h).elim, },
  { rw sup_insert,
    by_cases hx : xs.sup f  f x,
    { refine x, mem_insert_self _ _, sup_eq_left.mpr hx⟩, },
    by_cases hxs : xs.nonempty,
    { obtain a, ham, ha := ih hxs,
      refine a, mem_insert_of_mem ham, _⟩,
      simpa only [ha, sup_eq_right] using le_of_not_le hx, },
    { rw not_nonempty_iff_eq_empty.mp hxs,
      refine x, mem_singleton_self _, _⟩,
      simp, } }
end

end finset

I've managed to reproduce.

view this post on Zulip Pontus Sundqvist (Mar 24 2021 at 20:01):

Thanks. You're right, I should have posted that to begin with.

view this post on Zulip Kevin Buzzard (Mar 24 2021 at 20:01):

It seems to me that the proof for general beta needs semilattice_sup_bot and linear_order; both of these extend partial_order unfortunately, so it's difficult (for me) to put both structures on a type at once in a compatible way.

view this post on Zulip Kevin Buzzard (Mar 24 2021 at 20:03):

set_option old_structure_cmd true
class semilattice_sup_bot_linear_order_mashup (β : Type*)
  extends semilattice_sup_bot β, linear_order β

lemma exists_mem_eq_sup' [semilattice_sup_bot_linear_order_mashup β] (s : finset α) (h : s.nonempty) (f : α  β) :
   a, a  s  s.sup f = f a :=
begin
  classical,
  induction s using finset.induction_on with x xs hxm ih,
  { exact (not_nonempty_empty h).elim, },
  { rw sup_insert,
    by_cases hx : xs.sup f  f x,
    { refine x, mem_insert_self _ _, sup_eq_left.mpr hx⟩, },
    by_cases hxs : xs.nonempty,
    { obtain a, ham, ha := ih hxs,
      refine a, mem_insert_of_mem ham, _⟩,
      simpa only [ha, sup_eq_right] using le_of_not_le hx, },
    { rw not_nonempty_iff_eq_empty.mp hxs,
      refine x, mem_singleton_self _, _⟩,
      simp, } }
end

view this post on Zulip Kevin Buzzard (Mar 24 2021 at 20:08):

instance : semilattice_sup_bot_linear_order_mashup  :=
{ ..(show semilattice_sup_bot , by apply_instance),
  ..(show linear_order , by apply_instance) }

view this post on Zulip Kevin Buzzard (Mar 24 2021 at 20:09):

instance [complete_linear_order β] : semilattice_sup_bot_linear_order_mashup β :=
{ ..(show linear_order β, by apply_instance),
  ..(show semilattice_sup_bot β, by apply_instance)
  } -- fails
/-
type mismatch at field 'bot_le'
  semilattice_sup_bot.bot_le
has type
  ∀ (a : β),
    @has_le.le β
      (@preorder.to_has_le β
         (@partial_order.to_preorder β
            (@partial_order.mk β (@semilattice_sup_bot.le β (show semilattice_sup_bot β, from ?m_1))
               (@semilattice_sup_bot.lt β (show semilattice_sup_bot β, from ?m_1))
               _
               _
               _
               _)))
      (@has_bot.bot β (@has_bot.mk β (@semilattice_sup_bot.bot β (show semilattice_sup_bot β, from ?m_1))))
      a
but is expected to have type
  ∀ (a : β),
    @has_le.le β
      (@preorder.to_has_le β
         (@partial_order.to_preorder β
            (@partial_order.mk β
               (@linear_order.le β (show linear_order β, from @complete_linear_order.to_linear_order β _inst_1))
               (@linear_order.lt β (show linear_order β, from @complete_linear_order.to_linear_order β _inst_1))
               _
               _
               _
               _)))
      (@has_bot.bot β (@has_bot.mk β (@semilattice_sup_bot.bot β (show semilattice_sup_bot β, from ?m_1))))
      a
-/

aargh

view this post on Zulip Kevin Buzzard (Mar 24 2021 at 20:13):

Got it working:

import data.finset.lattice


open order_dual multiset

universes u_1 u_2 u_3
variables {α : Type u_1} {β : Type u_2} {γ : Type u_3}

set_option old_structure_cmd true
class semilattice_sup_bot_linear_order_mashup (β : Type*)
  extends semilattice_sup_bot β, linear_order β

instance : semilattice_sup_bot_linear_order_mashup  :=
{ ..(show semilattice_sup_bot , by apply_instance),
  ..(show linear_order , by apply_instance) }

instance foo [complete_linear_order β] : linear_order β := infer_instance
instance bar [complete_linear_order β] : semilattice_sup_bot β := infer_instance

instance baz [complete_linear_order β] : semilattice_sup_bot_linear_order_mashup β :=
{ ..foo,
  ..bar
  }

namespace finset

lemma exists_mem_eq_sup' [semilattice_sup_bot_linear_order_mashup β] (s : finset α) (h : s.nonempty) (f : α  β) :
   a, a  s  s.sup f = f a :=
begin
etc etc
end

end finset

view this post on Zulip Kevin Buzzard (Mar 24 2021 at 20:14):

so yes you're right, one can get away with weaker typeclass assumptions, however it seems to me that it might involve making a new typeclass.

view this post on Zulip Kevin Buzzard (Mar 24 2021 at 20:17):

instance baz [complete_linear_order β] : semilattice_sup_bot_linear_order_mashup β :=
{ ..(infer_instance : linear_order β),
  ..(infer_instance : semilattice_sup_bot β) }

Got it working -- dunno why I had that weird error (which I blamed on a diamond but which might not be the case) earlier.

view this post on Zulip Eric Wieser (Mar 24 2021 at 22:25):

Would the docs#finset.exists_mem_eq_sup lemma have worked for docs#conditionally_complete_linear_order?

view this post on Zulip Eric Wieser (Mar 24 2021 at 22:27):

I wrote that lemma to try and prove to Bhavik Mehta that some graph theory degree stuff was overkill and that there was already enough api about finsets, but concluded that actually the API was too sparse to be useful.

view this post on Zulip Eric Wieser (Mar 24 2021 at 22:35):

Ah, I think I remember getting stuck because order.conditionally_complete_lattice can't be imported in data.finset.lattice. And also that typeclass doesn't work anyway.

view this post on Zulip Mario Carneiro (Mar 24 2021 at 22:46):

Note that every linear_order is already a lattice, so this mashup is just linear_order_with_bot

view this post on Zulip Kevin Buzzard (Mar 25 2021 at 08:09):

In other words a linear order where all finite sups exist. Examples are nat and nnreal

view this post on Zulip Alistair Tucker (Apr 14 2021 at 08:19):

@Pontus Sundqvist I think this lemma should work for nat now.


Last updated: May 14 2021 at 04:22 UTC