The level-aware transfer! elaborator

A MetaM elab tactic (not a backtracking macro) that infers a relation level from the goal Expr, runs it through the univalence-free guard LevelRefusal.classify, and then either refuses with the report (when the goal forces the equiv top) or proceeds — logging the level used and delegating to the proven transfer macro.

This connects the three pieces — Levels/RelatedAt (the (m,n) levels), TransferTactic (the binder tactic), and LevelRefusal (the refusal guard) — into one pipeline: a goal Expr ↦ inferred level ↦ refuse-or-transfer, with the level reported.

The Expr-level inferencer (a conservative version)

inferGoalLevel walks the goal term:

• ∀/→ binders are traversed (forward transfer adds no strength);
• an Eq whose carrier is a Sort — an equation between types — needs an equivalence-as-equality and is inferred equiv (the refused univalence case);
• any other Eq or an Iff is a leaf transferred via an injective encoding: level embedding;
• everything else defaults to map (the weakest level).

This is an Expr-level version of the GoalShape-model inferLevel (which walked a hand-rolled GoalShape): the level is computed from the goal. It is conservative on leaf carriers — the per-subterm minimal-level solver (looking up each leaf's registered RelatedAt level and threading the meet through binders) is the larger engine; this version captures the one structural rule that matters for the refusal discipline (type-equality ⇒ equiv).

partial def Transfer.inferGoalLevel (e : Lean.Expr) : Lean.MetaM RelLevel

Infer the minimal RelLevel the goal Expr needs. See the module docstring for the rules. Conservative on leaves (embedding); the only equiv-forcing rule is an equation between Sorts (a type equality, needing univalence).

def Transfer.tacticTransfer! : Lean.ParserDescr

transfer! — the level-aware transfer. Infers the goal's level from its Expr, classifies it, and either refuses (with the univalence-free report) or logs the level and runs the proven transfer.

Equations

• Transfer.tacticTransfer! = Lean.ParserDescr.node `Transfer.tacticTransfer! 1024 (Lean.ParserDescr.nonReservedSymbol "transfer!" false)

def Transfer.«command#transfer_level_» : Lean.ParserDescr

A command that reports the inferred level + permission of a goal type, for inspection/testing without running a proof.

Equations

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

Demonstrations

The success cases are self-checking: by transfer! builds only if the level inferred is permitted and transfer closes the goal.