derive_param_congr — a constructor-congruence Related deriver

The Related kernel (Transfer/Base/Related.lean) auto-composes binary-op trees on a single carrier (composeBinOp over RelatedBinOp squares) but stops at any structure head: it provides no constructor congruence for user inductives. Crossing a structure boundary (e.g. a value of a single-constructor structure that encodes to the product of its fields) therefore needs, per type, one product-encoding enc plus one constructor-congruence Related instance — the Param_<T> boilerplate.

This file generates that boilerplate. It is the Trocq/Elpi Param_<T> analogue for the Related kernel: a metaprogram that, for a single-constructor structure T, reads the constructor's field names and types and emits

• a ParamEnc T α instance — the product encoding enc x = (ParamEnc.enc x.f₁, …, ParamEnc.enc x.fₙ), where each field's encoding is resolved recursively through ParamEnc (so nested derived structures compose automatically), and
• the constructor congruence Related (ParamEnc.enc) (T.mk a₁ … aₙ) (a₁', …, aₙ') from the per-field Related (ParamEnc.enc) aᵢ aᵢ' facts.

With both registered, instance resolution transports a structured value compositionally — the constructor congruence on top, the base-carrier RelatedBinOp squares underneath — with no monolithic whole-op leaf.

Surface

• derive_param_congr T — a command elaborator (works in-file), and
• deriving instance ParamCongr for T / deriving ParamCongr — the registered deriving handler (live for downstream modules, since initialize takes effect only after this module is imported).

Both route to the same generator, deriveParamCongrCore.

Reflective-vs-assumed boundary

• Reflective (read off the structure): the constructor name, the field names, the field types (hence the aᵢ binders), the structure's parameters (the generated instances are parametric in them), and each field's encoded type αᵢ (via ParamEnc.enc-type inference, so nested structures' encodings compose).
• Assumed / out of scope (matching the structure focus of relational parametricity derivers): single constructor only (multi-constructor inductives and indexed/dependent families are rejected); the per-field encodings are whatever ParamEnc resolves to (an atomic field uses the low-priority id leaf; a nested structure uses its own derived instance — derive bottom-up); the base-carrier op squares (RelatedBinOp) are supplied, never invented — the relatedBinOpOfLeaf bridge only re-uses an existing id-registered square at the ParamEnc-leaf encoding.

1. The field-encoding typeclass

class Transfer.Deriving.ParamEnc (A : Type) (α : outParam Type) : Type

ParamEnc A α: a registered encoding A → α for the structure-field recursion. The derived ParamEnc T _ instance for a structure encodes it to the product of its fields' encodings, so the recursion is automatic.

• enc : A → α

  The encoding map.

@[instance_reducible, instance 100]

instance Transfer.Deriving.paramEncLeaf {A : Type} : ParamEnc A A

Leaf. An atomic type encodes to itself by id. Low priority so a derived structure instance (default priority) wins when both could apply.

Equations

• Transfer.Deriving.paramEncLeaf = { enc := id }

@[instance 100]

instance Transfer.Deriving.relatedBinOpOfLeaf {A : Type} (op bop : A → A → A) [h : RelatedBinOp id op bop] : RelatedBinOp ParamEnc.enc op bop

Bridge. Any base-carrier RelatedBinOp registered at the id encoding lifts to the ParamEnc-leaf encoding for free (ParamEnc.enc at a leaf type is definitionally id). One instance re-uses every id-registered op square under the derived congruence — no per-op boilerplate.

@[instance 100]

instance Transfer.Deriving.paramEncLeafRelated {A : Type} (a : A) : Related ParamEnc.enc a a

Leaf-encoding Related. a transports to itself along the ParamEnc leaf (it is id). Gives the base case of the congruence's per-coordinate composition an RHS that is literally the input (not ParamEnc.enc a), so composeBinOp terminates cleanly at base-carrier variables.

class Transfer.Deriving.ParamCongr (A : Sort u_1) : Prop

Marker class keying the deriving handler (deriving instance ParamCongr for T). The handler generates the ParamEnc/Related instances and ignores the literal class.

2. The generator

def Transfer.Deriving.mkTupleStx (xs : Array Lean.Term) : Lean.Elab.Command.CommandElabM Lean.Term

Build the anonymous tuple syntax (x₀, …, xₙ₋₁) (right-nested Prod.mk); a singleton is returned bare.

Equations

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

def Transfer.Deriving.mkProdTypeStx (xs : Array Lean.Term) : Lean.Elab.Command.CommandElabM Lean.Term

Build the right-nested product type syntax x₀ × … × xₙ₋₁; a singleton is returned bare.

Equations

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

def Transfer.Deriving.deriveParamCongrCore (declName : Lean.Name) : Lean.Elab.Command.CommandElabM Unit

The core generator: read single-constructor structure declName and emit its ParamEnc product-encoding instance and its constructor-congruence Related instance.

Equations

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

3. Surfaces

def Transfer.Deriving.deriveParamCongrCmd : Lean.ParserDescr

In-file command: derive_param_congr T.

Equations

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

def Transfer.Deriving.elabDeriveParamCongr : Lean.Elab.Command.CommandElab

Equations

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

def Transfer.Deriving.paramCongrDerivingHandler (declNames : Array Lean.Name) : Lean.Elab.Command.CommandElabM Bool

The registered deriving handler (deriving instance ParamCongr for T). Single-constructor structures only; declines otherwise so another handler can take over.

Equations

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