uniform dist over Fin n set

Stream: mathlib4

[Hannah Leung]

Hi there, I am new to Lean4. Sorry if my question is too naive. I am trying to get a uniform distribution over a Fin set : Fin n, where n > 0. So far I've got the following, but I am having trouble getting the fact that n > 0 through.

variable (n : ℕ) [hn : Fact (0 < n)]

def finNonempty (n : ℕ) [hn : Fact (0 < n)] : Nonempty (Fin n) :=
  ⟨⟨0, hn.out⟩⟩

lemma bnonempty (n : ℕ) (hs : Nonempty (Fin n)):
(Finset.univ : Finset (Fin n)).Nonempty :=
    Finset.univ_nonempty

def uniformBin {α : Type*} (n : ℕ) : PMF (Fin n) :=
  PMF.uniformOfFinset (Finset.univ : Finset (Fin n)) (bnonempty n (finNonempty n))

lean4 complains that "failed to synthesize Fact (0 < n)".

[Rémy Degenne]

If you are fine with a Measure instead of a PMF: ProbabilityTheory.uniformOn

[Yaël Dillies]

The issue is that def uniformBin {α : Type*} (n : ℕ) : redeclares a new n, with no relation to the precedent one. Try instead def uniformBin {α : Type*} :

[Hannah Leung]

Rémy Degenne said:

If you are fine with a Measure instead of a PMF: ProbabilityTheory.uniformOn

I am curious about this choice, is it because it's easier to use and better supported?

[Hannah Leung]

Yaël Dillies said:

The issue is that def uniformBin {α : Type*} (n : ℕ) : redeclares a new n, with no relation to the precedent one. Try instead def uniformBin {α : Type*} :

How does lean make association of the parameters in precedent definitions? This is confusing to me? What is the name of the mechanism?

[Bolton Bailey]

Welcome to the Zulip!

Presumably the name you are looking for is "Section Variables". Here is a reference to the manual, although I feel the manual does not particularly explain well this point of confusion.

[Bolton Bailey]

I think what is going on is that this code is effectively equivalent to one in which the variable you put in the definition itself shadows the one declared in the variable statement:

import Mathlib

def finNonempty (n : ℕ) [hn : Fact (0 < n)]  (n : ℕ) [hn : Fact (0 < n)] : Nonempty (Fin n) :=
  ⟨⟨0, hn.out⟩⟩

lemma bnonempty (n : ℕ) [hn : Fact (0 < n)] (n : ℕ) (hs : Nonempty (Fin n)):
(Finset.univ : Finset (Fin n)).Nonempty :=
    Finset.univ_nonempty

noncomputable def uniformBin (n : ℕ) [hn : Fact (0 < n)] {α : Type*} (n : ℕ) : PMF (Fin n) := _ -- cursor here to see the context
  -- PMF.uniformOfFinset (Finset.univ : Finset (Fin n)) (bnonempty n (finNonempty n)) -- gives the same error