summaryrefslogtreecommitdiff
path: root/backends/lean/Base/Progress
diff options
context:
space:
mode:
authorSon Ho2023-10-17 10:36:15 +0200
committerSon Ho2023-10-17 10:44:20 +0200
commit61368028027a7c160c33b05ec605c26833212667 (patch)
treea841ad12878ec4f9314b2af17f1a774b41b6dd7b /backends/lean/Base/Progress
parent584726e9c4e4378129a35f6cfbbbf934448d10a9 (diff)
Refold the scalar types when applying progress
Diffstat (limited to 'backends/lean/Base/Progress')
-rw-r--r--backends/lean/Base/Progress/Progress.lean26
1 files changed, 25 insertions, 1 deletions
diff --git a/backends/lean/Base/Progress/Progress.lean b/backends/lean/Base/Progress/Progress.lean
index 8b0759c5..ecf05dab 100644
--- a/backends/lean/Base/Progress/Progress.lean
+++ b/backends/lean/Base/Progress/Progress.lean
@@ -8,6 +8,27 @@ namespace Progress
open Lean Elab Term Meta Tactic
open Utils
+-- TODO: the scalar types annoyingly often get reduced when we use the progress
+-- tactic. We should find a way of controling reduction. For now we use rewriting
+-- lemmas to make sure the goal remains clean, but this complexifies proof terms.
+-- It seems there used to be a `fold` tactic.
+theorem scalar_isize_eq : Primitives.Scalar .Isize = Primitives.Isize := by rfl
+theorem scalar_i8_eq : Primitives.Scalar .I8 = Primitives.I8 := by rfl
+theorem scalar_i16_eq : Primitives.Scalar .I16 = Primitives.I16 := by rfl
+theorem scalar_i32_eq : Primitives.Scalar .I32 = Primitives.I32 := by rfl
+theorem scalar_i64_eq : Primitives.Scalar .I64 = Primitives.I64 := by rfl
+theorem scalar_i128_eq : Primitives.Scalar .I128 = Primitives.I128 := by rfl
+theorem scalar_usize_eq : Primitives.Scalar .Usize = Primitives.Usize := by rfl
+theorem scalar_u8_eq : Primitives.Scalar .U8 = Primitives.U8 := by rfl
+theorem scalar_u16_eq : Primitives.Scalar .U16 = Primitives.U16 := by rfl
+theorem scalar_u32_eq : Primitives.Scalar .U32 = Primitives.U32 := by rfl
+theorem scalar_u64_eq : Primitives.Scalar .U64 = Primitives.U64 := by rfl
+theorem scalar_u128_eq : Primitives.Scalar .U128 = Primitives.U128 := by rfl
+def scalar_eqs := [
+ ``scalar_isize_eq, ``scalar_i8_eq, ``scalar_i16_eq, ``scalar_i32_eq, ``scalar_i64_eq, ``scalar_i128_eq,
+ ``scalar_usize_eq, ``scalar_u8_eq, ``scalar_u16_eq, ``scalar_u32_eq, ``scalar_u64_eq, ``scalar_u128_eq
+]
+
inductive TheoremOrLocal where
| Theorem (thName : Name)
| Local (asm : LocalDecl)
@@ -111,8 +132,11 @@ def progressWith (fExpr : Expr) (th : TheoremOrLocal)
splitEqAndPost fun hEq hPost ids => do
trace[Progress] "eq and post:\n{hEq} : {← inferType hEq}\n{hPost}"
tryTac (
- simpAt [] [``Primitives.bind_tc_ret, ``Primitives.bind_tc_fail, ``Primitives.bind_tc_div]
+ simpAt true []
+ [``Primitives.bind_tc_ret, ``Primitives.bind_tc_fail, ``Primitives.bind_tc_div]
[hEq.fvarId!] (.targets #[] true))
+ -- TODO: remove this (some types get unfolded too much: we "fold" them back)
+ tryTac (simpAt true [] scalar_eqs [] .wildcard_dep)
-- Clear the equality, unless the user requests not to do so
let mgoal ← do
if keep.isSome then getMainGoal