diff --git a/CvxLean/Command/Solve.lean b/CvxLean/Command/Solve.lean index 6481dfaf..171ba549 100644 --- a/CvxLean/Command/Solve.lean +++ b/CvxLean/Command/Solve.lean @@ -6,7 +6,7 @@ import CvxLean.Command.Solve.Conic Given a problem `p : Minimization D R` a user can call `solve p` to call an external solver and obtain a result. If successful, three new definitions are added to the environment: -* `p.reduced : Minimization (D × E) R` is the problem in conic form. +* `p.conicForm : Minimization (D × E) R` is the problem in conic form. * `p.status : String` is the status of the solution. * `p.solution : D` is the solution to the problem. * `p.value : R` is the value of the solution. @@ -32,16 +32,16 @@ def getProblemName (stx : Syntax) : MetaM Name := do /-- Call DCP and get the problem in conic form as well as `ψ`, the backward map from the equivalence. -/ -def getReducedProblemAndBwdMap (prob : Expr) : MetaM (MinimizationExpr × Expr) := do +def getCanonizedProblemAndBwdMap (prob : Expr) : MetaM (MinimizationExpr × Expr) := do let ogProb ← MinimizationExpr.fromExpr prob - let (redProb, eqvProof) ← DCP.canonize ogProb + let (canonProb, eqvProof) ← DCP.canonize ogProb let backwardMap ← mkAppM ``Minimization.Equivalence.psi #[eqvProof] - return (redProb, backwardMap) + return (canonProb, backwardMap) syntax (name := solve) "solve " term : command /-- The `solve` command. It works as follows: -1. Reduce optimization problem to conic form. +1. Canonize optimization problem to conic form. 2. Extract problem data using `determineCoeffsFromExpr`. 3. Obtain a solution using `solutionDataFromProblemData`, which calls an external solver. 4. Store the result in the enviroment. -/ @@ -61,19 +61,19 @@ unsafe def evalSolve : CommandElab := fun stx => mvarId.assign mvarVal } catch _ => pure () - -- Create prob.reduced. - let (redProb, backwardMap) ← getReducedProblemAndBwdMap probTerm - let redProbExpr := redProb.toExpr + -- Create prob.conicForm. + let (canonProb, backwardMap) ← getCanonizedProblemAndBwdMap probTerm + let canonProbExpr := canonProb.toExpr let probName ← getProblemName probInstance.raw - simpleAddDefn (probName ++ `reduced) redProbExpr + simpleAddDefn (probName ++ `conicForm) canonProbExpr - -- Call the solver on prob.reduced and get a point in E. - let (coeffsData, sections) ← determineCoeffsFromExpr redProb + -- Call the solver on prob.conicForm and get a point in E. + let (coeffsData, sections) ← determineCoeffsFromExpr canonProb trace[CvxLean.debug] "Coeffs data:\n{coeffsData}" - let solData ← solutionDataFromProblemData redProb coeffsData sections + let solData ← solutionDataFromProblemData canonProb coeffsData sections trace[CvxLean.debug] "Solution data:\n{solData}" -- Add status to the environment. @@ -84,8 +84,8 @@ unsafe def evalSolve : CommandElab := fun stx => pure () -- Solution makes sense, handle the numerical solution. - let solPointExpr ← exprFromSolutionData redProb solData - trace[CvxLean.debug] "Solution point (reduced problem): {solPointExpr}" + let solPointExpr ← exprFromSolutionData canonProb solData + trace[CvxLean.debug] "Solution point (canonized problem): {solPointExpr}" let backwardMapFloat ← realToFloat <| ← whnf backwardMap let solPointExprFloat ← realToFloat solPointExpr @@ -97,7 +97,7 @@ unsafe def evalSolve : CommandElab := fun stx => simpleAddAndCompileDefn (probName ++ `solution) probSolPointFloat -- Also add value of optimal point. - let probSolValue := mkApp redProb.objFun solPointExpr + let probSolValue := mkApp canonProb.objFun solPointExpr let probSolValueFloat ← realToFloat probSolValue check probSolValueFloat diff --git a/CvxLean/Demos/LT2024.lean b/CvxLean/Demos/LT2024.lean index a47c050b..742b94a8 100644 --- a/CvxLean/Demos/LT2024.lean +++ b/CvxLean/Demos/LT2024.lean @@ -45,7 +45,7 @@ equivalence eqv₂/q₂ : p₂ := by solve q₂ -#print q₂.reduced +#print q₂.conicForm #eval q₂.status #eval q₂.solution @@ -81,7 +81,7 @@ equivalence* eqv₃/q₃ : p₃ 100 10 0.5 2 0.5 2 := by solve q₃ -#print q₃.reduced +#print q₃.conicForm #eval q₃.status #eval q₃.solution diff --git a/CvxLean/Examples/CovarianceEstimation.lean b/CvxLean/Examples/CovarianceEstimation.lean index cf2ca3e3..97940e8a 100644 --- a/CvxLean/Examples/CovarianceEstimation.lean +++ b/CvxLean/Examples/CovarianceEstimation.lean @@ -86,7 +86,7 @@ def yₚ : Fin Nₚ → Fin nₚ → ℝ := ![![0, 2], ![2, 0], ![-2, 0], ![0, - solve covEstimationConvex nₚ Nₚ αₚ yₚ -#print covEstimationConvex.reduced +#print covEstimationConvex.conicForm -- minimize -- -(-(Nₚ • log (sqrt ((2 * π) ^ nₚ)) + Nₚ • (-Vec.sum t.0 / 2)) + -- -(↑Nₚ * trace ((covarianceMatrix fun i => yₚ i) * Rᵀ) / 2)) diff --git a/CvxLean/Examples/HypersonicShapeDesign.lean b/CvxLean/Examples/HypersonicShapeDesign.lean index 15c2e4d1..90e401e9 100644 --- a/CvxLean/Examples/HypersonicShapeDesign.lean +++ b/CvxLean/Examples/HypersonicShapeDesign.lean @@ -61,7 +61,7 @@ lemma one_sub_bₚ_nonneg : 0 ≤ 1 - bₚ := by time_cmd solve hypersonicShapeDesignConvex aₚ bₚ aₚ_nonneg bₚ_nonneg bₚ_lt_one -#print hypersonicShapeDesignConvex.reduced +#print hypersonicShapeDesignConvex.conicForm -- Final width of wedge. def wₚ_opt := eqv₁.backward_map aₚ.float bₚ.float hypersonicShapeDesignConvex.solution @@ -116,7 +116,7 @@ equivalence* eqv₂/hypersonicShapeDesignSimpler (a b : ℝ) (ha : 0 ≤ a) (hb time_cmd solve hypersonicShapeDesignSimpler aₚ bₚ aₚ_nonneg bₚ_nonneg bₚ_lt_one -#print hypersonicShapeDesignSimpler.reduced +#print hypersonicShapeDesignSimpler.conicForm -- Final width of wedge. def wₚ'_opt := diff --git a/CvxLean/Examples/VehicleSpeedScheduling.lean b/CvxLean/Examples/VehicleSpeedScheduling.lean index 9d36e319..463c7271 100644 --- a/CvxLean/Examples/VehicleSpeedScheduling.lean +++ b/CvxLean/Examples/VehicleSpeedScheduling.lean @@ -93,10 +93,10 @@ equivalence* eqv₁/vehSpeedSchedConvex (n : ℕ) (d : Fin n → ℝ) -- The problem is technically in DCP form if `F` is DCP convex. The only issue is that we do not -- have an atom for the perspective function, so the objective function --- `Vec.sum (t * Vec.map F (d / t))` cannot be reduced directly. +-- `Vec.sum (t * Vec.map F (d / t))` cannot be canonized directly. -- However, if we fix `F`, we can use other atoms. For example, if `F` is quadratic, the problem can --- be reduced. Let `F(s) = a * s^2 + b * s + c` with `0 ≤ a`. +-- be canonized. Let `F(s) = a * s^2 + b * s + c` with `0 ≤ a`. equivalence* eqv₂/vehSpeedSchedQuadratic (n : ℕ) (d : Fin n → ℝ) (τmin τmax smin smax : Fin n → ℝ) (a b c : ℝ) (h_n_pos : 0 < n) (h_d_pos : StrongLT 0 d) diff --git a/CvxLean/Tactic/DCP/AtomCmd.lean b/CvxLean/Tactic/DCP/AtomCmd.lean index a3485367..7a099462 100644 --- a/CvxLean/Tactic/DCP/AtomCmd.lean +++ b/CvxLean/Tactic/DCP/AtomCmd.lean @@ -91,9 +91,9 @@ def getMonoArgsCount (curv : Curvature) (argKinds : Array ArgKind) : ℕ := | Curvature.Convex => 1 + acc | _ => acc) 0 -/-- Use the DCP procedure to reduce the graph implementation to a problem that +/-- Use the DCP procedure to canon the graph implementation to a problem that uses only cone constraints and affine atoms. -/ -def reduceAtomData (objCurv : Curvature) (atomData : GraphAtomData) : CommandElabM GraphAtomData := do +def canonAtomData (objCurv : Curvature) (atomData : GraphAtomData) : CommandElabM GraphAtomData := do liftTermElabM do -- `xs` are the arguments of the atom. lambdaTelescope atomData.expr fun xs atomExpr => do @@ -149,7 +149,7 @@ def reduceAtomData (objCurv : Curvature) (atomData : GraphAtomData) : CommandEla for c in pat.optimality.constr.map Tree.val do trace[Meta.debug] "pat opt constr: {c}" check c - -- `vs1` are the variables already present in the unreduced graph implementation. + -- `vs1` are the variables already present in the uncanon graph implementation. let vs1 := originalVarsDecls.map (mkFVar ·.fvarId) -- `vs2` are the variables to be added to the graph implementation. let vs2 := pat.newVarDecls.toArray.map (mkFVar ·.fvarId) @@ -160,8 +160,8 @@ def reduceAtomData (objCurv : Curvature) (atomData : GraphAtomData) : CommandEla trace[Meta.debug] "xs: {xs}" -- TODO: move because copied from DCP tactic. - let reducedConstrs := pat.reducedExprs.constr.map Tree.val - let reducedConstrs := reducedConstrs.filterIdx (fun i => ¬ pat.isVCond[i]!) + let canonConstrs := pat.canonExprs.constr.map Tree.val + let canonConstrs := canonConstrs.filterIdx (fun i => ¬ pat.isVCond[i]!) -- TODO: move because copied from DCP tactic. let newConstrProofs := pat.feasibility.fold #[] fun acc fs => @@ -219,18 +219,18 @@ def reduceAtomData (objCurv : Curvature) (atomData : GraphAtomData) : CommandEla for nf in newFeasibility do trace[Meta.debug] "newFeasibility: {← inferType nf}" - let constraintsFromReducedConstraints := + let constraintsFromCanonConstraints := pat.optimality.constr.map Tree.val - for cfrc in constraintsFromReducedConstraints do - trace[Meta.debug] "constraintsFromReducedConstraints: {← inferType cfrc}" + for cfrc in constraintsFromCanonConstraints do + trace[Meta.debug] "constraintsFromCanonConstraints: {← inferType cfrc}" - if reducedConstrs.size != constraintsFromReducedConstraints.size then - throwError ("Expected same length: {reducedConstrs} and " ++ - "{constraintsFromReducedConstraints}") + if canonConstrs.size != constraintsFromCanonConstraints.size then + throwError ("Expected same length: {canonConstrs} and " ++ + "{constraintsFromCanonConstraints}") - let objFunFromReducedObjFun := pat.optimality.objFun.val - trace[Meta.debug] "objFunFromReducedObjFun: {← inferType objFunFromReducedObjFun}" + let objFunFromCanonObjFun := pat.optimality.objFun.val + trace[Meta.debug] "objFunFromCanonObjFun: {← inferType objFunFromCanonObjFun}" trace[Meta.debug] "pat.optimality.objFun: {← inferType atomData.optimality}" @@ -238,18 +238,18 @@ def reduceAtomData (objCurv : Curvature) (atomData : GraphAtomData) : CommandEla withLocalDeclsDNondep bconds fun bs => do let optimalityXsBConds := mkAppN atomData.optimality (xs ++ bs ++ vs1) trace[Meta.debug] "newOptimality: {← inferType optimalityXsBConds}" - withLocalDeclsDNondep (reducedConstrs.map (fun rc => (`_, rc))) fun cs => do + withLocalDeclsDNondep (canonConstrs.map (fun rc => (`_, rc))) fun cs => do -- First, apply all constraints. - let mut optimalityAfterReduced := optimalityXsBConds - for i in [:reducedConstrs.size] do - trace[Meta.debug] "optimalityAfterReduced: {← inferType optimalityAfterReduced}" - let c := mkApp constraintsFromReducedConstraints[i]! cs[i]! - optimalityAfterReduced := mkApp optimalityAfterReduced c - -- Then, adjust the condition using `objFunFromReducedObjFun`. - trace[Meta.debug] "optimalityAfterReduced: {← inferType optimalityAfterReduced}" + let mut optimalityAfterCanon := optimalityXsBConds + for i in [:canonConstrs.size] do + trace[Meta.debug] "optimalityAfterCanon: {← inferType optimalityAfterCanon}" + let c := mkApp constraintsFromCanonConstraints[i]! cs[i]! + optimalityAfterCanon := mkApp optimalityAfterCanon c + -- Then, adjust the condition using `objFunFromCanonObjFun`. + trace[Meta.debug] "optimalityAfterCanon: {← inferType optimalityAfterCanon}" let monoArgsCount := getMonoArgsCount objCurv atomData.argKinds let optimalityAfterApplyWithConditionAdjusted ← - lambdaTelescope (← whnf optimalityAfterReduced) <| fun xs e => do + lambdaTelescope (← whnf optimalityAfterCanon) <| fun xs e => do -- Every extra argument has an extra condition, e.g. x', x ≤ x. trace[Meta.debug] "xs: {xs}" let monoArgs := xs[:2 * monoArgsCount] @@ -260,16 +260,16 @@ def reduceAtomData (objCurv : Curvature) (atomData : GraphAtomData) : CommandEla if atomData.curvature == Curvature.Convex then mkAppOptM ``le_trans #[ atomRange, none, none, none, none, - optCondition, objFunFromReducedObjFun] + optCondition, objFunFromCanonObjFun] else -- TODO: concave. but convex_set too? mkAppOptM ``le_trans #[ atomRange, none, none, none, none, - objFunFromReducedObjFun, optCondition] + objFunFromCanonObjFun, optCondition] mkLambdaFVars monoArgs newCond trace[Meta.debug] "optimalityAfterApplyWithConditionAdjusted: {← inferType optimalityAfterApplyWithConditionAdjusted}" - trace[Meta.debug] "newOptimality applied: {← inferType optimalityAfterReduced}" + trace[Meta.debug] "newOptimality applied: {← inferType optimalityAfterCanon}" let ds := pat.newConstrVarsArray.map (mkFVar ·.fvarId) mkLambdaFVars (xs ++ bs ++ vs1 ++ vs2 ++ cs ++ ds) optimalityAfterApplyWithConditionAdjusted @@ -279,10 +279,10 @@ def reduceAtomData (objCurv : Curvature) (atomData : GraphAtomData) : CommandEla for vcondElim in atomData.vcondElim do let newVCondElim := mkAppN vcondElim (xs ++ vs1) let newVCondElim ← - withLocalDeclsDNondep (reducedConstrs.map (fun rc => (`_, rc))) fun cs => do + withLocalDeclsDNondep (canonConstrs.map (fun rc => (`_, rc))) fun cs => do let mut newVCondElim := newVCondElim - for i in [:reducedConstrs.size] do - let c := mkApp constraintsFromReducedConstraints[i]! cs[i]! + for i in [:canonConstrs.size] do + let c := mkApp constraintsFromCanonConstraints[i]! cs[i]! newVCondElim := mkApp newVCondElim c let ds := pat.newConstrVarsArray.map (mkFVar ·.fvarId) mkLambdaFVars (xs ++ vs1 ++ vs2) <| ← mkLambdaFVars (cs ++ ds) newVCondElim @@ -293,8 +293,8 @@ def reduceAtomData (objCurv : Curvature) (atomData : GraphAtomData) : CommandEla (← pat.newVarDecls.toArray.mapM fun decl => do return (decl.userName, ← mkLambdaFVars xs decl.type)) impObjFun := ← mkLambdaFVars xs $ ← mkLambdaFVars (vs1 ++ vs2) $ - pat.reducedExprs.objFun.val - impConstrs := ← (reducedConstrs ++ pat.newConstrs).mapM + pat.canonExprs.objFun.val + impConstrs := ← (canonConstrs ++ pat.newConstrs).mapM (fun c => do withLocalDeclsDNondep bconds fun bs => do return ← mkLambdaFVars xs <| ← mkLambdaFVars bs <| ← mkLambdaFVars (vs1 ++ vs2) c) @@ -600,10 +600,10 @@ def elabVCondElim (curv : Curvature) (argDecls : Array LocalDecl) (bconds vconds -- | Curvature.ConvexSet => Curvature.ConvexSet -- | _ => Curvature.Affine - trace[Meta.debug] "before reduce sol eq atom: {atomData.solEqAtom}" + trace[Meta.debug] "before canon sol eq atom: {atomData.solEqAtom}" - let atomData ← reduceAtomData objCurv atomData - -- trace[Meta.debug] "HERE Reduced atom: {atomData}" + let atomData ← canonAtomData objCurv atomData + -- trace[Meta.debug] "HERE Canon atom: {atomData}" let atomData ← addAtomDataDecls id.getId atomData -- trace[Meta.debug] "HERE Added atom" @@ -659,7 +659,7 @@ def elabVCondElim (curv : Curvature) (argDecls : Array LocalDecl) (bconds vconds } return atomData - let atomData ← reduceAtomData atomData.curvature atomData--Curvature.Affine atomData + let atomData ← canonAtomData atomData.curvature atomData--Curvature.Affine atomData let atomData ← addAtomDataDecls id.getId atomData liftTermElabM do diff --git a/CvxLean/Tactic/DCP/DCP.lean b/CvxLean/Tactic/DCP/DCP.lean index e072682e..99561821 100644 --- a/CvxLean/Tactic/DCP/DCP.lean +++ b/CvxLean/Tactic/DCP/DCP.lean @@ -190,19 +190,19 @@ def mkNewVarDeclList (newVars : OC NewVarsTree) : newVarDecls := t.fold newVarDecls Array.append return newVarDecls.toList -abbrev ReducedExpr := Expr -abbrev ReducedExprsTree := Tree ReducedExpr ReducedExpr +abbrev CanonExpr := Expr +abbrev CanonExprsTree := Tree CanonExpr CanonExpr /-- -/ -partial def mkReducedExprs : GraphAtomDataTree → NewVarsTree → MetaM (Tree Expr Expr) +partial def mkCanonExprs : GraphAtomDataTree → NewVarsTree → MetaM (Tree Expr Expr) | Tree.node atom childAtoms, Tree.node newVars childNewVars => do - let mut childReducedExprs := #[] + let mut childCanonExprs := #[] for i in [:childAtoms.size] do - childReducedExprs := childReducedExprs.push $ ← mkReducedExprs childAtoms[i]! childNewVars[i]! - let reducedExpr := atom.impObjFun - let reducedExpr := mkAppNBeta reducedExpr (childReducedExprs.map (·.val)) - let reducedExpr := mkAppNBeta reducedExpr (newVars.map (mkFVar ·.fvarId)) - return Tree.node reducedExpr childReducedExprs + childCanonExprs := childCanonExprs.push $ ← mkCanonExprs childAtoms[i]! childNewVars[i]! + let canonExpr := atom.impObjFun + let canonExpr := mkAppNBeta canonExpr (childCanonExprs.map (·.val)) + let canonExpr := mkAppNBeta canonExpr (newVars.map (mkFVar ·.fvarId)) + return Tree.node canonExpr childCanonExprs | Tree.leaf e, Tree.leaf () => pure $ Tree.leaf e | _, _ => throwError "Tree mismatch" @@ -217,13 +217,13 @@ abbrev VConds := Array VCond abbrev VCondsTree := Tree VConds Unit /-- -/ -partial def mkNewConstrs : GraphAtomDataTree → BCondsTree → NewVarsTree → ReducedExprsTree → MetaM NewConstrsTree - | Tree.node atom childAtoms, Tree.node bconds childBConds, Tree.node newVars childNewVars, Tree.node reducedExprs childReducedExprs => do +partial def mkNewConstrs : GraphAtomDataTree → BCondsTree → NewVarsTree → CanonExprsTree → MetaM NewConstrsTree + | Tree.node atom childAtoms, Tree.node bconds childBConds, Tree.node newVars childNewVars, Tree.node canonExprs childCanonExprs => do let mut childNewConstrs := #[] for i in [:childAtoms.size] do - childNewConstrs := childNewConstrs.push <| ← mkNewConstrs childAtoms[i]! childBConds[i]! childNewVars[i]! childReducedExprs[i]! + childNewConstrs := childNewConstrs.push <| ← mkNewConstrs childAtoms[i]! childBConds[i]! childNewVars[i]! childCanonExprs[i]! let newConstrs := atom.impConstrs - let newConstrs := newConstrs.map (mkAppNBeta · (childReducedExprs.map Tree.val)) + let newConstrs := newConstrs.map (mkAppNBeta · (childCanonExprs.map Tree.val)) let newConstrs := newConstrs.map (mkAppNBeta · bconds) let newConstrs := newConstrs.map (mkAppNBeta · (newVars.map (mkFVar ·.fvarId))) return Tree.node newConstrs childNewConstrs @@ -273,36 +273,36 @@ abbrev NewVarAssignment := Expr abbrev Solution := Array NewVarAssignment -structure ReducedExprWithSolution where - reducedExpr : ReducedExpr +structure CanonExprWithSolution where + canonExpr : CanonExpr solution : Solution -instance : Inhabited ReducedExprWithSolution := ⟨⟨default, default⟩⟩ +instance : Inhabited CanonExprWithSolution := ⟨⟨default, default⟩⟩ -abbrev ReducedExprsWithSolutionTree := Tree ReducedExprWithSolution ReducedExprWithSolution +abbrev CanonExprsWithSolutionTree := Tree CanonExprWithSolution CanonExprWithSolution -/-- Returns the reduced expression and an array of forward images of new vars -/ -partial def mkReducedWithSolution : GraphAtomDataTree → MetaM ReducedExprsWithSolutionTree +/-- Returns the canon expression and an array of forward images of new vars -/ +partial def mkCanonWithSolution : GraphAtomDataTree → MetaM CanonExprsWithSolutionTree | Tree.node atom childAtoms => do - let mut childReducedExprs := #[] + let mut childCanonExprs := #[] for i in [:childAtoms.size] do - childReducedExprs := childReducedExprs.push $ ← mkReducedWithSolution childAtoms[i]! - let sols := (atom.solution.map (mkAppNBeta · (childReducedExprs.1.map (·.val.1)).toArray)) - let reducedExpr := atom.impObjFun - let reducedExpr := mkAppNBeta reducedExpr (childReducedExprs.1.map (·.val.1)).toArray - let reducedExpr := mkAppNBeta reducedExpr sols - return Tree.node ⟨reducedExpr, sols⟩ childReducedExprs + childCanonExprs := childCanonExprs.push $ ← mkCanonWithSolution childAtoms[i]! + let sols := (atom.solution.map (mkAppNBeta · (childCanonExprs.1.map (·.val.1)).toArray)) + let canonExpr := atom.impObjFun + let canonExpr := mkAppNBeta canonExpr (childCanonExprs.1.map (·.val.1)).toArray + let canonExpr := mkAppNBeta canonExpr sols + return Tree.node ⟨canonExpr, sols⟩ childCanonExprs | Tree.leaf e => return Tree.leaf ⟨e, #[]⟩ /-- Combine all the solutions introduced by every atom expansion. A solution tells us how to assign new variables from old ones. Here, we collect all such assignments, which will be used later on to build the forward map between the -original and reduced problems. -/ -def mkForwardImagesNewVars (reducedWithSolution : OC ReducedExprsWithSolutionTree) : MetaM Solution := do - let reducedWithSolutionTrees := #[reducedWithSolution.objFun] ++ reducedWithSolution.constr +original and canon problems. -/ +def mkForwardImagesNewVars (canonWithSolution : OC CanonExprsWithSolutionTree) : MetaM Solution := do + let canonWithSolutionTrees := #[canonWithSolution.objFun] ++ canonWithSolution.constr let mut fm := #[] - for t in reducedWithSolutionTrees do + for t in canonWithSolutionTrees do fm := t.fold fm (fun acc a => Array.append acc a.solution) trace[Meta.debug] "forwardImagesNewVars {fm}" return fm @@ -313,17 +313,17 @@ abbrev SolEqAtomProofsTree := Tree SolEqAtomProof SolEqAtomProof /-- Proofs .-/ partial def mkSolEqAtom : GraphAtomDataTree → - ReducedExprsWithSolutionTree → + CanonExprsWithSolutionTree → VCondsTree → MetaM SolEqAtomProofsTree | Tree.node atom childAtoms, - Tree.node reducedWithSolution childReducedWithSolution, + Tree.node canonWithSolution childCanonWithSolution, Tree.node vcondVars childVCondVars => do -- Recursive calls for arguments. let mut childSolEqAtom := #[] for i in [:childAtoms.size] do childSolEqAtom := childSolEqAtom.push <| - ← mkSolEqAtom childAtoms[i]! childReducedWithSolution[i]! childVCondVars[i]! + ← mkSolEqAtom childAtoms[i]! childCanonWithSolution[i]! childVCondVars[i]! -- Rewrite arguments in atom expr. let mut solEqAtomR ← mkEqRefl atom.expr for c in childSolEqAtom do @@ -331,13 +331,13 @@ partial def mkSolEqAtom : -- Use solEqAtom of children to rewrite the arguments in the vconditions. let mut vconds := #[] for i in [:vcondVars.size] do - let mut vcondEqReducedVCond ← mkEqRefl atom.vconds[i]!.2 + let mut vcondEqCanonVCond ← mkEqRefl atom.vconds[i]!.2 for c in childSolEqAtom do - vcondEqReducedVCond ← mkCongr vcondEqReducedVCond c.val - vconds := vconds.push $ ← mkEqMPR vcondEqReducedVCond vcondVars[i]! + vcondEqCanonVCond ← mkCongr vcondEqCanonVCond c.val + vconds := vconds.push $ ← mkEqMPR vcondEqCanonVCond vcondVars[i]! -- Apply solEqAtom property of the atom. let solEqAtomL := atom.solEqAtom - let solEqAtomL := mkAppN solEqAtomL (childReducedWithSolution.map (·.val.1)) + let solEqAtomL := mkAppN solEqAtomL (childCanonWithSolution.map (·.val.1)) let solEqAtomL := mkAppN solEqAtomL vconds let solEqAtom ← mkEqTrans solEqAtomL solEqAtomR return Tree.node solEqAtom childSolEqAtom @@ -353,31 +353,31 @@ abbrev FeasibilityProofsTree := Tree FeasibilityProofs Unit /-- -/ partial def mkFeasibility : GraphAtomDataTree → - ReducedExprsWithSolutionTree → + CanonExprsWithSolutionTree → BCondsTree → VCondsTree → SolEqAtomProofsTree → MetaM FeasibilityProofsTree | Tree.node atom childAtoms, - Tree.node _reducedWithSolution childReducedWithSolution, + Tree.node _canonWithSolution childCanonWithSolution, Tree.node bconds childBConds, Tree.node vcondVars childVCondVars, Tree.node _solEqAtom childSolEqAtom => do -- Recursive calls for arguments. let mut childFeasibility := #[] for i in [:childAtoms.size] do - let c ← mkFeasibility childAtoms[i]! childReducedWithSolution[i]! childBConds[i]! childVCondVars[i]! childSolEqAtom[i]! + let c ← mkFeasibility childAtoms[i]! childCanonWithSolution[i]! childBConds[i]! childVCondVars[i]! childSolEqAtom[i]! childFeasibility := childFeasibility.push c -- Use solEqAtom of children to rewrite the arguments in the vconditions. let mut vconds := #[] for i in [:vcondVars.size] do - let mut vcondEqReducedVCond ← mkEqRefl atom.vconds[i]!.2 + let mut vcondEqCanonVCond ← mkEqRefl atom.vconds[i]!.2 for c in childSolEqAtom do - vcondEqReducedVCond ← mkCongr vcondEqReducedVCond c.val - vconds := vconds.push $ ← mkEqMPR vcondEqReducedVCond vcondVars[i]! + vcondEqCanonVCond ← mkCongr vcondEqCanonVCond c.val + vconds := vconds.push $ ← mkEqMPR vcondEqCanonVCond vcondVars[i]! -- Apply feasibility property of the atom. let feasibility := atom.feasibility - let feasibility := feasibility.map (mkAppN · (childReducedWithSolution.map (·.val.1))) + let feasibility := feasibility.map (mkAppN · (childCanonWithSolution.map (·.val.1))) let feasibility := feasibility.map (mkAppN · bconds) let feasibility := feasibility.map (mkAppN · vconds) let _ ← feasibility.mapM check @@ -411,7 +411,7 @@ abbrev OptimalityAndVCondElimProofsTree := Tree OptimalityAndVCondElimProofs Opt partial def mkOptimalityAndVCondElim : GraphAtomDataTree → ArgumentsTree → - ReducedExprsTree → + CanonExprsTree → NewVarsTree → NewConstrVarsTree → CurvatureTree → @@ -419,7 +419,7 @@ partial def mkOptimalityAndVCondElim : MetaM OptimalityAndVCondElimProofsTree | Tree.node atom childAtoms, Tree.node args childArgs, - Tree.node _reducedExpr childReducedExpr, + Tree.node _canonExpr childCanonExpr, Tree.node newVars childNewVars, Tree.node newConstrVars childNewConstrVars, Tree.node curvature childCurvature, @@ -429,7 +429,7 @@ partial def mkOptimalityAndVCondElim : let mut childOptimalityFiltered := #[] for i in [:childAtoms.size] do if atom.argKinds[i]! != ArgKind.Constant ∧ atom.argKinds[i]! != ArgKind.Neither then - let opt ← mkOptimalityAndVCondElim childAtoms[i]! childArgs[i]! childReducedExpr[i]! + let opt ← mkOptimalityAndVCondElim childAtoms[i]! childArgs[i]! childCanonExpr[i]! childNewVars[i]! childNewConstrVars[i]! childCurvature[i]! childBConds[i]! childOptimality := childOptimality.push opt childOptimalityFiltered := childOptimalityFiltered.push opt @@ -446,7 +446,7 @@ partial def mkOptimalityAndVCondElim : | Curvature.Concave, Curvature.Affine => mkAppM ``And.left #[atom.optimality] | Curvature.Convex, Curvature.Affine => mkAppM ``And.right #[atom.optimality] | _, _ => pure atom.optimality - let optimality := mkAppN optimality (childReducedExpr.map Tree.val) + let optimality := mkAppN optimality (childCanonExpr.map Tree.val) let optimality := mkAppN optimality bconds check optimality let optimality := mkAppN optimality (newVars.map (mkFVar ·.fvarId)) @@ -457,7 +457,7 @@ partial def mkOptimalityAndVCondElim : -- Apply vcond elim property of atom. let vcondElim := atom.vcondElim - let vcondElim := vcondElim.map (mkAppN · (childReducedExpr.map Tree.val)) + let vcondElim := vcondElim.map (mkAppN · (childCanonExpr.map Tree.val)) let vcondElim := vcondElim.map (mkAppN · (newVars.map (mkFVar ·.fvarId))) let vcondElim := vcondElim.map (mkAppN · (newConstrVars.map (mkFVar ·.fvarId))) let vcondElim := vcondElim.map (mkAppN · monoArgs) @@ -599,16 +599,16 @@ def makeConstrForward (oldDomain : Expr) (xs : Array Expr) (originalConstrVars : return constrForward /-- -/ -def makeObjFunBackward (newDomain : Expr) (redProblem : Expr) (xs : Array Expr) (ys : Array Expr) (objFunOpt : Expr) - (redConstrs : Array Expr) (newConstrs : Array Expr) +def makeObjFunBackward (newDomain : Expr) (canonProblem : Expr) (xs : Array Expr) (ys : Array Expr) (objFunOpt : Expr) + (canonConstrs : Array Expr) (newConstrs : Array Expr) (newConstrVars : Array LocalDecl) : MetaM Expr := do -- ∀ {x : E}, Minimization.constraints q x → Minimization.objFun p (g x) ≤ Minimization.objFun q x withLocalDeclD `p newDomain fun p => do let prs := (← Meta.mkProjections newDomain p).map (·.2.2) - withLocalDeclD `h (← mkAppM ``Minimization.constraints #[redProblem, p]) fun h => do - let (_, cprs) := Meta.composeAndWithProj (redConstrs ++ newConstrs).toList + withLocalDeclD `h (← mkAppM ``Minimization.constraints #[canonProblem, p]) fun h => do + let (_, cprs) := Meta.composeAndWithProj (canonConstrs ++ newConstrs).toList let hProj := cprs h let objFunBackwardBody := objFunOpt let objFunBackwardBody := objFunBackwardBody.replaceFVars @@ -621,15 +621,15 @@ def makeObjFunBackward (newDomain : Expr) (redProblem : Expr) (xs : Array Expr) return objFunBackward /-- -/ -def makeConstrBackward (vcondElimMap : Std.HashMap Nat Expr) (newDomain : Expr) (redProblem : Expr) (xs : Array Expr) (ys : Array Expr) (constrOpt : Array Expr) - (redConstrs : Array Expr) (newConstrs : Array Expr) (newConstrVars : Array LocalDecl) : MetaM Expr := do +def makeConstrBackward (vcondElimMap : Std.HashMap Nat Expr) (newDomain : Expr) (canonProblem : Expr) (xs : Array Expr) (ys : Array Expr) (constrOpt : Array Expr) + (canonConstrs : Array Expr) (newConstrs : Array Expr) (newConstrVars : Array LocalDecl) : MetaM Expr := do -- ∀ {x : E}, Minimization.constraints q x → Minimization.constraints p (g x) withLocalDeclD `p newDomain fun p => do let prs := (← Meta.mkProjections newDomain p).map (·.2.2) - withLocalDeclD `h (← mkAppM ``Minimization.constraints #[redProblem, p]) fun h => do - let (_, cprs) := Meta.composeAndWithProj (redConstrs ++ newConstrs).toList + withLocalDeclD `h (← mkAppM ``Minimization.constraints #[canonProblem, p]) fun h => do + let (_, cprs) := Meta.composeAndWithProj (canonConstrs ++ newConstrs).toList let hProj := cprs h let mut constrBackwardProofs := #[] let mut filteredCounter := 0 @@ -731,18 +731,18 @@ withExistingLocalDecls originalVarsDecls.toList do /-- -/ def mkSolEqAtomOC (originalVarsDecls : Array LocalDecl) (atoms : OC (Tree GraphAtomData Expr)) - (reducedWithSolution : OC ReducedExprsWithSolutionTree) + (canonWithSolution : OC CanonExprsWithSolutionTree) (vcondVars : OC (Tree (Array Expr) Unit)) (originalConstrVars : Array LocalDecl) : MetaM (OC (Tree Expr Expr)) := withExistingLocalDecls originalVarsDecls.toList do withExistingLocalDecls originalConstrVars.toList do - let solEqAtom ← OC.map3M mkSolEqAtom atoms reducedWithSolution vcondVars + let solEqAtom ← OC.map3M mkSolEqAtom atoms canonWithSolution vcondVars trace[Meta.debug] "solEqAtom {solEqAtom}" return solEqAtom /-- -/ def mkFeasibilityOC (originalVarsDecls : Array LocalDecl) (atoms : OC GraphAtomDataTree) - (reducedWithSolution : OC ReducedExprsWithSolutionTree) + (canonWithSolution : OC CanonExprsWithSolutionTree) (bconds : OC BCondsTree) (vcondVars : OC VCondsTree) (originalConstrVars : Array LocalDecl) @@ -750,26 +750,26 @@ def mkFeasibilityOC (originalVarsDecls : Array LocalDecl) MetaM (OC FeasibilityProofsTree) := withExistingLocalDecls originalVarsDecls.toList do withExistingLocalDecls originalConstrVars.toList do - let feasibility ← OC.map5M mkFeasibility atoms reducedWithSolution bconds vcondVars solEqAtom + let feasibility ← OC.map5M mkFeasibility atoms canonWithSolution bconds vcondVars solEqAtom trace[Meta.debug] "feasibility {feasibility}" return feasibility /-- -/ -def mkReducedExprsOC (originalVarsDecls : Array LocalDecl) (newVarDecls : List LocalDecl) +def mkCanonExprsOC (originalVarsDecls : Array LocalDecl) (newVarDecls : List LocalDecl) (atoms : OC (Tree GraphAtomData Expr)) (newVars : OC (Tree (Array LocalDecl) Unit)) : MetaM (OC (Tree Expr Expr)) := withExistingLocalDecls originalVarsDecls.toList do withExistingLocalDecls newVarDecls do - let reducedExprs ← OC.map2M mkReducedExprs atoms newVars - trace[Meta.debug] "reducedExprs {reducedExprs}" - return reducedExprs + let canonExprs ← OC.map2M mkCanonExprs atoms newVars + trace[Meta.debug] "canonExprs {canonExprs}" + return canonExprs /-- -/ def mkNewConstrsOC (originalVarsDecls : Array LocalDecl) (newVarDecls : List LocalDecl) (bconds : OC BCondsTree) - (atoms : OC (Tree GraphAtomData Expr)) (newVars : OC (Tree (Array LocalDecl) Unit)) (reducedExprs : OC (Tree Expr Expr)) + (atoms : OC (Tree GraphAtomData Expr)) (newVars : OC (Tree (Array LocalDecl) Unit)) (canonExprs : OC (Tree Expr Expr)) : MetaM (Array Expr × OC (Tree (Array LocalDecl) Unit) × Array LocalDecl):= withExistingLocalDecls (originalVarsDecls.toList) do withExistingLocalDecls newVarDecls do - let newConstrs ← OC.map4M mkNewConstrs atoms bconds newVars reducedExprs + let newConstrs ← OC.map4M mkNewConstrs atoms bconds newVars canonExprs trace[Meta.debug] "newConstrs {newConstrs}" let newConstrVars ← OC.mapM mkNewConstrVars newConstrs trace[Meta.debug] "newConstrs {newConstrs}" @@ -784,7 +784,7 @@ def mkOptimalityAndVCondElimOC (originalVarsDecls : Array LocalDecl) (newVarDecl (newConstrVarsArray : Array LocalDecl) (atoms : OC (Tree GraphAtomData Expr)) (args : OC (Tree (Array Expr) Unit)) - (reducedExprs : OC (Tree Expr Expr)) + (canonExprs : OC (Tree Expr Expr)) (newVars : OC (Tree (Array LocalDecl) Unit)) (newConstrVars : OC (Tree (Array LocalDecl) Unit)) (curvature : OC (Tree Curvature Curvature)) @@ -794,7 +794,7 @@ def mkOptimalityAndVCondElimOC (originalVarsDecls : Array LocalDecl) (newVarDecl withExistingLocalDecls originalVarsDecls.toList do withExistingLocalDecls newVarDecls do withExistingLocalDecls newConstrVarsArray.toList do - let optimalityAndVCondElim ← OC.map7M mkOptimalityAndVCondElim atoms args reducedExprs newVars newConstrVars curvature bconds + let optimalityAndVCondElim ← OC.map7M mkOptimalityAndVCondElim atoms args canonExprs newVars newConstrVars curvature bconds let optimality := optimalityAndVCondElim.map (fun oce => oce.map Prod.fst Prod.fst) let vcondElim := optimalityAndVCondElim.map (fun oce => oce.map Prod.snd Prod.snd) trace[Meta.debug] "optimality {optimality}" @@ -824,7 +824,7 @@ structure ProcessedAtomTree where (vcondElimMap : Std.HashMap ℕ Expr) (solEqAtom : OC (Tree Expr Expr)) (feasibility : OC (Tree (Array Expr) Unit)) - (reducedExprs : OC (Tree Expr Expr)) + (canonExprs : OC (Tree Expr Expr)) (optimality : OC (Tree Expr Expr)) instance : Inhabited ProcessedAtomTree := @@ -843,18 +843,18 @@ def mkProcessedAtomTree (objCurv : Curvature) (objFun : Expr) let newVars ← withExistingLocalDecls originalVarsDecls.toList do OC.map2MwithCounter mkNewVars atoms args let newVarDecls ← mkNewVarDeclList newVars - let reducedWithSolution ← withExistingLocalDecls originalVarsDecls.toList do - OC.mapM mkReducedWithSolution atoms + let canonWithSolution ← withExistingLocalDecls originalVarsDecls.toList do + OC.mapM mkCanonWithSolution atoms let forwardImagesNewVars ← withExistingLocalDecls originalVarsDecls.toList do - mkForwardImagesNewVars reducedWithSolution - let solEqAtom ← mkSolEqAtomOC originalVarsDecls atoms reducedWithSolution vcondVars originalConstrVars - let feasibility ← mkFeasibilityOC originalVarsDecls atoms reducedWithSolution bconds vcondVars + mkForwardImagesNewVars canonWithSolution + let solEqAtom ← mkSolEqAtomOC originalVarsDecls atoms canonWithSolution vcondVars originalConstrVars + let feasibility ← mkFeasibilityOC originalVarsDecls atoms canonWithSolution bconds vcondVars originalConstrVars solEqAtom - let reducedExprs ← mkReducedExprsOC originalVarsDecls newVarDecls atoms newVars + let canonExprs ← mkCanonExprsOC originalVarsDecls newVarDecls atoms newVars let (newConstrs, newConstrVars, newConstrVarsArray) - ← mkNewConstrsOC originalVarsDecls newVarDecls bconds atoms newVars reducedExprs + ← mkNewConstrsOC originalVarsDecls newVarDecls bconds atoms newVars canonExprs let (optimality, vcondElimMap) ← mkOptimalityAndVCondElimOC originalVarsDecls newVarDecls - newConstrVarsArray atoms args reducedExprs newVars newConstrVars curvature bconds vcondIdx + newConstrVarsArray atoms args canonExprs newVars newConstrVars curvature bconds vcondIdx return ProcessedAtomTree.mk (originalVarsDecls := originalVarsDecls) @@ -868,7 +868,7 @@ def mkProcessedAtomTree (objCurv : Curvature) (objFun : Expr) (vcondElimMap := vcondElimMap) (solEqAtom := solEqAtom) (feasibility := feasibility) - (reducedExprs := reducedExprs) + (canonExprs := canonExprs) (optimality := optimality) open Meta Elab Tactic @@ -900,7 +900,7 @@ def canonize (ogProblem : MinimizationExpr) : MetaM (MinimizationExpr × Expr) : -- Process the atom tree. let pat ← mkProcessedAtomTree Curvature.Convex objFun constraints originalVarsDecls - -- Create reduced problem and equivalence proof. + -- Create canon problem and equivalence proof. withExistingLocalDecls pat.originalVarsDecls.toList do -- Original problem variables. let originalVars := pat.originalVarsDecls.map fun decl => mkFVar decl.fvarId @@ -918,16 +918,16 @@ def canonize (ogProblem : MinimizationExpr) : MetaM (MinimizationExpr × Expr) : return (objFunForward, constrForward) withExistingLocalDecls pat.newVarDecls do - -- New variables added by the reduction. + -- New variables added by the canonization. let newVars := (pat.newVarDecls.map (mkFVar ·.fvarId)).toArray - -- Reduced variables: originalVars ⊎ newVars. - let redVars ← (originalVars ++ newVars).mapM fun x => do + -- Canon variables: originalVars ⊎ newVars. + let canonVars ← (originalVars ++ newVars).mapM fun x => do let decl ← x.fvarId!.getDecl return (decl.userName, decl.type) -- New domain: D × T where T is the domain of the new variables. - let E := Meta.composeDomain redVars.toList + let E := Meta.composeDomain canonVars.toList -- Function to replace variables by projections in the new domain. let mkDomain := fun e => @@ -936,33 +936,33 @@ def canonize (ogProblem : MinimizationExpr) : MetaM (MinimizationExpr × Expr) : let e := Expr.replaceFVars e (originalVars ++ newVars) prs.toArray mkLambdaFVars #[p] e - -- Reduced problem. - let redConstrs := pat.reducedExprs.constr.map Tree.val - let redConstrs := redConstrs.filterIdx (fun i => ¬ pat.isVCond[i]!) - let redProblem : MinimizationExpr := + -- Canon problem. + let canonConstrs := pat.canonExprs.constr.map Tree.val + let canonConstrs := canonConstrs.filterIdx (fun i => ¬ pat.isVCond[i]!) + let canonProblem : MinimizationExpr := { domain := E codomain := R - objFun := ← mkDomain pat.reducedExprs.objFun.val - constraints := ← mkDomain <| Meta.composeAnd (redConstrs ++ pat.newConstrs).toList } - let redProblemExpr := redProblem.toExpr + objFun := ← mkDomain pat.canonExprs.objFun.val + constraints := ← mkDomain <| Meta.composeAnd (canonConstrs ++ pat.newConstrs).toList } + let canonProblemExpr := canonProblem.toExpr -- Backward map: ψ. let backwardMap ← makeBackwardMap originalVars mkDomain let (objFunBackward, constrBackward) ← withExistingLocalDecls pat.newConstrVarsArray.toList do - let objFunBackward ← makeObjFunBackward E redProblemExpr originalVars newVars - pat.optimality.objFun.val redConstrs pat.newConstrs pat.newConstrVarsArray + let objFunBackward ← makeObjFunBackward E canonProblemExpr originalVars newVars + pat.optimality.objFun.val canonConstrs pat.newConstrs pat.newConstrVarsArray - let constrBackward ← makeConstrBackward pat.vcondElimMap E redProblemExpr originalVars - newVars (pat.optimality.constr.map (·.val)) redConstrs pat.newConstrs + let constrBackward ← makeConstrBackward pat.vcondElimMap E canonProblemExpr originalVars + newVars (pat.optimality.constr.map (·.val)) canonConstrs pat.newConstrs pat.newConstrVarsArray return (objFunBackward, constrBackward) -- Combine forward and backward maps into equivalence witness. let strongEqvProof ← mkAppOptM ``Minimization.StrongEquivalence.mk - #[D, E, R, none, ogProblemExpr, redProblemExpr, + #[D, E, R, none, ogProblemExpr, canonProblemExpr, -- phi forwardMap, -- psi @@ -977,7 +977,7 @@ def canonize (ogProblem : MinimizationExpr) : MetaM (MinimizationExpr × Expr) : objFunBackward] let eqvProof ← mkAppM ``Minimization.Equivalence.ofStrongEquivalence #[strongEqvProof] - return (redProblem, eqvProof) + return (canonProblem, eqvProof) def dcpBuilder : EquivalenceBuilder Unit := fun eqvExpr g => g.withContext do let ogProblem ← eqvExpr.toMinimizationExprLHS diff --git a/CvxLean/Tactic/PreDCP/PreDCP.lean b/CvxLean/Tactic/PreDCP/PreDCP.lean index 615b3f8c..02ae90a1 100644 --- a/CvxLean/Tactic/PreDCP/PreDCP.lean +++ b/CvxLean/Tactic/PreDCP/PreDCP.lean @@ -129,7 +129,7 @@ def evalStep (step : EggRewrite) (vars params : List Name) (paramsDecls : List L -- Distinguish between rewriting props and reals. No need to apply congruence if we are -- rewriting the whole constraint. if !(← inferType lhsSubExprAtProb).isProp then - -- Reduce to equality goal for real rewerites . + -- Reduce to equality goal for real rewrites . if !atObjFun then let gs ← g.apply (mkConst ``Iff.of_eq) if gs.length != 1 then diff --git a/CvxLean/Test/PreDCP/DQCP.lean b/CvxLean/Test/PreDCP/DQCP.lean index 0ffa868a..f65dc6b7 100644 --- a/CvxLean/Test/PreDCP/DQCP.lean +++ b/CvxLean/Test/PreDCP/DQCP.lean @@ -37,9 +37,9 @@ time_cmd reduction redqcp1/dqcp1 : qcp1 := by solve dqcp1 -#print dqcp1.reduced -- ... -#eval dqcp1.value -- -2.000000 -#eval dqcp1.solution -- (2.000000, 2.000000) +#print dqcp1.conicForm -- ... +#eval dqcp1.value -- -2.000000 +#eval dqcp1.solution -- (2.000000, 2.000000) end QCP1 @@ -61,9 +61,9 @@ time_cmd equivalence redqcp2/dqcp2 : qcp2 0.05 0.65 := by solve dqcp2 -#print dqcp2.reduced -- ... -#eval dqcp2.value -- 0.021286 -#eval dqcp2.solution -- 0.989524 +#print dqcp2.conicForm -- ... +#eval dqcp2.value -- 0.021286 +#eval dqcp2.solution -- 0.989524 end QCP2 @@ -83,9 +83,9 @@ time_cmd reduction redqcp3/dqcp3 : qcp3 := by solve dqcp3 -#print dqcp3.reduced -- ... -#eval dqcp3.value -- 0.000000 -#eval dqcp3.solution -- (12.000000, 4.000000) +#print dqcp3.conicForm -- ... +#eval dqcp3.value -- 0.000000 +#eval dqcp3.solution -- (12.000000, 4.000000) end QCP3 @@ -103,9 +103,9 @@ time_cmd reduction redqcp4/dqcp4 : qcp4 := by solve dqcp4 -#print dqcp4.reduced -- ... -#eval dqcp4.value -- -47.500000 -#eval dqcp4.solution -- 47.500000 +#print dqcp4.conicForm -- ... +#eval dqcp4.value -- -47.500000 +#eval dqcp4.solution -- 47.500000 end QCP4 diff --git a/CvxLean/Test/PreDCP/MainExample.lean b/CvxLean/Test/PreDCP/MainExample.lean index 140a1647..02a014a8 100644 --- a/CvxLean/Test/PreDCP/MainExample.lean +++ b/CvxLean/Test/PreDCP/MainExample.lean @@ -30,7 +30,7 @@ time_cmd equivalence eq/q : p := by solve q -#print q.reduced +#print q.conicForm -- optimization (x : ℝ) (t.0 : ℝ) (t.1 : ℝ) -- minimize x -- subject to diff --git a/CvxLean/Test/Solve/Problems/Exp.lean b/CvxLean/Test/Solve/Problems/Exp.lean index 9a747ac8..1f6e4df2 100644 --- a/CvxLean/Test/Solve/Problems/Exp.lean +++ b/CvxLean/Test/Solve/Problems/Exp.lean @@ -12,7 +12,7 @@ noncomputable def exp1 := solve exp1 -#print exp1.reduced +#print exp1.conicForm #eval exp1.status -- "PRIMAL_AND_DUAL_FEASIBLE" #eval exp1.value -- 2.302585 @@ -26,7 +26,7 @@ noncomputable def exp2 := solve exp2 -#print exp2.reduced +#print exp2.conicForm #eval exp2.status -- "PRIMAL_AND_DUAL_FEASIBLE" #eval exp2.value -- 22026.464907 diff --git a/CvxLean/Test/Solve/Problems/Linear.lean b/CvxLean/Test/Solve/Problems/Linear.lean index 681acdeb..7d549602 100644 --- a/CvxLean/Test/Solve/Problems/Linear.lean +++ b/CvxLean/Test/Solve/Problems/Linear.lean @@ -12,7 +12,7 @@ noncomputable def linear1 := solve linear1 -#print linear1.reduced +#print linear1.conicForm #eval linear1.status -- "PRIMAL_AND_DUAL_FEASIBLE" #eval linear1.value -- 11.500000 @@ -41,7 +41,7 @@ lemma linear2Solution : Solution linear2 := solve linear2 -#print linear2.reduced +#print linear2.conicForm #eval linear2.status -- "PRIMAL_AND_DUAL_FEASIBLE" #eval linear2.value -- 400.000000 @@ -56,7 +56,7 @@ noncomputable def linear3 := solve linear3 -#print linear3.reduced +#print linear3.conicForm #eval linear3.status -- "PRIMAL_AND_DUAL_FEASIBLE" #eval linear3.value -- -30.000000 @@ -73,7 +73,7 @@ noncomputable def linear4 := solve linear4 -#print linear4.reduced +#print linear4.conicForm #eval linear4.status -- "PRIMAL_AND_DUAL_FEASIBLE" #eval linear4.value -- 71.500000 @@ -113,7 +113,7 @@ noncomputable def linear5 := set_option trace.Meta.debug true in solve linear5 -#print linear5.reduced +#print linear5.conicForm #eval linear5.status -- "PRIMAL_AND_DUAL_FEASIBLE" #eval linear5.value -- 11.814741 diff --git a/CvxLean/Test/Solve/Problems/Log.lean b/CvxLean/Test/Solve/Problems/Log.lean index 5fa02849..d28c2ba9 100644 --- a/CvxLean/Test/Solve/Problems/Log.lean +++ b/CvxLean/Test/Solve/Problems/Log.lean @@ -5,30 +5,30 @@ section Log open CvxLean Minimization Real noncomputable def log1 := - optimization (x : ℝ) + optimization (x : ℝ) minimize (x) - subject to + subject to h₁ : 10 ≤ log x h₂ : 0 < x solve log1 -#print log1.reduced +#print log1.conicForm #eval log1.status -- "PRIMAL_AND_DUAL_FEASIBLE" #eval log1.value -- 22026.464907 #eval log1.solution -- 22026.464907 noncomputable def log2 := - optimization (x : ℝ) + optimization (x : ℝ) maximize (log x) - subject to + subject to h₁ : x ≤ 10 h₂ : 0 < x solve log2 -#print log2.reduced +#print log2.conicForm #eval log2.status -- "PRIMAL_AND_DUAL_FEASIBLE" #eval log2.value -- 2.302585 diff --git a/CvxLean/Test/Solve/Problems/LogDet.lean b/CvxLean/Test/Solve/Problems/LogDet.lean index 54798e4a..21587af2 100644 --- a/CvxLean/Test/Solve/Problems/LogDet.lean +++ b/CvxLean/Test/Solve/Problems/LogDet.lean @@ -29,7 +29,7 @@ noncomputable def logDet2 := solve logDet2 -#print logDet2.reduced +#print logDet2.conicForm #eval logDet2.status -- "PRIMAL_AND_DUAL_FEASIBLE" #eval logDet2.value -- 6.725434 diff --git a/CvxLean/Test/Solve/Problems/SDP.lean b/CvxLean/Test/Solve/Problems/SDP.lean index 87262646..d3f8f01f 100644 --- a/CvxLean/Test/Solve/Problems/SDP.lean +++ b/CvxLean/Test/Solve/Problems/SDP.lean @@ -28,7 +28,7 @@ noncomputable def sdp1 := solve sdp1 -#print sdp1.reduced +#print sdp1.conicForm #eval sdp1.status -- "PRIMAL_AND_DUAL_FEASIBLE" #eval sdp1.value -- -0.266754 diff --git a/CvxLean/Test/Solve/Problems/SO.lean b/CvxLean/Test/Solve/Problems/SO.lean index 12ce635b..6bc3c79a 100644 --- a/CvxLean/Test/Solve/Problems/SO.lean +++ b/CvxLean/Test/Solve/Problems/SO.lean @@ -14,7 +14,7 @@ noncomputable def so1 := solve so1 -#print so1.reduced +#print so1.conicForm #eval so1.status -- "PRIMAL_AND_DUAL_FEASIBLE" #eval so1.value -- 2.101003 @@ -29,7 +29,7 @@ def so2 := solve so2 -#print so2.reduced +#print so2.conicForm #eval so2.status -- "PRIMAL_AND_DUAL_FEASIBLE" #eval so2.value -- 0.426303 diff --git a/README.md b/README.md index da4750aa..2333a84b 100644 --- a/README.md +++ b/README.md @@ -4,7 +4,7 @@ CvxLean is a convex optimization modeling framework written in [Lean 4](https:// Problems are stated using definitions from [mathlib](https://github.com/leanprover-community/mathlib) and can be rigorously transformed both automatically and interactively. They can be solved by calling the backend solver [MOSEK](https://www.mosek.com/). -Our main contribution is a verified version of the [disciplined convex programming (DCP)](https://web.stanford.edu/~boyd/papers/disc_cvx_prog.html) reduction algorithm. +Our main contribution is a verified version of the [disciplined convex programming (DCP)](https://web.stanford.edu/~boyd/papers/disc_cvx_prog.html) canonization algorithm. ## Installation @@ -56,7 +56,7 @@ solve so1 It will show MOSEK's output and its return code, which should be zero. If successful, it will add several definitions to the environment: -* `so1.reduced`: the reduced version of the problem after applying DCP. +* `so1.conicForm`: the conic form of the problem after applying DCP. * `so1.status`: the feasibility status of the primal and the dual problem, in this case `"PRIMAL_AND_DUAL_FEASIBLE"`, i.e. optimal. * `so1.value`: if the problem is optimal, it corresponds to its optimal value. * `so1.solution`: if the problem is optimal, it corresponds to the optimal point.