Ignoring noncomputable

Stream: new members

[Arshak Parsa]

Is there any way to run the last #eval in this situation?

import Mathlib

open ProbabilityTheory

#check PMF.binomial (1/10) (by simp) 10 1

theorem th :
    (PMF.binomial (1/2) (by simp) 10 1) =
    10/1024:= by
  rw [PMF.binomial_apply];norm_num;ring_nf
  rw [← @ENNReal.inv_pow];norm_num
  exact Eq.symm ENNReal.div_eq_inv_mul

#eval (1/2 : Rat)^1 * (1-1/2)^((Fin.last 10 - 1) : ℕ) * (Nat.choose 10 1)

#reduce PMF.binomial (1/10) (by simp) 10 1

-- ignore noncomputable  tag
#eval PMF.binomial (1/10) (by simp) 10 1

I also ran #reduce but the output is not human readable!

[Eric Wieser]

(docs#PMF.binomial)

[Arshak Parsa]

I know it is tagged as noncomputable. Is there any way to tell Lean to ignore the noncomputable tag?

[Eric Wieser]

This is noncomputable because infty * x is noncomputable

[Eric Wieser]

Asking to ignore noncomputable is a bit like asking to ignore that a bike doesn't have a chain or that a car doesn't have an engine

[Eric Wieser]

Actually, in this case I think I can redefine this computably without any real consequence, so maybe I'll do so later today

[Arshak Parsa]

Eric Wieser said:

Asking to ignore noncomputable is a bit like asking to ignore that a bike doesn't have a chain or that a car doesn't have an engine

When p is a rational number, tagging binomial distribution as noncomputable is like classifying a bird as a reptile!

[Etienne Marion]

noncomputable is not a tag which was put here arbitrarily, it is a mandatory keyword. If you do not put it Lean raises an error. It was defined with p an ENNReal because ENNReal is the canonical codomain for a measure. AFAIK most users do not really care about computability so this is not really an issue

[Kyle Miller]

Yeah, you'd have to make a version of PMF that's rational-valued and a version of PMF.binomial that's specialized to rationals. Otherwise it's not really clear what you're wanting out of #eval, which compiles the expression and runs it.

[Kyle Miller]

This sort of works (it uses simp lemmas and a normalization routine), but norm_num doesn't seem to know anything about ENNReal so it gets stuck:

#norm_num [PMF.binomial_apply] : PMF.binomial (1/10) (by simp) 10 1
-- 10⁻¹ * (1 - 10⁻¹) ^ 9 * 10

[Kyle Miller]

There's a sense in which PMF.binomial could be computable (which is what Eric said he might do), but you have to remember that real numbers are Cauchy sequences. I think it was Eric that added a Repr instance for Real that would print the first few terms of the Cauchy sequence. So, make sure to temper your expectations with a "computable" PMF.binomial if that's not what you're looking for when you #eval.

[Eric Wieser]

Eric Wieser said:

Actually, in this case I think I can redefine this computably without any real consequence, so maybe I'll do so later today

#20856 is the hopefully-noncontroversial part of this

[Eric Wieser]

#20858 is the more dubious part