The `Transfer` aesop rule set #

This module populates the dedicated Transfer aesop rule set, bundling the transfer machinery (Related/composeBinOp leaf dispatch via transferGround, and the binder-traversing transfer tactic) as aesop rules. The set is opt-in: it is never part of aesop's default rule set, so a plain aesop call carries none of these rules.

What the set contains #

transferGround registered as a safe apply rule. It is the ground leaf closer: it discharges a = b whenever instance resolution synthesizes a Related id a b from the registered RelatedBinOp commuting squares. As a safe rule it applies whenever possible and never needs to be retracted.
transfer (exposed through the transferTac wrapper) registered as an unsafe 50% tactic rule. It performs the automatic binder traversal (∀/λ/Iff-of-∀) and re-dispatches each leaf to the registry, so the Transfer set closes the quantified and function-equality transfer shapes in addition to the ground composite.

The aesop cross-file rule (an API constraint) #

A rule set declared by declare_aesop_rule_sets is not visible in the file that declares it — it becomes visible only in files that import the declaring file (aesop's frontend enforces this; the same reason Mathlib keeps every rule set in a tiny Init.lean/Attr.lean that the main module imports). The set is therefore declared in the separate module AesopRuleSet, which this module imports; the registrations and the aesop (rule_sets := [Transfer]) demonstrations below live here, and any file importing this module can add further rules to the set.

Recipe for a file that imports this module #

public import Transfer.Integrations.AesopIntegration


@[expose] public section
attribute [aesop safe apply (rule_sets := [Transfer])]
  Transfer.transferGround

@[aesop unsafe 50% tactic (rule_sets := [Transfer])]
def myTransferTac : Lean.Elab.Tactic.TacticM Unit := ...   -- or wrap `transfer`

example (a b c : F) : a * b + c = bbFieldAdd (bbFieldMul a b) c := by
  aesop (rule_sets := [Transfer])

Why the set is off by default (the non-fabrication invariant) #

aesop fails open: it runs an open-ended best-first search and only reports failure when the whole search is exhausted. Adding the transfer rules to the default set would let any aesop call search the registry for a commuting square, which could mask a missing square — the failure mode the transfer layer surfaces (see Related.lean's "Scope and limits": the transfer is only as sound as the registered witnesses, and a missing witness must remain a visible residual goal). Keeping the set opt-in (rule_sets := [Transfer]) preserves fail-closed behavior everywhere else: elsewhere aesop neither sees nor silently consumes the transfer rules, so an absent square remains an open goal.

Registering the rules into the `Transfer` set #

The set is declared in AesopRuleSet (imported), so it is visible here and the registrations + the named-set form both work. transferGround (the ground leaf closer) is a safe apply rule; transferCore — the transfer elab's TacticM driver, a global constant — is registered directly as an unsafe tactic rule (no by-block wrapper needed, since the elab exposed a constant).

Demonstrations via the named set `aesop (rule_sets := [Transfer])` #

These run the named Transfer set directly (usable here because this file imports the declaring AesopRuleSet module), and engine-wide in any further importer.

The Transfer aesop rule set #