doc: documented and styled everything

.github/workflows/docs.yml

@@ -3,9 +3,6 @@ name: docs
 on:
   push:
     branches: ["main"]
-
-  pull_request:
-    branches: ["main"]
 
   workflow_dispatch:
 
@@ -34,10 +31,11 @@ jobs:
         with:
           repository: verified-optimization/CvxLean
           path: CvxLean
-      - name: Build egg-pre-dcp and CvxLean
+      - name: Build egg-pre-dcp, CvxLean, and CvxLeanTest
         working-directory: CvxLean
         run: |
           ./build.sh
+          lake build CvxLeanTest
       - name: Create dummy docs project
         run: |
           # Taken from https://github.com/leanprover-community/mathlib4_docs

.github/workflows/main.yml

@@ -38,6 +38,9 @@ jobs:
       - name: Build egg-pre-dcp and CvxLean
         run: |
           ./build.sh
+      - name: Check style 
+        run: |
+          ./scripts/style/check_style_all.sh
       - name: Test egg-pre-dcp 
         working-directory: egg-pre-dcp
         run: | 

.gitignore

@@ -13,4 +13,4 @@
 /scripts/evaluation/data
 /plots
 
-/CvxLean/Tactic/Solver/Mosek/Path.lean
+/CvxLean/Command/Solve/Mosek/Path.lean

CvxLean/Command/Solve/Conic.lean

