chore: fix regression due to changes in previous commits

The example was looping with the new `simp` reduction strategy. Here
is the looping trace.
```
List.reverseAux (List.reverseAux as []) bs
==> rewrite using reverseAux_reverseAux
List.reverseAux [] (List.reverseAux (List.reverseAux as []) bs)
==> unfold reverseAux
List.reverseAux (List.reverseAux as []) bs
==> rewrite using reverseAux_reverseAux
List.reverseAux [] (List.reverseAux (List.reverseAux as []) bs)
==> ...
```

src/Init/Data/List/Basic.lean

@@ -124,7 +124,8 @@ def appendTR (as bs : List α) : List α :=
   induction as with
   | nil  => rfl
   | cons a as ih =>
-    simp [reverseAux, List.append, ih, reverseAux_reverseAux]
+    rw [reverseAux, reverseAux_reverseAux]
+    simp [List.append, ih, reverseAux]
 
 instance : Append (List α) := ⟨List.append⟩
 

src/Init/SimpLemmas.lean

@@ -84,6 +84,10 @@ 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]
 @[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/Expr.lean

@@ -947,6 +947,37 @@ private def getAppRevArgsAux : Expr → Array Expr → Array Expr
   let nargs := e.getAppNumArgs
   withAppAux k e (mkArray nargs dummy) (nargs-1)
 
+/--
+Given `f a_1 ... a_n`, returns `#[a_1, ..., a_n]`.
+Note that `f` may be an application.
+The resulting array has size `n` even if `f.getAppNumArgs < n`.
+-/
+@[inline] def getAppArgsN (e : Expr) (n : Nat) : Array Expr :=
+  let dummy := mkSort levelZero
+  loop n e (mkArray n dummy)
+where
+  loop : Nat → Expr → Array Expr → Array Expr
+    | 0,   _,        as => as
+    | i+1, .app f a, as => loop i f (as.set! i a)
+    | _,   _,        as => as
+
+/--
+Given `e` of the form `f a_1 ... a_n`, return `f`.
+If `n` is greater than the number of arguments, then return `e.getAppFn`.
+-/
+def extractNumArgs (e : Expr) (n : Nat) : Expr :=
+  match n, e with
+  | 0,   _        => e
+  | n+1, .app f _ => extractNumArgs f n
+  | _,   _        => e
+
+/--
+Given `e` of the form `f a_1 ... a_n ... a_m`, return `f a_1 ... a_n`.
+If `n` is greater than the arity, then return `e`.
+-/
+def getAppPrefix (e : Expr) (n : Nat) : Expr :=
+  e.extractNumArgs (e.getAppNumArgs - n)
+
 /-- Given `e = fn a₁ ... aₙ`, runs `f` on `fn` and each of the arguments `aᵢ` and
 makes a new function application with the results. -/
 def traverseApp {M} [Monad M]

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

@@ -192,35 +192,40 @@ private def unfold? (e : Expr) : SimpM (Option Expr) := do
   else
     return none
 
-private partial def reduce (e : Expr) : SimpM Expr := withIncRecDepth do
+private def reduceStep (e : Expr) : SimpM Expr := do
   let cfg := (← read).config
-  if e.getAppFn.isMVar then
-    let e' ← instantiateMVars e
-    if e' != e then
-      return (← reduce e')
+  let f := e.getAppFn
+  if f.isMVar then
+    return (← instantiateMVars e)
   if cfg.beta then
-    let e' := e.headBeta
-    if e' != e then
-      return (← reduce e')
+    if f.isHeadBetaTargetFn false then
+      return f.betaRev e.getAppRevArgs
   -- TODO: eta reduction
   if cfg.proj then
     match (← reduceProjFn? e) with
-    | some e => return (← reduce e)
+    | some e => return e
     | none   => pure ()
   if cfg.iota then
     match (← reduceRecMatcher? e) with
-    | some e => return (← reduce e)
+    | some e => return e
     | none   => pure ()
   if cfg.zeta then
     if let some (args, _, _, v, b) := e.letFunAppArgs? then
-      return (← reduce <| mkAppN (b.instantiate1 v) args)
+      return mkAppN (b.instantiate1 v) args
   match (← unfold? e) with
   | some e' =>
     trace[Meta.Tactic.simp.rewrite] "unfold {mkConst e.getAppFn.constName!}, {e} ==> {e'}"
     recordSimpTheorem (.decl e.getAppFn.constName!)
-    reduce e'
+    return e'
   | none => return e
 
+private partial def reduce (e : Expr) : SimpM Expr := withIncRecDepth do
+  let e' ← reduceStep e
+  if e' == e then
+    return e'
+  else
+    reduce e'
+
 private partial def dsimp (e : Expr) : M Expr := do
   let cfg ← getConfig
   unless cfg.dsimp do
@@ -482,15 +487,25 @@ where
     else
       congrDefault e
 
-  simpApp (e : Expr) : M Result := do
-    let e ← reduce e
-    if !e.isApp then
-      simp e
-    else if isOfNatNatLit e then
-      -- Recall that we expand "orphan" kernel nat literals `n` into `ofNat n`
-      return { expr := e }
+  simpMatch? (e : Expr) : M (Option Result) := do
+    let .const declName _ := e.getAppFn
+      | return none
+    if let some info ← getMatcherInfo? declName then
+      simpMatchDiscrs? simp dsimp info e
     else
-      congr e
+      return none
+
+  simpApp (e : Expr) : M Result := do
+    let e' ← reduceStep e
+    if e' != e then
+      simp e'
+    else if isOfNatNatLit e' then
+      -- Recall that we expand "orphan" kernel nat literals `n` into `ofNat n`
+      return { expr := e' }
+    else if let some r ← simpMatch? e' then
+      simpLoop r
+    else
+      congr e'
 
   simpConst (e : Expr) : M Result :=
     return { expr := (← reduce e) }

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

@@ -190,6 +190,46 @@ The resulting proof is built using `congr` and `congrFun` theorems.
       i := i + 1
     return r
 
+/--
+Given a match-application `e` with `MatcherInfo` `info`, return `some result`
+if at least of one of the discriminants has been simplified.
+-/
+@[specialize] def simpMatchDiscrs?
+    [Monad m] [MonadLiftT MetaM m] [MonadLiftT IO m] [MonadRef m] [MonadOptions m] [MonadTrace m] [AddMessageContext m]
+    (simp : Expr → m Result)
+    (dsimp : Expr → m Expr)
+    (info : MatcherInfo) (e : Expr) : m (Option Result) := do
+  let numArgs := e.getAppNumArgs
+  if numArgs < info.arity then
+    return none
+  let prefixSize := info.numParams + 1 /- motive -/
+  let n     := numArgs - prefixSize
+  let f     := e.extractNumArgs n
+  let infos := (← getFunInfoNArgs f n).paramInfo
+  let args  := e.getAppArgsN n
+  let mut r : Result := { expr := f }
+  let mut modified := false
+  for i in [0 : info.numDiscrs] do
+    let arg := args[i]!
+    if i < infos.size && !infos[i]!.hasFwdDeps then
+      let argNew ← simp arg
+      if argNew.expr != arg then modified := true
+      r ← mkCongr r argNew
+    else if (← whnfD (← inferType r.expr)).isArrow then
+      let argNew ← simp arg
+      if argNew.expr != arg then modified := true
+      r ← mkCongr r argNew
+    else
+      let argNew ← dsimp arg
+      if argNew != arg then modified := true
+      r ← mkCongrFun r argNew
+  unless modified do
+    return none
+  for i in [info.numDiscrs : args.size] do
+    let arg := args[i]!
+    r ← mkCongrFun r arg
+  return some r
+
 /--
 Helper class for generalizing `mkCongrSimp?`
 -/

tests/lean/1079.lean.expected.out

@@ -1,11 +1,16 @@
 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.unify] @ite_self:1000, failed to unify
-      if ?c then ?a else ?a
-    with
-      if True then Ordering.eq else Ordering.gt
-[Meta.Tactic.simp.rewrite] @ite_true:1000, if True then Ordering.eq else Ordering.gt ==> Ordering.eq
+[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

@@ -0,0 +1,23 @@
+/-!
+Test support for `if-then-else` terms in the simplifier.
+The condition should be simplified before trying to apply congruence.
+We are currently accomplished that using pre-simp theorems.
+TODO: replace them with simprocs.
+In the following example, the term `g (a + <num>)` takes an
+exponential amount of time to be simplified without the pre-simp theorems.
+-/
+
+def myid (x : Nat) := 0 + x
+
+@[simp] theorem myid_eq : myid x = x := by simp [myid]
+
+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]

tests/lean/run/simpMatchDiscrIssue.lean

@@ -0,0 +1,24 @@
+/-!
+Test support for `match`-applications in the simplifier.
+The discriminants should be simplified before trying to apply congruence.
+In the following example, the term `g (a + <num>)` takes an
+exponential amount of time to be simplified the discriminants are not simplified,
+and the `match`-application reduced before visiting the alternatives.
+-/
+
+def myid (x : Nat) := 0 + x
+
+@[simp] theorem myid_eq : myid x = x := by simp [myid]
+
+def f (x : Nat) (y z : Nat) : Nat :=
+  match myid x with
+  | 0   => y
+  | _+1 => 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+64) = a := by
+  simp [g, f, h]

tests/lean/run/simpPreIssue.lean

@@ -0,0 +1,37 @@
+/-!
+Test a simplifier issue. `simpApp` first tries to `reduce` the term. If the
+term is reduce, pre-simp rules should be tried again before trying to use
+congruence. In the following example, the term `g (a + <num>)` takes an
+exponential amount of time to be simplified when the pre-simp rules are not
+tried before applying congruence.
+-/
+
+def myid (x : Nat) := 0 + x
+
+@[simp] theorem myid_eq : myid x = x := by simp [myid]
+
+def myif (c : Prop) [Decidable c] (a b : α) : α :=
+  if c then a else b
+
+@[simp ↓] theorem myif_cond_true (c : Prop) {_ : Decidable c} (a b : α) (h : c) : (myif c a b) = a := by
+  simp [myif, h]
+
+@[simp ↓] theorem myif_cond_false (c : Prop) {_ : Decidable c} (a b : α) (h : Not c) : (myif c a b) = b := by
+  simp [myif, h]
+
+@[congr] theorem myif_congr {x y u v : α} {s : Decidable b} [Decidable c]
+    (h₁ : b = c) (h₂ : c → x = u) (h₃ : ¬ c → y = v) : myif b x y = myif c u v := by
+  unfold myif
+  apply @ite_congr <;> assumption
+
+def f (x : Nat) (y z : Nat) : Nat :=
+  myif (myid x = 0) y z
+
+def g (x : Nat) : Nat :=
+  match x with
+  | 0 => 1
+  | a+1 => f x (g a + 1) (g a)
+
+-- `simp` should not be exponential on `g (a + <num>)`
+theorem ex (h : a = 1) : g (a+32) = a := by
+  simp [g, f, h]

tests/lean/simpZetaFalse.lean.expected.out

@@ -17,7 +17,8 @@ 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_self 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)))
 x z : Nat
 h : f (f x) = x
 h' : z = x

tests/lean/simp_trace.lean.expected.out

@@ -34,7 +34,7 @@ Try this: simp (config := { unfoldPartialApp := true }) only [f1, modify, modify
         | (a, s) => (fun s => set (g s)) a s
 [Meta.Tactic.simp.rewrite] unfold getThe, getThe Nat s ==> MonadStateOf.get s
 [Meta.Tactic.simp.rewrite] unfold StateT.get, StateT.get s ==> pure (s, s)
-[Meta.Tactic.simp.rewrite] unfold StateT.set, StateT.set (g a) s ==> pure (PUnit.unit, g a)
+[Meta.Tactic.simp.rewrite] unfold StateT.set, StateT.set (g s) s ==> pure (PUnit.unit, g s)
 [Meta.Tactic.simp.rewrite] @eq_self:1000, (fun s => (PUnit.unit, g s)) = fun s => (PUnit.unit, g s) ==> True
 Try this: simp only [bla, h]
 [Meta.Tactic.simp.rewrite] unfold bla, bla x ==> match h x with