feat: generalize set atoms

verified-optimization · Mar 8, 2024 · 3281a89 · 3281a89
1 parent 01fdac0
commit 3281a89
Show file tree

Hide file tree

Showing 2 changed files with 57 additions and 0 deletions.
diff --git a/CvxLean/Tactic/DCP/AtomLibrary/Sets/Eq.lean b/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
diff --git a/CvxLean/Tactic/DCP/AtomLibrary/Sets/Le.lean b/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