feat: improve pre_dcp, and some docs and clean-up

.gitignore

@@ -10,7 +10,7 @@
 *.code-workspace
 
 /playground
-/evaluation
+/scripts/evaluation/data
 /plots
 
 /CvxLean/Tactic/Solver/Mosek/Path.lean

CvxLean/Command/Equivalence.lean

@@ -40,9 +40,11 @@ type `Equivalence p q`. -/
 def elabEquivalenceProof (lhs : Expr) (rhsName : Name) (stx : Syntax) : TermElabM (Expr × Expr) :=
   elabTransformationProof TransformationGoal.Equivalence lhs rhsName stx
 
+/-- Open an equivalence environment. -/
 syntax (name := equivalence)
   "equivalence" ident "/" ident declSig ":=" Lean.Parser.Term.byTactic : command
 
+/-- Open an equivalence environment and try to generate a computable backward map. -/
 syntax (name := equivalenceAndBwdMap)
   "equivalence'" ident "/" ident declSig ":=" Lean.Parser.Term.byTactic : command
 

CvxLean/Command/Reduction.lean

@@ -27,7 +27,7 @@ environment:
 Writing `reduction'` instead of `reduction` will also generate a backward solution map at the
 level of floats.
 
-It is essentially the same as `Command/Equivalence.lean`, except that the goal is to prove a
+It is essentially the same as `CvxLean/Command/Equivalence.lean`, except that the goal is to prove a
 reduction instead of an equivalence. We note that proving that two problems are equivalent is
 usually preferred.
 -/
@@ -45,9 +45,11 @@ type `Reduction p q`. -/
 def elabReductionProof (lhs : Expr) (rhsName : Name) (stx : Syntax) : TermElabM (Expr × Expr) :=
   elabTransformationProof TransformationGoal.Reduction lhs rhsName stx
 
+/-- Open a reduction environment. -/
 syntax (name := reduction)
   "reduction" ident "/" ident declSig ":=" Lean.Parser.Term.byTactic : command
 
+/-- Open a reduction environment and try to generate a computable backward map. -/
 syntax (name := reductionAndBwdMap)
   "reduction'" ident "/" ident declSig ":=" Lean.Parser.Term.byTactic : command
 

CvxLean/Command/Relaxation.lean

@@ -20,10 +20,10 @@ environment:
 * `q := r`,
 * `rel : p ≽' q`.
 
-This command is very similar to `equivalence` (`Command/Equivalence.lean`) and `reduction`
-(`Command/Reduction.lean`) in how it is designed. Of course, the key difference is that the goal
-is to prove a relaxation. Note that in this case, there is no option to create a backward map as
-relaxations do not guarantee that the solution can be mapped back.
+This command is very similar to `equivalence` (`CvxLean/Command/Equivalence.lean`) and `reduction`
+(`CvxLean/Command/Reduction.lean`) in how it is designed. Of course, the key difference is that the
+goal is to prove a relaxation. Note that in this case, there is no option to create a backward map
+as relaxations do not guarantee that the solution can be mapped back.
 -/
 
 namespace CvxLean
@@ -39,10 +39,11 @@ type `Relaxation p q`. -/
 def elabRelaxationProof (lhs : Expr) (rhsName : Name) (stx : Syntax) : TermElabM (Expr × Expr) :=
   elabTransformationProof TransformationGoal.Relaxation lhs rhsName stx
 
+/-- Open a relaxation environment. -/
 syntax (name := relaxation)
   "relaxation" ident "/" ident declSig ":=" Lean.Parser.Term.byTactic : command
 
