From 1018aa1af83e639a6b41b5650bf3b717e7f8de68 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Wed, 12 Jun 2024 14:46:52 +0200
Subject: Deactivate the coercion from Nat to Scalar

---
 backends/lean/Base/Primitives/Scalar.lean | 7 +++++++
 1 file changed, 7 insertions(+)

(limited to 'backends/lean/Base/Primitives')

diff --git a/backends/lean/Base/Primitives/Scalar.lean b/backends/lean/Base/Primitives/Scalar.lean
index 8fb067e1..157ade2c 100644
--- a/backends/lean/Base/Primitives/Scalar.lean
+++ b/backends/lean/Base/Primitives/Scalar.lean
@@ -351,10 +351,17 @@ instance [Decide (Scalar.cMin ty ≤ v ∧ v ≤ Scalar.cMax ty)] : InBounds ty
 @[simp] abbrev Scalar.check_bounds (ty : ScalarTy) (x : Int) : Bool :=
   (Scalar.cMin ty ≤ x || Scalar.min ty ≤ x) ∧ (x ≤ Scalar.cMax ty || x ≤ Scalar.max ty)
 
+/- Discussion:
+   This coercion can be slightly annoying at times, because if we write
+   something like `u = 3` (where `u` is, for instance, as `U32`), then instead of
+   coercing `u` to `Int`, Lean will lift `3` to `U32`).
+   For now we deactivate it.
+
 -- TODO(raitobezarius): the inbounds constraint is a bit ugly as we can pretty trivially
 -- discharge the lhs on ≥ 0.
 instance {ty: ScalarTy} [InBounds ty (Int.ofNat n)]: OfNat (Scalar ty) (n: ℕ) where
   ofNat := Scalar.ofInt n
+-/
 
 theorem Scalar.check_bounds_imp_in_bounds {ty : ScalarTy} {x : Int}
   (h: Scalar.check_bounds ty x) :
-- 
cgit v1.2.3


From c8272aeea205ca9cb36e22757473ca2a931a4933 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Wed, 12 Jun 2024 14:52:34 +0200
Subject: Update the scalar notation for the Lean backend

---
 backends/lean/Base/Primitives/Scalar.lean | 50 +++++++++++++++----------------
 1 file changed, 25 insertions(+), 25 deletions(-)

(limited to 'backends/lean/Base/Primitives')

diff --git a/backends/lean/Base/Primitives/Scalar.lean b/backends/lean/Base/Primitives/Scalar.lean
index 157ade2c..5f14a14f 100644
--- a/backends/lean/Base/Primitives/Scalar.lean
+++ b/backends/lean/Base/Primitives/Scalar.lean
@@ -313,13 +313,13 @@ theorem Scalar.bound_suffices (ty : ScalarTy) (x : Int) :
   apply And.intro <;> have hmin := Scalar.cMin_bound ty <;> have hmax := Scalar.cMax_bound ty <;> linarith
 
 /- [match_pattern] attribute: allows to us `Scalar.ofIntCore` inside of patterns.
