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 8655f7706f
refactor: structural recursion: prove .eq_def directly (#10606) 
This PR changes how Lean proves the equational theorems for structural
recursion. The core idea is to let-bind the `f` argument to `brecOn` and
rewriting `.brecOn` with an unfolding theorem. This means no extra case
split for the `.rec` in `.brecOn` is needed, and `simp` doesn't change
the `f` argument which can break the definitional equality with the
defined function. With this, we can prove the unfolding theorem first,
and derive the equational theorems from that, like for all other ways of
defining recursive functions.

Backs out the changes from #10415, the old strategy works well with the
new goals.

Fixes #5667
Fixes #10431
Fixes #10195
Fixes #2962
2025-10-07 12:53:09 +00:00
..
Compiler fix: RC dec insertion for unused variables (#10689) 2025-10-06 22:05:17 +00:00
Data chore: remove public section from end of files (#10684) 2025-10-06 13:30:48 +00:00
DocString chore: rename String.Pos to String.Pos.Raw (#10624) 2025-10-01 07:45:24 +00:00
Elab refactor: structural recursion: prove .eq_def directly (#10606) 2025-10-07 12:53:09 +00:00
ErrorExplanations feat: overhaul meta system (#10362) 2025-09-17 21:04:29 +00:00
Language chore: module system fixes and refinements from Mathlib porting (#10643) 2025-10-02 08:28:08 +00:00
Linter fix: some ExtraModUses (#10620) 2025-10-03 15:50:40 +00:00
Meta refactor: structural recursion: prove .eq_def directly (#10606) 2025-10-07 12:53:09 +00:00
Parser fix: some ExtraModUses (#10620) 2025-10-03 15:50:40 +00:00
ParserCompiler fix: some ExtraModUses (#10620) 2025-10-03 15:50:40 +00:00
PremiseSelection feat: helper functions for premise selection API (#10512) 2025-09-24 11:45:40 +00:00
PrettyPrinter chore: remove public section from end of files (#10684) 2025-10-06 13:30:48 +00:00
Server chore: remove public section from end of files (#10684) 2025-10-06 13:30:48 +00:00
Util doc: fix url to profile.ts source (#10628) 2025-10-07 12:41:04 +00:00
Widget test: improve language server test coverage (#10574) 2025-09-30 11:15:03 +00:00
AddDecl.lean chore: module system fixes and refinements from Mathlib porting (#10643) 2025-10-02 08:28:08 +00:00
Attributes.lean chore: module system fixes and refinements from Mathlib porting (#10643) 2025-10-02 08:28:08 +00:00
AuxRecursor.lean refactor: module-ize Lean (#9330) 2025-07-25 12:02:51 +00:00
BuiltinDocAttr.lean feat: docstrings with Verso syntax (#10307) 2025-09-10 07:03:57 +00:00
Class.lean refactor: update and consolidate attribute-related error messages (#9495) 2025-07-26 02:03:18 +00:00
Compiler.lean chore: remove public section from end of files (#10684) 2025-10-06 13:30:48 +00:00
CoreM.lean fix: backtracking kernel errors under Elab.async (#10438) 2025-09-18 12:33:57 +00:00
Data.lean chore: remove public section from end of files (#10684) 2025-10-06 13:30:48 +00:00
Declaration.lean refactor: module-ize Lean (#9330) 2025-07-25 12:02:51 +00:00
DeclarationRange.lean feat: default let rec and where decls to private under the module system (#9759) 2025-08-06 15:53:51 +00:00
DefEqAttrib.lean perf: clarify and granularize access to async env ext state (#9587) 2025-08-02 17:01:08 +00:00
DocString.lean refactor: module-ize Lean (#9330) 2025-07-25 12:02:51 +00:00
Elab.lean chore: remove public section from end of files (#10684) 2025-10-06 13:30:48 +00:00
EnvExtension.lean feat: shake import minimizer aware of the module system and arbitrary elaboration dependencies (#10575) 2025-09-28 16:00:00 +00:00
Environment.lean feat: shake import minimizer aware of the module system and arbitrary elaboration dependencies (#10575) 2025-09-28 16:00:00 +00:00
ErrorExplanation.lean feat: add useful functions in Parsec, add error variant and Std.Data.ByteSlice (#9599) 2025-09-11 14:53:41 +00:00
ErrorExplanations.lean chore: remove public section from end of files (#10684) 2025-10-06 13:30:48 +00:00
Exception.lean feat: docstrings with Verso syntax (#10307) 2025-09-10 07:03:57 +00:00
Expr.lean fix: make getArg!' compute the correct arg index to access (#10567) 2025-09-26 11:54:49 +00:00
ExtraModUses.lean feat: shake import minimizer aware of the module system and arbitrary elaboration dependencies (#10575) 2025-09-28 16:00:00 +00:00
HeadIndex.lean refactor: module-ize Lean (#9330) 2025-07-25 12:02:51 +00:00
Hygiene.lean perf: make macro scope numbering less dependent on surrounding context (#10027) 2025-08-22 13:16:02 +00:00
ImportingFlag.lean chore: miscellaneous documentation typos (#10009) 2025-08-20 21:39:03 +00:00
InternalExceptionId.lean chore: reorganize Init imports around strings (#10289) 2025-09-07 17:09:14 +00:00
KeyedDeclsAttribute.lean fix: some ExtraModUses (#10620) 2025-10-03 15:50:40 +00:00
LabelAttribute.lean chore: reorganize Init imports around strings (#10289) 2025-09-07 17:09:14 +00:00
Level.lean fix: complete overhaul of structural recursion on inductives predicates (#9995) 2025-09-01 08:17:58 +00:00
Linter.lean chore: remove public section from end of files (#10684) 2025-10-06 13:30:48 +00:00
LoadDynlib.lean fix: do not allow access to private primitives in public scope (#9890) 2025-08-14 15:34:54 +00:00
LocalContext.lean feat: clean up type annotations when elaborating declaration bodies (#9674) 2025-08-18 04:43:20 +00:00
Log.lean chore: rename String.Pos to String.Pos.Raw (#10624) 2025-10-01 07:45:24 +00:00
Message.lean refactor: module-ize Lean (#9330) 2025-07-25 12:02:51 +00:00
Meta.lean feat: @[method_specs] to generate specification theorems from class instances (#10302) 2025-09-15 11:17:06 +00:00
MetavarContext.lean fix: remove superfluous Monad instances from some spec lemmas (#10564) (#10618) 2025-09-29 15:02:43 +00:00
Modifiers.lean fix: privacy checks and import all (#10550) 2025-09-26 13:26:10 +00:00
MonadEnv.lean chore: module system fixes and refinements from Mathlib porting (#10643) 2025-10-02 08:28:08 +00:00
Namespace.lean refactor: module-ize Lean (#9330) 2025-07-25 12:02:51 +00:00
Parser.lean feat: add unicode(...) parser syntax and pp.unicode option (#10373) 2025-09-14 04:40:03 +00:00
ParserCompiler.lean chore: minor module system fixes from batteries port (#10496) 2025-09-24 08:59:23 +00:00
PremiseSelection.lean feat: basic premise selection algorithm based on MePo (#7844) 2025-09-23 06:40:22 +00:00
PrettyPrinter.lean perf: shorten rebuild critical path by 19% (#9626) 2025-08-01 11:18:21 +00:00
PrivateName.lean refactor: module-ize Lean (#9330) 2025-07-25 12:02:51 +00:00
ProjFns.lean refactor: module-ize Lean (#9330) 2025-07-25 12:02:51 +00:00
ReducibilityAttrs.lean chore: use ofConstName in error messages (#10121) 2025-08-25 23:20:36 +00:00
Replay.lean refactor: module-ize Lean (#9330) 2025-07-25 12:02:51 +00:00
ReservedNameAction.lean refactor: module-ize Lean (#9330) 2025-07-25 12:02:51 +00:00
ResolveName.lean fix: privacy checks and import all (#10550) 2025-09-26 13:26:10 +00:00
Runtime.lean refactor: module-ize Lean (#9330) 2025-07-25 12:02:51 +00:00
ScopedEnvExtension.lean feat: change delimiting of local attributes in implicit sections (#9968) 2025-08-28 15:48:42 +00:00
Server.lean chore: remove public section from end of files (#10684) 2025-10-06 13:30:48 +00:00
Setup.lean feat: shake import minimizer aware of the module system and arbitrary elaboration dependencies (#10575) 2025-09-28 16:00:00 +00:00
Shell.lean refactor: port more of shell.cpp to Lean (#10086) 2025-08-26 20:02:42 +00:00
Structure.lean chore: error messages consistency (#10143) 2025-08-26 17:55:43 +00:00
SubExpr.lean refactor: module-ize Lean (#9330) 2025-07-25 12:02:51 +00:00
Syntax.lean chore: rename String.Pos to String.Pos.Raw (#10624) 2025-10-01 07:45:24 +00:00
ToExpr.lean chore: kernel changes ahead of String redefinition (#10330) 2025-09-17 09:12:07 +00:00
ToLevel.lean refactor: module-ize Lean (#9330) 2025-07-25 12:02:51 +00:00
Util.lean chore: remove public section from end of files (#10684) 2025-10-06 13:30:48 +00:00
Widget.lean chore: remove public section from end of files (#10684) 2025-10-06 13:30:48 +00:00