From b954f12526eb6eca25d1f77c5b2729ad23b447a3 Mon Sep 17 00:00:00 2001
From: Leni Aniva <v@leni.sh>
Date: Sat, 13 Apr 2024 19:41:49 -0700
Subject: [PATCH 01/38] refactor: Move all tactic operations to the bottom

---
 Pantograph/Goal.lean | 127 ++++++++++++++++++++++---------------------
 1 file changed, 64 insertions(+), 63 deletions(-)

diff --git a/Pantograph/Goal.lean b/Pantograph/Goal.lean
index 484ff51..c6700b6 100644
--- a/Pantograph/Goal.lean
+++ b/Pantograph/Goal.lean
@@ -80,6 +80,70 @@ private def newMVarSet (mctxOld: @&MetavarContext) (mctxNew: @&MetavarContext):
       acc.insert mvarId
     ) SSet.empty
 
+
+protected def GoalState.focus (state: GoalState) (goalId: Nat): Option GoalState := do
+  let goal ← state.savedState.tactic.goals.get? goalId
+  return {
+    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
+
+--- Tactic execution functions ---
+
 /-- 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
@@ -446,67 +510,4 @@ protected def GoalState.tryCalc (state: GoalState) (goalId: Nat) (pred: String):
   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
--/
-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
-
-
 end Pantograph

From 75b4648ba9d53e7032c1196b55e92483ca761a24 Mon Sep 17 00:00:00 2001
From: Leni Aniva <v@leni.sh>
Date: Sun, 14 Apr 2024 15:40:57 -0700
Subject: [PATCH 02/38] feat: mapply stub

---
 Pantograph/Goal.lean | 66 ++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 66 insertions(+)

diff --git a/Pantograph/Goal.lean b/Pantograph/Goal.lean
index c6700b6..176e48e 100644
--- a/Pantograph/Goal.lean
+++ b/Pantograph/Goal.lean
@@ -252,6 +252,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)
@@ -275,6 +276,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)
@@ -324,6 +326,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)
@@ -369,6 +372,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
 
@@ -452,6 +456,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
@@ -510,4 +515,65 @@ protected def GoalState.tryCalc (state: GoalState) (goalId: Nat) (pred: String):
   catch exception =>
     return .failure #[← exception.toMessageData.toString]
 
