From cf1289f159ddddf85430fbdd04d47d4f3be6eeae Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Sun, 5 May 2024 13:24:29 -0700 Subject: [PATCH] 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