## Stream: general

### Topic: Why's noncomputable linear_ordered preferred over orde...

#### Junyan Xu (Jun 09 2022 at 05:31):

• Lean's typeclass inference prefers docs#ordered_add_comm_group over docs#linear_ordered_add_comm_group, so it doesn't demand I mark test1 below noncomputable. (Or maybe it just finds the former before the latter.)
• A similar test shows it also prefers docs#ordered_ring over docs#linear_ordered_ring.
• However, it prefers docs#linear_ordered_comm_ring over docs#ordered_comm_ring, as test2 below shows (you may delete the first two instances when testing the last two).
• This is currently making docs#surreal.dyadic_map noncomputable in my surreal multiplication branch. I tried to lower the priority of the linear_ordered_comm_ring instance, but to no avail.
• What could be the cause of these behaviors? For reference:
linear_ordered_add_comm_group extends ordered_add_comm_group α, linear_order α
linear_ordered_ring extends ordered_ring α, linear_order α, nontrivial α
linear_ordered_comm_ring extends linear_ordered_ring α, comm_monoid α

• Can we make Lean always prefer the computable instance when it's available?

import algebra.order.ring

instance : ordered_add_comm_group unit := sorry

noncomputable instance : linear_ordered_add_comm_group unit :=
{ le_total := sorry,
decidable_le := classical.dec_rel _,

def test1 : bool := if () + () = () then tt else ff /- OK -/

instance : ordered_comm_ring unit := sorry

noncomputable instance : linear_ordered_comm_ring unit :=
{ le_total := sorry,
decidable_le := classical.dec_rel _,
.. unit.ordered_comm_ring }

def test2 : bool := if () + () = () then tt else ff
/- missing 'noncomputable' modifier, definition 'test'
depends on 'unit.linear_ordered_comm_ring' -/


#### Eric Wieser (Jun 09 2022 at 06:38):

Adding intermediate instances (like docs#comm_ring) would fix this

#### Junyan Xu (Jun 09 2022 at 06:51):

Adding docs#comm_ring doesn't fix it (tested for surreals), unfortuantely.

#### Eric Wieser (Jun 09 2022 at 07:18):

You can find out exactly what instance you need by looking at the path from linear_ordered_comm_ring to has_add

#### Eric Wieser (Jun 09 2022 at 07:18):

And adding an instance for the last step that is still computable

#### Eric Wieser (Jun 09 2022 at 07:18):

We do this already for real and complex

#### Junyan Xu (Jun 09 2022 at 07:21):

Hmm, then docs#ordered_ring should also work, let me try

#### Junyan Xu (Jun 09 2022 at 07:39):

It's cumbersome to move those fields around, so maybe I'll not try it for surreals, since everything works right now. ordered_comm_ring is the largest class that remains computable, and it's a shame that we have to break it down further. docs#surreal.dyadic_map should only require add_zero_class for the add_monoid_hom, and here are the paths from docs#ordered_comm_ring to docs#add_zero_class:

ordered_comm_ring ->
ordered_ring ->
comm_ring -> ring


#### Junyan Xu (Jun 09 2022 at 07:42):

and from docs#linear_ordered_comm_ring:

linear_ordered_comm_ring -> linear_ordered_ring -> ordered_ring


#### Junyan Xu (Jun 09 2022 at 07:43):

It seems to me the chain from ordered_comm_ring is shorter, no idea why Lean first finds linear_ordered_comm_ring`.

#### Eric Wieser (Jun 09 2022 at 07:47):

Lean starts from the right and works left; it takes the highest priority option at every step, breaking ties by recently. It doesn't optimize for depth in any way

Last updated: Dec 20 2023 at 11:08 UTC