Simp pipeline in Lean on a high level

Stream: lean4

[Lukas Stevens]

Hi, we had a small Isabelle hackathon here in Munich yesterday where we tried to add top-down simprocs to Isabelle (in addition to bottom-up simprocs). One inspiration for this feature was that they exist in Lean where you can parametrise a simproc by an up or down arrow. During this project I was wondering how the simp pipeline in Lean looks like on a high level and which consideration went into the design of the pipeline?

For reference, Isabelle starts descending into the term during a top-down phase and then proceeds symmetrically with a bottom-up phase:

Top-down

• congruence rules
• (new) top-down simprocs

Bottom-up

• rewrite rules
• conditional rewrite rules
• bottom-up simprocs
• solver
• looper