feat: lift some atoms to vectors/matrices

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

@@ -8,8 +8,9 @@ namespace CvxLean
 
 open Real
 
-declare_atom div [affine] (x : ℝ)+ (y : ℝ)& : x / y :=
-bconditions (hy : (0 : ℝ) ≤ y)
+declare_atom div1 [affine] (x : ℝ)+ (y : ℝ)& : x / y :=
+bconditions
+  (hy : 0 ≤ y)
 homogenity by
   simp [mul_div]
 additivity by
@@ -18,8 +19,21 @@ optimality by
   intros x' hx
   by_cases h : 0 = y
   · rw [← h, div_zero, div_zero]
-  · rw [div_le_div_right]
+  · rw [div_le_div_right (lt_of_le_of_ne hy h)]
+    apply hx
+
+declare_atom div2 [affine] (x : ℝ)- (y : ℝ)& : x / y :=
+bconditions
+  (hy : y ≤ 0)
+homogenity by
+  simp [mul_div]
+additivity by
+  simp [add_div]
+optimality by
+  intros x' hx
+  by_cases h : y = 0
+  · rw [h, div_zero, div_zero]
+  · rw [div_le_div_right_of_neg (lt_of_le_of_ne hy h)]
     apply hx
-    apply lt_of_le_of_ne hy h
 
 end CvxLean

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

@@ -1,4 +1,5 @@
 import CvxLean.Tactic.DCP.AtomCmd
+import CvxLean.Lib.Math.Data.Matrix
 
 /-!
 Atom for negation (affine).
@@ -9,12 +10,31 @@ namespace CvxLean
 declare_atom neg [affine] (x : ℝ)- : - x :=
 bconditions
 homogenity by
-  simp [neg_zero, add_zero]
-additivity by
-  rw [neg_add]
   simp
+additivity by
+  simp; ring
 optimality by
   intros x' hx
-  apply neg_le_neg hx
+  simp [hx]
+
+declare_atom Vec.neg [affine] (n : ℕ)& (x : Fin n → ℝ)- : -x :=
+bconditions
+homogenity by
+  ext i; simp
+additivity by
+  ext i; simp; ring
+optimality by
+  intros x' hx
+  simp [hx]
+
+declare_atom Matrix.neg [affine] (m : ℕ)& (n : ℕ)& (A : Matrix.{0, 0, 0} (Fin m) (Fin n) ℝ)- : -A :=
+bconditions
+homogenity by
+  ext i j; simp
+additivity by
+  ext i j; simp; ring
+optimality by
+  intros A' hA i j
+  simp [hA i j]
 
 end CvxLean

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

@@ -27,6 +27,16 @@ optimality by
   intros _ h
   simp [h]
 
+declare_atom Vec.powOne [affine] (n : ℕ)& (x : Fin n → ℝ)+ : x ^ (1 : ℝ) :=
+bconditions
+homogenity by
+  ext i; simp
+additivity by
+  ext i; simp
+optimality by
+  intros _ h i
+  simp [h i]
+
 declare_atom powNegOne [convex] (x : ℝ)- : x ^ (-1 : ℝ) :=
 vconditions
   (hx : 0 < x)

CvxLean/Tactic/DCP/AtomLibrary/Sets/Cones.lean

@@ -17,6 +17,15 @@ declare_atom zeroCone [cone] (x : ℝ)? : zeroCone x :=
 optimality by
   simp [zeroCone]
 
+declare_atom Vec.zeroCone [cone] (n : ℕ)& (x : (Fin n) → ℝ)? : Vec.zeroCone x :=
+optimality by
+  simp [Vec.zeroCone]
+
+declare_atom Matrix.zeroCone [cone] (m : ℕ)& (n : ℕ)& (M : Matrix.{0,0,0} (Fin m) (Fin n) ℝ)? :
+  Matrix.zeroCone M :=
+optimality by
+  simp [Matrix.zeroCone]
+
 end ZeroCone
 
 /- Nonnegative orthant cone atoms. -/
@@ -27,12 +36,12 @@ optimality by
   simp [nonnegOrthCone]
 
 declare_atom Vec.nonnegOrthCone [cone]
-  (n : Nat)& (x : (Fin n) → ℝ)? : Vec.nonnegOrthCone x :=
+  (n : ℕ)& (x : (Fin n) → ℝ)? : Vec.nonnegOrthCone x :=
 optimality by
   simp [Vec.nonnegOrthCone]
 
 declare_atom Matrix.nonnegOrthCone [cone]
-  (m : Nat)& (n : Nat)& (M : Matrix.{0,0,0} (Fin m) (Fin n) ℝ)? :
+  (m : ℕ)& (n : ℕ)& (M : Matrix.{0,0,0} (Fin m) (Fin n) ℝ)? :
   Real.Matrix.nonnegOrthCone M :=
 optimality by
   simp [Matrix.nonnegOrthCone]
@@ -45,7 +54,7 @@ section ExpCone
 declare_atom expCone [cone] (x : ℝ)? (y : ℝ)? (z : ℝ)? : expCone x y z :=
 optimality le_refl _
 
-declare_atom Vec.expCone [cone] (n : Nat)& (x : (Fin n) → ℝ)? (y : (Fin n) → ℝ)?
+declare_atom Vec.expCone [cone] (n : ℕ)& (x : (Fin n) → ℝ)? (y : (Fin n) → ℝ)?
   (z : (Fin n) → ℝ)? : Vec.expCone x y z :=
 optimality le_refl _
 
@@ -54,19 +63,19 @@ end ExpCone
 /- Second-order cone and rotated second-order cone atoms. -/
 section SOCone
 
