max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2
lean4-htt/src/Lean
History
Joachim Breitner 720cbd6434
feat: theorems are opaque (#12973) 
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>
2026-03-23 13:57:07 +00:00
..
Compiler fix: interaction of extern annotations and calls to functions with borrowed parameters (#13052) 2026-03-23 10:03:26 +00:00
Data feat: stricter meta check for temporary programs in native_decide etc (#13005) 2026-03-20 15:51:18 +00:00
DocString fix: error messages from Verso docstring parser (#12372) 2026-02-07 07:49:06 +00:00
Elab feat: theorems are opaque (#12973) 2026-03-23 13:57:07 +00:00
Language chore: shake core (#12276) 2026-02-05 09:10:32 +00:00
LibrarySuggestions chore: fix core after rebootstrap 2026-02-25 11:40:02 +01:00
Linter fix: make option linter.unusedSimpArgs respect linter.all (#12560) 2026-03-09 15:12:02 +00:00
Meta feat: theorems are opaque (#12973) 2026-03-23 13:57:07 +00:00
Parser feat: unfold and rewrap instances in inferInstanceAs and deriving 2026-03-22 13:25:46 +01:00
ParserCompiler
PrettyPrinter feat: stricter meta check for temporary programs in native_decide etc (#13005) 2026-03-20 15:51:18 +00:00
Server feat: stricter meta check for temporary programs in native_decide etc (#13005) 2026-03-20 15:51:18 +00:00
Util feat: theorems are opaque (#12973) 2026-03-23 13:57:07 +00:00
Widget feat: use StateT.run instead of function application (#5121) 2026-03-03 03:12:26 +00:00
AddDecl.lean feat: add structured TraceResult to TraceData (#12698) 2026-03-10 02:42:57 +00:00
Attributes.lean fix: run @[init] declarations in declaration order (#12221) 2026-01-29 15:32:56 +00:00
AuxRecursor.lean feat: experimental option to move non-meta compilation out of lean build step (#10291) 2026-03-20 10:39:39 +00:00
BuiltinDocAttr.lean
Class.lean feat: add [univ_out_params] (#12423) 2026-02-11 15:42:00 +00:00
Compiler.lean feat: unify name demangling with single Lean implementation (#12539) 2026-03-06 12:29:35 +00:00
CoreM.lean feat: theorems are opaque (#12973) 2026-03-23 13:57:07 +00:00
Data.lean feat: persistent hash map iterator (#12852) 2026-03-10 08:01:32 +00:00
Declaration.lean feat: theorems are opaque (#12973) 2026-03-23 13:57:07 +00:00
DeclarationRange.lean
DefEqAttrib.lean feat: theorems are opaque (#12973) 2026-03-23 13:57:07 +00:00
DocString.lean
Elab.lean feat: idbg interactive debug expression evaluator (#12648) 2026-02-23 17:22:44 +00:00
EnvExtension.lean fix: mark failed compilations as noncomputable (#12625) 2026-02-23 09:18:21 +00:00
Environment.lean feat: theorems are opaque (#12973) 2026-03-23 13:57:07 +00:00
ErrorExplanation.lean feat: stricter meta check for temporary programs in native_decide etc (#13005) 2026-03-20 15:51:18 +00:00
Exception.lean refactor: move error explanation text to the manual (#11688) 2025-12-26 17:14:58 +00:00
Expr.lean fix: fix a collection of docstring errors (#12959) 2026-03-19 06:42:11 +00:00
ExtraModUses.lean
HeadIndex.lean
Hygiene.lean
IdentifierSuggestion.lean chore: shake core (#12276) 2026-02-05 09:10:32 +00:00
ImportingFlag.lean
InternalExceptionId.lean chore: shake core (#12276) 2026-02-05 09:10:32 +00:00
KeyedDeclsAttribute.lean chore: be consistent about setting [inline] before compilation (#12389) 2026-03-20 13:46:23 +00:00
LabelAttribute.lean chore: shake core (#12276) 2026-02-05 09:10:32 +00:00
Level.lean chore: deprecate levelZero and levelOne (#12720) 2026-03-04 01:03:08 +00:00
LibrarySuggestions.lean
Linter.lean
LoadDynlib.lean feat: throw an error when export declarations have borrow annotations (#13017) 2026-03-20 23:22:52 +00:00
LocalContext.lean feat: new, extensible do elaborator (#12459) 2026-02-21 17:17:29 +00:00
Log.lean refactor: move error explanation text to the manual (#11688) 2025-12-26 17:14:58 +00:00
Message.lean feat: add structured TraceResult to TraceData (#12698) 2026-03-10 02:42:57 +00:00
Meta.lean feat: unfold and rewrap instances in inferInstanceAs and deriving 2026-03-22 13:25:46 +01:00
MetavarContext.lean fix: fix a collection of docstring errors (#12959) 2026-03-19 06:42:11 +00:00
Modifiers.lean
MonadEnv.lean refactor: ignore borrow annotations at export/extern tricks (#12930) 2026-03-16 10:03:40 +00:00
Namespace.lean fix: namespace used in private import and current module vanishes dowstream (#12840) 2026-03-20 13:27:26 +00:00
OriginalConstKind.lean refactor: move getOriginalConstKind? into its own module to avoid future import cycle (#12265) 2026-02-01 16:18:51 +00:00
Parser.lean
ParserCompiler.lean chore: shake core (#12276) 2026-02-05 09:10:32 +00:00
PrettyPrinter.lean chore: shake core (#12276) 2026-02-05 09:10:32 +00:00
PrivateName.lean
ProjFns.lean fix: detect stuck mvars through auxiliary parent projections (#12564) 2026-02-23 03:46:06 +00:00
ReducibilityAttrs.lean refactor: rename instance_reducible to implicit_reducible (#12567) 2026-02-18 22:19:16 +00:00
Replay.lean refactor: remove Lean.Environment.replay from core (#12972) 2026-03-18 22:11:42 +00:00
ReservedNameAction.lean feat: add structured TraceResult to TraceData (#12698) 2026-03-10 02:42:57 +00:00
ResolveName.lean fix: pretty printing of constants should consider accessibility of names (#12654) 2026-02-25 00:01:19 +00:00
Runtime.lean
ScopedEnvExtension.lean
Server.lean
Setup.lean perf: separate meta and non-meta initializers (#12016) 2026-02-26 08:05:19 +00:00
Shell.lean feat: increase default stack size from 8MB to 1GB (#12971) 2026-03-20 15:40:00 +00:00
Structure.lean chore: use terminology "non-recursive structure" instead of "struct-like" (#12749) 2026-03-09 03:44:38 +00:00
SubExpr.lean chore: shake core (#12276) 2026-02-05 09:10:32 +00:00
Syntax.lean feat: order instances for string positions (#12641) 2026-02-23 08:20:52 +00:00
ToExpr.lean
ToLevel.lean fix: address unused simp theorem warnings (#12829) 2026-03-06 23:12:03 +00:00
Util.lean
Widget.lean