LCGs.v

LCGs.v

Require Import Coq.ZArith.ZArith.

Inductive rand : Set :=
| State : Z -> rand.

(* 線形合同法による疑似乱数 *)
Definition next (r : rand) : rand :=
  match r with
  | State s => 
    let s' := Z.modulo (Z.mul 48271 s) 2147483647 in 
    State s'
  end.

Fixpoint nextN (n : nat) (r : rand) : rand :=
  match n with
  | O => r
  | S n => nextN n (next r)
  end.

Definition get (r : rand) : Z :=
  match r with
  | State s => s
  end.

Require Import List.
Import ListNotations.

Fixpoint nexts (n : nat) (r : rand) : list Z :=
  match n with
  | O => nil
  | S n => get r :: nexts n (next r)
  end.

Definition seed : Z := 1073741823.
Definition n := 12345.

Compute List.map (fun z => Z.modulo z 2) (nexts 10 (State seed)).
Compute Z.modulo (get (nextN n (State seed))) 2.