From 6166c410a4b3353377e640acbae9f56e877a9118 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Tue, 11 Jul 2023 15:23:49 +0200
Subject: Work on the progress tactic

---
 backends/lean/Base/Progress/Base.lean     | 175 ++++++++++++++++++++++++++++++
 backends/lean/Base/Progress/Progress.lean | 112 +++++++++++++++++++
 2 files changed, 287 insertions(+)
 create mode 100644 backends/lean/Base/Progress/Base.lean
 create mode 100644 backends/lean/Base/Progress/Progress.lean

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

diff --git a/backends/lean/Base/Progress/Base.lean b/backends/lean/Base/Progress/Base.lean
new file mode 100644
index 00000000..3f44f46c
--- /dev/null
+++ b/backends/lean/Base/Progress/Base.lean
@@ -0,0 +1,175 @@
+import Lean
+import Base.Utils
+import Base.Primitives
+
+namespace Progress
+
+open Lean Elab Term Meta
+open Utils
+
+-- We can't define and use trace classes in the same file
+initialize registerTraceClass `Progress
+
+-- 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 getFirstConj (e : Expr) : MetaM (Expr × Option Expr) := do
+  e.withApp fun f args =>
+  if f.isConstOf ``And ∧ args.size = 2 then pure (args.get! 0, some (args.get! 1))
+  else pure (e, none)
+
+-- Destruct an equaliy and return the two sides
+def destEq (e : Expr) : MetaM (Expr × Expr) := do
+  e.withApp fun f args =>
+  if f.isConstOf ``Eq ∧ args.size = 3 then pure (args.get! 1, args.get! 2)
+  else throwError "Not an equality: {e}"
+
+-- Return the set of FVarIds in the expression
+partial def getFVarIds (e : Expr) (hs : HashSet FVarId := HashSet.empty) : MetaM (HashSet FVarId) := do
+  e.withApp fun body args => do
+  let hs := if body.isFVar then hs.insert body.fvarId! else hs
+  args.foldlM (fun hs arg => getFVarIds arg hs) hs
+
+/- # Progress tactic -/
+
+structure PSpecDesc where
+  -- The universally quantified variables
+  fvars : Array Expr
+  -- The existentially quantified variables
+  evars : Array Expr
+  -- The function
+  fName : Name
+  -- The function arguments
+  fLevels : List Level
+  args : Array Expr
+  -- The universally quantified variables which appear in the function arguments
+  argsFVars : Array FVarId
+  -- The returned value
+  ret : Expr
+  -- The postcondition (if there is)
+  post : Option Expr
+
+section Methods
+  variable [MonadLiftT MetaM m] [MonadControlT MetaM m] [Monad m] [MonadOptions m]
+  variable [MonadTrace m] [MonadLiftT IO m] [MonadRef m] [AddMessageContext m]
+  variable [MonadError m]
+  variable {a : Type}
+
+  /- Analyze a pspec theorem to decompose its arguments.
+
+     PSpec theorems should be of the following shape:
+     ```
+     ∀ x1 ... xn, H1 → ... Hn → ∃ y1 ... ym. f x1 ... xn = .ret ... ∧ Post1 ∧ ... ∧ Postk
+     ```
+
+     The continuation `k` receives the following inputs:
+     - universally quantified variables
+     - assumptions
+     - existentially quantified variables
+     - function name
+     - function arguments
+     - return
+     - postconditions
+
+     TODO: generalize for when we do inductive proofs
+  -/
+  partial
+  def withPSpec [Inhabited (m a)] [Nonempty (m a)] (th : Expr) (k : PSpecDesc → m a)
+    (sanityChecks : Bool := false) :
+    m a := do
+    trace[Progress] "Theorem: {th}"
+    -- Dive into the quantified variables and the assumptions
+    forallTelescope th fun fvars th => do
+    trace[Progress] "All argumens: {fvars}"
+  /-  -- Filter the argumens which are not propositions
+    let rec getFirstPropIdx (i : Nat) : MetaM Nat := do
+      if i ≥ fargs.size then pure i
+      else do
+        let x := fargs.get! i
+        if ← Meta.isProp (← inferType x) then pure i
+        else getFirstPropIdx (i + 1)
+    let i ← getFirstPropIdx 0
+    let fvars := fargs.extract 0 i
+    let hyps := fargs.extract i fargs.size
+    trace[Progress] "Quantified variables: {fvars}"
+    trace[Progress] "Assumptions: {hyps}"
+    -- Sanity check: all hypotheses are propositions (in particular, all the
+    -- quantified variables are at the beginning)
+    let hypsAreProp ← hyps.allM fun x => do Meta.isProp (← inferType x)
+    if ¬ hypsAreProp then
+      throwError "The theorem doesn't have the proper shape: all the quantified arguments should be at the beginning"
+      -/
+    -- Dive into the existentials
+    existsTelescope th fun evars th => do
+    trace[Progress] "Existentials: {evars}"
+    -- Take the first conjunct
+    let (th, post) ← getFirstConj th
+    -- Destruct the equality
+    let (th, ret) ← destEq th
+    -- Destruct the application to get the name
+    th.withApp fun f args => do
+    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
+    -- Sanity check
+    if sanityChecks then
+      let fvarsSet : HashSet FVarId := HashSet.ofArray (fvars.map (fun x => x.fvarId!))
+      let filtArgsFVars := allArgsFVars.toArray.filter (fun fvar => ¬ fvarsSet.contains fvar)
+      if ¬ filtArgsFVars.isEmpty then
+        let filtArgsFVars := filtArgsFVars.map (fun fvarId => Expr.fvar fvarId)
+        throwError "Some of the function inputs are not universally quantified: {filtArgsFVars}"
+    let argsFVars := fvars.map (fun x => x.fvarId!)
+    let argsFVars := argsFVars.filter (fun fvar => allArgsFVars.contains fvar)
+    -- Return
+    trace[Progress] "Function: {f.constName!}";
+    let thDesc := {
+      fvars := fvars
+      evars := evars
+      fName := f.constName!
+      fLevels := f.constLevels!
+      args := args
+      argsFVars
+      ret := ret
+      post := post
+    }
+    k thDesc
+end Methods
+
+
+def getPSpecFunName (th : Expr) : MetaM Name :=
+  withPSpec th (fun d => do pure d.fName) true
+
+structure PSpecAttr where
+  attr : AttributeImpl
+  ext  : MapDeclarationExtension Name
+  deriving Inhabited
+
+/- The persistent map from function to pspec theorems. -/
+initialize pspecAttr : PSpecAttr ← do
+  let ext ← mkMapDeclarationExtension `pspecMap
+  let attrImpl := {
+    name := `pspec
+    descr := "Marks theorems to use with the `progress` tactic"
+    add := fun thName stx attrKind => do
+      Attribute.Builtin.ensureNoArgs stx
+      -- TODO: use the attribute kind
+      unless attrKind == AttributeKind.global do
+        throwError "invalid attribute 'pspec', must be global"
+      -- Lookup the theorem
+      let env ← getEnv
+      let thDecl := env.constants.find! thName
+      let fName ← MetaM.run' (getPSpecFunName thDecl.type)
+      trace[Progress] "Registering spec theorem for {fName}"
+      let env := ext.addEntry env (fName, thName)
+      setEnv env
+      pure ()
+  }
+  registerBuiltinAttribute attrImpl
+  pure { attr := attrImpl, ext := ext }
+
+def PSpecAttr.find? (s : PSpecAttr) (name : Name) : MetaM (Option Name) := do
+  return (s.ext.getState (← getEnv)).find? name
+  --return s.ext.find? (← getEnv) name
+
+
+end Progress
diff --git a/backends/lean/Base/Progress/Progress.lean b/backends/lean/Base/Progress/Progress.lean
new file mode 100644
index 00000000..1b9ee55c
--- /dev/null
+++ b/backends/lean/Base/Progress/Progress.lean
@@ -0,0 +1,112 @@
+import Lean
+import Base.Arith
+import Base.Progress.Base
+
+namespace Progress
+
+open Lean Elab Term Meta Tactic
+open Utils
+
+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
+      apply
+      sorry
+
+  #eval pspecAttr.find? ``Primitives.Vec.index
+end Test
+
+#check isDefEq
+#check allGoals
+
+def progressLookupTheorem (asmTac : TacticM Unit) : TacticM Unit := do
+  withMainContext do
+  -- Retrieve the goal
+  let mgoal ← Tactic.getMainGoal
+  let goalTy ← mgoal.getType
+  -- Dive into the goal to lookup the theorem
+  let (fName, fLevels, args) ← do
+    withPSpec goalTy fun desc =>
+    -- TODO: check that no universally quantified variables in the arguments
+    pure (desc.fName, desc.fLevels, desc.args)
+  -- TODO: also try the assumptions
+  trace[Progress] "Function: {fName}"
+  -- TODO: use a list of theorems, and try them one by one?
+  let thName ← do
+    match ← pspecAttr.find? fName with
+    | none => throwError "Could not find a pspec theorem for {fName}"
+    | some thName => pure thName
+  trace[Progress] "Lookuped up: {thName}"
+  /- Apply the theorem
+     We try to match the theorem with the goal
+     In order to do so, we introduce meta-variables for all the parameters
+     (i.e., quantified variables and assumpions), and unify those with the goal.
+     Remark: we do not introduce meta-variables for the quantified variables
+     which don't appear in the function arguments (we want to let them
+     quantified).
+     We also make sure that all the meta variables which appear in the
+     function arguments have been instantiated
+   -/  
+  let env ← getEnv
+  let thDecl := env.constants.find! thName
+  let thTy := thDecl.type
+  -- TODO: the tactic fails if we uncomment withNewMCtxDepth
+  -- withNewMCtxDepth do
+  let (mvars, binders, thExBody) ← forallMetaTelescope thTy
+  -- Introduce the existentially quantified variables and the post-condition
+  -- in the context
+  let thBody ←
+    existsTelescope thExBody fun _evars thBody => do
+    let (thBody, _) ← destEq thBody
+    -- There shouldn't be any existential variables in thBody
+    pure thBody
+  -- Match the body with the target
+  let target := mkAppN (.const fName fLevels) args
+  trace[Progress] "mvars:\n{mvars.map Expr.mvarId!}"
+  trace[Progress] "thBody: {thBody}"
+  trace[Progress] "target: {target}"
+  let ok ← isDefEq thBody target
+  if ¬ ok then throwError "Could not unify the theorem with the target:\n- theorem: {thBody}\n- target: {target}"
+  postprocessAppMVars `progress mgoal mvars binders true true
+  Term.synthesizeSyntheticMVarsNoPostponing
+  let thBody ← instantiateMVars thBody
+  trace[Progress] "thBody (after instantiation): {thBody}"
+  -- Add the instantiated theorem to the assumptions (we apply it on the metavariables).
+  let th ← mkAppOptM thName (mvars.map some)
+  let asmName ← mkFreshUserName `h
+  let thTy ← inferType th
+  let thAsm ← Utils.addDecl asmName th thTy (asLet := false)
+  -- Update the set of goals
+  let curGoals ← getUnsolvedGoals
+  let newGoals := mvars.map Expr.mvarId!
+  let newGoals ← newGoals.filterM fun mvar => not <$> mvar.isAssigned
+  trace[Progress] "new goals: {newGoals}"
+  setGoals newGoals.toList
+  allGoals asmTac
+  let newGoals ← getUnsolvedGoals
+  setGoals (newGoals ++ curGoals)
+  -- 
+  pure ()
+
+elab "progress" : tactic => do
+  progressLookupTheorem (firstTac [assumptionTac, Arith.intTac])
+
+namespace Test
+  open Primitives
+
+  set_option trace.Progress true
+
+  @[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
+      tauto
+      
+end Test
+
+end Progress
-- 
cgit v1.2.3


From a18d899a2c2b9bdd36f4a5a4b70472c12a835a96 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Wed, 12 Jul 2023 14:34:55 +0200
Subject: Finish a first version of the progress tactic

---
 backends/lean/Base/Progress/Base.lean     | 24 +--------------------
 backends/lean/Base/Progress/Progress.lean | 36 ++++++++++++++++++++++++-------
 2 files changed, 29 insertions(+), 31 deletions(-)

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

diff --git a/backends/lean/Base/Progress/Base.lean b/backends/lean/Base/Progress/Base.lean
index 3f44f46c..613f38f8 100644
--- a/backends/lean/Base/Progress/Base.lean
+++ b/backends/lean/Base/Progress/Base.lean
@@ -10,26 +10,6 @@ open Utils
 -- We can't define and use trace classes in the same file
 initialize registerTraceClass `Progress
 
--- 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 getFirstConj (e : Expr) : MetaM (Expr × Option Expr) := do
-  e.withApp fun f args =>
-  if f.isConstOf ``And ∧ args.size = 2 then pure (args.get! 0, some (args.get! 1))
-  else pure (e, none)
-
--- Destruct an equaliy and return the two sides
-def destEq (e : Expr) : MetaM (Expr × Expr) := do
-  e.withApp fun f args =>
-  if f.isConstOf ``Eq ∧ args.size = 3 then pure (args.get! 1, args.get! 2)
-  else throwError "Not an equality: {e}"
-
--- Return the set of FVarIds in the expression
-partial def getFVarIds (e : Expr) (hs : HashSet FVarId := HashSet.empty) : MetaM (HashSet FVarId) := do
-  e.withApp fun body args => do
-  let hs := if body.isFVar then hs.insert body.fvarId! else hs
-  args.foldlM (fun hs arg => getFVarIds arg hs) hs
-
 /- # Progress tactic -/
 
 structure PSpecDesc where
@@ -103,7 +83,7 @@ section Methods
     existsTelescope th fun evars th => do
     trace[Progress] "Existentials: {evars}"
     -- Take the first conjunct
-    let (th, post) ← getFirstConj th
+    let (th, post) ← optSplitConj th
     -- Destruct the equality
     let (th, ret) ← destEq th
     -- Destruct the application to get the name
@@ -169,7 +149,5 @@ initialize pspecAttr : PSpecAttr ← do
 
 def PSpecAttr.find? (s : PSpecAttr) (name : Name) : MetaM (Option Name) := do
   return (s.ext.getState (← getEnv)).find? name
-  --return s.ext.find? (← getEnv) name
-
 
 end Progress
diff --git a/backends/lean/Base/Progress/Progress.lean b/backends/lean/Base/Progress/Progress.lean
index 1b9ee55c..4c68b3bd 100644
--- a/backends/lean/Base/Progress/Progress.lean
+++ b/backends/lean/Base/Progress/Progress.lean
@@ -21,9 +21,6 @@ namespace Test
   #eval pspecAttr.find? ``Primitives.Vec.index
 end Test
 
-#check isDefEq
-#check allGoals
-
 def progressLookupTheorem (asmTac : TacticM Unit) : TacticM Unit := do
   withMainContext do
   -- Retrieve the goal
@@ -80,7 +77,28 @@ def progressLookupTheorem (asmTac : TacticM Unit) : TacticM Unit := do
   let th ← mkAppOptM thName (mvars.map some)
   let asmName ← mkFreshUserName `h
   let thTy ← inferType th
-  let thAsm ← Utils.addDecl asmName th thTy (asLet := false)
+  let thAsm ← Utils.addDeclTac asmName th thTy (asLet := false)
+  withMainContext do -- The context changed - TODO: remove once addDeclTac is updated
+  let ngoal ← getMainGoal
+  trace[Progress] "current goal: {ngoal}"
+  trace[Progress] "current goal: {← ngoal.isAssigned}"
+  -- The assumption should be of the shape:
+  -- `∃ x1 ... xn, f args = ... ∧ ...`
+  -- We introduce the existentially quantified variables and split the top-most
+  -- conjunction if there is one
+  splitAllExistsTac thAsm fun h => do
+    -- Split the conjunction
+    let splitConj (k : Expr → TacticM Unit) : TacticM Unit := do
+      if ← isConj (← inferType h) then
+        splitConjTac h (fun h _ => k h)
+      else k h
+    -- Simplify the target by using the equality
+    splitConj fun h => do
+    simpAt [] [] [h.fvarId!] (.targets #[] true)
+    -- Clear the equality
+    let mgoal ← getMainGoal
+    let mgoal ← mgoal.tryClearMany #[h.fvarId!]
+    setGoals (mgoal :: (← getUnsolvedGoals))
   -- Update the set of goals
   let curGoals ← getUnsolvedGoals
   let newGoals := mvars.map Expr.mvarId!
@@ -94,7 +112,7 @@ def progressLookupTheorem (asmTac : TacticM Unit) : TacticM Unit := do
   pure ()
 
 elab "progress" : tactic => do
-  progressLookupTheorem (firstTac [assumptionTac, Arith.intTac])
+  progressLookupTheorem (firstTac [assumptionTac, Arith.scalarTac])
 
 namespace Test
   open Primitives
@@ -103,10 +121,12 @@ namespace Test
 
   @[pspec]
   theorem vec_index_test2 (α : Type u) (v: Vec α) (i: Usize) (h: i.val < v.val.length) :
-    ∃ x, v.index α i = .ret x := by
+    ∃ (x: α), v.index α i = .ret x := by
       progress
-      tauto
-      
+      simp
+
+  set_option trace.Progress false
+
 end Test
 
 end Progress
-- 
cgit v1.2.3


From 59e4a06480b5365f48dc68de80f44841f94094ed Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Wed, 12 Jul 2023 15:41:29 +0200
Subject: Improve the handling of arithmetic bounds

---
 backends/lean/Base/Progress/Progress.lean | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

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

diff --git a/backends/lean/Base/Progress/Progress.lean b/backends/lean/Base/Progress/Progress.lean
index 4c68b3bd..a4df5c96 100644
--- a/backends/lean/Base/Progress/Progress.lean
+++ b/backends/lean/Base/Progress/Progress.lean
@@ -92,9 +92,10 @@ def progressLookupTheorem (asmTac : TacticM Unit) : TacticM Unit := do
       if ← isConj (← inferType h) then
         splitConjTac h (fun h _ => k h)
       else k h
-    -- Simplify the target by using the equality
+    -- Simplify the target by using the equality and some monad simplifications
     splitConj fun h => do
-    simpAt [] [] [h.fvarId!] (.targets #[] true)
+    simpAt [] [``Primitives.bind_tc_ret, ``Primitives.bind_tc_fail, ``Primitives.bind_tc_div]
+           [h.fvarId!] (.targets #[] true)
     -- Clear the equality
     let mgoal ← getMainGoal
     let mgoal ← mgoal.tryClearMany #[h.fvarId!]
-- 
cgit v1.2.3


From eb97bdb6761437e492bcf1a95b4fa43d2b69601b Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Wed, 12 Jul 2023 18:04:19 +0200
Subject: Improve progress to use assumptions and start working on a nice
 syntax

---
 backends/lean/Base/Progress/Base.lean     |   2 +-
 backends/lean/Base/Progress/Progress.lean | 107 +++++++++++++++++++++---------
 2 files changed, 77 insertions(+), 32 deletions(-)

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

diff --git a/backends/lean/Base/Progress/Base.lean b/backends/lean/Base/Progress/Base.lean
index 613f38f8..a288d889 100644
--- a/backends/lean/Base/Progress/Base.lean
+++ b/backends/lean/Base/Progress/Base.lean
@@ -60,7 +60,7 @@ section Methods
     trace[Progress] "Theorem: {th}"
     -- Dive into the quantified variables and the assumptions
     forallTelescope th fun fvars th => do
-    trace[Progress] "All argumens: {fvars}"
+    trace[Progress] "All arguments: {fvars}"
   /-  -- Filter the argumens which are not propositions
     let rec getFirstPropIdx (i : Nat) : MetaM Nat := do
       if i ≥ fargs.size then pure i
diff --git a/backends/lean/Base/Progress/Progress.lean b/backends/lean/Base/Progress/Progress.lean
index a4df5c96..b0db465d 100644
--- a/backends/lean/Base/Progress/Progress.lean
+++ b/backends/lean/Base/Progress/Progress.lean
@@ -21,24 +21,11 @@ namespace Test
   #eval pspecAttr.find? ``Primitives.Vec.index
 end Test
 
-def progressLookupTheorem (asmTac : TacticM Unit) : TacticM Unit := do
-  withMainContext do
-  -- Retrieve the goal
-  let mgoal ← Tactic.getMainGoal
-  let goalTy ← mgoal.getType
-  -- Dive into the goal to lookup the theorem
-  let (fName, fLevels, args) ← do
-    withPSpec goalTy fun desc =>
-    -- TODO: check that no universally quantified variables in the arguments
-    pure (desc.fName, desc.fLevels, desc.args)
-  -- TODO: also try the assumptions
-  trace[Progress] "Function: {fName}"
-  -- TODO: use a list of theorems, and try them one by one?
-  let thName ← do
-    match ← pspecAttr.find? fName with
-    | none => throwError "Could not find a pspec theorem for {fName}"
-    | some thName => pure thName
-  trace[Progress] "Lookuped up: {thName}"
+inductive TheoremOrLocal where
+| Theorem (thName : Name)
+| Local (asm : LocalDecl)
+
+def progressWith (fnExpr : Expr) (th : TheoremOrLocal) (ids : Array Name) (asmTac : TacticM Unit) : TacticM Unit := do
   /- Apply the theorem
      We try to match the theorem with the goal
      In order to do so, we introduce meta-variables for all the parameters
@@ -48,10 +35,14 @@ def progressLookupTheorem (asmTac : TacticM Unit) : TacticM Unit := do
      quantified).
      We also make sure that all the meta variables which appear in the
      function arguments have been instantiated
-   -/  
+   -/
   let env ← getEnv
-  let thDecl := env.constants.find! thName
-  let thTy := thDecl.type
+  let thTy ← do
+    match th with
+    | .Theorem thName =>
+      let thDecl := env.constants.find! thName
+      pure thDecl.type
+    | .Local asmDecl => pure asmDecl.type
   -- TODO: the tactic fails if we uncomment withNewMCtxDepth
   -- withNewMCtxDepth do
   let (mvars, binders, thExBody) ← forallMetaTelescope thTy
@@ -63,18 +54,19 @@ def progressLookupTheorem (asmTac : TacticM Unit) : TacticM Unit := do
     -- There shouldn't be any existential variables in thBody
     pure thBody
   -- Match the body with the target
-  let target := mkAppN (.const fName fLevels) args
-  trace[Progress] "mvars:\n{mvars.map Expr.mvarId!}"
-  trace[Progress] "thBody: {thBody}"
-  trace[Progress] "target: {target}"
-  let ok ← isDefEq thBody target
-  if ¬ ok then throwError "Could not unify the theorem with the target:\n- theorem: {thBody}\n- target: {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}"
+  let mgoal ← Tactic.getMainGoal
   postprocessAppMVars `progress mgoal mvars binders true true
   Term.synthesizeSyntheticMVarsNoPostponing
   let thBody ← instantiateMVars thBody
   trace[Progress] "thBody (after instantiation): {thBody}"
   -- Add the instantiated theorem to the assumptions (we apply it on the metavariables).
-  let th ← mkAppOptM thName (mvars.map some)
+  let th ← do
+    match th with
+    | .Theorem thName => mkAppOptM thName (mvars.map some)
+    |  .Local decl => mkAppOptM' (mkFVar decl.fvarId) (mvars.map some)
   let asmName ← mkFreshUserName `h
   let thTy ← inferType th
   let thAsm ← Utils.addDeclTac asmName th thTy (asLet := false)
@@ -112,18 +104,71 @@ def progressLookupTheorem (asmTac : TacticM Unit) : TacticM Unit := do
   -- 
   pure ()
 
-elab "progress" : tactic => do
-  progressLookupTheorem (firstTac [assumptionTac, Arith.scalarTac])
+-- The array of ids are identifiers to use when introducing fresh variables
+def progressAsmsOrLookupTheorem (ids : Array Name) (asmTac : TacticM Unit) : TacticM Unit := do
+  withMainContext do
+  -- Retrieve the goal
+  let mgoal ← Tactic.getMainGoal
+  let goalTy ← mgoal.getType
+  -- Dive into the goal to lookup the theorem
+  let (fName, fLevels, 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
+  trace[Progress] "Function: {fName}"
+  -- Try all the assumptions one by one and if it fails try to lookup a theorem
+  let ctx ← Lean.MonadLCtx.getLCtx
+  let decls ← ctx.getDecls
+  for decl in decls.reverse do
+    trace[Progress] "Trying assumption: {decl.userName} : {decl.type}"
+    try
+      progressWith fnExpr (.Local decl) ids asmTac
+      return ()
+    catch _ => continue
+  -- It failed: try to lookup a theorem
+  -- TODO: use a list of theorems, and try them one by one?
+  trace[Progress] "No assumption succeeded: trying to lookup a theorem"
+  let thName ← do
+    match ← pspecAttr.find? fName with
+    | none => throwError "Could not find a pspec theorem for {fName}"
+    | some thName => pure thName
+  trace[Progress] "Lookuped up: {thName}"
+  -- Apply the theorem
+  progressWith fnExpr (.Theorem thName) ids asmTac
+
+#check Syntax
+syntax progressArgs := ("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] "Progressing arguments: {args}"
+  let args := args.getArgs
+  let ids :=
+    if args.size > 0 then
+      let args := (args.get! 0).getArgs
+      let args := (args.get! 2).getArgs
+      args.map Syntax.getId
+    else #[]
+  trace[Progress] "Ids: {ids}"
+  --if args[0] ≠ some "as" then throwError "Invalid syntax: should be: `progress as ⟨ ... ⟩`"
+  progressAsmsOrLookupTheorem ids (firstTac [assumptionTac, Arith.scalarTac])
+
+elab "progress" args:progressArgs : tactic =>
+  evalProgress args
 
 namespace Test
   open Primitives
 
   set_option trace.Progress true
+  set_option pp.rawOnError true
 
   @[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
+      progress as ⟨ x y z ⟩
       simp
 
   set_option trace.Progress false
-- 
cgit v1.2.3


From 6cc0279045d40231f1cce83f0edb7aada1e59d92 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Thu, 13 Jul 2023 10:37:16 +0200
Subject: Finish implementing the syntax for `progress`

---
 backends/lean/Base/Progress/Progress.lean | 98 ++++++++++++++++++++++---------
 1 file changed, 70 insertions(+), 28 deletions(-)

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

diff --git a/backends/lean/Base/Progress/Progress.lean b/backends/lean/Base/Progress/Progress.lean
index b0db465d..835dc468 100644
--- a/backends/lean/Base/Progress/Progress.lean
+++ b/backends/lean/Base/Progress/Progress.lean
@@ -25,7 +25,17 @@ inductive TheoremOrLocal where
 | Theorem (thName : Name)
 | Local (asm : LocalDecl)
 
-def progressWith (fnExpr : Expr) (th : TheoremOrLocal) (ids : Array Name) (asmTac : TacticM Unit) : TacticM Unit := do
+/- Type to propagate the errors of `progressWith`.
+   We need this because we use the exceptions to backtrack, when trying to
+   use the assumptions for instance. When there is actually an error we want
+   to propagate to the user, we return it. -/
+inductive ProgressError
+| Ok
+| Error (msg : MessageData)
+deriving Inhabited
+
+def progressWith (fnExpr : Expr) (th : TheoremOrLocal) (ids : Array Name)
+  (asmTac : TacticM Unit) : TacticM ProgressError := do
   /- Apply the theorem
      We try to match the theorem with the goal
      In order to do so, we introduce meta-variables for all the parameters
@@ -77,32 +87,62 @@ def progressWith (fnExpr : Expr) (th : TheoremOrLocal) (ids : Array Name) (asmTa
   -- The assumption should be of the shape:
   -- `∃ x1 ... xn, f args = ... ∧ ...`
   -- We introduce the existentially quantified variables and split the top-most
-  -- conjunction if there is one
-  splitAllExistsTac thAsm fun h => do
-    -- Split the conjunction
-    let splitConj (k : Expr → TacticM Unit) : TacticM Unit := do
-      if ← isConj (← inferType h) then
-        splitConjTac h (fun h _ => k h)
-      else k h
-    -- Simplify the target by using the equality and some monad simplifications
-    splitConj fun h => do
+  -- conjunction if there is one. We use the provided `ids` list to name the
+  -- introduced variables.
+  let res ← splitAllExistsTac thAsm ids.toList fun h ids => do
+    -- Split the conjunctions.
+    -- For the conjunctions, we split according once to separate the equality `f ... = .ret ...`
+    -- from the postcondition, if there is, then continue to split the postcondition if there
+    -- are remaining ids.
+    let splitEqAndPost (k : Expr → Option Expr → List Name → TacticM ProgressError) : TacticM ProgressError := do
+      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)
+        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,
+    -- then continue splitting the post-condition
+    splitEqAndPost fun hEq hPost ids => do
+    trace[Progress] "eq and post:\n{hEq} : {← inferType hEq}\n{hPost}"
     simpAt [] [``Primitives.bind_tc_ret, ``Primitives.bind_tc_fail, ``Primitives.bind_tc_div]
-           [h.fvarId!] (.targets #[] true)
+           [hEq.fvarId!] (.targets #[] true)
     -- Clear the equality
     let mgoal ← getMainGoal
-    let mgoal ← mgoal.tryClearMany #[h.fvarId!]
+    let mgoal ← mgoal.tryClearMany #[hEq.fvarId!]
     setGoals (mgoal :: (← getUnsolvedGoals))
-  -- Update the set of goals
-  let curGoals ← getUnsolvedGoals
-  let newGoals := mvars.map Expr.mvarId!
-  let newGoals ← newGoals.filterM fun mvar => not <$> mvar.isAssigned
-  trace[Progress] "new goals: {newGoals}"
-  setGoals newGoals.toList
-  allGoals asmTac
-  let newGoals ← getUnsolvedGoals
-  setGoals (newGoals ++ curGoals)
-  -- 
-  pure ()
+    trace[Progress] "Goal after splitting eq and post and simplifying the target: {mgoal}"
+    -- Continue splitting following the ids provided by the user
+    if ¬ ids.isEmpty then
+      let hPost ←
+        match hPost with
+        | none => do return (.Error m!"Too many ids provided ({ids}): there is no postcondition to split")
+        | some hPost => pure hPost
+      let curPostId := (← hPost.fvarId!.getDecl).userName
+      let rec splitPost (hPost : Expr) (ids : List Name) : TacticM ProgressError := do
+        match ids with
+        | [] => pure .Ok -- Stop
+        | nid :: ids => do
+          -- Split
+          if ← isConj 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
+    else return .Ok
+  match res with
+  | .Error _ => return res -- Can we get there? We're using "return"
+  | .Ok =>
+    -- Update the set of goals
+    let curGoals ← getUnsolvedGoals
+    let newGoals := mvars.map Expr.mvarId!
+    let newGoals ← newGoals.filterM fun mvar => not <$> mvar.isAssigned
+    trace[Progress] "new goals: {newGoals}"
+    setGoals newGoals.toList
+    allGoals asmTac
+    let newGoals ← getUnsolvedGoals
+    setGoals (newGoals ++ curGoals)
+    --
+    pure .Ok
 
 -- The array of ids are identifiers to use when introducing fresh variables
 def progressAsmsOrLookupTheorem (ids : Array Name) (asmTac : TacticM Unit) : TacticM Unit := do
@@ -124,8 +164,9 @@ def progressAsmsOrLookupTheorem (ids : Array Name) (asmTac : TacticM Unit) : Tac
   for decl in decls.reverse do
     trace[Progress] "Trying assumption: {decl.userName} : {decl.type}"
     try
-      progressWith fnExpr (.Local decl) ids asmTac
-      return ()
+      match ← progressWith fnExpr (.Local decl) ids asmTac with
+      | .Ok => return ()
+      | .Error msg => throwError msg
     catch _ => continue
   -- It failed: try to lookup a theorem
   -- TODO: use a list of theorems, and try them one by one?
@@ -136,9 +177,10 @@ def progressAsmsOrLookupTheorem (ids : Array Name) (asmTac : TacticM Unit) : Tac
     | some thName => pure thName
   trace[Progress] "Lookuped up: {thName}"
   -- Apply the theorem
-  progressWith fnExpr (.Theorem thName) ids asmTac
+  match ← progressWith fnExpr (.Theorem thName) ids asmTac with
+  | .Ok => return ()
+  | .Error msg => throwError msg
 
-#check Syntax
 syntax progressArgs := ("as" " ⟨ " (ident)+ " ⟩")?
 
 def evalProgress (args : TSyntax `Progress.progressArgs) : TacticM Unit := do
