diff --git a/mathlib4/Mathlib/Tactic/ClickSuggestions/Unfold.lean b/mathlib4/Mathlib/Tactic/ClickSuggestions/Unfold.lean index e972fdb6b..fc2494fa1 100644 --- a/mathlib4/Mathlib/Tactic/ClickSuggestions/Unfold.lean +++ b/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 diff --git a/reference-manual/Manual/Axioms.lean b/reference-manual/Manual/Axioms.lean index 2772f4744..ca652f161 100644 --- a/reference-manual/Manual/Axioms.lean +++ b/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) diff --git a/reference-manual/Manual/BasicTypes/BitVec.lean b/reference-manual/Manual/BasicTypes/BitVec.lean index 78e8e8f07..9fe6d6fe6 100644 --- a/reference-manual/Manual/BasicTypes/BitVec.lean +++ b/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" diff --git a/reference-manual/Manual/BasicTypes/Float.lean b/reference-manual/Manual/BasicTypes/Float.lean index b0b615256..210c62ba8 100644 --- a/reference-manual/Manual/BasicTypes/Float.lean +++ b/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} diff --git a/reference-manual/Manual/ValidatingProofs.lean b/reference-manual/Manual/ValidatingProofs.lean index 57ea002ce..a19e8f540 100644 --- a/reference-manual/Manual/ValidatingProofs.lean +++ b/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.