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/IList/IList.lean | 142 ++++++++++++++++++++++++++++++++++++
 1 file changed, 142 insertions(+)
 create mode 100644 backends/lean/Base/IList/IList.lean

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

diff --git a/backends/lean/Base/IList/IList.lean b/backends/lean/Base/IList/IList.lean
new file mode 100644
index 00000000..2a335cac
--- /dev/null
+++ b/backends/lean/Base/IList/IList.lean
@@ -0,0 +1,142 @@
+/- Complementary list functions and lemmas which operate on integers rather
+   than natural numbers. -/
+
+import Std.Data.Int.Lemmas
+import Base.Arith
+
+namespace List
+
+def len (ls : List α) : Int :=
+  match ls with
+  | [] => 0
+  | _ :: tl => 1 + len tl
+
+-- 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)
+
+-- Remark: if i < 0, then the result is the defaul element
+def index [Inhabited α] (ls : List α) (i : Int) : α :=
+  match ls with
+  | [] => Inhabited.default
+  | x :: tl =>
+    if i = 0 then x else index tl (i - 1)
+
+-- 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 α :=
+  match ls with
+  | [] => []
+  | x :: tl => if i = 0 then y :: tl else x :: update tl (i - 1) y
+
+-- Remark: the whole list is dropped if the index is not in bounds (in particular
+-- if it is < 0)
+def idrop (i : Int) (ls : List α) : List α :=
+  match ls with
+  | [] => []
+  | x :: tl => if i = 0 then x :: tl else idrop (i - 1) tl
+
+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]
+
+@[simp] theorem idrop_nil : idrop i ([] : List α) = [] := by simp [idrop]
+@[simp] theorem idrop_zero : idrop 0 (ls : List α) = ls := by cases ls <;> simp [idrop]
+@[simp] theorem idrop_nzero_cons (hne : i ≠ 0) : idrop i ((x :: tl) : List α) = idrop (i - 1) tl := by simp [*, idrop]
+
+theorem len_eq_length (ls : List α) : ls.len = ls.length := by
+  induction ls
+  . rfl
+  . simp [*, Int.ofNat_succ, Int.add_comm]
+
+@[simp] theorem len_append (l1 l2 : List α) : (l1 ++ l2).len = l1.len + l2.len := by
+  -- Remark: simp loops here because of the following rewritings:
+  -- @Nat.cast_add: ↑(List.length l1 + List.length l2) ==> ↑(List.length l1) + ↑(List.length l2)
+  -- Int.ofNat_add_ofNat: ↑(List.length l1) + ↑(List.length l2) ==> ↑(List.length l1 + List.length l2)
+  -- TODO: post an issue?
+  simp only [len_eq_length]
+  simp only [length_append]
+  simp only [Int.ofNat_add]
+
+@[simp]
+theorem length_update (ls : List α) (i : Int) (x : α) : (ls.update i x).length = ls.length := by
+  revert i
+  induction ls <;> simp_all [length, update]
+  intro; split <;> simp [*]
+
+@[simp]
+theorem len_update (ls : List α) (i : Int) (x : α) : (ls.update i x).len = ls.len := by
+  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'
+  induction l1
+  . intro l1'; cases l1' <;> simp [*]
+  . intro l1'; cases l1' <;> simp_all; tauto
+
+theorem right_length_eq_append_eq (l1 l2 l1' l2' : List α) (heq : l2.length = l2'.length) :
+  l1 ++ l2 = l1' ++ l2' ↔ l1 = l1' ∧ l2 = l2' := by
+  have := left_length_eq_append_eq l1 l2 l1' l2'
+  constructor <;> intro heq2 <;>
+  have : l1.length + l2.length = l1'.length + l2'.length := by
+    have : (l1 ++ l2).length = (l1' ++ l2').length := by simp [*]
+    simp only [length_append] at this
+    apply this
+  . simp [heq] at this
+    tauto
+  . tauto
+
+theorem left_len_eq_append_eq (l1 l2 l1' l2' : List α) (heq : l1.len = l1'.len) :
+  l1 ++ l2 = l1' ++ l2' ↔ l1 = l1' ∧ l2 = l2' := by
+  simp [len_eq_length] at heq
+  apply left_length_eq_append_eq
+  assumption
+
+theorem right_len_eq_append_eq (l1 l2 l1' l2' : List α) (heq : l2.len = l2'.len) :
+  l1 ++ l2 = l1' ++ l2' ↔ l1 = l1' ∧ l2 = l2' := by
+  simp [len_eq_length] at heq
+  apply right_length_eq_append_eq
+  assumption
+
+open Arith in
+theorem idrop_eq_nil_of_le (hineq : ls.len ≤ i) : idrop i ls = [] := by
+  revert i
+  induction ls <;> simp [*]
+  rename_i hd tl hi
+  intro i hineq
+  if heq: i = 0 then
+    simp [*] at *
+    have := tl.len_pos
+    linarith
+  else
+    simp at hineq
+    have : 0 < i := by int_tac
+    simp [*]
+    apply hi
+    linarith
+
+end Lemmas
+
+end List
-- 
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/IList')

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 6ef1d360b89fd9f9383e63609888bf925a6a16ab Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Thu, 20 Jul 2023 12:08:09 +0200
Subject: Improve progress further and move some lemmas

---
 backends/lean/Base/IList/IList.lean       | 67 ++++++++++++++++++++++
 backends/lean/Base/Progress/Progress.lean | 55 +++++++++++-------
 tests/lean/Hashmap/Properties.lean        | 92 +++----------------------------
 3 files changed, 109 insertions(+), 105 deletions(-)

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

diff --git a/backends/lean/Base/IList/IList.lean b/backends/lean/Base/IList/IList.lean
index ddb10236..1773e593 100644
--- a/backends/lean/Base/IList/IList.lean
+++ b/backends/lean/Base/IList/IList.lean
@@ -175,6 +175,73 @@ theorem idrop_eq_nil_of_le (hineq : ls.len ≤ i) : idrop i ls = [] := by
     apply hi
     linarith
 
+@[simp]
+theorem index_ne
+  {α : Type u} [Inhabited α] (l: List α) (i: ℤ) (j: ℤ) (x: α) :
+   0 ≤ i → i < l.len → 0 ≤ j → j < l.len → j ≠ i →
+    (l.update i x).index j = l.index j
+  :=
+  λ _ _ _ _ _ => match l with
+  | [] => by simp at *
+  | hd :: tl =>
+    if h: i = 0 then
+      have : j ≠ 0 := by scalar_tac
+      by simp [*]
+    else if h : j = 0 then
+      have : i ≠ 0 := by scalar_tac
+      by simp [*]
+    else
+      by
+        simp [*]
+        simp at *
+        apply index_ne <;> scalar_tac
+
+@[simp]
+theorem index_eq
+  {α : Type u} [Inhabited α] (l: List α) (i: ℤ) (x: α) :
+   0 ≤ i → i < l.len →
+    (l.update i x).index i = x
+  :=
+  fun _ _ => match l with
+  | [] => by simp at *; exfalso; scalar_tac -- TODO: exfalso needed. Son FIXME
+  | hd :: tl =>
+    if h: i = 0 then
+      by
+        simp [*]
+    else
+      by
+        simp [*]
+        simp at *
+        apply index_eq <;> scalar_tac
+
+def allP {α : Type u} (l : List α) (p: α → Prop) : Prop :=
+  foldr (fun a r => p a ∧ r) True l
+
+@[simp]
+theorem allP_nil {α : Type u} (p: α → Prop) : allP [] p :=
+  by simp [allP, foldr]
+
+@[simp]
+theorem allP_cons {α : Type u} (hd: α) (tl : List α) (p: α → Prop) :
+  allP (hd :: tl) p ↔ p hd ∧ allP tl p
+  := by simp [allP, foldr]
+
+def pairwise_rel
+  {α : Type u} (rel : α → α → Prop) (l: List α) : Prop
+  := match l with
+  | [] => True
+  | hd :: tl => allP tl (rel hd) ∧ pairwise_rel rel tl
+
+@[simp]
+theorem pairwise_rel_nil {α : Type u} (rel : α → α → Prop) :
+  pairwise_rel rel []
+  := by simp [pairwise_rel]
+
+@[simp]
+theorem pairwise_rel_cons {α : Type u} (rel : α → α → Prop) (hd: α) (tl: List α) :
+  pairwise_rel rel (hd :: tl) ↔ allP tl (rel hd) ∧ pairwise_rel rel tl
+  := by simp [pairwise_rel]
+
 end Lemmas
 
 end List
diff --git a/backends/lean/Base/Progress/Progress.lean b/backends/lean/Base/Progress/Progress.lean
index 974a6364..1f734415 100644
--- a/backends/lean/Base/Progress/Progress.lean
+++ b/backends/lean/Base/Progress/Progress.lean
@@ -39,7 +39,7 @@ inductive ProgressError
 | Error (msg : MessageData)
 deriving Inhabited
 
-def progressWith (fnExpr : Expr) (th : TheoremOrLocal) (ids : Array Name)
+def progressWith (fnExpr : Expr) (th : TheoremOrLocal) (keep : Option Name) (ids : Array Name)
   (asmTac : TacticM Unit) : TacticM ProgressError := do
   /- Apply the theorem
      We try to match the theorem with the goal
@@ -88,7 +88,7 @@ def progressWith (fnExpr : Expr) (th : TheoremOrLocal) (ids : Array Name)
     match th with
     | .Theorem thName => mkAppOptM thName (mvars.map some)
     | .Local decl => mkAppOptM' (mkFVar decl.fvarId) (mvars.map some)
-  let asmName ← mkFreshUserName `h
+  let asmName ← do match keep with | none => mkFreshUserName `h | some n => do pure n
   let thTy ← inferType th
   let thAsm ← Utils.addDeclTac asmName th thTy (asLet := false)
   withMainContext do -- The context changed - TODO: remove once addDeclTac is updated
@@ -109,7 +109,9 @@ def progressWith (fnExpr : Expr) (th : TheoremOrLocal) (ids : Array Name)
       if ← isConj (← inferType h) then do
         let hName := (← h.fvarId!.getDecl).userName
         let (optId, ids) := listTryPopHead ids
-        let optIds := match optId with | none => none | some id => some (hName, id)
+        let optIds ← match optId with
+          | none => do pure (some (hName, ← mkFreshUserName `h))
+          | some id => do pure (some (hName, id))
         splitConjTac h optIds (fun hEq hPost => k hEq (some hPost) ids)
       else k h none ids
     -- Simplify the target by using the equality and some monad simplifications,
@@ -118,9 +120,12 @@ def progressWith (fnExpr : Expr) (th : TheoremOrLocal) (ids : Array Name)
     trace[Progress] "eq and post:\n{hEq} : {← inferType hEq}\n{hPost}"
     simpAt [] [``Primitives.bind_tc_ret, ``Primitives.bind_tc_fail, ``Primitives.bind_tc_div]
            [hEq.fvarId!] (.targets #[] true)
-    -- Clear the equality
-    let mgoal ← getMainGoal
-    let mgoal ← mgoal.tryClearMany #[hEq.fvarId!]
+    -- Clear the equality, unless the user requests not to do so
+    let mgoal ← do
+      if keep.isSome then getMainGoal
+      else do
+        let mgoal ← getMainGoal
+        mgoal.tryClearMany #[hEq.fvarId!]
     setGoals (mgoal :: (← getUnsolvedGoals))
     trace[Progress] "Goal after splitting eq and post and simplifying the target: {mgoal}"
     -- Continue splitting following the ids provided by the user
@@ -170,7 +175,7 @@ def getFirstArg (args : Array Expr) : Option Expr := do
 
 /- Helper: try to lookup a theorem and apply it, or continue with another tactic
    if it fails -/
-def tryLookupApply (ids : Array Name) (asmTac : TacticM Unit) (fnExpr : Expr)
+def tryLookupApply (keep : Option Name) (ids : Array Name) (asmTac : TacticM Unit) (fnExpr : Expr)
   (kind : String) (th : Option TheoremOrLocal) (x : TacticM Unit) : TacticM Unit := do
   let res ← do
     match th with
@@ -182,7 +187,7 @@ def tryLookupApply (ids : Array Name) (asmTac : TacticM Unit) (fnExpr : Expr)
       -- Apply the theorem
       let res ← do
         try
-          let res ← progressWith fnExpr th ids asmTac
+          let res ← progressWith fnExpr th keep ids asmTac
           pure (some res)
         catch _ => none
   match res with
@@ -191,7 +196,7 @@ def tryLookupApply (ids : Array Name) (asmTac : TacticM Unit) (fnExpr : Expr)
   | none => x
 
 -- The array of ids are identifiers to use when introducing fresh variables
-def progressAsmsOrLookupTheorem (withTh : Option TheoremOrLocal) (ids : Array Name) (asmTac : TacticM Unit) : TacticM Unit := do
+def progressAsmsOrLookupTheorem (keep : Option Name) (withTh : Option TheoremOrLocal) (ids : Array Name) (asmTac : TacticM Unit) : TacticM Unit := do
   withMainContext do
   -- Retrieve the goal
   let mgoal ← Tactic.getMainGoal
@@ -209,7 +214,7 @@ def progressAsmsOrLookupTheorem (withTh : Option TheoremOrLocal) (ids : Array Na
   -- Otherwise, lookup one.
   match withTh with
   | some th => do
-    match ← progressWith fnExpr th ids asmTac with
+    match ← progressWith fnExpr th keep ids asmTac with
     | .Ok => return ()
     | .Error msg => throwError msg
   | none =>
@@ -218,7 +223,7 @@ def progressAsmsOrLookupTheorem (withTh : Option TheoremOrLocal) (ids : Array Na
     let decls ← ctx.getDecls
     for decl in decls.reverse do
       trace[Progress] "Trying assumption: {decl.userName} : {decl.type}"
-      let res ← do try progressWith fnExpr (.Local decl) ids asmTac catch _ => continue
+      let res ← do try progressWith fnExpr (.Local decl) keep ids asmTac catch _ => continue
       match res with
       | .Ok => return ()
       | .Error msg => throwError msg
@@ -228,7 +233,7 @@ def progressAsmsOrLookupTheorem (withTh : Option TheoremOrLocal) (ids : Array Na
     let pspec ← do
       let thName ← pspecAttr.find? fName
       pure (thName.map fun th => .Theorem th)
-    tryLookupApply ids asmTac fnExpr "pspec theorem" pspec do
+    tryLookupApply keep ids asmTac fnExpr "pspec theorem" pspec do
     -- It failed: try to lookup a *class* expr spec theorem (those are more
     -- specific than class spec theorems)
     let pspecClassExpr ← do
@@ -237,7 +242,7 @@ def progressAsmsOrLookupTheorem (withTh : Option TheoremOrLocal) (ids : Array Na
       | some arg => do
         let thName ← pspecClassExprAttr.find? fName arg
         pure (thName.map fun th => .Theorem th)
-    tryLookupApply ids asmTac fnExpr "pspec class expr theorem" pspecClassExpr do
+    tryLookupApply keep ids asmTac fnExpr "pspec class expr theorem" pspecClassExpr do
     -- It failed: try to lookup a *class* spec theorem
     let pspecClass ← do
       match ← getFirstArgAppName args with
@@ -245,7 +250,7 @@ def progressAsmsOrLookupTheorem (withTh : Option TheoremOrLocal) (ids : Array Na
       | some argName => do
         let thName ← pspecClassAttr.find? fName argName
         pure (thName.map fun th => .Theorem th)
-    tryLookupApply ids asmTac fnExpr "pspec class theorem" pspecClass do
+    tryLookupApply keep ids asmTac fnExpr "pspec class theorem" pspecClass do
     -- Try a recursive call - we try the assumptions of kind "auxDecl"
     let ctx ← Lean.MonadLCtx.getLCtx
     let decls ← ctx.getAllDecls
@@ -253,21 +258,29 @@ def progressAsmsOrLookupTheorem (withTh : Option TheoremOrLocal) (ids : Array Na
       | .default | .implDetail => false | .auxDecl => true)
     for decl in decls.reverse do
       trace[Progress] "Trying recursive assumption: {decl.userName} : {decl.type}"
-      let res ← do try progressWith fnExpr (.Local decl) ids asmTac catch _ => continue
+      let res ← do try progressWith fnExpr (.Local decl) keep ids asmTac catch _ => continue
       match res with
       | .Ok => return ()
       | .Error msg => throwError msg
     -- Nothing worked: failed
     throwError "Progress failed"
 
-syntax progressArgs := ("with" ident)? ("as" " ⟨ " (ident)+ " ⟩")?
+syntax progressArgs := ("keep" ("as" (ident))?)? ("with" ident)? ("as" " ⟨ " (ident)+ " ⟩")?
 
 def evalProgress (args : TSyntax `Progress.progressArgs) : TacticM Unit := do
   let args := args.raw
   -- Process the arguments to retrieve the identifiers to use
   trace[Progress] "Progress arguments: {args}"
   let args := args.getArgs
-  let withArg := (args.get! 0).getArgs
+  let keep : Option Name ← do
+    let args := (args.get! 0).getArgs
+    if args.size > 0 then do
+      let args := (args.get! 1).getArgs
+      if args.size > 0 then pure (some (args.get! 1).getId)
+      else do pure (some (← mkFreshUserName `h))
+    else pure none
+  trace[Progress] "Keep: {keep}"
+  let withArg := (args.get! 1).getArgs
   let withArg ← do
     if withArg.size > 0 then
       let id := withArg.get! 1
@@ -287,11 +300,11 @@ def evalProgress (args : TSyntax `Progress.progressArgs) : TacticM Unit := do
         | id :: _ =>
           pure (some (.Theorem id))
     else pure none
-  let args := (args.get! 1).getArgs
+  let args := (args.get! 2).getArgs
   let args := (args.get! 2).getArgs
   let ids := args.map Syntax.getId
   trace[Progress] "User-provided ids: {ids}"
-  progressAsmsOrLookupTheorem withArg ids (firstTac [assumptionTac, Arith.scalarTac])
+  progressAsmsOrLookupTheorem keep withArg ids (firstTac [assumptionTac, Arith.scalarTac])
 
 elab "progress" args:progressArgs : tactic =>
   evalProgress args
@@ -306,11 +319,11 @@ namespace Test
   #eval showStoredPSpec
   #eval showStoredPSpecClass
 
-  theorem Scalar.add_spec {ty} {x y : Scalar ty}
+  theorem Scalar.add_spec1 {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
+    progress keep as h with Scalar.add_spec as ⟨ z ⟩
     simp [*]
 
 /-
diff --git a/tests/lean/Hashmap/Properties.lean b/tests/lean/Hashmap/Properties.lean
index 3b9b960f..baa8f5c8 100644
--- a/tests/lean/Hashmap/Properties.lean
+++ b/tests/lean/Hashmap/Properties.lean
@@ -3,75 +3,6 @@ import Hashmap.Funs
 open Primitives
 open Result
 
-namespace List
-
-theorem index_ne
-  {α : Type u} [Inhabited α] (l: List α) (i: ℤ) (j: ℤ) (x: α) :
-   0 ≤ i → i < l.len → 0 ≤ j → j < l.len → j ≠ i →
-    (l.update i x).index j = l.index j
-  :=
-  λ _ _ _ _ _ => match l with
-  | [] => by simp at *
-  | hd :: tl =>
-    if h: i = 0 then
-      have : j ≠ 0 := by scalar_tac
-      by simp [*]
-    else if h : j = 0 then
-      have : i ≠ 0 := by scalar_tac
-      by simp [*]
-    else
-      by
-        simp [*]
-        simp at *
-        apply index_ne <;> scalar_tac
-
-theorem index_eq
-  {α : Type u} [Inhabited α] (l: List α) (i: ℤ) (x: α) :
-   0 ≤ i → i < l.len →
-    (l.update i x).index i = x
-  :=
-  fun _ _ => match l with
-  | [] => by simp at *; exfalso; scalar_tac -- TODO: exfalso needed. Son FIXME
-  | hd :: tl =>
-    if h: i = 0 then
-      by
-        simp [*]
-    else
-      by
-        simp [*]
-        simp at *
-        apply index_eq <;> scalar_tac
-
-def allP {α : Type u} (l : List α) (p: α → Prop) : Prop :=
-  foldr (fun a r => p a ∧ r) True l
-
-@[simp]
-theorem allP_nil {α : Type u} (p: α → Prop) : allP [] p :=
-  by simp [allP, foldr]
-
-@[simp]
-theorem allP_cons {α : Type u} (hd: α) (tl : List α) (p: α → Prop) :
-  allP (hd :: tl) p ↔ p hd ∧ allP tl p
-  := by simp [allP, foldr]
-
-def pairwise_rel 
-  {α : Type u} (rel : α → α → Prop) (l: List α) : Prop
-  := match l with
-  | [] => True
-  | hd :: tl => allP tl (rel hd) ∧ pairwise_rel rel tl
-
-@[simp]
-theorem pairwise_rel_nil {α : Type u} (rel : α → α → Prop) :
-  pairwise_rel rel []
-  := by simp [pairwise_rel]
-
-@[simp]
-theorem pairwise_rel_cons {α : Type u} (rel : α → α → Prop) (hd: α) (tl: List α) :
-  pairwise_rel rel (hd :: tl) ↔ allP tl (rel hd) ∧ pairwise_rel rel tl
-  := by simp [pairwise_rel]
-
-end List
-
 namespace hashmap
 
 namespace List
@@ -104,18 +35,16 @@ theorem insert_in_list_spec {α : Type} (key: Usize) (value: α) (ls: List α) :
         rw [insert_in_list_loop]
         simp [h]
     else
+      have ⟨ b, hi ⟩ := insert_in_list_spec key value tl
       by
-        -- TODO: use progress: detect that this is a recursive call, or give
-        -- the possibility of specifying an identifier
-        have ⟨ b, hi ⟩ := insert_in_list_spec key value tl
         exists b
         simp [insert_in_list, List.lookup]
-        rw [insert_in_list_loop] -- TODO: Using it in simp leads to infinite recursion
+        rw [insert_in_list_loop] -- TODO: Using simp leads to infinite recursion
         simp [h]
         simp [insert_in_list] at hi
         exact hi
 
-set_option trace.Progress true
+-- Variation: use progress
 @[pspec]
 theorem insert_in_list_spec1 {α : Type} (key: Usize) (value: α) (ls: List α) :
   ∃ b,
@@ -134,18 +63,13 @@ theorem insert_in_list_spec1 {α : Type} (key: Usize) (value: α) (ls: List α)
         simp only [insert_in_list]
         rw [insert_in_list_loop]
         conv => rhs; ext; simp [*]
-        progress as ⟨ b hi ⟩
-
-        -- TODO: use progress: detect that this is a recursive call, or give
-        -- the possibility of specifying an identifier
-        have ⟨ b, hi ⟩ := insert_in_list_spec key value tl
+        progress keep as heq as ⟨ b hi ⟩
+        simp only [insert_in_list] at heq
         exists b
-        simp [insert_in_list, List.lookup]
-        rw [insert_in_list_loop] -- TODO: Using it in simp leads to infinite recursion
-        simp [h]
-        simp [insert_in_list] at hi
-        exact hi
+        simp only [heq, hi]
+        simp [*, List.lookup]
 
+-- Variation: use tactics from the beginning
 @[pspec]
 theorem insert_in_list_spec2 {α : Type} (key: Usize) (value: α) (ls: List α) :
   ∃ b,
-- 
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/IList')

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 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/IList')

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