From 3e8060b5501ec83940a4309389a68898df26ebd0 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Mon, 17 Jul 2023 23:37:31 +0200
Subject: Reorganize the Lean backend

---
 backends/lean/Base/Primitives/Base.lean   | 130 ++++++++
 backends/lean/Base/Primitives/Scalar.lean | 507 ++++++++++++++++++++++++++++++
 backends/lean/Base/Primitives/Vec.lean    | 113 +++++++
 3 files changed, 750 insertions(+)
 create mode 100644 backends/lean/Base/Primitives/Base.lean
 create mode 100644 backends/lean/Base/Primitives/Scalar.lean
 create mode 100644 backends/lean/Base/Primitives/Vec.lean

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

diff --git a/backends/lean/Base/Primitives/Base.lean b/backends/lean/Base/Primitives/Base.lean
new file mode 100644
index 00000000..db462c38
--- /dev/null
+++ b/backends/lean/Base/Primitives/Base.lean
@@ -0,0 +1,130 @@
+import Lean
+
+namespace Primitives
+
+--------------------
+-- ASSERT COMMAND --Std.
+--------------------
+
+open Lean Elab Command Term Meta
+
+syntax (name := assert) "#assert" term: command
+
+@[command_elab assert]
+unsafe
+def assertImpl : CommandElab := fun (_stx: Syntax) => do
+  runTermElabM (fun _ => do
+    let r ← evalTerm Bool (mkConst ``Bool) _stx[1]
+    if not r then
+      logInfo ("Assertion failed for:\n" ++ _stx[1])
+      throwError ("Expression reduced to false:\n"  ++ _stx[1])
+    pure ())
+
+#eval 2 == 2
+#assert (2 == 2)
+
+-------------
+-- PRELUDE --
+-------------
+
+-- Results & monadic combinators
+
+inductive Error where
+   | assertionFailure: Error
+   | integerOverflow: Error
+   | divisionByZero: Error
+   | arrayOutOfBounds: Error
+   | maximumSizeExceeded: Error
+   | panic: Error
+deriving Repr, BEq
+
+open Error
+
+inductive Result (α : Type u) where
+  | ret (v: α): Result α
+  | fail (e: Error): Result α
+  | div
+deriving Repr, BEq
+
+open Result
+
+instance Result_Inhabited (α : Type u) : Inhabited (Result α) :=
+  Inhabited.mk (fail panic)
+
+instance Result_Nonempty (α : Type u) : Nonempty (Result α) :=
+  Nonempty.intro div
+
+/- HELPERS -/
+
+def ret? {α: Type u} (r: Result α): Bool :=
+  match r with
+  | ret _ => true
+  | fail _ | div => false
+
+def div? {α: Type u} (r: Result α): Bool :=
+  match r with
+  | div => true
+  | ret _ | fail _ => false
+
+def massert (b:Bool) : Result Unit :=
+  if b then ret () else fail assertionFailure
+
+def eval_global {α: Type u} (x: Result α) (_: ret? x): α :=
+  match x with
+  | fail _ | div => by contradiction
+  | ret x => x
+
+/- DO-DSL SUPPORT -/
+
+def bind {α : Type u} {β : Type v} (x: Result α) (f: α -> Result β) : Result β :=
+  match x with
+  | ret v  => f v 
+  | fail v => fail v
+  | div => div
+
+-- Allows using Result in do-blocks
+instance : Bind Result where
+  bind := bind
+
+-- Allows using return x in do-blocks
+instance : Pure Result where
+  pure := fun x => ret x
+
+@[simp] theorem bind_ret (x : α) (f : α → Result β) : bind (.ret x) f = f x := by simp [bind]
+@[simp] theorem bind_fail (x : Error) (f : α → Result β) : bind (.fail x) f = .fail x := by simp [bind]
+@[simp] theorem bind_div (f : α → Result β) : bind .div f = .div := by simp [bind]
+
+/- CUSTOM-DSL SUPPORT -/
+
+-- Let-binding the Result of a monadic operation is oftentimes not sufficient,
+-- because we may need a hypothesis for equational reasoning in the scope. We
+-- rely on subtype, and a custom let-binding operator, in effect recreating our
+-- own variant of the do-dsl
+
+def Result.attach {α: Type} (o : Result α): Result { x : α // o = ret x } :=
+  match o with
+  | ret x => ret ⟨x, rfl⟩
+  | fail e => fail e
+  | div => div
+
+@[simp] theorem bind_tc_ret (x : α) (f : α → Result β) :
+  (do let y ← .ret x; f y) = f x := by simp [Bind.bind, bind]
+
+@[simp] theorem bind_tc_fail (x : Error) (f : α → Result β) :
+  (do let y ← fail x; f y) = fail x := by simp [Bind.bind, bind]
+
+@[simp] theorem bind_tc_div (f : α → Result β) :
+  (do let y ← div; f y) = div := by simp [Bind.bind, bind]
+
+----------
+-- MISC --
+----------
+
+@[simp] def mem.replace (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 ]` -/
+register_simp_attr aeneas
+
+end Primitives
diff --git a/backends/lean/Base/Primitives/Scalar.lean b/backends/lean/Base/Primitives/Scalar.lean
new file mode 100644
index 00000000..241dfa07
--- /dev/null
+++ b/backends/lean/Base/Primitives/Scalar.lean
@@ -0,0 +1,507 @@
+import Lean
+import Lean.Meta.Tactic.Simp
+import Mathlib.Tactic.Linarith
+import Base.Primitives.Base
+
+namespace Primitives
+
+----------------------
+-- MACHINE INTEGERS --
+----------------------
+
+-- We redefine our machine integers types.
+
+-- For Isize/Usize, we reuse `getNumBits` from `USize`. You cannot reduce `getNumBits`
+-- using the simplifier, meaning that proofs do not depend on the compile-time value of
+-- USize.size. (Lean assumes 32 or 64-bit platforms, and Rust doesn't really support, at
+-- least officially, 16-bit microcontrollers, so this seems like a fine design decision
+-- for now.)
+
+-- Note from Chris Bailey: "If there's more than one salient property of your
+-- definition then the subtyping strategy might get messy, and the property part
+-- of a subtype is less discoverable by the simplifier or tactics like
+-- library_search." So, we will not add refinements on the return values of the
+-- operations defined on Primitives, but will rather rely on custom lemmas to
+-- invert on possible return values of the primitive operations.
+
+-- Machine integer constants, done via `ofNatCore`, which requires a proof that
+-- the `Nat` fits within the desired integer type. We provide a custom tactic.
+
+open Result Error
+open System.Platform.getNumBits
+
+-- TODO: is there a way of only importing System.Platform.getNumBits?
+--
+@[simp] def size_num_bits : Nat := (System.Platform.getNumBits ()).val
+
+-- Remark: Lean seems to use < for the comparisons with the upper bounds by convention.
+
+-- The "structured" bounds
+def Isize.smin : Int := - (HPow.hPow 2 (size_num_bits - 1))
+def Isize.smax : Int := (HPow.hPow 2 (size_num_bits - 1)) - 1
+def I8.smin    : Int := - (HPow.hPow 2 7)
+def I8.smax    : Int := HPow.hPow 2 7 - 1
+def I16.smin   : Int := - (HPow.hPow 2 15)
+def I16.smax   : Int := HPow.hPow 2 15 - 1
+def I32.smin   : Int := -(HPow.hPow 2 31)
+def I32.smax   : Int := HPow.hPow 2 31 - 1
+def I64.smin   : Int := -(HPow.hPow 2 63)
+def I64.smax   : Int := HPow.hPow 2 63 - 1
+def I128.smin  : Int := -(HPow.hPow 2 127)
+def I128.smax  : Int := HPow.hPow 2 127 - 1
+def Usize.smin : Int := 0
+def Usize.smax : Int := HPow.hPow 2 size_num_bits - 1
+def U8.smin    : Int := 0
+def U8.smax    : Int := HPow.hPow 2 8 - 1
+def U16.smin   : Int := 0
+def U16.smax   : Int := HPow.hPow 2 16 - 1
+def U32.smin   : Int := 0
+def U32.smax   : Int := HPow.hPow 2 32 - 1
+def U64.smin   : Int := 0
+def U64.smax   : Int := HPow.hPow 2 64 - 1
+def U128.smin  : Int := 0
+def U128.smax  : Int := HPow.hPow 2 128 - 1
+
+-- The "normalized" bounds, that we use in practice
+def I8.min    := -128
+def I8.max   := 127
+def I16.min  := -32768
+def I16.max  := 32767
+def I32.min  := -2147483648
+def I32.max  := 2147483647
+def I64.min  := -9223372036854775808
+def I64.max  := 9223372036854775807
+def I128.min := -170141183460469231731687303715884105728
+def I128.max := 170141183460469231731687303715884105727
+@[simp] def U8.min   := 0
+def U8.max   := 255
+@[simp] def U16.min  := 0
+def U16.max  := 65535
+@[simp] def U32.min  := 0
+def U32.max  := 4294967295
+@[simp] def U64.min  := 0
+def U64.max  := 18446744073709551615
+@[simp] def U128.min := 0
+def U128.max := 340282366920938463463374607431768211455
+@[simp] def Usize.min := 0
+
+def Isize.refined_min : { n:Int // n = I32.min ∨ n = I64.min } :=
+  ⟨ Isize.smin, by
+    simp [Isize.smin]
+    cases System.Platform.numBits_eq <;>
+    unfold System.Platform.numBits at * <;> simp [*] ⟩
+
+def Isize.refined_max : { n:Int // n = I32.max ∨ n = I64.max } :=
+  ⟨ Isize.smax, by
+    simp [Isize.smax]
+    cases System.Platform.numBits_eq <;>
+    unfold System.Platform.numBits at * <;> simp [*] ⟩
+
+def Usize.refined_max : { n:Int // n = U32.max ∨ n = U64.max } :=
+  ⟨ Usize.smax, by
+    simp [Usize.smax]
+    cases System.Platform.numBits_eq <;>
+    unfold System.Platform.numBits at * <;> simp [*] ⟩
+
+def Isize.min := Isize.refined_min.val
+def Isize.max := Isize.refined_max.val
+def Usize.max := Usize.refined_max.val
+
+inductive ScalarTy :=
+| Isize
+| I8
+| I16
+| I32
+| I64
+| I128
+| Usize
+| U8
+| U16
+| U32
+| U64
+| U128
+
+def Scalar.smin (ty : ScalarTy) : Int :=
+  match ty with
+  | .Isize => Isize.smin
+  | .I8    => I8.smin
+  | .I16   => I16.smin
+  | .I32   => I32.smin
+  | .I64   => I64.smin
+  | .I128  => I128.smin
+  | .Usize => Usize.smin
+  | .U8    => U8.smin
+  | .U16   => U16.smin
+  | .U32   => U32.smin
+  | .U64   => U64.smin
+  | .U128  => U128.smin
+
+def Scalar.smax (ty : ScalarTy) : Int :=
+  match ty with
+  | .Isize => Isize.smax
+  | .I8    => I8.smax
+  | .I16   => I16.smax
+  | .I32   => I32.smax
+  | .I64   => I64.smax
+  | .I128  => I128.smax
+  | .Usize => Usize.smax
+  | .U8    => U8.smax
+  | .U16   => U16.smax
+  | .U32   => U32.smax
+  | .U64   => U64.smax
+  | .U128  => U128.smax
+
+def Scalar.min (ty : ScalarTy) : Int :=
+  match ty with
+  | .Isize => Isize.min
+  | .I8    => I8.min
+  | .I16   => I16.min
+  | .I32   => I32.min
+  | .I64   => I64.min
+  | .I128  => I128.min
+  | .Usize => Usize.min
+  | .U8    => U8.min
+  | .U16   => U16.min
+  | .U32   => U32.min
+  | .U64   => U64.min
+  | .U128  => U128.min
+
+def Scalar.max (ty : ScalarTy) : Int :=
+  match ty with
+  | .Isize => Isize.max
+  | .I8    => I8.max
+  | .I16   => I16.max
+  | .I32   => I32.max
+  | .I64   => I64.max
+  | .I128  => I128.max
+  | .Usize => Usize.max
+  | .U8    => U8.max
+  | .U16   => U16.max
+  | .U32   => U32.max
+  | .U64   => U64.max
+  | .U128  => U128.max
+
+def Scalar.smin_eq (ty : ScalarTy) : Scalar.min ty = Scalar.smin ty := by
+  cases ty <;> rfl
+
+def Scalar.smax_eq (ty : ScalarTy) : Scalar.max ty = Scalar.smax ty := by
+  cases ty <;> rfl
+
+-- "Conservative" bounds
+-- We use those because we can't compare to the isize bounds (which can't
+-- reduce at compile-time). Whenever we perform an arithmetic operation like
+-- addition we need to check that the result is in bounds: we first compare
+-- to the conservative bounds, which reduce, then compare to the real bounds.
+-- This is useful for the various #asserts that we want to reduce at
+-- type-checking time.
+def Scalar.cMin (ty : ScalarTy) : Int :=
+  match ty with
+  | .Isize => Scalar.min .I32
+  | _ => Scalar.min ty
+
+def Scalar.cMax (ty : ScalarTy) : Int :=
+  match ty with
+  | .Isize => Scalar.max .I32
+  | .Usize => Scalar.max .U32
+  | _ => Scalar.max ty
+
+theorem Scalar.cMin_bound ty : Scalar.min ty ≤ Scalar.cMin ty := by
+  cases ty <;> simp [Scalar.min, Scalar.max, Scalar.cMin, Scalar.cMax] at *
+  have h := Isize.refined_min.property
+  cases h <;> simp [*, Isize.min]
+
+theorem Scalar.cMax_bound ty : Scalar.cMax ty ≤ Scalar.max ty := by
+  cases ty <;> simp [Scalar.min, Scalar.max, Scalar.cMin, Scalar.cMax] at *
+  . have h := Isize.refined_max.property
+    cases h <;> simp [*, Isize.max]
+  . have h := Usize.refined_max.property
+    cases h <;> simp [*, Usize.max]
+
+theorem Scalar.cMin_suffices ty (h : Scalar.cMin ty ≤ x) : Scalar.min ty ≤ x := by
+  have := Scalar.cMin_bound ty
+  linarith
+
+theorem Scalar.cMax_suffices ty (h : x ≤ Scalar.cMax ty) : x ≤ Scalar.max ty := by
+  have := Scalar.cMax_bound ty
+  linarith
+
+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 ->
+  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
+
+def Scalar.ofIntCore {ty : ScalarTy} (x : Int)
+  (hmin : Scalar.min ty ≤ x) (hmax : x ≤ Scalar.max ty) : Scalar ty :=
+  { val := x, hmin := hmin, hmax := hmax }
+
+-- Tactic to prove that integers are in bounds
+-- TODO: use this: https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/instance.20with.20tactic.20autoparam
+syntax "intlit" : tactic
+macro_rules
+  | `(tactic| intlit) => `(tactic| apply Scalar.bound_suffices; decide)
+
+def Scalar.ofInt {ty : ScalarTy} (x : Int)
+  (h : Scalar.min ty ≤ x ∧ x ≤ Scalar.max ty := by intlit) : Scalar ty :=
+  -- 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
+-- and
+-- 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) :=
+  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)
+
+def Scalar.div {ty : ScalarTy} (x : Scalar ty) (y : Scalar ty) : Result (Scalar ty) :=
+  if y.val != 0 then Scalar.tryMk ty (x.val / y.val) else fail divisionByZero
+
+-- Our custom remainder operation, which satisfies the semantics of Rust
+-- TODO: is there a better way?
+def scalar_rem (x y : Int) : Int :=
+  if 0 ≤ x then |x| % |y|
+  else - (|x| % |y|)
+
+-- Our custom division operation, which satisfies the semantics of Rust
+-- TODO: is there a better way?
+def scalar_div (x y : Int) : Int :=
+  if 0 ≤ x && 0 ≤ y then |x| / |y|
+  else if 0 ≤ x && y < 0 then - (|x| / |y|)
+  else if x < 0 && 0 ≤ y then - (|x| / |y|)
+  else |x| / |y|
+
+-- Checking that the remainder operation is correct
+#assert scalar_rem 1 2 = 1
+#assert scalar_rem (-1) 2 = -1
+#assert scalar_rem 1 (-2) = 1
+#assert scalar_rem (-1) (-2) = -1
+#assert scalar_rem 7 3 = (1:Int)
+#assert scalar_rem (-7) 3 = -1
+#assert scalar_rem 7 (-3) = 1
+#assert scalar_rem (-7) (-3) = -1
+
+-- Checking that the division operation is correct
+#assert scalar_div 3 2 = 1
+#assert scalar_div (-3) 2 = -1
+#assert scalar_div 3 (-2) = -1
+#assert scalar_div (-3) (-2) = 1
+#assert scalar_div 7 3 = 2
+#assert scalar_div (-7) 3 = -2
+#assert scalar_div 7 (-3) = -2
+#assert scalar_div (-7) (-3) = 2
+
+def Scalar.rem {ty : ScalarTy} (x : Scalar ty) (y : Scalar ty) : Result (Scalar ty) :=
+  if y.val != 0 then Scalar.tryMk ty (x.val % y.val) else fail divisionByZero
+
+def Scalar.add {ty : ScalarTy} (x : Scalar ty) (y : Scalar ty) : Result (Scalar ty) :=
+  Scalar.tryMk ty (x.val + y.val)
+
+def Scalar.sub {ty : ScalarTy} (x : Scalar ty) (y : Scalar ty) : Result (Scalar ty) :=
+  Scalar.tryMk ty (x.val - y.val)
+
+def Scalar.mul {ty : ScalarTy} (x : Scalar ty) (y : Scalar ty) : Result (Scalar ty) :=
+  Scalar.tryMk ty (x.val * y.val)
+
+-- TODO: instances of +, -, * etc. for scalars
+
+-- Cast an integer from a [src_ty] to a [tgt_ty]
+-- TODO: check the semantics of casts in Rust
+def Scalar.cast {src_ty : ScalarTy} (tgt_ty : ScalarTy) (x : Scalar src_ty) : Result (Scalar tgt_ty) :=
+  Scalar.tryMk tgt_ty x.val
+
+-- The scalar types
+-- We declare the definitions as reducible so that Lean can unfold them (useful
+-- for type class resolution for instance).
+@[reducible] def Isize := Scalar .Isize
+@[reducible] def I8    := Scalar .I8
+@[reducible] def I16   := Scalar .I16
+@[reducible] def I32   := Scalar .I32
+@[reducible] def I64   := Scalar .I64
+@[reducible] def I128  := Scalar .I128
+@[reducible] def Usize := Scalar .Usize
+@[reducible] def U8    := Scalar .U8
+@[reducible] def U16   := Scalar .U16
+@[reducible] def U32   := Scalar .U32
+@[reducible] def U64   := Scalar .U64
+@[reducible] def U128  := Scalar .U128
+
+-- TODO: below: not sure this is the best way.
+-- Should we rather overload operations like +, -, etc.?
+-- Also, it is possible to automate the generation of those definitions
+-- with macros (but would it be a good idea? It would be less easy to
+-- read the file, which is not supposed to change a lot)
+
+-- Negation
+
+/--
+Remark: there is no heterogeneous negation in the Lean prelude: we thus introduce
+one here.
+
+The notation typeclass for heterogeneous addition.
+This enables the notation `- a : β` where `a : α`.
+-/
+class HNeg (α : Type u) (β : outParam (Type v)) where
+  /-- `- a` computes the negation of `a`.
+  The meaning of this notation is type-dependent. -/
+  hNeg : α → β
+
+prefix:75  "-"   => HNeg.hNeg
+
+instance : HNeg Isize (Result Isize) where hNeg x := Scalar.neg x
+instance : HNeg I8 (Result I8) where hNeg x := Scalar.neg x
+instance : HNeg I16 (Result I16) where hNeg x := Scalar.neg x
+instance : HNeg I32 (Result I32) where hNeg x := Scalar.neg x
+instance : HNeg I64 (Result I64) where hNeg x := Scalar.neg x
+instance : HNeg I128 (Result I128) where hNeg x := Scalar.neg x
+
+-- Addition
+instance {ty} : HAdd (Scalar ty) (Scalar ty) (Result (Scalar ty)) where
+  hAdd x y := Scalar.add x y
+
+-- Substraction
+instance {ty} : HSub (Scalar ty) (Scalar ty) (Result (Scalar ty)) where
+  hSub x y := Scalar.sub x y
+
+-- Multiplication
+instance {ty} : HMul (Scalar ty) (Scalar ty) (Result (Scalar ty)) where
+  hMul x y := Scalar.mul x y
+
+-- Division
+instance {ty} : HDiv (Scalar ty) (Scalar ty) (Result (Scalar ty)) where
+  hDiv x y := Scalar.div x y
+
+-- Remainder
+instance {ty} : HMod (Scalar ty) (Scalar ty) (Result (Scalar ty)) where
+  hMod x y := Scalar.rem x y
+
+-- ofIntCore
+-- TODO: typeclass?
+def Isize.ofIntCore := @Scalar.ofIntCore .Isize
+def I8.ofIntCore    := @Scalar.ofIntCore .I8
+def I16.ofIntCore   := @Scalar.ofIntCore .I16
+def I32.ofIntCore   := @Scalar.ofIntCore .I32
+def I64.ofIntCore   := @Scalar.ofIntCore .I64
+def I128.ofIntCore  := @Scalar.ofIntCore .I128
+def Usize.ofIntCore := @Scalar.ofIntCore .Usize
+def U8.ofIntCore    := @Scalar.ofIntCore .U8
+def U16.ofIntCore   := @Scalar.ofIntCore .U16
+def U32.ofIntCore   := @Scalar.ofIntCore .U32
+def U64.ofIntCore   := @Scalar.ofIntCore .U64
+def U128.ofIntCore  := @Scalar.ofIntCore .U128
+
+--  ofInt
+-- TODO: typeclass?
+def Isize.ofInt := @Scalar.ofInt .Isize
+def I8.ofInt    := @Scalar.ofInt .I8
+def I16.ofInt   := @Scalar.ofInt .I16
+def I32.ofInt   := @Scalar.ofInt .I32
+def I64.ofInt   := @Scalar.ofInt .I64
+def I128.ofInt  := @Scalar.ofInt .I128
+def Usize.ofInt := @Scalar.ofInt .Usize
+def U8.ofInt    := @Scalar.ofInt .U8
+def U16.ofInt   := @Scalar.ofInt .U16
+def U32.ofInt   := @Scalar.ofInt .U32
+def U64.ofInt   := @Scalar.ofInt .U64
+def U128.ofInt  := @Scalar.ofInt .U128
+
+-- Comparisons
+instance {ty} : LT (Scalar ty) where
+  lt a b := LT.lt a.val b.val
+
+instance {ty} : LE (Scalar ty) where le a b := LE.le a.val b.val
+
+instance Scalar.decLt {ty} (a b : Scalar ty) : Decidable (LT.lt a b) := Int.decLt ..
+instance Scalar.decLe {ty} (a b : Scalar ty) : Decidable (LE.le a b) := Int.decLe ..
+
+theorem Scalar.eq_of_val_eq {ty} : ∀ {i j : Scalar ty}, Eq i.val j.val → Eq i j
+  | ⟨_, _, _⟩, ⟨_, _, _⟩, rfl => rfl
+
+theorem Scalar.val_eq_of_eq {ty} {i j : Scalar ty} (h : Eq i j) : Eq i.val j.val :=
+  h ▸ rfl
+
+theorem Scalar.ne_of_val_ne {ty} {i j : Scalar ty} (h : Not (Eq i.val j.val)) : Not (Eq i j) :=
+  fun h' => absurd (val_eq_of_eq h') h
+
+instance (ty : ScalarTy) : DecidableEq (Scalar ty) :=
+  fun i j =>
+    match decEq i.val j.val with
+    | isTrue h  => isTrue (Scalar.eq_of_val_eq h)
+    | isFalse h => isFalse (Scalar.ne_of_val_ne h)
+
+/- Remark: we can't write the following instance because of restrictions about
+   the type class parameters (`ty` doesn't appear in the return type, which is
+   forbidden):
+
+   ```
+   instance Scalar.cast (ty : ScalarTy) : Coe (Scalar ty) Int where coe := λ v => v.val
+   ```
+ -/
+def Scalar.toInt {ty} (n : Scalar ty) : Int := n.val
+
+-- -- We now define a type class that subsumes the various machine integer types, so
+-- -- as to write a concise definition for scalar_cast, rather than exhaustively
+-- -- enumerating all of the possible pairs. We remark that Rust has sane semantics
+-- -- and fails if a cast operation would involve a truncation or modulo.
+
+-- class MachineInteger (t: Type) where
+--   size: Nat
+--   val: t -> Fin size
+--   ofNatCore: (n:Nat) -> LT.lt n size -> t
+
+-- set_option hygiene false in
+-- run_cmd
+--   for typeName in [`UInt8, `UInt16, `UInt32, `UInt64, `USize].map Lean.mkIdent do
+--   Lean.Elab.Command.elabCommand (← `(
+--     namespace $typeName
+--     instance: MachineInteger $typeName where
+--       size := size
+--       val := val
+--       ofNatCore := ofNatCore
+--     end $typeName
+--   ))
+
+-- -- Aeneas only instantiates the destination type (`src` is implicit). We rely on
+-- -- Lean to infer `src`.
+
+-- def scalar_cast { src: Type } (dst: Type) [ MachineInteger src ] [ MachineInteger dst ] (x: src): Result dst :=
+--   if h: MachineInteger.val x < MachineInteger.size dst then
+--     .ret (MachineInteger.ofNatCore (MachineInteger.val x).val h)
+--   else
+--     .fail integerOverflow
+
+end Primitives
diff --git a/backends/lean/Base/Primitives/Vec.lean b/backends/lean/Base/Primitives/Vec.lean
new file mode 100644
index 00000000..7851a232
--- /dev/null
+++ b/backends/lean/Base/Primitives/Vec.lean
@@ -0,0 +1,113 @@
+import Lean
+import Lean.Meta.Tactic.Simp
+import Init.Data.List.Basic
+import Mathlib.Tactic.RunCmd
+import Mathlib.Tactic.Linarith
+import Base.IList
+import Base.Primitives.Scalar
+import Base.Arith
+
+namespace Primitives
+
+open Result Error
+
+-------------
+-- VECTORS --
+-------------
+
+def Vec (α : Type u) := { l : List α // List.length l ≤ Usize.max }
+
+-- TODO: do we really need it? It should be with Subtype by default
+instance Vec.cast (a : Type): Coe (Vec a) (List a)  where coe := λ v => v.val
+
+instance (a : Type) : Arith.HasIntProp (Vec a) where
+  prop_ty := λ v => v.val.length ≤ Scalar.max ScalarTy.Usize
+  prop := λ ⟨ _, l ⟩ => l
+
+example {a: Type} (v : Vec a) : v.val.length ≤ Scalar.max ScalarTy.Usize := by
+  intro_has_int_prop_instances
+  simp_all [Scalar.max, Scalar.min]
+
+example {a: Type} (v : Vec a) : v.val.length ≤ Scalar.max ScalarTy.Usize := by
+  scalar_tac
+
+def Vec.new (α : Type u): Vec α := ⟨ [], by apply Scalar.cMax_suffices .Usize; simp ⟩
+
+def Vec.len (α : Type u) (v : Vec α) : Usize :=
+  let ⟨ v, l ⟩ := v
+  Usize.ofIntCore (List.length v) (by simp [Scalar.min, Usize.min]) l
+
+def Vec.length {α : Type u} (v : Vec α) : Int := v.val.len
+
+-- This shouldn't be used
+def Vec.push_fwd (α : Type u) (_ : Vec α) (_ : α) : Unit := ()
+
+-- This is actually the backward function
+def Vec.push (α : Type u) (v : Vec α) (x : α) : Result (Vec α)
+  :=
+  let nlen := List.length v.val + 1
+  if h : nlen ≤ U32.max || nlen ≤ Usize.max then
+    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
+    return ⟨ List.concat v.val x, by simp at *; assumption ⟩
+  else
+    fail maximumSizeExceeded
+
+-- This shouldn't be used
+def Vec.insert_fwd (α : Type u) (v: Vec α) (i: Usize) (_: α): Result Unit :=
+  if i.val < List.length v.val then
+    .ret ()
+  else
+    .fail arrayOutOfBounds
+
+-- This is actually the backward function
+def Vec.insert (α : Type u) (v: Vec α) (i: Usize) (x: α): Result (Vec α) :=
+  if i.val < List.length v.val then
+    -- TODO: maybe we should redefine a list library which uses integers
+    -- (instead of natural numbers)
+    .ret ⟨ v.val.update i.val x, by have := v.property; simp [*] ⟩
+  else
+    .fail arrayOutOfBounds
+
+-- TODO: remove
+def Vec.index_to_fin {α : Type u} {v: Vec α} {i: Usize} (h : i.val < List.length v.val) :
+  Fin (List.length v.val) :=
+  let j := i.val.toNat
+  let h: j < List.length v.val := by
+    have heq := @Int.toNat_lt (List.length v.val) i.val i.hmin
+    apply heq.mpr
+    assumption
+  ⟨j, h⟩
+
+def Vec.index (α : Type u) (v: Vec α) (i: Usize): Result α :=
+  match v.val.indexOpt i.val with
+  | none => fail .arrayOutOfBounds
+  | some x => ret x
+
+-- This shouldn't be used
+def Vec.index_back (α : Type u) (v: Vec α) (i: Usize) (_: α): Result Unit :=
+  if i.val < List.length v.val then
+    .ret ()
+  else
+    .fail arrayOutOfBounds
+
+def Vec.index_mut (α : Type u) (v: Vec α) (i: Usize): Result α :=
+  if h: i.val < List.length v.val then
+    let i := Vec.index_to_fin h
+    .ret (List.get v.val i)
+  else
+    .fail arrayOutOfBounds
+
+def Vec.index_mut_back (α : Type u) (v: Vec α) (i: Usize) (x: α): Result (Vec α) :=
+  if h: i.val < List.length v.val then
+    let i := Vec.index_to_fin h
+    .ret ⟨ List.set v.val i x, by
+      have h: List.length v.val ≤ Usize.max := v.property
+      simp [*] at *
+    ⟩
+  else
+    .fail arrayOutOfBounds
+
+end Primitives
-- 
cgit v1.3.1


From 2fa3cb8ee04dd7ff4184e3e1000fdc025abc50a4 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Mon, 17 Jul 2023 23:37:48 +0200
Subject: Start proving theorems for primitive definitions

---
 backends/lean/Base/Diverge/Base.lean      |  3 +-
 backends/lean/Base/IList/IList.lean       | 66 ++++++++++++++++++-----
 backends/lean/Base/Primitives/Scalar.lean |  1 +
 backends/lean/Base/Primitives/Vec.lean    | 89 +++++++++++++++++++------------
 backends/lean/Base/Progress/Base.lean     |  3 +-
 backends/lean/Base/Progress/Progress.lean |  4 ++
 6 files changed, 116 insertions(+), 50 deletions(-)

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

diff --git a/backends/lean/Base/Diverge/Base.lean b/backends/lean/Base/Diverge/Base.lean
index 0a9ea4c4..4ff1d923 100644
--- a/backends/lean/Base/Diverge/Base.lean
+++ b/backends/lean/Base/Diverge/Base.lean
@@ -3,8 +3,7 @@ import Lean.Meta.Tactic.Simp
 import Init.Data.List.Basic
 import Mathlib.Tactic.RunCmd
 import Mathlib.Tactic.Linarith
-
-import Base.Primitives
+import Base.Primitives.Base
 
 /- TODO: this is very useful, but is there more? -/
 set_option profiler true
diff --git a/backends/lean/Base/IList/IList.lean b/backends/lean/Base/IList/IList.lean
index 2a335cac..ddb10236 100644
--- a/backends/lean/Base/IList/IList.lean
+++ b/backends/lean/Base/IList/IList.lean
@@ -11,12 +11,27 @@ def len (ls : List α) : Int :=
   | [] => 0
   | _ :: tl => 1 + len tl
 
+@[simp] theorem len_nil : len ([] : List α) = 0 := by simp [len]
+@[simp] theorem len_cons : len ((x :: tl) : List α) = 1 + len tl := by simp [len]
+
+theorem len_pos : 0 ≤ (ls : List α).len := by
+  induction ls <;> simp [*]
+  linarith
+
+instance (a : Type u) : Arith.HasIntProp (List a) where
+  prop_ty := λ ls => 0 ≤ ls.len
+  prop := λ ls => ls.len_pos
+
 -- Remark: if i < 0, then the result is none
 def indexOpt (ls : List α) (i : Int) : Option α :=
   match ls with
   | [] => none
   | hd :: tl => if i = 0 then some hd else indexOpt tl (i - 1)
 
+@[simp] theorem indexOpt_nil : indexOpt ([] : List α) i = none := by simp [indexOpt]
+@[simp] theorem indexOpt_zero_cons : indexOpt ((x :: tl) : List α) 0 = some x := by simp [indexOpt]
+@[simp] theorem indexOpt_nzero_cons (hne : i ≠ 0) : indexOpt ((x :: tl) : List α) i = indexOpt tl (i - 1) := by simp [*, indexOpt]
+
 -- Remark: if i < 0, then the result is the defaul element
 def index [Inhabited α] (ls : List α) (i : Int) : α :=
   match ls with
@@ -24,6 +39,43 @@ def index [Inhabited α] (ls : List α) (i : Int) : α :=
   | x :: tl =>
     if i = 0 then x else index tl (i - 1)
 
+@[simp] theorem index_zero_cons [Inhabited α] : index ((x :: tl) : List α) 0 = x := by simp [index]
+@[simp] theorem index_nzero_cons [Inhabited α] (hne : i ≠ 0) : index ((x :: tl) : List α) i = index tl (i - 1) := by simp [*, index]
+
+theorem indexOpt_bounds (ls : List α) (i : Int) :
+  ls.indexOpt i = none ↔ i < 0 ∨ ls.len ≤ i :=
+  match ls with
+  | [] =>
+    have : ¬ (i < 0) → 0 ≤ i := by intro; linarith -- TODO: simplify (we could boost int_tac)
+    by simp; tauto
+  | _ :: tl =>
+    have := indexOpt_bounds tl (i - 1)
+    if h: i = 0 then
+      by
+        simp [*];
+        -- TODO: int_tac/scalar_tac should also explore the goal!
+        have := tl.len_pos
+        linarith
+    else by
+      simp [*]
+      constructor <;> intros <;>
+      -- TODO: tactic to split all disjunctions
+      rename_i hor <;> cases hor <;>
+      first | left; int_tac | right; int_tac
+
+theorem indexOpt_eq_index [Inhabited α] (ls : List α) (i : Int) :
+  0 ≤ i →
+  i < ls.len →
+  ls.indexOpt i = some (ls.index i) :=
+  match ls with
+  | [] => by simp; intros; linarith
+  | hd :: tl =>
+    if h: i = 0 then
+      by simp [*]
+    else
+      have hi := indexOpt_eq_index tl (i - 1)
+      by simp [*]; intros;  apply hi <;> int_tac
+
 -- Remark: the list is unchanged if the index is not in bounds (in particular
 -- if it is < 0)
 def update (ls : List α) (i : Int) (y : α) : List α :=
@@ -42,12 +94,6 @@ section Lemmas
 
 variable {α : Type u} 
 
-@[simp] theorem len_nil : len ([] : List α) = 0 := by simp [len]
-@[simp] theorem len_cons : len ((x :: tl) : List α) = 1 + len tl := by simp [len]
-
-@[simp] theorem index_zero_cons [Inhabited α] : index ((x :: tl) : List α) 0 = x := by simp [index]
-@[simp] theorem index_nzero_cons [Inhabited α] (hne : i ≠ 0) : index ((x :: tl) : List α) i = index tl (i - 1) := by simp [*, index]
-
 @[simp] theorem update_nil : update ([] : List α) i y = [] := by simp [update]
 @[simp] theorem update_zero_cons : update ((x :: tl) : List α) 0 y = y :: tl := by simp [update]
 @[simp] theorem update_nzero_cons (hne : i ≠ 0) : update ((x :: tl) : List α) i y = x :: update tl (i - 1) y := by simp [*, update]
@@ -81,14 +127,6 @@ theorem len_update (ls : List α) (i : Int) (x : α) : (ls.update i x).len = ls.
   simp [len_eq_length]
 
 
-theorem len_pos : 0 ≤ (ls : List α).len := by
-  induction ls <;> simp [*]
-  linarith
-
-instance (a : Type u) : Arith.HasIntProp (List a) where
-  prop_ty := λ ls => 0 ≤ ls.len
-  prop := λ ls => ls.len_pos
-
 theorem left_length_eq_append_eq (l1 l2 l1' l2' : List α) (heq : l1.length = l1'.length) :
   l1 ++ l2 = l1' ++ l2' ↔ l1 = l1' ∧ l2 = l2' := by
   revert l1'
diff --git a/backends/lean/Base/Primitives/Scalar.lean b/backends/lean/Base/Primitives/Scalar.lean
index 241dfa07..3f88caa2 100644
--- a/backends/lean/Base/Primitives/Scalar.lean
+++ b/backends/lean/Base/Primitives/Scalar.lean
@@ -2,6 +2,7 @@ import Lean
 import Lean.Meta.Tactic.Simp
 import Mathlib.Tactic.Linarith
 import Base.Primitives.Base
+import Base.Diverge.Base
 
 namespace Primitives
 
diff --git a/backends/lean/Base/Primitives/Vec.lean b/backends/lean/Base/Primitives/Vec.lean
index 7851a232..4ecfa28f 100644
--- a/backends/lean/Base/Primitives/Vec.lean
+++ b/backends/lean/Base/Primitives/Vec.lean
@@ -6,6 +6,7 @@ import Mathlib.Tactic.Linarith
 import Base.IList
 import Base.Primitives.Scalar
 import Base.Arith
+import Base.Progress.Base
 
 namespace Primitives
 
@@ -56,58 +57,80 @@ def Vec.push (α : Type u) (v : Vec α) (x : α) : Result (Vec α)
     fail maximumSizeExceeded
 
 -- This shouldn't be used
-def Vec.insert_fwd (α : Type u) (v: Vec α) (i: Usize) (_: α): Result Unit :=
-  if i.val < List.length v.val then
+def Vec.insert_fwd (α : Type u) (v: Vec α) (i: Usize) (_: α) : Result Unit :=
+  if i.val < v.length then
     .ret ()
   else
     .fail arrayOutOfBounds
 
 -- This is actually the backward function
-def Vec.insert (α : Type u) (v: Vec α) (i: Usize) (x: α): Result (Vec α) :=
-  if i.val < List.length v.val then
-    -- TODO: maybe we should redefine a list library which uses integers
-    -- (instead of natural numbers)
+def Vec.insert (α : Type u) (v: Vec α) (i: Usize) (x: α) : Result (Vec α) :=
+  if i.val < v.length then
     .ret ⟨ v.val.update i.val x, by have := v.property; simp [*] ⟩
   else
     .fail arrayOutOfBounds
 
--- TODO: remove
-def Vec.index_to_fin {α : Type u} {v: Vec α} {i: Usize} (h : i.val < List.length v.val) :
-  Fin (List.length v.val) :=
-  let j := i.val.toNat
-  let h: j < List.length v.val := by
-    have heq := @Int.toNat_lt (List.length v.val) i.val i.hmin
-    apply heq.mpr
-    assumption
-  ⟨j, h⟩
-
-def Vec.index (α : Type u) (v: Vec α) (i: Usize): Result α :=
+@[pspec]
+theorem Vec.insert_spec {α : Type u} (v: Vec α) (i: Usize) (x: α) :
+  i.val < v.length →
+  ∃ nv, v.insert α i x = ret nv ∧ nv.val = v.val.update i.val x := by
+  intro h
+  simp [insert, *]
+
+def Vec.index (α : Type u) (v: Vec α) (i: Usize) : Result α :=
   match v.val.indexOpt i.val with
   | none => fail .arrayOutOfBounds
   | some x => ret x
 
+@[pspec]
+theorem Vec.index_spec {α : Type u} [Inhabited α] (v: Vec α) (i: Usize) :
+  i.val < v.length →
+  v.index α i = ret (v.val.index i.val) := by
+  intro
+  simp only [index]
+  -- TODO: dependent rewrite
+  have h := List.indexOpt_eq_index v.val i.val (by scalar_tac) (by simp[length] at *; simp [*])
+  simp only [*]
+
 -- This shouldn't be used
-def Vec.index_back (α : Type u) (v: Vec α) (i: Usize) (_: α): Result Unit :=
+def Vec.index_back (α : Type u) (v: Vec α) (i: Usize) (_: α) : Result Unit :=
   if i.val < List.length v.val then
     .ret ()
   else
     .fail arrayOutOfBounds
 
-def Vec.index_mut (α : Type u) (v: Vec α) (i: Usize): Result α :=
-  if h: i.val < List.length v.val then
-    let i := Vec.index_to_fin h
-    .ret (List.get v.val i)
-  else
-    .fail arrayOutOfBounds
+def Vec.index_mut (α : Type u) (v: Vec α) (i: Usize) : Result α :=
+  match v.val.indexOpt i.val with
+  | none => fail .arrayOutOfBounds
+  | some x => ret x
 
-def Vec.index_mut_back (α : Type u) (v: Vec α) (i: Usize) (x: α): Result (Vec α) :=
-  if h: i.val < List.length v.val then
-    let i := Vec.index_to_fin h
-    .ret ⟨ List.set v.val i x, by
-      have h: List.length v.val ≤ Usize.max := v.property
-      simp [*] at *
-    ⟩
-  else
-    .fail arrayOutOfBounds
+@[pspec]
+theorem Vec.index_mut_spec {α : Type u} [Inhabited α] (v: Vec α) (i: Usize) :
+  i.val < v.length →
+  v.index_mut α i = ret (v.val.index i.val) := by
+  intro
+  simp only [index_mut]
+  -- TODO: dependent rewrite
+  have h := List.indexOpt_eq_index v.val i.val (by scalar_tac) (by simp[length] at *; simp [*])
+  simp only [*]
+
+def Vec.index_mut_back (α : Type u) (v: Vec α) (i: Usize) (x: α) : Result (Vec α) :=
+  match v.val.indexOpt i.val with
+  | none => fail .arrayOutOfBounds
+  | some _ =>
+    .ret ⟨ v.val.update i.val x, by have := v.property; simp [*] ⟩
+
+@[pspec]
+theorem Vec.index_mut_back_spec {α : Type u} (v: Vec α) (i: Usize) (x : α) :
+  i.val < v.length →
+  ∃ nv, v.index_mut_back α i x = ret nv ∧
+  nv.val = v.val.update i.val x
+  := by
+  intro
+  simp only [index_mut_back]
+  have h := List.indexOpt_bounds v.val i.val
+  split
+  . simp_all [length]; cases h <;> scalar_tac
+  . simp_all
 
 end Primitives
diff --git a/backends/lean/Base/Progress/Base.lean b/backends/lean/Base/Progress/Base.lean
index a288d889..00b0a478 100644
--- a/backends/lean/Base/Progress/Base.lean
+++ b/backends/lean/Base/Progress/Base.lean
@@ -1,6 +1,7 @@
 import Lean
+import Std.Lean.HashSet
 import Base.Utils
-import Base.Primitives
+import Base.Primitives.Base
 
 namespace Progress
 
diff --git a/backends/lean/Base/Progress/Progress.lean b/backends/lean/Base/Progress/Progress.lean
index af7b426a..001967e5 100644
--- a/backends/lean/Base/Progress/Progress.lean
+++ b/backends/lean/Base/Progress/Progress.lean
@@ -7,6 +7,7 @@ namespace Progress
 open Lean Elab Term Meta Tactic
 open Utils
 
+/-
 -- TODO: remove
 namespace Test
   open Primitives
@@ -20,6 +21,7 @@ namespace Test
 
   #eval pspecAttr.find? ``Primitives.Vec.index
 end Test
+-/
 
 inductive TheoremOrLocal where
 | Theorem (thName : Name)
@@ -200,6 +202,7 @@ def evalProgress (args : TSyntax `Progress.progressArgs) : TacticM Unit := do
 elab "progress" args:progressArgs : tactic =>
   evalProgress args
 
