Merge pull request 'feat: Prograde tactics' (#83) from tactic/eval into dev

Reviewed-on: #83

Pantograph.lean

@@ -125,7 +125,7 @@ def execute (command: Protocol.Command): MainM Lean.Json := do
           pure ( Except.ok (← goalAssign goalState args.goalId expr))
         | .none, .none, .some type, .none, .none => do
           let binderName := args.binderName?.getD ""
-          pure ( Except.ok (← goalHave goalState args.goalId binderName type))
+          pure ( Except.ok (← goalState.tryHave args.goalId binderName type))
         | .none, .none, .none, .some pred, .none => do
           pure ( Except.ok (← goalCalc goalState args.goalId pred))
         | .none, .none, .none, .none, .some true => do

Pantograph/Compile.lean

@@ -2,7 +2,7 @@
 import Pantograph.Protocol
 import Pantograph.Compile.Frontend
 import Pantograph.Compile.Elab
-
+import Pantograph.Compile.Parse
 
 open Lean
 

Pantograph/Compile/Parse.lean

@@ -0,0 +1,14 @@
+import Lean
+
+open Lean
+
+namespace Pantograph.Compile
+
+def parseTermM [Monad m] [MonadEnv m] (s: String): m (Except String Syntax) := do
+  return Parser.runParserCategory
+    (env := ← MonadEnv.getEnv)
+    (catName := `term)
+    (input := s)
+    (fileName := "<stdin>")
+
+end Pantograph.Compile

Pantograph/Goal.lean

@@ -5,6 +5,7 @@ All the functions starting with `try` resume their inner monadic state.
 -/
 import Pantograph.Protocol
 import Pantograph.Tactic
+import Pantograph.Compile.Parse
 import Lean
 
 
@@ -21,8 +22,6 @@ structure GoalState where
 
   -- The root hole which is the search target
   root: MVarId
-  -- New metavariables acquired in this state
-  newMVars: SSet MVarId
 
   -- Parent state metavariable source
   parentMVar?: Option MVarId
@@ -47,7 +46,6 @@ protected def GoalState.create (expr: Expr): Elab.TermElabM GoalState := do
   return {
     root,
     savedState,
-    newMVars := SSet.insert .empty root,
     parentMVar? := .none,
   }
 protected def GoalState.isConv (state: GoalState): Bool :=
@@ -88,15 +86,6 @@ private def GoalState.restoreTacticM (state: GoalState) (goal: MVarId): Elab.Tac
   Elab.Tactic.setGoals [goal]
 
 
-private def newMVarSet (mctxOld: @&MetavarContext) (mctxNew: @&MetavarContext): SSet MVarId :=
-  mctxNew.decls.foldl (fun acc mvarId mvarDecl =>
-    if let .some prevMVarDecl := mctxOld.decls.find? mvarId then
-      assert! prevMVarDecl.type == mvarDecl.type
-      acc
-    else
-      acc.insert mvarId
-    ) SSet.empty
-
 protected def GoalState.focus (state: GoalState) (goalId: Nat): Option GoalState := do
   let goal ← state.savedState.tactic.goals.get? goalId
   return {
@@ -165,6 +154,20 @@ protected def GoalState.getMVarEAssignment (goalState: GoalState) (mvar: MVarId)
 
 --- Tactic execution functions ---
 
+protected def GoalState.step (state: GoalState) (mvarId: MVarId) (tacticM: Elab.Tactic.TacticM Unit)
+  : Elab.TermElabM GoalState := do
+  unless (← getMCtx).decls.contains mvarId do
+    throwError s!"MVarId is not in context: {mvarId.name}"
+  mvarId.checkNotAssigned `GoalState.step
+  let (_, newGoals) ← tacticM { elaborator := .anonymous } |>.run { goals := [mvarId] }
+  let nextElabState ← MonadBacktrack.saveState
+  return {
+    state with
+    savedState := { term := nextElabState, tactic := newGoals },
+    parentMVar? := .some mvarId,
+    calcPrevRhs? := .none,
+  }
+
 /-- Response for executing a tactic -/
 inductive TacticResult where
   -- Goes to next state
@@ -179,35 +182,21 @@ inductive TacticResult where
   | invalidAction (message: String)
 
 /-- Executes a `TacticM` monads on this `GoalState`, collecting the errors as necessary -/
-protected def GoalState.executeTactic (state: GoalState) (goalId: Nat) (tacticM: Elab.Tactic.TacticM Unit):
+protected def GoalState.tryTacticM (state: GoalState) (goalId: Nat) (tacticM: Elab.Tactic.TacticM Unit):
       Elab.TermElabM TacticResult := do
-  state.restoreElabM
-  let goal ← match state.savedState.tactic.goals.get? goalId with
+  let mvarId ← match state.savedState.tactic.goals.get? goalId with
     | .some goal => pure $ goal
     | .none => return .indexError goalId
-  goal.checkNotAssigned `GoalState.executeTactic
   try
-    let (_, newGoals) ← tacticM { elaborator := .anonymous } |>.run { goals := [goal] }
-    if (← getThe Core.State).messages.hasErrors then
-      let messages := (← getThe Core.State).messages.toArray
-      let errors ← (messages.map (·.data)).mapM fun md => md.toString
-      return .failure errors
-    let nextElabState ← MonadBacktrack.saveState
-    let nextMCtx := nextElabState.meta.meta.mctx
-    let prevMCtx := state.mctx
-    return .success {
-      state with
-      savedState := { term := nextElabState, tactic := newGoals },
-      newMVars := newMVarSet prevMCtx nextMCtx,
-      parentMVar? := .some goal,
-      calcPrevRhs? := .none,
-    }
+    let nextState ← state.step mvarId tacticM
+    return .success nextState
   catch exception =>
     return .failure #[← exception.toMessageData.toString]
 
 /-- Execute a string tactic on given state -/
 protected def GoalState.tryTactic (state: GoalState) (goalId: Nat) (tactic: String):
     Elab.TermElabM TacticResult := do
+  state.restoreElabM
   let tactic ← match Parser.runParserCategory
     (env := ← MonadEnv.getEnv)
     (catName := if state.isConv then `conv else `tactic)
@@ -215,7 +204,7 @@ protected def GoalState.tryTactic (state: GoalState) (goalId: Nat) (tactic: Stri
     (fileName := filename) with
     | .ok stx => pure $ stx
     | .error error => return .parseError error
-  state.executeTactic goalId $ Elab.Tactic.evalTactic tactic
+  state.tryTacticM goalId $ Elab.Tactic.evalTactic tactic
 
 protected def GoalState.tryAssign (state: GoalState) (goalId: Nat) (expr: String):
       Elab.TermElabM TacticResult := do
@@ -227,103 +216,21 @@ protected def GoalState.tryAssign (state: GoalState) (goalId: Nat) (expr: String
     (fileName := filename) with
     | .ok syn => pure syn
     | .error error => return .parseError error
-  state.executeTactic goalId $ Tactic.evalAssign expr
+  state.tryTacticM goalId $ Tactic.evalAssign expr
 
 -- Specialized Tactics
 
-protected def GoalState.tryHave (state: GoalState) (goalId: Nat) (binderName: String) (type: String):
-      Elab.TermElabM TacticResult := do
-  state.restoreElabM
-  let goal ← match state.savedState.tactic.goals.get? goalId with
-    | .some goal => pure goal
-    | .none => return .indexError goalId
-  goal.checkNotAssigned `GoalState.tryHave
-  let type ← match Parser.runParserCategory
-    (env := state.env)
-    (catName := `term)
-    (input := type)
-    (fileName := filename) with
-    | .ok syn => pure syn
-    | .error error => return .parseError error
-  let binderName := binderName.toName
-  try
-    -- Implemented similarly to the intro tactic
-    let nextGoals: List MVarId ← goal.withContext do
-      let type ← Elab.Term.elabType (stx := type)
-      let lctx ← MonadLCtx.getLCtx
-
-      -- The branch goal inherits the same context, but with a different type
-      let mvarBranch ← Meta.mkFreshExprMVarAt lctx (← Meta.getLocalInstances) type
-
-      -- Create the context for the `upstream` goal
-      let fvarId ← mkFreshFVarId
-      let lctxUpstream := lctx.mkLocalDecl fvarId binderName type
-      let fvar   := mkFVar fvarId
-      let mvarUpstream ←
-        withTheReader Meta.Context (fun ctx => { ctx with lctx := lctxUpstream }) do
-          Meta.withNewLocalInstances #[fvar] 0 do
-            let mvarUpstream ← Meta.mkFreshExprMVarAt (← getLCtx) (← Meta.getLocalInstances)
-              (← goal.getType) (kind := MetavarKind.synthetic) (userName := .anonymous)
-            let expr: Expr := .app (.lam binderName type mvarBranch .default) mvarUpstream
-            goal.assign expr
-            pure mvarUpstream
-
-      pure [mvarBranch.mvarId!, mvarUpstream.mvarId!]
-    return .success {
-      root := state.root,
-      savedState := {
-        term := ← MonadBacktrack.saveState,
-        tactic := { goals := nextGoals }
-      },
-      newMVars := nextGoals.toSSet,
-      parentMVar? := .some goal,
-      calcPrevRhs? := .none
-    }
-  catch exception =>
-    return .failure #[← exception.toMessageData.toString]
 protected def GoalState.tryLet (state: GoalState) (goalId: Nat) (binderName: String) (type: String):
       Elab.TermElabM TacticResult := do
   state.restoreElabM
-  let goal ← match state.savedState.tactic.goals.get? goalId with
-    | .some goal => pure goal
-    | .none => return .indexError goalId
-  goal.checkNotAssigned `GoalState.tryLet
   let type ← match Parser.runParserCategory
-    (env := state.env)
+    (env := ← MonadEnv.getEnv)
     (catName := `term)
     (input := type)
     (fileName := filename) with
     | .ok syn => pure syn
     | .error error => return .parseError error
-  let binderName := binderName.toName
-  try
-    -- Implemented similarly to the intro tactic
-    let nextGoals: List MVarId ← goal.withContext do
-      let type ← Elab.Term.elabType (stx := type)
-      let lctx ← MonadLCtx.getLCtx
-
-      -- The branch goal inherits the same context, but with a different type
-      let mvarBranch ← Meta.mkFreshExprMVarAt lctx (← Meta.getLocalInstances) type
-
-      let upstreamType := .letE binderName type mvarBranch (← goal.getType) false
-      let mvarUpstream ← Meta.mkFreshExprMVarAt (← getLCtx) (← Meta.getLocalInstances)
-        upstreamType (kind := MetavarKind.synthetic) (userName := (← goal.getTag))
-
-      goal.assign mvarUpstream
-
-      pure [mvarBranch.mvarId!, mvarUpstream.mvarId!]
-    return .success {
-      root := state.root,
-      savedState := {
-        term := ← MonadBacktrack.saveState,
-        tactic := { goals := nextGoals }
-      },
-      newMVars := nextGoals.toSSet,
-      parentMVar? := .some goal,
-      calcPrevRhs? := .none
-    }
-  catch exception =>
-    return .failure #[← exception.toMessageData.toString]
+  state.tryTacticM goalId $ Tactic.evalLet binderName.toName type
 
 /-- Enter conv tactic mode -/
 protected def GoalState.conv (state: GoalState) (goalId: Nat):
@@ -345,12 +252,9 @@ protected def GoalState.conv (state: GoalState) (goalId: Nat):
     return (← MonadBacktrack.saveState, convMVar)
   try
     let (nextSavedState, convRhs) ← tacticM { elaborator := .anonymous } |>.run' state.savedState.tactic
-    let prevMCtx := state.mctx
-    let nextMCtx := nextSavedState.term.meta.meta.mctx
     return .success {
       root := state.root,
       savedState := nextSavedState
-      newMVars := newMVarSet prevMCtx nextMCtx,
       parentMVar? := .some goal,
       convMVar? := .some (convRhs, goal),
       calcPrevRhs? := .none
@@ -384,12 +288,9 @@ protected def GoalState.convExit (state: GoalState):
     MonadBacktrack.saveState
   try
     let nextSavedState ← tacticM { elaborator := .anonymous } |>.run' state.savedState.tactic
-    let nextMCtx := nextSavedState.term.meta.meta.mctx
-    let prevMCtx := state.savedState.term.meta.meta.mctx
     return .success {
       root := state.root,
       savedState := nextSavedState
-      newMVars := newMVarSet prevMCtx nextMCtx,
       parentMVar? := .some convGoal,
       convMVar? := .none
       calcPrevRhs? := .none
@@ -469,7 +370,6 @@ protected def GoalState.tryCalc (state: GoalState) (goalId: Nat) (pred: String):
         term := ← MonadBacktrack.saveState,
         tactic := { goals },
       },
-      newMVars := goals.toSSet,
       parentMVar? := .some goal,
       calcPrevRhs?
     }
@@ -480,24 +380,16 @@ protected def GoalState.tryCalc (state: GoalState) (goalId: Nat) (pred: String):
 protected def GoalState.tryMotivatedApply (state: GoalState) (goalId: Nat) (recursor: String):
       Elab.TermElabM TacticResult := do
   state.restoreElabM
-  let recursor ← match Parser.runParserCategory
-    (env := state.env)
-    (catName := `term)
-    (input := recursor)
-    (fileName := filename) with
+  let recursor ← match (← Compile.parseTermM recursor) with
     | .ok syn => pure syn
     | .error error => return .parseError error
-  state.executeTactic goalId (tacticM := Tactic.motivatedApply recursor)
+  state.tryTacticM goalId (tacticM := Tactic.evalMotivatedApply recursor)
 protected def GoalState.tryNoConfuse (state: GoalState) (goalId: Nat) (eq: String):
       Elab.TermElabM TacticResult := do
   state.restoreElabM
-  let recursor ← match Parser.runParserCategory
-    (env := state.env)
-    (catName := `term)
-    (input := eq)
-    (fileName := filename) with
+  let eq ← match (← Compile.parseTermM eq) with
     | .ok syn => pure syn
     | .error error => return .parseError error
-  state.executeTactic goalId (tacticM := Tactic.noConfuse recursor)
+  state.tryTacticM goalId (tacticM := Tactic.evalNoConfuse eq)
 
 end Pantograph

Pantograph/Library.lean

@@ -162,8 +162,21 @@ def goalTactic (state: GoalState) (goalId: Nat) (tactic: String): CoreM TacticRe
 def goalAssign (state: GoalState) (goalId: Nat) (expr: String): CoreM TacticResult :=
   runTermElabM <| state.tryAssign goalId expr
 @[export pantograph_goal_have_m]
-def goalHave (state: GoalState) (goalId: Nat) (binderName: String) (type: String): CoreM TacticResult :=
-  runTermElabM <| state.tryHave goalId binderName type
+protected def GoalState.tryHave (state: GoalState) (goalId: Nat) (binderName: String) (type: String): CoreM TacticResult := do
+  let type ← match (← Compile.parseTermM type) with
+    | .ok syn => pure syn
+    | .error error => return .parseError error
+  runTermElabM do
+    state.restoreElabM
+    state.tryTacticM goalId $ Tactic.evalHave binderName.toName type
+@[export pantograph_goal_try_define_m]
+protected def GoalState.tryDefine (state: GoalState) (goalId: Nat) (binderName: String) (expr: String): CoreM TacticResult := do
+  let expr ← match (← Compile.parseTermM expr) with
+    | .ok syn => pure syn
+    | .error error => return .parseError error
+  runTermElabM do
+    state.restoreElabM
+    state.tryTacticM goalId (Tactic.evalDefine binderName.toName expr)
 @[export pantograph_goal_let_m]
 def goalLet (state: GoalState) (goalId: Nat) (binderName: String) (type: String): CoreM TacticResult :=
   runTermElabM <| state.tryLet goalId binderName type
@@ -179,11 +192,5 @@ def goalCalc (state: GoalState) (goalId: Nat) (pred: String): CoreM TacticResult
 @[export pantograph_goal_focus]
 def goalFocus (state: GoalState) (goalId: Nat): Option GoalState :=
   state.focus goalId
-@[export pantograph_goal_motivated_apply_m]
-def goalMotivatedApply (state: GoalState) (goalId: Nat) (recursor: String): CoreM TacticResult :=
-  runTermElabM <| state.tryMotivatedApply goalId recursor
-@[export pantograph_goal_no_confuse_m]
-def goalNoConfuse (state: GoalState) (goalId: Nat) (eq: String): CoreM TacticResult :=
-  runTermElabM <| state.tryNoConfuse goalId eq
 
 end Pantograph

Pantograph/Protocol.lean

@@ -51,7 +51,7 @@ structure Variable where
   /-- The name displayed to the user -/
   userName: String
   /-- Does the name contain a dagger -/
-  isInaccessible?: Option Bool := .none
+  isInaccessible: Bool := false
   type?: Option Expression  := .none
   value?: Option Expression := .none
   deriving Lean.ToJson

Pantograph/Serial.lean

@@ -200,7 +200,7 @@ def serializeExpression (options: @&Protocol.Options) (e: Expr): MetaM Protocol.
 
 
 /-- Adapted from ppGoal -/
-def serializeGoal (options: @&Protocol.Options) (goal: MVarId) (mvarDecl: MetavarDecl) (parentDecl?: Option MetavarDecl)
+def serializeGoal (options: @&Protocol.Options) (goal: MVarId) (mvarDecl: MetavarDecl) (parentDecl?: Option MetavarDecl := .none)
       : MetaM Protocol.Goal := do
   -- Options for printing; See Meta.ppGoal for details
   let showLetValues  := true
@@ -215,11 +215,13 @@ def serializeGoal (options: @&Protocol.Options) (goal: MVarId) (mvarDecl: Metava
         return {
           name := ofName fvarId.name,
           userName:= ofName userName.simpMacroScopes,
+          isInaccessible := userName.isInaccessibleUserName
         }
       | .ldecl _ fvarId userName _ _ _ _ => do
         return {
           name := ofName fvarId.name,
           userName := toString userName.simpMacroScopes,
+          isInaccessible := userName.isInaccessibleUserName
         }
     let ppVar (localDecl : LocalDecl) : MetaM Protocol.Variable := do
       match localDecl with
@@ -229,7 +231,7 @@ def serializeGoal (options: @&Protocol.Options) (goal: MVarId) (mvarDecl: Metava
         return {
           name := ofName fvarId.name,
           userName:= ofName userName,
-          isInaccessible? := .some userName.isInaccessibleUserName
+          isInaccessible := userName.isInaccessibleUserName
           type? := .some (← serializeExpression options type)
         }
       | .ldecl _ fvarId userName type val _ _ => do
@@ -243,7 +245,7 @@ def serializeGoal (options: @&Protocol.Options) (goal: MVarId) (mvarDecl: Metava
         return {
           name := ofName fvarId.name,
           userName:= ofName userName,
-          isInaccessible? := .some userName.isInaccessibleUserName
+          isInaccessible := userName.isInaccessibleUserName
           type? := .some (← serializeExpression options type)
           value? := value?
         }
@@ -287,7 +289,8 @@ protected def GoalState.serializeGoals
 
 /-- Print the metavariables in a readable format -/
 @[export pantograph_goal_state_diag_m]
-protected def GoalState.diag (goalState: GoalState) (parent?: Option GoalState := .none) (options: Protocol.GoalDiag := {}): MetaM String := do
+protected def GoalState.diag (goalState: GoalState) (parent?: Option GoalState := .none) (options: Protocol.GoalDiag := {}): CoreM String := do
+  let metaM: MetaM String := do
     goalState.restoreMetaM
     let savedState := goalState.savedState
     let goals := savedState.tactic.goals
@@ -310,6 +313,7 @@ protected def GoalState.diag (goalState: GoalState) (parent?: Option GoalState :
           printMVar pref mvarId decl
         )
     pure $ result ++ "\n" ++ (resultGoals.map (· ++ "\n") |> String.join) ++ (resultOthers.map (· ++ "\n") |> String.join)
+  metaM.run' {}
   where
     printMVar (pref: String) (mvarId: MVarId) (decl: MetavarDecl): MetaM String := mvarId.withContext do
       let resultFVars: List String ←

Pantograph/Tactic.lean

@@ -1,5 +1,5 @@
-
 import Pantograph.Tactic.Assign
 import Pantograph.Tactic.Congruence
 import Pantograph.Tactic.MotivatedApply
 import Pantograph.Tactic.NoConfuse
+import Pantograph.Tactic.Prograde

Pantograph/Tactic/Assign.lean

@@ -4,15 +4,8 @@ open Lean
 
 namespace Pantograph.Tactic
 
-private def newMVarSet (mctxOld: @&MetavarContext) (mctxNew: @&MetavarContext): SSet MVarId :=
-  mctxNew.decls.foldl (fun acc mvarId mvarDecl =>
-    if let .some prevMVarDecl := mctxOld.decls.find? mvarId then
-      assert! prevMVarDecl.type == mvarDecl.type
-      acc
-    else
-      acc.insert mvarId
-    ) SSet.empty
-def assign (goal: MVarId) (expr: Expr): MetaM (List MVarId) := do
+/-- WARNING: This should be used with a function like `elabTermWithHoles` that properly collects the mvar information from `expr`. -/
+def assign (goal: MVarId) (expr: Expr) (nextGoals: List MVarId): MetaM (List MVarId) := do
   goal.checkNotAssigned `Pantograph.Tactic.assign
 
   -- This run of the unifier is critical in resolving mvars in passing
@@ -20,15 +13,18 @@ def assign (goal: MVarId) (expr: Expr): MetaM (List MVarId) := do
   let goalType ← goal.getType
   unless ← Meta.isDefEq goalType exprType do
     throwError s!"{← Meta.ppExpr expr} : {← Meta.ppExpr exprType} ≠ {← Meta.ppExpr goalType}"
-
-  let nextGoals ← Meta.getMVars expr
   goal.assign expr
-  nextGoals.toList.filterM (not <$> ·.isAssigned)
+  nextGoals.filterM (not <$> ·.isAssigned)
 
 def evalAssign : Elab.Tactic.Tactic := fun stx => Elab.Tactic.withMainContext do
-  let goalType ← Elab.Tactic.getMainTarget
-  let expr ← Elab.Term.elabTermAndSynthesize (stx := stx) (expectedType? := .some goalType)
-  let nextGoals ← assign (← Elab.Tactic.getMainGoal) expr
+  let target ← Elab.Tactic.getMainTarget
+  let goal ← Elab.Tactic.getMainGoal
+  goal.checkNotAssigned `Pantograph.Tactic.evalAssign
+  let (expr, nextGoals) ← Elab.Tactic.elabTermWithHoles stx
+    (expectedType? := .some target)
+    (tagSuffix := .anonymous )
+    (allowNaturalHoles := true)
+  goal.assign expr
   Elab.Tactic.setGoals nextGoals
 
 

Pantograph/Tactic/Congruence.lean

@@ -4,12 +4,12 @@ open Lean
 
 namespace Pantograph.Tactic
 
-def congruenceArg: Elab.Tactic.TacticM Unit := do
-  let goal ← Elab.Tactic.getMainGoal
-  let .some (β, _, _) := (← goal.getType).eq? | throwError "Goal is not an Eq"
-  let userName := (← goal.getDecl).userName
+def congruenceArg (mvarId: MVarId): MetaM (List MVarId) := mvarId.withContext do
+  mvarId.checkNotAssigned `Pantograph.Tactic.congruenceArg
+  let target ← mvarId.getType
+  let .some (β, _, _) := target.eq? | throwError "Goal is not an Eq"
+  let userName := (← mvarId.getDecl).userName
 
-  let nextGoals ← goal.withContext do
   let u ← Meta.mkFreshLevelMVar
   let α ← Meta.mkFreshExprMVar (.some $ mkSort u)
     .natural (userName := userName ++ `α)
@@ -21,19 +21,23 @@ def congruenceArg: Elab.Tactic.TacticM Unit := do
     .synthetic (userName := userName ++ `a₂)
   let h ← Meta.mkFreshExprMVar (.some $ ← Meta.mkEq a₁ a₂)
     .synthetic (userName := userName ++ `h)
-    let conduitType ← Meta.mkEq (← Meta.mkEq (.app f a₁) (.app f a₂)) (← goal.getType)
+  let conduitType ← Meta.mkEq (← Meta.mkEq (.app f a₁) (.app f a₂)) target
   let conduit ← Meta.mkFreshExprMVar conduitType
     .synthetic (userName := userName ++ `conduit)
-    goal.assign $ ← Meta.mkEqMP conduit (← Meta.mkCongrArg f h)
-    return [α, a₁, a₂, f,  h, conduit]
-  Elab.Tactic.setGoals <| nextGoals.map (·.mvarId!)
+  mvarId.assign $ ← Meta.mkEqMP conduit (← Meta.mkCongrArg f h)
+  let result := [α, a₁, a₂, f,  h, conduit]
+  return result.map (·.mvarId!)
 
-def congruenceFun: Elab.Tactic.TacticM Unit := do
+def evalCongruenceArg: Elab.Tactic.TacticM Unit := do
   let goal ← Elab.Tactic.getMainGoal
-  let .some (β, _, _) := (← goal.getType).eq? | throwError "Goal is not an Eq"
-  let userName := (← goal.getDecl).userName
+  let nextGoals ← congruenceArg goal
+  Elab.Tactic.setGoals nextGoals
 
-  let nextGoals ← goal.withContext do
+def congruenceFun (mvarId: MVarId): MetaM (List MVarId) := mvarId.withContext do
+  mvarId.checkNotAssigned `Pantograph.Tactic.congruenceFun
+  let target ← mvarId.getType
+  let .some (β, _, _) := target.eq? | throwError "Goal is not an Eq"
+  let userName := (← mvarId.getDecl).userName
   let u ← Meta.mkFreshLevelMVar
   let α ← Meta.mkFreshExprMVar (.some $ mkSort u)
     .natural (userName := userName ++ `α)
@@ -46,19 +50,23 @@ def congruenceFun: Elab.Tactic.TacticM Unit := do
     .synthetic (userName := userName ++ `a)
   let h ← Meta.mkFreshExprMVar (.some $ ← Meta.mkEq f₁ f₂)
     .synthetic (userName := userName ++ `h)
-    let conduitType ← Meta.mkEq (← Meta.mkEq (.app f₁ a) (.app f₂ a)) (← goal.getType)
+  let conduitType ← Meta.mkEq (← Meta.mkEq (.app f₁ a) (.app f₂ a)) target
   let conduit ← Meta.mkFreshExprMVar conduitType
     .synthetic (userName := userName ++ `conduit)
-    goal.assign $ ← Meta.mkEqMP conduit (← Meta.mkCongrFun h a)
-    return [α, f₁, f₂, h, a, conduit]
-  Elab.Tactic.setGoals <| nextGoals.map (·.mvarId!)
+  mvarId.assign $ ← Meta.mkEqMP conduit (← Meta.mkCongrFun h a)
+  let result := [α, f₁, f₂, h, a, conduit]
+  return result.map (·.mvarId!)
 
-def congruence: Elab.Tactic.TacticM Unit := do
+def evalCongruenceFun: Elab.Tactic.TacticM Unit := do
   let goal ← Elab.Tactic.getMainGoal
-  let .some (β, _, _) := (← goal.getType).eq? | throwError "Goal is not an Eq"
-  let userName := (← goal.getDecl).userName
+  let nextGoals ← congruenceFun goal
+  Elab.Tactic.setGoals nextGoals
 
-  let nextGoals ← goal.withContext do
+def congruence (mvarId: MVarId): MetaM (List MVarId) := mvarId.withContext do
+  mvarId.checkNotAssigned `Pantograph.Tactic.congruence
+  let target ← mvarId.getType
+  let .some (β, _, _) := target.eq? | throwError "Goal is not an Eq"
+  let userName := (← mvarId.getDecl).userName
   let u ← Meta.mkFreshLevelMVar
   let α ← Meta.mkFreshExprMVar (.some $ mkSort u)
     .natural (userName := userName ++ `α)
@@ -75,11 +83,16 @@ def congruence: Elab.Tactic.TacticM Unit := do
     .synthetic (userName := userName ++ `h₁)
   let h₂ ← Meta.mkFreshExprMVar (.some $ ← Meta.mkEq a₁ a₂)
     .synthetic (userName := userName ++ `h₂)
-    let conduitType ← Meta.mkEq (← Meta.mkEq (.app f₁ a₁) (.app f₂ a₂)) (← goal.getType)
+  let conduitType ← Meta.mkEq (← Meta.mkEq (.app f₁ a₁) (.app f₂ a₂)) target
   let conduit ← Meta.mkFreshExprMVar conduitType
     .synthetic (userName := userName ++ `conduit)
-    goal.assign $ ← Meta.mkEqMP conduit (← Meta.mkCongr h₁ h₂)
-    return [α, f₁, f₂, a₁, a₂, h₁, h₂, conduit]
-  Elab.Tactic.setGoals <| nextGoals.map (·.mvarId!)
+  mvarId.assign $ ← Meta.mkEqMP conduit (← Meta.mkCongr h₁ h₂)
+  let result := [α, f₁, f₂, a₁, a₂, h₁, h₂, conduit]
+  return result.map (·.mvarId!)
+
+def evalCongruence: Elab.Tactic.TacticM Unit := do
+  let goal ← Elab.Tactic.getMainGoal
+  let nextGoals ← congruence goal
+  Elab.Tactic.setGoals nextGoals
 
 end Pantograph.Tactic

Pantograph/Tactic/MotivatedApply.lean

@@ -62,13 +62,10 @@ def collectMotiveArguments (forallBody: Expr): SSet Nat :=
   | _ => SSet.empty
 
 /-- Applies a symbol of the type `∀ (motive: α → Sort u) (a: α)..., (motive α)` -/
-def motivatedApply: Elab.Tactic.Tactic := λ stx => do
-  let goal ← Elab.Tactic.getMainGoal
-  let nextGoals: List MVarId ← goal.withContext do
-    let recursor ← Elab.Term.elabTerm (stx := stx) .none
+def motivatedApply (mvarId: MVarId) (recursor: Expr) : MetaM (Array Meta.InductionSubgoal) := mvarId.withContext do
+  mvarId.checkNotAssigned `Pantograph.Tactic.motivatedApply
   let recursorType ← Meta.inferType recursor
-
-    let resultant ← goal.getType
+  let resultant ← mvarId.getType
 
   let info ← match getRecursorInformation recursorType with
     | .some info => pure info
@@ -95,11 +92,14 @@ def motivatedApply: Elab.Tactic.Tactic := λ stx => do
   -- Create the conduit type which proves the result of the motive is equal to the goal
   let conduitType ← info.conduitType newMVars resultant
   let goalConduit ← Meta.mkFreshExprMVar conduitType .natural (userName := `conduit)
-    goal.assign $ ← Meta.mkEqMP goalConduit (mkAppN recursor newMVars)
+  mvarId.assign $ ← Meta.mkEqMP goalConduit (mkAppN recursor newMVars)
   newMVars := newMVars ++ [goalConduit]
 
-    let nextGoals := newMVars.toList.map (·.mvarId!)
-    pure nextGoals
-  Elab.Tactic.setGoals nextGoals
+  return newMVars.map (λ mvar => { mvarId := mvar.mvarId!})
+
+def evalMotivatedApply : Elab.Tactic.Tactic := fun stx => Elab.Tactic.withMainContext do
+  let recursor ← Elab.Term.elabTerm (stx := stx) .none
+  let nextGoals ← motivatedApply (← Elab.Tactic.getMainGoal) recursor
+  Elab.Tactic.setGoals $ nextGoals.toList.map (·.mvarId)
 
 end Pantograph.Tactic

Pantograph/Tactic/NoConfuse.lean

@@ -4,15 +4,19 @@ open Lean
 
 namespace Pantograph.Tactic
 
-def noConfuse: Elab.Tactic.Tactic := λ stx => do
-  let goal ← Elab.Tactic.getMainGoal
-  goal.withContext do
-    let absurd ← Elab.Term.elabTerm (stx := stx) .none
-    let noConfusion ← Meta.mkNoConfusion (target := ← goal.getType) (h := absurd)
+def noConfuse (mvarId: MVarId) (h: Expr): MetaM Unit := mvarId.withContext do
+  mvarId.checkNotAssigned `Pantograph.Tactic.noConfuse
+  let target ← mvarId.getType
+  let noConfusion ← Meta.mkNoConfusion (target := target) (h := h)
 
-    unless ← Meta.isDefEq (← Meta.inferType noConfusion) (← goal.getType) do
-      throwError "invalid noConfuse call: The resultant type {← Meta.ppExpr $ ← Meta.inferType noConfusion} cannot be unified with {← Meta.ppExpr $ ← goal.getType}"
-    goal.assign noConfusion
+  unless ← Meta.isDefEq (← Meta.inferType noConfusion) target do
+    throwError "invalid noConfuse call: The resultant type {← Meta.ppExpr $ ← Meta.inferType noConfusion} cannot be unified with {← Meta.ppExpr target}"
+  mvarId.assign noConfusion
+
+def evalNoConfuse: Elab.Tactic.Tactic := λ stx => do
+  let goal ← Elab.Tactic.getMainGoal
+  let h ← goal.withContext $ Elab.Term.elabTerm (stx := stx) .none
+  noConfuse goal h
   Elab.Tactic.setGoals []
 
 end Pantograph.Tactic

Pantograph/Tactic/Prograde.lean

@@ -0,0 +1,87 @@
+/- Prograde (forward) reasoning tactics -/
+
+import Lean
+open Lean
+
+namespace Pantograph.Tactic
+
+/-- Introduces a fvar to the current mvar -/
+def define (mvarId: MVarId) (binderName: Name) (expr: Expr): MetaM (FVarId × MVarId) := mvarId.withContext do
+  mvarId.checkNotAssigned `Pantograph.Tactic.define
+  let type ← Meta.inferType expr
+
+  Meta.withLetDecl binderName type expr λ fvar => do
+    let mvarUpstream ← Meta.mkFreshExprMVarAt (← getLCtx) (← Meta.getLocalInstances)
+      (← mvarId.getType) (kind := MetavarKind.synthetic) (userName := .anonymous)
+    mvarId.assign mvarUpstream
+    pure (fvar.fvarId!, mvarUpstream.mvarId!)
+
+def evalDefine (binderName: Name) (expr: Syntax): Elab.Tactic.TacticM Unit := do
+  let goal ← Elab.Tactic.getMainGoal
+  let expr ← goal.withContext $ Elab.Term.elabTerm (stx := expr) (expectedType? := .none)
+  let (_, mvarId) ← define goal binderName expr
+  Elab.Tactic.setGoals [mvarId]
+
+structure BranchResult where
+  fvarId?: Option FVarId := .none
+  branch: MVarId
+  main: MVarId
+
+def «have» (mvarId: MVarId) (binderName: Name) (type: Expr): MetaM BranchResult := mvarId.withContext do
+  mvarId.checkNotAssigned `Pantograph.Tactic.have
+  let lctx ← MonadLCtx.getLCtx
+  -- The branch goal inherits the same context, but with a different type
+  let mvarBranch ← Meta.mkFreshExprMVarAt lctx (← Meta.getLocalInstances) type
+
+  -- Create the context for the `upstream` goal
+  let fvarId ← mkFreshFVarId
+  let lctxUpstream := lctx.mkLocalDecl fvarId binderName type
+  let mvarUpstream ←
+    withTheReader Meta.Context (fun ctx => { ctx with lctx := lctxUpstream }) do
+      Meta.withNewLocalInstances #[.fvar fvarId] 0 do
+        let mvarUpstream ← Meta.mkFreshExprMVarAt (← getLCtx) (← Meta.getLocalInstances)
+          (← mvarId.getType) (kind := MetavarKind.synthetic) (userName := ← mvarId.getTag)
+        --let expr: Expr := .app (.lam binderName type mvarBranch .default) mvarUpstream
+        mvarId.assign mvarUpstream
+        pure mvarUpstream
+
+  return {
+    fvarId? := .some fvarId,
+    branch := mvarBranch.mvarId!,
+    main := mvarUpstream.mvarId!,
+  }
+
+def evalHave (binderName: Name) (type: Syntax): Elab.Tactic.TacticM Unit := do
+  let goal ← Elab.Tactic.getMainGoal
+  let nextGoals: List MVarId ← goal.withContext do
+    let type ← Elab.Term.elabType (stx := type)
+    let result ← «have» goal binderName type
+    pure [result.branch, result.main]
+  Elab.Tactic.setGoals nextGoals
+
+def «let» (mvarId: MVarId) (binderName: Name) (type: Expr): MetaM BranchResult := mvarId.withContext do
+  mvarId.checkNotAssigned `Pantograph.Tactic.let
+  let lctx ← MonadLCtx.getLCtx
+
+  -- The branch goal inherits the same context, but with a different type
+  let mvarBranch ← Meta.mkFreshExprMVarAt lctx (← Meta.getLocalInstances) type (userName := binderName)
+
+  assert! ¬ type.hasLooseBVars
+  let mvarUpstream ← Meta.withLetDecl binderName type mvarBranch $ λ fvar => do
+    let mvarUpstream ← Meta.mkFreshExprMVarAt (← getLCtx) (← Meta.getLocalInstances)
+      (type := ← mvarId.getType) (kind := MetavarKind.synthetic) (userName := ← mvarId.getTag)
+    mvarId.assign $ .letE binderName type fvar mvarUpstream (nonDep := false)
+    pure mvarUpstream
+
+  return {
+    branch := mvarBranch.mvarId!,
+    main := mvarUpstream.mvarId!,
+  }
+
+def evalLet (binderName: Name) (type: Syntax): Elab.Tactic.TacticM Unit := do
+  let goal ← Elab.Tactic.getMainGoal
+  let type ← goal.withContext $ Elab.Term.elabType (stx := type)
+  let result ← «let» goal binderName type
+  Elab.Tactic.setGoals [result.branch, result.main]
+
+end Pantograph.Tactic

Test/Common.lean

@@ -1,6 +1,7 @@
 import Pantograph.Goal
 import Pantograph.Library
 import Pantograph.Protocol
+import Pantograph.Condensed
 import Lean
 import LSpec
 
@@ -10,12 +11,7 @@ namespace Pantograph
 
 deriving instance Repr for Expr
 -- Use strict equality check for expressions
---instance : BEq Expr := ⟨Expr.equal⟩
-instance (priority := 80) (x y : Expr) : LSpec.Testable (x.equal y) :=
-  if h : Expr.equal x y then
-    .isTrue h
-  else
-    .isFalse h $ s!"Expected to be equalaaa: '{x.dbgToString}' and '{y.dbgToString}'"
+instance : BEq Expr := ⟨Expr.equal⟩
 
 def uniq (n: Nat): Name := .num (.str .anonymous "_uniq") n
 
@@ -25,6 +21,7 @@ def Goal.devolatilizeVars (goal: Goal): Goal :=
   {
     goal with
     vars := goal.vars.map removeInternalAux,
+
   }
   where removeInternalAux (v: Variable): Variable :=
     {
@@ -47,6 +44,24 @@ deriving instance DecidableEq, Repr for InteractionError
 deriving instance DecidableEq, Repr for Option
 end Protocol
 
+namespace Condensed
+
+deriving instance BEq, Repr for LocalDecl
+deriving instance BEq, Repr for Goal
+
+protected def LocalDecl.devolatilize (decl: LocalDecl): LocalDecl :=
+  {
+    decl with fvarId := { name := .anonymous }
+  }
+protected def Goal.devolatilize (goal: Goal): Goal :=
+  {
+    goal with
+    mvarId := { name := .anonymous },
+    context := goal.context.map LocalDecl.devolatilize
+  }
+
+end Condensed
+
 def TacticResult.toString : TacticResult → String
   | .success state => s!".success ({state.goals.length} goals)"
   | .failure messages =>
@@ -73,11 +88,13 @@ def runCoreMSeq (env: Environment) (coreM: CoreM LSpec.TestSeq) (options: Array
 def runMetaMSeq (env: Environment) (metaM: MetaM LSpec.TestSeq): IO LSpec.TestSeq :=
   runCoreMSeq env metaM.run'
 def runTermElabMInMeta { α } (termElabM: Lean.Elab.TermElabM α): Lean.MetaM α :=
-  termElabM.run' (ctx := Pantograph.Condensed.elabContext)
+  termElabM.run' (ctx := Condensed.elabContext)
+def runTermElabMSeq (env: Environment) (termElabM: Elab.TermElabM LSpec.TestSeq): IO LSpec.TestSeq :=
+  runMetaMSeq env $ termElabM.run' (ctx := Condensed.elabContext)
 
 def exprToStr (e: Expr): Lean.MetaM String := toString <$> Meta.ppExpr e
 
-def parseSentence (s: String): MetaM Expr := do
+def parseSentence (s: String): Elab.TermElabM Expr := do
   let recursor ← match Parser.runParserCategory
     (env := ← MonadEnv.getEnv)
     (catName := `term)
@@ -85,7 +102,7 @@ def parseSentence (s: String): MetaM Expr := do
     (fileName := filename) with
     | .ok syn => pure syn
     | .error error => throwError "Failed to parse: {error}"
-  runTermElabMInMeta $ Elab.Term.elabTerm (stx := recursor) .none
+  Elab.Term.elabTerm (stx := recursor) .none
 
 def runTacticOnMVar (tacticM: Elab.Tactic.TacticM Unit) (goal: MVarId): Elab.TermElabM (List MVarId) := do
     let (_, newGoals) ← tacticM { elaborator := .anonymous } |>.run { goals := [goal] }
@@ -95,6 +112,35 @@ def mvarUserNameAndType (mvarId: MVarId): MetaM (Name × String) := do
   let t ← exprToStr (← mvarId.getType)
   return (name, t)
 
+
+-- Monadic testing
+
+abbrev TestT := StateT LSpec.TestSeq
+
+def addTest [Monad m] (test: LSpec.TestSeq): TestT m Unit := do
+  set $ (← get) ++ test
+
+def runTest [Monad m] (t: TestT m Unit): m LSpec.TestSeq :=
+  Prod.snd <$> t.run LSpec.TestSeq.done
+
+def runTestTermElabM (env: Environment) (t: TestT Elab.TermElabM Unit):
+  IO LSpec.TestSeq :=
+  runTermElabMSeq env $ runTest t
+
+def cdeclOf (userName: Name) (type: Expr): Condensed.LocalDecl :=
+  { userName, type }
+
+def buildGoal (nameType: List (String × String)) (target: String) (userName?: Option String := .none):
+    Protocol.Goal :=
+  {
+    userName?,
+    target := { pp? := .some target},
+    vars := (nameType.map fun x => ({
+      userName := x.fst,
+      type? := .some { pp? := .some x.snd },
+    })).toArray
+  }
+
 end Test
 
 end Pantograph

Test/Integration.lean

@@ -85,14 +85,14 @@ def test_tactic : IO LSpec.TestSeq :=
   let goal1: Protocol.Goal := {
     name := "_uniq.11",
     target := { pp? := .some "∀ (q : Prop), x ∨ q → q ∨ x" },
-    vars := #[{ name := "_uniq.10", userName := "x", isInaccessible? := .some false, type? := .some { pp? := .some "Prop" }}],
+    vars := #[{ name := "_uniq.10", userName := "x", type? := .some { pp? := .some "Prop" }}],
   }
   let goal2: Protocol.Goal := {
     name := "_uniq.17",
     target := { pp? := .some "x ∨ y → y ∨ x" },
     vars := #[
-      { name := "_uniq.10", userName := "x", isInaccessible? := .some false, type? := .some { pp? := .some "Prop" }},
-      { name := "_uniq.16", userName := "y", isInaccessible? := .some false, type? := .some { pp? := .some "Prop" }}
+      { name := "_uniq.10", userName := "x", type? := .some { pp? := .some "Prop" }},
+      { name := "_uniq.16", userName := "y", type? := .some { pp? := .some "Prop" }}
     ],
   }
   subroutine_runner [

Test/Main.lean

@@ -52,6 +52,7 @@ def main (args: List String) := do
     ("Tactic/Congruence", Tactic.Congruence.suite env_default),
     ("Tactic/Motivated Apply", Tactic.MotivatedApply.suite env_default),
     ("Tactic/No Confuse", Tactic.NoConfuse.suite env_default),
+    ("Tactic/Prograde", Tactic.Prograde.suite env_default),
   ]
   let tests: List (String × IO LSpec.TestSeq) := suites.foldl (λ acc (name, suite) => acc ++ (addPrefix name suite)) []
   LSpec.lspecIO (← runTestGroup name_filter tests)

Test/Metavar.lean

@@ -60,7 +60,6 @@ def buildGoal (nameType: List (String × String)) (target: String) (userName?: O
     vars := (nameType.map fun x => ({
       userName := x.fst,
       type? := .some { pp? := .some x.snd },
-      isInaccessible? := .some false
     })).toArray
   }
 def proofRunner (env: Lean.Environment) (tests: TestM Unit): IO LSpec.TestSeq := do
@@ -198,15 +197,16 @@ def test_proposition_generation: TestM Unit := do
       addTest $ assertUnreachable $ other.toString
       return ()
   addTest $ LSpec.check ":= λ (x: Nat), _" ((← state2.serializeGoals (options := ← read)).map (·.target.pp?) =
-    #[.some "∀ (x : Nat), ?m.29 x"])
+    #[.some "?m.29 x"])
   addTest $ LSpec.test "(2 root)" state2.rootExpr?.isNone
 
-  let state3 ← match ← state2.tryAssign (goalId := 0) (expr := "fun x => Eq.refl x") with
+  let assign := "Eq.refl x"
+  let state3 ← match ← state2.tryAssign (goalId := 0) (expr := assign) with
     | .success state => pure state
     | other => do
       addTest $ assertUnreachable $ other.toString
       return ()
-  addTest $ LSpec.check ":= Eq.refl" ((← state3.serializeGoals (options := ← read)).map (·.target.pp?) =
+  addTest $ LSpec.check s!":= {assign}" ((← state3.serializeGoals (options := ← read)).map (·.target.pp?) =
     #[])
 
   addTest $ LSpec.test "(3 root)" state3.rootExpr?.isSome

Test/Proofs.lean

@@ -58,7 +58,6 @@ def buildNamedGoal (name: String) (nameType: List (String × String)) (target: S
     vars := (nameType.map fun x => ({
       userName := x.fst,
       type? := .some { pp? := .some x.snd },
-      isInaccessible? := .some false
     })).toArray
   }
 def buildGoal (nameType: List (String × String)) (target: String) (userName?: Option String := .none):
@@ -69,7 +68,6 @@ def buildGoal (nameType: List (String × String)) (target: String) (userName?: O
     vars := (nameType.map fun x => ({
       userName := x.fst,
       type? := .some { pp? := .some x.snd },
-      isInaccessible? := .some false
     })).toArray
   }
 def proofRunner (env: Lean.Environment) (tests: TestM Unit): IO LSpec.TestSeq := do
@@ -175,7 +173,6 @@ def test_delta_variable: TestM Unit := do
       vars := (nameType.map fun x => ({
         userName := x.fst,
         type? := x.snd.map (λ type => { pp? := type }),
-        isInaccessible? := x.snd.map (λ _ => false)
       })).toArray
     }
 
@@ -256,9 +253,9 @@ def test_or_comm: TestM Unit := do
       name := state1g0,
       target := { pp? := .some "q ∨ p" },
       vars := #[
-        { name := fvP, userName := "p", type? := .some { pp? := .some "Prop" }, isInaccessible? := .some false },
-        { name := fvQ, userName := "q", type? := .some { pp? := .some "Prop" }, isInaccessible? := .some false },
-        { name := fvH, userName := "h", type? := .some { pp? := .some "p ∨ q" }, isInaccessible? := .some false }
+        { name := fvP, userName := "p", type? := .some { pp? := .some "Prop" } },
+        { name := fvQ, userName := "q", type? := .some { pp? := .some "Prop" } },
+        { name := fvH, userName := "h", type? := .some { pp? := .some "p ∨ q" } }
       ]
     }])
   addTest $ LSpec.check "(1 parent)" state1.parentExpr?.isSome
@@ -351,75 +348,12 @@ def test_or_comm: TestM Unit := do
       userName? := .some caseName,
       target := { pp? := .some "q ∨ p" },
       vars := #[
-        { userName := "p", type? := .some typeProp, isInaccessible? := .some false },
-        { userName := "q", type? := .some typeProp, isInaccessible? := .some false },
-        { userName := "h✝", type? := .some { pp? := .some varName }, isInaccessible? := .some true }
+        { userName := "p", type? := .some typeProp },
+        { userName := "q", type? := .some typeProp },
+        { userName := "h✝", type? := .some { pp? := .some varName }, isInaccessible := true }
       ]
     }
 
-def test_have: TestM Unit := do
-  let state? ← startProof (.expr "∀ (p q: Prop), p → ((p ∨ q) ∨ (p ∨ q))")
-  let state0 ← match state? with
-    | .some state => pure state
-    | .none => do
-      addTest $ assertUnreachable "Goal could not parse"
-      return ()
-  let tactic := "intro p q h"
-  let state1 ← match ← state0.tryTactic (goalId := 0) (tactic := tactic) with
-    | .success state => pure state
-    | other => do
-      addTest $ assertUnreachable $ other.toString
-      return ()
-  addTest $ LSpec.check tactic ((← state1.serializeGoals (options := ← read)).map (·.devolatilize) =
-    #[buildGoal [("p", "Prop"), ("q", "Prop"), ("h", "p")] "(p ∨ q) ∨ p ∨ q"])
-
-  let expr := "Or.inl (Or.inl h)"
-  let state2 ← match ← state1.tryAssign (goalId := 0) (expr := expr) with
-    | .success state => pure state
-    | other => do
-      addTest $ assertUnreachable $ other.toString
-      return ()
-  addTest $ LSpec.check s!":= {expr}" ((← state2.serializeGoals (options := ← read)).map (·.devolatilize) =
-    #[])
-
-  let haveBind := "y"
-  let haveType := "p ∨ q"
-  let state2 ← match ← state1.tryHave (goalId := 0) (binderName := haveBind) (type := haveType) with
-    | .success state => pure state
-    | other => do
-      addTest $ assertUnreachable $ other.toString
-      return ()
-  addTest $ LSpec.check s!"have {haveBind}: {haveType}" ((← state2.serializeGoals (options := ← read)).map (·.devolatilize) =
-    #[
-      buildGoal [("p", "Prop"), ("q", "Prop"), ("h", "p")] "p ∨ q",
-      buildGoal [("p", "Prop"), ("q", "Prop"), ("h", "p"), ("y", "p ∨ q")] "(p ∨ q) ∨ p ∨ q"
-    ])
-
-  let expr := "Or.inl h"
-  let state3 ← match ← state2.tryAssign (goalId := 0) (expr := expr) with
-    | .success state => pure state
-    | other => do
-      addTest $ assertUnreachable $ other.toString
-      return ()
-  addTest $ LSpec.check s!":= {expr}" ((← state3.serializeGoals (options := ← read)).map (·.devolatilize) =
-    #[])
-
-  let state2b ← match state3.continue state2 with
-    | .ok state => pure state
-    | .error e => do
-      addTest $ assertUnreachable e
-      return ()
-  let expr := "Or.inl y"
-  let state4 ← match ← state2b.tryAssign (goalId := 0) (expr := expr) with
-    | .success state => pure state
-    | other => do
-      addTest $ assertUnreachable $ other.toString
-      return ()
-  addTest $ LSpec.check s!":= {expr}" ((← state4.serializeGoals (options := ← read)).map (·.devolatilize) =
-    #[])
-
-  addTest $ LSpec.check "(4 root)" state4.rootExpr?.isSome
-
 example : ∀ (a b c1 c2: Nat), (b + a) + c1 = (b + a) + c2 → (a + b) + c1 = (b + a) + c2 := by
   intro a b c1 c2 h
   conv =>
@@ -607,83 +541,6 @@ def test_calc: TestM Unit := do
         ("h1", "a + b = b + c"), ("h2", "b + c = c + d")] ++ free
       buildGoal free target userName?
 
-def test_let (specialized: Bool): TestM Unit := do
-  let state? ← startProof (.expr "∀ (a: Nat) (p: Prop), p → p ∨ ¬p")
-  let state0 ← match state? with
-    | .some state => pure state
-    | .none => do
-      addTest $ assertUnreachable "Goal could not parse"
-      return ()
-  let tactic := "intro a p h"
-  let state1 ← match ← state0.tryTactic (goalId := 0) (tactic := tactic) with
-    | .success state => pure state
-    | other => do
-      addTest $ assertUnreachable $ other.toString
-      return ()
-  addTest $ LSpec.check tactic ((← state1.serializeGoals (options := ← read)).map (·.devolatilize) =
-    #[interiorGoal [] "p ∨ ¬p"])
-
-
-  let letType := "Nat"
-  let expr := s!"let b: {letType} := _; _"
-  let result2 ← match specialized with
-    | true => state1.tryLet (goalId := 0) (binderName := "b") (type := letType)
-    | false => state1.tryAssign (goalId := 0) (expr := expr)
-  let state2 ← match result2 with
-    | .success state => pure state
-    | other => do
-      addTest $ assertUnreachable $ other.toString
-      return ()
-  let serializedState2 ← state2.serializeGoals (options := ← read)
-  addTest $ LSpec.check expr (serializedState2.map (·.devolatilize) =
-    #[
-      interiorGoal [] letType,
-      interiorGoal [] "let b := ?m.20;\np ∨ ¬p"
-    ])
-  -- Check that the goal mvar ids match up
-  addTest $ LSpec.check "(mvarId)" ((serializedState2.map (·.name) |>.get! 0) = "_uniq.20")
-
-  let tactic := "exact a"
-  let state3 ← match ← state2.tryTactic (goalId := 0) (tactic := tactic) with
-    | .success state => pure state
-    | other => do
-      addTest $ assertUnreachable $ other.toString
-      return ()
-  addTest $ LSpec.check tactic ((← state3.serializeGoals (options := ← read)).map (·.devolatilize) = #[])
-
-  let state3r ← match state3.continue state2 with
-    | .error msg => do
-      addTest $ assertUnreachable $ msg
-      return ()
-    | .ok state => pure state
-  addTest $ LSpec.check "(continue)" ((← state3r.serializeGoals (options := ← read)).map (·.devolatilize) =
-    #[interiorGoal [] "let b := a;\np ∨ ¬p"])
-
-  let tactic := "exact h"
-  match ← state3r.tryTactic (goalId := 0) (tactic := tactic) with
-  | .failure #[message] =>
-    addTest $ LSpec.check tactic  (message = "type mismatch\n  h\nhas type\n  p : Prop\nbut is expected to have type\n  let b := a;\n  p ∨ ¬p : Prop")
-  | other => do
-    addTest $ assertUnreachable $ other.toString
-
-  let tactic := "intro b"
-  let state4 ← match ← state3r.tryTactic (goalId := 0) (tactic := tactic) with
-    | .success state => pure state
-    | other => do
-      addTest $ assertUnreachable $ other.toString
-      return ()
-  let tactic := "exact Or.inl h"
-  let state5 ← match ← state4.tryTactic (goalId := 0) (tactic := tactic) with
-    | .success state => pure state
-    | other => do
-      addTest $ assertUnreachable $ other.toString
-      return ()
-  addTest $ LSpec.test "(5 root)" state5.rootExpr?.isSome
-  where
-    interiorGoal (free: List (String × String)) (target: String) (userName?: Option String := .none) :=
-      let free := [("a", "Nat"), ("p", "Prop"), ("h", "p")] ++ free
-      buildGoal free target userName?
-
 def test_nat_zero_add: TestM Unit := do
   let state? ← startProof (.expr "∀ (n: Nat), n + 0 = n")
   let state0 ← match state? with
@@ -843,7 +700,6 @@ def test_nat_zero_add_alt: TestM Unit := do
           name := fvN,
           userName := "n",
           type? := .some { pp? := .some "Nat", sexp? := .some "(:c Nat)" },
-          isInaccessible? := .some false
         }],
       }
     ])
@@ -856,11 +712,8 @@ def suite (env: Environment): List (String × IO LSpec.TestSeq) :=
     ("Nat.add_comm delta", test_delta_variable),
     ("arithmetic", test_arith),
     ("Or.comm", test_or_comm),
-    ("have", test_have),
     ("conv", test_conv),
     ("calc", test_calc),
-    ("let via assign", test_let false),
-    ("let via tryLet", test_let true),
     ("Nat.zero_add", test_nat_zero_add),
     ("Nat.zero_add alt", test_nat_zero_add_alt),
   ]

Test/Tactic.lean

@@ -1,3 +1,4 @@
 import Test.Tactic.Congruence
 import Test.Tactic.MotivatedApply
 import Test.Tactic.NoConfuse
+import Test.Tactic.Prograde

Test/Tactic/Congruence.lean

@@ -7,16 +7,13 @@ open Pantograph
 
 namespace Pantograph.Test.Tactic.Congruence
 
-def test_congr_arg_list (env: Environment): IO LSpec.TestSeq :=
+def test_congr_arg_list : TestT Elab.TermElabM Unit := do
   let expr := "λ {α} (l1 l2 : List α) (h: l1 = l2) => l1.reverse = l2.reverse"
-  runMetaMSeq env do
   let expr ← parseSentence expr
   Meta.lambdaTelescope expr $ λ _ body => do
-      let mut tests := LSpec.TestSeq.done
     let target ← Meta.mkFreshExprSyntheticOpaqueMVar body
-      let (newGoals, test) ← runTermElabMInMeta do
-        let newGoals ← runTacticOnMVar Tactic.congruenceArg target.mvarId!
-        let test := LSpec.check "goals" ((← newGoals.mapM (λ x => mvarUserNameAndType x)) =
+    let newGoals ← runTacticOnMVar Tactic.evalCongruenceArg target.mvarId!
+    addTest $ LSpec.check "goals" ((← newGoals.mapM (λ x => mvarUserNameAndType x)) =
       [
         (`α, "Sort ?u.30"),
         (`a₁, "?α"),
@@ -25,26 +22,20 @@ def test_congr_arg_list (env: Environment): IO LSpec.TestSeq :=
         (`h, "?a₁ = ?a₂"),
         (`conduit, "(?f ?a₁ = ?f ?a₂) = (l1.reverse = l2.reverse)"),
       ])
-        return (newGoals, test)
-      tests := tests ++ test
     let f := newGoals.get! 3
     let h := newGoals.get! 4
     let c := newGoals.get! 5
     let results ← f.apply (← parseSentence "List.reverse")
-      tests := tests ++ (LSpec.check "apply" (results.length = 0))
-      tests := tests ++ (LSpec.check "h" ((← exprToStr $ ← h.getType) = "?a₁ = ?a₂"))
-      tests := tests ++ (LSpec.check "conduit" ((← exprToStr $ ← c.getType) = "(?a₁.reverse = ?a₂.reverse) = (l1.reverse = l2.reverse)"))
-      return tests
-def test_congr_arg (env: Environment): IO LSpec.TestSeq :=
+    addTest $ LSpec.check "apply" (results.length = 0)
+    addTest $ LSpec.check "h" ((← exprToStr $ ← h.getType) = "?a₁ = ?a₂")
+    addTest $ LSpec.check "conduit" ((← exprToStr $ ← c.getType) = "(?a₁.reverse = ?a₂.reverse) = (l1.reverse = l2.reverse)")
+def test_congr_arg : TestT Elab.TermElabM Unit := do
   let expr := "λ (n m: Nat) (h: n = m) => n * n = m * m"
-  runMetaMSeq env do
   let expr ← parseSentence expr
   Meta.lambdaTelescope expr $ λ _ body => do
-      let mut tests := LSpec.TestSeq.done
     let target ← Meta.mkFreshExprSyntheticOpaqueMVar body
-      let test ← runTermElabMInMeta do
-        let newGoals ← runTacticOnMVar Tactic.congruenceArg target.mvarId!
-        pure $ LSpec.check "goals" ((← newGoals.mapM (λ x => mvarUserNameAndType x)) =
+    let newGoals ← runTacticOnMVar Tactic.evalCongruenceArg target.mvarId!
+    addTest $  LSpec.check "goals" ((← newGoals.mapM (λ x => mvarUserNameAndType x)) =
       [
         (`α, "Sort ?u.70"),
         (`a₁, "?α"),
@@ -53,18 +44,13 @@ def test_congr_arg (env: Environment): IO LSpec.TestSeq :=
         (`h, "?a₁ = ?a₂"),
         (`conduit, "(?f ?a₁ = ?f ?a₂) = (n * n = m * m)"),
       ])
-      tests := tests ++ test
-      return tests
-def test_congr_fun (env: Environment): IO LSpec.TestSeq :=
+def test_congr_fun : TestT Elab.TermElabM Unit := do
   let expr := "λ (n m: Nat) => (n + m) + (n + m) = (n + m) * 2"
-  runMetaMSeq env do
   let expr ← parseSentence expr
   Meta.lambdaTelescope expr $ λ _ body => do
-      let mut tests := LSpec.TestSeq.done
     let target ← Meta.mkFreshExprSyntheticOpaqueMVar body
-      let test ← runTermElabMInMeta do
-        let newGoals ← runTacticOnMVar Tactic.congruenceFun target.mvarId!
-        pure $ LSpec.check "goals" ((← newGoals.mapM (λ x => mvarUserNameAndType x)) =
+    let newGoals ← runTacticOnMVar Tactic.evalCongruenceFun target.mvarId!
+    addTest $ LSpec.check "goals" ((← newGoals.mapM (λ x => mvarUserNameAndType x)) =
       [
         (`α, "Sort ?u.159"),
         (`f₁, "?α → Nat"),
@@ -73,18 +59,13 @@ def test_congr_fun (env: Environment): IO LSpec.TestSeq :=
         (`a, "?α"),
         (`conduit, "(?f₁ ?a = ?f₂ ?a) = (n + m + (n + m) = (n + m) * 2)"),
       ])
-      tests := tests ++ test
-      return tests
-def test_congr (env: Environment): IO LSpec.TestSeq :=
+def test_congr : TestT Elab.TermElabM Unit := do
   let expr := "λ (a b: Nat) => a = b"
-  runMetaMSeq env do
   let expr ← parseSentence expr
   Meta.lambdaTelescope expr $ λ _ body => do
-      let mut tests := LSpec.TestSeq.done
     let target ← Meta.mkFreshExprSyntheticOpaqueMVar body
-      let test ← runTermElabMInMeta do
-        let newGoals ← runTacticOnMVar Tactic.congruence target.mvarId!
-        pure $ LSpec.check "goals" ((← newGoals.mapM (λ x => mvarUserNameAndType x)) =
+    let newGoals ← runTacticOnMVar Tactic.evalCongruence target.mvarId!
+    addTest $  LSpec.check "goals" ((← newGoals.mapM (λ x => mvarUserNameAndType x)) =
       [
         (`α, "Sort ?u.10"),
         (`f₁, "?α → Nat"),
@@ -95,15 +76,13 @@ def test_congr (env: Environment): IO LSpec.TestSeq :=
         (`h₂, "?a₁ = ?a₂"),
         (`conduit, "(?f₁ ?a₁ = ?f₂ ?a₂) = (a = b)"),
       ])
-      tests := tests ++ test
-      return tests
 
 def suite (env: Environment): List (String × IO LSpec.TestSeq) :=
   [
-    ("congrArg List.reverse", test_congr_arg_list env),
-    ("congrArg", test_congr_arg env),
-    ("congrFun", test_congr_fun env),
-    ("congr", test_congr env),
-  ]
+    ("congrArg List.reverse", test_congr_arg_list),
+    ("congrArg", test_congr_arg),
+    ("congrFun", test_congr_fun),
+    ("congr", test_congr),
+  ] |>.map (λ (name, t) => (name, runTestTermElabM env t))
 
 end Pantograph.Test.Tactic.Congruence

Test/Tactic/MotivatedApply.lean

@@ -7,25 +7,21 @@ open Pantograph
 
 namespace Pantograph.Test.Tactic.MotivatedApply
 
-def test_type_extract (env: Environment): IO LSpec.TestSeq :=
-  runMetaMSeq env do
-    let mut tests := LSpec.TestSeq.done
+def test_type_extract : TestT Elab.TermElabM Unit := do
   let recursor ← parseSentence "@Nat.brecOn"
   let recursorType ← Meta.inferType recursor
-    tests := tests ++ LSpec.check "recursorType" ("{motive : Nat → Sort ?u.1} → (t : Nat) → ((t : Nat) → Nat.below t → motive t) → motive t" =
+  addTest $ LSpec.check "recursorType" ("{motive : Nat → Sort ?u.1} → (t : Nat) → ((t : Nat) → Nat.below t → motive t) → motive t" =
     (← exprToStr recursorType))
   let info ← match Tactic.getRecursorInformation recursorType with
     | .some info => pure info
     | .none => throwError "Failed to extract recursor info"
-    tests := tests ++ LSpec.check "iMotive" (info.iMotive = 2)
+  addTest $ LSpec.check "iMotive" (info.iMotive = 2)
   let motiveType := info.getMotiveType
-    tests := tests ++ LSpec.check "motiveType" ("Nat → Sort ?u.1" =
+  addTest $ LSpec.check "motiveType" ("Nat → Sort ?u.1" =
     (← exprToStr motiveType))
-    return tests
 
-def test_nat_brec_on (env: Environment): IO LSpec.TestSeq :=
+def test_nat_brec_on : TestT Elab.TermElabM Unit := do
   let expr := "λ (n t: Nat) => n + 0 = n"
-  runMetaMSeq env do
   let expr ← parseSentence expr
   Meta.lambdaTelescope expr $ λ _ body => do
     let recursor ← match Parser.runParserCategory
@@ -35,25 +31,21 @@ def test_nat_brec_on (env: Environment): IO LSpec.TestSeq :=
       (fileName := filename) with
       | .ok syn => pure syn
       | .error error => throwError "Failed to parse: {error}"
-      let mut tests := LSpec.TestSeq.done
     -- Apply the tactic
     let target ← Meta.mkFreshExprSyntheticOpaqueMVar body
-      let tactic := Tactic.motivatedApply recursor
-      let test ← runTermElabMInMeta do
+    let tactic := Tactic.evalMotivatedApply recursor
     let newGoals ← runTacticOnMVar tactic target.mvarId!
-        pure $ LSpec.check "goals" ((← newGoals.mapM (λ g => do exprToStr (← g.getType))) =
+    let test :=  LSpec.check "goals" ((← newGoals.mapM (λ g => do exprToStr (← g.getType))) =
       [
         "Nat → Prop",
         "Nat",
         "∀ (t : Nat), Nat.below t → ?motive t",
         "?motive ?m.67 = (n + 0 = n)",
       ])
-      tests := tests ++ test
-      return tests
+    addTest test
 
-def test_list_brec_on (env: Environment): IO LSpec.TestSeq :=
+def test_list_brec_on : TestT Elab.TermElabM Unit := do
   let expr := "λ {α : Type} (l: List α) => l ++ [] = [] ++ l"
-  runMetaMSeq env do
   let expr ← parseSentence expr
   Meta.lambdaTelescope expr $ λ _ body => do
     let recursor ← match Parser.runParserCategory
@@ -63,13 +55,11 @@ def test_list_brec_on (env: Environment): IO LSpec.TestSeq :=
       (fileName := filename) with
       | .ok syn => pure syn
       | .error error => throwError "Failed to parse: {error}"
-      let mut tests := LSpec.TestSeq.done
     -- Apply the tactic
     let target ← Meta.mkFreshExprSyntheticOpaqueMVar body
-      let tactic := Tactic.motivatedApply recursor
-      let test ← runTermElabMInMeta do
+    let tactic := Tactic.evalMotivatedApply recursor
     let newGoals ← runTacticOnMVar tactic target.mvarId!
-        pure $ LSpec.check "goals" ((← newGoals.mapM (λ g => do exprToStr (← g.getType))) =
+    addTest $ LSpec.check "goals" ((← newGoals.mapM (λ g => do exprToStr (← g.getType))) =
       [
         "Type ?u.90",
         "List ?m.92 → Prop",
@@ -77,12 +67,9 @@ def test_list_brec_on (env: Environment): IO LSpec.TestSeq :=
         "∀ (t : List ?m.92), List.below t → ?motive t",
         "?motive ?m.94 = (l ++ [] = [] ++ l)",
       ])
-      tests := tests ++ test
-      return tests
 
-def test_partial_motive_instantiation (env: Environment): IO LSpec.TestSeq := do
+def test_partial_motive_instantiation : TestT Elab.TermElabM Unit := do
   let expr := "λ (n t: Nat) => n + 0 = n"
-  runMetaMSeq env $ runTermElabMInMeta do
   let recursor ← match Parser.runParserCategory
     (env := ← MonadEnv.getEnv)
     (catName := `term)
@@ -92,13 +79,12 @@ def test_partial_motive_instantiation (env: Environment): IO LSpec.TestSeq := do
     | .error error => throwError "Failed to parse: {error}"
   let expr ← parseSentence expr
   Meta.lambdaTelescope expr $ λ _ body => do
-      let mut tests := LSpec.TestSeq.done
     -- Apply the tactic
     let target ← Meta.mkFreshExprSyntheticOpaqueMVar body
-      let tactic := Tactic.motivatedApply recursor
+    let tactic := Tactic.evalMotivatedApply recursor
     let newGoals ← runTacticOnMVar tactic target.mvarId!
     let majorId := 67
-      tests := tests ++ (LSpec.check "goals" ((← newGoals.mapM (λ g => do exprToStr (← g.getType))) =
+    addTest $ (LSpec.check "goals" ((← newGoals.mapM (λ g => do exprToStr (← g.getType))) =
       [
         "Nat → Prop",
         "Nat",
@@ -106,25 +92,22 @@ def test_partial_motive_instantiation (env: Environment): IO LSpec.TestSeq := do
         s!"?motive ?m.{majorId} = (n + 0 = n)",
       ]))
     let [motive, major, step, conduit] := newGoals | panic! "Incorrect goal number"
-      tests := tests ++ (LSpec.check "goal name" (major.name.toString = s!"_uniq.{majorId}"))
+    addTest $ (LSpec.check "goal name" (major.name.toString = s!"_uniq.{majorId}"))
 
     -- Assign motive to `λ x => x + _`
     let motive_assign ← parseSentence "λ (x: Nat) => @Nat.add x + 0 = _"
     motive.assign motive_assign
 
-      let test ← conduit.withContext do
+    addTest $ ← conduit.withContext do
       let t := toString (← Meta.ppExpr $ ← conduit.getType)
       return LSpec.check "conduit" (t = s!"(?m.{majorId}.add + 0 = ?m.138 ?m.{majorId}) = (n + 0 = n)")
-      tests := tests ++ test
-
-      return tests
 
 def suite (env: Environment): List (String × IO LSpec.TestSeq) :=
   [
-    ("type_extract", test_type_extract env),
-    ("Nat.brecOn", test_nat_brec_on env),
-    ("List.brecOn", test_list_brec_on env),
-    ("Nat.brecOn partial motive instantiation", test_partial_motive_instantiation env),
-  ]
+    ("type_extract", test_type_extract),
+    ("Nat.brecOn", test_nat_brec_on),
+    ("List.brecOn", test_list_brec_on),
+    ("Nat.brecOn partial motive instantiation", test_partial_motive_instantiation),
+  ] |>.map (λ (name, t) => (name, runTestTermElabM env t))
 
 end Pantograph.Test.Tactic.MotivatedApply

Test/Tactic/NoConfuse.lean

@@ -7,9 +7,8 @@ open Pantograph
 
 namespace Pantograph.Test.Tactic.NoConfuse
 
-def test_nat (env: Environment): IO LSpec.TestSeq :=
+def test_nat : TestT Elab.TermElabM Unit := do
   let expr := "λ (n: Nat) (h: 0 = n + 1) => False"
-  runMetaMSeq env do
   let expr ← parseSentence expr
   Meta.lambdaTelescope expr $ λ _ body => do
     let recursor ← match Parser.runParserCategory
@@ -19,20 +18,14 @@ def test_nat (env: Environment): IO LSpec.TestSeq :=
       (fileName := filename) with
       | .ok syn => pure syn
       | .error error => throwError "Failed to parse: {error}"
-      let mut tests := LSpec.TestSeq.done
     -- Apply the tactic
     let target ← Meta.mkFreshExprSyntheticOpaqueMVar body
-      let tactic := Tactic.noConfuse recursor
-      let test ← runTermElabMInMeta do
+    let tactic := Tactic.evalNoConfuse recursor
     let newGoals ← runTacticOnMVar tactic target.mvarId!
-        pure $ LSpec.check "goals" ((← newGoals.mapM (λ g => do exprToStr (← g.getType))) =
-          [])
-      tests := tests ++ test
-      return tests
+    addTest $ LSpec.check "goals" ((← newGoals.mapM (λ g => do exprToStr (← g.getType))) = [])
 
-def test_nat_fail (env: Environment): IO LSpec.TestSeq :=
+def test_nat_fail : TestT Elab.TermElabM Unit := do
   let expr := "λ (n: Nat) (h: n = n) => False"
-  runMetaMSeq env do
   let expr ← parseSentence expr
   Meta.lambdaTelescope expr $ λ _ body => do
     let recursor ← match Parser.runParserCategory
@@ -42,21 +35,17 @@ def test_nat_fail (env: Environment): IO LSpec.TestSeq :=
       (fileName := filename) with
       | .ok syn => pure syn
       | .error error => throwError "Failed to parse: {error}"
-      let mut tests := LSpec.TestSeq.done
     -- Apply the tactic
     let target ← Meta.mkFreshExprSyntheticOpaqueMVar body
     try
-        let tactic := Tactic.noConfuse recursor
-        let _ ← runTermElabMInMeta $ runTacticOnMVar tactic target.mvarId!
-        tests := tests ++ assertUnreachable "Tactic should fail"
+      let tactic := Tactic.evalNoConfuse recursor
+      let _ ← runTacticOnMVar tactic target.mvarId!
+      addTest $ assertUnreachable "Tactic should fail"
     catch _ =>
-        tests := tests ++ LSpec.check "Tactic should fail" true
-        return tests
-      return tests
+      addTest $ LSpec.check "Tactic should fail" true
 
-def test_list (env: Environment): IO LSpec.TestSeq :=
+def test_list : TestT Elab.TermElabM Unit := do
   let expr := "λ (l: List Nat) (h: [] = 1 :: l) => False"
-  runMetaMSeq env do
   let expr ← parseSentence expr
   Meta.lambdaTelescope expr $ λ _ body => do
     let recursor ← match Parser.runParserCategory
@@ -66,22 +55,18 @@ def test_list (env: Environment): IO LSpec.TestSeq :=
       (fileName := filename) with
       | .ok syn => pure syn
       | .error error => throwError "Failed to parse: {error}"
-      let mut tests := LSpec.TestSeq.done
     -- Apply the tactic
     let target ← Meta.mkFreshExprSyntheticOpaqueMVar body
-      let tactic := Tactic.noConfuse recursor
-      let test ← runTermElabMInMeta do
+    let tactic := Tactic.evalNoConfuse recursor
     let newGoals ← runTacticOnMVar tactic target.mvarId!
-        pure $ LSpec.check "goals" ((← newGoals.mapM (λ g => do exprToStr (← g.getType))) =
-          [])
-      tests := tests ++ test
-      return tests
+    addTest $ LSpec.check "goals"
+      ((← newGoals.mapM (λ g => do exprToStr (← g.getType))) = [])
 
 def suite (env: Environment): List (String × IO LSpec.TestSeq) :=
   [
-    ("Nat", test_nat env),
-    ("Nat fail", test_nat_fail env),
-    ("List", test_list env),
-  ]
+    ("Nat", test_nat),
+    ("Nat fail", test_nat_fail),
+    ("List", test_list),
+  ] |>.map (λ (name, t) => (name, runTestTermElabM env t))
 
 end Pantograph.Test.Tactic.NoConfuse

Test/Tactic/Prograde.lean

@@ -0,0 +1,266 @@
+import LSpec
+import Lean
+import Test.Common
+
+open Lean
+open Pantograph
+
+namespace Pantograph.Test.Tactic.Prograde
+
+def test_eval : TestT Elab.TermElabM Unit := do
+  let expr := "forall (p q : Prop) (h: p), And (Or p q) (Or p q)"
+  let expr ← parseSentence expr
+  Meta.forallTelescope expr $ λ _ body => do
+    let e ← match Parser.runParserCategory
+      (env := ← MonadEnv.getEnv)
+      (catName := `term)
+      (input := "Or.inl h")
+      (fileName := filename) with
+      | .ok syn => pure syn
+      | .error error => throwError "Failed to parse: {error}"
+    -- Apply the tactic
+    let goal ← Meta.mkFreshExprSyntheticOpaqueMVar body
+    let target: Expr := mkAnd
+      (mkOr (.fvar ⟨uniq 8⟩) (.fvar ⟨uniq 9⟩))
+      (mkOr (.fvar ⟨uniq 8⟩) (.fvar ⟨uniq 9⟩))
+    let h := .fvar ⟨uniq 8⟩
+    addTest $ LSpec.test "goals before" ((← toCondensedGoal goal.mvarId!).devolatilize == {
+      context := #[
+        cdeclOf `p (.sort 0),
+        cdeclOf `q (.sort 0),
+        cdeclOf `h h
+      ],
+      target,
+    })
+    let tactic := Tactic.evalDefine `h2 e
+    let m := .mvar ⟨uniq 13⟩
+    let [newGoal] ← runTacticOnMVar tactic goal.mvarId! | panic! "Incorrect goal number"
+    addTest $ LSpec.test "goals after" ((← toCondensedGoal newGoal).devolatilize == {
+      context := #[
+        cdeclOf `p (.sort 0),
+        cdeclOf `q (.sort 0),
+        cdeclOf `h h,
+        {
+          userName := `h2,
+          type := mkOr h m,
+          value? := .some $ mkApp3 (mkConst `Or.inl) h m (.fvar ⟨uniq 10⟩)
+        }
+      ],
+      target,
+    })
+    addTest $ LSpec.test "assign" ((← getExprMVarAssignment? goal.mvarId!) == .some (.mvar newGoal))
+
+def test_proof_eval : TestT Elab.TermElabM Unit := do
+  let rootExpr ← parseSentence "∀ (p q: Prop), p → ((p ∨ q) ∨ (p ∨ q))"
+  let state0 ← GoalState.create rootExpr
+  let tactic := "intro p q h"
+  let state1 ← match ← state0.tryTactic (goalId := 0) (tactic := tactic) with
+    | .success state => pure state
+    | other => do
+      addTest $ assertUnreachable $ other.toString
+      return ()
+  addTest $ LSpec.check tactic ((← state1.serializeGoals).map (·.devolatilize) =
+    #[buildGoal [("p", "Prop"), ("q", "Prop"), ("h", "p")] "(p ∨ q) ∨ p ∨ q"])
+
+  let expr := "Or.inl (Or.inl h)"
+  let state2 ← match ← state1.tryAssign (goalId := 0) (expr := expr) with
+    | .success state => pure state
+    | other => do
+      addTest $ assertUnreachable $ other.toString
+      return ()
+  addTest $ LSpec.check s!":= {expr}" ((← state2.serializeGoals).map (·.devolatilize) =
+    #[])
+
+  let evalBind := "y"
+  let evalExpr := "Or.inl h"
+  let state2 ← match ← state1.tryDefine (goalId := 0) (binderName := evalBind) (expr := evalExpr) with
+    | .success state => pure state
+    | other => do
+      addTest $ assertUnreachable $ other.toString
+      return ()
+  addTest $ LSpec.check s!"eval {evalBind} := {evalExpr}" ((← state2.serializeGoals).map (·.devolatilize) =
+    #[{
+      target := { pp? := .some  "(p ∨ q) ∨ p ∨ q"},
+      vars := #[
+        { userName := "p", type? := .some { pp? := .some "Prop" } },
+        { userName := "q", type? := .some { pp? := .some "Prop" } },
+        { userName := "h", type? := .some { pp? := .some "p" } },
+        { userName := "y",
+          type? := .some { pp? := .some "p ∨ ?m.25" },
+          value? := .some { pp? := .some "Or.inl h" },
+        }
+      ]
+  }])
+
+  let expr := "Or.inl y"
+  let state3 ← match ← state2.tryAssign (goalId := 0) (expr := expr) with
+    | .success state => pure state
+    | other => do
+      addTest $ assertUnreachable $ other.toString
+      return ()
+  addTest $ LSpec.check s!":= {expr}" ((← state3.serializeGoals).map (·.devolatilize) =
+    #[])
+
+  addTest $ LSpec.check "(3 root)" state3.rootExpr?.isSome
+
+def test_proof_have : TestT Elab.TermElabM Unit := do
+  let rootExpr ← parseSentence "∀ (p q: Prop), p → ((p ∨ q) ∨ (p ∨ q))"
+  let state0 ← GoalState.create rootExpr
+  let tactic := "intro p q h"
+  let state1 ← match ← state0.tryTactic (goalId := 0) (tactic := tactic) with
+    | .success state => pure state
+    | other => do
+      addTest $ assertUnreachable $ other.toString
+      return ()
+  addTest $ LSpec.check tactic ((← state1.serializeGoals).map (·.devolatilize) =
+    #[buildGoal [("p", "Prop"), ("q", "Prop"), ("h", "p")] "(p ∨ q) ∨ p ∨ q"])
+
+  let expr := "Or.inl (Or.inl h)"
+  let state2 ← match ← state1.tryAssign (goalId := 0) (expr := expr) with
+    | .success state => pure state
+    | other => do
+      addTest $ assertUnreachable $ other.toString
+      return ()
+  addTest $ LSpec.check s!":= {expr}" ((← state2.serializeGoals).map (·.devolatilize) =
+    #[])
+
+  let haveBind := "y"
+  let haveType := "p ∨ q"
+  let state2 ← match ← state1.tryHave (goalId := 0) (binderName := haveBind) (type := haveType) with
+    | .success state => pure state
+    | other => do
+      addTest $ assertUnreachable $ other.toString
+      return ()
+  addTest $ LSpec.check s!"have {haveBind}: {haveType}" ((← state2.serializeGoals).map (·.devolatilize) =
+    #[
+      buildGoal [("p", "Prop"), ("q", "Prop"), ("h", "p")] "p ∨ q",
+      buildGoal [("p", "Prop"), ("q", "Prop"), ("h", "p"), ("y", "p ∨ q")] "(p ∨ q) ∨ p ∨ q"
+    ])
+
+  let expr := "Or.inl h"
+  let state3 ← match ← state2.tryAssign (goalId := 0) (expr := expr) with
+    | .success state => pure state
+    | other => do
+      addTest $ assertUnreachable $ other.toString
+      return ()
+  addTest $ LSpec.check s!":= {expr}" ((← state3.serializeGoals).map (·.devolatilize) =
+    #[])
+
+  let state2b ← match state3.continue state2 with
+    | .ok state => pure state
+    | .error e => do
+      addTest $ assertUnreachable e
+      return ()
+  let expr := "Or.inl y"
+  let state4 ← match ← state2b.tryAssign (goalId := 0) (expr := expr) with
+    | .success state => pure state
+    | other => do
+      addTest $ assertUnreachable $ other.toString
+      return ()
+  addTest $ LSpec.check s!":= {expr}" ((← state4.serializeGoals).map (·.devolatilize) =
+    #[])
+
+  addTest $ LSpec.check "(4 root)" state4.rootExpr?.isSome
+
+def test_let (specialized: Bool): TestT Elab.TermElabM Unit := do
+  let rootExpr ← parseSentence "∀ (p q: Prop), p → ((p ∨ q) ∨ (p ∨ q))"
+  let state0 ← GoalState.create rootExpr
+  let tactic := "intro a p h"
+  let state1 ← match ← state0.tryTactic (goalId := 0) (tactic := tactic) with
+    | .success state => pure state
+    | other => do
+      addTest $ assertUnreachable $ other.toString
+      return ()
+  addTest $ LSpec.check tactic ((← state1.serializeGoals).map (·.devolatilize) =
+    #[{
+      target := { pp? := .some mainTarget },
+      vars := interiorVars,
+    }])
+
+  let letType := "Nat"
+  let expr := s!"let b: {letType} := _; _"
+  let result2 ← match specialized with
+    | true => state1.tryLet (goalId := 0) (binderName := "b") (type := letType)
+    | false => state1.tryAssign (goalId := 0) (expr := expr)
+  let state2 ← match result2 with
+    | .success state => pure state
+    | other => do
+      addTest $ assertUnreachable $ other.toString
+      return ()
+  let serializedState2 ← state2.serializeGoals
+  let letBindName := if specialized then "b" else "_1"
+  addTest $ LSpec.check expr (serializedState2.map (·.devolatilize) =
+    #[{
+      target := { pp? := .some letType },
+      vars := interiorVars,
+      userName? := .some letBindName
+    },
+    {
+      target := { pp? := .some mainTarget },
+      vars := interiorVars ++ #[{
+        userName := "b",
+        type? := .some { pp? := .some letType },
+        value? := .some { pp? := .some s!"?{letBindName}" },
+      }],
+      userName? := if specialized then .none else .some "_2",
+    }
+    ])
+
+  let tactic := "exact 1"
+  let state3 ← match ← state2.tryTactic (goalId := 0) (tactic := tactic) with
+    | .success state => pure state
+    | other => do
+      addTest $ assertUnreachable $ other.toString
+      return ()
+  addTest $ LSpec.check tactic ((← state3.serializeGoals).map (·.devolatilize) = #[])
+
+  let state3r ← match state3.continue state2 with
+    | .error msg => do
+      addTest $ assertUnreachable $ msg
+      return ()
+    | .ok state => pure state
+  addTest $ LSpec.check "(continue)" ((← state3r.serializeGoals).map (·.devolatilize) =
+    #[
+    {
+      target := { pp? := .some mainTarget },
+      vars := interiorVars ++ #[{
+        userName := "b",
+        type? := .some { pp? := .some "Nat" },
+        value? := .some { pp? := .some "1" },
+      }],
+      userName? := if specialized then .none else .some "_2",
+    }
+    ])
+
+  let tactic := "exact h"
+  match ← state3r.tryTactic (goalId := 0) (tactic := tactic) with
+  | .failure #[message] =>
+    addTest $ LSpec.check tactic  (message = s!"type mismatch\n  h\nhas type\n  a : Prop\nbut is expected to have type\n  {mainTarget} : Prop")
+  | other => do
+    addTest $ assertUnreachable $ other.toString
+
+  let tactic := "exact Or.inl (Or.inl h)"
+  let state4 ← match ← state3r.tryTactic (goalId := 0) (tactic := tactic) with
+    | .success state => pure state
+    | other => do
+      addTest $ assertUnreachable $ other.toString
+      return ()
+  addTest $ LSpec.test "(4 root)" state4.rootExpr?.isSome
+  where
+    mainTarget := "(a ∨ p) ∨ a ∨ p"
+    interiorVars: Array Protocol.Variable := #[
+        { userName := "a", type? := .some { pp? := .some "Prop" }, },
+        { userName := "p", type? := .some { pp? := .some "Prop" }, },
+        { userName := "h", type? := .some { pp? := .some "a" }, }
+      ]
+
+def suite (env: Environment): List (String × IO LSpec.TestSeq) :=
+  [
+    ("eval", test_eval),
+    ("Proof eval", test_proof_eval),
+    ("Proof have", test_proof_have),
+    ("let via assign", test_let false),
+    ("let via tryLet", test_let true),
+  ] |>.map (λ (name, t) => (name, runTestTermElabM env t))
+
+end Pantograph.Test.Tactic.Prograde

