From 876137dff361620d8ade1a4ee94fa9274df0bdc6 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Tue, 25 Jul 2023 14:08:44 +0200
Subject: Improve int_tac and scalar_tac

---
 backends/lean/Base/Progress/Progress.lean | 13 ++++++++++++-
 1 file changed, 12 insertions(+), 1 deletion(-)

(limited to 'backends/lean/Base/Progress/Progress.lean')

diff --git a/backends/lean/Base/Progress/Progress.lean b/backends/lean/Base/Progress/Progress.lean
index c0ddc63d..a281f1d2 100644
--- a/backends/lean/Base/Progress/Progress.lean
+++ b/backends/lean/Base/Progress/Progress.lean
@@ -307,7 +307,18 @@ def evalProgress (args : TSyntax `Progress.progressArgs) : TacticM Unit := do
     let args := (args.get! 2).getArgs
     (args.get! 3).getArgs.size > 0
   trace[Progress] "Split post: {splitPost}"
-  progressAsmsOrLookupTheorem keep withArg ids splitPost (firstTac [assumptionTac, Arith.scalarTac])
+  /- For scalarTac we have a fast track: if the goal is not a linear
+     arithmetic goal, we skip (note that otherwise, scalarTac would try
+     to prove a contradiction) -/
+  let scalarTac : TacticM Unit := do
+    if ← Arith.goalIsLinearInt then
+      -- Also: we don't try to split the goal if it is a conjunction
+      -- (it shouldn't be)
+      Arith.scalarTac false
+    else
+      throwError "Not a linear arithmetic goal"
+  progressAsmsOrLookupTheorem keep withArg ids splitPost (
+    firstTac [assumptionTac, scalarTac])
 
 elab "progress" args:progressArgs : tactic =>
   evalProgress args
-- 
cgit v1.2.3