Incomplete List Verification APIs

Stream: mathlib4

[David J. Webb]

I noticed that the documentation for Init.Data.List.Find has several incomplete APIs - idxOf, finIdxOf?, and IdxOf?. Is anyone working on these?

I've proved a few of the missing theorems for use in my own work, so I'm considering working on filling in the rest of the API - but I don't want to duplicate work that's already underway.

[Kim Morrison]

As far as I'm aware no one is currently working on these. I would like these filled, and am happy to review and merge PRs doing so, or to discuss here what should be done!

[David J. Webb]

Okay great, I will move that up my to-do list!

There were a few proofs here: #Is there code for X? > ✔ List index and membership, and I've got

theorem idxOf?_getElem?_iff {α : Type} [inst : DecidableEq α] {a : α} {n : ℕ} {L : List α}
    (h : ∀ i < n, L[i]? ≠ a) : n = List.idxOf? a L ↔ L[n]? = a

and

theorem idxOf?_append {α : Type} [BEq α] [LawfulBEq α] {l₁ l₂ : List α} {a : α} :
    idxOf? a (l₁ ++ l₂) = if a ∈ l₁ then idxOf? a l₁
    else (List.idxOf? a l₂).map (· + l₁.length)

which (I hope) seems like enough for the computable enumeration stuff I'm working on. I figure as long as I've knee-deep in lists, I may as well keep plugging away after that.

[David J. Webb]

My very rudimentary approach is going to be to follow the current suggestions in the documentation, and then add any other ? versions of non-? lemmas that exist already. But if there's anything else that should be added, I'd be happy to chip away at it.

[David J. Webb]

@Kim Morrison Got to a stopping point in my computability formalization work, so, gonna get started on Lists now :)

[Kim Morrison]

Thank you, looking forward to it. (Be aware that I'm about to be away for two weeks, so don't expect speedy reviews from me. It's possibly that others will be able to review/merge in the meantime, however!)

[Eric Wieser]

David J. Webb said:

theorem idxOf?_append {α : Type} [BEq α] [LawfulBEq α] {l₁ l₂ : List α} {a : α} :
    idxOf? a (l₁ ++ l₂) = if a ∈ l₁ then idxOf? a l₁
    else (List.idxOf? a l₂).map (· + l₁.length)

I wonder if this would be better as
idxOf? a (l₁ ++ l₂) = idxOf? a l₁ <|> (List.idxOf? a l₂).map (· + l₁.length)

[David J. Webb]

I was pattern matching to List.idxOf_append

[Eric Wieser]

That's a good answer on your side, I guess then I'm curious whether @Kim Morrison thinks <|> would be a more convenient spelling of the List one.

[David J. Webb]

I have a draft PR for the idxOf API now - I proved the lemmas in my usual Mathlib workspace, but creating a new one just for tinkering with Lean itself is causing trouble. Once I've resolved that (so that I can be sure the changes to Find.lean actually compile), I will make it an actual PR.

[Kim Morrison]

Happy if you make the naming changes to resolve those naming discrepancies. Remember though that we prefer to put _iff in a name if it's at all non-obvious the statement will be an iff.