hgcongr engine — head-pair-keyed DB, attribute, and tactic

This module holds the engine for hgcongr (heterogeneous cross-head generalized congruence): the head-pair-keyed environment extension, the @[hgcongr] attribute (makeHGCongrLemma), and the hgcongr tactic core. The registered correspondences and demos live in the importer HGCongr.lean.

The split is mandatory: an initialize env-extension declaration cannot be evaluated in the same module that defines it, and applying @[hgcongr] to a lemma forces that evaluation at elaboration time. So the extension + attribute must sit in a module imported before any @[hgcongr] use (the same reason Mathlib keeps gcongrExt in GCongr/Core.lean, used only by importers, and the reason ParamDB.lean is split from its consumers here). See HGCongr.lean for the design rationale, the rcongr/gcongr contrast, and the upstream-patch spec.

The head-pair-keyed lemma database

structure Transfer.HGCongrKey : Type

Lookup key for a heterogeneous congruence lemma: the relation together with both heads. Unlike gcongr's GCongrKey (one head), this stores the LHS head f and RHS head g of a conclusion R (f a..) (g b..). The diagonal lhsHead = rhsHead recovers the homogeneous gcongr key.

• relName : Lean.Name

  The relation name, e.g. Eq.

• lhsHead : Lean.Name

  The LHS head function, e.g. HMul.hMul.

• rhsHead : Lean.Name

  The RHS head function, e.g. bbFieldMul (may differ from lhsHead).

@[instance_reducible]

instance Transfer.instInhabitedHGCongrKey : Inhabited HGCongrKey

Equations

• Transfer.instInhabitedHGCongrKey = { default := Transfer.instInhabitedHGCongrKey.default }

def Transfer.instBEqHGCongrKey.beq : HGCongrKey → HGCongrKey → Bool

Equations

• Transfer.instBEqHGCongrKey.beq { relName := a, lhsHead := a_1, rhsHead := a_2 } { relName := b, lhsHead := b_1, rhsHead := b_2 } = (a == b && (a_1 == b_1 && a_2 == b_2))
• Transfer.instBEqHGCongrKey.beq x✝¹ x✝ = false

@[instance_reducible]

instance Transfer.instBEqHGCongrKey : BEq HGCongrKey

Equations

• Transfer.instBEqHGCongrKey = { beq := Transfer.instBEqHGCongrKey.beq }

@[instance_reducible]

instance Transfer.instHashableHGCongrKey : Hashable HGCongrKey

Equations

• Transfer.instHashableHGCongrKey = { hash := Transfer.instHashableHGCongrKey.hash }

def Transfer.instHashableHGCongrKey.hash : HGCongrKey → UInt64

Equations

• Transfer.instHashableHGCongrKey.hash { relName := a, lhsHead := a_1, rhsHead := a_2 } = mixHash (mixHash (mixHash 0 (hash a)) (hash a_1)) (hash a_2)

structure Transfer.HGCongrLemma : Type

Data for one registered heterogeneous congruence lemma.

• key : HGCongrKey

  The head-pair key under which the lemma is stored.

• declName : Lean.Name

  The lemma's declaration name.

• mainSubgoals : Array (ℕ × ℕ × Bool)

  For each per-argument main subgoal: the hypothesis index, the number of leading binders to intro, and whether it is contravariant.

• numHyps : ℕ

  The number of arguments to supply when applying the lemma.

• numVarying : ℕ

  The number of varying-argument pairs (for priority/diagnostics).

@[instance_reducible]

instance Transfer.instInhabitedHGCongrLemma : Inhabited HGCongrLemma

Equations

• Transfer.instInhabitedHGCongrLemma = { default := Transfer.instInhabitedHGCongrLemma.default }

@[reducible, inline]

abbrev Transfer.HGCongrLemmas : Type

The head-pair-keyed lemma collection stored in the environment extension.

Equations

• Transfer.HGCongrLemmas = Std.HashMap Transfer.HGCongrKey (List Transfer.HGCongrLemma)

opaque Transfer.hgcongrExt : Lean.SimpleScopedEnvExtension HGCongrLemma HGCongrLemmas

Environment extension for @[hgcongr] lemmas, keyed on the head pair. Contrast Mathlib.Tactic.GCongr.gcongrExt, keyed on a single head.

Registration: makeHGCongrLemma

The heterogeneous analogue of makeGCongrLemma. The two structural differences from gcongr are (a) no lhsHead == rhsHead / arity-equality guard, and (b) varying-argument pairs are recovered from the hypotheses rather than by a positional zip of the two argument lists (which is ill-defined when the heads have different arities, as HMul.hMul/bbFieldMul do).

def Transfer.makeHGCongrLemma (hyps : Array Lean.Expr) (target : Lean.Expr) (declName : Lean.Name) : Lean.MetaM HGCongrLemma

Build the HGCongrLemma for a lemma with hypotheses hyps and conclusion target of the form R (f a₁ … aₘ) (g b₁ … bₙ), f and g possibly different (and m ≠ n permitted). Each hypothesis Rᵢ lᵢ rᵢ whose sides are free variables appearing among the LHS-args and RHS-args (in either order) becomes a varying pair and a recursive main subgoal.

Equations

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

The hgcongr tactic

def Transfer.applyAtArity (mvarId : Lean.MVarId) (e : Lean.Expr) (arity : ℕ) : Lean.MetaM (List Lean.MVarId)

Close mvarId with e applied to exactly arity arguments, the arity being supplied rather than inferred from the goal. Instance-implicit arguments that unification left unassigned are synthesized; the metavariables still unassigned afterwards are returned as goals.

Equations

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

partial def Transfer.hgcongrCore (g : Lean.MVarId) : Lean.MetaM (List Lean.MVarId)

The core descent. Mirror of Lean.MVarId.gcongr but with the head-pair lookup. On a goal R (f a..) (g b..):

• try rfl first (closes leaves and the homogeneous reflexive case);
• read (relName, lhsHead, rhsHead), look up the (f, g) correspondence in the head-pair DB, apply the lemma at the LHS-head arity, recurse on the per-argument main subgoals, and rfl-discharge any leftover side goals;
• otherwise return the goal unsolved.

def Transfer.tacticHgcongr : Lean.ParserDescr

hgcongr — heterogeneous (cross-head) generalized congruence.

Reduce a relational goal R (f a₁ … aₘ) (g b₁ … bₙ) whose two sides have a registered head correspondence (f, g) (a @[hgcongr] lemma) to its per-argument subgoals, recursing. The heads f, g may differ (the case @[gcongr] rejects); the diagonal f = g recovers gcongr's homogeneous descent. Leaves and reflexive steps are closed by rfl.

Equations

• Transfer.tacticHgcongr = Lean.ParserDescr.node `Transfer.tacticHgcongr 1024 (Lean.ParserDescr.nonReservedSymbol "hgcongr" false)