Cannot prove index is valid

Stream: lean4

[𝚠𝚘𝚓𝚌𝚒𝚎𝚌𝚑 𝚗𝚊𝚠𝚛𝚘𝚌𝚔𝚒]

I am running into issues with the get_elem_tactic tactic not being able to prove list indices are valid in certain situations where another argument also depends on the index being valid. It seems like something is going wrong with the elaboration order, though I am not certain of that. Here is an MVP:

axiom A : Type
axiom B : A → Type
axiom as : List A
axiom fn : (l : Nat) → (_ : l < as.length) → Option (B as[l])

example {l : Nat} {llen : l < as.length} {b : B as[l]}
                                             -- ^ failed to prove index is valid
    (b_mem : b ∈ fn l llen) : True := sorry

example {l : Nat} {llen : l < as.length} {b : B as[l]} /- works -/ : True := sorry

Does this look like something worth reporting on the GitHub issue tracker?

[Robin Arnez]

Yes, please report this! This seems to be because actually the index proof has been determined using unification and get_elem_tactic fails with "no goals" (lol).

[Joachim Breitner]

Thanks for the extra analysis, good catc. Please mention it on the issue as well!