Indexing after List.findIdx?

Stream: new members

[Mark Fischer]

I may have worked myself into a corner. Maybe somebody more experienced than me can help me navigate my way out. While I'm sure there's a theorem in Mathlib for this, I can't find it, so I've been trying to prove this for myself. It's also just for practice anyway, but I think I'm just not fully there yet with proofs by induction.

example (l : List α) (p : α → Bool) (i : ℕ) (h : List.findIdx? p l = some i) : i < l.length := by
  induction l with
  | nil => simp only [List.findIdx?_nil] at h
  | cons x xs ih =>
    by_cases hb : p x
    . simp_all only [List.findIdx?_cons, zero_add, List.findIdx?_succ, ite_true, Option.some.injEq,List.length_cons]
      linarith
    . simp_all only [List.findIdx?_cons, zero_add, List.findIdx?_succ, ite_false,
      Option.map_eq_some', Bool.not_eq_true, List.length_cons]
      obtain ⟨i', ih', ip⟩ := h
      rw [← ip]
      refine Nat.succ_lt_succ ?_
      sorry

[Timo Carlin-Burns]

With proofs by induction, it's important to choose your induction hypothesis carefully. In this case, I think your induction hypothesis is not strong enough. Consider the goal state in the cons case:

ih: List.findIdx? p xs = some i → i < List.length xs
h: List.findIdx? p (x :: xs) = some i
hb: ¬p x = true
⊢ i < List.length (x :: xs)

We can only use ih if the first match in xs is at position i, but that's not possible.h tells that the first match in x :: xs is at position i, which would mean the first match in xs is at position i - 1.

You can use induction ... generalizing ... to get a stronger induction hypothesis like this:

example (l : List α) (p : α → Bool) (i : ℕ) (h : List.findIdx? p l = some i) : i < l.length := by
  induction l generalizing i with -- we need our induction hypothesis to apply for all `i`
  | nil => simp only [List.findIdx?_nil] at h
  | cons x xs ih =>
    by_cases hb : p x
    . simp_all only [List.findIdx?_cons, zero_add, List.findIdx?_succ, ite_true, Option.some.injEq,List.length_cons]
      linarith
    . simp_all only [List.findIdx?_cons, zero_add, List.findIdx?_succ, ite_false,
      Option.map_eq_some', Bool.not_eq_true, List.length_cons]
      obtain ⟨i', ih', ip⟩ := h
      rw [← ip]
      refine Nat.succ_lt_succ ?_
      apply ih
      exact ih'

(Note that this is not magic. You could do this manually with revert i; induction l; intro i)

[Mark Fischer]

Ah, revert i! I see. thanks