# Zulip Chat Archive

## 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⟩
end Monad
```

#### 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):

#### 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