+/-
 -- TODO: remove
 namespace Test
   open Primitives
@@ -215,5 +218,6 @@ namespace Test
   set_option trace.Progress false
 
 end Test
+-/
 
 end Progress
-- 
cgit v1.3.1


From 0f430c055c3a531ceab83635adc5df92f0015c6e Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Tue, 18 Jul 2023 16:55:27 +0200
Subject: Make modifications to Vec.lean

---
 backends/lean/Base/Primitives/Vec.lean | 8 +++++---
 1 file changed, 5 insertions(+), 3 deletions(-)

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

diff --git a/backends/lean/Base/Primitives/Vec.lean b/backends/lean/Base/Primitives/Vec.lean
index 4ecfa28f..be3a0e5b 100644
--- a/backends/lean/Base/Primitives/Vec.lean
+++ b/backends/lean/Base/Primitives/Vec.lean
@@ -38,7 +38,8 @@ def Vec.len (α : Type u) (v : Vec α) : Usize :=
   let ⟨ v, l ⟩ := v
   Usize.ofIntCore (List.length v) (by simp [Scalar.min, Usize.min]) l
 
-def Vec.length {α : Type u} (v : Vec α) : Int := v.val.len
+@[simp]
+abbrev Vec.length {α : Type u} (v : Vec α) : Int := v.val.len
 
 -- This shouldn't be used
 def Vec.push_fwd (α : Type u) (_ : Vec α) (_ : α) : Unit := ()
