Ground Term Evaluation for Sym.simp

This module provides simplification procedures (Simproc) for evaluating ground terms of builtin types. It is designed for the Sym.Simp simplifier and addresses performance issues in the standard Meta.Simp simprocs.

Design Differences from Meta.Simp Simprocs

1. Pure Value Extraction

It uses the pure getValue? functions defined in Lean.Meta.Sym.LitValues.

2. Proof by Definitional Equality

All evaluation steps produce Eq.refl proofs and. The kernel verifies correctness by checking that the input and output are definitionally equal.

3. Specialized Lemmas for Predicates

Predicates (<, ≤, =, etc.) use specialized lemmas that short-circuit the standard decide proof chain:

-- Standard approach (Meta.Simp)
eq_true (of_decide_eq_true (h : decide (a < b) = true)) : (a < b) = True

-- Specialized lemma (Sym.Simp)
theorem Int.lt_eq_true (a b : Int) (h : decide (a < b) = true) : (a < b) = True :=
  eq_true (of_decide_eq_true h)

The simproc applies the lemma directly with rfl for h:

Int.lt_eq_true 5 7 rfl : (5 < 7) = True

This avoids reconstructing Decidable instances at each call site.

4. Maximal Sharing

Results are passed through share to maintain the invariant that structurally equal subterms have pointer equality. This enables O(1) cache lookup in the simplifier.

5. Type Dispatch via match_expr

Operations dispatch on the type expression directly. It assumes non-standard instances are not used.

TODO: additional bit-vector operations, Char, String support

def Lean.Meta.Sym.Simp.commandDeclare_eval_bin__ : ParserDescr

Equations

• One or more equations did not get rendered due to their size.

def Lean.Meta.Sym.Simp.commandDeclare_eval_bin_bitwise__ : ParserDescr

Equations

• One or more equations did not get rendered due to their size.

def Lean.Meta.Sym.Simp.commandDeclare_eval_bin_bool_pred__ : ParserDescr

Equations

• One or more equations did not get rendered due to their size.

structure Lean.Meta.Sym.Simp.EvalStepConfig : Type

• maxExponent : Nat

def Lean.Meta.Sym.Simp.evalGround (config : EvalStepConfig := { }) : Simproc

Simplification procedure that evaluates ground terms of builtin types.

Important: This procedure assumes subterms have already been simplified. It evaluates a single operation on literal arguments only. For example:

• 2 + 3 → evaluates to 5
• 2 + (3 * 4) → returns .rfl (the argument 3 * 4 is not a literal)

The simplifier is responsible for term traversal, ensuring subterms are reduced before evalGround is called on the parent expression.

Equations

• One or more equations did not get rendered due to their size.