non-local error message with induction in Lean4

Stream: new members

[Samuel Thomas]

I'm running into a weird error message with Lean 4 that feels like it's being reported in the wrong place.

I'm trying to write a function that is analogous to List.enum but is defined on Vectors (Lists of known length). I want to pass along the fact that the added indices are less than the length of the list. I've simplified the following example so that this function just pairs every element with 0. Here is the simplified implementation.

abbrev Vector (α : Type u) (n : Nat) := { l : List α // l.length = n }

def Vector.enum {α : Type u} {n : Nat} (l : Vector α n) : Vector (Fin n × α) n :=
  match Nat.decLt 0 n with
  | isTrue p =>
    let l' := l.val.map (λ a => (Fin.mk 0 p, a))
    let p' : List.length l' = n := by
      induction l.property with
      | refl => simp
    ⟨ l', p' ⟩
  | isFalse _ =>
    let p := by
      have lprop := l.property
      simp_arith [*] at *
      subst n
      rfl
    ⟨ [], p ⟩

The language server is reporting the following error at the definition of the function Vector.enum.

application type mismatch
   l.val
 argument has type
   Vector α n✝
 but function has type
   { l // List.length l = n } → List α

If I replace the induction in the isTrue branch with just sorry. Then this function is able to be defined (though obviously it yells at me that the function uses sorry.

What is induction doing that causes this function not to type check? Why is the error message being reported at the function definition, rather than when I call l.val? Is there a way to make this proof go through without induction?

[Reid Barton]

I think you cannot do induction on l.property like this, because it would set n to List.length l but the type of l depends on n.

[Reid Barton]

This way works

    let p' : List.length l' = n := by
      cases l
      subst n
      simp
    ⟨ l', p' ⟩

[Samuel Thomas]

Ah thank you. That makes sense and I can get the proof to go through now. Do you think that it's a bug that the error reporting is using the name of the function as the location of the error?