Non-computable bot in Fin.

Stream: mathlib4

[Wrenna Robson]

There are some instances here for Fin n with [NeZero n]: in particular there's Fin.instBoundedOrder. This is meant to prevent non-computable instances being used to construct these instances non-computably.

However, in practice if I use ⊥ in a definition, Lean flags it as noncomputable, and it seems ultimately to be constructing ⊥ from the CompleteLinearOrder on Fin n, which is non-computable.

Can we either: a) define the complete linear order on Fin n in a computable way that extends these other instances, or b) stop this non-computable instance of ⊥ being used?

[Wrenna Robson]

Possibly related: Lean does not seem able to synthesise an OrderBot for Fin n simply using its BoundedOrder instance.

[Yaël Dillies]

In these situations, we have in the past added computable shortcut instances

[Yaël Dillies]

Can you click through the infoview to tell us exactly how it went from Bot to CompleteLinearOrder in this case?

[Wrenna Robson]

Aye, and it seems like that ought to work here (Fin.instBoundedOrder is computable!) but in practice it uses non-computable.

[Yaël Dillies]

... or give us a MWE to do so ourselves

[Wrenna Robson]

Aye, one sec.

[Yaël Dillies]

Wrenna Robson said:

Aye, and it seems like that ought to work here (Fin.instBoundedOrder is computable!) but in practice it uses non-computable.

There might be paths from Bot and CompleteLinearOrder that don't go through BoundedOrder

[Eric Wieser]

I think this will be fixed in the next Lean release

[Wrenna Robson]

Yeah that is what I think is happening. Just trying to work out how to click through.

[Eric Wieser]

In the meantime

attribute [-instance] Fin.completeLinearOrder in
instance : Bot (Fin 3) := inferInstance

fixes it

[Wrenna Robson]

Aha

[Wrenna Robson]

Thank you.