From f9dc77673b5b4746b825d1d07f4d1fb200b8f5ec Mon Sep 17 00:00:00 2001
From: Joachim Breitner <mail@joachim-breitner.de>
Date: Mon, 1 Dec 2025 13:51:55 +0100
Subject: [PATCH] feat: dedicated fix operator for well-founded recursion on
 Nat (#7965)
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

This PR lets recursive functions defined by well-founded recursion use a
different `fix` function when the termination measure is of type `Nat`.
This fix-point operator use structural recursion on “fuel”, initialized
by the given measure, and is thus reasonable to reduce, e.g. in `by
decide` proofs.

Extra provisions are in place that the fixpoint operator only starts
reducing when the fuel is fully known, to prevent “accidential” defeqs
when the remaining fuel for the recursive calls match the initial fuel
for that recursive argument.

To opt-out, the idiom `termination_by (n,0)` can be used.

We still use `@[irreducible]` as the default for such recursive
definitions, to avoid unexpected `defeq` lemmas. Making these functions
`@[semireducible]` by default showed performance regressions in lean.
When the measure is of type `Nat`, the system will accept an explicit
`@[semireducible]` without the usual warning.

Fixes #5234. Fixes: #11181.
---
 src/Init/WF.lean                            |  47 +++++++
 src/Lean/Compiler/InlineAttrs.lean          |   1 +
 src/Lean/Elab/PreDefinition/WF/Fix.lean     |  21 +++-
 src/Lean/Elab/PreDefinition/WF/Main.lean    |  14 ++-
 src/Lean/Elab/PreDefinition/WF/Unfold.lean  |  11 +-
 src/Lean/Meta/Tactic/FunInd.lean            | 132 +++++++++++---------
 src/Std/Sat/AIG/Basic.lean                  |   1 +
 stage0/src/stdlib_flags.h                   |   2 +
 tests/lean/run/1026.lean                    |   4 +-
 tests/lean/run/4928.lean                    |   2 +-
 tests/lean/run/hasNotBit.lean               |  23 ----
 tests/lean/run/issue10651.lean              |   6 +-
 tests/lean/run/issue11181.lean              |  10 ++
 tests/lean/run/issue2021.lean               |  46 +++++++
 tests/lean/run/issue2102.lean               |   6 +-
 tests/lean/run/issue2171.lean               |   2 +-
 tests/lean/run/letToHaveCleanup.lean        |   4 +-
 tests/lean/run/structuralEqn6.lean          |   2 +-
 tests/lean/run/wfEqns5.lean                 |   6 +-
 tests/lean/run/wfirred.lean                 |  57 ++++-----
 tests/lean/run/wfrec-nat.lean               | 130 +++++++++++++++++++
 tests/lean/wfrecUnusedLet.lean.expected.out |   2 +-
 tests/pkg/module/Module/Basic.lean          |   4 +-
 tests/pkg/module/Module/ImportedAll.lean    |   2 +-
 tests/pkg/module/Module/NonModule.lean      |   2 +-
 25 files changed, 383 insertions(+), 154 deletions(-)
 create mode 100644 tests/lean/run/issue11181.lean
 create mode 100644 tests/lean/run/issue2021.lean
 create mode 100644 tests/lean/run/wfrec-nat.lean

diff --git a/src/Init/WF.lean b/src/Init/WF.lean
index a22f03cab2..b33c4b4453 100644
--- a/src/Init/WF.lean
+++ b/src/Init/WF.lean
@@ -439,6 +439,53 @@ end
 
 end PSigma
 
+namespace WellFounded
+
+variable {α : Sort u}
+variable {motive : α → Sort v}
+variable (h : α → Nat)
+variable (F : (x : α) → ((y : α) → InvImage (· < ·) h y x → motive y) → motive x)
+
+/-- Helper gadget that prevents reduction of `Nat.eager n` unless `n` evalutes to a ground term. -/
+def Nat.eager (n : Nat) : Nat :=
+  if Nat.beq n n = true then n else n
+
+theorem Nat.eager_eq (n : Nat) : Nat.eager n = n := ite_self n
+
+/--
+A well-founded fixpoint operator specialized for `Nat`-valued measures. Given a measure `h`, it expects
+its higher order function argument `F` to invoke its argument only on values `y` that are smaller
+than `x` with regard to `h`.
+
+In contrast to to `WellFounded.fix`, this fixpoint operator reduces on closed terms. (More precisely:
+when `h x` evalutes to a ground value)
+
+-/
+def Nat.fix : (x : α) → motive x :=
+  let rec go : ∀ (fuel : Nat) (x : α), (h x < fuel) → motive x :=
+    Nat.rec
+      (fun _ hfuel => (Nat.not_succ_le_zero _ hfuel).elim)
+      (fun _ ih x hfuel => F x (fun y hy => ih y (Nat.lt_of_lt_of_le hy (Nat.le_of_lt_add_one hfuel))))
+  fun x => go (Nat.eager (h x + 1)) x (Nat.eager_eq _ ▸ Nat.lt_add_one _)
+
+protected theorem Nat.fix.go_congr (x : α) (fuel₁ fuel₂ : Nat) (h₁ : h x < fuel₁) (h₂ : h x < fuel₂) :
+    Nat.fix.go h F fuel₁ x h₁ = Nat.fix.go h F fuel₂ x h₂ := by
+  induction fuel₁ generalizing x fuel₂ with
+  | zero => contradiction
+  | succ fuel₁ ih =>
+    cases fuel₂ with
+    | zero => contradiction
+    | succ fuel₂ =>
+      exact congrArg (F x) (funext fun y => funext fun hy => ih y fuel₂ _ _ )
+
+theorem Nat.fix_eq (x : α) :
+    Nat.fix h F x = F x (fun y _ => Nat.fix h F y) := by
+  unfold Nat.fix
+  simp [Nat.eager_eq]
+  exact congrArg (F x) (funext fun _ => funext fun _ => Nat.fix.go_congr ..)
+
+end WellFounded
+
 /--
 The `wfParam` gadget is used internally during the construction of recursive functions by
 wellfounded recursion, to keep track of the parameter for which the automatic introduction
diff --git a/src/Lean/Compiler/InlineAttrs.lean b/src/Lean/Compiler/InlineAttrs.lean
index 224b8261f7..2cec66e953 100644
--- a/src/Lean/Compiler/InlineAttrs.lean
+++ b/src/Lean/Compiler/InlineAttrs.lean
@@ -37,6 +37,7 @@ private def isValidMacroInline (declName : Name) : CoreM Bool := do
   let isRec (declName' : Name) : Bool :=
     isBRecOnRecursor env declName' ||
     declName' == ``WellFounded.fix ||
+    declName' == ``WellFounded.Nat.fix ||
     declName' == declName ++ `_unary -- Auxiliary declaration created by `WF` module
   if Option.isSome <| info.value.find? fun e => e.isConst && isRec e.constName! then
     -- It contains a `brecOn` or `WellFounded.fix` application. So, it should be recursvie
diff --git a/src/Lean/Elab/PreDefinition/WF/Fix.lean b/src/Lean/Elab/PreDefinition/WF/Fix.lean
index afe0464f92..6e293abdeb 100644
--- a/src/Lean/Elab/PreDefinition/WF/Fix.lean
+++ b/src/Lean/Elab/PreDefinition/WF/Fix.lean
@@ -237,21 +237,32 @@ def solveDecreasingGoals (funNames : Array Name) (argsPacker : ArgsPacker) (decr
             Term.reportUnsolvedGoals remainingGoals
   instantiateMVars value
 
+def isNatLtWF (wfRel : Expr) : MetaM (Option Expr) := do
+  match_expr wfRel with
+  | invImage _ β f wfRelβ =>
+    unless (← isDefEq β (mkConst ``Nat)) do return none
+    unless (← isDefEq wfRelβ (mkConst ``Nat.lt_wfRel)) do return none
+    return f
+  | _ => return none
+
 def mkFix (preDef : PreDefinition) (prefixArgs : Array Expr) (argsPacker : ArgsPacker)
     (wfRel : Expr) (funNames : Array Name) (decrTactics : Array (Option DecreasingBy)) :
     TermElabM Expr := do
   let type ← instantiateForall preDef.type prefixArgs
   let (wfFix, varName) ← forallBoundedTelescope type (some 1) fun x type => do
     let x := x[0]!
+    let varName ← x.fvarId!.getUserName -- See comment below.
     let α ← inferType x
     let u ← getLevel α
     let v ← getLevel type
     let motive ← mkLambdaFVars #[x] type
-    let rel := mkProj ``WellFoundedRelation 0 wfRel
-    let wf  := mkProj ``WellFoundedRelation 1 wfRel
-    let wf ← mkAppM `Lean.opaqueId #[wf]
-    let varName ← x.fvarId!.getUserName -- See comment below.
-    return (mkApp4 (mkConst ``WellFounded.fix [u, v]) α motive rel wf, varName)
+    if let some measure ← isNatLtWF wfRel then
+      return (mkApp3 (mkConst `WellFounded.Nat.fix [u, v]) α motive measure, varName)
+    else
+      let rel := mkProj ``WellFoundedRelation 0 wfRel
+      let wf  := mkProj ``WellFoundedRelation 1 wfRel
+      let wf ← mkAppM `Lean.opaqueId #[wf]
+      return (mkApp4 (mkConst ``WellFounded.fix [u, v]) α motive rel wf, varName)
   forallBoundedTelescope (← whnf (← inferType wfFix)).bindingDomain! (some 2) fun xs _ => do
     let x   := xs[0]!
     -- Remark: we rename `x` here to make sure we preserve the variable name in the
diff --git a/src/Lean/Elab/PreDefinition/WF/Main.lean b/src/Lean/Elab/PreDefinition/WF/Main.lean
index dc790be35e..ac0205bad6 100644
--- a/src/Lean/Elab/PreDefinition/WF/Main.lean
+++ b/src/Lean/Elab/PreDefinition/WF/Main.lean
@@ -53,12 +53,6 @@ def wfRecursion (docCtx : LocalContext × LocalInstances) (preDefs : Array PreDe
     -- No termination_by here, so use GuessLex to infer one
     guessLex preDefs unaryPreDefProcessed fixedParamPerms argsPacker
 
-  -- Warn about likely unwanted reducibility attributes
-  preDefs.forM fun preDef =>
-    preDef.modifiers.attrs.forM fun a => do
-      if a.name = `reducible || a.name = `semireducible then
-        logWarningAt a.stx s!"marking functions defined by well-founded recursion as `{a.name}` is not effective"
-
   let preDefNonRec ← forallBoundedTelescope unaryPreDef.type fixedParamPerms.numFixed fun fixedArgs type => do
     let type ← whnfForall type
     unless type.isForall do
@@ -66,6 +60,14 @@ def wfRecursion (docCtx : LocalContext × LocalInstances) (preDefs : Array PreDe
     let packedArgType := type.bindingDomain!
     elabWFRel (preDefs.map (·.declName)) unaryPreDef.declName fixedParamPerms fixedArgs argsPacker packedArgType wf fun wfRel => do
       trace[Elab.definition.wf] "wfRel: {wfRel}"
+      let useNatRec := (← isNatLtWF wfRel).isSome
+      -- Warn about likely unwanted reducibility attributes
+      unless useNatRec do
+        preDefs.forM fun preDef =>
+          preDef.modifiers.attrs.forM fun a => do
+            if a.name = `reducible || a.name = `semireducible then
+              logWarningAt a.stx s!"marking functions defined by well-founded recursion as `{a.name}` is not effective"
+
       let (value, envNew) ← withoutModifyingEnv' do
         addAsAxiom unaryPreDef
         let value ← mkFix unaryPreDefProcessed fixedArgs argsPacker wfRel (preDefs.map (·.declName)) (preDefs.map (·.termination.decreasingBy?))
diff --git a/src/Lean/Elab/PreDefinition/WF/Unfold.lean b/src/Lean/Elab/PreDefinition/WF/Unfold.lean
index 8a82212342..76b3fa7f73 100644
--- a/src/Lean/Elab/PreDefinition/WF/Unfold.lean
+++ b/src/Lean/Elab/PreDefinition/WF/Unfold.lean
@@ -36,9 +36,14 @@ def rwFixEq (mvarId : MVarId) : MetaM MVarId := mvarId.withContext do
   -- lhs should be an application of the declNameNonrec, which unfolds to an
   -- application of fix in one step
   let some lhs' ← delta? lhs | throwError "rwFixEq: cannot delta-reduce {lhs}"
-  let_expr WellFounded.fix _α _C _r _hwf F x := lhs'
-    | throwTacticEx `rwFixEq mvarId "expected saturated fixed-point application in {lhs'}"
-  let h := mkAppN (mkConst ``WellFounded.fix_eq lhs'.getAppFn.constLevels!) lhs'.getAppArgs
+  let h ← match_expr lhs' with
+    | WellFounded.fix _α _C _r _hwf _F _x =>
+      pure <| mkAppN (mkConst ``WellFounded.fix_eq lhs'.getAppFn.constLevels!) lhs'.getAppArgs
+    | WellFounded.Nat.fix _α _C _motive _F _x =>
+      pure <| mkAppN (mkConst ``WellFounded.Nat.fix_eq lhs'.getAppFn.constLevels!) lhs'.getAppArgs
+    | _ => throwTacticEx `rwFixEq mvarId m!"expected saturated fixed-point application in {lhs'}"
+  let F := lhs'.appFn!.appArg!
+  let x := lhs'.appArg!
 
   -- We used to just rewrite with `fix_eq` and continue with whatever RHS that produces, but that
   -- would include more copies of `fix` resulting in large and confusing terms.
diff --git a/src/Lean/Meta/Tactic/FunInd.lean b/src/Lean/Meta/Tactic/FunInd.lean
index b279ca3850..b5e59ccd13 100644
--- a/src/Lean/Meta/Tactic/FunInd.lean
+++ b/src/Lean/Meta/Tactic/FunInd.lean
@@ -927,7 +927,7 @@ where doRealize (inductName : Name) := do
   -- to make sure that `target` indeed the last parameter
   let e := info.value
   let e ← lambdaTelescope e fun params body => do
-    if body.isAppOfArity ``WellFounded.fix 5 then
+    if body.isAppOfArity ``WellFounded.fix 5 || body.isAppOfArity ``WellFounded.Nat.fix 4 then
       forallBoundedTelescope (← inferType body) (some 1) fun xs _ => do
         unless xs.size = 1 do
           throwError "functional induction: Failed to eta-expand{indentExpr e}"
@@ -935,68 +935,76 @@ where doRealize (inductName : Name) := do
     else
       pure e
   let (e', paramMask) ← lambdaTelescope e fun params funBody => MatcherApp.withUserNames params varNames do
-    match_expr funBody with
-    | fix@WellFounded.fix α _motive rel wf body target =>
-      unless params.back! == target do
-        throwError "functional induction: expected the target as last parameter{indentExpr e}"
-      let fixedParamPerms := params.pop
-      let motiveType ←
-        if unfolding then
-          withLocalDeclD `r (← instantiateForall info.type params) fun r =>
-            mkForallFVars #[target, r] (.sort 0)
-        else
-          mkForallFVars #[target] (.sort 0)
-      withLocalDeclD `motive motiveType fun motive => do
-        let fn := mkAppN (← mkConstWithLevelParams name) fixedParamPerms
-        let isRecCall : Expr → Option Expr := fun e =>
-          e.withApp fun f xs =>
-            if f.isFVarOf motive.fvarId! && xs.size > 0 then
-            mkApp fn xs[0]!
-          else
-            none
-
-        let motiveArg ←
-          if unfolding then
-            let motiveArg := mkApp2 motive target (mkAppN (← mkConstWithLevelParams name) params)
-            mkLambdaFVars #[target] motiveArg
-          else
-            pure motive
-        let e' := .const ``WellFounded.fix [fix.constLevels![0]!, levelZero]
-        let e' := mkApp4 e' α motiveArg rel wf
-        check e'
-        let (body', mvars) ← M2.run do
-          forallTelescope (← inferType e').bindingDomain! fun xs goal => do
-            if xs.size ≠ 2 then
-              throwError "expected recursor argument to take 2 parameters, got {xs}" else
-            let targets : Array Expr := xs[*...1]
-            let genIH := xs[1]!
-            let extraParams := xs[2...*]
-            -- open body with the same arg
-            let body ← instantiateLambda body targets
-            lambdaTelescope1 body fun oldIH body => do
-              let body ← instantiateLambda body extraParams
-              let body' ← withRewrittenMotiveArg goal (rwFun #[name]) fun goal => do
-                buildInductionBody #[oldIH, genIH.fvarId!] #[] goal oldIH genIH.fvarId! isRecCall body
-              if body'.containsFVar oldIH then
-                throwError m!"Did not fully eliminate `{mkFVar oldIH}` from induction principle body:{indentExpr body}"
-              mkLambdaFVars (targets.push genIH) (← mkLambdaFVars extraParams body')
-        let e' := mkApp2 e' body' target
-        let e' ← mkLambdaFVars #[target] e'
-        let e' ← abstractIndependentMVars mvars (← motive.fvarId!.getDecl).index e'
-        let e' ← mkLambdaFVars #[motive] e'
-
-        -- We used to pass (usedOnly := false) below in the hope that the types of the
-        -- induction principle match the type of the function better.
-        -- But this leads to avoidable parameters that make functional induction strictly less
-        -- useful (e.g. when the unused parameter mentions bound variables in the users' goal)
-        let (paramMask, e') ← mkLambdaFVarsMasked fixedParamPerms e'
-        let e' ← instantiateMVars e'
-        return (e', paramMask)
-    | _ =>
-      if funBody.isAppOf ``WellFounded.fix then
-        throwError "Function `{name}` defined via `{.ofConstName ``WellFounded.fix}` with unexpected arity {funBody.getAppNumArgs}:{indentExpr funBody}"
+    unless funBody.isApp && funBody.appFn!.isApp do
+      throwError "functional induction: unexpected body {funBody}"
+    let body := funBody.appFn!.appArg!
+    let target := funBody.appArg!
+    unless params.back! == target do
+      throwError "functional induction: expected the target as last parameter{indentExpr e}"
+    let fixedParamPerms := params.pop
+    let motiveType ←
+      if unfolding then
+        withLocalDeclD `r (← instantiateForall info.type params) fun r =>
+          mkForallFVars #[target, r] (.sort 0)
       else
-        throwError "Function `{name}` not defined via `{.ofConstName ``WellFounded.fix}`:{indentExpr funBody}"
+        mkForallFVars #[target] (.sort 0)
+    withLocalDeclD `motive motiveType fun motive => do
+      let fn := mkAppN (← mkConstWithLevelParams name) fixedParamPerms
+      let isRecCall : Expr → Option Expr := fun e =>
+        e.withApp fun f xs =>
+          if f.isFVarOf motive.fvarId! && xs.size > 0 then
+          mkApp fn xs[0]!
+        else
+          none
+
+      let motiveArg ←
+        if unfolding then
+          let motiveArg := mkApp2 motive target (mkAppN (← mkConstWithLevelParams name) params)
+          mkLambdaFVars #[target] motiveArg
+        else
+          pure motive
+
+      let e' ← match_expr funBody with
+        | fix@WellFounded.fix α _motive rel wf _body _target =>
+          let e' := .const ``WellFounded.fix [fix.constLevels![0]!, levelZero]
+          pure <| mkApp4 e' α motiveArg rel wf
+        | fix@WellFounded.Nat.fix α _motive measure _body _target =>
+          let e' := .const `WellFounded.Nat.fix [fix.constLevels![0]!, levelZero]
+          pure <| mkApp3 e' α motiveArg measure
+        | _ =>
+          if funBody.isAppOf ``WellFounded.fix || funBody.isAppOf `WellFounded.Nat.Fix then
+            throwError "Function {name} defined via WellFounded.fix with unexpected arity {funBody.getAppNumArgs}:{indentExpr funBody}"
+          else
+            throwError "Function {name} not defined via WellFounded.fix:{indentExpr funBody}"
+      check e'
+      let (body', mvars) ← M2.run do
+        forallTelescope (← inferType e').bindingDomain! fun xs goal => do
+          if xs.size ≠ 2 then
+            throwError "expected recursor argument to take 2 parameters, got {xs}" else
+          let targets : Array Expr := xs[*...1]
+          let genIH := xs[1]!
+          let extraParams := xs[2...*]
+          -- open body with the same arg
+          let body ← instantiateLambda body targets
+          lambdaTelescope1 body fun oldIH body => do
+            let body ← instantiateLambda body extraParams
+            let body' ← withRewrittenMotiveArg goal (rwFun #[name]) fun goal => do
+              buildInductionBody #[oldIH, genIH.fvarId!] #[] goal oldIH genIH.fvarId! isRecCall body
+            if body'.containsFVar oldIH then
+              throwError m!"Did not fully eliminate `{mkFVar oldIH}` from induction principle body:{indentExpr body}"
+            mkLambdaFVars (targets.push genIH) (← mkLambdaFVars extraParams body')
+      let e' := mkApp2 e' body' target
+      let e' ← mkLambdaFVars #[target] e'
+      let e' ← abstractIndependentMVars mvars (← motive.fvarId!.getDecl).index e'
+      let e' ← mkLambdaFVars #[motive] e'
+
+      -- We used to pass (usedOnly := false) below in the hope that the types of the
+      -- induction principle match the type of the function better.
+      -- But this leads to avoidable parameters that make functional induction strictly less
+      -- useful (e.g. when the unused parameter mentions bound variables in the users' goal)
+      let (paramMask, e') ← mkLambdaFVarsMasked fixedParamPerms e'
+      let e' ← instantiateMVars e'
+      return (e', paramMask)
 
   unless (← isTypeCorrect e') do
     logError m!"failed to derive a type-correct induction principle:{indentExpr e'}"
diff --git a/src/Std/Sat/AIG/Basic.lean b/src/Std/Sat/AIG/Basic.lean
index 6567d5c1d9..75a79e20b3 100644
--- a/src/Std/Sat/AIG/Basic.lean
+++ b/src/Std/Sat/AIG/Basic.lean
@@ -485,6 +485,7 @@ where
       let lval := go lhs.gate decls assign (by omega) h2
       let rval := go rhs.gate decls assign (by omega) h2
       xor lval lhs.invert && xor rval rhs.invert
+  termination_by (x, 0) -- Don't allow reduction, we have large concrete gate entries
 
 /--
 Denotation of an `AIG` at a specific `Entrypoint`.
diff --git a/stage0/src/stdlib_flags.h b/stage0/src/stdlib_flags.h
index 79a0e58edd..f4d5f7ddae 100644
--- a/stage0/src/stdlib_flags.h
+++ b/stage0/src/stdlib_flags.h
@@ -1,5 +1,7 @@
 #include "util/options.h"
 
+// please update stage0
+
 namespace lean {
 options get_default_options() {
     options opts;
diff --git a/tests/lean/run/1026.lean b/tests/lean/run/1026.lean
index fd649b794f..945b4a4e7b 100644
--- a/tests/lean/run/1026.lean
+++ b/tests/lean/run/1026.lean
@@ -16,7 +16,7 @@ info: foo.eq_def (n : Nat) :
     if n = 0 then 0
     else
       have x := n - 1;
-      have this := foo._proof_4;
+      have this := foo._proof_3;
       foo x
 -/
 #guard_msgs in
@@ -28,7 +28,7 @@ info: foo.eq_unfold :
     if n = 0 then 0
     else
       have x := n - 1;
-      have this := foo._proof_4;
+      have this := foo._proof_3;
       foo x
 -/
 #guard_msgs in
diff --git a/tests/lean/run/4928.lean b/tests/lean/run/4928.lean
index d054f79d03..93ee9678e6 100644
--- a/tests/lean/run/4928.lean
+++ b/tests/lean/run/4928.lean
@@ -46,7 +46,7 @@ end
 /--
 error: Failed: `fail` tactic was invoked
 x : List Nat
-⊢ (invImage (fun x => PSum.casesOn x (fun x => x.length) fun x => x.length) sizeOfWFRel).1 (PSum.inr x.tail)
+⊢ InvImage (fun x1 x2 => x1 < x2) (fun x => PSum.casesOn x (fun x => x.length) fun x => x.length) (PSum.inr x.tail)
     (PSum.inl x)
 -/
 #guard_msgs in
diff --git a/tests/lean/run/hasNotBit.lean b/tests/lean/run/hasNotBit.lean
index c33e38857a..a1d9901623 100644
--- a/tests/lean/run/hasNotBit.lean
+++ b/tests/lean/run/hasNotBit.lean
@@ -30,13 +30,6 @@ elab "refl0" : tactic =>
   Lean.Elab.Tactic.closeMainGoalUsing `refl0 fun _ _ =>
     Lean.Meta.mkEqRefl (Lean.mkRawNatLit 0)
 
-/--
-error: (kernel) declaration type mismatch, '_example' has type
-  ∀ {α : Type u_1} {x : α}, 0 = 0
-but it is expected to have type
-  ∀ {α : Type u_1} {x : α}, Nat.land 1 (Nat.shiftRight 8 [x].ctorIdx) = 0
--/
-#guard_msgs in
 example : Nat.land 1 (Nat.shiftRight 8 ([x].ctorIdx)) = 0 := by
   refl0
 
@@ -45,13 +38,6 @@ elab "eagerrefl0" : tactic =>
   Lean.Elab.Tactic.closeMainGoalUsing `refl0 fun _ _ => do
     Lean.Meta.mkAppM `eagerReduce #[← Lean.Meta.mkEqRefl (Lean.mkRawNatLit 0)]
 
-/--
-error: (kernel) declaration type mismatch, '_example' has type
-  ∀ {α : Type u_1} {x : α}, 0 = 0
-but it is expected to have type
-  ∀ {α : Type u_1} {x : α}, Nat.land 1 (Nat.shiftRight 8 [x].ctorIdx) = 0
--/
-#guard_msgs in
 example : Nat.land 1 (Nat.shiftRight 8 ([x].ctorIdx)) = 0 := by
   eagerrefl0
 
@@ -61,15 +47,6 @@ elab "eagerrefl0'" : tactic =>
     let u ← getLevel goal
     return mkApp2 (mkConst ``eagerReduce [u]) goal (← mkEqRefl (mkRawNatLit 0))
 
-/--
-error: (kernel) application type mismatch
-  eagerReduce (Eq.refl 0)
-argument has type
-  0 = 0
-but function has type
-  Nat.land 1 (Nat.shiftRight 8 [x].ctorIdx) = 0 → Nat.land 1 (Nat.shiftRight 8 [x].ctorIdx) = 0
--/
-#guard_msgs in
 example : Nat.land 1 (Nat.shiftRight 8 ([x].ctorIdx)) = 0 := by
   eagerrefl0'
 
diff --git a/tests/lean/run/issue10651.lean b/tests/lean/run/issue10651.lean
index 9401d9763b..ab2d66da80 100644
--- a/tests/lean/run/issue10651.lean
+++ b/tests/lean/run/issue10651.lean
@@ -10,9 +10,9 @@ termination_by x
 
 /--
 info: equations:
-theorem f.eq_1 : f 0 = 1
-theorem f.eq_2 : f 100 = 2
-theorem f.eq_3 : f 1000 = 3
+@[defeq] theorem f.eq_1 : f 0 = 1
+@[defeq] theorem f.eq_2 : f 100 = 2
+@[defeq] theorem f.eq_3 : f 1000 = 3
 theorem f.eq_4 : ∀ (x_2 : Nat), (x_2 = 99 → False) → (x_2 = 999 → False) → f x_2.succ = f x_2
 -/
 #guard_msgs(pass trace, all) in
diff --git a/tests/lean/run/issue11181.lean b/tests/lean/run/issue11181.lean
new file mode 100644
index 0000000000..cea9b4484a
--- /dev/null
+++ b/tests/lean/run/issue11181.lean
@@ -0,0 +1,10 @@
+set_option warn.sorry false
+
+
+theorem Nat.foo₁ (n : Nat) : n ^^^ 0 = n ^^^ 0 := by
+  cases n
+  · simp only [HXor.hXor, instXorOp, xor, bitwise, Bool.bne_true, Bool.not_false, ↓reduceIte]
+  · sorry
+
+theorem Nat.foo₂ : 0 ^^^ 0 = 0 ^^^ 0 := by
+  simp only [HXor.hXor, instXorOp, xor, bitwise, Bool.bne_true, Bool.not_false, ↓reduceIte]
diff --git a/tests/lean/run/issue2021.lean b/tests/lean/run/issue2021.lean
new file mode 100644
index 0000000000..81ba85182b
--- /dev/null
+++ b/tests/lean/run/issue2021.lean
@@ -0,0 +1,46 @@
+prelude -- optional
+import Init.WF
+import Init.WFTactics
+import Init.Data.Nat.Basic
+namespace Nat'
+
+protected def modCore (y : Nat) : Nat → Nat → Nat
+  | Nat.zero, x => x
+  | Nat.succ fuel, x => if 0 < y ∧ y ≤ x then Nat'.modCore y fuel (x - y) else x
+
+protected def mod' (x y : @& Nat) : Nat :=
+Nat'.modCore y x x
+
+@[simp] theorem zero_mod' (b : Nat) : Nat'.mod' 0 b = 0 := rfl
+
+end Nat'
+
+namespace Nat
+
+private def gcdF' (x : Nat) : (∀ x₁, x₁ < x → Nat → Nat) → Nat → Nat :=
+  match x with
+  | 0      => fun _ y => y
+  | succ x => fun f y => f (Nat'.mod' y (succ x)) sorry (succ x)
+
+noncomputable def gcd' (a b : Nat) : Nat :=
+  WellFounded.fix (measure id).wf gcdF' a b
+
+@[simp] theorem gcd'_zero_left (y : Nat) : gcd' 0 y = y :=
+  rfl
+
+theorem gcd'_succ (x y : Nat) : gcd' (succ x) y = gcd' (Nat'.mod' y (succ x)) (succ x) :=
+  rfl   -- replace with `id rfl` and everything is ok
+
+/--
+error: (kernel) application type mismatch
+  @Eq.ndrec Nat (n✝ + 1) (fun n => gcd' n 0 = n) (of_eq_true (eq_self (n✝ + 1)))
+argument has type
+  n✝ + 1 = n✝ + 1
+but function has type
+  (fun n => gcd' n 0 = n) (n✝ + 1) → ∀ {b : Nat}, n✝ + 1 = b → (fun n => gcd' n 0 = n) b
+-/
+#guard_msgs in
+@[simp] theorem gcd'_zero_right (n : Nat) : gcd' n 0 = n := by
+  cases n <;> simp [gcd'_succ]
+
+end Nat
diff --git a/tests/lean/run/issue2102.lean b/tests/lean/run/issue2102.lean
index f56cf4909b..7668bf90b0 100644
--- a/tests/lean/run/issue2102.lean
+++ b/tests/lean/run/issue2102.lean
@@ -37,7 +37,8 @@ head✝ : T✝
 tl : List T✝
 x✝ :
   (y : (T : Type) ×' List T) →
-    (invImage (fun x => PSigma.casesOn x fun T ls => sizeOf ls) sizeOfWFRel).1 y ⟨T✝, head✝ :: tl⟩ → Option (List y.1)
+    InvImage (fun x1 x2 => x1 < x2) (fun x => PSigma.casesOn x fun T ls => sizeOf ls) y ⟨T✝, head✝ :: tl⟩ →
+      Option (List y.1)
 res : Option { x // x✝ ⟨T✝, tl⟩ ⋯ = some x } := (x✝ ⟨T✝, tl⟩ ⋯).attach
 T : Type
 ls : List T
@@ -61,7 +62,8 @@ head✝ : T✝
 tl : List T✝
 x✝ :
   (y : (T : Type) ×' List T) →
-    (invImage (fun x => PSigma.casesOn x fun T ls => sizeOf ls) sizeOfWFRel).1 y ⟨T✝, head✝ :: tl⟩ → Option (List y.1)
+    InvImage (fun x1 x2 => x1 < x2) (fun x => PSigma.casesOn x fun T ls => sizeOf ls) y ⟨T✝, head✝ :: tl⟩ →
+      Option (List y.1)
 res : Option { x // x✝ ⟨T✝, tl⟩ ⋯ = some x } := (x✝ ⟨T✝, tl⟩ ⋯).attach
 T : Type
 ls : List T
diff --git a/tests/lean/run/issue2171.lean b/tests/lean/run/issue2171.lean
index ed1ac3fd87..92d4963b70 100644
--- a/tests/lean/run/issue2171.lean
+++ b/tests/lean/run/issue2171.lean
@@ -3,7 +3,7 @@ def g (n : Nat) : Nat :=
     1
   else
     4 + g (n - 1)
-  termination_by n
+  termination_by (n,0)
   decreasing_by simp_wf; omega
 
 example : g 10000 = id g (id 10000) := rfl
diff --git a/tests/lean/run/letToHaveCleanup.lean b/tests/lean/run/letToHaveCleanup.lean
index da0138cd1d..84f3c4d383 100644
--- a/tests/lean/run/letToHaveCleanup.lean
+++ b/tests/lean/run/letToHaveCleanup.lean
@@ -171,11 +171,11 @@ def fnWFRec (n : Nat) : let α := Nat; α :=
 info: @[irreducible] def fnWFRec : Nat →
   have α : Type := Nat;
   α :=
-fnWFRec._proof_1.fix fun n a =>
+WellFounded.Nat.fix (fun x => x) fun n a =>
   (match (motive :=
       (n : Nat) →
         ((y : Nat) →
-            (invImage (fun x => x) sizeOfWFRel).1 y n →
+            InvImage (fun x1 x2 => x1 < x2) (fun x => x) y n →
               let α : Type := Nat;
               α) →
           let α : Type := Nat;
diff --git a/tests/lean/run/structuralEqn6.lean b/tests/lean/run/structuralEqn6.lean
index 1acb9df7b5..e88de20d03 100644
--- a/tests/lean/run/structuralEqn6.lean
+++ b/tests/lean/run/structuralEqn6.lean
@@ -80,7 +80,7 @@ info: equations:
 theorem trailingZeros2'.aux.eq_1 : ∀ (i : Int) (hi : i ≠ 0) (acc k_2 : Nat) (hk_2 : i.natAbs ≤ k_2 + 1),
   trailingZeros2'.aux k_2.succ i hi hk_2 acc =
     if h : i % 2 = 0 then trailingZeros2'.aux k_2 (i / 2) ⋯ ⋯ (acc + 1) else acc
-theorem trailingZeros2'.aux.eq_2 : ∀ (i : Int) (hi : i ≠ 0) (acc : Nat) (hk_2 : i.natAbs ≤ 0),
+@[defeq] theorem trailingZeros2'.aux.eq_2 : ∀ (i : Int) (hi : i ≠ 0) (acc : Nat) (hk_2 : i.natAbs ≤ 0),
   trailingZeros2'.aux 0 i hi hk_2 acc = acc
 -/
 #guard_msgs(pass trace, all) in
diff --git a/tests/lean/run/wfEqns5.lean b/tests/lean/run/wfEqns5.lean
index 824f980835..245b3cf62a 100644
--- a/tests/lean/run/wfEqns5.lean
+++ b/tests/lean/run/wfEqns5.lean
@@ -6,7 +6,7 @@ termination_by n => n
 
 /--
 info: equations:
-theorem foo.eq_1 : foo 0 0 = 0
+@[defeq] theorem foo.eq_1 : foo 0 0 = 0
 theorem foo.eq_2 : ∀ (x : Nat), (x = 0 → False) → foo 0 x = x
 theorem foo.eq_3 : ∀ (x n : Nat), foo n.succ x = foo n x
 -/
@@ -53,7 +53,7 @@ termination_by n => n
 
 /--
 info: equations:
-theorem bar.eq_1 : ∀ (x : Nat),
+@[defeq] theorem bar.eq_1 : ∀ (x : Nat),
   bar 0 x =
     match x with
     | 0 => 0
@@ -120,7 +120,7 @@ termination_by n => n
 
 /--
 info: equations:
-theorem Structural.bar.eq_1 : ∀ (x : Nat),
+@[defeq] theorem Structural.bar.eq_1 : ∀ (x : Nat),
   bar 0 x =
     match x with
     | 0 => 0
diff --git a/tests/lean/run/wfirred.lean b/tests/lean/run/wfirred.lean
index 718986522f..aeb415f738 100644
--- a/tests/lean/run/wfirred.lean
+++ b/tests/lean/run/wfirred.lean
@@ -1,13 +1,13 @@
 /-!
-Tests that definitions by well-founded recursion are irreducible.
+Tests that definitions by well-founded recursion (not on Nat) are irreducible.
 -/
 
 set_option pp.mvars false
 
-def foo : Nat → Nat
-  | 0 => 0
-  | n+1 => foo n
-termination_by n => n
+def foo : Nat → Nat → Nat
+  | 0,  m => m
+  | n+1, m => foo n (m + n)
+termination_by n m => (n, m)
 
 /--
 error: Type mismatch
@@ -15,10 +15,10 @@ error: Type mismatch
 has type
   ?_ = ?_
 but is expected to have type
-  foo 0 = 0
+  foo 0 m = m
 -/
 #guard_msgs in
-example : foo 0 = 0 := rfl
+example : foo 0 m = m := rfl
 
 /--
 error: Type mismatch
@@ -26,35 +26,22 @@ error: Type mismatch
 has type
   ?_ = ?_
 but is expected to have type
-  foo (n + 1) = foo n
+  foo (n + 1) m = foo n (m + n)
 -/
 #guard_msgs in
-example : foo (n+1) = foo n := rfl
+example : foo (n+1) m = foo n (m + n) := rfl
 
 -- also for closed terms
 /--
 error: Tactic `rfl` failed: The left-hand side
-  foo 0
+  foo 0 0
 is not definitionally equal to the right-hand side
   0
 
-⊢ foo 0 = 0
+⊢ foo 0 0 = 0
 -/
 #guard_msgs in
-example : foo 0 = 0 := by rfl
-
--- It only works on closed terms:
-/--
-error: Tactic `rfl` failed: The left-hand side
-  foo (n + 1)
-is not definitionally equal to the right-hand side
-  foo n
-
-n : Nat
-⊢ foo (n + 1) = foo n
--/
-#guard_msgs in
-example : foo (n+1) = foo n := by rfl
+example : foo 0 0 = 0 := by rfl
 
 section Unsealed
 
@@ -68,10 +55,10 @@ error: Type mismatch
 has type
   ?_ = ?_
 but is expected to have type
-  foo 0 = 0
+  foo 0 0 = 0
 -/
 #guard_msgs in
-example : foo 0 = 0 := rfl
+example : foo 0 0 = 0 := rfl
 
 /--
 error: Type mismatch
@@ -79,10 +66,10 @@ error: Type mismatch
 has type
   ?_ = ?_
 but is expected to have type
-  foo (n + 1) = foo n
+  foo (n + 1) m = foo n (n + m)
 -/
 #guard_msgs in
-example : foo (n+1) = foo n := rfl
+example : foo (n+1) m = foo n (n +m ):= rfl
 
 end Unsealed
 
@@ -94,15 +81,15 @@ error: Type mismatch
 has type
   ?_ = ?_
 but is expected to have type
-  foo 0 = 0
+  foo 0 m = m
 -/
 #guard_msgs in
-example : foo 0 = 0 := rfl
+example : foo 0 m = m := rfl
 
-def bar : Nat → Nat
-  | 0 => 0
-  | n+1 => bar n
-termination_by n => n
+def bar : Nat → Nat → Nat
+  | 0, m => m
+  | n+1, m => bar n (m + n)
+termination_by n m => (n, m)
 
 -- Once unsealed, the full internals are visible. This allows one to prove, for example
 -- an equality like the following
diff --git a/tests/lean/run/wfrec-nat.lean b/tests/lean/run/wfrec-nat.lean
new file mode 100644
index 0000000000..bae7eeba98
--- /dev/null
+++ b/tests/lean/run/wfrec-nat.lean
@@ -0,0 +1,130 @@
+/-!
+Tests around the special case of well-founded recursion on Nat.
+-/
+
+set_option warn.sorry false
+
+namespace T1
+
+@[semireducible]
+def foo : List α → Nat
+  | [] => 0
+  | _::xs => 1 + (foo xs)
+termination_by xs => xs.length
+
+-- Closed terms should evaluate
+
+example : foo ([] : List Unit) = 0 := rfl
+example : foo ([] : List Unit) = 0 := by decide
+example : foo ([] : List Unit) = 0 := by decide +kernel
+example : foo [1,2,3,4,5] = 5 := rfl
+example : foo [1,2,3,4,5] = 5 := by decide
+example : foo [1,2,3,4,5] = 5 := by decide +kernel
+
+-- Open terms should not (these wouldn't even without the provisions with `WellFounded.Nat.eager`,
+-- the fuel does not line up)
+
+example : foo (x::xs) = 1 + foo xs := by (fail_if_success rfl); simp [foo]
+example : foo (x::y::z::xs) = 1+ (1+(1+ foo xs)) := by (fail_if_success rfl); simp [foo]
+
+end T1
+
+-- Variant where the fuel does not line up
+
+namespace T2
+@[semireducible] def foo : List α → Nat
+  | [] => 0
+  | _::xs => 1 + (foo xs)
+termination_by xs => 2 * xs.length
+
+example : foo ([] : List Unit) = 0 := rfl
+example : foo ([] : List Unit) = 0 := by decide
+example : foo ([] : List Unit) = 0 := by decide +kernel
+example : foo [1,2,3,4,5] = 5 := rfl
+example : foo [1,2,3,4,5] = 5 := by decide
+example : foo [1,2,3,4,5] = 5 := by decide +kernel
+
+-- Open terms should not (these wouldn't even without the provisions, the fuel does not line up)
+
+example : foo (x::xs) = 1 + foo xs := by (fail_if_success rfl); simp [foo]
+example : foo (x::y::z::xs) = 1+ (1 + ( 1+ foo xs)) := by (fail_if_success rfl); simp [foo]
+
+end T2
+
+-- Idiom to switch to `WellFounded.fix`
+
+namespace T3
+def foo : List α → Nat
+  | [] => 0
+  | _::xs => 1 + (foo xs)
+termination_by xs => (xs.length, 0)
+
+example : foo ([] : List Unit) = 0 := by (fail_if_success rfl); simp [foo]
+example : foo ([] : List Unit) = 0 := by (fail_if_success decide); simp [foo]
+example : foo ([] : List Unit) = 0 := by (fail_if_success decide +kernel); simp [foo]
+example : foo [1,2,3,4,5] = 5 := by (fail_if_success rfl); simp [foo]
+example : foo [1,2,3,4,5] = 5 := by (fail_if_success decide); simp [foo]
+example : foo [1,2,3,4,5] = 5 := by (fail_if_success decide +kernel); simp [foo]
+
+-- Open terms should not (these wouldn't even without the provisions, the fuel does not line up)
+
+example : foo (x::xs) = 1 + foo xs := by (fail_if_success rfl); simp [foo]
+example : foo (x::y::z::xs) = 1+ (1 + ( 1+ foo xs)) := by (fail_if_success rfl); simp [foo]
+
+end T3
+
+-- Defeq between similar functions
+
+namespace T4
+
+@[semireducible] def foo (b : Bool) : Nat → Nat
+  | 0 => 0
+  | n+1 => 1 + foo b n
+termination_by n => n
+
+@[semireducible] def bar (b : Bool) : Nat → Nat
+  | 0 => 0
+  | n+1 => cond b 1 2 + bar b n
+termination_by n => n
+
+@[semireducible] def baz : Nat → Nat
+  | 0 => 0
+  | n+1 => 1 + baz n
+termination_by n => n
+
+example : foo true n = bar true n := rfl
+example : foo true n = baz n := rfl
+example : bar true n = baz n := rfl
+
+end T4
+
+-- For comparison: with wfrec
+
+namespace T4wfrec
+
+def foo (b : Bool) : Nat → Nat
+  | 0 => 0
+  | n+1 => 1 + foo b n
+termination_by n => (n, 0)
+
+def bar (b : Bool) : Nat → Nat
+  | 0 => 0
+  | n+1 => cond b 1 2 + bar b n
+termination_by n => (n, 0)
+
+def baz : Nat → Nat
+  | 0 => 0
+  | n+1 => 1 + baz n
+termination_by n => (n, 0)
+
+example : foo true n = bar true n := by (fail_if_success rfl); sorry
+example : foo true n = baz n := by (fail_if_success rfl); sorry
+example : bar true n = baz n := by (fail_if_success rfl); sorry
+
+unseal foo bar baz
+
+example : foo true n = bar true n := rfl
+example : foo true n = baz n := rfl
+example : bar true n = baz n := rfl
+
+end T4wfrec
diff --git a/tests/lean/wfrecUnusedLet.lean.expected.out b/tests/lean/wfrecUnusedLet.lean.expected.out
index df3e7ff0de..6bea16a759 100644
--- a/tests/lean/wfrecUnusedLet.lean.expected.out
+++ b/tests/lean/wfrecUnusedLet.lean.expected.out
@@ -1,5 +1,5 @@
 @[irreducible] def f : Nat → Nat :=
-f._proof_1.fix fun n a =>
+WellFounded.Nat.fix (fun x => x) fun n a =>
   if h : n = 0 then 1
   else
     let y := 42;
diff --git a/tests/pkg/module/Module/Basic.lean b/tests/pkg/module/Module/Basic.lean
index 3173550061..dbfab41f79 100644
--- a/tests/pkg/module/Module/Basic.lean
+++ b/tests/pkg/module/Module/Basic.lean
@@ -259,7 +259,7 @@ info: private theorem f_struct.eq_unfold : f_struct = fun x =>
 -/
 #guard_msgs(pass trace, all) in #print sig f_struct.eq_unfold
 
-/-- info: private theorem f_wfrec.eq_1 : ∀ (x : Nat), f_wfrec 0 x = x -/
+/-- info: @[defeq] private theorem f_wfrec.eq_1 : ∀ (x : Nat), f_wfrec 0 x = x -/
 #guard_msgs(pass trace, all) in #print sig f_wfrec.eq_1
 
 /--
@@ -279,7 +279,7 @@ info: private theorem f_wfrec.eq_unfold : f_wfrec = fun x x_1 =>
 -/
 #guard_msgs in #print sig f_wfrec.eq_unfold
 
-/-- info: theorem f_exp_wfrec.eq_1 : ∀ (x : Nat), f_exp_wfrec 0 x = x -/
+/-- info: @[defeq] theorem f_exp_wfrec.eq_1 : ∀ (x : Nat), f_exp_wfrec 0 x = x -/
 #guard_msgs in #print sig f_exp_wfrec.eq_1
 
 /--
diff --git a/tests/pkg/module/Module/ImportedAll.lean b/tests/pkg/module/Module/ImportedAll.lean
index 0972a63b62..8de160d484 100644
--- a/tests/pkg/module/Module/ImportedAll.lean
+++ b/tests/pkg/module/Module/ImportedAll.lean
@@ -105,7 +105,7 @@ info: theorem f_wfrec.induct_unfolding : ∀ (motive : Nat → Nat → Nat → P
 -/
 #guard_msgs(pass trace, all) in #print sig f_wfrec.induct_unfolding
 
-/-- info: theorem f_exp_wfrec.eq_1 : ∀ (x : Nat), f_exp_wfrec 0 x = x -/
+/-- info: @[defeq] theorem f_exp_wfrec.eq_1 : ∀ (x : Nat), f_exp_wfrec 0 x = x -/
 #guard_msgs in #print sig f_exp_wfrec.eq_1
 
 /--
diff --git a/tests/pkg/module/Module/NonModule.lean b/tests/pkg/module/Module/NonModule.lean
index 48bfa62e2b..5e2bb12dd6 100644
--- a/tests/pkg/module/Module/NonModule.lean
+++ b/tests/pkg/module/Module/NonModule.lean
@@ -54,7 +54,7 @@ info: theorem f_wfrec.induct_unfolding : ∀ (motive : Nat → Nat → Nat → P
 -/
 #guard_msgs(pass trace, all) in #print sig f_wfrec.induct_unfolding
 
-/-- info: theorem f_exp_wfrec.eq_1 : ∀ (x : Nat), f_exp_wfrec 0 x = x -/
+/-- info: @[defeq] theorem f_exp_wfrec.eq_1 : ∀ (x : Nat), f_exp_wfrec 0 x = x -/
 #guard_msgs(pass trace, all) in
 #print sig f_exp_wfrec.eq_1