Lift and Unlift utilities

This file provides utility functions for lifting and unlifting equalities.

A lifting (resp. unlifting) function transforms an expression e into an expression e' living in a common universe level (resp. in the original universe levels), together with a proof that the expression in the common universe level is the lift of the other one: e' = lift e when lifting, e = lift e' when unlifting. These proofs are combined by congruence to obtain the equivalence between the original equality and the transformed one.

@[reducible, inline]

abbrev liftMetadata : Type

A type alias for lifting/unlifting functions. Given an expression and the common universe level, return the transformed expression together with a proof that the expression living in the common universe level is the lift of the other one.

Equations

• liftMetadata = (Lean.Expr → Lean.Level → Lean.MetaM (Lean.Expr × Lean.Expr))

@[reducible, inline]

abbrev finisherMetadata : Type

A type alias for finisher functions. Given the two sides a b of an equality living in the original universe levels and the common universe level, return a proof of a = b ↔ lift a = lift b.

Equations

• finisherMetadata = (Lean.Expr → Lean.Expr → Lean.Level → Lean.MetaM Lean.Expr)

def transformExpr (e : Lean.Expr) (maxLvl : Lean.Level) (impl_ref : IO.Ref (Array liftMetadata)) : Lean.MetaM (Lean.Expr × Lean.Expr)

Transforms an expression using the registered lifting/unlifting functions given in impl_ref. Returns the first successful transformation along with its proof.

Equations

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

def mkEqCongr (pl pr : Lean.Expr) : Lean.MetaM Lean.Expr

From pl : a = c and pr : b = d, build a proof of (a = b) = (c = d).

Equations

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

def constructProof (unlift : Bool) (lhs rhs lhs_t rhs_t pl pr : Lean.Expr) (maxLvl : Lean.Level) (finisher_ref : IO.Ref (Array finisherMetadata)) : Lean.MetaM Lean.Expr

Constructs a proof of (lhs = rhs) = (lhs_t = rhs_t) from the proofs pl pr returned by the lifting/unlifting functions for both sides and a finisher. When lifting, pl : lhs_t = lift lhs; when unlifting, pl : lhs = lift lhs_t (and similarly for pr).

Equations

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

def transformEquality (unlift : Bool) (getLvl : Lean.Expr → Lean.MetaM Lean.Level) (lift_ref : IO.Ref (Array liftMetadata)) (finisher_ref : IO.Ref (Array finisherMetadata)) (eq : Lean.Expr) : Lean.MetaM (Lean.Expr × Lean.Expr)

Lifts or unlifts an equality expression by transforming both sides using the registered lifting/ unlifting functions. Returns the transformed equality and a proof of equality between the original and transformed expressions.

Equations

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