Merge pull request 'feat: Elementarized tactics with motives, congruence, and absurdity' (#72) from goal/mapply into dev

Reviewed-on: #72
2024-06-12 13:52:45 -07:00 · 2024-06-12 13:52:45 -07:00 · bd20bf76da
parent 67e7f22b0a 2d2cf75183
commit bd20bf76da
22 changed files with 1251 additions and 251 deletions
--- a/4
+++ b/4
@ -1,9 +1,9 @@
 LIB := ./.lake/build/lib/Pantograph.olean
 EXE := ./.lake/build/bin/pantograph
-SOURCE := $(wildcard Pantograph/*.lean) $(wildcard *.lean) lean-toolchain
+SOURCE := $(wildcard *.lean Pantograph/*.lean Pantograph/**/*.lean) lean-toolchain

 TEST_EXE := ./.lake/build/bin/test
-TEST_SOURCE := $(wildcard Test/*.lean)
+TEST_SOURCE := $(wildcard Test/*.lean Test/**/*.lean)

 $(LIB) $(EXE): $(SOURCE)
 	lake build pantograph
--- a/Pantograph.lean
+++ b/Pantograph.lean
@ -73,7 +73,7 @@ def execute (command: Protocol.Command): MainM Lean.Json := do
    Environment.addDecl args
  expr_echo (args: Protocol.ExprEcho): MainM (CR Protocol.ExprEchoResult) := do
    let state ← get
-    exprEcho args.expr args.type? state.options
+    exprEcho args.expr (expectedType? := args.type?) (levels := args.levels.getD #[]) (options := state.options)
  options_set (args: Protocol.OptionsSet): MainM (CR Protocol.OptionsSetResult) := do
    let state ← get
    let options := state.options
@ -90,13 +90,13 @@ def execute (command: Protocol.Command): MainM Lean.Json := do
      }
    }
    return .ok {  }
