param_solve — the common generalization of rcongr and param_cc

rcongr (RCongr.lean) and param_cc (ParamCongrClosure.lean) are the two evaluation strategies of one underlying object: proof transfer along the Related/Param relation, i.e. deciding Related enc a b in the theory generated by the registered Param witnesses. That generating rule system is

• atoms — registered Related/RelatedBinOp instances + context hypotheses;
• congruence (functoriality) — composeBinOp/rcongrBinOp (R_arrow): from Related enc a a', Related enc b b' infer Related enc (op a b) (bop a' b'). This is the cross-head congruence rule — the same content as a RelatedBinOp square, a @[hgcongr] head-pair lemma, and the Trocq R_arrow combinator;
• equivalence — reflexivity / symmetry / transitivity on the relation.

The two tactics are the two ways to run that system:

tactic	direction	rules	does	misses
rcongr	top-down, goal-directed (lazy, SLD-style)	congruence only, by matching the goal head	descend nested op-trees / binders, leave per-arg subgoals	chain transitively through context (trans is a horizontal combinator, not a descent step)
param_cc	bottom-up, saturating (eager, fixpoint)	congruence + equivalence, to closure	chain refl/sym/trans through context hyps + squares	descend into structure the way the term translation ⟦·⟧ does

Neither subsumes the other operationally: rcongr provably cannot close a pure transitivity goal (ParamCongrClosure.lean pins this with #guard_msgs), and a saturating closure does not itself perform the structural binder/op-tree descent. They are the descent direction and the closure direction of the same relation — exactly the e-graph duality the repo already uses for ZX (Quantum/ZXEgraph): closure is the saturation, congruence-descent is one rewrite applied by matching.

What param_solve is

param_solve is the common generalization: goal-directed cross-head descent (the rcongr strategy) with the saturating closure (param_cc) as the leaf discharger. On a goal Related enc t t' (or an = bridged to one):

1. if t = op a b is a binary op-tree node with a registered RelatedBinOp square, apply the cross-head congruence rule rcongrBinOp, leaving the two per-argument relatedness subgoals, and recurse on each (the descent — rcongr's job, which produces the structural proof term);
2. at a leaf, first try the registry (inferInstance) / rfl; if that fails, fall into the closure paramCCCore (param_cc's job — surface context relatedness hypotheses as equations and saturate with grind), which chains transitivity / context hypotheses that the descent leaf cannot.

So descent handles the structural/op-tree direction param_cc does not expose as subgoals, and closure handles the transitive-context chaining rcongr cannot reach. The result closes the union of the two tactics' goals through a single descent-then-closure-leaf driver. This is param_transfer/⟦·⟧ with a congruence-closure backend — the full Trocq engine, of which the two component tactics are restrictions.

The descent backend

param_solve drives the descent through rcongrBinOp (the in-tree Related/RelatedBinOp congruence rule), so it is self-contained over that database. The attribute-driven, relation-generic descent — hgcongr (HGCongr.lean), keyed on registered head pairs (f, g) — is the pluggable general form of step 1: swapping rcongrBinOp for an hgcongr lookup generalizes the descent to any registered cross-head correspondence without changing the closure leaf. The two-tactic decomposition is the point; the head DB used for descent is a parameter.

Scope: the encoding-relation collapse

Related enc a b is definitionally the encoding equation enc a = b. Over such a relation grind's congruence-closure core is already complete — it performs congruence (as function congruence on enc-images) and equivalence closure — so param_cc alone discharges much of what descent produces, and the descent and closure strategies overlap heavily. The case where the two are independently necessary (neither subsumes the other) is the relation-generic residual: a relation that is not an encoding equation, where congruence must be applied via relation lemmas (no = for grind to stand in on) and equivalence supplied as transitivity/symmetry relation lemmas. There descent and closure are distinct engines, and param_solve's descent-then-closure-leaf shape is the unification. The present file realizes that shape over the encoding relation the in-tree Related admits; the relation-generic procedure (a union-find over a relation equivalence graph, the full Emil Gjørup–Spitters cubical congruence-closure run at the set level) is not implemented here, as in ParamCongrClosure.lean.

def Transfer.paramSolveGuardedStep (recurse : Lean.Elab.Tactic.TacticM Unit) : Lean.Elab.Tactic.TacticM Unit

One guarded descent step on a Related goal: apply rcongrBinOpOn (else rcongrUnOpOn), run recurse on each operand goal, and close the guard with transfer_guard_disch. Fails, leaving the goal unchanged, when no guarded square matches, an operand goal is not closed, or the discharger does not close the guard.

Equations

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

partial def Transfer.paramSolveCore : Lean.Elab.Tactic.TacticM Unit

The unified descent + closure-leaf driver. A TacticM recursion that runs the goal-directed cross-head descent of rcongr and discharges each leaf by the saturating closure of param_cc:

• on Related enc (op a b) (bop a' b') (a binary op-tree node), apply the cross-head congruence rule rcongrBinOp and recurse on the two per-argument relatedness subgoals — the descent;
• on a Related leaf, try the registry (inferInstance) / rfl; on failure, try a guarded square (paramSolveGuardedStep, guard closed by transfer_guard_disch); on failure, invoke paramCCCore — the closure — which surfaces context relatedness hypotheses as equations and saturates with grind, reaching transitivity / context chains the descent leaf cannot;
• on an = goal, bridge to Related id _ _ via transferGround and descend; if the bridge does not apply, discharge directly by the closure.

Each binary step strips one op layer, so the descent is well-founded on op-tree size; the closure leaf is terminal.

def Transfer.tacticParam_solve : Lean.ParserDescr

param_solve — the common generalization of rcongr (descent) and param_cc (closure).

Closes a relatedness goal Related enc t t' (or an = bridged to one) by goal-directed cross-head descent through the registered RelatedBinOp op-tree and the guarded squares RelatedBinOpOn/RelatedUnOpOn (each guard closed by transfer_guard_disch, or the step fails), discharging each leaf by the saturating relational congruence closure (context relatedness hypotheses + registered squares, transitively to a fixpoint via grind). It closes the union of what rcongr and param_cc close — both the structural cross-head op-trees of the former and the transitivity / context chains of the latter — through a single descent-then-closure-leaf strategy. See the module docstring for the rule system both tactics restrict, and the encoding-relation collapse / relation-generic residual.

Equations

• Transfer.tacticParam_solve = Lean.ParserDescr.node `Transfer.tacticParam_solve 1024 (Lean.ParserDescr.nonReservedSymbol "param_solve" false)

Demonstrations: param_solve closes the union

1. Pure cross-head op-tree (the rcongr reach), via descent

2. Pure transitivity (the param_cc reach rcongr cannot do), via closure

The goal Related enc a b from Related enc a c and a separate c = b. Descent does not apply (a is not an op-tree node); the leaf falls into the closure, which surfaces hac.rel : enc a = c and chains through hcb. rcongr provably fails this goal — pinned with #guard_msgs in ParamCongrClosure.lean.

3. Combined: cross-head descent and a closure leaf

A cross-head op-tree whose operands are related to their images only by context hypotheses, with one leaf needing the closure. param_solve descends through the op node (descent) and discharges the operand leaves by the closure (chaining the context relatedness hypotheses + the registered square) — both strategies in one proof.

4. Registered-square composite (no context), via descent + registry leaves

Named witnesses (for axiom-hygiene verification)

theorem Transfer.param_solve_descent_demo (a b c : ExampleField.F) : a * b + c = ExampleField.bbFieldAdd (ExampleField.bbFieldMul a b) c

Named cross-head-descent demo (axiom-hygiene witness for param_solve).

theorem Transfer.param_solve_trans_demo {A α : Type} (enc : A → α) (a : A) (c b : α) (hac : Related enc a c) (hcb : c = b) : Related enc a b

Named transitivity-via-closure demo (axiom-hygiene witness for param_solve). This goal is out of rcongr's reach.

theorem Transfer.param_solve_combined_demo {A α : Type} (enc : A → α) (op : A → A → A) (bop : α → α → α) [RelatedBinOp enc op bop] (a b : A) (a' b'' c : α) (ha : Related enc a a') (hb : Related enc b b'') (hbc : b'' = c) : Related enc (op a b) (bop a' c)

Named combined descent+closure demo (axiom-hygiene witness for param_solve).