generalized functions of `Fin n`?

Stream: mathlib4

[Arien Malec]

This is a little puzzle, worked in Lean 3, but fails in Lean 4

import Mathlib.Data.Vector

namespace Vector
infixr:67 " ::ᵥ " => Vector.cons

def mOfFn {m} [Monad m] {α : Type u} : ∀ {n}, (Fin n → m α) → m (Vector α n)
  | 0, _ => pure nil
  | _ + 1, f => do
    let a ← f 0
    let v ← mOfFn fun i => f i.succ
    pure (a ::ᵥ v)

theorem mOfFn_pure {m} [Monad m] [LawfulMonad m] {α} :
    ∀ {n} (f : Fin n → α), (@mOfFn m _ _ _ fun i => pure (f i)) = pure (ofFn f)
  | 0, f => rfl
  | n + 1, f => by simp [mOfFn, @mOfFn_pure m _ _ _ n f, ofFn] -- issue with `f` here

end Vector

error is:

argument
  f
has type
  Fin (n + 1) → α : Type u_1
but is expected to have type
  Fin n → ?m.10511 : Type u_1

[Arien Malec]

maybe it wants the fun i =>f i.succ like above?

[Mario Carneiro]

lean 4's message seems very reasonable here. I don't see how this could typecheck, f is not a Fin n function

[Arien Malec]

I think that's right, but how'd it work in Lean 3?

[Mario Carneiro]

what's the original code?

[Arien Malec]

Ah, in Lean 3, there's some magic with function parameters? There's a fix often where in Lean 3 the f is elided, and is required in Lean 4

[Arien Malec]

theorem m_of_fn_pure {m} [monad m] [is_lawful_monad m] {α} :
  ∀ {n} (f : fin n → α), @m_of_fn m _ _ _ (λ i, pure (f i)) = pure (of_fn f)
| 0     f := rfl
| (n+1) f := by simp [m_of_fn, @m_of_fn_pure n, of_fn]

[Mario Carneiro]

I don't think the argument is f

[Mario Carneiro]

does it not work with nothing / _?

[Arien Malec]

so it does....

[Arien Malec]

Now I've simp'd to a do notation....

[Arien Malec]

which is sort of unhelpful...

[Mario Carneiro]

I guess the lean 3 proof is using the simp lemma let a <- pure b; f a ~> f b

[Mario Carneiro]

which should also exist in lean 4

[Arien Malec]

what's the lemma called in Lean 3?

[Arien Malec]

there's pure_bind

[Arien Malec]

Through

theorem mOfFn_pure {m} [Monad m] [LawfulMonad m] {α} :
    ∀ {n} (f : Fin n → α), (@mOfFn m _ _ _ fun i => pure (f i)) = pure (ofFn f)
  | 0, f => rfl
  | n + 1, f => by
      simp only [mOfFn, @mOfFn_pure m _ _ _ n _, ofFn, pure_bind, bind_pure_comp]

I have the goal to ((fun a => f 0 ::ᵥ a) <$> mOfFn fun i => pure (f (Fin.succ i))) = pure (f 0 ::ᵥ ofFn fun i => f (Fin.succ i)) which feels close...