Merge pull request 'feat: Add support for the `have`, `conv`, and `calc` tactics' (#59) from goal/have-conv-calc into dev

Reviewed-on: #59
2024-04-11 15:36:19 -07:00 · 2024-04-11 15:36:19 -07:00 · f20ee8dc87
parent a11df9f2e9 a41b95e540
commit f20ee8dc87
9 changed files with 669 additions and 140 deletions
--- a/Pantograph.lean
+++ b/Pantograph.lean
@ -114,12 +114,22 @@ def execute (command: Protocol.Command): MainM Lean.Json := do
    match state.goalStates.find? args.stateId with
    | .none => return .error $ errorIndex s!"Invalid state index {args.stateId}"
    | .some goalState => do
-      let nextGoalState?: Except _ GoalState ← match args.tactic?, args.expr? with
-        | .some tactic, .none => do
+      let nextGoalState?: Except _ GoalState ←
+        match args.tactic?, args.expr?, args.have?, args.calc?, args.conv?  with
+        | .some tactic, .none, .none, .none, .none => do
          pure ( Except.ok (← goalTactic goalState args.goalId tactic))
-        | .none, .some expr => do
-          pure ( Except.ok (← goalTryAssign goalState args.goalId expr))
-        | _, _ => pure (Except.error <| errorI "arguments" "Exactly one of {tactic, expr} must be supplied")
+        | .none, .some expr, .none, .none, .none => do
+          pure ( Except.ok (← goalAssign goalState args.goalId expr))
+        | .none, .none, .some type, .none, .none => do
+          let binderName := args.binderName?.getD ""
+          pure ( Except.ok (← goalHave goalState args.goalId binderName type))
+        | .none, .none, .none, .some pred, .none => do
+          pure ( Except.ok (← goalCalc goalState args.goalId pred))
+        | .none, .none, .none, .none, .some true => do
+          pure ( Except.ok (← goalConv goalState args.goalId))
+        | .none, .none, .none, .none, .some false => do
+          pure ( Except.ok (← goalConvExit goalState))
+        | _, _, _, _, _ => pure (Except.error <| errorI "arguments" "Exactly one of {tactic, expr, have} must be supplied")
      match nextGoalState? with
      | .error error => return .error error
      | .ok (.success nextGoalState) =>
@ -137,6 +147,8 @@ def execute (command: Protocol.Command): MainM Lean.Json := do
        return .ok { parseError? := .some message }
      | .ok (.indexError goalId) =>
        return .error $ errorIndex s!"Invalid goal id index {goalId}"
+      | .ok (.invalidAction message) =>
+        return .error $ errorI "invalid" message
      | .ok (.failure messages) =>
        return .ok { tacticErrors? := .some messages }
  goal_continue (args: Protocol.GoalContinue): MainM (CR Protocol.GoalContinueResult) := do
--- a/Pantograph/Goal.lean
+++ b/Pantograph/Goal.lean
@ -1,3 +1,8 @@
+/-
+Functions for handling metavariables
+
+All the functions starting with `try` resume their inner monadic state.
+-/
 import Pantograph.Protocol
 import Lean

@ -10,6 +15,11 @@ def Lean.MessageLog.getErrorMessages (log : MessageLog) : MessageLog :=
 namespace Pantograph
 open Lean

+def filename: String := "<pantograph>"
+
+/--
+Represents an interconnected set of metavariables, or a state in proof search
+ -/
 structure GoalState where
  savedState : Elab.Tactic.SavedState

@ -18,21 +28,22 @@ structure GoalState where
  -- New metavariables acquired in this state
  newMVars: SSet MVarId

-  -- The id of the goal in the parent
-  parentGoalId: Nat := 0
-
  -- Parent state metavariable source
-  parentMVar: Option MVarId
+  parentMVar?: Option MVarId

-abbrev M := Elab.TermElabM
+  -- Existence of this field shows that we are currently in `conv` mode.
+  convMVar?: Option (MVarId × MVarId) := .none
+  -- Previous RHS for calc, so we don't have to repeat it every time
+  -- WARNING: If using `state with` outside of `calc`, this must be set to `.none`
+  calcPrevRhs?: Option Expr := .none

-protected def GoalState.create (expr: Expr): M GoalState := do
+protected def GoalState.create (expr: Expr): Elab.TermElabM GoalState := do
  -- May be necessary to immediately synthesise all metavariables if we need to leave the elaboration context.
  -- See https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Unknown.20universe.20metavariable/near/360130070

  --Elab.Term.synthesizeSyntheticMVarsNoPostponing
  --let expr ← instantiateMVars expr
-  let goal := (← Meta.mkFreshExprMVar expr (kind := MetavarKind.synthetic) (userName := .anonymous))
+  let goal ← Meta.mkFreshExprMVar expr (kind := MetavarKind.synthetic) (userName := .anonymous)
  let savedStateMonad: Elab.Tactic.TacticM Elab.Tactic.SavedState := MonadBacktrack.saveState
  let root := goal.mvarId!
  let savedState ← savedStateMonad { elaborator := .anonymous } |>.run' { goals := [root]}
@ -40,28 +51,38 @@ protected def GoalState.create (expr: Expr): M GoalState := do
    savedState,
    root,
    newMVars := SSet.insert .empty root,
-    parentMVar := .none,
+    parentMVar? := .none,
  }
-protected def GoalState.goals (state: GoalState): List MVarId := state.savedState.tactic.goals
-
-protected def GoalState.runM {α: Type} (state: GoalState) (m: Elab.TermElabM α) : M α := do
-  state.savedState.term.restore
-  m
-
+protected def GoalState.isConv (state: GoalState): Bool :=
+  state.convMVar?.isSome
+protected def GoalState.goals (state: GoalState): List MVarId :=
+  state.savedState.tactic.goals
 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
 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 :=
  state.savedState.term.restore
-def GoalState.restoreMetaM (state: GoalState): MetaM Unit :=
-  state.savedState.term.meta.restore
+private def GoalState.restoreTacticM (state: GoalState) (goal: MVarId): Elab.Tactic.TacticM Unit := do
+  state.savedState.restore
+  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

 /-- Inner function for executing tactic on goal state -/
 def executeTactic (state: Elab.Tactic.SavedState) (goal: MVarId) (tactic: Syntax) :
-    M (Except (Array String) Elab.Tactic.SavedState):= do
+    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]
@ -87,19 +108,22 @@ inductive TacticResult where
  | parseError (message: String)
  -- The goal index is out of bounds
  | indexError (goalId: Nat)
+  -- The given action cannot be executed in the state
+  | invalidAction (message: String)

 /-- Execute tactic on given state -/
