param_transfer, end-to-end ∀-transfer

This module is the term-level transfer capstone for the ∀-fragment of the Param engine. It closes the last manual seam in ParamTransfer.lean: forallTransfer there required the caller to name the domain Param .map0 .map2a A A'. Here the domain witness is synthesized by instance resolution through a small TransferDom class, and a param_transfer tactic applies the abstraction-theorem ∀-rule (forallTransfer) so the caller writes nothing structural — no commuting square, no domain relation, no Param term.

The two levels and why TransferDom (not HasParam)

ParamSynth.HasParam resolves witnesses at the fixed self-relation level (.map1, .map1) (forward + backward maps, used for the arrow/app rule). But the ∀-rule forallTransfer consumes the domain at (.map0, .map2a) (forward nothing, backward a section A' → A + map_in_R) — the univalence-free level that Map1_forall needs. These levels are incomparable in the obvious direction, so the ∀-rule gets its own resolver: TransferDom A A' carries a Param .map0 .map2a A A', with instances for

• the diagonal TransferDom A A (graph Eq, via paramDiag) — so same-type ∀-transfer resolves with no caller input; and
• the Num ↦ ℕ change-of-representation TransferDom Num ℕ (graph of the cast, via paramNumNat) — so a change of representation resolves too.

What it delivers

With TransferDom resolving the domain, forallTransferAuto and the param_transfer tactic reduce a goal (∀ a, P a) → (∀ a', P' a') to the pointwise obligation ∀ a a' (_ : dom.R a a'), P a → P' a' — the only content the caller supplies, and on related pairs it is usually closed by intro/assumption/exact. The domain Param, the reflection through ULift/PLift, and the abstraction-theorem combinator are all invisible.

What is not implemented here is the full ⟦t⟧ translation over arbitrary terms: a constant database (@[param]) plus app/lam recursion beyond ∀-statements, i.e. the MetaM/Elpi-style synthesizer that infers the Param witnesses and per-subterm (m, n) levels for any term, not just the universally-quantified Prop-fragment handled here.

TransferDom: the domain Param at the ∀-rule level, by resolution

class Transfer.Param.TransferDom (A A' : Type u) : Type u

TransferDom A A' carries the domain Param .map0 .map2a A A' that the abstraction-theorem ∀-rule (forallTransfer) consumes. Resolution of this class is what makes the domain witness automatic: the caller of param_transfer never names it. The level is (.map0, .map2a) — the univalence-free level Map1_forall requires — deliberately distinct from HasParam's (.map1, .map1) self-relation level.

• dom : Param MapClass.map0 MapClass.map2a A A'

@[instance_reducible]

instance Transfer.Param.instTransferDomDiag (A : Type u) : TransferDom A A

The diagonal instance: same-type ∀-transfer resolves automatically. The domain Param is paramDiag (graph Eq), so on related pairs (a, a') the relation is a = a' and the pointwise obligation is ∀ a, P a → P' a.

Equations

• Transfer.Param.instTransferDomDiag A = { dom := Transfer.Param.paramDiag }

@[instance_reducible]

instance Transfer.Param.instTransferDomNumNat : TransferDom Num ℕ

The Num ↦ ℕ instance: a change of representation resolves automatically. The domain Param is paramNumNat (graph of the cast Num → ℕ), so on related pairs (n, k) the relation is (n : ℕ) = k.

Equations

• Transfer.Param.instTransferDomNumNat = { dom := Transfer.Param.paramNumNat }

forallTransferAuto: forallTransfer with the domain resolved

theorem Transfer.Param.forallTransferAuto {A A' : Type u} [TransferDom A A'] {P : A → Prop} {P' : A' → Prop} (PB : ∀ (a : A) (a' : A'), TransferDom.dom.R a a' → P a → P' a') : (∀ (a : A), P a) → ∀ (a' : A'), P' a'

forallTransfer with the domain Param synthesized by TransferDom.

Identical to forallTransfer except the domain witness is not an explicit argument — it is resolved from TransferDom A A'. The only argument the caller supplies is the pointwise implication PB, stated against the resolved relation (TransferDom.dom).R.

The param_transfer tactic

param_transfer refines the goal by forallTransferAuto, which resolves the domain Param via TransferDom and leaves the pointwise obligation. The caller then discharges that obligation (typically intro/assumption/exact), with no structural relation named.

def Transfer.Param.tacticParam_transfer : Lean.ParserDescr

Close (or reduce) a goal (∀ a, P a) → (∀ a', P' a') by the abstraction-theorem ∀-rule with the domain Param synthesized via TransferDom. Leaves the pointwise obligation ∀ a a' (_ : (TransferDom.dom).R a a'), P a → P' a'.

Equations

• Transfer.Param.tacticParam_transfer = Lean.ParserDescr.node `Transfer.Param.tacticParam_transfer 1024 (Lean.ParserDescr.nonReservedSymbol "param_transfer" false)

End-to-end auto demos — the caller names nothing structural

Each demo below transfers a universally-quantified statement with the domain Param resolved automatically by TransferDom. The only thing written by hand is the pointwise part, closed by intro/exact/assumption.

Same-type ↔ via the engine, domain auto-resolved

For completeness, the biconditional engine forall_iff_transfer_engine is a same-type result; here we expose that the diagonal domain it uses is exactly the one TransferDom resolves, so the ↔-fragment is auto-domain too.