+def getForallArgsBody: Expr → List Expr × Expr
+  | .forallE _ d b _ =>
+    let (innerArgs, innerBody) := getForallArgsBody b
+    (d :: innerArgs, innerBody)
+  | e => ([], e)
+def collectMotiveArguments (forallBody: Expr): SSet Nat :=
+  -- Get all de Bruijn indices
+  Id.run $ do
+    Expr.foldlM (λ acc subexpr => do
+      match subexpr with
+      | .app (.bvar i) _ => return acc.insert i
+      | _ => return acc
+      ) SSet.empty forallBody
+
+protected def GoalState.tryMotivatedApply (state: GoalState) (goalId: Nat) (recursor: 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.tryMotivatedApply
+
+  let recursor ← match Parser.runParserCategory
+    (env := state.env)
+    (catName := `term)
+    (input := recursor)
+    (fileName := filename) with
+    | .ok syn => pure syn
+    | .error error => return .parseError error
+  try
+    -- Implemented similarly to the intro tactic
+    let nextGoals: List MVarId ← goal.withContext do
+      let recursor ← Elab.Term.elabType (stx := recursor)
+      let recursorType ← Meta.inferType recursor
+
+      let (forallArgs, forallBody) := getForallArgsBody recursorType
+      let motiveIndices := collectMotiveArguments forallBody
+
+      let numArgs ← Meta.getExpectedNumArgs recursorType
+
+      let rec go (i: Nat): MetaM (List MVarId × Expr) := do
+        let argType := forallArgs.get! i
+        sorry
+      let (newMVars, assign) ← go numArgs
+
+      goal.assign assign
+
+      pure newMVars
+    return .success {
+      root := state.root,
+      savedState := {
+        term := ← MonadBacktrack.saveState,
+        tactic := { goals := nextGoals }
+      },
+      newMVars := nextGoals.toSSet,
+      parentMVar? := .some goal,
+      calcPrevRhs? := .none
+    }
+  catch exception =>
+    return .failure #[← exception.toMessageData.toString]
+
 end Pantograph

From dbd54f767938027c43427a0eb90245ccc420e26d Mon Sep 17 00:00:00 2001
From: Leni Aniva <v@leni.sh>
Date: Mon, 15 Apr 2024 12:47:02 -0700
Subject: [PATCH 03/38] feat: Implement the mapply tactic

---
 Pantograph/Goal.lean | 24 ++++++++----
 Test/Common.lean     | 11 ++++--
 Test/Proofs.lean     | 87 +++++++++++++++++++++++++++++++++++++++++++-
 3 files changed, 111 insertions(+), 11 deletions(-)

diff --git a/Pantograph/Goal.lean b/Pantograph/Goal.lean
index 176e48e..0fdf2e1 100644
--- a/Pantograph/Goal.lean
+++ b/Pantograph/Goal.lean
@@ -547,7 +547,7 @@ protected def GoalState.tryMotivatedApply (state: GoalState) (goalId: Nat) (recu
   try
     -- Implemented similarly to the intro tactic
     let nextGoals: List MVarId ← goal.withContext do
-      let recursor ← Elab.Term.elabType (stx := recursor)
+      let recursor ← Elab.Term.elabTerm (stx := recursor) .none
       let recursorType ← Meta.inferType recursor
 
       let (forallArgs, forallBody) := getForallArgsBody recursorType
@@ -555,14 +555,24 @@ protected def GoalState.tryMotivatedApply (state: GoalState) (goalId: Nat) (recu
 
       let numArgs ← Meta.getExpectedNumArgs recursorType
 
-      let rec go (i: Nat): MetaM (List MVarId × Expr) := do
-        let argType := forallArgs.get! i
-        sorry
-      let (newMVars, assign) ← go numArgs
+      let rec go (i: Nat) (prev: Array Expr): MetaM (Array Expr) := do
+        if i ≥ numArgs then
+          return prev
+        else
+          let argType := forallArgs.get! i
+          -- If `argType` has motive references, its goal needs to be placed in it
+          let argType := argType.instantiateRev prev
+          -- Create the goal
+          let argGoal ← Meta.mkFreshExprMVar argType .natural .anonymous
+          let prev :=  prev ++ [argGoal]
+          go (i + 1) prev
+        termination_by numArgs - i
+      let newMVars ← go 0 #[]
 
-      goal.assign assign
+      -- Create the main goal for the return type of the recursor
+      goal.assign (mkAppN recursor newMVars)
 
-      pure newMVars
+      pure $ newMVars.toList.map (·.mvarId!)
     return .success {
       root := state.root,
       savedState := {
diff --git a/Test/Common.lean b/Test/Common.lean
index 8719ebd..8b8e977 100644
--- 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,13 @@ 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 Expression
 deriving instance DecidableEq, Repr for Variable
 deriving instance DecidableEq, Repr for Goal
diff --git a/Test/Proofs.lean b/Test/Proofs.lean
index e14ba4a..ae94054 100644
--- a/Test/Proofs.lean
+++ b/Test/Proofs.lean
@@ -49,6 +49,16 @@ def startProof (start: Start): TestM (Option GoalState) := do
         let goal ← GoalState.create (expr := expr)
         return Option.some goal
 
+def buildNamedGoal (name: String) (nameType: List (String × String)) (target: String): Protocol.Goal :=
+  {
+    name,
+    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?,
@@ -582,7 +592,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,6 +635,80 @@ 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.70" [("n", "Nat")] "Nat → Sort ?u.66",
+      buildNamedGoal "_uniq.71" [("n", "Nat")] "Nat",
+      buildNamedGoal "_uniq.72" [("n", "Nat")] "(t : Nat) → Nat.below t → ?m.70 t"
+    ])
+
+  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 stateF ← match ← state3.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)) =
+    #[])
+
+  addTest $ LSpec.check "(F root)" stateF.rootExpr?.isSome
+
 def suite (env: Environment): List (String × IO LSpec.TestSeq) :=
   let tests := [
     ("Nat.add_comm", test_nat_add_comm false),
@@ -637,6 +721,7 @@ 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),
   ]
   tests.map (fun (name, test) => (name, proofRunner env test))
 

From 7aa7e6d7e948a22cec20a259c4f244f11711be65 Mon Sep 17 00:00:00 2001
From: Leni Aniva <v@leni.sh>
Date: Mon, 15 Apr 2024 12:56:28 -0700
Subject: [PATCH 04/38] feat: Library interface for mapply

---
 Pantograph/Library.lean | 58 +++++++++++++++++++----------------------
 1 file changed, 27 insertions(+), 31 deletions(-)

diff --git a/Pantograph/Library.lean b/Pantograph/Library.lean
index 6b8e2e2..01b5a42 100644
--- a/Pantograph/Library.lean
+++ b/Pantograph/Library.lean
@@ -158,37 +158,6 @@ def goalStartExpr (expr: String): Lean.CoreM (Protocol.CR GoalState) :=
       | .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)
@@ -212,5 +181,32 @@ def goalPrint (state: GoalState) (options: @&Protocol.Options): Lean.CoreM Proto
         serializeExpression options (← unfoldAuxLemmas 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_motivated_apply_m]
+def goalMotivatedApply (state: GoalState) (goalId: Nat) (recursor: String): Lean.CoreM TacticResult :=
+  runTermElabM <| state.tryMotivatedApply goalId recursor
 
 end Pantograph

From fec13ddb5176323a2878f00be197fa976c5c7e1e Mon Sep 17 00:00:00 2001
From: Leni Aniva <v@leni.sh>
Date: Thu, 18 Apr 2024 14:19:25 -0700
Subject: [PATCH 05/38] chore: Code cleanup

---
 Pantograph/Goal.lean    | 27 +++++++++++++++++----------
 Pantograph/Library.lean |  2 +-
 Test/Proofs.lean        | 11 +++++++----
 3 files changed, 25 insertions(+), 15 deletions(-)

diff --git a/Pantograph/Goal.lean b/Pantograph/Goal.lean
index 0fdf2e1..5c6a583 100644
--- a/Pantograph/Goal.lean
+++ b/Pantograph/Goal.lean
@@ -232,7 +232,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 := {
@@ -521,13 +521,9 @@ def getForallArgsBody: Expr → List Expr × Expr
     (d :: innerArgs, innerBody)
   | e => ([], e)
 def collectMotiveArguments (forallBody: Expr): SSet Nat :=
-  -- Get all de Bruijn indices
-  Id.run $ do
-    Expr.foldlM (λ acc subexpr => do
-      match subexpr with
-      | .app (.bvar i) _ => return acc.insert i
-      | _ => return acc
-      ) SSet.empty forallBody
+  match forallBody with
+  | .app (.bvar i) _ => SSet.empty.insert i
+  | _ => SSet.empty
 
 protected def GoalState.tryMotivatedApply (state: GoalState) (goalId: Nat) (recursor: String):
       Elab.TermElabM TacticResult := do
@@ -552,6 +548,7 @@ protected def GoalState.tryMotivatedApply (state: GoalState) (goalId: Nat) (recu
 
       let (forallArgs, forallBody) := getForallArgsBody recursorType
       let motiveIndices := collectMotiveArguments forallBody
+      --IO.println s!"{motiveIndices.toList} from {← Meta.ppExpr forallBody}"
 
       let numArgs ← Meta.getExpectedNumArgs recursorType
 
@@ -563,16 +560,26 @@ protected def GoalState.tryMotivatedApply (state: GoalState) (goalId: Nat) (recu
           -- If `argType` has motive references, its goal needs to be placed in it
           let argType := argType.instantiateRev prev
           -- Create the goal
-          let argGoal ← Meta.mkFreshExprMVar argType .natural .anonymous
+          let userName := if motiveIndices.contains (numArgs - i - 1) then `motive else .anonymous
+          let argGoal ← Meta.mkFreshExprMVar argType .syntheticOpaque (userName := userName)
+          IO.println s!"Creating [{i}] {← Meta.ppExpr argGoal}"
           let prev :=  prev ++ [argGoal]
           go (i + 1) prev
         termination_by numArgs - i
       let newMVars ← go 0 #[]
 
+      -- FIXME: Add an `Eq` target and swap out the motive type
+
+      --let sourceType := forallBody.instantiateRev newMVars
+      --unless ← withTheReader Meta.Context (λ ctx => { ctx with config := { ctx.config with } }) $
+      --       Meta.isDefEq sourceType (← goal.getType) do
+      --  throwError "invalid mapply: The resultant type {← Meta.ppExpr sourceType} cannot be unified with {← Meta.ppExpr $ ← goal.getType}"
+
       -- Create the main goal for the return type of the recursor
       goal.assign (mkAppN recursor newMVars)
 
-      pure $ newMVars.toList.map (·.mvarId!)
+      let nextGoals ← newMVars.toList.map (·.mvarId!) |>.filterM (not <$> ·.isAssigned)
+      pure nextGoals
     return .success {
       root := state.root,
       savedState := {
diff --git a/Pantograph/Library.lean b/Pantograph/Library.lean
index 01b5a42..00b4bc7 100644
--- a/Pantograph/Library.lean
+++ b/Pantograph/Library.lean
@@ -38,7 +38,7 @@ namespace Pantograph
 
 def defaultTermElabMContext: Lean.Elab.Term.Context := {
     autoBoundImplicit := true,
-    declName? := some "_pantograph".toName,
+    declName? := .some `_pantograph,
     errToSorry := false
   }
 def runMetaM { α } (metaM: Lean.MetaM α): Lean.CoreM α :=
diff --git a/Test/Proofs.lean b/Test/Proofs.lean
index ae94054..1adc9d4 100644
--- a/Test/Proofs.lean
+++ b/Test/Proofs.lean
@@ -49,9 +49,11 @@ def startProof (start: Start): TestM (Option GoalState) := do
         let goal ← GoalState.create (expr := expr)
         return Option.some goal
 
-def buildNamedGoal (name: String) (nameType: List (String × String)) (target: String): 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,
@@ -59,7 +61,8 @@ def buildNamedGoal (name: String) (nameType: List (String × String)) (target: S
       isInaccessible? := .some false
     })).toArray
   }
-def buildGoal (nameType: List (String × String)) (target: String) (userName?: Option String := .none): Protocol.Goal :=
+def buildGoal (nameType: List (String × String)) (target: String) (userName?: Option String := .none):
+    Protocol.Goal :=
   {
     userName?,
     target := { pp? := .some target},
@@ -658,9 +661,9 @@ def test_nat_zero_add: TestM Unit := do
       return ()
   addTest $ LSpec.check s!"mapply {recursor}" ((← state2.serializeGoals (options := ← read)).map (·.devolatilizeVars) =
     #[
-      buildNamedGoal "_uniq.70" [("n", "Nat")] "Nat → Sort ?u.66",
+      buildNamedGoal "_uniq.70" [("n", "Nat")] "Nat → Sort ?u.66" (.some "motive"),
       buildNamedGoal "_uniq.71" [("n", "Nat")] "Nat",
-      buildNamedGoal "_uniq.72" [("n", "Nat")] "(t : Nat) → Nat.below t → ?m.70 t"
+      buildNamedGoal "_uniq.72" [("n", "Nat")] "(t : Nat) → Nat.below t → ?motive t"
     ])
 
   let tactic := "exact n"

From 398b1c39edd070d4c14981201d630cfc30a19632 Mon Sep 17 00:00:00 2001
From: Leni Aniva <v@leni.sh>
Date: Fri, 19 Apr 2024 12:37:17 -0700
Subject: [PATCH 06/38] refactor: Common tactic execute function

---
 Pantograph/Goal.lean                  | 127 ++++++--------------------
 Pantograph/Tactic.lean                |   2 +
 Pantograph/Tactic/MotivatedApply.lean |  59 ++++++++++++
 3 files changed, 89 insertions(+), 99 deletions(-)
 create mode 100644 Pantograph/Tactic.lean
 create mode 100644 Pantograph/Tactic/MotivatedApply.lean

diff --git a/Pantograph/Goal.lean b/Pantograph/Goal.lean
index 5c6a583..0b7e306 100644
--- 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 :=
@@ -144,24 +145,6 @@ protected def GoalState.assignedExprOf? (goalState: GoalState) (mvar: MVarId): O
 
 --- Tactic execution functions ---
 
-/-- 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 Message.data).mapM fun md => md.toString
-        return .error errors
-      else
-        return .ok (← MonadBacktrack.saveState)
-    catch exception =>
-      return .error #[← exception.toMessageData.toString]
-  tacticM tactic { elaborator := .anonymous } |>.run' state.tactic
-
 /-- Response for executing a tactic -/
 inductive TacticResult where
   -- Goes to next state
@@ -175,14 +158,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):
-    Elab.TermElabM TacticResult := do
+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 Message.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)
@@ -190,22 +194,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):
@@ -515,15 +504,6 @@ protected def GoalState.tryCalc (state: GoalState) (goalId: Nat) (pred: String):
   catch exception =>
     return .failure #[← exception.toMessageData.toString]
 
-def getForallArgsBody: Expr → List Expr × Expr
-  | .forallE _ d b _ =>
-    let (innerArgs, innerBody) := getForallArgsBody b
-    (d :: innerArgs, innerBody)
-  | e => ([], e)
-def collectMotiveArguments (forallBody: Expr): SSet Nat :=
-  match forallBody with
-  | .app (.bvar i) _ => SSet.empty.insert i
-  | _ => SSet.empty
 
 protected def GoalState.tryMotivatedApply (state: GoalState) (goalId: Nat) (recursor: String):
       Elab.TermElabM TacticResult := do
@@ -540,57 +520,6 @@ protected def GoalState.tryMotivatedApply (state: GoalState) (goalId: Nat) (recu
     (fileName := filename) with
     | .ok syn => pure syn
     | .error error => return .parseError error
-  try
-    -- Implemented similarly to the intro tactic
-    let nextGoals: List MVarId ← goal.withContext do
-      let recursor ← Elab.Term.elabTerm (stx := recursor) .none
-      let recursorType ← Meta.inferType recursor
-
-      let (forallArgs, forallBody) := getForallArgsBody recursorType
-      let motiveIndices := collectMotiveArguments forallBody
-      --IO.println s!"{motiveIndices.toList} from {← Meta.ppExpr forallBody}"
-
-      let numArgs ← Meta.getExpectedNumArgs recursorType
-
-      let rec go (i: Nat) (prev: Array Expr): MetaM (Array Expr) := do
-        if i ≥ numArgs then
-          return prev
-        else
-          let argType := forallArgs.get! i
-          -- If `argType` has motive references, its goal needs to be placed in it
-          let argType := argType.instantiateRev prev
-          -- Create the goal
-          let userName := if motiveIndices.contains (numArgs - i - 1) then `motive else .anonymous
-          let argGoal ← Meta.mkFreshExprMVar argType .syntheticOpaque (userName := userName)
-          IO.println s!"Creating [{i}] {← Meta.ppExpr argGoal}"
-          let prev :=  prev ++ [argGoal]
-          go (i + 1) prev
-        termination_by numArgs - i
-      let newMVars ← go 0 #[]
-
-      -- FIXME: Add an `Eq` target and swap out the motive type
-
-      --let sourceType := forallBody.instantiateRev newMVars
-      --unless ← withTheReader Meta.Context (λ ctx => { ctx with config := { ctx.config with } }) $
-      --       Meta.isDefEq sourceType (← goal.getType) do
-      --  throwError "invalid mapply: The resultant type {← Meta.ppExpr sourceType} cannot be unified with {← Meta.ppExpr $ ← goal.getType}"
-
-      -- Create the main goal for the return type of the recursor
-      goal.assign (mkAppN recursor newMVars)
-
-      let nextGoals ← newMVars.toList.map (·.mvarId!) |>.filterM (not <$> ·.isAssigned)
-      pure nextGoals
-    return .success {
-      root := state.root,
-      savedState := {
-        term := ← MonadBacktrack.saveState,
-        tactic := { goals := nextGoals }
-      },
-      newMVars := nextGoals.toSSet,
-      parentMVar? := .some goal,
-      calcPrevRhs? := .none
-    }
-  catch exception =>
-    return .failure #[← exception.toMessageData.toString]
+  state.execute goalId (tacticM := Tactic.motivatedApply recursor)
 
 end Pantograph
diff --git a/Pantograph/Tactic.lean b/Pantograph/Tactic.lean
new file mode 100644
index 0000000..0148548
--- /dev/null
+++ b/Pantograph/Tactic.lean
@@ -0,0 +1,2 @@
+
+import Pantograph.Tactic.MotivatedApply
diff --git a/Pantograph/Tactic/MotivatedApply.lean b/Pantograph/Tactic/MotivatedApply.lean
new file mode 100644
index 0000000..50a660f
--- /dev/null
+++ b/Pantograph/Tactic/MotivatedApply.lean
@@ -0,0 +1,59 @@
+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 collectMotiveArguments (forallBody: Expr): SSet Nat :=
+  match forallBody with
+  | .app (.bvar i) _ => SSet.empty.insert i
+  | _ => SSet.empty
+
+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 (forallArgs, forallBody) := getForallArgsBody recursorType
+    let motiveIndices := collectMotiveArguments forallBody
+    --IO.println s!"{motiveIndices.toList} from {← Meta.ppExpr forallBody}"
+
+    let numArgs ← Meta.getExpectedNumArgs recursorType
+
+    let rec go (i: Nat) (prev: Array Expr): MetaM (Array Expr) := do
+      if i ≥ numArgs then
+        return prev
+      else
+        let argType := forallArgs.get! i
+        -- If `argType` has motive references, its goal needs to be placed in it
+        let argType := argType.instantiateRev prev
+        -- Create the goal
+        let userName := if motiveIndices.contains (numArgs - i - 1) then `motive else .anonymous
+        let argGoal ← Meta.mkFreshExprMVar argType .syntheticOpaque (userName := userName)
+        IO.println s!"Creating [{i}] {← Meta.ppExpr argGoal}"
+        let prev :=  prev ++ [argGoal]
+        go (i + 1) prev
+      termination_by numArgs - i
+    let newMVars ← go 0 #[]
+
+    -- FIXME: Add an `Eq` target and swap out the motive type
+
+    --let sourceType := forallBody.instantiateRev newMVars
+    --unless ← withTheReader Meta.Context (λ ctx => { ctx with config := { ctx.config with } }) $
+    --       Meta.isDefEq sourceType (← goal.getType) do
+    --  throwError "invalid mapply: The resultant type {← Meta.ppExpr sourceType} cannot be unified with {← Meta.ppExpr $ ← goal.getType}"
+
+    -- Create the main goal for the return type of the recursor
+    goal.assign (mkAppN recursor newMVars)
+
+    let nextGoals ← newMVars.toList.map (·.mvarId!) |>.filterM (not <$> ·.isAssigned)
+    pure nextGoals
+  Elab.Tactic.setGoals nextGoals
+
+end Pantograph.Tactic

From 4a92e655f6515d1c6eaaaa991721f5cfb2774154 Mon Sep 17 00:00:00 2001
From: Leni Aniva <v@leni.sh>
Date: Sat, 20 Apr 2024 13:09:41 -0700
Subject: [PATCH 07/38] test: Tactic test stub

---
 Pantograph/Tactic/MotivatedApply.lean |  1 +
 Test/Main.lean                        |  2 ++
 Test/Tactic.lean                      |  1 +
 Test/Tactic/MotivatedApply.lean       | 11 +++++++++++
 4 files changed, 15 insertions(+)
 create mode 100644 Test/Tactic.lean
 create mode 100644 Test/Tactic/MotivatedApply.lean

diff --git a/Pantograph/Tactic/MotivatedApply.lean b/Pantograph/Tactic/MotivatedApply.lean
index 50a660f..817942d 100644
--- a/Pantograph/Tactic/MotivatedApply.lean
+++ b/Pantograph/Tactic/MotivatedApply.lean
@@ -14,6 +14,7 @@ def collectMotiveArguments (forallBody: Expr): SSet Nat :=
   | .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
diff --git a/Test/Main.lean b/Test/Main.lean
index 1aa1d3d..ae897d4 100644
--- 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,7 @@ def main (args: List String) := do
     ("Metavar", Metavar.suite env_default),
     ("Proofs", Proofs.suite env_default),
     ("Serial", Serial.suite env_default),
+    ("Tactic/Motivated Apply", Tactic.MotivatedApply.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)
diff --git a/Test/Tactic.lean b/Test/Tactic.lean
new file mode 100644
index 0000000..4284a41
--- /dev/null
+++ b/Test/Tactic.lean
@@ -0,0 +1 @@
+import Test.Tactic.MotivatedApply
diff --git a/Test/Tactic/MotivatedApply.lean b/Test/Tactic/MotivatedApply.lean
new file mode 100644
index 0000000..04d7825
--- /dev/null
+++ b/Test/Tactic/MotivatedApply.lean
@@ -0,0 +1,11 @@
+import LSpec
+import Lean
+
+open Lean
+
+namespace Pantograph.Test.Tactic.MotivatedApply
+
+def suite (env: Environment): List (String × IO LSpec.TestSeq) :=
+  []
+
+end Pantograph.Test.Tactic.MotivatedApply

From 3812aa56ecb871a9531d3cabec61a51eab7acbde Mon Sep 17 00:00:00 2001
From: Leni Aniva <v@leni.sh>
Date: Mon, 22 Apr 2024 00:11:41 -0700
Subject: [PATCH 08/38] feat: Phantom var in mapply

---
 Makefile                              |  4 +-
 Pantograph/Goal.lean                  |  2 +-
 Pantograph/Tactic/MotivatedApply.lean | 88 +++++++++++++++++++++------
 Test/Common.lean                      |  6 ++
 Test/Proofs.lean                      |  9 ++-
 Test/Tactic/MotivatedApply.lean       | 65 +++++++++++++++++++-
 6 files changed, 147 insertions(+), 27 deletions(-)

diff --git a/Makefile b/Makefile
index 5d4ad6b..86f9e5b 100644
--- a/Makefile
+++ b/Makefile
@@ -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
diff --git a/Pantograph/Goal.lean b/Pantograph/Goal.lean
index 0b7e306..17d94c0 100644
--- a/Pantograph/Goal.lean
+++ b/Pantograph/Goal.lean
@@ -126,7 +126,7 @@ protected def GoalState.continue (target: GoalState) (branch: GoalState): Except
 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
+  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
diff --git a/Pantograph/Tactic/MotivatedApply.lean b/Pantograph/Tactic/MotivatedApply.lean
index 817942d..9826e3d 100644
--- a/Pantograph/Tactic/MotivatedApply.lean
+++ b/Pantograph/Tactic/MotivatedApply.lean
@@ -9,6 +9,54 @@ def getForallArgsBody: Expr → List Expr × Expr
     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
+  iMajor: 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) (resultant: Expr): MetaM Expr := do
+  let motiveType := info.getMotiveType
+  let resultantType ← Meta.inferType resultant
+  return replaceForallBody motiveType resultantType
+
+protected def phantomType (info: RecursorWithMotive) (mvars: Array Expr) (resultant: Expr): MetaM Expr := do
+  let goalMotive := mvars.get! (info.nArgs - info.iMotive - 1)
+  let goalMajor := mvars.get! (info.nArgs - info.iMajor - 1)
+  Meta.mkEq (.app goalMotive goalMajor) resultant
+
+end RecursorWithMotive
+
+def getRecursorInformation (recursorType: Expr): Option RecursorWithMotive := do
+  let (args, body) := getForallArgsBody recursorType
+  let (iMotive, iMajor) ← match body with
+    | .app (.bvar iMotive) (.bvar iMajor) => pure (iMotive, iMajor)
+    | _ => .none
+  return {
+    args,
+    body,
+    iMotive,
+    iMajor,
+  }
+
 def collectMotiveArguments (forallBody: Expr): SSet Nat :=
   match forallBody with
   | .app (.bvar i) _ => SSet.empty.insert i
@@ -21,38 +69,38 @@ def motivatedApply: Elab.Tactic.Tactic := λ stx => do
     let recursor ← Elab.Term.elabTerm (stx := stx) .none
     let recursorType ← Meta.inferType recursor
 
-    let (forallArgs, forallBody) := getForallArgsBody recursorType
-    let motiveIndices := collectMotiveArguments forallBody
-    --IO.println s!"{motiveIndices.toList} from {← Meta.ppExpr forallBody}"
+    let resultant ← goal.getType
 
-    let numArgs ← Meta.getExpectedNumArgs recursorType
+    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 ≥ numArgs then
+      if i ≥ info.nArgs then
         return prev
       else
-        let argType := forallArgs.get! i
+        let argType := info.args.get! i
         -- If `argType` has motive references, its goal needs to be placed in it
         let argType := argType.instantiateRev prev
-        -- Create the goal
-        let userName := if motiveIndices.contains (numArgs - i - 1) then `motive else .anonymous
-        let argGoal ← Meta.mkFreshExprMVar argType .syntheticOpaque (userName := userName)
-        IO.println s!"Creating [{i}] {← Meta.ppExpr argGoal}"
+        let bvarIndex := info.nArgs - i - 1
+        let argGoal ← if bvarIndex = info.iMotive then
+            let surrogateMotiveType ← info.surrogateMotiveType resultant
+            Meta.mkFreshExprMVar surrogateMotiveType .syntheticOpaque (userName := `motive)
+          else if bvarIndex = info.iMajor then
+            Meta.mkFreshExprMVar argType .syntheticOpaque (userName := `major)
+          else
+            Meta.mkFreshExprMVar argType .syntheticOpaque (userName := .anonymous)
         let prev :=  prev ++ [argGoal]
         go (i + 1) prev
-      termination_by numArgs - i
-    let newMVars ← go 0 #[]
+      termination_by info.nArgs - i
+    let mut newMVars ← go 0 #[]
 
-    -- FIXME: Add an `Eq` target and swap out the motive type
-
-    --let sourceType := forallBody.instantiateRev newMVars
-    --unless ← withTheReader Meta.Context (λ ctx => { ctx with config := { ctx.config with } }) $
-    --       Meta.isDefEq sourceType (← goal.getType) do
-    --  throwError "invalid mapply: The resultant type {← Meta.ppExpr sourceType} cannot be unified with {← Meta.ppExpr $ ← goal.getType}"
-
-    -- Create the main goal for the return type of the recursor
     goal.assign (mkAppN recursor newMVars)
 
+    let phantomType ← info.phantomType newMVars resultant
+    let goalPhantom ← Meta.mkFreshExprMVar phantomType .syntheticOpaque (userName := `phantom)
+    newMVars := newMVars ++ [goalPhantom]
+
     let nextGoals ← newMVars.toList.map (·.mvarId!) |>.filterM (not <$> ·.isAssigned)
     pure nextGoals
   Elab.Tactic.setGoals nextGoals
diff --git a/Test/Common.lean b/Test/Common.lean
index 8b8e977..6ea4fb2 100644
--- a/Test/Common.lean
+++ b/Test/Common.lean
@@ -63,6 +63,12 @@ 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 runTacticOnMVar (tacticM: Elab.Tactic.TacticM Unit) (goal: MVarId): Elab.TermElabM (List MVarId) := do
+    let (_, newGoals) ← tacticM { elaborator := .anonymous } |>.run { goals := [goal] }
+    return newGoals.goals
+
 end Test
 
 end Pantograph
diff --git a/Test/Proofs.lean b/Test/Proofs.lean
index 1adc9d4..43c346b 100644
--- a/Test/Proofs.lean
+++ b/Test/Proofs.lean
@@ -661,9 +661,10 @@ def test_nat_zero_add: TestM Unit := do
       return ()
   addTest $ LSpec.check s!"mapply {recursor}" ((← state2.serializeGoals (options := ← read)).map (·.devolatilizeVars) =
     #[
-      buildNamedGoal "_uniq.70" [("n", "Nat")] "Nat → Sort ?u.66" (.some "motive"),
-      buildNamedGoal "_uniq.71" [("n", "Nat")] "Nat",
-      buildNamedGoal "_uniq.72" [("n", "Nat")] "(t : Nat) → Nat.below t → ?motive t"
+      buildNamedGoal "_uniq.67" [("n", "Nat")] "Nat → Prop" (.some "motive"),
+      buildNamedGoal "_uniq.68" [("n", "Nat")] "Nat" (.some "major"),
+      buildNamedGoal "_uniq.69" [("n", "Nat")] "∀ (t : Nat), Nat.below t → ?motive t",
+      buildNamedGoal "_uniq.70" [("n", "Nat")] "?motive ?major = (n + 0 = n)" (.some "phantom")
     ])
 
   let tactic := "exact n"
@@ -710,6 +711,8 @@ def test_nat_zero_add: TestM Unit := do
   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 suite (env: Environment): List (String × IO LSpec.TestSeq) :=
diff --git a/Test/Tactic/MotivatedApply.lean b/Test/Tactic/MotivatedApply.lean
index 04d7825..60ed7be 100644
--- a/Test/Tactic/MotivatedApply.lean
+++ b/Test/Tactic/MotivatedApply.lean
@@ -1,11 +1,74 @@
 import LSpec
 import Lean
+import Test.Common
 
 open Lean
+open Pantograph
 
 namespace Pantograph.Test.Tactic.MotivatedApply
 
+def valueAndType (recursor: String): MetaM (Expr × Expr) := do
+  let recursor ← match Parser.runParserCategory
+    (env := ← MonadEnv.getEnv)
+    (catName := `term)
+    (input := recursor)
+    (fileName := filename) with
+    | .ok syn => pure syn
+    | .error error => throwError "Failed to parse: {error}"
+  runTermElabMInMeta do
+    let recursor ← Elab.Term.elabTerm (stx := recursor) .none
+    let recursorType ← Meta.inferType recursor
+    return (recursor, recursorType)
+
+
+def test_type_extract (env: Environment): IO LSpec.TestSeq :=
+  runMetaMSeq env do
+    let mut tests := LSpec.TestSeq.done
+    let (recursor, recursorType) ← valueAndType "@Nat.brecOn"
+    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)
+    tests := tests ++ LSpec.check "iMajor" (info.iMajor = 1)
+    let motiveType := info.getMotiveType
+    tests := tests ++ LSpec.check "motiveType" ("Nat → Sort ?u.1" =
+      (← exprToStr motiveType))
+    return tests
+
+def test_execute (env: Environment): IO LSpec.TestSeq :=
+  let expr := "λ (n t: Nat) => n + 0 = n"
+  runMetaMSeq env do
+    let (expr, exprType) ← valueAndType 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 ?major = (n + 0 = n)",
+          ])
+      tests := tests ++ test
+      return tests
+
 def suite (env: Environment): List (String × IO LSpec.TestSeq) :=
-  []
+  [
+    ("type_extract", test_type_extract env),
+    ("execute", test_execute env),
+  ]
 
 end Pantograph.Test.Tactic.MotivatedApply

From feff62a3c53de6ba111cb6aa48371a2ae0effb7e Mon Sep 17 00:00:00 2001
From: Leni Aniva <v@leni.sh>
Date: Mon, 22 Apr 2024 09:52:13 -0700
Subject: [PATCH 09/38] fix: Remove determination of major

---
 Pantograph/Tactic/MotivatedApply.lean | 15 ++++++---------
 Test/Proofs.lean                      |  4 ++--
 Test/Tactic/MotivatedApply.lean       |  3 +--
 3 files changed, 9 insertions(+), 13 deletions(-)

diff --git a/Pantograph/Tactic/MotivatedApply.lean b/Pantograph/Tactic/MotivatedApply.lean
index 9826e3d..1201174 100644
--- a/Pantograph/Tactic/MotivatedApply.lean
+++ b/Pantograph/Tactic/MotivatedApply.lean
@@ -22,7 +22,6 @@ structure RecursorWithMotive where
 
   -- .bvar index for the motive and major from the body
   iMotive: Nat
-  iMajor: Nat
 
 namespace RecursorWithMotive
 
@@ -39,22 +38,22 @@ protected def surrogateMotiveType (info: RecursorWithMotive) (resultant: Expr):
   return replaceForallBody motiveType resultantType
 
 protected def phantomType (info: RecursorWithMotive) (mvars: Array Expr) (resultant: Expr): MetaM Expr := do
-  let goalMotive := mvars.get! (info.nArgs - info.iMotive - 1)
-  let goalMajor := mvars.get! (info.nArgs - info.iMajor - 1)
-  Meta.mkEq (.app goalMotive goalMajor) resultant
+  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
-  let (iMotive, iMajor) ← match body with
-    | .app (.bvar iMotive) (.bvar iMajor) => pure (iMotive, iMajor)
+  if ¬ body.isApp then
+    .none
+  let iMotive ← match body.getAppFn with
+    | .bvar iMotive => pure iMotive
     | _ => .none
   return {
     args,
     body,
     iMotive,
-    iMajor,
   }
 
 def collectMotiveArguments (forallBody: Expr): SSet Nat :=
@@ -86,8 +85,6 @@ def motivatedApply: Elab.Tactic.Tactic := λ stx => do
         let argGoal ← if bvarIndex = info.iMotive then
             let surrogateMotiveType ← info.surrogateMotiveType resultant
             Meta.mkFreshExprMVar surrogateMotiveType .syntheticOpaque (userName := `motive)
-          else if bvarIndex = info.iMajor then
-            Meta.mkFreshExprMVar argType .syntheticOpaque (userName := `major)
           else
             Meta.mkFreshExprMVar argType .syntheticOpaque (userName := .anonymous)
         let prev :=  prev ++ [argGoal]
diff --git a/Test/Proofs.lean b/Test/Proofs.lean
index 43c346b..2df0868 100644
--- a/Test/Proofs.lean
+++ b/Test/Proofs.lean
@@ -662,9 +662,9 @@ def test_nat_zero_add: TestM Unit := do
   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" (.some "major"),
+      buildNamedGoal "_uniq.68" [("n", "Nat")] "Nat",
       buildNamedGoal "_uniq.69" [("n", "Nat")] "∀ (t : Nat), Nat.below t → ?motive t",
-      buildNamedGoal "_uniq.70" [("n", "Nat")] "?motive ?major = (n + 0 = n)" (.some "phantom")
+      buildNamedGoal "_uniq.70" [("n", "Nat")] "?motive ?m.68 = (n + 0 = n)" (.some "phantom")
     ])
 
   let tactic := "exact n"
