nnreal lattice broken

Stream: general

[Johan Commelin]

While bumping mathlib in LTE, I hit the following issue.

import data.real.nnreal

open_locale nnreal

example : nnreal.semilattice_inf = lattice.to_semilattice_inf ℝ≥0 := rfl -- fails

[Johan Commelin]

I guess this is a bug in mathlib that wasn't there before. Can we somehow lint against introducing such bugs? I guess that's hard.

[Johan Commelin]

FYI, the LHS is among these derived instances, where as the RHS comes from a chain of instances that ultimately leads to conditionally_complete_linear_order_bot ℝ≥0

@[derive [
  ordered_semiring, comm_monoid_with_zero, -- to ensure these instance are computable
  floor_semiring,
  semilattice_inf, densely_ordered, order_bot,
  canonically_linear_ordered_add_monoid, linear_ordered_comm_group_with_zero, archimedean,
  linear_ordered_semiring, ordered_comm_semiring, canonically_ordered_comm_semiring,
  has_sub, has_ordered_sub, has_div, inhabited]]
def nnreal := {r : ℝ // 0 ≤ r}

-- <snip>

noncomputable instance : conditionally_complete_linear_order_bot ℝ≥0 :=
nonneg.conditionally_complete_linear_order_bot real.Sup_empty.le

[Eric Wieser]

Do you know which field disagrees?

[Yaël Dillies]

Might it have to do with the renaming min → inf, max → sup?

[Mario Carneiro]

looks like inf

[Mario Carneiro]

example : nnreal.semilattice_inf.inf = (lattice.to_semilattice_inf ℝ≥0).inf := rfl -- fails

[Mario Carneiro]

#eval tactic.whnf `(nnreal.semilattice_inf.inf) >>= tactic.trace
-- λ (x y : {x // (λ (x : ℝ), x ∈ set.Ici 0) x}), ⟨x.val ⊓ y.val, _⟩
#eval tactic.whnf `((lattice.to_semilattice_inf ℝ≥0).inf) >>= tactic.trace
-- λ (a b : {x // x ∈ set.Ici 0}), ite (a ≤ b) a b

[Yaël Dillies]

What happens if you replace the RHS with (lattice.to_semilattice_inf ℝ≥0).min?

[Mario Carneiro]

so yes, it looks like the culprit is using min as inf instead of inheriting it

[Yaël Dillies]

Where does this happen? In docs#nonneg.conditionally_complete_linear_order_bot?

[Mario Carneiro]

it gets down to

example :
  (lattice.to_semilattice_inf ℝ≥0).inf =
  (distrib_lattice.to_lattice (set.Ici (0:ℝ))).inf := rfl -- ok
example :
  nnreal.semilattice_inf.inf =
  (distrib_lattice.to_lattice (set.Ici (0:ℝ))).inf := rfl -- fail

[Mario Carneiro]

this is via docs#ord_connected_subset_conditionally_complete_linear_order and docs#subset_conditionally_complete_linear_order

[Mario Carneiro]

note that one of the type class args in distrib_lattice.to_lattice (set.Ici (0:ℝ)) is docs#linear_order.to_distrib_lattice which definitely introduces an if via docs#linear_order.to_lattice which uses inf := min

[Yaël Dillies]

Why do we still carry around min and maxfields, actually? Surely it would be better and safer to only have sup and inf?

[Mario Carneiro]

we don't

[Mario Carneiro]

linear_order.to_lattice clearly needs to make up an inf from min

[Yaël Dillies]

But why does it even have a min in the first place?

[Mario Carneiro]

min is a function

[Mario Carneiro]

not a field

[Mario Carneiro]

if you have a linear order and want a lattice, you have to make up an inf field and the obvious way to do so is if a <= b then a else b also known as min a b

[Mario Carneiro]

I think it might make sense to put inf in linear_order as a field though to avoid this

[Yaël Dillies]

Yes; that was my question all along. Why does linear_order not have a inf field?

[Mario Carneiro]

because it's an order typeclass

[Yaël Dillies]

... precisely?

[Mario Carneiro]

back in the old days we weren't as aggressive about having things at the bottom of the hierarchy have literally everything

[Yaël Dillies]

Yeah, it's more and more common these days. I will myself add another two fields to boolean_algebra soonish.

[Mario Carneiro]

it's also possible to fix this issue in src#subset_conditionally_complete_linear_order without a huge refactor

[Mario Carneiro]

by overriding the inf fields inherited from distrib_lattice.to_lattice s with the ones coming from the lattice instance

[Mario Carneiro]

oh! linear_order already has a min field

[Mario Carneiro]

I guess the aggressive refactor has already happened

[Mario Carneiro]

so actually the real culprit is src#subtype.linear_order

[Mario Carneiro]

src#linear_order.lift can be forgiven for not overriding the max field since it wasn't given enough data to do so, but subtype.linear_order is definitely committing crimes against defeq

[Eric Wieser]

since it wasn't given enough data to do so

I think we should probably add has_inf and has_sup arguments to it

[Eric Wieser]

Having helper functions insiduously populate defaults with bad values seems like a bad thing.

[Mario Carneiro]

You can accomplish the same thing by applying lattice.copy to the result, but I see what you mean about bad defaults

[Mario Carneiro]

I think it is not uncommon for these kinds of non-instance helper definitions to fill in fields though

[Mario Carneiro]

after all, at some point you actually have to provide a value, you can't just always be delegating to the caller

[Mario Carneiro]

In this case I think we actually want two helper definitions, since the natural side condition for a min argument in linear_order.lift is f (min a b) = min (f a) (f b) and you can't easily discharge that by rfl if you want the default field

[Eric Wieser]

Note that for things like docs#function.injective.monoid we just force the user to deal with that annoying side goal

[Eric Wieser]

Because having duplicates is mainly just providing users extra tools to shoot themselves in the foot with (and a maintenance nightmare)

[Mario Carneiro]

In function.injective.monoid there is no possible default value though

[Mario Carneiro]

that's just the actual requirement on the definition

[Mario Carneiro]

the same would also be true for a lattice.lift, you would have f (inf a b) = inf (f a) (f b) and no possibility to otherwise discharge it, but for linear orders we have a default value for the field

[Johan Commelin]

Luckily we have

theorem semilattice_inf.ext {α} {A B : semilattice_inf α}
  (H : ∀ x y : α, (by haveI := A; exact x ≤ y) ↔ x ≤ y) : A = B :=
begin
  have := partial_order.ext H,
  have ss := funext (λ x, funext $ semilattice_inf.ext_inf H x),
  casesI A, casesI B,
  injection this; congr'
end

so I can at least keep that part of LTE sorry-free.

[Eric Wieser]

In function.injective.monoid there's a perfectly sensible default for has_pow M ℕ; the one used by docs#monoid.mk

[Eric Wieser]

But it's usually a trap to actually use it

[Eric Wieser]

Which is why I refactored function.injective.monoid to not use those defaults any more

[Violeta Hernández]

Johan Commelin said:

I guess this is a bug in mathlib that wasn't there before. Can we somehow lint against introducing such bugs? I guess that's hard.

We can always add examples for things like these

[Johan Commelin]

True. But I meant a more principled and generic way.

[Johan Commelin]

That example would only test that this particular example (semilattice_inf) wouldn't break. But a similar issue might pop up involving metric_space, or whatever...

[Yury G. Kudryashov]

In #15056 I'm trying to fix the diamond. In this branch, subtype.lattice _ _ is definitionally equal to linear_order.to_lattice but this equality doesn't work with instances transparency. How do I find which semireducible definition it fails to unfold?

[Yury G. Kudryashov]

BTW, definitions line docs#function.injective.linear_ordered_comm_monoid use linear_order.lift, so they create diamonds whenever we use them for subtypes.

[Yury G. Kudryashov]

Should we move has_sup and has_inf to core?

[Yury G. Kudryashov]

Then rewrite linear_order.lift so that it takes has_sup and has_inf arguments?

[Yury G. Kudryashov]

BTW, why tests/lean/perf/perm_ac_dlof_50.lean in the lean3 test suite doesn't cause problems?

[Yury G. Kudryashov]

@Gabriel Ebner :up:

[Yury G. Kudryashov]

It tries to import a non-existing file, then use a non-existing class.

[Yury G. Kudryashov]

Another question: why docs#linear_order.decidable_le is not an instance but docs#has_le.le.decidable is an instance?

[Eric Wieser]

What would be the advantage of moving has_inf to core?

[Eric Wieser]

docs#linear_order.lift should certainly take has_inf and has_sup arguments

[Yury G. Kudryashov]

Or we can rename min/max fields of linear_order to inf/sup, then drop workarounds in conditionally_complete_linear_order_with_bot etc.

[Eric Wieser]

What workarounds are you thinking of?

[Yury G. Kudryashov]

renaming

[Alex J. Best]

Yury G. Kudryashov said:

BTW, why tests/lean/perf/perm_ac_dlof_50.lean in the lean3 test suite doesn't cause problems?

I guess the perf subfolder just isn't run as part of any CI?

[Eric Wieser]

Is renaming causing problems?

[Yury G. Kudryashov]

No, but it is easy to forget to do it in some other case.

[Yury G. Kudryashov]

The following works/fails in my branch:

import order.lattice

variables [linear_order α] {P : α → Prop} (Psup : ∀⦃x y⦄, P x → P y → P (x ⊔ y)) (Pinf : ∀⦃x y⦄, P x → P y → P (x ⊓ y))

example : @semilattice_sup.to_partial_order _ (subtype.semilattice_sup Psup) = infer_instance :=
by tactic.reflexivity tactic.transparency.instances -- works

example : @semilattice_sup.to_has_sup _ (subtype.semilattice_sup Psup) = infer_instance :=
by tactic.reflexivity tactic.transparency.instances -- works

example : subtype.semilattice_sup Psup = infer_instance :=
by tactic.reflexivity tactic.transparency.instances -- fails

[Yury G. Kudryashov]

How can it happen?