strict instance requirement

Stream: new members

[Pontus Sundqvist]

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?

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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.

[Pontus Sundqvist]

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

[Kevin Buzzard]

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.

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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.

[Kevin Buzzard]

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.

[Eric Wieser]

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

[Eric Wieser]

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.

[Eric Wieser]

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.

[Mario Carneiro]

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

[Kevin Buzzard]

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

[Alistair Tucker]

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