Unlift tactic

This file defines the unlift_eq tactic, which performs the inverse operation of lift_eq. It takes an equality that has been lifted to a common universe level and attempts to unlift it back to its original form. The tactic is designed to work with various types of expressions, and can be extended by registering new unlift functions.

def registerUnliftExpr (f : liftMetadata) : IO Unit

Registers a new unlifting 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

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

def registerUnliftFinisher (f : finisherMetadata) : IO Unit

Registers a new finisher function for constructing the final proof of equality after unlifting 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

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

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

Unlifts an expression that has been lifted to a common universe level using the registered unlifting functions.

Equations

• unliftExpr a b c = transformExpr a b c unliftImplRef✝

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

Unlifts an equality expression that has been lifted to a common universe level using the registered unlifting functions and finisher functions.

Equations

• unliftEquality = transformEquality getLevelFromEq unliftImplRef✝ unliftFinisherRef✝

def EqUnlift : Lean.ParserDescr

Performs the inverse operation of lift_eq, transforming an equality that has been lifted to a common universe level back to its original form.

The tactic supports location specifiers like rw or simp:

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

Equations

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