Randomness

Stream: mathlib4

[Yaël Dillies]

Are there any good tutorials on how to use randomness, in particular the docs4#Rand monad?

[Sky Wilshaw]

The implementation looks a bit like Control.Monad.Random from haskell. They've probably got some good tutorials.

[Mario Carneiro]

I think it's just you use Rand A as a monad, within which you can call rand : Rand T to get random elements of any type T

[Yaël Dillies]

And how does one "run" it?

[Sky Wilshaw]

docs4#IO.runRand

[Sky Wilshaw]

Or to use it with a fixed seed presumably you can just use the StateM machinery

[Eric Wieser]

If it's just ported from mathlib, you can also use (some_rand_obj.run (ULift.up (mkStdGen seed))).1 (docs4#mkStdGen, docs4#StateT.run)

[Sky Wilshaw]

Checking the impl of docs4#IO.runRandWith, you can use (StateT.run cmd { down := mkStdGen seed }).fst

[Yaël Dillies]

Oh wait, so not much changed from the Lean 3 implementation?

[Sky Wilshaw]

Ah, Eric beat me to it!

[Eric Wieser]

You might be interested in https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/Stating.20properties.20of.20the.20results.20of.20monads/near/319573258, @Yaël Dillies, which has some example code

[Yaël Dillies]

Time to see whether the bug I found in https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/Not.20so.20random is still there :stuck_out_tongue_closed_eyes:

[Mario Carneiro]

it is, it's documented as such

[Yaël Dillies]

How would one fill this in?

import Mathlib.Control.Random

def Random.pi {α β g : Type} [RandomGen g] (r : α → RandG g β) : RandG g (α → β) := sorry

Do we have a typeclass to say that α is enumerable?

[Yaël Dillies]

Is docs4#Encodable a reasonable choice?

[Yaël Dillies]

Ah! Not there yet.

[Eric Wieser]

You could fill it in as pure default

[Eric Wieser]

What's the algorithm for an docs#encodable type?

[Eric Wieser]

I don't see how you would generate an infinite series of bits with a finite number of invocations of the random number generator

[Yaël Dillies]

I'm going with

class Enum (α : Type _) where
  enum : List α
  enum_nodup : enum.Nodup
  mem_enum : ∀ a : α, a ∈ enum

which sounds like it should work?

[Eric Wieser]

So fintype?

[Yaël Dillies]

No!

[Yaël Dillies]

I need an order on the elements, else I cannot pass around the monad.

[Eric Wieser]

/me laughs in quot.unquot

[Eric Wieser]

I don't think you can prove anything interesting about RandG anyway

[Eric Wieser]

So peeking under the quotient feels like fair game

[Yaël Dillies]

I can make it generate tests for my CATAM projects, however.

[Eric Wieser]

Right, my point is that the unsafe on docs4#Quot.unquot isn't a problem for you

[Yaël Dillies]

In my case, α is Fin n, so it feels a bit dumb not providing List.finRange directly

[Eric Wieser]

To the compiler, I would guess finset.univ.unquot is exactly that

[Eric Wieser]

But I guess we don't have docs4#Fintype so that's irrelevant

[Yaël Dillies]

Regardless, how do I then use this enumerating list to build my random function?

[Eric Wieser]

Oh, we have an ad-hoc port for precisely what you need! (the fin instances)

[Eric Wieser]

Yaël Dillies said:

Regardless, how do I then use this enumerating list to build my random function?

mmap over the list of all α, and turn the list back into a function

[Yaël Dillies]

Ah! List.ofFn!

[Eric Wieser]

No, the reverse; docs4#List.get

[Yaël Dillies]

Does that sound right?

def pi [Enum α] (r : α → RandG g β) : RandG g (α → β) :=
(λ l a ↦ _) <$> (Enum.enum : List α).mapM r

[Eric Wieser]

That's only going to work for Fin

[Eric Wieser]

You're going to need to produce a list of (a, b) pairs to do a lookup for other types (either by zipping with Enum.enum, or by using do b <- r a, pure (a, b) in the map.

[Eric Wieser]

Which is also going to be slower

[Yaël Dillies]

This is what it looks like now

class Enum (α : Type _) where
  enum : List α
  enum_nodup : enum.Nodup
  index : α → Fin enum.length
  enum_index : ∀ a, enum.get (index a) = a

instance {n : ℕ} : Enum (Fin n) :=
{ enum := List.finRange _,
  enum_nodup := List.nodup_finRange _,
  index := λ n ↦ ⟨n, by rw [List.length_finRange]; exact n.2⟩,
  enum_index := λ a ↦ by simp }

namespace Random
variable {α β g : Type} [RandomGen g]