@@ -88,7 +88,8 @@ unsafe def solutionDataFromProblemData (minExpr : MinimizationExpr) (data : Prob
     | Except.error err => throwSolveError err
 
 /-- -/
-unsafe def exprFromSolutionData (minExpr : MinimizationExpr) (solData : SolutionData) : MetaM Expr := do
+unsafe def exprFromSolutionData (minExpr : MinimizationExpr) (solData : SolutionData) :
+    MetaM Expr := do
   let vars ← decomposeDomainInstantiating minExpr
 
   -- Generate solution of the correct shape.
@@ -114,7 +115,7 @@ unsafe def exprFromSolutionData (minExpr : MinimizationExpr) (solData : Solution
         let exprs := (solPointExprArrayRaw.drop i).take n
 
         -- TODO: Code repetition.
-        let arrayExpr ← Lean.Expr.mkArray (mkConst ``Real) exprs
+        let arrayExpr ← Expr.mkArray (mkConst ``Real) exprs
         let arrayList ← mkAppM ``Array.toList #[arrayExpr]
         let v ← withLocalDeclD `i' (← mkAppM ``Fin #[toExpr n]) fun i' => do
           let i'' := mkApp2 (mkConst ``Fin.val) (toExpr n) i'
@@ -128,12 +129,12 @@ unsafe def exprFromSolutionData (minExpr : MinimizationExpr) (solData : Solution
         -- Matrix.
         let mut exprs := #[]
         for j in [:m] do
-          let arrayExpr ← Lean.Expr.mkArray (mkConst ``Real) ((solPointExprArrayRaw.drop (i + j * n)).take n)
+          let arrayExpr ← Expr.mkArray (mkConst ``Real)
+            ((solPointExprArrayRaw.drop (i + j * n)).take n)
           let listExpr ← mkAppM ``Array.toList #[arrayExpr]
           exprs := exprs.push listExpr
 
-        let arrayListExpr ←
-          Lean.Expr.mkArray (← mkAppM ``List #[mkConst ``Real]) exprs
+        let arrayListExpr ← Expr.mkArray (← mkAppM ``List #[mkConst ``Real]) exprs
 
         -- List of list representing the matrix.
         let listListExpr ← mkAppM ``Array.toList #[arrayListExpr]

CvxLean/Command/Solve/Float/Coeffs.lean

@@ -163,15 +163,16 @@ unsafe def unrollVectors (constraints : Expr) : MetaM (Array Expr) := do
           let idxExpr ← mkFinIdxExpr i n
           let ei := mkApp e idxExpr
           res := res.push (← mkAppM ``Real.zeroCone #[ei])
-    -- Vector positive orthant cone.
-    | .app (.app (.app (.const ``Real.Vec.posOrthCone _) (.app (.const ``Fin _) n)) _) e =>
+    -- Vector nonnegative orthant cone.
+    | .app (.app (.app (.const ``Real.Vec.nonnegOrthCone _) (.app (.const ``Fin _) n)) _) e =>
         let n : Nat ← evalExpr Nat (mkConst ``Nat) n
         for i in [:n] do
           let idxExpr ← mkFinIdxExpr i n
           let ei := mkApp e idxExpr
-          res := res.push (← mkAppM ``Real.posOrthCone #[ei])
+          res := res.push (← mkAppM ``Real.nonnegOrthCone #[ei])
     -- Vector exponential cone.
-    | .app (.app (.app (.app (.app (.const ``Real.Vec.expCone _) (.app (.const ``Fin _) n)) _) a) b) c =>
+    | .app (.app (.app (.app (.app
+      (.const ``Real.Vec.expCone _) (.app (.const ``Fin _) n)) _) a) b) c =>
         let n : Nat ← evalExpr Nat (mkConst ``Nat) n
         for i in [:n] do
           let idxExpr ← mkFinIdxExpr i n
@@ -277,7 +278,7 @@ unsafe def determineCoeffsFromExpr (minExpr : MinimizationExpr) :
           let res ← determineScalarCoeffsAux e p floatDomain
           data := data.addZeroConstraint res.1 res.2
           idx := idx + 1
-      | .app (.const ``Real.posOrthCone _) e => do
+      | .app (.const ``Real.nonnegOrthCone _) e => do
           let e ← realToFloat e
           let res ← determineScalarCoeffsAux e p floatDomain
           data := data.addPosOrthConstraint res.1 res.2
@@ -312,7 +313,7 @@ unsafe def determineCoeffsFromExpr (minExpr : MinimizationExpr) :
             let (ea, eb) ← determineScalarCoeffsAux e p floatDomain
             data := data.addSOConstraint ea eb
             idx := idx + 1
-      | .app (.app (.app (.app (.app (.const ``Real.Matrix.posOrthCone _)
+      | .app (.app (.app (.app (.app (.const ``Real.Matrix.nonnegOrthCone _)
           (.app (.const ``Fin _) m)) (.app (.const ``Fin _) n)) _) _) e => do
           let m : Nat ← evalExpr Nat (mkConst ``Nat) m
           let n : Nat ← evalExpr Nat (mkConst ``Nat) n

CvxLean/Command/Solve/Float/ProblemData.lean

@@ -11,8 +11,10 @@ The procedure that creates `ProblemData` from an optimization problem can be fou
 
 namespace CvxLean
 
-/-- Cones admitting scalar affine constraints. Note that the only cone that admits matrix affine
-constraints is the PSD cone. -/
+/-- Cones admitting scalar affine constraints. The `PosOrth` type actually corresponds to the
+nonnegative orthant, but at the solver level, it is usually called the positive orthant, so we use
+that terminology here. Note that the only cone that admits matrix affine constraints is the PSD
+cone. -/
 inductive ScalarConeType
   | Zero | PosOrth | Exp | Q | QR
 

CvxLean/Command/Solve/Float/RealToFloatCmd.lean

@@ -76,12 +76,12 @@ partial def realToFloat (e : Expr) : MetaM Expr := do
 environment extension. -/
 @[command_elab addRealToFloatCommand]
 def elabAddRealToFloatCommand : CommandElab
-| `(add_real_to_float : $real := $float) =>
-  liftTermElabM do
-    let real ← elabTermAndSynthesize real.raw none
-    let float ← elabTermAndSynthesize float.raw none
-    addRealToFloatData { real := real, float := float }
-| _ => throwUnsupportedSyntax
+  | `(add_real_to_float : $real := $float) =>
+      liftTermElabM do
+        let real ← elabTermAndSynthesize real.raw none
+        let float ← elabTermAndSynthesize float.raw none
+        addRealToFloatData { real := real, float := float }
+  | _ => throwUnsupportedSyntax
 
 macro_rules
 | `(add_real_to_float $idents:funBinder* : $real := $float) => do

CvxLean/Command/Solve/Mosek/CBF.lean

@@ -567,9 +567,8 @@ def addScalarConstraintsShiftCoord (p : Problem) (i : Nat) (v : Float) : Problem
   { p with scalarConstraintsShiftCoord :=
       p.scalarConstraintsShiftCoord.stack ev}
 
-def addPSDConstraintsScalarVariablesCoord
-  (p : Problem) (i : Nat) (eml : EncodedMatrixList)
-  : Problem :=
+def addPSDConstraintsScalarVariablesCoord (p : Problem) (i : Nat) (eml : EncodedMatrixList) :
+    Problem :=
   let emll := EncodedMatrixListList.fromIndexAndEncodedMatrixList i eml
   { p with PSDConstraintsScalarVariablesCoord :=
       p.PSDConstraintsScalarVariablesCoord.stack emll }

CvxLean/Command/Solve/Mosek/Path.lean

@@ -1,3 +1,4 @@
--- Change this to the location of the Mosek binary, e.g.
--- /Users/alice/mosek/10.0/tools/platform/osxaarch64/bin
-def mosekBinPath := "/Users/ramonfernandezmir/Documents/PhD-code/optimization/mosek/10.0/tools/platform/osxaarch64/bin"
+/-! Change this to the location of the Mosek binary, e.g.
+`/Users/alice/mosek/10.0/tools/platform/osxaarch64/bin` -/
+
+def mosekBinPath := ""

CvxLean/Command/Solve/Mosek/Sol.lean

@@ -133,7 +133,8 @@ instance : ToString Result where
     "INDEX | NAME | AT | ACTIVITY | LOWER LIMIT | UPPER LIMIT | DUAL LOWER | DUAL UPPER \n" ++
     (res.constraints.foldl (fun acc s => acc ++ (toString s) ++ "\n") "") ++ "\n" ++
     "VARIABLES \n" ++
-    "INDEX | NAME | AT | ACTIVITY | LOWER LIMIT | UPPER LIMIT | DUAL LOWER | DUAL UPPER | CONIC DUAL \n" ++
+    "INDEX | NAME | AT | ACTIVITY | LOWER LIMIT | UPPER LIMIT | DUAL LOWER | DUAL UPPER | " ++
+    "CONIC DUAL \n" ++
     (res.vars.foldl (fun acc s => acc ++ (toString s) ++ "\n") "") ++ "\n" ++
     "SYMMETRIC MATRIX VARIABLES \n" ++
     "INDEX | NAME | I | J | PRIMAL | DUAL \n" ++

CvxLean/Command/Util/TimeCmd.lean

@@ -1,15 +1,20 @@
 import Lean
 
+/-!
+Place `time_cmd` before any command to print the time taken by the command. Useful for simple
+profiling.
+-/
+
 open Lean Elab Command
 
 syntax (name := time_cmd) "time_cmd " command : command
 
 @[command_elab «time_cmd»]
 def evalTimeCmd : CommandElab := fun stx => match stx with
   | `(time_cmd $cmd) => do
-    let before ← BaseIO.toIO IO.monoMsNow
-    elabCommand cmd
-    let after ← BaseIO.toIO IO.monoMsNow
-    let diff := after - before
-    dbg_trace s!"Command time: {diff} ms"
+      let before ← BaseIO.toIO IO.monoMsNow
+      elabCommand cmd
+      let after ← BaseIO.toIO IO.monoMsNow
+      let diff := after - before
+      dbg_trace s!"Command time: {diff} ms"
   | _ => throwUnsupportedSyntax

CvxLean/Demos/LT2024.lean

@@ -1,5 +1,10 @@
 import CvxLean
 
+/-!
+This demo was used for Lean Together 2024, see the video here:
+<https://www.youtube.com/watch?v=GNOXmt5A_MQ>
+-/
+
 namespace LT2024
 
 noncomputable section
@@ -70,9 +75,6 @@ def p₃ (Awall Aflr α β γ δ : ℝ) :=
       c8 : γ ≤ d / w
       c9 : d / w ≤ δ
 
-
-set_option trace.Meta.debug true
-
 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')

CvxLean/Examples/CovarianceEstimation.lean

@@ -91,16 +91,16 @@ solve covEstimationConvex nₚ Nₚ αₚ yₚ
 --     -(-(Nₚ • log (sqrt ((2 * π) ^ nₚ)) + Nₚ • (-Vec.sum t.0 / 2)) +
 --         -(↑Nₚ * trace ((covarianceMatrix fun i => yₚ i) * Rᵀ) / 2))
 --   subject to
---     _ : Real.posOrthCone (αₚ - sum T.2)
+--     _ : Real.nonnegOrthCone (αₚ - sum T.2)
 --     _ : Vec.expCone t.0 1 (diag Y.1)
 --     _ :
 --       PSDCone
 --         (let Z := toUpperTri Y.1;
 --         let D := diagonal (diag Y.1);
 --         let X := fromBlocks D Z Zᵀ R;
 --         X)
---     _ : Matrix.posOrthCone (T.2 - R)
---     _ : Matrix.posOrthCone (T.2 + R)
+--     _ : Matrix.nonnegOrthCone (T.2 - R)
+--     _ : Matrix.nonnegOrthCone (T.2 + R)
 
 #eval covEstimationConvex.status   -- "PRIMAL_AND_DUAL_FEASIBLE"
 #eval covEstimationConvex.value    -- 14.124098

CvxLean/Examples/FittingSphere.lean

@@ -23,7 +23,7 @@ def mean {n : ℕ} (a : Fin n → ℝ) : ℝ := (1 / n) * ∑ i, (a i)
 `leastSquares_optimal_eq_mean`, following Marty Cohen's answer in
 https://math.stackexchange.com/questions/2554243. -/
 lemma leastSquares_alt_objFun {n : ℕ} (hn : 0 < n) (a : Fin n → ℝ) (x : ℝ) :
-  (∑ i, ((a i - x) ^ 2)) = n * ((x - mean a) ^ 2 + (mean (a ^ 2) - (mean a) ^ 2)) := by
+    (∑ i, ((a i - x) ^ 2)) = n * ((x - mean a) ^ 2 + (mean (a ^ 2) - (mean a) ^ 2)) := by
   calc
   -- 1) Σ (aᵢ - x)² = Σ (aᵢ² - 2aᵢx + x²)
   _ = ∑ i, ((a i) ^ 2 - 2 * (a i) * x + (x ^ 2)) := by
@@ -40,7 +40,7 @@ lemma leastSquares_alt_objFun {n : ℕ} (hn : 0 < n) (a : Fin n → ℝ) (x : 
 
 /-- Key result about least squares: `x* = mean a`. -/
 lemma leastSquares_optimal_eq_mean {n : ℕ} (hn : 0 < n) (a : Fin n → ℝ) (x : ℝ)
-  (h : (leastSquares a).optimal x) : x = mean a := by
+    (h : (leastSquares a).optimal x) : x = mean a := by
   simp [optimal, feasible, leastSquares] at h
   replace h : ∀ y, (x - mean a) ^ 2 ≤ (y - mean a) ^ 2  := by
     intros y
@@ -60,7 +60,7 @@ def leastSquaresVec {n : ℕ} (a : Fin n → ℝ) :=
 
 /-- Same as `leastSquares_optimal_eq_mean` in vector notation. -/
 lemma leastSquaresVec_optimal_eq_mean {n : ℕ} (hn : 0 < n) (a : Fin n → ℝ) (x : ℝ)
-  (h : (leastSquaresVec a).optimal x) : x = mean a := by
+    (h : (leastSquaresVec a).optimal x) : x = mean a := by
   apply leastSquares_optimal_eq_mean hn a
   simp [leastSquaresVec, leastSquares, optimal, feasible] at h ⊢
   intros y
@@ -96,7 +96,7 @@ equivalence* eqv/fittingSphereT (n m : ℕ) (x : Fin m → Fin n → ℝ) : fitt
   equivalence_step =>
     apply ChangeOfVariables.toEquivalence
       (fun (ct : (Fin n → ℝ) × ℝ) => (ct.1, sqrt (ct.2 + ‖ct.1‖ ^ 2)))
-    . rintro _ h; exact le_of_lt h
+    · rintro _ h; exact le_of_lt h
   rename_vars [c, t]
   -- Clean up.
   conv_constr h₁ => dsimp
@@ -128,21 +128,21 @@ lemma vec_squared_norm_error_eq_zero_iff {n m : ℕ} (a : Fin m → Fin n → 
   simp [rpow_two]
   rw [sum_eq_zero_iff_of_nonneg (fun _ _ => sq_nonneg _)]
   constructor
-  . intros h i
+  · intros h i
     have hi := h i (by simp)
     rwa [sq_eq_zero_iff, norm_eq_zero, sub_eq_zero] at hi
-  . intros h i _
+  · intros h i _
     rw [sq_eq_zero_iff, norm_eq_zero, sub_eq_zero]
     exact h i
 
 /-- This tells us that solving the relaxed problem is sufficient for optimal points if the solution
 is non-trivial. -/
 lemma optimal_convex_implies_optimal_t (hm : 0 < m) (c : Fin n → ℝ) (t : ℝ)
-  (h_nontrivial : x ≠ Vec.const m c)
-  (h_opt : (fittingSphereConvex n m x).optimal (c, t)) : (fittingSphereT n m x).optimal (c, t) := by
+    (h_nontrivial : x ≠ Vec.const m c) (h_opt : (fittingSphereConvex n m x).optimal (c, t)) :
+    (fittingSphereT n m x).optimal (c, t) := by
   simp [fittingSphereT, fittingSphereConvex, optimal, feasible] at h_opt ⊢
   constructor
-  . let a := Vec.norm x ^ 2 - 2 * mulVec x c
+  · let a := Vec.norm x ^ 2 - 2 * mulVec x c
     have h_ls : optimal (leastSquaresVec a) t := by
       refine ⟨trivial, ?_⟩
       intros y _
@@ -177,12 +177,12 @@ lemma optimal_convex_implies_optimal_t (hm : 0 < m) (c : Fin n → ℝ) (t : ℝ
         exfalso
         rw [h_t_add_c2_eq, zero_eq_mul] at h_t_add_c2_eq_zero
         rcases h_t_add_c2_eq_zero with (hc | h_sum_eq_zero)
-        . simp at hc; linarith
+        · simp at hc; linarith
         rw [vec_squared_norm_error_eq_zero_iff] at h_sum_eq_zero
         apply h_nontrivial
         funext i
         exact h_sum_eq_zero i
-  . intros c' x' _
+  · intros c' x' _
     exact h_opt c' x'
 
 /-- We express the nontriviality condition only in terms of `x` so that it can be checked. -/

CvxLean/Examples/TrussDesign.lean

@@ -63,7 +63,7 @@ equivalence* eqv₁/trussDesignGP (hmin hmax wmin wmax Rmax σ F₁ F₂ : ℝ)
     apply ChangeOfVariables.toEquivalence
       (fun (hwrA : ℝ × ℝ × ℝ × ℝ) =>
         (hwrA.1, hwrA.2.1, hwrA.2.2.1, sqrt (hwrA.2.2.2 / (2 * π) + hwrA.2.2.1 ^ 2)))
-    . rintro ⟨h, w, r, R⟩ ⟨c_r, _, _, _, _, _, _, c_R_lb, _⟩; dsimp at *
+    · rintro ⟨h, w, r, R⟩ ⟨c_r, _, _, _, _, _, _, c_R_lb, _⟩; dsimp at *
       simp [ChangeOfVariables.condition]
       have h_r_le : r ≤ 1.1 * r := (le_mul_iff_one_le_left c_r).mpr (by norm_num)
       exact le_trans (le_of_lt c_r) (le_trans h_r_le c_R_lb)
@@ -122,12 +122,12 @@ equivalence* eqv₂/trussDesignConvex (hmin hmax : ℝ) (hmin_pos : 0 < hmin)
     apply ChangeOfVariables.toEquivalence
       (fun (hwrA : ℝ × ℝ × ℝ × ℝ) =>
         (exp hwrA.1, exp hwrA.2.1, exp hwrA.2.2.1, exp hwrA.2.2.2))
-    . rintro ⟨h, w, r, A⟩ ⟨c_r, _, _, c_hmin, _, c_wmin, _, c_A_lb, _⟩; dsimp at *
+    · rintro ⟨h, w, r, A⟩ ⟨c_r, _, _, c_hmin, _, c_wmin, _, c_A_lb, _⟩; dsimp at *
       split_ands
-      . exact lt_of_lt_of_le hmin_pos c_hmin
-      . exact lt_of_lt_of_le wmin_pos c_wmin
-      . exact c_r
-      . have h_A_div_2π_pos : 0 < A / (2 * π) := lt_of_lt_of_le (by positivity) c_A_lb
+      · exact lt_of_lt_of_le hmin_pos c_hmin
+      · exact lt_of_lt_of_le wmin_pos c_wmin
+      · exact c_r
+      · have h_A_div_2π_pos : 0 < A / (2 * π) := lt_of_lt_of_le (by positivity) c_A_lb
         rwa [lt_div_iff (by positivity), zero_mul] at h_A_div_2π_pos
   conv_opt => dsimp
   rename_vars [h', w', r', A']