Make some proofs in Hashmap/Properties.lean and improve progress

5 files changed, 129 insertions, 74 deletions

diff --git a/backends/lean/Base/Arith/Int.lean b/backends/lean/Base/Arith/Int.lean
index ac011998..fa957293 100644
--- a/backends/lean/Base/Arith/Int.lean
+++ b/backends/lean/Base/Arith/Int.lean
@@ -198,7 +198,7 @@ def intTac (extraPreprocess :  Tactic.TacticM Unit) : Tactic.TacticM Unit := do
   -- Split the conjunctions in the goal
   Tactic.allGoals (Utils.repeatTac Utils.splitConjTarget)
   -- Call linarith
-  let linarith :=
+  let linarith := do
     let cfg : Linarith.LinarithConfig := {
       -- We do this with our custom preprocessing
       splitNe := false
diff --git a/backends/lean/Base/Progress/Base.lean b/backends/lean/Base/Progress/Base.lean
index 2fbd24dd..b54bdf7a 100644
--- a/backends/lean/Base/Progress/Base.lean
+++ b/backends/lean/Base/Progress/Base.lean
@@ -19,6 +19,7 @@ structure PSpecDesc where
   -- The existentially quantified variables
   evars : Array Expr
   -- The function
+  fExpr : Expr
   fName : Name
   -- The function arguments
   fLevels : List Level
@@ -60,21 +61,30 @@ section Methods
     m a := do
     trace[Progress] "Proposition: {th}"
     -- Dive into the quantified variables and the assumptions
-    forallTelescope th fun fvars th => do
+    forallTelescope th.consumeMData fun fvars th => do
     trace[Progress] "Universally quantified arguments and assumptions: {fvars}"
     -- Dive into the existentials
-    existsTelescope th fun evars th => do
+    existsTelescope th.consumeMData fun evars th => do
     trace[Progress] "Existentials: {evars}"
     trace[Progress] "Proposition after stripping the quantifiers: {th}"
     -- Take the first conjunct
-    let (th, post) ← optSplitConj th
+    let (th, post) ← optSplitConj th.consumeMData
     trace[Progress] "After splitting the conjunction:\n- eq: {th}\n- post: {post}"
     -- Destruct the equality
-    let (th, ret) ← destEq th
+    let (mExpr, ret) ← destEq th.consumeMData
     trace[Progress] "After splitting the equality:\n- lhs: {th}\n- rhs: {ret}"
-    -- Destruct the application to get the name
-    th.consumeMData.withApp fun f args => do
-    trace[Progress] "After stripping the arguments:\n- f: {f}\n- args: {args}"
+    -- Destruct the monadic application to dive into the bind, if necessary (this
+    -- is for when we use `withPSpec` inside of the `progress` tactic), and
+    -- destruct the application to get the function name
+    mExpr.consumeMData.withApp fun mf margs => do
+    trace[Progress] "After stripping the arguments of the monad expression:\n- mf: {mf}\n- margs: {margs}"
+    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)
+      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}"
     -- Compute the set of universally quantified variables which appear in the function arguments
     let allArgsFVars ← args.foldlM (fun hs arg => getFVarIds arg hs) HashSet.empty
