Expand description
simp rule sets: oriented rewrite rules compiled from proved lemmas,
indexed for fast lookup, instantiated by matching.
A simp rule is a lemma of shape ∀x₁…xₙ. C₁ → … → Cₖ → lhs = rhs (or
… lhs ↔ rhs), oriented left-to-right. Orientation is enforced at
registration: vars(rhs) ⊆ vars(lhs), vars(Cᵢ) ⊆ vars(lhs), and lhs
is not a bare variable — so matching the lhs against a goal subterm
determines the entire instantiation.
The tactic layer (crate::tactic::ProofState::simp) drives the rewrite
loop; this module finds one certified step at a time. Each step’s equality
carries its own derivation — PremiseMatch on the ∀-lemma, a
InferenceRule::UniversalInstTerm chain for the instantiation,
ModusPonens per discharged condition — so the kernel re-checks every
rewrite like any hand-written proof. Nothing here is trusted.
Structs§
- SimpSet
- An indexed set of simp rules.