max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2
lean4-htt/src/Init
History
Joe Hendrix ac7b95da86
feat: port Batteries.WF for executable well-founded fixpoints (#11620) 
This PR ports Batteries.WF to Init.WFC for executable well-founded
fixpoints. It introduces `csimp` theorems to replace the recursors and
non-executable definitions with executable definitions.

This ocassionally comes up on Zulip as it prevents admiting definitions
generated from well-founded induction. (e.g., [#lean4 > Computable
WellFounded.fix](https://leanprover.zulipchat.com/#narrow/channel/270676-lean4/topic/Computable.20WellFounded.2Efix/with/529347861)
and [#mathlib4 > Why Nat.find is computable, when Wellfounded.fix
isn't?](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Why.20Nat.2Efind.20is.20computable.2C.20when.20Wellfounded.2Efix.20isn't.3F/with/545143617)).

This was motivated by running into poor elaboration performance with
recursive definitions involving complex inductive types generated by a
custom elaborator. It would be helpful to explore bypassing the
elaborator and generating elaborated terms directly, but this requires
an executable fixpoint (such as `WellFounded.fixC` introduced in
batteries).
2025-12-12 18:22:54 +00:00
..
Control feat: add lemmas about EStateM.run (#11600) 2025-12-12 03:00:17 +00:00
Data feat: lint coercions that are deprecated or banned in core (#11511) 2025-12-12 15:09:13 +00:00
Grind chore: remove ≥6 month old deprecations (#11627) 2025-12-12 10:40:04 +00:00
GrindInstances feat: improves Fin n support in grind (#11319) 2025-11-22 06:51:25 +00:00
Internal refactor: make CCPO class Prop-valued (#11425) 2025-12-04 13:33:36 +00:00
Meta chore: rename Substring to Substring.Raw (#11154) 2025-11-16 09:30:04 +00:00
Omega chore: deprecate more duplications (#11004) 2025-10-30 05:58:29 +00:00
System chore: fix spelling (#11531) 2025-12-06 13:54:27 +00:00
BinderNameHint.lean chore: remove redundant imports in core (#10750) 2025-10-16 20:27:46 +00:00
BinderPredicates.lean feat: make private the default in module (#9044) 2025-06-28 16:30:53 +00:00
ByCases.lean chore: deprecate more duplications (#11004) 2025-10-30 05:58:29 +00:00
Classical.lean feat: grind_pattern for Exists.choose_spec (#11316) 2025-11-22 02:19:00 +00:00
Coe.lean doc: fix typo in Init.Coe module docstring (#11567) 2025-12-10 08:48:55 +00:00
Control.lean chore: remove public section from end of files (#10684) 2025-10-06 13:30:48 +00:00
Conv.lean feat: add enter [in patt] syntax (#10081) 2025-08-23 17:16:53 +00:00
Core.lean feat: @[suggest_for] annotations for prompting easy-to-miss names (#11554) 2025-12-10 22:50:45 +00:00
Data.lean chore: more reorganization of strings (#10928) 2025-10-23 11:56:11 +00:00
Dynamic.lean perf: do not export opaque bodies (#10119) 2025-08-27 20:59:59 +00:00
Ext.lean chore: add deprecations for duplicated theorems (#10967) 2025-10-29 05:26:16 +00:00
GetElem.lean feat: add mem_of_get_eq and of_getElem_eq (#11452) 2025-12-02 15:00:00 +00:00
Grind.lean feat: Field norm num (#11350) 2025-11-25 19:47:31 +00:00
GrindInstances.lean chore: remove public section from end of files (#10684) 2025-10-06 13:30:48 +00:00
Guard.lean chore: remove redundant imports in core (#10750) 2025-10-16 20:27:46 +00:00
Hints.lean feat: make private the default in module (#9044) 2025-06-28 16:30:53 +00:00
Internal.lean feat: make private the default in module (#9044) 2025-06-28 16:30:53 +00:00
LawfulBEqTactics.lean chore: remove redundant imports in core (#10750) 2025-10-16 20:27:46 +00:00
MacroTrace.lean feat: make private the default in module (#9044) 2025-06-28 16:30:53 +00:00
Meta.lean chore: remove redundant imports in core (#10750) 2025-10-16 20:27:46 +00:00
MetaTypes.lean feat: simp? +suggestions (#11032) 2025-11-03 03:26:16 +00:00
MethodSpecsSimp.lean feat: @[method_specs_simp] in Init (#10407) 2025-09-16 10:27:33 +00:00
Notation.lean fix: better performance for @[suggest_for] (#11598) 2025-12-11 15:21:33 +00:00
NotationExtra.lean chore: remove redundant imports in core (#10750) 2025-10-16 20:27:46 +00:00
Omega.lean chore: remove public section from end of files (#10684) 2025-10-06 13:30:48 +00:00
Prelude.lean feat: @[suggest_for] annotations for prompting easy-to-miss names (#11554) 2025-12-10 22:50:45 +00:00
PropLemmas.lean chore: remove ≥6 month old deprecations (#11627) 2025-12-12 10:40:04 +00:00
RCases.lean chore: remove redundant imports in core (#10750) 2025-10-16 20:27:46 +00:00
ShareCommon.lean chore: remove redundant imports in core (#10750) 2025-10-16 20:27:46 +00:00
SimpLemmas.lean fix: performance issue when elaborating match-expressions with many literals (#9372) 2025-07-15 03:52:23 +00:00
Simproc.lean chore: more module system fixes and improvements from Mathlib porting (#10655) 2025-10-08 11:30:09 +00:00
SizeOf.lean chore: rename Substring to Substring.Raw (#11154) 2025-11-16 09:30:04 +00:00
SizeOfLemmas.lean chore: remove redundant imports in core (#10750) 2025-10-16 20:27:46 +00:00
Syntax.lean feat: make private the default in module (#9044) 2025-06-28 16:30:53 +00:00
System.lean chore: remove public section from end of files (#10684) 2025-10-06 13:30:48 +00:00
Tactics.lean feat: add +all option to exact? and apply? (#11556) 2025-12-11 03:30:52 +00:00
TacticsExtra.lean chore: remove redundant imports in core (#10750) 2025-10-16 20:27:46 +00:00
Task.lean fix: revert the waitAny refactoring (#11000) 2025-10-29 08:27:16 +00:00
Try.lean feat: exact? +grind and exact? +try? discharger options (#11469) 2025-12-02 06:31:56 +00:00
Util.lean chore: reorganize Init imports around strings (#10289) 2025-09-07 17:09:14 +00:00
WF.lean feat: port Batteries.WF for executable well-founded fixpoints (#11620) 2025-12-12 18:22:54 +00:00
WFComputable.lean feat: port Batteries.WF for executable well-founded fixpoints (#11620) 2025-12-12 18:22:54 +00:00
WFExtrinsicFix.lean feat: remove Finite conditions from iterator consumers relying on a new fixpoint combinator (#11038) 2025-12-08 16:03:22 +00:00
WFTactics.lean chore: remove redundant imports in core (#10750) 2025-10-16 20:27:46 +00:00
While.lean fix: move the monad argument for ForIn, ForIn', and ForM (#10204) 2025-11-25 12:20:37 +00:00