Zulip Chat Archive
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
belownoncomputable
. (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 thelinear_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 _,
.. unit.ordered_add_comm_group }
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.
Junyan Xu (Jun 09 2022 at 06:54):
adding docs#add_comm_group does fix it though
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 >
ring > add_comm_group >
add_group > sub_neg_monoid > add_monoid > add_zero_class
add_comm_monoid > add_monoid
ordered_add_comm_group > add_comm_group
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: Aug 03 2023 at 10:10 UTC