feat: replace ite and dite shortcircuit theorems with simproc

Motivation: better `simp` cache behavior. Recall that `simp` cache
uses `dischargeDepth`.

src/Init/SimpLemmas.lean

@@ -10,6 +10,7 @@ import Init.Core
 set_option linter.missingDocs true -- keep it documented
 
 theorem of_eq_true (h : p = True) : p := h ▸ trivial
+theorem of_eq_false (h : p = False) : ¬ p := fun hp => False.elim (h.mp hp)
 
 theorem eq_true (h : p) : p = True :=
   propext ⟨fun _ => trivial, fun _ => h⟩
@@ -84,10 +85,14 @@ theorem dite_congr {_ : Decidable b} [Decidable c]
 @[simp] theorem ite_false (a b : α) : (if False then a else b) = b := rfl
 @[simp] theorem dite_true {α : Sort u} {t : True → α} {e : ¬ True → α} : (dite True t e) = t True.intro := rfl
 @[simp] theorem dite_false {α : Sort u} {t : False → α} {e : ¬ False → α} : (dite False t e) = e not_false := rfl
-@[simp ↓] theorem ite_cond_true {_ : Decidable c} (a b : α) (h : c) : (if c then a else b) = a := by simp [h]
-@[simp ↓] theorem ite_cond_false {_ : Decidable c} (a b : α) (h : ¬ c) : (if c then a else b) = b := by simp [h]
-@[simp ↓] theorem dite_cond_true {α : Sort u} {_ : Decidable c} {t : c → α} {e : ¬ c → α} (h : c) : (dite c t e) = t h := by simp [h]
-@[simp ↓] theorem dite_cond_false {α : Sort u} {_ : Decidable c} {t : c → α} {e : ¬ c → α} (h : ¬ c) : (dite c t e) = e h := by simp [h]
+/- simproc helper theorem -/
+theorem ite_cond_eq_true {α : Sort u} {c : Prop} {_ : Decidable c} (a b : α) (h : c = True) : (if c then a else b) = a := by simp [h]
+/- simproc helper theorem -/
+theorem ite_cond_eq_false {α : Sort u} {c : Prop} {_ : Decidable c} (a b : α) (h : c = False) : (if c then a else b) = b := by simp [h]
+/- simproc helper theorem -/
+theorem dite_cond_eq_true {α : Sort u} {c : Prop} {_ : Decidable c} {t : c → α} {e : ¬ c → α} (h : c = True) : (dite c t e) = t (of_eq_true h) := by simp [h]
+/- simproc helper theorem -/
+theorem dite_cond_eq_false {α : Sort u} {c : Prop} {_ : Decidable c} {t : c → α} {e : ¬ c → α} (h : c = False) : (dite c t e) = e (of_eq_false h) := by simp [h]
 @[simp] theorem ite_self {α : Sort u} {c : Prop} {d : Decidable c} (a : α) : ite c a a = a := by cases d <;> rfl
 @[simp] theorem and_self (p : Prop) : (p ∧ p) = p := propext ⟨(·.1), fun h => ⟨h, h⟩⟩
 @[simp] theorem and_true (p : Prop) : (p ∧ True) = p := propext ⟨(·.1), (⟨·, trivial⟩)⟩

src/Lean/Meta/Tactic/Simp/BuiltinSimprocs.lean

@@ -3,5 +3,6 @@ Copyright (c) 2023 Amazon.com, Inc. or its affiliates. All Rights Reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
+import Lean.Meta.Tactic.Simp.BuiltinSimprocs.Core
 import Lean.Meta.Tactic.Simp.BuiltinSimprocs.Nat
 import Lean.Meta.Tactic.Simp.BuiltinSimprocs.Fin

src/Lean/Meta/Tactic/Simp/BuiltinSimprocs/Core.lean

@@ -0,0 +1,40 @@
+/-
+Copyright (c) 2023 Amazon.com, Inc. or its affiliates. All Rights Reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+-/
+import Lean.Meta.Tactic.Simp.Simproc
+
+open Lean Meta Simp
+
+builtin_simproc ↓ reduceIte (ite _ _ _) := fun e => do
+  unless e.isAppOfArity' ``ite 5 do return none
+  let c := e.getArg! 1
+  let r ← simp c
+  if r.expr.isConstOf ``True then
+    let eNew  := e.getArg! 3
+    let pr    := mkApp (mkAppN (mkConst ``ite_cond_eq_true e.getAppFn.constLevels!) e.getAppArgs) (← r.getProof)
+    return some (.visit { expr := eNew, proof? := pr })
+  if r.expr.isConstOf ``False then
+    let eNew  := e.getArg! 4
+    let pr    := mkApp (mkAppN (mkConst ``ite_cond_eq_false e.getAppFn.constLevels!) e.getAppArgs) (← r.getProof)
+    return some (.visit { expr := eNew, proof? := pr })
+  return none
+
+builtin_simproc ↓ reduceDite (dite _ _ _) := fun e => do
+  unless e.isAppOfArity' ``dite 5 do return none
+  let c := e.getArg! 1
+  let r ← simp c
+  if r.expr.isConstOf ``True then
+    let pr    ← r.getProof
+    let h     := mkApp2 (mkConst ``of_eq_true) e pr
+    let eNew  := mkApp (e.getArg! 3) h |>.headBeta
+    let prNew := mkApp (mkAppN (mkConst ``dite_cond_eq_true e.getAppFn.constLevels!) e.getAppArgs) pr
+    return some (.visit { expr := eNew, proof? := prNew })
+  if r.expr.isConstOf ``False then
+    let pr    ← r.getProof
+    let h     := mkApp2 (mkConst ``of_eq_false) e pr
+    let eNew  := mkApp (e.getArg! 4) h |>.headBeta
+    let prNew := mkApp (mkAppN (mkConst ``dite_cond_eq_false e.getAppFn.constLevels!) e.getAppArgs) pr
+    return some (.visit { expr := eNew, proof? := prNew })
+  return none

tests/lean/run/simpIfPre.lean

@@ -11,6 +11,7 @@ def myid (x : Nat) := 0 + x
 
 @[simp] theorem myid_eq : myid x = x := by simp [myid]
 
+namespace Ex1
 def f (x : Nat) (y z : Nat) : Nat :=
   if myid x = 0 then y else z
 
@@ -21,3 +22,43 @@ def g (x : Nat) : Nat :=
 
 theorem ex (h : a = 1) : g (a+32) = a := by
   simp [g, f, h]
+end Ex1
+
+namespace Ex2
+def f (x : Nat) (y z : Nat) : Nat :=
+  if myid x > 0 then z else y
+
+def g (x : Nat) : Nat :=
+  match x with
+  | 0 => 1
+  | a+1 => f x (g a + 1) (g a)
+
+theorem ex (h : a = 1) : g (a+32) = a := by
+  simp [g, f, h]
+end Ex2
+
+namespace Ex3
+def f (x : Nat) (y z : Nat) : Nat :=
+  if _ : myid x = 0 then y else z
+
+def g (x : Nat) : Nat :=
+  match x with
+  | 0 => 1
+  | a+1 => f x (g a + 1) (g a)
+
+theorem ex (h : a = 1) : g (a+32) = a := by
+  simp [g, f, h]
+end Ex3
+
+namespace Ex4
+def f (x : Nat) (y z : Nat) : Nat :=
+  if _ : myid x > 0 then z else y
+
+def g (x : Nat) : Nat :=
+  match x with
+  | 0 => 1
+  | a+1 => f x (g a + 1) (g a)
+
+theorem ex (h : a = 1) : g (a+32) = a := by
+  simp [g, f, h]
+end Ex4