diff --git a/Test/Tactic/MotivatedApply.lean b/Test/Tactic/MotivatedApply.lean
index 60ed7be..1f751ed 100644
--- a/Test/Tactic/MotivatedApply.lean
+++ b/Test/Tactic/MotivatedApply.lean
@@ -31,7 +31,6 @@ def test_type_extract (env: Environment): IO LSpec.TestSeq :=
       | .some info => pure info
       | .none => throwError "Failed to extract recursor info"
     tests := tests ++ LSpec.check "iMotive" (info.iMotive = 2)
-    tests := tests ++ LSpec.check "iMajor" (info.iMajor = 1)
     let motiveType := info.getMotiveType
     tests := tests ++ LSpec.check "motiveType" ("Nat → Sort ?u.1" =
       (← exprToStr motiveType))
@@ -60,7 +59,7 @@ def test_execute (env: Environment): IO LSpec.TestSeq :=
             "Nat → Prop",
             "Nat",
             "∀ (t : Nat), Nat.below t → ?motive t",
-            "?motive ?major = (n + 0 = n)",
+            "?motive ?m.69 = (n + 0 = n)",
           ])
       tests := tests ++ test
       return tests

From 6ffb227cd641f77109c539152e0b38f6d2bfa125 Mon Sep 17 00:00:00 2001
From: Leni Aniva <v@leni.sh>
Date: Mon, 22 Apr 2024 10:02:09 -0700
Subject: [PATCH 10/38] feat: Conduit modus ponens

---
 Pantograph/Tactic/MotivatedApply.lean | 12 ++++++------
 Test/Proofs.lean                      | 15 +++++++++++++--
 2 files changed, 19 insertions(+), 8 deletions(-)

diff --git a/Pantograph/Tactic/MotivatedApply.lean b/Pantograph/Tactic/MotivatedApply.lean
index 1201174..821b681 100644
--- a/Pantograph/Tactic/MotivatedApply.lean
+++ b/Pantograph/Tactic/MotivatedApply.lean
@@ -37,7 +37,7 @@ protected def surrogateMotiveType (info: RecursorWithMotive) (resultant: Expr):
   let resultantType ← Meta.inferType resultant
   return replaceForallBody motiveType resultantType
 
-protected def phantomType (info: RecursorWithMotive) (mvars: Array Expr) (resultant: Expr): MetaM Expr := do
+protected def conduitType (info: RecursorWithMotive) (mvars: Array Expr) (resultant: Expr): MetaM Expr := do
   let motiveCall := Expr.instantiateRev info.body mvars
   Meta.mkEq motiveCall resultant
 
@@ -92,11 +92,11 @@ def motivatedApply: Elab.Tactic.Tactic := λ stx => do
       termination_by info.nArgs - i
     let mut newMVars ← go 0 #[]
 
-    goal.assign (mkAppN recursor newMVars)
-
-    let phantomType ← info.phantomType newMVars resultant
-    let goalPhantom ← Meta.mkFreshExprMVar phantomType .syntheticOpaque (userName := `phantom)
-    newMVars := newMVars ++ [goalPhantom]
+    -- 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 .syntheticOpaque (userName := `conduit)
+    goal.assign $ ← Meta.mkEqMP goalConduit (mkAppN recursor newMVars)
+    newMVars := newMVars ++ [goalConduit]
 
     let nextGoals ← newMVars.toList.map (·.mvarId!) |>.filterM (not <$> ·.isAssigned)
     pure nextGoals
diff --git a/Test/Proofs.lean b/Test/Proofs.lean
index 2df0868..429d4d2 100644
--- a/Test/Proofs.lean
+++ b/Test/Proofs.lean
@@ -664,7 +664,7 @@ def test_nat_zero_add: TestM Unit := do
       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 "phantom")
+      buildNamedGoal "_uniq.70" [("n", "Nat")] "?motive ?m.68 = (n + 0 = n)" (.some "conduit")
     ])
 
   let tactic := "exact n"
@@ -703,7 +703,18 @@ def test_nat_zero_add: TestM Unit := do
     #[buildGoal [("n", "Nat"), ("t", "Nat"), ("h", "Nat.below t")] "t + 0 = t"])
 
   let tactic := "simp"
-  let stateF ← match ← state3.tryTactic (goalId := 0) (tactic := tactic) with
+  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

From 4cff6677d27a9629eb44d173c321977ac860e5e8 Mon Sep 17 00:00:00 2001
From: Leni Aniva <v@leni.sh>
Date: Sat, 4 May 2024 23:36:42 -0700
Subject: [PATCH 11/38] chore: Lean version bump to 4.8.0-rc1

---
 Pantograph.lean          | 2 +-
 Pantograph/Goal.lean     | 4 ++--
 Pantograph/Protocol.lean | 1 -
 Test/Integration.lean    | 2 +-
 flake.lock               | 8 ++++----
 flake.nix                | 2 +-
 lean-toolchain           | 2 +-
 7 files changed, 10 insertions(+), 11 deletions(-)

diff --git a/Pantograph.lean b/Pantograph.lean
index f59bc11..74289d6 100644
--- a/Pantograph.lean
+++ b/Pantograph.lean
@@ -87,7 +87,7 @@ 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
diff --git a/Pantograph/Goal.lean b/Pantograph/Goal.lean
index 17d94c0..921f60b 100644
--- a/Pantograph/Goal.lean
+++ b/Pantograph/Goal.lean
@@ -169,7 +169,7 @@ protected def GoalState.execute (state: GoalState) (goalId: Nat) (tacticM: Elab.
     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 Message.data).mapM fun md => md.toString
+      let errors ← (messages.map (·.data)).mapM fun md => md.toString
       return .failure errors
     let nextElabState ← MonadBacktrack.saveState
     let nextMCtx := nextElabState.meta.meta.mctx
@@ -214,7 +214,7 @@ protected def GoalState.assign (state: GoalState) (goal: MVarId) (expr: Expr):
     goal.assign expr
     if (← getThe Core.State).messages.hasErrors then
       let messages := (← getThe Core.State).messages.getErrorMessages |>.toList.toArray
-      let errors ← (messages.map Message.data).mapM fun md => md.toString
+      let errors ← (messages.map (·.data)).mapM fun md => md.toString
       return .failure errors
     let prevMCtx := state.savedState.term.meta.meta.mctx
     let nextMCtx ← getMCtx
diff --git a/Pantograph/Protocol.lean b/Pantograph/Protocol.lean
index 17618fc..f73c3b0 100644
--- a/Pantograph/Protocol.lean
+++ b/Pantograph/Protocol.lean
@@ -193,7 +193,6 @@ 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.
diff --git a/Test/Integration.lean b/Test/Integration.lean
index 29cb82d..9bd5db6 100644
--- a/Test/Integration.lean
+++ b/Test/Integration.lean
@@ -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"
diff --git a/flake.lock b/flake.lock
index 39888a8..1a50363 100644
--- a/flake.lock
+++ b/flake.lock
@@ -42,16 +42,16 @@
         "nixpkgs-old": "nixpkgs-old"
       },
       "locked": {
-        "lastModified": 1711508550,
-        "narHash": "sha256-UK4DnYmwXLcqHA316Zkn0cnujdYlxqUf+b6S4l56Q3s=",
+        "lastModified": 1714704934,
+        "narHash": "sha256-q0kLyIahUXolkSrBZSegPF+R99WAH1YC96JfKoFntDE=",
         "owner": "leanprover",
         "repo": "lean4",
-        "rev": "b4caee80a3dfc5c9619d88b16c40cc3db90da4e2",
+        "rev": "dcccfb73cb247e9478220375ab7de03f7c67e505",
         "type": "github"
       },
       "original": {
         "owner": "leanprover",
-        "ref": "b4caee80a3dfc5c9619d88b16c40cc3db90da4e2",
+        "ref": "v4.8.0-rc1",
         "repo": "lean4",
         "type": "github"
       }
diff --git a/flake.nix b/flake.nix
index 2458805..ad40a3f 100644
--- a/flake.nix
+++ b/flake.nix
@@ -5,8 +5,8 @@
     nixpkgs.url = "github:nixos/nixpkgs/nixos-unstable";
     flake-parts.url = "github:hercules-ci/flake-parts";
     lean = {
-      url = "github:leanprover/lean4?ref=b4caee80a3dfc5c9619d88b16c40cc3db90da4e2";
       # Do not follow input's nixpkgs since it could cause build failures
+      url = "github:leanprover/lean4?ref=v4.8.0-rc1";
     };
     lspec = {
       url = "github:lurk-lab/LSpec?ref=3388be5a1d1390594a74ec469fd54a5d84ff6114";
diff --git a/lean-toolchain b/lean-toolchain
index c630636..d8a6d7e 100644
--- a/lean-toolchain
+++ b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:nightly-2024-03-27
+leanprover/lean4:v4.8.0-rc1

From 63417ef179066bfd847ff5efc5e74085268b1795 Mon Sep 17 00:00:00 2001
From: Leni Aniva <v@leni.sh>
Date: Sun, 5 May 2024 00:43:32 -0700
Subject: [PATCH 12/38] fix: Motive extra arguments not instiantiated

---
 Pantograph/Tactic/MotivatedApply.lean | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/Pantograph/Tactic/MotivatedApply.lean b/Pantograph/Tactic/MotivatedApply.lean
index 821b681..a7b9a07 100644
--- a/Pantograph/Tactic/MotivatedApply.lean
+++ b/Pantograph/Tactic/MotivatedApply.lean
@@ -32,8 +32,8 @@ protected def getMotiveType (info: RecursorWithMotive): Expr :=
   let a := info.args.get! level
   a
 
-protected def surrogateMotiveType (info: RecursorWithMotive) (resultant: Expr): MetaM Expr := do
-  let motiveType := info.getMotiveType
+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
 
@@ -83,7 +83,7 @@ def motivatedApply: Elab.Tactic.Tactic := λ stx => do
         let argType := argType.instantiateRev prev
         let bvarIndex := info.nArgs - i - 1
         let argGoal ← if bvarIndex = info.iMotive then
-            let surrogateMotiveType ← info.surrogateMotiveType resultant
+            let surrogateMotiveType ← info.surrogateMotiveType prev resultant
             Meta.mkFreshExprMVar surrogateMotiveType .syntheticOpaque (userName := `motive)
           else
             Meta.mkFreshExprMVar argType .syntheticOpaque (userName := .anonymous)

From 1e1995255a91a738f3e1ce0dc2a8f8842acc4152 Mon Sep 17 00:00:00 2001
From: Leni Aniva <v@leni.sh>
Date: Sun, 5 May 2024 10:36:43 -0700
Subject: [PATCH 13/38] test: mapply captures dependent types

---
 Test/Tactic/MotivatedApply.lean | 35 +++++++++++++++++++++++++++++++--
 1 file changed, 33 insertions(+), 2 deletions(-)

diff --git a/Test/Tactic/MotivatedApply.lean b/Test/Tactic/MotivatedApply.lean
index 1f751ed..84ca804 100644
--- a/Test/Tactic/MotivatedApply.lean
+++ b/Test/Tactic/MotivatedApply.lean
@@ -36,7 +36,7 @@ def test_type_extract (env: Environment): IO LSpec.TestSeq :=
       (← exprToStr motiveType))
     return tests
 
-def test_execute (env: Environment): IO LSpec.TestSeq :=
+def test_nat_brec_on (env: Environment): IO LSpec.TestSeq :=
   let expr := "λ (n t: Nat) => n + 0 = n"
   runMetaMSeq env do
     let (expr, exprType) ← valueAndType expr
@@ -64,10 +64,41 @@ def test_execute (env: Environment): IO LSpec.TestSeq :=
       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, exprType) ← valueAndType 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.92",
+            "List ?m.94 → Prop",
+            "List ?m.94",
+            "∀ (t : List ?m.94), List.below t → ?motive t",
+            "?motive ?m.96 = (l ++ [] = [] ++ l)",
+          ])
+      tests := tests ++ test
+      return tests
+
+
 def suite (env: Environment): List (String × IO LSpec.TestSeq) :=
   [
     ("type_extract", test_type_extract env),
-    ("execute", test_execute env),
+    ("nat_brec_on", test_nat_brec_on env),
+    ("list_brec_on", test_list_brec_on env),
   ]
 
 end Pantograph.Test.Tactic.MotivatedApply

From cf1289f159ddddf85430fbdd04d47d4f3be6eeae Mon Sep 17 00:00:00 2001
From: Leni Aniva <v@leni.sh>
Date: Sun, 5 May 2024 13:24:29 -0700
Subject: [PATCH 14/38] feat: NoConfuse tactic

---
 Pantograph/Goal.lean             |  16 +++++
 Pantograph/Tactic.lean           |   1 +
 Pantograph/Tactic/NoConfuse.lean |  18 ++++++
 Test/Main.lean                   |   1 +
 Test/Tactic.lean                 |   1 +
 Test/Tactic/NoConfuse.lean       | 100 +++++++++++++++++++++++++++++++
 6 files changed, 137 insertions(+)
 create mode 100644 Pantograph/Tactic/NoConfuse.lean
 create mode 100644 Test/Tactic/NoConfuse.lean

diff --git a/Pantograph/Goal.lean b/Pantograph/Goal.lean
index 921f60b..7ada190 100644
--- a/Pantograph/Goal.lean
+++ b/Pantograph/Goal.lean
@@ -521,5 +521,21 @@ protected def GoalState.tryMotivatedApply (state: GoalState) (goalId: Nat) (recu
     | .ok syn => pure syn
     | .error error => return .parseError error
   state.execute goalId (tacticM := Tactic.motivatedApply recursor)
+protected def GoalState.tryNoConfusion (state: GoalState) (goalId: Nat) (eq: 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.tryMotivatedApply
+
+  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
diff --git a/Pantograph/Tactic.lean b/Pantograph/Tactic.lean
index 0148548..5a7828c 100644
--- a/Pantograph/Tactic.lean
+++ b/Pantograph/Tactic.lean
@@ -1,2 +1,3 @@
 
 import Pantograph.Tactic.MotivatedApply
+import Pantograph.Tactic.NoConfuse
diff --git a/Pantograph/Tactic/NoConfuse.lean b/Pantograph/Tactic/NoConfuse.lean
new file mode 100644
index 0000000..b8bc84e
--- /dev/null
+++ 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
diff --git a/Test/Main.lean b/Test/Main.lean
index ae897d4..4a1ca69 100644
--- a/Test/Main.lean
+++ b/Test/Main.lean
@@ -50,6 +50,7 @@ def main (args: List String) := do
     ("Proofs", Proofs.suite env_default),
     ("Serial", Serial.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)
diff --git a/Test/Tactic.lean b/Test/Tactic.lean
index 4284a41..f1e2649 100644
--- a/Test/Tactic.lean
+++ b/Test/Tactic.lean
@@ -1 +1,2 @@
 import Test.Tactic.MotivatedApply
+import Test.Tactic.NoConfuse
diff --git a/Test/Tactic/NoConfuse.lean b/Test/Tactic/NoConfuse.lean
new file mode 100644
index 0000000..54c2be7
--- /dev/null
+++ b/Test/Tactic/NoConfuse.lean
@@ -0,0 +1,100 @@
+import LSpec
+import Lean
+import Test.Common
+
+open Lean
+open Pantograph
+
+namespace Pantograph.Test.Tactic.NoConfuse
+
+def valueAndType (recursor: String): MetaM (Expr × Expr) := do
+  let recursor ← match Parser.runParserCategory
+    (env := ← MonadEnv.getEnv)
+    (catName := `term)
+    (input := recursor)
+    (fileName := filename) with
+    | .ok syn => pure syn
+    | .error error => throwError "Failed to parse: {error}"
+  runTermElabMInMeta do
+    let recursor ← Elab.Term.elabTerm (stx := recursor) .none
+    let recursorType ← Meta.inferType recursor
+    return (recursor, recursorType)
+
+def test_nat (env: Environment): IO LSpec.TestSeq :=
+  let expr := "λ (n: Nat) (h: 0 = n + 1) => False"
+  runMetaMSeq env do
+    let (expr, exprType) ← valueAndType 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, _) ← valueAndType 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, exprType) ← valueAndType 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

From 2937675044bcefe266a9c1d1116dbec53ee3942a Mon Sep 17 00:00:00 2001
From: Leni Aniva <v@leni.sh>
Date: Sun, 5 May 2024 13:25:48 -0700
Subject: [PATCH 15/38] feat: Library interface for calling no_confuse

---
 Pantograph/Goal.lean    | 2 +-
 Pantograph/Library.lean | 3 +++
 2 files changed, 4 insertions(+), 1 deletion(-)

