Types for DCP

This file gives names to the main structures used by the DCP procedure for better readability.

@[reducible, inline]

abbrev CvxLean.DCP.GraphAtomDataTree : Type

Tree with all the atom data stored in the library. The leaves are just (affine or constant) expressions.

Equations

• CvxLean.DCP.GraphAtomDataTree = CvxLean.Tree CvxLean.GraphAtomData Lean.Expr

@[reducible, inline]

abbrev CvxLean.DCP.Argument : Type

This is the type of an argument.

Equations

• CvxLean.DCP.Argument = Lean.Expr

@[reducible, inline]

abbrev CvxLean.DCP.Arguments : Type

An atom may have several arguments.

Equations

• CvxLean.DCP.Arguments = Array CvxLean.DCP.Argument

@[reducible, inline]

abbrev CvxLean.DCP.ArgumentsTree : Type

Tree of the arguments of every atom unfolded (expressions at the nodes).

Equations

• CvxLean.DCP.ArgumentsTree = CvxLean.Tree CvxLean.DCP.Arguments Unit

@[reducible, inline]

abbrev CvxLean.DCP.CurvatureTree : Type

Curvatures in the atom tree.

Equations

• CvxLean.DCP.CurvatureTree = CvxLean.Tree CvxLean.Curvature CvxLean.Curvature

@[reducible, inline]

abbrev CvxLean.DCP.BCond : Type

A background condition is just an expression of type Prop.

Equations

• CvxLean.DCP.BCond = Lean.Expr

@[reducible, inline]

abbrev CvxLean.DCP.BConds : Type

An atom may have several background conditions.

Equations

• CvxLean.DCP.BConds = Array CvxLean.DCP.BCond

@[reducible, inline]

abbrev CvxLean.DCP.BCondsTree : Type

Background conditions of every atom in the atom tree.

Equations

• CvxLean.DCP.BCondsTree = CvxLean.Tree CvxLean.DCP.BConds CvxLean.DCP.BConds

@[reducible, inline]

abbrev CvxLean.DCP.AtomDataTrees : Type

Four trees: atom data tree, arguments tree, curvature tree, and background condition tree.

Equations

• CvxLean.DCP.AtomDataTrees = (CvxLean.DCP.GraphAtomDataTree × CvxLean.DCP.ArgumentsTree × CvxLean.DCP.CurvatureTree × CvxLean.DCP.BCondsTree)

@[reducible, inline]

abbrev CvxLean.DCP.NewVarsTree : Type

New variables introduced by every atom, as local declarations at the nodes.

Equations

• CvxLean.DCP.NewVarsTree = CvxLean.Tree (Array Lean.LocalDecl) Unit

@[reducible, inline]

abbrev CvxLean.DCP.NewConstrVarsTree : Type

Variables for the new constraints introduced by every atom, as local declarations at the nodes.

Equations

• CvxLean.DCP.NewConstrVarsTree = CvxLean.Tree (Array Lean.LocalDecl) Unit

@[reducible, inline]

abbrev CvxLean.DCP.NewConstrsTree : Type

All the new constraints introduced by each atom, as expressions at the node.

Equations

• CvxLean.DCP.NewConstrsTree = CvxLean.Tree (Array Lean.Expr) Unit

@[reducible, inline]

abbrev CvxLean.DCP.PreVCond : Type

In general a variable condition can either match a constraint exactly or it can be inferred from the other constraints, we represent that as a sum type. If a number is given, then it is interpreted as the index of the constraint that corresponds to the vcondition.

Equations

• CvxLean.DCP.PreVCond = (ℕ ⊕ Lean.Expr)

@[reducible, inline]

abbrev CvxLean.DCP.PreVConds : Type

Equations

• CvxLean.DCP.PreVConds = Array CvxLean.DCP.PreVCond

@[reducible, inline]

abbrev CvxLean.DCP.PreVCondsTree : Type

Equations

• CvxLean.DCP.PreVCondsTree = CvxLean.Tree CvxLean.DCP.PreVConds Unit

