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 (← goalState.tryHave args.goalId binderName type))
+          pure ( Except.ok (← goalHave goalState 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

@@ -1,14 +0,0 @@
-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,7 +5,6 @@ All the functions starting with `try` resume their inner monadic state.
 -/
 import Pantograph.Protocol
 import Pantograph.Tactic
-import Pantograph.Compile.Parse
 import Lean
 
 
@@ -22,6 +21,8 @@ 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
@@ -46,6 +47,7 @@ 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 :=
@@ -86,6 +88,15 @@ 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 {
@@ -154,20 +165,6 @@ 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
@@ -182,21 +179,35 @@ inductive TacticResult where
   | invalidAction (message: String)
 
 /-- Executes a `TacticM` monads on this `GoalState`, collecting the errors as necessary -/
-protected def GoalState.tryTacticM (state: GoalState) (goalId: Nat) (tacticM: Elab.Tactic.TacticM Unit):
+protected def GoalState.executeTactic (state: GoalState) (goalId: Nat) (tacticM: Elab.Tactic.TacticM Unit):
       Elab.TermElabM TacticResult := do
-  let mvarId ← match state.savedState.tactic.goals.get? goalId with
+  state.restoreElabM
+  let goal ← match state.savedState.tactic.goals.get? goalId with
     | .some goal => pure $ goal
     | .none => return .indexError goalId
+  goal.checkNotAssigned `GoalState.executeTactic
   try
-    let nextState ← state.step mvarId tacticM
+    let (_, newGoals) ← tacticM { elaborator := .anonymous } |>.run { goals := [goal] }
-    return .success nextState
+    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,
+    }
   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)
@@ -204,7 +215,7 @@ protected def GoalState.tryTactic (state: GoalState) (goalId: Nat) (tactic: Stri
     (fileName := filename) with
     | .ok stx => pure $ stx
     | .error error => return .parseError error
-  state.tryTacticM goalId $ Elab.Tactic.evalTactic tactic
+  state.executeTactic goalId $ Elab.Tactic.evalTactic tactic
 
 protected def GoalState.tryAssign (state: GoalState) (goalId: Nat) (expr: String):
       Elab.TermElabM TacticResult := do
@@ -216,21 +227,103 @@ protected def GoalState.tryAssign (state: GoalState) (goalId: Nat) (expr: String
     (fileName := filename) with
     | .ok syn => pure syn
     | .error error => return .parseError error
-  state.tryTacticM goalId $ Tactic.evalAssign expr
+  state.executeTactic goalId $ Tactic.evalAssign expr
 
 -- Specialized Tactics
 
-protected def GoalState.tryLet (state: GoalState) (goalId: Nat) (binderName: String) (type: String):
+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 := ← MonadEnv.getEnv)
+    (env := state.env)
     (catName := `term)
     (input := type)
     (fileName := filename) with
     | .ok syn => pure syn
     | .error error => return .parseError error
-  state.tryTacticM goalId $ Tactic.evalLet binderName.toName type
+  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)
+    (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]
 
 /-- Enter conv tactic mode -/
 protected def GoalState.conv (state: GoalState) (goalId: Nat):
@@ -252,9 +345,12 @@ 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
@@ -288,9 +384,12 @@ 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
@@ -370,6 +469,7 @@ protected def GoalState.tryCalc (state: GoalState) (goalId: Nat) (pred: String):
         term := ← MonadBacktrack.saveState,
         tactic := { goals },
       },
+      newMVars := goals.toSSet,
       parentMVar? := .some goal,
       calcPrevRhs?
     }
@@ -380,16 +480,24 @@ 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 (← Compile.parseTermM recursor) with
+  let recursor ← match Parser.runParserCategory
+    (env := state.env)
+    (catName := `term)
+    (input := recursor)
+    (fileName := filename) with
     | .ok syn => pure syn
     | .error error => return .parseError error
-  state.tryTacticM goalId (tacticM := Tactic.evalMotivatedApply recursor)
+  state.executeTactic goalId (tacticM := Tactic.motivatedApply recursor)
 protected def GoalState.tryNoConfuse (state: GoalState) (goalId: Nat) (eq: String):
       Elab.TermElabM TacticResult := do
   state.restoreElabM
-  let eq ← match (← Compile.parseTermM eq) with
+  let recursor ← match Parser.runParserCategory
+    (env := state.env)
+    (catName := `term)
+    (input := eq)
+    (fileName := filename) with
     | .ok syn => pure syn
     | .error error => return .parseError error
