doc: more tactics docs and some general refactoring

CvxLean/Command/Equivalence.lean

@@ -23,7 +23,7 @@ environment:
 * `q := r`,
 * `eqv : p ≡ q`.
 
-Writing `equivalence'` instead of `equivalence` will also generate a backward solution map at the
+Writing `equivalence*` instead of `equivalence` will also generate a backward solution map at the
 level of floats.
 -/
 
@@ -46,7 +46,7 @@ syntax (name := equivalence)
 
 /-- Open an equivalence environment and try to generate a computable backward map. -/
 syntax (name := equivalenceAndBwdMap)
-  "equivalence'" ident "/" ident declSig ":=" Lean.Parser.Term.byTactic : command
+  "equivalence*" ident "/" ident declSig ":=" Lean.Parser.Term.byTactic : command
 
 /-- Open an equivalence environment with a given left-hand-side problem (`lhsStx`) and perhaps some
 parameters (`xs`). From this, an equivalence goal is set to a target problem which is represented by
@@ -139,7 +139,7 @@ def evalEquivalence : CommandElab := fun stx => match stx with
 /-- Same as `equivalence` but also adds the backward map to the environment. -/
 @[command_elab «equivalenceAndBwdMap»]
 def evalEquivalenceAndBwdMap : CommandElab := fun stx => match stx with
-  | `(equivalence' $eqvId / $probId $declSig := $proofStx) => do
+  | `(equivalence* $eqvId / $probId $declSig := $proofStx) => do
       liftTermElabM do
         let (binders, lhsStx) := expandDeclSig declSig.raw
         elabBindersEx binders.getArgs fun xs =>

CvxLean/Command/Reduction.lean

@@ -24,7 +24,7 @@ environment:
 * `q := r`,
 * `red : p ≼ q`.
 
-Writing `reduction'` instead of `reduction` will also generate a backward solution map at the
+Writing `reduction*` instead of `reduction` will also generate a backward solution map at the
 level of floats.
 
 It is essentially the same as `CvxLean/Command/Equivalence.lean`, except that the goal is to prove a
@@ -51,7 +51,7 @@ syntax (name := reduction)
 
 /-- Open a reduction environment and try to generate a computable backward map. -/
 syntax (name := reductionAndBwdMap)
-  "reduction'" ident "/" ident declSig ":=" Lean.Parser.Term.byTactic : command
+  "reduction*" ident "/" ident declSig ":=" Lean.Parser.Term.byTactic : command
 
 /-- Open a reduction environment with a given left-hand-side problem (`lhsStx`) and perhaps some
 parameters (`xs`). From this, a reduction goal is set to a target problem which is represented by a
@@ -150,7 +150,7 @@ def evalReduction : CommandElab := fun stx => match stx with
 /-- Same as `reduction` but also adds the backward map to the environment. -/
 @[command_elab «reductionAndBwdMap»]
 def evalReductionAndBwdMap : CommandElab := fun stx => match stx with
-  | `(reduction' $eqvId / $probId $declSig := $proofStx) => do
+  | `(reduction* $eqvId / $probId $declSig := $proofStx) => do
       liftTermElabM do
         let (binders, lhsStx) := expandDeclSig declSig.raw
         elabBindersEx binders.getArgs fun xs =>

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
@@ -73,15 +73,15 @@ def p₃ (Awall Aflr α β γ δ : ℝ) :=
 
 set_option trace.Meta.debug true
 
-equivalence' eqv₃/q₃ : p₃ 100 10 0.5 2 0.5 2 := by
+equivalence* eqv₃/q₃ : p₃ 100 10 0.5 2 0.5 2 := by
   change_of_variables! (h') (h ↦ exp h')
   change_of_variables! (w') (w ↦ exp w')
   change_of_variables! (d') (d ↦ exp d')
   pre_dcp
 
 solve q₃
 
-#print q₃.reduced
+#print q₃.conicForm
 
 #eval q₃.status
 #eval q₃.solution

CvxLean/Examples/CovarianceEstimation.lean

