param_auto — one coordinator over every congruence surface #
Every native Lean relational tactic is congruence for one fixed relation, and the
engine tactics generalize that rule to a registered relation (see
Congruence/RCongr.lean, Examples/StrongExamples.lean). param_auto is the
single entry point that dispatches to all of them: the engine tactics
(param_solve = descent + closure, itself calling grind on the Eq leaves;
rcongr for cross-head descent) and the native relational tactics (norm_cast
for the cast graph, gcongr for ordered congruence, grind for Eq closure).
The point is a stable call site: a proof writes param_auto, and the dispatch
strategy underneath — the order of alternatives, goal-shape-directed routing,
per-relation specialization — can be optimized later without changing any call
site. It is currently a first-cascade; that is the coordinator in its simplest
form. A goal-directed router (inspect the relation head, jump straight to its
optimal solver) is a drop-in replacement behind the same name.
This realizes, as a tactic, the "one engine" picture: the coordinator descends the one graded congruence rule and hands each leaf to the fastest available decision procedure for that leaf's relation.
The coordinator: try each surface in turn. first moves past any alternative
that does not apply to the current goal, so one name closes goals from many
different relations. Optimize the dispatch (order / goal-directed routing)
behind this name without touching call sites.
Equations
- Transfer.tacticParam_auto = Lean.ParserDescr.node `Transfer.tacticParam_auto 1024 (Lean.ParserDescr.nonReservedSymbol "param_auto" false)
Instances For
One tactic, four relations #
Each goal below is congruence for a different fixed relation; param_auto
routes each to a surface that closes it.