Assign external definitions to library functions

Stream: general

[Markus de Medeiros]

This question is a bit messed up so I don't expect there to be a good answer. The PMF type in mathlib which is marked noncomputable, for good reason, but I want to execute PMF's using an external function binding (like in SampCert), and remove noncomputable marking. Is there any way to do this?

[Yury G. Kudryashov]

What's SampCert? How do you want to represent reals?

[Markus de Medeiros]

We don't represent reals, we're (currently) using it to represent randomly sampled values. This is the SampCert FFI code, which is used for the external definitions here

[Markus de Medeiros]

It works in SampCert because the monadic bind and return are defined inside the project, but if you want to do the same thing with Lean PMF's you need to somehow instruct Lean to use an extern binding for mathlib code. I'm wondering if this is at all possible.

[Yury G. Kudryashov]

I don't think that, e.g., extern prob_Pure does what you think it does.

[Yury G. Kudryashov]

probPure is defined as a function T → T → ENNReal but you implement it as a function T → T → T that returns the first argument.

[Markus de Medeiros]

That's exactly what it's supposed to do :) It's the imperative way to sample from the dirac distribution. You'll see that the other externed distributions involve eg. nondeterministic and nonterminating code, which is why SampCert does it that way.

I'm wondering if I can tell Lean to compile certain PMF's from mathlib using a similar technique. The main is telling Lean to attach an extern definition to library code, and marking noncomputable library code as computable.

[Yury G. Kudryashov]

That's not whatextern is supposed to do.

[Yury G. Kudryashov]

You should write a function PMF.sample with a correct type signature and use extern on it.