diff options
| author | Son Ho | 2024-05-21 12:08:32 +0200 |
|---|---|---|
| committer | Son Ho | 2024-05-21 12:08:32 +0200 |
| commit | 1db6738bdbda9f306e1aedd9fd54a2017e77539c (patch) | |
| tree | f01be95b52b5f657e367031e8df65dea0fa269f9 /backends/lean/Base | |
| parent | e07af56862e92efecb09209874ad24da77c0e001 (diff) | |
Fix an issue in the progress tactic
Diffstat (limited to 'backends/lean/Base')
| -rw-r--r-- | backends/lean/Base/Progress/Progress.lean | 13 |
1 files changed, 13 insertions, 0 deletions
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 |