@@ -94,6 +104,7 @@ section Methods
     let thDesc := {
       fvars := fvars
       evars := evars
+      fExpr
       fName := f.constName!
       fLevels := f.constLevels!
       args := args
diff --git a/backends/lean/Base/Progress/Progress.lean b/backends/lean/Base/Progress/Progress.lean
index 1f734415..dabd25b8 100644
--- a/backends/lean/Base/Progress/Progress.lean
+++ b/backends/lean/Base/Progress/Progress.lean
@@ -7,22 +7,6 @@ namespace Progress
 open Lean Elab Term Meta Tactic
 open Utils
 
-/-
--- TODO: remove
-namespace Test
-  open Primitives
-
-  set_option trace.Progress true
-
-  @[pspec]
-  theorem vec_index_test (α : Type u) (v: Vec α) (i: Usize) (h: i.val < v.val.length) :
-    ∃ x, v.index α i = .ret x := by
-      sorry
-
-  #eval pspecAttr.find? ``Primitives.Vec.index
-end Test
--/
-
 inductive TheoremOrLocal where
 | Theorem (thName : Name)
 | Local (asm : LocalDecl)
@@ -39,7 +23,7 @@ inductive ProgressError
 | Error (msg : MessageData)
 deriving Inhabited
 
-def progressWith (fnExpr : Expr) (th : TheoremOrLocal) (keep : Option Name) (ids : Array Name)
+def progressWith (fExpr : 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
@@ -66,7 +50,7 @@ def progressWith (fnExpr : Expr) (th : TheoremOrLocal) (keep : Option Name) (ids
   -- Introduce the existentially quantified variables and the post-condition
   -- in the context
   let thBody ←
-    existsTelescope thExBody fun _evars thBody => do
+    existsTelescope thExBody.consumeMData fun _evars thBody => do
     trace[Progress] "After stripping existentials: {thBody}"
     let (thBody, _) ← optSplitConj thBody
     trace[Progress] "After splitting the conjunction: {thBody}"
@@ -75,9 +59,9 @@ def progressWith (fnExpr : Expr) (th : TheoremOrLocal) (keep : Option Name) (ids
     -- There shouldn't be any existential variables in thBody
     pure thBody
   -- Match the body with the target
-  trace[Progress] "Maching `{thBody}` with `{fnExpr}`"
-  let ok ← isDefEq thBody fnExpr
-  if ¬ ok then throwError "Could not unify the theorem with the target:\n- theorem: {thBody}\n- target: {fnExpr}"
+  trace[Progress] "Matching `{thBody}` with `{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
   postprocessAppMVars `progress mgoal mvars binders true true
   Term.synthesizeSyntheticMVarsNoPostponing
@@ -139,8 +123,9 @@ def progressWith (fnExpr : Expr) (th : TheoremOrLocal) (keep : Option Name) (ids
         match ids with
         | [] => pure .Ok -- Stop
         | nid :: ids => do
+          trace[Progress] "Splitting post: {hPost}"
           -- Split
-          if ← isConj hPost then
+          if ← isConj (← inferType hPost) then
             splitConjTac hPost (some (nid, curPostId)) (λ _ nhPost => splitPost nhPost ids)
           else return (.Error m!"Too many ids provided ({nid :: ids}) not enough conjuncts to split in the postcondition")
       splitPost hPost ids
@@ -175,7 +160,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 (keep : Option Name) (ids : Array Name) (asmTac : TacticM Unit) (fnExpr : Expr)
+def tryLookupApply (keep : Option Name) (ids : Array Name) (asmTac : TacticM Unit) (fExpr : Expr)
   (kind : String) (th : Option TheoremOrLocal) (x : TacticM Unit) : TacticM Unit := do
   let res ← do
     match th with
@@ -187,7 +172,7 @@ def tryLookupApply (keep : Option Name) (ids : Array Name) (asmTac : TacticM Uni
       -- Apply the theorem
       let res ← do
         try
-          let res ← progressWith fnExpr th keep ids asmTac
+          let res ← progressWith fExpr th keep ids asmTac
           pure (some res)
         catch _ => none
   match res with
@@ -203,18 +188,16 @@ def progressAsmsOrLookupTheorem (keep : Option Name) (withTh : Option TheoremOrL
   let goalTy ← mgoal.getType
   trace[Progress] "goal: {goalTy}"
   -- Dive into the goal to lookup the theorem
-  let (fName, fLevels, args) ← do
+  let (fExpr, fName, args) ← do
     withPSpec goalTy fun desc =>
-    -- TODO: check that no universally quantified variables in the arguments
-    pure (desc.fName, desc.fLevels, desc.args)
-  -- TODO: this should be in the pspec desc
-  let fnExpr := mkAppN (.const fName fLevels) args
+    -- TODO: check that no quantified variables in the arguments
+    pure (desc.fExpr, desc.fName, desc.args)
   trace[Progress] "Function: {fName}"
   -- If the user provided a theorem/assumption: use it.
   -- Otherwise, lookup one.
   match withTh with
   | some th => do
-    match ← progressWith fnExpr th keep ids asmTac with
+    match ← progressWith fExpr th keep ids asmTac with
     | .Ok => return ()
     | .Error msg => throwError msg
   | none =>
@@ -223,7 +206,7 @@ def progressAsmsOrLookupTheorem (keep : Option Name) (withTh : Option TheoremOrL
     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) keep ids asmTac catch _ => continue
+      let res ← do try progressWith fExpr (.Local decl) keep ids asmTac catch _ => continue
       match res with
       | .Ok => return ()
       | .Error msg => throwError msg
@@ -233,7 +216,7 @@ def progressAsmsOrLookupTheorem (keep : Option Name) (withTh : Option TheoremOrL
     let pspec ← do
       let thName ← pspecAttr.find? fName
       pure (thName.map fun th => .Theorem th)
-    tryLookupApply keep ids asmTac fnExpr "pspec theorem" pspec do
+    tryLookupApply keep ids asmTac fExpr "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
@@ -242,7 +225,7 @@ def progressAsmsOrLookupTheorem (keep : Option Name) (withTh : Option TheoremOrL
       | some arg => do
         let thName ← pspecClassExprAttr.find? fName arg
         pure (thName.map fun th => .Theorem th)
-    tryLookupApply keep ids asmTac fnExpr "pspec class expr theorem" pspecClassExpr do
+    tryLookupApply keep ids asmTac fExpr "pspec class expr theorem" pspecClassExpr do
     -- It failed: try to lookup a *class* spec theorem
     let pspecClass ← do
       match ← getFirstArgAppName args with
@@ -250,7 +233,7 @@ def progressAsmsOrLookupTheorem (keep : Option Name) (withTh : Option TheoremOrL
       | some argName => do
         let thName ← pspecClassAttr.find? fName argName
         pure (thName.map fun th => .Theorem th)
-    tryLookupApply keep ids asmTac fnExpr "pspec class theorem" pspecClass do
+    tryLookupApply keep ids asmTac fExpr "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
@@ -258,7 +241,7 @@ def progressAsmsOrLookupTheorem (keep : Option Name) (withTh : Option TheoremOrL
       | .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) keep ids asmTac catch _ => continue
+      let res ← do try progressWith fExpr (.Local decl) keep ids asmTac catch _ => continue
       match res with
       | .Ok => return ()
       | .Error msg => throwError msg
@@ -310,7 +293,6 @@ elab "progress" args:progressArgs : tactic =>
   evalProgress args
 
 /-
--- TODO: remove
 namespace Test
   open Primitives Result
 
@@ -319,22 +301,14 @@ namespace Test
   #eval showStoredPSpec
   #eval showStoredPSpecClass
 
-  theorem Scalar.add_spec1 {ty} {x y : Scalar ty}
+  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 ⟩
+--    progress keep as h with Scalar.add_spec as ⟨ z ⟩
+    progress keep as h
     simp [*]
 
-/-
-  @[pspec]
-  theorem vec_index_test2 (α : Type u) (v: Vec α) (i: Usize) (h: i.val < v.val.length) :
-    ∃ (x: α), v.index α i = .ret x := by
-      progress with vec_index_test as ⟨ x ⟩
-      simp
-
-  set_option trace.Progress false
--/
 end Test -/
 
 end Progress
diff --git a/backends/lean/Base/Utils.lean b/backends/lean/Base/Utils.lean
index 8aa76d8e..44590176 100644
--- a/backends/lean/Base/Utils.lean
+++ b/backends/lean/Base/Utils.lean
@@ -308,8 +308,23 @@ def firstTac (tacl : List (TacticM Unit)) : TacticM Unit := do
   match tacl with
   | [] => pure ()
   | tac :: tacl =>
-    try tac
+    -- Should use try ... catch or Lean.observing?
+    -- Generally speaking we should use Lean.observing? to restore the state,
+    -- but with tactics the try ... catch variant seems to work
+    try do
+      tac
+      -- Check that there are no remaining goals
+      let gl ← Tactic.getUnsolvedGoals
+      if ¬ gl.isEmpty then throwError "tactic failed"
     catch _ => firstTac tacl
+/-    let res ← Lean.observing? do
+      tac
+      -- Check that there are no remaining goals
+      let gl ← Tactic.getUnsolvedGoals
+      if ¬ gl.isEmpty then throwError "tactic failed"
+    match res with
+    | some _ => pure ()
+    | none => firstTac tacl -/
 
 -- Split the goal if it is a conjunction
 def splitConjTarget : TacticM Unit := do
@@ -424,12 +439,13 @@ def splitExistsTac (h : Expr) (optId : Option Name) (k : Expr → Expr → Tacti
   let hTy ← inferType h
   if isExists hTy then do
     -- Try to use the user-provided names
-    let altVarNames ←
-      match optId with
-      | none => pure #[]
-      | some id => do
-        let hDecl ← h.fvarId!.getDecl
-        pure #[{ varNames := [id, hDecl.userName] }]
+    let altVarNames ← do
+      let hDecl ← h.fvarId!.getDecl
+      let id ← do
+        match optId with
+        | none => mkFreshUserName `x
+        | some id => pure id
+      pure #[{ varNames := [id, hDecl.userName] }]
     let newGoals ← goal.cases h.fvarId! altVarNames
     -- There should be exactly one goal
     match newGoals.toList with
@@ -511,7 +527,7 @@ example (h : a ∧ b) : a := by
 
 example (h : ∃ x y z, x + y + z ≥ 0) : ∃ x, x ≥ 0 := by
   split_all_exists h
-  rename_i x y z h
+  rename_i x y z
   exists x + y + z
 
 /- Call the simp tactic.
diff --git a/tests/lean/Hashmap/Properties.lean b/tests/lean/Hashmap/Properties.lean
index baa8f5c8..e065bb36 100644
--- a/tests/lean/Hashmap/Properties.lean
+++ b/tests/lean/Hashmap/Properties.lean
@@ -21,8 +21,9 @@ end List
 
 namespace HashMap
 
-@[pspec]
-theorem insert_in_list_spec {α : Type} (key: Usize) (value: α) (ls: List α) :
+abbrev Core.List := _root_.List
+
+theorem insert_in_list_spec0 {α : Type} (key: Usize) (value: α) (ls: List α) :
   ∃ b,
     insert_in_list α key value ls = ret b ∧
     (b ↔ List.lookup ls.v key = none)
@@ -35,7 +36,7 @@ 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
+      have ⟨ b, hi ⟩ := insert_in_list_spec0 key value tl
       by
         exists b
         simp [insert_in_list, List.lookup]
@@ -45,7 +46,6 @@ theorem insert_in_list_spec {α : Type} (key: Usize) (value: α) (ls: List α) :
         exact hi
 
 -- Variation: use progress
-@[pspec]
 theorem insert_in_list_spec1 {α : Type} (key: Usize) (value: α) (ls: List α) :
   ∃ b,
     insert_in_list α key value ls = ret b ∧
@@ -70,7 +70,6 @@ theorem insert_in_list_spec1 {α : Type} (key: Usize) (value: α) (ls: List α)
         simp [*, List.lookup]
 
 -- Variation: use tactics from the beginning
-@[pspec]
 theorem insert_in_list_spec2 {α : Type} (key: Usize) (value: α) (ls: List α) :
   ∃ b,
     insert_in_list α key value ls = ret b ∧
@@ -91,10 +90,10 @@ theorem insert_in_list_spec2 {α : Type} (key: Usize) (value: α) (ls: List α)
      progress as ⟨ b h ⟩
      simp [*]
 
-@[pspec]
 theorem insert_in_list_back_spec {α : Type} (key: Usize) (value: α) (l0: List α) :
   ∃ l1,
     insert_in_list_back α key value l0 = ret l1 ∧
+    -- We update the binding
     List.lookup l1.v key = value ∧
     (∀ k, k ≠ key → List.lookup l1.v k = List.lookup l0.v k)
   := match l0 with
@@ -112,11 +111,66 @@ theorem insert_in_list_back_spec {α : Type} (key: Usize) (value: α) (l0: List
          simp [insert_in_list_back, List.lookup]
          rw [insert_in_list_loop_back]
          simp [h, List.lookup]
-         have ⟨tl0 , _, _ ⟩ := insert_in_list_back_spec key value tl -- TODO: Use progress
-         simp [insert_in_list_back] at *
-         simp [List.lookup, *]
-         simp (config := {contextual := true}) [*]
-        
+         progress keep as heq as ⟨ tl hp1 hp2 ⟩
+         simp [insert_in_list_back] at heq
+         simp (config := {contextual := true}) [*, List.lookup]
+
+def distinct_keys (ls : Core.List (Usize × α)) := ls.pairwise_rel (λ x y => x.fst ≠ y.fst)
+
+def hash_mod_key (k : Usize) (l : Int) : Int :=
+  match hash_key k with
+  | .ret k => k.val % l
+  | _ => 0
+
+def slot_s_inv_hash (l i : Int) (ls : Core.List (Usize × α)) : Prop :=
+  ls.allP (λ (k, _) => hash_mod_key k l = i)
+
+@[simp]
+def slot_s_inv (l i : Int) (ls : Core.List (Usize × α)) : Prop :=
+  distinct_keys ls ∧
+  slot_s_inv_hash l i ls
+
+def slot_t_inv (l i : Int) (s : List α) : Prop := slot_s_inv l i s.v
+
+@[pspec]
+theorem insert_in_list_back_spec1 {α : Type} (l : Int) (key: Usize) (value: α) (l0: List α)
+  (hinv : slot_s_inv_hash l (hash_mod_key key l) l0.v) :
+  ∃ l1,
+    insert_in_list_back α key value l0 = ret l1 ∧
+    -- We update the binding
+    List.lookup l1.v key = value ∧
+    (∀ k, k ≠ key → List.lookup l1.v k = List.lookup l0.v k) ∧
+    -- We preserve part of the key invariant
+    slot_s_inv_hash l (hash_mod_key key l) l1.v
+  := match l0 with
+  | .Nil => by
+    simp [insert_in_list_back, insert_in_list_loop_back, List.lookup, List.v, slot_s_inv_hash]
+    tauto
+  | .Cons k v tl0 =>
+     if h: k = key then
+       by
+         simp [insert_in_list_back, List.lookup]
+         rw [insert_in_list_loop_back]
+         simp [h, List.lookup]
+         constructor
+         . intros; simp [*]
+         . simp [List.v, slot_s_inv_hash] at *
+           simp [*]
+     else
+       by
+         simp [insert_in_list_back, List.lookup]
+         rw [insert_in_list_loop_back]
+         simp [h, List.lookup]
+         have : slot_s_inv_hash l (hash_mod_key key l) (List.v tl0) := by
+           simp_all [List.v, slot_s_inv_hash]
+         progress keep as heq as ⟨ tl1 hp1 hp2 hp3 ⟩
+         simp only [insert_in_list_back] at heq
+         have : slot_s_inv_hash l (hash_mod_key key l) (List.v (List.Cons k v tl1)) := by
+           simp [List.v, slot_s_inv_hash] at *
+           simp [*]
+         simp (config := {contextual := true}) [*, List.lookup]
+
+
 end HashMap
 
 end hashmap