complete_lattice (with_top ℕ)

Stream: maths

[Eric Wieser]

Is this missing, or untrue?

[Johan Commelin]

I could only find

noncomputable instance : bounded_lattice enat :=
{ inf := min,
  inf_le_left := min_le_left,
  inf_le_right := min_le_right,
  le_inf := λ _ _ _, le_min,
  ..enat.order_top,
  ..enat.semilattice_sup_bot }

[Eric Wieser]

Yeah, I can find a bounded_lattice on with_top nat too

[Eric Wieser]

My motivation was to apply docs#exists_mem_eq_sup, so I guess the assumptions on that lemma are too strict

[Eric Wieser]

And therfore a new bounded_linear_order typeclass is needed?
(class bounded_linear_order extends bounded_lattice β, linear_order β)

[Rémy Degenne]

You should get it from docs#with_top.complete_linear_order

@[instance]
def with_top.complete_linear_order {α : Type u_1} [conditionally_complete_linear_order_bot α] :
complete_linear_order (with_top α)

since we have that N is a conditionally_complete_linear_order_bot

[Eric Wieser]

Thanks, I needed to import order.conditionally_complete_lattice

[Rémy Degenne]

and there is also docs#enat.complete_linear_order

[Eric Wieser]

Bad things seem to happen when I use that instance:

import order.conditionally_complete_lattice
import data.finset.lattice

variables {ι : Type*} [fintype ι] (foo : ι → ℕ)

open finset

def min_or_zero : ℕ :=
option.get_or_else (univ.sup (λ v, foo v) : with_top ℕ) 0

lemma exists_eq_min_or_zero [nonempty ι] :
  ∃ v, foo v = min_or_zero foo :=
begin
  obtain ⟨v', _, hv'⟩ :=
    exists_mem_eq_sup finset.univ univ_nonempty (λ v, (foo v : with_top ℕ)),
  refine ⟨v', _⟩,
  unfold min_or_zero,
  convert (option.get_or_else_coe _ _).symm,
  convert hv',
  sorry,
  -- canonically_linear_ordered_add_monoid.semilattice_sup_bot = semilattice_sup_bot_of_bounded_lattice (with_top ℕ)
end

[Eric Wieser]

The enat version works, but roption.get_or_else is hard to use

[Rémy Degenne]

this is the same issue as the other day with ennreal, with canonically_linear_ordered_add_monoid causing duplicate sup/bot when using that instance of semilattice_sup_bot

[Eric Wieser]

The full state is

@canonically_linear_ordered_add_monoid.semilattice_sup_bot (with_top ℕ)
      (@with_top.canonically_linear_ordered_add_monoid ℕ nat.canonically_linear_ordered_add_monoid) =
    @semilattice_sup_bot_of_bounded_lattice (with_top ℕ)
      (@complete_lattice.to_bounded_lattice (with_top ℕ)
         (@complete_linear_order.to_complete_lattice (with_top ℕ)
            (@with_top.complete_linear_order ℕ nat.conditionally_complete_linear_order_bot)))

[Rémy Degenne]

On branch#ennreal_lattice_issue I tried removing the instance canonically_linear_ordered_add_monoid.semilattice_sup_bot and after a small fix to one lemma about finsupp, it does not seem to cause any issue. But then you can't use any lemma for semilattice_sup_bot on a canonically_linear_ordered_add_monoid, which is a shame. I don't know enough about how those things work to be able to fix it

[Rémy Degenne]

The semilattice and order_bot parts of semilattice_sup_bot come from two different ancestors of canonically_linear_ordered_add_monoid. It looks like the way they are combined is not correct (in a way I don't understand)

[Eric Wieser]

This gives some hints of exactly what doesn't match - it's just the sup, the other operators are fine:

import order.conditionally_complete_lattice
import data.finset.lattice

variables {ι : Type*} [fintype ι] (foo : ι → ℕ)

open finset

def min_or_zero : ℕ :=
option.get_or_else (univ.sup (λ v, foo v) : with_top ℕ) 0

@[ext]
lemma semilattice_sup_bot.ext [α : Type*] (a b : semilattice_sup_bot α)
  (h_bot : a.bot = b.bot) (h_sup : a.sup = b.sup) (h_le : a.le = b.le) (h_lt : a.lt = b.lt) : a = b :=
begin
  casesI a, casesI b,
  congr,
  assumption',
end

lemma exists_eq_min_or_zero [nonempty ι] :
  ∃ v, foo v = min_or_zero foo :=
begin
  obtain ⟨v', _, hv'⟩ :=
    exists_mem_eq_sup finset.univ univ_nonempty (λ v, (foo v : with_top ℕ)),
  refine ⟨v', _⟩,
  unfold min_or_zero,
  convert (option.get_or_else_coe _ _).symm,
  convert hv',
  ext1,
  { congr, },
  { dunfold semilattice_sup_bot.sup lattice.sup bounded_lattice.sup complete_lattice.sup
      complete_linear_order.sup semilattice_sup_top.sup,
    -- max = λ (o₁ o₂ : with_top ℕ), option.bind o₁ (λ (a : ℕ), option.map (λ (b : ℕ), a ⊔ b) o₂)
    sorry },
  { congr, },
  { congr, },
end