@@ -168,7 +210,7 @@ namespace Test
   @[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 as ⟨ x y z ⟩
+      progress as ⟨ x ⟩
       simp
 
   set_option trace.Progress false
-- 
cgit v1.2.3


From 4f7ebc2358d78d31d63a609a32e5a732b82d468e Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Mon, 17 Jul 2023 12:12:34 +0200
Subject: Update the lean dependencies and update IList

---
 backends/lean/Base/Progress/Progress.lean | 3 ---
 1 file changed, 3 deletions(-)

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

diff --git a/backends/lean/Base/Progress/Progress.lean b/backends/lean/Base/Progress/Progress.lean
index 835dc468..35a3c25a 100644
--- a/backends/lean/Base/Progress/Progress.lean
+++ b/backends/lean/Base/Progress/Progress.lean
@@ -15,7 +15,6 @@ namespace Test
   @[pspec]
   theorem vec_index_test (α : Type u) (v: Vec α) (i: Usize) (h: i.val < v.val.length) :
     ∃ x, v.index α i = .ret x := by
-      apply
       sorry
 
   #eval pspecAttr.find? ``Primitives.Vec.index
@@ -195,7 +194,6 @@ def evalProgress (args : TSyntax `Progress.progressArgs) : TacticM Unit := do
       args.map Syntax.getId
     else #[]
   trace[Progress] "Ids: {ids}"
-  --if args[0] ≠ some "as" then throwError "Invalid syntax: should be: `progress as ⟨ ... ⟩`"
   progressAsmsOrLookupTheorem ids (firstTac [assumptionTac, Arith.scalarTac])
 
 elab "progress" args:progressArgs : tactic =>
@@ -205,7 +203,6 @@ namespace Test
   open Primitives
 
   set_option trace.Progress true
-  set_option pp.rawOnError true
 
   @[pspec]
   theorem vec_index_test2 (α : Type u) (v: Vec α) (i: Usize) (h: i.val < v.val.length) :
-- 
cgit v1.2.3


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/Progress/Progress.lean | 2 ++
 1 file changed, 2 insertions(+)

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

diff --git a/backends/lean/Base/Progress/Progress.lean b/backends/lean/Base/Progress/Progress.lean
index 35a3c25a..af7b426a 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
 
@@ -199,6 +200,7 @@ def evalProgress (args : TSyntax `Progress.progressArgs) : TacticM Unit := do
 elab "progress" args:progressArgs : tactic =>
   evalProgress args
 
+-- TODO: remove
 namespace Test
   open Primitives
 
-- 
cgit v1.2.3


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/Progress/Base.lean     | 3 ++-
 backends/lean/Base/Progress/Progress.lean | 4 ++++
 2 files changed, 6 insertions(+), 1 deletion(-)

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

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.2.3


From e07177ee2de3fd1346ab6b1fc09aefbcb0e24459 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Tue, 18 Jul 2023 12:22:59 +0200
Subject: Improve progress

---
 backends/lean/Base/Progress/Base.lean     | 11 ++++++++---
 backends/lean/Base/Progress/Progress.lean | 11 +++++++++--
 2 files changed, 17 insertions(+), 5 deletions(-)

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

diff --git a/backends/lean/Base/Progress/Base.lean b/backends/lean/Base/Progress/Base.lean
index 00b0a478..7eace667 100644
--- a/backends/lean/Base/Progress/Base.lean
+++ b/backends/lean/Base/Progress/Base.lean
@@ -58,10 +58,10 @@ section Methods
   def withPSpec [Inhabited (m a)] [Nonempty (m a)] (th : Expr) (k : PSpecDesc → m a)
     (sanityChecks : Bool := false) :
     m a := do
-    trace[Progress] "Theorem: {th}"
+    trace[Progress] "Proposition: {th}"
     -- Dive into the quantified variables and the assumptions
     forallTelescope th fun fvars th => do
-    trace[Progress] "All arguments: {fvars}"
+    trace[Progress] "Universally quantified arguments and assumptions: {fvars}"
   /-  -- Filter the argumens which are not propositions
     let rec getFirstPropIdx (i : Nat) : MetaM Nat := do
       if i ≥ fargs.size then pure i
@@ -83,12 +83,16 @@ section Methods
     -- Dive into the existentials
     existsTelescope th 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
+    trace[Progress] "After splitting the conjunction:\n- eq: {th}\n- post: {post}"
     -- Destruct the equality
     let (th, ret) ← destEq th
+    trace[Progress] "After splitting the equality:\n- lhs: {th}\n- rhs: {ret}"
     -- Destruct the application to get the name
-    th.withApp fun f args => do
+    th.consumeMData.withApp fun f args => do
+    trace[Progress] "After stripping the arguments:\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
@@ -114,6 +118,7 @@ section Methods
       post := post
     }
     k thDesc
