fix: split (for if-expressions) should work on non-propositional goals (#4349)

Remark: when splitting an `if-then-else` term, the subgoals now have
tags `isTrue` and `isFalse` instead of `inl` and `inr`.
closes #4313

---------

Co-authored-by: Mario Carneiro <di.gama@gmail.com>

src/Init/Data/AC.lean

@@ -146,8 +146,8 @@ theorem Context.evalList_mergeIdem (ctx : Context α) (h : ContextInformation.is
     | nil =>
       simp [mergeIdem, mergeIdem.loop]
       split
-      case inl h₂ => simp [evalList, h₂, h.1, EvalInformation.evalOp]
-      rfl
+      next h₂ => simp [evalList, h₂, h.1, EvalInformation.evalOp]
+      next => rfl
     | cons z zs =>
       by_cases h₂ : x = y
       case pos =>
@@ -191,11 +191,11 @@ theorem Context.evalList_insert
     . simp [evalList, h.1, EvalInformation.evalOp]
   | step y z zs ih =>
     simp [insert] at *; split
-    case inl => rfl
-    case inr =>
+    next => rfl
+    next =>
       split
-      case inl => simp [evalList, EvalInformation.evalOp]; rw [h.1, ctx.assoc.1, h.1 (evalList _ _ _)]
-      case inr => simp_all [evalList, EvalInformation.evalOp]; rw [h.1, ctx.assoc.1, h.1 (evalList _ _ _)]
+      next => simp [evalList, EvalInformation.evalOp]; rw [h.1, ctx.assoc.1, h.1 (evalList _ _ _)]
+      next => simp_all [evalList, EvalInformation.evalOp]; rw [h.1, ctx.assoc.1, h.1 (evalList _ _ _)]
 
 theorem Context.evalList_sort_congr
   (ctx : Context α)

src/Init/Data/Array/DecidableEq.lean

@@ -27,17 +27,17 @@ decreasing_by decreasing_trivial_pre_omega
 theorem eq_of_isEqv [DecidableEq α] (a b : Array α) : Array.isEqv a b (fun x y => x = y) → a = b := by
   simp [Array.isEqv]
   split
-  case inr => intro; contradiction
-  case inl hsz =>
+  next hsz =>
    intro h
    have aux := eq_of_isEqvAux a b hsz 0 (Nat.zero_le ..) h
    exact ext a b hsz fun i h _ => aux i (Nat.zero_le ..) _
+  next => intro; contradiction
 
 theorem isEqvAux_self [DecidableEq α] (a : Array α) (i : Nat) : Array.isEqvAux a a rfl (fun x y => x = y) i = true := by
   unfold Array.isEqvAux
   split
-  case inl h => simp [h, isEqvAux_self a (i+1)]
-  case inr h => simp [h]
+  next h => simp [h, isEqvAux_self a (i+1)]
+  next h => simp [h]
 termination_by a.size - i
 decreasing_by decreasing_trivial_pre_omega
 

src/Init/Data/BitVec/Lemmas.lean

@@ -244,10 +244,10 @@ theorem toInt_eq_msb_cond (x : BitVec w) :
 theorem toInt_eq_toNat_bmod (x : BitVec n) : x.toInt = Int.bmod x.toNat (2^n) := by
   simp only [toInt_eq_toNat_cond]
   split
-  case inl g =>
+  next g =>
     rw [Int.bmod_pos] <;> simp only [←Int.ofNat_emod, toNat_mod_cancel]
     omega
-  case inr g =>
+  next g =>
     rw [Int.bmod_neg] <;> simp only [←Int.ofNat_emod, toNat_mod_cancel]
     omega
 

src/Init/Data/Int/DivModLemmas.lean

@@ -1075,9 +1075,9 @@ theorem emod_mul_bmod_congr (x : Int) (n : Nat) : Int.bmod (x%n * y) n = Int.bmo
 theorem bmod_add_bmod_congr : Int.bmod (Int.bmod x n + y) n = Int.bmod (x + y) n := by
   rw [bmod_def x n]
   split
-  case inl p =>
+  next p =>
     simp only [emod_add_bmod_congr]
-  case inr p =>
+  next p =>
     rw [Int.sub_eq_add_neg, Int.add_right_comm, ←Int.sub_eq_add_neg]
     simp
 
@@ -1088,9 +1088,9 @@ theorem bmod_add_bmod_congr : Int.bmod (Int.bmod x n + y) n = Int.bmod (x + y) n
 theorem bmod_mul_bmod : Int.bmod (Int.bmod x n * y) n = Int.bmod (x * y) n := by
   rw [bmod_def x n]
   split
-  case inl p =>
+  next p =>
     simp
-  case inr p =>
+  next p =>
     rw [Int.sub_mul, Int.sub_eq_add_neg, ← Int.mul_neg]
     simp
 

src/Init/System/IO.lean

@@ -253,12 +253,9 @@ instance : ToString TaskState := ⟨TaskState.toString⟩
 @[extern "lean_io_wait"] opaque wait (t : Task α) : BaseIO α :=
   return t.get
 
-local macro "nonempty_list" : tactic =>
-  `(tactic| exact Nat.zero_lt_succ _)
-
 /-- Wait until any of the tasks in the given list has finished, then return its result. -/
 @[extern "lean_io_wait_any"] opaque waitAny (tasks : @& List (Task α))
-    (h : tasks.length > 0 := by nonempty_list) : BaseIO α :=
+    (h : tasks.length > 0 := by exact Nat.zero_lt_succ _) : BaseIO α :=
   return tasks[0].get
 
 /-- Helper method for implementing "deterministic" timeouts. It is the number of "small" memory allocations performed by the current execution thread. -/

src/Lean/Meta/Tactic/Cases.lean

@@ -323,6 +323,17 @@ def _root_.Lean.MVarId.byCases (mvarId : MVarId) (p : Expr) (hName : Name := `h)
     throwError "'byCases' tactic failed, unexpected number of subgoals"
   return ((← toByCasesSubgoal s₁), (← toByCasesSubgoal s₂))
 
+/--
+Given `dec : Decidable p`, split the goal in two subgoals: one containing the hypothesis `h : p` and another containing `h : ¬ p`.
+-/
+def _root_.Lean.MVarId.byCasesDec (mvarId : MVarId) (p : Expr) (dec : Expr) (hName : Name := `h) : MetaM (ByCasesSubgoal × ByCasesSubgoal) := do
+  let mvarId ← mvarId.assert `hByCases (mkApp (mkConst ``Decidable) p) dec
+  let (fvarId, mvarId) ← mvarId.intro1
+  let #[s₁, s₂] ← mvarId.cases fvarId #[{ varNames := [hName] }, { varNames := [hName] }] |
+    throwError "'byCasesDec' tactic failed, unexpected number of subgoals"
+  -- We flip `s₁` and `s₂` because `isFalse` is the first contructor.
+  return ((← toByCasesSubgoal s₂), (← toByCasesSubgoal s₁))
+
 builtin_initialize registerTraceClass `Meta.Tactic.cases
 
 end Lean.Meta

src/Lean/Meta/Tactic/SplitIf.lean

@@ -68,23 +68,24 @@ private def discharge? (numIndices : Nat) (useDecide : Bool) : Simp.Discharge :=
 def mkDischarge? (useDecide := false) : MetaM Simp.Discharge :=
   return discharge? (← getLCtx).numIndices useDecide
 
-/-- Return the condition of an `if` expression to case split. -/
-partial def findIfToSplit? (e : Expr) : Option Expr :=
+/-- Return the condition and decidable instance of an `if` expression to case split. -/
+private partial def findIfToSplit? (e : Expr) : Option (Expr × Expr) :=
   if let some iteApp := e.find? fun e => (e.isIte || e.isDIte) && !(e.getArg! 1 5).hasLooseBVars then
     let cond := iteApp.getArg! 1 5
+    let dec := iteApp.getArg! 2 5
     -- Try to find a nested `if` in `cond`
-    findIfToSplit? cond |>.getD cond
+    findIfToSplit? cond |>.getD (cond, dec)
   else
     none
 
 def splitIfAt? (mvarId : MVarId) (e : Expr) (hName? : Option Name) : MetaM (Option (ByCasesSubgoal × ByCasesSubgoal)) := do
   let e ← instantiateMVars e
-  if let some cond := findIfToSplit? e then
+  if let some (cond, decInst) := findIfToSplit? e then
     let hName ← match hName? with
       | none       => mkFreshUserName `h
       | some hName => pure hName
-    trace[Meta.Tactic.splitIf] "splitting on {cond}"
-    return some (←  mvarId.byCases cond hName)
+    trace[Meta.Tactic.splitIf] "splitting on {decInst}"
+    return some (← mvarId.byCasesDec cond decInst hName)
   else
     return none
 

src/lake/Lake/Util/Compare.lean

@@ -51,9 +51,13 @@ instance [EqOfCmpWrt α (fun a => a) cmp] : EqOfCmp α cmp where
 theorem eq_of_compareOfLessAndEq [LT α] [DecidableEq α] {a a' : α}
 [Decidable (a < a')] (h : compareOfLessAndEq a a' = .eq) : a = a' := by
   unfold compareOfLessAndEq at h
-  split at h; case inl => exact False.elim h
-  split at h; case inr => exact False.elim h
-  assumption
+  split at h
+  next =>
+    exact False.elim h
+  next =>
+    split at h
+    next => assumption
+    next => exact False.elim h
 
 theorem compareOfLessAndEq_rfl [LT α] [DecidableEq α] {a : α}
 [Decidable (a < a)] (lt_irrefl : ¬ a < a) : compareOfLessAndEq a a = .eq := by

tests/lean/run/4313.lean

@@ -0,0 +1,27 @@
+example {A B : Prop} {p : Prop} [Decidable p] (h : if p then A else B) :
+   A ∨ B := by
+  split at h
+  · exact .inl h
+  · exact .inr h
+
+example {A B : Type} {p : Prop} [Decidable p] (h : if p then A else B) :
+    Sum A B := by
+  split at h
+  · exact .inl h
+  · exact .inr h
+
+example {A B : Type} (h : match b with | true => A | false => B) :
+    Sum A B := by
+  split at h
+  · exact .inl h
+  · exact .inr h
+
+open Int in
+theorem bmod_add_bmod_congr : Int.bmod (Int.bmod x n + y) n = Int.bmod (x + y) n := by
+  rw [bmod_def x n]
+  split -- `split` now generates the more meaningful `isTrue` and `isFalse` tags.
+  case isTrue p =>
+    simp only [emod_add_bmod_congr]
+  case isFalse p =>
+    rw [Int.sub_eq_add_neg, Int.add_right_comm, ←Int.sub_eq_add_neg]
+    simp