Lift tactic

This file defines the lift_eq tactic, which lifts an equality to a common universe level. It propagates the lifting through the structure of the equality. The tactic is implemented in a way that it can be easily extended to support new types of expressions by registering new lifting functions.

def registerLiftExpr (f : liftMetadata) : IO Unit

Registers a new lifting function for expressions. The function should take an expression, a universe level (most likely the common universe level where the equality is being lifted), and a list of proofs, and return a new expression and an updated list of proofs.

Equations

• registerLiftExpr f = ST.Ref.modify liftImplRef✝ fun (x : Array liftMetadata) => x.push f

def registerLiftFinisher (f : finisherMetadata) : IO Unit

Registers a new finisher function for constructing the final proof of equality after lifting inner expressions. The function should take the original left-hand side and right-hand side, the transformed left-hand side and right-hand side, the common universe level, and return a proof of equality.

Equations

• registerLiftFinisher f = ST.Ref.modify liftFinisherRef✝ fun (x : Array finisherMetadata) => x.push f

def liftExpr (a : Lean.Expr) (b : Lean.Level) (c : List Lean.Expr) : Lean.MetaM (Lean.Expr × List Lean.Expr)

Lifts an expression to a common universe level using the registered lifting functions.

Equations

• liftExpr a b c = transformExpr a b c liftImplRef✝

def getMaxLvl (eq : Lean.Expr) : Lean.MetaM Lean.Level

Gets the maximum universe level from an equality expression by collecting all universe levels from the left-hand side and right-hand side of the equality.

Equations

• getMaxLvl eq = do let univs ← collectExprUniverses eq computeMaxLevel univs

def liftEquality (eq : Lean.Expr) : Lean.MetaM (Lean.Expr × Lean.Expr)

Lifts an equality expression to a common universe level using the registered lifting functions and finisher functions.

Equations

• liftEquality = transformEquality getMaxLvl liftImplRef✝ liftFinisherRef✝

def liftEqualityWithLevel (Lvl : Lean.Level) (eq : Lean.Expr) : Lean.MetaM (Lean.Expr × Lean.Expr)

Same as liftEquality, but allows specifying a universe level that will be taken into account when computing the maximum universe level.

Equations

• liftEqualityWithLevel Lvl eq = transformEquality (fun (e : Lean.Expr) => do let univs ← collectExprUniverses e computeMaxLevel (Lvl :: univs)) liftImplRef✝ liftFinisherRef✝ eq

def EqLift : Lean.ParserDescr

Transforms an equality expression by lifting both sides to a common universe level.

The tactic supports location specifiers like rw or simp:

• lift_eq — applies to the goal
• lift_eq at h — applies to hypothesis h
• lift_eq at h₁ h₂ — applies to multiple hypotheses
• lift_eq at h ⊢ — applies to hypothesis h and the goal
• lift_eq at * — applies to all hypotheses and the goal

Equations

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