fix: must not reduce ite in the discriminant of match-expression when reducibility setting is .reducible (#5419)

closes #5388

See updated comment for additional details.

src/Init/GetElem.lean

@@ -156,11 +156,11 @@ theorem getElem?_neg [GetElem? cont idx elem dom] [LawfulGetElem cont idx elem d
 theorem getElem!_pos [GetElem? cont idx elem dom] [LawfulGetElem cont idx elem dom]
     [Inhabited elem] (c : cont) (i : idx) (h : dom c i) [Decidable (dom c i)] :
     c[i]! = c[i]'h := by
-  simp only [getElem!_def, getElem?_def, h]
+  simp [getElem!_def, getElem?_def, h]
 
 theorem getElem!_neg [GetElem? cont idx elem dom] [LawfulGetElem cont idx elem dom]
     [Inhabited elem] (c : cont) (i : idx) (h : ¬dom c i) [Decidable (dom c i)] : c[i]! = default := by
-  simp only [getElem!_def, getElem?_def, h]
+  simp [getElem!_def, getElem?_def, h]
 
 namespace Fin
 

src/Lean/Meta/WHNF.lean

@@ -13,6 +13,7 @@ import Lean.Meta.Offset
 import Lean.Meta.CtorRecognizer
 import Lean.Meta.Match.MatcherInfo
 import Lean.Meta.Match.MatchPatternAttr
+import Lean.Meta.Transform
 
 namespace Lean.Meta
 
@@ -435,33 +436,65 @@ inductive ReduceMatcherResult where
   | notMatcher
   | partialApp
 
+/-!
+The "match" compiler uses dependent if-then-else `dite` and other auxiliary declarations to compile match-expressions such as
+```
+match v with
+| 'a' => 1
+| 'b' => 2
+| _   => 3
+```
+because it is more efficient than using `casesOn` recursors.
+The method `reduceMatcher?` fails if these auxiliary definitions cannot be unfolded in the current
+transparency setting. This is problematic because tactics such as `simp` use `TransparencyMode.reducible`, and
+most users assume that expressions such as
+```
+match 0 with
+| 0 => 1
+| 100 => 2
+| _ => 3
+```
+should reduce in any transparency mode.
+
+Thus, if the transparency mode is `.reducible` or `.instances`, we first
+eagerly unfold `dite` constants used in the auxiliary match-declaration, and then
+use a custom `canUnfoldAtMatcher` predicate for `whnfMatcher`.
+
+Remark: we used to include `dite` (and `ite`) as auxiliary declarations to unfold at
+`canUnfoldAtMatcher`, but this is problematic because the `dite`/`ite` may occur in the
+discriminant. See issue #5388.
+
+This solution is not very modular because modifications at the `match` compiler require changes here.
+We claim this is defensible because it is reducing the auxiliary declaration defined by the `match` compiler.
+
+Remark: if the eager unfolding is problematic, we may cache the result.
+We may also consider not using `dite` in the `match`-compiler and use `Decidable.casesOn`, but it will require changes
+in how we generate equation lemmas.
+
+Alternative solution: tactics that use `TransparencyMode.reducible` should rely on the equations we generated for match-expressions.
+This solution is also not perfect because the match-expression above will not reduce during type checking when we are not using
+`TransparencyMode.default` or `TransparencyMode.all`.
+-/
+
 /--
-  The "match" compiler uses `if-then-else` expressions and other auxiliary declarations to compile match-expressions such as
-  ```
-  match v with
-  | 'a' => 1
-  | 'b' => 2
-  | _   => 3
-  ```
-  because it is more efficient than using `casesOn` recursors.
-  The method `reduceMatcher?` fails if these auxiliary definitions (e.g., `ite`) cannot be unfolded in the current
-  transparency setting. This is problematic because tactics such as `simp` use `TransparencyMode.reducible`, and
-  most users assume that expressions such as
-  ```
-  match 0 with
-  | 0 => 1
-  | 100 => 2
-  | _ => 3
-  ```
-  should reduce in any transparency mode.
-  Thus, we define a custom `canUnfoldAtMatcher` predicate for `whnfMatcher`.
+Eagerly unfold `dite` constants in `e`. This is an auxiliary function used to reduce match expressions.
+See comment above.
+-/
+private def unfoldNestedDIte (e : Expr) : CoreM Expr := do
+  if e.find? (fun e => e.isAppOf ``dite) matches some _ then
+    Core.transform e fun e => do
+      if let .const ``dite us := e then
+        let constInfo ← getConstInfo ``dite
+        let e ← instantiateValueLevelParams constInfo us
+        return .done e
+      else
+        return .continue
+  else
+    return e
 
-  This solution is not very modular because modifications at the `match` compiler require changes here.
-  We claim this is defensible because it is reducing the auxiliary declaration defined by the `match` compiler.
-
-  Alternative solution: tactics that use `TransparencyMode.reducible` should rely on the equations we generated for match-expressions.
-  This solution is also not perfect because the match-expression above will not reduce during type checking when we are not using
-  `TransparencyMode.default` or `TransparencyMode.all`.
+/--
+Auxiliary predicate for `whnfMatcher`.
+See comment above.
 -/
 def canUnfoldAtMatcher (cfg : Config) (info : ConstantInfo) : CoreM Bool := do
   match cfg.transparency with
@@ -473,9 +506,7 @@ def canUnfoldAtMatcher (cfg : Config) (info : ConstantInfo) : CoreM Bool := do
     else if hasMatchPatternAttribute (← getEnv) info.name then
       return true
     else
-      return info.name == ``ite
-       || info.name == ``dite
-       || info.name == ``decEq
+      return info.name == ``decEq
        || info.name == ``Nat.decEq
        || info.name == ``Char.ofNat   || info.name == ``Char.ofNatAux
        || info.name == ``String.decEq || info.name == ``List.hasDecEq
@@ -515,7 +546,9 @@ def reduceMatcher? (e : Expr) : MetaM ReduceMatcherResult := do
   if args.size < prefixSz + info.numAlts then
     return ReduceMatcherResult.partialApp
   let constInfo ← getConstInfo declName
-  let f ← instantiateValueLevelParams constInfo declLevels
+  let mut f ← instantiateValueLevelParams constInfo declLevels
+  if (← getTransparency) matches .instances | .reducible then
+    f ← unfoldNestedDIte f
   let auxApp := mkAppN f args[0:prefixSz]
   let auxAppType ← inferType auxApp
   forallBoundedTelescope auxAppType info.numAlts fun hs _ => do

src/Std/Tactic/BVDecide/LRAT/Internal/Formula/RupAddResult.lean

@@ -920,7 +920,7 @@ theorem confirmRupHint_preserves_invariant_helper {n : Nat} (f : DefaultFormula
             · constructor
               · simp only [l'] at l'_eq_true
                 simp only [hasAssignment, l'_eq_true, ite_true] at h2
-                simp only [hasAssignment, l_eq_false, ↓reduceIte, getElem!, l_eq_i, i_in_bounds,
+                simp only [hasAssignment, l_eq_false, ↓reduceIte, ↓reduceDIte, getElem!, l_eq_i, i_in_bounds,
                   Array.get_eq_getElem, h1, addAssignment, l'_eq_true, hasNeg_addPos, decidableGetElem?, reduceCtorEq] at h
                 exact unassigned_of_has_neither _ h2 h
               · intro k k_ne_j_succ k_ne_zero

tests/lean/run/5388.lean

@@ -0,0 +1,6 @@
+example (k : Prop)  (h : k) [Decidable k] (h' : c = 1) :
+    let ⟨a, _⟩ := if k then (1, 0) else (0, 1)
+    a = c := by
+  simp [h]
+  guard_target =ₛ 1 = c
+  rw [h']

tests/lean/run/bv_math_lit_perf.lean

@@ -21,7 +21,7 @@ def f (x : BitVec 32) : Nat :=
 #guard_msgs(drop all) in
 #print equations f
 
-set_option maxHeartbeats 300
+set_option maxHeartbeats 800
 example : f 500#32 = x := by
   simp [f]
   sorry