flake.lock

@@ -91,16 +91,16 @@
     "lspec": {
       "flake": false,
       "locked": {
-        "lastModified": 1701971219,
-        "narHash": "sha256-HYDRzkT2UaLDrqKNWesh9C4LJNt0JpW0u68wYVj4Byw=",
+        "lastModified": 1722857503,
+        "narHash": "sha256-F9uaymiw1wTCLrJm4n1Bpk3J8jW6poedQzvnnQlZ6Kw=",
         "owner": "lurk-lab",
         "repo": "LSpec",
-        "rev": "3388be5a1d1390594a74ec469fd54a5d84ff6114",
+        "rev": "8a51034d049c6a229d88dd62f490778a377eec06",
         "type": "github"
       },
       "original": {
         "owner": "lurk-lab",
-        "ref": "3388be5a1d1390594a74ec469fd54a5d84ff6114",
+        "ref": "8a51034d049c6a229d88dd62f490778a377eec06",
         "repo": "LSpec",
         "type": "github"
       }

flake.nix

@@ -9,7 +9,7 @@
       url = "github:leanprover/lean4?ref=v4.10.0-rc1";
     };
     lspec = {
-      url = "github:lurk-lab/LSpec?ref=3388be5a1d1390594a74ec469fd54a5d84ff6114";
+      url = "github:lurk-lab/LSpec?ref=8a51034d049c6a229d88dd62f490778a377eec06";
       flake = false;
     };
   };
@@ -63,9 +63,11 @@
       packages = {
         inherit (leanPkgs) lean lean-all;
         inherit (project) sharedLib executable;
-        inherit project leanPkgs;
         default = project.executable;
       };
+      legacyPackages = {
+        inherit project leanPkgs;
+      };
       checks = {
         test = pkgs.runCommand "test" {
           buildInputs = [ test.executable leanPkgs.lean-all ];