def pi [Enum α] [BEq α] (r : α → RandG g β) : RandG g (α → β) :=
(λ l a ↦ List.get l $ ⟨Enum.index a, sorry⟩) <$> (Enum.enum : List α).mapM r

[Yaël Dillies]

The problem is that I cannot fill in the sorry because I don't know that the list I'm getting out of the mapM has the right length, which is exactly the same problem as you had, right?

[Eric Wieser]

Yes, you need a docs4#Vector.mapM (docs#vector.mmap)

[Eric Wieser]

Or to map over the subtype

[Yaël Dillies]

Do we not have docs4#List.length_mapM?

[Eric Wieser]

How would you state it?

[Yaël Dillies]

Oh

[Eric Wieser]

You could just grab that vector lemma from mathport

[Yaël Dillies]

I guess I need to port Data.Vector.Basic, then :P

[Eric Wieser]

It has some dependencies yet

[Eric Wieser]

I think data.fin.tuple.basic and data.list.of_fn

[Kyle Miller]

@Yaël Dillies You probably don't want an Enum that has an actual List of all elements if you're going to be choosing random elements for programming purposes (for example, a random 32-bit integer is impossible this way, or, equivalently, getting a random Fin 32 -> Fin 2).

Another option is to have Enum be a wrapper around Equiv to a Fin n for some n. A while back I had some experiment with this: https://gist.github.com/kmill/9055e1fc32d75b818cbb036650d309ed#file-vec_experiment2-lean-L73 (not for randomness though)

[Yaël Dillies]

I'm not sure I understand your objection.

[Yaël Dillies]

I just managed to get a $10 × 10$ matrix of random Bools!

[[true, false, false, true, false, false, false, true, true, false], [false, false, false, false, false, true, false, false, false, false], [false, false, false, true, false, false, false, false, false, true], [false, false, false, false, false, false, false, false, false, true], [false, true, true, true, false, true, true, false, false, false], [false, false, false, false, true, false, false, true, true, true], [false, true, true, false, true, false, false, true, false, false], [true, false, false, true, true, false, true, false, false, false], [false, false, false, false, true, false, true, false, true, true], [true, false, false, true, true, false, true, false, false, true]]

[Yaël Dillies]

(and I set the probability to 0.33333333333)

[Yaël Dillies]

The other ingredient was

instance {α : Type _} {β : α → Type _} [Enum α] [∀ a, ToString (β a)] : ToString (∀ a, β a) :=
⟨λ f ↦ toString $ Enum.enum.map $ λ a ↦ toString $ f a⟩

[Eric Wieser]

That seems like bad ToString

[Eric Wieser]

Also, you'll get nice line-wrappign if you implement Repr instead

[Yaël Dillies]

How should I unbad my ToString?

[Eric Wieser]

Well right now it pretends functions are lists

[Eric Wieser]

You could print it as λ a ↦ [elems...].get ⟨Enum.index a, _⟩

[Yaël Dillies]

That's the role of Repr, right? ToString can just "look nice"

[Eric Wieser]

I have no idea what docs4#ToString is for

[Kyle Miller]

I thought you were using a different design, where you use Enum and choose elements uniformly at random, since this is something you can do for everything that implements Enum.

[Yaël Dillies]

Ah no, the role of Enum here is to pick a canonical order in which to run the dice rolls.

[Yaël Dillies]

I just defined