-   This is particularly useful once we introduce notations like `#u32` (which
+   This is particularly useful once we introduce notations like `u32` (which
    desugards to `Scalar.ofIntCore`) as it allows to write expressions like this:
    Example:
    ```
    match x with
-   | 0#u32 => ...
-   | 1#u32 => ...
+   | 0u32 => ...
+   | 1u32 => ...
    | ...
    ```
  -/
@@ -328,7 +328,7 @@ theorem Scalar.bound_suffices (ty : ScalarTy) (x : Int) :
   { val := x, hmin := h.left, hmax := h.right }
 
 -- The definitions below are used later to introduce nice syntax for constants,
--- like `1#u32`. We are reusing the technique described here: https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Different.20elaboration.20inside.2Foutside.20of.20match.20patterns/near/425455284
+-- like `1u32`. We are reusing the technique described here: https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Different.20elaboration.20inside.2Foutside.20of.20match.20patterns/near/425455284
 
 class InBounds (ty : ScalarTy) (x : Int) :=
   hInBounds : Scalar.cMin ty ≤ x ∧ x ≤ Scalar.cMax ty
@@ -1281,38 +1281,38 @@ def U128.ofIntCore  := @Scalar.ofIntCore .U128
 @[match_pattern] abbrev U64.ofInt   := @Scalar.ofInt .U64
 @[match_pattern] abbrev U128.ofInt  := @Scalar.ofInt .U128
 
-postfix:max "#isize" => Isize.ofInt
-postfix:max "#i8"    => I8.ofInt
-postfix:max "#i16"   => I16.ofInt
-postfix:max "#i32"   => I32.ofInt
-postfix:max "#i64"   => I64.ofInt
-postfix:max "#i128"  => I128.ofInt
-postfix:max "#usize" => Usize.ofInt
-postfix:max "#u8"    => U8.ofInt
-postfix:max "#u16"   => U16.ofInt
-postfix:max "#u32"   => U32.ofInt
-postfix:max "#u64"   => U64.ofInt
-postfix:max "#u128"  => U128.ofInt
+postfix:max "isize" => Isize.ofInt
+postfix:max "i8"    => I8.ofInt
+postfix:max "i16"   => I16.ofInt
+postfix:max "i32"   => I32.ofInt
+postfix:max "i64"   => I64.ofInt
+postfix:max "i128"  => I128.ofInt
+postfix:max "usize" => Usize.ofInt
+postfix:max "u8"    => U8.ofInt
+postfix:max "u16"   => U16.ofInt
+postfix:max "u32"   => U32.ofInt
+postfix:max "u64"   => U64.ofInt
+postfix:max "u128"  => U128.ofInt
 
 /- Testing the notations -/
-example := 0#u32
-example := 1#u32
-example := 1#i32
-example := 0#isize
-example := (-1)#isize
+example := 0u32
+example := 1u32
+example := 1i32
+example := 0isize
+example := (-1)isize
 example (x : U32) : Bool :=
   match x with
-  | 0#u32 => true
+  | 0u32 => true
   | _ => false
 
 example (x : U32) : Bool :=
   match x with
-  | 1#u32 => true
+  | 1u32 => true
   | _ => false
 
 example (x : I32) : Bool :=
   match x with
-  | (-1)#i32 => true
+  | (-1)i32 => true
   | _ => false
 
 -- Notation for pattern matching
@@ -1334,7 +1334,7 @@ example {ty} (x : Scalar ty) : Bool :=
   | _ => false
 
 -- Testing the notations
-example : Result Usize := 0#usize + 1#usize
+example : Result Usize := 0usize + 1usize
 
 -- TODO: factor those lemmas out
 @[simp] theorem Scalar.ofInt_val_eq {ty} (h : Scalar.min ty ≤ x ∧ x ≤ Scalar.max ty) : (Scalar.ofIntCore x h).val = x := by
-- 
cgit v1.2.3


From fe59d3afe131e9f83cbdf73b1c8089ad090d92fb Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Wed, 12 Jun 2024 16:18:05 +0200
Subject: Update CoreConvertNum.lean

---
 backends/lean/Base/Primitives/CoreConvertNum.lean | 44 +++++++++++------------
 1 file changed, 22 insertions(+), 22 deletions(-)

(limited to 'backends/lean/Base/Primitives')

diff --git a/backends/lean/Base/Primitives/CoreConvertNum.lean b/backends/lean/Base/Primitives/CoreConvertNum.lean
index eb456a96..bc3db8b2 100644
--- a/backends/lean/Base/Primitives/CoreConvertNum.lean
+++ b/backends/lean/Base/Primitives/CoreConvertNum.lean
@@ -18,40 +18,40 @@ namespace num -- core.convert.num
 
 -- Conversions
 def FromUsizeBool.from (b : Bool) : Usize :=
-  if b then 1#usize else 0#usize
+  if b then 1usize else 0usize
 
 def FromU8Bool.from (b : Bool) : U8 :=
-  if b then 1#u8 else 0#u8
+  if b then 1u8 else 0u8
 
 def FromU16Bool.from (b : Bool) : U16 :=
-  if b then 1#u16 else 0#u16
+  if b then 1u16 else 0u16
 
 def FromU32Bool.from (b : Bool) : U32 :=
-  if b then 1#u32 else 0#u32
+  if b then 1u32 else 0u32
 
 def FromU64Bool.from (b : Bool) : U64 :=
-  if b then 1#u64 else 0#u64
+  if b then 1u64 else 0u64
 
 def FromU128Bool.from (b : Bool) : U128 :=
-  if b then 1#u128 else 0#u128
+  if b then 1u128 else 0u128
 
 def FromIsizeBool.from (b : Bool) : Isize :=
-  if b then 1#isize else 0#isize
+  if b then 1isize else 0isize
 
 def FromI8Bool.from (b : Bool) : I8 :=
-  if b then 1#i8 else 0#i8
+  if b then 1i8 else 0i8
 
 def FromI16Bool.from (b : Bool) : I16 :=
-  if b then 1#i16 else 0#i16
+  if b then 1i16 else 0i16
 
 def FromI32Bool.from (b : Bool) : I32 :=
-  if b then 1#i32 else 0#i32
+  if b then 1i32 else 0i32
 
 def FromI64Bool.from (b : Bool) : I64 :=
-  if b then 1#i64 else 0#i64
+  if b then 1i64 else 0i64
 
 def FromI128Bool.from (b : Bool) : I128 :=
-  if b then 1#i128 else 0#i128
+  if b then 1i128 else 0i128
 
 def FromUsizeU8.from (x : U8) : Usize := ⟨ x.val, by scalar_tac, by scalar_tac ⟩
 
@@ -259,18 +259,18 @@ def FromI128I128 : core.convert.From I128 I128 := {
 }
 
 -- to_le_bytes
-def core.num.U8.to_le_bytes (x : U8) : Array U8 1#usize := sorry
-def core.num.U16.to_le_bytes (x : U16) : Array U8 2#usize := sorry
-def core.num.U32.to_le_bytes (x : U32) : Array U8 4#usize := sorry
-def core.num.U64.to_le_bytes (x : U64) : Array U8 8#usize := sorry
-def core.num.U128.to_le_bytes (x : U128) : Array U8 128#usize := sorry
+def core.num.U8.to_le_bytes (x : U8) : Array U8 1usize := sorry
+def core.num.U16.to_le_bytes (x : U16) : Array U8 2usize := sorry
+def core.num.U32.to_le_bytes (x : U32) : Array U8 4usize := sorry
+def core.num.U64.to_le_bytes (x : U64) : Array U8 8usize := sorry
+def core.num.U128.to_le_bytes (x : U128) : Array U8 128usize := sorry
 
 -- to_be_bytes
-def core.num.U8.to_be_bytes (x : U8) : Array U8 1#usize := sorry
-def core.num.U16.to_be_bytes (x : U16) : Array U8 2#usize := sorry
-def core.num.U32.to_be_bytes (x : U32) : Array U8 4#usize := sorry
-def core.num.U64.to_be_bytes (x : U64) : Array U8 8#usize := sorry
-def core.num.U128.to_be_bytes (x : U128) : Array U8 128#usize := sorry
+def core.num.U8.to_be_bytes (x : U8) : Array U8 1usize := sorry
+def core.num.U16.to_be_bytes (x : U16) : Array U8 2usize := sorry
+def core.num.U32.to_be_bytes (x : U32) : Array U8 4usize := sorry
+def core.num.U64.to_be_bytes (x : U64) : Array U8 8usize := sorry
+def core.num.U128.to_be_bytes (x : U128) : Array U8 128usize := sorry
 
 end core.convert
 
-- 
cgit v1.2.3


From dd2b973a86680308807d7f26aff81d3310550f84 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Wed, 12 Jun 2024 18:20:23 +0200
Subject: Revert "Update CoreConvertNum.lean"

This reverts commit fe59d3afe131e9f83cbdf73b1c8089ad090d92fb.
---
 backends/lean/Base/Primitives/CoreConvertNum.lean | 44 +++++++++++------------
 1 file changed, 22 insertions(+), 22 deletions(-)

(limited to 'backends/lean/Base/Primitives')

diff --git a/backends/lean/Base/Primitives/CoreConvertNum.lean b/backends/lean/Base/Primitives/CoreConvertNum.lean
index bc3db8b2..eb456a96 100644
--- a/backends/lean/Base/Primitives/CoreConvertNum.lean
+++ b/backends/lean/Base/Primitives/CoreConvertNum.lean
@@ -18,40 +18,40 @@ namespace num -- core.convert.num
 
 -- Conversions
 def FromUsizeBool.from (b : Bool) : Usize :=
-  if b then 1usize else 0usize
+  if b then 1#usize else 0#usize
 
 def FromU8Bool.from (b : Bool) : U8 :=
-  if b then 1u8 else 0u8
+  if b then 1#u8 else 0#u8
 
 def FromU16Bool.from (b : Bool) : U16 :=
-  if b then 1u16 else 0u16
+  if b then 1#u16 else 0#u16
 
 def FromU32Bool.from (b : Bool) : U32 :=
-  if b then 1u32 else 0u32
+  if b then 1#u32 else 0#u32
 
 def FromU64Bool.from (b : Bool) : U64 :=
-  if b then 1u64 else 0u64
+  if b then 1#u64 else 0#u64
 
 def FromU128Bool.from (b : Bool) : U128 :=
-  if b then 1u128 else 0u128
+  if b then 1#u128 else 0#u128
 
 def FromIsizeBool.from (b : Bool) : Isize :=
-  if b then 1isize else 0isize
+  if b then 1#isize else 0#isize
 
 def FromI8Bool.from (b : Bool) : I8 :=
-  if b then 1i8 else 0i8
+  if b then 1#i8 else 0#i8
 
 def FromI16Bool.from (b : Bool) : I16 :=
-  if b then 1i16 else 0i16
+  if b then 1#i16 else 0#i16
 
 def FromI32Bool.from (b : Bool) : I32 :=
-  if b then 1i32 else 0i32
+  if b then 1#i32 else 0#i32
 
 def FromI64Bool.from (b : Bool) : I64 :=
-  if b then 1i64 else 0i64
+  if b then 1#i64 else 0#i64
 
 def FromI128Bool.from (b : Bool) : I128 :=
-  if b then 1i128 else 0i128
+  if b then 1#i128 else 0#i128
 
 def FromUsizeU8.from (x : U8) : Usize := ⟨ x.val, by scalar_tac, by scalar_tac ⟩
 
@@ -259,18 +259,18 @@ def FromI128I128 : core.convert.From I128 I128 := {
 }
 
 -- to_le_bytes
-def core.num.U8.to_le_bytes (x : U8) : Array U8 1usize := sorry
-def core.num.U16.to_le_bytes (x : U16) : Array U8 2usize := sorry
-def core.num.U32.to_le_bytes (x : U32) : Array U8 4usize := sorry
-def core.num.U64.to_le_bytes (x : U64) : Array U8 8usize := sorry
-def core.num.U128.to_le_bytes (x : U128) : Array U8 128usize := sorry
+def core.num.U8.to_le_bytes (x : U8) : Array U8 1#usize := sorry
+def core.num.U16.to_le_bytes (x : U16) : Array U8 2#usize := sorry
+def core.num.U32.to_le_bytes (x : U32) : Array U8 4#usize := sorry
+def core.num.U64.to_le_bytes (x : U64) : Array U8 8#usize := sorry
+def core.num.U128.to_le_bytes (x : U128) : Array U8 128#usize := sorry
 
 -- to_be_bytes
-def core.num.U8.to_be_bytes (x : U8) : Array U8 1usize := sorry
-def core.num.U16.to_be_bytes (x : U16) : Array U8 2usize := sorry
-def core.num.U32.to_be_bytes (x : U32) : Array U8 4usize := sorry
-def core.num.U64.to_be_bytes (x : U64) : Array U8 8usize := sorry
-def core.num.U128.to_be_bytes (x : U128) : Array U8 128usize := sorry
+def core.num.U8.to_be_bytes (x : U8) : Array U8 1#usize := sorry
+def core.num.U16.to_be_bytes (x : U16) : Array U8 2#usize := sorry
+def core.num.U32.to_be_bytes (x : U32) : Array U8 4#usize := sorry
+def core.num.U64.to_be_bytes (x : U64) : Array U8 8#usize := sorry
+def core.num.U128.to_be_bytes (x : U128) : Array U8 128#usize := sorry
 
 end core.convert
 
-- 
cgit v1.2.3


From d36736fa4e7eb9f42f35303b8080d17ddbee92d2 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Wed, 12 Jun 2024 18:20:52 +0200
Subject: Revert "Update the scalar notation for the Lean backend"

This reverts commit c8272aeea205ca9cb36e22757473ca2a931a4933.
---
 backends/lean/Base/Primitives/Scalar.lean | 50 +++++++++++++++----------------
 1 file changed, 25 insertions(+), 25 deletions(-)

(limited to 'backends/lean/Base/Primitives')

diff --git a/backends/lean/Base/Primitives/Scalar.lean b/backends/lean/Base/Primitives/Scalar.lean
index 5f14a14f..157ade2c 100644
--- a/backends/lean/Base/Primitives/Scalar.lean
+++ b/backends/lean/Base/Primitives/Scalar.lean
@@ -313,13 +313,13 @@ theorem Scalar.bound_suffices (ty : ScalarTy) (x : Int) :
   apply And.intro <;> have hmin := Scalar.cMin_bound ty <;> have hmax := Scalar.cMax_bound ty <;> linarith
 
 /- [match_pattern] attribute: allows to us `Scalar.ofIntCore` inside of patterns.
-   This is particularly useful once we introduce notations like `u32` (which
+   This is particularly useful once we introduce notations like `#u32` (which
    desugards to `Scalar.ofIntCore`) as it allows to write expressions like this:
    Example:
    ```
    match x with
-   | 0u32 => ...
-   | 1u32 => ...
+   | 0#u32 => ...
+   | 1#u32 => ...
    | ...
    ```
  -/
@@ -328,7 +328,7 @@ theorem Scalar.bound_suffices (ty : ScalarTy) (x : Int) :
   { val := x, hmin := h.left, hmax := h.right }
 
 -- The definitions below are used later to introduce nice syntax for constants,
--- like `1u32`. We are reusing the technique described here: https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Different.20elaboration.20inside.2Foutside.20of.20match.20patterns/near/425455284
+-- like `1#u32`. We are reusing the technique described here: https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Different.20elaboration.20inside.2Foutside.20of.20match.20patterns/near/425455284
 
 class InBounds (ty : ScalarTy) (x : Int) :=
   hInBounds : Scalar.cMin ty ≤ x ∧ x ≤ Scalar.cMax ty
@@ -1281,38 +1281,38 @@ def U128.ofIntCore  := @Scalar.ofIntCore .U128
 @[match_pattern] abbrev U64.ofInt   := @Scalar.ofInt .U64
 @[match_pattern] abbrev U128.ofInt  := @Scalar.ofInt .U128
 
-postfix:max "isize" => Isize.ofInt
-postfix:max "i8"    => I8.ofInt
-postfix:max "i16"   => I16.ofInt
-postfix:max "i32"   => I32.ofInt
-postfix:max "i64"   => I64.ofInt
-postfix:max "i128"  => I128.ofInt
-postfix:max "usize" => Usize.ofInt
-postfix:max "u8"    => U8.ofInt
-postfix:max "u16"   => U16.ofInt
-postfix:max "u32"   => U32.ofInt
-postfix:max "u64"   => U64.ofInt
-postfix:max "u128"  => U128.ofInt
+postfix:max "#isize" => Isize.ofInt
+postfix:max "#i8"    => I8.ofInt
+postfix:max "#i16"   => I16.ofInt
+postfix:max "#i32"   => I32.ofInt
+postfix:max "#i64"   => I64.ofInt
+postfix:max "#i128"  => I128.ofInt
+postfix:max "#usize" => Usize.ofInt
+postfix:max "#u8"    => U8.ofInt
+postfix:max "#u16"   => U16.ofInt
+postfix:max "#u32"   => U32.ofInt
+postfix:max "#u64"   => U64.ofInt
+postfix:max "#u128"  => U128.ofInt
 
 /- Testing the notations -/
-example := 0u32
-example := 1u32
-example := 1i32
-example := 0isize
-example := (-1)isize
+example := 0#u32
+example := 1#u32
+example := 1#i32
+example := 0#isize
+example := (-1)#isize
 example (x : U32) : Bool :=
   match x with
-  | 0u32 => true
+  | 0#u32 => true
   | _ => false
 
 example (x : U32) : Bool :=
   match x with
-  | 1u32 => true
+  | 1#u32 => true
   | _ => false
 
 example (x : I32) : Bool :=
   match x with
-  | (-1)i32 => true
+  | (-1)#i32 => true
   | _ => false
 
 -- Notation for pattern matching
@@ -1334,7 +1334,7 @@ example {ty} (x : Scalar ty) : Bool :=
   | _ => false
 
 -- Testing the notations
-example : Result Usize := 0usize + 1usize
+example : Result Usize := 0#usize + 1#usize
 
 -- TODO: factor those lemmas out
 @[simp] theorem Scalar.ofInt_val_eq {ty} (h : Scalar.min ty ≤ x ∧ x ≤ Scalar.max ty) : (Scalar.ofIntCore x h).val = x := by
-- 
cgit v1.2.3


From 79e19aa701086de9f080357d817284559f900bcc Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Wed, 12 Jun 2024 18:40:17 +0200
Subject: Update the scalar notations in Lean

---
 backends/lean/Base/Primitives/Scalar.lean          | 123 ++++-----------------
 backends/lean/Base/Primitives/ScalarNotations.lean |  87 +++++++++++++++
 2 files changed, 108 insertions(+), 102 deletions(-)
 create mode 100644 backends/lean/Base/Primitives/ScalarNotations.lean

(limited to 'backends/lean/Base/Primitives')

diff --git a/backends/lean/Base/Primitives/Scalar.lean b/backends/lean/Base/Primitives/Scalar.lean
index 157ade2c..f4264b9b 100644
--- a/backends/lean/Base/Primitives/Scalar.lean
+++ b/backends/lean/Base/Primitives/Scalar.lean
@@ -312,38 +312,13 @@ theorem Scalar.bound_suffices (ty : ScalarTy) (x : Int) :
   λ h => by
   apply And.intro <;> have hmin := Scalar.cMin_bound ty <;> have hmax := Scalar.cMax_bound ty <;> linarith
 
-/- [match_pattern] attribute: allows to us `Scalar.ofIntCore` inside of patterns.
-   This is particularly useful once we introduce notations like `#u32` (which
-   desugards to `Scalar.ofIntCore`) as it allows to write expressions like this:
-   Example:
-   ```
-   match x with
-   | 0#u32 => ...
-   | 1#u32 => ...
-   | ...
-   ```
- -/
-@[match_pattern] def Scalar.ofIntCore {ty : ScalarTy} (x : Int)
+def Scalar.ofIntCore {ty : ScalarTy} (x : Int)
   (h : Scalar.min ty ≤ x ∧ x ≤ Scalar.max ty) : Scalar ty :=
   { val := x, hmin := h.left, hmax := h.right }
 
--- The definitions below are used later to introduce nice syntax for constants,
--- like `1#u32`. We are reusing the technique described here: https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Different.20elaboration.20inside.2Foutside.20of.20match.20patterns/near/425455284
-
-class InBounds (ty : ScalarTy) (x : Int) :=
-  hInBounds : Scalar.cMin ty ≤ x ∧ x ≤ Scalar.cMax ty
-
--- This trick to trigger reduction for decidable propositions comes from
--- here: https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/instance.20with.20tactic.20autoparam/near/343495807
-class Decide (p : Prop) [Decidable p] : Prop where
-  isTrue : p
-instance : @Decide p (.isTrue h) := @Decide.mk p (_) h
-
-instance [Decide (Scalar.cMin ty ≤ v ∧ v ≤ Scalar.cMax ty)] : InBounds ty v where
-  hInBounds := Decide.isTrue
-
-@[reducible, match_pattern] def Scalar.ofInt {ty : ScalarTy} (x : Int) [InBounds ty x] : Scalar ty :=
-  Scalar.ofIntCore x (Scalar.bound_suffices ty x InBounds.hInBounds)
+@[reducible] def Scalar.ofInt {ty : ScalarTy} (x : Int)
+  (hInBounds : Scalar.cMin ty ≤ x ∧ x ≤ Scalar.cMax ty := by decide) : Scalar ty :=
+  Scalar.ofIntCore x (Scalar.bound_suffices ty x hInBounds)
 
 @[simp] abbrev Scalar.in_bounds (ty : ScalarTy) (x : Int) : Prop :=
   Scalar.min ty ≤ x ∧ x ≤ Scalar.max ty
@@ -412,9 +387,8 @@ theorem Scalar.tryMk_eq (ty : ScalarTy) (x : Int) :
   simp [tryMk, ofOption, tryMkOpt]
   split_ifs <;> simp
 
-instance (ty: ScalarTy) : InBounds ty 0 where
-  hInBounds := by
-    induction ty <;> simp [Scalar.cMax, Scalar.cMin, Scalar.max, Scalar.min] <;> decide
+@[simp] theorem zero_in_cbounds {ty : ScalarTy} : Scalar.cMin ty ≤ 0 ∧ 0 ≤ Scalar.cMax ty := by
+  cases ty <;> simp [Scalar.cMax, Scalar.cMin, Scalar.max, Scalar.min] <;> decide
 
 def Scalar.neg {ty : ScalarTy} (x : Scalar ty) : Result (Scalar ty) := Scalar.tryMk ty (- x.val)
 
@@ -1268,73 +1242,18 @@ def U128.ofIntCore  := @Scalar.ofIntCore .U128
 
 --  ofInt
 -- TODO: typeclass?
-@[match_pattern] abbrev Isize.ofInt := @Scalar.ofInt .Isize
-@[match_pattern] abbrev I8.ofInt    := @Scalar.ofInt .I8
-@[match_pattern] abbrev I16.ofInt   := @Scalar.ofInt .I16
-@[match_pattern] abbrev I32.ofInt   := @Scalar.ofInt .I32
-@[match_pattern] abbrev I64.ofInt   := @Scalar.ofInt .I64
-@[match_pattern] abbrev I128.ofInt  := @Scalar.ofInt .I128
-@[match_pattern] abbrev Usize.ofInt := @Scalar.ofInt .Usize
-@[match_pattern] abbrev U8.ofInt    := @Scalar.ofInt .U8
-@[match_pattern] abbrev U16.ofInt   := @Scalar.ofInt .U16
-@[match_pattern] abbrev U32.ofInt   := @Scalar.ofInt .U32
-@[match_pattern] abbrev U64.ofInt   := @Scalar.ofInt .U64
-@[match_pattern] abbrev U128.ofInt  := @Scalar.ofInt .U128
-
-postfix:max "#isize" => Isize.ofInt
-postfix:max "#i8"    => I8.ofInt
-postfix:max "#i16"   => I16.ofInt
-postfix:max "#i32"   => I32.ofInt
-postfix:max "#i64"   => I64.ofInt
-postfix:max "#i128"  => I128.ofInt
-postfix:max "#usize" => Usize.ofInt
-postfix:max "#u8"    => U8.ofInt
-postfix:max "#u16"   => U16.ofInt
-postfix:max "#u32"   => U32.ofInt
-postfix:max "#u64"   => U64.ofInt
-postfix:max "#u128"  => U128.ofInt
-
-/- Testing the notations -/
-example := 0#u32
-example := 1#u32
-example := 1#i32
-example := 0#isize
-example := (-1)#isize
-example (x : U32) : Bool :=
-  match x with
-  | 0#u32 => true
-  | _ => false
-
-example (x : U32) : Bool :=
-  match x with
-  | 1#u32 => true
-  | _ => false
-
-example (x : I32) : Bool :=
-  match x with
-  | (-1)#i32 => true
-  | _ => false
-
--- Notation for pattern matching
--- We make the precedence looser than the negation.
-notation:70 a:70 "#scalar" => Scalar.mk (a) _ _
-
-example {ty} (x : Scalar ty) : ℤ :=
-  match x with
-  | v#scalar => v
-
-example {ty} (x : Scalar ty) : Bool :=
-  match x with
-  | 1#scalar => true
-  | _ => false
-
-example {ty} (x : Scalar ty) : Bool :=
-  match x with
-  | -(1 : Int)#scalar => true
-  | _ => false
-
--- Testing the notations
-example : Result Usize := 0#usize + 1#usize
+abbrev Isize.ofInt := @Scalar.ofInt .Isize
+abbrev I8.ofInt    := @Scalar.ofInt .I8
+abbrev I16.ofInt   := @Scalar.ofInt .I16
+abbrev I32.ofInt   := @Scalar.ofInt .I32
+abbrev I64.ofInt   := @Scalar.ofInt .I64
+abbrev I128.ofInt  := @Scalar.ofInt .I128
+abbrev Usize.ofInt := @Scalar.ofInt .Usize
+abbrev U8.ofInt    := @Scalar.ofInt .U8
+abbrev U16.ofInt   := @Scalar.ofInt .U16
+abbrev U32.ofInt   := @Scalar.ofInt .U32
+abbrev U64.ofInt   := @Scalar.ofInt .U64
+abbrev U128.ofInt  := @Scalar.ofInt .U128
 
 -- TODO: factor those lemmas out
 @[simp] theorem Scalar.ofInt_val_eq {ty} (h : Scalar.min ty ≤ x ∧ x ≤ Scalar.max ty) : (Scalar.ofIntCore x h).val = x := by
@@ -1464,18 +1383,18 @@ theorem coe_max {ty: ScalarTy} (a b: Scalar ty): ↑(Max.max a b) = (Max.max (
 -- Max theory
 -- TODO: do the min theory later on.
 
-theorem Scalar.zero_le_unsigned {ty} (s: ¬ ty.isSigned) (x: Scalar ty): Scalar.ofInt 0 ≤ x := by
+theorem Scalar.zero_le_unsigned {ty} (s: ¬ ty.isSigned) (x: Scalar ty): Scalar.ofInt 0 (by simp) ≤ x := by
   apply (Scalar.le_equiv _ _).2
   convert x.hmin
   cases ty <;> simp [ScalarTy.isSigned] at s <;> simp [Scalar.min]
 
 @[simp]
 theorem Scalar.max_unsigned_left_zero_eq {ty} [s: Fact (¬ ty.isSigned)] (x: Scalar ty):
-  Max.max (Scalar.ofInt 0) x = x := max_eq_right (Scalar.zero_le_unsigned s.out x)
+  Max.max (Scalar.ofInt 0 (by simp)) x = x := max_eq_right (Scalar.zero_le_unsigned s.out x)
 
 @[simp]
 theorem Scalar.max_unsigned_right_zero_eq {ty} [s: Fact (¬ ty.isSigned)] (x: Scalar ty):
-  Max.max x (Scalar.ofInt 0) = x := max_eq_left (Scalar.zero_le_unsigned s.out x)
+  Max.max x (Scalar.ofInt 0 (by simp)) = x := max_eq_left (Scalar.zero_le_unsigned s.out x)
 
 -- Leading zeros
 def core.num.Usize.leading_zeros (x : Usize) : U32 := sorry
diff --git a/backends/lean/Base/Primitives/ScalarNotations.lean b/backends/lean/Base/Primitives/ScalarNotations.lean
new file mode 100644
index 00000000..50d8c1b6
--- /dev/null
+++ b/backends/lean/Base/Primitives/ScalarNotations.lean
@@ -0,0 +1,87 @@
+import Lean
+import Lean.Meta.Tactic.Simp
+import Mathlib.Tactic.Linarith
+import Base.Primitives.Scalar
+import Base.Arith
+
+namespace Primitives
+
+open Lean Meta Elab Term
+
+macro x:term:max "#isize" : term => `(Isize.ofInt $x (by scalar_tac))
+macro x:term:max "#i8"    : term => `(I8.ofInt $x (by scalar_tac))
+macro x:term:max "#i16"   : term => `(I16.ofInt $x (by scalar_tac))
+macro x:term:max "#i32"   : term => `(I32.ofInt $x (by scalar_tac))
+macro x:term:max "#i64"   : term => `(I64.ofInt $x (by scalar_tac))
+macro x:term:max "#i128"  : term => `(I128.ofInt $x (by scalar_tac))
+macro x:term:max "#usize" : term => `(Usize.ofInt $x (by scalar_tac))
+macro x:term:max "#u8"    : term => `(U8.ofInt $x (by scalar_tac))
+macro x:term:max "#u16"   : term => `(U16.ofInt $x (by scalar_tac))
+macro x:term:max "#u32"   : term => `(U32.ofInt $x (by scalar_tac))
+macro x:term:max "#u64"   : term => `(U64.ofInt $x (by scalar_tac))
+macro x:term:max "#u128"  : term => `(U128.ofInt $x (by scalar_tac))
+
+macro x:term:max noWs "u32"   : term => `(U32.ofInt $x (by scalar_tac))
+
+-- Notation for pattern matching
+-- We make the precedence looser than the negation.
+notation:70 a:70 "#scalar" => Scalar.mk (a) _ _
+
+/- Testing the notations -/
+example := 0#u32
+example := 1#u32
+example := 1#i32
+example := 0#isize
+example := (-1)#isize
+
+/-
+-- This doesn't work anymore
+example (x : U32) : Bool :=
+  match x with
+  | 0#u32 => true
+  | _ => false
+
+example (x : U32) : Bool :=
+  match x with
+  | 1#u32 => true
+  | _ => false
+
+example (x : I32) : Bool :=
+  match x with
+  | (-1)#i32 => true
+  | _ => false
+-/
+
+example (x : U32) : Bool :=
+  match x with
+  | 0#scalar => true
+  | _ => false
+
+example (x : U32) : Bool :=
+  match x with
+  | 1#scalar => true
+  | _ => false
+
+example (x : I32) : Bool :=
+  match x with
+  | (-1)#scalar => true
+  | _ => false
+
+example {ty} (x : Scalar ty) : ℤ :=
+  match x with
+  | v#scalar => v
+
+example {ty} (x : Scalar ty) : Bool :=
+  match x with
+  | 1#scalar => true
+  | _ => false
+
+example {ty} (x : Scalar ty) : Bool :=
+  match x with
+  | -(1 : Int)#scalar => true
+  | _ => false
+
+-- Testing the notations
+example : Result Usize := 0#usize + 1#usize
+
+end Primitives
-- 
cgit v1.2.3


From a46d785eb548043535a05d1b67dde48c18f5cf5f Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Wed, 12 Jun 2024 18:46:08 +0200
Subject: Add an example

---
 backends/lean/Base/Primitives/ScalarNotations.lean | 3 +++
 1 file changed, 3 insertions(+)

(limited to 'backends/lean/Base/Primitives')

diff --git a/backends/lean/Base/Primitives/ScalarNotations.lean b/backends/lean/Base/Primitives/ScalarNotations.lean
index 50d8c1b6..cc6e6f02 100644
--- a/backends/lean/Base/Primitives/ScalarNotations.lean
+++ b/backends/lean/Base/Primitives/ScalarNotations.lean
@@ -84,4 +84,7 @@ example {ty} (x : Scalar ty) : Bool :=
 -- Testing the notations
 example : Result Usize := 0#usize + 1#usize
 
+-- More complex expressions
+example (x y : Int) (h : 0 ≤ x + y ∧ x + y ≤ 1000) : U32 := (x + y)#u32
+
 end Primitives
-- 
cgit v1.2.3


From b25d1e2da70a1ed417f55650d80736df22e912d5 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Thu, 13 Jun 2024 10:47:26 +0200
Subject: Fix a proof

---
 backends/lean/Base/Primitives/ArraySlice.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'backends/lean/Base/Primitives')

diff --git a/backends/lean/Base/Primitives/ArraySlice.lean b/backends/lean/Base/Primitives/ArraySlice.lean
index 157f9df1..17ee626f 100644
--- a/backends/lean/Base/Primitives/ArraySlice.lean
+++ b/backends/lean/Base/Primitives/ArraySlice.lean
@@ -126,7 +126,7 @@ abbrev Slice.v {α : Type u} (v : Slice α) : List α := v.val
 example {a: Type u} (v : Slice a) : v.length ≤ Scalar.max ScalarTy.Usize := by
   scalar_tac
 
-def Slice.new (α : Type u): Slice α := ⟨ [], by apply Scalar.cMax_suffices .Usize; simp; decide ⟩
+def Slice.new (α : Type u): Slice α := ⟨ [], by apply Scalar.cMax_suffices .Usize; simp ⟩
 
 -- TODO: very annoying that the α is an explicit parameter
 def Slice.len (α : Type u) (v : Slice α) : Usize :=
-- 
cgit v1.2.3


From 1979d72b37d3a4abdff555da3f75ecfc9f629c26 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Thu, 13 Jun 2024 11:33:13 +0200
Subject: Fix more issues

---
 backends/lean/Base/Primitives/CoreConvertNum.lean  |  1 +
 backends/lean/Base/Primitives/ScalarNotations.lean | 33 +++++++++++++---------
 backends/lean/Base/Primitives/Vec.lean             |  4 +--
 3 files changed, 22 insertions(+), 16 deletions(-)

(limited to 'backends/lean/Base/Primitives')

diff --git a/backends/lean/Base/Primitives/CoreConvertNum.lean b/backends/lean/Base/Primitives/CoreConvertNum.lean
index eb456a96..b53d11db 100644
--- a/backends/lean/Base/Primitives/CoreConvertNum.lean
+++ b/backends/lean/Base/Primitives/CoreConvertNum.lean
@@ -4,6 +4,7 @@ import Init.Data.List.Basic
 import Mathlib.Tactic.Linarith
 import Base.IList
 import Base.Primitives.Scalar
+import Base.Primitives.ScalarNotations
 import Base.Primitives.ArraySlice
 import Base.Arith
 import Base.Progress.Base
diff --git a/backends/lean/Base/Primitives/ScalarNotations.lean b/backends/lean/Base/Primitives/ScalarNotations.lean
index cc6e6f02..94c0c779 100644
--- a/backends/lean/Base/Primitives/ScalarNotations.lean
+++ b/backends/lean/Base/Primitives/ScalarNotations.lean
@@ -8,20 +8,18 @@ namespace Primitives
 
 open Lean Meta Elab Term
 
-macro x:term:max "#isize" : term => `(Isize.ofInt $x (by scalar_tac))
-macro x:term:max "#i8"    : term => `(I8.ofInt $x (by scalar_tac))
-macro x:term:max "#i16"   : term => `(I16.ofInt $x (by scalar_tac))
-macro x:term:max "#i32"   : term => `(I32.ofInt $x (by scalar_tac))
-macro x:term:max "#i64"   : term => `(I64.ofInt $x (by scalar_tac))
-macro x:term:max "#i128"  : term => `(I128.ofInt $x (by scalar_tac))
-macro x:term:max "#usize" : term => `(Usize.ofInt $x (by scalar_tac))
-macro x:term:max "#u8"    : term => `(U8.ofInt $x (by scalar_tac))
-macro x:term:max "#u16"   : term => `(U16.ofInt $x (by scalar_tac))
-macro x:term:max "#u32"   : term => `(U32.ofInt $x (by scalar_tac))
-macro x:term:max "#u64"   : term => `(U64.ofInt $x (by scalar_tac))
-macro x:term:max "#u128"  : term => `(U128.ofInt $x (by scalar_tac))
-
-macro x:term:max noWs "u32"   : term => `(U32.ofInt $x (by scalar_tac))
+macro:max x:term:max noWs "#isize" : term => `(Isize.ofInt $x (by scalar_tac))
+macro:max x:term:max noWs "#i8"    : term => `(I8.ofInt $x (by scalar_tac))
+macro:max x:term:max noWs "#i16"   : term => `(I16.ofInt $x (by scalar_tac))
+macro:max x:term:max noWs "#i32"   : term => `(I32.ofInt $x (by scalar_tac))
+macro:max x:term:max noWs "#i64"   : term => `(I64.ofInt $x (by scalar_tac))
+macro:max x:term:max noWs "#i128"  : term => `(I128.ofInt $x (by scalar_tac))
+macro:max x:term:max noWs "#usize" : term => `(Usize.ofInt $x (by scalar_tac))
+macro:max x:term:max noWs "#u8"    : term => `(U8.ofInt $x (by scalar_tac))
+macro:max x:term:max noWs "#u16"   : term => `(U16.ofInt $x (by scalar_tac))
+macro:max x:term:max noWs "#u32"   : term => `(U32.ofInt $x (by scalar_tac))
+macro:max x:term:max noWs "#u64"   : term => `(U64.ofInt $x (by scalar_tac))
+macro:max x:term:max noWs "#u128"  : term => `(U128.ofInt $x (by scalar_tac))
 
 -- Notation for pattern matching
 -- We make the precedence looser than the negation.
@@ -87,4 +85,11 @@ example : Result Usize := 0#usize + 1#usize
 -- More complex expressions
 example (x y : Int) (h : 0 ≤ x + y ∧ x + y ≤ 1000) : U32 := (x + y)#u32
 
+section Scalar.Examples
+abbrev NList (a : Type) (x : U32) := { l : List a // l.length = x.val }
+
+example : NList Int 0#u32 := ⟨ [], by simp ⟩
+
+end Scalar.Examples
+
 end Primitives
diff --git a/backends/lean/Base/Primitives/Vec.lean b/backends/lean/Base/Primitives/Vec.lean
index 5ed7b606..d144fcb8 100644
--- a/backends/lean/Base/Primitives/Vec.lean
+++ b/backends/lean/Base/Primitives/Vec.lean
@@ -34,7 +34,7 @@ abbrev Vec.v {α : Type u} (v : Vec α) : List α := v.val
 example {a: Type u} (v : Vec a) : v.length ≤ Scalar.max ScalarTy.Usize := by
   scalar_tac
 
-def Vec.new (α : Type u): Vec α := ⟨ [], by apply Scalar.cMax_suffices .Usize; simp; decide ⟩
+def Vec.new (α : Type u): Vec α := ⟨ [], by apply Scalar.cMax_suffices .Usize; simp ⟩
 
 instance (α : Type u) : Inhabited (Vec α) := by
   constructor
@@ -192,7 +192,7 @@ def alloc.slice.Slice.to_vec
 def core.slice.Slice.reverse (T : Type) (s : Slice T) : Slice T :=
   ⟨ s.val.reverse, by sorry ⟩
 
-def alloc.vec.Vec.with_capacity (T : Type) (s : Usize) : alloc.vec.Vec T := Vec.new T
+def alloc.vec.Vec.with_capacity (T : Type) (_ : Usize) : alloc.vec.Vec T := Vec.new T
 
 /- [alloc::vec::{(core::ops::deref::Deref for alloc::vec::Vec<T, A>)#9}::deref]:
    Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/alloc/src/vec/mod.rs', lines 2624:4-2624:27
-- 
cgit v1.2.3


From 87d088fa9e4493f32ae3f8d447ff1ff6d44e6396 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Thu, 13 Jun 2024 15:07:21 +0200
Subject: Fix more issues with the scalar notations

---
 backends/lean/Base/Primitives/ScalarNotations.lean | 44 ++++++++++++++--------
 1 file changed, 29 insertions(+), 15 deletions(-)

(limited to 'backends/lean/Base/Primitives')

diff --git a/backends/lean/Base/Primitives/ScalarNotations.lean b/backends/lean/Base/Primitives/ScalarNotations.lean
index 94c0c779..3bc86a9c 100644
--- a/backends/lean/Base/Primitives/ScalarNotations.lean
+++ b/backends/lean/Base/Primitives/ScalarNotations.lean
@@ -8,18 +8,24 @@ namespace Primitives
 
 open Lean Meta Elab Term
 
-macro:max x:term:max noWs "#isize" : term => `(Isize.ofInt $x (by scalar_tac))
-macro:max x:term:max noWs "#i8"    : term => `(I8.ofInt $x (by scalar_tac))
-macro:max x:term:max noWs "#i16"   : term => `(I16.ofInt $x (by scalar_tac))
-macro:max x:term:max noWs "#i32"   : term => `(I32.ofInt $x (by scalar_tac))
-macro:max x:term:max noWs "#i64"   : term => `(I64.ofInt $x (by scalar_tac))
-macro:max x:term:max noWs "#i128"  : term => `(I128.ofInt $x (by scalar_tac))
-macro:max x:term:max noWs "#usize" : term => `(Usize.ofInt $x (by scalar_tac))
-macro:max x:term:max noWs "#u8"    : term => `(U8.ofInt $x (by scalar_tac))
-macro:max x:term:max noWs "#u16"   : term => `(U16.ofInt $x (by scalar_tac))
-macro:max x:term:max noWs "#u32"   : term => `(U32.ofInt $x (by scalar_tac))
-macro:max x:term:max noWs "#u64"   : term => `(U64.ofInt $x (by scalar_tac))
-macro:max x:term:max noWs "#u128"  : term => `(U128.ofInt $x (by scalar_tac))
+/- Something strange happens here: when we solve the goal with scalar_tac, it
+   sometimes leaves meta-variables in place, which then causes issues when
+   type-checking functions. For instance, it happens when we have const-generics
+   in the translation: the constants contain meta-variables, which are then
+   used in the types, which cause issues later. An example is given below:
+ -/
+macro:max x:term:max noWs "#isize" : term => `(Isize.ofInt $x (by first | decide | scalar_tac))
+macro:max x:term:max noWs "#i8"    : term => `(I8.ofInt $x (by first | decide | scalar_tac))
+macro:max x:term:max noWs "#i16"   : term => `(I16.ofInt $x (by first | decide | scalar_tac))
+macro:max x:term:max noWs "#i32"   : term => `(I32.ofInt $x (by first | decide | scalar_tac))
+macro:max x:term:max noWs "#i64"   : term => `(I64.ofInt $x (by first | decide | scalar_tac))
+macro:max x:term:max noWs "#i128"  : term => `(I128.ofInt $x (by first | decide | scalar_tac))
+macro:max x:term:max noWs "#usize" : term => `(Usize.ofInt $x (by first | decide | scalar_tac))
+macro:max x:term:max noWs "#u8"    : term => `(U8.ofInt $x (by first | decide | scalar_tac))
+macro:max x:term:max noWs "#u16"   : term => `(U16.ofInt $x (by first | decide | scalar_tac))
+macro:max x:term:max noWs "#u32"   : term => `(U32.ofInt $x (by first | decide | scalar_tac))
+macro:max x:term:max noWs "#u64"   : term => `(U64.ofInt $x (by first | decide | scalar_tac))
+macro:max x:term:max noWs "#u128"  : term => `(U128.ofInt $x (by first | decide | scalar_tac))
 
 -- Notation for pattern matching
 -- We make the precedence looser than the negation.
@@ -32,6 +38,8 @@ example := 1#i32
 example := 0#isize
 example := (-1)#isize
 
+example := 1#u32
+
 /-
 -- This doesn't work anymore
 example (x : U32) : Bool :=
@@ -85,10 +93,16 @@ example : Result Usize := 0#usize + 1#usize
 -- More complex expressions
 example (x y : Int) (h : 0 ≤ x + y ∧ x + y ≤ 1000) : U32 := (x + y)#u32
 
-section Scalar.Examples
-abbrev NList (a : Type) (x : U32) := { l : List a // l.length = x.val }
+namespace Scalar.Examples
+
+  abbrev Array (a : Type) (len : U32) := { l : List a // l.length = len.val }
+
+  -- Checking the syntax
+  example : Array Int 0#u32 := ⟨ [], by simp ⟩
 
-example : NList Int 0#u32 := ⟨ [], by simp ⟩
+  /- The example below fails if we don't use `decide` in the elaboration
+     of the scalar notation -/
+  example (a : Array (Array Int 32#u32) 32#u32) := a
 
 end Scalar.Examples
 
-- 
cgit v1.2.3


From b3dd78ff4c8785b6ff9bce9927df90f8c78a9109 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Thu, 13 Jun 2024 22:04:13 +0200
Subject: Update Lean to v4.9.0-rc1

---
 backends/lean/Base/Primitives/ArraySlice.lean |  3 +--
 backends/lean/Base/Primitives/Scalar.lean     | 24 ++++++++++++------------
 backends/lean/Base/Primitives/Vec.lean        |  3 +--
 3 files changed, 14 insertions(+), 16 deletions(-)

(limited to 'backends/lean/Base/Primitives')

diff --git a/backends/lean/Base/Primitives/ArraySlice.lean b/backends/lean/Base/Primitives/ArraySlice.lean
index 17ee626f..be460987 100644
--- a/backends/lean/Base/Primitives/ArraySlice.lean
+++ b/backends/lean/Base/Primitives/ArraySlice.lean
@@ -325,8 +325,7 @@ theorem Slice.subslice_spec {α : Type u} [Inhabited α] (s : Slice α) (r : Ran
   have := List.index_slice r.start.val r.end_.val i s.val (by scalar_tac) (by scalar_tac) (by trivial) (by scalar_tac)
   simp [*]
 
-attribute [pp_dot] List.len List.length List.index -- use the dot notation when printing
-set_option pp.coercions false -- do not print coercions with ↑ (this doesn't parse)
+set_option pp.fieldNotation.generalized true
 
 def Slice.update_subslice (α : Type u) (s : Slice α) (r : Range Usize) (ss : Slice α) : Result (Slice α) :=
   -- TODO: not completely sure here
diff --git a/backends/lean/Base/Primitives/Scalar.lean b/backends/lean/Base/Primitives/Scalar.lean
index f4264b9b..9f809ead 100644
--- a/backends/lean/Base/Primitives/Scalar.lean
+++ b/backends/lean/Base/Primitives/Scalar.lean
@@ -1,6 +1,5 @@
 import Lean
 import Lean.Meta.Tactic.Simp
-import Mathlib.Tactic.Linarith
 import Base.Primitives.Base
 import Base.Primitives.Core
 import Base.Diverge.Base
@@ -9,6 +8,9 @@ import Base.Arith.Int
 
 namespace Primitives
 
+-- Deactivate the warnings which appear when we use `#assert`
+set_option linter.hashCommand false
+
 ----------------------
 -- MACHINE INTEGERS --
 ----------------------
@@ -279,11 +281,11 @@ theorem Scalar.cMax_bound ty : Scalar.cMax ty ≤ Scalar.max ty := by
 
 theorem Scalar.cMin_suffices ty (h : Scalar.cMin ty ≤ x) : Scalar.min ty ≤ x := by
   have := Scalar.cMin_bound ty
-  linarith
+  omega
 
 theorem Scalar.cMax_suffices ty (h : x ≤ Scalar.cMax ty) : x ≤ Scalar.max ty := by
   have := Scalar.cMax_bound ty
-  linarith
+  omega
 
 /-- The scalar type.
 
@@ -310,7 +312,7 @@ theorem Scalar.bound_suffices (ty : ScalarTy) (x : Int) :
   Scalar.min ty ≤ x ∧ x ≤ Scalar.max ty
   :=
   λ h => by
-  apply And.intro <;> have hmin := Scalar.cMin_bound ty <;> have hmax := Scalar.cMax_bound ty <;> linarith
+  apply And.intro <;> have hmin := Scalar.cMin_bound ty <;> have hmax := Scalar.cMax_bound ty <;> omega
 
 def Scalar.ofIntCore {ty : ScalarTy} (x : Int)
   (h : Scalar.min ty ≤ x ∧ x ≤ Scalar.max ty) : Scalar ty :=
@@ -345,7 +347,7 @@ theorem Scalar.check_bounds_imp_in_bounds {ty : ScalarTy} {x : Int}
   have ⟨ hmin, hmax ⟩ := h
   have hbmin := Scalar.cMin_bound ty
   have hbmax := Scalar.cMax_bound ty
-  cases hmin <;> cases hmax <;> apply And.intro <;> linarith
+  cases hmin <;> cases hmax <;> apply And.intro <;> omega
 
 theorem Scalar.check_bounds_eq_in_bounds (ty : ScalarTy) (x : Int) :
   Scalar.check_bounds ty x ↔ Scalar.in_bounds ty x := by
@@ -730,7 +732,6 @@ theorem Scalar.add_spec {ty} {x y : Scalar ty}
   (∃ z, x + y = ok z ∧ (↑z : Int) = ↑x + ↑y) := by
   have h := @add_equiv ty x y
   split at h <;> simp_all
-  apply h
 
 theorem Scalar.add_unsigned_spec {ty} (s: ¬ ty.isSigned) {x y : Scalar ty}
   (hmax : ↑x + ↑y ≤ Scalar.max ty) :
@@ -738,7 +739,7 @@ theorem Scalar.add_unsigned_spec {ty} (s: ¬ ty.isSigned) {x y : Scalar ty}
   have hmin : Scalar.min ty ≤ ↑x + ↑y := by
     have hx := x.hmin
     have hy := y.hmin
-    cases ty <;> simp [min, ScalarTy.isSigned] at * <;> linarith
+    cases ty <;> simp [min, ScalarTy.isSigned] at * <;> omega
   apply add_spec <;> assumption
 
 /- Fine-grained theorems -/
@@ -825,7 +826,6 @@ theorem Scalar.sub_spec {ty} {x y : Scalar ty}
   ∃ z, x - y = ok z ∧ (↑z : Int) = ↑x - ↑y := by
   have h := @sub_equiv ty x y
   split at h <;> simp_all
-  apply h
 
 theorem Scalar.sub_unsigned_spec {ty : ScalarTy} (s : ¬ ty.isSigned)
   {x y : Scalar ty} (hmin : Scalar.min ty ≤ ↑x - ↑y) :
@@ -834,7 +834,7 @@ theorem Scalar.sub_unsigned_spec {ty : ScalarTy} (s : ¬ ty.isSigned)
     have hx := x.hmin
     have hxm := x.hmax
     have hy := y.hmin
-    cases ty <;> simp [min, max, ScalarTy.isSigned] at * <;> linarith
+    cases ty <;> simp [min, max, ScalarTy.isSigned] at * <;> omega
   intros
   apply sub_spec <;> assumption
 
@@ -1030,11 +1030,11 @@ theorem Scalar.div_unsigned_spec {ty} (s: ¬ ty.isSigned) (x : Scalar ty) {y : S
   have hx := x.hmin
   have hy := y.hmin
   simp [h] at hx hy
-  have hmin : 0 ≤ ↑x / ↑y := Int.ediv_nonneg hx hy
+  have hmin : 0 ≤ x.val / y.val := Int.ediv_nonneg hx hy
   have hmax : ↑x / ↑y ≤ Scalar.max ty := by
     have := Int.ediv_le_self ↑y hx
     have := x.hmax
-    linarith
+    omega
   have hs := @div_spec ty x y hnz
   simp [*] at hs
   apply hs
@@ -1151,7 +1151,7 @@ theorem Scalar.rem_unsigned_spec {ty} (s: ¬ ty.isSigned) (x : Scalar ty) {y : S
     have h : (0 : Int) < y := by int_tac
     have h := Int.emod_lt_of_pos ↑x h
     have := y.hmax
-    linarith
+    omega
   have hs := @rem_spec ty x y hnz
   simp [*] at hs
   simp [*]
diff --git a/backends/lean/Base/Primitives/Vec.lean b/backends/lean/Base/Primitives/Vec.lean
index d144fcb8..0b010944 100644
--- a/backends/lean/Base/Primitives/Vec.lean
+++ b/backends/lean/Base/Primitives/Vec.lean
@@ -2,7 +2,6 @@
 import Lean
 import Lean.Meta.Tactic.Simp
 import Init.Data.List.Basic
-import Mathlib.Tactic.Linarith
 import Base.IList
 import Base.Primitives.Scalar
 import Base.Primitives.ArraySlice
@@ -59,7 +58,7 @@ def Vec.push (α : Type u) (v : Vec α) (x : α) : Result (Vec α)
     have h : nlen ≤ Usize.max := by
       simp [Usize.max] at *
       have hm := Usize.refined_max.property
-      cases h <;> cases hm <;> simp [U32.max, U64.max] at * <;> try linarith
+      cases h <;> cases hm <;> simp [U32.max, U64.max] at * <;> try omega
     ok ⟨ List.concat v.val x, by simp at *; assumption ⟩
   else
     fail maximumSizeExceeded
-- 
cgit v1.2.3