[#14953] feat: remove deprecated in-kernel native reduction

mathlib4/Mathlib/Tactic/ClickSuggestions/Unfold.lean

@@ -92,8 +92,6 @@ where
           return ← go e (acc.push e)
         if let some e ← reduceNat? e then
           return acc.push e
-        if let some e ← reduceNative? e then
-          return acc.push e
         if let some e ← unfoldProjDefaultInst? e then
           -- when unfolding a default instance, don't add it to the array of unfolds.
           let e ← whnfCore e

reference-manual/Manual/Axioms.lean

@@ -181,7 +181,7 @@ Because they occur only in a proof, the compiler has no problem generating code:
 tag := "standard-axioms"
 %%%
 
-There are seven standard axioms in Lean. The first three axioms are important parts of how mathematics is done in Lean:
+There are four standard axioms in Lean. The first three axioms are important parts of how mathematics is done in Lean:
  * ```signature
    Classical.choice.{u} {α : Sort u} : Nonempty α → α
    ```
@@ -202,40 +202,8 @@ Uses of this axiom are not intended to occur in finished proofs, as it can be us
    sorryAx {α : Sort u} (synthetic := true) : α
    ```
 
-Three final axioms do not truly exist for their _mathematical_ content; from a mathematical perspective they prove trivial statements:
-
- * ```signature
-    Lean.trustCompiler : True
-   ```
-
- * ```signature
-    Lean.ofReduceBool (a b : Bool) : Lean.reduceBool a = b → a = b
-   ```
- * ```signature
-    Lean.ofReduceNat (a b : Nat) : Lean.reduceNat a = b → a = b
-   ```
-
-These axioms instead track proofs that depend on the correctness of the entire compiler, and not just on the much smaller {tech}`kernel`.
-
-:::example "Creating and Tracking Proofs That Trust the Compiler"
-The functions {name}`Lean.reduceBool` and {name}`Lean.reduceNat` can be invoked to have the compiler perform a calculation; this can greatly improve performance of implementations of proof by reflection.
-
-```lean
-def largeNumber : Nat := Lean.reduceNat (230_000 + 4_500 + 1_000_067)
-```
-
-The resulting term depends on the axiom {name}`Lean.trustCompiler` in order to track the fact that this calculation depends on the correctness of the compiler.
-
-```lean (name := printAxExC1)
-#print axioms largeNumber
-```
-```leanOutput printAxExC1
-'largeNumber' depends on axioms: [Lean.trustCompiler]
-```
-:::
-
 :::example "Axioms and the `native_decide` Tactic"
-Instead of appealing to {name}`Lean.trustCompiler`, the {tactic}`native_decide` tactic creates a bespoke axiom for each invocation.
+The {tactic}`native_decide` tactic creates a bespoke axiom for each invocation.
 This allows each axiom to be audited for the precise statement that it proves.
 
 ```lean (name := printAxExC2)

reference-manual/Manual/BasicTypes/BitVec.lean

@@ -167,7 +167,7 @@ tag := "BitVec-automation"
 
 In addition to the full suite of automation and tools provided by Lean for every type, the {tactic}`bv_decide` tactic can solve many bitvector-related problems.
 This tactic invokes an external automated theorem prover (`cadical`) and reconstructs the proof that it provides in Lean's own logic.
-The resulting proofs rely only on the axiom {name}`Lean.ofReduceBool`; the external prover is not part of the trusted code base.
+The resulting proofs rely only on a dedicated axiom that {tactic}`bv_decide` generates for each invocation; the external prover is not part of the trusted code base.
 
 :::example "Popcount"
 

reference-manual/Manual/BasicTypes/Float.lean

@@ -359,7 +359,7 @@ Floating-point numbers fall into one of three categories:
 ### Inequalities
 
 The decision procedures for inequalities are opaque constants in the logic.
-They can only be used via the {name}`Lean.ofReduceBool` axiom, e.g. via the {tactic}`native_decide` tactic.
+They can only be used via native evaluation, e.g. via the {tactic}`native_decide` tactic.
 
 {docstring Float.le}
 

reference-manual/Manual/ValidatingProofs.lean

@@ -110,7 +110,7 @@ This command prints the set of axioms used by the theorem and the theorems it de
 The three axioms above are standard axioms of Lean's logic, and benign.
 
 * If {name}`sorryAx` is reported, then this theorem or one of its dependencies uses {lean}`sorry` or is otherwise incomplete.
-* If {name}`Lean.trustCompiler` is reported, then native evaluation is used; see below for a discussion.
+* If an axiom generated by native evaluation is reported, then compiled code is trusted as part of the proof; see below for a discussion.
 * Any other axiom means that a custom axiom was declared and used, and the theorem is only valid relative to the soundness of these axioms.
 
 ## Trust
@@ -227,11 +227,11 @@ This is used by the {tactic}`decide`{keywordOf Lean.Parser.Tactic.decide}` +nati
 Specific uses wrapped in {tech}[honest] tactics (e.g. {tactic}`bv_decide`) are generally trustworthy.
 The trusted code base is larger (it includes Lean's compilation toolchain and library annotations in the standard library), but still fixed and vetted.
 
-General use ({tactic}`decide`{keywordOf Lean.Parser.Tactic.decide}` +native` or direct use of {name}`Lean.ofReduceBool`) can be used to create invalid proofs whenever the native evaluation of a term disagrees with the kernel's evaluation.
+General use ({tactic}`decide`{keywordOf Lean.Parser.Tactic.decide}` +native` or direct use of `Lean.ofReduceBool`) can be used to create invalid proofs whenever the native evaluation of a term disagrees with the kernel's evaluation.
 In particular, for every {attr}`implemented_by`/{attr}`extern` attribute in libraries it becomes part of the trusted code base that the replacement is semantically equivalent.
 
-All these uses show up as an axiom {name}`Lean.trustCompiler` in {keywordOf Lean.Parser.Command.printAxioms}`#print axioms`.
+All these uses show up as an axiom `Lean.trustCompiler` in {keywordOf Lean.Parser.Command.printAxioms}`#print axioms`.
 External checkers (`lean4checker`, `comparator`) cannot check such proofs, as they do not have access to the Lean compiler.
 When that level of checking is needed, proofs have to avoid using native evaluation.
 
-Since Lean 4.29.0, the {tactic}`decide`{keywordOf Lean.Parser.Tactic.decide}` +native` and {tactic}`bv_decide` tactics no longer use {name}`Lean.trustCompiler`, but instead introduce one dedicated axiom for each computation that is asserted by native computation. The {name}`Lean.trustCompiler` machinery is deprecated and will eventually be removed.
+Since Lean 4.29.0, the {tactic}`decide`{keywordOf Lean.Parser.Tactic.decide}` +native` and {tactic}`bv_decide` tactics no longer use `Lean.trustCompiler`, but instead introduce one dedicated axiom for each computation that is asserted by native computation. The `Lean.trustCompiler` machinery has since been removed.