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 and the common universe level where the equality is being lifted, and return the lifted expression e' together with a proof of e' = lift e.

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. The function should take the original left-hand side and right-hand side a b and the common universe level, and return a proof of a = b ↔ lift a = lift b.

Equations

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

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

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

Equations

• liftExpr a b = transformExpr a b 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 __do_lift ← collectEqUniverses eq computeMaxLevel __do_lift

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 false 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

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

def liftEqualityAt (loc : Lean.Elab.Tactic.Location) (transform : (Lean.Expr → Lean.MetaM (Lean.Expr × Lean.Expr)) → Lean.Expr → Lean.MetaM (Lean.Expr × Lean.Expr) := id) : Lean.Elab.Tactic.TacticM Unit

Lifts the equalities at a location, and applies the transformation transform built from the lifting function. When the location contains several equalities, they are all lifted to a common universe level (the maximum of their universe levels), so that the lifted equalities can be used together.

Equations

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

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

All the equalities are lifted to a common universe level, so that the lifted equalities can be used to rewrite each other.

Equations

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