max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2
lean4-htt/src/Init
History
Leonardo de Moura 6a87c0e530
feat: add Sym.Simp.evalGround simproc (#12031) 
This PR adds `Sym.Simp.evalGround`, a simplification procedure for
evaluating ground terms of builtin numeric types. It is designed for
`Sym.simp`.

Key design differences from `Meta.Simp` simprocs:

- Pure value extraction: `getValue?` functions are `OptionT Id` rather
than
`MetaM`, avoiding `whnf` overhead since `Sym` maintains canonical forms
- Specialized predicate lemmas: comparisons use pre-proved lemmas like
  `Int.lt_eq_true` applied with `rfl`, avoiding `Decidable` instance
  reconstruction at each call site
- Type dispatch via `match_expr`: assumes standard instances, no
synthesis

Supported types: `Nat`, `Int`, `Rat`, `Fin n`, `BitVec n`,
`UInt8/16/32/64`,
`Int8/16/32/64`.

Supported operations: arithmetic (`+`, `-`, `*`, `/`, `%`, `^`), bitwise
(`&&&`, `|||`, `^^^`, `~~~`), shifts (`<<<`, `>>>`), comparisons (`<`,
`≤`,
`>`, `≥`, `=`, `≠`, `∣`), and boolean predicates (`==`, `!=`).
2026-01-17 05:13:12 +00:00
..
Control style: fix typos in Init/ and Std/ docstrings (#11864) 2026-01-09 07:24:07 +00:00
Data feat: add grind annotations for list and array slices (#11993) 2026-01-15 16:43:10 +00:00
Grind chore: remove superfluous (generalizing := false) after revert of #11696 (#11952) 2026-01-09 10:14:18 +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
Sym feat: add Sym.Simp.evalGround simproc (#12031) 2026-01-17 05:13:12 +00:00
System style: fix typos in Init/ and Std/ docstrings (#11864) 2026-01-09 07:24:07 +00:00
BinderNameHint.lean chore: remove redundant imports in core (#10750) 2025-10-16 20:27:46 +00:00
BinderPredicates.lean
ByCases.lean chore: deprecate more duplications (#11004) 2025-10-30 05:58:29 +00:00
Classical.lean style: fix typos in Init/ and Std/ docstrings (#11864) 2026-01-09 07:24:07 +00:00
Coe.lean doc: fix typo in Init.Coe module docstring (#11567) 2025-12-10 08:48:55 +00:00
Control.lean feat: MonadAttach (#11532) 2025-12-16 18:57:00 +00:00
Conv.lean feat: add enter [in patt] syntax (#10081) 2025-08-23 17:16:53 +00:00
Core.lean perf: faster T.ctor.injEq generation using substVars and some curry (#11998) 2026-01-13 23:02:18 +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 guards for grind patterns for getElem?_eq_none theorems (#11761) 2026-01-05 08:55:02 +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
Internal.lean
LawfulBEqTactics.lean chore: remove redundant imports in core (#10750) 2025-10-16 20:27:46 +00:00
MacroTrace.lean
Meta.lean chore: remove redundant imports in core (#10750) 2025-10-16 20:27:46 +00:00
MetaTypes.lean chore: don't extract standalone constants as closed terms (#12027) 2026-01-16 14:52:14 +00:00
MethodSpecsSimp.lean feat: @[method_specs_simp] in Init (#10407) 2025-09-16 10:27:33 +00:00
Notation.lean style: fix typos in Init/ and Std/ docstrings (#11864) 2026-01-09 07:24:07 +00:00
NotationExtra.lean style: fix typos in Init/ and Std/ docstrings (#11864) 2026-01-09 07:24:07 +00:00
Omega.lean chore: remove public section from end of files (#10684) 2025-10-06 13:30:48 +00:00
Prelude.lean chore: don't extract standalone constants as closed terms (#12027) 2026-01-16 14:52:14 +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 feat: simpForall and simpArrow in Sym.simp (#11950) 2026-01-09 06:20:04 +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
Sym.lean feat: add Sym.Simp.evalGround simproc (#12031) 2026-01-17 05:13:12 +00:00
Syntax.lean
System.lean chore: remove public section from end of files (#10684) 2025-10-06 13:30:48 +00:00
Tactics.lean fix: pretty-printing of the extract_lets tactic (#12006) 2026-01-14 15:11:09 +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: add first_par combinator for try? with grind +locals (#11949) 2026-01-09 21:09:41 +00:00
Util.lean chore: reorganize Init imports around strings (#10289) 2025-09-07 17:09:14 +00:00
WF.lean style: fix typos in Init/ and Std/ docstrings (#11864) 2026-01-09 07:24:07 +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