need for 'explicit' type conversion using rw

Stream: new members

[Jasper Ganten]

Hello, I am tinkering around with PMFs and proving my definition of binomial is the PMF.binomial, I came across this problem:

import Mathlib

noncomputable def binom_do_rec (p : ENNReal) (h : p ≤ 1) : (n : ℕ) → PMF (Fin (n+1))
  | 0 => PMF.pure 0
  | n+1 => do
    let Head ← PMF.bernoulli p h
    let X ← binom_do_rec p h n
    if Head then
      return X+1
    else
      return X

theorem my_binom_is_binom (p : ENNReal) (h : p ≤ 1) : binom_do_rec p h = PMF.binomial p h := by
  ext n S
  refine DFunLike.congr ?_ rfl
  induction n with
  | zero =>
    dsimp [binom_do_rec]
    ext x
    simp
    rw [Fin.fin_one_eq_zero x, if_pos rfl]
    rw [PMF.binomial_apply_self p h] -- does not find instance of (PMF.binomial p h ?n) ↑?n
    rw [ pow_zero]
  | succ m hm => sorry

The proof state is 1 = (PMF.binomial p h 0) 0. I got that the casting of the 0 is not trivial and AI pointed me to the workaround:

    have : (0 : Fin 1) = ↑(0 : ℕ) := by simp
    rw [this]

before the rewrite in question works but I still wonder why the casting is not done by lean? Are there stronger tactics that manage this (simp only did not work in my case). How can I figure out if the problem is lean not casting/converting or maybe just not the correct theorem in the general case?
Many thanks!

[Jasper Ganten]

note: the beginning also feels kind of sketchy - happy for any suggestion :)

[Kenny Lau]

why are you using do in definitions...

[Kenny Lau]

Also I would recommend that you define it directly rather than recursively.

[Kenny Lau]

I see, you also referenced the already-defined PMF.binomial.

[Kenny Lau]

you can refer to how the source code defines it directly, as I predicted

[Kenny Lau]

@Jasper Ganten here's the correct code, note the first part as well:

import Mathlib

noncomputable def binom_do_rec (p : ENNReal) (h : p ≤ 1) : (n : ℕ) → PMF (Fin (n+1))
  | 0 => PMF.pure 0
  | n+1 => do
    let Head ← PMF.bernoulli p h
    let X ← binom_do_rec p h n
    if Head then
      return X.succ
    else
      return X.castSucc

theorem my_binom_is_binom (p : ENNReal) (h : p ≤ 1) : binom_do_rec p h = PMF.binomial p h := by
  ext n S
  refine DFunLike.congr ?_ rfl
  induction n with
  | zero =>
    ext x
    simp [binom_do_rec, Fin.fin_one_eq_zero x]
  | succ m hm => sorry

[Kenny Lau]

you need succ and castSucc instead of +1

[Kenny Lau]

and simp is quite powerful if you just supply it with the relevant lemmas

[Jasper Ganten]

Kenny Lau said:

why are you using do in definitions...

more or less as an exercise... if done more beautifully I think (especially for the discrete PMFs) the code becomes more like the intuitive definition. thats the motivation

[Jasper Ganten]

I think my error was to only try simp only, which then doesnt do the necessary simplifications!

[Jasper Ganten]

Kenny Lau said:

you need succ and castSucc instead of +1

I get why this is much 'cleaner' but shouldnt the return automatically try to convert?
If the defintion is not correct then this should throw an error, or not?
Thanks for your answers :)

[Aaron Liu]

Jasper Ganten said:

Kenny Lau said:

you need succ and castSucc instead of +1

I get why this is much 'cleaner' but shouldnt the return automatically try to convert?
If the defintion is not correct then this should throw an error, or not?
Thanks for your answers :)

It converts to a Nat, and then to a Fin, which introduces a mod n in the value

[Kenny Lau]

Jasper Ganten said:

Kenny Lau said:

you need succ and castSucc instead of +1

I get why this is much 'cleaner' but shouldnt the return automatically try to convert?
If the defintion is not correct then this should throw an error, or not?
Thanks for your answers :)

It does throw and error if you click on the code itself (the top right corner of every code block has a little button that allows you to run it online)

[Kenny Lau]

image.png

[Aaron Liu]

Did they get rid of the Fin -> Nat -> Fin shenanigans?

