Zulip Chat Archive

Stream: maths

Topic: complete_lattice (with_top ℕ)


view this post on Zulip Eric Wieser (Feb 12 2021 at 16:40):

Is this missing, or untrue?

view this post on Zulip Johan Commelin (Feb 12 2021 at 16:45):

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 }

view this post on Zulip Eric Wieser (Feb 12 2021 at 16:46):

Yeah, I can find a bounded_lattice on with_top nat too

view this post on Zulip Eric Wieser (Feb 12 2021 at 16:46):

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

view this post on Zulip Eric Wieser (Feb 12 2021 at 16:46):

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

view this post on Zulip Rémy Degenne (Feb 12 2021 at 16:48):

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

view this post on Zulip Eric Wieser (Feb 12 2021 at 16:50):

Thanks, I needed to import order.conditionally_complete_lattice

view this post on Zulip Rémy Degenne (Feb 12 2021 at 16:53):

and there is also docs#enat.complete_linear_order

view this post on Zulip Eric Wieser (Feb 12 2021 at 16:57):

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

view this post on Zulip Eric Wieser (Feb 12 2021 at 16:58):

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

view this post on Zulip Rémy Degenne (Feb 12 2021 at 16:59):

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

view this post on Zulip Eric Wieser (Feb 12 2021 at 17:00):

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

view this post on Zulip Rémy Degenne (Feb 12 2021 at 17:03):

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

view this post on Zulip Rémy Degenne (Feb 12 2021 at 17:06):

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)

view this post on Zulip Eric Wieser (Feb 12 2021 at 17:56):

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

Last updated: May 18 2021 at 06:15 UTC