Case split on proposition in `if`

Stream: new members

[Josh Cohen]

Suppose I have the following

def foo (l1 l2: List Nat) : List Nat :=
  match l1 with
  | [] => []
  | x :: xs => if x ∈ l2 then x :: foo xs l2 else foo xs l2

theorem fooLength l1 l2: (foo l1 l2).length <= l1.length := by
  induction l1 with
  | nil => simp[foo]
  | cons x xs IH => simp[foo]; by_cases (x ∈ l2)

by_cases does not reduce the if-expression, and cases fails because Prop is not an inductive type. What is the best way to reason by cases here?

[Aaron Liu]

Well there's the split tactic

[Aaron Liu]

and if you have mathlib there's the split_ifs tactic

[Josh Cohen]

split works sometimes, but I have found it to be somewhat unpredictable if the if-expression is nested inside something else (e.g. a match)

[Aaron Liu]

also docs#if_pos and docs#if_neg