@@ -89,7 +90,7 @@ theorem Vec.index_spec {α : Type u} [Inhabited α] (v: Vec α) (i: Usize) :
   intro
   simp only [index]
   -- TODO: dependent rewrite
-  have h := List.indexOpt_eq_index v.val i.val (by scalar_tac) (by simp[length] at *; simp [*])
+  have h := List.indexOpt_eq_index v.val i.val (by scalar_tac) (by simp [*])
   simp only [*]
 
 -- This shouldn't be used
@@ -111,13 +112,14 @@ theorem Vec.index_mut_spec {α : Type u} [Inhabited α] (v: Vec α) (i: Usize) :
   intro
   simp only [index_mut]
   -- TODO: dependent rewrite
-  have h := List.indexOpt_eq_index v.val i.val (by scalar_tac) (by simp[length] at *; simp [*])
+  have h := List.indexOpt_eq_index v.val i.val (by scalar_tac) (by simp [*])
   simp only [*]
 
 def Vec.index_mut_back (α : Type u) (v: Vec α) (i: Usize) (x: α) : Result (Vec α) :=
   match v.val.indexOpt i.val with
   | none => fail .arrayOutOfBounds
   | some _ =>
+    -- TODO: int_tac: introduce the refinements in the context?
     .ret ⟨ v.val.update i.val x, by have := v.property; simp [*] ⟩
 
 @[pspec]
-- 
cgit v1.3.1


From 3df0b36891975935c3d8035f56389ee6bbcbf251 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Wed, 19 Jul 2023 18:13:31 +0200
Subject: Add arithmetic spec lemmas

---
 backends/lean/Base/Primitives/Scalar.lean | 167 ++++++++++++++++++++++++++++--
 1 file changed, 161 insertions(+), 6 deletions(-)

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

diff --git a/backends/lean/Base/Primitives/Scalar.lean b/backends/lean/Base/Primitives/Scalar.lean
index 3f88caa2..aaa4027f 100644
--- a/backends/lean/Base/Primitives/Scalar.lean
+++ b/backends/lean/Base/Primitives/Scalar.lean
@@ -3,6 +3,8 @@ import Lean.Meta.Tactic.Simp
 import Mathlib.Tactic.Linarith
 import Base.Primitives.Base
 import Base.Diverge.Base
+import Base.Progress.Base
+import Base.Arith.Int
 
 namespace Primitives
 
@@ -122,6 +124,22 @@ inductive ScalarTy :=
 | U64
 | U128
 
+def ScalarTy.isSigned (ty : ScalarTy) : Bool :=
+  match ty with
+  | Isize
+  | I8
+  | I16
+  | I32
+  | I64
+  | I128 => true
+  | Usize
+  | U8
+  | U16
+  | U32
+  | U64
+  | U128 => false
+
+
 def Scalar.smin (ty : ScalarTy) : Int :=
   match ty with
   | .Isize => Isize.smin
@@ -289,23 +307,30 @@ def Scalar.tryMk (ty : ScalarTy) (x : Int) : Result (Scalar ty) :=
 
 def Scalar.neg {ty : ScalarTy} (x : Scalar ty) : Result (Scalar ty) := Scalar.tryMk ty (- x.val)
 
-def Scalar.div {ty : ScalarTy} (x : Scalar ty) (y : Scalar ty) : Result (Scalar ty) :=
-  if y.val != 0 then Scalar.tryMk ty (x.val / y.val) else fail divisionByZero
-
 -- Our custom remainder operation, which satisfies the semantics of Rust
 -- TODO: is there a better way?
 def scalar_rem (x y : Int) : Int :=
-  if 0 ≤ x then |x| % |y|
+  if 0 ≤ x then x % y
   else - (|x| % |y|)
 
+@[simp]
+def scalar_rem_nonneg {x y : Int} (hx : 0 ≤ x) : scalar_rem x y = x % y := by
+  intros
+  simp [*, scalar_rem]
+
 -- Our custom division operation, which satisfies the semantics of Rust
 -- TODO: is there a better way?
 def scalar_div (x y : Int) : Int :=
-  if 0 ≤ x && 0 ≤ y then |x| / |y|
+  if 0 ≤ x && 0 ≤ y then x / y
   else if 0 ≤ x && y < 0 then - (|x| / |y|)
   else if x < 0 && 0 ≤ y then - (|x| / |y|)
   else |x| / |y|
 
+@[simp]
+def scalar_div_nonneg {x y : Int} (hx : 0 ≤ x) (hy : 0 ≤ y) : scalar_div x y = x / y := by
+  intros
+  simp [*, scalar_div]
+
 -- Checking that the remainder operation is correct
 #assert scalar_rem 1 2 = 1
 #assert scalar_rem (-1) 2 = -1
@@ -326,8 +351,11 @@ def scalar_div (x y : Int) : Int :=
 #assert scalar_div 7 (-3) = -2
 #assert scalar_div (-7) (-3) = 2
 
+def Scalar.div {ty : ScalarTy} (x : Scalar ty) (y : Scalar ty) : Result (Scalar ty) :=
+  if y.val != 0 then Scalar.tryMk ty (scalar_div x.val y.val) else fail divisionByZero
+
 def Scalar.rem {ty : ScalarTy} (x : Scalar ty) (y : Scalar ty) : Result (Scalar ty) :=
-  if y.val != 0 then Scalar.tryMk ty (x.val % y.val) else fail divisionByZero
+  if y.val != 0 then Scalar.tryMk ty (scalar_rem x.val y.val) else fail divisionByZero
 
 def Scalar.add {ty : ScalarTy} (x : Scalar ty) (y : Scalar ty) : Result (Scalar ty) :=
   Scalar.tryMk ty (x.val + y.val)
@@ -410,6 +438,133 @@ instance {ty} : HDiv (Scalar ty) (Scalar ty) (Result (Scalar ty)) where
 instance {ty} : HMod (Scalar ty) (Scalar ty) (Result (Scalar ty)) where
   hMod x y := Scalar.rem x y
 
