From 7763a8ef8d5190fad39e9e677c5f44c536973655 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Wed, 12 Jun 2024 14:45:58 +0200
Subject: Add the Simp.Config to the simp wrappers

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

(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 f2a56e50..39a48044 100644
--- a/backends/lean/Base/Progress/Progress.lean
+++ b/backends/lean/Base/Progress/Progress.lean
@@ -135,7 +135,7 @@ def progressWith (fExpr : Expr) (th : TheoremOrLocal)
     Tactic.focus do
     let _ ←
       tryTac
-        (simpAt true []
+        (simpAt true {} []
                [``Primitives.bind_tc_ok, ``Primitives.bind_tc_fail, ``Primitives.bind_tc_div]
                [hEq.fvarId!] (.targets #[] true))
     -- It may happen that at this point the goal is already solved (though this is rare)
@@ -144,7 +144,7 @@ def progressWith (fExpr : Expr) (th : TheoremOrLocal)
     else
        trace[Progress] "goal after applying the eq and simplifying the binds: {← getMainGoal}"
        -- TODO: remove this (some types get unfolded too much: we "fold" them back)
-       let _ ← tryTac (simpAt true [] scalar_eqs [] .wildcard_dep)
+       let _ ← tryTac (simpAt true {} [] scalar_eqs [] .wildcard_dep)
        trace[Progress] "goal after folding back scalar types: {← getMainGoal}"
        -- Clear the equality, unless the user requests not to do so
        let mgoal ← do
-- 
cgit v1.2.3


From f5deac2b0f42e2a87fc26da50c902729e0ed1039 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Wed, 12 Jun 2024 14:46:38 +0200
Subject: Slightly simplify the progress tactic

---
 backends/lean/Base/Progress/Progress.lean | 12 ++++--------
 1 file changed, 4 insertions(+), 8 deletions(-)

(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 39a48044..03d464d7 100644
--- a/backends/lean/Base/Progress/Progress.lean
+++ b/backends/lean/Base/Progress/Progress.lean
@@ -58,17 +58,13 @@ def progressWith (fExpr : Expr) (th : TheoremOrLocal)
      We also make sure that all the meta variables which appear in the
      function arguments have been instantiated
    -/
-  let env ← getEnv
   let thTy ← do
     match th with
     | .Theorem thName =>
-      let thDecl := env.constants.find! thName
-      -- We have to introduce fresh meta-variables for the universes already
-      let ul : List (Name × Level) ←
-        thDecl.levelParams.mapM (λ x => do pure (x, ← mkFreshLevelMVar))
-      let ulMap : HashMap Name Level := HashMap.ofList ul
-      let thTy := thDecl.type.instantiateLevelParamsCore (λ x => ulMap.find! x)
-      pure thTy
+      -- Lookup the theorem and introduce fresh meta-variables for the universes
+      let th ← mkConstWithFreshMVarLevels thName
+      -- Retrieve the type
+      inferType th
     | .Local asmDecl => pure asmDecl.type
   trace[Progress] "Looked up theorem/assumption type: {thTy}"
   -- TODO: the tactic fails if we uncomment withNewMCtxDepth
-- 
cgit v1.2.3