diff --git a/Pantograph/Goal.lean b/Pantograph/Goal.lean
index 7ada190..11e5b20 100644
--- a/Pantograph/Goal.lean
+++ b/Pantograph/Goal.lean
@@ -521,7 +521,7 @@ protected def GoalState.tryMotivatedApply (state: GoalState) (goalId: Nat) (recu
     | .ok syn => pure syn
     | .error error => return .parseError error
   state.execute goalId (tacticM := Tactic.motivatedApply recursor)
-protected def GoalState.tryNoConfusion (state: GoalState) (goalId: Nat) (eq: String):
+protected def GoalState.tryNoConfuse (state: GoalState) (goalId: Nat) (eq: String):
       Elab.TermElabM TacticResult := do
   state.restoreElabM
   let goal ← match state.savedState.tactic.goals.get? goalId with
diff --git a/Pantograph/Library.lean b/Pantograph/Library.lean
index 00b4bc7..608aeeb 100644
--- a/Pantograph/Library.lean
+++ b/Pantograph/Library.lean
@@ -208,5 +208,8 @@ def goalFocus (state: GoalState) (goalId: Nat): Option GoalState :=
 @[export pantograph_goal_motivated_apply_m]
 def goalMotivatedApply (state: GoalState) (goalId: Nat) (recursor: String): Lean.CoreM TacticResult :=
   runTermElabM <| state.tryMotivatedApply goalId recursor
+@[export pantograph_goal_no_confuse_m]
+def goalNoConfuse (state: GoalState) (goalId: Nat) (recursor: String): Lean.CoreM TacticResult :=
+  runTermElabM <| state.tryNoConfuse goalId recursor
 
 end Pantograph

From 679871cbc659ce9ff58e832d20f51f52ae3dc2f1 Mon Sep 17 00:00:00 2001
From: Leni Aniva <v@leni.sh>
Date: Sun, 5 May 2024 13:26:46 -0700
Subject: [PATCH 16/38] fix: NoConfuse arg name

---
 Pantograph/Library.lean | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/Pantograph/Library.lean b/Pantograph/Library.lean
index 608aeeb..6dda2f0 100644
--- a/Pantograph/Library.lean
+++ b/Pantograph/Library.lean
@@ -209,7 +209,7 @@ def goalFocus (state: GoalState) (goalId: Nat): Option GoalState :=
 def goalMotivatedApply (state: GoalState) (goalId: Nat) (recursor: String): Lean.CoreM TacticResult :=
   runTermElabM <| state.tryMotivatedApply goalId recursor
 @[export pantograph_goal_no_confuse_m]
-def goalNoConfuse (state: GoalState) (goalId: Nat) (recursor: String): Lean.CoreM TacticResult :=
-  runTermElabM <| state.tryNoConfuse goalId recursor
+def goalNoConfuse (state: GoalState) (goalId: Nat) (eq: String): Lean.CoreM TacticResult :=
+  runTermElabM <| state.tryNoConfuse goalId eq
 
 end Pantograph

From aa106f7591b8719ce91baa25e7434b808b62e0d6 Mon Sep 17 00:00:00 2001
From: Leni Aniva <v@leni.sh>
Date: Mon, 6 May 2024 22:20:20 -0700
Subject: [PATCH 17/38] feat: Do not filter mvars from mapply

---
 Pantograph/Tactic/MotivatedApply.lean | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/Pantograph/Tactic/MotivatedApply.lean b/Pantograph/Tactic/MotivatedApply.lean
index a7b9a07..f570560 100644
--- a/Pantograph/Tactic/MotivatedApply.lean
+++ b/Pantograph/Tactic/MotivatedApply.lean
@@ -94,11 +94,11 @@ def motivatedApply: Elab.Tactic.Tactic := λ stx => do
 
     -- Create the conduit type which proves the result of the motive is equal to the goal
     let conduitType ← info.conduitType newMVars resultant
-    let goalConduit ← Meta.mkFreshExprMVar conduitType .syntheticOpaque (userName := `conduit)
+    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!) |>.filterM (not <$> ·.isAssigned)
+    let nextGoals := newMVars.toList.map (·.mvarId!)
     pure nextGoals
   Elab.Tactic.setGoals nextGoals
 

From 69ec70ffbe7caec196c549bf30018c6433e4104b Mon Sep 17 00:00:00 2001
From: Leni Aniva <v@leni.sh>
Date: Mon, 6 May 2024 22:39:17 -0700
Subject: [PATCH 18/38] feat: Do not explicitly show delay assigned mvar

---
 Pantograph/Serial.lean | 9 ++++++---
 Test/Proofs.lean       | 2 +-
 2 files changed, 7 insertions(+), 4 deletions(-)

diff --git a/Pantograph/Serial.lean b/Pantograph/Serial.lean
index 950818e..26b0c9f 100644
--- a/Pantograph/Serial.lean
+++ b/Pantograph/Serial.lean
@@ -102,9 +102,12 @@ partial def serializeExpressionSexp (expr: Expr) (sanitize: Bool := true): MetaM
     | .fvar fvarId =>
       let name := ofName fvarId.name
       pure s!"(:fv {name})"
-    | .mvar mvarId =>
-      let name := ofName mvarId.name
-      pure s!"(:mv {name})"
+    | .mvar mvarId => do
+      if ← mvarId.isDelayedAssigned then
+        pure s!"(:mv)"
+      else
+        let name := ofName mvarId.name
+        pure s!"(:mv {name})"
     | .sort level =>
       let level := serializeSortLevel level sanitize
       pure s!"(:sort {level})"
diff --git a/Test/Proofs.lean b/Test/Proofs.lean
index 429d4d2..8e77227 100644
--- a/Test/Proofs.lean
+++ b/Test/Proofs.lean
@@ -245,7 +245,7 @@ def test_or_comm: TestM Unit := do
   let state2parent ← serializeExpressionSexp state2.parentExpr?.get! (sanitize := false)
   -- This is due to delayed assignment
   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)))")
+    "((:mv) (:fv _uniq.16) ((:c Eq.refl) ((:c Or) (:fv _uniq.10) (:fv _uniq.13)) (:fv _uniq.16)))")
 
   let state3_1 ← match ← state2.tryTactic (goalId := 0) (tactic := "apply Or.inr") with
     | .success state => pure state

From 66a5dfcf3c615a3f5d970acd624364d3dc5551d5 Mon Sep 17 00:00:00 2001
From: Leni Aniva <v@leni.sh>
Date: Wed, 8 May 2024 12:41:21 -0700
Subject: [PATCH 19/38] feat: Diagnostics command for FFI users

---
 Pantograph/Library.lean |  4 +++
 Pantograph/Serial.lean  | 63 ++++++++++++++++++++++-------------------
 2 files changed, 38 insertions(+), 29 deletions(-)

diff --git a/Pantograph/Library.lean b/Pantograph/Library.lean
index 6dda2f0..fa5d414 100644
--- a/Pantograph/Library.lean
+++ b/Pantograph/Library.lean
@@ -212,4 +212,8 @@ def goalMotivatedApply (state: GoalState) (goalId: Nat) (recursor: String): Lean
 def goalNoConfuse (state: GoalState) (goalId: Nat) (eq: String): Lean.CoreM TacticResult :=
   runTermElabM <| state.tryNoConfuse goalId eq
 
+@[export pantograph_goal_diag]
+def goalDiag (state: GoalState) (diagOptions: Protocol.GoalDiag) : Lean.CoreM String :=
+  runMetaM $ state.diag diagOptions
+
 end Pantograph
diff --git a/Pantograph/Serial.lean b/Pantograph/Serial.lean
index 26b0c9f..b2a4529 100644
--- a/Pantograph/Serial.lean
+++ b/Pantograph/Serial.lean
@@ -270,51 +270,56 @@ 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
-  | .some decl => printMVar ">" root decl
-  | .none => IO.println s!">{root.name}: ??"
-  goals.forM (fun mvarId => do
-    if mvarId != root then
-      match mctx.decls.find? mvarId with
-      | .some decl => printMVar "⊢" mvarId decl
-      | .none => IO.println s!"⊢{mvarId.name}: ??"
+  let result: String ← match mctx.decls.find? root with
+    | .some decl => printMVar ">" root decl
+    | .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 => 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
-      if options.printContext then
-        decl.lctx.fvarIdToDecl.forM printFVar
+    printMVar (pref: String) (mvarId: MVarId) (decl: MetavarDecl): MetaM String := do
+      let resultFVars: List String ←
+        if options.printContext then
+          decl.lctx.fvarIdToDecl.toList.mapM (λ (fvarId, decl) =>
+            do pure $ (← printFVar fvarId decl) ++ "\n")
+        else
+          pure []
       let type ← if options.instantiate
         then instantiateMVars 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}"
-      if options.printValue then
-        if let Option.some value := (← getMCtx).eAssignment.find? mvarId then
-          let value ← if options.instantiate
-            then instantiateMVars 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}"
+      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
+            let value ← if options.instantiate
+              then instantiateMVars value
+              else pure $ value
+            pure s!"\n := {← Meta.ppExpr value}"
+          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}]"

From e58dbc66a92ef10b014a30745a542ec0dd9be6ef Mon Sep 17 00:00:00 2001
From: Leni Aniva <v@leni.sh>
Date: Wed, 8 May 2024 20:51:36 -0700
Subject: [PATCH 20/38] fix: Consistent naming in library functions

---
 Pantograph/Library.lean | 7 +++----
 1 file changed, 3 insertions(+), 4 deletions(-)

diff --git a/Pantograph/Library.lean b/Pantograph/Library.lean
index fa5d414..3ae852f 100644
--- a/Pantograph/Library.lean
+++ b/Pantograph/Library.lean
@@ -180,6 +180,9 @@ def goalPrint (state: GoalState) (options: @&Protocol.Options): Lean.CoreM Proto
       parent? := ← state.parentExpr?.mapM (λ expr => do
         serializeExpression options (← unfoldAuxLemmas expr)),
     }
+@[export pantograph_goal_diag_m]
+def goalDiag (state: GoalState) (diagOptions: Protocol.GoalDiag) : Lean.CoreM String :=
+  runMetaM $ state.diag diagOptions
 
 @[export pantograph_goal_tactic_m]
 def goalTactic (state: GoalState) (goalId: Nat) (tactic: String): Lean.CoreM TacticResult :=
@@ -212,8 +215,4 @@ def goalMotivatedApply (state: GoalState) (goalId: Nat) (recursor: String): Lean
 def goalNoConfuse (state: GoalState) (goalId: Nat) (eq: String): Lean.CoreM TacticResult :=
   runTermElabM <| state.tryNoConfuse goalId eq
 
-@[export pantograph_goal_diag]
-def goalDiag (state: GoalState) (diagOptions: Protocol.GoalDiag) : Lean.CoreM String :=
-  runMetaM $ state.diag diagOptions
-
 end Pantograph

From 0b88f6708e299f0282f048364a885f7913525bc7 Mon Sep 17 00:00:00 2001
From: Leni Aniva <v@leni.sh>
Date: Thu, 9 May 2024 14:02:43 -0700
Subject: [PATCH 21/38] test: Delayed mvar assignment for mapply

---
 Test/Proofs.lean | 52 ++++++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 52 insertions(+)

diff --git a/Test/Proofs.lean b/Test/Proofs.lean
index 8e77227..04fe79c 100644
--- a/Test/Proofs.lean
+++ b/Test/Proofs.lean
@@ -726,6 +726,57 @@ def test_nat_zero_add: TestM Unit := do
   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 ()
+  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 := "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 state2b ← match state3m2.resume (state3m2.goals ++ state2.goals) with
+    | .ok state => pure state
+    | .error e => do
+      addTest $ assertUnreachable e
+      return ()
+  addTest $ LSpec.check "resume" ((← state2b.serializeGoals (options := ← read)).map (·.devolatilizeVars) =
+    #[buildGoal [("n", "Nat"), ("t", "Nat"), ("h", "Nat.below t")] "t + 0 = t"])
+
 def suite (env: Environment): List (String × IO LSpec.TestSeq) :=
   let tests := [
     ("Nat.add_comm", test_nat_add_comm false),
@@ -739,6 +790,7 @@ def suite (env: Environment): List (String × IO LSpec.TestSeq) :=
     ("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))
 

From 03ecb6cf19b7741a6bb20f2eb969374ac59b8643 Mon Sep 17 00:00:00 2001
From: Leni Aniva <v@leni.sh>
Date: Sat, 11 May 2024 20:01:02 -0700
Subject: [PATCH 22/38] feat: Partial instantiate metavariables

---
 Pantograph/Library.lean         |  4 ++--
 Pantograph/Serial.lean          | 32 ++++++++++++++++++-------
 Test/Integration.lean           |  4 ++--
 Test/Proofs.lean                |  2 +-
 Test/Serial.lean                |  1 +
 Test/Tactic/MotivatedApply.lean | 42 +++++++++++++++++++++++++++++++--
 6 files changed, 70 insertions(+), 15 deletions(-)

diff --git a/Pantograph/Library.lean b/Pantograph/Library.lean
index 3ae852f..59d7adc 100644
--- a/Pantograph/Library.lean
+++ b/Pantograph/Library.lean
@@ -176,9 +176,9 @@ def goalPrint (state: GoalState) (options: @&Protocol.Options): Lean.CoreM Proto
     state.restoreMetaM
     return {
       root? := ← state.rootExpr?.mapM (λ expr => do
-        serializeExpression options (← unfoldAuxLemmas expr)),
+        serializeExpression options (← instantiateAll expr)),
       parent? := ← state.parentExpr?.mapM (λ expr => do
-        serializeExpression options (← unfoldAuxLemmas expr)),
+        serializeExpression options (← instantiateAll expr)),
     }
 @[export pantograph_goal_diag_m]
 def goalDiag (state: GoalState) (diagOptions: Protocol.GoalDiag) : Lean.CoreM String :=
diff --git a/Pantograph/Serial.lean b/Pantograph/Serial.lean
index b2a4529..cdb35ce 100644
--- a/Pantograph/Serial.lean
+++ b/Pantograph/Serial.lean
@@ -18,6 +18,23 @@ namespace Pantograph
 def unfoldAuxLemmas (e : Expr) : CoreM Expr := do
   Lean.Meta.deltaExpand e Lean.Name.isAuxLemma
 
+def instantiatePartialDelayedMVars (e: Expr): MetaM Expr := do
+  Meta.transform e
+    (pre := fun e => e.withApp fun f args => do
+      if let .mvar mvarId := f then
+        if let some decl ← getDelayedMVarAssignment? mvarId then
+          if args.size ≥ decl.fvars.size then
+            let pending ← instantiateMVars (.mvar decl.mvarIdPending)
+            if !pending.isMVar then
+              return .visit <| (← Meta.mkLambdaFVars decl.fvars pending).beta args
+      return .continue)
+
+def instantiateAll (e: Expr): MetaM Expr := do
+  let e ← instantiateMVars e
+  let e ← unfoldAuxLemmas e
+  let e ← instantiatePartialDelayedMVars e
+  return e
+
 --- Input Functions ---
 
 /-- Read syntax object from string -/
@@ -103,11 +120,9 @@ partial def serializeExpressionSexp (expr: Expr) (sanitize: Bool := true): MetaM
       let name := ofName fvarId.name
       pure s!"(:fv {name})"
     | .mvar mvarId => do
-      if ← mvarId.isDelayedAssigned then
-        pure s!"(:mv)"
-      else
+        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})"
@@ -210,7 +225,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,
@@ -219,9 +234,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
@@ -248,10 +263,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 (← instantiateAll mvarDecl.type)),
       vars := vars.reverse.toArray
     }
   where
+  instantiate := instantiateAll
   ofName (n: Name) := serializeName n (sanitize := false)
 
 protected def GoalState.serializeGoals
diff --git a/Test/Integration.lean b/Test/Integration.lean
index 9bd5db6..66b3637 100644
--- a/Test/Integration.lean
+++ b/Test/Integration.lean
@@ -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 [
diff --git a/Test/Proofs.lean b/Test/Proofs.lean
index 04fe79c..496bcc8 100644
--- a/Test/Proofs.lean
+++ b/Test/Proofs.lean
@@ -245,7 +245,7 @@ def test_or_comm: TestM Unit := do
   let state2parent ← serializeExpressionSexp state2.parentExpr?.get! (sanitize := false)
   -- This is due to delayed assignment
   addTest $ LSpec.test "(2 parent)" (state2parent ==
-    "((:mv) (:fv _uniq.16) ((:c Eq.refl) ((:c Or) (:fv _uniq.10) (:fv _uniq.13)) (:fv _uniq.16)))")
+    "((:mvd _uniq.43) (:fv _uniq.16) ((:c Eq.refl) ((:c Or) (:fv _uniq.10) (:fv _uniq.13)) (:fv _uniq.16)))")
 
   let state3_1 ← match ← state2.tryTactic (goalId := 0) (tactic := "apply Or.inr") with
     | .success state => pure state
diff --git a/Test/Serial.lean b/Test/Serial.lean
index f55c18f..093dd8b 100644
--- a/Test/Serial.lean
+++ b/Test/Serial.lean
@@ -52,6 +52,7 @@ def test_sexp_of_elab (env: Environment): IO LSpec.TestSeq := do
     ("λ 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)"),
+    ("(2: Nat) <= (5: Nat)", "((:c LE.le) (:mv _uniq.37) (:mv _uniq.38) ((:c OfNat.ofNat) (:mv _uniq.23) (:lit 2) (:mv _uniq.24)) ((:c OfNat.ofNat) (:mv _uniq.33) (:lit 5) (:mv _uniq.34)))"),
   ]
   let termElabM: Elab.TermElabM LSpec.TestSeq := entries.foldlM (λ suites (source, target) => do
     let env ← MonadEnv.getEnv
diff --git a/Test/Tactic/MotivatedApply.lean b/Test/Tactic/MotivatedApply.lean
index 84ca804..ad8ebdc 100644
--- a/Test/Tactic/MotivatedApply.lean
+++ b/Test/Tactic/MotivatedApply.lean
@@ -93,12 +93,50 @@ def test_list_brec_on (env: Environment): IO LSpec.TestSeq :=
       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, exprType) ← valueAndType 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!
+      tests := tests ++ (LSpec.check "goals" ((← newGoals.mapM (λ g => do exprToStr (← g.getType))) =
+        [
+          "Nat → Prop",
+          "Nat",
+          "∀ (t : Nat), Nat.below t → ?motive t",
+          "?motive ?m.69 = (n + 0 = n)",
+        ]))
+      let [motive, major, step, conduit] := newGoals | panic! "Incorrect goal number"
+      tests := tests ++ (LSpec.check "goal name" (major.name.toString = "_uniq.69"))
+
+      -- Assign motive to `λ x => x + _`
+      let (motive_assign, _) ← valueAndType "λ (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 = "(?m.69.add + 0 = ?m.140 ?m.69) = (n + 0 = n)")
+      tests := tests ++ test
+
+      return tests
 
 def suite (env: Environment): List (String × IO LSpec.TestSeq) :=
   [
     ("type_extract", test_type_extract env),
-    ("nat_brec_on", test_nat_brec_on env),
-    ("list_brec_on", test_list_brec_on 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

From c04b363de70611f68e45c938a03dfff0be4efc34 Mon Sep 17 00:00:00 2001
From: Leni Aniva <v@leni.sh>
Date: Sun, 12 May 2024 22:33:38 -0700
Subject: [PATCH 23/38] feat: Handle delay assigned mvars

---
 Pantograph/Goal.lean   |  3 ++-
 Pantograph/Serial.lean | 35 +++++++++++++++++++++++++++++++++--
 Test/Integration.lean  |  4 ++--
 Test/Metavar.lean      |  2 +-
 Test/Proofs.lean       | 32 +++++++++++++++++++++++++++-----
 5 files changed, 65 insertions(+), 11 deletions(-)

diff --git a/Pantograph/Goal.lean b/Pantograph/Goal.lean
index 11e5b20..e1d36b3 100644
--- a/Pantograph/Goal.lean
+++ b/Pantograph/Goal.lean
@@ -98,7 +98,8 @@ 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"
+    let invalid_goals := goals.filter (λ goal => ¬ state.mvars.contains goal) |>.map (·.name.toString)
+    .error s!"Goals {invalid_goals} are 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 =>
diff --git a/Pantograph/Serial.lean b/Pantograph/Serial.lean
index cdb35ce..14a4002 100644
--- a/Pantograph/Serial.lean
+++ b/Pantograph/Serial.lean
@@ -32,7 +32,7 @@ def instantiatePartialDelayedMVars (e: Expr): MetaM Expr := do
 def instantiateAll (e: Expr): MetaM Expr := do
   let e ← instantiateMVars e
   let e ← unfoldAuxLemmas e
-  let e ← instantiatePartialDelayedMVars e
+  --let e ← instantiatePartialDelayedMVars e
   return e
 
 --- Input Functions ---
@@ -101,6 +101,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
 
@@ -109,7 +110,37 @@ 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 .mvar mvarId := e.getAppFn | return .none
+    let .some decl ← getDelayedMVarAssignment? mvarId | return .none
+    let mvarIdPending := decl.mvarIdPending
+    -- Print the function application e. See Lean's `withOverApp`
+    let args := e.getAppArgs
+
+    -- Not enough arguments to instantiate this
+    if args.size < decl.fvars.size then
+      return .none
+
+    let callee ← self $ ← instantiateMVars $ .mvar mvarIdPending
+    let sites ←
+      decl.fvars.zip args |>.mapM (λ (fvar, arg) => do
+        let fvarName := Expr.fvarId! fvar |>.name
+        return s!"({toString fvarName} {← self arg})"
+      )
+    let tailArgs ← args.toList.drop decl.fvars.size |>.mapM self
+
+
+    let sites := " ".intercalate sites.toList
+    let result := if tailArgs.isEmpty then
+        s!"(:subst {callee} {sites})"
+      else
+        let tailArgs := " ".intercalate tailArgs
+        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.
diff --git a/Test/Integration.lean b/Test/Integration.lean
index 66b3637..9bd5db6 100644
--- a/Test/Integration.lean
+++ b/Test/Integration.lean
@@ -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.17",
+    name := "_uniq.14",
     target := { pp? := .some "x ∨ y → y ∨ x" },
     vars := #[
       { name := "_uniq.10", userName := "x", isInaccessible? := .some false, type? := .some { pp? := .some "Prop" }},
-      { name := "_uniq.16", userName := "y", isInaccessible? := .some false, type? := .some { pp? := .some "Prop" }}
+      { name := "_uniq.13", userName := "y", isInaccessible? := .some false, type? := .some { pp? := .some "Prop" }}
     ],
   }
   subroutine_runner [
diff --git a/Test/Metavar.lean b/Test/Metavar.lean
index 33fe8cb..0818881 100644
--- 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
diff --git a/Test/Proofs.lean b/Test/Proofs.lean
index 496bcc8..0d31273 100644
--- a/Test/Proofs.lean
+++ b/Test/Proofs.lean
@@ -243,9 +243,10 @@ def test_or_comm: TestM Unit := do
   addTest $ LSpec.check "(2 root)" state2.rootExpr?.isNone
 
   let state2parent ← serializeExpressionSexp state2.parentExpr?.get! (sanitize := false)
-  -- This is due to delayed assignment
+  let substHead := "((:c Or.casesOn) (:fv _uniq.10) (:fv _uniq.13) (:lambda t._@._hyg.26 ((:c Or) (:fv _uniq.10) (:fv _uniq.13)) (:forall h ((:c Eq) ((:c Or) (:fv _uniq.10) (:fv _uniq.13)) (:fv _uniq.16) 0) ((:c Or) (:fv _uniq.13) (:fv _uniq.10)))) (:fv _uniq.16) (:lambda h._@._hyg.27 (:fv _uniq.10) (:subst (:lambda h._@._hyg.28 ((:c Eq) ((:c Or) (:fv _uniq.10) (:fv _uniq.13)) (:fv _uniq.16) ((:c Or.inl) (:fv _uniq.10) (:fv _uniq.13) (:fv _uniq.47))) (:subst (:subst (:mv _uniq.59) (_uniq.54 (:fv _uniq.16)) (_uniq.55 (:fv _uniq.50))) (_uniq.50 0))) (_uniq.47 0))) (:lambda h._@._hyg.29 (:fv _uniq.13) (:subst (:lambda h._@._hyg.30 ((:c Eq) ((:c Or) (:fv _uniq.10) (:fv _uniq.13)) (:fv _uniq.16) ((:c Or.inr) (:fv _uniq.10) (:fv _uniq.13) (:fv _uniq.60))) (:subst (:subst (:mv _uniq.72) (_uniq.67 (:fv _uniq.16)) (_uniq.68 (:fv _uniq.63))) (_uniq.63 0))) (_uniq.60 0))))"
+  let extra := "((:c Eq.refl) ((:c Or) (:fv _uniq.10) (:fv _uniq.13)) (:fv _uniq.16)))"
   addTest $ LSpec.test "(2 parent)" (state2parent ==
-    "((:mvd _uniq.43) (:fv _uniq.16) ((:c Eq.refl) ((:c Or) (:fv _uniq.10) (:fv _uniq.13)) (:fv _uniq.16)))")
+    s!"((:subst {substHead} (_uniq.41 (:fv _uniq.16))) {extra}")
 
   let state3_1 ← match ← state2.tryTactic (goalId := 0) (tactic := "apply Or.inr") with
     | .success state => pure state
@@ -769,13 +770,34 @@ def test_nat_zero_add_alt: TestM Unit := do
     | other => do
       addTest $ assertUnreachable $ other.toString
       return ()
-  let state2b ← match state3m2.resume (state3m2.goals ++ state2.goals) with
+  addTest $ LSpec.check tactic $ state3m2.goals.map (·.name.toString) = ["_uniq.85", "_uniq.86", "_uniq.84"]
+  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 ()
-  addTest $ LSpec.check "resume" ((← state2b.serializeGoals (options := ← read)).map (·.devolatilizeVars) =
-    #[buildGoal [("n", "Nat"), ("t", "Nat"), ("h", "Nat.below t")] "t + 0 = t"])
+
+  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"
+  addTest $ LSpec.check "resume" ((← state2b.serializeGoals (options := { ← read with printExprAST := true })) =
+    #[
+      {
+        name := "_uniq.70",
+        userName? := .some "conduit",
+        target := {
+          pp? := .some "?m.79 ?m.68 = (n + 0 = n)",
+          sexp? := .some s!"((:c Eq) (:sort 0) (:subst ((:c Eq) (:mv _uniq.84) (:mv _uniq.85) (:mv _uniq.86)) (_uniq.77 (:mv _uniq.68))) ((:c Eq) (:c Nat) ({cNatAdd} (:fv {fvN}) {cNat0}) (:fv {fvN})))",
+        },
+        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 := [

From f813d4a8dd201a01674917b18d1d39c7ec8138af Mon Sep 17 00:00:00 2001
From: Leni Aniva <v@leni.sh>
Date: Mon, 13 May 2024 13:49:05 -0700
Subject: [PATCH 24/38] refactor: Delayed mvar instantiation function

---
 Pantograph/Serial.lean | 43 +++++++++++++++++++++++++-----------------
 Test/Proofs.lean       |  8 +++++---
 2 files changed, 31 insertions(+), 20 deletions(-)

diff --git a/Pantograph/Serial.lean b/Pantograph/Serial.lean
index 14a4002..a95180e 100644
--- a/Pantograph/Serial.lean
+++ b/Pantograph/Serial.lean
@@ -101,6 +101,26 @@ partial def serializeSortLevel (level: Level) (sanitize: Bool): String :=
   | _, .zero => s!"{k}"
   | _, _ => s!"(+ {u_str} {k})"
 
+structure DelayedMVarInvocation where
+  mvarIdPending: MVarId
+  args: Array (FVarId × Expr)
+  tail: Array Expr
+
+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
+  -- Print the function application e. See Lean's `withOverApp`
+  let args := e.getAppArgs
+
+  assert! args.size >= decl.fvars.size
+
+  return .some {
+    mvarIdPending,
+    args := decl.fvars.map (·.fvarId!) |>.zip args,
+    tail := args.toList.drop decl.fvars.size |>.toArray,
+  }
+
 
 /--
  Completely serializes an expression tree. Json not used due to compactness
@@ -111,30 +131,19 @@ partial def serializeExpressionSexp (expr: Expr) (sanitize: Bool := true): MetaM
   self expr
   where
   delayedMVarToSexp (e: Expr): MetaM (Option String) := do
-    let .mvar mvarId := e.getAppFn | return .none
-    let .some decl ← getDelayedMVarAssignment? mvarId | return .none
-    let mvarIdPending := decl.mvarIdPending
-    -- Print the function application e. See Lean's `withOverApp`
-    let args := e.getAppArgs
-
-    -- Not enough arguments to instantiate this
-    if args.size < decl.fvars.size then
-      return .none
-
-    let callee ← self $ ← instantiateMVars $ .mvar mvarIdPending
-    let sites ←
-      decl.fvars.zip args |>.mapM (λ (fvar, arg) => do
-        let fvarName := Expr.fvarId! fvar |>.name
-        return s!"({toString fvarName} {← self arg})"
+    let .some invocation ← toDelayedMVarInvocation e | return .none
+    let callee ← self $ ← instantiateMVars $ .mvar invocation.mvarIdPending
+    let sites ← invocation.args.mapM (λ (fvar, arg) => do
+        pure s!"({toString fvar.name} {← self arg})"
       )
-    let tailArgs ← args.toList.drop decl.fvars.size |>.mapM self
+    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
+        let tailArgs := " ".intercalate tailArgs.toList
         s!"((:subst {callee} {sites}) {tailArgs})"
     return .some result
 
diff --git a/Test/Proofs.lean b/Test/Proofs.lean
index 0d31273..54b5016 100644
--- a/Test/Proofs.lean
+++ b/Test/Proofs.lean
@@ -748,10 +748,11 @@ def test_nat_zero_add_alt: TestM Unit := do
     | 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 "_uniq.68" [("n", "Nat")] "Nat",
+      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")
     ])
@@ -770,7 +771,8 @@ def test_nat_zero_add_alt: TestM Unit := do
     | other => do
       addTest $ assertUnreachable $ other.toString
       return ()
-  addTest $ LSpec.check tactic $ state3m2.goals.map (·.name.toString) = ["_uniq.85", "_uniq.86", "_uniq.84"]
+  let (eqL, eqR, eqT) := ("_uniq.85", "_uniq.86", "_uniq.84")
+  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
@@ -788,7 +790,7 @@ def test_nat_zero_add_alt: TestM Unit := do
         userName? := .some "conduit",
         target := {
           pp? := .some "?m.79 ?m.68 = (n + 0 = n)",
-          sexp? := .some s!"((:c Eq) (:sort 0) (:subst ((:c Eq) (:mv _uniq.84) (:mv _uniq.85) (:mv _uniq.86)) (_uniq.77 (:mv _uniq.68))) ((:c Eq) (:c Nat) ({cNatAdd} (:fv {fvN}) {cNat0}) (:fv {fvN})))",
+          sexp? := .some s!"((:c Eq) (:sort 0) (:subst ((:c Eq) (:mv {eqT}) (:mv {eqL}) (:mv {eqR})) (_uniq.77 (:mv {major}))) ((:c Eq) (:c Nat) ({cNatAdd} (:fv {fvN}) {cNat0}) (:fv {fvN})))",
         },
         vars := #[{
           name := fvN,

From bc09f4a29df6e32a1b016b6b563d58b9a26f2411 Mon Sep 17 00:00:00 2001
From: Leni Aniva <v@leni.sh>
Date: Mon, 13 May 2024 13:58:50 -0700
Subject: [PATCH 25/38] refactor: Expr related functions to Expr.lean

---
 Pantograph/Expr.lean    | 52 +++++++++++++++++++++++++++++++++++++++++
 Pantograph/Library.lean |  4 ++++
 Pantograph/Serial.lean  | 43 +---------------------------------
 3 files changed, 57 insertions(+), 42 deletions(-)
 create mode 100644 Pantograph/Expr.lean

diff --git a/Pantograph/Expr.lean b/Pantograph/Expr.lean
new file mode 100644
index 0000000..14d063e
--- /dev/null
+++ b/Pantograph/Expr.lean
@@ -0,0 +1,52 @@
+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
+
+def instantiatePartialDelayedMVars (e: Expr): MetaM Expr := do
+  Meta.transform e
+    (pre := fun e => e.withApp fun f args => do
+      if let .mvar mvarId := f then
+        if let some decl ← getDelayedMVarAssignment? mvarId then
+          if args.size ≥ decl.fvars.size then
+            let pending ← instantiateMVars (.mvar decl.mvarIdPending)
+            if !pending.isMVar then
+              return .visit <| (← Meta.mkLambdaFVars decl.fvars pending).beta args
+      return .continue)
+
+@[export pantograph_instantiate_all_meta_m]
+def instantiateAll (e: Expr): MetaM Expr := do
+  let e ← instantiateMVars e
+  let e ← unfoldAuxLemmas e
+  --let e ← instantiatePartialDelayedMVars e
+  return e
+
+structure DelayedMVarInvocation where
+  mvarIdPending: MVarId
+  args: Array (FVarId × Expr)
+  tail: Array Expr
+
+@[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
+  -- Print the function application e. See Lean's `withOverApp`
+  let args := e.getAppArgs
+
+  assert! args.size >= decl.fvars.size
+
+  return .some {
+    mvarIdPending,
+    args := decl.fvars.map (·.fvarId!) |>.zip args,
+    tail := args.toList.drop decl.fvars.size |>.toArray,
+  }
+
+end Pantograph
diff --git a/Pantograph/Library.lean b/Pantograph/Library.lean
index 59d7adc..9c64b69 100644
--- a/Pantograph/Library.lean
+++ b/Pantograph/Library.lean
@@ -78,6 +78,10 @@ def createCoreState (imports: Array String): IO Lean.Core.State := do
     (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 :=
   Environment.catalog ({}: Protocol.EnvCatalog)
diff --git a/Pantograph/Serial.lean b/Pantograph/Serial.lean
index a95180e..58d4ea7 100644
--- a/Pantograph/Serial.lean
+++ b/Pantograph/Serial.lean
@@ -2,6 +2,7 @@
 All serialisation functions
 -/
 import Lean
+import Pantograph.Expr
 
 import Pantograph.Protocol
 import Pantograph.Goal
@@ -10,30 +11,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
-
-def instantiatePartialDelayedMVars (e: Expr): MetaM Expr := do
-  Meta.transform e
-    (pre := fun e => e.withApp fun f args => do
-      if let .mvar mvarId := f then
-        if let some decl ← getDelayedMVarAssignment? mvarId then
-          if args.size ≥ decl.fvars.size then
-            let pending ← instantiateMVars (.mvar decl.mvarIdPending)
-            if !pending.isMVar then
-              return .visit <| (← Meta.mkLambdaFVars decl.fvars pending).beta args
-      return .continue)
-
-def instantiateAll (e: Expr): MetaM Expr := do
-  let e ← instantiateMVars e
-  let e ← unfoldAuxLemmas e
-  --let e ← instantiatePartialDelayedMVars e
-  return e
 
 --- Input Functions ---
 
@@ -101,26 +80,6 @@ partial def serializeSortLevel (level: Level) (sanitize: Bool): String :=
   | _, .zero => s!"{k}"
   | _, _ => s!"(+ {u_str} {k})"
 
-structure DelayedMVarInvocation where
-  mvarIdPending: MVarId
-  args: Array (FVarId × Expr)
-  tail: Array Expr
-
-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
-  -- Print the function application e. See Lean's `withOverApp`
-  let args := e.getAppArgs
-
-  assert! args.size >= decl.fvars.size
-
-  return .some {
-    mvarIdPending,
-    args := decl.fvars.map (·.fvarId!) |>.zip args,
-    tail := args.toList.drop decl.fvars.size |>.toArray,
-  }
-
 
 /--
  Completely serializes an expression tree. Json not used due to compactness

From 5c7bb288b2914d5179fa117289e4455893b3ddd2 Mon Sep 17 00:00:00 2001
From: Leni Aniva <v@leni.sh>
Date: Tue, 14 May 2024 19:08:25 -0700
Subject: [PATCH 26/38] feat: Display full free variable list in subst

---
 Pantograph/Expr.lean   | 12 ++++++++++--
 Pantograph/Serial.lean |  8 +++++---
 Test/Proofs.lean       |  8 ++++----
 3 files changed, 19 insertions(+), 9 deletions(-)

diff --git a/Pantograph/Expr.lean b/Pantograph/Expr.lean
index 14d063e..7e691d5 100644
--- a/Pantograph/Expr.lean
+++ b/Pantograph/Expr.lean
@@ -30,7 +30,7 @@ def instantiateAll (e: Expr): MetaM Expr := do
 
 structure DelayedMVarInvocation where
   mvarIdPending: MVarId
-  args: Array (FVarId × Expr)
+  args: Array (FVarId × (Option Expr))
   tail: Array Expr
 
 @[export pantograph_to_delayed_mvar_invocation_meta_m]
@@ -38,14 +38,22 @@ def toDelayedMVarInvocation (e: Expr): MetaM (Option DelayedMVarInvocation) := d
   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
+  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 := decl.fvars.map (·.fvarId!) |>.zip args,
+    args := subst.toArray,
     tail := args.toList.drop decl.fvars.size |>.toArray,
   }
 
diff --git a/Pantograph/Serial.lean b/Pantograph/Serial.lean
index 58d4ea7..3d46ee2 100644
--- a/Pantograph/Serial.lean
+++ b/Pantograph/Serial.lean
@@ -92,12 +92,14 @@ partial def serializeExpressionSexp (expr: Expr) (sanitize: Bool := true): MetaM
   delayedMVarToSexp (e: Expr): MetaM (Option String) := do
     let .some invocation ← toDelayedMVarInvocation e | return .none
     let callee ← self $ ← instantiateMVars $ .mvar invocation.mvarIdPending
-    let sites ← invocation.args.mapM (λ (fvar, arg) => do
-        pure s!"({toString fvar.name} {← self arg})"
+    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})"
diff --git a/Test/Proofs.lean b/Test/Proofs.lean
index 54b5016..b09e403 100644
--- a/Test/Proofs.lean
+++ b/Test/Proofs.lean
@@ -243,10 +243,10 @@ def test_or_comm: TestM Unit := do
   addTest $ LSpec.check "(2 root)" state2.rootExpr?.isNone
 
   let state2parent ← serializeExpressionSexp state2.parentExpr?.get! (sanitize := false)
-  let substHead := "((:c Or.casesOn) (:fv _uniq.10) (:fv _uniq.13) (:lambda t._@._hyg.26 ((:c Or) (:fv _uniq.10) (:fv _uniq.13)) (:forall h ((:c Eq) ((:c Or) (:fv _uniq.10) (:fv _uniq.13)) (:fv _uniq.16) 0) ((:c Or) (:fv _uniq.13) (:fv _uniq.10)))) (:fv _uniq.16) (:lambda h._@._hyg.27 (:fv _uniq.10) (:subst (:lambda h._@._hyg.28 ((:c Eq) ((:c Or) (:fv _uniq.10) (:fv _uniq.13)) (:fv _uniq.16) ((:c Or.inl) (:fv _uniq.10) (:fv _uniq.13) (:fv _uniq.47))) (:subst (:subst (:mv _uniq.59) (_uniq.54 (:fv _uniq.16)) (_uniq.55 (:fv _uniq.50))) (_uniq.50 0))) (_uniq.47 0))) (:lambda h._@._hyg.29 (:fv _uniq.13) (:subst (:lambda h._@._hyg.30 ((:c Eq) ((:c Or) (:fv _uniq.10) (:fv _uniq.13)) (:fv _uniq.16) ((:c Or.inr) (:fv _uniq.10) (:fv _uniq.13) (:fv _uniq.60))) (:subst (:subst (:mv _uniq.72) (_uniq.67 (:fv _uniq.16)) (_uniq.68 (:fv _uniq.63))) (_uniq.63 0))) (_uniq.60 0))))"
-  let extra := "((:c Eq.refl) ((:c Or) (:fv _uniq.10) (:fv _uniq.13)) (:fv _uniq.16)))"
+  let substHead := "((:c Or.casesOn) (:fv _uniq.10) (:fv _uniq.13) (:lambda t._@._hyg.26 ((:c Or) (:fv _uniq.10) (:fv _uniq.13)) (:forall h ((:c Eq) ((:c Or) (:fv _uniq.10) (:fv _uniq.13)) (:fv _uniq.16) 0) ((:c Or) (:fv _uniq.13) (:fv _uniq.10)))) (:fv _uniq.16) (:lambda h._@._hyg.27 (:fv _uniq.10) (:subst (:lambda h._@._hyg.28 ((:c Eq) ((:c Or) (:fv _uniq.10) (:fv _uniq.13)) (:fv _uniq.16) ((:c Or.inl) (:fv _uniq.10) (:fv _uniq.13) (:fv _uniq.47))) (:subst (:subst (:mv _uniq.59) (:fv _uniq.10) (:fv _uniq.13) (:fv _uniq.47) (:fv _uniq.16) (:fv _uniq.50)) (:fv _uniq.10) (:fv _uniq.13) (:fv _uniq.16) (:fv _uniq.47) 0)) (:fv _uniq.10) (:fv _uniq.13) (:fv _uniq.16) 0)) (:lambda h._@._hyg.29 (:fv _uniq.13) (:subst (:lambda h._@._hyg.30 ((:c Eq) ((:c Or) (:fv _uniq.10) (:fv _uniq.13)) (:fv _uniq.16) ((:c Or.inr) (:fv _uniq.10) (:fv _uniq.13) (:fv _uniq.60))) (:subst (:subst (:mv _uniq.72) (:fv _uniq.10) (:fv _uniq.13) (:fv _uniq.60) (:fv _uniq.16) (:fv _uniq.63)) (:fv _uniq.10) (:fv _uniq.13) (:fv _uniq.16) (:fv _uniq.60) 0)) (:fv _uniq.10) (:fv _uniq.13) (:fv _uniq.16) 0)))"
+  let extra := "((:c Eq.refl) ((:c Or) (:fv _uniq.10) (:fv _uniq.13)) (:fv _uniq.16))"
   addTest $ LSpec.test "(2 parent)" (state2parent ==
-    s!"((:subst {substHead} (_uniq.41 (:fv _uniq.16))) {extra}")
+    s!"((:subst {substHead} (:fv _uniq.10) (:fv _uniq.13) (:fv _uniq.16) (:fv _uniq.16)) {extra})")
 
   let state3_1 ← match ← state2.tryTactic (goalId := 0) (tactic := "apply Or.inr") with
     | .success state => pure state
@@ -790,7 +790,7 @@ def test_nat_zero_add_alt: TestM Unit := do
         userName? := .some "conduit",
         target := {
           pp? := .some "?m.79 ?m.68 = (n + 0 = n)",
-          sexp? := .some s!"((:c Eq) (:sort 0) (:subst ((:c Eq) (:mv {eqT}) (:mv {eqL}) (:mv {eqR})) (_uniq.77 (:mv {major}))) ((:c Eq) (:c Nat) ({cNatAdd} (:fv {fvN}) {cNat0}) (:fv {fvN})))",
+          sexp? := .some s!"((:c Eq) (:sort 0) (:subst ((:c Eq) (:mv {eqT}) (:mv {eqL}) (:mv {eqR})) (:fv {fvN}) (:mv {major})) ((:c Eq) (:c Nat) ({cNatAdd} (:fv {fvN}) {cNat0}) (:fv {fvN})))",
         },
         vars := #[{
           name := fvN,

From cf174280014dcfa3533e15b85a455bd2146e2951 Mon Sep 17 00:00:00 2001
From: Leni Aniva <v@leni.sh>
Date: Wed, 15 May 2024 21:34:15 -0700
Subject: [PATCH 27/38] fix: Panic in partial instantiation

---
 Pantograph/Expr.lean  | 10 ++++++++--
 Test/Integration.lean |  4 ++--
 Test/Proofs.lean      |  6 +++---
 3 files changed, 13 insertions(+), 7 deletions(-)

diff --git a/Pantograph/Expr.lean b/Pantograph/Expr.lean
index 7e691d5..85c7f35 100644
--- a/Pantograph/Expr.lean
+++ b/Pantograph/Expr.lean
@@ -14,18 +14,24 @@ def instantiatePartialDelayedMVars (e: Expr): MetaM Expr := do
   Meta.transform e
     (pre := fun e => e.withApp fun f args => do
       if let .mvar mvarId := f then
+        if ← mvarId.isAssigned then
+          return .visit <| (← instantiateMVars e)
         if let some decl ← getDelayedMVarAssignment? mvarId then
           if args.size ≥ decl.fvars.size then
+            -- Do not use instantiateMVars here. Only one step of instantiation should happen.
             let pending ← instantiateMVars (.mvar decl.mvarIdPending)
             if !pending.isMVar then
-              return .visit <| (← Meta.mkLambdaFVars decl.fvars pending).beta args
+              let pending := pending.abstract decl.fvars
+              let pending := pending.instantiateRevRange 0 decl.fvars.size args
+              let pending := mkAppRange pending decl.fvars.size args.size args
+              return .visit <| pending
       return .continue)
 
 @[export pantograph_instantiate_all_meta_m]
 def instantiateAll (e: Expr): MetaM Expr := do
   let e ← instantiateMVars e
+  let e ← instantiatePartialDelayedMVars e
   let e ← unfoldAuxLemmas e
-  --let e ← instantiatePartialDelayedMVars e
   return e
 
 structure DelayedMVarInvocation where
diff --git a/Test/Integration.lean b/Test/Integration.lean
index 9bd5db6..66b3637 100644
--- a/Test/Integration.lean
+++ b/Test/Integration.lean
@@ -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 [
diff --git a/Test/Proofs.lean b/Test/Proofs.lean
index b09e403..ea6ff11 100644
--- a/Test/Proofs.lean
+++ b/Test/Proofs.lean
@@ -771,7 +771,7 @@ def test_nat_zero_add_alt: TestM Unit := do
     | other => do
       addTest $ assertUnreachable $ other.toString
       return ()
-  let (eqL, eqR, eqT) := ("_uniq.85", "_uniq.86", "_uniq.84")
+  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
@@ -789,8 +789,8 @@ def test_nat_zero_add_alt: TestM Unit := do
         name := "_uniq.70",
         userName? := .some "conduit",
         target := {
-          pp? := .some "?m.79 ?m.68 = (n + 0 = n)",
-          sexp? := .some s!"((:c Eq) (:sort 0) (:subst ((:c Eq) (:mv {eqT}) (:mv {eqL}) (:mv {eqR})) (:fv {fvN}) (:mv {major})) ((:c Eq) (:c Nat) ({cNatAdd} (:fv {fvN}) {cNat0}) (:fv {fvN})))",
+          pp? := .some "(?motive.a = ?motive.a) = (n + 0 = n)",
+          sexp? := .some s!"((:c Eq) (:sort 0) ((:c Eq) (:mv {eqT}) (:mv {eqL}) (:mv {eqR})) ((:c Eq) (:c Nat) ({cNatAdd} (:fv {fvN}) {cNat0}) (:fv {fvN})))",
         },
         vars := #[{
           name := fvN,

From 6ad24b72d474f015543e425f148fb7a3dc7b81da Mon Sep 17 00:00:00 2001
From: Leni Aniva <v@leni.sh>
Date: Thu, 16 May 2024 10:31:38 -0700
Subject: [PATCH 28/38] fix: Nested delayed assignment instantiation

---
 Pantograph/Expr.lean   | 93 ++++++++++++++++++++++++++++++++++--------
 Pantograph/Serial.lean |  4 +-
 Test/Proofs.lean       | 37 ++++++++++++-----
 3 files changed, 106 insertions(+), 28 deletions(-)

diff --git a/Pantograph/Expr.lean b/Pantograph/Expr.lean
index 85c7f35..9f4b8d9 100644
--- a/Pantograph/Expr.lean
+++ b/Pantograph/Expr.lean
@@ -10,35 +10,94 @@ def _root_.Lean.Name.isAuxLemma (n : Lean.Name) : Bool := n matches .num (.str _
 def unfoldAuxLemmas (e : Expr) : CoreM Expr := do
   Lean.Meta.deltaExpand e Lean.Name.isAuxLemma
 
-def instantiatePartialDelayedMVars (e: Expr): MetaM Expr := do
-  Meta.transform e
+/--
+Force the instantiation of delayed metavariables even if they cannot be fully
+instantiated. This is used during resumption.
+
+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 result ← Meta.transform (← instantiateMVars eOrig)
     (pre := fun e => e.withApp fun f args => do
+      --IO.println s!"{padding} V {toString e}"
       if let .mvar mvarId := f then
         if ← mvarId.isAssigned then
-          return .visit <| (← instantiateMVars e)
-        if let some decl ← getDelayedMVarAssignment? mvarId then
-          if args.size ≥ decl.fvars.size then
-            -- Do not use instantiateMVars here. Only one step of instantiation should happen.
-            let pending ← instantiateMVars (.mvar decl.mvarIdPending)
-            if !pending.isMVar then
-              let pending := pending.abstract decl.fvars
-              let pending := pending.instantiateRevRange 0 decl.fvars.size args
-              let pending := mkAppRange pending decl.fvars.size args.size args
-              return .visit <| pending
-      return .continue)
+          --IO.println s!"{padding} A ?{mvarId.name}"
+          return .continue <| .some (← self e)
+        if let some { fvars, mvarIdPending } ← getDelayedMVarAssignment? mvarId then
+          -- No progress can be made on this
+          if !(← mvarIdPending.isAssigned) then
+            --IO.println s!"{padding} D/T1: {toString e}"
+            let args ← args.mapM self
+            let result := mkAppN f args
+            return .done result
 
+          --IO.println s!"{padding} D ?{mvarId.name} := [{fvars.size}] ?{mvarIdPending.name}"
+          -- This asstion fails when a tactic or elaboration function is
+          -- implemented incorrectly. See `instantiateExprMVars`
+          if args.size < fvars.size then
+            --IO.println s!"{padding} Illegal callsite: {args.size} < {fvars.size}"
+            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}"
+          assert! !(← mvarIdPending.isDelayedAssigned)
+          let pending ← self (.mvar mvarIdPending)
+          if pending == .mvar mvarIdPending then
+            -- No progress could be made on this case
+            --IO.println s!"{padding}D/N {toString e}"
+            assert! !(← mvarIdPending.isAssigned)
+            assert! !(← mvarIdPending.isDelayedAssigned)
+          --else if pending.isMVar then
+          --  assert! !(← pending.mvarId!.isAssigned)
+          --  assert! !(← pending.mvarId!.isDelayedAssigned)
+          --  -- Progress made, but this is now another delayed assigned mvar
+          --  let nextMVarId ← mkFreshMVarId
+          --  assignDelayedMVar nextMVarId fvars pending.mvarId!
+          --  let args ← args.mapM self
+          --  let result := mkAppN (.mvar nextMVarId) args
+          --  return .done result
+          else
+            -- Progress has been made on this mvar
+            let pending := pending.abstract fvars
+            let args ← args.mapM self
+            -- Craete the function call structure
+            let subst := pending.instantiateRevRange 0 fvars.size args
+            let result := mkAppRange subst fvars.size args.size args
+            --IO.println s!"{padding}D/T2 {toString result}"
+            return .done result
+      return .continue)
+  --IO.println s!"{padding}Result {toString result}"
+  return result
+  where
+  self e := instantiateDelayedMVars e
+
+/--
+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 ← instantiateMVars e
-  let e ← instantiatePartialDelayedMVars e
+  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
@@ -48,7 +107,9 @@ def toDelayedMVarInvocation (e: Expr): MetaM (Option DelayedMVarInvocation) := d
   -- Print the function application e. See Lean's `withOverApp`
   let args := e.getAppArgs
 
-  assert! args.size >= decl.fvars.size
+  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
diff --git a/Pantograph/Serial.lean b/Pantograph/Serial.lean
index 3d46ee2..17dee2d 100644
--- a/Pantograph/Serial.lean
+++ b/Pantograph/Serial.lean
@@ -91,7 +91,7 @@ partial def serializeExpressionSexp (expr: Expr) (sanitize: Bool := true): MetaM
   where
   delayedMVarToSexp (e: Expr): MetaM (Option String) := do
     let .some invocation ← toDelayedMVarInvocation e | return .none
-    let callee ← self $ ← instantiateMVars $ .mvar invocation.mvarIdPending
+    let callee ← self $ .mvar invocation.mvarIdPending
     let sites ← invocation.args.mapM (λ (fvarId, arg) => do
         let arg := match arg with
           | .some arg => arg
@@ -264,7 +264,7 @@ 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 (← instantiateAll mvarDecl.type)),
+      target := (← serializeExpression options (← instantiate mvarDecl.type)),
       vars := vars.reverse.toArray
     }
   where
diff --git a/Test/Proofs.lean b/Test/Proofs.lean
index ea6ff11..aa730ba 100644
--- a/Test/Proofs.lean
+++ b/Test/Proofs.lean
@@ -226,11 +226,25 @@ 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 ← 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}) (:fv {fvP}) (:fv {fvQ}) 0))))")
   let tactic := "cases h"
   let state2 ← match ← state1.tryTactic (goalId := 0) (tactic := tactic) with
     | .success state => pure state
@@ -239,22 +253,25 @@ def test_or_comm: TestM Unit := do
       return ()
   addTest $ LSpec.check tactic ((← state2.serializeGoals (options := ← read)).map (·.devolatilize) =
     #[branchGoal "inl" "p", branchGoal "inr" "q"])
+  let (caseL, caseR) := ("_uniq.62", "_uniq.75")
+  addTest $ LSpec.check tactic ((← state2.serializeGoals (options := ← read)).map (·.name) =
+    #[caseL, caseR])
   addTest $ LSpec.check "(2 parent)" state2.parentExpr?.isSome
   addTest $ LSpec.check "(2 root)" state2.rootExpr?.isNone
 
-  let state2parent ← serializeExpressionSexp state2.parentExpr?.get! (sanitize := false)
-  let substHead := "((:c Or.casesOn) (:fv _uniq.10) (:fv _uniq.13) (:lambda t._@._hyg.26 ((:c Or) (:fv _uniq.10) (:fv _uniq.13)) (:forall h ((:c Eq) ((:c Or) (:fv _uniq.10) (:fv _uniq.13)) (:fv _uniq.16) 0) ((:c Or) (:fv _uniq.13) (:fv _uniq.10)))) (:fv _uniq.16) (:lambda h._@._hyg.27 (:fv _uniq.10) (:subst (:lambda h._@._hyg.28 ((:c Eq) ((:c Or) (:fv _uniq.10) (:fv _uniq.13)) (:fv _uniq.16) ((:c Or.inl) (:fv _uniq.10) (:fv _uniq.13) (:fv _uniq.47))) (:subst (:subst (:mv _uniq.59) (:fv _uniq.10) (:fv _uniq.13) (:fv _uniq.47) (:fv _uniq.16) (:fv _uniq.50)) (:fv _uniq.10) (:fv _uniq.13) (:fv _uniq.16) (:fv _uniq.47) 0)) (:fv _uniq.10) (:fv _uniq.13) (:fv _uniq.16) 0)) (:lambda h._@._hyg.29 (:fv _uniq.13) (:subst (:lambda h._@._hyg.30 ((:c Eq) ((:c Or) (:fv _uniq.10) (:fv _uniq.13)) (:fv _uniq.16) ((:c Or.inr) (:fv _uniq.10) (:fv _uniq.13) (:fv _uniq.60))) (:subst (:subst (:mv _uniq.72) (:fv _uniq.10) (:fv _uniq.13) (:fv _uniq.60) (:fv _uniq.16) (:fv _uniq.63)) (:fv _uniq.10) (:fv _uniq.13) (:fv _uniq.16) (:fv _uniq.60) 0)) (:fv _uniq.10) (:fv _uniq.13) (:fv _uniq.16) 0)))"
-  let extra := "((:c Eq.refl) ((:c Or) (:fv _uniq.10) (:fv _uniq.13)) (:fv _uniq.16))"
+  let state2parent ← 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}))"
   addTest $ LSpec.test "(2 parent)" (state2parent ==
-    s!"((:subst {substHead} (:fv _uniq.10) (:fv _uniq.13) (:fv _uniq.16) (:fv _uniq.16)) {extra})")
+    s!"((:c Or.casesOn) (:fv {fvP}) (:fv {fvQ}) (:lambda t._@._hyg.26 {orPQ} (:forall h ((:c Eq) {orPQ} (:fv {fvH}) 0) {orQP})) (:fv {fvH}) (:lambda h._@._hyg.27 (:fv {fvP}) (:lambda h._@._hyg.28 ((:c Eq) {orPQ} (:fv {fvH}) ((:c Or.inl) (:fv {fvP}) (:fv {fvQ}) 0)) (:mv {caseL}))) (:lambda h._@._hyg.29 (:fv {fvQ}) (:lambda h._@._hyg.30 ((:c Eq) {orPQ} (:fv {fvH}) ((:c Or.inr) (:fv {fvP}) (:fv {fvQ}) 0)) (:mv {caseR}))) ((:c Eq.refl) {orPQ} (:fv {fvH})))")
 
   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 ← 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.87))")
   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
@@ -262,8 +279,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

From 2f951c8fefcf3566fd5f2b38c508db96ef5cba00 Mon Sep 17 00:00:00 2001
From: Leni Aniva <v@leni.sh>
Date: Sun, 19 May 2024 15:43:10 -0700
Subject: [PATCH 29/38] fix: Decoupling of mvars during instantiation

---
 Pantograph/Expr.lean    | 114 ++++++++++++++++++++++------------------
 Pantograph/Goal.lean    |  10 ++++
 Pantograph/Library.lean |  10 ++--
 Pantograph/Serial.lean  |   2 +-
 Test/Proofs.lean        |  51 ++++++++++++++----
 5 files changed, 122 insertions(+), 65 deletions(-)

diff --git a/Pantograph/Expr.lean b/Pantograph/Expr.lean
index 9f4b8d9..8f890e3 100644
--- a/Pantograph/Expr.lean
+++ b/Pantograph/Expr.lean
@@ -12,7 +12,8 @@ def unfoldAuxLemmas (e : Expr) : CoreM Expr := do
 
 /--
 Force the instantiation of delayed metavariables even if they cannot be fully
-instantiated. This is used during resumption.
+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
@@ -24,60 +25,73 @@ 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 "  "
+partial def instantiateDelayedMVars (eOrig: Expr) : MetaM Expr := do
+  --let padding := String.join $ List.replicate level "│ "
   --IO.println s!"{padding}Starting {toString eOrig}"
-  let result ← Meta.transform (← instantiateMVars eOrig)
+  let mut result ← Meta.transform (← instantiateMVars eOrig)
     (pre := fun e => e.withApp fun f args => do
-      --IO.println s!"{padding} V {toString e}"
-      if let .mvar mvarId := f then
-        if ← mvarId.isAssigned then
-          --IO.println s!"{padding} A ?{mvarId.name}"
-          return .continue <| .some (← self e)
-        if let some { fvars, mvarIdPending } ← getDelayedMVarAssignment? mvarId then
-          -- No progress can be made on this
-          if !(← mvarIdPending.isAssigned) then
-            --IO.println s!"{padding} D/T1: {toString e}"
-            let args ← args.mapM self
-            let result := mkAppN f args
-            return .done result
+      let .mvar mvarId := f | return .continue
+      --IO.println s!"{padding}├V {e}"
+      let mvarDecl ← mvarId.getDecl
 
-          --IO.println s!"{padding} D ?{mvarId.name} := [{fvars.size}] ?{mvarIdPending.name}"
-          -- This asstion fails when a tactic or elaboration function is
-          -- implemented incorrectly. See `instantiateExprMVars`
-          if args.size < fvars.size then
-            --IO.println s!"{padding} Illegal callsite: {args.size} < {fvars.size}"
-            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}"
-          assert! !(← mvarIdPending.isDelayedAssigned)
-          let pending ← self (.mvar mvarIdPending)
-          if pending == .mvar mvarIdPending then
-            -- No progress could be made on this case
-            --IO.println s!"{padding}D/N {toString e}"
-            assert! !(← mvarIdPending.isAssigned)
-            assert! !(← mvarIdPending.isDelayedAssigned)
-          --else if pending.isMVar then
-          --  assert! !(← pending.mvarId!.isAssigned)
-          --  assert! !(← pending.mvarId!.isDelayedAssigned)
-          --  -- Progress made, but this is now another delayed assigned mvar
-          --  let nextMVarId ← mkFreshMVarId
-          --  assignDelayedMVar nextMVarId fvars pending.mvarId!
-          --  let args ← args.mapM self
-          --  let result := mkAppN (.mvar nextMVarId) args
-          --  return .done result
-          else
-            -- Progress has been made on this mvar
-            let pending := pending.abstract fvars
-            let args ← args.mapM self
-            -- Craete the function call structure
-            let subst := pending.instantiateRevRange 0 fvars.size args
-            let result := mkAppRange subst fvars.size args.size args
-            --IO.println s!"{padding}D/T2 {toString result}"
-            return .done result
-      return .continue)
-  --IO.println s!"{padding}Result {toString result}"
+      -- 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}"
+          let r := (← Expr.abstractM inner fvars).instantiateRev args
+          pure r
+
+        -- Tail arguments
+        let result := mkAppN pending (List.drop fvars.size args.toList |>.toArray)
+        --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
+  self e := instantiateDelayedMVars e --(level := level + 1)
 
 /--
 Convert an expression to an equiavlent form with
diff --git a/Pantograph/Goal.lean b/Pantograph/Goal.lean
index e1d36b3..8efc20f 100644
--- a/Pantograph/Goal.lean
+++ b/Pantograph/Goal.lean
@@ -62,6 +62,16 @@ 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 :=
diff --git a/Pantograph/Library.lean b/Pantograph/Library.lean
index 9c64b69..34e1ecc 100644
--- a/Pantograph/Library.lean
+++ b/Pantograph/Library.lean
@@ -179,10 +179,12 @@ def goalPrint (state: GoalState) (options: @&Protocol.Options): Lean.CoreM Proto
   runMetaM do
     state.restoreMetaM
     return {
-      root? := ← state.rootExpr?.mapM (λ expr => do
-        serializeExpression options (← instantiateAll expr)),
-      parent? := ← state.parentExpr?.mapM (λ expr => do
-        serializeExpression options (← instantiateAll 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) : Lean.CoreM String :=
diff --git a/Pantograph/Serial.lean b/Pantograph/Serial.lean
index 17dee2d..a6c0ece 100644
--- a/Pantograph/Serial.lean
+++ b/Pantograph/Serial.lean
@@ -264,7 +264,7 @@ 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 (← instantiate mvarDecl.type)),
+      target := (← serializeExpression options (← instantiateMVars (← instantiate mvarDecl.type))),
       vars := vars.reverse.toArray
     }
   where
diff --git a/Test/Proofs.lean b/Test/Proofs.lean
index aa730ba..9c45138 100644
--- a/Test/Proofs.lean
+++ b/Test/Proofs.lean
@@ -84,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
@@ -243,8 +264,9 @@ def test_or_comm: TestM Unit := do
   addTest $ LSpec.check "(1 parent)" state1.parentExpr?.isSome
   addTest $ LSpec.check "(1 root)" state1.rootExpr?.isNone
 
-  let state1parent ← 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}) (:fv {fvP}) (:fv {fvQ}) 0))))")
+  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
@@ -253,25 +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"])
-  let (caseL, caseR) := ("_uniq.62", "_uniq.75")
+  let (caseL, caseR) := ("_uniq.64", "_uniq.77")
   addTest $ LSpec.check tactic ((← state2.serializeGoals (options := ← read)).map (·.name) =
     #[caseL, caseR])
-  addTest $ LSpec.check "(2 parent)" state2.parentExpr?.isSome
+  addTest $ LSpec.check "(2 parent exists)" state2.parentExpr?.isSome
   addTest $ LSpec.check "(2 root)" state2.rootExpr?.isNone
 
-  let state2parent ← serializeExpressionSexp (← instantiateAll state2.parentExpr?.get!) (sanitize := false)
+  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 ==
-    s!"((:c Or.casesOn) (:fv {fvP}) (:fv {fvQ}) (:lambda t._@._hyg.26 {orPQ} (:forall h ((:c Eq) {orPQ} (:fv {fvH}) 0) {orQP})) (:fv {fvH}) (:lambda h._@._hyg.27 (:fv {fvP}) (:lambda h._@._hyg.28 ((:c Eq) {orPQ} (:fv {fvH}) ((:c Or.inl) (:fv {fvP}) (:fv {fvQ}) 0)) (:mv {caseL}))) (:lambda h._@._hyg.29 (:fv {fvQ}) (:lambda h._@._hyg.30 ((:c Eq) {orPQ} (:fv {fvH}) ((:c Or.inr) (:fv {fvP}) (:fv {fvQ}) 0)) (:mv {caseR}))) ((:c Eq.refl) {orPQ} (:fv {fvH})))")
+    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 (← 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.87))")
+  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
@@ -800,14 +828,16 @@ def test_nat_zero_add_alt: TestM Unit := do
   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 "(?motive.a = ?motive.a) = (n + 0 = n)",
-          sexp? := .some s!"((:c Eq) (:sort 0) ((:c Eq) (:mv {eqT}) (:mv {eqL}) (:mv {eqR})) ((:c Eq) (:c Nat) ({cNatAdd} (:fv {fvN}) {cNat0}) (:fv {fvN})))",
+          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,
@@ -820,6 +850,7 @@ def test_nat_zero_add_alt: TestM Unit := do
 
 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),

From cc74d41b150343215f40f391b52f308adc14a65c Mon Sep 17 00:00:00 2001
From: Leni Aniva <v@leni.sh>
Date: Mon, 20 May 2024 10:55:52 -0700
Subject: [PATCH 30/38] feat: Congruence tactics

---
 Pantograph/Tactic.lean            |  1 +
 Pantograph/Tactic/Congruence.lean | 78 +++++++++++++++++++++++++++++++
 2 files changed, 79 insertions(+)
 create mode 100644 Pantograph/Tactic/Congruence.lean

diff --git a/Pantograph/Tactic.lean b/Pantograph/Tactic.lean
index 5a7828c..225ad31 100644
--- a/Pantograph/Tactic.lean
+++ b/Pantograph/Tactic.lean
@@ -1,3 +1,4 @@
 
+import Pantograph.Tactic.Congruence
 import Pantograph.Tactic.MotivatedApply
 import Pantograph.Tactic.NoConfuse
diff --git a/Pantograph/Tactic/Congruence.lean b/Pantograph/Tactic/Congruence.lean
new file mode 100644
index 0000000..3de904f
--- /dev/null
+++ b/Pantograph/Tactic/Congruence.lean
@@ -0,0 +1,78 @@
+import Lean
+
+open Lean
+
+namespace Pantograph.Tactic
+
+def congruenceArg: Elab.Tactic.TacticM Unit := do
+  let goal ← Elab.Tactic.getMainGoal
+  let .some (beta, _, _) := (← goal.getType).eq? | throwError "Goal is not an Eq"
+  -- Create the descendant goals
+
+  let nextGoals ← goal.withContext do
+    let u ← Meta.mkFreshLevelMVar
+    let alpha ← Meta.mkFreshExprMVar (.some $ mkSort u) .natural .anonymous
+    let f ← Meta.mkFreshExprMVar (.some <| .forallE .anonymous alpha beta .default)
+      .synthetic (userName := goal.name ++ `f)
+    let a₁ ← Meta.mkFreshExprMVar (.some alpha)
+      .synthetic (userName := goal.name ++ `a₁)
+    let a₂ ← Meta.mkFreshExprMVar (.some alpha)
+      .synthetic (userName := goal.name ++ `a₂)
+    let h ← Meta.mkEq a₁ a₂
+    let conduitType ← Meta.mkEq (← Meta.mkEq (.app f a₁) (.app f a₂)) (← goal.getType)
+    let conduit ← Meta.mkFreshExprMVar conduitType
+      .synthetic (userName := goal.name ++ `conduit)
+    goal.assign $ ← Meta.mkEqMP conduit (← Meta.mkCongrArg f h)
+    return [alpha, 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 (beta, _, _) := (← goal.getType).eq? | throwError "Goal is not an Eq"
+  -- Create the descendant goals
+
+  let nextGoals ← goal.withContext do
+    let u ← Meta.mkFreshLevelMVar
+    let alpha ← Meta.mkFreshExprMVar (.some $ mkSort u) .natural .anonymous
+    let fType := .forallE .anonymous alpha beta .default
+    let f₁ ← Meta.mkFreshExprMVar (.some fType)
+      .synthetic (userName := goal.name ++ `f₁)
+    let f₂ ← Meta.mkFreshExprMVar (.some fType)
+      .synthetic (userName := goal.name ++ `f₂)
+    let a ← Meta.mkFreshExprMVar (.some alpha)
+      .synthetic (userName := goal.name ++ `a)
+    let h ← Meta.mkEq f₁ f₂
+    let conduitType ← Meta.mkEq (← Meta.mkEq (.app f₁ a) (.app f₂ a)) (← goal.getType)
+    let conduit ← Meta.mkFreshExprMVar conduitType
+      .synthetic (userName := goal.name ++ `conduit)
+    goal.assign $ ← Meta.mkEqMP conduit (← Meta.mkCongrFun h a)
+    return [alpha, 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 (beta, _, _) := (← goal.getType).eq? | throwError "Goal is not an Eq"
+  -- Create the descendant goals
+
+  let nextGoals ← goal.withContext do
+    let u ← Meta.mkFreshLevelMVar
+    let alpha ← Meta.mkFreshExprMVar (.some $ mkSort u) .natural .anonymous
+    let fType := .forallE .anonymous alpha beta .default
+    let f₁ ← Meta.mkFreshExprMVar (.some fType)
+      .synthetic (userName := goal.name ++ `f₁)
+    let f₂ ← Meta.mkFreshExprMVar (.some fType)
+      .synthetic (userName := goal.name ++ `f₂)
+    let a₁ ← Meta.mkFreshExprMVar (.some alpha)
+      .synthetic (userName := goal.name ++ `a₁)
+    let a₂ ← Meta.mkFreshExprMVar (.some alpha)
+      .synthetic (userName := goal.name ++ `a₂)
+    let h₁ ← Meta.mkEq f₁ f₂
+    let h₂ ← Meta.mkEq a₁ a₂
+    let conduitType ← Meta.mkEq (← Meta.mkEq (.app f₁ a₁) (.app f₂ a₂)) (← goal.getType)
+    let conduit ← Meta.mkFreshExprMVar conduitType
+      .synthetic (userName := goal.name ++ `conduit)
+    goal.assign $ ← Meta.mkEqMP conduit (← Meta.mkCongr h₁ h₂)
+    return [alpha, f₁, f₂, a₁, a₂, h₁, h₂, conduit]
+  Elab.Tactic.setGoals <| nextGoals.map (·.mvarId!)
+
+end Pantograph.Tactic

From 92acf7782c66f9efc6026a5896be35b84b202f5d Mon Sep 17 00:00:00 2001
From: Leni Aniva <v@leni.sh>
Date: Mon, 20 May 2024 11:51:35 -0700
Subject: [PATCH 31/38] test: CongruenceArg tactic

---
 Pantograph/Tactic/Congruence.lean | 81 +++++++++++++++++--------------
 Test/Common.lean                  | 15 ++++++
 Test/Main.lean                    |  1 +
 Test/Tactic.lean                  |  1 +
 Test/Tactic/Congruence.lean       | 36 ++++++++++++++
 Test/Tactic/NoConfuse.lean        |  6 +--
 6 files changed, 100 insertions(+), 40 deletions(-)
 create mode 100644 Test/Tactic/Congruence.lean

diff --git a/Pantograph/Tactic/Congruence.lean b/Pantograph/Tactic/Congruence.lean
index 3de904f..bbb9d75 100644
--- a/Pantograph/Tactic/Congruence.lean
+++ b/Pantograph/Tactic/Congruence.lean
@@ -6,73 +6,80 @@ namespace Pantograph.Tactic
 
 def congruenceArg: Elab.Tactic.TacticM Unit := do
   let goal ← Elab.Tactic.getMainGoal
-  let .some (beta, _, _) := (← goal.getType).eq? | throwError "Goal is not an Eq"
-  -- Create the descendant goals
+  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 alpha ← Meta.mkFreshExprMVar (.some $ mkSort u) .natural .anonymous
-    let f ← Meta.mkFreshExprMVar (.some <| .forallE .anonymous alpha beta .default)
-      .synthetic (userName := goal.name ++ `f)
-    let a₁ ← Meta.mkFreshExprMVar (.some alpha)
-      .synthetic (userName := goal.name ++ `a₁)
-    let a₂ ← Meta.mkFreshExprMVar (.some alpha)
-      .synthetic (userName := goal.name ++ `a₂)
-    let h ← Meta.mkEq a₁ a₂
+    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 := goal.name ++ `conduit)
+      .synthetic (userName := userName ++ `conduit)
     goal.assign $ ← Meta.mkEqMP conduit (← Meta.mkCongrArg f h)
-    return [alpha, a₁, a₂, f,  h, conduit]
+    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 (beta, _, _) := (← goal.getType).eq? | throwError "Goal is not an Eq"
-  -- Create the descendant goals
+  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 alpha ← Meta.mkFreshExprMVar (.some $ mkSort u) .natural .anonymous
-    let fType := .forallE .anonymous alpha beta .default
+    let α ← Meta.mkFreshExprMVar (.some $ mkSort u)
+      .natural (userName := userName ++ `α)
+    let fType := .forallE .anonymous α β .default
     let f₁ ← Meta.mkFreshExprMVar (.some fType)
-      .synthetic (userName := goal.name ++ `f₁)
+      .synthetic (userName := userName ++ `f₁)
     let f₂ ← Meta.mkFreshExprMVar (.some fType)
-      .synthetic (userName := goal.name ++ `f₂)
-    let a ← Meta.mkFreshExprMVar (.some alpha)
-      .synthetic (userName := goal.name ++ `a)
-    let h ← Meta.mkEq f₁ f₂
+      .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 := goal.name ++ `conduit)
+      .synthetic (userName := userName ++ `conduit)
     goal.assign $ ← Meta.mkEqMP conduit (← Meta.mkCongrFun h a)
