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

Pantograph/Tactic.lean

@@ -1,2 +1,3 @@
 
 import Pantograph.Tactic.MotivatedApply
+import Pantograph.Tactic.NoConfuse

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

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)

Test/Tactic.lean

@@ -1 +1,2 @@
 import Test.Tactic.MotivatedApply
+import Test.Tactic.NoConfuse

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