+
 end Methods
 
 
diff --git a/backends/lean/Base/Progress/Progress.lean b/backends/lean/Base/Progress/Progress.lean
index 001967e5..ace92f4f 100644
--- a/backends/lean/Base/Progress/Progress.lean
+++ b/backends/lean/Base/Progress/Progress.lean
@@ -55,14 +55,20 @@ def progressWith (fnExpr : Expr) (th : TheoremOrLocal) (ids : Array Name)
       let thDecl := env.constants.find! thName
       pure thDecl.type
     | .Local asmDecl => pure asmDecl.type
+  trace[Progress] "theorem/assumption type: {thTy}"
   -- TODO: the tactic fails if we uncomment withNewMCtxDepth
   -- withNewMCtxDepth do
   let (mvars, binders, thExBody) ← forallMetaTelescope thTy
+  trace[Progress] "After stripping foralls: {thExBody}"
   -- Introduce the existentially quantified variables and the post-condition
   -- in the context
   let thBody ←
     existsTelescope thExBody fun _evars thBody => do
+    trace[Progress] "After stripping existentials: {thBody}"
+    let (thBody, _) ← optSplitConj thBody
+    trace[Progress] "After splitting the conjunction: {thBody}"
     let (thBody, _) ← destEq thBody
+    trace[Progress] "After splitting equality: {thBody}"
     -- There shouldn't be any existential variables in thBody
     pure thBody
   -- Match the body with the target