@[reducible, inline]

abbrev CvxLean.DCP.VCond : Type

This is different from PreVCond and instead holds proofs of variable conditions. Still, it could either be a variable corresponding to a constraint, or an expression involving several constraints, in case it is inferred.

Equations

• CvxLean.DCP.VCond = Lean.Expr

@[reducible, inline]

abbrev CvxLean.DCP.VConds : Type

Several proofs of vconditions.

Equations

• CvxLean.DCP.VConds = Array CvxLean.DCP.VCond

@[reducible, inline]

abbrev CvxLean.DCP.VCondsTree : Type

All the vcondition proofs for the atom.

Equations

• CvxLean.DCP.VCondsTree = CvxLean.Tree CvxLean.DCP.VConds Unit

@[reducible, inline]

abbrev CvxLean.DCP.VCondIdx : Type

It is useful to only consider the vconditions that need to be eliminated because they match a constraint exactly. This represents the index of such constraint.

Equations

• CvxLean.DCP.VCondIdx = ℕ

@[reducible, inline]

abbrev CvxLean.DCP.VCondsIdxs : Type

Several VCondIdxs.

Equations

• CvxLean.DCP.VCondsIdxs = Array CvxLean.DCP.VCondIdx

@[reducible, inline]

abbrev CvxLean.DCP.VCondsIdxsTree : Type

All the indices of all the vconditions marked for elimination.

Equations

• CvxLean.DCP.VCondsIdxsTree = CvxLean.Tree CvxLean.DCP.VCondsIdxs Unit

@[reducible, inline]

abbrev CvxLean.DCP.NewVarAssignment : Type

A solution is just an expression (involving the atom arguments).

Equations

• CvxLean.DCP.NewVarAssignment = Lean.Expr

@[reducible, inline]

abbrev CvxLean.DCP.Solution : Type

If an atom has several implementation variables, we need a solution for each of them.

Equations

• CvxLean.DCP.Solution = Array CvxLean.DCP.NewVarAssignment

@[reducible, inline]

abbrev CvxLean.DCP.CanonExpr : Type

A canonized expression.

Equations

• CvxLean.DCP.CanonExpr = Lean.Expr

@[reducible, inline]

abbrev CvxLean.DCP.CanonExprsTree : Type

A tree of canonized expressions.

Equations

• CvxLean.DCP.CanonExprsTree = CvxLean.Tree CvxLean.DCP.CanonExpr CvxLean.DCP.CanonExpr

structure CvxLean.DCP.CanonExprWithSolution : Type

Canonized expression and solution put together.

• canonExpr : CvxLean.DCP.CanonExpr
• solution : CvxLean.DCP.Solution

instance CvxLean.DCP.instInhabitedCanonExprWithSolution : Inhabited CvxLean.DCP.CanonExprWithSolution

Equations

• CvxLean.DCP.instInhabitedCanonExprWithSolution = { default := { canonExpr := default, solution := default } }

@[reducible, inline]

abbrev CvxLean.DCP.CanonExprsWithSolutionTree : Type

Tree of canonized expression and solution for each atom.

Equations

• CvxLean.DCP.CanonExprsWithSolutionTree = CvxLean.Tree CvxLean.DCP.CanonExprWithSolution CvxLean.DCP.CanonExprWithSolution

@[reducible, inline]

abbrev CvxLean.DCP.SolEqAtomProof : Type

A proof of solution-equals-atom for an atom.

Equations

• CvxLean.DCP.SolEqAtomProof = Lean.Expr

@[reducible, inline]

abbrev CvxLean.DCP.SolEqAtomProofsTree : Type

Tree of all the solution-equals-atom proofs in the atom tree.

Equations

• CvxLean.DCP.SolEqAtomProofsTree = CvxLean.Tree CvxLean.DCP.SolEqAtomProof CvxLean.DCP.SolEqAtomProof

@[reducible, inline]

abbrev CvxLean.DCP.FeasibilityProof : Type

