Update the syntax of the progress tactic

5 files changed, 117 insertions, 111 deletions

diff --git a/backends/lean/Base/Arith/Int.lean b/backends/lean/Base/Arith/Int.lean
index 48a30a49..7a5bbe98 100644
--- a/backends/lean/Base/Arith/Int.lean
+++ b/backends/lean/Base/Arith/Int.lean
@@ -147,7 +147,7 @@ def introInstances (declToUnfold : Name) (lookup : Expr → MetaM (Option Expr))
   let hs ← collectInstancesFromMainCtx lookup
   hs.toArray.mapM fun e => do
     let type ← inferType e
-    let name ← mkFreshUserName `h
+    let name ← mkFreshAnonPropUserName
     -- Add a declaration
     let nval ← Utils.addDeclTac name e type (asLet := false)
     -- Simplify to unfold the declaration to unfold (i.e., the projector)
diff --git a/backends/lean/Base/Arith/Scalar.lean b/backends/lean/Base/Arith/Scalar.lean
index 6f4a8eba..b792ff21 100644
--- a/backends/lean/Base/Arith/Scalar.lean
+++ b/backends/lean/Base/Arith/Scalar.lean
@@ -12,7 +12,7 @@ def scalarTacExtraPreprocess : Tactic.TacticM Unit := do
    -- Inroduce the bounds for the isize/usize types
    let add (e : Expr) : Tactic.TacticM Unit := do
      let ty ← inferType e
-     let _ ← Utils.addDeclTac (← mkFreshUserName `h) e ty (asLet := false)
+     let _ ← Utils.addDeclTac (← Utils.mkFreshAnonPropUserName) e ty (asLet := false)
    add (← mkAppM ``Scalar.cMin_bound #[.const ``ScalarTy.Isize []])
    add (← mkAppM ``Scalar.cMax_bound #[.const ``ScalarTy.Usize []])
    add (← mkAppM ``Scalar.cMax_bound #[.const ``ScalarTy.Isize []])
diff --git a/backends/lean/Base/Progress/Progress.lean b/backends/lean/Base/Progress/Progress.lean
index 4a406bdf..9300edff 100644
--- a/backends/lean/Base/Progress/Progress.lean
+++ b/backends/lean/Base/Progress/Progress.lean
@@ -79,7 +79,7 @@ def progressWith (fExpr : Expr) (th : TheoremOrLocal)
     match th with
     | .Theorem thName => mkAppOptM thName (mvars.map some)
     | .Local decl => mkAppOptM' (mkFVar decl.fvarId) (mvars.map some)
-  let asmName ← do match keep with | none => mkFreshUserName `h | some n => do pure n
+  let asmName ← do match keep with | none => mkFreshAnonPropUserName | 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
@@ -101,8 +101,8 @@ def progressWith (fExpr : Expr) (th : TheoremOrLocal)
         let hName := (← h.fvarId!.getDecl).userName
         let (optIds, ids) ← do
           match ids with
-          | [] => do pure (some (hName, ← mkFreshUserName `h), [])
-          | none :: ids => do pure (some (hName, ← mkFreshUserName `h), ids)
+          | [] => do pure (some (hName, ← mkFreshAnonPropUserName), [])
+          | none :: ids => do pure (some (hName, ← mkFreshAnonPropUserName), ids)
           | some id :: ids => do pure (some (hName, id), ids)
         splitConjTac h optIds (fun hEq hPost => k hEq (some hPost) ids)
       else k h none ids
@@ -142,7 +142,7 @@ def progressWith (fExpr : Expr) (th : TheoremOrLocal)
           -- Split
           let nid ← do
             match nid with
-            | none => mkFreshUserName `h
+            | none => mkFreshAnonPropUserName
             | some nid => pure nid
           trace[Progress] "\n- prevId: {prevId}\n- nid: {nid}\n- remaining ids: {ids}"
           if ← isConj (← inferType hPost) then
@@ -270,23 +270,26 @@ def progressAsmsOrLookupTheorem (keep : Option Name) (withTh : Option TheoremOrL
     -- Nothing worked: failed
     throwError "Progress failed"
 
-syntax progressArgs := ("keep" ("as" (ident))?)? ("with" ident)? ("as" " ⟨ " (ident <|> "_"),* " .."? " ⟩")?
+syntax progressArgs := ("keep" (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 (keepArg, withArg, asArgs) ←
+    match args.getArgs.toList with
+    | [keepArg, withArg, asArgs] => do pure (keepArg, withArg, asArgs)
+    | _ => throwError "Unexpected: invalid arguments"
   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
+    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))
   trace[Progress] "Keep: {keep}"
   let withArg ← do
-    let withArg := (args.get! 1).getArgs
+    let withArg := withArg.getArgs
     if withArg.size > 0 then
       let id := withArg.get! 1
       trace[Progress] "With arg: {id}"
@@ -306,12 +309,12 @@ def evalProgress (args : TSyntax `Progress.progressArgs) : TacticM Unit := do
           pure (some (.Theorem id))
     else pure none
   let ids :=
-    let args := (args.get! 2).getArgs
+    let args := asArgs.getArgs
     let args := (args.get! 2).getSepArgs
     args.map (λ s => if s.isIdent then some s.getId else none)
   trace[Progress] "User-provided ids: {ids}"
   let splitPost : Bool :=
-    let args := (args.get! 2).getArgs
+    let args := asArgs.getArgs
     (args.get! 3).getArgs.size > 0
   trace[Progress] "Split post: {splitPost}"
   /- For scalarTac we have a fast track: if the goal is not a linear
@@ -343,15 +346,15 @@ namespace Test
     (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 as ⟨ x, h1 .. ⟩
-    simp [*]
+    progress keep _ as ⟨ z, h1 .. ⟩
+    simp [*, h1]
 
   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 [*]
+    progress keep h with Scalar.add_spec as ⟨ z ⟩
+    simp [*, h]
 
   /- Checking that universe instantiation works: the original spec uses
      `α : Type u` where u is quantified, while here we use `α : Type 0` -/
diff --git a/backends/lean/Base/Utils.lean b/backends/lean/Base/Utils.lean
index f6dc45c7..1f8f1455 100644
--- a/backends/lean/Base/Utils.lean
+++ b/backends/lean/Base/Utils.lean
@@ -201,6 +201,10 @@ partial def mapVisit (k : Nat → Expr → MetaM Expr) (e : Expr) : MetaM Expr :
     | .proj _ _ b => return e.updateProj! (← visit (i + 1) b)
   visit 0 e
 
+-- Generate a fresh user name for an anonymous proposition to introduce in the
+-- assumptions
+def mkFreshAnonPropUserName := mkFreshUserName `_
+
 section Methods
   variable [MonadLiftT MetaM m] [MonadControlT MetaM m] [Monad m] [MonadError m]
   variable {a : Type}
@@ -411,7 +415,7 @@ def splitDisjTac (h : Expr) (kleft kright : TacticM Unit) : TacticM Unit := do
   trace[Arith] "left: {inl}: {mleft}"
   trace[Arith] "right: {inr}: {mright}"
   -- Create the match expression
-  withLocalDeclD (← mkFreshUserName `h) hTy fun hVar => do
+  withLocalDeclD (← mkFreshAnonPropUserName) hTy fun hVar => do
   let motive ← mkLambdaFVars #[hVar] goalType
   let casesExpr ← mkAppOptM ``Or.casesOn #[a, b, motive, h, inl, inr]
   let mgoal ← getMainGoal
@@ -505,8 +509,8 @@ def splitConjTac (h : Expr) (optIds : Option (Name × Name)) (k : Expr → Expr
     let altVarNames ←
       match optIds with
       | none => do
-        let id0 ← mkFreshUserName `h
-        let id1 ← mkFreshUserName `h
+        let id0 ← mkFreshAnonPropUserName
+        let id1 ← mkFreshAnonPropUserName
         pure #[{ varNames := [id0, id1] }]
       | some (id0, id1) => do
         pure #[{ varNames := [id0, id1] }]
@@ -532,7 +536,7 @@ partial def splitFullConjTacAux [Inhabited α] [Nonempty α] (keepCurrentName :
     let ids ← do
       if keepCurrentName then do
         let cur := (← h.fvarId!.getDecl).userName
-        let nid ← mkFreshUserName `h
+        let nid ← mkFreshAnonPropUserName
         pure (some (cur, nid))
       else
         pure none
diff --git a/tests/lean/Hashmap/Properties.lean b/tests/lean/Hashmap/Properties.lean
index 208875a6..96b8193d 100644
--- a/tests/lean/Hashmap/Properties.lean
+++ b/tests/lean/Hashmap/Properties.lean
@@ -95,7 +95,7 @@ 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 keep as heq as ⟨ b, hi ⟩
+        progress keep heq as ⟨ b, hi ⟩
         simp only [insert_in_list] at heq
         exists b
 
@@ -219,7 +219,7 @@ theorem insert_in_list_back_spec_aux {α : Type} (l : Int) (key: Usize) (value:
        have : distinct_keys (List.v tl0) := by checkpoint
          simp [distinct_keys] at hdk
          simp [hdk, distinct_keys]
-       progress keep as heq as ⟨ tl1 .. ⟩
+       progress keep heq as ⟨ tl1 .. ⟩
        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 checkpoint
          simp [List.v, slot_s_inv_hash] at *
@@ -289,8 +289,7 @@ theorem insert_no_resize_spec {α : Type} (hm : HashMap α) (key : Usize) (value
   have _ : (Vec.len (List α) hm.slots).val ≠ 0 := by checkpoint
    intro
    simp_all [inv]
-  -- TODO: progress keep as ⟨ ... ⟩ : conflict
-  progress keep as h as ⟨ hash_mod, hhm ⟩
+  progress keep _ as ⟨ hash_mod, hhm ⟩
   have _ : 0 ≤ hash_mod.val := by checkpoint scalar_tac
   have _ : hash_mod.val < Vec.length hm.slots := by
     have : 0 < hm.slots.val.len := by
@@ -324,11 +323,12 @@ theorem insert_no_resize_spec {α : Type} (hm : HashMap α) (key : Usize) (value
   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
+  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
     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 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 [inv, slots_t_inv, slot_t_inv] at hinv
     have h := hinv.right.left hash_mod.val (by assumption) (by assumption)
@@ -337,88 +337,87 @@ theorem insert_no_resize_spec {α : Type} (hm : HashMap α) (key : Usize) (value
   -- 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 keep as 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
-    have hupdt : lookup nhm key = some value := by checkpoint
-      simp [lookup, List.lookup] at *
+  -- 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
+  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
+    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 < 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 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,
-      -- 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 < 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
+    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
+      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 _ := hinv.right.left i hipos (by simp_all)
+      simp [hhm, h_veq] at * -- TODO: annoying
+      -- 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'"
+        -- Also, it is annoying to do this kind
+        -- of rewritings by hand. We could have a different simp
+        -- which safely substitutes variables when we have an
+        -- equality `x = ...` and `x` doesn't appear in the rhs
+        simp [h_ieq] at *
+        simp [*]
       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 _ := hinv.right.left i hipos (by simp_all)
-        simp [hhm, h_veq] at * -- TODO: annoying
-        -- We need a case disjunction
-        if h_ieq : i = key.val % _root_.List.len hm.slots.val then
-          -- TODO: simp_all loops (investigate).
-          -- Also, it is annoying to do this kind
-          -- of rewritings by hand. We could have a different simp
-          -- which safely substitutes variables when we have an
-          -- equality `x = ...` and `x` doesn't appear in the rhs
-          simp [h_ieq] at *
-          simp [*]
-        else
-          simp [*]
-      . simp [*]
-    simp_all
+    . -- TODO: simp[*] fails: "(deterministic) timeout at 'whnf'"
+      simp [hinv, h_veq]
+  simp_all
 
 end HashMap