-protected def GoalState.execute (state: GoalState) (goalId: Nat) (tactic: String):
-    M TacticResult := do
+protected def GoalState.tryTactic (state: GoalState) (goalId: Nat) (tactic: 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.tryTactic
  let tactic ← match Parser.runParserCategory
    (env := ← MonadEnv.getEnv)
-    (catName := `tactic)
+    (catName := if state.isConv then `conv else `tactic)
    (input := tactic)
-    (fileName := "<stdin>") with
+    (fileName := filename) with
    | .ok stx => pure $ stx
    | .error error => return .parseError error
  match (← executeTactic (state := state.savedState) (goal := goal) (tactic := tactic)) with
@ -108,47 +132,33 @@ protected def GoalState.execute (state: GoalState) (goalId: Nat) (tactic: String
  | .ok nextSavedState =>
    -- Assert that the definition of metavariables are the same
    let nextMCtx := nextSavedState.term.meta.meta.mctx
-    let prevMCtx := state.savedState.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.
-    let newMVars ← nextMCtx.decls.foldlM (fun acc mvarId mvarDecl => do
-      if let .some prevMVarDecl := prevMCtx.decls.find? mvarId then
-        assert! prevMVarDecl.type == mvarDecl.type
-        return acc
-      else
-        return acc.insert mvarId
-      ) SSet.empty
    return .success {
-      root := state.root,
+      state with
      savedState := nextSavedState
-      newMVars,
-      parentGoalId := goalId,
-      parentMVar := .some goal,
+      newMVars := newMVarSet prevMCtx nextMCtx,
+      parentMVar? := .some goal,
+      calcPrevRhs? := .none,
    }

-protected def GoalState.tryAssign (state: GoalState) (goalId: Nat) (expr: String): M TacticResult := do
-  state.restoreElabM
-  let goal ← match state.savedState.tactic.goals.get? goalId with
-    | .some goal => pure goal
-    | .none => return .indexError goalId
-  let expr ← match Parser.runParserCategory
-    (env := state.env)
-    (catName := `term)
-    (input := expr)
-    (fileName := "<stdin>") with
-    | .ok syn => pure syn
-    | .error error => return .parseError error
-  let tacticM:  Elab.Tactic.TacticM TacticResult := do
-    state.savedState.restore
-    Elab.Tactic.setGoals [goal]
-    try
-      let expr ← Elab.Term.elabTerm (stx := expr) (expectedType? := .none)
-      -- Attempt to unify the expression
+/-- Assumes elabM has already been restored. Assumes expr has already typechecked -/
+protected def GoalState.assign (state: GoalState) (goal: MVarId) (expr: Expr):
+      Elab.TermElabM TacticResult := do
  let goalType ← goal.getType
+  try
+    -- For some reason this is needed. One of the unit tests will fail if this isn't here
+    let error?: Option String ← goal.withContext (do
      let exprType ← Meta.inferType expr
-      if !(← Meta.isDefEq goalType exprType) then
-        return .failure #["Type unification failed", toString (← Meta.ppExpr goalType), toString (← Meta.ppExpr exprType)]
-      goal.checkNotAssigned `GoalState.tryAssign
+      if ← Meta.isDefEq goalType exprType then
+        pure .none
+      else do
+        return .some s!"{← Meta.ppExpr expr} : {← Meta.ppExpr exprType} != {← Meta.ppExpr goalType}"
+    )
+    if let .some error := error? then
+      return .parseError error
+    goal.checkNotAssigned `GoalState.assign
    goal.assign expr
    if (← getThe Core.State).messages.hasErrors then
      let messages := (← getThe Core.State).messages.getErrorMessages |>.toList.toArray
@ -159,26 +169,245 @@ protected def GoalState.tryAssign (state: GoalState) (goalId: Nat) (expr: String
      let nextMCtx ← getMCtx
      -- 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 ← nextMCtx.decls.foldlM (fun acc mvarId mvarDecl => do
-          if let .some prevMVarDecl := prevMCtx.decls.find? mvarId then
-            assert! prevMVarDecl.type == mvarDecl.type
-            return acc
-          else
-            return mvarId :: acc
-          ) []
-        -- The new goals are the newMVars that lack an assignment
-        Elab.Tactic.setGoals (← newMVars.filterM (λ mvar => do pure !(← mvar.isAssigned)))
-        let nextSavedState ← MonadBacktrack.saveState
+      let newMVars := newMVarSet prevMCtx nextMCtx
+      let nextGoals ← newMVars.toList.filterM (λ mvar => do pure !(← mvar.isAssigned))
      return .success {
        root := state.root,
-          savedState := nextSavedState,
-          newMVars := newMVars.toSSet,
-          parentGoalId := goalId,
-          parentMVar := .some goal,
+        savedState := {
+          term := ← MonadBacktrack.saveState,
+          tactic := { goals := nextGoals }
+        },
+        newMVars,
+        parentMVar? := .some goal,
      }
  catch exception =>
    return .failure #[← exception.toMessageData.toString]
-  tacticM { elaborator := .anonymous } |>.run' state.savedState.tactic
+
+protected def GoalState.tryAssign (state: GoalState) (goalId: Nat) (expr: 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
+  let expr ← match Parser.runParserCategory
+    (env := state.env)
+    (catName := `term)
+    (input := expr)
+    (fileName := filename) with
+    | .ok syn => pure syn
+    | .error error => return .parseError error
+  let goalType ← goal.getType
+  try
+    let expr ← goal.withContext $
+      Elab.Term.elabTermAndSynthesize (stx := expr) (expectedType? := .some goalType)
+    state.assign goal expr
+  catch exception =>
+    return .failure #[← exception.toMessageData.toString]
+
+-- Specialized Tactics
+
+protected def GoalState.tryHave (state: GoalState) (goalId: Nat) (binderName: String) (type: String):
+      Elab.TermElabM TacticResult := do
+  state.restoreElabM
+  let goal ← match state.savedState.tactic.goals.get? goalId with
+    | .some goal => pure goal
+    | .none => return .indexError goalId
+  let type ← match Parser.runParserCategory
+    (env := state.env)
+    (catName := `term)
+    (input := type)
+    (fileName := filename) with
+    | .ok syn => pure syn
+    | .error error => return .parseError error
+  let binderName := binderName.toName
+  try
+    -- Implemented similarly to the intro tactic
+    let nextGoals: List MVarId ← goal.withContext $ (do
+      let type ← Elab.Term.elabType (stx := type)
+      let lctx ← MonadLCtx.getLCtx
+
+      -- The branch goal inherits the same context, but with a different type
+      let mvarBranch ← Meta.mkFreshExprMVarAt lctx (← Meta.getLocalInstances) type
+
+      -- Create the context for the `upstream` goal
+      let fvarId ← mkFreshFVarId
+      let lctxUpstream := lctx.mkLocalDecl fvarId binderName type
+      let fvar   := mkFVar fvarId
+      let mvarUpstream ←
+        withTheReader Meta.Context (fun ctx => { ctx with lctx := lctxUpstream }) do
+          Meta.withNewLocalInstances #[fvar] 0 (do
+            let mvarUpstream ← Meta.mkFreshExprMVarAt (← getLCtx) (← Meta.getLocalInstances)
+              (← goal.getType) (kind := MetavarKind.synthetic) (userName := .anonymous)
+            let expr: Expr := .app (.lam binderName type mvarBranch .default) mvarUpstream
+            goal.assign expr
+            pure mvarUpstream)
+
+      pure [mvarBranch.mvarId!, mvarUpstream.mvarId!]
+    )
+    return .success {
+      root := state.root,
+      savedState := {
+        term := ← MonadBacktrack.saveState,
+        tactic := { goals := nextGoals }
+      },
+      newMVars := nextGoals.toSSet,
+      parentMVar? := .some goal,
+    }
+  catch exception =>
+    return .failure #[← exception.toMessageData.toString]
+
+/-- Enter conv tactic mode -/
+protected def GoalState.conv (state: GoalState) (goalId: Nat):
+      Elab.TermElabM TacticResult := do
+  if state.convMVar?.isSome then
+    return .invalidAction "Already in conv state"
+  let goal ← match state.savedState.tactic.goals.get? goalId with
+    | .some goal => pure goal
+    | .none => return .indexError goalId
+  let tacticM :  Elab.Tactic.TacticM (Elab.Tactic.SavedState × MVarId) := do
+    state.restoreTacticM goal
+
+    -- See Lean.Elab.Tactic.Conv.convTarget
+    let convMVar ← Elab.Tactic.withMainContext do
+      let (rhs, newGoal) ← Elab.Tactic.Conv.mkConvGoalFor (← Elab.Tactic.getMainTarget)
+      Elab.Tactic.setGoals [newGoal.mvarId!]
+      pure rhs.mvarId!
+    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),
+    }
+  catch exception =>
+    return .failure #[← exception.toMessageData.toString]
+
+/-- Exit from `conv` mode. Resumes all goals before the mode starts and applys the conv -/
+protected def GoalState.convExit (state: GoalState):
+      Elab.TermElabM TacticResult := do
+  let (convRhs, convGoal) ← match state.convMVar? with
+    | .some mvar => pure mvar
+    | .none => return .invalidAction "Not in conv state"
+  let tacticM :  Elab.Tactic.TacticM Elab.Tactic.SavedState:= do
+    -- Vide `Lean.Elab.Tactic.Conv.convert`
+    state.savedState.restore
+
+    -- Close all existing goals with `refl`
+    for mvarId in (← Elab.Tactic.getGoals) do
+      liftM <| mvarId.refl <|> mvarId.inferInstance <|> pure ()
+    Elab.Tactic.pruneSolvedGoals
+    unless (← Elab.Tactic.getGoals).isEmpty do
+      throwError "convert tactic failed, there are unsolved goals\n{Elab.goalsToMessageData (← Elab.Tactic.getGoals)}"
+
+    Elab.Tactic.setGoals [convGoal]
+
+    let targetNew ← instantiateMVars (.mvar convRhs)
+    let proof ← instantiateMVars (.mvar convGoal)
+
+    Elab.Tactic.liftMetaTactic1 fun mvarId => mvarId.replaceTargetEq targetNew proof
+    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
+    }
+  catch exception =>
+    return .failure #[← exception.toMessageData.toString]
+
+protected def GoalState.tryCalc (state: GoalState) (goalId: Nat) (pred: String):
+      Elab.TermElabM TacticResult := do
+  state.restoreElabM
+  if state.convMVar?.isSome then
+    return .invalidAction "Cannot initiate `calc` while in `conv` state"
+  let goal ← match state.savedState.tactic.goals.get? goalId with
+    | .some goal => pure goal
+    | .none => return .indexError goalId
+  let `(term|$pred) ← match Parser.runParserCategory
+    (env := state.env)
+    (catName := `term)
+    (input := pred)
+    (fileName := filename) with
+    | .ok syn => pure syn
+    | .error error => return .parseError error
+  try
+    goal.withContext do
+    let target ← instantiateMVars (← goal.getDecl).type
+    let tag := (← goal.getDecl).userName
+
+    let mut step ← Elab.Term.elabType <| ← do
+      if let some prevRhs := state.calcPrevRhs? then
+        Elab.Term.annotateFirstHoleWithType pred (← Meta.inferType prevRhs)
+      else
+        pure pred
+
+    let some (_, lhs, rhs) ← Elab.Term.getCalcRelation? step |
+      throwErrorAt pred "invalid 'calc' step, relation expected{indentExpr step}"
+    if let some prevRhs := state.calcPrevRhs? then
+      unless (← Meta.isDefEqGuarded lhs prevRhs) do
+        throwErrorAt pred "invalid 'calc' step, left-hand-side is{indentD m!"{lhs} : {← Meta.inferType lhs}"}\nprevious right-hand-side is{indentD m!"{prevRhs} : {← Meta.inferType prevRhs}"}" -- "
+
+    -- Creates a mvar to represent the proof that the calc tactic solves the
+    -- current branch
+    -- In the Lean `calc` tactic this is gobbled up by
+    -- `withCollectingNewGoalsFrom`
+    let mut proof ← Meta.mkFreshExprMVarAt (← getLCtx) (← Meta.getLocalInstances) step
+      (userName := tag ++ `calc)
+    let mvarBranch := proof.mvarId!
+
+    let calcPrevRhs? := Option.some rhs
+    let mut proofType ← Meta.inferType proof
+    let mut remainder := Option.none
+
+    -- The calc tactic either solves the main goal or leaves another relation.
+    -- Replace the main goal, and save the new goal if necessary
+    if ¬(← Meta.isDefEq proofType target) then
+      let rec throwFailed :=
+        throwError "'calc' tactic failed, has type{indentExpr proofType}\nbut it is expected to have type{indentExpr target}"
+      let some (_, _, rhs) ← Elab.Term.getCalcRelation? proofType | throwFailed
+      let some (r, _, rhs') ← Elab.Term.getCalcRelation? target | throwFailed
+      let lastStep := mkApp2 r rhs rhs'
+      let lastStepGoal ← Meta.mkFreshExprSyntheticOpaqueMVar lastStep tag
+      (proof, proofType) ← Elab.Term.mkCalcTrans proof proofType lastStepGoal lastStep
+      unless (← Meta.isDefEq proofType target) do throwFailed
+      remainder := .some lastStepGoal.mvarId!
+    goal.assign proof
+
+    let goals := [ mvarBranch ] ++ remainder.toList
+    return .success {
+      root := state.root,
+      savedState := {
+        term := ← MonadBacktrack.saveState,
+        tactic := { goals },
+      },
+      newMVars := goals.toSSet,
+      parentMVar? := .some goal,
+      calcPrevRhs?
+    }
+  catch exception =>
+    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
@ -197,8 +426,8 @@ protected def GoalState.resume (state: GoalState) (goals: List MVarId): Except S
        term := state.savedState.term,
        tactic := { goals := unassigned },
      },
+      calcPrevRhs? := .none,
    }
-
 /--
 Brings into scope all goals from `branch`
 -/
@ -221,7 +450,7 @@ protected def GoalState.rootExpr? (goalState: GoalState): Option Expr := do
    assert! goalState.goals.isEmpty
    return expr
 protected def GoalState.parentExpr? (goalState: GoalState): Option Expr := do
-  let parent ← goalState.parentMVar
+  let parent ← goalState.parentMVar?
  let expr := goalState.mctx.eAssignment.find! parent
  let (expr, _) := instantiateMVarsCore (mctx := goalState.mctx) (e := expr)
  return expr
--- a/Pantograph/Library.lean
+++ b/Pantograph/Library.lean
@ -136,8 +136,8 @@ def parseElabExpr (expr: String) (expectedType?: Option String := .none): Lean.E

@[export pantograph_expr_echo_m]
 def exprEcho (expr: String) (expectedType?: Option String := .none) (options: @&Protocol.Options):
-    Lean.CoreM (Protocol.CR Protocol.ExprEchoResult) := do
-  let termElabM: Lean.Elab.TermElabM _ := do
+    Lean.CoreM (Protocol.CR Protocol.ExprEchoResult) :=
+  runTermElabM do
    let expr ← match ← parseElabExpr expr expectedType? with
      | .error e => return .error e
      | .ok expr => pure expr
@ -149,40 +149,58 @@ def exprEcho (expr: String) (expectedType?: Option String := .none) (options: @&
      }
    catch exception =>
      return .error $ errorI "typing" (← exception.toMessageData.toString)
-  runTermElabM termElabM

@[export pantograph_goal_start_expr_m]
 def goalStartExpr (expr: String): Lean.CoreM (Protocol.CR GoalState) :=
-  let termElabM: Lean.Elab.TermElabM _ := do
+  runTermElabM do
    let expr ← match ← parseElabType expr with
      | .error e => return .error e
      | .ok expr => pure $ expr
    return .ok $ ← GoalState.create expr
-  runTermElabM termElabM

@[export pantograph_goal_tactic_m]
 def goalTactic (state: GoalState) (goalId: Nat) (tactic: String): Lean.CoreM TacticResult :=
-  runTermElabM <| GoalState.execute state goalId tactic
+  runTermElabM <| state.tryTactic goalId tactic

-@[export pantograph_goal_try_assign_m]
-def goalTryAssign (state: GoalState) (goalId: Nat) (expr: String): Lean.CoreM TacticResult :=
-  runTermElabM <| GoalState.tryAssign state goalId expr
+@[export pantograph_goal_assign_m]
+def goalAssign (state: GoalState) (goalId: Nat) (expr: String): Lean.CoreM TacticResult :=
+  runTermElabM <| state.tryAssign goalId expr

-@[export pantograph_goal_continue]
-def goalContinue (target: GoalState) (branch: GoalState): Except String GoalState :=
-  target.continue branch
+@[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_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)

+@[export pantograph_goal_continue]
+def goalContinue (target: GoalState) (branch: GoalState): Except String GoalState :=
+  target.continue branch
+
@[export pantograph_goal_serialize_m]
 def goalSerialize (state: GoalState) (options: @&Protocol.Options): Lean.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 := do
-  let metaM := do
+def goalPrint (state: GoalState) (options: @&Protocol.Options): Lean.CoreM Protocol.GoalPrintResult :=
+  runMetaM do
    state.restoreMetaM
    return {
      root? := ← state.rootExpr?.mapM (λ expr => do
@ -190,7 +208,6 @@ def goalPrint (state: GoalState) (options: @&Protocol.Options): Lean.CoreM Proto
      parent? := ← state.parentExpr?.mapM (λ expr => do
        serialize_expression options (← unfoldAuxLemmas expr)),
    }
-  runMetaM metaM


 end Pantograph
--- a/Pantograph/Protocol.lean
+++ b/Pantograph/Protocol.lean
@ -209,6 +209,14 @@ structure GoalTactic where
  -- One of the fields here must be filled
  tactic?: Option String := .none
  expr?: Option String := .none
+  have?: Option String := .none
+  calc?: Option String := .none
+  -- true to enter `conv`, `false` to exit. In case of exit the `goalId` is ignored.
+  conv?: Option Bool := .none
+
+  -- In case of the `have` tactic, the new free variable name is provided here
+  binderName?: Option String := .none
+
  deriving Lean.FromJson
 structure GoalTacticResult where
  -- The next goal state id. Existence of this field shows success
--- a/Pantograph/Serial.lean
+++ b/Pantograph/Serial.lean
@ -254,9 +254,7 @@ protected def GoalState.serializeGoals
    MetaM (Array Protocol.Goal):= do
  state.restoreMetaM
  let goals := state.goals.toArray
-  let parentDecl? := parent.bind (λ parentState =>
-    let parentGoal := parentState.goals.get! state.parentGoalId
-    parentState.mctx.findDecl? parentGoal)
+  let parentDecl? := parent.bind (λ parentState => parentState.mctx.findDecl? state.parentMVar?.get!)
  goals.mapM fun goal => do
    match state.mctx.findDecl? goal with
    | .some mvarDecl =>
--- a/README.md
+++ b/README.md
@ -81,7 +81,12 @@ See `Pantograph/Protocol.lean` for a description of the parameters and return va
  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>]}`: Start a new goal from a given expression or symbol
- `goal.tactic {"stateId": <id>, "goalId": <id>, ["tactic": <tactic>], ["expr": <expr>]}`: Execute a tactic string on a given goal
+- `goal.tactic {"stateId": <id>, "goalId": <id>, ["tactic": <tactic>], ["expr":
+  <expr>]}`: Execute a tactic string on a given goal. `tactic` executes an
+  ordinary tactic, `expr` assigns an expression to the current goal, `have`
+  executes the have tactic, ``calc` (of the form `lhs op rhs`) executes one step
+  of `calc`, and `"conv": true`/`"conv": false` enters/exits conversion tactic
+  mode.
 - `goal.continue {"stateId": <id>, ["branch": <id>], ["goals": <names>]}`: Continue from a proof state
 - `goal.remove {"stateIds": [<id>]}"`: Remove a bunch of stored goals.
 - `goal.print {"stateId": <id>}"`: Print a goal state
--- a/Test/Common.lean
+++ b/Test/Common.lean
@ -37,6 +37,7 @@ def TacticResult.toString : TacticResult → String
    s!".failure {messages}"
  | .parseError error => s!".parseError {error}"
  | .indexError index => s!".indexError {index}"
+  | .invalidAction error => s!".invalidAction {error}"

 namespace Test

--- a/Test/Metavar.lean
+++ b/Test/Metavar.lean
@ -8,7 +8,7 @@ namespace Pantograph.Test.Metavar
 open Pantograph
 open Lean

-abbrev TestM := StateRefT LSpec.TestSeq (ReaderT Protocol.Options M)
+abbrev TestM := StateRefT LSpec.TestSeq (ReaderT Protocol.Options Elab.TermElabM)

 def addTest (test: LSpec.TestSeq): TestM Unit := do
  set $ (← get) ++ test
@ -84,7 +84,7 @@ def test_m_couple: TestM Unit := do
      addTest $ assertUnreachable "Goal could not parse"
      return ()

-  let state1 ← match ← state0.execute (goalId := 0) (tactic := "apply Nat.le_trans") with
+  let state1 ← match ← state0.tryTactic (goalId := 0) (tactic := "apply Nat.le_trans") with
    | .success state => pure state
    | other => do
      addTest $ assertUnreachable $ other.toString
@ -93,7 +93,7 @@ def test_m_couple: TestM Unit := do
    #[.some "2 ≤ ?m", .some "?m ≤ 5", .some "Nat"])
  addTest $ LSpec.test "(1 root)" state1.rootExpr?.isNone
  -- Set m to 3
-  let state2 ← match ← state1.execute (goalId := 2) (tactic := "exact 3") with
+  let state2 ← match ← state1.tryTactic (goalId := 2) (tactic := "exact 3") with
    | .success state => pure state
    | other => do
      addTest $ assertUnreachable $ other.toString
@ -116,14 +116,14 @@ def test_m_couple_simp: TestM Unit := do
      addTest $ assertUnreachable "Goal could not parse"
      return ()

-  let state1 ← match ← state0.execute (goalId := 0) (tactic := "apply Nat.le_trans") with
+  let state1 ← match ← state0.tryTactic (goalId := 0) (tactic := "apply Nat.le_trans") with
    | .success state => pure state
    | other => do
      addTest $ assertUnreachable $ other.toString
      return ()
  addTest $ LSpec.check "apply Nat.le_trans" ((← state1.serializeGoals (options := ← read)).map (·.target.pp?) =
    #[.some "2 ≤ ?m", .some "?m ≤ 5", .some "Nat"])
-  let state2 ← match ← state1.execute (goalId := 2) (tactic := "exact 2") with
+  let state2 ← match ← state1.tryTactic (goalId := 2) (tactic := "exact 2") with
    | .success state => pure state
    | other => do
      addTest $ assertUnreachable $ other.toString
@ -137,7 +137,7 @@ def test_m_couple_simp: TestM Unit := do
  addTest $ LSpec.check "exact 2" ((← state1b.serializeGoals (options := ← read)).map (·.target.pp?) =
    #[.some "2 ≤ 2", .some "2 ≤ 5"])
  addTest $ LSpec.test "(2 root)" state1b.rootExpr?.isNone
-  let state3 ← match ← state1b.execute (goalId := 0) (tactic := "simp") with
+  let state3 ← match ← state1b.tryTactic (goalId := 0) (tactic := "simp") with
    | .success state => pure state
    | other => do
      addTest $ assertUnreachable $ other.toString
@ -147,7 +147,7 @@ def test_m_couple_simp: TestM Unit := do
      addTest $ assertUnreachable $ msg
      return ()
    | .ok state => pure state
-  let state5 ← match ← state4.execute (goalId := 0) (tactic := "simp") with
+  let state5 ← match ← state4.tryTactic (goalId := 0) (tactic := "simp") with
    | .success state => pure state
    | other => do
      addTest $ assertUnreachable $ other.toString
@ -174,7 +174,7 @@ def test_proposition_generation: TestM Unit := do
      addTest $ assertUnreachable "Goal could not parse"
      return ()

-  let state1 ← match ← state0.execute (goalId := 0) (tactic := "apply PSigma.mk") with
+  let state1 ← match ← state0.tryTactic (goalId := 0) (tactic := "apply PSigma.mk") with
    | .success state => pure state
    | other => do
      addTest $ assertUnreachable $ other.toString
@ -216,7 +216,7 @@ def test_partial_continuation: TestM Unit := do
      addTest $ assertUnreachable "Goal could not parse"
      return ()

-  let state1 ← match ← state0.execute (goalId := 0) (tactic := "apply Nat.le_trans") with
+  let state1 ← match ← state0.tryTactic (goalId := 0) (tactic := "apply Nat.le_trans") with
    | .success state => pure state
    | other => do
      addTest $ assertUnreachable $ other.toString
@ -224,7 +224,7 @@ def test_partial_continuation: TestM Unit := do
  addTest $ LSpec.check "apply Nat.le_trans" ((← state1.serializeGoals (options := ← read)).map (·.target.pp?) =
    #[.some "2 ≤ ?m", .some "?m ≤ 5", .some "Nat"])

-  let state2 ← match ← state1.execute (goalId := 2) (tactic := "apply Nat.succ") with
+  let state2 ← match ← state1.tryTactic (goalId := 2) (tactic := "apply Nat.succ") with
    | .success state => pure state
    | other => do
      addTest $ assertUnreachable $ other.toString
--- a/Test/Proofs.lean
+++ b/Test/Proofs.lean
@ -14,7 +14,7 @@ inductive Start where
  | copy (name: String) -- Start from some name in the environment
  | expr (expr: String) -- Start from some expression

-abbrev TestM := StateRefT LSpec.TestSeq (ReaderT Protocol.Options M)
+abbrev TestM := StateRefT LSpec.TestSeq (ReaderT Protocol.Options Elab.TermElabM)

 def addTest (test: LSpec.TestSeq): TestM Unit := do
  set $ (← get) ++ test
@ -75,7 +75,7 @@ def proofRunner (env: Lean.Environment) (tests: TestM Unit): IO LSpec.TestSeq :=
 example: ∀ (a b: Nat), a + b = b + a := by
  intro n m
  rw [Nat.add_comm]
-def proof_nat_add_comm (manual: Bool): TestM Unit := do
+def test_nat_add_comm (manual: Bool): TestM Unit := do
  let state? ← startProof <| match manual with
    | false => .copy "Nat.add_comm"
    | true => .expr "∀ (a b: Nat), a + b = b + a"
@ -86,7 +86,7 @@ def proof_nat_add_comm (manual: Bool): TestM Unit := do
      addTest $ assertUnreachable "Goal could not parse"
      return ()

-  let state1 ← match ← state0.execute (goalId := 0) (tactic := "intro n m") with
+  let state1 ← match ← state0.tryTactic (goalId := 0) (tactic := "intro n m") with
    | .success state => pure state
    | other => do
      addTest $ assertUnreachable $ other.toString
@ -94,13 +94,13 @@ def proof_nat_add_comm (manual: Bool): TestM Unit := do
  addTest $ LSpec.check "intro n m" ((← state1.serializeGoals (options := ← read)).map (·.devolatilize) =
    #[buildGoal [("n", "Nat"), ("m", "Nat")] "n + m = m + n"])

-  match ← state1.execute (goalId := 0) (tactic := "assumption") with
+  match ← state1.tryTactic (goalId := 0) (tactic := "assumption") with
  | .failure #[message] =>
    addTest $ LSpec.check "assumption" (message = "tactic 'assumption' failed\nn m : Nat\n⊢ n + m = m + n")
  | other => do
    addTest $ assertUnreachable $ other.toString

-  let state2 ← match ← state1.execute (goalId := 0) (tactic := "rw [Nat.add_comm]") with
+  let state2 ← match ← state1.tryTactic (goalId := 0) (tactic := "rw [Nat.add_comm]") with
    | .success state => pure state
    | other => do
      addTest $ assertUnreachable $ other.toString
@ -108,7 +108,7 @@ def proof_nat_add_comm (manual: Bool): TestM Unit := do
  addTest $ LSpec.test "rw [Nat.add_comm]" state2.goals.isEmpty

  return ()
-def proof_delta_variable: TestM Unit := do
+def test_delta_variable: TestM Unit := do
  let options: Protocol.Options := { noRepeat := true }
  let state? ← startProof <| .expr "∀ (a b: Nat), a + b = b + a"
  addTest $ LSpec.check "Start goal" state?.isSome
@ -118,14 +118,14 @@ def proof_delta_variable: TestM Unit := do
      addTest $ assertUnreachable "Goal could not parse"
      return ()

-  let state1 ← match ← state0.execute (goalId := 0) (tactic := "intro n") with
+  let state1 ← match ← state0.tryTactic (goalId := 0) (tactic := "intro n") with
    | .success state => pure state
    | other => do
      addTest $ assertUnreachable $ other.toString
      return ()
  addTest $ LSpec.check "intro n" ((← state1.serializeGoals (parent := state0) options).map (·.devolatilize) =
    #[buildGoalSelective [("n", .some "Nat")] "∀ (b : Nat), n + b = b + n"])
-  let state2 ← match ← state1.execute (goalId := 0) (tactic := "intro m") with
+  let state2 ← match ← state1.tryTactic (goalId := 0) (tactic := "intro m") with
    | .success state => pure state
    | other => do
      addTest $ assertUnreachable $ other.toString
@ -149,7 +149,7 @@ example (w x y z : Nat) (p : Nat → Prop)
        (h : p (x * y + z * w * x)) : p (x * w * z + y * x) := by
  simp [Nat.add_assoc, Nat.add_comm, Nat.add_left_comm, Nat.mul_comm, Nat.mul_assoc, Nat.mul_left_comm] at *
  assumption
-def proof_arith: TestM Unit := do
+def test_arith: TestM Unit := do
  let state? ← startProof (.expr "∀ (w x y z : Nat) (p : Nat → Prop) (h : p (x * y + z * w * x)), p (x * w * z + y * x)")
  let state0 ← match state? with
    | .some state => pure state
@ -157,26 +157,28 @@ def proof_arith: TestM Unit := do
      addTest $ assertUnreachable "Goal could not parse"
      return ()

-  let state1 ← match ← state0.execute (goalId := 0) (tactic := "intros") with
+  let tactic := "intros"
+  let state1 ← match ← state0.tryTactic (goalId := 0) (tactic := tactic) with
    | .success state => pure state
    | other => do
      addTest $ assertUnreachable $ other.toString
      return ()
-  addTest $ LSpec.check "intros" (state1.goals.length = 1)
+  addTest $ LSpec.check tactic (state1.goals.length = 1)
  addTest $ LSpec.test "(1 root)" state1.rootExpr?.isNone
-  let state2 ← match ← state1.execute (goalId := 0) (tactic := "simp [Nat.add_assoc, Nat.add_comm, Nat.add_left_comm, Nat.mul_comm, Nat.mul_assoc, Nat.mul_left_comm] at *") with
+  let state2 ← match ← state1.tryTactic (goalId := 0) (tactic := "simp [Nat.add_assoc, Nat.add_comm, Nat.add_left_comm, Nat.mul_comm, Nat.mul_assoc, Nat.mul_left_comm] at *") with
    | .success state => pure state
    | other => do
      addTest $ assertUnreachable $ other.toString
      return ()
  addTest $ LSpec.check "simp ..." (state2.goals.length = 1)
  addTest $ LSpec.check "(2 root)" state2.rootExpr?.isNone
-  let state3 ← match ← state2.execute (goalId := 0) (tactic := "assumption") with
+  let tactic := "assumption"
+  let state3 ← match ← state2.tryTactic (goalId := 0) (tactic := tactic) with
    | .success state => pure state
    | other => do
      addTest $ assertUnreachable $ other.toString
      return ()
-  addTest $ LSpec.test "assumption" state3.goals.isEmpty
+  addTest $ LSpec.test tactic state3.goals.isEmpty
  addTest $ LSpec.check "(3 root)" state3.rootExpr?.isSome
  return ()

@ -195,7 +197,7 @@ example: ∀ (p q: Prop), p ∨ q → q ∨ p := by
    assumption
  . apply Or.inl
    assumption
-def proof_or_comm: TestM Unit := do
+def test_or_comm: TestM Unit := do
  let state? ← startProof (.expr "∀ (p q: Prop), p ∨ q → q ∨ p")
  let state0 ← match state? with
    | .some state => pure state
@ -205,21 +207,24 @@ def proof_or_comm: TestM Unit := do
  addTest $ LSpec.check "(0 parent)" state0.parentExpr?.isNone
  addTest $ LSpec.check "(0 root)" state0.rootExpr?.isNone

-  let state1 ← match ← state0.execute (goalId := 0) (tactic := "intro p q h") with
+  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 "intro n m" ((← state1.serializeGoals (options := ← read)).map (·.devolatilize) =
+  addTest $ LSpec.check tactic ((← state1.serializeGoals (options := ← read)).map (·.devolatilize) =
    #[buildGoal [("p", "Prop"), ("q", "Prop"), ("h", "p ∨ q")] "q ∨ p"])
  addTest $ LSpec.check "(1 parent)" state1.parentExpr?.isSome
  addTest $ LSpec.check "(1 root)" state1.rootExpr?.isNone
-  let state2 ← match ← state1.execute (goalId := 0) (tactic := "cases h") with
+
+  let tactic := "cases h"
+  let state2 ← match ← state1.tryTactic (goalId := 0) (tactic := tactic) with
    | .success state => pure state
    | other => do
      addTest $ assertUnreachable $ other.toString
      return ()
-  addTest $ LSpec.check "cases h" ((← state2.serializeGoals (options := ← read)).map (·.devolatilize) =
+  addTest $ LSpec.check tactic ((← state2.serializeGoals (options := ← read)).map (·.devolatilize) =
    #[branchGoal "inl" "p", branchGoal "inr" "q"])
  addTest $ LSpec.check "(2 parent)" state2.parentExpr?.isSome
  addTest $ LSpec.check "(2 root)" state2.rootExpr?.isNone
@ -229,7 +234,7 @@ def proof_or_comm: TestM Unit := do
  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)))")

-  let state3_1 ← match ← state2.execute (goalId := 0) (tactic := "apply Or.inr") with
+  let state3_1 ← match ← state2.tryTactic (goalId := 0) (tactic := "apply Or.inr") with
    | .success state => pure state
    | other => do
      addTest $ assertUnreachable $ other.toString
@ -237,7 +242,7 @@ def proof_or_comm: TestM Unit := do
  let state3_1parent ← serialize_expression_ast 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))")
  addTest $ LSpec.check "· apply Or.inr" (state3_1.goals.length = 1)
-  let state4_1 ← match ← state3_1.execute (goalId := 0) (tactic := "assumption") with
+  let state4_1 ← match ← state3_1.tryTactic (goalId := 0) (tactic := "assumption") with
    | .success state => pure state
    | other => do
      addTest $ assertUnreachable $ other.toString
@ -246,13 +251,13 @@ def proof_or_comm: TestM Unit := do
  let state4_1parent ← serialize_expression_ast state4_1.parentExpr?.get! (sanitize := false)
  addTest $ LSpec.test "(4_1 parent)" (state4_1parent == "(:fv _uniq.47)")
  addTest $ LSpec.check "(4_1 root)" state4_1.rootExpr?.isNone
-  let state3_2 ← match ← state2.execute (goalId := 1) (tactic := "apply Or.inl") with
+  let state3_2 ← match ← state2.tryTactic (goalId := 1) (tactic := "apply Or.inl") with
    | .success state => pure state
    | other => do
      addTest $ assertUnreachable $ other.toString
      return ()
  addTest $ LSpec.check "· apply Or.inl" (state3_2.goals.length = 1)
-  let state4_2 ← match ← state3_2.execute (goalId := 0) (tactic := "assumption") with
+  let state4_2 ← match ← state3_2.tryTactic (goalId := 0) (tactic := "assumption") with
    | .success state => pure state
    | other => do
      addTest $ assertUnreachable $ other.toString
@ -266,13 +271,13 @@ def proof_or_comm: TestM Unit := do
      return ()
    | .ok state => pure state
  addTest $ LSpec.test "(resume)" (state2b.goals == [state2.goals.get! 0])
-  let state3_1 ← match ← state2b.execute (goalId := 0) (tactic := "apply Or.inr") with
+  let state3_1 ← match ← state2b.tryTactic (goalId := 0) (tactic := "apply Or.inr") with
    | .success state => pure state
    | other => do
      addTest $ assertUnreachable $ other.toString
      return ()
  addTest $ LSpec.check "· apply Or.inr" (state3_1.goals.length = 1)
-  let state4_1 ← match ← state3_1.execute (goalId := 0) (tactic := "assumption") with
+  let state4_1 ← match ← state3_1.tryTactic (goalId := 0) (tactic := "assumption") with
    | .success state => pure state
    | other => do
      addTest $ assertUnreachable $ other.toString
@ -293,14 +298,268 @@ def proof_or_comm: TestM Unit := do
      ]
    }

+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 =>
+    lhs
+    congr
+    . rw [Nat.add_comm]
+    . rfl
+  exact h
+
+def test_conv: TestM Unit := do
+  let state? ← startProof (.expr "∀ (a b c1 c2: Nat), (b + a) + c1 = (b + a) + c2 → (a + b) + c1 = (b + a) + c2")
+  let state0 ← match state? with
+    | .some state => pure state
+    | .none => do
+      addTest $ assertUnreachable "Goal could not parse"
+      return ()
+
+  let tactic := "intro a b c1 c2 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 [] "a + b + c1 = b + a + c2"])
+
+  let state2 ← match ← state1.conv (goalId := 0) with
+    | .success state => pure state
+    | other => do
+      addTest $ assertUnreachable $ other.toString
+      return ()
+  addTest $ LSpec.check "conv => ..." ((← state2.serializeGoals (options := ← read)).map (·.devolatilize) =
+    #[{ interiorGoal [] "a + b + c1 = b + a + c2" with isConversion := true }])
+
+  let convTactic := "rhs"
+  let state3R ← match ← state2.tryTactic (goalId := 0) convTactic with
+    | .success state => pure state
+    | other => do
+      addTest $ assertUnreachable $ other.toString
+      return ()
+  addTest $ LSpec.check s!"  {convTactic} (discard)" ((← state3R.serializeGoals (options := ← read)).map (·.devolatilize) =
+    #[{ interiorGoal [] "b + a + c2" with isConversion := true }])
+
+  let convTactic := "lhs"
+  let state3L ← match ← state2.tryTactic (goalId := 0) convTactic with
+    | .success state => pure state
+    | other => do
+      addTest $ assertUnreachable $ other.toString
+      return ()
+  addTest $ LSpec.check s!"  {convTactic}" ((← state3L.serializeGoals (options := ← read)).map (·.devolatilize) =
+    #[{ interiorGoal [] "a + b + c1" with isConversion := true }])
+
+  let convTactic := "congr"
+  let state4 ← match ← state3L.tryTactic (goalId := 0) convTactic with
+    | .success state => pure state
+    | other => do
+      addTest $ assertUnreachable $ other.toString
+      return ()
+  addTest $ LSpec.check s!"  {convTactic}" ((← state4.serializeGoals (options := ← read)).map (·.devolatilize) =
+    #[
+      { interiorGoal [] "a + b" with isConversion := true, userName? := .some "a" },
+      { interiorGoal [] "c1" with isConversion := true, userName? := .some "a" }
+    ])
+
+  let convTactic := "rw [Nat.add_comm]"
+  let state5_1 ← match ← state4.tryTactic (goalId := 0) convTactic with
+    | .success state => pure state
+    | other => do
+      addTest $ assertUnreachable $ other.toString
+      return ()
+  addTest $ LSpec.check s!"  · {convTactic}" ((← state5_1.serializeGoals (options := ← read)).map (·.devolatilize) =
+    #[{ interiorGoal [] "b + a" with isConversion := true, userName? := .some "a" }])
+
+  let convTactic := "rfl"
+  let state6_1 ← match ← state5_1.tryTactic (goalId := 0) convTactic with
+    | .success state => pure state
+    | other => do
+      addTest $ assertUnreachable $ other.toString
+      return ()
+  addTest $ LSpec.check s!"    {convTactic}" ((← state6_1.serializeGoals (options := ← read)).map (·.devolatilize) =
+    #[])
+
+  let state4_1 ← match state6_1.continue state4 with
+    | .ok state => pure state
+    | .error e => do
+      addTest $ expectationFailure "continue" e
+      return ()
+
+  let convTactic := "rfl"
+  let state6 ← match ← state4_1.tryTactic (goalId := 0) convTactic with
+    | .success state => pure state
+    | other => do
+      addTest $ assertUnreachable $ other.toString
+      return ()
+  addTest $ LSpec.check s!"  · {convTactic}" ((← state6.serializeGoals (options := ← read)).map (·.devolatilize) =
+    #[])
+
+  let state1_1 ← match ← state6.convExit with
+    | .success state => pure state
+    | other => do
+      addTest $ assertUnreachable $ other.toString
+      return ()
+
+  let tactic := "exact h"
+  let stateF ← match ← state1_1.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)).map (·.devolatilize) =
+    #[])
+
+  where
+    h := "b + a + c1 = b + a + c2"
+    interiorGoal (free: List (String × String)) (target: String) :=
+      let free := [("a", "Nat"), ("b", "Nat"), ("c1", "Nat"), ("c2", "Nat"), ("h", h)] ++ free
+      buildGoal free target
+
+example : ∀ (a b c d: Nat), a + b = b + c → b + c = c + d → a + b = c + d := by
+  intro a b c d h1 h2
+  calc a + b = b + c := by apply h1
+    _ = c + d := by apply h2
+
+def test_calc: TestM Unit := do
+  let state? ← startProof (.expr "∀ (a b c d: Nat), a + b = b + c → b + c = c + d → a + b = c + d")
+  let state0 ← match state? with
+    | .some state => pure state
+    | .none => do
+      addTest $ assertUnreachable "Goal could not parse"
+      return ()
+  let tactic := "intro a b c d h1 h2"
+  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 [] "a + b = c + d"])
+  let pred := "a + b = b + c"
+  let state2 ← match ← state1.tryCalc (goalId := 0) (pred := pred) with
+    | .success state => pure state
+    | other => do
+      addTest $ assertUnreachable $ other.toString
+      return ()
+  addTest $ LSpec.check s!"calc {pred} := _" ((← state2.serializeGoals (options := ← read)).map (·.devolatilize) =
+    #[
+      interiorGoal [] "a + b = b + c" (.some "calc"),
+      interiorGoal [] "b + c = c + d"
+    ])
+
+  let tactic := "apply h1"
+  let state2m ← match ← state2.tryTactic (goalId := 0) (tactic := tactic) with
+    | .success state => pure state
+    | other => do
+      addTest $ assertUnreachable $ other.toString
+      return ()
+  let state3 ← match state2m.continue state2 with
+    | .ok state => pure state
+    | .error e => do
+      addTest $ expectationFailure "continue" e
+      return ()
+  let pred := "_ = c + d"
+  let state4 ← match ← state3.tryCalc (goalId := 0) (pred := pred) with
+    | .success state => pure state
+    | other => do
+      addTest $ assertUnreachable $ other.toString
+      return ()
+  addTest $ LSpec.check s!"calc {pred} := _" ((← state4.serializeGoals (options := ← read)).map (·.devolatilize) =
+    #[
+      interiorGoal [] "b + c = c + d" (.some "calc")
+    ])
+  let tactic := "apply h2"
+  let state4m ← match ← state4.tryTactic (goalId := 0) (tactic := tactic) with
+    | .success state => pure state
+    | other => do
+      addTest $ assertUnreachable $ other.toString
+      return ()
+  addTest $ LSpec.test "(4m root)" state4m.rootExpr?.isSome
+
+
+  where
+    interiorGoal (free: List (String × String)) (target: String) (userName?: Option String := .none) :=
+      let free := [("a", "Nat"), ("b", "Nat"), ("c", "Nat"), ("d", "Nat"),
+        ("h1", "a + b = b + c"), ("h2", "b + c = c + d")] ++ free
+      buildGoal free target userName?
+
 def suite (env: Environment): List (String × IO LSpec.TestSeq) :=
  let tests := [
-    ("Nat.add_comm", proof_nat_add_comm false),
-    ("Nat.add_comm manual", proof_nat_add_comm true),
-    ("Nat.add_comm delta", proof_delta_variable),
-    ("arithmetic", proof_arith),
-    ("Or.comm", proof_or_comm)
+    ("Nat.add_comm", test_nat_add_comm false),
+    ("Nat.add_comm manual", test_nat_add_comm true),
+    ("Nat.add_comm delta", test_delta_variable),
+    ("arithmetic", test_arith),
+    ("Or.comm", test_or_comm),
+    ("have", test_have),
+    ("conv", test_conv),
+    ("calc", test_calc),
  ]
  tests.map (fun (name, test) => (name, proofRunner env test))

+
+
 end Pantograph.Test.Proofs