-  options_print (_: Protocol.OptionsPrint): MainM (CR Protocol.OptionsPrintResult) := do
+  options_print (_: Protocol.OptionsPrint): MainM (CR Protocol.Options) := do
    return .ok (← get).options
  goal_start (args: Protocol.GoalStart): MainM (CR Protocol.GoalStartResult) := do
    let state ← get
    let env ← Lean.MonadEnv.getEnv
    let expr?: Except _ GoalState ← runTermElabM (match args.expr, args.copyFrom with
-      | .some expr, .none => goalStartExpr expr
+      | .some expr, .none => goalStartExpr expr (args.levels.getD #[])
      | .none, .some copyFrom =>
        (match env.find? <| copyFrom.toName with
        | .none => return .error <| errorIndex s!"Symbol not found: {copyFrom}"
--- a/Pantograph/Expr.lean
+++ b/Pantograph/Expr.lean
@ -0,0 +1,140 @@
+import Lean
+
+open Lean
+
+namespace Pantograph
+
+def _root_.Lean.Name.isAuxLemma (n : Lean.Name) : Bool := n matches .num (.str _ "_auxLemma") _
+
+/-- Unfold all lemmas created by `Lean.Meta.mkAuxLemma`. These end in `_auxLemma.nn` where `nn` is a number. -/
+def unfoldAuxLemmas (e : Expr) : CoreM Expr := do
+  Lean.Meta.deltaExpand e Lean.Name.isAuxLemma
+
+/--
+Force the instantiation of delayed metavariables even if they cannot be fully
+instantiated. This is used during resumption to provide diagnostic data about
+the current goal.
+
+Since Lean 4 does not have an `Expr` constructor corresponding to delayed
+metavariables, any delayed metavariables must be recursively handled by this
+function to ensure that nested delayed metavariables can be properly processed.
+The caveat is this recursive call will lead to infinite recursion if a loop
+between metavariable assignment exists.
+
+This function ensures any metavariable in the result is either
+1. Delayed assigned with its pending mvar not assigned in any form
+2. Not assigned (delay or not)
+ -/
+partial def instantiateDelayedMVars (eOrig: Expr) : MetaM Expr := do
+  --let padding := String.join $ List.replicate level "│ "
+  --IO.println s!"{padding}Starting {toString eOrig}"
+  let mut result ← Meta.transform (← instantiateMVars eOrig)
+    (pre := fun e => e.withApp fun f args => do
+      let .mvar mvarId := f | return .continue
+      --IO.println s!"{padding}├V {e}"
+      let mvarDecl ← mvarId.getDecl
+
+      -- This is critical to maintaining the interdependency of metavariables.
+      -- Without setting `.syntheticOpaque`, Lean's metavariable elimination
+      -- system will not make the necessary delayed assigned mvars in case of
+      -- nested mvars.
+      mvarId.setKind .syntheticOpaque
+
+      let lctx ← MonadLCtx.getLCtx
+      if mvarDecl.lctx.any (λ decl => !lctx.contains decl.fvarId) then
+        let violations := mvarDecl.lctx.decls.foldl (λ acc decl? => match decl? with
+          | .some decl => if lctx.contains decl.fvarId then acc else acc ++ [decl.fvarId.name]
+          | .none => acc) []
+        panic! s!"Local context variable violation: {violations}"
+
+      if let .some assign ← getExprMVarAssignment? mvarId then
+        --IO.println s!"{padding}├A ?{mvarId.name}"
+        assert! !(← mvarId.isDelayedAssigned)
+        return .visit (mkAppN assign args)
+      else if let some { fvars, mvarIdPending } ← getDelayedMVarAssignment? mvarId then
+        --let substTableStr := String.intercalate ", " $ Array.zipWith fvars args (λ fvar assign => s!"{fvar.fvarId!.name} := {assign}") |>.toList
+        --IO.println s!"{padding}├MD ?{mvarId.name} := ?{mvarIdPending.name} [{substTableStr}]"
+
+        if args.size < fvars.size then
+          throwError "Not enough arguments to instantiate a delay assigned mvar. This is due to bad implementations of a tactic: {args.size} < {fvars.size}. Expr: {toString e}; Origin: {toString eOrig}"
+        --if !args.isEmpty then
+          --IO.println s!"{padding}├── Arguments Begin"
+        let args ← args.mapM self
+        --if !args.isEmpty then
+          --IO.println s!"{padding}├── Arguments End"
+        if !(← mvarIdPending.isAssignedOrDelayedAssigned) then
+          --IO.println s!"{padding}├T1"
+          let result := mkAppN f args
+          return .done result
+
+        let pending ← mvarIdPending.withContext do
+          let inner ← instantiateDelayedMVars (.mvar mvarIdPending) --(level := level + 1)
+          --IO.println s!"{padding}├Pre: {inner}"
+          pure <| (← inner.abstractM fvars).instantiateRev args
+
+        -- Tail arguments
+        let result := mkAppRange pending fvars.size args.size args
+        --IO.println s!"{padding}├MD {result}"
+        return .done result
+      else
+        assert! !(← mvarId.isAssigned)
+        assert! !(← mvarId.isDelayedAssigned)
+        --if !args.isEmpty then
+        --  IO.println s!"{padding}├── Arguments Begin"
+        let args ← args.mapM self
+        --if !args.isEmpty then
+        --  IO.println s!"{padding}├── Arguments End"
+
+        --IO.println s!"{padding}├M ?{mvarId.name}"
+        return .done (mkAppN f args))
+  --IO.println s!"{padding}└Result {result}"
+  return result
+  where
+  self e := instantiateDelayedMVars e --(level := level + 1)
+
+/--
+Convert an expression to an equiavlent form with
+1. No nested delayed assigned mvars
+2. No aux lemmas
+3. No assigned mvars
+ -/
+@[export pantograph_instantiate_all_meta_m]
+def instantiateAll (e: Expr): MetaM Expr := do
+  let e ← instantiateDelayedMVars e
+  let e ← unfoldAuxLemmas e
+  return e
+
+structure DelayedMVarInvocation where
+  mvarIdPending: MVarId
+  args: Array (FVarId × (Option Expr))
+  -- Extra arguments applied to the result of this substitution
+  tail: Array Expr
+
+-- The pending mvar of any delayed assigned mvar must not be assigned in any way.
+@[export pantograph_to_delayed_mvar_invocation_meta_m]
+def toDelayedMVarInvocation (e: Expr): MetaM (Option DelayedMVarInvocation) := do
+  let .mvar mvarId := e.getAppFn | return .none
+  let .some decl ← getDelayedMVarAssignment? mvarId | return .none
+  let mvarIdPending := decl.mvarIdPending
+  let mvarDecl ← mvarIdPending.getDecl
+  -- Print the function application e. See Lean's `withOverApp`
+  let args := e.getAppArgs
+
+  assert! args.size ≥ decl.fvars.size
+  assert! !(← mvarIdPending.isAssigned)
+  assert! !(← mvarIdPending.isDelayedAssigned)
+  let fvarArgMap: HashMap FVarId Expr := HashMap.ofList $ (decl.fvars.map (·.fvarId!) |>.zip args).toList
+  let subst ← mvarDecl.lctx.foldlM (init := []) λ acc localDecl => do
+    let fvarId := localDecl.fvarId
+    let a := fvarArgMap.find? fvarId
+    return acc ++ [(fvarId, a)]
+
+  assert! decl.fvars.all (λ fvar => mvarDecl.lctx.findFVar? fvar |>.isSome)
+
+  return .some {
+    mvarIdPending,
+    args := subst.toArray,
+    tail := args.toList.drop decl.fvars.size |>.toArray,
+  }
+
+end Pantograph
--- a/Pantograph/Goal.lean
+++ b/Pantograph/Goal.lean
@ -4,6 +4,7 @@ Functions for handling metavariables
 All the functions starting with `try` resume their inner monadic state.
 -/
 import Pantograph.Protocol
+import Pantograph.Tactic
 import Lean

 def Lean.MessageLog.getErrorMessages (log : MessageLog) : MessageLog :=
@ -61,11 +62,21 @@ protected def GoalState.mctx (state: GoalState): MetavarContext :=
  state.savedState.term.meta.meta.mctx
 protected def GoalState.env (state: GoalState): Environment :=
  state.savedState.term.meta.core.env
+
+protected def GoalState.withContext (state: GoalState) (mvarId: MVarId) (m: MetaM α): MetaM α := do
+  let metaM := mvarId.withContext m
+  metaM.run' (← read) state.savedState.term.meta.meta
+
+protected def GoalState.withParentContext (state: GoalState) (m: MetaM α): MetaM α := do
+  state.withContext state.parentMVar?.get! m
+protected def GoalState.withRootContext (state: GoalState) (m: MetaM α): MetaM α := do
+  state.withContext state.root m
+
 private def GoalState.mvars (state: GoalState): SSet MVarId :=
  state.mctx.decls.foldl (init := .empty) fun acc k _ => acc.insert k
 protected def GoalState.restoreMetaM (state: GoalState): MetaM Unit :=
  state.savedState.term.meta.restore
-private def GoalState.restoreElabM (state: GoalState): Elab.TermElabM Unit :=
+protected def GoalState.restoreElabM (state: GoalState): Elab.TermElabM Unit :=
  state.savedState.term.restore
 private def GoalState.restoreTacticM (state: GoalState) (goal: MVarId): Elab.Tactic.TacticM Unit := do
  state.savedState.restore
@ -80,23 +91,69 @@ private def newMVarSet (mctxOld: @&MetavarContext) (mctxNew: @&MetavarContext):
      acc.insert mvarId
    ) SSet.empty

-/-- Inner function for executing tactic on goal state -/
-def executeTactic (state: Elab.Tactic.SavedState) (goal: MVarId) (tactic: Syntax) :
-    Elab.TermElabM (Except (Array String) Elab.Tactic.SavedState):= do
-  let tacticM (stx: Syntax):  Elab.Tactic.TacticM (Except (Array String) Elab.Tactic.SavedState) := do
-    state.restore
-    Elab.Tactic.setGoals [goal]
-    try
-      Elab.Tactic.evalTactic stx
-      if (← getThe Core.State).messages.hasErrors then
-        let messages := (← getThe Core.State).messages.getErrorMessages |>.toList.toArray
-        let errors ← (messages.map (·.data)).mapM fun md => md.toString
-        return .error errors
+protected def GoalState.focus (state: GoalState) (goalId: Nat): Option GoalState := do
+  let goal ← state.savedState.tactic.goals.get? goalId
+  return {
+    state with
+    savedState := {
+      state.savedState with
+      tactic := { goals := [goal] },
+    },
+    calcPrevRhs? := .none,
+  }
+
+/--
+Brings into scope a list of goals
+-/
+protected def GoalState.resume (state: GoalState) (goals: List MVarId): Except String GoalState :=
+  if ¬ (goals.all (λ goal => state.mvars.contains goal)) then
+    let invalid_goals := goals.filter (λ goal => ¬ state.mvars.contains goal) |>.map (·.name.toString)
+    .error s!"Goals {invalid_goals} are not in scope"
  else
-        return .ok (← MonadBacktrack.saveState)
-    catch exception =>
-      return .error #[← exception.toMessageData.toString]
-  tacticM tactic { elaborator := .anonymous } |>.run' state.tactic
+    -- Set goals to the goals that have not been assigned yet, similar to the `focus` tactic.
+    let unassigned := goals.filter (λ goal =>
+      let mctx := state.mctx
+      ¬(mctx.eAssignment.contains goal || mctx.dAssignment.contains goal))
+    .ok {
+      state with
+      savedState := {
+        term := state.savedState.term,
+        tactic := { goals := unassigned },
+      },
+      calcPrevRhs? := .none,
+    }
+/--
+Brings into scope all goals from `branch`
+-/
+protected def GoalState.continue (target: GoalState) (branch: GoalState): Except String GoalState :=
+  if !target.goals.isEmpty then
+    .error s!"Target state has unresolved goals"
+  else if target.root != branch.root then
+    .error s!"Roots of two continued goal states do not match: {target.root.name} != {branch.root.name}"
+  else
+    target.resume (goals := branch.goals)
+
+protected def GoalState.rootExpr? (goalState: GoalState): Option Expr := do
+  let expr ← goalState.mctx.eAssignment.find? goalState.root
+  let (expr, _) := instantiateMVarsCore (mctx := goalState.mctx) (e := expr)
+  if expr.hasExprMVar then
+    -- Must not assert that the goal state is empty here. We could be in a branch goal.
+    --assert! ¬goalState.goals.isEmpty
+    .none
+  else
+    assert! goalState.goals.isEmpty
+    return expr
+protected def GoalState.parentExpr? (goalState: GoalState): Option Expr := do
+  let parent ← goalState.parentMVar?
+  let expr := goalState.mctx.eAssignment.find! parent
+  let (expr, _) := instantiateMVarsCore (mctx := goalState.mctx) (e := expr)
+  return expr
+protected def GoalState.assignedExprOf? (goalState: GoalState) (mvar: MVarId): Option Expr := do
+  let expr ← goalState.mctx.eAssignment.find? mvar
+  let (expr, _) := instantiateMVarsCore (mctx := goalState.mctx) (e := expr)
+  return expr
+
+--- Tactic execution functions ---

 /-- Response for executing a tactic -/
 inductive TacticResult where
@ -111,14 +168,35 @@ inductive TacticResult where
  -- The given action cannot be executed in the state
  | invalidAction (message: String)

-/-- Execute tactic on given state -/
-protected def GoalState.tryTactic (state: GoalState) (goalId: Nat) (tactic: String):
+protected def GoalState.execute (state: GoalState) (goalId: Nat) (tacticM: Elab.Tactic.TacticM Unit):
          Elab.TermElabM TacticResult := do
  state.restoreElabM
  let goal ← match state.savedState.tactic.goals.get? goalId with
    | .some goal => pure $ goal
    | .none => return .indexError goalId
-  goal.checkNotAssigned `GoalState.tryTactic
+  goal.checkNotAssigned `GoalState.execute
+  try
+    let (_, newGoals) ← tacticM { elaborator := .anonymous } |>.run { goals := [goal] }
+    if (← getThe Core.State).messages.hasErrors then
+      let messages := (← getThe Core.State).messages.getErrorMessages |>.toList.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 tactic on given state -/
+protected def GoalState.tryTactic (state: GoalState) (goalId: Nat) (tactic: String):
+    Elab.TermElabM TacticResult := do
  let tactic ← match Parser.runParserCategory
    (env := ← MonadEnv.getEnv)
    (catName := if state.isConv then `conv else `tactic)
@ -126,22 +204,7 @@ protected def GoalState.tryTactic (state: GoalState) (goalId: Nat) (tactic: Stri
    (fileName := filename) with
    | .ok stx => pure $ stx
    | .error error => return .parseError error
-  match ← executeTactic (state := state.savedState) (goal := goal) (tactic := tactic) with
-  | .error errors =>
-    return .failure errors
-  | .ok nextSavedState =>
-    -- Assert that the definition of metavariables are the same
-    let nextMCtx := nextSavedState.term.meta.meta.mctx
-    let prevMCtx := state.mctx
-    -- Generate a list of mvarIds that exist in the parent state; Also test the
-    -- assertion that the types have not changed on any mvars.
-    return .success {
-      state with
-      savedState := nextSavedState
-      newMVars := newMVarSet prevMCtx nextMCtx,
-      parentMVar? := .some goal,
-      calcPrevRhs? := .none,
-    }
+  state.execute goalId $ Elab.Tactic.evalTactic tactic

 /-- Assumes elabM has already been restored. Assumes expr has already typechecked -/
 protected def GoalState.assign (state: GoalState) (goal: MVarId) (expr: Expr):
@ -168,7 +231,7 @@ protected def GoalState.assign (state: GoalState) (goal: MVarId) (expr: Expr):
    -- Generate a list of mvarIds that exist in the parent state; Also test the
    -- assertion that the types have not changed on any mvars.
    let newMVars := newMVarSet prevMCtx nextMCtx
-    let nextGoals ← newMVars.toList.filterM (λ mvar => do pure !(← mvar.isAssigned))
+    let nextGoals ← newMVars.toList.filterM (not <$> ·.isAssigned)
    return .success {
      root := state.root,
      savedState := {
@ -188,6 +251,7 @@ protected def GoalState.tryAssign (state: GoalState) (goalId: Nat) (expr: String
  let goal ← match state.savedState.tactic.goals.get? goalId with
    | .some goal => pure goal
    | .none => return .indexError goalId
+  goal.checkNotAssigned `GoalState.tryAssign
  let expr ← match Parser.runParserCategory
    (env := state.env)
    (catName := `term)
@ -211,6 +275,7 @@ protected def GoalState.tryHave (state: GoalState) (goalId: Nat) (binderName: St
  let goal ← match state.savedState.tactic.goals.get? goalId with
    | .some goal => pure goal
    | .none => return .indexError goalId
+  goal.checkNotAssigned `GoalState.tryHave
  let type ← match Parser.runParserCategory
    (env := state.env)
    (catName := `term)
@ -260,6 +325,7 @@ protected def GoalState.tryLet (state: GoalState) (goalId: Nat) (binderName: Str
  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)
@ -305,6 +371,7 @@ protected def GoalState.conv (state: GoalState) (goalId: Nat):
  let goal ← match state.savedState.tactic.goals.get? goalId with
    | .some goal => pure goal
    | .none => return .indexError goalId
+  goal.checkNotAssigned `GoalState.conv
  let tacticM :  Elab.Tactic.TacticM (Elab.Tactic.SavedState × MVarId) := do
    state.restoreTacticM goal

@ -388,6 +455,7 @@ protected def GoalState.tryCalc (state: GoalState) (goalId: Nat) (pred: String):
    (fileName := filename) with
    | .ok syn => pure syn
    | .error error => return .parseError error
+  goal.checkNotAssigned `GoalState.tryCalc
  let calcPrevRhs? := state.calcPrevRhsOf? goalId
  let target ← instantiateMVars (← goal.getDecl).type
  let tag := (← goal.getDecl).userName
@ -447,66 +515,27 @@ protected def GoalState.tryCalc (state: GoalState) (goalId: Nat) (pred: String):
    return .failure #[← exception.toMessageData.toString]


-protected def GoalState.focus (state: GoalState) (goalId: Nat): Option GoalState := do
-  let goal ← state.savedState.tactic.goals.get? goalId
-  return {
-    state with
-    savedState := {
-      state.savedState with
-      tactic := { goals := [goal] },
-    },
-    calcPrevRhs? := .none,
-  }
-
-/--
-Brings into scope a list of goals
-/
-protected def GoalState.resume (state: GoalState) (goals: List MVarId): Except String GoalState :=
-  if ¬ (goals.all (λ goal => state.mvars.contains goal)) then
-    .error s!"Goals not in scope"
-  else
-    -- Set goals to the goals that have not been assigned yet, similar to the `focus` tactic.
-    let unassigned := goals.filter (λ goal =>
-      let mctx := state.mctx
-      ¬(mctx.eAssignment.contains goal || mctx.dAssignment.contains goal))
-    .ok {
-      state with
-      savedState := {
-        term := state.savedState.term,
-        tactic := { goals := unassigned },
-      },
-      calcPrevRhs? := .none,
-    }
-/--
-Brings into scope all goals from `branch`
-/
-protected def GoalState.continue (target: GoalState) (branch: GoalState): Except String GoalState :=
-  if !target.goals.isEmpty then
-    .error s!"Target state has unresolved goals"
-  else if target.root != branch.root then
-    .error s!"Roots of two continued goal states do not match: {target.root.name} != {branch.root.name}"
-  else
-    target.resume (goals := branch.goals)
-
-protected def GoalState.rootExpr? (goalState: GoalState): Option Expr := do
-  let expr ← goalState.mctx.eAssignment.find? goalState.root
-  let (expr, _) := instantiateMVarsCore (mctx := goalState.mctx) (e := expr)
-  if expr.hasMVar then
-    -- Must not assert that the goal state is empty here. We could be in a branch goal.
-    --assert! ¬goalState.goals.isEmpty
-    .none
-  else
-    assert! goalState.goals.isEmpty
-    return expr
-protected def GoalState.parentExpr? (goalState: GoalState): Option Expr := do
-  let parent ← goalState.parentMVar?
-  let expr := goalState.mctx.eAssignment.find! parent
-  let (expr, _) := instantiateMVarsCore (mctx := goalState.mctx) (e := expr)
-  return expr
-protected def GoalState.assignedExprOf? (goalState: GoalState) (mvar: MVarId): Option Expr := do
-  let expr ← goalState.mctx.eAssignment.find? mvar
-  let (expr, _) := instantiateMVarsCore (mctx := goalState.mctx) (e := expr)
-  return expr
-
+protected def GoalState.tryMotivatedApply (state: GoalState) (goalId: Nat) (recursor: String):
+      Elab.TermElabM TacticResult := do
+  state.restoreElabM
+  let recursor ← match Parser.runParserCategory
+    (env := state.env)
+    (catName := `term)
+    (input := recursor)
+    (fileName := filename) with
+    | .ok syn => pure syn
+    | .error error => return .parseError error
+  state.execute goalId (tacticM := Tactic.motivatedApply recursor)
+protected def GoalState.tryNoConfuse (state: GoalState) (goalId: Nat) (eq: String):
+      Elab.TermElabM TacticResult := do
+  state.restoreElabM
+  let recursor ← match Parser.runParserCategory
+    (env := state.env)
+    (catName := `term)
+    (input := eq)
+    (fileName := filename) with
+    | .ok syn => pure syn
+    | .error error => return .parseError error
+  state.execute goalId (tacticM := Tactic.noConfuse recursor)

 end Pantograph
--- a/Pantograph/Library.lean
+++ b/Pantograph/Library.lean
@ -34,16 +34,16 @@ def setOptionFromString' (opts : Options) (entry : String) : ExceptT String IO O

 end Lean

+open Lean
+
 namespace Pantograph

-def defaultTermElabMContext: Lean.Elab.Term.Context := {
-    autoBoundImplicit := true,
-    declName? := some "_pantograph".toName,
+def defaultTermElabMContext: Elab.Term.Context := {
    errToSorry := false
  }
-def runMetaM { α } (metaM: Lean.MetaM α): Lean.CoreM α :=
+def runMetaM { α } (metaM: MetaM α): CoreM α :=
  metaM.run'
-def runTermElabM { α } (termElabM: Lean.Elab.TermElabM α): Lean.CoreM α :=
+def runTermElabM { α } (termElabM: Elab.TermElabM α): CoreM α :=
  termElabM.run' (ctx := defaultTermElabMContext) |>.run'

 def errorI (type desc: String): Protocol.InteractionError := { error := type, desc := desc }
@ -56,13 +56,13 @@ unsafe def initSearch (sp: String): IO Unit := do

 /-- Creates a Core.Context object needed to run all monads -/
@[export pantograph_create_core_context]
-def createCoreContext (options: Array String): IO Lean.Core.Context := do
-  let options? ← options.foldlM Lean.setOptionFromString' Lean.Options.empty |>.run
+def createCoreContext (options: Array String): IO Core.Context := do
+  let options? ← options.foldlM setOptionFromString' Options.empty |>.run
  let options ← match options? with
    | .ok options => pure options
    | .error e => throw $ IO.userError s!"Options cannot be parsed: {e}"
  return {
-    currNamespace := Lean.Name.str .anonymous "Aniva"
+    currNamespace := Name.str .anonymous "Aniva"
    openDecls := [],     -- No 'open' directives needed
    fileName := "<Pantograph>",
    fileMap := { source := "", positions := #[0] },
@ -71,41 +71,45 @@ def createCoreContext (options: Array String): IO Lean.Core.Context := do

 /-- Creates a Core.State object needed to run all monads -/
@[export pantograph_create_core_state]
-def createCoreState (imports: Array String): IO Lean.Core.State := do
+def createCoreState (imports: Array String): IO Core.State := do
  let env ← Lean.importModules
    (imports := imports.map (λ str => { module := str.toName, runtimeOnly := false }))
    (opts := {})
    (trustLevel := 1)
  return { env := env }

+@[export pantograph_create_meta_context]
+def createMetaContext: IO Lean.Meta.Context := do
+  return {}
+
@[export pantograph_env_catalog_m]
-def envCatalog: Lean.CoreM Protocol.EnvCatalogResult :=
+def envCatalog: CoreM Protocol.EnvCatalogResult :=
  Environment.catalog ({}: Protocol.EnvCatalog)

@[export pantograph_env_inspect_m]
 def envInspect (name: String) (value: Bool) (dependency: Bool) (options: @&Protocol.Options):
-    Lean.CoreM (Protocol.CR Protocol.EnvInspectResult) :=
+    CoreM (Protocol.CR Protocol.EnvInspectResult) :=
  Environment.inspect ({
    name, value? := .some value, dependency?:= .some dependency
  }: Protocol.EnvInspect) options

@[export pantograph_env_add_m]
 def envAdd (name: String) (type: String) (value: String) (isTheorem: Bool):
-    Lean.CoreM (Protocol.CR Protocol.EnvAddResult) :=
+    CoreM (Protocol.CR Protocol.EnvAddResult) :=
  Environment.addDecl { name, type, value, isTheorem }

-def parseElabType (type: String): Lean.Elab.TermElabM (Protocol.CR Lean.Expr) := do
-  let env ← Lean.MonadEnv.getEnv
+def parseElabType (type: String): Elab.TermElabM (Protocol.CR Expr) := do
+  let env ← MonadEnv.getEnv
  let syn ← match parseTerm env type with
    | .error str => return .error $ errorI "parsing" str
    | .ok syn => pure syn
  match ← elabType syn with
  | .error str => return .error $ errorI "elab" str
-  | .ok expr => return .ok (← Lean.instantiateMVars expr)
+  | .ok expr => return .ok (← instantiateMVars expr)

 /-- This must be a TermElabM since the parsed expr contains extra information -/
-def parseElabExpr (expr: String) (expectedType?: Option String := .none): Lean.Elab.TermElabM (Protocol.CR Lean.Expr) := do
-  let env ← Lean.MonadEnv.getEnv
+def parseElabExpr (expr: String) (expectedType?: Option String := .none): Elab.TermElabM (Protocol.CR Expr) := do
+  let env ← MonadEnv.getEnv
  let expectedType? ← match ← expectedType?.mapM parseElabType with
    | .none => pure $ .none
    | .some (.ok t) => pure $ .some t
@ -115,17 +119,17 @@ def parseElabExpr (expr: String) (expectedType?: Option String := .none): Lean.E
    | .ok syn => pure syn
  match ← elabTerm syn expectedType? with
  | .error str => return .error $ errorI "elab" str
-  | .ok expr => return .ok (← Lean.instantiateMVars expr)
+  | .ok expr => return .ok (← instantiateMVars expr)

@[export pantograph_expr_echo_m]
-def exprEcho (expr: String) (expectedType?: Option String := .none) (options: @&Protocol.Options):
-    Lean.CoreM (Protocol.CR Protocol.ExprEchoResult) :=
-  runTermElabM do
+def exprEcho (expr: String) (expectedType?: Option String := .none) (levels: Array String := #[])  (options: @&Protocol.Options := {}):
+    CoreM (Protocol.CR Protocol.ExprEchoResult) :=
+  runTermElabM $ Elab.Term.withLevelNames (levels.toList.map (·.toName)) do
    let expr ← match ← parseElabExpr expr expectedType? with
      | .error e => return .error e
      | .ok expr => pure expr
    try
-      let type ← unfoldAuxLemmas (← Lean.Meta.inferType expr)
+      let type ← unfoldAuxLemmas (← Meta.inferType expr)
      return .ok {
          type := (← serializeExpression options type),
          expr := (← serializeExpression options expr)
@ -134,44 +138,13 @@ def exprEcho (expr: String) (expectedType?: Option String := .none) (options: @&
      return .error $ errorI "typing" (← exception.toMessageData.toString)

@[export pantograph_goal_start_expr_m]
-def goalStartExpr (expr: String): Lean.CoreM (Protocol.CR GoalState) :=
-  runTermElabM do
+def goalStartExpr (expr: String) (levels: Array String): CoreM (Protocol.CR GoalState) :=
+  runTermElabM $ Elab.Term.withLevelNames (levels.toList.map (·.toName)) do
    let expr ← match ← parseElabType expr with
      | .error e => return .error e
      | .ok expr => pure $ expr
    return .ok $ ← GoalState.create expr

-@[export pantograph_goal_tactic_m]
-def goalTactic (state: GoalState) (goalId: Nat) (tactic: String): Lean.CoreM TacticResult :=
-  runTermElabM <| state.tryTactic goalId tactic
-
-@[export pantograph_goal_assign_m]
-def goalAssign (state: GoalState) (goalId: Nat) (expr: String): Lean.CoreM TacticResult :=
-  runTermElabM <| state.tryAssign goalId expr
-
-@[export pantograph_goal_have_m]
-def goalHave (state: GoalState) (goalId: Nat) (binderName: String) (type: String): Lean.CoreM TacticResult :=
-  runTermElabM <| state.tryHave goalId binderName type
-@[export pantograph_goal_let_m]
-def goalLet (state: GoalState) (goalId: Nat) (binderName: String) (type: String): Lean.CoreM TacticResult :=
-  runTermElabM <| state.tryLet goalId binderName type
-
-@[export pantograph_goal_conv_m]
-def goalConv (state: GoalState) (goalId: Nat): Lean.CoreM TacticResult :=
-  runTermElabM <| state.conv goalId
-
-@[export pantograph_goal_conv_exit_m]
-def goalConvExit (state: GoalState): Lean.CoreM TacticResult :=
-  runTermElabM <| state.convExit
-
-@[export pantograph_goal_calc_m]
-def goalCalc (state: GoalState) (goalId: Nat) (pred: String): Lean.CoreM TacticResult :=
-  runTermElabM <| state.tryCalc goalId pred
-
-@[export pantograph_goal_focus]
-def goalFocus (state: GoalState) (goalId: Nat): Option GoalState :=
-  state.focus goalId
-
@[export pantograph_goal_resume]
 def goalResume (target: GoalState) (goals: Array String): Except String GoalState :=
  target.resume (goals.map (λ n => { name := n.toName }) |>.toList)
@ -181,19 +154,69 @@ def goalContinue (target: GoalState) (branch: GoalState): Except String GoalStat
  target.continue branch

@[export pantograph_goal_serialize_m]
-def goalSerialize (state: GoalState) (options: @&Protocol.Options): Lean.CoreM (Array Protocol.Goal) :=
+def goalSerialize (state: GoalState) (options: @&Protocol.Options): CoreM (Array Protocol.Goal) :=
  runMetaM <| state.serializeGoals (parent := .none) options

@[export pantograph_goal_print_m]
-def goalPrint (state: GoalState) (options: @&Protocol.Options): Lean.CoreM Protocol.GoalPrintResult :=
+def goalPrint (state: GoalState) (options: @&Protocol.Options): CoreM Protocol.GoalPrintResult :=
  runMetaM do
    state.restoreMetaM
    return {
-      root? := ← state.rootExpr?.mapM (λ expr => do
-        serializeExpression options (← unfoldAuxLemmas expr)),
-      parent? := ← state.parentExpr?.mapM (λ expr => do
-        serializeExpression options (← unfoldAuxLemmas expr)),
+      root? := ← state.rootExpr?.mapM (λ expr =>
+        state.withRootContext do
+          serializeExpression options (← instantiateAll expr)),
+      parent? := ← state.parentExpr?.mapM (λ expr =>
+        state.withParentContext do
+          serializeExpression options (← instantiateAll expr)),
    }
+@[export pantograph_goal_diag_m]
+def goalDiag (state: GoalState) (diagOptions: Protocol.GoalDiag) : CoreM String :=
+  runMetaM $ state.diag diagOptions
+
+@[export pantograph_goal_tactic_m]
+def goalTactic (state: GoalState) (goalId: Nat) (tactic: String): CoreM TacticResult :=
+  runTermElabM <| state.tryTactic goalId tactic
+@[export pantograph_goal_assign_m]
+def goalAssign (state: GoalState) (goalId: Nat) (expr: String): CoreM TacticResult :=
+  runTermElabM <| state.tryAssign goalId expr
+@[export pantograph_goal_have_m]
+def goalHave (state: GoalState) (goalId: Nat) (binderName: String) (type: String): CoreM TacticResult :=
+  runTermElabM <| state.tryHave goalId binderName type
+@[export pantograph_goal_let_m]
+def goalLet (state: GoalState) (goalId: Nat) (binderName: String) (type: String): CoreM TacticResult :=
+  runTermElabM <| state.tryLet goalId binderName type
+@[export pantograph_goal_conv_m]
+def goalConv (state: GoalState) (goalId: Nat): CoreM TacticResult :=
+  runTermElabM <| state.conv goalId
+@[export pantograph_goal_conv_exit_m]
+def goalConvExit (state: GoalState): CoreM TacticResult :=
+  runTermElabM <| state.convExit
+@[export pantograph_goal_calc_m]
+def goalCalc (state: GoalState) (goalId: Nat) (pred: String): CoreM TacticResult :=
+  runTermElabM <| state.tryCalc goalId pred
+@[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
+
+inductive TacticExecute where
+  | congruenceArg
+  | congruenceFun
+  | congruence
+@[export pantograph_goal_tactic_execute_m]
+def goalTacticExecute (state: GoalState) (goalId: Nat) (tacticExecute: TacticExecute): CoreM TacticResult :=
+  runTermElabM do
+    state.restoreElabM
+    state.execute goalId $ match tacticExecute with
+      | .congruenceArg => Tactic.congruenceArg
+      | .congruenceFun => Tactic.congruenceFun
+      | .congruence => Tactic.congruence
+


 end Pantograph
--- a/Pantograph/Protocol.lean
+++ b/Pantograph/Protocol.lean
@ -101,6 +101,8 @@ structure StatResult where
 structure ExprEcho where
  expr: String
  type?: Option String
+  -- universe levels
+  levels: Option (Array String) := .none
  deriving Lean.FromJson
 structure ExprEchoResult where
  expr: Expression
@ -193,11 +195,12 @@ structure OptionsSetResult where
  deriving Lean.ToJson
 structure OptionsPrint where
  deriving Lean.FromJson
-abbrev OptionsPrintResult := Options

 structure GoalStart where
  -- Only one of the fields below may be populated.
  expr: Option String     -- Directly parse in an expression
+  -- universe levels
+  levels: Option (Array String) := .none
  copyFrom: Option String -- Copy the type from a theorem in the environment
  deriving Lean.FromJson
 structure GoalStartResult where
@ -274,6 +277,7 @@ structure GoalDiag where
  -- Print all mvars
  printAll: Bool := false
  instantiate: Bool := true
+  printSexp: Bool := false


 /-- Executes the Lean compiler on a single file -/
--- a/Pantograph/Serial.lean
+++ b/Pantograph/Serial.lean
@ -1,7 +1,10 @@
 /-
-All serialisation functions
+All serialisation functions;
+This replicates the behaviour of `Scope`s in `Lean/Elab/Command.lean` without
+using `Scope`s.
 -/
 import Lean
+import Pantograph.Expr

 import Pantograph.Protocol
 import Pantograph.Goal
@ -10,13 +13,8 @@ open Lean

 -- Symbol processing functions --

-def Lean.Name.isAuxLemma (n : Lean.Name) : Bool := n matches .num (.str _ "_auxLemma") _
-
 namespace Pantograph

-/-- Unfold all lemmas created by `Lean.Meta.mkAuxLemma`. These end in `_auxLemma.nn` where `nn` is a number. -/
-def unfoldAuxLemmas (e : Expr) : CoreM Expr := do
-  Lean.Meta.deltaExpand e Lean.Name.isAuxLemma

 --- Input Functions ---

@ -84,6 +82,7 @@ partial def serializeSortLevel (level: Level) (sanitize: Bool): String :=
  | _, .zero => s!"{k}"
  | _, _ => s!"(+ {u_str} {k})"

+
 /--
 Completely serializes an expression tree. Json not used due to compactness

@ -92,7 +91,28 @@ A `_` symbol in the AST indicates automatic deductions not present in the origin
 partial def serializeExpressionSexp (expr: Expr) (sanitize: Bool := true): MetaM String := do
  self expr
  where
-  self (e: Expr): MetaM String :=
+  delayedMVarToSexp (e: Expr): MetaM (Option String) := do
+    let .some invocation ← toDelayedMVarInvocation e | return .none
+    let callee ← self $ .mvar invocation.mvarIdPending
+    let sites ← invocation.args.mapM (λ (fvarId, arg) => do
+        let arg := match arg with
+          | .some arg => arg
+          | .none => .fvar fvarId
+        self arg
+      )
+    let tailArgs ← invocation.tail.mapM self
+
+    let sites := " ".intercalate sites.toList
+    let result := if tailArgs.isEmpty then
+        s!"(:subst {callee} {sites})"
+      else
+        let tailArgs := " ".intercalate tailArgs.toList
+        s!"((:subst {callee} {sites}) {tailArgs})"
+    return .some result
+
+  self (e: Expr): MetaM String := do
+    if let .some result ← delayedMVarToSexp e then
+      return result
    match e with
    | .bvar deBruijnIndex =>
      -- This is very common so the index alone is shown. Literals are handled below.
@ -102,9 +122,10 @@ partial def serializeExpressionSexp (expr: Expr) (sanitize: Bool := true): MetaM
    | .fvar fvarId =>
      let name := ofName fvarId.name
      pure s!"(:fv {name})"
-    | .mvar mvarId =>
+    | .mvar mvarId => do
+        let pref := if ← mvarId.isDelayedAssigned then "mvd" else "mv"
        let name := ofName mvarId.name
-      pure s!"(:mv {name})"
+        pure s!"(:{pref} {name})"
    | .sort level =>
      let level := serializeSortLevel level sanitize
      pure s!"(:sort {level})"
@ -207,7 +228,7 @@ def serializeGoal (options: @&Protocol.Options) (goal: MVarId) (mvarDecl: Metava
      match localDecl with
      | .cdecl _ fvarId userName type _ _ =>
        let userName := userName.simpMacroScopes
-        let type ← instantiateMVars type
+        let type ← instantiate type
        return {
          name := ofName fvarId.name,
          userName:= ofName userName,
@ -216,9 +237,9 @@ def serializeGoal (options: @&Protocol.Options) (goal: MVarId) (mvarDecl: Metava
        }
      | .ldecl _ fvarId userName type val _ _ => do
        let userName := userName.simpMacroScopes
-        let type ← instantiateMVars type
+        let type ← instantiate type
        let value? ← if showLetValues then
-          let val ← instantiateMVars val
+          let val ← instantiate val
          pure $ .some (← serializeExpression options val)
        else
          pure $ .none
@ -245,10 +266,11 @@ def serializeGoal (options: @&Protocol.Options) (goal: MVarId) (mvarDecl: Metava
      name := ofName goal.name,
      userName? := if mvarDecl.userName == .anonymous then .none else .some (ofName mvarDecl.userName),
      isConversion := isLHSGoal? mvarDecl.type |>.isSome,
-      target := (← serializeExpression options (← instantiateMVars mvarDecl.type)),
+      target := (← serializeExpression options (← instantiate mvarDecl.type)),
      vars := vars.reverse.toArray
    }
  where
+  instantiate := instantiateAll
  ofName (n: Name) := serializeName n (sanitize := false)

 protected def GoalState.serializeGoals
@ -267,51 +289,62 @@ protected def GoalState.serializeGoals
    | .none => throwError s!"Metavariable does not exist in context {goal.name}"

 /-- Print the metavariables in a readable format -/
-protected def GoalState.diag (goalState: GoalState) (options: Protocol.GoalDiag := {}): MetaM Unit := do
+protected def GoalState.diag (goalState: GoalState) (options: Protocol.GoalDiag := {}): MetaM String := do
  goalState.restoreMetaM
  let savedState := goalState.savedState
  let goals := savedState.tactic.goals
  let mctx ← getMCtx
  let root := goalState.root
  -- Print the root
-  match mctx.decls.find? root with
+  let result: String ← match mctx.decls.find? root with
    | .some decl => printMVar ">" root decl
-  | .none => IO.println s!">{root.name}: ??"
-  goals.forM (fun mvarId => do
-    if mvarId != root then
+    | .none => pure s!">{root.name}: ??"
+  let resultGoals ← goals.filter (· != root) |>.mapM (fun mvarId =>
    match mctx.decls.find? mvarId with
    | .some decl => printMVar "⊢" mvarId decl
-      | .none => IO.println s!"⊢{mvarId.name}: ??"
+    | .none => pure s!"⊢{mvarId.name}: ??"
  )
  let goals := goals.toSSet
-  mctx.decls.forM (fun mvarId decl => do
-    if goals.contains mvarId || mvarId == root then
-      pure ()
-    -- Print the remainig ones that users don't see in Lean
-    else if options.printAll then
+  let resultOthers ← mctx.decls.toList.filter (λ (mvarId, _) =>
+      !(goals.contains mvarId || mvarId == root) && options.printAll)
+  |>.mapM (fun (mvarId, decl) => do
      let pref := if goalState.newMVars.contains mvarId then "~" else " "
      printMVar pref mvarId decl
-    else
-      pure ()
-      --IO.println s!" {mvarId.name}{userNameToString decl.userName}"
  )
+  pure $ result ++ (resultGoals.map (· ++ "\n") |> String.join) ++ (resultOthers.map (· ++ "\n") |> String.join)
  where
-    printMVar (pref: String) (mvarId: MVarId) (decl: MetavarDecl): MetaM Unit := do
+    printMVar (pref: String) (mvarId: MVarId) (decl: MetavarDecl): MetaM String := mvarId.withContext do
+      let resultFVars: List String ←
        if options.printContext then
-        decl.lctx.fvarIdToDecl.forM printFVar
+          decl.lctx.fvarIdToDecl.toList.mapM (λ (fvarId, decl) =>
+            do pure $ (← printFVar fvarId decl) ++ "\n")
+        else
+          pure []
      let type ← if options.instantiate
-        then instantiateMVars decl.type
+        then instantiateAll decl.type
        else pure $ decl.type
-      let type_sexp ← serializeExpressionSexp type (sanitize := false)
-      IO.println s!"{pref}{mvarId.name}{userNameToString decl.userName}: {← Meta.ppExpr decl.type} {type_sexp}"
+      let type_sexp ← if options.printSexp then
+          let sexp ← serializeExpressionSexp type (sanitize := false)
+          pure <| " " ++ sexp
+        else
+          pure ""
+      let resultMain: String := s!"{pref}{mvarId.name}{userNameToString decl.userName}: {← Meta.ppExpr decl.type}{type_sexp}"
+      let resultValue: String ←
        if options.printValue then
-        if let Option.some value := (← getMCtx).eAssignment.find? mvarId then
+          if let .some value ← getExprMVarAssignment? mvarId then
            let value ← if options.instantiate
-            then instantiateMVars value
+              then instantiateAll value
              else pure $ value
-          IO.println s!" := {← Meta.ppExpr value}"
-    printFVar (fvarId: FVarId) (decl: LocalDecl): MetaM Unit := do
-      IO.println s!" | {fvarId.name}{userNameToString decl.userName}: {← Meta.ppExpr decl.type}"
+            pure s!"\n := {← Meta.ppExpr value}"
+          else if let .some { mvarIdPending, .. } ← getDelayedMVarAssignment? mvarId then
+            pure s!"\n := $ {mvarIdPending.name}"
+          else
+            pure ""
+        else
+          pure ""
+      pure $ (String.join resultFVars) ++ resultMain ++ resultValue
+    printFVar (fvarId: FVarId) (decl: LocalDecl): MetaM String := do
+      pure s!" | {fvarId.name}{userNameToString decl.userName}: {← Meta.ppExpr decl.type}"
    userNameToString : Name → String
      | .anonymous => ""
      | other => s!"[{other}]"
--- a/Pantograph/Tactic.lean
+++ b/Pantograph/Tactic.lean
@ -0,0 +1,4 @@
+
+import Pantograph.Tactic.Congruence
+import Pantograph.Tactic.MotivatedApply
+import Pantograph.Tactic.NoConfuse
--- a/Pantograph/Tactic/Congruence.lean
+++ b/Pantograph/Tactic/Congruence.lean
@ -0,0 +1,85 @@
+import Lean
+
+open Lean
+
+namespace Pantograph.Tactic
+
+def congruenceArg: Elab.Tactic.TacticM Unit := do
+  let goal ← Elab.Tactic.getMainGoal
+  let .some (β, _, _) := (← goal.getType).eq? | throwError "Goal is not an Eq"
+  let userName := (← goal.getDecl).userName
+
+  let nextGoals ← goal.withContext do
+    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₂)) (← goal.getType)
+    let conduit ← Meta.mkFreshExprMVar conduitType
+      .synthetic (userName := userName ++ `conduit)
+    goal.assign $ ← Meta.mkEqMP conduit (← Meta.mkCongrArg f h)
+    return [α, a₁, a₂, f,  h, conduit]
+  Elab.Tactic.setGoals <| nextGoals.map (·.mvarId!)
+
+def congruenceFun: Elab.Tactic.TacticM Unit := do
+  let goal ← Elab.Tactic.getMainGoal
+  let .some (β, _, _) := (← goal.getType).eq? | throwError "Goal is not an Eq"
+  let userName := (← goal.getDecl).userName
+
+  let nextGoals ← 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 h ← Meta.mkFreshExprMVar (.some $ ← Meta.mkEq f₁ f₂)
+      .synthetic (userName := userName ++ `h)
+    let conduitType ← Meta.mkEq (← Meta.mkEq (.app f₁ a) (.app f₂ a)) (← goal.getType)
+    let conduit ← Meta.mkFreshExprMVar conduitType
+      .synthetic (userName := userName ++ `conduit)
+    goal.assign $ ← Meta.mkEqMP conduit (← Meta.mkCongrFun h a)
+    return [α, f₁, f₂, h, a, conduit]
+  Elab.Tactic.setGoals <| nextGoals.map (·.mvarId!)
+
+def congruence: Elab.Tactic.TacticM Unit := do
+  let goal ← Elab.Tactic.getMainGoal
+  let .some (β, _, _) := (← goal.getType).eq? | throwError "Goal is not an Eq"
+  let userName := (← goal.getDecl).userName
+
+  let nextGoals ← 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
--- a/Pantograph/Tactic/MotivatedApply.lean
+++ b/Pantograph/Tactic/MotivatedApply.lean
@ -0,0 +1,105 @@
+import Lean
+
+open Lean
+
+namespace Pantograph.Tactic
+
+def getForallArgsBody: Expr → List Expr × Expr
+  | .forallE _ d b _ =>
+    let (innerArgs, innerBody) := getForallArgsBody b
+    (d :: innerArgs, innerBody)
+  | e => ([], e)
+
+def replaceForallBody: Expr → Expr → Expr
+  | .forallE param domain body binderInfo, target =>
+    let body := replaceForallBody body target
+    .forallE param domain body binderInfo
+  | _, target => target
+
+structure RecursorWithMotive where
+  args: List Expr
+  body: Expr
+
+  -- .bvar index for the motive and major from the body
+  iMotive: Nat
+
+namespace RecursorWithMotive
+
+protected def nArgs (info: RecursorWithMotive): Nat := info.args.length
+
+protected def getMotiveType (info: RecursorWithMotive): Expr :=
+  let level := info.nArgs - info.iMotive - 1
+  let a := info.args.get! level
+  a
+
+protected def surrogateMotiveType (info: RecursorWithMotive) (mvars: Array Expr) (resultant: Expr): MetaM Expr := do
+  let motiveType := Expr.instantiateRev info.getMotiveType mvars
+  let resultantType ← Meta.inferType resultant
+  return replaceForallBody motiveType resultantType
+
+protected def conduitType (info: RecursorWithMotive) (mvars: Array Expr) (resultant: Expr): MetaM Expr := do
+  let motiveCall := Expr.instantiateRev info.body mvars
+  Meta.mkEq motiveCall resultant
+
+end RecursorWithMotive
+
+def getRecursorInformation (recursorType: Expr): Option RecursorWithMotive := do
+  let (args, body) := getForallArgsBody recursorType
+  if ¬ body.isApp then
+    .none
+  let iMotive ← match body.getAppFn with
+    | .bvar iMotive => pure iMotive
+    | _ => .none
+  return {
+    args,
+    body,
+    iMotive,
+  }
+
+def collectMotiveArguments (forallBody: Expr): SSet Nat :=
+  match forallBody with
+  | .app (.bvar i) _ => SSet.empty.insert i
+  | _ => SSet.empty
+
+/-- Applies a symbol of the type `∀ (motive: α → Sort u) (a: α)..., (motive α)` -/
+def motivatedApply: Elab.Tactic.Tactic := λ stx => do
+  let goal ← Elab.Tactic.getMainGoal
+  let nextGoals: List MVarId ← goal.withContext do
+    let recursor ← Elab.Term.elabTerm (stx := stx) .none
+    let recursorType ← Meta.inferType recursor
+
+    let resultant ← goal.getType
+
+    let info ← match getRecursorInformation recursorType with
+      | .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
+      if i ≥ info.nArgs then
+        return prev
+      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 conduitType ← info.conduitType newMVars resultant
+    let goalConduit ← Meta.mkFreshExprMVar conduitType .natural (userName := `conduit)
+    goal.assign $ ← Meta.mkEqMP goalConduit (mkAppN recursor newMVars)
+    newMVars := newMVars ++ [goalConduit]
+
+    let nextGoals := newMVars.toList.map (·.mvarId!)
+    pure nextGoals
+  Elab.Tactic.setGoals nextGoals
+
+end Pantograph.Tactic
--- a/Pantograph/Tactic/NoConfuse.lean
+++ b/Pantograph/Tactic/NoConfuse.lean
@ -0,0 +1,18 @@
+import Lean
+
+open Lean
+
+namespace Pantograph.Tactic
+
+def noConfuse: Elab.Tactic.Tactic := λ stx => do
+  let goal ← Elab.Tactic.getMainGoal
+  goal.withContext do
+    let absurd ← Elab.Term.elabTerm (stx := stx) .none
+    let noConfusion ← Meta.mkNoConfusion (target := ← goal.getType) (h := absurd)
+
+    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
--- a/README.md
+++ b/README.md
@ -82,8 +82,8 @@ where the application of `assumption` should lead to a failure.
 See `Pantograph/Protocol.lean` for a description of the parameters and return values in JSON.
 * `reset`: Delete all cached expressions and proof trees
 * `stat`: Display resource usage
-* `expr.echo {"expr": <expr>, "type": <optional expected type>}`: Determine the
-  type of an expression and format it
+* `expr.echo {"expr": <expr>, "type": <optional expected type>, ["levels": [<levels>]]}`: Determine the
+  type of an expression and format it.
 * `env.catalog`: Display a list of all safe Lean symbols in the current environment
 * `env.inspect {"name": <name>, "value": <bool>}`: Show the type and package of a
  given symbol; If value flag is set, the value is printed or hidden. By default
@ -91,7 +91,7 @@ See `Pantograph/Protocol.lean` for a description of the parameters and return va
 * `options.set { key: value, ... }`: Set one or more options (not Lean options; those
  have to be set via command line arguments.), for options, see `Pantograph/Protocol.lean`
 * `options.print`: Display the current set of options
-* `goal.start {["name": <name>], ["expr": <expr>], ["copyFrom": <symbol>]}`:
+* `goal.start {["name": <name>], ["expr": <expr>], ["levels": [<levels>]], ["copyFrom": <symbol>]}`:
  Start a new proof from a given expression or symbol
 * `goal.tactic {"stateId": <id>, "goalId": <id>, ...}`: Execute a tactic string on a
  given goal. The tactic is supplied as additional key-value pairs in one of the following formats:
--- a/Test/Common.lean
+++ b/Test/Common.lean
@ -10,11 +10,9 @@ namespace Pantograph

 -- Auxiliary functions
 namespace Protocol
-/-- Set internal names to "" -/
-def Goal.devolatilize (goal: Goal): Goal :=
+def Goal.devolatilizeVars (goal: Goal): Goal :=
  {
    goal with
-    name := "",
    vars := goal.vars.map removeInternalAux,
  }
  where removeInternalAux (v: Variable): Variable :=
@ -22,6 +20,14 @@ def Goal.devolatilize (goal: Goal): Goal :=
      v with
      name := ""
    }
+/-- Set internal names to "" -/
+def Goal.devolatilize (goal: Goal): Goal :=
+  {
+    goal.devolatilizeVars with
+    name := "",
+  }
+
+deriving instance DecidableEq, Repr for Name
 deriving instance DecidableEq, Repr for Expression
 deriving instance DecidableEq, Repr for Variable
 deriving instance DecidableEq, Repr for Goal
@ -58,6 +64,26 @@ def runMetaMSeq (env: Environment) (metaM: MetaM LSpec.TestSeq): IO LSpec.TestSe
 def runTermElabMInMeta { α } (termElabM: Lean.Elab.TermElabM α): Lean.MetaM α :=
  termElabM.run' (ctx := Pantograph.defaultTermElabMContext)

+def exprToStr (e: Expr): Lean.MetaM String := toString <$> Meta.ppExpr e
+
+def parseSentence (s: String): MetaM Expr := do
+  let recursor ← match Parser.runParserCategory
+    (env := ← MonadEnv.getEnv)
+    (catName := `term)
+    (input := s)
+    (fileName := filename) with
+    | .ok syn => pure syn
+    | .error error => throwError "Failed to parse: {error}"
+  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] }
+    return newGoals.goals
+def mvarUserNameAndType (mvarId: MVarId): MetaM (Name × String) := do
+  let name := (← mvarId.getDecl).userName
+  let t ← exprToStr (← mvarId.getType)
+  return (name, t)
+
 end Test

 end Pantograph
--- a/Test/Integration.lean
+++ b/Test/Integration.lean
@ -35,7 +35,7 @@ def subroutine_runner (steps: List (MainM LSpec.TestSeq)): IO LSpec.TestSeq := d
 def test_elab : IO LSpec.TestSeq :=
  subroutine_runner [
    subroutine_step "expr.echo"
-      [("expr", .str "λ {α : Sort (u + 1)} => List α")]
+      [("expr", .str "λ {α : Sort (u + 1)} => List α"), ("levels", .arr #["u"])]
     (Lean.toJson ({
       type := { pp? := .some "{α : Type u} → Type u" },
       expr := { pp? := .some "fun {α} => List α" }
@ -65,7 +65,7 @@ def test_option_modify : IO LSpec.TestSeq :=
    subroutine_step "options.print"
      []
     (Lean.toJson ({ options with printExprAST := true }:
-      Protocol.OptionsPrintResult))
+      Protocol.Options))
  ]
 def test_malformed_command : IO LSpec.TestSeq :=
  let invalid := "invalid"
@ -88,11 +88,11 @@ def test_tactic : IO LSpec.TestSeq :=
    vars := #[{ name := "_uniq.10", userName := "x", isInaccessible? := .some false, type? := .some { pp? := .some "Prop" }}],
  }
  let goal2: Protocol.Goal := {
-    name := "_uniq.14",
+    name := "_uniq.17",
    target := { pp? := .some "x ∨ y → y ∨ x" },
    vars := #[
      { name := "_uniq.10", userName := "x", isInaccessible? := .some false, type? := .some { pp? := .some "Prop" }},
-      { name := "_uniq.13", userName := "y", isInaccessible? := .some false, type? := .some { pp? := .some "Prop" }}
+      { name := "_uniq.16", userName := "y", isInaccessible? := .some false, type? := .some { pp? := .some "Prop" }}
    ],
  }
  subroutine_runner [
--- a/Test/Main.lean
+++ b/Test/Main.lean
@ -5,6 +5,7 @@ import Test.Library
 import Test.Metavar
 import Test.Proofs
 import Test.Serial
+import Test.Tactic

 -- Test running infrastructure

@ -48,6 +49,9 @@ def main (args: List String) := do
    ("Metavar", Metavar.suite env_default),
    ("Proofs", Proofs.suite env_default),
    ("Serial", Serial.suite env_default),
+    ("Tactic/Congruence", Tactic.Congruence.suite env_default),
+    ("Tactic/Motivated Apply", Tactic.MotivatedApply.suite env_default),
+    ("Tactic/No Confuse", Tactic.NoConfuse.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)
--- a/Test/Metavar.lean
+++ b/Test/Metavar.lean
@ -263,7 +263,7 @@ def test_partial_continuation: TestM Unit := do

  -- Continuation should fail if the state does not exist:
  match state0.resume coupled_goals with
-  | .error error => addTest $ LSpec.check "(continuation failure message)" (error = "Goals not in scope")
+  | .error error => addTest $ LSpec.check "(continuation failure message)" (error = "Goals [_uniq.40, _uniq.41, _uniq.38, _uniq.47] are not in scope")
  | .ok _ => addTest $ assertUnreachable "(continuation failure)"
  -- Continuation should fail if some goals have not been solved
  match state2.continue state1 with
--- a/Test/Proofs.lean
+++ b/Test/Proofs.lean
@ -49,7 +49,20 @@ def startProof (start: Start): TestM (Option GoalState) := do
        let goal ← GoalState.create (expr := expr)
        return Option.some goal

-def buildGoal (nameType: List (String × String)) (target: String) (userName?: Option String := .none): Protocol.Goal :=
+def buildNamedGoal (name: String) (nameType: List (String × String)) (target: String)
+    (userName?: Option String := .none): Protocol.Goal :=
+  {
+    name,
+    userName?,
+    target := { pp? := .some target},
+    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):
+    Protocol.Goal :=
  {
    userName?,
    target := { pp? := .some target},
@ -71,6 +84,27 @@ def proofRunner (env: Lean.Environment) (tests: TestM Unit): IO LSpec.TestSeq :=
  | .ok (_, a) =>
    return a

+def test_identity: TestM Unit := do
+  let state? ← startProof (.expr "∀ (p: Prop), p → p")
+  let state0 ← match state? with
+    | .some state => pure state
+    | .none => do
+      addTest $ assertUnreachable "Goal could not parse"
+      return ()
+
+  let tactic := "intro p h"
+  let state1 ← match ← state0.tryTactic (goalId := 0) (tactic := tactic) with
+    | .success state => pure state
+    | other => do
+      addTest $ assertUnreachable $ other.toString
+      return ()
+  let inner := "_uniq.12"
+  addTest $ LSpec.check tactic ((← state1.serializeGoals (options := ← read)).map (·.name) =
+    #[inner])
+  let state1parent ← state1.withParentContext do
+    serializeExpressionSexp (← instantiateAll state1.parentExpr?.get!) (sanitize := false)
+  addTest $ LSpec.test "(1 parent)" (state1parent == s!"(:lambda p (:sort 0) (:lambda h 0 (:subst (:mv {inner}) 1 0)))")
+
 -- Individual test cases
 example: ∀ (a b: Nat), a + b = b + a := by
  intro n m
@ -213,11 +247,26 @@ def test_or_comm: TestM Unit := do
    | other => do
      addTest $ assertUnreachable $ other.toString
      return ()
-  addTest $ LSpec.check tactic ((← state1.serializeGoals (options := ← read)).map (·.devolatilize) =
-    #[buildGoal [("p", "Prop"), ("q", "Prop"), ("h", "p ∨ q")] "q ∨ p"])
+  let fvP := "_uniq.10"
+  let fvQ := "_uniq.13"
+  let fvH := "_uniq.16"
+  let state1g0 := "_uniq.17"
+  addTest $ LSpec.check tactic ((← state1.serializeGoals (options := ← read)) =
+    #[{
+      name := state1g0,
+      target := { pp? := .some "q ∨ p" },
+      vars := #[
+        { name := fvP, userName := "p", type? := .some { pp? := .some "Prop" }, isInaccessible? := .some false },
+        { name := fvQ, userName := "q", type? := .some { pp? := .some "Prop" }, isInaccessible? := .some false },
+        { name := fvH, userName := "h", type? := .some { pp? := .some "p ∨ q" }, isInaccessible? := .some false }
+      ]
+    }])
  addTest $ LSpec.check "(1 parent)" state1.parentExpr?.isSome
  addTest $ LSpec.check "(1 root)" state1.rootExpr?.isNone

+  let state1parent ← state1.withParentContext do
+    serializeExpressionSexp (← instantiateAll state1.parentExpr?.get!) (sanitize := false)
+  addTest $ LSpec.test "(1 parent)" (state1parent == s!"(:lambda p (:sort 0) (:lambda q (:sort 0) (:lambda h ((:c Or) 1 0) (:subst (:mv {state1g0}) 2 1 0))))")
  let tactic := "cases h"
  let state2 ← match ← state1.tryTactic (goalId := 0) (tactic := tactic) with
    | .success state => pure state
@ -226,21 +275,31 @@ def test_or_comm: TestM Unit := do
      return ()
  addTest $ LSpec.check tactic ((← state2.serializeGoals (options := ← read)).map (·.devolatilize) =
    #[branchGoal "inl" "p", branchGoal "inr" "q"])
-  addTest $ LSpec.check "(2 parent)" state2.parentExpr?.isSome
+  let (caseL, caseR) := ("_uniq.64", "_uniq.77")
+  addTest $ LSpec.check tactic ((← state2.serializeGoals (options := ← read)).map (·.name) =
+    #[caseL, caseR])
+  addTest $ LSpec.check "(2 parent exists)" state2.parentExpr?.isSome
  addTest $ LSpec.check "(2 root)" state2.rootExpr?.isNone

-  let state2parent ← serializeExpressionSexp state2.parentExpr?.get! (sanitize := false)
-  -- This is due to delayed assignment
+  let state2parent ← state2.withParentContext do
+    serializeExpressionSexp (← instantiateAll state2.parentExpr?.get!) (sanitize := false)
+  let orPQ := s!"((:c Or) (:fv {fvP}) (:fv {fvQ}))"
+  let orQP := s!"((:c Or) (:fv {fvQ}) (:fv {fvP}))"
+  let motive := s!"(:lambda t._@._hyg.26 {orPQ} (:forall h ((:c Eq) ((:c Or) (:fv {fvP}) (:fv {fvQ})) (:fv {fvH}) 0) {orQP}))"
+  let caseL := s!"(:lambda h._@._hyg.27 (:fv {fvP}) (:lambda h._@._hyg.28 ((:c Eq) {orPQ} (:fv {fvH}) ((:c Or.inl) (:fv {fvP}) (:fv {fvQ}) 0)) (:subst (:mv {caseL}) (:fv {fvP}) (:fv {fvQ}) 1)))"
+  let caseR := s!"(:lambda h._@._hyg.29 (:fv {fvQ}) (:lambda h._@._hyg.30 ((:c Eq) {orPQ} (:fv {fvH}) ((:c Or.inr) (:fv {fvP}) (:fv {fvQ}) 0)) (:subst (:mv {caseR}) (:fv {fvP}) (:fv {fvQ}) 1)))"
+  let conduit := s!"((:c Eq.refl) {orPQ} (:fv {fvH}))"
  addTest $ LSpec.test "(2 parent)" (state2parent ==
-    "((:mv _uniq.43) (:fv _uniq.16) ((:c Eq.refl) ((:c Or) (:fv _uniq.10) (:fv _uniq.13)) (:fv _uniq.16)))")
+    s!"((:c Or.casesOn) (:fv {fvP}) (:fv {fvQ}) {motive} (:fv {fvH}) {caseL} {caseR} {conduit})")

  let state3_1 ← match ← state2.tryTactic (goalId := 0) (tactic := "apply Or.inr") with
    | .success state => pure state
    | other => do
      addTest $ assertUnreachable $ other.toString
      return ()
-  let state3_1parent ← serializeExpressionSexp state3_1.parentExpr?.get! (sanitize := false)
-  addTest $ LSpec.test "(3_1 parent)" (state3_1parent == "((:c Or.inr) (:fv _uniq.13) (:fv _uniq.10) (:mv _uniq.78))")
+  let state3_1parent ← state3_1.withParentContext do
+    serializeExpressionSexp (← instantiateAll state3_1.parentExpr?.get!) (sanitize := false)
+  addTest $ LSpec.test "(3_1 parent)" (state3_1parent == s!"((:c Or.inr) (:fv {fvQ}) (:fv {fvP}) (:mv _uniq.91))")
  addTest $ LSpec.check "· apply Or.inr" (state3_1.goals.length = 1)
  let state4_1 ← match ← state3_1.tryTactic (goalId := 0) (tactic := "assumption") with
    | .success state => pure state
@ -248,8 +307,8 @@ def test_or_comm: TestM Unit := do
      addTest $ assertUnreachable $ other.toString
      return ()
  addTest $ LSpec.check "  assumption" state4_1.goals.isEmpty
-  let state4_1parent ← serializeExpressionSexp state4_1.parentExpr?.get! (sanitize := false)
-  addTest $ LSpec.test "(4_1 parent)" (state4_1parent == "(:fv _uniq.47)")
+  let state4_1parent ← instantiateAll state4_1.parentExpr?.get!
+  addTest $ LSpec.test "(4_1 parent)" state4_1parent.isFVar
  addTest $ LSpec.check "(4_1 root)" state4_1.rootExpr?.isNone
  let state3_2 ← match ← state2.tryTactic (goalId := 1) (tactic := "apply Or.inl") with
    | .success state => pure state
@ -582,7 +641,7 @@ def test_let (specialized: Bool): TestM Unit := do
      interiorGoal [] "let b := ?m.20;\np ∨ ¬p"
    ])
  -- Check that the goal mvar ids match up
-  addTest $ LSpec.check expr ((serializedState2.map (·.name) |>.get! 0) = "_uniq.20")
+  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
@ -625,8 +684,173 @@ def test_let (specialized: Bool): TestM Unit := do
      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
+    | .some state => pure state
+    | .none => do
+      addTest $ assertUnreachable "Goal could not parse"
+      return ()
+  let tactic := "intro n"
+  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 [("n", "Nat")] "n + 0 = n"])
+  let recursor := "@Nat.brecOn"
+  let state2 ← match ← state1.tryMotivatedApply (goalId := 0) (recursor := recursor) with
+    | .success state => pure state
+    | other => do
+      addTest $ assertUnreachable $ other.toString
+      return ()
+  addTest $ LSpec.check s!"mapply {recursor}" ((← state2.serializeGoals (options := ← read)).map (·.devolatilizeVars) =
+    #[
+      buildNamedGoal "_uniq.67" [("n", "Nat")] "Nat → Prop" (.some "motive"),
+      buildNamedGoal "_uniq.68" [("n", "Nat")] "Nat",
+      buildNamedGoal "_uniq.69" [("n", "Nat")] "∀ (t : Nat), Nat.below t → ?motive t",
+      buildNamedGoal "_uniq.70" [("n", "Nat")] "?motive ?m.68 = (n + 0 = n)" (.some "conduit")
+    ])
+
+  let tactic := "exact n"
+  let state3b ← match ← state2.tryTactic (goalId := 1) (tactic := tactic) with
+    | .success state => pure state
+    | other => do
+      addTest $ assertUnreachable $ other.toString
+      return ()
+  addTest $ LSpec.check tactic ((← state3b.serializeGoals (options := ← read)).map (·.devolatilize) =
+    #[])
+  let state2b ← match state3b.continue state2 with
+    | .ok state => pure state
+    | .error e => do
+      addTest $ assertUnreachable e
+      return ()
+  let tactic := "exact (λ x => x + 0 = x)"
+  let state3c ← match ← state2b.tryTactic (goalId := 0) (tactic := tactic) with
+    | .success state => pure state
+    | other => do
+      addTest $ assertUnreachable $ other.toString
+      return ()
+  addTest $ LSpec.check tactic ((← state3c.serializeGoals (options := ← read)).map (·.devolatilize) =
+    #[])
+  let state2c ← match state3c.continue state2b with
+    | .ok state => pure state
+    | .error e => do
+      addTest $ assertUnreachable e
+      return ()
+  let tactic := "intro t h"
+  let state3 ← match ← state2c.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) =
+    #[buildGoal [("n", "Nat"), ("t", "Nat"), ("h", "Nat.below t")] "t + 0 = t"])
+
+  let tactic := "simp"
+  let state3d ← match ← state3.tryTactic (goalId := 0) (tactic := tactic) with
+    | .success state => pure state
+    | other => do
+      addTest $ assertUnreachable $ other.toString
+      return ()
+  let state2d ← match state3d.continue state2c with
+    | .ok state => pure state
+    | .error e => do
+      addTest $ assertUnreachable e
+      return ()
+  let tactic := "rfl"
+  let stateF ← match ← state2d.tryTactic (goalId := 0) (tactic := tactic) with
+    | .success state => pure state
+    | other => do
+      addTest $ assertUnreachable $ other.toString
+      return ()
+  addTest $ LSpec.check tactic ((← stateF.serializeGoals (options := ← read)) =
+    #[])
+
+  let expr := stateF.mctx.eAssignment.find! stateF.root
+  let (expr, _) := instantiateMVarsCore (mctx := stateF.mctx) (e := expr)
+  addTest $ LSpec.check "(F root)" stateF.rootExpr?.isSome
+
+def test_nat_zero_add_alt: TestM Unit := do
+  let state? ← startProof (.expr "∀ (n: Nat), n + 0 = n")
+  let state0 ← match state? with
+    | .some state => pure state
+    | .none => do
+      addTest $ assertUnreachable "Goal could not parse"
+      return ()
+  let tactic := "intro n"
+  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 [("n", "Nat")] "n + 0 = n"])
+  let recursor := "@Nat.brecOn"
+  let state2 ← match ← state1.tryMotivatedApply (goalId := 0) (recursor := recursor) with
+    | .success state => pure state
+    | other => do
+      addTest $ assertUnreachable $ other.toString
+      return ()
+  let major := "_uniq.68"
+  addTest $ LSpec.check s!"mapply {recursor}" ((← state2.serializeGoals (options := ← read)).map (·.devolatilizeVars) =
+    #[
+      buildNamedGoal "_uniq.67" [("n", "Nat")] "Nat → Prop" (.some "motive"),
+      buildNamedGoal major [("n", "Nat")] "Nat",
+      buildNamedGoal "_uniq.69" [("n", "Nat")] "∀ (t : Nat), Nat.below t → ?motive t",
+      buildNamedGoal "_uniq.70" [("n", "Nat")] "?motive ?m.68 = (n + 0 = n)" (.some "conduit")
+    ])
+
+  let tactic := "intro x"
+  let state3m ← match ← state2.tryTactic (goalId := 0) (tactic := tactic) with
+    | .success state => pure state
+    | other => do
+      addTest $ assertUnreachable $ other.toString
+      return ()
+  addTest $ LSpec.check tactic ((← state3m.serializeGoals (options := ← read)).map (·.devolatilize) =
+    #[buildGoal [("n", "Nat"), ("x", "Nat")] "Prop" (.some "motive")])
+  let tactic := "apply Eq"
+  let state3m2 ← match ← state3m.tryTactic (goalId := 0) (tactic := tactic) with
+    | .success state => pure state
+    | other => do
+      addTest $ assertUnreachable $ other.toString
+      return ()
+  let (eqL, eqR, eqT) := ("_uniq.88", "_uniq.89", "_uniq.87")
+  addTest $ LSpec.check tactic $ state3m2.goals.map (·.name.toString) = [eqL, eqR, eqT]
+  let [_motive, _major, _step, conduit] := state2.goals | panic! "Goals conflict"
+  let state2b ← match state3m2.resume [conduit] with
+    | .ok state => pure state
+    | .error e => do
+      addTest $ assertUnreachable e
+      return ()
+
+  let cNatAdd := "(:c HAdd.hAdd) (:c Nat) (:c Nat) (:c Nat) ((:c instHAdd) (:c Nat) (:c instAddNat))"
+  let cNat0 := "((:c OfNat.ofNat) (:c Nat) (:lit 0) ((:c instOfNatNat) (:lit 0)))"
+  let fvN := "_uniq.63"
+  let conduitRight := s!"((:c Eq) (:c Nat) ({cNatAdd} (:fv {fvN}) {cNat0}) (:fv {fvN}))"
+  let substOf (mv: String) := s!"(:subst (:mv {mv}) (:fv {fvN}) (:mv {major}))"
+  addTest $ LSpec.check "resume" ((← state2b.serializeGoals (options := { ← read with printExprAST := true })) =
+    #[
+      {
+        name := "_uniq.70",
+        userName? := .some "conduit",
+        target := {
+          pp? := .some "(?m.92 ?m.68 = ?m.94 ?m.68) = (n + 0 = n)",
+          sexp? := .some s!"((:c Eq) (:sort 0) ((:c Eq) {substOf eqT} {substOf eqL} {substOf eqR}) {conduitRight})",
+        },
+        vars := #[{
+          name := fvN,
+          userName := "n",
+          type? := .some { pp? := .some "Nat", sexp? := .some "(:c Nat)" },
+          isInaccessible? := .some false
+        }],
+      }
+    ])
+
 def suite (env: Environment): List (String × IO LSpec.TestSeq) :=
  let tests := [
+    ("identity", test_identity),
    ("Nat.add_comm", test_nat_add_comm false),
    ("Nat.add_comm manual", test_nat_add_comm true),
    ("Nat.add_comm delta", test_delta_variable),
@ -637,6 +861,8 @@ def suite (env: Environment): List (String × IO LSpec.TestSeq) :=
    ("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),
  ]
  tests.map (fun (name, test) => (name, proofRunner env test))

--- a/Test/Serial.lean
+++ b/Test/Serial.lean
@ -47,13 +47,15 @@ def test_sexp_of_symbol (env: Environment): IO LSpec.TestSeq := do
    return LSpec.TestSeq.append suites test) LSpec.TestSeq.done

 def test_sexp_of_elab (env: Environment): IO LSpec.TestSeq := do
-  let entries: List (String × String) := [
-    ("λ x: Nat × Bool => x.1", "(:lambda x ((:c Prod) (:c Nat) (:c Bool)) ((:c Prod.fst) (:c Nat) (:c Bool) 0))"),
-    ("λ x: Array Nat => x.data", "(:lambda x ((:c Array) (:c Nat)) ((:c Array.data) (:c Nat) 0))"),
-    -- This tests `autoBoundImplicit`
-    ("λ {α : Sort (u + 1)} => List α", "(:lambda α (:sort (+ u 1)) ((:c List) 0) :implicit)"),
+  let entries: List (String × (List Name) × String) := [
+    ("λ x: Nat × Bool => x.1", [], "(:lambda x ((:c Prod) (:c Nat) (:c Bool)) ((:c Prod.fst) (:c Nat) (:c Bool) 0))"),
+    ("λ x: Array Nat => x.data", [], "(:lambda x ((:c Array) (:c Nat)) ((:c Array.data) (:c Nat) 0))"),
+    ("λ {α: Sort (u + 1)} => List α", [`u], "(:lambda α (:sort (+ u 1)) ((:c List) 0) :implicit)"),
+    ("λ {α} => List α", [], "(:lambda α (:sort (+ (:mv _uniq.4) 1)) ((:c List) 0) :implicit)"),
+    ("(2: Nat) <= (5: Nat)", [], "((:c LE.le) (:mv _uniq.18) (:mv _uniq.19) ((:c OfNat.ofNat) (:mv _uniq.4) (:lit 2) (:mv _uniq.5)) ((:c OfNat.ofNat) (:mv _uniq.14) (:lit 5) (:mv _uniq.15)))"),
  ]
-  let termElabM: Elab.TermElabM LSpec.TestSeq := entries.foldlM (λ suites (source, target) => do
+  entries.foldlM (λ suites (source, levels, target) =>
+    let termElabM := do
      let env ← MonadEnv.getEnv
      let s ← match parseTerm env source with
        | .ok s => pure s
@ -61,9 +63,10 @@ def test_sexp_of_elab (env: Environment): IO LSpec.TestSeq := do
      let expr ← match (← elabTerm s) with
        | .ok expr => pure expr
        | .error e => return elabFailure e
-    let test := LSpec.check source ((← serializeExpressionSexp expr) = target)
-    return LSpec.TestSeq.append suites test) LSpec.TestSeq.done
-  runMetaMSeq env $ termElabM.run' (ctx := defaultTermElabMContext)
+      return LSpec.check source ((← serializeExpressionSexp expr) = target)
+    let metaM := (Elab.Term.withLevelNames levels termElabM).run' (ctx := defaultTermElabMContext)
+    return LSpec.TestSeq.append suites (← runMetaMSeq env metaM))
+    LSpec.TestSeq.done

 def test_sexp_of_expr (env: Environment): IO LSpec.TestSeq := do
  let entries: List (Expr × String) := [
--- a/Test/Tactic.lean
+++ b/Test/Tactic.lean
@ -0,0 +1,3 @@
+import Test.Tactic.Congruence
+import Test.Tactic.MotivatedApply
+import Test.Tactic.NoConfuse
--- a/Test/Tactic/Congruence.lean
+++ b/Test/Tactic/Congruence.lean
@ -0,0 +1,80 @@
+import LSpec
+import Lean
+import Test.Common
+
+open Lean
+open Pantograph
+
+namespace Pantograph.Test.Tactic.Congruence
+
+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 test ← runTermElabMInMeta do
+        let newGoals ← runTacticOnMVar Tactic.congruenceArg target.mvarId!
+        pure $ LSpec.check "goals" ((← newGoals.mapM (λ x => mvarUserNameAndType x)) =
+          [
+            (`α, "Sort ?u.70"),
+            (`a₁, "?α"),
+            (`a₂, "?α"),
+            (`f, "?α → Nat"),
+            (`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"
+  runMetaMSeq env do
+    let expr ← parseSentence expr
+    Meta.lambdaTelescope expr $ λ _ body => do
+      let mut tests := LSpec.TestSeq.done
+      let target ← Meta.mkFreshExprSyntheticOpaqueMVar body
+      let test ← runTermElabMInMeta do
+        let newGoals ← runTacticOnMVar Tactic.congruenceFun target.mvarId!
+        pure $ LSpec.check "goals" ((← newGoals.mapM (λ x => mvarUserNameAndType x)) =
+          [
+            (`α, "Sort ?u.159"),
+            (`f₁, "?α → Nat"),
+            (`f₂, "?α → Nat"),
+            (`h, "?f₁ = ?f₂"),
+            (`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"
+  runMetaMSeq env do
+    let expr ← parseSentence expr
+    Meta.lambdaTelescope expr $ λ _ body => do
+      let mut tests := LSpec.TestSeq.done
+      let target ← Meta.mkFreshExprSyntheticOpaqueMVar body
+      let test ← runTermElabMInMeta do
+        let newGoals ← runTacticOnMVar Tactic.congruence target.mvarId!
+        pure $ LSpec.check "goals" ((← newGoals.mapM (λ x => mvarUserNameAndType x)) =
+          [
+            (`α, "Sort ?u.10"),
+            (`f₁, "?α → Nat"),
+            (`f₂, "?α → Nat"),
+            (`a₁, "?α"),
+            (`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", test_congr_arg env),
+    ("congrFun", test_congr_fun env),
+    ("congr", test_congr env),
+  ]
+
+end Pantograph.Test.Tactic.Congruence
--- a/Test/Tactic/MotivatedApply.lean
+++ b/Test/Tactic/MotivatedApply.lean
@ -0,0 +1,130 @@
+import LSpec
+import Lean
+import Test.Common
+
+open Lean
+open Pantograph
+
+namespace Pantograph.Test.Tactic.MotivatedApply
+
+def test_type_extract (env: Environment): IO LSpec.TestSeq :=
+  runMetaMSeq env do
+    let mut tests := LSpec.TestSeq.done
+    let recursor ← parseSentence "@Nat.brecOn"
+    let recursorType ← Meta.inferType recursor
+    tests := tests ++ LSpec.check "recursorType" ("{motive : Nat → Sort ?u.1} → (t : Nat) → ((t : Nat) → Nat.below t → motive t) → motive t" =
+      (← exprToStr recursorType))
+    let info ← match Tactic.getRecursorInformation recursorType with
+      | .some info => pure info
+      | .none => throwError "Failed to extract recursor info"
+    tests := tests ++ LSpec.check "iMotive" (info.iMotive = 2)
+    let motiveType := info.getMotiveType
+    tests := tests ++ LSpec.check "motiveType" ("Nat → Sort ?u.1" =
+      (← exprToStr motiveType))
+    return tests
+
+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
+        (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)
+      (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
+      let mut tests := LSpec.TestSeq.done
+      -- Apply the tactic
+      let target ← Meta.mkFreshExprSyntheticOpaqueMVar body
+      let tactic := Tactic.motivatedApply recursor
+      let newGoals ← runTacticOnMVar tactic target.mvarId!
+      let majorId := 67
+      tests := tests ++ (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"
+      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
+
+      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 env),
+    ("Nat.brecOn", test_nat_brec_on env),
+    ("List.brecOn", test_list_brec_on env),
+    ("Nat.brecOn partial motive instantiation", test_partial_motive_instantiation env),
+  ]
+
+end Pantograph.Test.Tactic.MotivatedApply
--- a/Test/Tactic/NoConfuse.lean
+++ b/Test/Tactic/NoConfuse.lean
@ -0,0 +1,87 @@
+import LSpec
+import Lean
+import Test.Common
+
+open Lean
+open Pantograph
+
+namespace Pantograph.Test.Tactic.NoConfuse
+
+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
+        (env := ← MonadEnv.getEnv)
+        (catName := `term)
+        (input := "h")
+        (fileName := filename) with
+        | .ok syn => pure syn
+        | .error error => throwError "Failed to parse: {error}"
+      let mut tests := LSpec.TestSeq.done
+      -- Apply the tactic
+      let target ← Meta.mkFreshExprSyntheticOpaqueMVar body
+      let tactic := Tactic.noConfuse recursor
+      let test ← runTermElabMInMeta do
+        let 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 (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
+        (env := ← MonadEnv.getEnv)
+        (catName := `term)
+        (input := "h")
+        (fileName := filename) with
+        | .ok syn => pure syn
+        | .error error => throwError "Failed to parse: {error}"
+      let mut tests := LSpec.TestSeq.done
+      -- Apply the tactic
+      let target ← Meta.mkFreshExprSyntheticOpaqueMVar body
+      try
+        let tactic := Tactic.noConfuse recursor
+        let _ ← runTermElabMInMeta $ runTacticOnMVar tactic target.mvarId!
+        tests := tests ++ assertUnreachable "Tactic should fail"
+      catch _ =>
+        tests := tests ++ LSpec.check "Tactic should fail" true
+        return tests
+      return tests
+
+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
+        (env := ← MonadEnv.getEnv)
+        (catName := `term)
+        (input := "h")
+        (fileName := filename) with
+        | .ok syn => pure syn
+        | .error error => throwError "Failed to parse: {error}"
+      let mut tests := LSpec.TestSeq.done
+      -- Apply the tactic
+      let target ← Meta.mkFreshExprSyntheticOpaqueMVar body
+      let tactic := Tactic.noConfuse recursor
+      let test ← runTermElabMInMeta do
+        let 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 env),
+    ("Nat fail", test_nat_fail env),
+    ("List", test_list env),
+  ]
+
+end Pantograph.Test.Tactic.NoConfuse