From 39286862e3fa8752ea2cf0754b824a91fc5cd4b7 Mon Sep 17 00:00:00 2001
From: Joachim Breitner <mail@joachim-breitner.de>
Date: Fri, 10 May 2024 08:45:21 +0200
Subject: [PATCH] feat: well-founded definitions irreducible by default (#4061)
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

we keep running into examples where working with well-founded recursion
is slow because defeq checks (which are all over the place, including
failing ones that are back-tracked) unfold well-founded definitions.

The definition of a function defined by well-founded recursion should be
an implementation detail that should only be peeked inside by the
equation generator and the functional induction generator.

We now mark the mutual recursive function as irreducible (if the user
did not
set a flag explicitly), and use `withAtLeastTransparency .all` when
producing
the equations.

Proofs can be fixed by using rewriting, or – a bit blunt, but nice for
adjusting
existing proofs – using `unseal` (a.k.a. `attribute [local
semireducible]`).

Mathlib performance does not change a whole lot:

http://speed.lean-fro.org/mathlib4/compare/08b82265-75db-4a28-b12b-08751b9ad04a/to/16f46d5e-28b1-41c4-a107-a6f6594841f8
Build instructions -0.126 %, four modules with significant instructions
decrease.

To reduce impact, these definitions were changed:

* `Nat.mod`, to make `1 % n` reduce definitionally, so that `1` as a
`Fin 2` literal
works nicely. Theorems with larger `Fin` literals tend to need a `unseal
Nat.modCore`
   https://github.com/leanprover/lean4/pull/4098
* `List.ofFn` rewritten to be structurally recursive and not go via
`Array.ofFn`:
   https://github.com/leanprover-community/batteries/pull/784

Alternative designs explored were

 * Making `WellFounded.fix` irreducible.

One benefit is that recursive functions with equal definitions (possibly
after
instantiating fixed parameters) are defeq; this is used in mathlib to
relate

[`OrdinalApprox.gfpApprox`](https://leanprover-community.github.io/mathlib4_docs/Mathlib/SetTheory/Ordinal/FixedPointApproximants.html#OrdinalApprox.gfpApprox)
with `.lfpApprox`.

   But the downside is that one cannot use `unseal` in a
targeted way, being explicit in which recursive function needs to be
reducible here.

And in cases where Lean does unwanted unfolding, we’d still unfold the
recursive
definition once to expose `WellFounded.fix`, leading to large terms for
often no good
   reason.

* Defining `WellFounded.fix` to unroll defintionally once before hitting
a irreducible
`WellFounded.fixF`. This was explored in #4002. It shares most of the
ups and downs
with the previous variant, with the additional neat benefit that
function calls that
do not lead to recursive cases (e.g. a `[]` base case) reduce nicely.
This means that
   the majority of existing `rfl` proofs continue to work.

Issue #4051, which demonstrates how badly things can go if wf recursive
functions can be
unrolled, showed that making the recursive function irreducible there
leads to noticeably
faster elaboration than making `WellFounded.fix` irreducible; this is
good evidence that
the present PR is the way to go.

This fixes https://github.com/leanprover/lean4/issues/3988

---------

Co-authored-by: Leonardo de Moura <leomoura@amazon.com>
---
 RELEASES.md                                 |  13 +-
 src/Init/Data/Fin/Lemmas.lean               |   6 +
 src/Init/Data/Int/DivModLemmas.lean         |   7 +
 src/Init/Data/Nat/Bitwise/Lemmas.lean       |   5 +-
 src/Init/Data/Nat/Gcd.lean                  |  10 +-
 src/Init/Data/Nat/Lemmas.lean               |   6 +-
 src/Lean/Elab/PreDefinition/WF/Eqns.lean    |   2 +-
 src/Lean/Elab/PreDefinition/WF/Main.lean    |  17 ++-
 src/Lean/ReducibilityAttrs.lean             |   5 +
 stage0/src/stdlib_flags.h                   |   2 +
 tests/lean/run/1921.lean                    |   2 +-
 tests/lean/run/2389.lean                    |   4 +-
 tests/lean/run/ack.lean                     |   1 +
 tests/lean/run/casesRec.lean                |   2 +-
 tests/lean/run/defaultEliminator.lean       |   2 +-
 tests/lean/run/lazylistThunk.lean           |   2 +-
 tests/lean/run/splitIssue.lean              |  16 +--
 tests/lean/run/splitList.lean               |  32 ++---
 tests/lean/run/wfirred.lean                 | 139 ++++++++++++++++++++
 tests/lean/wfrecUnusedLet.lean.expected.out |   2 +-
 20 files changed, 228 insertions(+), 47 deletions(-)
 create mode 100644 tests/lean/run/wfirred.lean

diff --git a/RELEASES.md b/RELEASES.md
index 940cc2de9b..32378cc2a6 100644
--- a/RELEASES.md
+++ b/RELEASES.md
@@ -11,7 +11,18 @@ of each version.
 v4.9.0 (development in progress)
 ---------
 
-v4.8.0 
+* Functions defined by well-founded recursion are now marked as
+  `@[irreducible]`, which should prevent expensive and often unfruitful
+  unfolding of such definitions.
+
+  Existing proofs that hold by definitional equality (e.g. `rfl`) can be
+  rewritten to explictly unfold the function definition (using `simp`,
+  `unfold`, `rw`), or the recursive function can be temporariliy made
+  semireducible (using `unseal f in` before the command) or the function
+  definition itself can be marked as `@[semireducible]` to get the previous
+  behavor.
+
+v4.8.0
 ---------
 
 * **Executables configured with `supportInterpreter := true` on Windows should now be run via `lake exe` to function properly.**
diff --git a/src/Init/Data/Fin/Lemmas.lean b/src/Init/Data/Fin/Lemmas.lean
index 3f9fc0f431..1a0f5b9113 100644
--- a/src/Init/Data/Fin/Lemmas.lean
+++ b/src/Init/Data/Fin/Lemmas.lean
@@ -11,6 +11,9 @@ import Init.ByCases
 import Init.Conv
 import Init.Omega
 
+-- Remove after the next stage0 update
+set_option allowUnsafeReducibility true
+
 namespace Fin
 
 /-- If you actually have an element of `Fin n`, then the `n` is always positive -/
@@ -205,6 +208,7 @@ theorem val_add_one {n : Nat} (i : Fin (n + 1)) :
   | .inl h => cases Fin.eq_of_val_eq h; simp
   | .inr h => simpa [Fin.ne_of_lt h] using val_add_one_of_lt h
 
+unseal Nat.modCore in
 @[simp] theorem val_two {n : Nat} : (2 : Fin (n + 3)).val = 2 := rfl
 
 theorem add_one_pos (i : Fin (n + 1)) (h : i < Fin.last n) : (0 : Fin (n + 1)) < i + 1 := by
@@ -239,6 +243,7 @@ theorem succ_ne_zero {n} : ∀ k : Fin n, Fin.succ k ≠ 0
 
 @[simp] theorem succ_zero_eq_one : Fin.succ (0 : Fin (n + 1)) = 1 := rfl
 
+unseal Nat.modCore in
 /-- Version of `succ_one_eq_two` to be used by `dsimp` -/
 @[simp] theorem succ_one_eq_two : Fin.succ (1 : Fin (n + 2)) = 2 := rfl
 
@@ -390,6 +395,7 @@ theorem castSucc_lt_last (a : Fin n) : castSucc a < last n := a.is_lt
 
 @[simp] theorem castSucc_zero : castSucc (0 : Fin (n + 1)) = 0 := rfl
 
+unseal Nat.modCore in
 @[simp] theorem castSucc_one {n : Nat} : castSucc (1 : Fin (n + 2)) = 1 := rfl
 
 /-- `castSucc i` is positive when `i` is positive -/
diff --git a/src/Init/Data/Int/DivModLemmas.lean b/src/Init/Data/Int/DivModLemmas.lean
index d532d40a42..a6a33b293f 100644
--- a/src/Init/Data/Int/DivModLemmas.lean
+++ b/src/Init/Data/Int/DivModLemmas.lean
@@ -14,6 +14,8 @@ import Init.RCases
 # Lemmas about integer division needed to bootstrap `omega`.
 -/
 
+-- Remove after the next stage0 update
+set_option allowUnsafeReducibility true
 
 open Nat (succ)
 
@@ -142,12 +144,14 @@ theorem eq_one_of_mul_eq_one_left {a b : Int} (H : 0 ≤ b) (H' : a * b = 1) : b
   | ofNat _ => show ofNat _ = _ by simp
   | -[_+1] => show -ofNat _ = _ by simp
 
+unseal Nat.div in
 @[simp] protected theorem div_zero : ∀ a : Int, div a 0 = 0
   | ofNat _ => show ofNat _ = _ by simp
   | -[_+1] => rfl
 
 @[simp] theorem zero_fdiv (b : Int) : fdiv 0 b = 0 := by cases b <;> rfl
 
+unseal Nat.div in
 @[simp] protected theorem fdiv_zero : ∀ a : Int, fdiv a 0 = 0
   | 0      => rfl
   | succ _ => rfl
@@ -765,11 +769,13 @@ theorem ediv_eq_ediv_of_mul_eq_mul {a b c d : Int}
   | (n:Nat) => congrArg ofNat (Nat.div_one _)
   | -[n+1] => by simp [Int.div, neg_ofNat_succ]; rfl
 
+unseal Nat.div in
 @[simp] protected theorem div_neg : ∀ a b : Int, a.div (-b) = -(a.div b)
   | ofNat m, 0 => show ofNat (m / 0) = -↑(m / 0) by rw [Nat.div_zero]; rfl
   | ofNat m, -[n+1] | -[m+1], succ n => (Int.neg_neg _).symm
   | ofNat m, succ n | -[m+1], 0 | -[m+1], -[n+1] => rfl
 
+unseal Nat.div in
 @[simp] protected theorem neg_div : ∀ a b : Int, (-a).div b = -(a.div b)
   | 0, n => by simp [Int.neg_zero]
   | succ m, (n:Nat) | -[m+1], 0 | -[m+1], -[n+1] => rfl
@@ -938,6 +944,7 @@ theorem fdiv_nonneg {a b : Int} (Ha : 0 ≤ a) (Hb : 0 ≤ b) : 0 ≤ a.fdiv b :
   match a, b, eq_ofNat_of_zero_le Ha, eq_ofNat_of_zero_le Hb with
   | _, _, ⟨_, rfl⟩, ⟨_, rfl⟩ => ofNat_fdiv .. ▸ ofNat_zero_le _
 
+unseal Nat.div in
 theorem fdiv_nonpos : ∀ {a b : Int}, 0 ≤ a → b ≤ 0 → a.fdiv b ≤ 0
   | 0, 0, _, _ | 0, -[_+1], _, _ | succ _, 0, _, _ | succ _, -[_+1], _, _ => ⟨_⟩
 
diff --git a/src/Init/Data/Nat/Bitwise/Lemmas.lean b/src/Init/Data/Nat/Bitwise/Lemmas.lean
index c59bff8945..53467f2982 100644
--- a/src/Init/Data/Nat/Bitwise/Lemmas.lean
+++ b/src/Init/Data/Nat/Bitwise/Lemmas.lean
@@ -50,7 +50,10 @@ noncomputable def div2Induction {motive : Nat → Sort u}
       apply hyp
       exact Nat.div_lt_self n_pos (Nat.le_refl _)
 
-@[simp] theorem zero_and (x : Nat) : 0 &&& x = 0 := by rfl
+@[simp] theorem zero_and (x : Nat) : 0 &&& x = 0 := by
+  simp only [HAnd.hAnd, AndOp.and, land]
+  unfold bitwise
+  simp
 
 @[simp] theorem and_zero (x : Nat) : x &&& 0 = 0 := by
   simp only [HAnd.hAnd, AndOp.and, land]
diff --git a/src/Init/Data/Nat/Gcd.lean b/src/Init/Data/Nat/Gcd.lean
index c5a633e586..78961e04e0 100644
--- a/src/Init/Data/Nat/Gcd.lean
+++ b/src/Init/Data/Nat/Gcd.lean
@@ -37,11 +37,11 @@ def gcd (m n : @& Nat) : Nat :=
   termination_by m
   decreasing_by simp_wf; apply mod_lt _ (zero_lt_of_ne_zero _); assumption
 
-@[simp] theorem gcd_zero_left (y : Nat) : gcd 0 y = y :=
-  rfl
+@[simp] theorem gcd_zero_left (y : Nat) : gcd 0 y = y := by
+  rw [gcd]; rfl
 
-theorem gcd_succ (x y : Nat) : gcd (succ x) y = gcd (y % succ x) (succ x) :=
-  rfl
+theorem gcd_succ (x y : Nat) : gcd (succ x) y = gcd (y % succ x) (succ x) := by
+  rw [gcd]; rfl
 
 @[simp] theorem gcd_one_left (n : Nat) : gcd 1 n = 1 := by
   rw [gcd_succ, mod_one]
@@ -64,7 +64,7 @@ instance : Std.IdempotentOp gcd := ⟨gcd_self⟩
 
 theorem gcd_rec (m n : Nat) : gcd m n = gcd (n % m) m :=
   match m with
-  | 0 => by have := (mod_zero n).symm; rwa [gcd_zero_right]
+  | 0 => by have := (mod_zero n).symm; rwa [gcd, gcd_zero_right]
   | _ + 1 => by simp [gcd_succ]
 
 @[elab_as_elim] theorem gcd.induction {P : Nat → Nat → Prop} (m n : Nat)
diff --git a/src/Init/Data/Nat/Lemmas.lean b/src/Init/Data/Nat/Lemmas.lean
index 50124336f2..af9f3104b1 100644
--- a/src/Init/Data/Nat/Lemmas.lean
+++ b/src/Init/Data/Nat/Lemmas.lean
@@ -677,6 +677,10 @@ protected theorem pow_lt_pow_iff_right {a n m : Nat} (h : 1 < a) :
 
 /-! ### log2 -/
 
+@[simp]
+theorem log2_zero : Nat.log2 0 = 0 := by
+  simp [Nat.log2]
+
 theorem le_log2 (h : n ≠ 0) : k ≤ n.log2 ↔ 2 ^ k ≤ n := by
   match k with
   | 0 => simp [show 1 ≤ n from Nat.pos_of_ne_zero h]
@@ -697,7 +701,7 @@ theorem log2_self_le (h : n ≠ 0) : 2 ^ n.log2 ≤ n := (le_log2 h).1 (Nat.le_r
 
 theorem lt_log2_self : n < 2 ^ (n.log2 + 1) :=
   match n with
-  | 0 => Nat.zero_lt_two
+  | 0 => by simp
   | n+1 => (log2_lt n.succ_ne_zero).1 (Nat.le_refl _)
 
 /-! ### dvd -/
diff --git a/src/Lean/Elab/PreDefinition/WF/Eqns.lean b/src/Lean/Elab/PreDefinition/WF/Eqns.lean
index 8b1c6ae689..41d69f15b8 100644
--- a/src/Lean/Elab/PreDefinition/WF/Eqns.lean
+++ b/src/Lean/Elab/PreDefinition/WF/Eqns.lean
@@ -81,7 +81,7 @@ private partial def mkProof (declName : Name) (type : Expr) : MetaM Expr := do
     let (_, mvarId) ← main.mvarId!.intros
     let rec go (mvarId : MVarId) : MetaM Unit := do
       trace[Elab.definition.wf.eqns] "step\n{MessageData.ofGoal mvarId}"
-      if (← tryURefl mvarId) then
+      if ← withAtLeastTransparency .all (tryURefl mvarId) then
         return ()
       else if (← tryContradiction mvarId) then
         return ()
diff --git a/src/Lean/Elab/PreDefinition/WF/Main.lean b/src/Lean/Elab/PreDefinition/WF/Main.lean
index f05f560bb7..97a7560e84 100644
--- a/src/Lean/Elab/PreDefinition/WF/Main.lean
+++ b/src/Lean/Elab/PreDefinition/WF/Main.lean
@@ -132,12 +132,15 @@ def wfRecursion (preDefs : Array PreDefinition) : TermElabM Unit := do
       return { unaryPreDef with value }
   trace[Elab.definition.wf] ">> {preDefNonRec.declName} :=\n{preDefNonRec.value}"
   let preDefs ← preDefs.mapM fun d => eraseRecAppSyntax d
-  if (← isOnlyOneUnaryDef preDefs fixedPrefixSize) then
-    addNonRec preDefNonRec (applyAttrAfterCompilation := false)
-  else
-    withEnableInfoTree false do
+  -- Do not complain if the user sets @[semireducible], which usually is a noop,
+  -- we recognize that below and then do not set @[irreducible]
+  withOptions (allowUnsafeReducibility.set · true) do
+    if (← isOnlyOneUnaryDef preDefs fixedPrefixSize) then
       addNonRec preDefNonRec (applyAttrAfterCompilation := false)
-    addNonRecPreDefs fixedPrefixSize argsPacker preDefs preDefNonRec
+    else
+      withEnableInfoTree false do
+        addNonRec preDefNonRec (applyAttrAfterCompilation := false)
+      addNonRecPreDefs fixedPrefixSize argsPacker preDefs preDefNonRec
   -- We create the `_unsafe_rec` before we abstract nested proofs.
   -- Reason: the nested proofs may be referring to the _unsafe_rec.
   addAndCompilePartialRec preDefs
@@ -146,6 +149,10 @@ def wfRecursion (preDefs : Array PreDefinition) : TermElabM Unit := do
   for preDef in preDefs do
     markAsRecursive preDef.declName
     applyAttributesOf #[preDef] AttributeApplicationTime.afterCompilation
+    -- Unless the user asks for something else, mark the definition as irreducible
+    unless preDef.modifiers.attrs.any fun a =>
+      a.name = `semireducible || a.name = `reducible || a.name = `semireducible do
+      setIrreducibleAttribute preDef.declName
 
 builtin_initialize registerTraceClass `Elab.definition.wf
 
diff --git a/src/Lean/ReducibilityAttrs.lean b/src/Lean/ReducibilityAttrs.lean
index f843f0e4fc..2dac2267a2 100644
--- a/src/Lean/ReducibilityAttrs.lean
+++ b/src/Lean/ReducibilityAttrs.lean
@@ -184,4 +184,9 @@ def isIrreducible [Monad m] [MonadEnv m] (declName : Name) : m Bool := do
   | .irreducible => return true
   | _ => return false
 
+/-- Set the given declaration as `[irreducible]` -/
+def setIrreducibleAttribute [Monad m] [MonadEnv m] (declName : Name) : m Unit := do
+  setReducibilityStatus declName ReducibilityStatus.irreducible
+
+
 end Lean
diff --git a/stage0/src/stdlib_flags.h b/stage0/src/stdlib_flags.h
index 0699845ba4..158ed2fe60 100644
--- a/stage0/src/stdlib_flags.h
+++ b/stage0/src/stdlib_flags.h
@@ -1,5 +1,7 @@
 #include "util/options.h"
 
+// please auto update stage0
+
 namespace lean {
 options get_default_options() {
     options opts;
diff --git a/tests/lean/run/1921.lean b/tests/lean/run/1921.lean
index bdde9e9c3d..39cb992987 100644
--- a/tests/lean/run/1921.lean
+++ b/tests/lean/run/1921.lean
@@ -6,4 +6,4 @@ def f := #[true].any id 0 USize.size
 -- `native_decide` used to prove `false` here, due to a bug in `Array.anyMUnsafe`.
 example : f = true := by native_decide
 
-example : f = true := by simp (config := { decide := true }) [f, Array.any, Array.anyM]
+example : f = true := by simp (config := { decide := true }) [f, Array.any, Array.anyM, Array.anyM.loop]
diff --git a/tests/lean/run/2389.lean b/tests/lean/run/2389.lean
index 6923e6c5e6..c1d6cc1df8 100644
--- a/tests/lean/run/2389.lean
+++ b/tests/lean/run/2389.lean
@@ -26,7 +26,9 @@ def onlyZeros : Tree → Prop
   | .node [] => True
   | .node (x::s) => onlyZeros x ∧ onlyZeros (.node s)
 
-/-- Pattern-matching on `OnlyZeros` works despite `below` and `brecOn` not being generated. -/
+unseal onlyZeros in
+/-- Pattern-matching on `OnlyZeros` works despite `below` and `brecOn` not being generated
+if we make `onlyZeros` semireducible-/
 def toFixPoint : OnlyZeros t → onlyZeros t
   | .leaf => rfl
   | .node [] _ => True.intro
diff --git a/tests/lean/run/ack.lean b/tests/lean/run/ack.lean
index 41fd2ed6ea..54c8166c8e 100644
--- a/tests/lean/run/ack.lean
+++ b/tests/lean/run/ack.lean
@@ -28,6 +28,7 @@ info: [reduction] unfolded declarations (max: 1725, num: 4):
    Acc.rec ↦ 754use `set_option diagnostics.threshold <num>` to control threshold for reporting counters
 -/
 #guard_msgs in
+unseal ack in
 set_option diagnostics.threshold 500 in
 set_option diagnostics true in
 theorem ex : ack 3 2 = 29 :=
diff --git a/tests/lean/run/casesRec.lean b/tests/lean/run/casesRec.lean
index 2adf9e10e1..a8f4c639a2 100644
--- a/tests/lean/run/casesRec.lean
+++ b/tests/lean/run/casesRec.lean
@@ -8,7 +8,7 @@ def f (x : Nat) : Nat := by
 
 #eval f 10
 
-example : f x.succ = 2 * f x := rfl
+example : f x.succ = 2 * f x := by rw [f]; rfl
 end Ex1
 
 namespace Ex2
diff --git a/tests/lean/run/defaultEliminator.lean b/tests/lean/run/defaultEliminator.lean
index 5884879315..bc9c02f25a 100644
--- a/tests/lean/run/defaultEliminator.lean
+++ b/tests/lean/run/defaultEliminator.lean
@@ -22,7 +22,7 @@ termination_by (x, y)
 
 example (x y : Nat) : f x y > 0 := by
   induction x, y with
-  | zero_zero => decide
+  | zero_zero => simp [f]
   | succ_zero x ih => simp [f, ih]
   | zero_succ y ih => simp [f, ih]
   | succ_succ x y ih => simp [f, ih]
diff --git a/tests/lean/run/lazylistThunk.lean b/tests/lean/run/lazylistThunk.lean
index fc3f451ffb..785481da4f 100644
--- a/tests/lean/run/lazylistThunk.lean
+++ b/tests/lean/run/lazylistThunk.lean
@@ -25,7 +25,7 @@ in the list, ignoring delays
 
 theorem length_toList (l : LazyList α) : l.toList.length = l.length := by
   match l with
-  | nil => rfl
+  | nil => simp [length_toList]
   | cons a as => simp [length_toList as]
   | delayed as => simp [length_toList as.get]
 
diff --git a/tests/lean/run/splitIssue.lean b/tests/lean/run/splitIssue.lean
index b555f35416..fa0ee1dca1 100644
--- a/tests/lean/run/splitIssue.lean
+++ b/tests/lean/run/splitIssue.lean
@@ -15,23 +15,21 @@ termination_by l => l.length
 decreasing_by
   all_goals sorry
 
-theorem len_nil : len ([] : List α) = 0 := by
-  simp [len]
-
--- The `simp [len]` above generated the following equation theorems for len
+-- The equational theorems are
 #check @len.eq_1
 #check @len.eq_2
 #check @len.eq_3 -- It is conditional, and may be tricky to use.
+#check @len.eq_def
+
+theorem len_nil : len ([] : List α) = 0 := by
+  simp [len]
 
 theorem len_1 (a : α) : len [a] = 1 := by
   simp [len]
 
 theorem len_2 (a b : α) (bs : List α) : len (a::b::bs) = 1 + len (b::bs) := by
   conv => lhs; unfold len
-  rfl
-
--- The `unfold` tactic above generated the following theorem
-#check @len.eq_def
+  cases bs <;> simp [splitList, len_1]
 
 theorem len_cons (a : α) (as : List α) : len (a::as) = 1 + len as := by
   cases as with
@@ -41,7 +39,7 @@ theorem len_cons (a : α) (as : List α) : len (a::as) = 1 + len as := by
 theorem listlen : ∀ l : List α, l.length = len l := by
   intro l
   induction l with
-  | nil => rfl
+  | nil => simp [len]
   | cons h t ih =>
     simp [List.length, len_cons, ih]
     rw [Nat.add_comm]
diff --git a/tests/lean/run/splitList.lean b/tests/lean/run/splitList.lean
index 26f22f3a75..5d0229eb27 100644
--- a/tests/lean/run/splitList.lean
+++ b/tests/lean/run/splitList.lean
@@ -34,23 +34,21 @@ def len : List α → Nat
       len fst + len snd
 termination_by xs => xs.length
 
-theorem len_nil : len ([] : List α) = 0 := by
- simp [len]
 
--- The `simp [len]` above generated the following equation theorems for len
+-- The equational theorems are
 #check @len.eq_1
 #check @len.eq_2
 #check @len.eq_3
+#check @len.eq_def
+
+theorem len_nil : len ([] : List α) = 0 := by
+  simp [len]
 
 theorem len_1 (a : α) : len [a] = 1 := by
   simp [len]
 
 theorem len_2 (a b : α) (bs : List α) : len (a::b::bs) = 1 + len (b::bs) := by
-  conv => lhs; unfold len
-  rfl
-
--- The `unfold` tactic above generated the following theorem
-#check @len.eq_def
+  simp [len, splitList]
 
 theorem len_cons (a : α) (as : List α) : len (a::as) = 1 + len as := by
   cases as with
@@ -60,7 +58,7 @@ theorem len_cons (a : α) (as : List α) : len (a::as) = 1 + len as := by
 theorem listlen : ∀ l : List α, l.length = len l := by
   intro l
   induction l with
-  | nil => rfl
+  | nil => simp [len_nil]
   | cons h t ih =>
     simp [List.length, len_cons, ih]
     rw [Nat.add_comm]
@@ -85,23 +83,21 @@ decreasing_by
     subst h₂
     simp_arith [eq_of_heq h₃] at this |- ; simp [this]
 
-theorem len_nil : len ([] : List α) = 0 := by
-  simp [len]
-
--- The `simp [len]` above generated the following equation theorems for len
+-- The equational theorems are
 #check @len.eq_1
 #check @len.eq_2
 #check @len.eq_3
+#check @len.eq_def
+
+theorem len_nil : len ([] : List α) = 0 := by
+  simp [len]
 
 theorem len_1 (a : α) : len [a] = 1 := by
   simp [len]
 
 theorem len_2 (a b : α) (bs : List α) : len (a::b::bs) = 1 + len (b::bs) := by
   conv => lhs; unfold len
-  rfl
-
--- The `unfold` tactic above generated the following theorem
-#check @len.eq_def
+  simp [len, splitList]
 
 theorem len_cons (a : α) (as : List α) : len (a::as) = 1 + len as := by
   cases as with
@@ -111,7 +107,7 @@ theorem len_cons (a : α) (as : List α) : len (a::as) = 1 + len as := by
 theorem listlen : ∀ l : List α, l.length = len l := by
   intro l
   induction l with
-  | nil => rfl
+  | nil => simp [len_nil]
   | cons h t ih =>
     simp [List.length, len_cons, ih]
     rw [Nat.add_comm]
diff --git a/tests/lean/run/wfirred.lean b/tests/lean/run/wfirred.lean
new file mode 100644
index 0000000000..6916071e95
--- /dev/null
+++ b/tests/lean/run/wfirred.lean
@@ -0,0 +1,139 @@
+/-!
+Tests that definitions by well-founded recursion are irreducible.
+-/
+
+def foo : Nat → Nat
+  | 0 => 0
+  | n+1 => foo n
+termination_by n => n
+
+/--
+error: type mismatch
+  rfl
+has type
+  foo 0 = foo 0 : Prop
+but is expected to have type
+  foo 0 = 0 : Prop
+-/
+#guard_msgs in
+example : foo 0 = 0 := rfl
+
+/--
+error: type mismatch
+  rfl
+has type
+  foo (n + 1) = foo (n + 1) : Prop
+but is expected to have type
+  foo (n + 1) = foo n : Prop
+-/
+#guard_msgs in
+example : foo (n+1) = foo n := rfl
+
+-- This succeeding is a bug or misfeature in the rfl tactic, using the kernel defeq check
+#guard_msgs in
+example : foo 0 = 0 := by rfl
+
+-- It only works on closed terms:
+/--
+error: The rfl tactic failed. Possible reasons:
+- The goal is not a reflexive relation (neither `=` nor a relation with a @[refl] lemma).
+- The arguments of the relation are not equal.
+Try using the reflexivitiy lemma for your relation explicitly, e.g. `exact Eq.rfl`.
+n : Nat
+⊢ foo (n + 1) = foo n
+-/
+#guard_msgs in
+example : foo (n+1) = foo n := by rfl
+
+section Unsealed
+
+unseal foo
+
+example : foo 0 = 0 := rfl
+example : foo 0 = 0 := by rfl
+
+example : foo (n+1) = foo n := rfl
+example : foo (n+1) = foo n := by rfl
+
+end Unsealed
+
+--should be sealed again here
+
+/--
+error: type mismatch
+  rfl
+has type
+  foo 0 = foo 0 : Prop
+but is expected to have type
+  foo 0 = 0 : Prop
+-/
+#guard_msgs in
+example : foo 0 = 0 := rfl
+
+
+def bar : Nat → Nat
+  | 0 => 0
+  | n+1 => bar n
+termination_by n => n
+
+-- Once unsealed, the full internals are visible. This allows one to prove, for example
+
+/--
+error: type mismatch
+  rfl
+has type
+  foo = foo : Prop
+but is expected to have type
+  foo = bar : Prop
+-/
+#guard_msgs in
+example : foo = bar := rfl
+
+
+unseal foo bar in
+example : foo = bar := rfl
+
+
+-- Attributes on the definition take precedence
+@[semireducible] def baz : Nat → Nat
+  | 0 => 0
+  | n+1 => baz n
+termination_by n => n
+
+example : baz 0 = 0 := rfl
+
+seal baz in
+/--
+error: type mismatch
+  rfl
+has type
+  baz 0 = baz 0 : Prop
+but is expected to have type
+  baz 0 = 0 : Prop
+-/
+#guard_msgs in
+example : baz 0 = 0 := rfl
+
+example : baz 0 = 0 := rfl
+
+@[reducible] def quux : Nat → Nat
+  | 0 => 0
+  | n+1 => quux n
+termination_by n => n
+
+example : quux 0 = 0 := rfl
+
+set_option allowUnsafeReducibility true in
+seal quux in
+/--
+error: type mismatch
+  rfl
+has type
+  quux 0 = quux 0 : Prop
+but is expected to have type
+  quux 0 = 0 : Prop
+-/
+#guard_msgs in
+example : quux 0 = 0 := rfl
+
+example : quux 0 = 0 := rfl
diff --git a/tests/lean/wfrecUnusedLet.lean.expected.out b/tests/lean/wfrecUnusedLet.lean.expected.out
index 7fbd9db3dc..a9c7f8c558 100644
--- a/tests/lean/wfrecUnusedLet.lean.expected.out
+++ b/tests/lean/wfrecUnusedLet.lean.expected.out
@@ -1,4 +1,4 @@
-def f : Nat → Nat :=
+@[irreducible] def f : Nat → Nat :=
 f.proof_1.fix fun n a =>
   if h : n = 0 then 1
   else