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,31 +287,29 @@ 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
-    goalState.restoreMetaM
+  let savedState := goalState.savedState
-    let savedState := goalState.savedState
+  let goals := savedState.tactic.goals
-    let goals := savedState.tactic.goals
+  let mctx ← getMCtx
-    let mctx ← getMCtx
+  let root := goalState.root
-    let root := goalState.root
+  -- Print the root
-    -- Print the root
+  let result: String ← match mctx.decls.find? root with
-    let result: String ← match mctx.decls.find? root with
+    | .some decl => printMVar ">" root decl
-      | .some decl => printMVar ">" root decl
+    | .none => pure s!">{root.name}: ??"
-      | .none => pure s!">{root.name}: ??"
+  let resultGoals ← goals.filter (· != root) |>.mapM (fun mvarId =>
-    let resultGoals ← goals.filter (· != root) |>.mapM (fun mvarId =>
+    match mctx.decls.find? mvarId with
-      match mctx.decls.find? mvarId with
+    | .some decl => printMVar "⊢" mvarId decl
-      | .some decl => printMVar "⊢" mvarId decl
+    | .none => pure s!"⊢{mvarId.name}: ??"
-      | .none => pure s!"⊢{mvarId.name}: ??"
+  )
-    )
+  let goals := goals.toSSet
-    let goals := goals.toSSet
+  let resultOthers ← mctx.decls.toList.filter (λ (mvarId, _) =>
-    let resultOthers ← mctx.decls.toList.filter (λ (mvarId, _) =>
+      !(goals.contains mvarId || mvarId == root) && options.printAll)
-        !(goals.contains mvarId || mvarId == root) && options.printAll)
+      |>.mapM (fun (mvarId, decl) => do
-        |>.mapM (fun (mvarId, decl) => do
+        let pref := if parentHasMVar mvarId then " " else "~"
-          let pref := if parentHasMVar mvarId then " " else "~"
+        printMVar pref mvarId decl
-          printMVar pref mvarId decl
+      )
-        )
+  pure $ result ++ "\n" ++ (resultGoals.map (· ++ "\n") |> String.join) ++ (resultOthers.map (· ++ "\n") |> String.join)
-    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,95 +4,82 @@ 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 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 ++ `α)
-  let f ← Meta.mkFreshExprMVar (.some <| .forallE .anonymous α β .default)
-    .synthetic (userName := userName ++ `f)
-  let a₁ ← Meta.mkFreshExprMVar (.some α)
-    .synthetic (userName := userName ++ `a₁)
-  let a₂ ← Meta.mkFreshExprMVar (.some α)
-    .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 conduit ← Meta.mkFreshExprMVar conduitType
-    .synthetic (userName := userName ++ `conduit)
-  mvarId.assign $ ← Meta.mkEqMP conduit (← Meta.mkCongrArg f h)
-  let result := [α, a₁, a₂, f,  h, conduit]
-  return result.map (·.mvarId!)
-
-def evalCongruenceArg: 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 u ← Meta.mkFreshLevelMVar
-  let target ← mvarId.getType
+    let α ← Meta.mkFreshExprMVar (.some $ mkSort u)
-  let .some (β, _, _) := target.eq? | throwError "Goal is not an Eq"
+      .natural (userName := userName ++ `α)
-  let userName := (← mvarId.getDecl).userName
+    let f ← Meta.mkFreshExprMVar (.some <| .forallE .anonymous α β .default)
-  let u ← Meta.mkFreshLevelMVar
+      .synthetic (userName := userName ++ `f)
-  let α ← Meta.mkFreshExprMVar (.some $ mkSort u)
+    let a₁ ← Meta.mkFreshExprMVar (.some α)
-    .natural (userName := userName ++ `α)
+      .synthetic (userName := userName ++ `a₁)
-  let fType := .forallE .anonymous α β .default
+    let a₂ ← Meta.mkFreshExprMVar (.some α)
-  let f₁ ← Meta.mkFreshExprMVar (.some fType)
+      .synthetic (userName := userName ++ `a₂)
-    .synthetic (userName := userName ++ `f₁)
+    let h ← Meta.mkFreshExprMVar (.some $ ← Meta.mkEq a₁ a₂)
-  let f₂ ← Meta.mkFreshExprMVar (.some fType)
+      .synthetic (userName := userName ++ `h)
-    .synthetic (userName := userName ++ `f₂)
+    let conduitType ← Meta.mkEq (← Meta.mkEq (.app f a₁) (.app f a₂)) (← goal.getType)
-  let a ← Meta.mkFreshExprMVar (.some α)
+    let conduit ← Meta.mkFreshExprMVar conduitType
-    .synthetic (userName := userName ++ `a)
+      .synthetic (userName := userName ++ `conduit)
-  let h ← Meta.mkFreshExprMVar (.some $ ← Meta.mkEq f₁ f₂)
+    goal.assign $ ← Meta.mkEqMP conduit (← Meta.mkCongrArg f h)
-    .synthetic (userName := userName ++ `h)
+    return [α, a₁, a₂, f,  h, conduit]
-  let conduitType ← Meta.mkEq (← Meta.mkEq (.app f₁ a) (.app f₂ a)) target
+  Elab.Tactic.setGoals <| nextGoals.map (·.mvarId!)
-  let conduit ← Meta.mkFreshExprMVar conduitType
-    .synthetic (userName := userName ++ `conduit)
-  mvarId.assign $ ← Meta.mkEqMP conduit (← Meta.mkCongrFun h a)
-  let result := [α, f₁, f₂, h, a, conduit]
-  return result.map (·.mvarId!)
 
