Generate random Fin n

Stream: new members

[Jesse Slater]

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]

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]

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]

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]

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]

@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]

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

[Jesse Slater]

@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]

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]

Thank you, this is perfect!

[Eric Wieser]

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

[Eric Wieser]

docs#Random.instRandomFinSucc

[Eric Wieser]

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