refactor: DCP canonization not reduction

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
 

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

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))

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 :=

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)

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,37 +219,37 @@ 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}"
 
             let newOptimality ←
               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