Reorganize a bit the Lean library

4 files changed, 36 insertions, 22 deletions

diff --git a/backends/lean/Base.lean b/backends/lean/Base.lean
new file mode 100644
index 00000000..960b2bb5
--- /dev/null
+++ b/backends/lean/Base.lean
@@ -0,0 +1 @@
+import Base.Primitives
diff --git a/backends/lean/Primitives.lean b/backends/lean/Base/Primitives.lean
index e7826fbf..d3de1d10 100644
--- a/backends/lean/Primitives.lean
+++ b/backends/lean/Base/Primitives.lean
@@ -282,6 +282,7 @@ structure Scalar (ty : ScalarTy) where
   val : Int
   hmin : Scalar.min ty ≤ val
   hmax : val ≤ Scalar.max ty
+deriving Repr
 
 theorem Scalar.bound_suffices (ty : ScalarTy) (x : Int) :
   Scalar.cMin ty ≤ x ∧ x ≤ Scalar.cMax ty ->
@@ -296,8 +297,24 @@ def Scalar.ofIntCore {ty : ScalarTy} (x : Int)
 
 def Scalar.ofInt {ty : ScalarTy} (x : Int)
   (h : Scalar.min ty ≤ x ∧ x ≤ Scalar.max ty) : Scalar ty :=
-  let ⟨ hmin, hmax ⟩ := h
-  Scalar.ofIntCore x hmin hmax
+  -- Remark: we initially wrote:
+  --  let ⟨ hmin, hmax ⟩ := h
+  --  Scalar.ofIntCore x hmin hmax
+  -- We updated to the line below because a similar pattern in `Scalar.tryMk`
+  -- made reduction block. Both versions seem to work for `Scalar.ofInt`, though.
+  -- TODO: investigate
+  Scalar.ofIntCore x h.left h.right
+
+@[simp] def Scalar.check_bounds (ty : ScalarTy) (x : Int) : Bool :=
+  (Scalar.cMin ty ≤ x || Scalar.min ty ≤ x) ∧ (x ≤ Scalar.cMax ty || x ≤ Scalar.max ty)
+
+theorem Scalar.check_bounds_prop {ty : ScalarTy} {x : Int} (h: Scalar.check_bounds ty x) :
+  Scalar.min ty ≤ x ∧ x ≤ Scalar.max ty := by
+  simp at *
+  have ⟨ hmin, hmax ⟩ := h
+  have hbmin := Scalar.cMin_bound ty
+  have hbmax := Scalar.cMax_bound ty
+  cases hmin <;> cases hmax <;> apply And.intro <;> linarith
 
 -- Further thoughts: look at what has been done here:
 -- https://github.com/leanprover-community/mathlib4/blob/master/Mathlib/Data/Fin/Basic.lean
@@ -305,16 +322,15 @@ def Scalar.ofInt {ty : ScalarTy} (x : Int)
 -- https://github.com/leanprover-community/mathlib4/blob/master/Mathlib/Data/UInt.lean
 -- which both contain a fair amount of reasoning already!
 def Scalar.tryMk (ty : ScalarTy) (x : Int) : Result (Scalar ty) :=
-  -- TODO: write this with only one if then else
-  if h: (Scalar.cMin ty ≤ x || Scalar.min ty ≤ x) && (x ≤ Scalar.cMax ty || x ≤ Scalar.max ty) then
-    let h: Scalar.min ty ≤ x ∧ x ≤ Scalar.max ty := by
-      simp at *
-      have ⟨ hmin, hmax ⟩ := h
-      have hbmin := Scalar.cMin_bound ty
-      have hbmax := Scalar.cMax_bound ty
-      cases hmin <;> cases hmax <;> apply And.intro <;> linarith
-    let ⟨ hmin, hmax ⟩ := h
-    return Scalar.ofIntCore x hmin hmax
+  if h:Scalar.check_bounds ty x then
+    -- If we do:
+    -- ```
+    -- let ⟨ hmin, hmax ⟩ := (Scalar.check_bounds_prop h)
+    -- Scalar.ofIntCore x hmin hmax
+    -- ```
+    -- then normalization blocks (for instance, some proofs which use reflexivity fail).
+    -- However, the version below doesn't block reduction (TODO: investigate):
+    return Scalar.ofInt x (Scalar.check_bounds_prop h)
   else fail integerOverflow
 
 def Scalar.neg {ty : ScalarTy} (x : Scalar ty) : Result (Scalar ty) := Scalar.tryMk ty (- x.val)
@@ -626,11 +642,8 @@ def vec_index_mut_back (α : Type u) (v: Vec α) (i: Usize) (x: α): Result (Vec
 -- MISC --
 ----------
 
-def mem_replace_fwd (a : Type) (x : a) (_ : a) : a :=
-  x
-
-def mem_replace_back (a : Type) (_ : a) (y : a) : a :=
-  y
+@[simp] def mem_replace_fwd (a : Type) (x : a) (_ : a) : a := x
+@[simp] def mem_replace_back (a : Type) (_ : a) (y : a) : a := y
 
 /-- Aeneas-translated function -- useful to reduce non-recursive definitions.
  Use with `simp [ aeneas ]` -/
diff --git a/backends/lean/lake-manifest.json b/backends/lean/lake-manifest.json
index 7b23fc19..e5d362fc 100644
--- a/backends/lean/lake-manifest.json
+++ b/backends/lean/lake-manifest.json
@@ -4,24 +4,24 @@
  [{"git":
    {"url": "https://github.com/leanprover-community/mathlib4.git",
     "subDir?": null,
-    "rev": "f89ee53085b8aad0bacd3bc94d7ef4b8d9aba643",
+    "rev": "cdb1b898e4317567699181f27533182046ebc544",
     "name": "mathlib",
     "inputRev?": null}},
   {"git":
    {"url": "https://github.com/gebner/quote4",
     "subDir?": null,
-    "rev": "2412c4fdf4a8b689f4467618e5e7b371ae5014aa",
+    "rev": "c71f94e34c1cda52eef5c93dc9da409ab2727420",
     "name": "Qq",
     "inputRev?": "master"}},
   {"git":
    {"url": "https://github.com/JLimperg/aesop",
     "subDir?": null,
-    "rev": "7fe9ecd9339b0e1796e89d243b776849c305c690",
+    "rev": "ca73109cc40837bc61df8024c9016da4b4f99d4c",
     "name": "aesop",
     "inputRev?": "master"}},
   {"git":
    {"url": "https://github.com/leanprover/std4",
     "subDir?": null,
-    "rev": "24897887905b3a1254b244369f5dd2cf6174b0ee",
+    "rev": "6932c4ea52914dc6b0488944e367459ddc4d01a6",
     "name": "std",
     "inputRev?": "main"}}]}
diff --git a/backends/lean/lakefile.lean b/backends/lean/lakefile.lean
index c5e27d1c..21a4a332 100644
--- a/backends/lean/lakefile.lean
+++ b/backends/lean/lakefile.lean
@@ -8,4 +8,4 @@ require mathlib from git
 package «base» {}
 
 @[default_target]
-lean_lib «Primitives» {}
+lean_lib «Base» {}