feat: vehicle speed scheduling case study

verified-optimization · Jan 26, 2024 · 90607a7 · 90607a7
2 parents 4c7e043 + 17160c6
commit 90607a7
Show file tree

Hide file tree

Showing 29 changed files with 910 additions and 417 deletions.
diff --git a/CvxLean/Command/Equivalence.lean b/CvxLean/Command/Equivalence.lean
@@ -79,80 +79,78 @@ def evalEquivalenceAux (probIdStx eqvIdStx : TSyntax `ident) (xs : Array (Syntax
       [])
 
   if bwdMap then
-    trace[Meta.debug] "HERE"
-    -- Get psi, reduce it appropriately and convert to float.
-    let psi := (← whnf eqv).getArg! 7
-
-    let mut simpCtx ← Simp.Context.mkDefault
-    let simpCfg : Simp.Config :=
-      { zeta             := true
-        beta             := true
-        eta              := true
-        iota             := true
-        proj             := true
-        decide           := true
-        arith            := true
-        dsimp            := true
-        unfoldPartialApp := true
-        etaStruct        := .all }
-    simpCtx := { simpCtx with config := simpCfg }
-
-    let mut simpThms := {}
-    simpThms ← simpThms.addDeclToUnfold ``Minimization.Equivalence.mk
-    simpThms ← simpThms.addDeclToUnfold ``Minimization.Equivalence.refl
-    simpThms ← simpThms.addDeclToUnfold ``Minimization.Equivalence.trans
-    simpThms ← simpThms.addDeclToUnfold ``Minimization.Equivalence.ofStrongEquivalence
-    simpThms ← simpThms.addDeclToUnfold ``Minimization.Equivalence.ofEq
-    simpThms ← simpThms.addDeclToUnfold ``Minimization.Equivalence.psi
-    simpThms ← simpThms.addDeclToUnfold ``Minimization.Equivalence.map_objFun
-    simpThms ← simpThms.addDeclToUnfold ``Minimization.Equivalence.map_objFun_log
-    simpThms ← simpThms.addDeclToUnfold ``Minimization.Equivalence.map_objFun_sq
-    simpThms ← simpThms.addDeclToUnfold ``Minimization.Equivalence.rewrite_objFun
-    simpThms ← simpThms.addDeclToUnfold ``Minimization.Equivalence.map_domain
-    simpThms ← simpThms.addDeclToUnfold ``Minimization.Equivalence.rewrite_objFun
-    simpThms ← simpThms.addDeclToUnfold ``Minimization.Equivalence.rewrite_constraints
-    simpThms ← simpThms.addDeclToUnfold ``Minimization.Equivalence.rewrite_constraint_1
-    simpThms ← simpThms.addDeclToUnfold ``Minimization.Equivalence.rewrite_constraint_2
-    simpThms ← simpThms.addDeclToUnfold ``Minimization.Equivalence.rewrite_constraint_3
-    simpThms ← simpThms.addDeclToUnfold ``Minimization.Equivalence.rewrite_constraint_4
-    simpThms ← simpThms.addDeclToUnfold ``Minimization.Equivalence.rewrite_constraint_5
-    simpThms ← simpThms.addDeclToUnfold ``Minimization.Equivalence.rewrite_constraint_6
-    simpThms ← simpThms.addDeclToUnfold ``Minimization.Equivalence.rewrite_constraint_7
-    simpThms ← simpThms.addDeclToUnfold ``Minimization.Equivalence.rewrite_constraint_8
-    simpThms ← simpThms.addDeclToUnfold ``Minimization.Equivalence.rewrite_constraint_9
-    simpThms ← simpThms.addDeclToUnfold ``Minimization.Equivalence.rewrite_constraint_10
-    simpThms ← simpThms.addDeclToUnfold ``Minimization.Equivalence.rewrite_constraint_1_last
-    simpThms ← simpThms.addDeclToUnfold ``Minimization.Equivalence.rewrite_constraint_2_last
-    simpThms ← simpThms.addDeclToUnfold ``Minimization.Equivalence.rewrite_constraint_3_last
-    simpThms ← simpThms.addDeclToUnfold ``Minimization.Equivalence.rewrite_constraint_4_last
-    simpThms ← simpThms.addDeclToUnfold ``Minimization.Equivalence.rewrite_constraint_5_last
-    simpThms ← simpThms.addDeclToUnfold ``Minimization.Equivalence.rewrite_constraint_6_last
-    simpThms ← simpThms.addDeclToUnfold ``Minimization.Equivalence.rewrite_constraint_7_last
-    simpThms ← simpThms.addDeclToUnfold ``Minimization.Equivalence.rewrite_constraint_8_last
-    simpThms ← simpThms.addDeclToUnfold ``Minimization.Equivalence.rewrite_constraint_9_last
-    simpThms ← simpThms.addDeclToUnfold ``Minimization.Equivalence.rewrite_constraint_10_last
-    simpThms ← simpThms.addDeclToUnfold ``CvxLean.ChangeOfVariables.toEquivalence
-    simpThms ← simpThms.addDeclToUnfold ``Eq.mpr
-    simpThms ← simpThms.addDeclToUnfold ``Eq.mp
-    simpCtx := { simpCtx with simpTheorems := #[simpThms] }
-
-    let (res, _) ← simp psi simpCtx
-    let psi := res.expr
-
-    try
-      let psiF ← realToFloat psi
-      Lean.addAndCompile <|
-        Declaration.defnDecl
-          (mkDefinitionValEx (eqvId ++ `backward_map)
-          []
-          (← inferType psiF)
-          psiF
-          (Lean.ReducibilityHints.regular 0)
-          (DefinitionSafety.safe)
-          [])
-    catch e =>
-      trace[Meta.debug]
-        "`equivalence` warning: failed to create `phi_float` - {e.toMessageData}."
+    lambdaTelescope eqv fun eqvArgs eqvBody => do
+      -- Get psi, reduce it appropriately and convert to float.
+      let psi := (← whnf eqvBody).getArg! 7
+
+      let mut simpCtx ← Simp.Context.mkDefault
+      let simpCfg : Simp.Config :=
+        { zeta             := true
+          beta             := true
+          eta              := true
+          iota             := true
+          proj             := true
+          decide           := true
+          arith            := true
+          dsimp            := true
+          unfoldPartialApp := true
+          etaStruct        := .all }
+      simpCtx := { simpCtx with config := simpCfg }
+
+      let mut simpThms := {}
+      simpThms ← simpThms.addDeclToUnfold ``Minimization.Equivalence.mk
+      simpThms ← simpThms.addDeclToUnfold ``Minimization.Equivalence.refl
+      simpThms ← simpThms.addDeclToUnfold ``Minimization.Equivalence.trans
+      simpThms ← simpThms.addDeclToUnfold ``Minimization.Equivalence.ofStrongEquivalence
+      simpThms ← simpThms.addDeclToUnfold ``Minimization.Equivalence.ofEq
+      simpThms ← simpThms.addDeclToUnfold ``Minimization.Equivalence.psi
+      simpThms ← simpThms.addDeclToUnfold ``Minimization.Equivalence.map_objFun
+      simpThms ← simpThms.addDeclToUnfold ``Minimization.Equivalence.map_objFun_log
+      simpThms ← simpThms.addDeclToUnfold ``Minimization.Equivalence.map_objFun_sq
+      simpThms ← simpThms.addDeclToUnfold ``Minimization.Equivalence.rewrite_objFun
+      simpThms ← simpThms.addDeclToUnfold ``Minimization.Equivalence.map_domain
+      simpThms ← simpThms.addDeclToUnfold ``Minimization.Equivalence.add_constraint
+      simpThms ← simpThms.addDeclToUnfold ``Minimization.Equivalence.rewrite_objFun
+      simpThms ← simpThms.addDeclToUnfold ``Minimization.Equivalence.rewrite_constraints
+      simpThms ← simpThms.addDeclToUnfold ``Minimization.Equivalence.rewrite_constraint_1
+      simpThms ← simpThms.addDeclToUnfold ``Minimization.Equivalence.rewrite_constraint_2
+      simpThms ← simpThms.addDeclToUnfold ``Minimization.Equivalence.rewrite_constraint_3
+      simpThms ← simpThms.addDeclToUnfold ``Minimization.Equivalence.rewrite_constraint_4
+      simpThms ← simpThms.addDeclToUnfold ``Minimization.Equivalence.rewrite_constraint_5
+      simpThms ← simpThms.addDeclToUnfold ``Minimization.Equivalence.rewrite_constraint_6
+      simpThms ← simpThms.addDeclToUnfold ``Minimization.Equivalence.rewrite_constraint_7
+      simpThms ← simpThms.addDeclToUnfold ``Minimization.Equivalence.rewrite_constraint_8
+      simpThms ← simpThms.addDeclToUnfold ``Minimization.Equivalence.rewrite_constraint_9
+      simpThms ← simpThms.addDeclToUnfold ``Minimization.Equivalence.rewrite_constraint_10
+      simpThms ← simpThms.addDeclToUnfold ``Minimization.Equivalence.rewrite_constraint_1_last
+      simpThms ← simpThms.addDeclToUnfold ``Minimization.Equivalence.rewrite_constraint_2_last
+      simpThms ← simpThms.addDeclToUnfold ``Minimization.Equivalence.rewrite_constraint_3_last
+      simpThms ← simpThms.addDeclToUnfold ``Minimization.Equivalence.rewrite_constraint_4_last
+      simpThms ← simpThms.addDeclToUnfold ``Minimization.Equivalence.rewrite_constraint_5_last
+      simpThms ← simpThms.addDeclToUnfold ``Minimization.Equivalence.rewrite_constraint_6_last
+      simpThms ← simpThms.addDeclToUnfold ``Minimization.Equivalence.rewrite_constraint_7_last
+      simpThms ← simpThms.addDeclToUnfold ``Minimization.Equivalence.rewrite_constraint_8_last
+      simpThms ← simpThms.addDeclToUnfold ``Minimization.Equivalence.rewrite_constraint_9_last
+      simpThms ← simpThms.addDeclToUnfold ``Minimization.Equivalence.rewrite_constraint_10_last
+      simpThms ← simpThms.addDeclToUnfold ``CvxLean.ChangeOfVariables.toEquivalence
+      simpThms ← simpThms.addDeclToUnfold ``Eq.mpr
+      simpThms ← simpThms.addDeclToUnfold ``Eq.mp
+      simpCtx := { simpCtx with simpTheorems := #[simpThms] }
+
+      let (res, _) ← simp psi simpCtx
+
+      -- NOTE: We ignore arguments with `Prop`s here as keeping them would only mean requiring
+      -- proofs about floats.
+      let eqvNonPropArgs ← eqvArgs.filterM fun arg => do
+        return !(← inferType (← inferType arg)).isProp
+      let psi ← mkLambdaFVars eqvNonPropArgs res.expr
+
+      try
+        let psiF ← realToFloat psi
+        Lean.simpleAddAndCompileDefn (eqvId ++ `backward_map) psiF
+      catch e =>
+        trace[Meta.debug]
+          "`equivalence` error: failed to create `{eqvId}.backward_map`.\n{e.toMessageData}"
 
 /-- Create `equivalence` command. It is similar to the `reduction` command, but requires an
 `Equivalence` instead of a `Reduction`. -/

diff --git a/CvxLean/Command/Solve.lean b/CvxLean/Command/Solve.lean
@@ -7,36 +7,9 @@ open Lean Lean.Elab Lean.Elab.Term Lean.Elab.Command Lean.Meta
 
 open Minimization
 
--- /-- Equivalent to the `#reduce` command. TODO: Move. -/
--- def reduceExpr (e : Expr) : MetaM Expr :=
---   withTransparency (mode := TransparencyMode.all) <|
---     reduce e (skipProofs := true) (skipTypes := true)
-
-/-- Reduce like `Meta.DiscrTree.whnfDT`. -/
-partial def whnfUntilValue (e : Expr) : MetaM Expr := do
-  let e ← step e
-  match e.etaExpandedStrict? with
-  | some e => whnfUntilValue e
-  | none   => return e
-where
-  step (e : Expr) := do
-    let e ← whnfCore e
-    match (← unfoldDefinition? e) with
-    | some e' => if isBadKey e'.getAppFn then return e else step e'
-    | none    => return e
-  isBadKey (fn : Expr) : Bool :=
-    match fn with
-    | Expr.lit ..   => false
-    | Expr.const .. => false
-    | Expr.fvar ..  => false
-    | Expr.proj ..  => false
-    | Expr.forallE _ _ b _ => b.hasLooseBVars
-    | _ => true
-
-/-- Get problem name. Used to add information about the solution to the
-environment. -/
+/-- Get problem name. Used to add information about the solution to the environment. -/
 def getProblemName (term : Syntax) : MetaM Lean.Name := do
-  -- TODO: Full name with paraemters.
+  -- TODO: Full name with parameters.
   let idStx := match term with
     | Syntax.ident _ _ _ _ => term
     | Syntax.node _ _ args => args.getD 0 Syntax.missing
@@ -49,25 +22,10 @@ def getProblemName (term : Syntax) : MetaM Lean.Name := do
 /-- -/
 def getReducedProblemAndBwdMap (prob : Expr) : MetaM (Meta.MinimizationExpr × Expr) := do
   let ogProb ← Meta.MinimizationExpr.fromExpr prob
-
   let (redProb, eqvProof) ← DCP.canonize ogProb
-
   let backwardMap ← mkAppM ``Minimization.Equivalence.psi #[eqvProof]
-
   return (redProb, backwardMap)
 
-/-- Add problem declaration inferring type. -/
-def addProblemDeclaration (n : Lean.Name) (e : Expr) (compile : Bool) : MetaM Unit := do
-  let ty ← inferType e
-  let reducibility := Lean.ReducibilityHints.regular 0
-  let safety := DefinitionSafety.safe
-  let defVal := mkDefinitionValEx n ([] : List Lean.Name) ty e reducibility safety ([n] : List Lean.Name)
-  let decl := Declaration.defnDecl defVal
-  if compile then
-    Lean.addAndCompile decl
-  else
-    Lean.addDecl decl
-
 syntax (name := solve) "solve " term : command
 
 set_option maxHeartbeats 1000000
@@ -94,11 +52,12 @@ unsafe def evalSolve : CommandElab := fun stx =>
 
       let probName ← getProblemName probInstance.raw
 
-      addProblemDeclaration (probName ++ `reduced) redProbExpr false
+      simpleAddDefn (probName ++ `reduced) redProbExpr
 
       -- Call the solver on prob.reduced and get a point in E.
       let (coeffsData, sections) ← determineCoeffsFromExpr redProb
       trace[Meta.debug] "coeffsData: {coeffsData}"
+
       let solPointResponse ← Meta.conicSolverFromValues redProb coeffsData sections
       trace[Meta.debug] "solPointResponse: {solPointResponse}"
 
@@ -111,8 +70,7 @@ unsafe def evalSolve : CommandElab := fun stx =>
           trace[Meta.debug] "solPoint.summary: {solPoint.summary}"
 
           -- Add status to the environment.
-          addProblemDeclaration
-            (probName ++ `status) (mkStrLit solPoint.summary.problemStatus) true
+          simpleAddAndCompileDefn (probName ++ `status) (mkStrLit solPoint.summary.problemStatus)
 
           -- TODO: For now, we are only handling this case.
           if solPoint.summary.problemStatus != "PRIMAL_AND_DUAL_FEASIBLE" then
@@ -129,18 +87,20 @@ unsafe def evalSolve : CommandElab := fun stx =>
           trace[Meta.debug] "probSolPointFloat: {probSolPointFloat}"
 
           -- Add the solution point to the environment.
-          addProblemDeclaration (probName ++ `solution) probSolPointFloat true
+          simpleAddAndCompileDefn (probName ++ `solution) probSolPointFloat
 
           -- Also add value of optimal point.
           let probSolValue := mkApp redProb.objFun solPointExpr
           let probSolValueFloat ← realToFloat probSolValue
           trace[Meta.debug] "probSolValueFloat {probSolValueFloat}"
           check probSolValueFloat
+
           let mut probSolValueFloat := Expr.headBeta probSolValueFloat
           trace[Meta.debug] "probSolValueFloat reduced: {probSolValueFloat}"
+
           if probSolValueFloat.getAppFn.isConstOf `CvxLean.maximizeNeg then
             probSolValueFloat := probSolValueFloat.getAppArgs[2]!
-          addProblemDeclaration (probName ++ `value) probSolValueFloat true
+          simpleAddAndCompileDefn (probName ++ `value) probSolValueFloat
 
           pure ()
   | _ => throwUnsupportedSyntax

diff --git a/CvxLean/Command/Solve/Float/Coeffs.lean b/CvxLean/Command/Solve/Float/Coeffs.lean
@@ -155,7 +155,7 @@ unsafe def unrollVectors (constraints : Expr) : MetaM (Array Expr) := do
           let idxExpr ← mkFinIdxExpr i n
           let ei := mkApp e idxExpr
           res := res.push (← mkAppM ``Real.zeroCone #[ei])
-    -- Positive orthant cone.
+    -- Vector positive orthant cone.
     | .app (.app (.app (.const ``Real.Vec.posOrthCone _) (.app (.const ``Fin _) n)) _) e =>
         let n : Nat ← evalExpr Nat (mkConst ``Nat) n
         for i in [:n] do
@@ -171,6 +171,15 @@ unsafe def unrollVectors (constraints : Expr) : MetaM (Array Expr) := do
           let bi := mkApp b idxExpr
           let ci := mkApp c idxExpr
           res := res.push (← mkAppM ``Real.expCone #[ai, bi, ci])
+    -- Vector second-order cone.
+    | .app (.app (.app (.app (.app (.const ``Real.Vec.soCone _)
+        exprN@(.app (.const ``Fin _) n)) (.app (.const ``Fin _) m)) finTypeN) t) X =>
+        let m : Nat ← evalExpr Nat (mkConst ``Nat) m
+        for i in [:m] do
+          let idxExpr ← mkFinIdxExpr i m
+          let ti := mkApp t idxExpr
+          let Xi := mkApp X idxExpr
+          res := res.push (mkAppN (mkConst ``Real.soCone) #[exprN, finTypeN, ti, Xi])
     | _ =>
         res := res.push c
 

diff --git a/CvxLean/Command/Solve/Float/Cones.lean b/CvxLean/Command/Solve/Float/Cones.lean