-    return [alpha, f₁, f₂, h, a, conduit]
+    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 (beta, _, _) := (← goal.getType).eq? | throwError "Goal is not an Eq"
-  -- Create the descendant goals
+  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 alpha ← Meta.mkFreshExprMVar (.some $ mkSort u) .natural .anonymous
-    let fType := .forallE .anonymous alpha beta .default
+    let α ← Meta.mkFreshExprMVar (.some $ mkSort u)
+      .natural (userName := userName ++ `α)
+    let fType := .forallE .anonymous α β .default
     let f₁ ← Meta.mkFreshExprMVar (.some fType)
-      .synthetic (userName := goal.name ++ `f₁)
+      .synthetic (userName := userName ++ `f₁)
     let f₂ ← Meta.mkFreshExprMVar (.some fType)
-      .synthetic (userName := goal.name ++ `f₂)
-    let a₁ ← Meta.mkFreshExprMVar (.some alpha)
-      .synthetic (userName := goal.name ++ `a₁)
-    let a₂ ← Meta.mkFreshExprMVar (.some alpha)
-      .synthetic (userName := goal.name ++ `a₂)
-    let h₁ ← Meta.mkEq f₁ f₂
-    let h₂ ← Meta.mkEq a₁ a₂
+      .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 := goal.name ++ `conduit)
+      .synthetic (userName := userName ++ `conduit)
     goal.assign $ ← Meta.mkEqMP conduit (← Meta.mkCongr h₁ h₂)
