List.map prints with do notation in goals under coercion

Stream: new members

[Success Moses]

Hello,
My code :

open List Fin
variable (n : ℕ) (M : Type) [Monoid M] (a : M) (l : List M) (f : (Fin (n.succ)) -> M)

open scoped Fin.NatCast

instance {n : ℕ} : CoeFun (Fin (n.succ) → α) (fun _ => Fin n → α) :=
  ⟨fun f => f ∘ Fin.castSucc⟩

variable (f₁ : Fin (n.succ) → α)
#check (f₁ : (Fin n) → α)

theorem Fin.prod_range_succ :
    ((finRange n.succ).map f).prod = ((finRange n).map (f)).prod * f n := by
  sorry

I am trying to prove the theorem prod_range_succ but the goal looks like this

n : ℕ
M : Type
inst✝ : Monoid M
f : Fin n.succ → M
⊢ (map f (finRange n.succ)).prod =
  (map f do
        let a ← finRange n
        pure ↑↑a).prod *
    f ↑n

finRange n becomes do notation. The do notation looks wierd. Is it something I did wrong here? I created a custom way to cast Fin n.succ -> a to Fin n -> a so that the theorem type-checks. Did I break something?

[Kenny Lau]

yeah, you shouldn't try to make a custom coercion

[Aaron Liu]

Lean decided it wanted to do a coercion inside the monad and it used the instance for that

[Robin Arnez]

Don't try to abuse coercions, just be explicit with what you want (also avoid open scoped Fin.NatCast and use appropriate functions like Fin.last instead):

import Mathlib

open List Fin

theorem List.prod_finRange_succ_last {M : Type*} [Monoid M] {n : ℕ} (f : Fin n.succ → M) :
    ((finRange n.succ).map f).prod = ((finRange n).map (f ∘ castSucc)).prod * f (Fin.last n) := by
  rw [List.finRange_succ_last, map_append, map_singleton, map_map, prod_append, prod_singleton]

[Success Moses]

Hi, thanks for providing a proof @Robin Arnez . Is there any structure of \N, apart from Fin n, that has a proof that k < n and does not have the typing problem like Fin n?

[Kenny Lau]

it's not a "problem", if you require proofs, then the proofs will have to change every time

[Aaron Liu]

Success Moses said:

and does not have the typing problem like Fin n?

Which problem are you referring to?

[Success Moses]

import Mathlib

open List Fin

theorem List.prod_finRange_succ_last {M : Type*} [Monoid M] {n : ℕ} (f : Fin n.succ → M) :
    ((finRange n.succ).map f).prod = ((finRange n).map (f ∘ castSucc)).prod * f (Fin.last n) := by
  rw [List.finRange_succ_last, map_append, map_singleton, map_map, prod_append, prod_singleton]

Like in this proof, f has to be composed with castSucc to typecheck. A function defined on List Nat does not have this problem.

[Kenny Lau]

that's the purpose of having types