[Kenny Lau]

it could be possible

[Kyle Miller]

Kenny Lau said:

why are you using do in definitions...

It's the Giry monad!

I thought I remembered that there was a do in the definition of product measures at some point, but I can't find it. Maybe it it got generalized because of the universe level constraints with do.

[Jasper Ganten]

how should I think about the limitations of do notation?
I was given the task to explore discrete PMFs and write them down using do but I am not even sure if bernoulli can be written from the dirac PMFs in do notation...

[Kyle Miller]

The universe limitation is that Bind.bind requires both the source and target to be in the same universe. If all of your types are in Type for example, then do is ok. Otherwise, you can use PMF.bind manually.

[Kyle Miller]

I think you're right that Bernoulli is basic (in the sense that it can't be defined with do alone and uniform PMFs), without some sort of operation to re-weight things.

[Kyle Miller]

A kind of fun definition of the binomial distribution is

noncomputable def binom₀ (p : ENNReal) (h : p ≤ 1) (n : ℕ) : PMF ℕ := do
  let choices ← sequence <| List.replicate n (PMF.bernoulli p h)
  return choices.count true

It's very clearly "take a sequence of n weighted coin flips and count the number of heads".

Proving the support of this is what I thought it was took some doing though... The proof I came up with is really not good. It's clear though that there's some missing theory for dealing with do/monads and PMFs.

theorem binom_support (p : ENNReal) (h0 : 0 < p) (h1 : p < 1) (n : ℕ) :
    (binom₀ p h1.le n).support = Set.Iic n

code

import Mathlib

noncomputable def binom₀ (p : ENNReal) (h : p ≤ 1) (n : ℕ) : PMF ℕ := do
  let choices ← sequence <| List.replicate n (PMF.bernoulli p h)
  return choices.count true

theorem PMF.monad_pure_eq_pure (α : Type*) (x : α) : (Pure.pure x : PMF α) = PMF.pure x := rfl

universe u

theorem List.sequence_nil {α : Type u} {f : Type u → Type u} [Applicative f] :
    sequence ([] : List (f α)) = pure [] := rfl

theorem List.sequence_cons {α : Type u} {f : Type u → Type u} [Applicative f]
    (x : f α) (xs : List (f α)) :
    sequence (x :: xs) = List.cons <$> x <*> sequence xs := rfl

