fix: logic in non-trivial atoms

Omit original variables in atom reduction

CvxLean/Tactic/DCP/AtomLibrary/Fns/Huber.lean

@@ -109,14 +109,12 @@ optimality by
     intros i
     simp [Vec.huber]
     rw [←rpow_two]
-    apply huber.optimality (x i) (v i) (w i) ((w i) ^ 2) (|x i|)
+    apply huber.optimality (x i) (v i) (w i) ((w i) ^ 2)
     { unfold posOrthCone; simpa using c1 i }
     { unfold posOrthCone; simpa using c2 i }
     { unfold posOrthCone; simpa using c3 i }
     { unfold posOrthCone; simpa using c4 i }
     { unfold rotatedSoCone; simp [sq_nonneg]; norm_num }
-    { unfold posOrthCone; simp [le_abs_self] }
-    { unfold posOrthCone; rw [←sub_le_iff_le_add, zero_sub]; simp [neg_le_abs_self] }
 
 vconditionElimination
 

CvxLean/Tactic/DCP/AtomLibrary/Fns/KLDiv.lean

@@ -91,18 +91,12 @@ feasibility
     unfold posOrthCone at h
     simpa using h)
 optimality by
-  apply klDiv.optimality x y t c1
-  { unfold posOrthCone expCone at *
-    simpa using c2 }
+  exact klDiv.optimality x y t c1 c2
 vconditionElimination
   (hx : by
-    apply klDiv.vcondElim0 x y t c1
-    unfold posOrthCone at *
-    simpa using c2)
+    exact klDiv.vcondElim0 x y t c1 c2)
   (hy : by
-    apply klDiv.vcondElim1 x y t c1
-    unfold posOrthCone expCone at *
-    simpa using c2)
+    exact klDiv.vcondElim1 x y t c1 c2)
 
 declare_atom Vec.klDiv [convex] (m : Nat)& (x : Fin m → ℝ)? (y : Fin m → ℝ)? :
   Vec.klDiv x y :=
@@ -130,20 +124,11 @@ feasibility
     unfold posOrthCone at h
     simpa [Vec.const] using h)
 optimality fun i => by
-    unfold Vec.expCone at c1
-    apply klDiv.optimality (x i) (y i) (t i) (c1 i)
-    unfold posOrthCone expCone at *
-    simpa [Vec.const] using (c2 i)
+    exact klDiv.optimality (x i) (y i) (t i) (c1 i) (c2 i)
 vconditionElimination
   (hx : fun i => by
-    unfold Vec.expCone at c1
-    apply klDiv.vcondElim0 (x i) (y i) (t i) (c1 i)
-    unfold posOrthCone expCone at *
-    simpa [Vec.const] using (c2 i))
+    exact klDiv.vcondElim0 (x i) (y i) (t i) (c1 i) (c2 i))
   (hy : fun i => by
-    unfold Vec.expCone at c1
-    apply klDiv.vcondElim1 (x i) (y i) (t i) (c1 i)
-    unfold posOrthCone expCone at *
-    simpa [Vec.const] using (c2 i))
+    exact klDiv.vcondElim1 (x i) (y i) (t i) (c1 i) (c2 i))
 
 end CvxLean

CvxLean/Tactic/DCP/Atoms.lean

@@ -141,7 +141,7 @@ def reduceAtomData (objCurv : Curvature) (atomData : GraphAtomData) : CommandEla
       trace[Meta.debug] "xsDecls: {xsDecls.map (·.userName)}"
 
       trace[Meta.debug] "before PAT "
-      let pat ← DCP.mkProcessedAtomTree objCurv objFun constraints.toList (xsDecls ++ originalVarsDecls)
+      let pat ← DCP.mkProcessedAtomTree objCurv objFun constraints.toList (originalVarsDecls)
       trace[Meta.debug] "after PAT "
       -- `pat` is the atom tree resulting from the DCP procedure.
 

CvxLean/Test/Convexify/Stanford.lean

@@ -0,0 +1,36 @@
+import CvxLean.Command.Solve
+import CvxLean.Tactic.ChangeOfVariables.Basic
+import CvxLean.Tactic.Convexify.Convexify
+import CvxLean.Test.Util.TimeCmd
+
+namespace Stanford
+
+noncomputable section
+
+open CvxLean Minimization Real
+
+/- Exercise 3.67. -/
+section E367
+
+def e367 :=
+  optimization (x1 x2 x3 x4 x5 x6 : ℝ)
+    minimize (-(sqrt x1 + sqrt x2 + sqrt x3 + sqrt x4 + sqrt x5 + sqrt x6) ^ (2 : ℝ))
+    subject to
+      h1 : 0 < x1
+      h2 : 0 < x2
+      h3 : 0 < x3
+      h4 : 0 < x4
+      h5 : 0 < x5
+      h6 : 0 < x6
+
+set_option maxHeartbeats 100000000
+time_cmd reduction red367/dcp367 : e367 := by
+  convexify
+
+#print dcp367
+
+end E367
+
+end
+
+end Stanford