-  state.tryTacticM goalId (tacticM := Tactic.evalNoConfuse eq)
+  state.executeTactic goalId (tacticM := Tactic.noConfuse recursor)
 
 end Pantograph

Pantograph/Library.lean

@@ -162,21 +162,8 @@ 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]
-protected def GoalState.tryHave (state: GoalState) (goalId: Nat) (binderName: String) (type: String): CoreM TacticResult := do
+def goalHave (state: GoalState) (goalId: Nat) (binderName: String) (type: String): CoreM TacticResult :=
-  let type ← match (← Compile.parseTermM type) with
+  runTermElabM <| state.tryHave goalId binderName type
-    | .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
@@ -192,5 +179,11 @@ 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: Bool := false
+  isInaccessible?: Option Bool := .none
   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 := .none)
+def serializeGoal (options: @&Protocol.Options) (goal: MVarId) (mvarDecl: MetavarDecl) (parentDecl?: Option MetavarDecl)
       : MetaM Protocol.Goal := do
   -- Options for printing; See Meta.ppGoal for details
   let showLetValues  := true
@@ -215,13 +215,11 @@ 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
@@ -231,7 +229,7 @@ def serializeGoal (options: @&Protocol.Options) (goal: MVarId) (mvarDecl: Metava
         return {
           name := ofName fvarId.name,
           userName:= ofName userName,
-          isInaccessible := userName.isInaccessibleUserName
+          isInaccessible? := .some userName.isInaccessibleUserName
           type? := .some (← serializeExpression options type)
         }
       | .ldecl _ fvarId userName type val _ _ => do
@@ -245,7 +243,7 @@ def serializeGoal (options: @&Protocol.Options) (goal: MVarId) (mvarDecl: Metava
         return {
           name := ofName fvarId.name,
           userName:= ofName userName,
-          isInaccessible := userName.isInaccessibleUserName
+          isInaccessible? := .some userName.isInaccessibleUserName
           type? := .some (← serializeExpression options type)
           value? := value?
         }
@@ -289,8 +287,7 @@ 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 := {}): CoreM String := do
+protected def GoalState.diag (goalState: GoalState) (parent?: Option GoalState := .none) (options: Protocol.GoalDiag := {}): MetaM String := do
-  let metaM: MetaM String := do
   goalState.restoreMetaM
   let savedState := goalState.savedState
   let goals := savedState.tactic.goals
@@ -313,7 +310,6 @@ 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,8 +4,15 @@ open Lean
 
 namespace Pantograph.Tactic
 
-/-- WARNING: This should be used with a function like `elabTermWithHoles` that properly collects the mvar information from `expr`. -/
+private def newMVarSet (mctxOld: @&MetavarContext) (mctxNew: @&MetavarContext): SSet MVarId :=
-def assign (goal: MVarId) (expr: Expr) (nextGoals: List MVarId): MetaM (List MVarId) := do
+  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
   goal.checkNotAssigned `Pantograph.Tactic.assign
 
   -- This run of the unifier is critical in resolving mvars in passing
@@ -13,18 +20,15 @@ def assign (goal: MVarId) (expr: Expr) (nextGoals: List MVarId): MetaM (List MVa
   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.filterM (not <$> ·.isAssigned)
+  nextGoals.toList.filterM (not <$> ·.isAssigned)
 
 def evalAssign : Elab.Tactic.Tactic := fun stx => Elab.Tactic.withMainContext do
-  let target ← Elab.Tactic.getMainTarget
+  let goalType ← Elab.Tactic.getMainTarget
-  let goal ← Elab.Tactic.getMainGoal
+  let expr ← Elab.Term.elabTermAndSynthesize (stx := stx) (expectedType? := .some goalType)
-  goal.checkNotAssigned `Pantograph.Tactic.evalAssign
+  let nextGoals ← assign (← Elab.Tactic.getMainGoal) expr
-  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 (mvarId: MVarId): MetaM (List MVarId) := mvarId.withContext do
+def congruenceArg: Elab.Tactic.TacticM Unit := do
-  mvarId.checkNotAssigned `Pantograph.Tactic.congruenceArg
+  let goal ← Elab.Tactic.getMainGoal
-  let target ← mvarId.getType
+  let .some (β, _, _) := (← goal.getType).eq? | throwError "Goal is not an Eq"
-  let .some (β, _, _) := target.eq? | throwError "Goal is not an Eq"
+  let userName := (← goal.getDecl).userName
-  let userName := (← mvarId.getDecl).userName
 
+  let nextGoals ← goal.withContext do
     let u ← Meta.mkFreshLevelMVar
     let α ← Meta.mkFreshExprMVar (.some $ mkSort u)
       .natural (userName := userName ++ `α)