-    return [alpha, f₁, f₂, a₁, a₂, h₁, h₂, conduit]
+    return [α, f₁, f₂, a₁, a₂, h₁, h₂, conduit]
   Elab.Tactic.setGoals <| nextGoals.map (·.mvarId!)
 
 end Pantograph.Tactic
diff --git a/Test/Common.lean b/Test/Common.lean
index 6ea4fb2..c656309 100644
--- a/Test/Common.lean
+++ b/Test/Common.lean
@@ -27,6 +27,7 @@ def Goal.devolatilize (goal: Goal): Goal :=
     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
@@ -65,9 +66,23 @@ def runTermElabMInMeta { α } (termElabM: Lean.Elab.TermElabM α): Lean.MetaM α
 
 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
 
diff --git a/Test/Main.lean b/Test/Main.lean
index 4a1ca69..31042c5 100644
--- a/Test/Main.lean
+++ b/Test/Main.lean
@@ -49,6 +49,7 @@ 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),
   ]
diff --git a/Test/Tactic.lean b/Test/Tactic.lean
index f1e2649..5863ec0 100644
--- a/Test/Tactic.lean
+++ b/Test/Tactic.lean
@@ -1,2 +1,3 @@
+import Test.Tactic.Congruence
 import Test.Tactic.MotivatedApply
 import Test.Tactic.NoConfuse
