Auto-weakening of witnesses + a unified transfer entry

ParamWeaken.lean proves the lattice action Param.weaken : Param m n A B → m' ⊑ m → n' ⊑ n → Param m' n' A B and weaken_lands_below (synthesize-high, use-low). ParamResolve.lean consults it for a hardcoded candidate list. This module supplies two things at the surface level:

1. Auto-weakening (upstream's Trocq Use "all sub-class versions")

Upstream Trocq, on registering a relatedness lemma, synthesizes every lattice-below class version so a goal at a lower class resolves without the user restating the lemma. This module mirrors that two ways:

• allWeakenings (the enumerating function): given a witness at (m, n), returns the full below-set {(m', n', Param m' n' A B) | m' ⊑ m, n' ⊑ n}, each entry produced by Param.weaken. belowList/mem_belowList give the decidable below-set with its membership characterization.
• RegisteredParam (a sibling registry typeclass, distinct from paramExt): carries one witness at its strongest available class (m, n) (the level pair is an outParam, recovered from (A, B)). The tactic auto_weaken then closes a goal at any lattice-lower (m', n') by Param.weaken (by decide) (by decide) RegisteredParam.reg — the user registers once, at the strong level, and lower-class goals resolve with no hand-written lower witness.

Param.weaken is the engine; this module is the surface that makes "register high, use low" automatic.

2. A unified transfer entry — transfer_auto

param_transfer (the ∀-rule) and the R_arrow app-rule are separate surface entries. transfer_auto is a single tactic dispatching both:

• a ∀-implication goal (∀ a, P a) → (∀ a', P' a') runs the abstraction-theorem ∀-rule with the domain Param resolved by TransferDom (forallTransferAuto), falling back to an explicit-domain forallTransfer;
• an R_arrow PA PB f f' relatedness goal peels to its pointwise codomain obligation (the app-rule content).

It runs the translation at a fixed output class (the univalence-free Prop-motive level the ∀/arrow combinators consume). Per-subterm level inference — picking the minimal output class per occurrence — is the job of the constraint-graph solver inferParamLevels in ParamInfer.lean; that solver generalizes the fixed class choice here (its inferRootClass is exactly the class transfer_auto would synthesize at, then Param.weaken down). This file documents that consumption point; it does not duplicate the solver.

Part 1a — allWeakenings: enumerate every lattice-below class version

def Transfer.Param.allClasses : List MapClass

The six structure classes, in ascending lattice order.

Equations

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

def Transfer.Param.belowList (m : MapClass) : List MapClass

The decidable below-set of a class m: every class m' ⊑ m.

Equations

• Transfer.Param.belowList m = List.filter (fun (m' : Transfer.Param.MapClass) => m'.le m) Transfer.Param.allClasses

theorem Transfer.Param.mem_belowList {m' m : MapClass} (h : m'.le m = true) : m' ∈ belowList m

Membership in belowList m is exactly the lattice order m' ⊑ m.

theorem Transfer.Param.belowList_le {m' m : MapClass} (h : m' ∈ belowList m) : m'.le m = true

The converse: anything in belowList m really is ⊑ m.

def Transfer.Param.allWeakenings {m n : MapClass} {A B : Type u} (p : Param m n A B) : List ((m' : MapClass) × (n' : MapClass) × Param m' n' A B)

All sub-class versions of a witness. Given a Param m n A B, synthesize every lattice-below class version (m', n', Param m' n' A B) via Param.weaken. This is the data-level analogue of upstream's Trocq Use "register every sub-class version": one registration at (m, n) materialises the whole below-set, so a consumer at any lower class has a witness ready.

Equations

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

Part 1b — RegisteredParam + auto_weaken: register high, resolve low

RegisteredParam A B m n is a sibling registry typeclass (independent of ParamDB.paramExt): it carries one witness at the strongest class (m, n) a type pair offers, with (m, n) an outParam so resolution recovers it from (A, B). The auto_weaken tactic then closes a goal at any lattice-lower (m', n') from that single registration.

class Transfer.Param.RegisteredParam (A B : Type u) (m n : outParam MapClass) : Type u

A sibling registry typeclass carrying a Param m n A B witness at the strongest available class for the pair (A, B). The level pair (m, n) is an outParam, recovered during resolution — the user registers once, at the strong level. Deliberately NOT ParamDB.paramExt: this is the lattice auto-weakening registry, a sibling mechanism.

• reg : Param m n A B

  The registered witness, at the strongest available class.

def Transfer.Param.tacticAuto_weaken : Lean.ParserDescr

Close a Param m' n' A B goal by auto-weakening a registered witness. Resolves RegisteredParam A B m n (the strong registration) and applies Param.weaken down to the goal's (m', n'), discharging the ⊑ side conditions by decide. The user never writes the lower-class witness.

Equations

• Transfer.Param.tacticAuto_weaken = Lean.ParserDescr.node `Transfer.Param.tacticAuto_weaken 1024 (Lean.ParserDescr.nonReservedSymbol "auto_weaken" false)

Part 1 — demonstrations of auto-weakening

A single witness is registered at a high class (map3, map0) (the embedding shape), closing goals at strictly lower classes automatically — no hand-written lower-class witness.

@[instance_reducible]

instance Transfer.Param.regNatNat : RegisteredParam ℕ ℕ MapClass.map3 MapClass.map0

A concrete registration at the high class (map3, map0): the diagonal on Nat as the graph of id (forward map3, backward map0). This stands in for any strong witness one would register.

Equations

• Transfer.Param.regNatNat = { reg := { R := Eq, fwd := { map := id, map_in_R := ⋯, R_in_map := ⋯ }, bwd := { } } }

Part 2 — the unified transfer tactic transfer_auto

A single entry subsuming the per-shape param_transfer (∀-rule) and the R_arrow app-rule. It runs at the fixed univalence-free output class the ∀/arrow combinators consume; ParamInfer.inferRootClass generalizes the class choice (see the module docstring).

def Transfer.Param.tacticTransfer_auto : Lean.ParserDescr

Unified transfer. For the goal's shape:

• a ∀-implication goal runs the abstraction-theorem ∀-rule with the domain Param resolved by TransferDom (forallTransferAuto), or an explicit domain (forallTransfer);
• an R_arrow PA PB f f' relatedness goal peels to its pointwise codomain obligation (the app-rule). The caller then discharges the residual pointwise content.

Equations

• Transfer.Param.tacticTransfer_auto = Lean.ParserDescr.node `Transfer.Param.tacticTransfer_auto 1024 (Lean.ParserDescr.nonReservedSymbol "transfer_auto" false)

∀-goal demos (the abstraction-theorem rule, domain auto-resolved)

Arrow-goal demo (the R_arrow app-rule, peeled to pointwise)

Dependence on the ParamInfer level-inference build

transfer_auto fixes the output class to the univalence-free Prop-motive level the combinators consume. The general engine chooses, per occurrence, the minimal class — the job of ParamInfer.inferParamLevels / inferRootClass (the constraint-graph least-fixpoint solver over the proven lattice). The generalization fits together exactly as documented in ParamInfer: read off inferRootClass for the goal's (shape-abstracted) type, synthesize at that class, and Param.weaken down — the very move auto_weaken automates here. The two halves compose: inferRootClass (which class) + auto_weaken/Param.weaken (land there).