From 5b4f8a37ebbbbd435b400af11ce65ec9c96ec428 Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Thu, 15 Aug 2024 23:41:17 -0700 Subject: [PATCH] refactor: All Tactic/ tactics into MetaM form --- Pantograph/Goal.lean | 4 +- Pantograph/Library.lean | 6 - Pantograph/Tactic/Congruence.lean | 153 ++++++++++++++------------ Pantograph/Tactic/MotivatedApply.lean | 68 ++++++------ Pantograph/Tactic/NoConfuse.lean | 20 ++-- Test/Tactic/Congruence.lean | 8 +- Test/Tactic/MotivatedApply.lean | 6 +- Test/Tactic/NoConfuse.lean | 6 +- 8 files changed, 141 insertions(+), 130 deletions(-) diff --git a/Pantograph/Goal.lean b/Pantograph/Goal.lean index b54c5f7..9be5164 100644 --- a/Pantograph/Goal.lean +++ b/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 diff --git a/Pantograph/Library.lean b/Pantograph/Library.lean index 6fff21e..c4ce4ff 100644 --- a/Pantograph/Library.lean +++ b/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 diff --git a/Pantograph/Tactic/Congruence.lean b/Pantograph/Tactic/Congruence.lean index bbb9d75..2ff23d2 100644 --- a/Pantograph/Tactic/Congruence.lean +++ b/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 userName := (← goal.getDecl).userName + let nextGoals ← congruenceArg goal + Elab.Tactic.setGoals nextGoals - let nextGoals ← goal.withContext do - let u ← Meta.mkFreshLevelMVar - let α ← Meta.mkFreshExprMVar (.some $ mkSort u) - .natural (userName := userName ++ `α) - let f ← Meta.mkFreshExprMVar (.some <| .forallE .anonymous α β .default) - .synthetic (userName := userName ++ `f) - let a₁ ← Meta.mkFreshExprMVar (.some α) - .synthetic (userName := userName ++ `a₁) - let a₂ ← Meta.mkFreshExprMVar (.some α) - .synthetic (userName := userName ++ `a₂) - let h ← Meta.mkFreshExprMVar (.some $ ← Meta.mkEq a₁ a₂) - .synthetic (userName := userName ++ `h) - let conduitType ← Meta.mkEq (← Meta.mkEq (.app f a₁) (.app f a₂)) (← goal.getType) - let conduit ← Meta.mkFreshExprMVar conduitType - .synthetic (userName := userName ++ `conduit) - goal.assign $ ← Meta.mkEqMP conduit (← Meta.mkCongrArg f h) - return [α, a₁, a₂, f, h, conduit] - Elab.Tactic.setGoals <| nextGoals.map (·.mvarId!) +def congruenceFun (mvarId: MVarId): MetaM (List MVarId) := mvarId.withContext do + mvarId.checkNotAssigned `Pantograph.Tactic.congruenceFun + 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 fType := .forallE .anonymous α β .default + let f₁ ← Meta.mkFreshExprMVar (.some fType) + .synthetic (userName := userName ++ `f₁) + let f₂ ← Meta.mkFreshExprMVar (.some fType) + .synthetic (userName := userName ++ `f₂) + let a ← Meta.mkFreshExprMVar (.some α) + .synthetic (userName := userName ++ `a) + let h ← Meta.mkFreshExprMVar (.some $ ← Meta.mkEq f₁ f₂) + .synthetic (userName := userName ++ `h) + let conduitType ← Meta.mkEq (← Meta.mkEq (.app f₁ a) (.app f₂ a)) 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 userName := (← goal.getDecl).userName + let nextGoals ← congruenceFun goal + 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 h ← Meta.mkFreshExprMVar (.some $ ← Meta.mkEq f₁ f₂) - .synthetic (userName := userName ++ `h) - let conduitType ← Meta.mkEq (← Meta.mkEq (.app f₁ a) (.app f₂ a)) (← goal.getType) - let conduit ← Meta.mkFreshExprMVar conduitType - .synthetic (userName := userName ++ `conduit) - goal.assign $ ← Meta.mkEqMP conduit (← Meta.mkCongrFun h a) - return [α, f₁, f₂, h, a, conduit] - Elab.Tactic.setGoals <| nextGoals.map (·.mvarId!) +def congruence (mvarId: MVarId): MetaM (List MVarId) := mvarId.withContext do + mvarId.checkNotAssigned `Pantograph.Tactic.congruence + 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 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₂)) 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 userName := (← goal.getDecl).userName - - let nextGoals ← goal.withContext do - let u ← Meta.mkFreshLevelMVar - let α ← Meta.mkFreshExprMVar (.some $ mkSort u) - .natural (userName := userName ++ `α) - let fType := .forallE .anonymous α β .default - let f₁ ← Meta.mkFreshExprMVar (.some fType) - .synthetic (userName := userName ++ `f₁) - let f₂ ← Meta.mkFreshExprMVar (.some fType) - .synthetic (userName := userName ++ `f₂) - let a₁ ← Meta.mkFreshExprMVar (.some α) - .synthetic (userName := userName ++ `a₁) - let a₂ ← Meta.mkFreshExprMVar (.some α) - .synthetic (userName := userName ++ `a₂) - let h₁ ← Meta.mkFreshExprMVar (.some $ ← Meta.mkEq f₁ f₂) - .synthetic (userName := userName ++ `h₁) - let h₂ ← Meta.mkFreshExprMVar (.some $ ← Meta.mkEq a₁ a₂) - .synthetic (userName := userName ++ `h₂) - let conduitType ← Meta.mkEq (← Meta.mkEq (.app f₁ a₁) (.app f₂ a₂)) (← goal.getType) - let conduit ← Meta.mkFreshExprMVar conduitType - .synthetic (userName := userName ++ `conduit) - goal.assign $ ← Meta.mkEqMP conduit (← Meta.mkCongr h₁ h₂) - return [α, f₁, f₂, a₁, a₂, h₁, h₂, conduit] - Elab.Tactic.setGoals <| nextGoals.map (·.mvarId!) + let nextGoals ← congruence goal + Elab.Tactic.setGoals nextGoals end Pantograph.Tactic diff --git a/Pantograph/Tactic/MotivatedApply.lean b/Pantograph/Tactic/MotivatedApply.lean index f570560..37d0099 100644 --- a/Pantograph/Tactic/MotivatedApply.lean +++ b/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 - 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 +def motivatedApply (mvarId: MVarId) (recursor: Expr) : MetaM (List Meta.InductionSubgoal) := mvarId.withContext do + mvarId.checkNotAssigned `Pantograph.Tactic.motivatedApply + let recursorType ← Meta.inferType recursor + let resultant ← mvarId.getType - 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 - | .some info => pure info - | .none => throwError "Recursor return type does not correspond with the invocation of a motive: {← Meta.ppExpr recursorType}" + let rec go (i: Nat) (prev: Array Expr): MetaM (Array Expr) := do + if i ≥ info.nArgs then + return prev + else + let argType := info.args.get! i + -- If `argType` has motive references, its goal needs to be placed in it + let argType := argType.instantiateRev prev + let bvarIndex := info.nArgs - i - 1 + let argGoal ← if bvarIndex = info.iMotive then + let surrogateMotiveType ← info.surrogateMotiveType prev resultant + Meta.mkFreshExprMVar surrogateMotiveType .syntheticOpaque (userName := `motive) + else + Meta.mkFreshExprMVar argType .syntheticOpaque (userName := .anonymous) + let prev := prev ++ [argGoal] + go (i + 1) prev + termination_by info.nArgs - i + let mut newMVars ← go 0 #[] - let rec go (i: Nat) (prev: Array Expr): MetaM (Array Expr) := do - if i ≥ info.nArgs then - return prev - else - let argType := info.args.get! i - -- If `argType` has motive references, its goal needs to be placed in it - let argType := argType.instantiateRev prev - let bvarIndex := info.nArgs - i - 1 - let argGoal ← if bvarIndex = info.iMotive then - let surrogateMotiveType ← info.surrogateMotiveType prev resultant - Meta.mkFreshExprMVar surrogateMotiveType .syntheticOpaque (userName := `motive) - else - Meta.mkFreshExprMVar argType .syntheticOpaque (userName := .anonymous) - let prev := prev ++ [argGoal] - go (i + 1) prev - termination_by info.nArgs - i - let mut newMVars ← go 0 #[] + -- Create the conduit type which proves the result of the motive is equal to the goal + let conduitType ← info.conduitType newMVars resultant + let goalConduit ← Meta.mkFreshExprMVar conduitType .natural (userName := `conduit) + mvarId.assign $ ← Meta.mkEqMP goalConduit (mkAppN recursor newMVars) + newMVars := newMVars ++ [goalConduit] - -- Create the conduit type which proves the result of the motive is equal to the goal - let conduitType ← info.conduitType newMVars resultant - let goalConduit ← Meta.mkFreshExprMVar conduitType .natural (userName := `conduit) - goal.assign $ ← Meta.mkEqMP goalConduit (mkAppN recursor newMVars) - newMVars := newMVars ++ [goalConduit] + return newMVars.toList.map (λ mvar => { mvarId := mvar.mvarId!}) - let nextGoals := newMVars.toList.map (·.mvarId!) - pure nextGoals - Elab.Tactic.setGoals nextGoals +def evalMotivatedApply : Elab.Tactic.Tactic := fun stx => Elab.Tactic.withMainContext do + let recursor ← Elab.Term.elabTerm (stx := stx) .none + let nextGoals ← motivatedApply (← Elab.Tactic.getMainGoal) recursor + Elab.Tactic.setGoals $ nextGoals.map (·.mvarId) end Pantograph.Tactic diff --git a/Pantograph/Tactic/NoConfuse.lean b/Pantograph/Tactic/NoConfuse.lean index b8bc84e..f4ce78f 100644 --- a/Pantograph/Tactic/NoConfuse.lean +++ b/Pantograph/Tactic/NoConfuse.lean @@ -4,15 +4,19 @@ 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) +def noConfuse (mvarId: MVarId) (h: Expr): MetaM Unit := mvarId.withContext do + mvarId.checkNotAssigned `Pantograph.Tactic.noConfuse + let target ← mvarId.getType + let noConfusion ← Meta.mkNoConfusion (target := target) (h := h) - 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 + unless ← Meta.isDefEq (← Meta.inferType noConfusion) target do + throwError "invalid noConfuse call: The resultant type {← Meta.ppExpr $ ← Meta.inferType noConfusion} cannot be unified with {← Meta.ppExpr target}" + mvarId.assign noConfusion + +def evalNoConfuse: Elab.Tactic.Tactic := λ stx => do + let goal ← Elab.Tactic.getMainGoal + let h ← goal.withContext $ Elab.Term.elabTerm (stx := stx) .none + noConfuse goal h Elab.Tactic.setGoals [] end Pantograph.Tactic diff --git a/Test/Tactic/Congruence.lean b/Test/Tactic/Congruence.lean index 38c94f3..836041c 100644 --- a/Test/Tactic/Congruence.lean +++ b/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"), diff --git a/Test/Tactic/MotivatedApply.lean b/Test/Tactic/MotivatedApply.lean index 091e309..4fb05e3 100644 --- a/Test/Tactic/MotivatedApply.lean +++ b/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))) = diff --git a/Test/Tactic/NoConfuse.lean b/Test/Tactic/NoConfuse.lean index cc15198..ac277e2 100644 --- a/Test/Tactic/NoConfuse.lean +++ b/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))) = [])