Zulip Chat Archive

Stream: general

Topic: nnreal lattice broken


Johan Commelin (May 12 2022 at 07:56):

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 (May 12 2022 at 08:01):

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 (May 12 2022 at 08:05):

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 (May 12 2022 at 08:40):

Do you know which field disagrees?

Yaël Dillies (May 12 2022 at 08:42):

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

Mario Carneiro (May 12 2022 at 08:43):

looks like inf

Mario Carneiro (May 12 2022 at 08:43):

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

Mario Carneiro (May 12 2022 at 08:45):

#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 (May 12 2022 at 08:45):

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

Mario Carneiro (May 12 2022 at 08:46):

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

Yaël Dillies (May 12 2022 at 08:47):

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

Mario Carneiro (May 12 2022 at 09:09):

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 (May 12 2022 at 09:10):

this is via docs#ord_connected_subset_conditionally_complete_linear_order and docs#subset_conditionally_complete_linear_order

Mario Carneiro (May 12 2022 at 09:12):

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 (May 12 2022 at 09:13):

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 (May 12 2022 at 09:14):

we don't

Mario Carneiro (May 12 2022 at 09:15):

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

Yaël Dillies (May 12 2022 at 09:15):

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

Mario Carneiro (May 12 2022 at 09:15):

min is a function

Mario Carneiro (May 12 2022 at 09:15):

not a field

Mario Carneiro (May 12 2022 at 09:16):

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 (May 12 2022 at 09:17):

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

Yaël Dillies (May 12 2022 at 09:17):

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

Mario Carneiro (May 12 2022 at 09:17):

because it's an order typeclass

Yaël Dillies (May 12 2022 at 09:18):

... precisely?

Mario Carneiro (May 12 2022 at 09:18):

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 (May 12 2022 at 09:19):

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

Mario Carneiro (May 12 2022 at 09:19):

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

Mario Carneiro (May 12 2022 at 09:20):

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

Mario Carneiro (May 12 2022 at 09:35):

oh! linear_order already has a min field

Mario Carneiro (May 12 2022 at 09:36):

I guess the aggressive refactor has already happened

Mario Carneiro (May 12 2022 at 09:41):

so actually the real culprit is src#subtype.linear_order

Mario Carneiro (May 12 2022 at 09:43):

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 (May 12 2022 at 10:17):

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 (May 12 2022 at 10:18):

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

Mario Carneiro (May 12 2022 at 10:19):

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

Mario Carneiro (May 12 2022 at 10:20):

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

Mario Carneiro (May 12 2022 at 10:21):

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

Mario Carneiro (May 12 2022 at 10:23):

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 (May 12 2022 at 10:28):

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

Eric Wieser (May 12 2022 at 10:29):

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

Mario Carneiro (May 12 2022 at 11:20):

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

Mario Carneiro (May 12 2022 at 11:20):

that's just the actual requirement on the definition

Mario Carneiro (May 12 2022 at 11:21):

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 (May 12 2022 at 11:25):

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 (May 12 2022 at 12:08):

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

Eric Wieser (May 12 2022 at 12:08):

But it's usually a trap to actually use it

Eric Wieser (May 12 2022 at 12:09):

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

Violeta Hernández (May 13 2022 at 02:40):

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 (May 13 2022 at 05:06):

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

Johan Commelin (May 13 2022 at 05:07):

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 (Jun 29 2022 at 17:51):

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 (Jun 29 2022 at 18:03):

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 (Jun 29 2022 at 18:03):

Should we move has_sup and has_inf to core?

Yury G. Kudryashov (Jun 29 2022 at 18:04):

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

Yury G. Kudryashov (Jun 29 2022 at 18:07):

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

Yury G. Kudryashov (Jun 29 2022 at 18:07):

@Gabriel Ebner :up:

Yury G. Kudryashov (Jun 29 2022 at 18:07):

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

Yury G. Kudryashov (Jun 29 2022 at 18:08):

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

Eric Wieser (Jun 29 2022 at 18:14):

What would be the advantage of moving has_inf to core?

Eric Wieser (Jun 29 2022 at 18:14):

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

Yury G. Kudryashov (Jun 29 2022 at 18:17):

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 (Jun 29 2022 at 18:33):

What workarounds are you thinking of?

Yury G. Kudryashov (Jun 29 2022 at 18:37):

renaming

Alex J. Best (Jun 29 2022 at 18:43):

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 (Jun 29 2022 at 18:45):

Is renaming causing problems?

Yury G. Kudryashov (Jun 29 2022 at 18:46):

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

Yury G. Kudryashov (Jun 29 2022 at 18:52):

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 (Jun 29 2022 at 18:52):

How can it happen?


Last updated: Dec 20 2023 at 11:08 UTC