Pantograph/Goal.lean

@@ -383,13 +383,13 @@ protected def GoalState.tryMotivatedApply (state: GoalState) (goalId: Nat) (recu
   let recursor ← match (← Compile.parseTermM recursor) with
     | .ok syn => pure syn
     | .error error => return .parseError error
-  state.tryTacticM goalId (tacticM := Tactic.motivatedApply recursor)
+  state.tryTacticM goalId (tacticM := Tactic.evalMotivatedApply recursor)
 protected def GoalState.tryNoConfuse (state: GoalState) (goalId: Nat) (eq: String):
       Elab.TermElabM TacticResult := do
   state.restoreElabM
   let eq ← match (← Compile.parseTermM eq) with
     | .ok syn => pure syn
     | .error error => return .parseError error
-  state.tryTacticM goalId (tacticM := Tactic.noConfuse eq)
+  state.tryTacticM goalId (tacticM := Tactic.evalNoConfuse eq)
 
 end Pantograph

Pantograph/Library.lean

@@ -192,11 +192,5 @@ def goalCalc (state: GoalState) (goalId: Nat) (pred: String): CoreM TacticResult
 @[export pantograph_goal_focus]
 def goalFocus (state: GoalState) (goalId: Nat): Option GoalState :=
   state.focus goalId
-@[export pantograph_goal_motivated_apply_m]
-def goalMotivatedApply (state: GoalState) (goalId: Nat) (recursor: String): CoreM TacticResult :=
-  runTermElabM <| state.tryMotivatedApply goalId recursor
-@[export pantograph_goal_no_confuse_m]
-def goalNoConfuse (state: GoalState) (goalId: Nat) (eq: String): CoreM TacticResult :=
-  runTermElabM <| state.tryNoConfuse goalId eq
 
 end Pantograph

Pantograph/Tactic/Congruence.lean

@@ -4,82 +4,95 @@ open Lean
 
 namespace Pantograph.Tactic
 
-def congruenceArg: Elab.Tactic.TacticM Unit := do
+def congruenceArg (mvarId: MVarId): MetaM (List MVarId) := mvarId.withContext do
+  mvarId.checkNotAssigned `Pantograph.Tactic.congruenceArg
+  let target ← mvarId.getType
+  let .some (β, _, _) := target.eq? | throwError "Goal is not an Eq"
+  let userName := (← mvarId.getDecl).userName
+
+  let u ← Meta.mkFreshLevelMVar
+  let α ← Meta.mkFreshExprMVar (.some $ mkSort u)
+    .natural (userName := userName ++ `α)
+  let f ← Meta.mkFreshExprMVar (.some <| .forallE .anonymous α β .default)
+    .synthetic (userName := userName ++ `f)
+  let a₁ ← Meta.mkFreshExprMVar (.some α)
+    .synthetic (userName := userName ++ `a₁)
+  let a₂ ← Meta.mkFreshExprMVar (.some α)
+    .synthetic (userName := userName ++ `a₂)
+  let h ← Meta.mkFreshExprMVar (.some $ ← Meta.mkEq a₁ a₂)
+    .synthetic (userName := userName ++ `h)
+  let conduitType ← Meta.mkEq (← Meta.mkEq (.app f a₁) (.app f a₂)) target
+  let conduit ← Meta.mkFreshExprMVar conduitType
+    .synthetic (userName := userName ++ `conduit)
+  mvarId.assign $ ← Meta.mkEqMP conduit (← Meta.mkCongrArg f h)
+  let result := [α, a₁, a₂, f,  h, conduit]
+  return result.map (·.mvarId!)
+
+def evalCongruenceArg: Elab.Tactic.TacticM Unit := do
   let goal ← Elab.Tactic.getMainGoal
-  let .some (β, _, _) := (← goal.getType).eq? | throwError "Goal is not an Eq"
+  let nextGoals ← congruenceArg goal
-  let userName := (← goal.getDecl).userName
+  Elab.Tactic.setGoals nextGoals
 
-  let nextGoals ← goal.withContext do
+def congruenceFun (mvarId: MVarId): MetaM (List MVarId) := mvarId.withContext do
-    let u ← Meta.mkFreshLevelMVar
+  mvarId.checkNotAssigned `Pantograph.Tactic.congruenceFun
-    let α ← Meta.mkFreshExprMVar (.some $ mkSort u)
+  let target ← mvarId.getType
-      .natural (userName := userName ++ `α)
+  let .some (β, _, _) := target.eq? | throwError "Goal is not an Eq"
-    let f ← Meta.mkFreshExprMVar (.some <| .forallE .anonymous α β .default)
+  let userName := (← mvarId.getDecl).userName
-      .synthetic (userName := userName ++ `f)
+  let u ← Meta.mkFreshLevelMVar
-    let a₁ ← Meta.mkFreshExprMVar (.some α)
+  let α ← Meta.mkFreshExprMVar (.some $ mkSort u)
-      .synthetic (userName := userName ++ `a₁)
+    .natural (userName := userName ++ `α)
-    let a₂ ← Meta.mkFreshExprMVar (.some α)
+  let fType := .forallE .anonymous α β .default
-      .synthetic (userName := userName ++ `a₂)
+  let f₁ ← Meta.mkFreshExprMVar (.some fType)
-    let h ← Meta.mkFreshExprMVar (.some $ ← Meta.mkEq a₁ a₂)
+    .synthetic (userName := userName ++ `f₁)
-      .synthetic (userName := userName ++ `h)
+  let f₂ ← Meta.mkFreshExprMVar (.some fType)
-    let conduitType ← Meta.mkEq (← Meta.mkEq (.app f a₁) (.app f a₂)) (← goal.getType)
+    .synthetic (userName := userName ++ `f₂)
-    let conduit ← Meta.mkFreshExprMVar conduitType
+  let a ← Meta.mkFreshExprMVar (.some α)
-      .synthetic (userName := userName ++ `conduit)
+    .synthetic (userName := userName ++ `a)
-    goal.assign $ ← Meta.mkEqMP conduit (← Meta.mkCongrArg f h)
+  let h ← Meta.mkFreshExprMVar (.some $ ← Meta.mkEq f₁ f₂)
-    return [α, a₁, a₂, f,  h, conduit]
+    .synthetic (userName := userName ++ `h)
-  Elab.Tactic.setGoals <| nextGoals.map (·.mvarId!)
+  let conduitType ← Meta.mkEq (← Meta.mkEq (.app f₁ a) (.app f₂ a)) target
+  let conduit ← Meta.mkFreshExprMVar conduitType
+    .synthetic (userName := userName ++ `conduit)
+  mvarId.assign $ ← Meta.mkEqMP conduit (← Meta.mkCongrFun h a)
+  let result := [α, f₁, f₂, h, a, conduit]
+  return result.map (·.mvarId!)
 
-def congruenceFun: Elab.Tactic.TacticM Unit := do
+def evalCongruenceFun: Elab.Tactic.TacticM Unit := do
   let goal ← Elab.Tactic.getMainGoal
-  let .some (β, _, _) := (← goal.getType).eq? | throwError "Goal is not an Eq"
+  let nextGoals ← congruenceFun goal
-  let userName := (← goal.getDecl).userName
+  Elab.Tactic.setGoals nextGoals
 
-  let nextGoals ← goal.withContext do
+def congruence (mvarId: MVarId): MetaM (List MVarId) := mvarId.withContext do
-    let u ← Meta.mkFreshLevelMVar
+  mvarId.checkNotAssigned `Pantograph.Tactic.congruence
-    let α ← Meta.mkFreshExprMVar (.some $ mkSort u)
+  let target ← mvarId.getType
-      .natural (userName := userName ++ `α)
+  let .some (β, _, _) := target.eq? | throwError "Goal is not an Eq"
-    let fType := .forallE .anonymous α β .default
+  let userName := (← mvarId.getDecl).userName
-    let f₁ ← Meta.mkFreshExprMVar (.some fType)
+  let u ← Meta.mkFreshLevelMVar
-      .synthetic (userName := userName ++ `f₁)
+  let α ← Meta.mkFreshExprMVar (.some $ mkSort u)
-    let f₂ ← Meta.mkFreshExprMVar (.some fType)
+    .natural (userName := userName ++ `α)
-      .synthetic (userName := userName ++ `f₂)
+  let fType := .forallE .anonymous α β .default
-    let a ← Meta.mkFreshExprMVar (.some α)
+  let f₁ ← Meta.mkFreshExprMVar (.some fType)
-      .synthetic (userName := userName ++ `a)
+    .synthetic (userName := userName ++ `f₁)
-    let h ← Meta.mkFreshExprMVar (.some $ ← Meta.mkEq f₁ f₂)
+  let f₂ ← Meta.mkFreshExprMVar (.some fType)
-      .synthetic (userName := userName ++ `h)
+    .synthetic (userName := userName ++ `f₂)
-    let conduitType ← Meta.mkEq (← Meta.mkEq (.app f₁ a) (.app f₂ a)) (← goal.getType)
+  let a₁ ← Meta.mkFreshExprMVar (.some α)
-    let conduit ← Meta.mkFreshExprMVar conduitType
+    .synthetic (userName := userName ++ `a₁)
-      .synthetic (userName := userName ++ `conduit)
+  let a₂ ← Meta.mkFreshExprMVar (.some α)
-    goal.assign $ ← Meta.mkEqMP conduit (← Meta.mkCongrFun h a)
+    .synthetic (userName := userName ++ `a₂)
-    return [α, f₁, f₂, h, a, conduit]
+  let h₁ ← Meta.mkFreshExprMVar (.some $ ← Meta.mkEq f₁ f₂)
-  Elab.Tactic.setGoals <| nextGoals.map (·.mvarId!)
+    .synthetic (userName := userName ++ `h₁)
+  let h₂ ← Meta.mkFreshExprMVar (.some $ ← Meta.mkEq a₁ a₂)
+    .synthetic (userName := userName ++ `h₂)
+  let conduitType ← Meta.mkEq (← Meta.mkEq (.app f₁ a₁) (.app f₂ a₂)) target
+  let conduit ← Meta.mkFreshExprMVar conduitType
+    .synthetic (userName := userName ++ `conduit)
+  mvarId.assign $ ← Meta.mkEqMP conduit (← Meta.mkCongr h₁ h₂)
+  let result := [α, f₁, f₂, a₁, a₂, h₁, h₂, conduit]
+  return result.map (·.mvarId!)
 
-def congruence: Elab.Tactic.TacticM Unit := do
+def evalCongruence: Elab.Tactic.TacticM Unit := do
   let goal ← Elab.Tactic.getMainGoal
-  let .some (β, _, _) := (← goal.getType).eq? | throwError "Goal is not an Eq"
+  let nextGoals ← congruence goal
-  let userName := (← goal.getDecl).userName
+  Elab.Tactic.setGoals nextGoals
-
-  let nextGoals ← goal.withContext do
-    let u ← Meta.mkFreshLevelMVar
-    let α ← Meta.mkFreshExprMVar (.some $ mkSort u)
-      .natural (userName := userName ++ `α)
-    let fType := .forallE .anonymous α β .default
-    let f₁ ← Meta.mkFreshExprMVar (.some fType)
-      .synthetic (userName := userName ++ `f₁)
-    let f₂ ← Meta.mkFreshExprMVar (.some fType)
-      .synthetic (userName := userName ++ `f₂)
-    let a₁ ← Meta.mkFreshExprMVar (.some α)
-      .synthetic (userName := userName ++ `a₁)
-    let a₂ ← Meta.mkFreshExprMVar (.some α)
-      .synthetic (userName := userName ++ `a₂)
-    let h₁ ← Meta.mkFreshExprMVar (.some $ ← Meta.mkEq f₁ f₂)
-      .synthetic (userName := userName ++ `h₁)
-    let h₂ ← Meta.mkFreshExprMVar (.some $ ← Meta.mkEq a₁ a₂)
-      .synthetic (userName := userName ++ `h₂)
-    let conduitType ← Meta.mkEq (← Meta.mkEq (.app f₁ a₁) (.app f₂ a₂)) (← goal.getType)
-    let conduit ← Meta.mkFreshExprMVar conduitType
-      .synthetic (userName := userName ++ `conduit)
-    goal.assign $ ← Meta.mkEqMP conduit (← Meta.mkCongr h₁ h₂)
-    return [α, f₁, f₂, a₁, a₂, h₁, h₂, conduit]
-  Elab.Tactic.setGoals <| nextGoals.map (·.mvarId!)
 
 end Pantograph.Tactic

Pantograph/Tactic/MotivatedApply.lean

@@ -62,44 +62,44 @@ def collectMotiveArguments (forallBody: Expr): SSet Nat :=
   | _ => SSet.empty
 
 /-- Applies a symbol of the type `∀ (motive: α → Sort u) (a: α)..., (motive α)` -/
-def motivatedApply: Elab.Tactic.Tactic := λ stx => do
+def motivatedApply (mvarId: MVarId) (recursor: Expr) : MetaM (List Meta.InductionSubgoal) := mvarId.withContext do
-  let goal ← Elab.Tactic.getMainGoal
+  mvarId.checkNotAssigned `Pantograph.Tactic.motivatedApply
-  let nextGoals: List MVarId ← goal.withContext do
+  let recursorType ← Meta.inferType recursor
-    let recursor ← Elab.Term.elabTerm (stx := stx) .none
+  let resultant ← mvarId.getType
-    let recursorType ← Meta.inferType recursor
 
-    let resultant ← goal.getType
+  let info ← match getRecursorInformation recursorType with
+    | .some info => pure info
+    | .none => throwError "Recursor return type does not correspond with the invocation of a motive: {← Meta.ppExpr recursorType}"
 
-    let info ← match getRecursorInformation recursorType with
+  let rec go (i: Nat) (prev: Array Expr): MetaM (Array Expr) := do
-      | .some info => pure info
+    if i ≥ info.nArgs then
-      | .none => throwError "Recursor return type does not correspond with the invocation of a motive: {← Meta.ppExpr recursorType}"
+      return prev
+    else
+      let argType := info.args.get! i
+      -- If `argType` has motive references, its goal needs to be placed in it
+      let argType := argType.instantiateRev prev
+      let bvarIndex := info.nArgs - i - 1
+      let argGoal ← if bvarIndex = info.iMotive then
+          let surrogateMotiveType ← info.surrogateMotiveType prev resultant
+          Meta.mkFreshExprMVar surrogateMotiveType .syntheticOpaque (userName := `motive)
+        else
+          Meta.mkFreshExprMVar argType .syntheticOpaque (userName := .anonymous)
+      let prev :=  prev ++ [argGoal]
+      go (i + 1) prev
+    termination_by info.nArgs - i
+  let mut newMVars ← go 0 #[]
 
-    let rec go (i: Nat) (prev: Array Expr): MetaM (Array Expr) := do
+  -- Create the conduit type which proves the result of the motive is equal to the goal
-      if i ≥ info.nArgs then
+  let conduitType ← info.conduitType newMVars resultant
-        return prev
+  let goalConduit ← Meta.mkFreshExprMVar conduitType .natural (userName := `conduit)
-      else
+  mvarId.assign $ ← Meta.mkEqMP goalConduit (mkAppN recursor newMVars)
-        let argType := info.args.get! i
+  newMVars := newMVars ++ [goalConduit]
-        -- If `argType` has motive references, its goal needs to be placed in it
-        let argType := argType.instantiateRev prev
-        let bvarIndex := info.nArgs - i - 1
-        let argGoal ← if bvarIndex = info.iMotive then
-            let surrogateMotiveType ← info.surrogateMotiveType prev resultant
-            Meta.mkFreshExprMVar surrogateMotiveType .syntheticOpaque (userName := `motive)
-          else
-            Meta.mkFreshExprMVar argType .syntheticOpaque (userName := .anonymous)
-        let prev :=  prev ++ [argGoal]
-        go (i + 1) prev
-      termination_by info.nArgs - i
-    let mut newMVars ← go 0 #[]
 
-    -- Create the conduit type which proves the result of the motive is equal to the goal
+  return newMVars.toList.map (λ mvar => { mvarId := mvar.mvarId!})
-    let conduitType ← info.conduitType newMVars resultant
-    let goalConduit ← Meta.mkFreshExprMVar conduitType .natural (userName := `conduit)
-    goal.assign $ ← Meta.mkEqMP goalConduit (mkAppN recursor newMVars)
-    newMVars := newMVars ++ [goalConduit]
 
-    let nextGoals := newMVars.toList.map (·.mvarId!)
+def evalMotivatedApply : Elab.Tactic.Tactic := fun stx => Elab.Tactic.withMainContext do
-    pure nextGoals
+  let recursor ← Elab.Term.elabTerm (stx := stx) .none
-  Elab.Tactic.setGoals nextGoals
+  let nextGoals ← motivatedApply (← Elab.Tactic.getMainGoal) recursor
+  Elab.Tactic.setGoals $ nextGoals.map (·.mvarId)
 
 end Pantograph.Tactic

Pantograph/Tactic/NoConfuse.lean

@@ -4,15 +4,19 @@ open Lean
 
 namespace Pantograph.Tactic
 
-def noConfuse: Elab.Tactic.Tactic := λ stx => do
+def noConfuse (mvarId: MVarId) (h: Expr): MetaM Unit := mvarId.withContext do
-  let goal ← Elab.Tactic.getMainGoal
+  mvarId.checkNotAssigned `Pantograph.Tactic.noConfuse
-  goal.withContext do
+  let target ← mvarId.getType
-    let absurd ← Elab.Term.elabTerm (stx := stx) .none
+  let noConfusion ← Meta.mkNoConfusion (target := target) (h := h)
-    let noConfusion ← Meta.mkNoConfusion (target := ← goal.getType) (h := absurd)
 
-    unless ← Meta.isDefEq (← Meta.inferType noConfusion) (← goal.getType) do
+  unless ← Meta.isDefEq (← Meta.inferType noConfusion) target do
-      throwError "invalid noConfuse call: The resultant type {← Meta.ppExpr $ ← Meta.inferType noConfusion} cannot be unified with {← Meta.ppExpr $ ← goal.getType}"
+    throwError "invalid noConfuse call: The resultant type {← Meta.ppExpr $ ← Meta.inferType noConfusion} cannot be unified with {← Meta.ppExpr target}"
-    goal.assign noConfusion
+  mvarId.assign noConfusion
+
+def evalNoConfuse: Elab.Tactic.Tactic := λ stx => do
+  let goal ← Elab.Tactic.getMainGoal
+  let h ← goal.withContext $ Elab.Term.elabTerm (stx := stx) .none
+  noConfuse goal h
   Elab.Tactic.setGoals []
 
 end Pantograph.Tactic

Test/Tactic/Congruence.lean

@@ -12,7 +12,7 @@ def test_congr_arg_list : TestT Elab.TermElabM Unit := do
   let expr ← parseSentence expr
   Meta.lambdaTelescope expr $ λ _ body => do
     let target ← Meta.mkFreshExprSyntheticOpaqueMVar body
-    let newGoals ← runTacticOnMVar Tactic.congruenceArg target.mvarId!
+    let newGoals ← runTacticOnMVar Tactic.evalCongruenceArg target.mvarId!
     addTest $ LSpec.check "goals" ((← newGoals.mapM (λ x => mvarUserNameAndType x)) =
       [
         (`α, "Sort ?u.30"),