diff --git a/Test/Tactic/Congruence.lean b/Test/Tactic/Congruence.lean
new file mode 100644
index 0000000..7ef358a
--- /dev/null
+++ b/Test/Tactic/Congruence.lean
@@ -0,0 +1,36 @@
+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 suite (env: Environment): List (String × IO LSpec.TestSeq) :=
+  [
+    ("congrArg", test_congr_arg env),
+  ]
+
+end Pantograph.Test.Tactic.Congruence
diff --git a/Test/Tactic/NoConfuse.lean b/Test/Tactic/NoConfuse.lean
index 54c2be7..442e2ca 100644
--- a/Test/Tactic/NoConfuse.lean
+++ b/Test/Tactic/NoConfuse.lean
@@ -92,9 +92,9 @@ def test_list (env: Environment): IO LSpec.TestSeq :=
 
 def suite (env: Environment): List (String × IO LSpec.TestSeq) :=
   [
-    ("nat", test_nat env),
-    ("nat_fail", test_nat_fail env),
-    ("list", test_list env),
+    ("Nat", test_nat env),
+    ("Nat fail", test_nat_fail env),
+    ("List", test_list env),
   ]
 
 end Pantograph.Test.Tactic.NoConfuse

From 75df7268c5c229769c606963b2ef2bb178810bdd Mon Sep 17 00:00:00 2001
From: Leni Aniva <v@leni.sh>
Date: Mon, 20 May 2024 11:55:38 -0700
Subject: [PATCH 32/38] test: Simplify testing structure for tactics

---
 Test/Tactic/MotivatedApply.lean | 44 ++++++++++++---------------------
 Test/Tactic/NoConfuse.lean      | 19 +++-----------
 2 files changed, 19 insertions(+), 44 deletions(-)

diff --git a/Test/Tactic/MotivatedApply.lean b/Test/Tactic/MotivatedApply.lean
index ad8ebdc..154e34c 100644
--- a/Test/Tactic/MotivatedApply.lean
+++ b/Test/Tactic/MotivatedApply.lean
@@ -7,24 +7,11 @@ open Pantograph
 
 namespace Pantograph.Test.Tactic.MotivatedApply
 