@@ -21,23 +21,19 @@ def congruenceArg (mvarId: MVarId): MetaM (List MVarId) := mvarId.withContext 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₂)) target
+    let conduitType ← Meta.mkEq (← Meta.mkEq (.app f a₁) (.app f a₂)) (← goal.getType)
     let conduit ← Meta.mkFreshExprMVar conduitType
       .synthetic (userName := userName ++ `conduit)
-  mvarId.assign $ ← Meta.mkEqMP conduit (← Meta.mkCongrArg f h)
+    goal.assign $ ← Meta.mkEqMP conduit (← Meta.mkCongrArg f h)
-  let result := [α, a₁, a₂, f,  h, conduit]
+    return [α, a₁, a₂, f,  h, conduit]
-  return result.map (·.mvarId!)
+  Elab.Tactic.setGoals <| nextGoals.map (·.mvarId!)
 
-def evalCongruenceArg: Elab.Tactic.TacticM Unit := do
+def congruenceFun: Elab.Tactic.TacticM Unit := do
   let goal ← Elab.Tactic.getMainGoal
-  let nextGoals ← congruenceArg goal
+  let .some (β, _, _) := (← goal.getType).eq? | throwError "Goal is not an Eq"
-  Elab.Tactic.setGoals nextGoals
+  let userName := (← goal.getDecl).userName
 
-def congruenceFun (mvarId: MVarId): MetaM (List MVarId) := mvarId.withContext do
+  let nextGoals ← goal.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 ++ `α)
@@ -50,23 +46,19 @@ def congruenceFun (mvarId: MVarId): MetaM (List MVarId) := mvarId.withContext 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)) target
+    let conduitType ← Meta.mkEq (← Meta.mkEq (.app f₁ a) (.app f₂ a)) (← goal.getType)
     let conduit ← Meta.mkFreshExprMVar conduitType
       .synthetic (userName := userName ++ `conduit)
-  mvarId.assign $ ← Meta.mkEqMP conduit (← Meta.mkCongrFun h a)
+    goal.assign $ ← Meta.mkEqMP conduit (← Meta.mkCongrFun h a)
-  let result := [α, f₁, f₂, h, a, conduit]
+    return [α, f₁, f₂, h, a, conduit]
-  return result.map (·.mvarId!)
+  Elab.Tactic.setGoals <| nextGoals.map (·.mvarId!)
 
-def evalCongruenceFun: Elab.Tactic.TacticM Unit := do
+def congruence: Elab.Tactic.TacticM Unit := do
   let goal ← Elab.Tactic.getMainGoal
-  let nextGoals ← congruenceFun goal
+  let .some (β, _, _) := (← goal.getType).eq? | throwError "Goal is not an Eq"
-  Elab.Tactic.setGoals nextGoals
+  let userName := (← goal.getDecl).userName
 
-def congruence (mvarId: MVarId): MetaM (List MVarId) := mvarId.withContext do
+  let nextGoals ← goal.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 ++ `α)
@@ -83,16 +75,11 @@ def congruence (mvarId: MVarId): MetaM (List MVarId) := mvarId.withContext 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₂)) target
+    let conduitType ← Meta.mkEq (← Meta.mkEq (.app f₁ a₁) (.app f₂ a₂)) (← goal.getType)
     let conduit ← Meta.mkFreshExprMVar conduitType
       .synthetic (userName := userName ++ `conduit)
-  mvarId.assign $ ← Meta.mkEqMP conduit (← Meta.mkCongr h₁ h₂)
+    goal.assign $ ← Meta.mkEqMP conduit (← Meta.mkCongr h₁ h₂)
-  let result := [α, f₁, f₂, a₁, a₂, h₁, h₂, conduit]
+    return [α, f₁, f₂, a₁, a₂, h₁, h₂, conduit]
-  return result.map (·.mvarId!)
+  Elab.Tactic.setGoals <| nextGoals.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,10 +62,13 @@ def collectMotiveArguments (forallBody: Expr): SSet Nat :=
   | _ => SSet.empty
 
 /-- Applies a symbol of the type `∀ (motive: α → Sort u) (a: α)..., (motive α)` -/
-def motivatedApply (mvarId: MVarId) (recursor: Expr) : MetaM (Array Meta.InductionSubgoal) := mvarId.withContext do
+def motivatedApply: Elab.Tactic.Tactic := λ stx => do
-  mvarId.checkNotAssigned `Pantograph.Tactic.motivatedApply
+  let goal ← Elab.Tactic.getMainGoal
+  let nextGoals: List MVarId ← goal.withContext do
+    let recursor ← Elab.Term.elabTerm (stx := stx) .none
     let recursorType ← Meta.inferType recursor
-  let resultant ← mvarId.getType
+
+    let resultant ← goal.getType
 
     let info ← match getRecursorInformation recursorType with
       | .some info => pure info
@@ -92,14 +95,11 @@ def motivatedApply (mvarId: MVarId) (recursor: Expr) : MetaM (Array Meta.Inducti
     -- 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)
-  mvarId.assign $ ← Meta.mkEqMP goalConduit (mkAppN recursor newMVars)
+    goal.assign $ ← Meta.mkEqMP goalConduit (mkAppN recursor newMVars)
     newMVars := newMVars ++ [goalConduit]
 
-  return newMVars.map (λ mvar => { mvarId := mvar.mvarId!})
+    let nextGoals := newMVars.toList.map (·.mvarId!)
-
+    pure nextGoals
-def evalMotivatedApply : Elab.Tactic.Tactic := fun stx => Elab.Tactic.withMainContext do
+  Elab.Tactic.setGoals nextGoals
-  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,19 +4,15 @@ open Lean
 
 namespace Pantograph.Tactic
 
-def noConfuse (mvarId: MVarId) (h: Expr): MetaM Unit := mvarId.withContext do
+def noConfuse: Elab.Tactic.Tactic := λ stx => do
-  mvarId.checkNotAssigned `Pantograph.Tactic.noConfuse
-  let target ← mvarId.getType
-  let noConfusion ← Meta.mkNoConfusion (target := target) (h := h)
-
-  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
+  goal.withContext do
-  noConfuse goal h
+    let absurd ← Elab.Term.elabTerm (stx := stx) .none
+    let noConfusion ← Meta.mkNoConfusion (target := ← goal.getType) (h := absurd)
+
+    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
   Elab.Tactic.setGoals []
 
 end Pantograph.Tactic

Pantograph/Tactic/Prograde.lean

@@ -1,87 +0,0 @@
-/- 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,7 +1,6 @@
 import Pantograph.Goal
 import Pantograph.Library
 import Pantograph.Protocol
-import Pantograph.Condensed
 import Lean
 import LSpec
 
@@ -11,7 +10,12 @@ namespace Pantograph
 
 deriving instance Repr for Expr
 -- Use strict equality check for expressions
-instance : BEq Expr := ⟨Expr.equal⟩
+--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}'"
 
 def uniq (n: Nat): Name := .num (.str .anonymous "_uniq") n
 
@@ -21,7 +25,6 @@ def Goal.devolatilizeVars (goal: Goal): Goal :=
   {
     goal with
     vars := goal.vars.map removeInternalAux,
-
   }
   where removeInternalAux (v: Variable): Variable :=
     {
@@ -44,24 +47,6 @@ 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 =>
@@ -88,13 +73,11 @@ 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 := Condensed.elabContext)
+  termElabM.run' (ctx := Pantograph.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): Elab.TermElabM Expr := do
+def parseSentence (s: String): MetaM Expr := do
   let recursor ← match Parser.runParserCategory
     (env := ← MonadEnv.getEnv)
     (catName := `term)