@@ -34,7 +34,7 @@ def test_congr_arg : TestT Elab.TermElabM Unit := do
   let expr ← parseSentence expr
   Meta.lambdaTelescope expr $ λ _ body => do
     let target ← Meta.mkFreshExprSyntheticOpaqueMVar body
-    let newGoals ← runTacticOnMVar Tactic.congruenceArg target.mvarId!
+    let newGoals ← runTacticOnMVar Tactic.evalCongruenceArg target.mvarId!
     addTest $  LSpec.check "goals" ((← newGoals.mapM (λ x => mvarUserNameAndType x)) =
       [
         (`α, "Sort ?u.70"),
@@ -49,7 +49,7 @@ def test_congr_fun : TestT Elab.TermElabM Unit := do
   let expr ← parseSentence expr
   Meta.lambdaTelescope expr $ λ _ body => do
     let target ← Meta.mkFreshExprSyntheticOpaqueMVar body
-    let newGoals ← runTacticOnMVar Tactic.congruenceFun target.mvarId!
+    let newGoals ← runTacticOnMVar Tactic.evalCongruenceFun target.mvarId!
     addTest $ LSpec.check "goals" ((← newGoals.mapM (λ x => mvarUserNameAndType x)) =
       [
         (`α, "Sort ?u.159"),
@@ -64,7 +64,7 @@ def test_congr : TestT Elab.TermElabM Unit := do
   let expr ← parseSentence expr
   Meta.lambdaTelescope expr $ λ _ body => do
     let target ← Meta.mkFreshExprSyntheticOpaqueMVar body
-    let newGoals ← runTacticOnMVar Tactic.congruence target.mvarId!
+    let newGoals ← runTacticOnMVar Tactic.evalCongruence target.mvarId!
     addTest $  LSpec.check "goals" ((← newGoals.mapM (λ x => mvarUserNameAndType x)) =
       [
         (`α, "Sort ?u.10"),

Test/Tactic/MotivatedApply.lean

@@ -33,7 +33,7 @@ def test_nat_brec_on : TestT Elab.TermElabM Unit := do
       | .error error => throwError "Failed to parse: {error}"
     -- Apply the tactic
     let target ← Meta.mkFreshExprSyntheticOpaqueMVar body
-    let tactic := Tactic.motivatedApply recursor
+    let tactic := Tactic.evalMotivatedApply recursor
     let newGoals ← runTacticOnMVar tactic target.mvarId!
     let test :=  LSpec.check "goals" ((← newGoals.mapM (λ g => do exprToStr (← g.getType))) =
       [
@@ -57,7 +57,7 @@ def test_list_brec_on : TestT Elab.TermElabM Unit := do
       | .error error => throwError "Failed to parse: {error}"
     -- Apply the tactic
     let target ← Meta.mkFreshExprSyntheticOpaqueMVar body
-    let tactic := Tactic.motivatedApply recursor
+    let tactic := Tactic.evalMotivatedApply recursor
     let newGoals ← runTacticOnMVar tactic target.mvarId!
     addTest $ LSpec.check "goals" ((← newGoals.mapM (λ g => do exprToStr (← g.getType))) =
       [
@@ -81,7 +81,7 @@ def test_partial_motive_instantiation : TestT Elab.TermElabM Unit := do
   Meta.lambdaTelescope expr $ λ _ body => do
     -- Apply the tactic
     let target ← Meta.mkFreshExprSyntheticOpaqueMVar body
-    let tactic := Tactic.motivatedApply recursor
+    let tactic := Tactic.evalMotivatedApply recursor
     let newGoals ← runTacticOnMVar tactic target.mvarId!
     let majorId := 67
     addTest $ (LSpec.check "goals" ((← newGoals.mapM (λ g => do exprToStr (← g.getType))) =

Test/Tactic/NoConfuse.lean

@@ -20,7 +20,7 @@ def test_nat : TestT Elab.TermElabM Unit := do
       | .error error => throwError "Failed to parse: {error}"
     -- Apply the tactic
     let target ← Meta.mkFreshExprSyntheticOpaqueMVar body
-    let tactic := Tactic.noConfuse recursor
+    let tactic := Tactic.evalNoConfuse recursor
     let newGoals ← runTacticOnMVar tactic target.mvarId!
     addTest $ LSpec.check "goals" ((← newGoals.mapM (λ g => do exprToStr (← g.getType))) = [])
 
@@ -38,7 +38,7 @@ def test_nat_fail : TestT Elab.TermElabM Unit := do
     -- Apply the tactic
     let target ← Meta.mkFreshExprSyntheticOpaqueMVar body
     try
-      let tactic := Tactic.noConfuse recursor
+      let tactic := Tactic.evalNoConfuse recursor
       let _ ← runTacticOnMVar tactic target.mvarId!
       addTest $ assertUnreachable "Tactic should fail"
     catch _ =>
@@ -57,7 +57,7 @@ def test_list : TestT Elab.TermElabM Unit := do
       | .error error => throwError "Failed to parse: {error}"
     -- Apply the tactic
     let target ← Meta.mkFreshExprSyntheticOpaqueMVar body
-    let tactic := Tactic.noConfuse recursor
+    let tactic := Tactic.evalNoConfuse recursor
     let newGoals ← runTacticOnMVar tactic target.mvarId!
     addTest $ LSpec.check "goals"
       ((← newGoals.mapM (λ g => do exprToStr (← g.getType))) = [])