Module simp 

Simplifier Tactic

Normalizes goals by applying rewrite rules from the context and performing arithmetic evaluation. This is a general-purpose simplification tactic.

Algorithm

The simp tactic works in four steps:

1. Extract hypotheses: Peel implications and extract x = t as rewrites
2. Simplify LHS: Apply substitutions and arithmetic bottom-up
3. Simplify RHS: Apply substitutions and arithmetic bottom-up
4. Compare: Goal succeeds if simplified LHS equals simplified RHS

Supported Simplifications

• Reflexive equalities: Eq a a succeeds immediately
• Constant folding: Eq (add 2 3) 5 simplifies to Eq 5 5
• Hypothesis substitution: Given x = 0, x + 1 becomes 0 + 1 then 1

Arithmetic Operations

Supports add, sub, mul, div, mod on integer literals. Non-literal arithmetic is left unevaluated.

Fuel Limit

Simplification uses a fuel counter to prevent infinite loops from cyclic rewrites. The default fuel is 1000 simplification steps.

Enums

STerm

Simplified representation of Syntax terms for rewriting.

Functions

check_goal

Check if a goal is provable by simplification.

Type Aliases

Substitution

Substitution mapping variable indices to replacement terms.