fin_random instance

Stream: general

[Fabian Glöckle]

The following code runs successfully, but fails if 1000 is replaced by 10000:

import system.random.basic

meta def rnd_comp (g : Type) [random_gen g] : list (fin 1000) → nat → rand_g g (list (fin 1000))
| l 0 := return l
| l (n+1) := have h : 0 < 1000 := by obviously, do x ← rand.random (fin 1000), (rnd_comp (x::l) n)

meta def trace_rnd : tactic (list nat) :=
do
  g ← tactic.mk_generator,
  res ← tactic.run_rand $ rnd_comp std_gen [] 30,
  return (list.map (λ (x : fin 1000), x) res)

#eval trace_rnd >>= tactic.trace

In the latter case, the random (fin 10000) instance from docs#fin_random is no longer found, despite h : 0 < 10000 being available in the context.
As I do not know how type class resolution works, I thought I'll better report this. (I can, however, easily work around it.)

[Reid Barton]

What you need is fact (0 < 10000) in the type class context. I'm not sure how to cajole the equation compiler into doing it right.

[Reid Barton]

There is a global instance docs#succ_pos'' that in principle should provide fact (0 < 10000) but I guess the elaborator gives up before doing enough unfolding to see this

[Fabian Glöckle]

I don't know how to get the fact, but the hypothesis is there:

failed to synthesize type class instance for
g : Type,
_inst_1 : random_gen g,
rnd_comp : list (fin 10000) → ℕ → rand_g g (list (fin 10000)),
l : list (fin 10000),
n : ℕ,
h : 0 < 10000
⊢ random (fin 10000)

[Fabian Glöckle]

Oh, I see.
So the fact comes from docs#succ_pos'', not from the local context

[Mario Carneiro]

you can also use nat.succ 9999 instead of 10000

[Fabian Glöckle]

Mario Carneiro said:

you can also use nat.succ 9999 instead of 10000

yes, that works :D

[Fabian Glöckle]

thank you both!

[Mario Carneiro]

meta def rnd_comp (g : Type) [random_gen g] : list (fin 10000) → nat → rand_g g (list (fin 10000))
| l 0 := return l
| l (n+1) := do
  x ← by haveI := fact.mk (by norm_num : 0 < 10000); exact rand.random (fin 10000),
  rnd_comp (x::l) n

[Fabian Glöckle]

very elegant :+1: thanks!