+-- TODO: make progress work at a more fine grained level (see `Scalar.add_unsigned_spec`)
+@[cpspec]
+theorem Scalar.add_spec {ty} {x y : Scalar ty}
+  (hmin : Scalar.min ty ≤ x.val + y.val)
+  (hmax : x.val + y.val ≤ Scalar.max ty) :
+  ∃ z, x + y = ret z ∧ z.val = x.val + y.val := by
+  simp [HAdd.hAdd, add, Add.add]
+  simp [tryMk]
+  split
+  . simp [pure]
+    rfl
+  . tauto
+
+theorem Scalar.add_unsigned_spec {ty} (s: ¬ ty.isSigned) {x y : Scalar ty}
+  (hmax : x.val + y.val ≤ Scalar.max ty) :
+  ∃ z, x + y = ret z ∧ z.val = x.val + y.val := by
+  have hmin : Scalar.min ty ≤ x.val + y.val := by
+    have hx := x.hmin
+    have hy := y.hmin
+    cases ty <;> simp [min] at * <;> linarith
+  apply add_spec <;> assumption
+
+-- TODO: make it finer grained
+@[cpspec]
+theorem Scalar.sub_spec {ty} {x y : Scalar ty}
+  (hmin : Scalar.min ty ≤ x.val - y.val)
+  (hmax : x.val - y.val ≤ Scalar.max ty) :
+  ∃ z, x - y = ret z ∧ z.val = x.val - y.val := by
+  simp [HSub.hSub, sub, Sub.sub]
+  simp [tryMk]
+  split
+  . simp [pure]
+    rfl
+  . tauto
+
+theorem Scalar.sub_unsigned_spec {ty} (s: ¬ ty.isSigned) {x y : Scalar ty}
+  (hmin : Scalar.min ty ≤ x.val - y.val) :
+  ∃ z, x - y = ret z ∧ z.val = x.val - y.val := by
+  have : x.val - y.val ≤ Scalar.max ty := by
+    have hx := x.hmin
+    have hxm := x.hmax
+    have hy := y.hmin
+    cases ty <;> simp [min, max] at * <;> linarith
+  intros
+  apply sub_spec <;> assumption
+
+-- TODO: make it finer grained
+@[cpspec]
+theorem Scalar.mul_spec {ty} {x y : Scalar ty}
+  (hmin : Scalar.min ty ≤ x.val * y.val)
+  (hmax : x.val * y.val ≤ Scalar.max ty) :
+  ∃ z, x * y = ret z ∧ z.val = x.val * y.val := by
+  simp [HMul.hMul, mul, Mul.mul]
+  simp [tryMk]
+  split
+  . simp [pure]
+    rfl
+  . tauto
+
+theorem Scalar.mul_unsigned_spec {ty} (s: ¬ ty.isSigned) {x y : Scalar ty}
+  (hmax : x.val * y.val ≤ Scalar.max ty) :
+  ∃ z, x * y = ret z ∧ z.val = x.val * y.val := by
+  have : Scalar.min ty ≤ x.val * y.val := by
+    have hx := x.hmin
+    have hy := y.hmin
+    cases ty <;> simp at * <;> apply mul_nonneg hx hy
+  apply mul_spec <;> assumption
+
+-- TODO: make it finer grained
+@[cpspec]
+theorem Scalar.div_spec {ty} {x y : Scalar ty}
+  (hnz : y.val ≠ 0)
+  (hmin : Scalar.min ty ≤ scalar_div x.val y.val)
+  (hmax : scalar_div x.val y.val ≤ Scalar.max ty) :
+  ∃ z, x / y = ret z ∧ z.val = scalar_div x.val y.val := by
+  simp [HDiv.hDiv, div, Div.div]
+  simp [tryMk, *]
+  simp [pure]
+  rfl
+
+theorem Scalar.div_unsigned_spec {ty} (s: ¬ ty.isSigned) (x : Scalar ty) {y : Scalar ty}
+  (hnz : y.val ≠ 0) :
+  ∃ z, x / y = ret z ∧ z.val = x.val / y.val := by
+  have h : Scalar.min ty = 0 := by cases ty <;> simp at *
+  have hx := x.hmin
+  have hy := y.hmin
+  simp [h] at hx hy
+  have hmin : 0 ≤ x.val / y.val := Int.ediv_nonneg hx hy
+  have hmax : x.val / y.val ≤ Scalar.max ty := by
+    have := Int.ediv_le_self y.val hx
+    have := x.hmax
+    linarith
+  have hs := @div_spec ty x y hnz
+  simp [*] at hs
+  apply hs
+
+-- TODO: make it finer grained
+@[cpspec]
+theorem Scalar.rem_spec {ty} {x y : Scalar ty}
+  (hnz : y.val ≠ 0)
+  (hmin : Scalar.min ty ≤ scalar_rem x.val y.val)
+  (hmax : scalar_rem x.val y.val ≤ Scalar.max ty) :
+  ∃ z, x % y = ret z ∧ z.val = scalar_rem x.val y.val := by
+  simp [HMod.hMod, rem]
+  simp [tryMk, *]
+  simp [pure]
+  rfl
+
+theorem Scalar.rem_unsigned_spec {ty} (s: ¬ ty.isSigned) (x : Scalar ty) {y : Scalar ty}
+  (hnz : y.val ≠ 0) :
+  ∃ z, x % y = ret z ∧ z.val = scalar_rem x.val y.val := by
+  have h : Scalar.min ty = 0 := by cases ty <;> simp at *
+  have hx := x.hmin
+  have hy := y.hmin
+  simp [h] at hx hy
+  have hmin : 0 ≤ x.val % y.val := Int.emod_nonneg x.val hnz
+  have hmax : x.val % y.val ≤ Scalar.max ty := by
+    have h := @Int.ediv_emod_unique x.val y.val (x.val % y.val) (x.val / y.val)
+    simp at h
+    have : 0 < y.val := by int_tac
+    simp [*] at h
+    have := y.hmax
+    linarith
+  have hs := @rem_spec ty x y hnz
+  simp [*] at hs
+  simp [*]
+
 -- ofIntCore
 -- TODO: typeclass?
 def Isize.ofIntCore := @Scalar.ofIntCore .Isize
-- 
cgit v1.3.1


From d87e35e1a53b2252cc2c8c554216115773fd9678 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Thu, 20 Jul 2023 11:38:55 +0200
Subject: Add fine-grained lemmas for the arithmetic operations

---
 backends/lean/Base/Primitives/Scalar.lean | 137 ++++++++++++++++++++++++++++--
 backends/lean/Base/Progress/Base.lean     |   2 +-
 2 files changed, 131 insertions(+), 8 deletions(-)

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

diff --git a/backends/lean/Base/Primitives/Scalar.lean b/backends/lean/Base/Primitives/Scalar.lean
index aaa4027f..1e9b51c2 100644
--- a/backends/lean/Base/Primitives/Scalar.lean
+++ b/backends/lean/Base/Primitives/Scalar.lean
@@ -438,7 +438,7 @@ instance {ty} : HDiv (Scalar ty) (Scalar ty) (Result (Scalar ty)) where
 instance {ty} : HMod (Scalar ty) (Scalar ty) (Result (Scalar ty)) where
   hMod x y := Scalar.rem x y
 
--- TODO: make progress work at a more fine grained level (see `Scalar.add_unsigned_spec`)
+-- Generic theorem - shouldn't be used much
 @[cpspec]
 theorem Scalar.add_spec {ty} {x y : Scalar ty}
   (hmin : Scalar.min ty ≤ x.val + y.val)
@@ -460,7 +460,32 @@ theorem Scalar.add_unsigned_spec {ty} (s: ¬ ty.isSigned) {x y : Scalar ty}
     cases ty <;> simp [min] at * <;> linarith
   apply add_spec <;> assumption
 
--- TODO: make it finer grained
+/- Fine-grained theorems -/
+@[cepspec] theorem Usize.add_spec {x y : Usize} (hmax : x.val + y.val ≤ Usize.max) :
+  ∃ z, x + y = ret z ∧ z.val = x.val + y.val := by
+  apply Scalar.add_unsigned_spec <;> simp only [Scalar.max, *]
+
+@[cepspec] theorem U8.add_spec {x y : U8} (hmax : x.val + y.val ≤ U8.max) :
+  ∃ z, x + y = ret z ∧ z.val = x.val + y.val := by
+  apply Scalar.add_unsigned_spec <;> simp only [Scalar.max, *]
+
+@[cepspec] theorem U16.add_spec {x y : U16} (hmax : x.val + y.val ≤ U16.max) :
+  ∃ z, x + y = ret z ∧ z.val = x.val + y.val := by
+  apply Scalar.add_unsigned_spec <;> simp only [Scalar.max, *]
+
+@[cepspec] theorem U32.add_spec {x y : U32} (hmax : x.val + y.val ≤ U32.max) :
+  ∃ z, x + y = ret z ∧ z.val = x.val + y.val := by
+  apply Scalar.add_unsigned_spec <;> simp only [Scalar.max, *]
+
+@[cepspec] theorem U64.add_spec {x y : U64} (hmax : x.val + y.val ≤ U64.max) :
+  ∃ z, x + y = ret z ∧ z.val = x.val + y.val := by
+  apply Scalar.add_unsigned_spec <;> simp only [Scalar.max, *]
+
+@[cepspec] theorem U128.add_spec {x y : U128} (hmax : x.val + y.val ≤ U128.max) :
+  ∃ z, x + y = ret z ∧ z.val = x.val + y.val := by
+  apply Scalar.add_unsigned_spec <;> simp only [Scalar.max, *]
+
+-- Generic theorem - shouldn't be used much
 @[cpspec]
 theorem Scalar.sub_spec {ty} {x y : Scalar ty}
   (hmin : Scalar.min ty ≤ x.val - y.val)
@@ -484,8 +509,32 @@ theorem Scalar.sub_unsigned_spec {ty} (s: ¬ ty.isSigned) {x y : Scalar ty}
   intros
   apply sub_spec <;> assumption
 
--- TODO: make it finer grained
-@[cpspec]
+/- Fine-grained theorems -/
+@[cepspec] theorem Usize.sub_spec {x y : Usize} (hmin : Usize.min ≤ x.val - y.val) :
+  ∃ z, x - y = ret z ∧ z.val = x.val - y.val := by
+  apply Scalar.sub_unsigned_spec <;> simp only [Scalar.min, *]
+
+@[cepspec] theorem U8.sub_spec {x y : U8} (hmin : U8.min ≤ x.val - y.val) :
+  ∃ z, x - y = ret z ∧ z.val = x.val - y.val := by
+  apply Scalar.sub_unsigned_spec <;> simp only [Scalar.min, *]
+
+@[cepspec] theorem U16.sub_spec {x y : U16} (hmin : U16.min ≤ x.val - y.val) :
+  ∃ z, x - y = ret z ∧ z.val = x.val - y.val := by
+  apply Scalar.sub_unsigned_spec <;> simp only [Scalar.min, *]
+
+@[cepspec] theorem U32.sub_spec {x y : U32} (hmin : U32.min ≤ x.val - y.val) :
+  ∃ z, x - y = ret z ∧ z.val = x.val - y.val := by
+  apply Scalar.sub_unsigned_spec <;> simp only [Scalar.min, *]
+
+@[cepspec] theorem U64.sub_spec {x y : U64} (hmin : U64.min ≤ x.val - y.val) :
+  ∃ z, x - y = ret z ∧ z.val = x.val - y.val := by
+  apply Scalar.sub_unsigned_spec <;> simp only [Scalar.min, *]
+
+@[cepspec] theorem U128.sub_spec {x y : U128} (hmin : U128.min ≤ x.val - y.val) :
+  ∃ z, x - y = ret z ∧ z.val = x.val - y.val := by
+  apply Scalar.sub_unsigned_spec <;> simp only [Scalar.min, *]
+
+-- Generic theorem - shouldn't be used much
 theorem Scalar.mul_spec {ty} {x y : Scalar ty}
   (hmin : Scalar.min ty ≤ x.val * y.val)
   (hmax : x.val * y.val ≤ Scalar.max ty) :
@@ -506,7 +555,32 @@ theorem Scalar.mul_unsigned_spec {ty} (s: ¬ ty.isSigned) {x y : Scalar ty}
     cases ty <;> simp at * <;> apply mul_nonneg hx hy
   apply mul_spec <;> assumption
 
--- TODO: make it finer grained
+/- Fine-grained theorems -/
+@[cepspec] theorem Usize.mul_spec {x y : Usize} (hmax : x.val * y.val ≤ Usize.max) :
+  ∃ z, x * y = ret z ∧ z.val = x.val * y.val := by
+  apply Scalar.mul_unsigned_spec <;> simp only [Scalar.max, *]
+
+@[cepspec] theorem U8.mul_spec {x y : U8} (hmax : x.val * y.val ≤ U8.max) :
+  ∃ z, x * y = ret z ∧ z.val = x.val * y.val := by
+  apply Scalar.mul_unsigned_spec <;> simp only [Scalar.max, *]
+
+@[cepspec] theorem U16.mul_spec {x y : U16} (hmax : x.val * y.val ≤ U16.max) :
+  ∃ z, x * y = ret z ∧ z.val = x.val * y.val := by
+  apply Scalar.mul_unsigned_spec <;> simp only [Scalar.max, *]
+
+@[cepspec] theorem U32.mul_spec {x y : U32} (hmax : x.val * y.val ≤ U32.max) :
+  ∃ z, x * y = ret z ∧ z.val = x.val * y.val := by
+  apply Scalar.mul_unsigned_spec <;> simp only [Scalar.max, *]
+
+@[cepspec] theorem U64.mul_spec {x y : U64} (hmax : x.val * y.val ≤ U64.max) :
+  ∃ z, x * y = ret z ∧ z.val = x.val * y.val := by
+  apply Scalar.mul_unsigned_spec <;> simp only [Scalar.max, *]
+
+@[cepspec] theorem U128.mul_spec {x y : U128} (hmax : x.val * y.val ≤ U128.max) :
+  ∃ z, x * y = ret z ∧ z.val = x.val * y.val := by
+  apply Scalar.mul_unsigned_spec <;> simp only [Scalar.max, *]
+
+-- Generic theorem - shouldn't be used much
 @[cpspec]
 theorem Scalar.div_spec {ty} {x y : Scalar ty}
   (hnz : y.val ≠ 0)
