Main DCP algorithm

This file contains the main DCP algorithm (canonize), it can also be used as a tactic (dcp). It uses the processed atom tree from mkProcessedAtomTree in CvxLean/Tactic/DCP/DCPMakers.lean to build the forward and backward maps and prove the four properties of a StrongEquivalence.

def CvxLean.DCP.makeForwardMap (oldDomain : Lean.Expr) (xs : Array Lean.Expr) (forwardImagesNewVars : Array Lean.Expr) : Lean.MetaM Lean.Expr

Create the forward map (φ) from the forward images given by the processed atom tree.

Equations

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

def CvxLean.DCP.makeConstrForward (oldDomain : Lean.Expr) (xs : Array Lean.Expr) (originalConstrVars : Array Lean.LocalDecl) (oldProblem : Lean.Expr) (constraints : Array Lean.Expr) (isVCond : Array Bool) (constraintsEq : Array Lean.Expr) (feasibility : CvxLean.OC CvxLean.DCP.FeasibilityProofsTree) : Lean.MetaM Lean.Expr

Build the proof of StrongEquivalence.phi_feasibility. This uses the feasibility proofs.

Equations

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

def CvxLean.DCP.makeObjFunForward (oldDomain : Lean.Expr) (xs : Array Lean.Expr) (originalConstrVars : Array Lean.LocalDecl) (oldProblem : Lean.Expr) (constraints : Array Lean.Expr) (objFunEq : Lean.Expr) : Lean.MetaM Lean.Expr

Build a proof of StrongEquivalence.phi_optimality. We can actually prove equality here, using the solution-equal-atom property from the top atom that unfolds the objective function.

Equations

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

def CvxLean.DCP.makeBackwardMap (xs : Array Lean.Expr) (mkDomainFunc : Lean.Expr → Lean.MetaM Lean.Expr) : Lean.MetaM Lean.Expr

Create the backward map (ψ), which is simply a projection.

Equations

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

def CvxLean.DCP.makeConstrBackward (vcondElimMap : CvxLean.DCP.VCondElimMap) (newDomain : Lean.Expr) (canonProblem : Lean.Expr) (xs : Array Lean.Expr) (ys : Array Lean.Expr) (constrOpt : Array Lean.Expr) (canonConstrs : Array Lean.Expr) (newConstrs : Array Lean.Expr) (newConstrVars : Array Lean.LocalDecl) : Lean.MetaM Lean.Expr

Build a proof of StrongEquivalence.psi_feasibility. The proofs here come from the optimality proofs and vcondition elimination.

Equations

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

def CvxLean.DCP.makeObjFunBackward (newDomain : Lean.Expr) (canonProblem : Lean.Expr) (xs : Array Lean.Expr) (ys : Array Lean.Expr) (objFunOpt : Lean.Expr) (canonConstrs : Array Lean.Expr) (newConstrs : Array Lean.Expr) (newConstrVars : Array Lean.LocalDecl) : Lean.MetaM Lean.Expr

Build a proof of StrongEquivalence.psi_optimality. The proofs here come from optimality proofs on the objective function component.

Equations

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

def CvxLean.DCP.canonize (ogProblem : CvxLean.Meta.MinimizationExpr) : Lean.MetaM (CvxLean.Meta.MinimizationExpr × Lean.Expr)

Main canonization procedure. Given a minimization expression, return the canonized problem, in conic form, and a proof of equivalence.

Equations

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

def CvxLean.DCP.dcpBuilder : CvxLean.Meta.EquivalenceBuilder Unit

Equations

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

def CvxLean.Tactic.dcp : Lean.ParserDescr

Tactic to canonize a problem into DCP form. It can be used directly in an equivalence or reduction environment. However, note, that the main use of this transformation is to solve problems using the solve command.

Equations

• CvxLean.Tactic.dcp = Lean.ParserDescr.node `CvxLean.Tactic.dcp 1024 (Lean.ParserDescr.nonReservedSymbol "dcp" false)

def CvxLean.Tactic.evalDcp : Lean.Elab.Tactic.Tactic

Equations

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