-def valueAndType (recursor: String): MetaM (Expr × Expr) := do
-  let recursor ← match Parser.runParserCategory
-    (env := ← MonadEnv.getEnv)
-    (catName := `term)
-    (input := recursor)
-    (fileName := filename) with
-    | .ok syn => pure syn
-    | .error error => throwError "Failed to parse: {error}"
-  runTermElabMInMeta do
-    let recursor ← Elab.Term.elabTerm (stx := recursor) .none
-    let recursorType ← Meta.inferType recursor
-    return (recursor, recursorType)
-
-
 def test_type_extract (env: Environment): IO LSpec.TestSeq :=
   runMetaMSeq env do
     let mut tests := LSpec.TestSeq.done
-    let (recursor, recursorType) ← valueAndType "@Nat.brecOn"
+    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
@@ -39,7 +26,7 @@ def test_type_extract (env: Environment): IO LSpec.TestSeq :=
 def test_nat_brec_on (env: Environment): IO LSpec.TestSeq :=
   let expr := "λ (n t: Nat) => n + 0 = n"
   runMetaMSeq env do
-    let (expr, exprType) ← valueAndType expr
+    let expr ← parseSentence expr
     Meta.lambdaTelescope expr $ λ _ body => do
       let recursor ← match Parser.runParserCategory
         (env := ← MonadEnv.getEnv)
@@ -59,7 +46,7 @@ def test_nat_brec_on (env: Environment): IO LSpec.TestSeq :=
             "Nat → Prop",
             "Nat",
             "∀ (t : Nat), Nat.below t → ?motive t",
-            "?motive ?m.69 = (n + 0 = n)",
+            "?motive ?m.67 = (n + 0 = n)",
           ])
       tests := tests ++ test
       return tests
@@ -67,7 +54,7 @@ def test_nat_brec_on (env: Environment): IO LSpec.TestSeq :=
 def test_list_brec_on (env: Environment): IO LSpec.TestSeq :=
   let expr := "λ {α : Type} (l: List α) => l ++ [] = [] ++ l"
   runMetaMSeq env do
-    let (expr, exprType) ← valueAndType expr
+    let expr ← parseSentence expr
     Meta.lambdaTelescope expr $ λ _ body => do
       let recursor ← match Parser.runParserCategory
         (env := ← MonadEnv.getEnv)
@@ -84,11 +71,11 @@ def test_list_brec_on (env: Environment): IO LSpec.TestSeq :=
         let newGoals ← runTacticOnMVar tactic target.mvarId!
         pure $ LSpec.check "goals" ((← newGoals.mapM (λ g => do exprToStr (← g.getType))) =
           [
-            "Type ?u.92",
-            "List ?m.94 → Prop",
-            "List ?m.94",
-            "∀ (t : List ?m.94), List.below t → ?motive t",
-            "?motive ?m.96 = (l ++ [] = [] ++ l)",
+            "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
@@ -103,30 +90,31 @@ def test_partial_motive_instantiation (env: Environment): IO LSpec.TestSeq := do
       (fileName := filename) with
       | .ok syn => pure syn
       | .error error => throwError "Failed to parse: {error}"
-    let (expr, exprType) ← valueAndType expr
+    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",
-          "?motive ?m.69 = (n + 0 = n)",
+          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 = "_uniq.69"))
+      tests := tests ++ (LSpec.check "goal name" (major.name.toString = s!"_uniq.{majorId}"))
 
       -- Assign motive to `λ x => x + _`
-      let (motive_assign, _) ← valueAndType "λ (x: Nat) => @Nat.add x + 0 = _"
+      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 = "(?m.69.add + 0 = ?m.140 ?m.69) = (n + 0 = n)")
+        return LSpec.check "conduit" (t = s!"(?m.{majorId}.add + 0 = ?m.138 ?m.{majorId}) = (n + 0 = n)")
       tests := tests ++ test
 
       return tests
diff --git a/Test/Tactic/NoConfuse.lean b/Test/Tactic/NoConfuse.lean
index 442e2ca..c672a0b 100644
--- a/Test/Tactic/NoConfuse.lean
+++ b/Test/Tactic/NoConfuse.lean
@@ -7,23 +7,10 @@ open Pantograph
 
 namespace Pantograph.Test.Tactic.NoConfuse
 
-def valueAndType (recursor: String): MetaM (Expr × Expr) := do
-  let recursor ← match Parser.runParserCategory
-    (env := ← MonadEnv.getEnv)
-    (catName := `term)
-    (input := recursor)
-    (fileName := filename) with
-    | .ok syn => pure syn
-    | .error error => throwError "Failed to parse: {error}"
-  runTermElabMInMeta do
-    let recursor ← Elab.Term.elabTerm (stx := recursor) .none
-    let recursorType ← Meta.inferType recursor
-    return (recursor, recursorType)
-
 def test_nat (env: Environment): IO LSpec.TestSeq :=
   let expr := "λ (n: Nat) (h: 0 = n + 1) => False"
   runMetaMSeq env do
-    let (expr, exprType) ← valueAndType expr
+    let expr ← parseSentence expr
     Meta.lambdaTelescope expr $ λ _ body => do
       let recursor ← match Parser.runParserCategory
         (env := ← MonadEnv.getEnv)
@@ -46,7 +33,7 @@ def test_nat (env: Environment): IO LSpec.TestSeq :=
 def test_nat_fail (env: Environment): IO LSpec.TestSeq :=
   let expr := "λ (n: Nat) (h: n = n) => False"
   runMetaMSeq env do
-    let (expr, _) ← valueAndType expr
+    let expr ← parseSentence expr
     Meta.lambdaTelescope expr $ λ _ body => do
       let recursor ← match Parser.runParserCategory
         (env := ← MonadEnv.getEnv)
@@ -70,7 +57,7 @@ def test_nat_fail (env: Environment): IO LSpec.TestSeq :=
 def test_list (env: Environment): IO LSpec.TestSeq :=
   let expr := "λ (l: List Nat) (h: [] = 1 :: l) => False"
   runMetaMSeq env do
-    let (expr, exprType) ← valueAndType expr
+    let expr ← parseSentence expr
     Meta.lambdaTelescope expr $ λ _ body => do
       let recursor ← match Parser.runParserCategory
         (env := ← MonadEnv.getEnv)

From bbc00cbbb80748a53c2741bd2e4ee1415ba92f8d Mon Sep 17 00:00:00 2001
From: Leni Aniva <v@leni.sh>
Date: Mon, 20 May 2024 14:00:04 -0700
Subject: [PATCH 33/38] feat: Congruence tactic FFI interface and tests

---
 Pantograph/Goal.lean        | 12 +---------
 Pantograph/Library.lean     | 16 ++++++++++++++
 Test/Tactic/Congruence.lean | 44 +++++++++++++++++++++++++++++++++++++
 3 files changed, 61 insertions(+), 11 deletions(-)

diff --git a/Pantograph/Goal.lean b/Pantograph/Goal.lean
index 3a8e2fe..46888e7 100644
--- a/Pantograph/Goal.lean
+++ b/Pantograph/Goal.lean
@@ -76,7 +76,7 @@ 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
@@ -518,11 +518,6 @@ protected def GoalState.tryCalc (state: GoalState) (goalId: Nat) (pred: String):
 protected def GoalState.tryMotivatedApply (state: GoalState) (goalId: Nat) (recursor: String):
       Elab.TermElabM TacticResult := do
   state.restoreElabM
-  let goal ← match state.savedState.tactic.goals.get? goalId with
-    | .some goal => pure goal
-    | .none => return .indexError goalId
-  goal.checkNotAssigned `GoalState.tryMotivatedApply
-
   let recursor ← match Parser.runParserCategory
     (env := state.env)
     (catName := `term)
@@ -534,11 +529,6 @@ protected def GoalState.tryMotivatedApply (state: GoalState) (goalId: Nat) (recu
 protected def GoalState.tryNoConfuse (state: GoalState) (goalId: Nat) (eq: 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.tryMotivatedApply
-
   let recursor ← match Parser.runParserCategory
     (env := state.env)
     (catName := `term)
diff --git a/Pantograph/Library.lean b/Pantograph/Library.lean
index 20eaa34..e0625e8 100644
--- a/Pantograph/Library.lean
+++ b/Pantograph/Library.lean
@@ -204,4 +204,20 @@ def goalMotivatedApply (state: GoalState) (goalId: Nat) (recursor: String): Lean
 def goalNoConfuse (state: GoalState) (goalId: Nat) (eq: String): Lean.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): Lean.CoreM TacticResult :=
+  runTermElabM do
+    state.restoreElabM
+    let tactic := match tacticExecute with
+      | .congruenceArg => Tactic.congruenceArg
+      | .congruenceFun => Tactic.congruenceFun
+      | .congruence => Tactic.congruence
+    state.execute goalId tactic
+
+
+
 end Pantograph
diff --git a/Test/Tactic/Congruence.lean b/Test/Tactic/Congruence.lean
index 7ef358a..1421263 100644
--- a/Test/Tactic/Congruence.lean
+++ b/Test/Tactic/Congruence.lean
@@ -27,10 +27,54 @@ def test_congr_arg (env: Environment): IO LSpec.TestSeq :=
           ])
       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

From bd42c396d71097b100852aa1f25d3759f76edfe0 Mon Sep 17 00:00:00 2001
From: Leni Aniva <v@leni.sh>
Date: Mon, 20 May 2024 14:19:10 -0700
Subject: [PATCH 34/38] chore: Code cleanup

---
 Pantograph/Expr.lean    | 5 ++---
 Pantograph/Library.lean | 3 +--
 2 files changed, 3 insertions(+), 5 deletions(-)

diff --git a/Pantograph/Expr.lean b/Pantograph/Expr.lean
index 8f890e3..63331af 100644
--- a/Pantograph/Expr.lean
+++ b/Pantograph/Expr.lean
@@ -70,11 +70,10 @@ partial def instantiateDelayedMVars (eOrig: Expr) : MetaM Expr := do
         let pending ← mvarIdPending.withContext do
           let inner ← instantiateDelayedMVars (.mvar mvarIdPending) --(level := level + 1)
           --IO.println s!"{padding}├Pre: {inner}"
-          let r := (← Expr.abstractM inner fvars).instantiateRev args
-          pure r
+          pure <| (← inner.abstractM fvars).instantiateRev args
 
         -- Tail arguments
-        let result := mkAppN pending (List.drop fvars.size args.toList |>.toArray)
+        let result := mkAppRange pending fvars.size args.size args
         --IO.println s!"{padding}├MD {result}"
         return .done result
       else
diff --git a/Pantograph/Library.lean b/Pantograph/Library.lean
index e0625e8..d3df45f 100644
--- a/Pantograph/Library.lean
+++ b/Pantograph/Library.lean
@@ -212,11 +212,10 @@ inductive TacticExecute where
 def goalTacticExecute (state: GoalState) (goalId: Nat) (tacticExecute: TacticExecute): Lean.CoreM TacticResult :=
   runTermElabM do
     state.restoreElabM
-    let tactic := match tacticExecute with
+    state.execute goalId $ match tacticExecute with
       | .congruenceArg => Tactic.congruenceArg
       | .congruenceFun => Tactic.congruenceFun
       | .congruence => Tactic.congruence
-    state.execute goalId tactic
 
 
 

From 3c90c94645eca5b8ecdc50773180a3543943d2bd Mon Sep 17 00:00:00 2001
From: Leni Aniva <v@leni.sh>
Date: Wed, 5 Jun 2024 13:45:13 -0700
Subject: [PATCH 35/38] fix: Execute instantiateAll in goal state diag

---
 Pantograph/Serial.lean | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/Pantograph/Serial.lean b/Pantograph/Serial.lean
index a6c0ece..e12bb7a 100644
--- a/Pantograph/Serial.lean
+++ b/Pantograph/Serial.lean
@@ -264,7 +264,7 @@ 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 (← instantiate mvarDecl.type))),
+      target := (← serializeExpression options (← instantiate mvarDecl.type)),
       vars := vars.reverse.toArray
     }
   where
@@ -319,7 +319,7 @@ protected def GoalState.diag (goalState: GoalState) (options: Protocol.GoalDiag
         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)
       let resultMain: String := s!"{pref}{mvarId.name}{userNameToString decl.userName}: {← Meta.ppExpr decl.type} {type_sexp}"
@@ -327,7 +327,7 @@ protected def GoalState.diag (goalState: GoalState) (options: Protocol.GoalDiag
         if options.printValue then
           if let Option.some value := (← getMCtx).eAssignment.find? mvarId then
             let value ← if options.instantiate
-              then instantiateMVars value
+              then instantiateAll value
               else pure $ value
             pure s!"\n := {← Meta.ppExpr value}"
           else

From 6dcff8b1518f8f6fa42095065398b879254fae09 Mon Sep 17 00:00:00 2001
From: Leni Aniva <v@leni.sh>
Date: Wed, 5 Jun 2024 15:56:20 -0700
Subject: [PATCH 36/38] fix: Print diag in mvar context

---
 Pantograph/Protocol.lean |  1 +
 Pantograph/Serial.lean   | 10 +++++++---
 2 files changed, 8 insertions(+), 3 deletions(-)

diff --git a/Pantograph/Protocol.lean b/Pantograph/Protocol.lean
index f73c3b0..271d4b7 100644
--- a/Pantograph/Protocol.lean
+++ b/Pantograph/Protocol.lean
@@ -273,6 +273,7 @@ structure GoalDiag where
   -- Print all mvars
   printAll: Bool := false
   instantiate: Bool := true
+  printSexp: Bool := false
 
 abbrev CR α := Except InteractionError α
 
diff --git a/Pantograph/Serial.lean b/Pantograph/Serial.lean
index e12bb7a..8f56468 100644
--- a/Pantograph/Serial.lean
+++ b/Pantograph/Serial.lean
@@ -311,7 +311,7 @@ protected def GoalState.diag (goalState: GoalState) (options: Protocol.GoalDiag
   )
   pure $ result ++ (resultGoals.map (· ++ "\n") |> String.join) ++ (resultOthers.map (· ++ "\n") |> String.join)
   where
-    printMVar (pref: String) (mvarId: MVarId) (decl: MetavarDecl): MetaM String := do
+    printMVar (pref: String) (mvarId: MVarId) (decl: MetavarDecl): MetaM String := mvarId.withContext do
       let resultFVars: List String ←
         if options.printContext then
           decl.lctx.fvarIdToDecl.toList.mapM (λ (fvarId, decl) =>
@@ -321,8 +321,12 @@ protected def GoalState.diag (goalState: GoalState) (options: Protocol.GoalDiag
       let type ← if options.instantiate
         then instantiateAll decl.type
         else pure $ decl.type
-      let type_sexp ← serializeExpressionSexp type (sanitize := false)
-      let resultMain: String := 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

From 3a534930894490d12248c4335d42cdf3e2baca56 Mon Sep 17 00:00:00 2001
From: Leni Aniva <v@leni.sh>
Date: Wed, 5 Jun 2024 16:14:52 -0700
Subject: [PATCH 37/38] feat: Show delayed assignment in goal diag

---
 Pantograph/Serial.lean | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

diff --git a/Pantograph/Serial.lean b/Pantograph/Serial.lean
index 8f56468..5cccb4e 100644
--- a/Pantograph/Serial.lean
+++ b/Pantograph/Serial.lean
@@ -329,11 +329,13 @@ protected def GoalState.diag (goalState: GoalState) (options: Protocol.GoalDiag
       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 instantiateAll value
               else pure $ value
             pure s!"\n := {← Meta.ppExpr value}"
+          else if let .some { mvarIdPending, .. } ← getDelayedMVarAssignment? mvarId then
+            pure s!"\n := $ {mvarIdPending.name}"
           else
             pure ""
         else

From 773a0afbd8a354093c9576df7be19f60f75d57df Mon Sep 17 00:00:00 2001
From: Leni Aniva <v@leni.sh>
Date: Tue, 11 Jun 2024 12:44:42 -0700
Subject: [PATCH 38/38] feat: Handling of universe level names in elab

---
 Pantograph.lean          |  4 +--
 Pantograph/Library.lean  | 66 ++++++++++++++++++++--------------------
 Pantograph/Protocol.lean |  4 +++
 Pantograph/Serial.lean   |  4 ++-
 README.md                |  6 ++--
 Test/Integration.lean    |  2 +-
 Test/Serial.lean         | 33 +++++++++++---------
 7 files changed, 64 insertions(+), 55 deletions(-)

diff --git a/Pantograph.lean b/Pantograph.lean
index c637303..e34e8e4 100644
--- a/Pantograph.lean
+++ b/Pantograph.lean
@@ -71,7 +71,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
@@ -94,7 +94,7 @@ def execute (command: Protocol.Command): MainM Lean.Json := 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}"
diff --git a/Pantograph/Library.lean b/Pantograph/Library.lean
index 6505fec..f14d8ea 100644
--- 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,7 +71,7 @@ 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 := {})
@@ -79,33 +79,33 @@ def createCoreState (imports: Array String): IO Lean.Core.State := do
   return { env := env }
 
 @[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 +115,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,38 +134,38 @@ 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 :=
+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): Lean.CoreM TacticResult :=
+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): Lean.CoreM TacticResult :=
+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): Lean.CoreM TacticResult :=
+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): Lean.CoreM TacticResult :=
+def goalConv (state: GoalState) (goalId: Nat): CoreM TacticResult :=
   runTermElabM <| state.conv goalId
 
 @[export pantograph_goal_conv_exit_m]
-def goalConvExit (state: GoalState): Lean.CoreM TacticResult :=
+def goalConvExit (state: GoalState): CoreM TacticResult :=
   runTermElabM <| state.convExit
 
 @[export pantograph_goal_calc_m]
-def goalCalc (state: GoalState) (goalId: Nat) (pred: String): Lean.CoreM TacticResult :=
+def goalCalc (state: GoalState) (goalId: Nat) (pred: String): CoreM TacticResult :=
   runTermElabM <| state.tryCalc goalId pred
 
 @[export pantograph_goal_focus]
@@ -181,11 +181,11 @@ 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 {
diff --git a/Pantograph/Protocol.lean b/Pantograph/Protocol.lean
index 17618fc..0d5da7e 100644
--- 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
@@ -198,6 +200,8 @@ 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
diff --git a/Pantograph/Serial.lean b/Pantograph/Serial.lean
index 950818e..8c16a01 100644
--- a/Pantograph/Serial.lean
+++ b/Pantograph/Serial.lean
@@ -1,5 +1,7 @@
 /-
-All serialisation functions
+All serialisation functions;
+This replicates the behaviour of `Scope`s in `Lean/Elab/Command.lean` without
+using `Scope`s.
 -/
 import Lean
 
diff --git a/README.md b/README.md
index 508d026..c136337 100644
--- 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:
diff --git a/Test/Integration.lean b/Test/Integration.lean
index 29cb82d..a9ced23 100644
--- 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 α" }
diff --git a/Test/Serial.lean b/Test/Serial.lean
index f55c18f..8819378 100644
--- a/Test/Serial.lean
+++ b/Test/Serial.lean
@@ -47,23 +47,26 @@ 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))"),
+  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))"),
     -- This tests `autoBoundImplicit`
-    ("λ {α : Sort (u + 1)} => List α", "(:lambda α (:sort (+ u 1)) ((:c List) 0) :implicit)"),
+    ("λ {α: Sort (u + 1)} => List α", [`u], "(:lambda α (:sort (+ u 1)) ((:c List) 0) :implicit)"),
+    ("λ {α} => List α", [], "(:lambda α (:sort (+ (:mv _uniq.4) 1)) ((:c List) 0) :implicit)"),
   ]
-  let termElabM: Elab.TermElabM LSpec.TestSeq := entries.foldlM (λ suites (source, target) => do
-    let env ← MonadEnv.getEnv
-    let s ← match parseTerm env source with
-      | .ok s => pure s
-      | .error e => return parseFailure e
-    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)
+  entries.foldlM (λ suites (source, levels, target) =>
+    let termElabM := do
+      let env ← MonadEnv.getEnv
+      let s ← match parseTerm env source with
+        | .ok s => pure s
+        | .error e => return parseFailure e
+      let expr ← match (← elabTerm s) with
+        | .ok expr => pure expr
+        | .error e => return elabFailure e
+      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) := [