ENat is noncomputable

Stream: mathlib4

[Geoffrey Irving]

I'm doing some verified computations with power series approximations (https://github.com/girving/series). I want my Series α to have a finite list of known, explicit coefficients, followed by a zero to infinite number of known zeros. This is nicely representable if Series has an order : ℕ∞ field. For intuition, the most important application of an infinite number of known series is so that constants cleanly embed as series, without knowing the order one eventually needs them to.

Unfortunately, the ℕ∞ ordering is noncomputable:

import Mathlib.Data.ENat.Lattice

variable {α : Type}

/-- `min` on `WithTop α` and `α` produces `α` -/
def WithTop.min_coe [Min α] (x : WithTop α) (y : α) : α := match x with
  | some x => min x y
  | ⊤ => y

/--- The size of the explicit coefficient array after a binary componentwise operation like add or sub.

Fails with failed to compile definition, compiler IR check failed at `binary_n._closed_0`. Error: depends on declaration 'instCompleteLinearOrderENat', which has no executable code; consider marking definition as 'noncomputable' -/
def binary_n (a0 a1 : ℕ∞) (b0 b1 : ℕ) : ℕ :=
  let a := min a0 a1
  max (WithTop.min_coe a b0) (WithTop.min_coe a b1)

so I am following the instructions given here:

Deprecation #
As it appears this has been unused since 2018, we are now deprecating it. If ENat does not serve your purposes, please raise this on the community Zulip.

What's the best way to proceed? For now I'll define my own computable version of min and it should be fine, just a bit clunky.

[Robin Arnez]

It's not that the ordering on ℕ∞ is noncomputable but that it took the wrong turn in instance synthesis, take:

import Mathlib.Data.ENat.Lattice

set_option pp.explicit true in
/--
info: @SemilatticeInf.toMin ENat
  (@Lattice.toSemilatticeInf ENat
    (@ConditionallyCompleteLattice.toLattice ENat
      (@ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ENat
        (@ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder ENat
          (@CompleteLinearOrder.toConditionallyCompleteLinearOrderBot ENat instCompleteLinearOrderENat)))))
-/
#guard_msgs in #synth Min ℕ∞

attribute [-instance] instCompleteLinearOrderENat

set_option pp.explicit true in
/--
info: @SemilatticeInf.toMin ENat
  (@Lattice.toSemilatticeInf ENat
    (@DistribLattice.toLattice ENat (@instDistribLatticeOfLinearOrder ENat instLinearOrderENat)))
-/
#guard_msgs in #synth Min ℕ∞

[Robin Arnez]

What you'd really hope to see is @LinearOrder.toMin ENat instLinearOrderENat but well, instance search takes detours quite often

[Kenny Lau]

maybe the solution is instead to lower the priority of ConditionallyCompleteLattice.toLattice compared to DistribLattice.toLattice?

[Robin Arnez]

Hmm or maybe even also reduce the priority of SemilatticeInf.toMin in comparison to LinearOrder.toMin?

[Robin Arnez]

Maybe we could make this a more general rule: When class A implies class B and both class A and class B provide an instance to C then B.toC should have lower priority in comparison to A.toC

[Eric Wieser]

Nrmally we just make a computable shortcut when this happens

[Eric Wieser]

So in this case, just add instance : Lattice ENat := inferInstance before the complete lattice is set up

[Eric Wieser]

Or without a mathlib change, if you don't want to wait

import Mathlib.Data.ENat.Lattice

variable {α : Type}

-- this should be upstreamed as a "computable shortcut instance"
instance : Lattice ENat := LinearOrder.toLattice

/-- `min` on `WithTop α` and `α` produces `α` -/
def WithTop.min_coe [Min α] (x : WithTop α) (y : α) : α := match x with
  | some x => min x y
  | ⊤ => y

/--- The size of the explicit coefficient array after a binary componentwise operation like add or sub. -/
def binary_n (a0 a1 : ℕ∞) (b0 b1 : ℕ) : ℕ :=
  let a := min a0 a1
  max (WithTop.min_coe a b0) (WithTop.min_coe a b1)

[Robin Arnez]

I guess maybe we could do that but it would probably be nice to reduce the amount of detours instance search takes in general

[Robin Arnez]

Again, we want to use LinearOrder.toMin here, really

[Eric Wieser]

We do this shortcut pattern pretty extensively already

[Eric Wieser]

Another solution would be to do search in two stages, using one that skips noncomputable instances the first time

[Eric Wieser]

Robin Arnez said:

Maybe we could make this a more general rule: When class A implies class B and both class A and class B provide an instance to C then B.toC should have lower priority in comparison to A.toC

I'd make the stronger claim that A.toC should not exist at all

[Robin Arnez]

You mean docs#LinearOrder.toMin should not exist and we should use docs#SemilatticeInf.toMin instead..?

[Eric Wieser]

Or at least the former should not be an instance

[Eric Wieser]

I think we start to get close to import considerations here though, where we want linear orders available before lattices

[Robin Arnez]

Well, I quickly threw together a little

Triangle detector

import Mathlib

open Lean Meta

partial def traverseStar (tree : Meta.DiscrTree.Trie α) : Array α :=
  if h : tree.2.size = 0 then
    tree.1
  else if tree.2[0].fst matches .star then
    traverseStar tree.2[0].snd
  else
    #[]

def triangleDetector : MetaM Unit := do
  let insts := instanceExtension.getState (← getEnv)
  let mut infos := #[]
  for (key, tree) in insts.discrTree.root do
    let .const nm _ := key | continue
    let entries := traverseStar tree
    let entries ← entries.filterMapM fun entry => do
      let type ← inferType entry.val
      forallTelescope type fun vars _ => do
        let #[α, inst] := vars | return none
        unless (← inst.fvarId!.getBinderInfo) matches .instImplicit do
          return none
        let .app (.const nm [.param _]) a ← inferType inst | return none
        if a != α then
          return none
        return some nm
    for a in entries do
      for b in entries do
        unless a.quickLt b do continue
        let synth1 ←
          withLocalDeclD `α (.sort 1) fun α =>
          withLocalDeclD `h (.app (.const a [0]) α) fun _h => do
            return (← synthInstance? (.app (.const b [0]) α)).isSome
        let synth2 ←
          withLocalDeclD `α (.sort 1) fun α =>
          withLocalDeclD `h (.app (.const b [0]) α) fun _h => do
            return (← synthInstance? (.app (.const a [0]) α)).isSome
        if synth1 && !synth2 then
          infos := infos.push s!"{a} -> {b} -> {nm}"
        else if synth2 && !synth1 then
          infos := infos.push s!"{b} -> {a} -> {nm}"
  Lean.logInfo ("\n".intercalate infos.toList)

#eval triangleDetector

which gives you this list. So those are the ones we need to consider at least.

[Eric Wieser]

I've tried multiple times to fix this for the normed hierarchy :)

[Robin Arnez]

There also some of these interesting four-sided shapes like

LinearOrder -> SemilatticeSup -> PartialOrder
LinearOrder -> SemilatticeInf -> PartialOrder

where I don't believe we can remove the A.toC connection without causing asymmetry