theorem binom_support (p : ENNReal) (h0 : 0 < p) (h1 : p < 1) (n : ℕ) :
    (binom₀ p h1.le n).support = Set.Iic n := by
  have : 0 < 1 - p := tsub_pos_of_lt h1
  have h1' : 1 - p ≠ 0 := (ne_of_lt this).symm
  have h0' : p ≠ 0 := h0.ne.symm
  ext i
  simp [binom₀, PMF.monad_map_eq_map]
  constructor
  · rintro ⟨xs, h, rfl⟩
    contrapose! h
    induction n generalizing xs with
    | zero =>
      simp [List.sequence_nil, PMF.monad_pure_eq_pure]
      rintro rfl
      simp at h
    | succ n ih =>
      simp [List.replicate, List.sequence_cons, PMF.monad_map_eq_map, PMF.monad_seq_eq_seq]
      simp [h1', h0']
      rintro f ys rfl
      rw [or_iff_not_imp_left, not_and_or, not_not, not_not]
      rintro (rfl | rfl)
      · apply ih
        simp at h
        omega
      · apply ih
        simp at h
        omega
  · intro h
    use (List.replicate (n - i) false ++ List.replicate i true)
    simp [List.count_replicate]
    induction n with
    | zero =>
      simp [List.sequence_nil, PMF.monad_pure_eq_pure]
      omega
    | succ n ih =>
      simp [List.replicate, List.sequence_cons, PMF.monad_map_eq_map, PMF.monad_seq_eq_seq]
      simp [h1', h0']
      rw [Nat.le_add_one_iff] at h
      obtain h | rfl := h
      · specialize ih h
        use List.cons false
        use (List.replicate (n - i) false ++ List.replicate i true)
        simp [ih]
        have : n + 1 - i = n - i + 1 := Nat.sub_add_comm h
        simp [this, List.replicate]
      · use List.cons true
        use List.replicate n true
        simp [List.replicate]
        clear ih
        induction n with
        | zero =>
          simp [List.sequence_nil, PMF.monad_pure_eq_pure]
        | succ n ih =>
          simp [List.replicate, List.sequence_cons, PMF.monad_map_eq_map, PMF.monad_seq_eq_seq]
          use List.cons true
          use List.replicate n true
          simp [h0', ih]

[Kenny Lau]

oh, the repeat function is called List.replicate!!!!! I was searching for that for so long, because I expected List.repeat (sorry off topic)

[Jasper Ganten]

@Kyle Miller That's amazing, thanks!
Why is the List converted to a sequence in your definition?
Is there no .count for lists (if yes, why)?
update: got it more or less - for flattening / evaluating the List

[Jasper Ganten]

@Kyle Miller The other question would be the motivation for using Set.Iic n as the support. Is this in general more elegant since going for some more explicit statement would result in proving the less-equal statement and show it from there?

[Kyle Miller]

Jasper Ganten said:

update: got it more or less - for flattening / evaluating the List

Yeah, the sequence function takes a list of PMFs and yields a PMF of lists.

The function is generic too, it works for any Traversable type.

[Kyle Miller]

Don't read much into the choice of Set.Iic -- it was just convenient when writing the theorem statement!

[Jasper Ganten]

Why is the step in between return a -> Pure.pure a -> PMF.pure a necessary? Is there a case when you don't want to apply the PMF.pure definition? Since simp handles the Pure.pure conversion this is not such a big thing but I wonder whats the reasoning behind this extra step in the interpretation of the do notation...

[Robin Arnez]

It's the same thing as 3 + 4 not being elaborated to Nat.add 3 4. The idea is that the "notation" pure should rather be used by lemmas, unless that's unwanted in which case there should a simp lemma converting it into the underlying operation (e.g. PMF.pure).

[Jasper Ganten]

I get that in a general case. But using do notation to my understanding already requires the Monad I am in to be specified. So if I say sth like (3+4 : Nat) should be elaborated.
A simpler case of my confusion is this:

noncomputable def pureDo (a : α) : (PMF α) := do
  return a

noncomputable def pureDo' (a : α) : (PMF α) := PMF.pure a

So why should the do notation in this case return a not be elaborated to PMF.pure?
To be honest I did not really understand what you wanted to say with 'unless thats unwanted'.
The main point is that the proofs for requires the additional step from Pure.pureto PMF.pure (a problem that is none if you use simp, but I am asking to undestand the elaboration).

noncomputable def pureDo {α} (a : α) : (PMF α) := do
  return a

noncomputable def pureDo' {α} (a : α) : (PMF α) := PMF.pure a

theorem pureDo_eval {α} (a : α) : (pureDo a) a = 1 := by
  rw [pureDo]
  simp only [Pure.pure] -- extra needed only with the do notation
  rw [PMF.pure_apply]
  exact if_pos rfl

theorem pureDo_eval' {α} (a : α) : (pureDo' a) a = 1 := by
  rw [pureDo']
  rw [PMF.pure_apply]
  exact if_pos rfl

[Aaron Liu]

It's the same reason we don't elaborate (3 + 4 : Real) to Real.add 3 4 and (3 + 4 : Rat) to Rat.add 3 4 and (3 + 4 : Int) to Int.add 3 4 and (3 + 4 : Nat) to Nat.add 3 4. It's so you can use the same lemmas (like docs#add_comm) for all these cases. In the case of monads we have stuff like docs#bind_pure.

[Kyle Miller]

You're running into the "multiple languages for the same thing" problem @Jasper Ganten. The PMF library seems to be written primarily in terms of PMF functions directly, and there's not much in the way of theory about monads. Yes, Pure.pure for PMF is defined to be PMF.pure, but the first is in the "monad language" and the second is in the "PMF language". It's best not to think of these two ways of expressing things as being exactly the same. You should think "these are (slightly) different languages, and it will take translation".

It would be worth writing some translation lemmas, like I did with PMF.monad_pure_eq_pure, and then possibly make a simp set, so that way you can write simp [pmf_of_do] and turn all the "do language" into "PMF language".

[Jasper Ganten]

Thanks to the both of you, this makes lots of sense. My confusion is probably the symptom of trying to learn lean and category theory/monads at the same time :smile: ... The suggestion to make a simp set is great, since there is not much I will do on the monad level (although it's intriguing to expand on this in the future maybe) :)