-def evalCongruenceFun: Elab.Tactic.TacticM Unit := do
+def congruenceFun: 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 u ← Meta.mkFreshLevelMVar
-  let target ← mvarId.getType
+    let α ← Meta.mkFreshExprMVar (.some $ mkSort u)
-  let .some (β, _, _) := target.eq? | throwError "Goal is not an Eq"
+      .natural (userName := userName ++ `α)
-  let userName := (← mvarId.getDecl).userName
+    let fType := .forallE .anonymous α β .default
-  let u ← Meta.mkFreshLevelMVar
+    let f₁ ← Meta.mkFreshExprMVar (.some fType)
-  let α ← Meta.mkFreshExprMVar (.some $ mkSort u)
+      .synthetic (userName := userName ++ `f₁)
-    .natural (userName := userName ++ `α)
+    let f₂ ← Meta.mkFreshExprMVar (.some fType)
-  let fType := .forallE .anonymous α β .default
+      .synthetic (userName := userName ++ `f₂)
-  let f₁ ← Meta.mkFreshExprMVar (.some fType)
+    let a ← Meta.mkFreshExprMVar (.some α)
-    .synthetic (userName := userName ++ `f₁)
+      .synthetic (userName := userName ++ `a)
-  let f₂ ← Meta.mkFreshExprMVar (.some fType)
+    let h ← Meta.mkFreshExprMVar (.some $ ← Meta.mkEq f₁ f₂)
-    .synthetic (userName := userName ++ `f₂)
+      .synthetic (userName := userName ++ `h)
-  let a₁ ← Meta.mkFreshExprMVar (.some α)
+    let conduitType ← Meta.mkEq (← Meta.mkEq (.app f₁ a) (.app f₂ a)) (← goal.getType)
-    .synthetic (userName := userName ++ `a₁)
+    let conduit ← Meta.mkFreshExprMVar conduitType
-  let a₂ ← Meta.mkFreshExprMVar (.some α)
+      .synthetic (userName := userName ++ `conduit)
-    .synthetic (userName := userName ++ `a₂)
+    goal.assign $ ← Meta.mkEqMP conduit (← Meta.mkCongrFun h a)
-  let h₁ ← Meta.mkFreshExprMVar (.some $ ← Meta.mkEq f₁ f₂)
+    return [α, f₁, f₂, h, a, conduit]
-    .synthetic (userName := userName ++ `h₁)
+  Elab.Tactic.setGoals <| nextGoals.map (·.mvarId!)
-  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 conduit ← Meta.mkFreshExprMVar conduitType
-    .synthetic (userName := userName ++ `conduit)
-  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
+def congruence: Elab.Tactic.TacticM Unit := do
   let goal ← Elab.Tactic.getMainGoal
-  let nextGoals ← congruence goal
+  let .some (β, _, _) := (← goal.getType).eq? | throwError "Goal is not an Eq"
-  Elab.Tactic.setGoals nextGoals
+  let userName := (← goal.getDecl).userName
+
+  let nextGoals ← goal.withContext do
+    let u ← Meta.mkFreshLevelMVar
+    let α ← Meta.mkFreshExprMVar (.some $ mkSort u)
+      .natural (userName := userName ++ `α)
+    let fType := .forallE .anonymous α β .default
+    let f₁ ← Meta.mkFreshExprMVar (.some fType)
+      .synthetic (userName := userName ++ `f₁)
+    let f₂ ← Meta.mkFreshExprMVar (.some fType)
+      .synthetic (userName := userName ++ `f₂)
+    let a₁ ← Meta.mkFreshExprMVar (.some α)
+      .synthetic (userName := userName ++ `a₁)
+    let a₂ ← Meta.mkFreshExprMVar (.some α)
+      .synthetic (userName := userName ++ `a₂)
+    let h₁ ← Meta.mkFreshExprMVar (.some $ ← Meta.mkEq f₁ f₂)
+      .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 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!)
 
 end Pantograph.Tactic

