feat: tactic builder and Lean Together demo

.github/workflows/main.yml

@@ -26,7 +26,7 @@ jobs:
       - name: Install elan
         run: |
           set -o pipefail
-          curl -sSfL https://github.com/leanprover/elan/releases/download/v1.4.5/elan-x86_64-unknown-linux-gnu.tar.gz | tar xz
+          curl -sSfL https://github.com/leanprover/elan/releases/download/v3.0.0/elan-x86_64-unknown-linux-gnu.tar.gz | tar xz
           ./elan-init -y --default-toolchain leanprover/lean4:v4.4.0-rc1
           echo "$HOME/.elan/bin" >> $GITHUB_PATH
       - name: Install Rust and Cargo
@@ -37,4 +37,13 @@ jobs:
         uses: actions/checkout@v3
       - name: Build CvxLean
         run: |
-          ./build.sh
+          set -o pipefail
+          lake update
+          lake exe cache get
+          lake run EggClean
+          lake build EggConvexify
+          lake build CvxLean
+      - name: Test CvxLean 
+        run: |
+          lake build CvxLeanTest
+          

CvxLean.lean

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

CvxLean/Command/Equivalence.lean

@@ -1,127 +1,72 @@
 import Lean
 import CvxLean.Lib.Equivalence
+import CvxLean.Syntax.Minimization
 import CvxLean.Meta.Util.Expr
+import CvxLean.Meta.Equivalence
+import CvxLean.Meta.TacticBuilder
 
 namespace CvxLean
 
-open Lean Lean.Elab Lean.Meta Lean.Elab.Tactic Lean.Elab.Term Lean.Elab.Command
-open Minimization
+open Lean Elab Meta Tactic Term Command Minimization
 
