Implementation of the lift_eq tactic for kernels.

This file contains functions that propagate the lifting of kernel expressions through several operators and primitives, and constructs the necessary proofs for the lift_eq tactic. Each function returns the lifted expression e' together with a proof of e' = e.lift, built by congruence from the compatibility lemmas of Kernel.lift (comp_lift, parallelComp_lift, ...).

def liftLemmaArgs (X Y X' Y' : Carrier) (ex ey : Lean.Expr) : Lean.MetaM (Array Lean.Expr)

The arguments shared by the compatibility lemmas of Kernel.lift for a kernel Kernel X Y: X [mX] Y [mY] X' [mX'] Y' [mY'] ex ey.

Equations

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

def liftBinary (κ η : Lean.Expr) (maxLvl : Lean.Level) (mkOp : Lean.Expr → Lean.Expr → Lean.MetaM Lean.Expr) (pf : Lean.Expr) : Lean.MetaM (Lean.Expr × Lean.Expr)

Lifts a binary kernel operation by lifting the inner kernels. mkOp builds the operation from the lifted kernels, and pf must be a proof of mkOp κ.lift η.lift = (mkOp κ η).lift.

Equations

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

def liftComposition (e : Lean.Expr) (maxLvl : Lean.Level) : Lean.MetaM (Lean.Expr × Lean.Expr)

Lifts a composition of kernels by lifting the inner kernels.

Equations

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

def liftParallelComp (e : Lean.Expr) (maxLvl : Lean.Level) : Lean.MetaM (Lean.Expr × Lean.Expr)

Lifts a parallel composition of kernels by lifting the inner kernels.

Equations

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

def liftProd (e : Lean.Expr) (maxLvl : Lean.Level) : Lean.MetaM (Lean.Expr × Lean.Expr)

Lifts a product of kernels by lifting the inner kernels.

Equations

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

def liftCompProd (e : Lean.Expr) (maxLvl : Lean.Level) : Lean.MetaM (Lean.Expr × Lean.Expr)

Lifts a composition-product of kernels by lifting the inner kernels.

Equations

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

def liftId (e : Lean.Expr) (maxLvl : Lean.Level) : Lean.MetaM (Lean.Expr × Lean.Expr)

Lifts the identity kernel by lifting the carrier type.

Equations

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

def liftDiscard (e : Lean.Expr) (maxLvl : Lean.Level) : Lean.MetaM (Lean.Expr × Lean.Expr)

Lifts a discard kernel by lifting the carrier type.

Equations

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

def liftCopy (e : Lean.Expr) (maxLvl : Lean.Level) : Lean.MetaM (Lean.Expr × Lean.Expr)

Lifts a copy kernel by lifting the carrier type.

Equations

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

def liftSwap (e : Lean.Expr) (maxLvl : Lean.Level) : Lean.MetaM (Lean.Expr × Lean.Expr)

Lifts a swap kernel by lifting the carrier types.

Equations

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

def liftKernel (e : Lean.Expr) (maxLvl : Lean.Level) : Lean.MetaM (Lean.Expr × Lean.Expr)

Lifts a kernel using Kernel.lift.

Equations

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

def finisherKernel (κ η : Lean.Expr) (maxLvl : Lean.Level) : Lean.MetaM Lean.Expr

The finisher for kernels: κ = η ↔ κ.lift = η.lift.

Equations

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