Pantograph/Tactic/MotivatedApply.lean

@@ -62,44 +62,44 @@ 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 recursorType ← Meta.inferType recursor
+  let nextGoals: List MVarId ← goal.withContext do
-  let resultant ← mvarId.getType
+    let recursor ← Elab.Term.elabTerm (stx := stx) .none
+    let recursorType ← Meta.inferType recursor
 
-  let info ← match getRecursorInformation recursorType with
+    let resultant ← goal.getType
-    | .some info => pure info
-    | .none => throwError "Recursor return type does not correspond with the invocation of a motive: {← Meta.ppExpr recursorType}"
 
-  let rec go (i: Nat) (prev: Array Expr): MetaM (Array Expr) := do
+    let info ← match getRecursorInformation recursorType with
-    if i ≥ info.nArgs then
+      | .some info => pure info
-      return prev
+      | .none => throwError "Recursor return type does not correspond with the invocation of a motive: {← Meta.ppExpr recursorType}"
-    else
-      let argType := info.args.get! i
-      -- If `argType` has motive references, its goal needs to be placed in it
-      let argType := argType.instantiateRev prev
-      let bvarIndex := info.nArgs - i - 1
-      let argGoal ← if bvarIndex = info.iMotive then
-          let surrogateMotiveType ← info.surrogateMotiveType prev resultant
-          Meta.mkFreshExprMVar surrogateMotiveType .syntheticOpaque (userName := `motive)
-        else
-          Meta.mkFreshExprMVar argType .syntheticOpaque (userName := .anonymous)
-      let prev :=  prev ++ [argGoal]
-      go (i + 1) prev
-    termination_by info.nArgs - i
-  let mut newMVars ← go 0 #[]
 
-  -- Create the conduit type which proves the result of the motive is equal to the goal
+    let rec go (i: Nat) (prev: Array Expr): MetaM (Array Expr) := do
-  let conduitType ← info.conduitType newMVars resultant
+      if i ≥ info.nArgs then
-  let goalConduit ← Meta.mkFreshExprMVar conduitType .natural (userName := `conduit)
+        return prev
-  mvarId.assign $ ← Meta.mkEqMP goalConduit (mkAppN recursor newMVars)
+      else
-  newMVars := newMVars ++ [goalConduit]
+        let argType := info.args.get! i
+        -- If `argType` has motive references, its goal needs to be placed in it
+        let argType := argType.instantiateRev prev
+        let bvarIndex := info.nArgs - i - 1
+        let argGoal ← if bvarIndex = info.iMotive then
+            let surrogateMotiveType ← info.surrogateMotiveType prev resultant
+            Meta.mkFreshExprMVar surrogateMotiveType .syntheticOpaque (userName := `motive)
+          else
+            Meta.mkFreshExprMVar argType .syntheticOpaque (userName := .anonymous)
+        let prev :=  prev ++ [argGoal]
+        go (i + 1) prev
+      termination_by info.nArgs - i
+    let mut newMVars ← go 0 #[]
 
-  return newMVars.map (λ mvar => { mvarId := mvar.mvarId!})
+    -- 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)
+    newMVars := newMVars ++ [goalConduit]
 
-def evalMotivatedApply : Elab.Tactic.Tactic := fun stx => Elab.Tactic.withMainContext do
+    let nextGoals := newMVars.toList.map (·.mvarId!)
-  let recursor ← Elab.Term.elabTerm (stx := stx) .none
+    pure nextGoals
-  let nextGoals ← motivatedApply (← Elab.Tactic.getMainGoal) recursor
+  Elab.Tactic.setGoals nextGoals
-  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,82 +7,103 @@ 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"
-  let expr ← parseSentence expr
+  runMetaMSeq env do
-  Meta.lambdaTelescope expr $ λ _ body => do
+    let expr ← parseSentence expr
-    let target ← Meta.mkFreshExprSyntheticOpaqueMVar body
+    Meta.lambdaTelescope expr $ λ _ body => do
-    let newGoals ← runTacticOnMVar Tactic.evalCongruenceArg target.mvarId!
+      let mut tests := LSpec.TestSeq.done
-    addTest $ LSpec.check "goals" ((← newGoals.mapM (λ x => mvarUserNameAndType x)) =
+      let target ← Meta.mkFreshExprSyntheticOpaqueMVar body
-      [
+      let (newGoals, test) ← runTermElabMInMeta do
-        (`α, "Sort ?u.30"),
+        let newGoals ← runTacticOnMVar Tactic.congruenceArg target.mvarId!
-        (`a₁, "?α"),
+        let test := LSpec.check "goals" ((← newGoals.mapM (λ x => mvarUserNameAndType x)) =
-        (`a₂, "?α"),
+          [
-        (`f, "?α → List α"),
+            (`α, "Sort ?u.30"),
-        (`h, "?a₁ = ?a₂"),
+            (`a₁, "?α"),
-        (`conduit, "(?f ?a₁ = ?f ?a₂) = (l1.reverse = l2.reverse)"),
+            (`a₂, "?α"),
-      ])
+            (`f, "?α → List α"),
-    let f := newGoals.get! 3
+            (`h, "?a₁ = ?a₂"),
-    let h := newGoals.get! 4
+            (`conduit, "(?f ?a₁ = ?f ?a₂) = (l1.reverse = l2.reverse)"),
-    let c := newGoals.get! 5
+          ])
-    let results ← f.apply (← parseSentence "List.reverse")
+        return (newGoals, test)
-    addTest $ LSpec.check "apply" (results.length = 0)
+      tests := tests ++ test
-    addTest $ LSpec.check "h" ((← exprToStr $ ← h.getType) = "?a₁ = ?a₂")
+      let f := newGoals.get! 3
-    addTest $ LSpec.check "conduit" ((← exprToStr $ ← c.getType) = "(?a₁.reverse = ?a₂.reverse) = (l1.reverse = l2.reverse)")
+      let h := newGoals.get! 4
-def test_congr_arg : TestT Elab.TermElabM Unit := do
+      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 :=
   let expr := "λ (n m: Nat) (h: n = m) => n * n = m * m"
-  let expr ← parseSentence expr
+  runMetaMSeq env do
-  Meta.lambdaTelescope expr $ λ _ body => do
+    let expr ← parseSentence expr
-    let target ← Meta.mkFreshExprSyntheticOpaqueMVar body
+    Meta.lambdaTelescope expr $ λ _ body => do
-    let newGoals ← runTacticOnMVar Tactic.evalCongruenceArg target.mvarId!
+      let mut tests := LSpec.TestSeq.done
-    addTest $  LSpec.check "goals" ((← newGoals.mapM (λ x => mvarUserNameAndType x)) =
+      let target ← Meta.mkFreshExprSyntheticOpaqueMVar body
-      [
+      let test ← runTermElabMInMeta do
-        (`α, "Sort ?u.70"),
+        let newGoals ← runTacticOnMVar Tactic.congruenceArg target.mvarId!
-        (`a₁, "?α"),
+        pure $ LSpec.check "goals" ((← newGoals.mapM (λ x => mvarUserNameAndType x)) =
-        (`a₂, "?α"),
+          [
-        (`f, "?α → Nat"),
+            (`α, "Sort ?u.70"),
-        (`h, "?a₁ = ?a₂"),
+            (`a₁, "?α"),
-        (`conduit, "(?f ?a₁ = ?f ?a₂) = (n * n = m * m)"),
+            (`a₂, "?α"),
-      ])
+            (`f, "?α → Nat"),
-def test_congr_fun : TestT Elab.TermElabM Unit := do
+            (`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 :=
   let expr := "λ (n m: Nat) => (n + m) + (n + m) = (n + m) * 2"
-  let expr ← parseSentence expr
+  runMetaMSeq env do
-  Meta.lambdaTelescope expr $ λ _ body => do
+    let expr ← parseSentence expr
-    let target ← Meta.mkFreshExprSyntheticOpaqueMVar body
+    Meta.lambdaTelescope expr $ λ _ body => do
-    let newGoals ← runTacticOnMVar Tactic.evalCongruenceFun target.mvarId!
+      let mut tests := LSpec.TestSeq.done
-    addTest $ LSpec.check "goals" ((← newGoals.mapM (λ x => mvarUserNameAndType x)) =
+      let target ← Meta.mkFreshExprSyntheticOpaqueMVar body
-      [
+      let test ← runTermElabMInMeta do
-        (`α, "Sort ?u.159"),
+        let newGoals ← runTacticOnMVar Tactic.congruenceFun target.mvarId!
-        (`f₁, "?α → Nat"),
+        pure $ LSpec.check "goals" ((← newGoals.mapM (λ x => mvarUserNameAndType x)) =
-        (`f₂, "?α → Nat"),
+          [
-        (`h, "?f₁ = ?f₂"),
+            (`α, "Sort ?u.159"),
-        (`a, "?α"),
+            (`f₁, "?α → Nat"),
-        (`conduit, "(?f₁ ?a = ?f₂ ?a) = (n + m + (n + m) = (n + m) * 2)"),
+            (`f₂, "?α → Nat"),
-      ])
+            (`h, "?f₁ = ?f₂"),
-def test_congr : TestT Elab.TermElabM Unit := do
+            (`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 :=
   let expr := "λ (a b: Nat) => a = b"
-  let expr ← parseSentence expr
+  runMetaMSeq env do
-  Meta.lambdaTelescope expr $ λ _ body => do
+    let expr ← parseSentence expr
-    let target ← Meta.mkFreshExprSyntheticOpaqueMVar body
+    Meta.lambdaTelescope expr $ λ _ body => do
-    let newGoals ← runTacticOnMVar Tactic.evalCongruence target.mvarId!
+      let mut tests := LSpec.TestSeq.done
-    addTest $  LSpec.check "goals" ((← newGoals.mapM (λ x => mvarUserNameAndType x)) =
+      let target ← Meta.mkFreshExprSyntheticOpaqueMVar body
-      [
+      let test ← runTermElabMInMeta do
-        (`α, "Sort ?u.10"),
+        let newGoals ← runTacticOnMVar Tactic.congruence target.mvarId!
-        (`f₁, "?α → Nat"),
+        pure $ LSpec.check "goals" ((← newGoals.mapM (λ x => mvarUserNameAndType x)) =
-        (`f₂, "?α → Nat"),
+          [
-        (`a₁, "?α"),
+            (`α, "Sort ?u.10"),
-        (`a₂, "?α"),
+            (`f₁, "?α → Nat"),
-        (`h₁, "?f₁ = ?f₂"),
+            (`f₂, "?α → Nat"),
-        (`h₂, "?a₁ = ?a₂"),
+            (`a₁, "?α"),
-        (`conduit, "(?f₁ ?a₁ = ?f₂ ?a₂) = (a = b)"),
+            (`a₂, "?α"),
-      ])
+            (`h₁, "?f₁ = ?f₂"),
+            (`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,23 +7,82 @@ 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 :=
-  let recursor ← parseSentence "@Nat.brecOn"
+  runMetaMSeq env do
-  let recursorType ← Meta.inferType recursor
+    let mut tests := LSpec.TestSeq.done
-  addTest $ LSpec.check "recursorType" ("{motive : Nat → Sort ?u.1} → (t : Nat) → ((t : Nat) → Nat.below t → motive t) → motive t" =
+    let recursor ← parseSentence "@Nat.brecOn"
-    (← exprToStr recursorType))
+    let recursorType ← Meta.inferType recursor
-  let info ← match Tactic.getRecursorInformation recursorType with
+    tests := tests ++ LSpec.check "recursorType" ("{motive : Nat → Sort ?u.1} → (t : Nat) → ((t : Nat) → Nat.below t → motive t) → motive t" =
-    | .some info => pure info
+      (← exprToStr recursorType))
-    | .none => throwError "Failed to extract recursor info"
+    let info ← match Tactic.getRecursorInformation recursorType with
-  addTest $ LSpec.check "iMotive" (info.iMotive = 2)
+      | .some info => pure info
-  let motiveType := info.getMotiveType
+      | .none => throwError "Failed to extract recursor info"
-  addTest $ LSpec.check "motiveType" ("Nat → Sort ?u.1" =
+    tests := tests ++ LSpec.check "iMotive" (info.iMotive = 2)
-    (← exprToStr motiveType))
+    let motiveType := info.getMotiveType
+    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"
-  let expr ← parseSentence expr
+  runMetaMSeq env do
-  Meta.lambdaTelescope expr $ λ _ body => do
+    let expr ← parseSentence expr
+    Meta.lambdaTelescope expr $ λ _ body => do
+      let recursor ← match Parser.runParserCategory
+        (env := ← MonadEnv.getEnv)
+        (catName := `term)
+        (input := "@Nat.brecOn")
+        (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 newGoals ← runTacticOnMVar tactic target.mvarId!
+        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)",
+          ])
+      tests := tests ++ test
+      return tests
+
+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
+        (env := ← MonadEnv.getEnv)
+        (catName := `term)
+        (input := "@List.brecOn")
+        (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 newGoals ← runTacticOnMVar tactic target.mvarId!
+        pure $ LSpec.check "goals" ((← newGoals.mapM (λ g => do exprToStr (← g.getType))) =
+          [
+            "Type ?u.90",
+            "List ?m.92 → Prop",
+            "List ?m.92",
+            "∀ (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
+  let expr := "λ (n t: Nat) => n + 0 = n"
+  runMetaMSeq env $ runTermElabMInMeta do
     let recursor ← match Parser.runParserCategory
       (env := ← MonadEnv.getEnv)
       (catName := `term)
@@ -31,83 +90,41 @@ def test_nat_brec_on : TestT Elab.TermElabM Unit := do
       (fileName := filename) with
       | .ok syn => pure syn
       | .error error => throwError "Failed to parse: {error}"
-    -- Apply the tactic
+    let expr ← parseSentence expr
-    let target ← Meta.mkFreshExprSyntheticOpaqueMVar body
+    Meta.lambdaTelescope expr $ λ _ body => do
-    let tactic := Tactic.evalMotivatedApply recursor
+      let mut tests := LSpec.TestSeq.done
-    let newGoals ← runTacticOnMVar tactic target.mvarId!
+      -- Apply the tactic
-    let test :=  LSpec.check "goals" ((← newGoals.mapM (λ g => do exprToStr (← g.getType))) =
+      let target ← Meta.mkFreshExprSyntheticOpaqueMVar body
-      [
+      let tactic := Tactic.motivatedApply recursor
-        "Nat → Prop",
+      let newGoals ← runTacticOnMVar tactic target.mvarId!
-        "Nat",
+      let majorId := 67
-        "∀ (t : Nat), Nat.below t → ?motive t",
+      tests := tests ++ (LSpec.check "goals" ((← newGoals.mapM (λ g => do exprToStr (← g.getType))) =
-        "?motive ?m.67 = (n + 0 = n)",
+        [
-      ])
+          "Nat → Prop",
-    addTest test
+          "Nat",
+          "∀ (t : Nat), Nat.below t → ?motive t",
+          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}"))
 
-def test_list_brec_on : TestT Elab.TermElabM Unit := do
+      -- Assign motive to `λ x => x + _`
-  let expr := "λ {α : Type} (l: List α) => l ++ [] = [] ++ l"
+      let motive_assign ← parseSentence "λ (x: Nat) => @Nat.add x + 0 = _"
-  let expr ← parseSentence expr
+      motive.assign motive_assign
-  Meta.lambdaTelescope expr $ λ _ body => do
-    let recursor ← match Parser.runParserCategory
-      (env := ← MonadEnv.getEnv)
-      (catName := `term)
-      (input := "@List.brecOn")
-      (fileName := filename) with
-      | .ok syn => pure syn
-      | .error error => throwError "Failed to parse: {error}"
-    -- Apply the tactic
-    let target ← Meta.mkFreshExprSyntheticOpaqueMVar body
-    let tactic := Tactic.evalMotivatedApply recursor
-    let newGoals ← runTacticOnMVar tactic target.mvarId!
-    addTest $ LSpec.check "goals" ((← newGoals.mapM (λ g => do exprToStr (← g.getType))) =
-      [
-        "Type ?u.90",
-        "List ?m.92 → Prop",
-        "List ?m.92",
-        "∀ (t : List ?m.92), List.below t → ?motive t",
-        "?motive ?m.94 = (l ++ [] = [] ++ l)",
-      ])
 
-def test_partial_motive_instantiation : TestT Elab.TermElabM Unit := do
+      let test ← conduit.withContext do
-  let expr := "λ (n t: Nat) => n + 0 = n"
+        let t := toString (← Meta.ppExpr $ ← conduit.getType)
-  let recursor ← match Parser.runParserCategory
+        return LSpec.check "conduit" (t = s!"(?m.{majorId}.add + 0 = ?m.138 ?m.{majorId}) = (n + 0 = n)")
-    (env := ← MonadEnv.getEnv)
+      tests := tests ++ test
-    (catName := `term)
-    (input := "@Nat.brecOn")
-    (fileName := filename) with
-    | .ok syn => pure syn
-    | .error error => throwError "Failed to parse: {error}"
-  let expr ← parseSentence expr
-  Meta.lambdaTelescope expr $ λ _ body => do
-    -- Apply the tactic
-    let target ← Meta.mkFreshExprSyntheticOpaqueMVar body
-    let tactic := Tactic.evalMotivatedApply recursor
-    let newGoals ← runTacticOnMVar tactic target.mvarId!
-    let majorId := 67
-    addTest $ (LSpec.check "goals" ((← newGoals.mapM (λ g => do exprToStr (← g.getType))) =
-      [
-        "Nat → Prop",
-        "Nat",
-        "∀ (t : Nat), Nat.below t → ?motive t",
-        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}"))
 
-    -- Assign motive to `λ x => x + _`
+      return tests
-    let motive_assign ← parseSentence "λ (x: Nat) => @Nat.add x + 0 = _"
-    motive.assign motive_assign
-
-    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)")
 
 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,66 +7,81 @@ 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"
-  let expr ← parseSentence expr
+  runMetaMSeq env do
-  Meta.lambdaTelescope expr $ λ _ body => do
+    let expr ← parseSentence expr
-    let recursor ← match Parser.runParserCategory
+    Meta.lambdaTelescope expr $ λ _ body => do
-      (env := ← MonadEnv.getEnv)
+      let recursor ← match Parser.runParserCategory
-      (catName := `term)
+        (env := ← MonadEnv.getEnv)
-      (input := "h")
+        (catName := `term)
-      (fileName := filename) with
+        (input := "h")
-      | .ok syn => pure syn
+        (fileName := filename) with
-      | .error error => throwError "Failed to parse: {error}"
+        | .ok syn => pure syn
-    -- Apply the tactic
+        | .error error => throwError "Failed to parse: {error}"
-    let target ← Meta.mkFreshExprSyntheticOpaqueMVar body
+      let mut tests := LSpec.TestSeq.done
-    let tactic := Tactic.evalNoConfuse recursor
+      -- Apply the tactic
-    let newGoals ← runTacticOnMVar tactic target.mvarId!
+      let target ← Meta.mkFreshExprSyntheticOpaqueMVar body
-    addTest $ LSpec.check "goals" ((← newGoals.mapM (λ g => do exprToStr (← g.getType))) = [])
+      let tactic := Tactic.noConfuse recursor
+      let test ← runTermElabMInMeta do
+        let newGoals ← runTacticOnMVar tactic target.mvarId!
+        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"
-  let expr ← parseSentence expr
+  runMetaMSeq env do
-  Meta.lambdaTelescope expr $ λ _ body => do
+    let expr ← parseSentence expr
-    let recursor ← match Parser.runParserCategory
+    Meta.lambdaTelescope expr $ λ _ body => do
-      (env := ← MonadEnv.getEnv)
+      let recursor ← match Parser.runParserCategory
-      (catName := `term)
+        (env := ← MonadEnv.getEnv)
-      (input := "h")
+        (catName := `term)
-      (fileName := filename) with
+        (input := "h")
-      | .ok syn => pure syn
+        (fileName := filename) with
-      | .error error => throwError "Failed to parse: {error}"
+        | .ok syn => pure syn
-    -- Apply the tactic
+        | .error error => throwError "Failed to parse: {error}"
-    let target ← Meta.mkFreshExprSyntheticOpaqueMVar body
+      let mut tests := LSpec.TestSeq.done
-    try
+      -- Apply the tactic
-      let tactic := Tactic.evalNoConfuse recursor
+      let target ← Meta.mkFreshExprSyntheticOpaqueMVar body
-      let _ ← runTacticOnMVar tactic target.mvarId!
+      try
-      addTest $ assertUnreachable "Tactic should fail"
+        let tactic := Tactic.noConfuse recursor
-    catch _ =>
+        let _ ← runTermElabMInMeta $ runTacticOnMVar tactic target.mvarId!
-      addTest $ LSpec.check "Tactic should fail" true
+        tests := tests ++ assertUnreachable "Tactic should fail"
+      catch _ =>
+        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"
-  let expr ← parseSentence expr
+  runMetaMSeq env do
-  Meta.lambdaTelescope expr $ λ _ body => do
+    let expr ← parseSentence expr
-    let recursor ← match Parser.runParserCategory
+    Meta.lambdaTelescope expr $ λ _ body => do
-      (env := ← MonadEnv.getEnv)
+      let recursor ← match Parser.runParserCategory
-      (catName := `term)
+        (env := ← MonadEnv.getEnv)
-      (input := "h")
+        (catName := `term)
-      (fileName := filename) with
+        (input := "h")
-      | .ok syn => pure syn
+        (fileName := filename) with
-      | .error error => throwError "Failed to parse: {error}"
+        | .ok syn => pure syn
-    -- Apply the tactic
+        | .error error => throwError "Failed to parse: {error}"
-    let target ← Meta.mkFreshExprSyntheticOpaqueMVar body
+      let mut tests := LSpec.TestSeq.done
-    let tactic := Tactic.evalNoConfuse recursor
+      -- Apply the tactic
-    let newGoals ← runTacticOnMVar tactic target.mvarId!
+      let target ← Meta.mkFreshExprSyntheticOpaqueMVar body
-    addTest $ LSpec.check "goals"
+      let tactic := Tactic.noConfuse recursor
-      ((← newGoals.mapM (λ g => do exprToStr (← g.getType))) = [])
+      let test ← runTermElabMInMeta do
+        let newGoals ← runTacticOnMVar tactic target.mvarId!
+        pure $ LSpec.check "goals" ((← 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" {