@@ -152,6 +158,7 @@ def progressAsmsOrLookupTheorem (ids : Array Name) (asmTac : TacticM Unit) : Tac
   -- Retrieve the goal
   let mgoal ← Tactic.getMainGoal
   let goalTy ← mgoal.getType
+  trace[Progress] "goal: {goalTy}"
   -- Dive into the goal to lookup the theorem
   let (fName, fLevels, args) ← do
     withPSpec goalTy fun desc =>
@@ -188,7 +195,7 @@ syntax progressArgs := ("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] "Progressing arguments: {args}"
+  trace[Progress] "Progress arguments: {args}"
   let args := args.getArgs
   let ids :=
     if args.size > 0 then
@@ -196,7 +203,7 @@ def evalProgress (args : TSyntax `Progress.progressArgs) : TacticM Unit := do
       let args := (args.get! 2).getArgs
       args.map Syntax.getId
     else #[]
-  trace[Progress] "Ids: {ids}"
+  trace[Progress] "User-provided ids: {ids}"
   progressAsmsOrLookupTheorem ids (firstTac [assumptionTac, Arith.scalarTac])
 
 elab "progress" args:progressArgs : tactic =>
-- 
cgit v1.2.3


From 204742bf2449c88abaea8ebd284c55d98b43488a Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Wed, 19 Jul 2023 14:48:08 +0200
Subject: Improve progress

---
 backends/lean/Base/Progress/Progress.lean | 115 +++++++++++++++++++++---------
 1 file changed, 80 insertions(+), 35 deletions(-)

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

diff --git a/backends/lean/Base/Progress/Progress.lean b/backends/lean/Base/Progress/Progress.lean
index ace92f4f..3b0248fe 100644
--- a/backends/lean/Base/Progress/Progress.lean
+++ b/backends/lean/Base/Progress/Progress.lean
@@ -55,7 +55,7 @@ def progressWith (fnExpr : Expr) (th : TheoremOrLocal) (ids : Array Name)
       let thDecl := env.constants.find! thName
       pure thDecl.type
     | .Local asmDecl => pure asmDecl.type
-  trace[Progress] "theorem/assumption type: {thTy}"
+  trace[Progress] "Looked up theorem/assumption type: {thTy}"
   -- TODO: the tactic fails if we uncomment withNewMCtxDepth
   -- withNewMCtxDepth do
   let (mvars, binders, thExBody) ← forallMetaTelescope thTy
@@ -84,7 +84,7 @@ def progressWith (fnExpr : Expr) (th : TheoremOrLocal) (ids : Array Name)
   let th ← do
     match th with
     | .Theorem thName => mkAppOptM thName (mvars.map some)
-    |  .Local decl => mkAppOptM' (mkFVar decl.fvarId) (mvars.map some)
+    | .Local decl => mkAppOptM' (mkFVar decl.fvarId) (mvars.map some)
   let asmName ← mkFreshUserName `h
   let thTy ← inferType th
   let thAsm ← Utils.addDeclTac asmName th thTy (asLet := false)
@@ -153,7 +153,7 @@ def progressWith (fnExpr : Expr) (th : TheoremOrLocal) (ids : Array Name)
     pure .Ok
 
 -- The array of ids are identifiers to use when introducing fresh variables
-def progressAsmsOrLookupTheorem (ids : Array Name) (asmTac : TacticM Unit) : TacticM Unit := do
+def progressAsmsOrLookupTheorem (withTh : Option TheoremOrLocal) (ids : Array Name) (asmTac : TacticM Unit) : TacticM Unit := do
   withMainContext do
   -- Retrieve the goal
   let mgoal ← Tactic.getMainGoal
@@ -167,44 +167,89 @@ def progressAsmsOrLookupTheorem (ids : Array Name) (asmTac : TacticM Unit) : Tac
   -- TODO: this should be in the pspec desc
   let fnExpr := mkAppN (.const fName fLevels) args
   trace[Progress] "Function: {fName}"
-  -- Try all the assumptions one by one and if it fails try to lookup a theorem
-  let ctx ← Lean.MonadLCtx.getLCtx
-  let decls ← ctx.getDecls
-  for decl in decls.reverse do
-    trace[Progress] "Trying assumption: {decl.userName} : {decl.type}"
-    try
-      match ← progressWith fnExpr (.Local decl) ids asmTac with
+  -- If the user provided a theorem/assumption: use it.
+  -- Otherwise, lookup one.
+  match withTh with
+  | some th => do
+    match ← progressWith fnExpr th ids asmTac with
+    | .Ok => return ()
+    | .Error msg => throwError msg
+  | none =>
+    -- Try all the assumptions one by one and if it fails try to lookup a theorem.
+    let ctx ← Lean.MonadLCtx.getLCtx
+    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
+      match res with
       | .Ok => return ()
       | .Error msg => throwError msg
-    catch _ => continue
-  -- It failed: try to lookup a theorem
-  -- TODO: use a list of theorems, and try them one by one?
-  trace[Progress] "No assumption succeeded: trying to lookup a theorem"
-  let thName ← do
-    match ← pspecAttr.find? fName with
-    | none => throwError "Could not find a pspec theorem for {fName}"
-    | some thName => pure thName
-  trace[Progress] "Lookuped up: {thName}"
-  -- Apply the theorem
-  match ← progressWith fnExpr (.Theorem thName) ids asmTac with
-  | .Ok => return ()
-  | .Error msg => throwError msg
-
-syntax progressArgs := ("as" " ⟨ " (ident)+ " ⟩")?
+    -- It failed: try to lookup a theorem
+    -- TODO: use a list of theorems, and try them one by one?
+    trace[Progress] "No assumption succeeded: trying to lookup a theorem"
+    let thName ← do
+      match ← pspecAttr.find? fName with
+      | none => throwError "Could not find a pspec theorem for {fName}"
+      | some thName => pure thName
+    trace[Progress] "Lookuped up theorem: {thName}"
+    -- Apply the theorem
+    let res ← do
+      try
+        let res ← progressWith fnExpr (.Theorem thName) ids asmTac
+        pure (some res)
+      catch _ => none
+    match res with
+    | some .Ok => return ()
+    | some (.Error msg) => throwError msg
+    | none =>
+    -- Try a recursive call - we try the assumptions of kind "auxDecl"
+    let ctx ← Lean.MonadLCtx.getLCtx
+    let decls ← ctx.getAllDecls
+    let decls := decls.filter (λ decl => match decl.kind with
+      | .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
+      match res with
+      | .Ok => return ()
+      | .Error msg => throwError msg
+    -- Nothing worked: failed
+    throwError "Progress failed"
+
+syntax progressArgs := ("with" ident)? ("as" " ⟨ " (ident)+ " ⟩")?
 
+#check Environment
+#check ConstMap
 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 ids :=
-    if args.size > 0 then
-      let args := (args.get! 0).getArgs
-      let args := (args.get! 2).getArgs
-      args.map Syntax.getId
-    else #[]
+  let withArg := (args.get! 0).getArgs
+  let withArg ← do
+    if withArg.size > 0 then
+      let id := withArg.get! 1
+      trace[Progress] "With arg: {id}"
+      -- Attempt to lookup a local declaration
+      match (← getLCtx).findFromUserName? id.getId with
+      | some decl => do
+        trace[Progress] "With arg: local decl"
+        pure (some (.Local decl))
+      | none => do
+        -- Not a local declaration: should be a theorem
+        trace[Progress] "With arg: theorem"
+        addCompletionInfo <| CompletionInfo.id id id.getId (danglingDot := false) {} none
+        let cs ← resolveGlobalConstWithInfos id
+        match cs with
+        | [] => throwError "Could not find theorem {id}"
+        | id :: _ =>
+          pure (some (.Theorem id))
+    else pure none
+  let args := (args.get! 1).getArgs
+  let args := (args.get! 2).getArgs
+  let ids := args.map Syntax.getId
   trace[Progress] "User-provided ids: {ids}"
-  progressAsmsOrLookupTheorem ids (firstTac [assumptionTac, Arith.scalarTac])
+  progressAsmsOrLookupTheorem withArg ids (firstTac [assumptionTac, Arith.scalarTac])
 
 elab "progress" args:progressArgs : tactic =>
   evalProgress args
@@ -215,16 +260,16 @@ namespace Test
   open Primitives
 
   set_option trace.Progress true
+  set_option pp.rawOnError true
 
   @[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 as ⟨ x ⟩
+      progress with vec_index_test as ⟨ x ⟩
       simp
 
   set_option trace.Progress false
 
-end Test
--/
+end Test -/
 
 end Progress
-- 
cgit v1.2.3


From 753907aafc2502ced0cd8c3f9bc43fb1c4b30e93 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Wed, 19 Jul 2023 14:48:36 +0200
Subject: Cleanup a bit

---
 backends/lean/Base/Progress/Progress.lean | 2 --
 1 file changed, 2 deletions(-)

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

diff --git a/backends/lean/Base/Progress/Progress.lean b/backends/lean/Base/Progress/Progress.lean
index 3b0248fe..9e2461a2 100644
--- a/backends/lean/Base/Progress/Progress.lean
+++ b/backends/lean/Base/Progress/Progress.lean
@@ -218,8 +218,6 @@ def progressAsmsOrLookupTheorem (withTh : Option TheoremOrLocal) (ids : Array Na
 
 syntax progressArgs := ("with" ident)? ("as" " ⟨ " (ident)+ " ⟩")?
 
-#check Environment
-#check ConstMap
 def evalProgress (args : TSyntax `Progress.progressArgs) : TacticM Unit := do
   let args := args.raw
   -- Process the arguments to retrieve the identifiers to use
-- 
cgit v1.2.3


From 36258c9ba583f19b5ddcb3b90e6521f9845b8944 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Wed, 19 Jul 2023 16:41:22 +0200
Subject: Start implementing support for some type classes for progress

---
 backends/lean/Base/Progress/Base.lean     | 64 ++++++++++++++++++++++++-
 backends/lean/Base/Progress/Progress.lean | 78 ++++++++++++++++++++++---------
 2 files changed, 117 insertions(+), 25 deletions(-)

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

diff --git a/backends/lean/Base/Progress/Base.lean b/backends/lean/Base/Progress/Base.lean
index 7eace667..0032c33d 100644
--- a/backends/lean/Base/Progress/Base.lean
+++ b/backends/lean/Base/Progress/Base.lean
@@ -121,19 +121,42 @@ section Methods
 
 end Methods
 
-
 def getPSpecFunName (th : Expr) : MetaM Name :=
   withPSpec th (fun d => do pure d.fName) true
 
+def getPSpecClassFunNames (th : Expr) : MetaM (Name × Name) :=
+  withPSpec th (fun d => do
+    let arg0 := d.args.get! 0
+    arg0.withApp fun f _ => do
+    if ¬ f.isConst then throwError "Not a constant: {f}"
+    pure (d.fName, f.constName)
+    ) true
+
+-- "Regular" pspec attribute
 structure PSpecAttr where
   attr : AttributeImpl
   ext  : MapDeclarationExtension Name
   deriving Inhabited
 
+/- pspec attribute for type classes: we use the name of the type class to
+   lookup another map. We use the *first* argument of the type class to lookup
+   into this second map.
+
+   Example:
+   ========
+   We use type classes for addition. For instance, the addition between two
+   U32 is written (without syntactic sugar) as `HAdd.add (Scalar ) x y`. As a consequence,
+   we store the theorem through the bindings: HAdd.add → Scalar → ...
+-/
+structure PSpecClassAttr where
+  attr : AttributeImpl
+  ext  : MapDeclarationExtension (NameMap Name)
+  deriving Inhabited
+
 /- The persistent map from function to pspec theorems. -/
 initialize pspecAttr : PSpecAttr ← do
   let ext ← mkMapDeclarationExtension `pspecMap
-  let attrImpl := {
+  let attrImpl : AttributeImpl := {
     name := `pspec
     descr := "Marks theorems to use with the `progress` tactic"
     add := fun thName stx attrKind => do
@@ -153,7 +176,44 @@ initialize pspecAttr : PSpecAttr ← do
   registerBuiltinAttribute attrImpl
   pure { attr := attrImpl, ext := ext }
 
+/- The persistent map from type classes to pspec theorems -/
+initialize pspecClassAttr : PSpecClassAttr ← do
+  let ext : MapDeclarationExtension (NameMap Name) ← mkMapDeclarationExtension `pspecClassMap
+  let attrImpl : AttributeImpl  := {
+    name := `cpspec
+    descr := "Marks theorems to use for type classes with the `progress` tactic"
+    add := fun thName stx attrKind => do
+      Attribute.Builtin.ensureNoArgs stx
+      -- TODO: use the attribute kind
+      unless attrKind == AttributeKind.global do
+        throwError "invalid attribute 'cpspec', must be global"
+      -- Lookup the theorem
+      let env ← getEnv
+      let thDecl := env.constants.find! thName
+      let (fName, argName) ← MetaM.run' (getPSpecClassFunNames thDecl.type)
+      trace[Progress] "Registering class spec theorem for ({fName}, {argName})"
+      -- Update the entry if there is one, add an entry if there is none
+      let env :=
+        match (ext.getState (← getEnv)).find? fName with
+        | none =>
+          let m := RBMap.ofList [(argName, thName)]
+          ext.addEntry env (fName, m)
+        | some m =>
+          let m := m.insert argName thName
+          ext.addEntry env (fName, m)
+      setEnv env
+      pure ()
+  }
+  registerBuiltinAttribute attrImpl
+  pure { attr := attrImpl, ext := ext }
+
+
 def PSpecAttr.find? (s : PSpecAttr) (name : Name) : MetaM (Option Name) := do
   return (s.ext.getState (← getEnv)).find? name
 
+def PSpecClassAttr.find? (s : PSpecClassAttr) (className argName : Name) : MetaM (Option Name) := do
+  match (s.ext.getState (← getEnv)).find? className with
+  | none => return none
+  | some map => return map.find? argName
+
 end Progress
diff --git a/backends/lean/Base/Progress/Progress.lean b/backends/lean/Base/Progress/Progress.lean
index 9e2461a2..64d1c14a 100644
--- a/backends/lean/Base/Progress/Progress.lean
+++ b/backends/lean/Base/Progress/Progress.lean
@@ -152,6 +152,15 @@ def progressWith (fnExpr : Expr) (th : TheoremOrLocal) (ids : Array Name)
     --
     pure .Ok
 
+-- Small utility: if `args` is not empty, return the name of the app in the first
+-- arg, if it is a const.
+def getFirstArgAppName (args : Array Expr) : MetaM (Option Name) := do
+  if args.size = 0 then pure none
+  else
+    (args.get! 0).withApp fun f _ => do
+    if f.isConst then pure (some f.constName)
+    else pure none
+
 -- 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
   withMainContext do
@@ -187,34 +196,57 @@ def progressAsmsOrLookupTheorem (withTh : Option TheoremOrLocal) (ids : Array Na
     -- It failed: try to lookup a theorem
     -- TODO: use a list of theorems, and try them one by one?
     trace[Progress] "No assumption succeeded: trying to lookup a theorem"
-    let thName ← do
-      match ← pspecAttr.find? fName with
-      | none => throwError "Could not find a pspec theorem for {fName}"
-      | some thName => pure thName
-    trace[Progress] "Lookuped up theorem: {thName}"
-    -- Apply the theorem
-    let res ← do
-      try
-        let res ← progressWith fnExpr (.Theorem thName) ids asmTac
-        pure (some res)
-      catch _ => none
+    let res ←
+        match ← pspecAttr.find? fName with
+        | some thName =>
+          trace[Progress] "Lookuped up theorem: {thName}"
+          -- Apply the theorem
+          let res ← do
+            try
+              let res ← progressWith fnExpr (.Theorem thName) ids asmTac
+              pure (some res)
+            catch _ => none
+        | none =>
+          trace[Progress] "Could not find a pspec theorem for {fName}"
+          throwError "TODO"
     match res with
     | some .Ok => return ()
     | some (.Error msg) => throwError msg
     | none =>
-    -- Try a recursive call - we try the assumptions of kind "auxDecl"
-    let ctx ← Lean.MonadLCtx.getLCtx
-    let decls ← ctx.getAllDecls
-    let decls := decls.filter (λ decl => match decl.kind with
-      | .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
+      -- It failed: try to lookup a *class* spec theorem
+      let res ← do
+        match ← getFirstArgAppName args with
+        | none => none
+        | some argName => do
+          match ← pspecClassAttr.find? fName argName with
+          | some thName =>
+            trace[Progress] "Lookuped up class theorem: {thName}"
+            -- Apply the theorem
+            let res ← do
+              try
+                let res ← progressWith fnExpr (.Theorem thName) ids asmTac
+                pure (some res)
+              catch _ => none
+          | none =>
+            trace[Progress] "Could not find a pspec theorem for {fName}"
+            pure none
       match res with
-      | .Ok => return ()
-      | .Error msg => throwError msg
-    -- Nothing worked: failed
-    throwError "Progress failed"
+      | some .Ok => return ()
+      | some (.Error msg) => throwError msg
+      | none =>
+      -- Try a recursive call - we try the assumptions of kind "auxDecl"
+      let ctx ← Lean.MonadLCtx.getLCtx
+      let decls ← ctx.getAllDecls
+      let decls := decls.filter (λ decl => match decl.kind with
+        | .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
+        match res with
+        | .Ok => return ()
+        | .Error msg => throwError msg
+      -- Nothing worked: failed
+      throwError "Progress failed"
 
 syntax progressArgs := ("with" ident)? ("as" " ⟨ " (ident)+ " ⟩")?
 
-- 
cgit v1.2.3


From abee28555eb9f95b1c548cc17b9fe746bc982b56 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Wed, 19 Jul 2023 18:50:19 +0200
Subject: Add some utilities for progress

---
 backends/lean/Base/Progress/Base.lean     | 19 +++++++++++++++++++
 backends/lean/Base/Progress/Progress.lean | 21 ++++++++++++++++-----
 2 files changed, 35 insertions(+), 5 deletions(-)

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

diff --git a/backends/lean/Base/Progress/Base.lean b/backends/lean/Base/Progress/Base.lean
index 0032c33d..785b9362 100644
--- a/backends/lean/Base/Progress/Base.lean
+++ b/backends/lean/Base/Progress/Base.lean
@@ -211,9 +211,28 @@ initialize pspecClassAttr : PSpecClassAttr ← do
 def PSpecAttr.find? (s : PSpecAttr) (name : Name) : MetaM (Option Name) := do
   return (s.ext.getState (← getEnv)).find? name
 
+def PSpecAttr.getState (s : PSpecAttr) : MetaM (NameMap Name) := do
+  pure (s.ext.getState (← getEnv))
+
 def PSpecClassAttr.find? (s : PSpecClassAttr) (className argName : Name) : MetaM (Option Name) := do
   match (s.ext.getState (← getEnv)).find? className with
   | none => return none
   | some map => return map.find? argName
 
+def PSpecClassAttr.getState (s : PSpecClassAttr) : MetaM (NameMap (NameMap Name)) := do
+  pure (s.ext.getState (← getEnv))
+
+def showStoredPSpec : MetaM Unit := do
+  let st ← pspecAttr.getState
+  let s := st.toList.foldl (fun s (f, th) => f!"{s}\n{f} → {th}") f!""
+  IO.println s
+
+def showStoredPSpecClass : MetaM Unit := do
+  let st ← pspecClassAttr.getState
+  let s := st.toList.foldl (fun s (f, m) =>
+    let ms := m.toList.foldl (fun s (f, th) =>
+      f!"{s}\n  {f} → {th}") f!""
+    f!"{s}\n{f} → [{ms}]") f!""
+  IO.println s
+
 end Progress
diff --git a/backends/lean/Base/Progress/Progress.lean b/backends/lean/Base/Progress/Progress.lean
index 64d1c14a..9c75ee3c 100644
--- a/backends/lean/Base/Progress/Progress.lean
+++ b/backends/lean/Base/Progress/Progress.lean
@@ -208,7 +208,7 @@ def progressAsmsOrLookupTheorem (withTh : Option TheoremOrLocal) (ids : Array Na
             catch _ => none
         | none =>
           trace[Progress] "Could not find a pspec theorem for {fName}"
-          throwError "TODO"
+          pure none
     match res with
     | some .Ok => return ()
     | some (.Error msg) => throwError msg
@@ -228,7 +228,7 @@ def progressAsmsOrLookupTheorem (withTh : Option TheoremOrLocal) (ids : Array Na
                 pure (some res)
               catch _ => none
           | none =>
-            trace[Progress] "Could not find a pspec theorem for {fName}"
+            trace[Progress] "Could not find a class pspec theorem for ({fName}, {argName})"
             pure none
       match res with
       | some .Ok => return ()
@@ -287,11 +287,22 @@ elab "progress" args:progressArgs : tactic =>
 /-
 -- TODO: remove
 namespace Test
-  open Primitives
+  open Primitives Result
 
   set_option trace.Progress true
-  set_option pp.rawOnError true
 
+  -- #eval do pspecClassAttr.getState
+  -- #eval showStoredPSpec
+  -- #eval showStoredPSpecClass
+
+/-  theorem Scalar.add_spec {ty} {x y : Scalar ty}
+    (hmin : Scalar.min ty ≤ x.val + y.val)
+    (hmax : x.val + y.val ≤ Scalar.max ty) :
+    ∃ z, x + y = ret z ∧ z.val = x.val + y.val := by
+    progress
+    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
@@ -299,7 +310,7 @@ namespace Test
       simp
 
   set_option trace.Progress false
-
+-/
 end Test -/
 
 end Progress
-- 
cgit v1.2.3


From 821b09b14794ebc2fe7b7047fc60fd56fb2cd107 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Wed, 19 Jul 2023 19:03:17 +0200
Subject: Fix a small issue with the persistent state of progress

---
 backends/lean/Base/Progress/Base.lean     | 9 +++++++++
 backends/lean/Base/Progress/Progress.lean | 9 ++++-----
 2 files changed, 13 insertions(+), 5 deletions(-)

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

diff --git a/backends/lean/Base/Progress/Base.lean b/backends/lean/Base/Progress/Base.lean
index 785b9362..72438d40 100644
--- a/backends/lean/Base/Progress/Base.lean
+++ b/backends/lean/Base/Progress/Base.lean
@@ -153,6 +153,15 @@ structure PSpecClassAttr where
   ext  : MapDeclarationExtension (NameMap Name)
   deriving Inhabited
 
+-- TODO: the original function doesn't define correctly the `addImportedFn`. Do a PR?
+def mkMapDeclarationExtension [Inhabited α] (name : Name := by exact decl_name%) : IO (MapDeclarationExtension α) :=
+  registerSimplePersistentEnvExtension {
+    name          := name,
+    addImportedFn := fun a => a.foldl (fun s a => a.foldl (fun s (k, v) => s.insert k v) s) RBMap.empty,
+    addEntryFn    := fun s n => s.insert n.1 n.2 ,
+    toArrayFn     := fun es => es.toArray.qsort (fun a b => Name.quickLt a.1 b.1)
+  }
+
 /- The persistent map from function to pspec theorems. -/
 initialize pspecAttr : PSpecAttr ← do
   let ext ← mkMapDeclarationExtension `pspecMap
diff --git a/backends/lean/Base/Progress/Progress.lean b/backends/lean/Base/Progress/Progress.lean
index 9c75ee3c..84053150 100644
--- a/backends/lean/Base/Progress/Progress.lean
+++ b/backends/lean/Base/Progress/Progress.lean
@@ -291,16 +291,15 @@ namespace Test
 
   set_option trace.Progress true
 
-  -- #eval do pspecClassAttr.getState
-  -- #eval showStoredPSpec
-  -- #eval showStoredPSpecClass
+  #eval showStoredPSpec
+  #eval showStoredPSpecClass
 
-/-  theorem Scalar.add_spec {ty} {x y : Scalar ty}
+  theorem Scalar.add_spec {ty} {x y : Scalar ty}
     (hmin : Scalar.min ty ≤ x.val + y.val)
     (hmax : x.val + y.val ≤ Scalar.max ty) :
     ∃ z, x + y = ret z ∧ z.val = x.val + y.val := by
     progress
-    simp [*] -/
+    simp [*]
 
 /-
   @[pspec]
-- 
cgit v1.2.3


From 975b7c555cbffef2648a6469b777d1f1760d926d Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Thu, 20 Jul 2023 11:22:18 +0200
Subject: Improve progress further

---
 backends/lean/Base/Progress/Base.lean     | 102 +++++++++++++++++++++------
 backends/lean/Base/Progress/Progress.lean | 112 +++++++++++++++++-------------
 2 files changed, 142 insertions(+), 72 deletions(-)

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

diff --git a/backends/lean/Base/Progress/Base.lean b/backends/lean/Base/Progress/Base.lean
index 72438d40..3599d866 100644
--- a/backends/lean/Base/Progress/Base.lean
+++ b/backends/lean/Base/Progress/Base.lean
@@ -62,24 +62,6 @@ section Methods
     -- Dive into the quantified variables and the assumptions
     forallTelescope th fun fvars th => do
     trace[Progress] "Universally quantified arguments and assumptions: {fvars}"
-  /-  -- Filter the argumens which are not propositions
-    let rec getFirstPropIdx (i : Nat) : MetaM Nat := do
-      if i ≥ fargs.size then pure i
-      else do
-        let x := fargs.get! i
-        if ← Meta.isProp (← inferType x) then pure i
-        else getFirstPropIdx (i + 1)
-    let i ← getFirstPropIdx 0
-    let fvars := fargs.extract 0 i
-    let hyps := fargs.extract i fargs.size
-    trace[Progress] "Quantified variables: {fvars}"
-    trace[Progress] "Assumptions: {hyps}"
-    -- Sanity check: all hypotheses are propositions (in particular, all the
-    -- quantified variables are at the beginning)
-    let hypsAreProp ← hyps.allM fun x => do Meta.isProp (← inferType x)
-    if ¬ hypsAreProp then
-      throwError "The theorem doesn't have the proper shape: all the quantified arguments should be at the beginning"
-      -/
     -- Dive into the existentials
     existsTelescope th fun evars th => do
     trace[Progress] "Existentials: {evars}"
@@ -98,6 +80,8 @@ section Methods
     let allArgsFVars ← args.foldlM (fun hs arg => getFVarIds arg hs) HashSet.empty
     -- Sanity check
     if sanityChecks then
+      -- All the variables which appear in the inputs given to the function are
+      -- universally quantified (in particular, they are not *existentially* quantified)
       let fvarsSet : HashSet FVarId := HashSet.ofArray (fvars.map (fun x => x.fvarId!))
       let filtArgsFVars := allArgsFVars.toArray.filter (fun fvar => ¬ fvarsSet.contains fvar)
       if ¬ filtArgsFVars.isEmpty then
@@ -132,6 +116,12 @@ def getPSpecClassFunNames (th : Expr) : MetaM (Name × Name) :=
     pure (d.fName, f.constName)
     ) true
 
+def getPSpecClassFunNameArg (th : Expr) : MetaM (Name × Expr) :=
+  withPSpec th (fun d => do
+    let arg0 := d.args.get! 0
+    pure (d.fName, arg0)
+    ) true
+
 -- "Regular" pspec attribute
 structure PSpecAttr where
   attr : AttributeImpl
@@ -145,14 +135,26 @@ structure PSpecAttr where
    Example:
    ========
    We use type classes for addition. For instance, the addition between two
-   U32 is written (without syntactic sugar) as `HAdd.add (Scalar ) x y`. As a consequence,
+   U32 is written (without syntactic sugar) as `HAdd.add (Scalar ty) x y`. As a consequence,
    we store the theorem through the bindings: HAdd.add → Scalar → ...
+
+   SH: TODO: this (and `PSpecClassExprAttr`) is a bit ad-hoc. For now it works for the
+   specs of the scalar operations, which is what I really need, but I'm not sure it
+   applies well to other situations. A better way would probably to use type classes, but
+   I couldn't get them to work on those cases. It is worth retrying.
 -/
 structure PSpecClassAttr where
   attr : AttributeImpl
   ext  : MapDeclarationExtension (NameMap Name)
   deriving Inhabited
 
+/- Same as `PSpecClassAttr` but we use the full first argument (it works when it
+   is a constant). -/
+structure PSpecClassExprAttr where
+  attr : AttributeImpl
+  ext  : MapDeclarationExtension (HashMap Expr Name)
+  deriving Inhabited
+
 -- TODO: the original function doesn't define correctly the `addImportedFn`. Do a PR?
 def mkMapDeclarationExtension [Inhabited α] (name : Name := by exact decl_name%) : IO (MapDeclarationExtension α) :=
   registerSimplePersistentEnvExtension {
@@ -216,21 +218,69 @@ initialize pspecClassAttr : PSpecClassAttr ← do
   registerBuiltinAttribute attrImpl
   pure { attr := attrImpl, ext := ext }
 
+/- The 2nd persistent map from type classes to pspec theorems -/
+initialize pspecClassExprAttr : PSpecClassExprAttr ← do
+  let ext : MapDeclarationExtension (HashMap Expr Name) ← mkMapDeclarationExtension `pspecClassExprMap
+  let attrImpl : AttributeImpl  := {
+    name := `cepspec
+    descr := "Marks theorems to use for type classes with the `progress` tactic"
+    add := fun thName stx attrKind => do
+      Attribute.Builtin.ensureNoArgs stx
+      -- TODO: use the attribute kind
+      unless attrKind == AttributeKind.global do
+        throwError "invalid attribute 'cpspec', must be global"
+      -- Lookup the theorem
+      let env ← getEnv
+      let thDecl := env.constants.find! thName
+      let (fName, arg) ← MetaM.run' (getPSpecClassFunNameArg thDecl.type)
+      -- Sanity check: no variables appear in the argument
+      MetaM.run' do
+        let fvars ← getFVarIds arg
+        if ¬ fvars.isEmpty then throwError "The first argument ({arg}) contains variables"
+      -- We store two bindings:
+      -- - arg to theorem name
+      -- - reduced arg to theorem name
+      let rarg ← MetaM.run' (reduce arg)
+      trace[Progress] "Registering class spec theorem for ({fName}, {arg}) and ({fName}, {rarg})"
+      -- Update the entry if there is one, add an entry if there is none
+      let env :=
+        match (ext.getState (← getEnv)).find? fName with
+        | none =>
+          let m := HashMap.ofList [(arg, thName), (rarg, thName)]
+          ext.addEntry env (fName, m)
+        | some m =>
+          let m := m.insert arg thName
+          let m := m.insert rarg thName
+          ext.addEntry env (fName, m)
+      setEnv env
+      pure ()
+  }
+  registerBuiltinAttribute attrImpl
+  pure { attr := attrImpl, ext := ext }
+
 
 def PSpecAttr.find? (s : PSpecAttr) (name : Name) : MetaM (Option Name) := do
   return (s.ext.getState (← getEnv)).find? name
 
-def PSpecAttr.getState (s : PSpecAttr) : MetaM (NameMap Name) := do
-  pure (s.ext.getState (← getEnv))
-
 def PSpecClassAttr.find? (s : PSpecClassAttr) (className argName : Name) : MetaM (Option Name) := do
   match (s.ext.getState (← getEnv)).find? className with
   | none => return none
   | some map => return map.find? argName
 
+def PSpecClassExprAttr.find? (s : PSpecClassExprAttr) (className : Name) (arg : Expr) : MetaM (Option Name) := do
+  match (s.ext.getState (← getEnv)).find? className with
+  | none => return none
+  | some map => return map.find? arg
+
+def PSpecAttr.getState (s : PSpecAttr) : MetaM (NameMap Name) := do
+  pure (s.ext.getState (← getEnv))
+
 def PSpecClassAttr.getState (s : PSpecClassAttr) : MetaM (NameMap (NameMap Name)) := do
   pure (s.ext.getState (← getEnv))
 
+def PSpecClassExprAttr.getState (s : PSpecClassExprAttr) : MetaM (NameMap (HashMap Expr Name)) := do
+  pure (s.ext.getState (← getEnv))
+
 def showStoredPSpec : MetaM Unit := do
   let st ← pspecAttr.getState
   let s := st.toList.foldl (fun s (f, th) => f!"{s}\n{f} → {th}") f!""
@@ -244,4 +294,12 @@ def showStoredPSpecClass : MetaM Unit := do
     f!"{s}\n{f} → [{ms}]") f!""
   IO.println s
 
+def showStoredPSpecExprClass : MetaM Unit := do
+  let st ← pspecClassExprAttr.getState
+  let s := st.toList.foldl (fun s (f, m) =>
+    let ms := m.toList.foldl (fun s (f, th) =>
+      f!"{s}\n  {f} → {th}") f!""
+    f!"{s}\n{f} → [{ms}]") f!""
+  IO.println s
+
 end Progress
diff --git a/backends/lean/Base/Progress/Progress.lean b/backends/lean/Base/Progress/Progress.lean
index 84053150..974a6364 100644
--- a/backends/lean/Base/Progress/Progress.lean
+++ b/backends/lean/Base/Progress/Progress.lean
@@ -27,6 +27,9 @@ inductive TheoremOrLocal where
 | Theorem (thName : Name)
 | Local (asm : LocalDecl)
 
+instance : ToMessageData TheoremOrLocal where
+  toMessageData := λ x => match x with | .Theorem thName => m!"{thName}" | .Local asm => m!"{asm.userName}"
+
 /- Type to propagate the errors of `progressWith`.
    We need this because we use the exceptions to backtrack, when trying to
    use the assumptions for instance. When there is actually an error we want
@@ -161,6 +164,32 @@ def getFirstArgAppName (args : Array Expr) : MetaM (Option Name) := do
     if f.isConst then pure (some f.constName)
     else pure none
 
+def getFirstArg (args : Array Expr) : Option Expr := do
+  if args.size = 0 then none
+  else some (args.get! 0)
+
+/- 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)
+  (kind : String) (th : Option TheoremOrLocal) (x : TacticM Unit) : TacticM Unit := do
+  let res ← do
+    match th with
+    | none =>
+      trace[Progress] "Could not find a {kind}"
+      pure none
+    | some th => do
+      trace[Progress] "Lookuped up {kind}: {th}"
+      -- Apply the theorem
+      let res ← do
+        try
+          let res ← progressWith fnExpr th ids asmTac
+          pure (some res)
+        catch _ => none
+  match res with
+  | some .Ok => return ()
+  | some (.Error msg) => throwError msg
+  | 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
   withMainContext do
@@ -196,57 +225,40 @@ def progressAsmsOrLookupTheorem (withTh : Option TheoremOrLocal) (ids : Array Na
     -- It failed: try to lookup a theorem
     -- TODO: use a list of theorems, and try them one by one?
     trace[Progress] "No assumption succeeded: trying to lookup a theorem"
-    let res ←
-        match ← pspecAttr.find? fName with
-        | some thName =>
-          trace[Progress] "Lookuped up theorem: {thName}"
-          -- Apply the theorem
-          let res ← do
-            try
-              let res ← progressWith fnExpr (.Theorem thName) ids asmTac
-              pure (some res)
-            catch _ => none
-        | none =>
-          trace[Progress] "Could not find a pspec theorem for {fName}"
-          pure none
-    match res with
-    | some .Ok => return ()
-    | some (.Error msg) => throwError msg
-    | none =>
-      -- It failed: try to lookup a *class* spec theorem
-      let res ← do
-        match ← getFirstArgAppName args with
-        | none => none
-        | some argName => do
-          match ← pspecClassAttr.find? fName argName with
-          | some thName =>
-            trace[Progress] "Lookuped up class theorem: {thName}"
-            -- Apply the theorem
-            let res ← do
-              try
-                let res ← progressWith fnExpr (.Theorem thName) ids asmTac
-                pure (some res)
-              catch _ => none
-          | none =>
-            trace[Progress] "Could not find a class pspec theorem for ({fName}, {argName})"
-            pure none
+    let pspec ← do
+      let thName ← pspecAttr.find? fName
+      pure (thName.map fun th => .Theorem th)
+    tryLookupApply 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
+      match getFirstArg args with
+      | none => pure none
+      | 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
+    -- It failed: try to lookup a *class* spec theorem
+    let pspecClass ← do
+      match ← getFirstArgAppName args with
+      | none => pure none
+      | 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
+    -- Try a recursive call - we try the assumptions of kind "auxDecl"
+    let ctx ← Lean.MonadLCtx.getLCtx
+    let decls ← ctx.getAllDecls
+    let decls := decls.filter (λ decl => match decl.kind with
+      | .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
       match res with
-      | some .Ok => return ()
-      | some (.Error msg) => throwError msg
-      | none =>
-      -- Try a recursive call - we try the assumptions of kind "auxDecl"
-      let ctx ← Lean.MonadLCtx.getLCtx
-      let decls ← ctx.getAllDecls
-      let decls := decls.filter (λ decl => match decl.kind with
-        | .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
-        match res with
-        | .Ok => return ()
-        | .Error msg => throwError msg
-      -- Nothing worked: failed
-      throwError "Progress failed"
+      | .Ok => return ()
+      | .Error msg => throwError msg
+    -- Nothing worked: failed
+    throwError "Progress failed"
 
 syntax progressArgs := ("with" ident)? ("as" " ⟨ " (ident)+ " ⟩")?
 
-- 
cgit v1.2.3


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

---
 backends/lean/Base/Progress/Base.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

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

diff --git a/backends/lean/Base/Progress/Base.lean b/backends/lean/Base/Progress/Base.lean
index 3599d866..2fbd24dd 100644
--- a/backends/lean/Base/Progress/Base.lean
+++ b/backends/lean/Base/Progress/Base.lean
@@ -240,7 +240,7 @@ initialize pspecClassExprAttr : PSpecClassExprAttr ← do
       -- We store two bindings:
       -- - arg to theorem name
       -- - reduced arg to theorem name
-      let rarg ← MetaM.run' (reduce arg)
+      let rarg ← MetaM.run' (reduceAll arg)
       trace[Progress] "Registering class spec theorem for ({fName}, {arg}) and ({fName}, {rarg})"
       -- Update the entry if there is one, add an entry if there is none
       let env :=
-- 
cgit v1.2.3


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/Progress/Progress.lean | 55 +++++++++++++++++++------------
 1 file changed, 34 insertions(+), 21 deletions(-)

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

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 [*]
 
 /-
-- 
cgit v1.2.3


From 03492250b45855fe9db5e0a28a96166607cd84a1 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Thu, 20 Jul 2023 14:14:34 +0200
Subject: Make some proofs in Hashmap/Properties.lean and improve progress

---
 backends/lean/Base/Progress/Base.lean     | 25 ++++++++----
 backends/lean/Base/Progress/Progress.lean | 68 ++++++++++---------------------
 2 files changed, 39 insertions(+), 54 deletions(-)

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

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
-- 
cgit v1.2.3


From 9b1498aa7fe014ac430467919504d35b0a688934 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Thu, 20 Jul 2023 16:13:35 +0200
Subject: Fix a naming issue with progress

---
 backends/lean/Base/Progress/Progress.lean | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

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

diff --git a/backends/lean/Base/Progress/Progress.lean b/backends/lean/Base/Progress/Progress.lean
index dabd25b8..1c509775 100644
--- a/backends/lean/Base/Progress/Progress.lean
+++ b/backends/lean/Base/Progress/Progress.lean
@@ -118,17 +118,17 @@ def progressWith (fExpr : Expr) (th : TheoremOrLocal) (keep : Option Name) (ids
         match hPost with
         | none => do return (.Error m!"Too many ids provided ({ids}): there is no postcondition to split")
         | some hPost => pure hPost
-      let curPostId := (← hPost.fvarId!.getDecl).userName
-      let rec splitPost (hPost : Expr) (ids : List Name) : TacticM ProgressError := do
+      let rec splitPost (prevId : Name) (hPost : Expr) (ids : List Name) : TacticM ProgressError := do
         match ids with
         | [] => pure .Ok -- Stop
         | nid :: ids => do
           trace[Progress] "Splitting post: {hPost}"
           -- Split
           if ← isConj (← inferType hPost) then
-            splitConjTac hPost (some (nid, curPostId)) (λ _ nhPost => splitPost nhPost ids)
+            splitConjTac hPost (some (prevId, nid)) (λ _ nhPost => splitPost nid nhPost ids)
           else return (.Error m!"Too many ids provided ({nid :: ids}) not enough conjuncts to split in the postcondition")
-      splitPost hPost ids
+      let curPostId := (← hPost.fvarId!.getDecl).userName
+      splitPost curPostId hPost ids
     else return .Ok
   match res with
   | .Error _ => return res -- Can we get there? We're using "return"
-- 
cgit v1.2.3


From 2dd56a51df01421fe7766858c9d37998db4123b5 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Tue, 25 Jul 2023 11:53:49 +0200
Subject: Improve the syntax of progress: `as ⟨ x, y .. ⟩`

---
 backends/lean/Base/Progress/Progress.lean | 77 ++++++++++++++++++-------------
 1 file changed, 46 insertions(+), 31 deletions(-)

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

diff --git a/backends/lean/Base/Progress/Progress.lean b/backends/lean/Base/Progress/Progress.lean
index 1c509775..c8f94e9e 100644
--- a/backends/lean/Base/Progress/Progress.lean
+++ b/backends/lean/Base/Progress/Progress.lean
@@ -23,7 +23,8 @@ inductive ProgressError
 | Error (msg : MessageData)
 deriving Inhabited
 
-def progressWith (fExpr : Expr) (th : TheoremOrLocal) (keep : Option Name) (ids : Array Name)
+def progressWith (fExpr : Expr) (th : TheoremOrLocal)
+  (keep : Option Name) (ids : Array Name) (splitPost : Bool)
   (asmTac : TacticM Unit) : TacticM ProgressError := do
   /- Apply the theorem
      We try to match the theorem with the goal
@@ -112,24 +113,31 @@ def progressWith (fExpr : Expr) (th : TheoremOrLocal) (keep : Option Name) (ids
         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
-    if ¬ ids.isEmpty then
-      let hPost ←
-        match hPost with
-        | none => do return (.Error m!"Too many ids provided ({ids}): there is no postcondition to split")
-        | some hPost => pure hPost
-      let rec splitPost (prevId : Name) (hPost : Expr) (ids : List Name) : TacticM ProgressError := do
+    -- Continue splitting following the post following the user's instructions
+    match hPost with
+    | none =>
+      -- Sanity check
+      if ¬ ids.isEmpty then
+        return (.Error m!"Too many ids provided ({ids}): there is no postcondition to split")
+      else return .Ok
+    | some hPost => do
+      let rec splitPostWithIds (prevId : Name) (hPost : Expr) (ids : List Name) : TacticM ProgressError := do
         match ids with
-        | [] => pure .Ok -- Stop
+        | [] =>
+          /- We used all the user provided ids.
+             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)
+          else pure .Ok
         | nid :: ids => do
           trace[Progress] "Splitting post: {hPost}"
           -- Split
           if ← isConj (← inferType hPost) then
-            splitConjTac hPost (some (prevId, nid)) (λ _ nhPost => splitPost nid nhPost ids)
+            splitConjTac hPost (some (prevId, nid)) (λ _ nhPost => splitPostWithIds nid nhPost ids)
           else return (.Error m!"Too many ids provided ({nid :: ids}) not enough conjuncts to split in the postcondition")
       let curPostId := (← hPost.fvarId!.getDecl).userName
-      splitPost curPostId hPost ids
-    else return .Ok
+      splitPostWithIds curPostId hPost ids
   match res with
   | .Error _ => return res -- Can we get there? We're using "return"
   | .Ok =>
@@ -160,7 +168,8 @@ 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) (fExpr : Expr)
+def tryLookupApply (keep : Option Name) (ids : Array Name) (splitPost : Bool)
+  (asmTac : TacticM Unit) (fExpr : Expr)
   (kind : String) (th : Option TheoremOrLocal) (x : TacticM Unit) : TacticM Unit := do
   let res ← do
     match th with
@@ -172,7 +181,7 @@ def tryLookupApply (keep : Option Name) (ids : Array Name) (asmTac : TacticM Uni
       -- Apply the theorem
       let res ← do
         try
-          let res ← progressWith fExpr th keep ids asmTac
+          let res ← progressWith fExpr th keep ids splitPost asmTac
           pure (some res)
         catch _ => none
   match res with
@@ -181,7 +190,8 @@ def tryLookupApply (keep : Option Name) (ids : Array Name) (asmTac : TacticM Uni
   | none => x
 
 -- The array of ids are identifiers to use when introducing fresh variables
-def progressAsmsOrLookupTheorem (keep : Option Name) (withTh : Option TheoremOrLocal) (ids : Array Name) (asmTac : TacticM Unit) : TacticM Unit := do
+def progressAsmsOrLookupTheorem (keep : Option Name) (withTh : Option TheoremOrLocal)
+  (ids : Array Name) (splitPost : Bool) (asmTac : TacticM Unit) : TacticM Unit := do
   withMainContext do
   -- Retrieve the goal
   let mgoal ← Tactic.getMainGoal
@@ -197,7 +207,7 @@ def progressAsmsOrLookupTheorem (keep : Option Name) (withTh : Option TheoremOrL
   -- Otherwise, lookup one.
   match withTh with
   | some th => do
-    match ← progressWith fExpr th keep ids asmTac with
+    match ← progressWith fExpr th keep ids splitPost asmTac with
     | .Ok => return ()
     | .Error msg => throwError msg
   | none =>
@@ -206,7 +216,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 fExpr (.Local decl) keep ids asmTac catch _ => continue
+      let res ← do try progressWith fExpr (.Local decl) keep ids splitPost asmTac catch _ => continue
       match res with
       | .Ok => return ()
       | .Error msg => throwError msg
@@ -216,7 +226,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 fExpr "pspec theorem" pspec do
+    tryLookupApply keep ids splitPost 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
@@ -225,7 +235,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 fExpr "pspec class expr theorem" pspecClassExpr do
+    tryLookupApply keep ids splitPost asmTac fExpr "pspec class expr theorem" pspecClassExpr do
     -- It failed: try to lookup a *class* spec theorem
     let pspecClass ← do
       match ← getFirstArgAppName args with
@@ -233,7 +243,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 fExpr "pspec class theorem" pspecClass do
+    tryLookupApply keep ids splitPost 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
@@ -241,14 +251,14 @@ 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 fExpr (.Local decl) keep ids asmTac catch _ => continue
+      let res ← do try progressWith fExpr (.Local decl) keep ids splitPost asmTac catch _ => continue
       match res with
       | .Ok => return ()
       | .Error msg => throwError msg
     -- Nothing worked: failed
     throwError "Progress failed"
 
-syntax progressArgs := ("keep" ("as" (ident))?)? ("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
@@ -263,8 +273,8 @@ def evalProgress (args : TSyntax `Progress.progressArgs) : TacticM Unit := do
       else do pure (some (← mkFreshUserName `h))
     else pure none
   trace[Progress] "Keep: {keep}"
-  let withArg := (args.get! 1).getArgs
   let withArg ← do
+    let withArg := (args.get! 1).getArgs
     if withArg.size > 0 then
       let id := withArg.get! 1
       trace[Progress] "With arg: {id}"
@@ -283,20 +293,25 @@ def evalProgress (args : TSyntax `Progress.progressArgs) : TacticM Unit := do
         | id :: _ =>
           pure (some (.Theorem id))
     else pure none
-  let args := (args.get! 2).getArgs
-  let args := (args.get! 2).getArgs
-  let ids := args.map Syntax.getId
+  let ids :=
+    let args := (args.get! 2).getArgs
+    let args := (args.get! 2).getSepArgs
+    args.map Syntax.getId
   trace[Progress] "User-provided ids: {ids}"
-  progressAsmsOrLookupTheorem keep withArg ids (firstTac [assumptionTac, Arith.scalarTac])
+  let splitPost : Bool :=
+    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])
 
 elab "progress" args:progressArgs : tactic =>
   evalProgress args
 
-/-
-namespace Test
+/-namespace Test
   open Primitives Result
 
   set_option trace.Progress true
+  set_option pp.rawOnError true
 
   #eval showStoredPSpec
   #eval showStoredPSpecClass
@@ -306,9 +321,9 @@ namespace Test
     (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
+    progress keep as h as ⟨ z, h1 .. ⟩
     simp [*]
 
-end Test -/
+end Test-/
 
 end Progress
-- 
cgit v1.2.3


From c652e97f7ab13164150331b4aa3f2e7ef11d24b9 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Tue, 25 Jul 2023 12:13:20 +0200
Subject: Add the possibility of using "_" as ident for progress

---
 backends/lean/Base/Progress/Progress.lean | 37 ++++++++++++++++++-------------
 1 file changed, 21 insertions(+), 16 deletions(-)

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

diff --git a/backends/lean/Base/Progress/Progress.lean b/backends/lean/Base/Progress/Progress.lean
index c8f94e9e..c0ddc63d 100644
--- a/backends/lean/Base/Progress/Progress.lean
+++ b/backends/lean/Base/Progress/Progress.lean
@@ -24,7 +24,7 @@ inductive ProgressError
 deriving Inhabited
 
 def progressWith (fExpr : Expr) (th : TheoremOrLocal)
-  (keep : Option Name) (ids : Array Name) (splitPost : Bool)
+  (keep : Option Name) (ids : Array (Option Name)) (splitPost : Bool)
   (asmTac : TacticM Unit) : TacticM ProgressError := do
   /- Apply the theorem
      We try to match the theorem with the goal
@@ -90,13 +90,14 @@ def progressWith (fExpr : Expr) (th : TheoremOrLocal)
     -- For the conjunctions, we split according once to separate the equality `f ... = .ret ...`
     -- from the postcondition, if there is, then continue to split the postcondition if there
     -- are remaining ids.
-    let splitEqAndPost (k : Expr → Option Expr → List Name → TacticM ProgressError) : TacticM ProgressError := do
+    let splitEqAndPost (k : Expr → Option Expr → List (Option Name) → TacticM ProgressError) : TacticM ProgressError := do
       if ← isConj (← inferType h) then do
         let hName := (← h.fvarId!.getDecl).userName
-        let (optId, ids) := listTryPopHead ids
-        let optIds ← match optId with
-          | none => do pure (some (hName, ← mkFreshUserName `h))
-          | some id => do pure (some (hName, id))
+        let (optIds, ids) ← do
+          match ids with
+          | [] => do pure (some (hName, ← mkFreshUserName `h), [])
+          | none :: ids => do pure (some (hName, ← mkFreshUserName `h), 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
     -- Simplify the target by using the equality and some monad simplifications,
@@ -121,8 +122,8 @@ def progressWith (fExpr : Expr) (th : TheoremOrLocal)
         return (.Error m!"Too many ids provided ({ids}): there is no postcondition to split")
       else return .Ok
     | some hPost => do
-      let rec splitPostWithIds (prevId : Name) (hPost : Expr) (ids : List Name) : TacticM ProgressError := do
-        match ids with
+      let rec splitPostWithIds (prevId : Name) (hPost : Expr) (ids0 : List (Option Name)) : TacticM ProgressError := do
+        match ids0 with
         | [] =>
           /- We used all the user provided ids.
              Split the remaining conjunctions by using fresh ids if the user
@@ -133,9 +134,13 @@ def progressWith (fExpr : Expr) (th : TheoremOrLocal)
         | nid :: ids => do
           trace[Progress] "Splitting post: {hPost}"
           -- Split
+          let nid ← do
+            match nid with
+            | none => mkFreshUserName `h
+            | some nid => pure nid
           if ← isConj (← inferType hPost) then
             splitConjTac hPost (some (prevId, nid)) (λ _ nhPost => splitPostWithIds nid nhPost ids)
-          else return (.Error m!"Too many ids provided ({nid :: ids}) not enough conjuncts to split in the postcondition")
+          else return (.Error m!"Too many ids provided ({ids0}) not enough conjuncts to split in the postcondition")
       let curPostId := (← hPost.fvarId!.getDecl).userName
       splitPostWithIds curPostId hPost ids
   match res with
@@ -168,7 +173,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) (splitPost : Bool)
+def tryLookupApply (keep : Option Name) (ids : Array (Option Name)) (splitPost : Bool)
   (asmTac : TacticM Unit) (fExpr : Expr)
   (kind : String) (th : Option TheoremOrLocal) (x : TacticM Unit) : TacticM Unit := do
   let res ← do
@@ -191,7 +196,7 @@ def tryLookupApply (keep : Option Name) (ids : Array Name) (splitPost : Bool)
 
 -- The array of ids are identifiers to use when introducing fresh variables
 def progressAsmsOrLookupTheorem (keep : Option Name) (withTh : Option TheoremOrLocal)
-  (ids : Array Name) (splitPost : Bool) (asmTac : TacticM Unit) : TacticM Unit := do
+  (ids : Array (Option Name)) (splitPost : Bool) (asmTac : TacticM Unit) : TacticM Unit := do
   withMainContext do
   -- Retrieve the goal
   let mgoal ← Tactic.getMainGoal
@@ -258,7 +263,7 @@ 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" ("as" (ident))?)? ("with" ident)? ("as" " ⟨ " (ident <|> "_"),* " .."? " ⟩")?
 
 def evalProgress (args : TSyntax `Progress.progressArgs) : TacticM Unit := do
   let args := args.raw
@@ -296,7 +301,7 @@ def evalProgress (args : TSyntax `Progress.progressArgs) : TacticM Unit := do
   let ids :=
     let args := (args.get! 2).getArgs
     let args := (args.get! 2).getSepArgs
-    args.map Syntax.getId
+    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
@@ -307,7 +312,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
@@ -321,9 +326,9 @@ elab "progress" args:progressArgs : tactic =>
     (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 ⟨ z, h1 .. ⟩
+    progress keep as h as ⟨ x, h1 .. ⟩
     simp [*]
 
-end Test-/
+end Test -/
 
 end Progress
-- 
cgit v1.2.3


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/Progress/Progress.lean | 13 ++++++++++++-
 1 file changed, 12 insertions(+), 1 deletion(-)

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

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.2.3


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

---
 backends/lean/Base/Progress/Base.lean     | 4 ++--
 backends/lean/Base/Progress/Progress.lean | 4 ++--
 2 files changed, 4 insertions(+), 4 deletions(-)

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

diff --git a/backends/lean/Base/Progress/Base.lean b/backends/lean/Base/Progress/Base.lean
index b54bdf7a..6f820a84 100644
--- a/backends/lean/Base/Progress/Base.lean
+++ b/backends/lean/Base/Progress/Base.lean
@@ -81,8 +81,8 @@ section Methods
     let (fExpr, f, args) ← do
       if mf.isConst ∧ mf.constName = ``Bind.bind then do
         -- Dive into the bind
-        let fExpr := margs.get! 4
-        fExpr.consumeMData.withApp fun f args => pure (fExpr, f, args)
+        let fExpr := (margs.get! 4).consumeMData
+        fExpr.withApp fun f args => pure (fExpr, f, args)
       else pure (mExpr, mf, margs)
     trace[Progress] "After stripping the arguments of the function call:\n- f: {f}\n- args: {args}"
     if ¬ f.isConst then throwError "Not a constant: {f}"
diff --git a/backends/lean/Base/Progress/Progress.lean b/backends/lean/Base/Progress/Progress.lean
index a281f1d2..a2c7764f 100644
--- a/backends/lean/Base/Progress/Progress.lean
+++ b/backends/lean/Base/Progress/Progress.lean
@@ -58,9 +58,9 @@ def progressWith (fExpr : Expr) (th : TheoremOrLocal)
     let (thBody, _) ← destEq thBody
     trace[Progress] "After splitting equality: {thBody}"
     -- There shouldn't be any existential variables in thBody
-    pure thBody
+    pure thBody.consumeMData
   -- Match the body with the target
-  trace[Progress] "Matching `{thBody}` with `{fExpr}`"
+  trace[Progress] "Matching:\n- body:\n{thBody}\n- target:\n{fExpr}"
   let ok ← isDefEq thBody fExpr
   if ¬ ok then throwError "Could not unify the theorem with the target:\n- theorem: {thBody}\n- target: {fExpr}"
   let mgoal ← Tactic.getMainGoal
-- 
cgit v1.2.3


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/Progress/Progress.lean | 34 +++++++++++++++++++++++++------
 1 file changed, 28 insertions(+), 6 deletions(-)

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

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
-- 
cgit v1.2.3


From 81e991822879a942af34489b7a072f31739f28f6 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Wed, 26 Jul 2023 12:37:17 +0200
Subject: Update the syntax of the progress tactic

---
 backends/lean/Base/Progress/Progress.lean | 41 +++++++++++++++++--------------
 1 file changed, 22 insertions(+), 19 deletions(-)

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

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` -/
-- 
cgit v1.2.3


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

---
 backends/lean/Base/Progress/Progress.lean | 17 ++++++++++++-----
 1 file changed, 12 insertions(+), 5 deletions(-)

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

diff --git a/backends/lean/Base/Progress/Progress.lean b/backends/lean/Base/Progress/Progress.lean
index 9300edff..6a4729dc 100644
--- a/backends/lean/Base/Progress/Progress.lean
+++ b/backends/lean/Base/Progress/Progress.lean
@@ -162,6 +162,7 @@ def progressWith (fExpr : Expr) (th : TheoremOrLocal)
     allGoals asmTac
     let newGoals ← getUnsolvedGoals
     setGoals (newGoals ++ curGoals)
+    trace[Progress] "progress: replaced the goals"
     --
     pure .Ok
 
@@ -281,12 +282,15 @@ def evalProgress (args : TSyntax `Progress.progressArgs) : TacticM Unit := do
     | [keepArg, withArg, asArgs] => do pure (keepArg, withArg, asArgs)
     | _ => throwError "Unexpected: invalid arguments"
   let keep : Option Name ← do
+    trace[Progress] "Keep arg: {keepArg}"
     let args := keepArg.getArgs
-    trace[Progress] "Keep args: {args}"
-    let arg := args.get! 1
-    trace[Progress] "Keep arg: {arg}"
-    if arg.isIdent then pure (some arg.getId)
-    else do pure (some (← mkFreshAnonPropUserName))
+    if args.size > 0 then do
+      trace[Progress] "Keep args: {args}"
+      let arg := args.get! 1
+      trace[Progress] "Keep arg: {arg}"
+      if arg.isIdent then pure (some arg.getId)
+      else do pure (some (← mkFreshAnonPropUserName))
+    else do pure none
   trace[Progress] "Keep: {keep}"
   let withArg ← do
     let withArg := withArg.getArgs
@@ -328,7 +332,10 @@ def evalProgress (args : TSyntax `Progress.progressArgs) : TacticM Unit := do
     else
       throwError "Not a linear arithmetic goal"
   progressAsmsOrLookupTheorem keep withArg ids splitPost (
+    withMainContext do
+    trace[Progress] "trying to solve assumption: {← getMainGoal}"
     firstTac [assumptionTac, scalarTac])
+  trace[Diverge] "Progress done"
 
 elab "progress" args:progressArgs : tactic =>
   evalProgress args
-- 
cgit v1.2.3