@@ -102,7 +85,7 @@ def parseSentence (s: String): Elab.TermElabM Expr := do
     (fileName := filename) with
     | .ok syn => pure syn
     | .error error => throwError "Failed to parse: {error}"
-  Elab.Term.elabTerm (stx := recursor) .none
+  runTermElabMInMeta $ 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] }
@@ -112,35 +95,6 @@ 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", type? := .some { pp? := .some "Prop" }}],
+    vars := #[{ name := "_uniq.10", userName := "x", isInaccessible? := .some false, 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", type? := .some { pp? := .some "Prop" }},
+      { name := "_uniq.10", userName := "x", isInaccessible? := .some false, type? := .some { pp? := .some "Prop" }},
-      { name := "_uniq.16", userName := "y", type? := .some { pp? := .some "Prop" }}
+      { name := "_uniq.16", userName := "y", isInaccessible? := .some false, type? := .some { pp? := .some "Prop" }}
     ],
   }
   subroutine_runner [

Test/Main.lean

@@ -52,7 +52,6 @@ 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,6 +60,7 @@ 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
@@ -197,16 +198,15 @@ 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 "?m.29 x"])
+    #[.some "∀ (x : Nat), ?m.29 x"])
   addTest $ LSpec.test "(2 root)" state2.rootExpr?.isNone
 
