## Stream: new members

### Topic: Generate random Fin n

#### Jesse Slater (Oct 21 2023 at 20:33):

I haven't worked with randomness in a functional language before, and I am having a bit of trouble. I am trying to apply a series of random functions to a number.
Here is the code I have:

def apply_random_n
{i : Nat}
(h : 0 < i)
(start n : Nat)
(v : Fin i → Nat → Nat)
: Nat :=
match n with
| 0 => start
| n' + 1 =>
let r : Fin i := ⟨0, h⟩
--r should be randomly generated each step
v r (apply_random_n h start n' v)


What do I need to change to generate r randomly each step? I see the Random.randFin function in mathlib, but I cannot figure out how to use it for the life of me.

#### Yaël Dillies (Oct 21 2023 at 20:42):

Here's a file I wrote for my computer projects last year:

Copyright (c) 2023 Yaël Dillies. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Yaël Dillies
-/
import Mathlib.Control.Random
import Catam.Mathlib.Data.Enum
import Catam.Mathlib.Data.Rat.Defs

/-!
# Additional randomness operations
-/

namespace Random
variable {g : Type} {α β : Type _} [RandomGen g] {n : ℕ} [NeZero n]

def randFin' : RandG g (Fin n) :=
λ ⟨g⟩ ↦ (randNat g 0 n).map (λ a ↦ Fin.ofNat' a $NeZero.pos n) ULift.up instance : Random (Fin n) where random := randFin' /-- Return true with probability p, false with probability 1 - p. If p ≤ 0, it always returns false. If 1 ≤ p, it always returns true. -/ def bernoulli (p : ℚ) : RandG g Bool := return (← rand (Fin p.den)) < p.num /-- Return a bipartite graph on n + n vertices where each edge is present independently with probability p. -/ def bipartiteGraph (n : ℕ) (p : ℚ) : RandG g (Fin n → Fin n → Bool) := Monad.pi$ λ _ ↦ Monad.pi $λ _ ↦ bernoulli p /-- Return an element of an enumerable type α uniformly at random. -/ def uniform [Enum α] [Nonempty α] : RandG g α := Enum.enum.get <$> randFin'

end Random


#### Alex J. Best (Oct 21 2023 at 20:42):

Functions in function languages are pure, they cannot depend on anything other than their inputs. So you'll need to work in some sort of monad for randomness docs#IO.rand or docs#RandG that Yael mentions, or pass in a random state and generator each time docs#randNat. What you want to do precisely

#### Yaël Dillies (Oct 21 2023 at 20:42):

along with

Copyright (c) 2023 Yaël Dillies. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Yaël Dillies
-/
import Mathlib.Data.Fin.Basic
import Mathlib.Data.List.Range
import Catam.Mathlib.Data.Vector.Basic

/-!
# Enumeration of types
-/

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 }

instance {α : Type _} {β : α → Type _} [Enum α] [∀ a, ToString (β a)] : ToString (∀ a, β a) :=
⟨λ f ↦ toString $Enum.enum.map$ λ a ↦ toString $f a⟩ instance [Enum α] [Nonempty α] : NeZero (Enum.enum : List α).length := ⟨λ h ↦ by haveI := ‹Nonempty α›.map Enum.index rw [h] at this exact not_isEmpty_of_nonempty (Fin 0) (inferInstance : IsEmpty (Fin 0))⟩ namespace Monad universe u v variable {α : Type u} {β : Type (max u v)} {m : Type (max u v) → Type _} -- TODO: Generalise to dependent types /-- Return a random function from random results for each input. -/ def pi [Enum α] [Monad m] (r : α → m β) : m (α → β) := (λ l a ↦ l.toList.get ⟨Enum.index a, by simp⟩) <$> Vector.mapM r ⟨Enum.enum, rfl⟩



#### Yaël Dillies (Oct 21 2023 at 20:44):

Sorry, I can't make the repo public because of fairness concerns, but I can certainly dump those prereqs into LeanCamCombi or something for me to avoid copying everything over here.

#### Jesse Slater (Oct 21 2023 at 20:55):

@Alex J. Best
I don't need anything fancy, just need to generate a series of random Fin n. This is not any sort of mission critical code, and I won't be writing any proofs about it, so I just want to simplest solution.

#### Jesse Slater (Oct 21 2023 at 20:59):

All I need to do with the result is look at it

#### Jesse Slater (Oct 21 2023 at 21:04):

@Yaël Dillies I am sure this would solve my problem, but I apologize, I have no idea how to use it.

#### Alex J. Best (Oct 21 2023 at 21:09):

Here is an example

import Std

def apply_random_n
{i : Nat}
(h : 0 < i)
(start n : Nat)
(v : Fin i → Nat → Nat)
(g : StdGen)
: Nat × StdGen :=
match n with
| 0 => (start, g)
| n' + 1 =>
let rs := (randNat g 0 (i - 1))
let r : Fin i := Fin.ofNat' rs.1 h
--r should be randomly generated each step
Prod.map (v r) id (apply_random_n h start n' v rs.2)

-- some code to demo how it works, you don't need to understand all of this, just that we have to update g every time
open Lean Meta
#eval show MetaM Unit from do
let mut g := mkStdGen
for _ in List.range 10 do
let a := apply_random_n (sorry : 0 < 10) 0 1 (fun j i => i + j.val) g
dbg_trace a.1
g := a.2 -- if you comment out this line there is no randomness


#### Jesse Slater (Oct 21 2023 at 21:20):

Thank you, this is perfect!

#### Eric Wieser (Oct 22 2023 at 08:01):

Don't we have a Fin instance for docs#Random ?

#### Eric Wieser (Oct 22 2023 at 08:01):

docs#Random.instRandomFinSucc

#### Eric Wieser (Oct 22 2023 at 08:01):

I guess we should change that to NeZero as in Yaël's example

Last updated: Dec 20 2023 at 11:08 UTC