-declare_atom soCone [cone] (n : Nat)& (t : ℝ)? (x : (Fin n) → ℝ)? :
+declare_atom soCone [cone] (n : ℕ)& (t : ℝ)? (x : (Fin n) → ℝ)? :
   soCone t x :=
 optimality le_refl _
 
-declare_atom Vec.soCone [cone] (n : Nat)& (m : Nat)& (t : Fin m → Real)?
+declare_atom Vec.soCone [cone] (n : ℕ)& (m : ℕ)& (t : Fin m → Real)?
   (X : Matrix.{0,0,0} (Fin m) (Fin n) Real)? : Vec.soCone t X :=
 optimality le_refl _
 
-declare_atom rotatedSoCone [cone] (n : Nat)& (v : ℝ)? (w : ℝ)?
+declare_atom rotatedSoCone [cone] (n : ℕ)& (v : ℝ)? (w : ℝ)?
   (x : (Fin n) → ℝ)? : rotatedSoCone v w x :=
 optimality le_refl _
 
-declare_atom Vec.rotatedSoCone [cone] (m : Nat)& (n : Nat)& (v : (Fin n) → ℝ)?
+declare_atom Vec.rotatedSoCone [cone] (m : ℕ)& (n : ℕ)& (v : (Fin n) → ℝ)?
   (w : (Fin n) → ℝ)? (x : (Fin n) → (Fin m) → ℝ)? : Vec.rotatedSoCone v w x :=
 optimality le_refl _
 

CvxLean/Tactic/DCP/AtomLibrary/Sets/Eq.lean

@@ -27,4 +27,39 @@ optimality by
   exact Eq.symm
 vconditionElimination
 
+declare_atom Vec.eq [convex_set] (n : ℕ)& (x : Fin n → ℝ)? (y : Fin n → ℝ)? : x = y :=
+vconditions
+implementationVars
+implementationObjective Real.Vec.zeroCone (y - x)
+implementationConstraints
+solution
+solutionEqualsAtom by
+  unfold Real.Vec.zeroCone Real.zeroCone
+  simp [sub_eq_iff_eq_add, zero_add]
+  aesop
+feasibility
+optimality by
+  unfold Real.Vec.zeroCone Real.zeroCone
+  simp [sub_eq_iff_eq_add, zero_add]
+  aesop
+vconditionElimination
+
+declare_atom Matrix.eq [convex_set] (m : ℕ)& (n : ℕ)& (X : Matrix.{0,0,0} (Fin m) (Fin n) ℝ)?
+  (Y : Matrix.{0,0,0} (Fin m) (Fin n) ℝ)? : X = Y :=
+vconditions
+implementationVars
+implementationObjective Real.Matrix.zeroCone (Y - X)
+implementationConstraints
+solution
+solutionEqualsAtom by
+  unfold Real.Matrix.zeroCone Real.zeroCone
+  simp [sub_eq_iff_eq_add, zero_add]
+  aesop
+feasibility
+optimality by
+  unfold Real.Matrix.zeroCone Real.zeroCone
+  simp [sub_eq_iff_eq_add, zero_add]
+  aesop
+vconditionElimination
+
 end CvxLean

CvxLean/Tactic/DCP/AtomLibrary/Sets/Le.lean

@@ -1,6 +1,7 @@
 import CvxLean.Tactic.DCP.AtomCmd
 import CvxLean.Tactic.DCP.AtomLibrary.Sets.Cones
 import CvxLean.Tactic.DCP.AtomLibrary.Fns.Sub
+import CvxLean.Lib.Math.Data.Matrix
 
 /-!
 Inequality atoms (convex set).
@@ -76,4 +77,25 @@ optimality by
   exact le.optimality _ _ _ _ (hx i) (hy i) (h i)
 vconditionElimination
 
+declare_atom Matrix.le [convex_set] (m : Nat)& (n : Nat)& (X : Matrix.{0,0,0} (Fin m) (Fin n) ℝ)-
+    (Y : Matrix.{0,0,0} (Fin m) (Fin n) ℝ)+ : X ≤ Y :=
+vconditions
+implementationVars
+implementationObjective Real.Matrix.nonnegOrthCone (Y - X)
+implementationConstraints
+solution
+solutionEqualsAtom by
+  unfold Real.Matrix.nonnegOrthCone Real.nonnegOrthCone
+  aesop
+feasibility
+optimality by
+  intros X' Y' hX hY h i j
+  unfold Real.Matrix.nonnegOrthCone Real.nonnegOrthCone at h
+  have hij := h i j
+  have hXij := hX i j
+  have hYij := hY i j
+  simp at hij hXij hYij
+  linarith
+vconditionElimination
+
 end CvxLean

CvxLean/Tactic/PreDCP/Egg/FromMinimization.lean

@@ -57,7 +57,11 @@ def opMap : HashMap String (String × Array EggTreeOpArgTag) :=
     ("mul",         ("mul",     #[.arg, .arg])),
     ("mul1",        ("mul",     #[.arg, .arg])),
     ("mul2",        ("mul",     #[.arg, .arg])),
+    ("mul3",        ("mul",     #[.arg, .arg])),
+    ("mul4",        ("mul",     #[.arg, .arg])),
     ("div",         ("div",     #[.arg, .arg])),
+    ("div1",        ("div",     #[.arg, .arg])),
+    ("div2",        ("div",     #[.arg, .arg])),
     ("quadOverLin", ("qol",     #[.arg, .arg])),
     ("geoMean",     ("geo",     #[.arg, .arg])),
     ("logSumExp₂",  ("lse",     #[.arg, .arg])),