def randFin' [NeZero n] : RandG g (Fin n) :=
  λ ⟨g⟩ ↦ randNat g 0 n |>.map (λ a ↦ Fin.ofNat' a $ NeZero.pos n) ULift.up

instance [Enum α] [Nonempty α] : NeZero (Enum.enum : List α).length := sorry

def uniform [Enum α] [Nonempty α] : RandG g α := Enum.enum.get <$> randFin'

which I assume is what you meant?

[Yaël Dillies]

I still don't understand your objection. If I had

def List.pi (l : List α) (f : ∀ a, List (β a)) : List (∀ a, β a) :=

then I would be able to provide an Enum (Fin 32 → Fin 2) instance and generate 32-bits integers uniformly at random.

[Yaël Dillies]

Or is your argument that it is too slow?

[Kyle Miller]

Mathematically it's fine, but a List (Fin 32 → Fin 2) that enumerates that type would take 96 gigabytes of RAM minimum.

[Kyle Miller]

(That's two 8-byte pointers per List.cons, and 8 bytes per Fin 32 -> Fin 2, which is an optimistic lower bound for how Lean would represent such a function.)

[Yaël Dillies]

How is your suggested Enum better?

[Yaël Dillies]

And more precisely does it make what I'm doing harder?

[Yaël Dillies]

Right now, I have

def pi [Enum α] (r : α → RandG g β) : RandG g (α → β) :=
(λ l a ↦ List.get l.toList $ ⟨Enum.index a, by simp⟩) <$> Vector.mapM r ⟨Enum.enum, rfl⟩

Do you see any obvious way of generalizing it to dependent types?

[Eric Wieser]

Put sigma types in the list?

[Yaël Dillies]

Yes but then I need a specific type of vectors whose keys are unique and complete.

[Yaël Dillies]

DVector, if you wish

[Eric Wieser]

docs#finmap? But I guess of fixed-length

[Eric Wieser]

Is this an #xy problem, or are you solving this problem because you find it interesting, independent of whether you actually need it?

[Yaël Dillies]

The latter

[Yaël Dillies]

I am happy to leave it as is, but I thought there might be something interesting here.

[Eric Wieser]

Yaël Dillies said:

Yes but then I need a specific type of vectors whose keys are unique and complete.

Why do you need the keys to be unique and complete? What goes wrong if you just have a vector of sigmas?

[Yaël Dillies]

Okay, they may not need be unique, but I need to find the entry corresponding to a key, so I need the key to exist.

[Eric Wieser]

Can't you just look in the ith index like you do now?

[Yaël Dillies]

Hmm...

[Eric Wieser]

Maybe you get stuck trying to cast the sigma type

[Yaël Dillies]

Indeed, I have lost the information that (l.toList.get $ Enum.index a).1 = a

(λ l a ↦ _ -- `β a`
) <$> Vector.mapM (λ a ↦ (r a).map $ Sigma.mk a) ⟨Enum.enum, rfl⟩

[Kyle Miller]

@Yaël Dillies This should be reasonably efficient (though it's still incomplete and would need more development). Generally, Array is more efficient than List.

import Mathlib.Logic.Equiv.Basic
import Std
import Mathlib.Control.Random
import Mathlib.Data.Nat.Order.Basic

def Fin.arrayOf (f : Fin n → α) : Array α := Id.run do
  let mut a := Array.mkEmpty n
  for h : i in [0 : n] do
    a := a.push (f ⟨i, h.2⟩)
  return a

def Fin.size_arrayOf (f : Fin n → α) : (Fin.arrayOf f).size = n := sorry
def Fin.get_arrayof (f : Fin n → α) (i : Fin (Fin.arrayOf f).size) :
  (Fin.arrayOf f).get i = f (by rw [← Fin.size_arrayOf f]; exact i) := sorry -- should cast

class Enum (α : Type _) where
  card : ℕ
  enum : Fin card ≃ α
  arrayOf : Unit → Array α -- a function, which prevents computing an `Array` unless one is actually needed.
  arrayOf_eq : arrayOf () = Fin.arrayOf enum

theorem Enum.size_arrayOf [Enum α] : (Enum.arrayOf () : Array α).size = Enum.card α := by
  rw [arrayOf_eq, Fin.size_arrayOf]

instance {n : ℕ} : Enum (Fin n) where
  card := n
  enum := Equiv.refl (Fin n)
  arrayOf := fun _ => Fin.arrayOf id
  arrayOf_eq := rfl

namespace Random
variable {α β g : Type} [RandomGen g]

def randFin' [NeZero n] : RandG g (Fin n) := do
  λ ⟨g⟩ ↦ randNat g 0 n |>.map (λ a ↦ Fin.ofNat' a $ NeZero.pos n) ULift.up

instance [Enum α] [Nonempty α] : NeZero (Enum.card α) := sorry

def uniform [Enum α] [Nonempty α] : RandG g α := Enum.enum <$> randFin'

def pi [Enum α] (β : α → Type _) (r : (x : α) → RandG g (β x)) : RandG g ((x : α) → β x) := do
  let a : Array ((x : α) × β x) ← -- graph of function we're constructing
    (Enum.arrayOf () : Array α).mapM (fun x => do return ⟨x, ← r x⟩)
  -- can't prove these two within the do block:
  have hsize : a.size = Enum.card α := sorry
  have hprop : ∀ i,
    (a.get i).1 = (Enum.arrayOf ()).get ⟨i, by { cases i; rwa [Enum.size_arrayOf, ← hsize] }⟩ := sorry
  return λ x ↦
    match h : a.get ⟨Enum.enum.symm x, sorry⟩ with
    | ⟨x', b⟩ => by
      have : x = x' := sorry
      subst this
      exact b

[Kyle Miller]

Having both Enum.enum and Enum.arrayOf gives instances the ability to provide efficient implementations of them. Instances can also fill in one using the other if they don't want to do anything special.

[Yaël Dillies]

Interesting! As a test case, can you generalize the following to dependent functions? Nevermind, you already have. Lean 4 notation is throwing me off.