feat: remove deprecated in-kernel native reduction (#14953)

This PR removes `Lean.reduceBool`, `Lean.reduceNat`,
`Lean.ofReduceBool`, `Lean.ofReduceNat` and `Lean.trustCompiler`, along
with the kernel's support for reducing applications of the first two by
running the compiler. They have been deprecated since 2026-02-01 in
favour of asserting native evaluations with axioms, which is what
`native_decide` and `bv_decide` already do through
`Lean.Meta.nativeEqTrue`. Nothing in the toolchain used them any more.

Removing the axioms makes `#print axioms`, and the upcoming `lake
check`, mean what it says for the whole environment.
`Lean.trustCompiler` was referenced unconditionally from the bodies of
`reduceBool` and `reduceNat` so that it would be reported for anything
reducing through them, which left it looking used in every environment
that merely imported them.

---------

Co-authored-by: Claude Opus 5 (1M context) <noreply@anthropic.com>

Author: Kha

src/Init/Core.lean

@@ -2327,86 +2327,6 @@ instance : Subsingleton (Squash α) where
     trivial
 
 namespace Lean
-/-! # Kernel reduction hints -/
-
-/--
-Depends on the correctness of the Lean compiler, interpreter, and all `[implemented_by ...]` and `[extern ...]` annotations.
--/
-@[deprecated "in-kernel native reduction is deprecated; assert native evaluations with axioms instead" (since := "2026-02-01")]
-axiom trustCompiler : True
-
-set_option linter.deprecated false in
-/--
-When the kernel tries to reduce a term `Lean.reduceBool c`, it will invoke the Lean interpreter to evaluate `c`.
-The kernel will not use the interpreter if `c` is not a constant.
-This feature is useful for performing proofs by reflection.
-
-Remark: the Lean frontend allows terms of the from `Lean.reduceBool t` where `t` is a term not containing
-free variables. The frontend automatically declares a fresh auxiliary constant `c` and replaces the term with
-`Lean.reduceBool c`. The main motivation is that the code for `t` will be pre-compiled.
-
-Warning: by using this feature, the Lean compiler and interpreter become part of your trusted code base.
-This is extra 30k lines of code. More importantly, you will probably not be able to check your development using
-external type checkers that do not implement this feature.
-Keep in mind that if you are using Lean as programming language, you are already trusting the Lean compiler and interpreter.
-So, you are mainly losing the capability of type checking your development using external checkers.
-
-Recall that the compiler trusts the correctness of all `[implemented_by ...]` and `[extern ...]` annotations.
-If an extern function is executed, then the trusted code base will also include the implementation of the associated
-foreign function.
--/
-@[deprecated "in-kernel native reduction is deprecated; assert native evaluations with axioms instead" (since := "2026-02-01")]
-opaque reduceBool (b : Bool) : Bool :=
-  -- This ensures that `#print axioms` will track use of `reduceBool`.
-  have := trustCompiler
-  b
-
-set_option linter.deprecated false in
-/--
-Similar to `Lean.reduceBool` for closed `Nat` terms.
-
-Remark: we do not have plans for supporting a generic `reduceValue {α} (a : α) : α := a`.
-The main issue is that it is non-trivial to convert an arbitrary runtime object back into a Lean expression.
-We believe `Lean.reduceBool` enables most interesting applications (e.g., proof by reflection).
--/
-@[deprecated "in-kernel native reduction is deprecated; assert native evaluations with axioms instead" (since := "2026-02-01")]
-opaque reduceNat (n : Nat) : Nat :=
-  -- This ensures that `#print axioms` will track use of `reduceNat`.
-  have := trustCompiler
-  n
-
-
-set_option linter.deprecated false in
-/--
-The axiom `ofReduceBool` is used to perform proofs by reflection. See `reduceBool`.
-
-This axiom is usually not used directly, because it has some syntactic restrictions.
-Instead, the `native_decide` tactic can be used to prove any proposition whose
-decidability instance can be evaluated to `true` using the lean compiler / interpreter.
-
-Warning: by using this feature, the Lean compiler and interpreter become part of your trusted code base.
-This is extra 30k lines of code. More importantly, you will probably not be able to check your development using
-external type checkers that do not implement this feature.
-Keep in mind that if you are using Lean as programming language, you are already trusting the Lean compiler and interpreter.
-So, you are mainly losing the capability of type checking your development using external checkers.
--/
-@[deprecated "in-kernel native reduction is deprecated; assert native evaluations with axioms instead" (since := "2026-02-01")]
-axiom ofReduceBool (a b : Bool) (h : reduceBool a = b) : a = b
-
-set_option linter.deprecated false in
-/--
-The axiom `ofReduceNat` is used to perform proofs by reflection. See `reduceBool`.
-
-Warning: by using this feature, the Lean compiler and interpreter become part of your trusted code base.
-This is extra 30k lines of code. More importantly, you will probably not be able to check your development using
-external type checkers that do not implement this feature.
-Keep in mind that if you are using Lean as programming language, you are already trusting the Lean compiler and interpreter.
-So, you are mainly losing the capability of type checking your development using external checkers.
--/
-@[deprecated "in-kernel native reduction is deprecated; assert native evaluations with axioms instead" (since := "2026-02-01")]
-axiom ofReduceNat (a b : Nat) (h : reduceNat a = b) : a = b
-
-
 /--
 The term `opaqueId x` will not be reduced by the kernel.
 -/

src/Lean/Environment.lean

@@ -640,7 +640,6 @@ private def asyncConsts (env : Environment) : AsyncConsts :=
 Constructs an elaboration environment from a given kernel environment's constants. All constants are
 accessible in both the private and public scope. All other data is empty.
 -/
-@[export lean_elab_environment_of_kernel_env]
 def ofKernelEnv (env : Kernel.Environment) : Environment :=
   { base.private := env, base.public := env, importRealizationCtx? := none }
 

src/Lean/Meta/ExprDefEq.lean

@@ -233,17 +233,6 @@ private def isDefEqEta (a b : Expr) : MetaM LBool := do
   else
     return .undef
 
-/-- Support for `Lean.reduceBool` and `Lean.reduceNat` -/
-def isDefEqNative (s t : Expr) : MetaM LBool := do
-  let isDefEq (s t) : MetaM LBool := toLBoolM <| Meta.isExprDefEqAux s t
-  let s? ← reduceNative? s
-  let t? ← reduceNative? t
-  match s?, t? with
-  | some s, some t => isDefEq s t
-  | some s, none   => isDefEq s t
-  | none,   some t => isDefEq s t
-  | none,   none   => pure LBool.undef
-
 /-- Support for reducing Nat basic operations. -/
 def isDefEqNat (s t : Expr) : MetaM LBool := do
   let isDefEq (s t) : MetaM LBool := toLBoolM <| Meta.isExprDefEqAux s t
@@ -2375,7 +2364,7 @@ private def isDefEqProjInst (t : Expr) (s : Expr) : MetaM LBool := do
 
 /--
 The special cases tried *after* the main `isExprDefEqExpensive` machinery has failed, as opposed
-to the early ones (`isDefEqNative`, `isDefEqNat`, `isDefEqOffset`).
+to the early ones (`isDefEqNat`, `isDefEqOffset`).
 
 `.false` means one of them decided the terms are *not* definitionally equal, and must not be read
 as "declined". `.undef` means they all declined — note that `isDefEqUnitLike` returning `false`
@@ -2427,7 +2416,6 @@ private def isExprDefEqExpensive (t : Expr) (s : Expr) : MetaM Bool := do
   if t != t' || s != s' then
     Meta.isExprDefEqAux t' s'
   else
-    whenUndefDo (isDefEqNative t s) do
     whenUndefDo (isDefEqNat t s) do
     whenUndefDo (isDefEqOffset t s) do
     whenUndefDo (isDefEqDelta t s) do

src/Lean/Meta/WHNF.lean

@@ -973,23 +973,6 @@ def reduceRecMatcher? (e : Expr) : MetaM (Option Expr) := do
           return none
       | _ => return none
 
-unsafe def reduceBoolNativeUnsafe (constName : Name) : MetaM Bool := evalConstCheck Bool `Bool constName
-unsafe def reduceNatNativeUnsafe (constName : Name) : MetaM Nat := evalConstCheck Nat `Nat constName
-@[implemented_by reduceBoolNativeUnsafe] opaque reduceBoolNative (constName : Name) : MetaM Bool
-@[implemented_by reduceNatNativeUnsafe] opaque reduceNatNative (constName : Name) : MetaM Nat
-
-def reduceNative? (e : Expr) : MetaM (Option Expr) :=
-  match e with
-  | Expr.app (Expr.const fName _) (Expr.const argName _) =>
-    if fName == ``Lean.reduceBool then do
-      return toExpr (← reduceBoolNative argName)
-    else if fName == ``Lean.reduceNat then do
-      return toExpr (← reduceNatNative argName)
-    else
-      return none
-  | _ =>
-    return none
-
 @[inline] def withNatValue (a : Expr) (k : Nat → MetaM (Option α)) : MetaM (Option α) := do
   if !a.hasExprMVar && a.hasFVar then
     return none
@@ -1086,12 +1069,9 @@ partial def whnfImp (e : Expr) : MetaM Expr :=
         match (← reduceNat? e') with
         | some v => cache useCache e v
         | none   =>
-          match (← reduceNative? e') with
-          | some v => cache useCache e v
-          | none   =>
-            match (← unfoldDefinition? e') with
-            | some e'' => cache useCache e (← whnfImp e'')
-            | none => cache useCache e e'
+          match (← unfoldDefinition? e') with
+          | some e'' => cache useCache e (← whnfImp e'')
+          | none => cache useCache e e'
 
 /-- If `e` is a projection function that satisfies `p`, then reduce it -/
 def reduceProjOf? (e : Expr) (p : Name → Bool) : MetaM (Option Expr) := do

src/Lean/Util/TestExtern.lean

@@ -30,7 +30,7 @@ syntax (name := testExternCmd) "test_extern " term : command
       let env ← getEnv
       if isExtern env f || (getImplementedBy? env f).isSome then
         let t' := (← unfold t f).expr
-        let r := mkApp (.const ``reduceBool []) (← mkDecide (← mkEq t t'))
+        let r ← mkDecide (← mkEq t t')
         if ! (← evalExpr Bool (.const ``Bool []) r) then
           throwError
             ("native implementation did not agree with reference implementation!\n" ++

src/kernel/type_checker.cpp

@@ -601,39 +601,9 @@ optional<expr> type_checker::unfold_definition(expr const & e) {
     }
 }
 
-static expr * g_lean_reduce_bool = nullptr;
-static expr * g_lean_reduce_nat  = nullptr;
-
-namespace ir {
-object * run_boxed_kernel(environment const & env, options const & opts, name const & fn, unsigned n, object **args);
-}
-
 expr mk_bool_true();
 expr mk_bool_false();
 
-optional<expr> reduce_native(environment const & env, expr const & e) {
-    if (!is_app(e)) return none_expr();
-    expr const & arg = app_arg(e);
-    if (!is_constant(arg)) return none_expr();
-    if (app_fn(e) == *g_lean_reduce_bool) {
-        object * r = ir::run_boxed_kernel(env, options(), const_name(arg), 0, nullptr);
-        if (!lean_is_scalar(r)) {
-            lean_dec_ref(r);
-            throw kernel_exception(env, "type checker failure, unexpected result value for 'Lean.reduceBool'");
-        }
-        return lean_unbox(r) == 0 ? some_expr(mk_bool_false()) : some_expr(mk_bool_true());
-    }
-    if (app_fn(e) == *g_lean_reduce_nat) {
-        object * r = ir::run_boxed_kernel(env, options(), const_name(arg), 0, nullptr);
-        if (lean_is_scalar(r) || lean_is_mpz(r)) {
-            return some_expr(mk_lit(literal(nat(r))));
-        } else {
-            throw kernel_exception(env, "type checker failure, unexpected result value for 'Lean.reduceNat'");
-        }
-    }
-    return none_expr();
-}
-
 static inline bool is_nat_lit_ext(expr const & e) { return e == *g_nat_zero || is_nat_lit(e); }
 static inline nat get_nat_val(expr const & e) {
     lean_assert(is_nat_lit_ext(e));
@@ -759,10 +729,7 @@ expr type_checker::whnf(expr const & e) {
     expr t = e;
     while (true) {
         expr t1 = whnf_core(t);
-        if (auto v = reduce_native(env(), t1)) {
-            m_st->m_whnf.insert(mk_pair(e, *v));
-            return *v;
-        } else if (auto v = reduce_nat(t1)) {
+        if (auto v = reduce_nat(t1)) {
             m_st->m_whnf.insert(mk_pair(e, *v));
             return *v;
         } else if (auto next_t = unfold_definition(t1)) {
@@ -1098,12 +1065,6 @@ lbool type_checker::lazy_delta_reduction(expr & t_n, expr & s_n) {
             }
         }
 
-        if (auto t_v = reduce_native(env(), t_n)) {
-            return to_lbool(is_def_eq_core(*t_v, s_n));
-        } else if (auto s_v = reduce_native(env(), s_n)) {
-            return to_lbool(is_def_eq_core(t_n, *s_v));
-        }
-
         switch (lazy_delta_reduction_step(t_n, s_n)) {
         case reduction_status::Continue:   break;
         case reduction_status::DefUnknown: return l_undef;
@@ -1340,8 +1301,6 @@ void initialize_type_checker() {
     g_nat_shiftLeft  = new_persistent_expr_const({"Nat", "shiftLeft"});
     g_nat_shiftRight = new_persistent_expr_const({"Nat", "shiftRight"});
     g_string_mk    = new_persistent_expr_const({"String", "ofList"});
-    g_lean_reduce_bool = new_persistent_expr_const({"Lean", "reduceBool"});
-    g_lean_reduce_nat  = new_persistent_expr_const({"Lean", "reduceNat"});
     register_name_generator_prefix(*g_kernel_fresh);
 }
 
@@ -1367,7 +1326,5 @@ void finalize_type_checker() {
     delete g_nat_shiftLeft;
     delete g_nat_shiftRight;
     delete g_string_mk;
-    delete g_lean_reduce_bool;
-    delete g_lean_reduce_nat;
 }
 }

src/library/ir_interpreter.cpp

@@ -1165,15 +1165,6 @@ object * run_boxed(elab_environment const & env, options const & opts, name cons
     return interpreter::with_interpreter<object *>(env, opts, fn, [&](interpreter & interp) { return interp.call_boxed(fn, n, args); });
 }
 
-extern "C" obj_res lean_elab_environment_of_kernel_env(obj_arg);
-elab_environment elab_environment_of_kernel_env(environment const & env) {
-    return elab_environment(lean_elab_environment_of_kernel_env(env.to_obj_arg()));
-}
-
-object * run_boxed_kernel(environment const & env, options const & opts, name const & fn, unsigned n, object **args) {
-    return run_boxed(elab_environment_of_kernel_env(env), opts, fn, n, args);
-}
-
 uint32 run_main(elab_environment const & env, options const & opts, list_ref<string_ref> const & args) {
     return interpreter::with_interpreter<uint32>(env, opts, "main", [&](interpreter & interp) { return interp.run_main(args); });
 }

tests/elab/kernel1.lean

@@ -21,35 +21,3 @@ def a3 := 20
 /-- info: a1 =?= a3 := false -/
 #guard_msgs in
 #eval checkDefEq `a1 `a3
-
-def v1 := 100000000000 + 100000000000
-def v2 := 200000000000
-def v3 := 200000000001
-def v4 : Bool := 20000000000 > 200000000001
-def v5 := 100000000000 - 100000000000
-
-def c1 := reduceNat v1
-def c2 := reduceNat v2
-def c3 := reduceNat v3
-def c4 := reduceBool v4
-def c5 := reduceNat v5
-
-/-- info: c1 =?= c2 := true -/
-#guard_msgs in
-#eval checkDefEq `c1 `c2
-
-/-- info: c1 =?= c3 := false -/
-#guard_msgs in
-#eval checkDefEq `c1 `c3
-
-/-- info: c5 =?= Nat.zero := true -/
-#guard_msgs in
-#eval checkDefEq `c5 `Nat.zero
-
-/-- info: Nat.zero =?= c5 := true -/
-#guard_msgs in
-#eval checkDefEq `Nat.zero `c5
-
-/-- info: c4 =?= Bool.true := false -/
-#guard_msgs in
-#eval checkDefEq `c4 `Bool.true