Compiler IR Check Failed with unknown declaration

Stream: mathlib4

[Bolton Bailey]

Here is a #mwe: I get an error message that tells me "unknown declaration PMF.pure. But this is strange because that def is imported. Why is this the case?

import Mathlib.LinearAlgebra.Lagrange
import Mathlib.Probability.ProbabilityMassFunction.Monad

class PolyCommitIOPMonad (F : Type) (M : Type -> Type)
  where
    open_at_point : CoinHandle -> M OpeningHandle
    randomness : (PMF F) -> M CoinHandle

#check PMF.pure -- PMF.pure.{u_1} {α : Type u_1} (a : α) : PMF α

-- compiler IR check failed at 'SendFieldElement._rarg', error: unknown declaration 'PMF.pure'
def SendFieldElement (F CoinHandle OpeningHandle : Type) [Field F]
    {M : Type -> Type} [PolyCommitIOPMonad F M] [Monad M] :
    M (OpeningHandle) := do
  let α <- PolyCommitIOPMonad.randomness (F := F) (M := M) (CoinHandle := CoinHandle) (PMF.pure 0 : PMF F)
  let f_0 <- PolyCommitIOPMonad.open_at_point F α
  return f_0

[Bolton Bailey]

Note also: If I mark the definition as noncomputable then the error goes away. But I don't want the definition to be noncomputable, and the error message doesn't tell me to do this anyway.

[Alex J. Best]

The definition of PMF.pure  is

noncomputable section

variable {α β γ : Type*}

open scoped Classical
open BigOperators NNReal ENNReal

open MeasureTheory

namespace PMF

section Pure

/-- The pure `PMF` is the `PMF` where all the mass lies in one point.
  The value of `pure a` is `1` at `a` and `0` elsewhere. -/
def pure (a : α) : PMF α :=
  ⟨fun a' => if a' = a then 1 else 0, hasSum_ite_eq _ _⟩

so this is using classical to provide a proof that equality is decidable, this should be converted to and explicit [DecidableEq alpha] to fix the problem, but I have no idea if this is just a band-aid, perhaps the rest of the theory will break down the line without a big redesign at this point

[Bolton Bailey]

I thought of this and I did a bit of tinkering with the definition. If I remove the noncomputable section and add the DecidableEq it still complains of noncomputability due to some typeclass of Ennreal. I am not sure why it does this.

[Alex J. Best]

Right that does make sense then that any definition involving PMF would have a lot of difficulty being computable, and even if it was would likely not be practically executable. Probably you'll get more mileage out of defining your own PMF's landing in something like Ennrat

[Bolton Bailey]

I still don't understand. If I have DecidableEq α, then shouldn't I be able to compute if a' = a then 1 else 0?

[Mario Carneiro]

only if 1 and 0 are computable (!)

[Bolton Bailey]

Why shouldn't they be? The real numbers 0 and 1 are

[Bolton Bailey]

:upside_down:

#eval (1 : ℝ) -- Real.ofCauchy (sorry /- 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, ... -/)
#eval (1 : ℝ≥0∞) -- failed to compile

[Bolton Bailey]

I suppose you're going to tell me it's because we can't determine if these numbers are greater than or equal to zero.

[Bolton Bailey]

If that's the answer, I don't see why that's important. The very fact that these terms typecheck means that they are greater than 0, so that should just be proof, not data, and shouldn't affect computability.

[Mario Carneiro]

no, they are noncomputable because of a silly reason most likely

[Ruben Van de Velde]

failed to compile definition, consider marking it as 'noncomputable' because it depends on 'ENNReal.instCanonicallyOrderedCommSemiringENNReal', and it does not have executable code

is the full error message here

[Ruben Van de Velde]

And if I put the #eval before that instance, it works

[Ruben Van de Velde]

Easiest solution:

--- Mathlib/Data/ENNReal/Basic.lean
+++ Mathlib/Data/ENNReal/Basic.lean
@@ -97,7 +97,7 @@ variable {α : Type*}
 /-- The extended nonnegative real numbers. This is usually denoted [0, ∞],
   and is relevant as the codomain of a measure. -/
 def ENNReal := WithTop ℝ≥0
-  deriving Zero, AddCommMonoidWithOne, SemilatticeSup, DistribLattice, Nontrivial
+  deriving Zero, One, AddCommMonoidWithOne, SemilatticeSup, DistribLattice, Nontrivial
 #align ennreal ENNReal

 @[inherit_doc]

(I'm not going to PR)