chore: address feedback

Motivations:
- We can simplify the big mutual recursion and the implementation.
- We can implement the support for `match`-expressions in the `pre` method.
- It is easier to define and simplify `Simprocs`.

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/Elab/PreDefinition/WF/Eqns.lean

@@ -122,7 +122,7 @@ where
     match (← reduceRecMatcher? e) with
     | some e' => return Simp.Step.done { expr := e' }
     | none    =>
-      match (← Simp.simpMatchCore? app e SplitIf.discharge?) with
+      match (← Simp.simpMatchCore? app.matcherName e SplitIf.discharge?) with
       | some r => return r
       | none => return Simp.Step.visit { expr := e }
 

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)
+    | _,   _,        _  => panic! "too few arguments at"
+
+/--
+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 stripArgsN (e : Expr) (n : Nat) : Expr :=
+  match n, e with
+  | 0,   _        => e
+  | n+1, .app f _ => stripArgsN 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.stripArgsN (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/AC/Main.lean

@@ -150,7 +150,7 @@ def rewriteUnnormalized (mvarId : MVarId) : MetaM Unit := do
   newGoal.refl
 where
   post (e : Expr) : SimpM Simp.Step := do
-    let ctx ← read
+    let ctx ← Simp.getContext
     match e, ctx.parent? with
     | bin op₁ l r, some (bin op₂ _ _) =>
       if ←isDefEq op₁ op₂ then

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

@@ -54,7 +54,7 @@ private def reduceProjFn? (e : Expr) : SimpM (Option Expr) := do
           | none   => return none
       if projInfo.fromClass then
         -- `class` projection
-        if (← read).isDeclToUnfold cinfo.name then
+        if (← getContext).isDeclToUnfold cinfo.name then
           /-
           If user requested `class` projection to be unfolded, we set transparency mode to `.instances`,
           and invoke `unfoldDefinition?`.
@@ -123,7 +123,7 @@ private def unfold? (e : Expr) : SimpM (Option Expr) := do
   if !f.isConst then
     return none
   let fName := f.constName!
-  let ctx ← read
+  let ctx ← getContext
   -- TODO: remove `rec` after we switch to new code generator
   let rec unfoldGround? : SimpM (Option Expr) := do
       unless ctx.config.ground do return none
@@ -192,61 +192,47 @@ private def unfold? (e : Expr) : SimpM (Option Expr) := do
   else
     return none
 
-private partial def reduce (e : Expr) : SimpM Expr := withIncRecDepth do
-  let cfg := (← read).config
-  if e.getAppFn.isMVar then
-    let e' ← instantiateMVars e
-    if e' != e then
-      return (← reduce e')
+private def reduceStep (e : Expr) : SimpM Expr := do
+  let cfg ← getConfig
+  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 dsimp (e : Expr) : M Expr := do
-  let cfg ← getConfig
-  unless cfg.dsimp do
-    return e
-  let pre (e : Expr) : M TransformStep := do
-    if let Step.visit r ← rewritePre e (fun _ => pure none) (rflOnly := true) then
-      if r.expr != e then
-        return .visit r.expr
-    return .continue
-  let post (e : Expr) : M TransformStep := do
-    if let Step.visit r ← rewritePost e (fun _ => pure none) (rflOnly := true) then
-      if r.expr != e then
-        return .visit r.expr
-    let mut eNew ← reduce e
-    if eNew.isFVar then
-      eNew ← reduceFVar cfg (← getSimpTheorems) eNew
-    if eNew != e then return .visit eNew else return .done e
-  transform (usedLetOnly := cfg.zeta) e (pre := pre) (post := post)
+private partial def reduce (e : Expr) : SimpM Expr := withIncRecDepth do
+  let e' ← reduceStep e
+  if e' == e then
+    return e'
+  else
+    reduce e'
 
-instance : Inhabited (M α) where
+instance : Inhabited (SimpM α) where
   default := fun _ _ _ => default
 
-partial def lambdaTelescopeDSimp (e : Expr) (k : Array Expr → Expr → M α) : M α := do
+partial def lambdaTelescopeDSimp (e : Expr) (k : Array Expr → Expr → SimpM α) : SimpM α := do
   go #[] e
 where
-  go (xs : Array Expr) (e : Expr) : M α := do
+  go (xs : Array Expr) (e : Expr) : SimpM α := do
     match e with
     | .lam n d b c => withLocalDecl n c (← dsimp d) fun x => go (xs.push x) (b.instantiate1 x)
     | e => k xs e
@@ -270,7 +256,377 @@ def getSimpLetCase (n : Name) (t : Expr) (b : Expr) : MetaM SimpLetCase := do
     else
       return SimpLetCase.dep
 
-partial def simp (e : Expr) : M Result := withIncRecDepth do
+def withNewLemmas {α} (xs : Array Expr) (f : SimpM α) : SimpM α := do
+  if (← getConfig).contextual then
+    let mut s ← getSimpTheorems
+    let mut updated := false
+    for x in xs do
+      if (← isProof x) then
+        s ← s.addTheorem (.fvar x.fvarId!) x
+        updated := true
+    if updated then
+      withSimpTheorems s f
+    else
+      f
+  else
+    f
+
+def simpLit (e : Expr) : SimpM Result := do
+  match e.natLit? with
+  | some n =>
+    /- If `OfNat.ofNat` is marked to be unfolded, we do not pack orphan nat literals as `OfNat.ofNat` applications
+        to avoid non-termination. See issue #788.  -/
+    if (← readThe Simp.Context).isDeclToUnfold ``OfNat.ofNat then
+      return { expr := e }
+    else
+      return { expr := (← mkNumeral (mkConst ``Nat) n) }
+  | none   => return { expr := e }
+
+def simpProj (e : Expr) : SimpM Result := do
+  match (← reduceProj? e) with
+  | some e => return { expr := e }
+  | none =>
+    let s := e.projExpr!
+    let motive? ← withLocalDeclD `s (← inferType s) fun s => do
+      let p := e.updateProj! s
+      if (← dependsOn (← inferType p) s.fvarId!) then
+        return none
+      else
+        let motive ← mkLambdaFVars #[s] (← mkEq e p)
+        if !(← isTypeCorrect motive) then
+          return none
+        else
+          return some motive
+    if let some motive := motive? then
+      let r ← simp s
+      let eNew := e.updateProj! r.expr
+      match r.proof? with
+      | none => return { expr := eNew }
+      | some h =>
+        let hNew ← mkEqNDRec motive (← mkEqRefl e) h
+        return { expr := eNew, proof? := some hNew }
+    else
+      return { expr := (← dsimp e) }
+
+def simpConst (e : Expr) : SimpM Result :=
+  return { expr := (← reduce e) }
+
+def simpLambda (e : Expr) : SimpM Result :=
+  withParent e <| lambdaTelescopeDSimp e fun xs e => withNewLemmas xs do
+    let r ← simp e
+    let eNew ← mkLambdaFVars xs r.expr
+    match r.proof? with
+    | none   => return { expr := eNew }
+    | some h =>
+      let p ← xs.foldrM (init := h) fun x h => do
+        mkFunExt (← mkLambdaFVars #[x] h)
+      return { expr := eNew, proof? := p }
+
+def simpArrow (e : Expr) : SimpM Result := do
+  trace[Debug.Meta.Tactic.simp] "arrow {e}"
+  let p := e.bindingDomain!
+  let q := e.bindingBody!
+  let rp ← simp p
+  trace[Debug.Meta.Tactic.simp] "arrow [{(← getConfig).contextual}] {p} [{← isProp p}] -> {q} [{← isProp q}]"
+  if (← pure (← getConfig).contextual <&&> isProp p <&&> isProp q) then
+    trace[Debug.Meta.Tactic.simp] "ctx arrow {rp.expr} -> {q}"
+    withLocalDeclD e.bindingName! rp.expr fun h => do
+      let s ← getSimpTheorems
+      let s ← s.addTheorem (.fvar h.fvarId!) h
+      withSimpTheorems s do
+        let rq ← simp q
+        match rq.proof? with
+        | none    => mkImpCongr e rp rq
+        | some hq =>
+          let hq ← mkLambdaFVars #[h] hq
+          /-
+            We use the default reducibility setting at `mkImpDepCongrCtx` and `mkImpCongrCtx` because they use the theorems
+            ```lean
+            @implies_dep_congr_ctx : ∀ {p₁ p₂ q₁ : Prop}, p₁ = p₂ → ∀ {q₂ : p₂ → Prop}, (∀ (h : p₂), q₁ = q₂ h) → (p₁ → q₁) = ∀ (h : p₂), q₂ h
+            @implies_congr_ctx : ∀ {p₁ p₂ q₁ q₂ : Prop}, p₁ = p₂ → (p₂ → q₁ = q₂) → (p₁ → q₁) = (p₂ → q₂)
+            ```
+            And the proofs may be from `rfl` theorems which are now omitted. Moreover, we cannot establish that the two
+            terms are definitionally equal using `withReducible`.
+            TODO (better solution): provide the problematic implicit arguments explicitly. It is more efficient and avoids this
+            problem.
+            -/
+          if rq.expr.containsFVar h.fvarId! then
+            return { expr := (← mkForallFVars #[h] rq.expr), proof? := (← withDefault <| mkImpDepCongrCtx (← rp.getProof) hq) }
+          else
+            return { expr := e.updateForallE! rp.expr rq.expr, proof? := (← withDefault <| mkImpCongrCtx (← rp.getProof) hq) }
+  else
+    mkImpCongr e rp (← simp q)
+
+def simpForall (e : Expr) : SimpM Result := withParent e do
+  trace[Debug.Meta.Tactic.simp] "forall {e}"
+  if e.isArrow then
+    simpArrow e
+  else if (← isProp e) then
+    /- The forall is a proposition. -/
+    let domain := e.bindingDomain!
+    if (← isProp domain) then
+      /-
+      The domain of the forall is also a proposition, and we can use `forall_prop_domain_congr`
+      IF we can simplify the domain.
+      -/
+      let rd ← simp domain
+      if let some h₁ := rd.proof? then
+        /- Using
+        ```
+        theorem forall_prop_domain_congr {p₁ p₂ : Prop} {q₁ : p₁ → Prop} {q₂ : p₂ → Prop}
+            (h₁ : p₁ = p₂)
+            (h₂ : ∀ a : p₂, q₁ (h₁.substr a) = q₂ a)
+            : (∀ a : p₁, q₁ a) = (∀ a : p₂, q₂ a)
+        ```
+        Remark: we should consider whether we want to add congruence lemma support for arbitrary `forall`-expressions.
+        Then, the theroem above can be marked as `@[congr]` and the following code deleted.
+        -/
+        let p₁ := domain
+        let p₂ := rd.expr
+        let q₁ := mkLambda e.bindingName! e.bindingInfo! p₁ e.bindingBody!
+        let result ← withLocalDecl e.bindingName! e.bindingInfo! p₂ fun a => withNewLemmas #[a] do
+          let prop := mkSort levelZero
+          let h₁_substr_a := mkApp6 (mkConst ``Eq.substr [levelOne]) prop (mkLambda `x .default prop (mkBVar 0)) p₂ p₁ h₁ a
+          let q_h₁_substr_a := e.bindingBody!.instantiate1 h₁_substr_a
+          let rb ← simp q_h₁_substr_a
+          let h₂ ← mkLambdaFVars #[a] (← rb.getProof)
+          let q₂ ← mkLambdaFVars #[a] rb.expr
+          let result ← mkForallFVars #[a] rb.expr
+          let proof := mkApp6 (mkConst ``forall_prop_domain_congr) p₁ p₂ q₁ q₂ h₁ h₂
+          return { expr := result, proof? := proof }
+        return result
+    let domain ← dsimp domain
+    withLocalDecl e.bindingName! e.bindingInfo! domain fun x => withNewLemmas #[x] do
+      let b := e.bindingBody!.instantiate1 x
+      let rb ← simp b
+      let eNew ← mkForallFVars #[x] rb.expr
+      match rb.proof? with
+      | none   => return { expr := eNew }
+      | some h => return { expr := eNew, proof? := (← mkForallCongr (← mkLambdaFVars #[x] h)) }
+  else
+    return { expr := (← dsimp e) }
+
+def simpLet (e : Expr) : SimpM Result := do
+  let .letE n t v b _ := e | unreachable!
+  if (← getConfig).zeta then
+    return { expr := b.instantiate1 v }
+  else
+    match (← getSimpLetCase n t b) with
+    | SimpLetCase.dep => return { expr := (← dsimp e) }
+    | SimpLetCase.nondep =>
+      let rv ← simp v
+      withLocalDeclD n t fun x => do
+        let bx := b.instantiate1 x
+        let rbx ← simp bx
+        let hb? ← match rbx.proof? with
+          | none => pure none
+          | some h => pure (some (← mkLambdaFVars #[x] h))
+        let e' := mkLet n t rv.expr (← rbx.expr.abstractM #[x])
+        match rv.proof?, hb? with
+        | none,   none   => return { expr := e' }
+        | some h, none   => return { expr := e', proof? := some (← mkLetValCongr (← mkLambdaFVars #[x] rbx.expr) h) }
+        | _,      some h => return { expr := e', proof? := some (← mkLetCongr (← rv.getProof) h) }
+    | SimpLetCase.nondepDepVar =>
+      let v' ← dsimp v
+      withLocalDeclD n t fun x => do
+        let bx := b.instantiate1 x
+        let rbx ← simp bx
+        let e' := mkLet n t v' (← rbx.expr.abstractM #[x])
+        match rbx.proof? with
+        | none => return { expr := e' }
+        | some h =>
+          let h ← mkLambdaFVars #[x] h
+          return { expr := e', proof? := some (← mkLetBodyCongr v' h) }
+
+@[export lean_dsimp]
+private partial def dsimpImpl (e : Expr) : SimpM Expr := do
+  let cfg ← getConfig
+  unless cfg.dsimp do
+    return e
+  let pre (e : Expr) : SimpM TransformStep := do
+    if let Step.visit r ← rewritePre e (fun _ => pure none) (rflOnly := true) then
+      if r.expr != e then
+        return .visit r.expr
+    return .continue
+  let post (e : Expr) : SimpM TransformStep := do
+    if let Step.visit r ← rewritePost e (fun _ => pure none) (rflOnly := true) then
+      if r.expr != e then
+        return .visit r.expr
+    let mut eNew ← reduce e
+    if eNew.isFVar then
+      eNew ← reduceFVar cfg (← getSimpTheorems) eNew
+    if eNew != e then return .visit eNew else return .done e
+  transform (usedLetOnly := cfg.zeta) e (pre := pre) (post := post)
+
+def visitFn (e : Expr) : SimpM Result := do
+  let f := e.getAppFn
+  let fNew ← simp f
+  if fNew.expr == f then
+    return { expr := e }
+  else
+    let args := e.getAppArgs
+    let eNew := mkAppN fNew.expr args
+    if fNew.proof?.isNone then return { expr := eNew }
+    let mut proof ← fNew.getProof
+    for arg in args do
+      proof ← Meta.mkCongrFun proof arg
+    return { expr := eNew, proof? := proof }
+
+def congrDefault (e : Expr) : SimpM Result := do
+  if let some result ← tryAutoCongrTheorem? e then
+    mkEqTrans result (← visitFn result.expr)
+  else
+    withParent e <| e.withApp fun f args => do
+      congrArgs (← simp f) args
+
+/-- Process the given congruence theorem hypothesis. Return true if it made "progress". -/
+def processCongrHypothesis (h : Expr) : SimpM Bool := do
+  forallTelescopeReducing (← inferType h) fun xs hType => withNewLemmas xs do
+    let lhs ← instantiateMVars hType.appFn!.appArg!
+    let r ← simp lhs
+    let rhs := hType.appArg!
+    rhs.withApp fun m zs => do
+      let val ← mkLambdaFVars zs r.expr
+      unless (← isDefEq m val) do
+        throwCongrHypothesisFailed
+      let mut proof ← r.getProof
+      if hType.isAppOf ``Iff then
+        try proof ← mkIffOfEq proof
+        catch _ => throwCongrHypothesisFailed
+      unless (← isDefEq h (← mkLambdaFVars xs proof)) do
+        throwCongrHypothesisFailed
+      /- We used to return `false` if `r.proof? = none` (i.e., an implicit `rfl` proof) because we
+          assumed `dsimp` would also be able to simplify the term, but this is not true
+          for non-trivial user-provided theorems.
+          Example:
+          ```
+          @[congr] theorem image_congr {f g : α → β} {s : Set α} (h : ∀ a, mem a s → f a = g a) : image f s = image g s :=
+          ...
+
+          example {Γ: Set Nat}: (image (Nat.succ ∘ Nat.succ) Γ) = (image (fun a => a.succ.succ) Γ) := by
+            simp only [Function.comp_apply]
+          ```
+          `Function.comp_apply` is a `rfl` theorem, but `dsimp` will not apply it because the composition
+          is not fully applied. See comment at issue #1113
+
+          Thus, we have an extra check now if `xs.size > 0`. TODO: refine this test.
+      -/
+      return r.proof?.isSome || (xs.size > 0 && lhs != r.expr)
+
+/-- Try to rewrite `e` children using the given congruence theorem -/
+def trySimpCongrTheorem? (c : SimpCongrTheorem) (e : Expr) : SimpM (Option Result) := withNewMCtxDepth do
+  trace[Debug.Meta.Tactic.simp.congr] "{c.theoremName}, {e}"
+  let thm ← mkConstWithFreshMVarLevels c.theoremName
+  let (xs, bis, type) ← forallMetaTelescopeReducing (← inferType thm)
+  if c.hypothesesPos.any (· ≥ xs.size) then
+    return none
+  let isIff := type.isAppOf ``Iff
+  let lhs := type.appFn!.appArg!
+  let rhs := type.appArg!
+  let numArgs := lhs.getAppNumArgs
+  let mut e := e
+  let mut extraArgs := #[]
+  if e.getAppNumArgs > numArgs then
+    let args := e.getAppArgs
+    e := mkAppN e.getAppFn args[:numArgs]
+    extraArgs := args[numArgs:].toArray
+  if (← isDefEq lhs e) then
+    let mut modified := false
+    for i in c.hypothesesPos do
+      let x := xs[i]!
+      try
+        if (← processCongrHypothesis x) then
+          modified := true
+      catch _ =>
+        trace[Meta.Tactic.simp.congr] "processCongrHypothesis {c.theoremName} failed {← inferType x}"
+        -- Remark: we don't need to check ex.isMaxRecDepth anymore since `try .. catch ..`
+        -- does not catch runtime exceptions by default.
+        return none
+    unless modified do
+      trace[Meta.Tactic.simp.congr] "{c.theoremName} not modified"
+      return none
+    unless (← synthesizeArgs (.decl c.theoremName) xs bis discharge?) do
+      trace[Meta.Tactic.simp.congr] "{c.theoremName} synthesizeArgs failed"
+      return none
+    let eNew ← instantiateMVars rhs
+    let mut proof ← instantiateMVars (mkAppN thm xs)
+    if isIff then
+      try proof ← mkAppM ``propext #[proof]
+      catch _ => return none
+    if (← hasAssignableMVar proof <||> hasAssignableMVar eNew) then
+      trace[Meta.Tactic.simp.congr] "{c.theoremName} has unassigned metavariables"
+      return none
+    congrArgs { expr := eNew, proof? := proof } extraArgs
+  else
+    return none
+
+def congr (e : Expr) : SimpM Result := do
+  let f := e.getAppFn
+  if f.isConst then
+    let congrThms ← getSimpCongrTheorems
+    let cs := congrThms.get f.constName!
+    for c in cs do
+      match (← trySimpCongrTheorem? c e) with
+      | none   => pure ()
+      | some r => return r
+    congrDefault e
+  else
+    congrDefault e
+
+def simpApp (e : Expr) : SimpM 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
+    congr e'
+
+def simpStep (e : Expr) : SimpM Result := do
+  match e with
+  | .mdata m e   => let r ← simp e; return { r with expr := mkMData m r.expr }
+  | .proj ..     => simpProj e
+  | .app ..      => simpApp e
+  | .lam ..      => simpLambda e
+  | .forallE ..  => simpForall e
+  | .letE ..     => simpLet e
+  | .const ..    => simpConst e
+  | .bvar ..     => unreachable!
+  | .sort ..     => return { expr := e }
+  | .lit ..      => simpLit e
+  | .mvar ..     => return { expr := (← instantiateMVars e) }
+  | .fvar ..     => return { expr := (← reduceFVar (← getConfig) (← getSimpTheorems) e) }
+
+def cacheResult (e : Expr) (cfg : Config) (r : Result) : SimpM Result := do
+  if cfg.memoize then
+    let dischargeDepth := (← readThe Simp.Context).dischargeDepth
+    modify fun s => { s with cache := s.cache.insert e { r with dischargeDepth } }
+  return r
+
+partial def simpLoop (e : Expr) (r : Result) : SimpM Result := do
+  let cfg ← getConfig
+  if (← get).numSteps > cfg.maxSteps then
+    throwError "simp failed, maximum number of steps exceeded"
+  else
+    let init := r.expr
+    modify fun s => { s with numSteps := s.numSteps + 1 }
+    match (← pre r.expr) with
+    | Step.done r'  => cacheResult e cfg (← mkEqTrans r r')
+    | Step.visit r' =>
+      let r ← mkEqTrans r r'
+      let r ← mkEqTrans r (← simpStep r.expr)
+      match (← post r.expr) with
+      | Step.done r'  => cacheResult e cfg (← mkEqTrans r r')
+      | Step.visit r' =>
+        let r ← mkEqTrans r r'
+        if cfg.singlePass || init == r.expr then
+          cacheResult e cfg r
+        else
+          simpLoop e r
+
+@[export lean_simp]
+def simpImpl (e : Expr) : SimpM Result := withIncRecDepth do
   checkSystem "simp"
   let cfg ← getConfig
   if (← isProof e) then
@@ -284,364 +640,7 @@ partial def simp (e : Expr) : M Result := withIncRecDepth do
       if result.dischargeDepth ≤ (← readThe Simp.Context).dischargeDepth then
         return result
   trace[Meta.Tactic.simp.heads] "{repr e.toHeadIndex}"
-  simpLoop { expr := e }
-
-where
-  simpLoop (r : Result) : M Result := do
-    let cfg ← getConfig
-    if (← get).numSteps > cfg.maxSteps then
-      throwError "simp failed, maximum number of steps exceeded"
-    else
-      let init := r.expr
-      modify fun s => { s with numSteps := s.numSteps + 1 }
-      match (← pre r.expr) with
-      | Step.done r'  => cacheResult cfg (← mkEqTrans r r')
-      | Step.visit r' =>
-        let r ← mkEqTrans r r'
-        let r ← mkEqTrans r (← simpStep r.expr)
-        match (← post r.expr) with
-        | Step.done r'  => cacheResult cfg (← mkEqTrans r r')
-        | Step.visit r' =>
-          let r ← mkEqTrans r r'
-          if cfg.singlePass || init == r.expr then
-            cacheResult cfg r
-          else
-            simpLoop r
-
-  simpStep (e : Expr) : M Result := do
-    match e with
-    | .mdata m e   => let r ← simp e; return { r with expr := mkMData m r.expr }
-    | .proj ..     => simpProj e
-    | .app ..      => simpApp e
-    | .lam ..      => simpLambda e
-    | .forallE ..  => simpForall e
-    | .letE ..     => simpLet e
-    | .const ..    => simpConst e
-    | .bvar ..     => unreachable!
-    | .sort ..     => return { expr := e }
-    | .lit ..      => simpLit e
-    | .mvar ..     => return { expr := (← instantiateMVars e) }
-    | .fvar ..     => return { expr := (← reduceFVar (← getConfig) (← getSimpTheorems) e) }
-
-  simpLit (e : Expr) : M Result := do
-    match e.natLit? with
-    | some n =>
-      /- If `OfNat.ofNat` is marked to be unfolded, we do not pack orphan nat literals as `OfNat.ofNat` applications
-         to avoid non-termination. See issue #788.  -/
-      if (← readThe Simp.Context).isDeclToUnfold ``OfNat.ofNat then
-        return { expr := e }
-      else
-        return { expr := (← mkNumeral (mkConst ``Nat) n) }
-    | none   => return { expr := e }
-
-  simpProj (e : Expr) : M Result := do
-    match (← reduceProj? e) with
-    | some e => return { expr := e }
-    | none =>
-      let s := e.projExpr!
-      let motive? ← withLocalDeclD `s (← inferType s) fun s => do
-        let p := e.updateProj! s
-        if (← dependsOn (← inferType p) s.fvarId!) then
-          return none
-        else
-          let motive ← mkLambdaFVars #[s] (← mkEq e p)
-          if !(← isTypeCorrect motive) then
-            return none
-          else
-            return some motive
-      if let some motive := motive? then
-        let r ← simp s
-        let eNew := e.updateProj! r.expr
-        match r.proof? with
-        | none => return { expr := eNew }
-        | some h =>
-          let hNew ← mkEqNDRec motive (← mkEqRefl e) h
-          return { expr := eNew, proof? := some hNew }
-      else
-        return { expr := (← dsimp e) }
-
-  congrArgs (r : Result) (args : Array Expr) : M Result := do
-    Simp.congrArgs simp dsimp r args
-
-  visitFn (e : Expr) : M Result := do
-    let f := e.getAppFn
-    let fNew ← simp f
-    if fNew.expr == f then
-      return { expr := e }
-    else
-      let args := e.getAppArgs
-      let eNew := mkAppN fNew.expr args
-      if fNew.proof?.isNone then return { expr := eNew }
-      let mut proof ← fNew.getProof
-      for arg in args do
-        proof ← Meta.mkCongrFun proof arg
-      return { expr := eNew, proof? := proof }
-
-  /-- Try to use automatically generated congruence theorems. See `mkCongrSimp?`. -/
-  tryAutoCongrTheorem? (e : Expr) : M (Option Result) := do
-    Simp.tryAutoCongrTheorem? simp dsimp e
-
-  congrDefault (e : Expr) : M Result := do
-    if let some result ← tryAutoCongrTheorem? e then
-      mkEqTrans result (← visitFn result.expr)
-    else
-      withParent e <| e.withApp fun f args => do
-        congrArgs (← simp f) args
-
-  /-- Process the given congruence theorem hypothesis. Return true if it made "progress". -/
-  processCongrHypothesis (h : Expr) : M Bool := do
-    forallTelescopeReducing (← inferType h) fun xs hType => withNewLemmas xs do
-      let lhs ← instantiateMVars hType.appFn!.appArg!
-      let r ← simp lhs
-      let rhs := hType.appArg!
-      rhs.withApp fun m zs => do
-        let val ← mkLambdaFVars zs r.expr
-        unless (← isDefEq m val) do
-          throwCongrHypothesisFailed
-        let mut proof ← r.getProof
-        if hType.isAppOf ``Iff then
-          try proof ← mkIffOfEq proof
-          catch _ => throwCongrHypothesisFailed
-        unless (← isDefEq h (← mkLambdaFVars xs proof)) do
-          throwCongrHypothesisFailed
-        /- We used to return `false` if `r.proof? = none` (i.e., an implicit `rfl` proof) because we
-           assumed `dsimp` would also be able to simplify the term, but this is not true
-           for non-trivial user-provided theorems.
-           Example:
-           ```
-           @[congr] theorem image_congr {f g : α → β} {s : Set α} (h : ∀ a, mem a s → f a = g a) : image f s = image g s :=
-           ...
-
-           example {Γ: Set Nat}: (image (Nat.succ ∘ Nat.succ) Γ) = (image (fun a => a.succ.succ) Γ) := by
-             simp only [Function.comp_apply]
-           ```
-           `Function.comp_apply` is a `rfl` theorem, but `dsimp` will not apply it because the composition
-           is not fully applied. See comment at issue #1113
-
-           Thus, we have an extra check now if `xs.size > 0`. TODO: refine this test.
-        -/
-        return r.proof?.isSome || (xs.size > 0 && lhs != r.expr)
-
-  /-- Try to rewrite `e` children using the given congruence theorem -/
-  trySimpCongrTheorem? (c : SimpCongrTheorem) (e : Expr) : M (Option Result) := withNewMCtxDepth do
-    trace[Debug.Meta.Tactic.simp.congr] "{c.theoremName}, {e}"
-    let thm ← mkConstWithFreshMVarLevels c.theoremName
-    let (xs, bis, type) ← forallMetaTelescopeReducing (← inferType thm)
-    if c.hypothesesPos.any (· ≥ xs.size) then
-      return none
-    let isIff := type.isAppOf ``Iff
-    let lhs := type.appFn!.appArg!
-    let rhs := type.appArg!
-    let numArgs := lhs.getAppNumArgs
-    let mut e := e
-    let mut extraArgs := #[]
-    if e.getAppNumArgs > numArgs then
-      let args := e.getAppArgs
-      e := mkAppN e.getAppFn args[:numArgs]
-      extraArgs := args[numArgs:].toArray
-    if (← isDefEq lhs e) then
-      let mut modified := false
-      for i in c.hypothesesPos do
-        let x := xs[i]!
-        try
-          if (← processCongrHypothesis x) then
-            modified := true
-        catch _ =>
-          trace[Meta.Tactic.simp.congr] "processCongrHypothesis {c.theoremName} failed {← inferType x}"
-          -- Remark: we don't need to check ex.isMaxRecDepth anymore since `try .. catch ..`
-          -- does not catch runtime exceptions by default.
-          return none
-      unless modified do
-        trace[Meta.Tactic.simp.congr] "{c.theoremName} not modified"
-        return none
-      unless (← synthesizeArgs (.decl c.theoremName) xs bis (← read).discharge?) do
-        trace[Meta.Tactic.simp.congr] "{c.theoremName} synthesizeArgs failed"
-        return none
-      let eNew ← instantiateMVars rhs
-      let mut proof ← instantiateMVars (mkAppN thm xs)
-      if isIff then
-        try proof ← mkAppM ``propext #[proof]
-        catch _ => return none
-      if (← hasAssignableMVar proof <||> hasAssignableMVar eNew) then
-        trace[Meta.Tactic.simp.congr] "{c.theoremName} has unassigned metavariables"
-        return none
-      congrArgs { expr := eNew, proof? := proof } extraArgs
-    else
-      return none
-
-  congr (e : Expr) : M Result := do
-    let f := e.getAppFn
-    if f.isConst then
-      let congrThms ← getSimpCongrTheorems
-      let cs := congrThms.get f.constName!
-      for c in cs do
-        match (← trySimpCongrTheorem? c e) with
-        | none   => pure ()
-        | some r => return r
-      congrDefault e
-    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 }
-    else
-      congr e
-
-  simpConst (e : Expr) : M Result :=
-    return { expr := (← reduce e) }
-
-  withNewLemmas {α} (xs : Array Expr) (f : M α) : M α := do
-    if (← getConfig).contextual then
-      let mut s ← getSimpTheorems
-      let mut updated := false
-      for x in xs do
-        if (← isProof x) then
-          s ← s.addTheorem (.fvar x.fvarId!) x
-          updated := true
-      if updated then
-        withSimpTheorems s f
-      else
-        f
-    else
-      f
-
-  simpLambda (e : Expr) : M Result :=
-    withParent e <| lambdaTelescopeDSimp e fun xs e => withNewLemmas xs do
-      let r ← simp e
-      let eNew ← mkLambdaFVars xs r.expr
-      match r.proof? with
-      | none   => return { expr := eNew }
-      | some h =>
-        let p ← xs.foldrM (init := h) fun x h => do
-          mkFunExt (← mkLambdaFVars #[x] h)
-        return { expr := eNew, proof? := p }
-
-  simpArrow (e : Expr) : M Result := do
-    trace[Debug.Meta.Tactic.simp] "arrow {e}"
-    let p := e.bindingDomain!
-    let q := e.bindingBody!
-    let rp ← simp p
-    trace[Debug.Meta.Tactic.simp] "arrow [{(← getConfig).contextual}] {p} [{← isProp p}] -> {q} [{← isProp q}]"
-    if (← pure (← getConfig).contextual <&&> isProp p <&&> isProp q) then
-      trace[Debug.Meta.Tactic.simp] "ctx arrow {rp.expr} -> {q}"
-      withLocalDeclD e.bindingName! rp.expr fun h => do
-        let s ← getSimpTheorems
-        let s ← s.addTheorem (.fvar h.fvarId!) h
-        withSimpTheorems s do
-          let rq ← simp q
-          match rq.proof? with
-          | none    => mkImpCongr e rp rq
-          | some hq =>
-            let hq ← mkLambdaFVars #[h] hq
-            /-
-              We use the default reducibility setting at `mkImpDepCongrCtx` and `mkImpCongrCtx` because they use the theorems
-              ```lean
-              @implies_dep_congr_ctx : ∀ {p₁ p₂ q₁ : Prop}, p₁ = p₂ → ∀ {q₂ : p₂ → Prop}, (∀ (h : p₂), q₁ = q₂ h) → (p₁ → q₁) = ∀ (h : p₂), q₂ h
-              @implies_congr_ctx : ∀ {p₁ p₂ q₁ q₂ : Prop}, p₁ = p₂ → (p₂ → q₁ = q₂) → (p₁ → q₁) = (p₂ → q₂)
-              ```
-              And the proofs may be from `rfl` theorems which are now omitted. Moreover, we cannot establish that the two
-              terms are definitionally equal using `withReducible`.
-              TODO (better solution): provide the problematic implicit arguments explicitly. It is more efficient and avoids this
-              problem.
-             -/
-            if rq.expr.containsFVar h.fvarId! then
-              return { expr := (← mkForallFVars #[h] rq.expr), proof? := (← withDefault <| mkImpDepCongrCtx (← rp.getProof) hq) }
-            else
-              return { expr := e.updateForallE! rp.expr rq.expr, proof? := (← withDefault <| mkImpCongrCtx (← rp.getProof) hq) }
-    else
-      mkImpCongr e rp (← simp q)
-
-  simpForall (e : Expr) : M Result := withParent e do
-    trace[Debug.Meta.Tactic.simp] "forall {e}"
-    if e.isArrow then
-      simpArrow e
-    else if (← isProp e) then
-      /- The forall is a proposition. -/
-      let domain := e.bindingDomain!
-      if (← isProp domain) then
-        /-
-        The domain of the forall is also a proposition, and we can use `forall_prop_domain_congr`
-        IF we can simplify the domain.
-        -/
-        let rd ← simp domain
-        if let some h₁ := rd.proof? then
-          /- Using
-          ```
-          theorem forall_prop_domain_congr {p₁ p₂ : Prop} {q₁ : p₁ → Prop} {q₂ : p₂ → Prop}
-              (h₁ : p₁ = p₂)
-              (h₂ : ∀ a : p₂, q₁ (h₁.substr a) = q₂ a)
-              : (∀ a : p₁, q₁ a) = (∀ a : p₂, q₂ a)
-          ```
-          Remark: we should consider whether we want to add congruence lemma support for arbitrary `forall`-expressions.
-          Then, the theroem above can be marked as `@[congr]` and the following code deleted.
-          -/
-          let p₁ := domain
-          let p₂ := rd.expr
-          let q₁ := mkLambda e.bindingName! e.bindingInfo! p₁ e.bindingBody!
-          let result ← withLocalDecl e.bindingName! e.bindingInfo! p₂ fun a => withNewLemmas #[a] do
-            let prop := mkSort levelZero
-            let h₁_substr_a := mkApp6 (mkConst ``Eq.substr [levelOne]) prop (mkLambda `x .default prop (mkBVar 0)) p₂ p₁ h₁ a
-            let q_h₁_substr_a := e.bindingBody!.instantiate1 h₁_substr_a
-            let rb ← simp q_h₁_substr_a
-            let h₂ ← mkLambdaFVars #[a] (← rb.getProof)
-            let q₂ ← mkLambdaFVars #[a] rb.expr
-            let result ← mkForallFVars #[a] rb.expr
-            let proof := mkApp6 (mkConst ``forall_prop_domain_congr) p₁ p₂ q₁ q₂ h₁ h₂
-            return { expr := result, proof? := proof }
-          return result
-      let domain ← dsimp domain
-      withLocalDecl e.bindingName! e.bindingInfo! domain fun x => withNewLemmas #[x] do
-        let b := e.bindingBody!.instantiate1 x
-        let rb ← simp b
-        let eNew ← mkForallFVars #[x] rb.expr
-        match rb.proof? with
-        | none   => return { expr := eNew }
-        | some h => return { expr := eNew, proof? := (← mkForallCongr (← mkLambdaFVars #[x] h)) }
-    else
-      return { expr := (← dsimp e) }
-
-  simpLet (e : Expr) : M Result := do
-    let .letE n t v b _ := e | unreachable!
-    if (← getConfig).zeta then
-      return { expr := b.instantiate1 v }
-    else
-      match (← getSimpLetCase n t b) with
-      | SimpLetCase.dep => return { expr := (← dsimp e) }
-      | SimpLetCase.nondep =>
-        let rv ← simp v
-        withLocalDeclD n t fun x => do
-          let bx := b.instantiate1 x
-          let rbx ← simp bx
-          let hb? ← match rbx.proof? with
-            | none => pure none
-            | some h => pure (some (← mkLambdaFVars #[x] h))
-          let e' := mkLet n t rv.expr (← rbx.expr.abstractM #[x])
-          match rv.proof?, hb? with
-          | none,   none   => return { expr := e' }
-          | some h, none   => return { expr := e', proof? := some (← mkLetValCongr (← mkLambdaFVars #[x] rbx.expr) h) }
-          | _,      some h => return { expr := e', proof? := some (← mkLetCongr (← rv.getProof) h) }
-      | SimpLetCase.nondepDepVar =>
-        let v' ← dsimp v
-        withLocalDeclD n t fun x => do
-          let bx := b.instantiate1 x
-          let rbx ← simp bx
-          let e' := mkLet n t v' (← rbx.expr.abstractM #[x])
-          match rbx.proof? with
-          | none => return { expr := e' }
-          | some h =>
-            let h ← mkLambdaFVars #[x] h
-            return { expr := e', proof? := some (← mkLetBodyCongr v' h) }
-
-  cacheResult (cfg : Config) (r : Result) : M Result := do
-    if cfg.memoize then
-      let dischargeDepth := (← readThe Simp.Context).dischargeDepth
-      modify fun s => { s with cache := s.cache.insert e { r with dischargeDepth } }
-    return r
+  simpLoop e { expr := e }
 
 @[inline] def withSimpConfig (ctx : Context) (x : MetaM α) : MetaM α :=
   withConfig (fun c => { c with etaStruct := ctx.config.etaStruct }) <| withReducible x
@@ -651,7 +650,7 @@ def main (e : Expr) (ctx : Context) (usedSimps : UsedSimps := {}) (methods : Met
   withSimpConfig ctx do withCatchingRuntimeEx do
     try
       withoutCatchingRuntimeEx do
-        let (r, s) ← simp e methods ctx |>.run { usedTheorems := usedSimps }
+        let (r, s) ← simp e methods.toMethodsRef ctx |>.run { usedTheorems := usedSimps }
         trace[Meta.Tactic.simp.numSteps] "{s.numSteps}"
         return (r, s.usedTheorems)
     catch ex =>
@@ -661,125 +660,23 @@ def dsimpMain (e : Expr) (ctx : Context) (usedSimps : UsedSimps := {}) (methods
   withSimpConfig ctx do withCatchingRuntimeEx do
     try
       withoutCatchingRuntimeEx do
-        let (r, s) ← dsimp e methods ctx |>.run { usedTheorems := usedSimps }
+        let (r, s) ← dsimp e methods.toMethodsRef ctx |>.run { usedTheorems := usedSimps }
         pure (r, s.usedTheorems)
     catch ex =>
       if ex.isRuntime then throwNestedTacticEx `dsimp ex else throw ex
 
-/--
-  Return true if `e` is of the form `(x : α) → ... → s = t → ... → False`
-
-  Recall that this kind of proposition is generated by Lean when creating equations for
-  functions and match-expressions with overlapping cases.
-  Example: the following `match`-expression has overlapping cases.
-  ```
-  def f (x y : Nat) :=
-    match x, y with
-    | Nat.succ n, Nat.succ m => ...
-    | _, _ => 0
-  ```
-  The second equation is of the form
-  ```
-  (x y : Nat) → ((n m : Nat) → x = Nat.succ n → y = Nat.succ m → False) → f x y = 0
-  ```
-  The hypothesis `(n m : Nat) → x = Nat.succ n → y = Nat.succ m → False` is essentially
-  saying the first case is not applicable.
--/
-partial def isEqnThmHypothesis (e : Expr) : Bool :=
-  e.isForall && go e
-where
-  go (e : Expr) : Bool :=
-    match e with
-    | .forallE _ d b _ => (d.isEq || d.isHEq || b.hasLooseBVar 0) && go b
-    | _ => e.consumeMData.isConstOf ``False
-
-abbrev Discharge := Expr → SimpM (Option Expr)
-
-def dischargeUsingAssumption? (e : Expr) : SimpM (Option Expr) := do
-  (← getLCtx).findDeclRevM? fun localDecl => do
-    if localDecl.isImplementationDetail then
-      return none
-    else if (← isDefEq e localDecl.type) then
-      return some localDecl.toExpr
-    else
-      return none
-
-/--
-  Tries to solve `e` using `unifyEq?`.
-  It assumes that `isEqnThmHypothesis e` is `true`.
--/
-partial def dischargeEqnThmHypothesis? (e : Expr) : MetaM (Option Expr) := do
-  assert! isEqnThmHypothesis e
-  let mvar ← mkFreshExprSyntheticOpaqueMVar e
-  withReader (fun ctx => { ctx with canUnfold? := canUnfoldAtMatcher }) do
-    if let .none ← go? mvar.mvarId! then
-      instantiateMVars mvar
-    else
-      return none
-where
-  go? (mvarId : MVarId) : MetaM (Option MVarId) :=
-    try
-      let (fvarId, mvarId) ← mvarId.intro1
-      mvarId.withContext do
-        let localDecl ← fvarId.getDecl
-        if localDecl.type.isEq || localDecl.type.isHEq then
-          if let some { mvarId, .. } ← unifyEq? mvarId fvarId {} then
-            go? mvarId
-          else
-            return none
-        else
-          go? mvarId
-    catch _  =>
-      return some mvarId
-
-namespace DefaultMethods
-mutual
-  partial def discharge? (e : Expr) : SimpM (Option Expr) := do
-    if isEqnThmHypothesis e then
-      if let some r ← dischargeUsingAssumption? e then
-        return some r
-      if let some r ← dischargeEqnThmHypothesis? e then
-        return some r
-    let ctx ← read
-    trace[Meta.Tactic.simp.discharge] ">> discharge?: {e}"
-    if ctx.dischargeDepth >= ctx.config.maxDischargeDepth then
-      trace[Meta.Tactic.simp.discharge] "maximum discharge depth has been reached"
-      return none
-    else
-      withReader (fun ctx => { ctx with dischargeDepth := ctx.dischargeDepth + 1 }) do
-        let r ← simp e { pre := pre, post := post, discharge? := discharge? }
-        if r.expr.consumeMData.isConstOf ``True then
-          try
-            return some (← mkOfEqTrue (← r.getProof))
-          catch _ =>
-            return none
-        else
-          return none
-
-  partial def pre (e : Expr) : SimpM Step :=
-    preDefault e discharge?
-
-  partial def post (e : Expr) : SimpM Step :=
-    postDefault e discharge?
-end
-
-def methods : Methods :=
-  { pre := pre, post := post, discharge? := discharge? }
-
-end DefaultMethods
-
 end Simp
 open Simp (UsedSimps)
 
 def simp (e : Expr) (ctx : Simp.Context) (discharge? : Option Simp.Discharge := none)
     (usedSimps : UsedSimps := {}) : MetaM (Simp.Result × UsedSimps) := do profileitM Exception "simp" (← getOptions) do
   match discharge? with
-  | none   => Simp.main e ctx usedSimps (methods := Simp.DefaultMethods.methods)
-  | some d => Simp.main e ctx usedSimps (methods := { pre := (Simp.preDefault · d), post := (Simp.postDefault · d), discharge? := d })
+  | none   => Simp.main e ctx usedSimps (methods := Simp.methodsDefault)
+  | some d => Simp.main e ctx usedSimps (methods := Simp.mkMethods d)
 
 def dsimp (e : Expr) (ctx : Simp.Context)
     (usedSimps : UsedSimps := {}) : MetaM (Expr × UsedSimps) := do profileitM Exception "dsimp" (← getOptions) do
-  Simp.dsimpMain e ctx usedSimps (methods := Simp.DefaultMethods.methods)
+  Simp.dsimpMain e ctx usedSimps (methods := Simp.methodsDefault)
 
 /-- See `simpTarget`. This method assumes `mvarId` is not assigned, and we are already using `mvarId`s local context. -/
 def simpTargetCore (mvarId : MVarId) (ctx : Simp.Context) (discharge? : Option Simp.Discharge := none)

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

@@ -7,6 +7,7 @@ import Lean.Meta.ACLt
 import Lean.Meta.Match.MatchEqsExt
 import Lean.Meta.AppBuilder
 import Lean.Meta.SynthInstance
+import Lean.Meta.Tactic.UnifyEq
 import Lean.Meta.Tactic.Simp.Types
 import Lean.Meta.Tactic.LinearArith.Simp
 
@@ -180,6 +181,13 @@ where
   inErasedSet (thm : SimpTheorem) : Bool :=
     erased.contains thm.origin
 
+@[inline] def andThen' (s : Step) (f? : Expr → SimpM Step) : SimpM Step := do
+  match s with
+  | Step.done _  => return s
+  | Step.visit r =>
+    let s' ← f? r.expr
+    return s'.updateResult (← mkEqTrans r s'.result)
+
 @[inline] def andThen (s : Step) (f? : Expr → SimpM (Option Step)) : SimpM Step := do
   match s with
   | Step.done _  => return s
@@ -227,7 +235,7 @@ def rewriteUsingDecide? (e : Expr) : MetaM (Option Result) := withReducibleAndIn
       return none
 
 @[inline] def tryRewriteUsingDecide? (e : Expr) : SimpM (Option Step) := do
-  if (← read).config.decide then
+  if (← getConfig).decide then
     match (← rewriteUsingDecide? e) with
     | some r => return Step.done r
     | none => return none
@@ -235,12 +243,48 @@ def rewriteUsingDecide? (e : Expr) : MetaM (Option Result) := withReducibleAndIn
     return none
 
 def simpArith? (e : Expr) : SimpM (Option Step) := do
-  if !(← read).config.arith then return none
-  let some (e', h) ← Linear.simp? e (← read).parent? | return none
+  if !(← getConfig).arith then return none
+  let some (e', h) ← Linear.simp? e (← getContext).parent? | return none
   return Step.visit { expr := e', proof? := h }
 
-def simpMatchCore? (app : MatcherApp) (e : Expr) (discharge? : Expr → SimpM (Option Expr)) : SimpM (Option Step) := do
-  for matchEq in (← Match.getEquationsFor app.matcherName).eqnNames do
+/--
+Given a match-application `e` with `MatcherInfo` `info`, return `some result`
+if at least of one of the discriminants has been simplified.
+-/
+def simpMatchDiscrs? (info : MatcherInfo) (e : Expr) : SimpM (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.stripArgsN 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
+
+def simpMatchCore? (matcherName : Name) (e : Expr) (discharge? : Expr → SimpM (Option Expr)) : SimpM (Option Step) := do
+  for matchEq in (← Match.getEquationsFor matcherName).eqnNames do
     -- Try lemma
     match (← withReducible <| Simp.tryTheorem? e { origin := .decl matchEq, proof := mkConst matchEq, rfl := (← isRflTheorem matchEq) } discharge?) with
     | none   => pure ()
@@ -248,33 +292,142 @@ def simpMatchCore? (app : MatcherApp) (e : Expr) (discharge? : Expr → SimpM (O
   return none
 
 def simpMatch? (discharge? : Expr → SimpM (Option Expr)) (e : Expr) : SimpM (Option Step) := do
-  if (← read).config.iota then
-    let some app ← matchMatcherApp? e | return none
-    simpMatchCore? app e discharge?
+  if (← getConfig).iota then
+    if let some e ← reduceRecMatcher? e then
+      return some (.visit { expr := e })
+    let .const declName _ := e.getAppFn
+      | return none
+    if let some info ← getMatcherInfo? declName then
+      if let some r ← simpMatchDiscrs? info e then
+        return some (.visit r)
+      simpMatchCore? declName e discharge?
+    else
+      return none
   else
     return none
 
 def rewritePre (e : Expr) (discharge? : Expr → SimpM (Option Expr)) (rflOnly := false) : SimpM Step := do
-  for thms in (← read).simpTheorems do
+  for thms in (← getContext).simpTheorems do
     if let some r ← rewrite? e thms.pre thms.erased discharge? (tag := "pre") (rflOnly := rflOnly) then
       return Step.visit r
   return Step.visit { expr := e }
 
 def rewritePost (e : Expr) (discharge? : Expr → SimpM (Option Expr)) (rflOnly := false) : SimpM Step := do
-  for thms in (← read).simpTheorems do
+  for thms in (← getContext).simpTheorems do
     if let some r ← rewrite? e thms.post thms.erased discharge? (tag := "post") (rflOnly := rflOnly) then
       return Step.visit r
   return Step.visit { expr := e }
 
-def preDefault (e : Expr) (discharge? : Expr → SimpM (Option Expr)) : SimpM Step := do
+partial def preDefault (e : Expr) (discharge? : Expr → SimpM (Option Expr)) : SimpM Step := do
   let s ← rewritePre e discharge?
-  andThen s tryRewriteUsingDecide?
+  let s ← andThen s (simpMatch? discharge?)
+  let s ← andThen s tryRewriteUsingDecide?
+  if s.result.expr == e then
+    return s
+  else
+    andThen s (preDefault · discharge?)
 
 def postDefault (e : Expr) (discharge? : Expr → SimpM (Option Expr)) : SimpM Step := do
   let s ← rewritePost e discharge?
-  let s ← andThen s (simpMatch? discharge?)
   let s ← andThen s simpArith?
   let s ← andThen s tryRewriteUsingDecide?
   andThen s tryRewriteCtorEq?
 
+/--
+  Return true if `e` is of the form `(x : α) → ... → s = t → ... → False`
+
+  Recall that this kind of proposition is generated by Lean when creating equations for
+  functions and match-expressions with overlapping cases.
+  Example: the following `match`-expression has overlapping cases.
+  ```
+  def f (x y : Nat) :=
+    match x, y with
+    | Nat.succ n, Nat.succ m => ...
+    | _, _ => 0
+  ```
+  The second equation is of the form
+  ```
+  (x y : Nat) → ((n m : Nat) → x = Nat.succ n → y = Nat.succ m → False) → f x y = 0
+  ```
+  The hypothesis `(n m : Nat) → x = Nat.succ n → y = Nat.succ m → False` is essentially
+  saying the first case is not applicable.
+-/
+partial def isEqnThmHypothesis (e : Expr) : Bool :=
+  e.isForall && go e
+where
+  go (e : Expr) : Bool :=
+    match e with
+    | .forallE _ d b _ => (d.isEq || d.isHEq || b.hasLooseBVar 0) && go b
+    | _ => e.consumeMData.isConstOf ``False
+
+def dischargeUsingAssumption? (e : Expr) : SimpM (Option Expr) := do
+  (← getLCtx).findDeclRevM? fun localDecl => do
+    if localDecl.isImplementationDetail then
+      return none
+    else if (← isDefEq e localDecl.type) then
+      return some localDecl.toExpr
+    else
+      return none
+
+/--
+  Tries to solve `e` using `unifyEq?`.
+  It assumes that `isEqnThmHypothesis e` is `true`.
+-/
+partial def dischargeEqnThmHypothesis? (e : Expr) : MetaM (Option Expr) := do
+  assert! isEqnThmHypothesis e
+  let mvar ← mkFreshExprSyntheticOpaqueMVar e
+  withReader (fun ctx => { ctx with canUnfold? := canUnfoldAtMatcher }) do
+    if let .none ← go? mvar.mvarId! then
+      instantiateMVars mvar
+    else
+      return none
+where
+  go? (mvarId : MVarId) : MetaM (Option MVarId) :=
+    try
+      let (fvarId, mvarId) ← mvarId.intro1
+      mvarId.withContext do
+        let localDecl ← fvarId.getDecl
+        if localDecl.type.isEq || localDecl.type.isHEq then
+          if let some { mvarId, .. } ← unifyEq? mvarId fvarId {} then
+            go? mvarId
+          else
+            return none
+        else
+          go? mvarId
+    catch _  =>
+      return some mvarId
+
+def dischargeDefault? (e : Expr) : SimpM (Option Expr) := do
+  if isEqnThmHypothesis e then
+    if let some r ← dischargeUsingAssumption? e then
+      return some r
+    if let some r ← dischargeEqnThmHypothesis? e then
+      return some r
+  let ctx ← getContext
+  trace[Meta.Tactic.simp.discharge] ">> discharge?: {e}"
+  if ctx.dischargeDepth >= ctx.config.maxDischargeDepth then
+    trace[Meta.Tactic.simp.discharge] "maximum discharge depth has been reached"
+    return none
+  else
+    withTheReader Context (fun ctx => { ctx with dischargeDepth := ctx.dischargeDepth + 1 }) do
+      let r ← simp e
+      if r.expr.consumeMData.isConstOf ``True then
+        try
+          return some (← mkOfEqTrue (← r.getProof))
+        catch _ =>
+          return none
+      else
+        return none
+
+abbrev Discharge := Expr → SimpM (Option Expr)
+
+def mkMethods (discharge? : Discharge) : Methods := {
+  pre        := (preDefault · discharge?)
+  post       := (postDefault · discharge?)
+  discharge? := discharge?
+}
+
+def methodsDefault : Methods :=
+  mkMethods dischargeDefault?
+
 end Lean.Meta.Simp

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

@@ -44,7 +44,19 @@ structure State where
   usedTheorems : UsedSimps := {}
   numSteps     : Nat := 0
 
-abbrev SimpM := ReaderT Context $ StateRefT State MetaM
+private opaque MethodsRefPointed : NonemptyType.{0}
+
+private def MethodsRef : Type := MethodsRefPointed.type
+
+instance : Nonempty MethodsRef := MethodsRefPointed.property
+
+abbrev SimpM := ReaderT MethodsRef $ ReaderT Context $ StateRefT State MetaM
+
+@[extern "lean_simp"]
+opaque simp (e : Expr) : SimpM Result
+
+@[extern "lean_dsimp"]
+opaque dsimp (e : Expr) : SimpM Expr
 
 inductive Step where
   | visit : Result → Step
@@ -65,31 +77,46 @@ structure Methods where
   discharge? : Expr → SimpM (Option Expr) := fun _ => return none
   deriving Inhabited
 
-/- Internal monad -/
-abbrev M := ReaderT Methods SimpM
+unsafe def Methods.toMethodsRefImpl (m : Methods) : MethodsRef :=
+  unsafeCast m
 
-def pre (e : Expr) : M Step := do
-  (← read).pre e
+@[implemented_by Methods.toMethodsRefImpl]
+opaque Methods.toMethodsRef (m : Methods) : MethodsRef
 
-def post (e : Expr) : M Step := do
-  (← read).post e
+unsafe def MethodsRef.toMethodsImpl (m : MethodsRef) : Methods :=
+  unsafeCast m
 
-def discharge? (e : Expr) : M (Option Expr) := do
-  (← read).discharge? e
+@[implemented_by MethodsRef.toMethodsImpl]
+opaque MethodsRef.toMethods (m : MethodsRef) : Methods
+
+def getMethods : SimpM Methods :=
+  return MethodsRef.toMethods (← read)
+
+def pre (e : Expr) : SimpM Step := do
+  (← getMethods).pre e
+
+def post (e : Expr) : SimpM Step := do
+  (← getMethods).post e
+
+def discharge? (e : Expr) : SimpM (Option Expr) := do
+  (← getMethods).discharge? e
+
+@[inline] def getContext : SimpM Context :=
+  readThe Context
 
 def getConfig : SimpM Config :=
-  return (← read).config
+  return (← getContext).config
 
-@[inline] def withParent (parent : Expr) (f : M α) : M α :=
+@[inline] def withParent (parent : Expr) (f : SimpM α) : SimpM α :=
   withTheReader Context (fun ctx => { ctx with parent? := parent }) f
 
-def getSimpTheorems : M SimpTheoremsArray :=
+def getSimpTheorems : SimpM SimpTheoremsArray :=
   return (← readThe Context).simpTheorems
 
-def getSimpCongrTheorems : M SimpCongrTheorems :=
+def getSimpCongrTheorems : SimpM SimpCongrTheorems :=
   return (← readThe Context).congrTheorems
 
-@[inline] def withSimpTheorems (s : SimpTheoremsArray) (x : M α) : M α := do
+@[inline] def withSimpTheorems (s : SimpTheoremsArray) (x : SimpM α) : SimpM α := do
   let cacheSaved := (← get).cache
   modify fun s => { s with cache := {} }
   try
@@ -168,11 +195,7 @@ where
 Given a simplified function result `r` and arguments `args`, simplify arguments using `simp` and `dsimp`.
 The resulting proof is built using `congr` and `congrFun` theorems.
 -/
-@[specialize] def congrArgs
-    [Monad m] [MonadLiftT MetaM m] [MonadLiftT IO m] [MonadRef m] [MonadOptions m] [MonadTrace m] [AddMessageContext m]
-    (simp : Expr → m Result)
-    (dsimp : Expr → m Expr)
-    (r : Result) (args : Array Expr) : m Result := do
+def congrArgs (r : Result) (args : Array Expr) : SimpM Result := do
   if args.isEmpty then
     return r
   else
@@ -190,25 +213,13 @@ The resulting proof is built using `congr` and `congrFun` theorems.
       i := i + 1
     return r
 
-/--
-Helper class for generalizing `mkCongrSimp?`
--/
-class MonadCongrCache (m : Type → Type) where
-  find? : Expr → m (Option (Option CongrTheorem))
-  save  : Expr → (Option CongrTheorem) → m Unit
-
-instance : MonadCongrCache M where
-  find? f := return (← get).congrCache.find? f
-  save f thm? := modify fun s => { s with congrCache := s.congrCache.insert f thm? }
-
 /--
 Retrieve auto-generated congruence lemma for `f`.
 
 Remark: If all argument kinds are `fixed` or `eq`, it returns `none` because
 using simple congruence theorems `congr`, `congrArg`, and `congrFun` produces a more compact proof.
 -/
-def mkCongrSimp? [Monad m] [MonadLiftT MetaM m] [MonadEnv m] [MonadCongrCache m]
-  (f : Expr) : m (Option CongrTheorem) := do
+def mkCongrSimp? (f : Expr) : SimpM (Option CongrTheorem) := do
   if f.isConst then if (← isMatcher f.constName!) then
     -- We always use simple congruence theorems for auxiliary match applications
     return none
@@ -217,22 +228,17 @@ def mkCongrSimp? [Monad m] [MonadLiftT MetaM m] [MonadEnv m] [MonadCongrCache m]
   if kinds.all fun k => match k with | CongrArgKind.fixed => true | CongrArgKind.eq => true | _ => false then
     /- See remark above. -/
     return none
-  match (← MonadCongrCache.find? f) with
+  match (← get).congrCache.find? f with
   | some thm? => return thm?
   | none =>
     let thm? ← mkCongrSimpCore? f info kinds
-    MonadCongrCache.save f thm?
+    modify fun s => { s with congrCache := s.congrCache.insert f thm? }
     return thm?
 
 /--
 Try to use automatically generated congruence theorems. See `mkCongrSimp?`.
 -/
-@[specialize] def tryAutoCongrTheorem?
-    [Monad m] [MonadEnv m] [MonadCongrCache m] [MonadLiftT MetaM m]
-    [MonadLiftT IO m] [MonadRef m] [MonadOptions m] [MonadTrace m] [AddMessageContext m]
-    (simp : Expr → m Result)
-    (dsimp : Expr → m Expr)
-    (e : Expr) : m (Option Result) := do
+def tryAutoCongrTheorem? (e : Expr) : SimpM (Option Result) := do
   let f := e.getAppFn
   -- TODO: cache
   let some cgrThm ← mkCongrSimp? f | return none

src/Lean/Meta/Tactic/Split.lean

@@ -22,12 +22,14 @@ def simpMatch (e : Expr) : MetaM Simp.Result := do
   (·.1) <$> Simp.main e (← getSimpMatchContext) (methods := { pre })
 where
   pre (e : Expr) : SimpM Simp.Step := do
-    let some app ← matchMatcherApp? e | return Simp.Step.visit { expr := e }
+    unless (← isMatcherApp e) do
+      return Simp.Step.visit { expr := e }
+    let matcherDeclName := e.getAppFn.constName!
     -- First try to reduce matcher
     match (← reduceRecMatcher? e) with
     | some e' => return Simp.Step.done { expr := e' }
     | none    =>
-      match (← Simp.simpMatchCore? app e SplitIf.discharge?) with
+      match (← Simp.simpMatchCore? matcherDeclName e SplitIf.discharge?) with
       | some r => return r
       | none => return Simp.Step.visit { expr := e }
 

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