From d4c5e09308e43cf7ab44973f0b1fa23f0ba42d22 Mon Sep 17 00:00:00 2001 From: Ramon Fernandez Mir Date: Sat, 24 Feb 2024 18:57:05 +0000 Subject: [PATCH 01/25] doc: `remove_constr` and `remove_trivial_constrs` --- CvxLean/Tactic/Basic/ChangeOfVariables.lean | 2 +- CvxLean/Tactic/Basic/RemoveConstr.lean | 33 +++++++++++++++++-- .../Tactic/Basic/RemoveTrivialConstrs.lean | 11 +++++-- 3 files changed, 40 insertions(+), 6 deletions(-) diff --git a/CvxLean/Tactic/Basic/ChangeOfVariables.lean b/CvxLean/Tactic/Basic/ChangeOfVariables.lean index 58c84c8d..88c3d55d 100644 --- a/CvxLean/Tactic/Basic/ChangeOfVariables.lean +++ b/CvxLean/Tactic/Basic/ChangeOfVariables.lean @@ -30,7 +30,7 @@ The resulting problem `q` looks as follows: optimization (u : ℝ) minimize exp u subject to - c : 0 < exp u := by + c : 0 < exp u ``` We provide `change_of_variables!` as a convenient variant that also tries to remove trivial constraints. In this case, it would remove `0 < exp u` as it is always true. diff --git a/CvxLean/Tactic/Basic/RemoveConstr.lean b/CvxLean/Tactic/Basic/RemoveConstr.lean index ba5ed613..193bbadc 100644 --- a/CvxLean/Tactic/Basic/RemoveConstr.lean +++ b/CvxLean/Tactic/Basic/RemoveConstr.lean @@ -2,6 +2,33 @@ import CvxLean.Meta.Equivalence import CvxLean.Meta.TacticBuilder import CvxLean.Meta.Util.Expr +/-! +# Tactic to remove constraints + +This file defines the `remove_constr` tactic. In some cases, a constraint may be trivially true or +it might be implied by the other constraints. + +We illustrate it with an example of how to use it inside the `equivalence` command: +``` +equivalence eqv/q : + optimization (x : ℝ) + minimize x + subject to + c₁ : 1 ≤ x + c₂ : 0 < x := by + remove_constr c₁ => + linarith +``` +The resulting problem `q` looks as follows: +``` +optimization (u : ℝ) + minimize exp u + subject to + c₁ : 1 ≤ x +``` +In this case, `c₂` follows from `c₁`, so it can be removed. +-/ + namespace CvxLean open Lean Expr Meta Elab Term Tactic @@ -36,7 +63,10 @@ def composeAndIntro (l : List Expr) : MetaM Expr := let esTy ← inferType es return mkApp4 (mkConst ``And.intro) eTy esTy e es -/-- -/ +/-- The main logic to remove constraints is found here. Essentially, if we want to remove +constraint `cᵢ`, we ask users to provide a proof that `c₁ ∧ ⋯ ∧ cᵢ₋₁ ∧ cᵢ₊₁ ∧ ⋯ ∧ cₙ → cᵢ`. From +this, we build a proof that `c₁ ∧ ... ∧ cᵢ₋₁ ∧ cᵢ₊₁ ∧ ... ∧ cₙ ↔ c₁ ∧ ... ∧ cₙ`. Then, the +equivalence can be build by using `Minimization.Equivalence.rewrite_constraints`. -/ def removeConstrBuilder (id : Name) (proof : Syntax) : EquivalenceBuilder Unit := fun eqvExpr g => g.withContext do let lhsMinExpr ← eqvExpr.toMinimizationExprLHS @@ -106,7 +136,6 @@ end Meta namespace Tactic -/-- -/ syntax (name := removeConstr) "remove_constr" ident " => " tacticSeq : tactic @[tactic removeConstr] diff --git a/CvxLean/Tactic/Basic/RemoveTrivialConstrs.lean b/CvxLean/Tactic/Basic/RemoveTrivialConstrs.lean index ef555f1e..11ce99c4 100644 --- a/CvxLean/Tactic/Basic/RemoveTrivialConstrs.lean +++ b/CvxLean/Tactic/Basic/RemoveTrivialConstrs.lean @@ -1,15 +1,21 @@ import CvxLean.Tactic.Basic.RemoveConstr import CvxLean.Tactic.Arith.Arith -namespace CvxLean +/-! +# Tactic to remove trivial constraints -open Lean +This file defines the `remove_trivial_constrs`. It essentially uses `remove_constr` on every +constraint and tries to establish the proof obligation using the `positivity!` tactic. This is +useful for constraints of the form `0 < exp x`, for example. +-/ +namespace CvxLean open Lean Meta Elab Term Tactic namespace Meta +/-- Iteratively try to apply `remove_constr` on every constraint. Do nothing if it fails. -/ def removeTrivialConstrsBuilder : EquivalenceBuilder Unit := fun eqvExpr g => g.withContext do let lhs ← eqvExpr.toMinimizationExprLHS let constrNames ← withLambdaBody lhs.constraints fun _ constrsBody => do @@ -34,7 +40,6 @@ namespace Tactic syntax (name := removeTrivialConstrs) "remove_trivial_constrs" : tactic -/-- -/ @[tactic removeTrivialConstrs] def evalRemoveTrivialConstrs : Tactic := fun stx => match stx with | `(tactic| remove_trivial_constrs) => do From 7cb59753c7e348b09819dc8de46197ce56d2072c Mon Sep 17 00:00:00 2001 From: Ramon Fernandez Mir Date: Tue, 27 Feb 2024 10:10:23 +0000 Subject: [PATCH 02/25] chore: clean up logs in extractor --- egg-pre-dcp/src/extract.rs | 20 ++++++++++---------- 1 file changed, 10 insertions(+), 10 deletions(-) diff --git a/egg-pre-dcp/src/extract.rs b/egg-pre-dcp/src/extract.rs index b467f04f..3a7efd90 100644 --- a/egg-pre-dcp/src/extract.rs +++ b/egg-pre-dcp/src/extract.rs @@ -276,29 +276,29 @@ pub fn get_steps_from_string_maybe_node_limit( let curvature = best_curvature; let num_vars = best_num_vars; + // Note: each domain constraint is an expression with 3 nodes, e.g. `0 <= x`. let term_size = best_term_size + 3 * (domains_len as u32); - if debug && curvature <= Curvature::Convex { - let total_nodes = runner.egraph.total_number_of_nodes(); - println!("Succeeded with node limit {:?} (using {:?} nodes).", node_limit, total_nodes); - println!("Best curvature: {:?}.", curvature); - println!("Best number of variables: {:?}.", num_vars); - println!("Best term size: {:?}.", term_size); - println!("Best term: {:?}.", best.to_string()); - } - // If term is not DCP, try with the next node limit. if curvature <= Curvature::Convex { if debug { + let total_nodes = runner.egraph.total_number_of_nodes(); + println!("Succeeded with node limit {:?} (using {:?} nodes).", node_limit, total_nodes); + println!("Best curvature: {:?}.", curvature); + println!("Best number of variables: {:?}.", num_vars); + println!("Best term size: {:?}.", term_size); + println!("Best term: {:?}.", best.to_string()); + let build_time = starting_time.elapsed().as_millis(); println!("E-graph building time: {:.2?} ms.", build_time); } } else { + // If term is not DCP, try with the next node limit. continue; } let after_build_time = Instant::now(); - // If term is DCP, extract the steps. + // If term is DCP, find the explanation. let mut egraph = runner.egraph; let mut explanation : Explanation = egraph.explain_equivalence(&expr, &best); From 1d23224d7b10fba4f1684b2472c5637480159720 Mon Sep 17 00:00:00 2001 From: Ramon Fernandez Mir Date: Tue, 27 Feb 2024 19:50:57 +0000 Subject: [PATCH 03/25] style: division notation in pre-DCP main example --- CvxLean/Test/PreDCP/MainExample.lean | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/CvxLean/Test/PreDCP/MainExample.lean b/CvxLean/Test/PreDCP/MainExample.lean index c864ccf9..140a1647 100644 --- a/CvxLean/Test/PreDCP/MainExample.lean +++ b/CvxLean/Test/PreDCP/MainExample.lean @@ -13,12 +13,14 @@ def p := optimization (x : ℝ) minimize (x) subject to - h1 : 0.001 ≤ x + h1 : 1 / 1000 ≤ x h2 : 1 / (sqrt x) ≤ (exp x) time_cmd equivalence eq/q : p := by pre_dcp +#check congrArg + #print q -- optimization (x : ℝ) -- minimize x From afe3b0ab0063d75db917fe34a092e5cffdd479d7 Mon Sep 17 00:00:00 2001 From: Ramon Fernandez Mir Date: Wed, 28 Feb 2024 15:45:18 +0000 Subject: [PATCH 04/25] refactor: `equivalence'` -> `equivalence*` --- CvxLean/Command/Equivalence.lean | 6 +++--- CvxLean/Demos/LT2024.lean | 2 +- CvxLean/Examples/FittingSphere.lean | 4 ++-- CvxLean/Examples/HypersonicShapeDesign.lean | 4 ++-- CvxLean/Examples/TrussDesign.lean | 4 ++-- CvxLean/Examples/VehicleSpeedScheduling.lean | 4 ++-- CvxLean/Lib/Equivalence.lean | 4 ++-- CvxLean/Test/BasicTactics/Other.lean | 2 +- 8 files changed, 15 insertions(+), 15 deletions(-) diff --git a/CvxLean/Command/Equivalence.lean b/CvxLean/Command/Equivalence.lean index 5ac28d75..a7e0d970 100644 --- a/CvxLean/Command/Equivalence.lean +++ b/CvxLean/Command/Equivalence.lean @@ -23,7 +23,7 @@ environment: * `q := r`, * `eqv : p ≡ q`. -Writing `equivalence'` instead of `equivalence` will also generate a backward solution map at the +Writing `equivalence*` instead of `equivalence` will also generate a backward solution map at the level of floats. -/ @@ -46,7 +46,7 @@ syntax (name := equivalence) /-- Open an equivalence environment and try to generate a computable backward map. -/ syntax (name := equivalenceAndBwdMap) - "equivalence'" ident "/" ident declSig ":=" Lean.Parser.Term.byTactic : command + "equivalence*" ident "/" ident declSig ":=" Lean.Parser.Term.byTactic : command /-- Open an equivalence environment with a given left-hand-side problem (`lhsStx`) and perhaps some parameters (`xs`). From this, an equivalence goal is set to a target problem which is represented by @@ -139,7 +139,7 @@ def evalEquivalence : CommandElab := fun stx => match stx with /-- Same as `equivalence` but also adds the backward map to the environment. -/ @[command_elab «equivalenceAndBwdMap»] def evalEquivalenceAndBwdMap : CommandElab := fun stx => match stx with - | `(equivalence' $eqvId / $probId $declSig := $proofStx) => do + | `(equivalence* $eqvId / $probId $declSig := $proofStx) => do liftTermElabM do let (binders, lhsStx) := expandDeclSig declSig.raw elabBindersEx binders.getArgs fun xs => diff --git a/CvxLean/Demos/LT2024.lean b/CvxLean/Demos/LT2024.lean index bf269529..a47c050b 100644 --- a/CvxLean/Demos/LT2024.lean +++ b/CvxLean/Demos/LT2024.lean @@ -73,7 +73,7 @@ def p₃ (Awall Aflr α β γ δ : ℝ) := set_option trace.Meta.debug true -equivalence' eqv₃/q₃ : p₃ 100 10 0.5 2 0.5 2 := by +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') change_of_variables! (d') (d ↦ exp d') diff --git a/CvxLean/Examples/FittingSphere.lean b/CvxLean/Examples/FittingSphere.lean index 7d614b6e..9c32c56c 100644 --- a/CvxLean/Examples/FittingSphere.lean +++ b/CvxLean/Examples/FittingSphere.lean @@ -91,7 +91,7 @@ instance : ChangeOfVariables fun ((c, t) : (Fin n → ℝ) × ℝ) => (c, sqrt ( condition := fun (_, r) => 0 ≤ r, property := fun ⟨c, r⟩ h => by simp [sqrt_sq h] } -equivalence' eqv/fittingSphereT (n m : ℕ) (x : Fin m → Fin n → ℝ) : fittingSphere n m x := by +equivalence* eqv/fittingSphereT (n m : ℕ) (x : Fin m → Fin n → ℝ) : fittingSphere n m x := by -- Change of variables. equivalence_step => apply ChangeOfVariables.toEquivalence @@ -106,7 +106,7 @@ equivalence' eqv/fittingSphereT (n m : ℕ) (x : Fin m → Fin n → ℝ) : fitt dsimp at h₁ ⊢; simp [Vec.sum, Vec.norm, Vec.const]; congr; funext i; congr 1; rw [norm_sub_sq (𝕜 := ℝ) (E := Fin n → ℝ), sq_sqrt (rpow_two _ ▸ le_of_lt (sqrt_pos.mp h₁))] simp [mulVec, inner, dotProduct] - + #print fittingSphereT -- optimization (c : Fin n → ℝ) (t : ℝ) -- minimize Vec.sum ((Vec.norm x ^ 2 - 2 * mulVec x c - Vec.const m t) ^ 2) diff --git a/CvxLean/Examples/HypersonicShapeDesign.lean b/CvxLean/Examples/HypersonicShapeDesign.lean index e7580962..15c2e4d1 100644 --- a/CvxLean/Examples/HypersonicShapeDesign.lean +++ b/CvxLean/Examples/HypersonicShapeDesign.lean @@ -27,7 +27,7 @@ def hypersonicShapeDesign := h₂ : Δx ≤ 1 h₃ : a * (1 / Δx) - (1 - b) * sqrt (1 - Δx ^ 2) ≤ 0 -equivalence' eqv₁/hypersonicShapeDesignConvex (a b : ℝ) (ha : 0 ≤ a) (hb₁ : 0 ≤ b) (hb₂ : b < 1) : +equivalence* eqv₁/hypersonicShapeDesignConvex (a b : ℝ) (ha : 0 ≤ a) (hb₁ : 0 ≤ b) (hb₂ : b < 1) : hypersonicShapeDesign a b := by pre_dcp @@ -84,7 +84,7 @@ def ldRatioₚ := 1 / (Float.sqrt ((1 / wₚ_opt ^ 2) - 1)) -- While the above is good enough, we simplify the problem further by performing a change of -- variables and simplifying appropriately. -equivalence' eqv₂/hypersonicShapeDesignSimpler (a b : ℝ) (ha : 0 ≤ a) (hb₁ : 0 ≤ b) +equivalence* eqv₂/hypersonicShapeDesignSimpler (a b : ℝ) (ha : 0 ≤ a) (hb₁ : 0 ≤ b) (hb₂ : b < 1) : hypersonicShapeDesignConvex a b ha hb₁ hb₂ := by change_of_variables (z) (Δx ↦ sqrt z) conv_constr h₁ => diff --git a/CvxLean/Examples/TrussDesign.lean b/CvxLean/Examples/TrussDesign.lean index 3fdd3ce9..fbbda49f 100644 --- a/CvxLean/Examples/TrussDesign.lean +++ b/CvxLean/Examples/TrussDesign.lean @@ -56,7 +56,7 @@ instance : ChangeOfVariables simp; rw [mul_comm _ (R ^ 2 - r ^ 2), ← mul_div, div_self (by positivity), mul_one] ring_nf; exact sqrt_sq hR } -equivalence' eqv₁/trussDesignGP (hmin hmax wmin wmax Rmax σ F₁ F₂ : ℝ) : +equivalence* eqv₁/trussDesignGP (hmin hmax wmin wmax Rmax σ F₁ F₂ : ℝ) : trussDesign hmin hmax wmin wmax Rmax σ F₁ F₂ := by -- Apply key change of variables. equivalence_step => @@ -114,7 +114,7 @@ instance : ChangeOfVariables property := fun (h', w', r', A') ⟨hh', hw', hr', hA'⟩ => by simp [exp_log hh', exp_log hw', exp_log hr', exp_log hA'] } -equivalence' eqv₂/trussDesignConvex (hmin hmax : ℝ) (hmin_pos : 0 < hmin) +equivalence* eqv₂/trussDesignConvex (hmin hmax : ℝ) (hmin_pos : 0 < hmin) (hmin_le_hmax : hmin ≤ hmax) (wmin wmax : ℝ) (wmin_pos : 0 < wmin) (wmin_le_wmax : wmin ≤ wmax) (Rmax σ F₁ F₂ : ℝ) : trussDesignGP hmin hmax wmin wmax Rmax σ F₁ F₂ := by -- Change variables. diff --git a/CvxLean/Examples/VehicleSpeedScheduling.lean b/CvxLean/Examples/VehicleSpeedScheduling.lean index 1720ab72..f5210779 100644 --- a/CvxLean/Examples/VehicleSpeedScheduling.lean +++ b/CvxLean/Examples/VehicleSpeedScheduling.lean @@ -52,7 +52,7 @@ private lemma fold_partial_sum [hn : Fact (0 < n)] (t : Fin n → ℝ) (i : Fin . rfl . linarith [hn.out] -equivalence' eqv₁/vehSpeedSchedConvex (n : ℕ) (d : Fin n → ℝ) +equivalence* eqv₁/vehSpeedSchedConvex (n : ℕ) (d : Fin n → ℝ) (τmin τmax smin smax : Fin n → ℝ) (F : ℝ → ℝ) (h_n_pos : 0 < n) (h_d_pos : StrongLT 0 d) (h_smin_pos : StrongLT 0 smin) : @vehSpeedSched n d τmin τmax smin smax F ⟨h_n_pos⟩ := by replace h_d_pos : ∀ i, 0 < d i := fun i => h_d_pos i @@ -98,7 +98,7 @@ equivalence' eqv₁/vehSpeedSchedConvex (n : ℕ) (d : Fin n → ℝ) -- However, if we fix `F`, we can use other atoms. For example, if `F` is quadratic, the problem can -- be reduced. Let `F(s) = a * s^2 + b * s + c` with `0 ≤ a`. -equivalence' eqv₂/vehSpeedSchedQuadratic (n : ℕ) (d : Fin n → ℝ) +equivalence* eqv₂/vehSpeedSchedQuadratic (n : ℕ) (d : Fin n → ℝ) (τmin τmax smin smax : Fin n → ℝ) (a b c : ℝ) (h_n_pos : 0 < n) (h_d_pos : StrongLT 0 d) (h_smin_pos : StrongLT 0 smin) : vehSpeedSchedConvex n d τmin τmax smin smax (fun s => a • s ^ (2 : ℝ) + b • s + c) diff --git a/CvxLean/Lib/Equivalence.lean b/CvxLean/Lib/Equivalence.lean index 2f134594..6761e2a0 100644 --- a/CvxLean/Lib/Equivalence.lean +++ b/CvxLean/Lib/Equivalence.lean @@ -221,14 +221,14 @@ def map_objFun {g : R → R} (h : ∀ {r s}, cs r → cs s → (g (f r) ≤ g (f ⟨h_feas_x, fun y h_feas_y => (h h_feas_x h_feas_y).mp (h_opt_x y h_feas_y)⟩ } @[equiv] -noncomputable def map_objFun_log {f : D → ℝ} (h : ∀ x, cs x → f x > 0) : +lemma map_objFun_log {f : D → ℝ} (h : ∀ x, cs x → f x > 0) : ⟨f, cs⟩ ≡ ⟨fun x => (Real.log (f x)), cs⟩ := by apply map_objFun intros r s h_feas_r h_feas_s exact Real.log_le_log_iff (h r h_feas_r) (h s h_feas_s) @[equiv] -noncomputable def map_objFun_sq {f : D → ℝ} (h : ∀ x, cs x → f x ≥ 0) : +lemma map_objFun_sq {f : D → ℝ} (h : ∀ x, cs x → f x ≥ 0) : ⟨f, cs⟩ ≡ ⟨fun x => (f x) ^ (2 : ℝ), cs⟩ := by apply map_objFun (g := fun x => x ^ (2 : ℝ)) intros r s h_feas_r h_feas_s diff --git a/CvxLean/Test/BasicTactics/Other.lean b/CvxLean/Test/BasicTactics/Other.lean index cd23ef7a..3f424065 100644 --- a/CvxLean/Test/BasicTactics/Other.lean +++ b/CvxLean/Test/BasicTactics/Other.lean @@ -130,7 +130,7 @@ def p := c₃ : log (y - 1) ≤ 2 * sqrt x + 1 c₄ : 3 * x + 5 * y ≤ 10 -equivalence' eqv3/q3 : p := by +equivalence* eqv3/q3 : p := by change_of_variables! (v) (y ↦ v + 1) change_of_variables! (w) (v ↦ exp w) remove_constr c₂ => From f0ae187081d1a53b84c97f63798e687c1e62449f Mon Sep 17 00:00:00 2001 From: Ramon Fernandez Mir Date: Wed, 28 Feb 2024 15:50:49 +0000 Subject: [PATCH 05/25] style: eta reduction in case study --- CvxLean/Examples/VehicleSpeedScheduling.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/CvxLean/Examples/VehicleSpeedScheduling.lean b/CvxLean/Examples/VehicleSpeedScheduling.lean index f5210779..40db03be 100644 --- a/CvxLean/Examples/VehicleSpeedScheduling.lean +++ b/CvxLean/Examples/VehicleSpeedScheduling.lean @@ -55,8 +55,8 @@ private lemma fold_partial_sum [hn : Fact (0 < n)] (t : Fin n → ℝ) (i : Fin equivalence* eqv₁/vehSpeedSchedConvex (n : ℕ) (d : Fin n → ℝ) (τmin τmax smin smax : Fin n → ℝ) (F : ℝ → ℝ) (h_n_pos : 0 < n) (h_d_pos : StrongLT 0 d) (h_smin_pos : StrongLT 0 smin) : @vehSpeedSched n d τmin τmax smin smax F ⟨h_n_pos⟩ := by - replace h_d_pos : ∀ i, 0 < d i := fun i => h_d_pos i - replace h_smin_pos : ∀ i, 0 < smin i := fun i => h_smin_pos i + replace h_d_pos : ∀ i, 0 < d i := h_d_pos + replace h_smin_pos : ∀ i, 0 < smin i := h_smin_pos haveI : Fact (0 < n) := ⟨h_n_pos⟩ -- Change variables `s ↦ d / t`. -- TODO: This can be done by change of variables by detecting that the variable is a vector. From 575a16ccb65e1f1132a2acb0ed8541a385480b9a Mon Sep 17 00:00:00 2001 From: Ramon Fernandez Mir Date: Wed, 28 Feb 2024 16:16:45 +0000 Subject: [PATCH 06/25] fix: equivalences cannot be lemmas --- CvxLean/Lib/Equivalence.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/CvxLean/Lib/Equivalence.lean b/CvxLean/Lib/Equivalence.lean index 6761e2a0..2f134594 100644 --- a/CvxLean/Lib/Equivalence.lean +++ b/CvxLean/Lib/Equivalence.lean @@ -221,14 +221,14 @@ def map_objFun {g : R → R} (h : ∀ {r s}, cs r → cs s → (g (f r) ≤ g (f ⟨h_feas_x, fun y h_feas_y => (h h_feas_x h_feas_y).mp (h_opt_x y h_feas_y)⟩ } @[equiv] -lemma map_objFun_log {f : D → ℝ} (h : ∀ x, cs x → f x > 0) : +noncomputable def map_objFun_log {f : D → ℝ} (h : ∀ x, cs x → f x > 0) : ⟨f, cs⟩ ≡ ⟨fun x => (Real.log (f x)), cs⟩ := by apply map_objFun intros r s h_feas_r h_feas_s exact Real.log_le_log_iff (h r h_feas_r) (h s h_feas_s) @[equiv] -lemma map_objFun_sq {f : D → ℝ} (h : ∀ x, cs x → f x ≥ 0) : +noncomputable def map_objFun_sq {f : D → ℝ} (h : ∀ x, cs x → f x ≥ 0) : ⟨f, cs⟩ ≡ ⟨fun x => (f x) ^ (2 : ℝ), cs⟩ := by apply map_objFun (g := fun x => x ^ (2 : ℝ)) intros r s h_feas_r h_feas_s From 4c0b58030ae80394992666f6e32a2812d2cc7b51 Mon Sep 17 00:00:00 2001 From: Ramon Fernandez Mir Date: Thu, 29 Feb 2024 15:56:46 +0000 Subject: [PATCH 07/25] chore: proof example in vehicle speed scheduling --- CvxLean/Examples/VehicleSpeedScheduling.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/CvxLean/Examples/VehicleSpeedScheduling.lean b/CvxLean/Examples/VehicleSpeedScheduling.lean index 40db03be..19ff3d5d 100644 --- a/CvxLean/Examples/VehicleSpeedScheduling.lean +++ b/CvxLean/Examples/VehicleSpeedScheduling.lean @@ -165,7 +165,7 @@ def τminₚ : Fin nₚ → ℝ := def τmaxₚ : Fin nₚ → ℝ := ![4.6528, 6.5147, 7.5178, 9.7478, 9.0641, 10.3891, 13.1540, 16.0878, 17.4352, 20.9539] -@[optimization_param] +@[optimization_param, simp] def sminₚ : Fin nₚ → ℝ := ![0.7828, 0.6235, 0.7155, 0.5340, 0.6329, 0.4259, 0.7798, 0.9604, 0.7298, 0.8405] @@ -174,7 +174,7 @@ def smaxₚ : Fin nₚ → ℝ := ![1.9624, 1.6036, 1.6439, 1.5641, 1.7194, 1.9090, 1.3193, 1.3366, 1.9470, 2.8803] lemma sminₚ_pos : StrongLT 0 sminₚ := by - intro i; fin_cases i <;> (simp [sminₚ]; norm_num) + intro i; fin_cases i <;> norm_num @[simp] lemma sminₚ_nonneg : 0 ≤ sminₚ := le_of_strongLT sminₚ_pos From ee9f4b1779bf457c44f8fa04587496bbad0758bb Mon Sep 17 00:00:00 2001 From: Ramon Fernandez Mir Date: Thu, 29 Feb 2024 16:14:54 +0000 Subject: [PATCH 08/25] doc: add TODO on leaving goals for pre-DCP --- CvxLean/Tactic/PreDCP/PreDCP.lean | 6 ++++++ 1 file changed, 6 insertions(+) diff --git a/CvxLean/Tactic/PreDCP/PreDCP.lean b/CvxLean/Tactic/PreDCP/PreDCP.lean index f7a22eca..615b3f8c 100644 --- a/CvxLean/Tactic/PreDCP/PreDCP.lean +++ b/CvxLean/Tactic/PreDCP/PreDCP.lean @@ -15,6 +15,12 @@ import CvxLean.Tactic.Basic.RewriteOpt This file defines the tactic `pre_dcp`, which calls `egg` to find a sequence of rewrites that turns an optimization problem into DCP form. + +### TODO + +* Currently, the tactic immediately fails if it cannot prove some side condition, we could instead + leave them as goals for the user to prove manually. Assuming that the interval arithmetic used on + the `egg` side is correct, they should all be provable. -/ namespace CvxLean From c0923ca1593996b3c60070ebd2ce887562c849b4 Mon Sep 17 00:00:00 2001 From: Ramon Fernandez Mir Date: Thu, 29 Feb 2024 16:21:24 +0000 Subject: [PATCH 09/25] doc: atom library extension --- CvxLean/Tactic/DCP/AtomExt.lean | 17 ++++++++++++++--- 1 file changed, 14 insertions(+), 3 deletions(-) diff --git a/CvxLean/Tactic/DCP/AtomExt.lean b/CvxLean/Tactic/DCP/AtomExt.lean index 22a86623..12672d64 100644 --- a/CvxLean/Tactic/DCP/AtomExt.lean +++ b/CvxLean/Tactic/DCP/AtomExt.lean @@ -1,5 +1,14 @@ import CvxLean.Tactic.DCP.DiscrTree +/-! +# Atom library (extension) + +This file defines the `GraphAtomData` type, which is what is stored when declaring an atom. This +includes defining `Curvature` and `ArgKind`, and the composition rule using them. + +The enviromnet extesion is also defined here. +-/ + namespace CvxLean open Lean Lean.Meta @@ -9,8 +18,7 @@ inductive Curvature where | Constant | Affine | Concave | Convex | AffineSet | ConvexSet deriving BEq, Inhabited -/-- Arguments of an atom are increasing (+), decreasing (-), constant (&) or -neither (?). -/ +/-- Arguments of an atom are increasing (+), decreasing (-), constant (&) or neither (?). -/ inductive ArgKind where | Increasing | Decreasing | Neither | Constant deriving BEq, Inhabited @@ -22,7 +30,10 @@ def curvatureInArg : Curvature → ArgKind → Curvature | Curvature.Concave, ArgKind.Decreasing => Curvature.Convex | Curvature.Convex, ArgKind.Increasing => Curvature.Convex | Curvature.Convex, ArgKind.Decreasing => Curvature.Concave - -- TODO: Explain this. + -- This requires some explanation. The only set atom that allows non-affine arguments is `≤`. The + -- rest, equality and cones, require affine arguments. We say that an expression `x ≤ y` is + -- decreasing in `x` in the following sense: if `x' ≤ x` then `x ≤ y → x' ≤ y`, where `→` is seen + -- as the order relation in `Prop`. | Curvature.ConvexSet, ArgKind.Increasing => Curvature.Concave | Curvature.ConvexSet, ArgKind.Decreasing => Curvature.Convex | _, _ => Curvature.Affine From da1ff241ec0ae19b5b97f82156c990ef2324ed0e Mon Sep 17 00:00:00 2001 From: Ramon Fernandez Mir Date: Thu, 29 Feb 2024 16:24:27 +0000 Subject: [PATCH 10/25] refactor: `Atoms` -> `AtomCmd` --- CvxLean/Tactic/DCP/{Atoms.lean => AtomCmd.lean} | 0 CvxLean/Tactic/DCP/AtomLibrary/Fns/Abs.lean | 3 +-- CvxLean/Tactic/DCP/AtomLibrary/Fns/Add.lean | 3 +-- CvxLean/Tactic/DCP/AtomLibrary/Fns/CumSum.lean | 3 +-- CvxLean/Tactic/DCP/AtomLibrary/Fns/Diag.lean | 3 +-- CvxLean/Tactic/DCP/AtomLibrary/Fns/Diagonal.lean | 3 +-- CvxLean/Tactic/DCP/AtomLibrary/Fns/Div.lean | 3 +-- CvxLean/Tactic/DCP/AtomLibrary/Fns/DotProduct.lean | 3 +-- CvxLean/Tactic/DCP/AtomLibrary/Fns/Entr.lean | 3 +-- CvxLean/Tactic/DCP/AtomLibrary/Fns/Exp.lean | 3 +-- CvxLean/Tactic/DCP/AtomLibrary/Fns/FromBlocks.lean | 3 +-- CvxLean/Tactic/DCP/AtomLibrary/Fns/GeoMean.lean | 3 +-- CvxLean/Tactic/DCP/AtomLibrary/Fns/Huber.lean | 3 +-- CvxLean/Tactic/DCP/AtomLibrary/Fns/Inv.lean | 3 +-- CvxLean/Tactic/DCP/AtomLibrary/Fns/KLDiv.lean | 3 +-- CvxLean/Tactic/DCP/AtomLibrary/Fns/Log.lean | 3 +-- CvxLean/Tactic/DCP/AtomLibrary/Fns/LogDet.lean | 3 +-- CvxLean/Tactic/DCP/AtomLibrary/Fns/LogSumExp.lean | 3 +-- CvxLean/Tactic/DCP/AtomLibrary/Fns/MatrixConst.lean | 3 +-- CvxLean/Tactic/DCP/AtomLibrary/Fns/MatrixMul.lean | 3 +-- CvxLean/Tactic/DCP/AtomLibrary/Fns/Max.lean | 3 +-- CvxLean/Tactic/DCP/AtomLibrary/Fns/MaximizeNeg.lean | 3 +-- CvxLean/Tactic/DCP/AtomLibrary/Fns/Min.lean | 3 +-- CvxLean/Tactic/DCP/AtomLibrary/Fns/Mul.lean | 3 +-- CvxLean/Tactic/DCP/AtomLibrary/Fns/MulVec.lean | 3 +-- CvxLean/Tactic/DCP/AtomLibrary/Fns/Neg.lean | 3 +-- CvxLean/Tactic/DCP/AtomLibrary/Fns/Norm.lean | 3 +-- CvxLean/Tactic/DCP/AtomLibrary/Fns/Nth.lean | 3 +-- CvxLean/Tactic/DCP/AtomLibrary/Fns/Perspective.lean | 3 +-- CvxLean/Tactic/DCP/AtomLibrary/Fns/PosSemidef.lean | 3 +-- CvxLean/Tactic/DCP/AtomLibrary/Fns/Power.lean | 3 +-- CvxLean/Tactic/DCP/AtomLibrary/Fns/QuadOverLin.lean | 3 +-- CvxLean/Tactic/DCP/AtomLibrary/Fns/SMul.lean | 3 +-- CvxLean/Tactic/DCP/AtomLibrary/Fns/Sq.lean | 3 +-- CvxLean/Tactic/DCP/AtomLibrary/Fns/Sqrt.lean | 3 +-- CvxLean/Tactic/DCP/AtomLibrary/Fns/Sub.lean | 3 +-- CvxLean/Tactic/DCP/AtomLibrary/Fns/Sum.lean | 3 +-- CvxLean/Tactic/DCP/AtomLibrary/Fns/ToUpperTri.lean | 3 +-- CvxLean/Tactic/DCP/AtomLibrary/Fns/Trace.lean | 3 +-- CvxLean/Tactic/DCP/AtomLibrary/Fns/Transpose.lean | 3 +-- CvxLean/Tactic/DCP/AtomLibrary/Fns/VecCons.lean | 3 +-- CvxLean/Tactic/DCP/AtomLibrary/Fns/VecConst.lean | 3 +-- CvxLean/Tactic/DCP/AtomLibrary/Fns/VecToMatrix.lean | 3 +-- CvxLean/Tactic/DCP/AtomLibrary/Sets/Cones.lean | 3 +-- CvxLean/Tactic/DCP/AtomLibrary/Sets/Eq.lean | 3 +-- CvxLean/Tactic/DCP/AtomLibrary/Sets/Le.lean | 3 +-- CvxLean/Tactic/PreDCP/UncheckedDCP.lean | 3 ++- 47 files changed, 47 insertions(+), 91 deletions(-) rename CvxLean/Tactic/DCP/{Atoms.lean => AtomCmd.lean} (100%) diff --git a/CvxLean/Tactic/DCP/Atoms.lean b/CvxLean/Tactic/DCP/AtomCmd.lean similarity index 100% rename from CvxLean/Tactic/DCP/Atoms.lean rename to CvxLean/Tactic/DCP/AtomCmd.lean diff --git a/CvxLean/Tactic/DCP/AtomLibrary/Fns/Abs.lean b/CvxLean/Tactic/DCP/AtomLibrary/Fns/Abs.lean index ecad63c3..4b71e87d 100644 --- a/CvxLean/Tactic/DCP/AtomLibrary/Fns/Abs.lean +++ b/CvxLean/Tactic/DCP/AtomLibrary/Fns/Abs.lean @@ -1,5 +1,4 @@ -import CvxLean.Tactic.DCP.Atoms -import CvxLean.Tactic.DCP.AtomLibrary.Sets.Cones +import CvxLean.Tactic.DCP.AtomCmdimport CvxLean.Tactic.DCP.AtomLibrary.Sets.Cones import CvxLean.Tactic.DCP.AtomLibrary.Fns.Add import CvxLean.Tactic.DCP.AtomLibrary.Fns.Sub import CvxLean.Lib.Math.Data.Matrix diff --git a/CvxLean/Tactic/DCP/AtomLibrary/Fns/Add.lean b/CvxLean/Tactic/DCP/AtomLibrary/Fns/Add.lean index d19961b6..c552055c 100644 --- a/CvxLean/Tactic/DCP/AtomLibrary/Fns/Add.lean +++ b/CvxLean/Tactic/DCP/AtomLibrary/Fns/Add.lean @@ -1,5 +1,4 @@ -import CvxLean.Tactic.DCP.Atoms -import CvxLean.Lib.Math.Data.Matrix +import CvxLean.Tactic.DCP.AtomCmdimport CvxLean.Lib.Math.Data.Matrix namespace CvxLean diff --git a/CvxLean/Tactic/DCP/AtomLibrary/Fns/CumSum.lean b/CvxLean/Tactic/DCP/AtomLibrary/Fns/CumSum.lean index 3c8149ad..c0403cd0 100644 --- a/CvxLean/Tactic/DCP/AtomLibrary/Fns/CumSum.lean +++ b/CvxLean/Tactic/DCP/AtomLibrary/Fns/CumSum.lean @@ -1,5 +1,4 @@ -import CvxLean.Tactic.DCP.Atoms -import CvxLean.Lib.Math.Data.Vec +import CvxLean.Tactic.DCP.AtomCmdimport CvxLean.Lib.Math.Data.Vec namespace CvxLean diff --git a/CvxLean/Tactic/DCP/AtomLibrary/Fns/Diag.lean b/CvxLean/Tactic/DCP/AtomLibrary/Fns/Diag.lean index 4e714f99..93128677 100644 --- a/CvxLean/Tactic/DCP/AtomLibrary/Fns/Diag.lean +++ b/CvxLean/Tactic/DCP/AtomLibrary/Fns/Diag.lean @@ -1,5 +1,4 @@ -import CvxLean.Tactic.DCP.Atoms -import CvxLean.Lib.Math.Data.Matrix +import CvxLean.Tactic.DCP.AtomCmdimport CvxLean.Lib.Math.Data.Matrix namespace CvxLean diff --git a/CvxLean/Tactic/DCP/AtomLibrary/Fns/Diagonal.lean b/CvxLean/Tactic/DCP/AtomLibrary/Fns/Diagonal.lean index 102b7d97..4626ac43 100644 --- a/CvxLean/Tactic/DCP/AtomLibrary/Fns/Diagonal.lean +++ b/CvxLean/Tactic/DCP/AtomLibrary/Fns/Diagonal.lean @@ -1,5 +1,4 @@ -import CvxLean.Tactic.DCP.Atoms -import CvxLean.Lib.Math.Data.Matrix +import CvxLean.Tactic.DCP.AtomCmdimport CvxLean.Lib.Math.Data.Matrix namespace CvxLean diff --git a/CvxLean/Tactic/DCP/AtomLibrary/Fns/Div.lean b/CvxLean/Tactic/DCP/AtomLibrary/Fns/Div.lean index e2371a19..888c7717 100644 --- a/CvxLean/Tactic/DCP/AtomLibrary/Fns/Div.lean +++ b/CvxLean/Tactic/DCP/AtomLibrary/Fns/Div.lean @@ -1,5 +1,4 @@ -import CvxLean.Tactic.DCP.Atoms - +import CvxLean.Tactic.DCP.AtomCmd namespace CvxLean open Real diff --git a/CvxLean/Tactic/DCP/AtomLibrary/Fns/DotProduct.lean b/CvxLean/Tactic/DCP/AtomLibrary/Fns/DotProduct.lean index 74262cdf..9bdc2b71 100644 --- a/CvxLean/Tactic/DCP/AtomLibrary/Fns/DotProduct.lean +++ b/CvxLean/Tactic/DCP/AtomLibrary/Fns/DotProduct.lean @@ -1,5 +1,4 @@ -import CvxLean.Tactic.DCP.Atoms - +import CvxLean.Tactic.DCP.AtomCmd namespace CvxLean declare_atom Vec.dotProduct1 [affine] (m : Nat)& (x : Fin m → ℝ)& (y : Fin m → ℝ)? : Matrix.dotProduct x y := diff --git a/CvxLean/Tactic/DCP/AtomLibrary/Fns/Entr.lean b/CvxLean/Tactic/DCP/AtomLibrary/Fns/Entr.lean index 3ad37997..9a958da6 100644 --- a/CvxLean/Tactic/DCP/AtomLibrary/Fns/Entr.lean +++ b/CvxLean/Tactic/DCP/AtomLibrary/Fns/Entr.lean @@ -1,5 +1,4 @@ -import CvxLean.Tactic.DCP.Atoms -import CvxLean.Tactic.DCP.AtomLibrary.Sets.Cones +import CvxLean.Tactic.DCP.AtomCmdimport CvxLean.Tactic.DCP.AtomLibrary.Sets.Cones import CvxLean.Lib.Math.Data.Real import CvxLean.Lib.Math.Data.Vec diff --git a/CvxLean/Tactic/DCP/AtomLibrary/Fns/Exp.lean b/CvxLean/Tactic/DCP/AtomLibrary/Fns/Exp.lean index 2e15d69e..0a850d1b 100644 --- a/CvxLean/Tactic/DCP/AtomLibrary/Fns/Exp.lean +++ b/CvxLean/Tactic/DCP/AtomLibrary/Fns/Exp.lean @@ -1,5 +1,4 @@ -import CvxLean.Tactic.DCP.Atoms -import CvxLean.Tactic.DCP.AtomLibrary.Sets.Cones +import CvxLean.Tactic.DCP.AtomCmdimport CvxLean.Tactic.DCP.AtomLibrary.Sets.Cones import CvxLean.Lib.Math.Data.Vec namespace CvxLean diff --git a/CvxLean/Tactic/DCP/AtomLibrary/Fns/FromBlocks.lean b/CvxLean/Tactic/DCP/AtomLibrary/Fns/FromBlocks.lean index 975915e6..eaaa34f3 100644 --- a/CvxLean/Tactic/DCP/AtomLibrary/Fns/FromBlocks.lean +++ b/CvxLean/Tactic/DCP/AtomLibrary/Fns/FromBlocks.lean @@ -1,5 +1,4 @@ -import CvxLean.Tactic.DCP.Atoms -import CvxLean.Lib.Math.Data.Matrix +import CvxLean.Tactic.DCP.AtomCmdimport CvxLean.Lib.Math.Data.Matrix namespace CvxLean diff --git a/CvxLean/Tactic/DCP/AtomLibrary/Fns/GeoMean.lean b/CvxLean/Tactic/DCP/AtomLibrary/Fns/GeoMean.lean index 66ba3710..f765a2e5 100644 --- a/CvxLean/Tactic/DCP/AtomLibrary/Fns/GeoMean.lean +++ b/CvxLean/Tactic/DCP/AtomLibrary/Fns/GeoMean.lean @@ -1,5 +1,4 @@ -import CvxLean.Tactic.DCP.Atoms -import CvxLean.Tactic.DCP.AtomLibrary.Sets.Cones +import CvxLean.Tactic.DCP.AtomCmdimport CvxLean.Tactic.DCP.AtomLibrary.Sets.Cones import CvxLean.Tactic.DCP.AtomLibrary.Sets.Le import CvxLean.Tactic.DCP.AtomLibrary.Fns.VecCons import CvxLean.Tactic.DCP.AtomLibrary.Fns.Add diff --git a/CvxLean/Tactic/DCP/AtomLibrary/Fns/Huber.lean b/CvxLean/Tactic/DCP/AtomLibrary/Fns/Huber.lean index cdd88602..e05ee935 100644 --- a/CvxLean/Tactic/DCP/AtomLibrary/Fns/Huber.lean +++ b/CvxLean/Tactic/DCP/AtomLibrary/Fns/Huber.lean @@ -1,5 +1,4 @@ -import CvxLean.Tactic.DCP.Atoms -import CvxLean.Tactic.DCP.AtomLibrary.Sets.Cones +import CvxLean.Tactic.DCP.AtomCmdimport CvxLean.Tactic.DCP.AtomLibrary.Sets.Cones import CvxLean.Tactic.DCP.AtomLibrary.Sets.Le import CvxLean.Tactic.DCP.AtomLibrary.Sets.Eq import CvxLean.Tactic.DCP.AtomLibrary.Fns.Sq diff --git a/CvxLean/Tactic/DCP/AtomLibrary/Fns/Inv.lean b/CvxLean/Tactic/DCP/AtomLibrary/Fns/Inv.lean index c7b524f0..3351b2da 100644 --- a/CvxLean/Tactic/DCP/AtomLibrary/Fns/Inv.lean +++ b/CvxLean/Tactic/DCP/AtomLibrary/Fns/Inv.lean @@ -1,5 +1,4 @@ -import CvxLean.Tactic.DCP.Atoms -import CvxLean.Tactic.DCP.AtomLibrary.Sets.Cones +import CvxLean.Tactic.DCP.AtomCmdimport CvxLean.Tactic.DCP.AtomLibrary.Sets.Cones import CvxLean.Tactic.DCP.AtomLibrary.Sets.Le import CvxLean.Tactic.DCP.AtomLibrary.Fns.VecCons import CvxLean.Tactic.DCP.AtomLibrary.Fns.Add diff --git a/CvxLean/Tactic/DCP/AtomLibrary/Fns/KLDiv.lean b/CvxLean/Tactic/DCP/AtomLibrary/Fns/KLDiv.lean index c877534d..05758ce2 100644 --- a/CvxLean/Tactic/DCP/AtomLibrary/Fns/KLDiv.lean +++ b/CvxLean/Tactic/DCP/AtomLibrary/Fns/KLDiv.lean @@ -1,5 +1,4 @@ -import CvxLean.Tactic.DCP.Atoms -import CvxLean.Tactic.DCP.AtomLibrary.Sets.Cones +import CvxLean.Tactic.DCP.AtomCmdimport CvxLean.Tactic.DCP.AtomLibrary.Sets.Cones import CvxLean.Tactic.DCP.AtomLibrary.Sets.Le import CvxLean.Tactic.DCP.AtomLibrary.Fns.Exp import CvxLean.Tactic.DCP.AtomLibrary.Fns.Sub diff --git a/CvxLean/Tactic/DCP/AtomLibrary/Fns/Log.lean b/CvxLean/Tactic/DCP/AtomLibrary/Fns/Log.lean index 05acde8e..d697b79a 100644 --- a/CvxLean/Tactic/DCP/AtomLibrary/Fns/Log.lean +++ b/CvxLean/Tactic/DCP/AtomLibrary/Fns/Log.lean @@ -1,5 +1,4 @@ -import CvxLean.Tactic.DCP.Atoms -import CvxLean.Tactic.DCP.AtomLibrary.Sets.Cones +import CvxLean.Tactic.DCP.AtomCmdimport CvxLean.Tactic.DCP.AtomLibrary.Sets.Cones import CvxLean.Lib.Math.Data.Vec namespace CvxLean diff --git a/CvxLean/Tactic/DCP/AtomLibrary/Fns/LogDet.lean b/CvxLean/Tactic/DCP/AtomLibrary/Fns/LogDet.lean index 08697222..389abcbe 100644 --- a/CvxLean/Tactic/DCP/AtomLibrary/Fns/LogDet.lean +++ b/CvxLean/Tactic/DCP/AtomLibrary/Fns/LogDet.lean @@ -1,5 +1,4 @@ -import CvxLean.Tactic.DCP.Atoms -import CvxLean.Tactic.DCP.AtomLibrary.Sets.Cones +import CvxLean.Tactic.DCP.AtomCmdimport CvxLean.Tactic.DCP.AtomLibrary.Sets.Cones import CvxLean.Tactic.DCP.AtomLibrary.Fns.Sum import CvxLean.Tactic.DCP.AtomLibrary.Fns.PosSemidef import CvxLean.Tactic.DCP.AtomLibrary.Fns.FromBlocks diff --git a/CvxLean/Tactic/DCP/AtomLibrary/Fns/LogSumExp.lean b/CvxLean/Tactic/DCP/AtomLibrary/Fns/LogSumExp.lean index 40d48873..05e06184 100644 --- a/CvxLean/Tactic/DCP/AtomLibrary/Fns/LogSumExp.lean +++ b/CvxLean/Tactic/DCP/AtomLibrary/Fns/LogSumExp.lean @@ -1,5 +1,4 @@ -import CvxLean.Tactic.DCP.Atoms -import CvxLean.Tactic.DCP.AtomLibrary.Sets.Cones +import CvxLean.Tactic.DCP.AtomCmdimport CvxLean.Tactic.DCP.AtomLibrary.Sets.Cones import CvxLean.Tactic.DCP.AtomLibrary.Sets.Le import CvxLean.Tactic.DCP.AtomLibrary.Fns.Exp import CvxLean.Tactic.DCP.AtomLibrary.Fns.Log diff --git a/CvxLean/Tactic/DCP/AtomLibrary/Fns/MatrixConst.lean b/CvxLean/Tactic/DCP/AtomLibrary/Fns/MatrixConst.lean index 365c7f38..6f190f87 100644 --- a/CvxLean/Tactic/DCP/AtomLibrary/Fns/MatrixConst.lean +++ b/CvxLean/Tactic/DCP/AtomLibrary/Fns/MatrixConst.lean @@ -1,5 +1,4 @@ -import CvxLean.Tactic.DCP.Atoms -import CvxLean.Lib.Math.Data.Matrix +import CvxLean.Tactic.DCP.AtomCmdimport CvxLean.Lib.Math.Data.Matrix namespace CvxLean diff --git a/CvxLean/Tactic/DCP/AtomLibrary/Fns/MatrixMul.lean b/CvxLean/Tactic/DCP/AtomLibrary/Fns/MatrixMul.lean index 8009bd57..27de7a18 100644 --- a/CvxLean/Tactic/DCP/AtomLibrary/Fns/MatrixMul.lean +++ b/CvxLean/Tactic/DCP/AtomLibrary/Fns/MatrixMul.lean @@ -1,5 +1,4 @@ -import CvxLean.Tactic.DCP.Atoms -import CvxLean.Lib.Math.Data.Matrix +import CvxLean.Tactic.DCP.AtomCmdimport CvxLean.Lib.Math.Data.Matrix namespace CvxLean diff --git a/CvxLean/Tactic/DCP/AtomLibrary/Fns/Max.lean b/CvxLean/Tactic/DCP/AtomLibrary/Fns/Max.lean index 089ed043..37868698 100644 --- a/CvxLean/Tactic/DCP/AtomLibrary/Fns/Max.lean +++ b/CvxLean/Tactic/DCP/AtomLibrary/Fns/Max.lean @@ -1,5 +1,4 @@ -import CvxLean.Tactic.DCP.Atoms -import CvxLean.Tactic.DCP.AtomLibrary.Sets.Le +import CvxLean.Tactic.DCP.AtomCmdimport CvxLean.Tactic.DCP.AtomLibrary.Sets.Le import CvxLean.Lib.Math.Data.Vec namespace CvxLean diff --git a/CvxLean/Tactic/DCP/AtomLibrary/Fns/MaximizeNeg.lean b/CvxLean/Tactic/DCP/AtomLibrary/Fns/MaximizeNeg.lean index 8df0d840..74ecc8b8 100644 --- a/CvxLean/Tactic/DCP/AtomLibrary/Fns/MaximizeNeg.lean +++ b/CvxLean/Tactic/DCP/AtomLibrary/Fns/MaximizeNeg.lean @@ -1,5 +1,4 @@ -import CvxLean.Tactic.DCP.Atoms - +import CvxLean.Tactic.DCP.AtomCmd namespace CvxLean declare_atom maximizeNeg [affine] (x : ℝ)- : maximizeNeg x := diff --git a/CvxLean/Tactic/DCP/AtomLibrary/Fns/Min.lean b/CvxLean/Tactic/DCP/AtomLibrary/Fns/Min.lean index 8f7a04c6..47e896cd 100644 --- a/CvxLean/Tactic/DCP/AtomLibrary/Fns/Min.lean +++ b/CvxLean/Tactic/DCP/AtomLibrary/Fns/Min.lean @@ -1,5 +1,4 @@ -import CvxLean.Tactic.DCP.Atoms -import CvxLean.Tactic.DCP.AtomLibrary.Sets.Le +import CvxLean.Tactic.DCP.AtomCmdimport CvxLean.Tactic.DCP.AtomLibrary.Sets.Le import CvxLean.Lib.Math.Data.Vec namespace CvxLean diff --git a/CvxLean/Tactic/DCP/AtomLibrary/Fns/Mul.lean b/CvxLean/Tactic/DCP/AtomLibrary/Fns/Mul.lean index 4e22f433..a16929f2 100644 --- a/CvxLean/Tactic/DCP/AtomLibrary/Fns/Mul.lean +++ b/CvxLean/Tactic/DCP/AtomLibrary/Fns/Mul.lean @@ -1,5 +1,4 @@ -import CvxLean.Tactic.DCP.Atoms - +import CvxLean.Tactic.DCP.AtomCmd namespace CvxLean declare_atom mul1 [affine] (x : ℝ)& (y : ℝ)+ : x * y := diff --git a/CvxLean/Tactic/DCP/AtomLibrary/Fns/MulVec.lean b/CvxLean/Tactic/DCP/AtomLibrary/Fns/MulVec.lean index 19716672..88412ea4 100644 --- a/CvxLean/Tactic/DCP/AtomLibrary/Fns/MulVec.lean +++ b/CvxLean/Tactic/DCP/AtomLibrary/Fns/MulVec.lean @@ -1,5 +1,4 @@ -import CvxLean.Tactic.DCP.Atoms - +import CvxLean.Tactic.DCP.AtomCmd namespace CvxLean declare_atom Matrix.mulVec [affine] (n : ℕ)& (m : ℕ)& diff --git a/CvxLean/Tactic/DCP/AtomLibrary/Fns/Neg.lean b/CvxLean/Tactic/DCP/AtomLibrary/Fns/Neg.lean index bb6dcfa7..6fa055c7 100644 --- a/CvxLean/Tactic/DCP/AtomLibrary/Fns/Neg.lean +++ b/CvxLean/Tactic/DCP/AtomLibrary/Fns/Neg.lean @@ -1,5 +1,4 @@ -import CvxLean.Tactic.DCP.Atoms - +import CvxLean.Tactic.DCP.AtomCmd namespace CvxLean declare_atom neg [affine] (x : ℝ)- : - x := diff --git a/CvxLean/Tactic/DCP/AtomLibrary/Fns/Norm.lean b/CvxLean/Tactic/DCP/AtomLibrary/Fns/Norm.lean index 3a519656..dee19779 100644 --- a/CvxLean/Tactic/DCP/AtomLibrary/Fns/Norm.lean +++ b/CvxLean/Tactic/DCP/AtomLibrary/Fns/Norm.lean @@ -1,5 +1,4 @@ -import CvxLean.Tactic.DCP.Atoms -import CvxLean.Tactic.DCP.AtomLibrary.Sets.Cones +import CvxLean.Tactic.DCP.AtomCmdimport CvxLean.Tactic.DCP.AtomLibrary.Sets.Cones import CvxLean.Tactic.DCP.AtomLibrary.Fns.VecCons import CvxLean.Lib.Math.Data.Vec diff --git a/CvxLean/Tactic/DCP/AtomLibrary/Fns/Nth.lean b/CvxLean/Tactic/DCP/AtomLibrary/Fns/Nth.lean index fe76717b..77ffb74f 100644 --- a/CvxLean/Tactic/DCP/AtomLibrary/Fns/Nth.lean +++ b/CvxLean/Tactic/DCP/AtomLibrary/Fns/Nth.lean @@ -1,5 +1,4 @@ -import CvxLean.Tactic.DCP.Atoms - +import CvxLean.Tactic.DCP.AtomCmd namespace CvxLean declare_atom Vec.nth [affine] (m : Nat)& (x : Fin m → ℝ)? (i : Fin m)& : x i := diff --git a/CvxLean/Tactic/DCP/AtomLibrary/Fns/Perspective.lean b/CvxLean/Tactic/DCP/AtomLibrary/Fns/Perspective.lean index cf2dc97f..c9e1b9d7 100644 --- a/CvxLean/Tactic/DCP/AtomLibrary/Fns/Perspective.lean +++ b/CvxLean/Tactic/DCP/AtomLibrary/Fns/Perspective.lean @@ -1,5 +1,4 @@ -import CvxLean.Tactic.DCP.Atoms -import CvxLean.Tactic.DCP.AtomLibrary.Sets.Cones +import CvxLean.Tactic.DCP.AtomCmdimport CvxLean.Tactic.DCP.AtomLibrary.Sets.Cones namespace CvxLean diff --git a/CvxLean/Tactic/DCP/AtomLibrary/Fns/PosSemidef.lean b/CvxLean/Tactic/DCP/AtomLibrary/Fns/PosSemidef.lean index 810fd183..9c0f9074 100644 --- a/CvxLean/Tactic/DCP/AtomLibrary/Fns/PosSemidef.lean +++ b/CvxLean/Tactic/DCP/AtomLibrary/Fns/PosSemidef.lean @@ -1,5 +1,4 @@ -import CvxLean.Tactic.DCP.Atoms -import CvxLean.Tactic.DCP.AtomLibrary.Sets.Cones +import CvxLean.Tactic.DCP.AtomCmdimport CvxLean.Tactic.DCP.AtomLibrary.Sets.Cones namespace CvxLean diff --git a/CvxLean/Tactic/DCP/AtomLibrary/Fns/Power.lean b/CvxLean/Tactic/DCP/AtomLibrary/Fns/Power.lean index 9fe3b499..48593e49 100644 --- a/CvxLean/Tactic/DCP/AtomLibrary/Fns/Power.lean +++ b/CvxLean/Tactic/DCP/AtomLibrary/Fns/Power.lean @@ -1,5 +1,4 @@ -import CvxLean.Tactic.DCP.Atoms -import CvxLean.Tactic.DCP.AtomLibrary.Sets.Cones +import CvxLean.Tactic.DCP.AtomCmdimport CvxLean.Tactic.DCP.AtomLibrary.Sets.Cones import CvxLean.Tactic.DCP.AtomLibrary.Sets.Le import CvxLean.Tactic.DCP.AtomLibrary.Fns.VecCons import CvxLean.Tactic.DCP.AtomLibrary.Fns.Add diff --git a/CvxLean/Tactic/DCP/AtomLibrary/Fns/QuadOverLin.lean b/CvxLean/Tactic/DCP/AtomLibrary/Fns/QuadOverLin.lean index 40e1ced8..5987408a 100644 --- a/CvxLean/Tactic/DCP/AtomLibrary/Fns/QuadOverLin.lean +++ b/CvxLean/Tactic/DCP/AtomLibrary/Fns/QuadOverLin.lean @@ -1,5 +1,4 @@ -import CvxLean.Tactic.DCP.Atoms -import CvxLean.Tactic.DCP.AtomLibrary.Sets.Cones +import CvxLean.Tactic.DCP.AtomCmdimport CvxLean.Tactic.DCP.AtomLibrary.Sets.Cones import CvxLean.Tactic.DCP.AtomLibrary.Sets.Le import CvxLean.Tactic.DCP.AtomLibrary.Fns.VecCons import CvxLean.Tactic.DCP.AtomLibrary.Fns.Add diff --git a/CvxLean/Tactic/DCP/AtomLibrary/Fns/SMul.lean b/CvxLean/Tactic/DCP/AtomLibrary/Fns/SMul.lean index 76bc399f..03b21e49 100644 --- a/CvxLean/Tactic/DCP/AtomLibrary/Fns/SMul.lean +++ b/CvxLean/Tactic/DCP/AtomLibrary/Fns/SMul.lean @@ -1,5 +1,4 @@ -import CvxLean.Tactic.DCP.Atoms - +import CvxLean.Tactic.DCP.AtomCmd namespace CvxLean declare_atom Nat.smul [affine] (n : ℕ)& (x : ℝ)+ : diff --git a/CvxLean/Tactic/DCP/AtomLibrary/Fns/Sq.lean b/CvxLean/Tactic/DCP/AtomLibrary/Fns/Sq.lean index 35e53edf..d08cd9e8 100644 --- a/CvxLean/Tactic/DCP/AtomLibrary/Fns/Sq.lean +++ b/CvxLean/Tactic/DCP/AtomLibrary/Fns/Sq.lean @@ -1,5 +1,4 @@ -import CvxLean.Tactic.DCP.Atoms -import CvxLean.Tactic.DCP.AtomLibrary.Sets.Cones +import CvxLean.Tactic.DCP.AtomCmdimport CvxLean.Tactic.DCP.AtomLibrary.Sets.Cones import CvxLean.Tactic.DCP.AtomLibrary.Fns.VecCons import CvxLean.Tactic.DCP.AtomLibrary.Fns.VecToMatrix diff --git a/CvxLean/Tactic/DCP/AtomLibrary/Fns/Sqrt.lean b/CvxLean/Tactic/DCP/AtomLibrary/Fns/Sqrt.lean index 8bfa27eb..1b31d8af 100644 --- a/CvxLean/Tactic/DCP/AtomLibrary/Fns/Sqrt.lean +++ b/CvxLean/Tactic/DCP/AtomLibrary/Fns/Sqrt.lean @@ -1,5 +1,4 @@ -import CvxLean.Tactic.DCP.Atoms -import CvxLean.Tactic.DCP.AtomLibrary.Sets.Cones +import CvxLean.Tactic.DCP.AtomCmdimport CvxLean.Tactic.DCP.AtomLibrary.Sets.Cones import CvxLean.Tactic.DCP.AtomLibrary.Fns.VecCons namespace CvxLean diff --git a/CvxLean/Tactic/DCP/AtomLibrary/Fns/Sub.lean b/CvxLean/Tactic/DCP/AtomLibrary/Fns/Sub.lean index 134fb5b9..06e5d576 100644 --- a/CvxLean/Tactic/DCP/AtomLibrary/Fns/Sub.lean +++ b/CvxLean/Tactic/DCP/AtomLibrary/Fns/Sub.lean @@ -1,5 +1,4 @@ -import CvxLean.Tactic.DCP.Atoms -import CvxLean.Lib.Math.Data.Matrix +import CvxLean.Tactic.DCP.AtomCmdimport CvxLean.Lib.Math.Data.Matrix namespace CvxLean diff --git a/CvxLean/Tactic/DCP/AtomLibrary/Fns/Sum.lean b/CvxLean/Tactic/DCP/AtomLibrary/Fns/Sum.lean index 5f6a4ea6..146e967f 100644 --- a/CvxLean/Tactic/DCP/AtomLibrary/Fns/Sum.lean +++ b/CvxLean/Tactic/DCP/AtomLibrary/Fns/Sum.lean @@ -1,5 +1,4 @@ -import CvxLean.Tactic.DCP.Atoms -import CvxLean.Lib.Math.Data.Vec +import CvxLean.Tactic.DCP.AtomCmdimport CvxLean.Lib.Math.Data.Vec import CvxLean.Lib.Math.Data.Matrix namespace CvxLean diff --git a/CvxLean/Tactic/DCP/AtomLibrary/Fns/ToUpperTri.lean b/CvxLean/Tactic/DCP/AtomLibrary/Fns/ToUpperTri.lean index 4ce6eb95..b2c63cec 100644 --- a/CvxLean/Tactic/DCP/AtomLibrary/Fns/ToUpperTri.lean +++ b/CvxLean/Tactic/DCP/AtomLibrary/Fns/ToUpperTri.lean @@ -1,5 +1,4 @@ -import CvxLean.Tactic.DCP.Atoms -import CvxLean.Lib.Math.Data.Matrix +import CvxLean.Tactic.DCP.AtomCmdimport CvxLean.Lib.Math.Data.Matrix import CvxLean.Lib.Math.LinearAlgebra.Matrix.ToUpperTri namespace CvxLean diff --git a/CvxLean/Tactic/DCP/AtomLibrary/Fns/Trace.lean b/CvxLean/Tactic/DCP/AtomLibrary/Fns/Trace.lean index ec0e2be2..34afaff9 100644 --- a/CvxLean/Tactic/DCP/AtomLibrary/Fns/Trace.lean +++ b/CvxLean/Tactic/DCP/AtomLibrary/Fns/Trace.lean @@ -1,5 +1,4 @@ -import CvxLean.Tactic.DCP.Atoms -import CvxLean.Lib.Math.Data.Matrix +import CvxLean.Tactic.DCP.AtomCmdimport CvxLean.Lib.Math.Data.Matrix namespace CvxLean diff --git a/CvxLean/Tactic/DCP/AtomLibrary/Fns/Transpose.lean b/CvxLean/Tactic/DCP/AtomLibrary/Fns/Transpose.lean index 2c13c947..a44f9824 100644 --- a/CvxLean/Tactic/DCP/AtomLibrary/Fns/Transpose.lean +++ b/CvxLean/Tactic/DCP/AtomLibrary/Fns/Transpose.lean @@ -1,5 +1,4 @@ -import CvxLean.Tactic.DCP.Atoms -import CvxLean.Lib.Math.Data.Matrix +import CvxLean.Tactic.DCP.AtomCmdimport CvxLean.Lib.Math.Data.Matrix namespace CvxLean diff --git a/CvxLean/Tactic/DCP/AtomLibrary/Fns/VecCons.lean b/CvxLean/Tactic/DCP/AtomLibrary/Fns/VecCons.lean index 74a6ede9..114101ef 100644 --- a/CvxLean/Tactic/DCP/AtomLibrary/Fns/VecCons.lean +++ b/CvxLean/Tactic/DCP/AtomLibrary/Fns/VecCons.lean @@ -1,5 +1,4 @@ -import CvxLean.Tactic.DCP.Atoms -import CvxLean.Lib.Math.Data.Matrix +import CvxLean.Tactic.DCP.AtomCmdimport CvxLean.Lib.Math.Data.Matrix namespace CvxLean diff --git a/CvxLean/Tactic/DCP/AtomLibrary/Fns/VecConst.lean b/CvxLean/Tactic/DCP/AtomLibrary/Fns/VecConst.lean index bd6708d4..a08c9f29 100644 --- a/CvxLean/Tactic/DCP/AtomLibrary/Fns/VecConst.lean +++ b/CvxLean/Tactic/DCP/AtomLibrary/Fns/VecConst.lean @@ -1,5 +1,4 @@ -import CvxLean.Tactic.DCP.Atoms -import CvxLean.Lib.Math.Data.Vec +import CvxLean.Tactic.DCP.AtomCmdimport CvxLean.Lib.Math.Data.Vec namespace CvxLean diff --git a/CvxLean/Tactic/DCP/AtomLibrary/Fns/VecToMatrix.lean b/CvxLean/Tactic/DCP/AtomLibrary/Fns/VecToMatrix.lean index 72c0ff0f..0bb870ac 100644 --- a/CvxLean/Tactic/DCP/AtomLibrary/Fns/VecToMatrix.lean +++ b/CvxLean/Tactic/DCP/AtomLibrary/Fns/VecToMatrix.lean @@ -1,5 +1,4 @@ -import CvxLean.Tactic.DCP.Atoms -import CvxLean.Lib.Math.Data.Vec +import CvxLean.Tactic.DCP.AtomCmdimport CvxLean.Lib.Math.Data.Vec import CvxLean.Lib.Math.Data.Matrix namespace CvxLean diff --git a/CvxLean/Tactic/DCP/AtomLibrary/Sets/Cones.lean b/CvxLean/Tactic/DCP/AtomLibrary/Sets/Cones.lean index a7e7d569..c7202035 100644 --- a/CvxLean/Tactic/DCP/AtomLibrary/Sets/Cones.lean +++ b/CvxLean/Tactic/DCP/AtomLibrary/Sets/Cones.lean @@ -1,5 +1,4 @@ -import CvxLean.Tactic.DCP.Atoms -import CvxLean.Lib.Cones.All +import CvxLean.Tactic.DCP.AtomCmdimport CvxLean.Lib.Cones.All import CvxLean.Syntax.Minimization namespace CvxLean diff --git a/CvxLean/Tactic/DCP/AtomLibrary/Sets/Eq.lean b/CvxLean/Tactic/DCP/AtomLibrary/Sets/Eq.lean index 737d605f..ff81113f 100644 --- a/CvxLean/Tactic/DCP/AtomLibrary/Sets/Eq.lean +++ b/CvxLean/Tactic/DCP/AtomLibrary/Sets/Eq.lean @@ -1,5 +1,4 @@ -import CvxLean.Tactic.DCP.Atoms -import CvxLean.Tactic.DCP.AtomLibrary.Sets.Cones +import CvxLean.Tactic.DCP.AtomCmdimport CvxLean.Tactic.DCP.AtomLibrary.Sets.Cones import CvxLean.Tactic.DCP.AtomLibrary.Fns.Sub namespace CvxLean diff --git a/CvxLean/Tactic/DCP/AtomLibrary/Sets/Le.lean b/CvxLean/Tactic/DCP/AtomLibrary/Sets/Le.lean index 0129c9a6..938fbdda 100644 --- a/CvxLean/Tactic/DCP/AtomLibrary/Sets/Le.lean +++ b/CvxLean/Tactic/DCP/AtomLibrary/Sets/Le.lean @@ -1,5 +1,4 @@ -import CvxLean.Tactic.DCP.Atoms -import CvxLean.Tactic.DCP.AtomLibrary.Sets.Cones +import CvxLean.Tactic.DCP.AtomCmdimport CvxLean.Tactic.DCP.AtomLibrary.Sets.Cones import CvxLean.Tactic.DCP.AtomLibrary.Fns.Sub namespace CvxLean diff --git a/CvxLean/Tactic/PreDCP/UncheckedDCP.lean b/CvxLean/Tactic/PreDCP/UncheckedDCP.lean index c5200d03..65705102 100644 --- a/CvxLean/Tactic/PreDCP/UncheckedDCP.lean +++ b/CvxLean/Tactic/PreDCP/UncheckedDCP.lean @@ -1,5 +1,6 @@ import CvxLean.Syntax.OptimizationParam import CvxLean.Meta.Util.Expr +import CvxLean.Meta.Util.Error import CvxLean.Tactic.DCP.DCP namespace CvxLean @@ -119,7 +120,7 @@ def uncheckedTreeFromMinimizationExpr (goalExprs : MinimizationExpr) : -- If `mkUncheckedTree` gives any `none` then we throw an error. let tree ← tree.mapM (fun o => match o with | some (n, t) => return (n, t) - | none => throwError "`pre_dcp` error: could not create unchecked DCP tree.") + | none => throwPreDCPError "could not create unchecked DCP tree.") return tree end UncheckedDCP From 37ee436fba4267ef112b570ee1f676377741775d Mon Sep 17 00:00:00 2001 From: Ramon Fernandez Mir Date: Thu, 29 Feb 2024 16:29:54 +0000 Subject: [PATCH 11/25] fix: line breaks in imports from refactor --- CvxLean/Tactic/DCP/AtomCmd.lean | 23 +++++++++++++------ CvxLean/Tactic/DCP/AtomLibrary/Fns/Abs.lean | 3 ++- CvxLean/Tactic/DCP/AtomLibrary/Fns/Add.lean | 3 ++- .../Tactic/DCP/AtomLibrary/Fns/CumSum.lean | 3 ++- CvxLean/Tactic/DCP/AtomLibrary/Fns/Diag.lean | 3 ++- .../Tactic/DCP/AtomLibrary/Fns/Diagonal.lean | 3 ++- CvxLean/Tactic/DCP/AtomLibrary/Fns/Div.lean | 1 + .../DCP/AtomLibrary/Fns/DotProduct.lean | 1 + CvxLean/Tactic/DCP/AtomLibrary/Fns/Entr.lean | 3 ++- CvxLean/Tactic/DCP/AtomLibrary/Fns/Exp.lean | 3 ++- .../DCP/AtomLibrary/Fns/FromBlocks.lean | 3 ++- .../Tactic/DCP/AtomLibrary/Fns/GeoMean.lean | 3 ++- CvxLean/Tactic/DCP/AtomLibrary/Fns/Huber.lean | 3 ++- CvxLean/Tactic/DCP/AtomLibrary/Fns/Inv.lean | 3 ++- CvxLean/Tactic/DCP/AtomLibrary/Fns/KLDiv.lean | 3 ++- CvxLean/Tactic/DCP/AtomLibrary/Fns/Log.lean | 3 ++- .../Tactic/DCP/AtomLibrary/Fns/LogDet.lean | 3 ++- .../Tactic/DCP/AtomLibrary/Fns/LogSumExp.lean | 3 ++- .../DCP/AtomLibrary/Fns/MatrixConst.lean | 3 ++- .../Tactic/DCP/AtomLibrary/Fns/MatrixMul.lean | 3 ++- CvxLean/Tactic/DCP/AtomLibrary/Fns/Max.lean | 3 ++- .../DCP/AtomLibrary/Fns/MaximizeNeg.lean | 1 + CvxLean/Tactic/DCP/AtomLibrary/Fns/Min.lean | 3 ++- CvxLean/Tactic/DCP/AtomLibrary/Fns/Mul.lean | 1 + .../Tactic/DCP/AtomLibrary/Fns/MulVec.lean | 1 + CvxLean/Tactic/DCP/AtomLibrary/Fns/Neg.lean | 1 + CvxLean/Tactic/DCP/AtomLibrary/Fns/Norm.lean | 3 ++- CvxLean/Tactic/DCP/AtomLibrary/Fns/Nth.lean | 1 + .../DCP/AtomLibrary/Fns/Perspective.lean | 3 ++- .../DCP/AtomLibrary/Fns/PosSemidef.lean | 3 ++- CvxLean/Tactic/DCP/AtomLibrary/Fns/Power.lean | 3 ++- .../DCP/AtomLibrary/Fns/QuadOverLin.lean | 3 ++- CvxLean/Tactic/DCP/AtomLibrary/Fns/SMul.lean | 1 + CvxLean/Tactic/DCP/AtomLibrary/Fns/Sq.lean | 3 ++- CvxLean/Tactic/DCP/AtomLibrary/Fns/Sqrt.lean | 3 ++- CvxLean/Tactic/DCP/AtomLibrary/Fns/Sub.lean | 3 ++- CvxLean/Tactic/DCP/AtomLibrary/Fns/Sum.lean | 3 ++- .../DCP/AtomLibrary/Fns/ToUpperTri.lean | 3 ++- CvxLean/Tactic/DCP/AtomLibrary/Fns/Trace.lean | 3 ++- .../Tactic/DCP/AtomLibrary/Fns/Transpose.lean | 3 ++- .../Tactic/DCP/AtomLibrary/Fns/VecCons.lean | 3 ++- .../Tactic/DCP/AtomLibrary/Fns/VecConst.lean | 3 ++- .../DCP/AtomLibrary/Fns/VecToMatrix.lean | 3 ++- .../Tactic/DCP/AtomLibrary/Sets/Cones.lean | 3 ++- CvxLean/Tactic/DCP/AtomLibrary/Sets/Eq.lean | 3 ++- CvxLean/Tactic/DCP/AtomLibrary/Sets/Le.lean | 3 ++- 46 files changed, 98 insertions(+), 44 deletions(-) diff --git a/CvxLean/Tactic/DCP/AtomCmd.lean b/CvxLean/Tactic/DCP/AtomCmd.lean index 50f775ff..c9e89487 100644 --- a/CvxLean/Tactic/DCP/AtomCmd.lean +++ b/CvxLean/Tactic/DCP/AtomCmd.lean @@ -5,22 +5,29 @@ import CvxLean.Tactic.DCP.AtomSyntax import CvxLean.Lib.Math.Data.Real import CvxLean.Tactic.DCP.DCP +/-! +# Atom library (command) + + +-/ + namespace CvxLean open Lean Expr Meta Elab Command -/-- -/ +/-- Given expressions `e₁, ..., eₙ` return `(And.intro e₁ ⋯ (And.intro eₙ₋₁ eₙ) ⋯)`, i.e., `∧` them, +with associativity to the right. -/ def mkAndIntro (xs : Array Expr) : MetaM Expr := do - let mut res := xs[xs.size-1]! - for i in [:xs.size-1] do - res ← mkAppM ``And.intro #[xs[xs.size-2-i]!, res] + let mut res := xs[xs.size - 1]! + for i in [:xs.size - 1] do + res ← mkAppM ``And.intro #[xs[xs.size - 2 - i]!, res] return res /-- -/ def mkExistsFVars (xs : Array Expr) (e : Expr) : MetaM Expr := do let mut res := e for i in [:xs.size] do - let x := xs[xs.size-i-1]! + let x := xs[xs.size - i - 1]! res ← mkAppM ``Exists #[← mkLambdaFVars #[x] res] return res @@ -29,12 +36,14 @@ def mkExistsIntro (xs : Array Expr) (e : Expr) : MetaM Expr := do let mut res := e for i in [:xs.size] do let x := xs[xs.size-i-1]! - res ← mkAppOptM ``Exists.intro #[none, some $ ← mkLambdaFVars #[x] (← inferType res), some x, some res] + res ← mkAppOptM ``Exists.intro + #[none, some <| ← mkLambdaFVars #[x] (← inferType res), some x, some res] return res /-- -/ def mkLetFVarsWith (e : Expr) (xs : Array Expr) (ts : Array Expr) : MetaM Expr := do - if xs.size != ts.size then throwError "Expected same length: {xs} and {ts}" + if xs.size != ts.size then + throwError "Expected same length: {xs} and {ts}" let mut e := e.abstract xs for i in [:xs.size] do let n := (← FVarId.getDecl xs[xs.size-1-i]!.fvarId!).userName diff --git a/CvxLean/Tactic/DCP/AtomLibrary/Fns/Abs.lean b/CvxLean/Tactic/DCP/AtomLibrary/Fns/Abs.lean index 4b71e87d..edf2de64 100644 --- a/CvxLean/Tactic/DCP/AtomLibrary/Fns/Abs.lean +++ b/CvxLean/Tactic/DCP/AtomLibrary/Fns/Abs.lean @@ -1,4 +1,5 @@ -import CvxLean.Tactic.DCP.AtomCmdimport CvxLean.Tactic.DCP.AtomLibrary.Sets.Cones +import CvxLean.Tactic.DCP.AtomCmd +import CvxLean.Tactic.DCP.AtomLibrary.Sets.Cones import CvxLean.Tactic.DCP.AtomLibrary.Fns.Add import CvxLean.Tactic.DCP.AtomLibrary.Fns.Sub import CvxLean.Lib.Math.Data.Matrix diff --git a/CvxLean/Tactic/DCP/AtomLibrary/Fns/Add.lean b/CvxLean/Tactic/DCP/AtomLibrary/Fns/Add.lean index c552055c..56babb01 100644 --- a/CvxLean/Tactic/DCP/AtomLibrary/Fns/Add.lean +++ b/CvxLean/Tactic/DCP/AtomLibrary/Fns/Add.lean @@ -1,4 +1,5 @@ -import CvxLean.Tactic.DCP.AtomCmdimport CvxLean.Lib.Math.Data.Matrix +import CvxLean.Tactic.DCP.AtomCmd +import CvxLean.Lib.Math.Data.Matrix namespace CvxLean diff --git a/CvxLean/Tactic/DCP/AtomLibrary/Fns/CumSum.lean b/CvxLean/Tactic/DCP/AtomLibrary/Fns/CumSum.lean index c0403cd0..244e7542 100644 --- a/CvxLean/Tactic/DCP/AtomLibrary/Fns/CumSum.lean +++ b/CvxLean/Tactic/DCP/AtomLibrary/Fns/CumSum.lean @@ -1,4 +1,5 @@ -import CvxLean.Tactic.DCP.AtomCmdimport CvxLean.Lib.Math.Data.Vec +import CvxLean.Tactic.DCP.AtomCmd +import CvxLean.Lib.Math.Data.Vec namespace CvxLean diff --git a/CvxLean/Tactic/DCP/AtomLibrary/Fns/Diag.lean b/CvxLean/Tactic/DCP/AtomLibrary/Fns/Diag.lean index 93128677..ae2efb26 100644 --- a/CvxLean/Tactic/DCP/AtomLibrary/Fns/Diag.lean +++ b/CvxLean/Tactic/DCP/AtomLibrary/Fns/Diag.lean @@ -1,4 +1,5 @@ -import CvxLean.Tactic.DCP.AtomCmdimport CvxLean.Lib.Math.Data.Matrix +import CvxLean.Tactic.DCP.AtomCmd +import CvxLean.Lib.Math.Data.Matrix namespace CvxLean diff --git a/CvxLean/Tactic/DCP/AtomLibrary/Fns/Diagonal.lean b/CvxLean/Tactic/DCP/AtomLibrary/Fns/Diagonal.lean index 4626ac43..5d234d2c 100644 --- a/CvxLean/Tactic/DCP/AtomLibrary/Fns/Diagonal.lean +++ b/CvxLean/Tactic/DCP/AtomLibrary/Fns/Diagonal.lean @@ -1,4 +1,5 @@ -import CvxLean.Tactic.DCP.AtomCmdimport CvxLean.Lib.Math.Data.Matrix +import CvxLean.Tactic.DCP.AtomCmd +import CvxLean.Lib.Math.Data.Matrix namespace CvxLean diff --git a/CvxLean/Tactic/DCP/AtomLibrary/Fns/Div.lean b/CvxLean/Tactic/DCP/AtomLibrary/Fns/Div.lean index 888c7717..f93fd087 100644 --- a/CvxLean/Tactic/DCP/AtomLibrary/Fns/Div.lean +++ b/CvxLean/Tactic/DCP/AtomLibrary/Fns/Div.lean @@ -1,4 +1,5 @@ import CvxLean.Tactic.DCP.AtomCmd + namespace CvxLean open Real diff --git a/CvxLean/Tactic/DCP/AtomLibrary/Fns/DotProduct.lean b/CvxLean/Tactic/DCP/AtomLibrary/Fns/DotProduct.lean index 9bdc2b71..1f7df35f 100644 --- a/CvxLean/Tactic/DCP/AtomLibrary/Fns/DotProduct.lean +++ b/CvxLean/Tactic/DCP/AtomLibrary/Fns/DotProduct.lean @@ -1,4 +1,5 @@ import CvxLean.Tactic.DCP.AtomCmd + namespace CvxLean declare_atom Vec.dotProduct1 [affine] (m : Nat)& (x : Fin m → ℝ)& (y : Fin m → ℝ)? : Matrix.dotProduct x y := diff --git a/CvxLean/Tactic/DCP/AtomLibrary/Fns/Entr.lean b/CvxLean/Tactic/DCP/AtomLibrary/Fns/Entr.lean index 9a958da6..87e2bdb7 100644 --- a/CvxLean/Tactic/DCP/AtomLibrary/Fns/Entr.lean +++ b/CvxLean/Tactic/DCP/AtomLibrary/Fns/Entr.lean @@ -1,4 +1,5 @@ -import CvxLean.Tactic.DCP.AtomCmdimport CvxLean.Tactic.DCP.AtomLibrary.Sets.Cones +import CvxLean.Tactic.DCP.AtomCmd +import CvxLean.Tactic.DCP.AtomLibrary.Sets.Cones import CvxLean.Lib.Math.Data.Real import CvxLean.Lib.Math.Data.Vec diff --git a/CvxLean/Tactic/DCP/AtomLibrary/Fns/Exp.lean b/CvxLean/Tactic/DCP/AtomLibrary/Fns/Exp.lean index 0a850d1b..3827b0d8 100644 --- a/CvxLean/Tactic/DCP/AtomLibrary/Fns/Exp.lean +++ b/CvxLean/Tactic/DCP/AtomLibrary/Fns/Exp.lean @@ -1,4 +1,5 @@ -import CvxLean.Tactic.DCP.AtomCmdimport CvxLean.Tactic.DCP.AtomLibrary.Sets.Cones +import CvxLean.Tactic.DCP.AtomCmd +import CvxLean.Tactic.DCP.AtomLibrary.Sets.Cones import CvxLean.Lib.Math.Data.Vec namespace CvxLean diff --git a/CvxLean/Tactic/DCP/AtomLibrary/Fns/FromBlocks.lean b/CvxLean/Tactic/DCP/AtomLibrary/Fns/FromBlocks.lean index eaaa34f3..f52c6c32 100644 --- a/CvxLean/Tactic/DCP/AtomLibrary/Fns/FromBlocks.lean +++ b/CvxLean/Tactic/DCP/AtomLibrary/Fns/FromBlocks.lean @@ -1,4 +1,5 @@ -import CvxLean.Tactic.DCP.AtomCmdimport CvxLean.Lib.Math.Data.Matrix +import CvxLean.Tactic.DCP.AtomCmd +import CvxLean.Lib.Math.Data.Matrix namespace CvxLean diff --git a/CvxLean/Tactic/DCP/AtomLibrary/Fns/GeoMean.lean b/CvxLean/Tactic/DCP/AtomLibrary/Fns/GeoMean.lean index f765a2e5..772adeb0 100644 --- a/CvxLean/Tactic/DCP/AtomLibrary/Fns/GeoMean.lean +++ b/CvxLean/Tactic/DCP/AtomLibrary/Fns/GeoMean.lean @@ -1,4 +1,5 @@ -import CvxLean.Tactic.DCP.AtomCmdimport CvxLean.Tactic.DCP.AtomLibrary.Sets.Cones +import CvxLean.Tactic.DCP.AtomCmd +import CvxLean.Tactic.DCP.AtomLibrary.Sets.Cones import CvxLean.Tactic.DCP.AtomLibrary.Sets.Le import CvxLean.Tactic.DCP.AtomLibrary.Fns.VecCons import CvxLean.Tactic.DCP.AtomLibrary.Fns.Add diff --git a/CvxLean/Tactic/DCP/AtomLibrary/Fns/Huber.lean b/CvxLean/Tactic/DCP/AtomLibrary/Fns/Huber.lean index e05ee935..45542ade 100644 --- a/CvxLean/Tactic/DCP/AtomLibrary/Fns/Huber.lean +++ b/CvxLean/Tactic/DCP/AtomLibrary/Fns/Huber.lean @@ -1,4 +1,5 @@ -import CvxLean.Tactic.DCP.AtomCmdimport CvxLean.Tactic.DCP.AtomLibrary.Sets.Cones +import CvxLean.Tactic.DCP.AtomCmd +import CvxLean.Tactic.DCP.AtomLibrary.Sets.Cones import CvxLean.Tactic.DCP.AtomLibrary.Sets.Le import CvxLean.Tactic.DCP.AtomLibrary.Sets.Eq import CvxLean.Tactic.DCP.AtomLibrary.Fns.Sq diff --git a/CvxLean/Tactic/DCP/AtomLibrary/Fns/Inv.lean b/CvxLean/Tactic/DCP/AtomLibrary/Fns/Inv.lean index 3351b2da..87ce4b9b 100644 --- a/CvxLean/Tactic/DCP/AtomLibrary/Fns/Inv.lean +++ b/CvxLean/Tactic/DCP/AtomLibrary/Fns/Inv.lean @@ -1,4 +1,5 @@ -import CvxLean.Tactic.DCP.AtomCmdimport CvxLean.Tactic.DCP.AtomLibrary.Sets.Cones +import CvxLean.Tactic.DCP.AtomCmd +import CvxLean.Tactic.DCP.AtomLibrary.Sets.Cones import CvxLean.Tactic.DCP.AtomLibrary.Sets.Le import CvxLean.Tactic.DCP.AtomLibrary.Fns.VecCons import CvxLean.Tactic.DCP.AtomLibrary.Fns.Add diff --git a/CvxLean/Tactic/DCP/AtomLibrary/Fns/KLDiv.lean b/CvxLean/Tactic/DCP/AtomLibrary/Fns/KLDiv.lean index 05758ce2..61107270 100644 --- a/CvxLean/Tactic/DCP/AtomLibrary/Fns/KLDiv.lean +++ b/CvxLean/Tactic/DCP/AtomLibrary/Fns/KLDiv.lean @@ -1,4 +1,5 @@ -import CvxLean.Tactic.DCP.AtomCmdimport CvxLean.Tactic.DCP.AtomLibrary.Sets.Cones +import CvxLean.Tactic.DCP.AtomCmd +import CvxLean.Tactic.DCP.AtomLibrary.Sets.Cones import CvxLean.Tactic.DCP.AtomLibrary.Sets.Le import CvxLean.Tactic.DCP.AtomLibrary.Fns.Exp import CvxLean.Tactic.DCP.AtomLibrary.Fns.Sub diff --git a/CvxLean/Tactic/DCP/AtomLibrary/Fns/Log.lean b/CvxLean/Tactic/DCP/AtomLibrary/Fns/Log.lean index d697b79a..51dd301d 100644 --- a/CvxLean/Tactic/DCP/AtomLibrary/Fns/Log.lean +++ b/CvxLean/Tactic/DCP/AtomLibrary/Fns/Log.lean @@ -1,4 +1,5 @@ -import CvxLean.Tactic.DCP.AtomCmdimport CvxLean.Tactic.DCP.AtomLibrary.Sets.Cones +import CvxLean.Tactic.DCP.AtomCmd +import CvxLean.Tactic.DCP.AtomLibrary.Sets.Cones import CvxLean.Lib.Math.Data.Vec namespace CvxLean diff --git a/CvxLean/Tactic/DCP/AtomLibrary/Fns/LogDet.lean b/CvxLean/Tactic/DCP/AtomLibrary/Fns/LogDet.lean index 389abcbe..f6c0074e 100644 --- a/CvxLean/Tactic/DCP/AtomLibrary/Fns/LogDet.lean +++ b/CvxLean/Tactic/DCP/AtomLibrary/Fns/LogDet.lean @@ -1,4 +1,5 @@ -import CvxLean.Tactic.DCP.AtomCmdimport CvxLean.Tactic.DCP.AtomLibrary.Sets.Cones +import CvxLean.Tactic.DCP.AtomCmd +import CvxLean.Tactic.DCP.AtomLibrary.Sets.Cones import CvxLean.Tactic.DCP.AtomLibrary.Fns.Sum import CvxLean.Tactic.DCP.AtomLibrary.Fns.PosSemidef import CvxLean.Tactic.DCP.AtomLibrary.Fns.FromBlocks diff --git a/CvxLean/Tactic/DCP/AtomLibrary/Fns/LogSumExp.lean b/CvxLean/Tactic/DCP/AtomLibrary/Fns/LogSumExp.lean index 05e06184..1c8c9f4f 100644 --- a/CvxLean/Tactic/DCP/AtomLibrary/Fns/LogSumExp.lean +++ b/CvxLean/Tactic/DCP/AtomLibrary/Fns/LogSumExp.lean @@ -1,4 +1,5 @@ -import CvxLean.Tactic.DCP.AtomCmdimport CvxLean.Tactic.DCP.AtomLibrary.Sets.Cones +import CvxLean.Tactic.DCP.AtomCmd +import CvxLean.Tactic.DCP.AtomLibrary.Sets.Cones import CvxLean.Tactic.DCP.AtomLibrary.Sets.Le import CvxLean.Tactic.DCP.AtomLibrary.Fns.Exp import CvxLean.Tactic.DCP.AtomLibrary.Fns.Log diff --git a/CvxLean/Tactic/DCP/AtomLibrary/Fns/MatrixConst.lean b/CvxLean/Tactic/DCP/AtomLibrary/Fns/MatrixConst.lean index 6f190f87..da27ce6a 100644 --- a/CvxLean/Tactic/DCP/AtomLibrary/Fns/MatrixConst.lean +++ b/CvxLean/Tactic/DCP/AtomLibrary/Fns/MatrixConst.lean @@ -1,4 +1,5 @@ -import CvxLean.Tactic.DCP.AtomCmdimport CvxLean.Lib.Math.Data.Matrix +import CvxLean.Tactic.DCP.AtomCmd +import CvxLean.Lib.Math.Data.Matrix namespace CvxLean diff --git a/CvxLean/Tactic/DCP/AtomLibrary/Fns/MatrixMul.lean b/CvxLean/Tactic/DCP/AtomLibrary/Fns/MatrixMul.lean index 27de7a18..e46e57e1 100644 --- a/CvxLean/Tactic/DCP/AtomLibrary/Fns/MatrixMul.lean +++ b/CvxLean/Tactic/DCP/AtomLibrary/Fns/MatrixMul.lean @@ -1,4 +1,5 @@ -import CvxLean.Tactic.DCP.AtomCmdimport CvxLean.Lib.Math.Data.Matrix +import CvxLean.Tactic.DCP.AtomCmd +import CvxLean.Lib.Math.Data.Matrix namespace CvxLean diff --git a/CvxLean/Tactic/DCP/AtomLibrary/Fns/Max.lean b/CvxLean/Tactic/DCP/AtomLibrary/Fns/Max.lean index 37868698..2e98fe93 100644 --- a/CvxLean/Tactic/DCP/AtomLibrary/Fns/Max.lean +++ b/CvxLean/Tactic/DCP/AtomLibrary/Fns/Max.lean @@ -1,4 +1,5 @@ -import CvxLean.Tactic.DCP.AtomCmdimport CvxLean.Tactic.DCP.AtomLibrary.Sets.Le +import CvxLean.Tactic.DCP.AtomCmd +import CvxLean.Tactic.DCP.AtomLibrary.Sets.Le import CvxLean.Lib.Math.Data.Vec namespace CvxLean diff --git a/CvxLean/Tactic/DCP/AtomLibrary/Fns/MaximizeNeg.lean b/CvxLean/Tactic/DCP/AtomLibrary/Fns/MaximizeNeg.lean index 74ecc8b8..c6b1aebf 100644 --- a/CvxLean/Tactic/DCP/AtomLibrary/Fns/MaximizeNeg.lean +++ b/CvxLean/Tactic/DCP/AtomLibrary/Fns/MaximizeNeg.lean @@ -1,4 +1,5 @@ import CvxLean.Tactic.DCP.AtomCmd + namespace CvxLean declare_atom maximizeNeg [affine] (x : ℝ)- : maximizeNeg x := diff --git a/CvxLean/Tactic/DCP/AtomLibrary/Fns/Min.lean b/CvxLean/Tactic/DCP/AtomLibrary/Fns/Min.lean index 47e896cd..a936af13 100644 --- a/CvxLean/Tactic/DCP/AtomLibrary/Fns/Min.lean +++ b/CvxLean/Tactic/DCP/AtomLibrary/Fns/Min.lean @@ -1,4 +1,5 @@ -import CvxLean.Tactic.DCP.AtomCmdimport CvxLean.Tactic.DCP.AtomLibrary.Sets.Le +import CvxLean.Tactic.DCP.AtomCmd +import CvxLean.Tactic.DCP.AtomLibrary.Sets.Le import CvxLean.Lib.Math.Data.Vec namespace CvxLean diff --git a/CvxLean/Tactic/DCP/AtomLibrary/Fns/Mul.lean b/CvxLean/Tactic/DCP/AtomLibrary/Fns/Mul.lean index a16929f2..d6fea771 100644 --- a/CvxLean/Tactic/DCP/AtomLibrary/Fns/Mul.lean +++ b/CvxLean/Tactic/DCP/AtomLibrary/Fns/Mul.lean @@ -1,4 +1,5 @@ import CvxLean.Tactic.DCP.AtomCmd + namespace CvxLean declare_atom mul1 [affine] (x : ℝ)& (y : ℝ)+ : x * y := diff --git a/CvxLean/Tactic/DCP/AtomLibrary/Fns/MulVec.lean b/CvxLean/Tactic/DCP/AtomLibrary/Fns/MulVec.lean index 88412ea4..df342282 100644 --- a/CvxLean/Tactic/DCP/AtomLibrary/Fns/MulVec.lean +++ b/CvxLean/Tactic/DCP/AtomLibrary/Fns/MulVec.lean @@ -1,4 +1,5 @@ import CvxLean.Tactic.DCP.AtomCmd + namespace CvxLean declare_atom Matrix.mulVec [affine] (n : ℕ)& (m : ℕ)& diff --git a/CvxLean/Tactic/DCP/AtomLibrary/Fns/Neg.lean b/CvxLean/Tactic/DCP/AtomLibrary/Fns/Neg.lean index 6fa055c7..79738ae7 100644 --- a/CvxLean/Tactic/DCP/AtomLibrary/Fns/Neg.lean +++ b/CvxLean/Tactic/DCP/AtomLibrary/Fns/Neg.lean @@ -1,4 +1,5 @@ import CvxLean.Tactic.DCP.AtomCmd + namespace CvxLean declare_atom neg [affine] (x : ℝ)- : - x := diff --git a/CvxLean/Tactic/DCP/AtomLibrary/Fns/Norm.lean b/CvxLean/Tactic/DCP/AtomLibrary/Fns/Norm.lean index dee19779..66f5c6f1 100644 --- a/CvxLean/Tactic/DCP/AtomLibrary/Fns/Norm.lean +++ b/CvxLean/Tactic/DCP/AtomLibrary/Fns/Norm.lean @@ -1,4 +1,5 @@ -import CvxLean.Tactic.DCP.AtomCmdimport CvxLean.Tactic.DCP.AtomLibrary.Sets.Cones +import CvxLean.Tactic.DCP.AtomCmd +import CvxLean.Tactic.DCP.AtomLibrary.Sets.Cones import CvxLean.Tactic.DCP.AtomLibrary.Fns.VecCons import CvxLean.Lib.Math.Data.Vec diff --git a/CvxLean/Tactic/DCP/AtomLibrary/Fns/Nth.lean b/CvxLean/Tactic/DCP/AtomLibrary/Fns/Nth.lean index 77ffb74f..6bc87753 100644 --- a/CvxLean/Tactic/DCP/AtomLibrary/Fns/Nth.lean +++ b/CvxLean/Tactic/DCP/AtomLibrary/Fns/Nth.lean @@ -1,4 +1,5 @@ import CvxLean.Tactic.DCP.AtomCmd + namespace CvxLean declare_atom Vec.nth [affine] (m : Nat)& (x : Fin m → ℝ)? (i : Fin m)& : x i := diff --git a/CvxLean/Tactic/DCP/AtomLibrary/Fns/Perspective.lean b/CvxLean/Tactic/DCP/AtomLibrary/Fns/Perspective.lean index c9e1b9d7..96e4bbda 100644 --- a/CvxLean/Tactic/DCP/AtomLibrary/Fns/Perspective.lean +++ b/CvxLean/Tactic/DCP/AtomLibrary/Fns/Perspective.lean @@ -1,4 +1,5 @@ -import CvxLean.Tactic.DCP.AtomCmdimport CvxLean.Tactic.DCP.AtomLibrary.Sets.Cones +import CvxLean.Tactic.DCP.AtomCmd +import CvxLean.Tactic.DCP.AtomLibrary.Sets.Cones namespace CvxLean diff --git a/CvxLean/Tactic/DCP/AtomLibrary/Fns/PosSemidef.lean b/CvxLean/Tactic/DCP/AtomLibrary/Fns/PosSemidef.lean index 9c0f9074..55cb3e97 100644 --- a/CvxLean/Tactic/DCP/AtomLibrary/Fns/PosSemidef.lean +++ b/CvxLean/Tactic/DCP/AtomLibrary/Fns/PosSemidef.lean @@ -1,4 +1,5 @@ -import CvxLean.Tactic.DCP.AtomCmdimport CvxLean.Tactic.DCP.AtomLibrary.Sets.Cones +import CvxLean.Tactic.DCP.AtomCmd +import CvxLean.Tactic.DCP.AtomLibrary.Sets.Cones namespace CvxLean diff --git a/CvxLean/Tactic/DCP/AtomLibrary/Fns/Power.lean b/CvxLean/Tactic/DCP/AtomLibrary/Fns/Power.lean index 48593e49..1d2cbe31 100644 --- a/CvxLean/Tactic/DCP/AtomLibrary/Fns/Power.lean +++ b/CvxLean/Tactic/DCP/AtomLibrary/Fns/Power.lean @@ -1,4 +1,5 @@ -import CvxLean.Tactic.DCP.AtomCmdimport CvxLean.Tactic.DCP.AtomLibrary.Sets.Cones +import CvxLean.Tactic.DCP.AtomCmd +import CvxLean.Tactic.DCP.AtomLibrary.Sets.Cones import CvxLean.Tactic.DCP.AtomLibrary.Sets.Le import CvxLean.Tactic.DCP.AtomLibrary.Fns.VecCons import CvxLean.Tactic.DCP.AtomLibrary.Fns.Add diff --git a/CvxLean/Tactic/DCP/AtomLibrary/Fns/QuadOverLin.lean b/CvxLean/Tactic/DCP/AtomLibrary/Fns/QuadOverLin.lean index 5987408a..450df790 100644 --- a/CvxLean/Tactic/DCP/AtomLibrary/Fns/QuadOverLin.lean +++ b/CvxLean/Tactic/DCP/AtomLibrary/Fns/QuadOverLin.lean @@ -1,4 +1,5 @@ -import CvxLean.Tactic.DCP.AtomCmdimport CvxLean.Tactic.DCP.AtomLibrary.Sets.Cones +import CvxLean.Tactic.DCP.AtomCmd +import CvxLean.Tactic.DCP.AtomLibrary.Sets.Cones import CvxLean.Tactic.DCP.AtomLibrary.Sets.Le import CvxLean.Tactic.DCP.AtomLibrary.Fns.VecCons import CvxLean.Tactic.DCP.AtomLibrary.Fns.Add diff --git a/CvxLean/Tactic/DCP/AtomLibrary/Fns/SMul.lean b/CvxLean/Tactic/DCP/AtomLibrary/Fns/SMul.lean index 03b21e49..970170c0 100644 --- a/CvxLean/Tactic/DCP/AtomLibrary/Fns/SMul.lean +++ b/CvxLean/Tactic/DCP/AtomLibrary/Fns/SMul.lean @@ -1,4 +1,5 @@ import CvxLean.Tactic.DCP.AtomCmd + namespace CvxLean declare_atom Nat.smul [affine] (n : ℕ)& (x : ℝ)+ : diff --git a/CvxLean/Tactic/DCP/AtomLibrary/Fns/Sq.lean b/CvxLean/Tactic/DCP/AtomLibrary/Fns/Sq.lean index d08cd9e8..4c4be25c 100644 --- a/CvxLean/Tactic/DCP/AtomLibrary/Fns/Sq.lean +++ b/CvxLean/Tactic/DCP/AtomLibrary/Fns/Sq.lean @@ -1,4 +1,5 @@ -import CvxLean.Tactic.DCP.AtomCmdimport CvxLean.Tactic.DCP.AtomLibrary.Sets.Cones +import CvxLean.Tactic.DCP.AtomCmd +import CvxLean.Tactic.DCP.AtomLibrary.Sets.Cones import CvxLean.Tactic.DCP.AtomLibrary.Fns.VecCons import CvxLean.Tactic.DCP.AtomLibrary.Fns.VecToMatrix diff --git a/CvxLean/Tactic/DCP/AtomLibrary/Fns/Sqrt.lean b/CvxLean/Tactic/DCP/AtomLibrary/Fns/Sqrt.lean index 1b31d8af..939fcb5d 100644 --- a/CvxLean/Tactic/DCP/AtomLibrary/Fns/Sqrt.lean +++ b/CvxLean/Tactic/DCP/AtomLibrary/Fns/Sqrt.lean @@ -1,4 +1,5 @@ -import CvxLean.Tactic.DCP.AtomCmdimport CvxLean.Tactic.DCP.AtomLibrary.Sets.Cones +import CvxLean.Tactic.DCP.AtomCmd +import CvxLean.Tactic.DCP.AtomLibrary.Sets.Cones import CvxLean.Tactic.DCP.AtomLibrary.Fns.VecCons namespace CvxLean diff --git a/CvxLean/Tactic/DCP/AtomLibrary/Fns/Sub.lean b/CvxLean/Tactic/DCP/AtomLibrary/Fns/Sub.lean index 06e5d576..23a00b75 100644 --- a/CvxLean/Tactic/DCP/AtomLibrary/Fns/Sub.lean +++ b/CvxLean/Tactic/DCP/AtomLibrary/Fns/Sub.lean @@ -1,4 +1,5 @@ -import CvxLean.Tactic.DCP.AtomCmdimport CvxLean.Lib.Math.Data.Matrix +import CvxLean.Tactic.DCP.AtomCmd +import CvxLean.Lib.Math.Data.Matrix namespace CvxLean diff --git a/CvxLean/Tactic/DCP/AtomLibrary/Fns/Sum.lean b/CvxLean/Tactic/DCP/AtomLibrary/Fns/Sum.lean index 146e967f..e2c2dd99 100644 --- a/CvxLean/Tactic/DCP/AtomLibrary/Fns/Sum.lean +++ b/CvxLean/Tactic/DCP/AtomLibrary/Fns/Sum.lean @@ -1,4 +1,5 @@ -import CvxLean.Tactic.DCP.AtomCmdimport CvxLean.Lib.Math.Data.Vec +import CvxLean.Tactic.DCP.AtomCmd +import CvxLean.Lib.Math.Data.Vec import CvxLean.Lib.Math.Data.Matrix namespace CvxLean diff --git a/CvxLean/Tactic/DCP/AtomLibrary/Fns/ToUpperTri.lean b/CvxLean/Tactic/DCP/AtomLibrary/Fns/ToUpperTri.lean index b2c63cec..bb5cfa0f 100644 --- a/CvxLean/Tactic/DCP/AtomLibrary/Fns/ToUpperTri.lean +++ b/CvxLean/Tactic/DCP/AtomLibrary/Fns/ToUpperTri.lean @@ -1,4 +1,5 @@ -import CvxLean.Tactic.DCP.AtomCmdimport CvxLean.Lib.Math.Data.Matrix +import CvxLean.Tactic.DCP.AtomCmd +import CvxLean.Lib.Math.Data.Matrix import CvxLean.Lib.Math.LinearAlgebra.Matrix.ToUpperTri namespace CvxLean diff --git a/CvxLean/Tactic/DCP/AtomLibrary/Fns/Trace.lean b/CvxLean/Tactic/DCP/AtomLibrary/Fns/Trace.lean index 34afaff9..b8ea6dc6 100644 --- a/CvxLean/Tactic/DCP/AtomLibrary/Fns/Trace.lean +++ b/CvxLean/Tactic/DCP/AtomLibrary/Fns/Trace.lean @@ -1,4 +1,5 @@ -import CvxLean.Tactic.DCP.AtomCmdimport CvxLean.Lib.Math.Data.Matrix +import CvxLean.Tactic.DCP.AtomCmd +import CvxLean.Lib.Math.Data.Matrix namespace CvxLean diff --git a/CvxLean/Tactic/DCP/AtomLibrary/Fns/Transpose.lean b/CvxLean/Tactic/DCP/AtomLibrary/Fns/Transpose.lean index a44f9824..38c88f81 100644 --- a/CvxLean/Tactic/DCP/AtomLibrary/Fns/Transpose.lean +++ b/CvxLean/Tactic/DCP/AtomLibrary/Fns/Transpose.lean @@ -1,4 +1,5 @@ -import CvxLean.Tactic.DCP.AtomCmdimport CvxLean.Lib.Math.Data.Matrix +import CvxLean.Tactic.DCP.AtomCmd +import CvxLean.Lib.Math.Data.Matrix namespace CvxLean diff --git a/CvxLean/Tactic/DCP/AtomLibrary/Fns/VecCons.lean b/CvxLean/Tactic/DCP/AtomLibrary/Fns/VecCons.lean index 114101ef..e045b27a 100644 --- a/CvxLean/Tactic/DCP/AtomLibrary/Fns/VecCons.lean +++ b/CvxLean/Tactic/DCP/AtomLibrary/Fns/VecCons.lean @@ -1,4 +1,5 @@ -import CvxLean.Tactic.DCP.AtomCmdimport CvxLean.Lib.Math.Data.Matrix +import CvxLean.Tactic.DCP.AtomCmd +import CvxLean.Lib.Math.Data.Matrix namespace CvxLean diff --git a/CvxLean/Tactic/DCP/AtomLibrary/Fns/VecConst.lean b/CvxLean/Tactic/DCP/AtomLibrary/Fns/VecConst.lean index a08c9f29..5eda8ac8 100644 --- a/CvxLean/Tactic/DCP/AtomLibrary/Fns/VecConst.lean +++ b/CvxLean/Tactic/DCP/AtomLibrary/Fns/VecConst.lean @@ -1,4 +1,5 @@ -import CvxLean.Tactic.DCP.AtomCmdimport CvxLean.Lib.Math.Data.Vec +import CvxLean.Tactic.DCP.AtomCmd +import CvxLean.Lib.Math.Data.Vec namespace CvxLean diff --git a/CvxLean/Tactic/DCP/AtomLibrary/Fns/VecToMatrix.lean b/CvxLean/Tactic/DCP/AtomLibrary/Fns/VecToMatrix.lean index 0bb870ac..5a1dc6da 100644 --- a/CvxLean/Tactic/DCP/AtomLibrary/Fns/VecToMatrix.lean +++ b/CvxLean/Tactic/DCP/AtomLibrary/Fns/VecToMatrix.lean @@ -1,4 +1,5 @@ -import CvxLean.Tactic.DCP.AtomCmdimport CvxLean.Lib.Math.Data.Vec +import CvxLean.Tactic.DCP.AtomCmd +import CvxLean.Lib.Math.Data.Vec import CvxLean.Lib.Math.Data.Matrix namespace CvxLean diff --git a/CvxLean/Tactic/DCP/AtomLibrary/Sets/Cones.lean b/CvxLean/Tactic/DCP/AtomLibrary/Sets/Cones.lean index c7202035..0a147e37 100644 --- a/CvxLean/Tactic/DCP/AtomLibrary/Sets/Cones.lean +++ b/CvxLean/Tactic/DCP/AtomLibrary/Sets/Cones.lean @@ -1,4 +1,5 @@ -import CvxLean.Tactic.DCP.AtomCmdimport CvxLean.Lib.Cones.All +import CvxLean.Tactic.DCP.AtomCmd +import CvxLean.Lib.Cones.All import CvxLean.Syntax.Minimization namespace CvxLean diff --git a/CvxLean/Tactic/DCP/AtomLibrary/Sets/Eq.lean b/CvxLean/Tactic/DCP/AtomLibrary/Sets/Eq.lean index ff81113f..27a0dcef 100644 --- a/CvxLean/Tactic/DCP/AtomLibrary/Sets/Eq.lean +++ b/CvxLean/Tactic/DCP/AtomLibrary/Sets/Eq.lean @@ -1,4 +1,5 @@ -import CvxLean.Tactic.DCP.AtomCmdimport CvxLean.Tactic.DCP.AtomLibrary.Sets.Cones +import CvxLean.Tactic.DCP.AtomCmd +import CvxLean.Tactic.DCP.AtomLibrary.Sets.Cones import CvxLean.Tactic.DCP.AtomLibrary.Fns.Sub namespace CvxLean diff --git a/CvxLean/Tactic/DCP/AtomLibrary/Sets/Le.lean b/CvxLean/Tactic/DCP/AtomLibrary/Sets/Le.lean index 938fbdda..d9231129 100644 --- a/CvxLean/Tactic/DCP/AtomLibrary/Sets/Le.lean +++ b/CvxLean/Tactic/DCP/AtomLibrary/Sets/Le.lean @@ -1,4 +1,5 @@ -import CvxLean.Tactic.DCP.AtomCmdimport CvxLean.Tactic.DCP.AtomLibrary.Sets.Cones +import CvxLean.Tactic.DCP.AtomCmd +import CvxLean.Tactic.DCP.AtomLibrary.Sets.Cones import CvxLean.Tactic.DCP.AtomLibrary.Fns.Sub namespace CvxLean From a54593ed7a42b11c43d5be1351944d2f5b0e747e Mon Sep 17 00:00:00 2001 From: Ramon Fernandez Mir Date: Thu, 29 Feb 2024 16:44:19 +0000 Subject: [PATCH 12/25] doc: helpers for `Expr` --- CvxLean/Meta/Util/Expr.lean | 114 +++++++++++++++++++++++--------- CvxLean/Tactic/DCP/AtomCmd.lean | 35 ---------- 2 files changed, 83 insertions(+), 66 deletions(-) diff --git a/CvxLean/Meta/Util/Expr.lean b/CvxLean/Meta/Util/Expr.lean index d8ae5cfa..0adea040 100644 --- a/CvxLean/Meta/Util/Expr.lean +++ b/CvxLean/Meta/Util/Expr.lean @@ -5,58 +5,96 @@ import CvxLean.Lib.Math.Data.Array Helper functions to create and manipulate Lean expressions. -/ -open Lean +namespace Lean + +open Lean Meta + +namespace Expr + +/-- Given expressions `e₁, ..., eₙ` return `(And.intro e₁ ⋯ (And.intro eₙ₋₁ eₙ) ⋯)`, i.e., `∧` them, +with associativity to the right. -/ +def mkAndIntro (xs : Array Expr) : MetaM Expr := do + let mut res := xs[xs.size - 1]! + for i in [:xs.size - 1] do + res ← mkAppM ``And.intro #[xs[xs.size - 2 - i]!, res] + return res + +/-- Make existential type. -/ +def mkExistsFVars (xs : Array Expr) (e : Expr) : MetaM Expr := do + let mut res := e + for i in [:xs.size] do + let x := xs[xs.size - i - 1]! + res ← mkAppM ``Exists #[← mkLambdaFVars #[x] res] + return res + +/-- Make existential term. -/ +def mkExistsIntro (xs : Array Expr) (e : Expr) : MetaM Expr := do + let mut res := e + for i in [:xs.size] do + let x := xs[xs.size - i - 1]! + res ← mkAppOptM ``Exists.intro + #[none, some <| ← mkLambdaFVars #[x] (← inferType res), some x, some res] + return res + +/-- Make let bindings from free variables `xs`. -/ +def mkLetFVarsWith (e : Expr) (xs : Array Expr) (ts : Array Expr) : MetaM Expr := do + if xs.size != ts.size then + throwError "Expected same length: {xs} and {ts}" + let mut e := e.abstract xs + for i in [:xs.size] do + let n := (← FVarId.getDecl xs[xs.size - 1 - i]!.fvarId!).userName + e := mkLet n (← inferType xs[xs.size - 1 - i]!) ts[xs.size - 1 - i]! e + return e /-- Check if `e` is constant by checking if it contains any free variable. -/ -def Lean.Expr.isConstant (e : Expr) : Bool := (Lean.collectFVars {} e).fvarSet.isEmpty +def isConstant (e : Expr) : Bool := (Lean.collectFVars {} e).fvarSet.isEmpty /-- Check if `e` is constant by checking if it contains any free variable from `vars`. -/ -def Lean.Expr.isRelativelyConstant (e : Expr) (vars : Array FVarId) : Bool := Id.run do +def isRelativelyConstant (e : Expr) (vars : Array FVarId) : Bool := Id.run do let fvarSet := (Lean.collectFVars {} e).fvarSet for v in vars do if fvarSet.contains v then return false return true /-- Remove the metadata from an expression. -/ -def Lean.Expr.removeMData (e : Expr) : CoreM Expr := do +def removeMData (e : Expr) : CoreM Expr := do let post (e : Expr) : CoreM TransformStep := do return TransformStep.done e.consumeMData Core.transform e (post := post) -/-- Combination of `elabTermAndSynthesize` and `ensureHasType`. -/ -def Lean.Elab.Term.elabTermAndSynthesizeEnsuringType (stx : Syntax) (expectedType? : Option Expr) - (errorMsgHeader? : Option String := none) : TermElabM Expr := do - let e ← elabTermAndSynthesize stx expectedType? - withRef stx <| ensureHasType expectedType? e errorMsgHeader? - -def Lean.Expr.mkAppBeta (e : Expr) (arg : Expr) := +/-- Basically `β`-reduction. -/ +def mkAppBeta (e : Expr) (arg : Expr) := e.bindingBody!.instantiate1 arg -def Lean.Expr.mkAppNBeta (e : Expr) (args : Array Expr) : Expr := Id.run do +/-- Same as `mkAppBeta` but with several arguments. -/ +def mkAppNBeta (e : Expr) (args : Array Expr) : Expr := Id.run do let mut e := e - for _arg in args do + for _ in args do e := e.bindingBody! e.instantiateRev args -def Lean.Expr.convertLambdasToLets (e : Expr) (args : Array Expr) : Expr := Id.run do +/-- Given a lambda term `e := λx₁. ... λxₙ. b` and values for every variable `xᵢ`, turn `e` into +`let x₁ := v₁; ... let xₙ := vₙ; b`. -/ +def convertLambdasToLets (e : Expr) (args : Array Expr) : Expr := Id.run do let mut e := e let mut names := #[] let mut tys := #[] - for _arg in args do + for _ in args do tys := tys.push e.bindingDomain! names := names.push e.bindingName! e := e.bindingBody! for i in [:args.size] do - e := mkLet names[args.size-1-i]! tys[args.size-1-i]! args[args.size-1-i]! e + e := mkLet names[args.size - 1 - i]! tys[args.size - 1 - i]! args[args.size - 1 - i]! e return e -def Lean.Expr.size : Expr → Nat - | bvar _ => 1 - | fvar _ => 1 - | mvar _ => 1 - | sort _ => 1 - | const _ _ => 1 - | app a b => size a + size b +/-- Size of expressions, which can be a useful heuristic. -/ +def size : Expr → Nat + | bvar _ => 1 + | fvar _ => 1 + | mvar _ => 1 + | sort _ => 1 + | const _ _ => 1 + | app a b => size a + size b | lam _ _ a _ => size a + 1 | forallE _ _ a _ => size a + 1 | letE _ _ a b _ => size a + size b + 1 @@ -66,27 +104,39 @@ def Lean.Expr.size : Expr → Nat open Meta -def Lean.Expr.mkProd (as : Array Expr) : MetaM Expr := +/-- Make a product of expressions. -/ +def mkProd (as : Array Expr) : MetaM Expr := if as.size == 0 then throwError "Empty list." else if as.size == 1 then return as[0]! else Array.foldrM - (fun e1 e2 => Lean.Meta.mkAppM ``Prod.mk #[e1, e2]) - as[as.size - 1]! - (as.take (as.size - 1)) + (fun e1 e2 => Lean.Meta.mkAppM ``Prod.mk #[e1, e2]) as[as.size - 1]! (as.take (as.size - 1)) -private def Lean.Expr.mkArrayAux (ty : Expr) (as : List Expr) : +private def mkArrayAux (ty : Expr) (as : List Expr) : MetaM Expr := do match as with | [] => return mkAppN (mkConst ``Array.empty [levelZero]) #[ty] | e::es => - let r ← Lean.Expr.mkArrayAux ty es + let r ← mkArrayAux ty es mkAppM ``Array.push #[r, e] -def Lean.Expr.mkArray (ty : Expr) (as : Array Expr) : MetaM Expr := - Lean.Expr.mkArrayAux ty as.data.reverse +/-- Make expression array of given type, from array of expressions. -/ +def mkArray (ty : Expr) (as : Array Expr) : MetaM Expr := + mkArrayAux ty as.data.reverse + +end Expr + +namespace Elab.Term + +/-- Combination of `elabTermAndSynthesize` and `ensureHasType`. -/ +def elabTermAndSynthesizeEnsuringType (stx : Syntax) (expectedType? : Option Expr) + (errorMsgHeader? : Option String := none) : TermElabM Expr := do + let e ← elabTermAndSynthesize stx expectedType? + withRef stx <| ensureHasType expectedType? e errorMsgHeader? + +end Elab.Term /-- Wrapper of `Lean.addAndCompile` for definitions with some default values. -/ def Lean.simpleAddAndCompileDefn (n : Name) (e : Expr) : MetaM Unit := do @@ -101,3 +151,5 @@ def Lean.simpleAddDefn (n : Name) (e : Expr) : MetaM Unit := do Declaration.defnDecl <| mkDefinitionValEx n [] (← inferType e) e (Lean.ReducibilityHints.regular 0) (DefinitionSafety.safe) [] + +end Lean diff --git a/CvxLean/Tactic/DCP/AtomCmd.lean b/CvxLean/Tactic/DCP/AtomCmd.lean index c9e89487..ebc3c312 100644 --- a/CvxLean/Tactic/DCP/AtomCmd.lean +++ b/CvxLean/Tactic/DCP/AtomCmd.lean @@ -15,41 +15,6 @@ namespace CvxLean open Lean Expr Meta Elab Command -/-- Given expressions `e₁, ..., eₙ` return `(And.intro e₁ ⋯ (And.intro eₙ₋₁ eₙ) ⋯)`, i.e., `∧` them, -with associativity to the right. -/ -def mkAndIntro (xs : Array Expr) : MetaM Expr := do - let mut res := xs[xs.size - 1]! - for i in [:xs.size - 1] do - res ← mkAppM ``And.intro #[xs[xs.size - 2 - i]!, res] - return res - -/-- -/ -def mkExistsFVars (xs : Array Expr) (e : Expr) : MetaM Expr := do - let mut res := e - for i in [:xs.size] do - let x := xs[xs.size - i - 1]! - res ← mkAppM ``Exists #[← mkLambdaFVars #[x] res] - return res - -/-- -/ -def mkExistsIntro (xs : Array Expr) (e : Expr) : MetaM Expr := do - let mut res := e - for i in [:xs.size] do - let x := xs[xs.size-i-1]! - res ← mkAppOptM ``Exists.intro - #[none, some <| ← mkLambdaFVars #[x] (← inferType res), some x, some res] - return res - -/-- -/ -def mkLetFVarsWith (e : Expr) (xs : Array Expr) (ts : Array Expr) : MetaM Expr := do - if xs.size != ts.size then - throwError "Expected same length: {xs} and {ts}" - let mut e := e.abstract xs - for i in [:xs.size] do - let n := (← FVarId.getDecl xs[xs.size-1-i]!.fvarId!).userName - e := mkLet n (← inferType xs[xs.size-1-i]!) ts[xs.size-1-i]! e - return e - -- TODO: This does not respect namespaces. /-- Introduce new names for the proofs in the atom to speed up proof building later. -/ def addAtomDataDecls (id : Lean.Name) (atomData : GraphAtomData) : CommandElabM GraphAtomData := do From 43f5cbeff66ce8d8015c02348035927a50684a58 Mon Sep 17 00:00:00 2001 From: Ramon Fernandez Mir Date: Thu, 29 Feb 2024 16:51:24 +0000 Subject: [PATCH 13/25] doc: add TODO to make `vconds` available --- CvxLean/Tactic/DCP/AtomCmd.lean | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/CvxLean/Tactic/DCP/AtomCmd.lean b/CvxLean/Tactic/DCP/AtomCmd.lean index ebc3c312..a3485367 100644 --- a/CvxLean/Tactic/DCP/AtomCmd.lean +++ b/CvxLean/Tactic/DCP/AtomCmd.lean @@ -8,7 +8,12 @@ import CvxLean.Tactic.DCP.DCP /-! # Atom library (command) +TODO +### TODO + +* Make `vconds` available in `impConstrs` and `impObj`, in the same way that `bconds` are in + `elabImpConstrs`. This needs to be synchronised with the DCP procedure. -/ namespace CvxLean From 9a05ee4ef8d6fbbb053374c36dae8922684de877 Mon Sep 17 00:00:00 2001 From: Ramon Fernandez Mir Date: Thu, 29 Feb 2024 17:30:54 +0000 Subject: [PATCH 14/25] doc: fix docs for removing constraints --- CvxLean/Tactic/Basic/RemoveConstr.lean | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) diff --git a/CvxLean/Tactic/Basic/RemoveConstr.lean b/CvxLean/Tactic/Basic/RemoveConstr.lean index 193bbadc..3713762b 100644 --- a/CvxLean/Tactic/Basic/RemoveConstr.lean +++ b/CvxLean/Tactic/Basic/RemoveConstr.lean @@ -11,20 +11,20 @@ it might be implied by the other constraints. We illustrate it with an example of how to use it inside the `equivalence` command: ``` equivalence eqv/q : - optimization (x : ℝ) - minimize x + optimization (u : ℝ) + minimize exp u subject to - c₁ : 1 ≤ x - c₂ : 0 < x := by + c₁ : 1 ≤ exp u + c₂ : 0 < exp u := by remove_constr c₁ => - linarith + positivity ``` The resulting problem `q` looks as follows: ``` optimization (u : ℝ) minimize exp u subject to - c₁ : 1 ≤ x + c₁ : 1 ≤ exp u ``` In this case, `c₂` follows from `c₁`, so it can be removed. -/ From afb97393eee5b4236180e1babfcbcb3c6e0d228a Mon Sep 17 00:00:00 2001 From: Ramon Fernandez Mir Date: Thu, 29 Feb 2024 17:31:00 +0000 Subject: [PATCH 15/25] doc: rename constraints --- CvxLean/Tactic/Basic/RenameConstrs.lean | 37 +++++++++++++++++++++---- 1 file changed, 32 insertions(+), 5 deletions(-) diff --git a/CvxLean/Tactic/Basic/RenameConstrs.lean b/CvxLean/Tactic/Basic/RenameConstrs.lean index 7fe9364c..ce22d8c0 100644 --- a/CvxLean/Tactic/Basic/RenameConstrs.lean +++ b/CvxLean/Tactic/Basic/RenameConstrs.lean @@ -1,13 +1,39 @@ import CvxLean.Meta.Equivalence import CvxLean.Meta.TacticBuilder +/-! +# Tactic to rename constraints + +This file defines the `rename_constrs` tactic. It takes a list of names, e.g., `[c₁, c₂, c₃]`. The +list must have the same length as the number of constraints in the current problem. + +We illustrate it with an example of how to use it inside the `equivalence` command: +``` +equivalence eqv/q : + optimization (x : ℝ) + minimize x + subject to + c₁ : 1 ≤ x + c₂ : 0 < x := by + rename_constrs [h₁, h₂] +``` +The resulting problem `q` looks as follows: +``` +optimization (x : ℝ) + minimize x + subject to + h₁ : 1 ≤ x + h₂ : 0 < x +``` +-/ + namespace CvxLean open Lean Meta Elab Tactic namespace Meta -/-- -/ +/-- Split meta-data into (CvxLean) label and expression and replace the label with `name`. -/ def replaceConstrName (name : Name) (e : Expr) : MetaM Expr := do let (_, e) ← decomposeLabel e return mkLabel name e @@ -21,7 +47,7 @@ def renameConstrsBuilder (names : Array Name) : EquivalenceBuilder Unit := fun e let newConstrs ← withLambdaBody lhsMinExpr.constraints fun p constraints => do let mut constraints := (← decomposeAnd constraints).toArray if constraints.size < names.size then - throwError "`rename_constrs` error: Too many constraint names. Expected {constraints.size}." + throwRenameConstrsError "too many constraint names. Expected {constraints.size}." for i in [:names.size] do let newConstr ← replaceConstrName names[i]! constraints[i]! constraints := constraints.set! i newConstr @@ -29,11 +55,11 @@ def renameConstrsBuilder (names : Array Name) : EquivalenceBuilder Unit := fun e let rhsMinExpr := { lhsMinExpr with constraints := newConstrs } if !(← isDefEq eqvExpr.rhs rhsMinExpr.toExpr) then - throwError "`rename_constrs` error: Failed to unify the goal." + throwRenameConstrsError "failed to unify the goal." -- Close goal by reflexivity. if let _ :: _ ← evalTacticAt (← `(tactic| equivalence_rfl)) g then - throwError "`rename_constrs` error: Failed to close the goal." + throwRenameConstrsError "failed to close the goal." end Meta @@ -41,9 +67,10 @@ namespace Tactic open Lean.Elab Lean.Elab.Tactic Lean.Meta +/-- Tactic to rename all constraints given a list of names. This does not change the mathematical +interpretation of the problem. -/ syntax (name := renameConstrs) "rename_constrs" "[" ident,* "]" : tactic -/-- -/ @[tactic renameConstrs] partial def evalRenameConstrs : Tactic := fun stx => match stx with | `(tactic| rename_constrs [$ids,*]) => do From e5ef756839305086688056146ce540e5d4bb70c5 Mon Sep 17 00:00:00 2001 From: Ramon Fernandez Mir Date: Thu, 29 Feb 2024 17:35:43 +0000 Subject: [PATCH 16/25] doc: refine rename constraints --- CvxLean/Tactic/Basic/RenameConstrs.lean | 9 +++++---- 1 file changed, 5 insertions(+), 4 deletions(-) diff --git a/CvxLean/Tactic/Basic/RenameConstrs.lean b/CvxLean/Tactic/Basic/RenameConstrs.lean index ce22d8c0..6ffa05d5 100644 --- a/CvxLean/Tactic/Basic/RenameConstrs.lean +++ b/CvxLean/Tactic/Basic/RenameConstrs.lean @@ -4,8 +4,9 @@ import CvxLean.Meta.TacticBuilder /-! # Tactic to rename constraints -This file defines the `rename_constrs` tactic. It takes a list of names, e.g., `[c₁, c₂, c₃]`. The -list must have the same length as the number of constraints in the current problem. +This file defines the `rename_constrs` tactic. It takes a list of names, e.g., `[c₁, c₂, c₃]`. It +will replace the names of the first `n` constraints in the problem, where `n` is the length of the +input list. We illustrate it with an example of how to use it inside the `equivalence` command: ``` @@ -38,8 +39,8 @@ def replaceConstrName (name : Name) (e : Expr) : MetaM Expr := do let (_, e) ← decomposeLabel e return mkLabel name e -/-- Rename the constraints using `names`. The `names` Array can be shorter then - the number of constraints; then only the first few constraints are renamed. -/ +/-- Rename the constraints using `names`. The `names` array can be shorter then the number of +constraints; then only the first few constraints are renamed. -/ def renameConstrsBuilder (names : Array Name) : EquivalenceBuilder Unit := fun eqvExpr g => do let lhsMinExpr ← eqvExpr.toMinimizationExprLHS From 962b3654f93bac20c5f4e65c042551edf3dc067d Mon Sep 17 00:00:00 2001 From: Ramon Fernandez Mir Date: Thu, 29 Feb 2024 17:35:49 +0000 Subject: [PATCH 17/25] doc: rename variables --- CvxLean/Tactic/Basic/RenameVars.lean | 34 ++++++++++++++++++++++++++-- 1 file changed, 32 insertions(+), 2 deletions(-) diff --git a/CvxLean/Tactic/Basic/RenameVars.lean b/CvxLean/Tactic/Basic/RenameVars.lean index 39053f01..d5f59a18 100644 --- a/CvxLean/Tactic/Basic/RenameVars.lean +++ b/CvxLean/Tactic/Basic/RenameVars.lean @@ -2,13 +2,42 @@ import CvxLean.Meta.Equivalence import CvxLean.Meta.TacticBuilder import CvxLean.Meta.Util.Expr +/-! +# Tactic to rename variables + +This file defines the `rename_vars` tactic. It takes a list of names, e.g., `[x, y, z]`. The +list must have the same length as the number of optimization variables in the current problem. + +We illustrate it with an example of how to use it inside the `equivalence` command: +``` +equivalence eqv/q : + optimization (x y z : ℝ) + minimize x + y + z + subject to + c₁ : 1 ≤ x + c₂ : 1 ≤ y + c₃ : 1 ≤ z := by + rename_constrs [a, b, c] +``` +The resulting problem `q` looks as follows: +``` +optimization (a b c : ℝ) + minimize a + b + c + subject to + c₁ : 1 ≤ a + c₂ : 1 ≤ b + c₃ : 1 ≤ c +``` +-/ + namespace CvxLean open Lean Expr Meta Elab Tactic namespace Meta -/-- -/ +/-- Get the domain type, and replace the variables names stored in it (as meta-data) by the new +variable names. The resulting problem is the same expression with the new domain type. -/ def renameVarsBuilder (names : Array Name) : EquivalenceBuilder Unit := fun eqvExpr g => do let lhsMinExpr ← eqvExpr.toMinimizationExprLHS let vars ← decomposeDomain (← instantiateMVars eqvExpr.domainLHS) @@ -46,9 +75,10 @@ end Meta namespace Tactic +/-- Tactic to rename all optimization variables given a list of names. This does not change the +mathematical interpretation of the problem. -/ syntax (name := renameVars) "rename_vars" "[" ident,* "]" : tactic -/-- -/ @[tactic renameVars] partial def evalRenameVars : Tactic := fun stx => match stx with | `(tactic| rename_vars [$ids,*]) => do From be1e4ace1a57f6429c2d2bb1c2c6efc83ec58e97 Mon Sep 17 00:00:00 2001 From: Ramon Fernandez Mir Date: Thu, 29 Feb 2024 17:37:58 +0000 Subject: [PATCH 18/25] style: use `throwRenameVarsError` --- CvxLean/Tactic/Basic/RenameVars.lean | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/CvxLean/Tactic/Basic/RenameVars.lean b/CvxLean/Tactic/Basic/RenameVars.lean index d5f59a18..b32eb386 100644 --- a/CvxLean/Tactic/Basic/RenameVars.lean +++ b/CvxLean/Tactic/Basic/RenameVars.lean @@ -59,16 +59,16 @@ def renameVarsBuilder (names : Array Name) : EquivalenceBuilder Unit := fun eqvE objFun := newObjFun, constraints := newConstrs } if !(← isDefEq eqvExpr.rhs rhsMinExpr.toExpr) then - throwError "`rename_vars` error: Failed to unify the goal." + throwRenameVarsError "failed to unify the goal." -- Close goal by reflexivity. if let _ :: _ ← evalTacticAt (← `(tactic| equivalence_rfl)) g then - throwError "`rename_vars` error: Failed to close the goal." + throwRenameVarsError "dailed to close the goal." where manipulateVars : List (Name × Expr) → List Name → MetaM (List (Name × Expr)) | (_, ty) :: vars, newName :: newNames => return (newName, ty) :: (← manipulateVars vars newNames) - | [], _ :: _ => throwError "Too many variable names given" + | [], _ :: _ => throwRenameVarsError "too many variable names given" | vars, [] => return vars end Meta From aa5f495059e5f9c7ae738d34f646b3cfae412197 Mon Sep 17 00:00:00 2001 From: Ramon Fernandez Mir Date: Thu, 29 Feb 2024 17:41:53 +0000 Subject: [PATCH 19/25] doc: reorder constraints --- CvxLean/Tactic/Basic/ReorderConstrs.lean | 49 +++++++++++++++++++----- 1 file changed, 39 insertions(+), 10 deletions(-) diff --git a/CvxLean/Tactic/Basic/ReorderConstrs.lean b/CvxLean/Tactic/Basic/ReorderConstrs.lean index 6b5a9aee..9399db17 100644 --- a/CvxLean/Tactic/Basic/ReorderConstrs.lean +++ b/CvxLean/Tactic/Basic/ReorderConstrs.lean @@ -1,6 +1,32 @@ import CvxLean.Meta.Equivalence import CvxLean.Meta.TacticBuilder +/-! +# Tactic to reorder constraints + +This file defines the `reorder_constrs` tactic. It takes a list of names, e.g., `[c₂, c₁, c₃]`. This +list must be a permutation of the constraint names. + +We illustrate it with an example of how to use it inside the `equivalence` command: +``` +equivalence eqv/q : + optimization (x : ℝ) + minimize x + subject to + c₁ : 1 ≤ x + c₂ : 0 < x := by + reorder_constrs [c₂, c₁] +``` +The resulting problem `q` looks as follows: +``` +optimization (x : ℝ) + minimize x + subject to + c₂ : 0 < x + c₁ : 1 ≤ x +``` +-/ + namespace CvxLean open Lean @@ -9,24 +35,26 @@ namespace Meta open Std Meta Elab Tactic -/-- -/ +/-- Given the constraint expression `e`, look through the names and re-order them according to +`ids`. -/ def reorderConstrsExpr (ids : Array Name) (e : Expr) : MetaM Expr := do let mut constrs : Std.HashMap Lean.Name Expr := {} for (cName, cExpr) in ← decomposeConstraints e do if constrs.contains cName then - throwError "`reorder_constrs` error: Constraint names are not unique: {cName}." + throwReorderConstrsError "constraint names are not unique ({cName})." constrs := constrs.insert cName cExpr let newConstrs ← ids.mapM fun id => do match constrs.find? id with - | none => throwError "`reorder_constrs` error: Unknown constraint: {id}" + | none => throwReorderConstrsError "unknown constraint {id}." | some c => return c if constrs.size < ids.size then - throwError "`reorder_constrs` error: Too many constraints" + throwReorderConstrsError "too many constraints." if ids.size < constrs.size then - throwError "`reorder_constrs` error: Not enough constraints" + throwReorderConstrsError "not enough constraints." return composeAnd newConstrs.data -/-- -/ +/-- Use `reorderConstrsExpr` to obtain the target problem. Then, they should be equivalent by +rewriting together with `tauto`. -/ def reorderConstrsBuilder (ids : Array Name) : EquivalenceBuilder Unit := fun eqvExpr g => g.withContext do let lhsMinExpr ← eqvExpr.toMinimizationExprLHS @@ -36,14 +64,14 @@ def reorderConstrsBuilder (ids : Array Name) : EquivalenceBuilder Unit := fun eq let rhsMinExpr := { lhsMinExpr with constraints := newConstrs } if !(← isDefEq eqvExpr.rhs rhsMinExpr.toExpr) then - throwError "`reorder_constrs` error: Failed to unify the goal." + throwReorderConstrsError "failed to unify the goal." if let [g] ← g.apply (mkConst ``Minimization.Equivalence.rewrite_constraints) then let (_, g) ← g.intros if let _ :: _ ← evalTacticAt (← `(tactic| tauto)) g then - throwError "`reorder_constrs` error: Failed to prove reordering correct." + throwReorderConstrsError "failed to prove reordering correct." else - throwError "`reorder_constrs` error: Failed to rewrite constraints." + throwReorderConstrsError "failed to rewrite constraints." end Meta @@ -51,9 +79,10 @@ namespace Tactic open Elab Tactic Meta +/-- Tactic that takes a permutation of the current constraint names (as a list) and reusults in the +same problem with the constraints re-ordered according to the list given. -/ syntax (name := reorderConstrs) "reorder_constrs" "[" ident,* "]" : tactic -/-- -/ @[tactic reorderConstrs] def evalReorderConstrs : Tactic := fun stx => match stx with | `(tactic| reorder_constrs [$ids,*]) => do From b687e199a49dbc6b873be9e33951c0cfecf91770 Mon Sep 17 00:00:00 2001 From: Ramon Fernandez Mir Date: Fri, 1 Mar 2024 12:23:39 +0000 Subject: [PATCH 20/25] feat: cleaner `equivalence_step`, `reduction_step`, and `relaxation_step` --- CvxLean/Meta/Equivalence.lean | 2 ++ CvxLean/Meta/Reduction.lean | 2 ++ CvxLean/Meta/Relaxation.lean | 2 ++ 3 files changed, 6 insertions(+) diff --git a/CvxLean/Meta/Equivalence.lean b/CvxLean/Meta/Equivalence.lean index 7f3d463e..873c6e8c 100644 --- a/CvxLean/Meta/Equivalence.lean +++ b/CvxLean/Meta/Equivalence.lean @@ -64,6 +64,8 @@ open Parser Elab Tactic elab "equivalence_step" _arr:darrow tac:tacticSeqIndentGt : tactic => do evalTactic <| ← `(tactic| equivalence_trans) evalTacticSeq1Indented tac.raw + evalTactic <| ← `(tactic| equivalence_rfl) + (← getMainGoal).setTag Name.anonymous end BasicTactics diff --git a/CvxLean/Meta/Reduction.lean b/CvxLean/Meta/Reduction.lean index 7430d9a7..0c4734a2 100644 --- a/CvxLean/Meta/Reduction.lean +++ b/CvxLean/Meta/Reduction.lean @@ -59,6 +59,8 @@ open Parser Elab Tactic elab "reduction_step" _arr:darrow tac:tacticSeqIndentGt : tactic => do evalTactic <| ← `(tactic| reduction_trans) evalTacticSeq1Indented tac.raw + evalTactic <| ← `(tactic| reduction_rfl) + (← getMainGoal).setTag Name.anonymous end Meta diff --git a/CvxLean/Meta/Relaxation.lean b/CvxLean/Meta/Relaxation.lean index c3c805b9..57e86391 100644 --- a/CvxLean/Meta/Relaxation.lean +++ b/CvxLean/Meta/Relaxation.lean @@ -59,6 +59,8 @@ open Parser Elab Tactic elab "relaxation_step" _arr:darrow tac:tacticSeqIndentGt : tactic => do evalTactic <| ← `(tactic| relaxation_trans) evalTacticSeq1Indented tac.raw + evalTactic <| ← `(tactic| relaxation_rfl) + (← getMainGoal).setTag Name.anonymous end Meta From 123a1b6eee6542f1ce7c2b90191e35d179fd35bb Mon Sep 17 00:00:00 2001 From: Ramon Fernandez Mir Date: Fri, 1 Mar 2024 12:38:04 +0000 Subject: [PATCH 21/25] fix: correct namespace for `Expr` helper functions --- CvxLean/Meta/Util/Expr.lean | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/CvxLean/Meta/Util/Expr.lean b/CvxLean/Meta/Util/Expr.lean index 0adea040..40c3d9f8 100644 --- a/CvxLean/Meta/Util/Expr.lean +++ b/CvxLean/Meta/Util/Expr.lean @@ -139,15 +139,15 @@ def elabTermAndSynthesizeEnsuringType (stx : Syntax) (expectedType? : Option Exp end Elab.Term /-- Wrapper of `Lean.addAndCompile` for definitions with some default values. -/ -def Lean.simpleAddAndCompileDefn (n : Name) (e : Expr) : MetaM Unit := do - Lean.addAndCompile <| +def simpleAddAndCompileDefn (n : Name) (e : Expr) : MetaM Unit := do + addAndCompile <| Declaration.defnDecl <| mkDefinitionValEx n [] (← inferType e) e (Lean.ReducibilityHints.regular 0) (DefinitionSafety.safe) [] /-- Wrapper of `Lean.addDecl` for definitions with some default values. -/ -def Lean.simpleAddDefn (n : Name) (e : Expr) : MetaM Unit := do - Lean.addDecl <| +def simpleAddDefn (n : Name) (e : Expr) : MetaM Unit := do + addDecl <| Declaration.defnDecl <| mkDefinitionValEx n [] (← inferType e) e (Lean.ReducibilityHints.regular 0) (DefinitionSafety.safe) [] From c0e81fff5dbac58dede075fa1da63756a540317e Mon Sep 17 00:00:00 2001 From: Ramon Fernandez Mir Date: Fri, 1 Mar 2024 13:18:27 +0000 Subject: [PATCH 22/25] fix: do not always try to close by `rfl` on manual steps --- CvxLean/Meta/Equivalence.lean | 3 ++- CvxLean/Meta/Reduction.lean | 3 ++- CvxLean/Meta/Relaxation.lean | 3 ++- 3 files changed, 6 insertions(+), 3 deletions(-) diff --git a/CvxLean/Meta/Equivalence.lean b/CvxLean/Meta/Equivalence.lean index 873c6e8c..b6043a33 100644 --- a/CvxLean/Meta/Equivalence.lean +++ b/CvxLean/Meta/Equivalence.lean @@ -64,7 +64,8 @@ open Parser Elab Tactic elab "equivalence_step" _arr:darrow tac:tacticSeqIndentGt : tactic => do evalTactic <| ← `(tactic| equivalence_trans) evalTacticSeq1Indented tac.raw - evalTactic <| ← `(tactic| equivalence_rfl) + if (← getGoals).length > 1 then + evalTactic <| ← `(tactic| try { equivalence_rfl }) (← getMainGoal).setTag Name.anonymous end BasicTactics diff --git a/CvxLean/Meta/Reduction.lean b/CvxLean/Meta/Reduction.lean index 0c4734a2..02162367 100644 --- a/CvxLean/Meta/Reduction.lean +++ b/CvxLean/Meta/Reduction.lean @@ -59,7 +59,8 @@ open Parser Elab Tactic elab "reduction_step" _arr:darrow tac:tacticSeqIndentGt : tactic => do evalTactic <| ← `(tactic| reduction_trans) evalTacticSeq1Indented tac.raw - evalTactic <| ← `(tactic| reduction_rfl) + if (← getGoals).length > 1 then + evalTactic <| ← `(tactic| try { reduction_rfl }) (← getMainGoal).setTag Name.anonymous end Meta diff --git a/CvxLean/Meta/Relaxation.lean b/CvxLean/Meta/Relaxation.lean index 57e86391..c5569a5a 100644 --- a/CvxLean/Meta/Relaxation.lean +++ b/CvxLean/Meta/Relaxation.lean @@ -59,7 +59,8 @@ open Parser Elab Tactic elab "relaxation_step" _arr:darrow tac:tacticSeqIndentGt : tactic => do evalTactic <| ← `(tactic| relaxation_trans) evalTacticSeq1Indented tac.raw - evalTactic <| ← `(tactic| relaxation_rfl) + if (← getGoals).length > 1 then + evalTactic <| ← `(tactic| try { relaxation_rfl }) (← getMainGoal).setTag Name.anonymous end Meta From cb56a662a02dd2ff34b81fe9b6e8b8d00de105e1 Mon Sep 17 00:00:00 2001 From: Ramon Fernandez Mir Date: Fri, 1 Mar 2024 13:21:22 +0000 Subject: [PATCH 23/25] refactor: `reduction'` -> `reduction*` --- CvxLean/Command/Reduction.lean | 6 +++--- CvxLean/Examples/CovarianceEstimation.lean | 2 +- 2 files changed, 4 insertions(+), 4 deletions(-) diff --git a/CvxLean/Command/Reduction.lean b/CvxLean/Command/Reduction.lean index 96dba4b0..3ede515d 100644 --- a/CvxLean/Command/Reduction.lean +++ b/CvxLean/Command/Reduction.lean @@ -24,7 +24,7 @@ environment: * `q := r`, * `red : p ≼ q`. -Writing `reduction'` instead of `reduction` will also generate a backward solution map at the +Writing `reduction*` instead of `reduction` will also generate a backward solution map at the level of floats. It is essentially the same as `CvxLean/Command/Equivalence.lean`, except that the goal is to prove a @@ -51,7 +51,7 @@ syntax (name := reduction) /-- Open a reduction environment and try to generate a computable backward map. -/ syntax (name := reductionAndBwdMap) - "reduction'" ident "/" ident declSig ":=" Lean.Parser.Term.byTactic : command + "reduction*" ident "/" ident declSig ":=" Lean.Parser.Term.byTactic : command /-- Open a reduction environment with a given left-hand-side problem (`lhsStx`) and perhaps some parameters (`xs`). From this, a reduction goal is set to a target problem which is represented by a @@ -150,7 +150,7 @@ def evalReduction : CommandElab := fun stx => match stx with /-- Same as `reduction` but also adds the backward map to the environment. -/ @[command_elab «reductionAndBwdMap»] def evalReductionAndBwdMap : CommandElab := fun stx => match stx with - | `(reduction' $eqvId / $probId $declSig := $proofStx) => do + | `(reduction* $eqvId / $probId $declSig := $proofStx) => do liftTermElabM do let (binders, lhsStx) := expandDeclSig declSig.raw elabBindersEx binders.getArgs fun xs => diff --git a/CvxLean/Examples/CovarianceEstimation.lean b/CvxLean/Examples/CovarianceEstimation.lean index 57019169..cf2ca3e3 100644 --- a/CvxLean/Examples/CovarianceEstimation.lean +++ b/CvxLean/Examples/CovarianceEstimation.lean @@ -17,7 +17,7 @@ noncomputable def covEstimation (n : ℕ) (N : ℕ) (α : ℝ) (y : Fin N → Fi c_pos_def : R.PosDef c_sparse : R⁻¹.abs.sum ≤ α -reduction' red/covEstimationConvex (n : ℕ) (N : ℕ) (α : ℝ) (y : Fin N → Fin n → ℝ) : +reduction* red/covEstimationConvex (n : ℕ) (N : ℕ) (α : ℝ) (y : Fin N → Fin n → ℝ) : covEstimation n N α y := by -- Change objective function. reduction_step => From fce0b0036bbd9b70b8d8e8ea3d3dcdd67656d328 Mon Sep 17 00:00:00 2001 From: Ramon Fernandez Mir Date: Fri, 1 Mar 2024 13:25:30 +0000 Subject: [PATCH 24/25] style: tag definition with `reducible` not `simp` --- CvxLean/Examples/VehicleSpeedScheduling.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/CvxLean/Examples/VehicleSpeedScheduling.lean b/CvxLean/Examples/VehicleSpeedScheduling.lean index 19ff3d5d..9d36e319 100644 --- a/CvxLean/Examples/VehicleSpeedScheduling.lean +++ b/CvxLean/Examples/VehicleSpeedScheduling.lean @@ -165,7 +165,7 @@ def τminₚ : Fin nₚ → ℝ := def τmaxₚ : Fin nₚ → ℝ := ![4.6528, 6.5147, 7.5178, 9.7478, 9.0641, 10.3891, 13.1540, 16.0878, 17.4352, 20.9539] -@[optimization_param, simp] +@[optimization_param, reducible] def sminₚ : Fin nₚ → ℝ := ![0.7828, 0.6235, 0.7155, 0.5340, 0.6329, 0.4259, 0.7798, 0.9604, 0.7298, 0.8405] From e2052f890f8ac96de315812b58972b4eb1a58ab8 Mon Sep 17 00:00:00 2001 From: Ramon Fernandez Mir Date: Fri, 1 Mar 2024 13:54:45 +0000 Subject: [PATCH 25/25] refactor: DCP canonization not reduction --- CvxLean/Command/Solve.lean | 30 +-- CvxLean/Demos/LT2024.lean | 4 +- CvxLean/Examples/CovarianceEstimation.lean | 2 +- CvxLean/Examples/HypersonicShapeDesign.lean | 4 +- CvxLean/Examples/VehicleSpeedScheduling.lean | 4 +- CvxLean/Tactic/DCP/AtomCmd.lean | 68 +++---- CvxLean/Tactic/DCP/DCP.lean | 194 +++++++++---------- CvxLean/Tactic/PreDCP/PreDCP.lean | 2 +- CvxLean/Test/PreDCP/DQCP.lean | 24 +-- CvxLean/Test/PreDCP/MainExample.lean | 2 +- CvxLean/Test/Solve/Problems/Exp.lean | 4 +- CvxLean/Test/Solve/Problems/Linear.lean | 10 +- CvxLean/Test/Solve/Problems/Log.lean | 12 +- CvxLean/Test/Solve/Problems/LogDet.lean | 2 +- CvxLean/Test/Solve/Problems/SDP.lean | 2 +- CvxLean/Test/Solve/Problems/SO.lean | 4 +- README.md | 4 +- 17 files changed, 186 insertions(+), 186 deletions(-) diff --git a/CvxLean/Command/Solve.lean b/CvxLean/Command/Solve.lean index 6481dfaf..171ba549 100644 --- a/CvxLean/Command/Solve.lean +++ b/CvxLean/Command/Solve.lean @@ -6,7 +6,7 @@ import CvxLean.Command.Solve.Conic Given a problem `p : Minimization D R` a user can call `solve p` to call an external solver and obtain a result. If successful, three new definitions are added to the environment: -* `p.reduced : Minimization (D × E) R` is the problem in conic form. +* `p.conicForm : Minimization (D × E) R` is the problem in conic form. * `p.status : String` is the status of the solution. * `p.solution : D` is the solution to the problem. * `p.value : R` is the value of the solution. @@ -32,16 +32,16 @@ def getProblemName (stx : Syntax) : MetaM Name := do /-- Call DCP and get the problem in conic form as well as `ψ`, the backward map from the equivalence. -/ -def getReducedProblemAndBwdMap (prob : Expr) : MetaM (MinimizationExpr × Expr) := do +def getCanonizedProblemAndBwdMap (prob : Expr) : MetaM (MinimizationExpr × Expr) := do let ogProb ← MinimizationExpr.fromExpr prob - let (redProb, eqvProof) ← DCP.canonize ogProb + let (canonProb, eqvProof) ← DCP.canonize ogProb let backwardMap ← mkAppM ``Minimization.Equivalence.psi #[eqvProof] - return (redProb, backwardMap) + return (canonProb, backwardMap) syntax (name := solve) "solve " term : command /-- The `solve` command. It works as follows: -1. Reduce optimization problem to conic form. +1. Canonize optimization problem to conic form. 2. Extract problem data using `determineCoeffsFromExpr`. 3. Obtain a solution using `solutionDataFromProblemData`, which calls an external solver. 4. Store the result in the enviroment. -/ @@ -61,19 +61,19 @@ unsafe def evalSolve : CommandElab := fun stx => mvarId.assign mvarVal } catch _ => pure () - -- Create prob.reduced. - let (redProb, backwardMap) ← getReducedProblemAndBwdMap probTerm - let redProbExpr := redProb.toExpr + -- Create prob.conicForm. + let (canonProb, backwardMap) ← getCanonizedProblemAndBwdMap probTerm + let canonProbExpr := canonProb.toExpr let probName ← getProblemName probInstance.raw - simpleAddDefn (probName ++ `reduced) redProbExpr + simpleAddDefn (probName ++ `conicForm) canonProbExpr - -- Call the solver on prob.reduced and get a point in E. - let (coeffsData, sections) ← determineCoeffsFromExpr redProb + -- Call the solver on prob.conicForm and get a point in E. + let (coeffsData, sections) ← determineCoeffsFromExpr canonProb trace[CvxLean.debug] "Coeffs data:\n{coeffsData}" - let solData ← solutionDataFromProblemData redProb coeffsData sections + let solData ← solutionDataFromProblemData canonProb coeffsData sections trace[CvxLean.debug] "Solution data:\n{solData}" -- Add status to the environment. @@ -84,8 +84,8 @@ unsafe def evalSolve : CommandElab := fun stx => pure () -- Solution makes sense, handle the numerical solution. - let solPointExpr ← exprFromSolutionData redProb solData - trace[CvxLean.debug] "Solution point (reduced problem): {solPointExpr}" + let solPointExpr ← exprFromSolutionData canonProb solData + trace[CvxLean.debug] "Solution point (canonized problem): {solPointExpr}" let backwardMapFloat ← realToFloat <| ← whnf backwardMap let solPointExprFloat ← realToFloat solPointExpr @@ -97,7 +97,7 @@ unsafe def evalSolve : CommandElab := fun stx => simpleAddAndCompileDefn (probName ++ `solution) probSolPointFloat -- Also add value of optimal point. - let probSolValue := mkApp redProb.objFun solPointExpr + let probSolValue := mkApp canonProb.objFun solPointExpr let probSolValueFloat ← realToFloat probSolValue check probSolValueFloat diff --git a/CvxLean/Demos/LT2024.lean b/CvxLean/Demos/LT2024.lean index a47c050b..742b94a8 100644 --- a/CvxLean/Demos/LT2024.lean +++ b/CvxLean/Demos/LT2024.lean @@ -45,7 +45,7 @@ equivalence eqv₂/q₂ : p₂ := by solve q₂ -#print q₂.reduced +#print q₂.conicForm #eval q₂.status #eval q₂.solution @@ -81,7 +81,7 @@ equivalence* eqv₃/q₃ : p₃ 100 10 0.5 2 0.5 2 := by solve q₃ -#print q₃.reduced +#print q₃.conicForm #eval q₃.status #eval q₃.solution diff --git a/CvxLean/Examples/CovarianceEstimation.lean b/CvxLean/Examples/CovarianceEstimation.lean index cf2ca3e3..97940e8a 100644 --- a/CvxLean/Examples/CovarianceEstimation.lean +++ b/CvxLean/Examples/CovarianceEstimation.lean @@ -86,7 +86,7 @@ def yₚ : Fin Nₚ → Fin nₚ → ℝ := ![![0, 2], ![2, 0], ![-2, 0], ![0, - solve covEstimationConvex nₚ Nₚ αₚ yₚ -#print covEstimationConvex.reduced +#print covEstimationConvex.conicForm -- minimize -- -(-(Nₚ • log (sqrt ((2 * π) ^ nₚ)) + Nₚ • (-Vec.sum t.0 / 2)) + -- -(↑Nₚ * trace ((covarianceMatrix fun i => yₚ i) * Rᵀ) / 2)) diff --git a/CvxLean/Examples/HypersonicShapeDesign.lean b/CvxLean/Examples/HypersonicShapeDesign.lean index 15c2e4d1..90e401e9 100644 --- a/CvxLean/Examples/HypersonicShapeDesign.lean +++ b/CvxLean/Examples/HypersonicShapeDesign.lean @@ -61,7 +61,7 @@ lemma one_sub_bₚ_nonneg : 0 ≤ 1 - bₚ := by time_cmd solve hypersonicShapeDesignConvex aₚ bₚ aₚ_nonneg bₚ_nonneg bₚ_lt_one -#print hypersonicShapeDesignConvex.reduced +#print hypersonicShapeDesignConvex.conicForm -- Final width of wedge. def wₚ_opt := eqv₁.backward_map aₚ.float bₚ.float hypersonicShapeDesignConvex.solution @@ -116,7 +116,7 @@ equivalence* eqv₂/hypersonicShapeDesignSimpler (a b : ℝ) (ha : 0 ≤ a) (hb time_cmd solve hypersonicShapeDesignSimpler aₚ bₚ aₚ_nonneg bₚ_nonneg bₚ_lt_one -#print hypersonicShapeDesignSimpler.reduced +#print hypersonicShapeDesignSimpler.conicForm -- Final width of wedge. def wₚ'_opt := diff --git a/CvxLean/Examples/VehicleSpeedScheduling.lean b/CvxLean/Examples/VehicleSpeedScheduling.lean index 9d36e319..463c7271 100644 --- a/CvxLean/Examples/VehicleSpeedScheduling.lean +++ b/CvxLean/Examples/VehicleSpeedScheduling.lean @@ -93,10 +93,10 @@ equivalence* eqv₁/vehSpeedSchedConvex (n : ℕ) (d : Fin n → ℝ) -- The problem is technically in DCP form if `F` is DCP convex. The only issue is that we do not -- have an atom for the perspective function, so the objective function --- `Vec.sum (t * Vec.map F (d / t))` cannot be reduced directly. +-- `Vec.sum (t * Vec.map F (d / t))` cannot be canonized directly. -- However, if we fix `F`, we can use other atoms. For example, if `F` is quadratic, the problem can --- be reduced. Let `F(s) = a * s^2 + b * s + c` with `0 ≤ a`. +-- be canonized. Let `F(s) = a * s^2 + b * s + c` with `0 ≤ a`. equivalence* eqv₂/vehSpeedSchedQuadratic (n : ℕ) (d : Fin n → ℝ) (τmin τmax smin smax : Fin n → ℝ) (a b c : ℝ) (h_n_pos : 0 < n) (h_d_pos : StrongLT 0 d) diff --git a/CvxLean/Tactic/DCP/AtomCmd.lean b/CvxLean/Tactic/DCP/AtomCmd.lean index a3485367..7a099462 100644 --- a/CvxLean/Tactic/DCP/AtomCmd.lean +++ b/CvxLean/Tactic/DCP/AtomCmd.lean @@ -91,9 +91,9 @@ def getMonoArgsCount (curv : Curvature) (argKinds : Array ArgKind) : ℕ := | Curvature.Convex => 1 + acc | _ => acc) 0 -/-- Use the DCP procedure to reduce the graph implementation to a problem that +/-- Use the DCP procedure to canon the graph implementation to a problem that uses only cone constraints and affine atoms. -/ -def reduceAtomData (objCurv : Curvature) (atomData : GraphAtomData) : CommandElabM GraphAtomData := do +def canonAtomData (objCurv : Curvature) (atomData : GraphAtomData) : CommandElabM GraphAtomData := do liftTermElabM do -- `xs` are the arguments of the atom. lambdaTelescope atomData.expr fun xs atomExpr => do @@ -149,7 +149,7 @@ def reduceAtomData (objCurv : Curvature) (atomData : GraphAtomData) : CommandEla for c in pat.optimality.constr.map Tree.val do trace[Meta.debug] "pat opt constr: {c}" check c - -- `vs1` are the variables already present in the unreduced graph implementation. + -- `vs1` are the variables already present in the uncanon graph implementation. let vs1 := originalVarsDecls.map (mkFVar ·.fvarId) -- `vs2` are the variables to be added to the graph implementation. let vs2 := pat.newVarDecls.toArray.map (mkFVar ·.fvarId) @@ -160,8 +160,8 @@ def reduceAtomData (objCurv : Curvature) (atomData : GraphAtomData) : CommandEla trace[Meta.debug] "xs: {xs}" -- TODO: move because copied from DCP tactic. - let reducedConstrs := pat.reducedExprs.constr.map Tree.val - let reducedConstrs := reducedConstrs.filterIdx (fun i => ¬ pat.isVCond[i]!) + let canonConstrs := pat.canonExprs.constr.map Tree.val + let canonConstrs := canonConstrs.filterIdx (fun i => ¬ pat.isVCond[i]!) -- TODO: move because copied from DCP tactic. let newConstrProofs := pat.feasibility.fold #[] fun acc fs => @@ -219,18 +219,18 @@ def reduceAtomData (objCurv : Curvature) (atomData : GraphAtomData) : CommandEla for nf in newFeasibility do trace[Meta.debug] "newFeasibility: {← inferType nf}" - let constraintsFromReducedConstraints := + let constraintsFromCanonConstraints := pat.optimality.constr.map Tree.val - for cfrc in constraintsFromReducedConstraints do - trace[Meta.debug] "constraintsFromReducedConstraints: {← inferType cfrc}" + for cfrc in constraintsFromCanonConstraints do + trace[Meta.debug] "constraintsFromCanonConstraints: {← inferType cfrc}" - if reducedConstrs.size != constraintsFromReducedConstraints.size then - throwError ("Expected same length: {reducedConstrs} and " ++ - "{constraintsFromReducedConstraints}") + if canonConstrs.size != constraintsFromCanonConstraints.size then + throwError ("Expected same length: {canonConstrs} and " ++ + "{constraintsFromCanonConstraints}") - let objFunFromReducedObjFun := pat.optimality.objFun.val - trace[Meta.debug] "objFunFromReducedObjFun: {← inferType objFunFromReducedObjFun}" + let objFunFromCanonObjFun := pat.optimality.objFun.val + trace[Meta.debug] "objFunFromCanonObjFun: {← inferType objFunFromCanonObjFun}" trace[Meta.debug] "pat.optimality.objFun: {← inferType atomData.optimality}" @@ -238,18 +238,18 @@ def reduceAtomData (objCurv : Curvature) (atomData : GraphAtomData) : CommandEla withLocalDeclsDNondep bconds fun bs => do let optimalityXsBConds := mkAppN atomData.optimality (xs ++ bs ++ vs1) trace[Meta.debug] "newOptimality: {← inferType optimalityXsBConds}" - withLocalDeclsDNondep (reducedConstrs.map (fun rc => (`_, rc))) fun cs => do + withLocalDeclsDNondep (canonConstrs.map (fun rc => (`_, rc))) fun cs => do -- First, apply all constraints. - let mut optimalityAfterReduced := optimalityXsBConds - for i in [:reducedConstrs.size] do - trace[Meta.debug] "optimalityAfterReduced: {← inferType optimalityAfterReduced}" - let c := mkApp constraintsFromReducedConstraints[i]! cs[i]! - optimalityAfterReduced := mkApp optimalityAfterReduced c - -- Then, adjust the condition using `objFunFromReducedObjFun`. - trace[Meta.debug] "optimalityAfterReduced: {← inferType optimalityAfterReduced}" + let mut optimalityAfterCanon := optimalityXsBConds + for i in [:canonConstrs.size] do + trace[Meta.debug] "optimalityAfterCanon: {← inferType optimalityAfterCanon}" + let c := mkApp constraintsFromCanonConstraints[i]! cs[i]! + optimalityAfterCanon := mkApp optimalityAfterCanon c + -- Then, adjust the condition using `objFunFromCanonObjFun`. + trace[Meta.debug] "optimalityAfterCanon: {← inferType optimalityAfterCanon}" let monoArgsCount := getMonoArgsCount objCurv atomData.argKinds let optimalityAfterApplyWithConditionAdjusted ← - lambdaTelescope (← whnf optimalityAfterReduced) <| fun xs e => do + lambdaTelescope (← whnf optimalityAfterCanon) <| fun xs e => do -- Every extra argument has an extra condition, e.g. x', x ≤ x. trace[Meta.debug] "xs: {xs}" let monoArgs := xs[:2 * monoArgsCount] @@ -260,16 +260,16 @@ def reduceAtomData (objCurv : Curvature) (atomData : GraphAtomData) : CommandEla if atomData.curvature == Curvature.Convex then mkAppOptM ``le_trans #[ atomRange, none, none, none, none, - optCondition, objFunFromReducedObjFun] + optCondition, objFunFromCanonObjFun] else -- TODO: concave. but convex_set too? mkAppOptM ``le_trans #[ atomRange, none, none, none, none, - objFunFromReducedObjFun, optCondition] + objFunFromCanonObjFun, optCondition] mkLambdaFVars monoArgs newCond trace[Meta.debug] "optimalityAfterApplyWithConditionAdjusted: {← inferType optimalityAfterApplyWithConditionAdjusted}" - trace[Meta.debug] "newOptimality applied: {← inferType optimalityAfterReduced}" + trace[Meta.debug] "newOptimality applied: {← inferType optimalityAfterCanon}" let ds := pat.newConstrVarsArray.map (mkFVar ·.fvarId) mkLambdaFVars (xs ++ bs ++ vs1 ++ vs2 ++ cs ++ ds) optimalityAfterApplyWithConditionAdjusted @@ -279,10 +279,10 @@ def reduceAtomData (objCurv : Curvature) (atomData : GraphAtomData) : CommandEla for vcondElim in atomData.vcondElim do let newVCondElim := mkAppN vcondElim (xs ++ vs1) let newVCondElim ← - withLocalDeclsDNondep (reducedConstrs.map (fun rc => (`_, rc))) fun cs => do + withLocalDeclsDNondep (canonConstrs.map (fun rc => (`_, rc))) fun cs => do let mut newVCondElim := newVCondElim - for i in [:reducedConstrs.size] do - let c := mkApp constraintsFromReducedConstraints[i]! cs[i]! + for i in [:canonConstrs.size] do + let c := mkApp constraintsFromCanonConstraints[i]! cs[i]! newVCondElim := mkApp newVCondElim c let ds := pat.newConstrVarsArray.map (mkFVar ·.fvarId) mkLambdaFVars (xs ++ vs1 ++ vs2) <| ← mkLambdaFVars (cs ++ ds) newVCondElim @@ -293,8 +293,8 @@ def reduceAtomData (objCurv : Curvature) (atomData : GraphAtomData) : CommandEla (← pat.newVarDecls.toArray.mapM fun decl => do return (decl.userName, ← mkLambdaFVars xs decl.type)) impObjFun := ← mkLambdaFVars xs $ ← mkLambdaFVars (vs1 ++ vs2) $ - pat.reducedExprs.objFun.val - impConstrs := ← (reducedConstrs ++ pat.newConstrs).mapM + pat.canonExprs.objFun.val + impConstrs := ← (canonConstrs ++ pat.newConstrs).mapM (fun c => do withLocalDeclsDNondep bconds fun bs => do return ← mkLambdaFVars xs <| ← mkLambdaFVars bs <| ← mkLambdaFVars (vs1 ++ vs2) c) @@ -600,10 +600,10 @@ def elabVCondElim (curv : Curvature) (argDecls : Array LocalDecl) (bconds vconds -- | Curvature.ConvexSet => Curvature.ConvexSet -- | _ => Curvature.Affine - trace[Meta.debug] "before reduce sol eq atom: {atomData.solEqAtom}" + trace[Meta.debug] "before canon sol eq atom: {atomData.solEqAtom}" - let atomData ← reduceAtomData objCurv atomData - -- trace[Meta.debug] "HERE Reduced atom: {atomData}" + let atomData ← canonAtomData objCurv atomData + -- trace[Meta.debug] "HERE Canon atom: {atomData}" let atomData ← addAtomDataDecls id.getId atomData -- trace[Meta.debug] "HERE Added atom" @@ -659,7 +659,7 @@ def elabVCondElim (curv : Curvature) (argDecls : Array LocalDecl) (bconds vconds } return atomData - let atomData ← reduceAtomData atomData.curvature atomData--Curvature.Affine atomData + let atomData ← canonAtomData atomData.curvature atomData--Curvature.Affine atomData let atomData ← addAtomDataDecls id.getId atomData liftTermElabM do diff --git a/CvxLean/Tactic/DCP/DCP.lean b/CvxLean/Tactic/DCP/DCP.lean index e072682e..99561821 100644 --- a/CvxLean/Tactic/DCP/DCP.lean +++ b/CvxLean/Tactic/DCP/DCP.lean @@ -190,19 +190,19 @@ def mkNewVarDeclList (newVars : OC NewVarsTree) : newVarDecls := t.fold newVarDecls Array.append return newVarDecls.toList -abbrev ReducedExpr := Expr -abbrev ReducedExprsTree := Tree ReducedExpr ReducedExpr +abbrev CanonExpr := Expr +abbrev CanonExprsTree := Tree CanonExpr CanonExpr /-- -/ -partial def mkReducedExprs : GraphAtomDataTree → NewVarsTree → MetaM (Tree Expr Expr) +partial def mkCanonExprs : GraphAtomDataTree → NewVarsTree → MetaM (Tree Expr Expr) | Tree.node atom childAtoms, Tree.node newVars childNewVars => do - let mut childReducedExprs := #[] + let mut childCanonExprs := #[] for i in [:childAtoms.size] do - childReducedExprs := childReducedExprs.push $ ← mkReducedExprs childAtoms[i]! childNewVars[i]! - let reducedExpr := atom.impObjFun - let reducedExpr := mkAppNBeta reducedExpr (childReducedExprs.map (·.val)) - let reducedExpr := mkAppNBeta reducedExpr (newVars.map (mkFVar ·.fvarId)) - return Tree.node reducedExpr childReducedExprs + childCanonExprs := childCanonExprs.push $ ← mkCanonExprs childAtoms[i]! childNewVars[i]! + let canonExpr := atom.impObjFun + let canonExpr := mkAppNBeta canonExpr (childCanonExprs.map (·.val)) + let canonExpr := mkAppNBeta canonExpr (newVars.map (mkFVar ·.fvarId)) + return Tree.node canonExpr childCanonExprs | Tree.leaf e, Tree.leaf () => pure $ Tree.leaf e | _, _ => throwError "Tree mismatch" @@ -217,13 +217,13 @@ abbrev VConds := Array VCond abbrev VCondsTree := Tree VConds Unit /-- -/ -partial def mkNewConstrs : GraphAtomDataTree → BCondsTree → NewVarsTree → ReducedExprsTree → MetaM NewConstrsTree - | Tree.node atom childAtoms, Tree.node bconds childBConds, Tree.node newVars childNewVars, Tree.node reducedExprs childReducedExprs => do +partial def mkNewConstrs : GraphAtomDataTree → BCondsTree → NewVarsTree → CanonExprsTree → MetaM NewConstrsTree + | Tree.node atom childAtoms, Tree.node bconds childBConds, Tree.node newVars childNewVars, Tree.node canonExprs childCanonExprs => do let mut childNewConstrs := #[] for i in [:childAtoms.size] do - childNewConstrs := childNewConstrs.push <| ← mkNewConstrs childAtoms[i]! childBConds[i]! childNewVars[i]! childReducedExprs[i]! + childNewConstrs := childNewConstrs.push <| ← mkNewConstrs childAtoms[i]! childBConds[i]! childNewVars[i]! childCanonExprs[i]! let newConstrs := atom.impConstrs - let newConstrs := newConstrs.map (mkAppNBeta · (childReducedExprs.map Tree.val)) + let newConstrs := newConstrs.map (mkAppNBeta · (childCanonExprs.map Tree.val)) let newConstrs := newConstrs.map (mkAppNBeta · bconds) let newConstrs := newConstrs.map (mkAppNBeta · (newVars.map (mkFVar ·.fvarId))) return Tree.node newConstrs childNewConstrs @@ -273,36 +273,36 @@ abbrev NewVarAssignment := Expr abbrev Solution := Array NewVarAssignment -structure ReducedExprWithSolution where - reducedExpr : ReducedExpr +structure CanonExprWithSolution where + canonExpr : CanonExpr solution : Solution -instance : Inhabited ReducedExprWithSolution := ⟨⟨default, default⟩⟩ +instance : Inhabited CanonExprWithSolution := ⟨⟨default, default⟩⟩ -abbrev ReducedExprsWithSolutionTree := Tree ReducedExprWithSolution ReducedExprWithSolution +abbrev CanonExprsWithSolutionTree := Tree CanonExprWithSolution CanonExprWithSolution -/-- Returns the reduced expression and an array of forward images of new vars -/ -partial def mkReducedWithSolution : GraphAtomDataTree → MetaM ReducedExprsWithSolutionTree +/-- Returns the canon expression and an array of forward images of new vars -/ +partial def mkCanonWithSolution : GraphAtomDataTree → MetaM CanonExprsWithSolutionTree | Tree.node atom childAtoms => do - let mut childReducedExprs := #[] + let mut childCanonExprs := #[] for i in [:childAtoms.size] do - childReducedExprs := childReducedExprs.push $ ← mkReducedWithSolution childAtoms[i]! - let sols := (atom.solution.map (mkAppNBeta · (childReducedExprs.1.map (·.val.1)).toArray)) - let reducedExpr := atom.impObjFun - let reducedExpr := mkAppNBeta reducedExpr (childReducedExprs.1.map (·.val.1)).toArray - let reducedExpr := mkAppNBeta reducedExpr sols - return Tree.node ⟨reducedExpr, sols⟩ childReducedExprs + childCanonExprs := childCanonExprs.push $ ← mkCanonWithSolution childAtoms[i]! + let sols := (atom.solution.map (mkAppNBeta · (childCanonExprs.1.map (·.val.1)).toArray)) + let canonExpr := atom.impObjFun + let canonExpr := mkAppNBeta canonExpr (childCanonExprs.1.map (·.val.1)).toArray + let canonExpr := mkAppNBeta canonExpr sols + return Tree.node ⟨canonExpr, sols⟩ childCanonExprs | Tree.leaf e => return Tree.leaf ⟨e, #[]⟩ /-- Combine all the solutions introduced by every atom expansion. A solution tells us how to assign new variables from old ones. Here, we collect all such assignments, which will be used later on to build the forward map between the -original and reduced problems. -/ -def mkForwardImagesNewVars (reducedWithSolution : OC ReducedExprsWithSolutionTree) : MetaM Solution := do - let reducedWithSolutionTrees := #[reducedWithSolution.objFun] ++ reducedWithSolution.constr +original and canon problems. -/ +def mkForwardImagesNewVars (canonWithSolution : OC CanonExprsWithSolutionTree) : MetaM Solution := do + let canonWithSolutionTrees := #[canonWithSolution.objFun] ++ canonWithSolution.constr let mut fm := #[] - for t in reducedWithSolutionTrees do + for t in canonWithSolutionTrees do fm := t.fold fm (fun acc a => Array.append acc a.solution) trace[Meta.debug] "forwardImagesNewVars {fm}" return fm @@ -313,17 +313,17 @@ abbrev SolEqAtomProofsTree := Tree SolEqAtomProof SolEqAtomProof /-- Proofs .-/ partial def mkSolEqAtom : GraphAtomDataTree → - ReducedExprsWithSolutionTree → + CanonExprsWithSolutionTree → VCondsTree → MetaM SolEqAtomProofsTree | Tree.node atom childAtoms, - Tree.node reducedWithSolution childReducedWithSolution, + Tree.node canonWithSolution childCanonWithSolution, Tree.node vcondVars childVCondVars => do -- Recursive calls for arguments. let mut childSolEqAtom := #[] for i in [:childAtoms.size] do childSolEqAtom := childSolEqAtom.push <| - ← mkSolEqAtom childAtoms[i]! childReducedWithSolution[i]! childVCondVars[i]! + ← mkSolEqAtom childAtoms[i]! childCanonWithSolution[i]! childVCondVars[i]! -- Rewrite arguments in atom expr. let mut solEqAtomR ← mkEqRefl atom.expr for c in childSolEqAtom do @@ -331,13 +331,13 @@ partial def mkSolEqAtom : -- Use solEqAtom of children to rewrite the arguments in the vconditions. let mut vconds := #[] for i in [:vcondVars.size] do - let mut vcondEqReducedVCond ← mkEqRefl atom.vconds[i]!.2 + let mut vcondEqCanonVCond ← mkEqRefl atom.vconds[i]!.2 for c in childSolEqAtom do - vcondEqReducedVCond ← mkCongr vcondEqReducedVCond c.val - vconds := vconds.push $ ← mkEqMPR vcondEqReducedVCond vcondVars[i]! + vcondEqCanonVCond ← mkCongr vcondEqCanonVCond c.val + vconds := vconds.push $ ← mkEqMPR vcondEqCanonVCond vcondVars[i]! -- Apply solEqAtom property of the atom. let solEqAtomL := atom.solEqAtom - let solEqAtomL := mkAppN solEqAtomL (childReducedWithSolution.map (·.val.1)) + let solEqAtomL := mkAppN solEqAtomL (childCanonWithSolution.map (·.val.1)) let solEqAtomL := mkAppN solEqAtomL vconds let solEqAtom ← mkEqTrans solEqAtomL solEqAtomR return Tree.node solEqAtom childSolEqAtom @@ -353,31 +353,31 @@ abbrev FeasibilityProofsTree := Tree FeasibilityProofs Unit /-- -/ partial def mkFeasibility : GraphAtomDataTree → - ReducedExprsWithSolutionTree → + CanonExprsWithSolutionTree → BCondsTree → VCondsTree → SolEqAtomProofsTree → MetaM FeasibilityProofsTree | Tree.node atom childAtoms, - Tree.node _reducedWithSolution childReducedWithSolution, + Tree.node _canonWithSolution childCanonWithSolution, Tree.node bconds childBConds, Tree.node vcondVars childVCondVars, Tree.node _solEqAtom childSolEqAtom => do -- Recursive calls for arguments. let mut childFeasibility := #[] for i in [:childAtoms.size] do - let c ← mkFeasibility childAtoms[i]! childReducedWithSolution[i]! childBConds[i]! childVCondVars[i]! childSolEqAtom[i]! + let c ← mkFeasibility childAtoms[i]! childCanonWithSolution[i]! childBConds[i]! childVCondVars[i]! childSolEqAtom[i]! childFeasibility := childFeasibility.push c -- Use solEqAtom of children to rewrite the arguments in the vconditions. let mut vconds := #[] for i in [:vcondVars.size] do - let mut vcondEqReducedVCond ← mkEqRefl atom.vconds[i]!.2 + let mut vcondEqCanonVCond ← mkEqRefl atom.vconds[i]!.2 for c in childSolEqAtom do - vcondEqReducedVCond ← mkCongr vcondEqReducedVCond c.val - vconds := vconds.push $ ← mkEqMPR vcondEqReducedVCond vcondVars[i]! + vcondEqCanonVCond ← mkCongr vcondEqCanonVCond c.val + vconds := vconds.push $ ← mkEqMPR vcondEqCanonVCond vcondVars[i]! -- Apply feasibility property of the atom. let feasibility := atom.feasibility - let feasibility := feasibility.map (mkAppN · (childReducedWithSolution.map (·.val.1))) + let feasibility := feasibility.map (mkAppN · (childCanonWithSolution.map (·.val.1))) let feasibility := feasibility.map (mkAppN · bconds) let feasibility := feasibility.map (mkAppN · vconds) let _ ← feasibility.mapM check @@ -411,7 +411,7 @@ abbrev OptimalityAndVCondElimProofsTree := Tree OptimalityAndVCondElimProofs Opt partial def mkOptimalityAndVCondElim : GraphAtomDataTree → ArgumentsTree → - ReducedExprsTree → + CanonExprsTree → NewVarsTree → NewConstrVarsTree → CurvatureTree → @@ -419,7 +419,7 @@ partial def mkOptimalityAndVCondElim : MetaM OptimalityAndVCondElimProofsTree | Tree.node atom childAtoms, Tree.node args childArgs, - Tree.node _reducedExpr childReducedExpr, + Tree.node _canonExpr childCanonExpr, Tree.node newVars childNewVars, Tree.node newConstrVars childNewConstrVars, Tree.node curvature childCurvature, @@ -429,7 +429,7 @@ partial def mkOptimalityAndVCondElim : let mut childOptimalityFiltered := #[] for i in [:childAtoms.size] do if atom.argKinds[i]! != ArgKind.Constant ∧ atom.argKinds[i]! != ArgKind.Neither then - let opt ← mkOptimalityAndVCondElim childAtoms[i]! childArgs[i]! childReducedExpr[i]! + let opt ← mkOptimalityAndVCondElim childAtoms[i]! childArgs[i]! childCanonExpr[i]! childNewVars[i]! childNewConstrVars[i]! childCurvature[i]! childBConds[i]! childOptimality := childOptimality.push opt childOptimalityFiltered := childOptimalityFiltered.push opt @@ -446,7 +446,7 @@ partial def mkOptimalityAndVCondElim : | Curvature.Concave, Curvature.Affine => mkAppM ``And.left #[atom.optimality] | Curvature.Convex, Curvature.Affine => mkAppM ``And.right #[atom.optimality] | _, _ => pure atom.optimality - let optimality := mkAppN optimality (childReducedExpr.map Tree.val) + let optimality := mkAppN optimality (childCanonExpr.map Tree.val) let optimality := mkAppN optimality bconds check optimality let optimality := mkAppN optimality (newVars.map (mkFVar ·.fvarId)) @@ -457,7 +457,7 @@ partial def mkOptimalityAndVCondElim : -- Apply vcond elim property of atom. let vcondElim := atom.vcondElim - let vcondElim := vcondElim.map (mkAppN · (childReducedExpr.map Tree.val)) + let vcondElim := vcondElim.map (mkAppN · (childCanonExpr.map Tree.val)) let vcondElim := vcondElim.map (mkAppN · (newVars.map (mkFVar ·.fvarId))) let vcondElim := vcondElim.map (mkAppN · (newConstrVars.map (mkFVar ·.fvarId))) let vcondElim := vcondElim.map (mkAppN · monoArgs) @@ -599,16 +599,16 @@ def makeConstrForward (oldDomain : Expr) (xs : Array Expr) (originalConstrVars : return constrForward /-- -/ -def makeObjFunBackward (newDomain : Expr) (redProblem : Expr) (xs : Array Expr) (ys : Array Expr) (objFunOpt : Expr) - (redConstrs : Array Expr) (newConstrs : Array Expr) +def makeObjFunBackward (newDomain : Expr) (canonProblem : Expr) (xs : Array Expr) (ys : Array Expr) (objFunOpt : Expr) + (canonConstrs : Array Expr) (newConstrs : Array Expr) (newConstrVars : Array LocalDecl) : MetaM Expr := do -- ∀ {x : E}, Minimization.constraints q x → Minimization.objFun p (g x) ≤ Minimization.objFun q x withLocalDeclD `p newDomain fun p => do let prs := (← Meta.mkProjections newDomain p).map (·.2.2) - withLocalDeclD `h (← mkAppM ``Minimization.constraints #[redProblem, p]) fun h => do - let (_, cprs) := Meta.composeAndWithProj (redConstrs ++ newConstrs).toList + withLocalDeclD `h (← mkAppM ``Minimization.constraints #[canonProblem, p]) fun h => do + let (_, cprs) := Meta.composeAndWithProj (canonConstrs ++ newConstrs).toList let hProj := cprs h let objFunBackwardBody := objFunOpt let objFunBackwardBody := objFunBackwardBody.replaceFVars @@ -621,15 +621,15 @@ def makeObjFunBackward (newDomain : Expr) (redProblem : Expr) (xs : Array Expr) return objFunBackward /-- -/ -def makeConstrBackward (vcondElimMap : Std.HashMap Nat Expr) (newDomain : Expr) (redProblem : Expr) (xs : Array Expr) (ys : Array Expr) (constrOpt : Array Expr) - (redConstrs : Array Expr) (newConstrs : Array Expr) (newConstrVars : Array LocalDecl) : MetaM Expr := do +def makeConstrBackward (vcondElimMap : Std.HashMap Nat Expr) (newDomain : Expr) (canonProblem : Expr) (xs : Array Expr) (ys : Array Expr) (constrOpt : Array Expr) + (canonConstrs : Array Expr) (newConstrs : Array Expr) (newConstrVars : Array LocalDecl) : MetaM Expr := do -- ∀ {x : E}, Minimization.constraints q x → Minimization.constraints p (g x) withLocalDeclD `p newDomain fun p => do let prs := (← Meta.mkProjections newDomain p).map (·.2.2) - withLocalDeclD `h (← mkAppM ``Minimization.constraints #[redProblem, p]) fun h => do - let (_, cprs) := Meta.composeAndWithProj (redConstrs ++ newConstrs).toList + withLocalDeclD `h (← mkAppM ``Minimization.constraints #[canonProblem, p]) fun h => do + let (_, cprs) := Meta.composeAndWithProj (canonConstrs ++ newConstrs).toList let hProj := cprs h let mut constrBackwardProofs := #[] let mut filteredCounter := 0 @@ -731,18 +731,18 @@ withExistingLocalDecls originalVarsDecls.toList do /-- -/ def mkSolEqAtomOC (originalVarsDecls : Array LocalDecl) (atoms : OC (Tree GraphAtomData Expr)) - (reducedWithSolution : OC ReducedExprsWithSolutionTree) + (canonWithSolution : OC CanonExprsWithSolutionTree) (vcondVars : OC (Tree (Array Expr) Unit)) (originalConstrVars : Array LocalDecl) : MetaM (OC (Tree Expr Expr)) := withExistingLocalDecls originalVarsDecls.toList do withExistingLocalDecls originalConstrVars.toList do - let solEqAtom ← OC.map3M mkSolEqAtom atoms reducedWithSolution vcondVars + let solEqAtom ← OC.map3M mkSolEqAtom atoms canonWithSolution vcondVars trace[Meta.debug] "solEqAtom {solEqAtom}" return solEqAtom /-- -/ def mkFeasibilityOC (originalVarsDecls : Array LocalDecl) (atoms : OC GraphAtomDataTree) - (reducedWithSolution : OC ReducedExprsWithSolutionTree) + (canonWithSolution : OC CanonExprsWithSolutionTree) (bconds : OC BCondsTree) (vcondVars : OC VCondsTree) (originalConstrVars : Array LocalDecl) @@ -750,26 +750,26 @@ def mkFeasibilityOC (originalVarsDecls : Array LocalDecl) MetaM (OC FeasibilityProofsTree) := withExistingLocalDecls originalVarsDecls.toList do withExistingLocalDecls originalConstrVars.toList do - let feasibility ← OC.map5M mkFeasibility atoms reducedWithSolution bconds vcondVars solEqAtom + let feasibility ← OC.map5M mkFeasibility atoms canonWithSolution bconds vcondVars solEqAtom trace[Meta.debug] "feasibility {feasibility}" return feasibility /-- -/ -def mkReducedExprsOC (originalVarsDecls : Array LocalDecl) (newVarDecls : List LocalDecl) +def mkCanonExprsOC (originalVarsDecls : Array LocalDecl) (newVarDecls : List LocalDecl) (atoms : OC (Tree GraphAtomData Expr)) (newVars : OC (Tree (Array LocalDecl) Unit)) : MetaM (OC (Tree Expr Expr)) := withExistingLocalDecls originalVarsDecls.toList do withExistingLocalDecls newVarDecls do - let reducedExprs ← OC.map2M mkReducedExprs atoms newVars - trace[Meta.debug] "reducedExprs {reducedExprs}" - return reducedExprs + let canonExprs ← OC.map2M mkCanonExprs atoms newVars + trace[Meta.debug] "canonExprs {canonExprs}" + return canonExprs /-- -/ def mkNewConstrsOC (originalVarsDecls : Array LocalDecl) (newVarDecls : List LocalDecl) (bconds : OC BCondsTree) - (atoms : OC (Tree GraphAtomData Expr)) (newVars : OC (Tree (Array LocalDecl) Unit)) (reducedExprs : OC (Tree Expr Expr)) + (atoms : OC (Tree GraphAtomData Expr)) (newVars : OC (Tree (Array LocalDecl) Unit)) (canonExprs : OC (Tree Expr Expr)) : MetaM (Array Expr × OC (Tree (Array LocalDecl) Unit) × Array LocalDecl):= withExistingLocalDecls (originalVarsDecls.toList) do withExistingLocalDecls newVarDecls do - let newConstrs ← OC.map4M mkNewConstrs atoms bconds newVars reducedExprs + let newConstrs ← OC.map4M mkNewConstrs atoms bconds newVars canonExprs trace[Meta.debug] "newConstrs {newConstrs}" let newConstrVars ← OC.mapM mkNewConstrVars newConstrs trace[Meta.debug] "newConstrs {newConstrs}" @@ -784,7 +784,7 @@ def mkOptimalityAndVCondElimOC (originalVarsDecls : Array LocalDecl) (newVarDecl (newConstrVarsArray : Array LocalDecl) (atoms : OC (Tree GraphAtomData Expr)) (args : OC (Tree (Array Expr) Unit)) - (reducedExprs : OC (Tree Expr Expr)) + (canonExprs : OC (Tree Expr Expr)) (newVars : OC (Tree (Array LocalDecl) Unit)) (newConstrVars : OC (Tree (Array LocalDecl) Unit)) (curvature : OC (Tree Curvature Curvature)) @@ -794,7 +794,7 @@ def mkOptimalityAndVCondElimOC (originalVarsDecls : Array LocalDecl) (newVarDecl withExistingLocalDecls originalVarsDecls.toList do withExistingLocalDecls newVarDecls do withExistingLocalDecls newConstrVarsArray.toList do - let optimalityAndVCondElim ← OC.map7M mkOptimalityAndVCondElim atoms args reducedExprs newVars newConstrVars curvature bconds + let optimalityAndVCondElim ← OC.map7M mkOptimalityAndVCondElim atoms args canonExprs newVars newConstrVars curvature bconds let optimality := optimalityAndVCondElim.map (fun oce => oce.map Prod.fst Prod.fst) let vcondElim := optimalityAndVCondElim.map (fun oce => oce.map Prod.snd Prod.snd) trace[Meta.debug] "optimality {optimality}" @@ -824,7 +824,7 @@ structure ProcessedAtomTree where (vcondElimMap : Std.HashMap ℕ Expr) (solEqAtom : OC (Tree Expr Expr)) (feasibility : OC (Tree (Array Expr) Unit)) - (reducedExprs : OC (Tree Expr Expr)) + (canonExprs : OC (Tree Expr Expr)) (optimality : OC (Tree Expr Expr)) instance : Inhabited ProcessedAtomTree := @@ -843,18 +843,18 @@ def mkProcessedAtomTree (objCurv : Curvature) (objFun : Expr) let newVars ← withExistingLocalDecls originalVarsDecls.toList do OC.map2MwithCounter mkNewVars atoms args let newVarDecls ← mkNewVarDeclList newVars - let reducedWithSolution ← withExistingLocalDecls originalVarsDecls.toList do - OC.mapM mkReducedWithSolution atoms + let canonWithSolution ← withExistingLocalDecls originalVarsDecls.toList do + OC.mapM mkCanonWithSolution atoms let forwardImagesNewVars ← withExistingLocalDecls originalVarsDecls.toList do - mkForwardImagesNewVars reducedWithSolution - let solEqAtom ← mkSolEqAtomOC originalVarsDecls atoms reducedWithSolution vcondVars originalConstrVars - let feasibility ← mkFeasibilityOC originalVarsDecls atoms reducedWithSolution bconds vcondVars + mkForwardImagesNewVars canonWithSolution + let solEqAtom ← mkSolEqAtomOC originalVarsDecls atoms canonWithSolution vcondVars originalConstrVars + let feasibility ← mkFeasibilityOC originalVarsDecls atoms canonWithSolution bconds vcondVars originalConstrVars solEqAtom - let reducedExprs ← mkReducedExprsOC originalVarsDecls newVarDecls atoms newVars + let canonExprs ← mkCanonExprsOC originalVarsDecls newVarDecls atoms newVars let (newConstrs, newConstrVars, newConstrVarsArray) - ← mkNewConstrsOC originalVarsDecls newVarDecls bconds atoms newVars reducedExprs + ← mkNewConstrsOC originalVarsDecls newVarDecls bconds atoms newVars canonExprs let (optimality, vcondElimMap) ← mkOptimalityAndVCondElimOC originalVarsDecls newVarDecls - newConstrVarsArray atoms args reducedExprs newVars newConstrVars curvature bconds vcondIdx + newConstrVarsArray atoms args canonExprs newVars newConstrVars curvature bconds vcondIdx return ProcessedAtomTree.mk (originalVarsDecls := originalVarsDecls) @@ -868,7 +868,7 @@ def mkProcessedAtomTree (objCurv : Curvature) (objFun : Expr) (vcondElimMap := vcondElimMap) (solEqAtom := solEqAtom) (feasibility := feasibility) - (reducedExprs := reducedExprs) + (canonExprs := canonExprs) (optimality := optimality) open Meta Elab Tactic @@ -900,7 +900,7 @@ def canonize (ogProblem : MinimizationExpr) : MetaM (MinimizationExpr × Expr) : -- Process the atom tree. let pat ← mkProcessedAtomTree Curvature.Convex objFun constraints originalVarsDecls - -- Create reduced problem and equivalence proof. + -- Create canon problem and equivalence proof. withExistingLocalDecls pat.originalVarsDecls.toList do -- Original problem variables. let originalVars := pat.originalVarsDecls.map fun decl => mkFVar decl.fvarId @@ -918,16 +918,16 @@ def canonize (ogProblem : MinimizationExpr) : MetaM (MinimizationExpr × Expr) : return (objFunForward, constrForward) withExistingLocalDecls pat.newVarDecls do - -- New variables added by the reduction. + -- New variables added by the canonization. let newVars := (pat.newVarDecls.map (mkFVar ·.fvarId)).toArray - -- Reduced variables: originalVars ⊎ newVars. - let redVars ← (originalVars ++ newVars).mapM fun x => do + -- Canon variables: originalVars ⊎ newVars. + let canonVars ← (originalVars ++ newVars).mapM fun x => do let decl ← x.fvarId!.getDecl return (decl.userName, decl.type) -- New domain: D × T where T is the domain of the new variables. - let E := Meta.composeDomain redVars.toList + let E := Meta.composeDomain canonVars.toList -- Function to replace variables by projections in the new domain. let mkDomain := fun e => @@ -936,33 +936,33 @@ def canonize (ogProblem : MinimizationExpr) : MetaM (MinimizationExpr × Expr) : let e := Expr.replaceFVars e (originalVars ++ newVars) prs.toArray mkLambdaFVars #[p] e - -- Reduced problem. - let redConstrs := pat.reducedExprs.constr.map Tree.val - let redConstrs := redConstrs.filterIdx (fun i => ¬ pat.isVCond[i]!) - let redProblem : MinimizationExpr := + -- Canon problem. + let canonConstrs := pat.canonExprs.constr.map Tree.val + let canonConstrs := canonConstrs.filterIdx (fun i => ¬ pat.isVCond[i]!) + let canonProblem : MinimizationExpr := { domain := E codomain := R - objFun := ← mkDomain pat.reducedExprs.objFun.val - constraints := ← mkDomain <| Meta.composeAnd (redConstrs ++ pat.newConstrs).toList } - let redProblemExpr := redProblem.toExpr + objFun := ← mkDomain pat.canonExprs.objFun.val + constraints := ← mkDomain <| Meta.composeAnd (canonConstrs ++ pat.newConstrs).toList } + let canonProblemExpr := canonProblem.toExpr -- Backward map: ψ. let backwardMap ← makeBackwardMap originalVars mkDomain let (objFunBackward, constrBackward) ← withExistingLocalDecls pat.newConstrVarsArray.toList do - let objFunBackward ← makeObjFunBackward E redProblemExpr originalVars newVars - pat.optimality.objFun.val redConstrs pat.newConstrs pat.newConstrVarsArray + let objFunBackward ← makeObjFunBackward E canonProblemExpr originalVars newVars + pat.optimality.objFun.val canonConstrs pat.newConstrs pat.newConstrVarsArray - let constrBackward ← makeConstrBackward pat.vcondElimMap E redProblemExpr originalVars - newVars (pat.optimality.constr.map (·.val)) redConstrs pat.newConstrs + let constrBackward ← makeConstrBackward pat.vcondElimMap E canonProblemExpr originalVars + newVars (pat.optimality.constr.map (·.val)) canonConstrs pat.newConstrs pat.newConstrVarsArray return (objFunBackward, constrBackward) -- Combine forward and backward maps into equivalence witness. let strongEqvProof ← mkAppOptM ``Minimization.StrongEquivalence.mk - #[D, E, R, none, ogProblemExpr, redProblemExpr, + #[D, E, R, none, ogProblemExpr, canonProblemExpr, -- phi forwardMap, -- psi @@ -977,7 +977,7 @@ def canonize (ogProblem : MinimizationExpr) : MetaM (MinimizationExpr × Expr) : objFunBackward] let eqvProof ← mkAppM ``Minimization.Equivalence.ofStrongEquivalence #[strongEqvProof] - return (redProblem, eqvProof) + return (canonProblem, eqvProof) def dcpBuilder : EquivalenceBuilder Unit := fun eqvExpr g => g.withContext do let ogProblem ← eqvExpr.toMinimizationExprLHS diff --git a/CvxLean/Tactic/PreDCP/PreDCP.lean b/CvxLean/Tactic/PreDCP/PreDCP.lean index 615b3f8c..02ae90a1 100644 --- a/CvxLean/Tactic/PreDCP/PreDCP.lean +++ b/CvxLean/Tactic/PreDCP/PreDCP.lean @@ -129,7 +129,7 @@ def evalStep (step : EggRewrite) (vars params : List Name) (paramsDecls : List L -- Distinguish between rewriting props and reals. No need to apply congruence if we are -- rewriting the whole constraint. if !(← inferType lhsSubExprAtProb).isProp then - -- Reduce to equality goal for real rewerites . + -- Reduce to equality goal for real rewrites . if !atObjFun then let gs ← g.apply (mkConst ``Iff.of_eq) if gs.length != 1 then diff --git a/CvxLean/Test/PreDCP/DQCP.lean b/CvxLean/Test/PreDCP/DQCP.lean index 0ffa868a..f65dc6b7 100644 --- a/CvxLean/Test/PreDCP/DQCP.lean +++ b/CvxLean/Test/PreDCP/DQCP.lean @@ -37,9 +37,9 @@ time_cmd reduction redqcp1/dqcp1 : qcp1 := by solve dqcp1 -#print dqcp1.reduced -- ... -#eval dqcp1.value -- -2.000000 -#eval dqcp1.solution -- (2.000000, 2.000000) +#print dqcp1.conicForm -- ... +#eval dqcp1.value -- -2.000000 +#eval dqcp1.solution -- (2.000000, 2.000000) end QCP1 @@ -61,9 +61,9 @@ time_cmd equivalence redqcp2/dqcp2 : qcp2 0.05 0.65 := by solve dqcp2 -#print dqcp2.reduced -- ... -#eval dqcp2.value -- 0.021286 -#eval dqcp2.solution -- 0.989524 +#print dqcp2.conicForm -- ... +#eval dqcp2.value -- 0.021286 +#eval dqcp2.solution -- 0.989524 end QCP2 @@ -83,9 +83,9 @@ time_cmd reduction redqcp3/dqcp3 : qcp3 := by solve dqcp3 -#print dqcp3.reduced -- ... -#eval dqcp3.value -- 0.000000 -#eval dqcp3.solution -- (12.000000, 4.000000) +#print dqcp3.conicForm -- ... +#eval dqcp3.value -- 0.000000 +#eval dqcp3.solution -- (12.000000, 4.000000) end QCP3 @@ -103,9 +103,9 @@ time_cmd reduction redqcp4/dqcp4 : qcp4 := by solve dqcp4 -#print dqcp4.reduced -- ... -#eval dqcp4.value -- -47.500000 -#eval dqcp4.solution -- 47.500000 +#print dqcp4.conicForm -- ... +#eval dqcp4.value -- -47.500000 +#eval dqcp4.solution -- 47.500000 end QCP4 diff --git a/CvxLean/Test/PreDCP/MainExample.lean b/CvxLean/Test/PreDCP/MainExample.lean index 140a1647..02a014a8 100644 --- a/CvxLean/Test/PreDCP/MainExample.lean +++ b/CvxLean/Test/PreDCP/MainExample.lean @@ -30,7 +30,7 @@ time_cmd equivalence eq/q : p := by solve q -#print q.reduced +#print q.conicForm -- optimization (x : ℝ) (t.0 : ℝ) (t.1 : ℝ) -- minimize x -- subject to diff --git a/CvxLean/Test/Solve/Problems/Exp.lean b/CvxLean/Test/Solve/Problems/Exp.lean index 9a747ac8..1f6e4df2 100644 --- a/CvxLean/Test/Solve/Problems/Exp.lean +++ b/CvxLean/Test/Solve/Problems/Exp.lean @@ -12,7 +12,7 @@ noncomputable def exp1 := solve exp1 -#print exp1.reduced +#print exp1.conicForm #eval exp1.status -- "PRIMAL_AND_DUAL_FEASIBLE" #eval exp1.value -- 2.302585 @@ -26,7 +26,7 @@ noncomputable def exp2 := solve exp2 -#print exp2.reduced +#print exp2.conicForm #eval exp2.status -- "PRIMAL_AND_DUAL_FEASIBLE" #eval exp2.value -- 22026.464907 diff --git a/CvxLean/Test/Solve/Problems/Linear.lean b/CvxLean/Test/Solve/Problems/Linear.lean index 681acdeb..7d549602 100644 --- a/CvxLean/Test/Solve/Problems/Linear.lean +++ b/CvxLean/Test/Solve/Problems/Linear.lean @@ -12,7 +12,7 @@ noncomputable def linear1 := solve linear1 -#print linear1.reduced +#print linear1.conicForm #eval linear1.status -- "PRIMAL_AND_DUAL_FEASIBLE" #eval linear1.value -- 11.500000 @@ -41,7 +41,7 @@ lemma linear2Solution : Solution linear2 := solve linear2 -#print linear2.reduced +#print linear2.conicForm #eval linear2.status -- "PRIMAL_AND_DUAL_FEASIBLE" #eval linear2.value -- 400.000000 @@ -56,7 +56,7 @@ noncomputable def linear3 := solve linear3 -#print linear3.reduced +#print linear3.conicForm #eval linear3.status -- "PRIMAL_AND_DUAL_FEASIBLE" #eval linear3.value -- -30.000000 @@ -73,7 +73,7 @@ noncomputable def linear4 := solve linear4 -#print linear4.reduced +#print linear4.conicForm #eval linear4.status -- "PRIMAL_AND_DUAL_FEASIBLE" #eval linear4.value -- 71.500000 @@ -113,7 +113,7 @@ noncomputable def linear5 := set_option trace.Meta.debug true in solve linear5 -#print linear5.reduced +#print linear5.conicForm #eval linear5.status -- "PRIMAL_AND_DUAL_FEASIBLE" #eval linear5.value -- 11.814741 diff --git a/CvxLean/Test/Solve/Problems/Log.lean b/CvxLean/Test/Solve/Problems/Log.lean index 5fa02849..d28c2ba9 100644 --- a/CvxLean/Test/Solve/Problems/Log.lean +++ b/CvxLean/Test/Solve/Problems/Log.lean @@ -5,30 +5,30 @@ section Log open CvxLean Minimization Real noncomputable def log1 := - optimization (x : ℝ) + optimization (x : ℝ) minimize (x) - subject to + subject to h₁ : 10 ≤ log x h₂ : 0 < x solve log1 -#print log1.reduced +#print log1.conicForm #eval log1.status -- "PRIMAL_AND_DUAL_FEASIBLE" #eval log1.value -- 22026.464907 #eval log1.solution -- 22026.464907 noncomputable def log2 := - optimization (x : ℝ) + optimization (x : ℝ) maximize (log x) - subject to + subject to h₁ : x ≤ 10 h₂ : 0 < x solve log2 -#print log2.reduced +#print log2.conicForm #eval log2.status -- "PRIMAL_AND_DUAL_FEASIBLE" #eval log2.value -- 2.302585 diff --git a/CvxLean/Test/Solve/Problems/LogDet.lean b/CvxLean/Test/Solve/Problems/LogDet.lean index 54798e4a..21587af2 100644 --- a/CvxLean/Test/Solve/Problems/LogDet.lean +++ b/CvxLean/Test/Solve/Problems/LogDet.lean @@ -29,7 +29,7 @@ noncomputable def logDet2 := solve logDet2 -#print logDet2.reduced +#print logDet2.conicForm #eval logDet2.status -- "PRIMAL_AND_DUAL_FEASIBLE" #eval logDet2.value -- 6.725434 diff --git a/CvxLean/Test/Solve/Problems/SDP.lean b/CvxLean/Test/Solve/Problems/SDP.lean index 87262646..d3f8f01f 100644 --- a/CvxLean/Test/Solve/Problems/SDP.lean +++ b/CvxLean/Test/Solve/Problems/SDP.lean @@ -28,7 +28,7 @@ noncomputable def sdp1 := solve sdp1 -#print sdp1.reduced +#print sdp1.conicForm #eval sdp1.status -- "PRIMAL_AND_DUAL_FEASIBLE" #eval sdp1.value -- -0.266754 diff --git a/CvxLean/Test/Solve/Problems/SO.lean b/CvxLean/Test/Solve/Problems/SO.lean index 12ce635b..6bc3c79a 100644 --- a/CvxLean/Test/Solve/Problems/SO.lean +++ b/CvxLean/Test/Solve/Problems/SO.lean @@ -14,7 +14,7 @@ noncomputable def so1 := solve so1 -#print so1.reduced +#print so1.conicForm #eval so1.status -- "PRIMAL_AND_DUAL_FEASIBLE" #eval so1.value -- 2.101003 @@ -29,7 +29,7 @@ def so2 := solve so2 -#print so2.reduced +#print so2.conicForm #eval so2.status -- "PRIMAL_AND_DUAL_FEASIBLE" #eval so2.value -- 0.426303 diff --git a/README.md b/README.md index da4750aa..2333a84b 100644 --- a/README.md +++ b/README.md @@ -4,7 +4,7 @@ CvxLean is a convex optimization modeling framework written in [Lean 4](https:// Problems are stated using definitions from [mathlib](https://github.com/leanprover-community/mathlib) and can be rigorously transformed both automatically and interactively. They can be solved by calling the backend solver [MOSEK](https://www.mosek.com/). -Our main contribution is a verified version of the [disciplined convex programming (DCP)](https://web.stanford.edu/~boyd/papers/disc_cvx_prog.html) reduction algorithm. +Our main contribution is a verified version of the [disciplined convex programming (DCP)](https://web.stanford.edu/~boyd/papers/disc_cvx_prog.html) canonization algorithm. ## Installation @@ -56,7 +56,7 @@ solve so1 It will show MOSEK's output and its return code, which should be zero. If successful, it will add several definitions to the environment: -* `so1.reduced`: the reduced version of the problem after applying DCP. +* `so1.conicForm`: the conic form of the problem after applying DCP. * `so1.status`: the feasibility status of the primal and the dual problem, in this case `"PRIMAL_AND_DUAL_FEASIBLE"`, i.e. optimal. * `so1.value`: if the problem is optimal, it corresponds to its optimal value. * `so1.solution`: if the problem is optimal, it corresponds to the optimal point.