-  let assign := "Eq.refl x"
+  let state3 ← match ← state2.tryAssign (goalId := 0) (expr := "fun x => Eq.refl x") with
-  let state3 ← match ← state2.tryAssign (goalId := 0) (expr := assign) with
     | .success state => pure state
     | other => do
       addTest $ assertUnreachable $ other.toString
       return ()
-  addTest $ LSpec.check s!":= {assign}" ((← state3.serializeGoals (options := ← read)).map (·.target.pp?) =
+  addTest $ LSpec.check ":= Eq.refl" ((← state3.serializeGoals (options := ← read)).map (·.target.pp?) =
     #[])
 
   addTest $ LSpec.test "(3 root)" state3.rootExpr?.isSome

Test/Proofs.lean

@@ -58,6 +58,7 @@ 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):
@@ -68,6 +69,7 @@ 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
@@ -173,6 +175,7 @@ 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
     }
 
@@ -253,9 +256,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" } },
+        { name := fvP, userName := "p", type? := .some { pp? := .some "Prop" }, isInaccessible? := .some false },
-        { name := fvQ, userName := "q", type? := .some { pp? := .some "Prop" } },
+        { name := fvQ, userName := "q", type? := .some { pp? := .some "Prop" }, isInaccessible? := .some false },
-        { name := fvH, userName := "h", type? := .some { pp? := .some "p ∨ q" } }
+        { name := fvH, userName := "h", type? := .some { pp? := .some "p ∨ q" }, isInaccessible? := .some false }
       ]
     }])
   addTest $ LSpec.check "(1 parent)" state1.parentExpr?.isSome
@@ -348,12 +351,75 @@ def test_or_comm: TestM Unit := do
       userName? := .some caseName,
       target := { pp? := .some "q ∨ p" },
       vars := #[
-        { userName := "p", type? := .some typeProp },
+        { userName := "p", type? := .some typeProp, isInaccessible? := .some false },
-        { userName := "q", type? := .some typeProp },
+        { userName := "q", type? := .some typeProp, isInaccessible? := .some false },
-        { userName := "h✝", type? := .some { pp? := .some varName }, isInaccessible := true }
+        { userName := "h✝", type? := .some { pp? := .some varName }, isInaccessible? := .some 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 =>
@@ -541,6 +607,83 @@ 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
@@ -700,6 +843,7 @@ 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
         }],
       }
     ])
@@ -712,8 +856,11 @@ 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,4 +1,3 @@
 import Test.Tactic.Congruence
 import Test.Tactic.MotivatedApply
 import Test.Tactic.NoConfuse
-import Test.Tactic.Prograde

Test/Tactic/Congruence.lean

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

Test/Tactic/MotivatedApply.lean

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

Test/Tactic/NoConfuse.lean

@@ -7,8 +7,9 @@ open Pantograph
 
 namespace Pantograph.Test.Tactic.NoConfuse
 
