feat: dedicated fix operator for well-founded recursion on Nat (#7965)

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

@@ -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

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

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

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?))

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.

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'}"

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`.

stage0/src/stdlib_flags.h

@@ -1,5 +1,7 @@
 #include "util/options.h"
 
+// please update stage0
+
 namespace lean {
 options get_default_options() {
     options opts;

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

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

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'
 

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

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]

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

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

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

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;

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

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

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

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

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;

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
 
 /--

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
 
 /--

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