A feasibility proof.

Equations

• CvxLean.DCP.FeasibilityProof = Lean.Expr

@[reducible, inline]

abbrev CvxLean.DCP.FeasibilityProofs : Type

An atom may have several feasibility proofs, one per implementation constraint.

Equations

• CvxLean.DCP.FeasibilityProofs = Array CvxLean.DCP.FeasibilityProof

@[reducible, inline]

abbrev CvxLean.DCP.FeasibilityProofsTree : Type

Tree of all the feasibility proofs in the atom tree.

Equations

• CvxLean.DCP.FeasibilityProofsTree = CvxLean.Tree CvxLean.DCP.FeasibilityProofs Unit

@[reducible, inline]

abbrev CvxLean.DCP.OptimalityProof : Type

Optimality proof. There is only one per atom.

Equations

• CvxLean.DCP.OptimalityProof = Lean.Expr

@[reducible, inline]

abbrev CvxLean.DCP.OptimalityProofsTree : Type

Tree of all the optimality proofs in the atom tree.

Equations

• CvxLean.DCP.OptimalityProofsTree = CvxLean.Tree CvxLean.DCP.OptimalityProof CvxLean.DCP.OptimalityProof

@[reducible, inline]

abbrev CvxLean.DCP.VCondElimProof : Type

A proof of vcondtion elimination.

Equations

• CvxLean.DCP.VCondElimProof = Lean.Expr

@[reducible, inline]

abbrev CvxLean.DCP.VCondElimProofs : Type

An atom may have several vconditions. Each needs a vcondition elimination proof.

Equations

• CvxLean.DCP.VCondElimProofs = Array CvxLean.DCP.VCondElimProof

@[reducible, inline]

abbrev CvxLean.DCP.OptimalityAndVCondElimProofs : Type

Optimality and vcondition elimination proofs together.

Equations

• CvxLean.DCP.OptimalityAndVCondElimProofs = (CvxLean.DCP.OptimalityProof × CvxLean.DCP.VCondElimProofs)

@[reducible, inline]

abbrev CvxLean.DCP.OptimalityAndVCondElimProofsTree : Type

Tree of all the optimality and vcondition elimination proofs in the atom tree.

Equations

• CvxLean.DCP.OptimalityAndVCondElimProofsTree = CvxLean.Tree CvxLean.DCP.OptimalityAndVCondElimProofs CvxLean.DCP.OptimalityAndVCondElimProofs

@[reducible, inline]

abbrev CvxLean.DCP.VCondElimMap : Type

Vcondition elimination map, from constraint index to the constraint expression.

Equations

• CvxLean.DCP.VCondElimMap = Std.HashMap ℕ Lean.Expr

structure CvxLean.DCP.ProcessedAtomTree : Type

This structure holds all the necessary information to build a canonized problem and a proof of equivalence. In CvxLean/Tactic/DCP/DCPMakers.lean, we define the procedure that takes an optimization problem, builds an atom tree and "processes" it to make a processed atom tree.

• originalVarsDecls : Array Lean.LocalDecl
• originalConstrVars : Array Lean.LocalDecl
• newVarDecls : List Lean.LocalDecl
• newConstrs : Array Lean.Expr
• newConstrVarsArray : Array Lean.LocalDecl
• forwardImagesNewVars : Array Lean.Expr
• constraints : List (Lean.Name × Lean.Expr)
• isVCond : Array Bool
• vcondElimMap : CvxLean.DCP.VCondElimMap
• solEqAtom : CvxLean.OC CvxLean.DCP.SolEqAtomProofsTree
• feasibility : CvxLean.OC CvxLean.DCP.FeasibilityProofsTree
• canonExprs : CvxLean.OC CvxLean.DCP.CanonExprsTree
• optimality : CvxLean.OC CvxLean.DCP.OptimalityProofsTree

instance CvxLean.DCP.instInhabitedProcessedAtomTree : Inhabited CvxLean.DCP.ProcessedAtomTree

Equations

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