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,13 @@ 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]
+section SimprocHelperLemmas
+set_option simprocs false
+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]
+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]
+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]
+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]
+end SimprocHelperLemmas
 @[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) c 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) c 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/1079.lean.expected.out

@@ -1,16 +1,6 @@
 1079.lean:3:2-6:12: error: alternative 'isFalse' has not been provided
-[Meta.Tactic.simp.discharge] >> discharge?: m = n
-[Meta.Tactic.simp.unify] @eq_self:1000, failed to unify
-      ?a = ?a
-    with
-      m = n
-[Meta.Tactic.simp.unify] Nat.succ.injEq:1000, failed to unify
-      Nat.succ ?n = Nat.succ ?n
-    with
-      m = n
 [Meta.Tactic.simp.rewrite] h:1000, m ==> n
 [Meta.Tactic.simp.rewrite] @eq_self:1000, n = n ==> True
-[Meta.Tactic.simp.rewrite] ↓ @ite_cond_true:1000, if m = n then Ordering.eq else Ordering.gt ==> Ordering.eq
 [Meta.Tactic.simp.unify] @eq_self:1000, failed to unify
       ?a = ?a
     with

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

tests/lean/simpZetaFalse.lean.expected.out

@@ -17,8 +17,7 @@ fun x h =>
             ite_congr (Eq.trans (congrFun (congrArg Eq h) x) (eq_self x)) (fun a => Eq.refl 1) fun a =>
               Eq.refl (y + 1)))
         1))
-    (of_eq_true
-      (Eq.trans (congrFun (congrArg Eq (ite_cond_true 1 (x * x + 1) (of_eq_true (Eq.refl True)))) 1) (eq_self 1)))
+    (of_eq_true (eq_self 1))
 x z : Nat
 h : f (f x) = x
 h' : z = x