720cbd6434
This PR makes theorems opaque in almost all ways, including in the kernel. Already now, because of proof irrelevance, theorems are almost never unfolded. Furthermore, the import handling allows conflicting theorem declaration with same type and different values. This is sound, but would be confusing if the value, and thus the import order, matters for completeness. So with this change, a `theorem` becomes more like an `opaque`: It has a value (for soundness), but it is never unfolded during reduction or type checking. There are still some places in meta code that have to peek into theorems (e.g. `FunInd`, wfrec processing), but these are code transformations, not reduction. One place where reducing proofs is necessary is reducing `Acc.rec` eliminating into Type. With this change, all proofs that need to be reducable that way have to be `def`, not `theorem`. This is already the case due to the module system. This does not affect uses of `Acc` via well-founded recursion, because that has already been made opaque in #5182. This moves the reduction behavior of `Acc.rec` further into the “supported by the theory but not relied upon by regular Lean“ corner. Fixes #12804 --------- Co-authored-by: Claude Opus 4.6 <noreply@anthropic.com>
16 lines
315 B
Text
16 lines
315 B
Text
/-!
|
|
# Theorems should be completely opaque
|
|
|
|
Theorems should not be delta-reducible.
|
|
-/
|
|
|
|
theorem simpleThm : True := trivial
|
|
|
|
-- The `delta` tactic should not unfold theorems
|
|
/--
|
|
error: Tactic `delta` failed: did not delta reduce [simpleThm]
|
|
|
|
⊢ True
|
|
-/
|
|
#guard_msgs in
|
|
example : True := by delta simpleThm; trivial
|