@@ -534,7 +608,32 @@ theorem Scalar.div_unsigned_spec {ty} (s: ¬ ty.isSigned) (x : Scalar ty) {y : S
   simp [*] at hs
   apply hs
 
--- TODO: make it finer grained
+/- Fine-grained theorems -/
+@[cepspec] theorem Usize.div_spec (x : Usize) {y : Usize} (hnz : y.val ≠ 0) :
+  ∃ z, x / y = ret z ∧ z.val = x.val / y.val := by
+  apply Scalar.div_unsigned_spec <;> simp [*]
+
+@[cepspec] theorem U8.div_spec (x : U8) {y : U8} (hnz : y.val ≠ 0) :
+  ∃ z, x / y = ret z ∧ z.val = x.val / y.val := by
+  apply Scalar.div_unsigned_spec <;> simp [Scalar.max, *]
+
+@[cepspec] theorem U16.div_spec (x : U16) {y : U16} (hnz : y.val ≠ 0) :
+  ∃ z, x / y = ret z ∧ z.val = x.val / y.val := by
+  apply Scalar.div_unsigned_spec <;> simp [Scalar.max, *]
+
+@[cepspec] theorem U32.div_spec (x : U32) {y : U32} (hnz : y.val ≠ 0) :
+  ∃ z, x / y = ret z ∧ z.val = x.val / y.val := by
+  apply Scalar.div_unsigned_spec <;> simp [Scalar.max, *]
+
+@[cepspec] theorem U64.div_spec (x : U64) {y : U64} (hnz : y.val ≠ 0) :
+  ∃ z, x / y = ret z ∧ z.val = x.val / y.val := by
+  apply Scalar.div_unsigned_spec <;> simp [Scalar.max, *]
+
+@[cepspec] theorem U128.div_spec (x : U128) {y : U128} (hnz : y.val ≠ 0) :
+  ∃ z, x / y = ret z ∧ z.val = x.val / y.val := by
+  apply Scalar.div_unsigned_spec <;> simp [Scalar.max, *]
+
+-- Generic theorem - shouldn't be used much
 @[cpspec]
 theorem Scalar.rem_spec {ty} {x y : Scalar ty}
   (hnz : y.val ≠ 0)
@@ -548,7 +647,7 @@ theorem Scalar.rem_spec {ty} {x y : Scalar ty}
 
 theorem Scalar.rem_unsigned_spec {ty} (s: ¬ ty.isSigned) (x : Scalar ty) {y : Scalar ty}
   (hnz : y.val ≠ 0) :
-  ∃ z, x % y = ret z ∧ z.val = scalar_rem x.val y.val := by
+  ∃ z, x % y = ret z ∧ z.val = x.val % y.val := by
   have h : Scalar.min ty = 0 := by cases ty <;> simp at *
   have hx := x.hmin
   have hy := y.hmin
@@ -565,6 +664,30 @@ theorem Scalar.rem_unsigned_spec {ty} (s: ¬ ty.isSigned) (x : Scalar ty) {y : S
   simp [*] at hs
   simp [*]
 
+@[cepspec] theorem Usize.rem_spec (x : Usize) {y : Usize} (hnz : y.val ≠ 0) :
+  ∃ z, x % y = ret z ∧ z.val = x.val % y.val := by
+  apply Scalar.rem_unsigned_spec <;> simp [*]
+
+@[cepspec] theorem U8.rem_spec (x : U8) {y : U8} (hnz : y.val ≠ 0) :
+  ∃ z, x % y = ret z ∧ z.val = x.val % y.val := by
+  apply Scalar.rem_unsigned_spec <;> simp [Scalar.max, *]
+
+@[cepspec] theorem U16.rem_spec (x : U16) {y : U16} (hnz : y.val ≠ 0) :
+  ∃ z, x % y = ret z ∧ z.val = x.val % y.val := by
+  apply Scalar.rem_unsigned_spec <;> simp [Scalar.max, *]
+
+@[cepspec] theorem U32.rem_spec (x : U32) {y : U32} (hnz : y.val ≠ 0) :
+  ∃ z, x % y = ret z ∧ z.val = x.val % y.val := by
+  apply Scalar.rem_unsigned_spec <;> simp [Scalar.max, *]
+
+@[cepspec] theorem U64.rem_spec (x : U64) {y : U64} (hnz : y.val ≠ 0) :
+  ∃ z, x % y = ret z ∧ z.val = x.val % y.val := by
+  apply Scalar.rem_unsigned_spec <;> simp [Scalar.max, *]
+
+@[cepspec] theorem U128.rem_spec (x : U128) {y : U128} (hnz : y.val ≠ 0) :
+  ∃ z, x % y = ret z ∧ z.val = x.val % y.val := by
+  apply Scalar.rem_unsigned_spec <;> simp [Scalar.max, *]
+
 -- ofIntCore
 -- TODO: typeclass?
 def Isize.ofIntCore := @Scalar.ofIntCore .Isize
diff --git a/backends/lean/Base/Progress/Base.lean b/backends/lean/Base/Progress/Base.lean
index 3599d866..2fbd24dd 100644
--- a/backends/lean/Base/Progress/Base.lean
+++ b/backends/lean/Base/Progress/Base.lean
@@ -240,7 +240,7 @@ initialize pspecClassExprAttr : PSpecClassExprAttr ← do
       -- We store two bindings:
       -- - arg to theorem name
       -- - reduced arg to theorem name
-      let rarg ← MetaM.run' (reduce arg)
+      let rarg ← MetaM.run' (reduceAll arg)
       trace[Progress] "Registering class spec theorem for ({fName}, {arg}) and ({fName}, {rarg})"
       -- Update the entry if there is one, add an entry if there is none
       let env :=
-- 
cgit v1.3.1


From 876137dff361620d8ade1a4ee94fa9274df0bdc6 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Tue, 25 Jul 2023 14:08:44 +0200
Subject: Improve int_tac and scalar_tac

---
 backends/lean/Base/Arith/Int.lean         | 63 +++++++++++++++++++++++++++----
 backends/lean/Base/Arith/Scalar.lean      |  6 +--
 backends/lean/Base/IList/IList.lean       | 12 ++----
 backends/lean/Base/Primitives/Vec.lean    | 25 ++++++------
 backends/lean/Base/Progress/Progress.lean | 13 ++++++-
 5 files changed, 87 insertions(+), 32 deletions(-)

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

diff --git a/backends/lean/Base/Arith/Int.lean b/backends/lean/Base/Arith/Int.lean
index fa957293..3415866e 100644
--- a/backends/lean/Base/Arith/Int.lean
+++ b/backends/lean/Base/Arith/Int.lean
@@ -24,12 +24,29 @@ class PropHasImp (x : Prop) where
   concl : Prop
   prop : x → concl
 
+instance (p : Int → Prop) : HasIntProp (Subtype p) where
+  prop_ty := λ x => p x
+  prop := λ x => x.property
+
 -- This also works for `x ≠ y` because this expression reduces to `¬ x = y`
 -- and `Ne` is marked as `reducible`
 instance (x y : Int) : PropHasImp (¬ x = y) where
   concl := x < y ∨ x > y
   prop := λ (h:x ≠ y) => ne_is_lt_or_gt h
 
+-- Check if a proposition is a linear integer proposition.
+-- We notably use this to check the goals.
+class IsLinearIntProp (x : Prop) where
+
+instance (x y : Int) : IsLinearIntProp (x < y) where
+instance (x y : Int) : IsLinearIntProp (x > y) where
+instance (x y : Int) : IsLinearIntProp (x ≤ y) where
+instance (x y : Int) : IsLinearIntProp (x ≥ y) where
+instance (x y : Int) : IsLinearIntProp (x ≥ y) where
+/- It seems we don't need to do any special preprocessing when the *goal*
+   has the following shape - I guess `linarith` automatically calls `intro` -/
+instance (x y : Int) : IsLinearIntProp (¬ x = y) where
+
 open Lean Lean.Elab Lean.Meta
 
 -- Explore a term by decomposing the applications (we explore the applied
@@ -189,14 +206,27 @@ def intTacPreprocess (extraPreprocess :  Tactic.TacticM Unit) : Tactic.TacticM U
 elab "int_tac_preprocess" : tactic =>
   intTacPreprocess (do pure ())
 
-def intTac (extraPreprocess :  Tactic.TacticM Unit) : Tactic.TacticM Unit := do
+-- Check if the goal is a linear arithmetic goal
+def goalIsLinearInt : Tactic.TacticM Bool := do
+  Tactic.withMainContext do
+  let gty ← Tactic.getMainTarget
+  match ← trySynthInstance (← mkAppM ``IsLinearIntProp #[gty]) with
+  | .some _ => pure true
+  | _ => pure false
+
+def intTac (splitGoalConjs : Bool) (extraPreprocess :  Tactic.TacticM Unit) : Tactic.TacticM Unit := do
   Tactic.withMainContext do
   Tactic.focus do
+  let g ← Tactic.getMainGoal
+  trace[Arith] "Original goal: {g}"
+  -- Introduce all the universally quantified variables (includes the assumptions)
+  let (_, g) ← g.intros
+  Tactic.setGoals [g]
   -- Preprocess - wondering if we should do this before or after splitting
   -- the goal. I think before leads to a smaller proof term?
   Tactic.allGoals (intTacPreprocess extraPreprocess)
   -- Split the conjunctions in the goal
-  Tactic.allGoals (Utils.repeatTac Utils.splitConjTarget)
+  if splitGoalConjs then Tactic.allGoals (Utils.repeatTac Utils.splitConjTarget)
   -- Call linarith
   let linarith := do
     let cfg : Linarith.LinarithConfig := {
@@ -204,10 +234,25 @@ def intTac (extraPreprocess :  Tactic.TacticM Unit) : Tactic.TacticM Unit := do
       splitNe := false
     }
     Tactic.liftMetaFinishingTactic <| Linarith.linarith false [] cfg
-  Tactic.allGoals linarith
-
-elab "int_tac" : tactic =>
-  intTac (do pure ())
+  Tactic.allGoals do
+    -- We check if the goal is a linear arithmetic goal: if yes, we directly
+    -- call linarith, otherwise we first apply exfalso (we do this because
+    -- linarith is too general and sometimes fails to do this correctly).
+    if ← goalIsLinearInt then do
+      trace[Arith] "linarith goal: {← Tactic.getMainGoal}"
+      linarith
+    else do
+      let g ← Tactic.getMainGoal
+      let gs ← g.apply (Expr.const ``False.elim [.zero])
+      let goals ← Tactic.getGoals
+      Tactic.setGoals (gs ++ goals)
+      Tactic.allGoals do
+        trace[Arith] "linarith goal: {← Tactic.getMainGoal}"
+        linarith
+
+elab "int_tac" args:(" split_goal"?): tactic =>
+  let split := args.raw.getArgs.size > 0
+  intTac split (do pure ())
 
 example (x : Int) (h0: 0 ≤ x) (h1: x ≠ 0) : 0 < x := by
   int_tac_preprocess
@@ -219,10 +264,14 @@ example (x : Int) (h0: 0 ≤ x) (h1: x ≠ 0) : 0 < x := by
 
 -- Checking that things append correctly when there are several disjunctions
 example (x y : Int) (h0: 0 ≤ x) (h1: x ≠ 0) (h2 : 0 ≤ y) (h3 : y ≠ 0) : 0 < x ∧ 0 < y := by
-  int_tac
+  int_tac split_goal
 
 -- Checking that things append correctly when there are several disjunctions
 example (x y : Int) (h0: 0 ≤ x) (h1: x ≠ 0) (h2 : 0 ≤ y) (h3 : y ≠ 0) : 0 < x ∧ 0 < y ∧ x + y ≥ 2 := by
+  int_tac split_goal
+
+-- Checking that we can prove exfalso
+example (a : Prop) (x : Int) (h0: 0 < x) (h1: x < 0) : a := by
   int_tac
 
 end Arith
diff --git a/backends/lean/Base/Arith/Scalar.lean b/backends/lean/Base/Arith/Scalar.lean
index f8903ecf..a56ea08b 100644
--- a/backends/lean/Base/Arith/Scalar.lean
+++ b/backends/lean/Base/Arith/Scalar.lean
@@ -28,11 +28,11 @@ elab "scalar_tac_preprocess" : tactic =>
   intTacPreprocess scalarTacExtraPreprocess
 
 -- A tactic to solve linear arithmetic goals in the presence of scalars
-def scalarTac : Tactic.TacticM Unit := do
-  intTac scalarTacExtraPreprocess
+def scalarTac (splitGoalConjs : Bool) : Tactic.TacticM Unit := do
+  intTac splitGoalConjs scalarTacExtraPreprocess
 
 elab "scalar_tac" : tactic =>
-  scalarTac
+  scalarTac false
 
 instance (ty : ScalarTy) : HasIntProp (Scalar ty) where
   -- prop_ty is inferred
diff --git a/backends/lean/Base/IList/IList.lean b/backends/lean/Base/IList/IList.lean
index 1773e593..2443b1a6 100644
--- a/backends/lean/Base/IList/IList.lean
+++ b/backends/lean/Base/IList/IList.lean
@@ -46,21 +46,18 @@ theorem indexOpt_bounds (ls : List α) (i : Int) :
   ls.indexOpt i = none ↔ i < 0 ∨ ls.len ≤ i :=
   match ls with
   | [] =>
-    have : ¬ (i < 0) → 0 ≤ i := by intro; linarith -- TODO: simplify (we could boost int_tac)
+    have : ¬ (i < 0) → 0 ≤ i := by int_tac
     by simp; tauto
   | _ :: tl =>
     have := indexOpt_bounds tl (i - 1)
     if h: i = 0 then
       by
         simp [*];
-        -- TODO: int_tac/scalar_tac should also explore the goal!
-        have := tl.len_pos
-        linarith
+        int_tac
     else by
       simp [*]
       constructor <;> intros <;>
-      -- TODO: tactic to split all disjunctions
-      rename_i hor <;> cases hor <;>
+      casesm* _ ∨ _ <;> -- splits all the disjunctions
       first | left; int_tac | right; int_tac
 
 theorem indexOpt_eq_index [Inhabited α] (ls : List α) (i : Int) :
@@ -126,7 +123,6 @@ theorem length_update (ls : List α) (i : Int) (x : α) : (ls.update i x).length
 theorem len_update (ls : List α) (i : Int) (x : α) : (ls.update i x).len = ls.len := by
   simp [len_eq_length]
 
-
 theorem left_length_eq_append_eq (l1 l2 l1' l2' : List α) (heq : l1.length = l1'.length) :
   l1 ++ l2 = l1' ++ l2' ↔ l1 = l1' ∧ l2 = l2' := by
   revert l1'
@@ -203,7 +199,7 @@ theorem index_eq
     (l.update i x).index i = x
   :=
   fun _ _ => match l with
-  | [] => by simp at *; exfalso; scalar_tac -- TODO: exfalso needed. Son FIXME
+  | [] => by simp at *; scalar_tac
   | hd :: tl =>
     if h: i = 0 then
       by
diff --git a/backends/lean/Base/Primitives/Vec.lean b/backends/lean/Base/Primitives/Vec.lean
index be3a0e5b..35092c29 100644
--- a/backends/lean/Base/Primitives/Vec.lean
+++ b/backends/lean/Base/Primitives/Vec.lean
@@ -16,20 +16,19 @@ open Result Error
 -- VECTORS --
 -------------
 
-def Vec (α : Type u) := { l : List α // List.length l ≤ Usize.max }
+def Vec (α : Type u) := { l : List α // l.length ≤ Usize.max }
 
 -- TODO: do we really need it? It should be with Subtype by default
-instance Vec.cast (a : Type): Coe (Vec a) (List a)  where coe := λ v => v.val
+instance Vec.cast (a : Type u): Coe (Vec a) (List a)  where coe := λ v => v.val
 
-instance (a : Type) : Arith.HasIntProp (Vec a) where
-  prop_ty := λ v => v.val.length ≤ Scalar.max ScalarTy.Usize
-  prop := λ ⟨ _, l ⟩ => l
+instance (a : Type u) : Arith.HasIntProp (Vec a) where
+  prop_ty := λ v => v.val.len ≤ Scalar.max ScalarTy.Usize
+  prop := λ ⟨ _, l ⟩ => by simp[Scalar.max, List.len_eq_length, *]
 
-example {a: Type} (v : Vec a) : v.val.length ≤ Scalar.max ScalarTy.Usize := by
-  intro_has_int_prop_instances
-  simp_all [Scalar.max, Scalar.min]
+@[simp]
+abbrev Vec.length {α : Type u} (v : Vec α) : Int := v.val.len
 
-example {a: Type} (v : Vec a) : v.val.length ≤ Scalar.max ScalarTy.Usize := by
+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 ⟩
@@ -38,9 +37,6 @@ def Vec.len (α : Type u) (v : Vec α) : Usize :=
   let ⟨ v, l ⟩ := v
   Usize.ofIntCore (List.length v) (by simp [Scalar.min, Usize.min]) l
 
-@[simp]
-abbrev Vec.length {α : Type u} (v : Vec α) : Int := v.val.len
-
 -- This shouldn't be used
 def Vec.push_fwd (α : Type u) (_ : Vec α) (_ : α) : Unit := ()
 
@@ -115,11 +111,14 @@ theorem Vec.index_mut_spec {α : Type u} [Inhabited α] (v: Vec α) (i: Usize) :
   have h := List.indexOpt_eq_index v.val i.val (by scalar_tac) (by simp [*])
   simp only [*]
 
+instance {α : Type u} (p : Vec α → Prop) : Arith.HasIntProp (Subtype p) where
+  prop_ty := λ x => p x
+  prop := λ x => x.property
+
 def Vec.index_mut_back (α : Type u) (v: Vec α) (i: Usize) (x: α) : Result (Vec α) :=
   match v.val.indexOpt i.val with
   | none => fail .arrayOutOfBounds
   | some _ =>
-    -- TODO: int_tac: introduce the refinements in the context?
     .ret ⟨ v.val.update i.val x, by have := v.property; simp [*] ⟩
 
 @[pspec]
diff --git a/backends/lean/Base/Progress/Progress.lean b/backends/lean/Base/Progress/Progress.lean
index c0ddc63d..a281f1d2 100644
--- a/backends/lean/Base/Progress/Progress.lean
+++ b/backends/lean/Base/Progress/Progress.lean
@@ -307,7 +307,18 @@ def evalProgress (args : TSyntax `Progress.progressArgs) : TacticM Unit := do
     let args := (args.get! 2).getArgs
     (args.get! 3).getArgs.size > 0
   trace[Progress] "Split post: {splitPost}"
-  progressAsmsOrLookupTheorem keep withArg ids splitPost (firstTac [assumptionTac, Arith.scalarTac])
+  /- For scalarTac we have a fast track: if the goal is not a linear
+     arithmetic goal, we skip (note that otherwise, scalarTac would try
+     to prove a contradiction) -/
+  let scalarTac : TacticM Unit := do
+    if ← Arith.goalIsLinearInt then
+      -- Also: we don't try to split the goal if it is a conjunction
+      -- (it shouldn't be)
+      Arith.scalarTac false
+    else
+      throwError "Not a linear arithmetic goal"
+  progressAsmsOrLookupTheorem keep withArg ids splitPost (
+    firstTac [assumptionTac, scalarTac])
 
 elab "progress" args:progressArgs : tactic =>
   evalProgress args
-- 
cgit v1.3.1


From 1854c631a6a7a3f8d45ad18e05547f9d3782c3ee Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Tue, 25 Jul 2023 16:26:08 +0200
Subject: Make progress on the hashmap properties

---
 backends/lean/Base/Arith/Base.lean        |  4 ++
 backends/lean/Base/Arith/Int.lean         |  2 +
 backends/lean/Base/Arith/Scalar.lean      |  3 +-
 backends/lean/Base/Primitives/Scalar.lean | 48 +++++++++-------
 backends/lean/Base/Primitives/Vec.lean    | 13 ++++-
 backends/lean/Base/Progress/Base.lean     |  4 +-
 backends/lean/Base/Progress/Progress.lean |  4 +-
 tests/lean/Hashmap/Properties.lean        | 92 +++++++++++++++++++++++++++++++
 8 files changed, 141 insertions(+), 29 deletions(-)

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

diff --git a/backends/lean/Base/Arith/Base.lean b/backends/lean/Base/Arith/Base.lean
index e008f7b9..9c11ed45 100644
--- a/backends/lean/Base/Arith/Base.lean
+++ b/backends/lean/Base/Arith/Base.lean
@@ -53,4 +53,8 @@ theorem int_pos_ind (p : Int → Prop) :
     rename_i m
     cases m <;> simp_all
 
+-- We sometimes need this to make sure no natural numbers appear in the goals
+-- TODO: there is probably something more general to do
+theorem nat_zero_eq_int_zero : (0 : Nat) = (0 : Int) := by simp
+
 end Arith
diff --git a/backends/lean/Base/Arith/Int.lean b/backends/lean/Base/Arith/Int.lean
index 3415866e..bc0676d8 100644
--- a/backends/lean/Base/Arith/Int.lean
+++ b/backends/lean/Base/Arith/Int.lean
@@ -225,6 +225,8 @@ def intTac (splitGoalConjs : Bool) (extraPreprocess :  Tactic.TacticM Unit) : Ta
   -- Preprocess - wondering if we should do this before or after splitting
   -- the goal. I think before leads to a smaller proof term?
   Tactic.allGoals (intTacPreprocess extraPreprocess)
+  -- More preprocessing
+  Tactic.allGoals (Utils.simpAt [] [``nat_zero_eq_int_zero] [] .wildcard)
   -- Split the conjunctions in the goal
   if splitGoalConjs then Tactic.allGoals (Utils.repeatTac Utils.splitConjTarget)
   -- Call linarith
diff --git a/backends/lean/Base/Arith/Scalar.lean b/backends/lean/Base/Arith/Scalar.lean
index a56ea08b..6f4a8eba 100644
--- a/backends/lean/Base/Arith/Scalar.lean
+++ b/backends/lean/Base/Arith/Scalar.lean
@@ -21,7 +21,8 @@ def scalarTacExtraPreprocess : Tactic.TacticM Unit := do
                  ``I8.min, ``I16.min, ``I32.min, ``I64.min, ``I128.min,
                  ``I8.max, ``I16.max, ``I32.max, ``I64.max, ``I128.max,
                  ``U8.min, ``U16.min, ``U32.min, ``U64.min, ``U128.min,
-                 ``U8.max, ``U16.max, ``U32.max, ``U64.max, ``U128.max
+                 ``U8.max, ``U16.max, ``U32.max, ``U64.max, ``U128.max,
+                 ``Usize.min
                  ] [] [] .wildcard
 
 elab "scalar_tac_preprocess" : tactic =>
diff --git a/backends/lean/Base/Primitives/Scalar.lean b/backends/lean/Base/Primitives/Scalar.lean
index 1e9b51c2..3beb7527 100644
--- a/backends/lean/Base/Primitives/Scalar.lean
+++ b/backends/lean/Base/Primitives/Scalar.lean
@@ -66,27 +66,33 @@ def U128.smin  : Int := 0
 def U128.smax  : Int := HPow.hPow 2 128 - 1
 
 -- The "normalized" bounds, that we use in practice
-def I8.min    := -128
-def I8.max   := 127
-def I16.min  := -32768
-def I16.max  := 32767
-def I32.min  := -2147483648
-def I32.max  := 2147483647
-def I64.min  := -9223372036854775808
-def I64.max  := 9223372036854775807
-def I128.min := -170141183460469231731687303715884105728
-def I128.max := 170141183460469231731687303715884105727
-@[simp] def U8.min   := 0
-def U8.max   := 255
-@[simp] def U16.min  := 0
-def U16.max  := 65535
-@[simp] def U32.min  := 0
-def U32.max  := 4294967295
-@[simp] def U64.min  := 0
-def U64.max  := 18446744073709551615
-@[simp] def U128.min := 0
-def U128.max := 340282366920938463463374607431768211455
-@[simp] def Usize.min := 0
+def I8.min    : Int   := -128
+def I8.max    : Int   := 127
+def I16.min   : Int  := -32768
+def I16.max   : Int  := 32767
+def I32.min   : Int  := -2147483648
+def I32.max   : Int  := 2147483647
+def I64.min   : Int  := -9223372036854775808
+def I64.max   : Int  := 9223372036854775807
+def I128.min  : Int := -170141183460469231731687303715884105728
+def I128.max  : Int := 170141183460469231731687303715884105727
+@[simp]
+def U8.min    : Int   := 0
+def U8.max    : Int   := 255
+@[simp]
+def U16.min   : Int  := 0
+def U16.max   : Int  := 65535
+@[simp]
+def U32.min   : Int  := 0
+def U32.max   : Int  := 4294967295
+@[simp]
+def U64.min   : Int  := 0
+def U64.max   : Int  := 18446744073709551615
+@[simp]
+def U128.min  : Int := 0
+def U128.max  : Int := 340282366920938463463374607431768211455
+@[simp]
+def Usize.min : Int := 0
 
 def Isize.refined_min : { n:Int // n = I32.min ∨ n = I64.min } :=
   ⟨ Isize.smin, by
diff --git a/backends/lean/Base/Primitives/Vec.lean b/backends/lean/Base/Primitives/Vec.lean
index 35092c29..5a709566 100644
--- a/backends/lean/Base/Primitives/Vec.lean
+++ b/backends/lean/Base/Primitives/Vec.lean
@@ -22,20 +22,27 @@ def Vec (α : Type u) := { l : List α // l.length ≤ Usize.max }
 instance Vec.cast (a : Type u): Coe (Vec a) (List a)  where coe := λ v => v.val
 
 instance (a : Type u) : Arith.HasIntProp (Vec a) where
-  prop_ty := λ v => v.val.len ≤ Scalar.max ScalarTy.Usize
+  prop_ty := λ v => 0 ≤ v.val.len ∧ v.val.len ≤ Scalar.max ScalarTy.Usize
   prop := λ ⟨ _, l ⟩ => by simp[Scalar.max, List.len_eq_length, *]
 
 @[simp]
 abbrev Vec.length {α : Type u} (v : Vec α) : Int := v.val.len
 
+@[simp]
+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 ⟩
 
+-- TODO: very annoying that the α is an explicit parameter
 def Vec.len (α : Type u) (v : Vec α) : Usize :=
-  let ⟨ v, l ⟩ := v
-  Usize.ofIntCore (List.length v) (by simp [Scalar.min, Usize.min]) l
+  Usize.ofIntCore v.val.len (by scalar_tac) (by scalar_tac)
+
+@[simp]
+theorem Vec.len_val {α : Type u} (v : Vec α) : (Vec.len α v).val = v.length :=
+  by rfl
 
 -- This shouldn't be used
 def Vec.push_fwd (α : Type u) (_ : Vec α) (_ : α) : Unit := ()
diff --git a/backends/lean/Base/Progress/Base.lean b/backends/lean/Base/Progress/Base.lean
index b54bdf7a..6f820a84 100644
--- a/backends/lean/Base/Progress/Base.lean
+++ b/backends/lean/Base/Progress/Base.lean
@@ -81,8 +81,8 @@ section Methods
     let (fExpr, f, args) ← do
       if mf.isConst ∧ mf.constName = ``Bind.bind then do
         -- Dive into the bind
-        let fExpr := margs.get! 4
-        fExpr.consumeMData.withApp fun f args => pure (fExpr, f, args)
+        let fExpr := (margs.get! 4).consumeMData
+        fExpr.withApp fun f args => pure (fExpr, f, args)
       else pure (mExpr, mf, margs)
     trace[Progress] "After stripping the arguments of the function call:\n- f: {f}\n- args: {args}"
     if ¬ f.isConst then throwError "Not a constant: {f}"
diff --git a/backends/lean/Base/Progress/Progress.lean b/backends/lean/Base/Progress/Progress.lean
index a281f1d2..a2c7764f 100644
--- a/backends/lean/Base/Progress/Progress.lean
+++ b/backends/lean/Base/Progress/Progress.lean
@@ -58,9 +58,9 @@ def progressWith (fExpr : Expr) (th : TheoremOrLocal)
     let (thBody, _) ← destEq thBody
     trace[Progress] "After splitting equality: {thBody}"
     -- There shouldn't be any existential variables in thBody
-    pure thBody
+    pure thBody.consumeMData
   -- Match the body with the target
-  trace[Progress] "Matching `{thBody}` with `{fExpr}`"
+  trace[Progress] "Matching:\n- body:\n{thBody}\n- target:\n{fExpr}"
   let ok ← isDefEq thBody fExpr
   if ¬ ok then throwError "Could not unify the theorem with the target:\n- theorem: {thBody}\n- target: {fExpr}"
   let mgoal ← Tactic.getMainGoal
diff --git a/tests/lean/Hashmap/Properties.lean b/tests/lean/Hashmap/Properties.lean
index de6bf636..b2d5570a 100644
--- a/tests/lean/Hashmap/Properties.lean
+++ b/tests/lean/Hashmap/Properties.lean
@@ -136,6 +136,40 @@ def slot_s_inv (l i : Int) (ls : Core.List (Usize × α)) : Prop :=
 
 def slot_t_inv (l i : Int) (s : List α) : Prop := slot_s_inv l i s.v
 
+-- Interpret the hashmap as a list of lists
+def v (hm : HashMap α) : Core.List (Core.List (Usize × α)) :=
+  hm.slots.val.map List.v
+
+-- Interpret the hashmap as an associative list
+def al_v (hm : HashMap α) : Core.List (Usize × α) :=
+  hm.v.flatten
+
+-- TODO: automatic derivation
+instance : Inhabited (List α) where
+  default := .Nil
+
+@[simp]
+def slots_s_inv (s : Core.List (List α)) : Prop :=
+  ∀ (i : Int), 0 ≤ i → i < s.len → slot_t_inv s.len i (s.index i)
+
+def slots_t_inv (s : Vec (List α)) : Prop :=
+  slots_s_inv s.v
+
+@[simp]
+def base_inv (hm : HashMap α) : Prop :=
+  -- [num_entries] correctly tracks the number of entries
+  hm.num_entries.val = hm.al_v.len ∧
+  -- Slots invariant
+  slots_t_inv hm.slots ∧
+  -- The capacity must be > 0 (otherwise we can't resize)
+  0 < hm.slots.length
+  -- TODO: load computation
+
+def inv (hm : HashMap α) : Prop :=
+  -- Base invariant
+  base_inv hm
+  -- TODO: either the hashmap is not overloaded, or we can't resize it
+
 theorem insert_in_list_back_spec_aux {α : Type} (l : Int) (key: Usize) (value: α) (l0: List α)
   (hinv : slot_s_inv_hash l (hash_mod_key key l) l0.v)
   (hdk : distinct_keys l0.v) :
@@ -191,6 +225,64 @@ theorem insert_in_list_back_spec_aux {α : Type} (l : Int) (key: Usize) (value:
        -- TODO: canonize addition by default?
        simp_all [Int.add_assoc, Int.add_comm, Int.add_left_comm]
 
+@[pspec]
+theorem insert_in_list_back_spec {α : Type} (l : Int) (key: Usize) (value: α) (l0: List α)
+  (hinv : slot_s_inv_hash l (hash_mod_key key l) l0.v)
+  (hdk : distinct_keys l0.v) :
+  ∃ l1,
+    insert_in_list_back α key value l0 = ret l1 ∧
+    -- We update the binding
+    l1.lookup key = value ∧
+    (∀ k, k ≠ key → l1.lookup k = l0.lookup k) ∧
+    -- We preserve part of the key invariant
+    slot_s_inv_hash l (hash_mod_key key l) l1.v ∧
+    -- Reasoning about the length
+    (match l0.lookup key with
+     | none => l1.len = l0.len + 1
+     | some _ => l1.len = l0.len) ∧
+    -- The keys are distinct
+    distinct_keys l1.v
+  := by
+  progress with insert_in_list_back_spec_aux as ⟨ l1 .. ⟩
+  exists l1
+
+def slots_t_lookup (s : Core.List (List α)) (k : Usize) : Option α :=
+  let i := hash_mod_key k s.len
+  let slot := s.index i
+  slot.lookup k
+
+def lookup (hm : HashMap α) (k : Usize) : Option α :=
+  slots_t_lookup hm.slots.val k
+
+@[simp]
+abbrev len_s (hm : HashMap α) : Int := hm.al_v.len
+
+set_option trace.Progress true
+/-set_option pp.explicit true
+set_option pp.universes true
+set_option pp.notation false-/
+
+theorem insert_no_resize_spec {α : Type} (hm : HashMap α) (key : Usize) (value : α)
+  (hinv : hm.inv) (hnsat : hm.lookup key = none → hm.len_s < Usize.max) :
+  ∃ nhm, hm.insert_no_resize α key value = ret nhm  ∧
+  -- We preserve the invariant
+  nhm.inv ∧
+  -- We updated the binding for key
+  nhm.lookup key = some value ∧
+  -- We left the other bindings unchanged
+  (∀ k, k ≠ key → nhm.lookup k = hm.lookup k) ∧
+  -- Reasoning about the length
+  (match hm.lookup key with
+   | none => nhm.len_s = hm.len_s + 1
+   | some _ => nhm.len_s = hm.len_s) := by
+  rw [insert_no_resize]
+  simp [hash_key]
+  have : (Vec.len (List α) hm.slots).val ≠ 0 := by
+   intro
+   simp_all [inv]
+  progress as ⟨ hash_mod ⟩
+  progress
+
 end HashMap
 
 end hashmap
-- 
cgit v1.3.1


From 0cc3c78137434d848188eee2a66b1e2cacfd102e Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Tue, 25 Jul 2023 19:06:05 +0200
Subject: Make progress on the proofs of the hashmap

---
 backends/lean/Base/Arith/Int.lean         |   1 +
 backends/lean/Base/IList/IList.lean       |  41 +++++++++++
 backends/lean/Base/Primitives/Base.lean   |   2 +-
 backends/lean/Base/Primitives/Vec.lean    |  20 +++---
 backends/lean/Base/Progress/Progress.lean |  34 +++++++--
 backends/lean/Base/Utils.lean             |  36 +++++++---
 tests/lean/Hashmap/Properties.lean        | 116 ++++++++++++++++++++++++++++--
 7 files changed, 216 insertions(+), 34 deletions(-)

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

diff --git a/backends/lean/Base/Arith/Int.lean b/backends/lean/Base/Arith/Int.lean
index bc0676d8..48a30a49 100644
--- a/backends/lean/Base/Arith/Int.lean
+++ b/backends/lean/Base/Arith/Int.lean
@@ -43,6 +43,7 @@ instance (x y : Int) : IsLinearIntProp (x > y) where
 instance (x y : Int) : IsLinearIntProp (x ≤ y) where
 instance (x y : Int) : IsLinearIntProp (x ≥ y) where
 instance (x y : Int) : IsLinearIntProp (x ≥ y) where
+instance (x y : Int) : IsLinearIntProp (x = y) where
 /- It seems we don't need to do any special preprocessing when the *goal*
    has the following shape - I guess `linarith` automatically calls `intro` -/
 instance (x y : Int) : IsLinearIntProp (¬ x = y) where
diff --git a/backends/lean/Base/IList/IList.lean b/backends/lean/Base/IList/IList.lean
index 2443b1a6..93047a1b 100644
--- a/backends/lean/Base/IList/IList.lean
+++ b/backends/lean/Base/IList/IList.lean
@@ -123,6 +123,10 @@ theorem length_update (ls : List α) (i : Int) (x : α) : (ls.update i x).length
 theorem len_update (ls : List α) (i : Int) (x : α) : (ls.update i x).len = ls.len := by
   simp [len_eq_length]
 
+@[simp]
+theorem len_map (ls : List α) (f : α → β) : (ls.map f).len = ls.len := by
+  simp [len_eq_length]
+
 theorem left_length_eq_append_eq (l1 l2 l1' l2' : List α) (heq : l1.length = l1'.length) :
   l1 ++ l2 = l1' ++ l2' ↔ l1 = l1' ∧ l2 = l2' := by
   revert l1'
@@ -210,6 +214,43 @@ theorem index_eq
         simp at *
         apply index_eq <;> scalar_tac
 
+theorem update_map_eq {α : Type u} {β : Type v} (ls : List α) (i : Int) (x : α) (f : α → β) :
+  (ls.update i x).map f = (ls.map f).update i (f x) :=
+  match ls with
+  | [] => by simp
+  | hd :: tl =>
+    if h : i = 0 then by simp [*]
+    else
+      have hi := update_map_eq tl (i - 1) x f
+      by simp [*]
+
+theorem len_flatten_update_eq {α : Type u} (ls : List (List α)) (i : Int) (x : List α)
+  (h0 : 0 ≤ i) (h1 : i < ls.len) :
+  (ls.update i x).flatten.len = ls.flatten.len + x.len - (ls.index i).len :=
+  match ls with
+  | [] => by simp at h1; int_tac
+  | hd :: tl => by
+    simp at h1
+    if h : i = 0 then simp [*]; int_tac
+    else
+      have hi := len_flatten_update_eq tl (i - 1) x (by int_tac) (by int_tac)
+      simp [*]
+      int_tac
+
+@[simp]
+theorem index_map_eq {α : Type u} {β : Type v} [Inhabited α] [Inhabited β] (ls : List α) (i : Int) (f : α → β)
+  (h0 : 0 ≤ i) (h1 : i < ls.len) :
+  (ls.map f).index i = f (ls.index i) :=
+  match ls with
+  | [] => by simp at h1; int_tac
+  | hd :: tl =>
+    if h : i = 0 then by
+      simp [*]
+    else
+      have hi := index_map_eq tl (i - 1) f (by int_tac) (by simp at h1; int_tac)
+      by
+        simp [*]
+
 def allP {α : Type u} (l : List α) (p: α → Prop) : Prop :=
   foldr (fun a r => p a ∧ r) True l
 
diff --git a/backends/lean/Base/Primitives/Base.lean b/backends/lean/Base/Primitives/Base.lean
index db462c38..7c0fa3bb 100644
--- a/backends/lean/Base/Primitives/Base.lean
+++ b/backends/lean/Base/Primitives/Base.lean
@@ -76,7 +76,7 @@ def eval_global {α: Type u} (x: Result α) (_: ret? x): α :=
 
 /- DO-DSL SUPPORT -/
 
-def bind {α : Type u} {β : Type v} (x: Result α) (f: α -> Result β) : Result β :=
+def bind {α : Type u} {β : Type v} (x: Result α) (f: α → Result β) : Result β :=
   match x with
   | ret v  => f v 
   | fail v => fail v
diff --git a/backends/lean/Base/Primitives/Vec.lean b/backends/lean/Base/Primitives/Vec.lean
index 5a709566..523372bb 100644
--- a/backends/lean/Base/Primitives/Vec.lean
+++ b/backends/lean/Base/Primitives/Vec.lean
@@ -75,10 +75,9 @@ def Vec.insert (α : Type u) (v: Vec α) (i: Usize) (x: α) : Result (Vec α) :=
     .fail arrayOutOfBounds
 
 @[pspec]
-theorem Vec.insert_spec {α : Type u} (v: Vec α) (i: Usize) (x: α) :
-  i.val < v.length →
+theorem Vec.insert_spec {α : Type u} (v: Vec α) (i: Usize) (x: α)
+  (hbound : i.val < v.length) :
   ∃ nv, v.insert α i x = ret nv ∧ nv.val = v.val.update i.val x := by
-  intro h
   simp [insert, *]
 
 def Vec.index (α : Type u) (v: Vec α) (i: Usize) : Result α :=
@@ -87,10 +86,9 @@ def Vec.index (α : Type u) (v: Vec α) (i: Usize) : Result α :=
   | some x => ret x
 
 @[pspec]
-theorem Vec.index_spec {α : Type u} [Inhabited α] (v: Vec α) (i: Usize) :
-  i.val < v.length →
+theorem Vec.index_spec {α : Type u} [Inhabited α] (v: Vec α) (i: Usize)
+  (hbound : i.val < v.length) :
   v.index α i = ret (v.val.index i.val) := by
-  intro
   simp only [index]
   -- TODO: dependent rewrite
   have h := List.indexOpt_eq_index v.val i.val (by scalar_tac) (by simp [*])
@@ -109,10 +107,9 @@ def Vec.index_mut (α : Type u) (v: Vec α) (i: Usize) : Result α :=
   | some x => ret x
 
 @[pspec]
-theorem Vec.index_mut_spec {α : Type u} [Inhabited α] (v: Vec α) (i: Usize) :
-  i.val < v.length →
+theorem Vec.index_mut_spec {α : Type u} [Inhabited α] (v: Vec α) (i: Usize)
+  (hbound : i.val < v.length) :
   v.index_mut α i = ret (v.val.index i.val) := by
-  intro
   simp only [index_mut]
   -- TODO: dependent rewrite
   have h := List.indexOpt_eq_index v.val i.val (by scalar_tac) (by simp [*])
@@ -129,12 +126,11 @@ def Vec.index_mut_back (α : Type u) (v: Vec α) (i: Usize) (x: α) : Result (Ve
     .ret ⟨ v.val.update i.val x, by have := v.property; simp [*] ⟩
 
 @[pspec]
-theorem Vec.index_mut_back_spec {α : Type u} (v: Vec α) (i: Usize) (x : α) :
-  i.val < v.length →
+theorem Vec.index_mut_back_spec {α : Type u} (v: Vec α) (i: Usize) (x : α)
+  (hbound : i.val < v.length) :
   ∃ nv, v.index_mut_back α i x = ret nv ∧
   nv.val = v.val.update i.val x
   := by
-  intro
   simp only [index_mut_back]
   have h := List.indexOpt_bounds v.val i.val
   split
diff --git a/backends/lean/Base/Progress/Progress.lean b/backends/lean/Base/Progress/Progress.lean
index a2c7764f..4a406bdf 100644
--- a/backends/lean/Base/Progress/Progress.lean
+++ b/backends/lean/Base/Progress/Progress.lean
@@ -1,6 +1,7 @@
 import Lean
 import Base.Arith
 import Base.Progress.Base
+import Base.Primitives -- TODO: remove?
 
 namespace Progress
 
@@ -41,7 +42,12 @@ def progressWith (fExpr : Expr) (th : TheoremOrLocal)
     match th with
     | .Theorem thName =>
       let thDecl := env.constants.find! thName
-      pure thDecl.type
+      -- We have to introduce fresh meta-variables for the universes already
+      let ul : List (Name × Level) ←
+        thDecl.levelParams.mapM (λ x => do pure (x, ← mkFreshLevelMVar))
+      let ulMap : HashMap Name Level := HashMap.ofList ul
+      let thTy := thDecl.type.instantiateLevelParamsCore (λ x => ulMap.find! x)
+      pure thTy
     | .Local asmDecl => pure asmDecl.type
   trace[Progress] "Looked up theorem/assumption type: {thTy}"
   -- TODO: the tactic fails if we uncomment withNewMCtxDepth
@@ -129,15 +135,16 @@ def progressWith (fExpr : Expr) (th : TheoremOrLocal)
              Split the remaining conjunctions by using fresh ids if the user
              instructed to fully split the post-condition, otherwise stop -/
           if splitPost then
-            splitFullConjTac hPost (λ _ => pure .Ok)
+            splitFullConjTac true hPost (λ _ => pure .Ok)
           else pure .Ok
         | nid :: ids => do
-          trace[Progress] "Splitting post: {hPost}"
+          trace[Progress] "Splitting post: {← inferType hPost}"
           -- Split
           let nid ← do
             match nid with
             | none => mkFreshUserName `h
             | some nid => pure nid
+          trace[Progress] "\n- prevId: {prevId}\n- nid: {nid}\n- remaining ids: {ids}"
           if ← isConj (← inferType hPost) then
             splitConjTac hPost (some (prevId, nid)) (λ _ nhPost => splitPostWithIds nid nhPost ids)
           else return (.Error m!"Too many ids provided ({ids0}) not enough conjuncts to split in the postcondition")
@@ -323,7 +330,7 @@ def evalProgress (args : TSyntax `Progress.progressArgs) : TacticM Unit := do
 elab "progress" args:progressArgs : tactic =>
   evalProgress args
 
-/- namespace Test
+namespace Test
   open Primitives Result
 
   set_option trace.Progress true
@@ -336,10 +343,25 @@ elab "progress" args:progressArgs : tactic =>
     (hmin : Scalar.min ty ≤ x.val + y.val)
     (hmax : x.val + y.val ≤ Scalar.max ty) :
     ∃ z, x + y = ret z ∧ z.val = x.val + y.val := by
---    progress keep as h with Scalar.add_spec as ⟨ z ⟩
     progress keep as h as ⟨ x, h1 .. ⟩
     simp [*]
 
-end Test -/
+  example {ty} {x y : Scalar ty}
+    (hmin : Scalar.min ty ≤ x.val + y.val)
+    (hmax : x.val + y.val ≤ Scalar.max ty) :
+    ∃ z, x + y = ret z ∧ z.val = x.val + y.val := by
+    progress keep as h with Scalar.add_spec as ⟨ z ⟩
+    simp [*]
+
+  /- Checking that universe instantiation works: the original spec uses
+     `α : 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.val = v.val.update i.val x := by
+    progress
+    simp [*]
+
+end Test
 
 end Progress
diff --git a/backends/lean/Base/Utils.lean b/backends/lean/Base/Utils.lean
index 66497a49..f6dc45c7 100644
--- a/backends/lean/Base/Utils.lean
+++ b/backends/lean/Base/Utils.lean
@@ -1,6 +1,7 @@
 import Lean
 import Mathlib.Tactic.Core
 import Mathlib.Tactic.LeftRight
+import Base.UtilsBase
 
 /-
 Mathlib tactics:
@@ -331,13 +332,13 @@ def assumptionTac : TacticM Unit :=
   liftMetaTactic fun mvarId => do mvarId.assumption; pure []
 
 def isConj (e : Expr) : MetaM Bool :=
-  e.withApp fun f args => pure (f.isConstOf ``And ∧ args.size = 2)
+  e.consumeMData.withApp fun f args => pure (f.isConstOf ``And ∧ args.size = 2)
 
 -- Return the first conjunct if the expression is a conjunction, or the
 -- expression itself otherwise. Also return the second conjunct if it is a
 -- conjunction.
 def optSplitConj (e : Expr) : MetaM (Expr × Option Expr) := do
-  e.withApp fun f args =>
+  e.consumeMData.withApp fun f args =>
   if f.isConstOf ``And ∧ args.size = 2 then pure (args.get! 0, some (args.get! 1))
   else pure (e, none)
 
@@ -345,6 +346,7 @@ def optSplitConj (e : Expr) : MetaM (Expr × Option Expr) := do
 def splitConjTarget : TacticM Unit := do
   withMainContext do
   let g ← getMainTarget
+  trace[Utils] "splitConjTarget: goal: {g}"
   -- The tactic was initially implemened with `_root_.Lean.MVarId.apply`
   -- but it tended to mess the goal by unfolding terms, even when it failed
   let (l, r) ← optSplitConj g
@@ -525,18 +527,26 @@ def splitConjTac (h : Expr) (optIds : Option (Name × Name)) (k : Expr → Expr
     throwError "Not a conjunction"
 
 -- Tactic to fully split a conjunction
-partial def splitFullConjTacAux [Inhabited α] [Nonempty α] (l : List Expr) (h : Expr) (k : List Expr → TacticM α)  : TacticM α := do
+partial def splitFullConjTacAux [Inhabited α] [Nonempty α] (keepCurrentName : Bool) (l : List Expr) (h : Expr) (k : List Expr → TacticM α)  : TacticM α := do
   try
-    splitConjTac h none (λ h1 h2 =>
-      splitFullConjTacAux l h1 (λ l1 =>
-        splitFullConjTacAux l1 h2 (λ l2 =>
+    let ids ← do
+      if keepCurrentName then do
+        let cur := (← h.fvarId!.getDecl).userName
+        let nid ← mkFreshUserName `h
+        pure (some (cur, nid))
+      else
+        pure none
+    splitConjTac h ids (λ h1 h2 =>
+      splitFullConjTacAux keepCurrentName l h1 (λ l1 =>
+        splitFullConjTacAux keepCurrentName l1 h2 (λ l2 =>
           k l2)))
   catch _ =>
     k (h :: l)
 
 -- Tactic to fully split a conjunction
-def splitFullConjTac [Inhabited α] [Nonempty α] (h : Expr) (k : List Expr → TacticM α)  : TacticM α := do
-  splitFullConjTacAux [] h (λ l => k l.reverse)
+-- `keepCurrentName`: if `true`, then the first conjunct has the name of the original assumption
+def splitFullConjTac [Inhabited α] [Nonempty α] (keepCurrentName : Bool) (h : Expr) (k : List Expr → TacticM α)  : TacticM α := do
+  splitFullConjTacAux keepCurrentName [] h (λ l => k l.reverse)
 
 syntax optAtArgs := ("at" ident)?
 def elabOptAtArgs (args : TSyntax `Utils.optAtArgs) : TacticM (Option Expr) := do
@@ -553,17 +563,21 @@ def elabOptAtArgs (args : TSyntax `Utils.optAtArgs) : TacticM (Option Expr) := d
 elab "split_conj" args:optAtArgs : tactic => do
   withMainContext do
   match ← elabOptAtArgs args with
-  | some fvar =>
+  | some fvar => do
+    trace[Utils] "split at {fvar}"
     splitConjTac fvar none (fun _ _ =>  pure ())
-  | none =>
+  | none => do
+    trace[Utils] "split goal"
     splitConjTarget
 
 elab "split_conjs" args:optAtArgs : tactic => do
   withMainContext do
   match ← elabOptAtArgs args with
   | some fvar =>
-    splitFullConjTac fvar (fun _ =>  pure ())
+    trace[Utils] "split at {fvar}"
+    splitFullConjTac false fvar (fun _ =>  pure ())
   | none =>
+    trace[Utils] "split goal"
     repeatTac splitConjTarget
 
 elab "split_existsl" " at " n:ident : tactic => do
diff --git a/tests/lean/Hashmap/Properties.lean b/tests/lean/Hashmap/Properties.lean
index b2d5570a..92285c0d 100644
--- a/tests/lean/Hashmap/Properties.lean
+++ b/tests/lean/Hashmap/Properties.lean
@@ -55,6 +55,7 @@ theorem match_lawful_beq [BEq α] [LawfulBEq α] [DecidableEq α] (x y : α) :
   (x == y) = (if x = y then true else false) := by
   split <;> simp_all
 
+@[pspec]
 theorem insert_in_list_spec0 {α : Type} (key: Usize) (value: α) (ls: List α) :
   ∃ b,
     insert_in_list α key value ls = ret b ∧
@@ -126,6 +127,10 @@ def hash_mod_key (k : Usize) (l : Int) : Int :=
   | .ret k => k.val % l
   | _ => 0
 
+@[simp]
+theorem hash_mod_key_eq : hash_mod_key k l = k.val % l := by
+  simp [hash_mod_key, hash_key]
+
 def slot_s_inv_hash (l i : Int) (ls : Core.List (Usize × α)) : Prop :=
   ls.allP (λ (k, _) => hash_mod_key k l = i)
 
@@ -246,6 +251,7 @@ theorem insert_in_list_back_spec {α : Type} (l : Int) (key: Usize) (value: α)
   progress with insert_in_list_back_spec_aux as ⟨ l1 .. ⟩
   exists l1
 
+@[simp]
 def slots_t_lookup (s : Core.List (List α)) (k : Usize) : Option α :=
   let i := hash_mod_key k s.len
   let slot := s.index i
@@ -260,7 +266,15 @@ abbrev len_s (hm : HashMap α) : Int := hm.al_v.len
 set_option trace.Progress true
 /-set_option pp.explicit true
 set_option pp.universes true
-set_option pp.notation false-/
+set_option pp.notation false -/
+
+-- Remark: α and β must live in the same universe, otherwise the
+-- bind doesn't work
+theorem if_update_eq
+  {α β : Type u} (b : Bool) (y : α) (e : Result α) (f : α → Result β) :
+  (if b then Bind.bind e f else f y) = Bind.bind (if b then e else pure y) f
+  := by
+  split <;> simp [Pure.pure]
 
 theorem insert_no_resize_spec {α : Type} (hm : HashMap α) (key : Usize) (value : α)
   (hinv : hm.inv) (hnsat : hm.lookup key = none → hm.len_s < Usize.max) :
@@ -270,18 +284,112 @@ theorem insert_no_resize_spec {α : Type} (hm : HashMap α) (key : Usize) (value
   -- We updated the binding for key
   nhm.lookup key = some value ∧
   -- We left the other bindings unchanged
-  (∀ k, k ≠ key → nhm.lookup k = hm.lookup k) ∧
+  (∀ k, ¬ k = key → nhm.lookup k = hm.lookup k) ∧
   -- Reasoning about the length
   (match hm.lookup key with
    | none => nhm.len_s = hm.len_s + 1
    | some _ => nhm.len_s = hm.len_s) := by
   rw [insert_no_resize]
   simp [hash_key]
-  have : (Vec.len (List α) hm.slots).val ≠ 0 := by
+  have _ : (Vec.len (List α) hm.slots).val ≠ 0 := by checkpoint
    intro
    simp_all [inv]
-  progress as ⟨ hash_mod ⟩
+  -- TODO: progress keep as ⟨ ... ⟩ : conflict
+  progress keep as h as ⟨ hash_mod, hhm ⟩
+  have _ : 0 ≤ hash_mod.val := by checkpoint scalar_tac
+  have _ : hash_mod.val < Vec.length hm.slots := by sorry
+  -- have h := Primitives.Vec.index_mut_spec hm.slots hash_mod
+  -- TODO: change the spec of Vec.index_mut to introduce a let-binding.
+  -- or: make progress introduce the let-binding by itself (this is clearer)
   progress
+  -- TODO: make progress use the names written in the goal
+  progress as ⟨ inserted ⟩
+  rw [if_update_eq] -- TODO: necessary because we don't have a join
+  -- TODO: progress to ...
+  have hipost :
+    ∃ i0, (if inserted = true then hm.num_entries + Usize.ofInt 1 else pure hm.num_entries) = ret i0 ∧
+    i0.val = if inserted then hm.num_entries.val + 1 else hm.num_entries.val
+    := by sorry
+  progress as ⟨ i0 ⟩
+  -- TODO: progress "eager" to match premises with assumptions while instantiating
+  -- meta-variables
+  have h_slot : slot_s_inv_hash hm.slots.length hash_mod.val (hm.slots.v.index hash_mod.val).v := by sorry
+  have hd : distinct_keys (hm.slots.v.index hash_mod.val).v := by checkpoint
+    simp [inv, slots_t_inv, slot_t_inv] at hinv
+    have h := hinv.right.left hash_mod.val (by assumption) (by assumption)
+    simp [h]
+  -- TODO: hide the variables and only keep the props
+  -- TODO: allow providing terms to progress to instantiate the meta variables
+  -- which are not propositions
+  progress as ⟨ l0, _, _, _, hlen .. ⟩
+  . checkpoint exact hm.slots.length
+  . checkpoint simp_all
+  . -- Finishing the proof
+    progress as ⟨ v ⟩
+    -- TODO: update progress to automate that
+    let nhm : HashMap α := { num_entries := i0, max_load_factor := hm.max_load_factor, max_load := hm.max_load, slots := v }
+    exists nhm
+    have hupdt : lookup nhm key = some value := by checkpoint
+      simp [lookup, List.lookup] at *
+      simp_all
+    have hlkp : ∀ k, ¬ k = key → nhm.lookup k = hm.lookup k := by checkpoint
+      simp [lookup, List.lookup] at *
+      intro k hk
+      -- We have to make a case disjunction: either the hashes are different,
+      -- in which case we don't even lookup the same slots, or the hashes
+      -- are the same, in which case we have to reason about what happens
+      -- in one slot
+      let k_hash_mod := k.val % v.val.len
+      have _ : 0 ≤ k_hash_mod := by sorry
+      have _ : k_hash_mod < Vec.length hm.slots := by sorry
+      if h_hm : k_hash_mod = hash_mod.val then
+        simp_all
+      else
+        simp_all
+    have _ :
+      match hm.lookup key with
+      | none => nhm.len_s = hm.len_s + 1
+      | some _ => nhm.len_s = hm.len_s := by checkpoint
+      simp only [lookup, List.lookup, len_s, al_v, HashMap.v, slots_t_lookup] at *
+      -- We have to do a case disjunction
+      simp_all
+      simp [_root_.List.update_map_eq]
+      -- TODO: dependent rewrites
+      have _ : key.val % hm.slots.val.len < (List.map List.v hm.slots.val).len := by
+        simp [*]
+      simp [_root_.List.len_flatten_update_eq, *]
+      split <;>
+      rename_i heq <;>
+      simp [heq] at hlen <;>
+      -- TODO: canonize addition by default? We need a tactic to simplify arithmetic equalities
+      -- with addition and substractions ((ℤ, +) is a ring or something - there should exist a tactic
+      -- somewhere in mathlib?)
+      simp [Int.add_assoc, Int.add_comm, Int.add_left_comm] <;>
+      int_tac
+    have hinv : inv nhm := by
+      simp [inv] at *
+      split_conjs
+      . match h: lookup hm key with
+        | none =>
+          simp [h, lookup] at *
+          simp_all
+        | some _ =>
+          simp_all [lookup]
+      . simp [slots_t_inv, slot_t_inv] at *
+        intro i hipos _
+        have hs := hinv.right.left i hipos (by simp_all)
+        -- We need a case disjunction
+        if i = key.val % _root_.List.len hm.slots.val then
+          simp_all
+        else
+          simp_all
+      . match h: lookup hm key with
+        | none =>
+          simp [h] at *
+          simp [*]
+        | some _ =>
+          simp_all
+    simp_all
 
 end HashMap
 
-- 
cgit v1.3.1


From 9e8fccbe4b667fc341b6544030f85af05fe89307 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Tue, 25 Jul 2023 20:12:48 +0200
Subject: Make progress on the proofs of the hashmap

---
 backends/lean/Base/Primitives/Scalar.lean | 47 ++++++++++++++++++++++---
 tests/lean/Hashmap/Properties.lean        | 58 +++++++++++++++++++++----------
 2 files changed, 83 insertions(+), 22 deletions(-)

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

diff --git a/backends/lean/Base/Primitives/Scalar.lean b/backends/lean/Base/Primitives/Scalar.lean
index 3beb7527..2e5be8bf 100644
--- a/backends/lean/Base/Primitives/Scalar.lean
+++ b/backends/lean/Base/Primitives/Scalar.lean
@@ -660,10 +660,8 @@ theorem Scalar.rem_unsigned_spec {ty} (s: ¬ ty.isSigned) (x : Scalar ty) {y : S
   simp [h] at hx hy
   have hmin : 0 ≤ x.val % y.val := Int.emod_nonneg x.val hnz
   have hmax : x.val % y.val ≤ Scalar.max ty := by
-    have h := @Int.ediv_emod_unique x.val y.val (x.val % y.val) (x.val / y.val)
-    simp at h
-    have : 0 < y.val := by int_tac
-    simp [*] at h
+    have h : 0 < y.val := by int_tac
+    have h := Int.emod_lt_of_pos x.val h
     have := y.hmax
     linarith
   have hs := @rem_spec ty x y hnz
@@ -724,6 +722,47 @@ def U32.ofInt   := @Scalar.ofInt .U32
 def U64.ofInt   := @Scalar.ofInt .U64
 def 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.ofInt x h).val = x := by
+  simp [Scalar.ofInt, Scalar.ofIntCore]
+
+@[simp] theorem Isize.ofInt_val_eq (h : Scalar.min ScalarTy.Isize ≤ x ∧ x ≤ Scalar.max ScalarTy.Isize) : (Isize.ofInt x h).val = x := by
+  apply Scalar.ofInt_val_eq h
+
+@[simp] theorem I8.ofInt_val_eq (h : Scalar.min ScalarTy.I8 ≤ x ∧ x ≤ Scalar.max ScalarTy.I8) : (I8.ofInt x h).val = x := by
+  apply Scalar.ofInt_val_eq h
+
+@[simp] theorem I16.ofInt_val_eq (h : Scalar.min ScalarTy.I16 ≤ x ∧ x ≤ Scalar.max ScalarTy.I16) : (I16.ofInt x h).val = x := by
+  apply Scalar.ofInt_val_eq h
+
+@[simp] theorem I32.ofInt_val_eq (h : Scalar.min ScalarTy.I32 ≤ x ∧ x ≤ Scalar.max ScalarTy.I32) : (I32.ofInt x h).val = x := by
+  apply Scalar.ofInt_val_eq h
+
+@[simp] theorem I64.ofInt_val_eq (h : Scalar.min ScalarTy.I64 ≤ x ∧ x ≤ Scalar.max ScalarTy.I64) : (I64.ofInt x h).val = x := by
+  apply Scalar.ofInt_val_eq h
+
+@[simp] theorem I128.ofInt_val_eq (h : Scalar.min ScalarTy.I128 ≤ x ∧ x ≤ Scalar.max ScalarTy.I128) : (I128.ofInt x h).val = x := by
+  apply Scalar.ofInt_val_eq h
+
+@[simp] theorem Usize.ofInt_val_eq (h : Scalar.min ScalarTy.Usize ≤ x ∧ x ≤ Scalar.max ScalarTy.Usize) : (Usize.ofInt x h).val = x := by
+  apply Scalar.ofInt_val_eq h
+
+@[simp] theorem U8.ofInt_val_eq (h : Scalar.min ScalarTy.U8 ≤ x ∧ x ≤ Scalar.max ScalarTy.U8) : (U8.ofInt x h).val = x := by
+  apply Scalar.ofInt_val_eq h
+
+@[simp] theorem U16.ofInt_val_eq (h : Scalar.min ScalarTy.U16 ≤ x ∧ x ≤ Scalar.max ScalarTy.U16) : (U16.ofInt x h).val = x := by
+  apply Scalar.ofInt_val_eq h
+
+@[simp] theorem U32.ofInt_val_eq (h : Scalar.min ScalarTy.U32 ≤ x ∧ x ≤ Scalar.max ScalarTy.U32) : (U32.ofInt x h).val = x := by
+  apply Scalar.ofInt_val_eq h
+
+@[simp] theorem U64.ofInt_val_eq (h : Scalar.min ScalarTy.U64 ≤ x ∧ x ≤ Scalar.max ScalarTy.U64) : (U64.ofInt x h).val = x := by
+  apply Scalar.ofInt_val_eq h
+
+@[simp] theorem U128.ofInt_val_eq (h : Scalar.min ScalarTy.U128 ≤ x ∧ x ≤ Scalar.max ScalarTy.U128) : (U128.ofInt x h).val = x := by
+  apply Scalar.ofInt_val_eq h
+
+
 -- Comparisons
 instance {ty} : LT (Scalar ty) where
   lt a b := LT.lt a.val b.val
diff --git a/tests/lean/Hashmap/Properties.lean b/tests/lean/Hashmap/Properties.lean
index 92285c0d..40b5009d 100644
--- a/tests/lean/Hashmap/Properties.lean
+++ b/tests/lean/Hashmap/Properties.lean
@@ -263,11 +263,6 @@ def lookup (hm : HashMap α) (k : Usize) : Option α :=
 @[simp]
 abbrev len_s (hm : HashMap α) : Int := hm.al_v.len
 
-set_option trace.Progress true
-/-set_option pp.explicit true
-set_option pp.universes true
-set_option pp.notation false -/
-
 -- Remark: α and β must live in the same universe, otherwise the
 -- bind doesn't work
 theorem if_update_eq
@@ -297,7 +292,12 @@ theorem insert_no_resize_spec {α : Type} (hm : HashMap α) (key : Usize) (value
   -- TODO: progress keep as ⟨ ... ⟩ : conflict
   progress keep as h as ⟨ hash_mod, hhm ⟩
   have _ : 0 ≤ hash_mod.val := by checkpoint scalar_tac
-  have _ : hash_mod.val < Vec.length hm.slots := by sorry
+  have _ : hash_mod.val < Vec.length hm.slots := by
+    have : 0 < hm.slots.val.len := by
+      simp [inv] at hinv
+      simp [hinv]
+    -- TODO: we want to automate that
+    simp [*, Int.emod_lt_of_pos]
   -- have h := Primitives.Vec.index_mut_spec hm.slots hash_mod
   -- TODO: change the spec of Vec.index_mut to introduce a let-binding.
   -- or: make progress introduce the let-binding by itself (this is clearer)
@@ -309,11 +309,26 @@ theorem insert_no_resize_spec {α : Type} (hm : HashMap α) (key : Usize) (value
   have hipost :
     ∃ i0, (if inserted = true then hm.num_entries + Usize.ofInt 1 else pure hm.num_entries) = ret i0 ∧
     i0.val = if inserted then hm.num_entries.val + 1 else hm.num_entries.val
-    := by sorry
+    := by
+    if inserted then
+      simp [*]
+      have : hm.num_entries.val + (Usize.ofInt 1).val ≤ Usize.max := by
+        simp [lookup] at hnsat
+        simp_all
+        simp [inv] at hinv
+        int_tac
+      progress
+      simp_all
+    else
+      simp_all [Pure.pure]
   progress as ⟨ i0 ⟩
   -- TODO: progress "eager" to match premises with assumptions while instantiating
   -- meta-variables
-  have h_slot : slot_s_inv_hash hm.slots.length hash_mod.val (hm.slots.v.index hash_mod.val).v := by sorry
+  have h_slot : slot_s_inv_hash hm.slots.length hash_mod.val (hm.slots.v.index hash_mod.val).v := by
+    simp [inv] at hinv
+    have h := hinv.right.left hash_mod.val (by assumption) (by assumption)
+    simp [slot_t_inv] at h
+    simp [h]
   have hd : distinct_keys (hm.slots.v.index hash_mod.val).v := by checkpoint
     simp [inv, slots_t_inv, slot_t_inv] at hinv
     have h := hinv.right.left hash_mod.val (by assumption) (by assumption)
@@ -329,10 +344,11 @@ theorem insert_no_resize_spec {α : Type} (hm : HashMap α) (key : Usize) (value
     -- TODO: update progress to automate that
     let nhm : HashMap α := { num_entries := i0, max_load_factor := hm.max_load_factor, max_load := hm.max_load, slots := v }
     exists nhm
+    -- TODO: later I don't want to inline nhm - we need to control simp
     have hupdt : lookup nhm key = some value := by checkpoint
       simp [lookup, List.lookup] at *
       simp_all
-    have hlkp : ∀ k, ¬ k = key → nhm.lookup k = hm.lookup k := by checkpoint
+    have hlkp : ∀ k, ¬ k = key → nhm.lookup k = hm.lookup k := by
       simp [lookup, List.lookup] at *
       intro k hk
       -- We have to make a case disjunction: either the hashes are different,
@@ -340,8 +356,19 @@ theorem insert_no_resize_spec {α : Type} (hm : HashMap α) (key : Usize) (value
       -- are the same, in which case we have to reason about what happens
       -- in one slot
       let k_hash_mod := k.val % v.val.len
-      have _ : 0 ≤ k_hash_mod := by sorry
-      have _ : k_hash_mod < Vec.length hm.slots := by sorry
+      have : 0 < hm.slots.val.len := by simp_all [inv]
+      have hvpos : 0 < v.val.len := by simp_all
+      have hvnz: v.val.len ≠ 0 := by
+        simp_all
+      have _ : 0 ≤ k_hash_mod := by
+        -- TODO: we want to automate this
+        simp
+        apply Int.emod_nonneg k.val hvnz
+      have _ : k_hash_mod < Vec.length hm.slots := by
+        -- TODO: we want to automate this
+        simp
+        have h := Int.emod_lt_of_pos k.val hvpos
+        simp_all
       if h_hm : k_hash_mod = hash_mod.val then
         simp_all
       else
@@ -377,18 +404,13 @@ theorem insert_no_resize_spec {α : Type} (hm : HashMap α) (key : Usize) (value
           simp_all [lookup]
       . simp [slots_t_inv, slot_t_inv] at *
         intro i hipos _
-        have hs := hinv.right.left i hipos (by simp_all)
+        have _ := hinv.right.left i hipos (by simp_all)
         -- We need a case disjunction
         if i = key.val % _root_.List.len hm.slots.val then
           simp_all
         else
           simp_all
-      . match h: lookup hm key with
-        | none =>
-          simp [h] at *
-          simp [*]
-        | some _ =>
-          simp_all
+      . simp_all
     simp_all
 
 end HashMap
-- 
cgit v1.3.1


From 3337c4ac3326c3132dcc322f55f23a7d2054ceb0 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Wed, 26 Jul 2023 15:00:11 +0200
Subject: Update some of the Vec function specs

---
 backends/lean/Base/Primitives/Vec.lean    | 13 ++++++++----
 backends/lean/Base/Progress/Progress.lean | 17 ++++++++++-----
 tests/lean/Hashmap/Properties.lean        | 35 +++++++++++++++++--------------
 3 files changed, 40 insertions(+), 25 deletions(-)

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

diff --git a/backends/lean/Base/Primitives/Vec.lean b/backends/lean/Base/Primitives/Vec.lean
index 523372bb..a09d6ac2 100644
--- a/backends/lean/Base/Primitives/Vec.lean
+++ b/backends/lean/Base/Primitives/Vec.lean
@@ -85,14 +85,19 @@ def Vec.index (α : Type u) (v: Vec α) (i: Usize) : Result α :=
   | none => fail .arrayOutOfBounds
   | some x => ret x
 
+/- In the theorems below: we don't always need the `∃ ..`, but we use one
+   so that `progress` introduces an opaque variable and an equality. This
+   helps control the context.
+ -/
+
 @[pspec]
 theorem Vec.index_spec {α : Type u} [Inhabited α] (v: Vec α) (i: Usize)
   (hbound : i.val < v.length) :
-  v.index α i = ret (v.val.index i.val) := by
+  ∃ x, v.index α i = ret x ∧ x = v.val.index i.val := by
   simp only [index]
   -- TODO: dependent rewrite
   have h := List.indexOpt_eq_index v.val i.val (by scalar_tac) (by simp [*])
-  simp only [*]
+  simp [*]
 
 -- This shouldn't be used
 def Vec.index_back (α : Type u) (v: Vec α) (i: Usize) (_: α) : Result Unit :=
@@ -109,11 +114,11 @@ def Vec.index_mut (α : Type u) (v: Vec α) (i: Usize) : Result α :=
 @[pspec]
 theorem Vec.index_mut_spec {α : Type u} [Inhabited α] (v: Vec α) (i: Usize)
   (hbound : i.val < v.length) :
-  v.index_mut α i = ret (v.val.index i.val) := by
+  ∃ x, v.index_mut α i = ret x ∧ x = v.val.index i.val := by
   simp only [index_mut]
   -- TODO: dependent rewrite
   have h := List.indexOpt_eq_index v.val i.val (by scalar_tac) (by simp [*])
-  simp only [*]
+  simp [*]
 
 instance {α : Type u} (p : Vec α → Prop) : Arith.HasIntProp (Subtype p) where
   prop_ty := λ x => p x
diff --git a/backends/lean/Base/Progress/Progress.lean b/backends/lean/Base/Progress/Progress.lean
index 9300edff..6a4729dc 100644
--- a/backends/lean/Base/Progress/Progress.lean
+++ b/backends/lean/Base/Progress/Progress.lean
@@ -162,6 +162,7 @@ def progressWith (fExpr : Expr) (th : TheoremOrLocal)
     allGoals asmTac
     let newGoals ← getUnsolvedGoals
     setGoals (newGoals ++ curGoals)
+    trace[Progress] "progress: replaced the goals"
     --
     pure .Ok
 
@@ -281,12 +282,15 @@ def evalProgress (args : TSyntax `Progress.progressArgs) : TacticM Unit := do
     | [keepArg, withArg, asArgs] => do pure (keepArg, withArg, asArgs)
     | _ => throwError "Unexpected: invalid arguments"
   let keep : Option Name ← do
+    trace[Progress] "Keep arg: {keepArg}"
     let args := keepArg.getArgs
-    trace[Progress] "Keep args: {args}"
-    let arg := args.get! 1
-    trace[Progress] "Keep arg: {arg}"
-    if arg.isIdent then pure (some arg.getId)
-    else do pure (some (← mkFreshAnonPropUserName))
+    if args.size > 0 then do
+      trace[Progress] "Keep args: {args}"
+      let arg := args.get! 1
+      trace[Progress] "Keep arg: {arg}"
+      if arg.isIdent then pure (some arg.getId)
+      else do pure (some (← mkFreshAnonPropUserName))
+    else do pure none
   trace[Progress] "Keep: {keep}"
   let withArg ← do
     let withArg := withArg.getArgs
@@ -328,7 +332,10 @@ def evalProgress (args : TSyntax `Progress.progressArgs) : TacticM Unit := do
     else
       throwError "Not a linear arithmetic goal"
   progressAsmsOrLookupTheorem keep withArg ids splitPost (
+    withMainContext do
+    trace[Progress] "trying to solve assumption: {← getMainGoal}"
     firstTac [assumptionTac, scalarTac])
+  trace[Diverge] "Progress done"
 
 elab "progress" args:progressArgs : tactic =>
   evalProgress args
diff --git a/tests/lean/Hashmap/Properties.lean b/tests/lean/Hashmap/Properties.lean
index 96b8193d..5d340b5c 100644
--- a/tests/lean/Hashmap/Properties.lean
+++ b/tests/lean/Hashmap/Properties.lean
@@ -285,7 +285,7 @@ theorem insert_no_resize_spec {α : Type} (hm : HashMap α) (key : Usize) (value
    | none => nhm.len_s = hm.len_s + 1
    | some _ => nhm.len_s = hm.len_s) := by
   rw [insert_no_resize]
-  simp [hash_key]
+  simp only [hash_key, bind_tc_ret] -- TODO: annoying
   have _ : (Vec.len (List α) hm.slots).val ≠ 0 := by checkpoint
    intro
    simp_all [inv]
@@ -297,10 +297,9 @@ theorem insert_no_resize_spec {α : Type} (hm : HashMap α) (key : Usize) (value
       simp [hinv]
     -- TODO: we want to automate that
     simp [*, Int.emod_lt_of_pos]
-  -- have h := Primitives.Vec.index_mut_spec hm.slots hash_mod
   -- TODO: change the spec of Vec.index_mut to introduce a let-binding.
   -- or: make progress introduce the let-binding by itself (this is clearer)
-  progress
+  progress as ⟨ l, h_leq ⟩
   -- TODO: make progress use the names written in the goal
   progress as ⟨ inserted ⟩
   rw [if_update_eq] -- TODO: necessary because we don't have a join
@@ -311,38 +310,42 @@ theorem insert_no_resize_spec {α : Type} (hm : HashMap α) (key : Usize) (value
     := by
     if inserted then
       simp [*]
-      have : hm.num_entries.val + (Usize.ofInt 1).val ≤ Usize.max := by
+      have hbounds : hm.num_entries.val + (Usize.ofInt 1).val ≤ Usize.max := by
         simp [lookup] at hnsat
         simp_all
         simp [inv] at hinv
         int_tac
-      progress
-      simp_all
+      -- TODO: progress fails in command line mode with "index out of bounds"
+      -- and I have no idea how to fix this. The error happens after progress
+      -- introduced the new goals. It must be when we exit the "withApp", etc.
+      -- helpers.
+      have ⟨ z, hp ⟩ := Usize.add_spec hbounds
+      simp [hp]
     else
-      simp_all [Pure.pure]
+      simp [*, Pure.pure]
   progress as ⟨ i0 ⟩
   -- TODO: progress "eager" to match premises with assumptions while instantiating
   -- meta-variables
-  have h_slot : slot_s_inv_hash hm.slots.length (hash_mod_key key hm.slots.length)
-    (List.v (List.index (hm.slots.val) hash_mod.val)) := by
+  have h_slot : slot_s_inv_hash hm.slots.length (hash_mod_key key hm.slots.length) l.v
+    := by
     simp [inv] at hinv
     have h := (hinv.right.left hash_mod.val (by assumption) (by assumption)).right
     simp [slot_t_inv, hhm] at h
-    simp [h, hhm]
-  have hd : distinct_keys (hm.slots.v.index hash_mod.val).v := by checkpoint
+    simp [h, hhm, h_leq]
+  have hd : distinct_keys l.v := by checkpoint
     simp [inv, slots_t_inv, slot_t_inv] at hinv
     have h := hinv.right.left hash_mod.val (by assumption) (by assumption)
-    simp [h]
+    simp [h, h_leq]
   -- TODO: hide the variables and only keep the props
   -- TODO: allow providing terms to progress to instantiate the meta variables
   -- which are not propositions
   progress as ⟨ l0, _, _, _, hlen .. ⟩
-  -- Finishing the proof
   progress keep hv as ⟨ v, h_veq ⟩
   -- TODO: update progress to automate that
   let nhm : HashMap α := { num_entries := i0, max_load_factor := hm.max_load_factor, max_load := hm.max_load, slots := v }
   exists nhm
-  -- TODO: later I don't want to inline nhm - we need to control simp
+  -- TODO: later I don't want to inline nhm - we need to control simp: deactivate
+  -- zeta reduction?
   have hupdt : lookup nhm key = some value := by checkpoint
     simp [lookup, List.lookup] at *
     simp_all
@@ -387,7 +390,7 @@ theorem insert_no_resize_spec {α : Type} (hm : HashMap α) (key : Usize) (value
     rename_i heq <;>
     simp [heq] at hlen <;>
     -- TODO: canonize addition by default? We need a tactic to simplify arithmetic equalities
-    -- with addition and substractions ((ℤ, +) is a ring or something - there should exist a tactic
+    -- with addition and substractions ((ℤ, +) is a group or something - there should exist a tactic
     -- somewhere in mathlib?)
     simp [Int.add_assoc, Int.add_comm, Int.add_left_comm] <;>
     int_tac
@@ -403,7 +406,7 @@ theorem insert_no_resize_spec {α : Type} (hm : HashMap α) (key : Usize) (value
     . simp [slots_t_inv, slot_t_inv] at *
       intro i hipos _
       have _ := hinv.right.left i hipos (by simp_all)
-      simp [hhm, h_veq] at * -- TODO: annoying
+      simp [hhm, h_veq] at * -- TODO: annoying, we do that because simp_all fails below
       -- We need a case disjunction
       if h_ieq : i = key.val % _root_.List.len hm.slots.val then
         -- TODO: simp_all fails: "(deterministic) timeout at 'whnf'"
-- 
cgit v1.3.1