The Param-witness synthesizer

This module is the Lean-idiomatic analogue of Trocq's Elpi logic-program search (https://github.com/rocq-community/trocq, the param.db / solve Elpi predicates): it composes Param annotated relations for closed type structure by typeclass resolution. Where Trocq drives an Elpi program that, given a goal type, picks the parametricity combinator (app / arrow / ∀) and recurses on the subterms, here the Lean instance resolver plays exactly that role — the combinators (paramArrow, …) become instances, and inferInstance performs the search.

What this synthesizer does (and at what level)

This synthesizer works at a fixed target level (m, n) = (.map1, .map1): the self-relation ("diagonal") fragment of the lattice, where every component carries a forward and a backward map and nothing else. At this level:

• idHasParam is the base case — the diagonal Param .map1 .map1 A A with R := Eq, forward and backward maps id (the leaf rule of ⟦·⟧);
• arrowHasParam is the recursive app/function rule — it composes a Param on A → B from Params on A and B via paramArrow.

Because paramArrow consumes and produces Param .map1 .map1, these two instances close under function-space formation: the resolver synthesizes a witness for any closed type built from base types by → (including curried multi-argument functions and higher-order arguments), with no manual proof. This is the app/arrow rule of the translation ⟦·⟧, applied automatically.

The minimal-(m, n) level solver

The minimal-level solver, which this module does not build, is the variant where the output level (m, n) is not fixed but searched for, subject to the per-combinator level arithmetic the arrow combinators encode. Recall (from ParamArrow.lean) that each arrow level consumes different component levels:

output	needs PA (domain, backward)	needs PB (codomain, forward)
Map1_arrow	Param .map0 .map1	Param .map1 .map0
Map2a_arrow	Param .map0 .map2b	Param .map2a .map0
Map2b_arrow	Param .map0 .map2a	Param .map2b .map0
Map3_arrow	Param .map0 .map3	Param .map3 .map0

So a full solver must, given a requested output (m, n), compute the minimal component levels at each recursion step (the level-meet / lattice order of ParamHierarchy.lean's weakening maps) and resolve sub-witnesses at those levels. That needs either outParam level inference with a Prolog-style level-arithmetic relation, or a dedicated MetaM solver (the Elpi param-database analogue). This module pins the fixed-(map1, map1) specialization, which is sound and automates the function-rule composition.

The resolvable class

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

HasParam m n A B: a typeclass carrying a Param m n A B witness. The level indices (m, n) are explicit (not outParam), so resolution runs at a fixed target level — the analogue of asking Trocq's Elpi search for a witness at a pinned annotation. The fixed level used by the base and arrow instances below is (.map1, .map1), the self-relation fragment.

• param : Param m n A B

Base instance: the identity / diagonal

@[instance_reducible]

instance Transfer.Param.idHasParam (A : Type u) : HasParam MapClass.map1 MapClass.map1 A A

The diagonal base case (leaf rule of ⟦·⟧): the equality relation on A as a Param .map1 .map1 A A, with forward and backward maps id. Built directly here so resolution has a self-relation witness for every closed base type.

Equations

• Transfer.Param.idHasParam A = { param := { R := Eq, fwd := { map := id }, bwd := { map := id } } }

The recursive app / arrow instance

@[instance_reducible]

instance Transfer.Param.arrowHasParam {A A' B B' : Type u} [HasParam MapClass.map1 MapClass.map1 A A'] [HasParam MapClass.map1 MapClass.map1 B B'] : HasParam MapClass.map1 MapClass.map1 (A → B) (A' → B')

The app/function rule as an instance: given self-relation witnesses on the domain A/A' and codomain B/B', compose a Param .map1 .map1 on the function space via paramArrow. With idHasParam, this closes resolution under →, so curried and higher-order function types synthesize automatically.

Equations

• Transfer.Param.arrowHasParam = { param := Transfer.Param.paramArrow Transfer.Param.HasParam.param Transfer.Param.HasParam.param }

Auto-synthesis with no manual proof

The resolver composes the curried/higher-order arrow witnesses purely from arrowHasParam + idHasParam. None of the examples below write a Param term by hand.

The synth_param tactic

A macro that closes a Param .map1 .map1 _ _ goal by delegating to the resolver: it asks for the corresponding HasParam instance and projects out the .param field. This is the surface command for "synthesize a witness for this (closed) type", the user-facing analogue of Trocq's automatic generation.

def Transfer.Param.tacticSynth_param : Lean.ParserDescr

Close a Param .map1 .map1 _ _ goal by typeclass-synthesizing the corresponding HasParam witness and projecting .param.

Equations

• Transfer.Param.tacticSynth_param = Lean.ParserDescr.node `Transfer.Param.tacticSynth_param 1024 (Lean.ParserDescr.nonReservedSymbol "synth_param" false)