-macro "equivalence_rfl" : tactic =>
-  `(tactic| exact Minimization.Equivalence.refl _)
-
-/-- Simply run `tacticCode` in `mvarId`. -/
-partial def runEquivalenceTactic (mvarId : MVarId) (tacticCode : Syntax) :
-  TermElabM Unit := do
-  let tacStx := ⟨tacticCode[1]⟩
-  let code ← `(tactic| $tacStx <;> try { equivalence_rfl })
-  instantiateMVarDeclMVars mvarId
-
-  withInfoHole mvarId do
-    let remainingGoals ← Tactic.run mvarId do
-      withTacticInfoContext tacticCode do
-        evalTactic code
-
-    match remainingGoals with
-    | [] => pure ()
-    | _ => reportUnsolvedGoals remainingGoals
-
-    synthesizeSyntheticMVars (mayPostpone := false)
-
-/-- Run equivalence tactic and return both the right-hand term (`q`) and the
-equivalence proof, of type `Equivalence p q`. -/
-def elabEquivalenceProof (prob : Expr) (stx : Syntax) :
-  TermElabM (Expr × Expr) := do
-  withRef stx do
-    let syntheticMVarsSaved := (← get).syntheticMVars
-    modify fun s => { s with syntheticMVars := {} }
-    try
-      let probTy ← inferType prob
-      let R := probTy.getArg! 1
-      let D := probTy.getArg! 0
-      let E ← Meta.mkFreshTypeMVar
-      let RPreorder ← Meta.mkFreshExprMVar
-        (some <| mkAppN (Lean.mkConst ``Preorder [levelZero]) #[R])
-      let prob₂ ← Meta.mkFreshExprMVar
-        (some <| mkApp2 (Lean.mkConst ``Minimization) E R)
-      let eqvTy := mkAppN
-        (mkConst ``Minimization.Equivalence)
-        #[R, D, E, RPreorder, prob, prob₂]
-      let eqv ← elabTerm stx (some eqvTy)
-
-      let some mvarDecl ← getSyntheticMVarDecl? eqv.mvarId! |
-        throwError "SyntheticMVarDecl not found."
-
-      modify fun s => { s with syntheticMVars := {} }
-
-      match mvarDecl.kind with
-      | SyntheticMVarKind.tactic tacticCode savedContext =>
-          withSavedContext savedContext do
-            runEquivalenceTactic eqv.mvarId! tacticCode
-      | _ => throwError "Expected SyntheticMVarDecl of kind tactic, got {mvarDecl.kind}"
-
-      let eqvWitness ← instantiateMVars eqv
-      let eqvWitnessTy ← inferType eqvWitness
-      if eqvWitnessTy.isAppOf ``Minimization.Equivalence then
-        -- NOTE(RFM): Equivalence 0:R 1:D 2:E 3:RPreorder 4:p 5:q
-        let rhs := eqvWitnessTy.getArg! 5
-        return (rhs, eqvWitness)
-      else
-        throwError "Expected equivalence witness, got {eqvWitness}."
-    finally
-      modify fun s => { s with syntheticMVars :=
-        s.syntheticMVars.mergeBy (fun _ _ a => a) syntheticMVarsSaved }
+/--  -/
+partial def runEquivalenceTactic (mvarId : MVarId) (stx : Syntax) : TermElabM Unit := do
+  runTransformationTactic TransformationGoal.Equivalence mvarId stx
 
+/-- 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
 
 syntax (name := equivalence)
-  "equivalence" ident "/" ident declSig ":=" term : command
+  "equivalence" ident "/" ident declSig ":=" Lean.Parser.Term.byTactic : command
 
-/-- Create `equivalence` command. It is similar to the `reduction` command, but
-it is more strict as it requires the target and goal problem to be strongly
-equivalent, instead of simply building a map from solution spaces. -/
+/-- Create `equivalence` command. It is similar to the `reduction` command, but requires an
+`Equivalence` instead of a `Reduction`. -/
 @[command_elab «equivalence»]
 def evalEquivalence : CommandElab := fun stx => match stx with
-| `(equivalence $eqvId / $probId $declSig := $proof) => do
+| `(equivalence $eqvId / $probId $declSig := $proofStx) => do
   liftTermElabM do
-    let (binders, prob) := expandDeclSig declSig.raw
+    let (binders, lhsStx) := expandDeclSig declSig.raw
     elabBindersEx binders.getArgs fun xs => do
       let D ← Meta.mkFreshTypeMVar
       let R ← Meta.mkFreshTypeMVar
-      let prob₁Ty := mkApp2 (Lean.mkConst ``Minimization) D R
-      let prob₁ ← elabTermAndSynthesizeEnsuringType prob (some prob₁Ty)
+      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 prob₁ do
+      for mvarId in ← getMVars lhs do
         try {
           let mvarVal ← synthInstance (← mvarId.getDecl).type
           mvarId.assign mvarVal }
         catch _ => pure ()
 
-      let (prob₂, proof) ← elabEquivalenceProof prob₁ proof.raw
-      let prob₂ ← instantiateMVars prob₂
-      let prob₂ ← mkLambdaFVars (xs.map Prod.snd) prob₂
-      let prob₂ ← instantiateMVars prob₂
+      let (rhs, eqv) ← elabEquivalenceProof lhs proofStx.raw
+
+      -- Add equivalent 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 prob₂)
-        prob₂
-        (Lean.ReducibilityHints.regular 0)
-        (DefinitionSafety.safe)
-        [probId.getId])
+          (mkDefinitionValEx probId.getId
+          []
+          (← inferType rhs)
+          rhs
+          (Lean.ReducibilityHints.regular 0)
+          (DefinitionSafety.safe)
+          [probId.getId])
 
-      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
+      -- Add equivalence proof to the environment.
+      let eqvTy ← inferType eqv
+      let eqvTy ← instantiateMVars eqvTy
+      let eqv ← instantiateMVars eqv
       Lean.addDecl <|
         Declaration.defnDecl
           (mkDefinitionValEx eqvId.getId
           []
-          proofTy
-          proof
+          eqvTy
+          eqv
           (Lean.ReducibilityHints.regular 0)
           (DefinitionSafety.safe)
           [probId.getId])