how to deal with "motive / result is not type correct"?

Stream: lean4

[Jan-Mirko Otter]

Hi,

I often find myself in the situation that many useful tactics fail to work if there are dependent types involved:

• conv refuses to select arguments if there are dependencies
• rw, generalize, cases ... do not work either

I understand why; if I just naively replace some expressions with some equal (but not defeq) expressions, some types which depend on it may not be definitional equal to what they are suppossed to be. In many cases, I manage to use dependent elimination, but not always.

Consider the following simple example: I have a filtered list, and I want to prove that getting something out of the filtered list is the same as getting something (possible at a different index) from the original list:

theorem get_from_filtered {T : Type u} (l : List T) (pred : T -> Bool)
  (idx : Fin (l.filter pred).length)
  : ∃ idx' : Fin l.length, (l.filter pred).get idx = l.get idx' :=by
  induction l
  . have : idx.val < 0 :=idx.isLt
    contradiction
  . rename_i head tail IH

    simp only [List.filter]

    -- how to continue from here?
    cases pred head -- does not work, result is not type correct

    sorry

Intuitively, the rest of the proof is clear. For example, if pred head is false and idx.val > 0, I can use the induction hypothesis.

However, I fail to simplify List.filter pred (head :: tail) given the value of pred head.

Do you have any tips how to continue here?