show that Array.find? and Array.findFinIdx? consistent

Stream: general

[Frederick Pu]

is there any theorem that says Array.find? and Array.findFinIdx? will return the same underlying element? ie:

​theorem Array.find?_eq_getElem_findFinIdx? {α : Type u}
(xs : Array α) (p : α → Bool):
 xs.find? p = (xs.findFinIdx? p).map (xs[·])

[Vlad]

import Mathlib.Tactic

example {α : Type*} {xs : Array α} {p : α → Bool} :
xs.find? p = (xs.findFinIdx? p).map (xs[·]) := by
  rcases xs with ⟨xs⟩; ext
  simp [List.findFinIdx?_eq_pmap_findIdx?, List.findIdx?_eq_fst_find?_zipIdx,
    List.find?_eq_some_iff_getElem]
  constructor
  · rintro ⟨_, _, _, rfl, _⟩; grind
  · grind

[Frederick Pu]

should this be in mathlib?

[Wrenna Robson]

I think there might actually be a case for this in Batteries if these are defined there. Though surely you want to look at findIdx also.

[Ayhon]

Vlad said:

  constructor
  · rintro ⟨_, _, _, rfl, _⟩; grind
  · grind

I'm curious, why do we need to specify explicitly a substitution for grind to be able to finish the proof. Isn't its e-matching engine already implicitly having the same effect?

[Kim Morrison]

I've added the theorems relating find? with findIdx? and findFinIdx? in lean#12204.

The PR includes both directions:

• Forward: expressing find? in terms of index functions
• Reverse: expressing index functions in terms of find?

All theorems are provided for List, Array, and Vector.

[Wrenna Robson]

Oh brilliant.