-/-- Relaxation command. -/
+/-- Definition of the `relaxation` command. -/
 @[command_elab «relaxation»]
 def evalRelaxation : CommandElab := fun stx => match stx with
 | `(relaxation $relIdStx / $probIdStx $declSig := $proofStx) => do

CvxLean/Command/Solve.lean

@@ -27,7 +27,8 @@ def getProblemName (stx : Syntax) : MetaM Name := do
   if ¬ idStx.getId.isStr then
     throwError "Invalid name for minimization problem: {idStx}."
 
-  return idStx.getId
+  let currNamespace ← getCurrNamespace
+  return currNamespace ++ idStx.getId
 
 /-- Call DCP and get the problem in conic form as well as `ψ`, the backward map from the
 equivalence. -/

CvxLean/Command/Solve/Float/Coeffs.lean

@@ -10,10 +10,10 @@ import CvxLean.Command.Solve.Float.RealToFloatLibrary
 # Extract coefficients from problem to generate problem data
 
 This file defines `determineCoeffsFromExpr`, which takes a `MinimizationExpr` and returns
-`ProblemData`. This procedure is used by `Commands/Solve.lean` to be able to call an external
-solver.
+`ProblemData`. This procedure is used by `CvxLean/Commands/Solve.lean` to be able to call an
+external solver.
 
-## TODO
+### TODO
 
 * This is probably a big source of inefficency for the `solve` command. We should come up with a
   better way to extract the numerical values from the Lean expressions.

CvxLean/Command/Solve/Float/FloatToReal.lean

@@ -2,8 +2,8 @@ import Mathlib.Data.Real.Basic
 import CvxLean.Lib.Math.Data.Real
 
 /-!
-Conversion used in `Solve/Conic.lean` to read the solver's output into an expression to which we can
-apply the backward map.
+Conversion used in `CvxLean/Command/Solve/Conic.lean` to read the solver's output into an expression
+to which we can apply the backward map.
 -/
 
 namespace CvxLean

CvxLean/Command/Solve/Float/ProblemData.lean

@@ -6,7 +6,7 @@ We provide an interface to build this data by adding any of the possible types o
 data can then be transformed in a straightforward manner into Conic Benchmark Format, for example.
 
 The procedure that creates `ProblemData` from an optimization problem can be found in
-`Command/Solve/Coeffs.lean`.
+`CvxLean/Command/Solve/Coeffs.lean`.
 -/
 
 namespace CvxLean
@@ -115,7 +115,7 @@ def addZeroConstraint (data : ProblemData) (a : Array Float) (b : Float) : Probl
 /-- Add exponential cone constraint `∑ i, aᵢxᵢ + b ∈ 𝒦ₑ` to problem data. Note that the
 second-order cone is `3`-dimensional, so to capture `(x, y, z) ∈ 𝒦ₑ` we do `x ∈ 𝒦ₑ`, `y ∈ 𝒦ₑ`, and
 `z ∈ 𝒦ₑ` consecutively. We keep track of how to group consecutive constraints in
-`Command/Solve/Float/Coeffs.lean`. -/
+`CvxLean/Command/Solve/Float/Coeffs.lean`. -/
 def addExpConstraint (data : ProblemData) (a : Array Float) (b : Float) : ProblemData :=
   data.addScalarAffineConstraintOnlyVector a b ScalarConeType.Exp
 

CvxLean/Command/Solve/Float/RealToFloatCmd.lean

@@ -14,7 +14,7 @@ import CvxLean.Command.Solve.Float.RealToFloatExt
 # Conversion of Real to Float (command)
 
 We define the `realToFloat` function to go from real `Expr`s to float `Expr`s as well as the
-`addRealToFloat` command to add new translations and the `#realToFloat` command to test the
+`add_real_to_float` command to add new translations and the `#real_to_float` command to test the
 translation.
 -/
 
@@ -23,7 +23,7 @@ namespace CvxLean
 open Lean Expr Elab Meta Command Term
 
 syntax (name := addRealToFloatCommand)
-  "addRealToFloat" Lean.Parser.Term.funBinder* ":" term ":=" term : command
+  "add_real_to_float" Lean.Parser.Term.funBinder* ":" term ":=" term : command
 
 /-- Traverse expression recursively and if a match is found in the real-to-float library return the
 float version. The "correctness" of this function depends on the translations defined in the
@@ -72,31 +72,31 @@ partial def realToFloat (e : Expr) : MetaM Expr := do
         return e
   | _ => return e
 
-/-- The `addRealToFloat` command, which simply adds the user-defined expressions to the environment
-extension. -/
+/-- The `add_real_to_float` command, which simply adds the user-defined expressions to the
+environment extension. -/
 @[command_elab addRealToFloatCommand]
 def elabAddRealToFloatCommand : CommandElab
-| `(addRealToFloat : $real := $float) =>
+| `(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
-| `(addRealToFloat $idents:funBinder* : $real := $float) => do
+| `(add_real_to_float $idents:funBinder* : $real := $float) => do
   if idents.size != 0 then
-    `(addRealToFloat : fun $idents:funBinder* => $real := fun $idents:funBinder* => $float)
+    `(add_real_to_float : fun $idents:funBinder* => $real := fun $idents:funBinder* => $float)
   else
     Macro.throwUnsupported
 
 syntax (name:=realToFloatCommand)
-  "#realToFloat" term : command
+  "#real_to_float" term : command
 
 /-- Transform the given expression to its float version and log the result. -/
 @[command_elab realToFloatCommand]
 unsafe def elabRealToFloatCommand : CommandElab
-| `(#realToFloat $stx) =>
+| `(#real_to_float $stx) =>
   liftTermElabM do
     let e ← elabTermAndSynthesize stx.raw none
     let res ← realToFloat e