From 1db6738bdbda9f306e1aedd9fd54a2017e77539c Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Tue, 21 May 2024 12:08:32 +0200
Subject: Fix an issue in the progress tactic

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

(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 ea38c630..f2a56e50 100644
--- a/backends/lean/Base/Progress/Progress.lean
+++ b/backends/lean/Base/Progress/Progress.lean
@@ -243,6 +243,9 @@ def progressAsmsOrLookupTheorem (keep : Option Name) (withTh : Option TheoremOrL
   -- Retrieve the goal
   let mgoal ← Tactic.getMainGoal
   let goalTy ← mgoal.getType
+  -- There might be uninstantiated meta-variables in the goal that we need
+  -- to instantiate (otherwise we will get stuck).
+  let goalTy ← instantiateMVars goalTy
   trace[Progress] "goal: {goalTy}"
   -- Dive into the goal to lookup the theorem
   -- Remark: if we don't isolate the call to `withPSpec` to immediately "close"
@@ -458,6 +461,16 @@ namespace Test
     f x = ok () := by
     progress
 
+  /- The use of `right` introduces a meta-variable in the goal, that we
+     need to instantiate (otherwise `progress` gets stuck) -/
+  example {ty} {x y : Scalar ty}
+    (hmin : Scalar.min ty ≤ x.val + y.val)
+    (hmax : x.val + y.val ≤ Scalar.max ty) :
+    False ∨ (∃ z, x + y = ok z ∧ z.val = x.val + y.val) := by
+    right
+    progress keep _ as ⟨ z, h1 .. ⟩
+    simp [*, h1]
+
 end Test
 
 end Progress
-- 
cgit v1.2.3