feat: relaxations and pre-DCP improvements

.github/workflows/main.yml

@@ -35,15 +35,13 @@ jobs:
           sh rustup-init.sh -y --default-toolchain none
       - name: Checkout
         uses: actions/checkout@v3
-      - name: Build CvxLean
+      - name: Build egg-pre-dcp and CvxLean
         run: |
-          set -o pipefail
-          lake update
-          lake exe cache get
-          lake run EggClean
-          lake build EggConvexify
-          lake build CvxLean
+          ./build.sh
+      - name: Test egg-pre-dcp 
+        working-directory: egg-pre-dcp
+        run: | 
+          cargo test
       - name: Test CvxLean 
         run: |
           lake build CvxLeanTest
-          

.gitignore

@@ -4,8 +4,8 @@
 /build
 /solver/*.cbf
 /solver/*.sol
-/egg-convexify/*.dot 
-/egg-convexify/*.svg
+/egg-pre-dcp/*.dot 
+/egg-pre-dcp/*.svg
 *.olean
 
 /playground

CvxLean.lean

@@ -1,6 +1,7 @@
-import CvxLean.Tactic.DCP.Algorithm
 import CvxLean.Tactic.Basic.All
+import CvxLean.Tactic.DCP.DCP
 import CvxLean.Tactic.PreDCP.PreDCP
 import CvxLean.Command.Solve
 import CvxLean.Command.Reduction
+import CvxLean.Command.Relaxation
 import CvxLean.Command.Equivalence

CvxLean/Command/Equivalence.lean

@@ -17,8 +17,8 @@ partial def runEquivalenceTactic (mvarId : MVarId) (stx : Syntax) : TermElabM Un
 
 /-- Run equivalence tactic and return both the right-hand term (`q`) and the equivalence proof, of
 type `Equivalence p q`. -/
-def elabEquivalenceProof (lhs : Expr) (stx : Syntax) : TermElabM (Expr × Expr) := do
-  elabTransformationProof TransformationGoal.Equivalence lhs stx
+def elabEquivalenceProof (lhs : Expr) (rhsName : Name) (stx : Syntax) : TermElabM (Expr × Expr) :=
+  elabTransformationProof TransformationGoal.Equivalence lhs rhsName stx
 
 syntax (name := equivalence)
   "equivalence" ident "/" ident declSig ":=" Lean.Parser.Term.byTactic : command
@@ -42,7 +42,8 @@ def evalEquivalenceAux (probIdStx eqvIdStx : TSyntax `ident) (xs : Array (Syntax
       mvarId.assign mvarVal }
     catch _ => pure ()
 
-  let (rhs, eqv) ← elabEquivalenceProof lhs proofStx.raw
+  let rhsName := probIdStx.getId
+  let (rhs, eqv) ← elabEquivalenceProof lhs rhsName proofStx
 
   -- Names for new definitions.
   let currNamespace ← getCurrNamespace

CvxLean/Command/Reduction.lean

@@ -15,16 +15,16 @@ def runReductionTactic (mvarId : MVarId) (stx : Syntax) : TermElabM Unit :=
 
 /-- Run reduction tactic and return both the right-hand term (`q`) and the reduction proof, of
 type `Reduction p q`. -/
-def elabReductionProof (lhs : Expr) (stx : Syntax) : TermElabM (Expr × Expr) :=
-  elabTransformationProof TransformationGoal.Reduction lhs stx
+def elabReductionProof (lhs : Expr) (rhsName : Name) (stx : Syntax) : TermElabM (Expr × Expr) :=
+  elabTransformationProof TransformationGoal.Reduction lhs rhsName stx
 
 syntax (name := reduction)
   "reduction" ident "/" ident declSig ":=" Lean.Parser.Term.byTactic : command
 
 /-- Reduction command. -/
 @[command_elab «reduction»]
 def evalReduction : CommandElab := fun stx => match stx with
-| `(reduction $eqvId / $probId $declSig := $proofStx) => do
+| `(reduction $redId / $probId $declSig := $proofStx) => do
   liftTermElabM do
     let (binders, lhsStx) := expandDeclSig declSig.raw
     elabBindersEx binders.getArgs fun xs => do
@@ -40,7 +40,8 @@ def evalReduction : CommandElab := fun stx => match stx with
           mvarId.assign mvarVal }
         catch _ => pure ()
 
-      let (rhs, proof) ← elabReductionProof lhs proofStx.raw
+      let rhsName := probId.getId
+      let (rhs, proof) ← elabReductionProof lhs rhsName proofStx.raw
 
       -- Add reduced problem to the environment.
       let rhs ← instantiateMVars rhs
@@ -54,7 +55,7 @@ def evalReduction : CommandElab := fun stx => match stx with
           rhs
           (Lean.ReducibilityHints.regular 0)
           (DefinitionSafety.safe)
-          [probId.getId])
+          [])
 
       -- Add reduction proof to the environment.
       let proofTy ← inferType proof
@@ -64,108 +65,13 @@ def evalReduction : CommandElab := fun stx => match stx with
       let proof ← instantiateMVars proof
       Lean.addDecl <|
         Declaration.defnDecl
-          (mkDefinitionValEx eqvId.getId
+          (mkDefinitionValEx redId.getId
           []
           proofTy
           proof
           (Lean.ReducibilityHints.regular 0)
           (DefinitionSafety.safe)
-          [probId.getId])
+          [])
   | _ => throwUnsupportedSyntax
 
 end CvxLean
-
--- import Lean
--- import CvxLean.Lib.Minimization
--- import CvxLean.Syntax.Minimization
--- import CvxLean.Meta.Util.Expr
-
--- namespace CvxLean
-
--- open Lean Lean.Elab Lean.Meta Lean.Elab.Tactic Lean.Elab.Term Lean.Elab.Command
--- open Minimization
-
--- /-- Run the tactics written by the user. -/
--- partial def runReductionTactic (mvarId : MVarId) (tacticCode : Syntax)
--- : TermElabM Unit := do
---   -- Recall, `tacticCode` is the whole `by ...` expression.
---   let code := tacticCode[1]
---   instantiateMVarDeclMVars mvarId
---   withInfoHole mvarId do
---     let (fvarDone, mvarId) ← MVarId.intro mvarId `done
---     let remainingGoals ← Tactic.run mvarId do
---       withTacticInfoContext tacticCode do
---         evalTactic code
-
---     match remainingGoals with
---     | [] => pure ()
---     | [g] => do
---       MVarId.withContext g do
---         if ← isDefEq (← inferType $ mkMVar g) (← inferType $ mkFVar fvarDone) then
---           MVarId.assign g (mkFVar fvarDone)
---         else
---           reportUnsolvedGoals remainingGoals
---     | _ => reportUnsolvedGoals remainingGoals
-
---     synthesizeSyntheticMVars (mayPostpone := false)
-
--- /-- Run reduction tactic and add instantiate metavariables accordingly. -/
--- def elabReductionProof (stx : Syntax) (expectedType : Expr) : TermElabM Expr :=
---   withRef stx do
---     let syntheticMVarsSaved := (← get).syntheticMVars
---     modify fun s => { s with syntheticMVars := {} }
---     try
---       let mvar ← elabTerm stx (some expectedType)
---       if not mvar.isMVar then
---         throwError "Expected MVar."
---       let some mvarDecl ← getSyntheticMVarDecl? mvar.mvarId!
---         | throwError "SyntheticMVarDecl not found."
-
---       modify fun s => { s with syntheticMVars := {} }
-
---       match mvarDecl.kind with
---       | SyntheticMVarKind.tactic tacticCode savedContext =>
---         withSavedContext savedContext do
---           runReductionTactic mvar.mvarId! tacticCode
---       | _ => throwError "Expected SyntheticMVarDecl of kind tactic."
---       return ← instantiateMVars mvar
---     finally
---       modify fun s => { s with syntheticMVars :=
---         s.syntheticMVars.mergeBy (fun _ _ a => a) syntheticMVarsSaved }
-
--- syntax (name := reduction)
---   "reduction" ident "/" ident declSig ":=" Parser.Term.byTactic : command
-
--- /-- Reduction command. -/
--- @[command_elab «reduction»]
--- def evalReduction : CommandElab := fun stx => match stx with
--- | `(reduction $redId / $probId $declSig := $proof) => do
---   liftTermElabM do
---     let (binders, prob) := expandDeclSig declSig.raw
---     elabBindersEx binders.getArgs fun xs => do
---       let D1 ← Meta.mkFreshTypeMVar
---       let R1 ← Meta.mkFreshTypeMVar
---       let D2 ← Meta.mkFreshTypeMVar
---       let R2 ← Meta.mkFreshTypeMVar
---       let prob₁Ty := mkApp2 (Lean.mkConst ``Minimization) D1 R1
---       let prob ← elabTermAndSynthesizeEnsuringType prob (some $ prob₁Ty)
---       let R2Preorder ← Meta.mkFreshExprMVar
---         (some $ mkAppN (Lean.mkConst ``Preorder [levelZero]) #[R2])
---       let prob₂Ty := mkAppN (Lean.mkConst ``Minimization) #[D2, R2]
---       let prob₂ ← Meta.mkFreshExprMVar (some $ prob₂Ty)
---       let proof ← elabReductionProof proof.raw
---         (← mkArrow
---           (mkAppN (Lean.mkConst ``Solution) #[D2, R2, R2Preorder, prob₂])
---           (← mkAppM ``Solution #[prob]))
---       let prob₂ ← instantiateMVars prob₂
---       let prob₂ ← mkLambdaFVars (xs.map Prod.snd) prob₂
---       -- TODO: Generalize the function in Solve to add definitions inferring type.
---       Lean.addDecl $ Declaration.defnDecl (mkDefinitionValEx probId.getId [] (← inferType prob₂) prob₂ (Lean.ReducibilityHints.regular 0) (DefinitionSafety.safe) [probId.getId])
---       let proofTy ← instantiateMVars (← mkArrow
---           (mkAppN (Lean.mkConst ``Solution) #[D2, R2, R2Preorder, (mkAppN (Lean.mkConst probId.getId) (xs.map Prod.snd))])
---           (← mkAppM ``Solution #[prob]))
---       let proofTy ← mkForallFVars (xs.map Prod.snd) proofTy
---       let proof ← mkLambdaFVars (xs.map Prod.snd) proof
---       Lean.addDecl $ Declaration.defnDecl (mkDefinitionValEx redId.getId [] proofTy proof (Lean.ReducibilityHints.regular 0) (DefinitionSafety.safe) [probId.getId])
---       -- TODO: Definitional height for Lean.ReducibilityHints.regular.
--- | _ => throwUnsupportedSyntax

CvxLean/Command/Relaxation.lean

@@ -0,0 +1,77 @@
+import Lean
+import CvxLean.Lib.Relaxation
+import CvxLean.Syntax.Minimization
+import CvxLean.Meta.Util.Expr
+import CvxLean.Meta.Relaxation
+import CvxLean.Meta.TacticBuilder
+
+namespace CvxLean
+
+open Lean Elab Meta Tactic Term Command Minimization
+
+/--  -/
+def runRelaxationTactic (mvarId : MVarId) (stx : Syntax) : TermElabM Unit :=
+  runTransformationTactic TransformationGoal.Relaxation mvarId stx
+
+/-- Run Relaxation tactic and return both the right-hand term (`q`) and the relaxation proof, of
+type `Relaxation p q`. -/
+def elabRelaxationProof (lhs : Expr) (rhsName : Name) (stx : Syntax) : TermElabM (Expr × Expr) :=
+  elabTransformationProof TransformationGoal.Relaxation lhs rhsName stx
+
+syntax (name := relaxation)
+  "relaxation" ident "/" ident declSig ":=" Lean.Parser.Term.byTactic : command
+
+/-- Relaxation command. -/
+@[command_elab «relaxation»]
+def evalRelaxation : CommandElab := fun stx => match stx with
+| `(relaxation $relId / $probId $declSig := $proofStx) => do
+  liftTermElabM do
+    let (binders, lhsStx) := expandDeclSig declSig.raw
+    elabBindersEx binders.getArgs fun xs => do
+      let D ← Meta.mkFreshTypeMVar
+      let R ← Meta.mkFreshTypeMVar
+      let lhsTy := mkApp2 (Lean.mkConst ``Minimization) D R
+      let lhs ← elabTermAndSynthesizeEnsuringType lhsStx (some lhsTy)
+
+      -- NOTE: `instantiateMVars` does not infer the preorder instance.
+      for mvarId in ← getMVars lhs do
+        try {
+          let mvarVal ← synthInstance (← mvarId.getDecl).type
+          mvarId.assign mvarVal }
+        catch _ => pure ()
+
+      let rhsName := probId.getId
+      let (rhs, proof) ← elabRelaxationProof lhs rhsName proofStx.raw
+
+      -- Add relaxed problem to the environment.
+      let rhs ← instantiateMVars rhs
+      let rhs ← mkLambdaFVars (xs.map Prod.snd) rhs
+      let rhs ← instantiateMVars rhs
+      Lean.addDecl <|
+        Declaration.defnDecl
+          (mkDefinitionValEx probId.getId
+          []
+          (← inferType rhs)
+          rhs
+          (Lean.ReducibilityHints.regular 0)
+          (DefinitionSafety.safe)
+          [])
+
+      -- Add Relaxation proof to the environment.
+      let proofTy ← inferType proof
+      let proofTy ← mkForallFVars (xs.map Prod.snd) proofTy
+      let proofTy ← instantiateMVars proofTy
+      let proof ← mkLambdaFVars (xs.map Prod.snd) proof
+      let proof ← instantiateMVars proof
+      Lean.addDecl <|
+        Declaration.defnDecl
+          (mkDefinitionValEx relId.getId
+          []
+          proofTy
+          proof
+          (Lean.ReducibilityHints.regular 0)
+          (DefinitionSafety.safe)
+          [])
+  | _ => throwUnsupportedSyntax
+
+end CvxLean