Zulip Chat Archive

Stream: new members

Topic: non-local error message with induction in Lean4


Samuel Thomas (Dec 18 2022 at 06:01):

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 (Dec 18 2022 at 07:16):

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 (Dec 18 2022 at 07:19):

This way works

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

Samuel Thomas (Dec 18 2022 at 07:29):

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?


Last updated: Dec 20 2023 at 11:08 UTC