3 files changed, 18 insertions, 8 deletions

diff --git a/backends/lean/Base/Primitives/ArraySlice.lean b/backends/lean/Base/Primitives/ArraySlice.lean
index be460987..899871af 100644
--- a/backends/lean/Base/Primitives/ArraySlice.lean
+++ b/backends/lean/Base/Primitives/ArraySlice.lean
@@ -129,7 +129,7 @@ example {a: Type u} (v : Slice a) : v.length ≤ Scalar.max ScalarTy.Usize := by
 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 :=
+abbrev Slice.len (α : Type u) (v : Slice α) : Usize :=
   Usize.ofIntCore v.val.len (by constructor <;> scalar_tac)
 
 @[simp]
diff --git a/backends/lean/Base/Primitives/Scalar.lean b/backends/lean/Base/Primitives/Scalar.lean
index 9f809ead..31038e0d 100644
--- a/backends/lean/Base/Primitives/Scalar.lean
+++ b/backends/lean/Base/Primitives/Scalar.lean
@@ -1301,22 +1301,25 @@ instance {ty} : LT (Scalar ty) where
 
 instance {ty} : LE (Scalar ty) where le a b := LE.le a.val b.val
 
--- Not marking this one with @[simp] on purpose
+-- Not marking this one with @[simp] on purpose: if we have `x = y` somewhere in the context,
+-- we may want to use it to substitute `y` with `x` somewhere.
+-- TODO: mark it as simp anyway?
 theorem Scalar.eq_equiv {ty : ScalarTy} (x y : Scalar ty) :
   x = y ↔ (↑x : Int) = ↑y := by
   cases x; cases y; simp_all
 
 -- This is sometimes useful when rewriting the goal with the local assumptions
+-- TODO: this doesn't get triggered
 @[simp] theorem Scalar.eq_imp {ty : ScalarTy} (x y : Scalar ty) :
   (↑x : Int) = ↑y → x = y := (eq_equiv x y).mpr
 
-theorem Scalar.lt_equiv {ty : ScalarTy} (x y : Scalar ty) :
+@[simp] theorem Scalar.lt_equiv {ty : ScalarTy} (x y : Scalar ty) :
   x < y ↔ (↑x : Int) < ↑y := by simp [LT.lt]
 
 @[simp] theorem Scalar.lt_imp {ty : ScalarTy} (x y : Scalar ty) :
   (↑x : Int) < (↑y) → x < y := (lt_equiv x y).mpr
 
-theorem Scalar.le_equiv {ty : ScalarTy} (x y : Scalar ty) :
+@[simp] theorem Scalar.le_equiv {ty : ScalarTy} (x y : Scalar ty) :
   x ≤ y ↔ (↑x : Int) ≤ ↑y := by simp [LE.le]
 
 @[simp] theorem Scalar.le_imp {ty : ScalarTy} (x y : Scalar ty) :
@@ -1377,8 +1380,6 @@ theorem coe_max {ty: ScalarTy} (a b: Scalar ty): ↑(Max.max a b) = (Max.max (â†
   -- TODO: there should be a shorter way to prove this.
   rw [max_def, max_def]
   split_ifs <;> simp_all
-  refine' absurd _ (lt_irrefl a)
-  exact lt_of_le_of_lt (by assumption) ((Scalar.lt_equiv _ _).2 (by assumption))
 
 -- Max theory
 -- TODO: do the min theory later on.
diff --git a/backends/lean/Base/Primitives/Vec.lean b/backends/lean/Base/Primitives/Vec.lean
index 0b010944..e584777a 100644
--- a/backends/lean/Base/Primitives/Vec.lean
+++ b/backends/lean/Base/Primitives/Vec.lean
@@ -33,14 +33,15 @@ 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 ⟩
+abbrev Vec.new (α : Type u): Vec α := ⟨ [], by apply Scalar.cMax_suffices .Usize; simp ⟩
 
 instance (α : Type u) : Inhabited (Vec α) := by
   constructor
   apply Vec.new
 
 -- TODO: very annoying that the α is an explicit parameter
-def Vec.len (α : Type u) (v : Vec α) : Usize :=
+@[simp]
+abbrev Vec.len (α : Type u) (v : Vec α) : Usize :=
   Usize.ofIntCore v.val.len (by constructor <;> scalar_tac)
 
 @[simp]
@@ -63,6 +64,14 @@ def Vec.push (α : Type u) (v : Vec α) (x : α) : Result (Vec α)
   else
     fail maximumSizeExceeded
 
+@[pspec]
+theorem Vec.push_spec {α : Type u} (v : Vec α) (x : α) (h : v.val.len < Usize.max) :
+  ∃ v1, v.push α x = ok v1 ∧
+  v1.val = v.val ++ [x] := by
+  simp [push]
+  split <;> simp_all [List.len_eq_length]
+  scalar_tac
+
 -- This shouldn't be used
 def Vec.insert_fwd (α : Type u) (v: Vec α) (i: Usize) (_: α) : Result Unit :=
   if i.val < v.length then