From 61368028027a7c160c33b05ec605c26833212667 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Tue, 17 Oct 2023 10:36:15 +0200
Subject: Refold the scalar types when applying progress

---
 backends/lean/Base/Progress/Progress.lean | 26 +++++++++++++++++++++++++-
 1 file changed, 25 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 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
-- 
cgit v1.2.3


From 81b7a7d706bc1a0f2f57bc254a8af158039a10cf Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Wed, 25 Oct 2023 18:44:28 +0200
Subject: Make the hashmap files typecheck again in Lean

---
 backends/lean/Base/Progress/Progress.lean | 3 ++-
 1 file changed, 2 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 ecf05dab..24c6f912 100644
--- a/backends/lean/Base/Progress/Progress.lean
+++ b/backends/lean/Base/Progress/Progress.lean
@@ -383,6 +383,7 @@ namespace Test
   -- #eval showStoredPSpec
   -- #eval showStoredPSpecClass
   -- #eval showStoredPSpecExprClass
+  open alloc.vec
 
   example {ty} {x y : Scalar ty}
     (hmin : Scalar.min ty ≤ x.val + y.val)
@@ -408,7 +409,7 @@ namespace Test
      `α : Type u` where u is quantified, while here we use `α : Type 0` -/
   example {α : Type} (v: Vec α) (i: Usize) (x : α)
     (hbounds : i.val < v.length) :
-    ∃ nv, v.index_mut_back α i x = ret nv ∧
+    ∃ nv, v.update_usize α i x = ret nv ∧
     nv.val = v.val.update i.val x := by
     progress
     simp [*]
-- 
cgit v1.2.3


From 00705bba68fed61d3b0bcde2c5fe0ecc83880870 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Thu, 9 Nov 2023 18:37:07 +0100
Subject: Update the failing proofs

---
 backends/lean/Base/Progress/Progress.lean | 2 +-
 1 file changed, 1 insertion(+), 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 24c6f912..ba63f09d 100644
--- a/backends/lean/Base/Progress/Progress.lean
+++ b/backends/lean/Base/Progress/Progress.lean
@@ -409,7 +409,7 @@ namespace Test
      `α : Type u` where u is quantified, while here we use `α : Type 0` -/
   example {α : Type} (v: Vec α) (i: Usize) (x : α)
     (hbounds : i.val < v.length) :
-    ∃ nv, v.update_usize α i x = ret nv ∧
+    ∃ nv, v.update_usize i x = ret nv ∧
     nv.val = v.val.update i.val x := by
     progress
     simp [*]
-- 
cgit v1.2.3