@@ -17,7 +17,7 @@ noncomputable def covEstimation (n : ℕ) (N : ℕ) (α : ℝ) (y : Fin N → Fi
       c_pos_def : R.PosDef
       c_sparse : R⁻¹.abs.sum ≤ α
 
-reduction' red/covEstimationConvex (n : ℕ) (N : ℕ) (α : ℝ) (y : Fin N → Fin n → ℝ) :
+reduction* red/covEstimationConvex (n : ℕ) (N : ℕ) (α : ℝ) (y : Fin N → Fin n → ℝ) :
   covEstimation n N α y := by
   -- Change objective function.
   reduction_step =>
@@ -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/FittingSphere.lean

@@ -91,7 +91,7 @@ instance : ChangeOfVariables fun ((c, t) : (Fin n → ℝ) × ℝ) => (c, sqrt (
     condition := fun (_, r) => 0 ≤ r,
     property := fun ⟨c, r⟩ h => by simp [sqrt_sq h] }
 
-equivalence' eqv/fittingSphereT (n m : ℕ) (x : Fin m → Fin n → ℝ) : fittingSphere n m x := by
+equivalence* eqv/fittingSphereT (n m : ℕ) (x : Fin m → Fin n → ℝ) : fittingSphere n m x := by
   -- Change of variables.
   equivalence_step =>
     apply ChangeOfVariables.toEquivalence
@@ -106,7 +106,7 @@ equivalence' eqv/fittingSphereT (n m : ℕ) (x : Fin m → Fin n → ℝ) : fitt
     dsimp at h₁ ⊢; simp [Vec.sum, Vec.norm, Vec.const]; congr; funext i; congr 1;
     rw [norm_sub_sq (𝕜 := ℝ) (E := Fin n → ℝ), sq_sqrt (rpow_two _ ▸ le_of_lt (sqrt_pos.mp h₁))]
     simp [mulVec, inner, dotProduct]
-  
+
 #print fittingSphereT
 -- optimization (c : Fin n → ℝ) (t : ℝ)
 --   minimize Vec.sum ((Vec.norm x ^ 2 - 2 * mulVec x c - Vec.const m t) ^ 2)

CvxLean/Examples/HypersonicShapeDesign.lean

@@ -27,7 +27,7 @@ def hypersonicShapeDesign :=
       h₂ : Δx ≤ 1
       h₃ : a * (1 / Δx) - (1 - b) * sqrt (1 - Δx ^ 2) ≤ 0
 
-equivalence' eqv₁/hypersonicShapeDesignConvex (a b : ℝ) (ha : 0 ≤ a) (hb₁ : 0 ≤ b) (hb₂ : b < 1) :
+equivalence* eqv₁/hypersonicShapeDesignConvex (a b : ℝ) (ha : 0 ≤ a) (hb₁ : 0 ≤ b) (hb₂ : b < 1) :
     hypersonicShapeDesign a b := by
   pre_dcp
 
@@ -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
@@ -84,7 +84,7 @@ def ldRatioₚ := 1 / (Float.sqrt ((1 / wₚ_opt ^ 2) - 1))
 -- While the above is good enough, we simplify the problem further by performing a change of
 -- variables and simplifying appropriately.
 
-equivalence' eqv₂/hypersonicShapeDesignSimpler (a b : ℝ) (ha : 0 ≤ a) (hb₁ : 0 ≤ b)
+equivalence* eqv₂/hypersonicShapeDesignSimpler (a b : ℝ) (ha : 0 ≤ a) (hb₁ : 0 ≤ b)
     (hb₂ : b < 1) : hypersonicShapeDesignConvex a b ha hb₁ hb₂ := by
   change_of_variables (z) (Δx ↦ sqrt z)
   conv_constr h₁ =>
@@ -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/TrussDesign.lean

@@ -56,7 +56,7 @@ instance : ChangeOfVariables
       simp; rw [mul_comm _ (R ^ 2 - r ^ 2), ← mul_div, div_self (by positivity), mul_one]
       ring_nf; exact sqrt_sq hR }
 
-equivalence' eqv₁/trussDesignGP (hmin hmax wmin wmax Rmax σ F₁ F₂ : ℝ) :
+equivalence* eqv₁/trussDesignGP (hmin hmax wmin wmax Rmax σ F₁ F₂ : ℝ) :
     trussDesign hmin hmax wmin wmax Rmax σ F₁ F₂ := by
   -- Apply key change of variables.
   equivalence_step =>
@@ -114,7 +114,7 @@ instance : ChangeOfVariables
     property := fun (h', w', r', A') ⟨hh', hw', hr', hA'⟩ => by
       simp [exp_log hh', exp_log hw', exp_log hr', exp_log hA'] }
 
-equivalence' eqv₂/trussDesignConvex (hmin hmax : ℝ) (hmin_pos : 0 < hmin)
+equivalence* eqv₂/trussDesignConvex (hmin hmax : ℝ) (hmin_pos : 0 < hmin)
     (hmin_le_hmax : hmin ≤ hmax) (wmin wmax : ℝ) (wmin_pos : 0 < wmin) (wmin_le_wmax : wmin ≤ wmax)
     (Rmax σ F₁ F₂ : ℝ) : trussDesignGP hmin hmax wmin wmax Rmax σ F₁ F₂ := by
   -- Change variables.

