getElem for Lists

Stream: new members

[Robert Shlyakhtenko]

I am working in a context where I frequently need to get an element corresponding to some list index. If I write something like l[i], then Lean (usually) complains and asks for a proof that the index I am trying to access is valid.

I don't want to have to write a proof every time I try to access an index, so I was wondering what the idiomatic workaround is. I tried l[i]!; my understanding is that this forces Lean to accept the index but will cause an error if I ever try to run the code (?).

However, this led to errors later on in the proof: somehow I got both l[i] and l[i]!] in the same expression (with Lean now somehow being able to infer that l[i] is a valid index using the get_elem_tactic, even though it couldn't infer this before), and I don't know how to get Lean to accept them as the same thing (since they are not syntactically equal).

What is considered the best way to handle this?

Thanks!

[Aaron Liu]

The workaround is to prove your index is valid and then have the proof so it's in your context and get_elem_tactic can just use that

[Aaron Liu]

can you provide a #mwe?

[Robert Shlyakhtenko]

Aaron Liu said:

The workaround is to prove your index is valid and then have the proof so it's in your context and get_elem_tactic can just use that

Thank you, that's a good tip! I didn't consider that it would be enough to just have the proof in the context.
I suppose I would still need to write in the proof explicitly at least once, though, to state the lemma.

In this case, maybe it's not so bad and I should just prove validity of all the indices instead of being lazy :)

[Vlad]

Robert Shlyakhtenko said:

I don't know how to get Lean to accept them as the same thing (since they are not syntactically equal).

docs#getElem!_pos