-def test_nat : TestT Elab.TermElabM Unit := do
+def test_nat (env: Environment): IO LSpec.TestSeq :=
   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
@@ -18,14 +19,20 @@ def test_nat : TestT Elab.TermElabM Unit := do
         (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.evalNoConfuse recursor
+      let tactic := Tactic.noConfuse recursor
+      let test ← runTermElabMInMeta do
         let newGoals ← runTacticOnMVar tactic target.mvarId!
-    addTest $ LSpec.check "goals" ((← newGoals.mapM (λ g => do exprToStr (← g.getType))) = [])
+        pure $ LSpec.check "goals" ((← newGoals.mapM (λ g => do exprToStr (← g.getType))) =
+          [])
+      tests := tests ++ test
+      return tests
 
-def test_nat_fail : TestT Elab.TermElabM Unit := do
+def test_nat_fail (env: Environment): IO LSpec.TestSeq :=
   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
@@ -35,17 +42,21 @@ def test_nat_fail : TestT Elab.TermElabM Unit := do
         (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.evalNoConfuse recursor
+        let tactic := Tactic.noConfuse recursor
-      let _ ← runTacticOnMVar tactic target.mvarId!
+        let _ ← runTermElabMInMeta $ runTacticOnMVar tactic target.mvarId!
-      addTest $ assertUnreachable "Tactic should fail"
+        tests := tests ++ assertUnreachable "Tactic should fail"
       catch _ =>
-      addTest $ LSpec.check "Tactic should fail" true
+        tests := tests ++ LSpec.check "Tactic should fail" true
+        return tests
+      return tests
 
-def test_list : TestT Elab.TermElabM Unit := do
+def test_list (env: Environment): IO LSpec.TestSeq :=
   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
@@ -55,18 +66,22 @@ def test_list : TestT Elab.TermElabM Unit := do
         (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.evalNoConfuse recursor
+      let tactic := Tactic.noConfuse recursor
+      let test ← runTermElabMInMeta do
         let newGoals ← runTacticOnMVar tactic target.mvarId!
-    addTest $ LSpec.check "goals"
+        pure $ LSpec.check "goals" ((← newGoals.mapM (λ g => do exprToStr (← g.getType))) =
-      ((← newGoals.mapM (λ g => do exprToStr (← g.getType))) = [])
+          [])
+      tests := tests ++ test
+      return tests
 
 def suite (env: Environment): List (String × IO LSpec.TestSeq) :=
   [
-    ("Nat", test_nat),
+    ("Nat", test_nat env),
-    ("Nat fail", test_nat_fail),
+    ("Nat fail", test_nat_fail env),
-    ("List", test_list),
+    ("List", test_list env),
-  ] |>.map (λ (name, t) => (name, runTestTermElabM env t))
+  ]
 
 end Pantograph.Test.Tactic.NoConfuse

Test/Tactic/Prograde.lean

@@ -1,266 +0,0 @@
-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": 1722857503,
+        "lastModified": 1701971219,
-        "narHash": "sha256-F9uaymiw1wTCLrJm4n1Bpk3J8jW6poedQzvnnQlZ6Kw=",
+        "narHash": "sha256-HYDRzkT2UaLDrqKNWesh9C4LJNt0JpW0u68wYVj4Byw=",
         "owner": "lurk-lab",
         "repo": "LSpec",
-        "rev": "8a51034d049c6a229d88dd62f490778a377eec06",
+        "rev": "3388be5a1d1390594a74ec469fd54a5d84ff6114",
         "type": "github"
       },
       "original": {
         "owner": "lurk-lab",
-        "ref": "8a51034d049c6a229d88dd62f490778a377eec06",
+        "ref": "3388be5a1d1390594a74ec469fd54a5d84ff6114",
         "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=8a51034d049c6a229d88dd62f490778a377eec06";
+      url = "github:lurk-lab/LSpec?ref=3388be5a1d1390594a74ec469fd54a5d84ff6114";
       flake = false;
     };
   };
@@ -63,10 +63,8 @@
       packages = {
         inherit (leanPkgs) lean lean-all;
         inherit (project) sharedLib executable;
-        default = project.executable;
-      };
-      legacyPackages = {
         inherit project leanPkgs;
+        default = project.executable;
       };
       checks = {
         test = pkgs.runCommand "test" {