CvxLean/Examples/VehicleSpeedScheduling.lean

@@ -52,11 +52,11 @@ private lemma fold_partial_sum [hn : Fact (0 < n)] (t : Fin n → ℝ) (i : Fin
   . rfl
   . linarith [hn.out]
 
-equivalence' eqv₁/vehSpeedSchedConvex (n : ℕ) (d : Fin n → ℝ)
+equivalence* eqv₁/vehSpeedSchedConvex (n : ℕ) (d : Fin n → ℝ)
     (τmin τmax smin smax : Fin n → ℝ) (F : ℝ → ℝ) (h_n_pos : 0 < n) (h_d_pos : StrongLT 0 d)
     (h_smin_pos : StrongLT 0 smin) : @vehSpeedSched n d τmin τmax smin smax F ⟨h_n_pos⟩ := by
-  replace h_d_pos : ∀ i, 0 < d i := fun i => h_d_pos i
-  replace h_smin_pos : ∀ i, 0 < smin i := fun i => h_smin_pos i
+  replace h_d_pos : ∀ i, 0 < d i := h_d_pos
+  replace h_smin_pos : ∀ i, 0 < smin i := h_smin_pos
   haveI : Fact (0 < n) := ⟨h_n_pos⟩
   -- Change variables `s ↦ d / t`.
   -- TODO: This can be done by change of variables by detecting that the variable is a vector.
@@ -93,12 +93,12 @@ 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 → ℝ)
+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)
     (h_smin_pos : StrongLT 0 smin) :
     vehSpeedSchedConvex n d τmin τmax smin smax (fun s => a • s ^ (2 : ℝ) + b • s + c)
@@ -165,7 +165,7 @@ def τminₚ : Fin nₚ → ℝ :=
 def τmaxₚ : Fin nₚ → ℝ :=
   ![4.6528, 6.5147, 7.5178, 9.7478, 9.0641, 10.3891, 13.1540, 16.0878, 17.4352, 20.9539]
 
-@[optimization_param]
+@[optimization_param, reducible]
 def sminₚ : Fin nₚ → ℝ :=
   ![0.7828, 0.6235, 0.7155, 0.5340, 0.6329, 0.4259, 0.7798, 0.9604, 0.7298, 0.8405]
 
@@ -174,7 +174,7 @@ def smaxₚ : Fin nₚ → ℝ :=
   ![1.9624, 1.6036, 1.6439, 1.5641, 1.7194, 1.9090, 1.3193, 1.3366, 1.9470, 2.8803]
 
 lemma sminₚ_pos : StrongLT 0 sminₚ := by
-  intro i; fin_cases i <;> (simp [sminₚ]; norm_num)
+  intro i; fin_cases i <;> norm_num
 
 @[simp]
 lemma sminₚ_nonneg : 0 ≤ sminₚ := le_of_strongLT sminₚ_pos

CvxLean/Meta/Equivalence.lean

@@ -64,6 +64,9 @@ open Parser Elab Tactic
 elab "equivalence_step" _arr:darrow tac:tacticSeqIndentGt : tactic => do
   evalTactic <| ← `(tactic| equivalence_trans)
   evalTacticSeq1Indented tac.raw
+  if (← getGoals).length > 1 then
+    evalTactic <| ← `(tactic| try { equivalence_rfl })
+  (← getMainGoal).setTag Name.anonymous
 
 end BasicTactics
 

CvxLean/Meta/Reduction.lean

@@ -59,6 +59,9 @@ open Parser Elab Tactic
 elab "reduction_step" _arr:darrow tac:tacticSeqIndentGt : tactic => do
   evalTactic <| ← `(tactic| reduction_trans)
   evalTacticSeq1Indented tac.raw
+  if (← getGoals).length > 1 then
+    evalTactic <| ← `(tactic| try { reduction_rfl })
+  (← getMainGoal).setTag Name.anonymous
 
 end Meta
 

CvxLean/Meta/Relaxation.lean

@@ -59,6 +59,9 @@ open Parser Elab Tactic
 elab "relaxation_step" _arr:darrow tac:tacticSeqIndentGt : tactic => do
   evalTactic <| ← `(tactic| relaxation_trans)
   evalTacticSeq1Indented tac.raw
+  if (← getGoals).length > 1 then
+    evalTactic <| ← `(tactic| try { relaxation_rfl })
+  (← getMainGoal).setTag Name.anonymous
 
 end Meta