From 9515bbad5b58ed1c51ac6d9fc9d7a4e5884b6273 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Thu, 6 Jul 2023 15:23:53 +0200
Subject: Reorganize a bit the lean backend files

---
 backends/lean/Base/Utils.lean | 119 ++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 119 insertions(+)
 create mode 100644 backends/lean/Base/Utils.lean

(limited to 'backends/lean/Base/Utils.lean')

diff --git a/backends/lean/Base/Utils.lean b/backends/lean/Base/Utils.lean
new file mode 100644
index 00000000..161b9ddb
--- /dev/null
+++ b/backends/lean/Base/Utils.lean
@@ -0,0 +1,119 @@
+import Lean
+
+namespace Utils
+
+open Lean Elab Term Meta
+
+-- Useful helper to explore definitions and figure out the variant
+-- of their sub-expressions.
+def explore_term (incr : String) (e : Expr) : MetaM Unit :=
+  match e with
+  | .bvar _ => do logInfo m!"{incr}bvar: {e}"; return ()
+  | .fvar _ => do logInfo m!"{incr}fvar: {e}"; return ()
+  | .mvar _ => do logInfo m!"{incr}mvar: {e}"; return ()
+  | .sort _ => do logInfo m!"{incr}sort: {e}"; return ()
+  | .const _ _ => do logInfo m!"{incr}const: {e}"; return ()
+  | .app fn arg => do
+    logInfo m!"{incr}app: {e}"
+    explore_term (incr ++ "  ") fn
+    explore_term (incr ++ "  ") arg
+  | .lam _bName bTy body _binfo => do
+    logInfo m!"{incr}lam: {e}"
+    explore_term (incr ++ "  ") bTy
+    explore_term (incr ++ "  ") body
+  | .forallE _bName bTy body _bInfo => do
+    logInfo m!"{incr}forallE: {e}"
+    explore_term (incr ++ "  ") bTy
+    explore_term (incr ++ "  ") body
+  | .letE _dName ty val body _nonDep => do
+    logInfo m!"{incr}letE: {e}"
+    explore_term (incr ++ "  ") ty
+    explore_term (incr ++ "  ") val
+    explore_term (incr ++ "  ") body
+  | .lit _ => do logInfo m!"{incr}lit: {e}"; return ()
+  | .mdata _ e => do
+    logInfo m!"{incr}mdata: {e}"
+    explore_term (incr ++ "  ") e
+  | .proj _ _ struct => do
+    logInfo m!"{incr}proj: {e}"
+    explore_term (incr ++ "  ") struct
+
+def explore_decl (n : Name) : TermElabM Unit := do
+  logInfo m!"Name: {n}"
+  let env ← getEnv
+  let decl := env.constants.find! n
+  match decl with
+  | .defnInfo val =>
+     logInfo m!"About to explore defn: {decl.name}"
+     logInfo m!"# Type:"
+     explore_term "" val.type
+     logInfo m!"# Value:"
+     explore_term "" val.value
+  | .axiomInfo _  => throwError m!"axiom: {n}"
+  | .thmInfo _    => throwError m!"thm: {n}"
+  | .opaqueInfo _ => throwError m!"opaque: {n}"
+  | .quotInfo _   => throwError m!"quot: {n}"
+  | .inductInfo _ => throwError m!"induct: {n}"
+  | .ctorInfo _   => throwError m!"ctor: {n}"
+  | .recInfo _    => throwError m!"rec: {n}"
+
+syntax (name := printDecl) "print_decl " ident : command
+
+open Lean.Elab.Command
+
+@[command_elab printDecl] def elabPrintDecl : CommandElab := fun stx => do
+  liftTermElabM do
+    let id := stx[1]
+    addCompletionInfo <| CompletionInfo.id id id.getId (danglingDot := false) {} none
+    let cs ← resolveGlobalConstWithInfos id
+    explore_decl cs[0]!
+
+private def test1 : Nat := 0
+private def test2 (x : Nat) : Nat := x
+
+print_decl test1
+print_decl test2
+
+-- A map visitor function for expressions (adapted from `AbstractNestedProofs.visit`)
+-- The continuation takes as parameters:
+-- - the current depth of the expression (useful for printing/debugging)
+-- - the expression to explore
+partial def mapVisit (k : Nat → Expr → MetaM Expr) (e : Expr) : MetaM Expr := do
+  let mapVisitBinders (xs : Array Expr) (k2 : MetaM Expr) : MetaM Expr := do
+    let localInstances ← getLocalInstances
+    let mut lctx ← getLCtx
+    for x in xs do
+      let xFVarId := x.fvarId!
+      let localDecl ← xFVarId.getDecl
+      let type      ← mapVisit k localDecl.type
+      let localDecl := localDecl.setType type
+      let localDecl ← match localDecl.value? with
+         | some value => let value ← mapVisit k value; pure <| localDecl.setValue value
+         | none       => pure localDecl
+      lctx :=lctx.modifyLocalDecl xFVarId fun _ => localDecl
+    withLCtx lctx localInstances k2
+  -- TODO: use a cache? (Lean.checkCache)
+  let rec visit (i : Nat) (e : Expr) : MetaM Expr := do
+    -- Explore
+    let e ← k i e
+    match e with
+    | .bvar _
+    | .fvar _
+    | .mvar _
+    | .sort _
+    | .lit _
+    | .const _ _ => pure e
+    | .app .. => do e.withApp fun f args => return mkAppN f (← args.mapM (visit (i + 1)))
+    | .lam .. =>
+      lambdaLetTelescope e fun xs b =>
+        mapVisitBinders xs do mkLambdaFVars xs (← visit (i + 1) b) (usedLetOnly := false)
+    | .forallE .. => do
+      forallTelescope e fun xs b => mapVisitBinders xs do mkForallFVars xs (← visit (i + 1) b)
+    | .letE .. => do
+      lambdaLetTelescope e fun xs b => mapVisitBinders xs do
+        mkLambdaFVars xs (← visit (i + 1) b) (usedLetOnly := false)
+    | .mdata _ b => return e.updateMData! (← visit (i + 1) b)
+    | .proj _ _ b => return e.updateProj! (← visit (i + 1) b)
+  visit 0 e
+
+end Utils
-- 
cgit v1.2.3


From 7206b48a73d6204baea99f4f4675be2518a8f8c2 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Mon, 10 Jul 2023 15:06:12 +0200
Subject: Start working on the progress tactic

---
 backends/lean/Base/Utils.lean | 95 +++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 95 insertions(+)

(limited to 'backends/lean/Base/Utils.lean')

diff --git a/backends/lean/Base/Utils.lean b/backends/lean/Base/Utils.lean
index 161b9ddb..2ce63620 100644
--- a/backends/lean/Base/Utils.lean
+++ b/backends/lean/Base/Utils.lean
@@ -116,4 +116,99 @@ partial def mapVisit (k : Nat → Expr → MetaM Expr) (e : Expr) : MetaM Expr :
     | .proj _ _ b => return e.updateProj! (← visit (i + 1) b)
   visit 0 e
 
+section Methods
+  variable [MonadLiftT MetaM m] [MonadControlT MetaM m] [Monad m] [MonadError m]
+  variable {a : Type}
+
+  /- Like `lambdaTelescopeN` but only destructs a fixed number of lambdas -/
+  def lambdaTelescopeN (e : Expr) (n : Nat) (k : Array Expr → Expr → m a) : m a :=
+    lambdaTelescope e fun xs body => do
+    if xs.size < n then throwError "lambdaTelescopeN: not enough lambdas"
+    let xs := xs.extract 0 n
+    let ys := xs.extract n xs.size
+    let body ← liftMetaM (mkLambdaFVars ys body)
+    k xs body
+
+  /- Like `lambdaTelescope`, but only destructs one lambda
+     TODO: is there an equivalent of this function somewhere in the
+     standard library? -/
+  def lambdaOne (e : Expr) (k : Expr → Expr → m a) : m a :=
+    lambdaTelescopeN e 1 λ xs b => k (xs.get! 0) b
+
+  def isExists (e : Expr) : Bool := e.getAppFn.isConstOf ``Exists ∧ e.getAppNumArgs = 2
+
+  -- Remark: Lean doesn't find the inhabited and nonempty instances if we don'
+  -- put them explicitely in the signature
+  partial def existsTelescopeProcess [Inhabited (m a)] [Nonempty (m a)]
+    (fvars : Array Expr) (e : Expr) (k : Array Expr → Expr → m a) : m a := do
+    -- Attempt to deconstruct an existential
+    if isExists e then do
+      let p := e.appArg!
+      lambdaOne p fun x ne =>
+      existsTelescopeProcess (fvars.push x) ne k
+    else
+      -- No existential: call the continuation
+      k fvars e
+
+  def existsTelescope [Inhabited (m a)] [Nonempty (m a)] (e : Expr) (k : Array Expr → Expr → m a) : m a := do
+    existsTelescopeProcess #[] e k
+
+end Methods
+
+def addDecl (name : Name) (val : Expr) (type : Expr) (asLet : Bool) : Tactic.TacticM Expr :=
+  -- I don't think we need that
+  Lean.Elab.Tactic.withMainContext do
+  -- Insert the new declaration
+  let withDecl := if asLet then withLetDecl name type val else withLocalDeclD name type
+  withDecl fun nval => do
+    -- For debugging
+    let lctx ← Lean.MonadLCtx.getLCtx
+    let fid := nval.fvarId!
+    let decl := lctx.get! fid
+    trace[Arith] "  new decl: \"{decl.userName}\" ({nval}) : {decl.type} := {decl.value}"
+    --
+    -- Tranform the main goal `?m0` to `let x = nval in ?m1`
+    let mvarId ← Tactic.getMainGoal
+    let newMVar ← mkFreshExprSyntheticOpaqueMVar (← mvarId.getType)
+    let newVal ← mkLetFVars #[nval] newMVar
+    -- There are two cases:
+    -- - asLet is true: newVal is `let $name := $val in $newMVar`
+    -- - asLet is false: ewVal is `λ $name => $newMVar`
+    --   We need to apply it to `val`
+    let newVal := if asLet then newVal else mkAppN newVal #[val]
+    -- Assign the main goal and update the current goal
+    mvarId.assign newVal
+    let goals ← Tactic.getUnsolvedGoals
+    Lean.Elab.Tactic.setGoals (newMVar.mvarId! :: goals)
+    -- Return the new value - note: we are in the *new* context, created
+    -- after the declaration was added, so it will persist
+    pure nval
+
+def addDeclSyntax (name : Name) (val : Syntax) (asLet : Bool) : Tactic.TacticM Unit :=
+  -- I don't think we need that
+  Lean.Elab.Tactic.withMainContext do
+  --
+  let val ← elabTerm val .none
+  let type ← inferType val
+  -- In some situations, the type will be left as a metavariable (for instance,
+  -- if the term is `3`, Lean has the choice between `Nat` and `Int` and will
+  -- not choose): we force the instantiation of the meta-variable
+  synthesizeSyntheticMVarsUsingDefault
+  --
+  let _ ← addDecl name val type asLet
+
+elab "custom_let " n:ident " := " v:term : tactic => do
+  addDeclSyntax n.getId v (asLet := true)
+
+elab "custom_have " n:ident " := " v:term : tactic =>
+  addDeclSyntax n.getId v (asLet := false)
+
+example : Nat := by
+  custom_let x := 4
+  custom_have y := 4
+  apply y
+
+example (x : Bool) : Nat := by
+  cases x <;> custom_let x := 3 <;> apply x
+
 end Utils
-- 
cgit v1.2.3


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

(limited to 'backends/lean/Base/Utils.lean')

diff --git a/backends/lean/Base/Utils.lean b/backends/lean/Base/Utils.lean
index 2ce63620..1351f3d4 100644
--- a/backends/lean/Base/Utils.lean
+++ b/backends/lean/Base/Utils.lean
@@ -1,4 +1,5 @@
 import Lean
+import Mathlib.Tactic.Core
 
 namespace Utils
 
@@ -211,4 +212,31 @@ example : Nat := by
 example (x : Bool) : Nat := by
   cases x <;> custom_let x := 3 <;> apply x
 
+-- Repeatedly apply a tactic
+partial def repeatTac (tac : Tactic.TacticM Unit) : Tactic.TacticM Unit := do
+  try
+    tac
+    Tactic.allGoals (Tactic.focus (repeatTac tac))
+  -- TODO: does this restore the state?
+  catch _ => pure ()
+
+def firstTac (tacl : List (Tactic.TacticM Unit)) : Tactic.TacticM Unit := do
+  match tacl with
+  | [] => pure ()
+  | tac :: tacl =>
+    try tac
+    catch _ => firstTac tacl
+
+-- Split the goal if it is a conjunction
+def splitConjTarget : Tactic.TacticM Unit := do
+  Tactic.withMainContext do
+  let and_intro := Expr.const ``And.intro []
+  let mvarIds' ← _root_.Lean.MVarId.apply (← Tactic.getMainGoal) and_intro
+  Term.synthesizeSyntheticMVarsNoPostponing
+  Tactic.replaceMainGoal mvarIds'
+
+-- Taken from Lean.Elab.Tactic.evalAssumption
+def assumptionTac : Tactic.TacticM Unit :=
+  Tactic.liftMetaTactic fun mvarId => do mvarId.assumption; pure []
+
 end Utils
-- 
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/Utils.lean | 247 ++++++++++++++++++++++++++++++++++++++----
 1 file changed, 225 insertions(+), 22 deletions(-)

(limited to 'backends/lean/Base/Utils.lean')

diff --git a/backends/lean/Base/Utils.lean b/backends/lean/Base/Utils.lean
index 1351f3d4..14feb567 100644
--- a/backends/lean/Base/Utils.lean
+++ b/backends/lean/Base/Utils.lean
@@ -1,9 +1,10 @@
 import Lean
 import Mathlib.Tactic.Core
+import Mathlib.Tactic.LeftRight
 
 namespace Utils
 
-open Lean Elab Term Meta
+open Lean Elab Term Meta Tactic
 
 -- Useful helper to explore definitions and figure out the variant
 -- of their sub-expressions.
@@ -156,9 +157,10 @@ section Methods
 
 end Methods
 
-def addDecl (name : Name) (val : Expr) (type : Expr) (asLet : Bool) : Tactic.TacticM Expr :=
+-- TODO: this should take a continuation
+def addDeclTac (name : Name) (val : Expr) (type : Expr) (asLet : Bool) : TacticM Expr :=
   -- I don't think we need that
-  Lean.Elab.Tactic.withMainContext do
+  withMainContext do
   -- Insert the new declaration
   let withDecl := if asLet then withLetDecl name type val else withLocalDeclD name type
   withDecl fun nval => do
@@ -169,7 +171,7 @@ def addDecl (name : Name) (val : Expr) (type : Expr) (asLet : Bool) : Tactic.Tac
     trace[Arith] "  new decl: \"{decl.userName}\" ({nval}) : {decl.type} := {decl.value}"
     --
     -- Tranform the main goal `?m0` to `let x = nval in ?m1`
-    let mvarId ← Tactic.getMainGoal
+    let mvarId ← getMainGoal
     let newMVar ← mkFreshExprSyntheticOpaqueMVar (← mvarId.getType)
     let newVal ← mkLetFVars #[nval] newMVar
     -- There are two cases:
@@ -179,30 +181,30 @@ def addDecl (name : Name) (val : Expr) (type : Expr) (asLet : Bool) : Tactic.Tac
     let newVal := if asLet then newVal else mkAppN newVal #[val]
     -- Assign the main goal and update the current goal
     mvarId.assign newVal
-    let goals ← Tactic.getUnsolvedGoals
-    Lean.Elab.Tactic.setGoals (newMVar.mvarId! :: goals)
+    let goals ← getUnsolvedGoals
+    setGoals (newMVar.mvarId! :: goals)
     -- Return the new value - note: we are in the *new* context, created
     -- after the declaration was added, so it will persist
     pure nval
 
-def addDeclSyntax (name : Name) (val : Syntax) (asLet : Bool) : Tactic.TacticM Unit :=
+def addDeclTacSyntax (name : Name) (val : Syntax) (asLet : Bool) : TacticM Unit :=
   -- I don't think we need that
-  Lean.Elab.Tactic.withMainContext do
+  withMainContext do
   --
-  let val ← elabTerm val .none
+  let val ← Term.elabTerm val .none
   let type ← inferType val
   -- In some situations, the type will be left as a metavariable (for instance,
   -- if the term is `3`, Lean has the choice between `Nat` and `Int` and will
   -- not choose): we force the instantiation of the meta-variable
   synthesizeSyntheticMVarsUsingDefault
   --
-  let _ ← addDecl name val type asLet
+  let _ ← addDeclTac name val type asLet
 
 elab "custom_let " n:ident " := " v:term : tactic => do
-  addDeclSyntax n.getId v (asLet := true)
+  addDeclTacSyntax n.getId v (asLet := true)
 
 elab "custom_have " n:ident " := " v:term : tactic =>
-  addDeclSyntax n.getId v (asLet := false)
+  addDeclTacSyntax n.getId v (asLet := false)
 
 example : Nat := by
   custom_let x := 4
@@ -213,14 +215,14 @@ example (x : Bool) : Nat := by
   cases x <;> custom_let x := 3 <;> apply x
 
 -- Repeatedly apply a tactic
-partial def repeatTac (tac : Tactic.TacticM Unit) : Tactic.TacticM Unit := do
+partial def repeatTac (tac : TacticM Unit) : TacticM Unit := do
   try
     tac
-    Tactic.allGoals (Tactic.focus (repeatTac tac))
+    allGoals (focus (repeatTac tac))
   -- TODO: does this restore the state?
   catch _ => pure ()
 
-def firstTac (tacl : List (Tactic.TacticM Unit)) : Tactic.TacticM Unit := do
+def firstTac (tacl : List (TacticM Unit)) : TacticM Unit := do
   match tacl with
   | [] => pure ()
   | tac :: tacl =>
@@ -228,15 +230,216 @@ def firstTac (tacl : List (Tactic.TacticM Unit)) : Tactic.TacticM Unit := do
     catch _ => firstTac tacl
 
 -- Split the goal if it is a conjunction
-def splitConjTarget : Tactic.TacticM Unit := do
-  Tactic.withMainContext do
+def splitConjTarget : TacticM Unit := do
+  withMainContext do
   let and_intro := Expr.const ``And.intro []
-  let mvarIds' ← _root_.Lean.MVarId.apply (← Tactic.getMainGoal) and_intro
+  let mvarIds' ← _root_.Lean.MVarId.apply (← getMainGoal) and_intro
   Term.synthesizeSyntheticMVarsNoPostponing
-  Tactic.replaceMainGoal mvarIds'
+  replaceMainGoal mvarIds'
 
--- Taken from Lean.Elab.Tactic.evalAssumption
-def assumptionTac : Tactic.TacticM Unit :=
-  Tactic.liftMetaTactic fun mvarId => do mvarId.assumption; pure []
+-- Taken from Lean.Elab.evalAssumption
+def assumptionTac : TacticM Unit :=
+  liftMetaTactic fun mvarId => do mvarId.assumption; pure []
+
+def isConj (e : Expr) : MetaM Bool :=
+  e.withApp fun f args => pure (f.isConstOf ``And ∧ args.size = 2)
+
+-- Return the first conjunct if the expression is a conjunction, or the
+-- expression itself otherwise. Also return the second conjunct if it is a
+-- conjunction.
+def optSplitConj (e : Expr) : MetaM (Expr × Option Expr) := do
+  e.withApp fun f args =>
+  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
+
+-- Tactic to split on a disjunction.
+-- The expression `h` should be an fvar.
+-- TODO: there must be simpler. Use use _root_.Lean.MVarId.cases for instance
+def splitDisjTac (h : Expr) (kleft kright : TacticM Unit) : TacticM Unit := do
+  trace[Arith] "assumption on which to split: {h}"
+  -- Retrieve the main goal
+  withMainContext do
+  let goalType ← getMainTarget
+  let hDecl := (← getLCtx).get! h.fvarId!
+  let hName := hDecl.userName
+  -- Case disjunction
+  let hTy ← inferType h
+  hTy.withApp fun f xs => do
+  trace[Arith] "as app: {f} {xs}"
+  -- Sanity check
+  if ¬ (f.isConstOf ``Or ∧ xs.size = 2) then throwError "Invalid argument to splitDisjTac"
+  let a := xs.get! 0
+  let b := xs.get! 1
+  -- Introduce the new goals
+  -- Returns:
+  -- - the match branch
+  -- - a fresh new mvar id
+  let mkGoal (hTy : Expr) (nGoalName : String) : MetaM (Expr × MVarId) := do
+    -- Introduce a variable for the assumption (`a` or `b`). Note that we reuse
+    -- the name of the assumption we split.
+    withLocalDeclD hName hTy fun var => do
+    -- The new goal
+    let mgoal ← mkFreshExprSyntheticOpaqueMVar goalType (tag := Name.mkSimple nGoalName)
+    -- Clear the assumption that we split
+    let mgoal ← mgoal.mvarId!.tryClearMany #[h.fvarId!]
+    -- The branch expression
+    let branch ← mkLambdaFVars #[var] (mkMVar mgoal)
+    pure (branch, mgoal)
+  let (inl, mleft) ← mkGoal a "left"
+  let (inr, mright) ← mkGoal b "right"
+  trace[Arith] "left: {inl}: {mleft}"
+  trace[Arith] "right: {inr}: {mright}"
+  -- Create the match expression
+  withLocalDeclD (← mkFreshUserName `h) hTy fun hVar => do
+  let motive ← mkLambdaFVars #[hVar] goalType
+  let casesExpr ← mkAppOptM ``Or.casesOn #[a, b, motive, h, inl, inr]
+  let mgoal ← getMainGoal
+  trace[Arith] "goals: {← getUnsolvedGoals}"
+  trace[Arith] "main goal: {mgoal}"
+  mgoal.assign casesExpr
+  let goals ← getUnsolvedGoals
+  -- Focus on the left
+  setGoals [mleft]
+  withMainContext kleft
+  let leftGoals ← getUnsolvedGoals
+  -- Focus on the right
+  setGoals [mright]
+  withMainContext kright
+  let rightGoals ← getUnsolvedGoals
+  -- Put all the goals back
+  setGoals (leftGoals ++ rightGoals ++ goals)
+  trace[Arith] "new goals: {← getUnsolvedGoals}"
+
+elab "split_disj " n:ident : tactic => do
+  withMainContext do
+  let decl ← Lean.Meta.getLocalDeclFromUserName n.getId
+  let fvar := mkFVar decl.fvarId
+  splitDisjTac fvar (fun _ => pure ()) (fun _ => pure ())
+
+example (x y : Int) (h0 : x ≤ y ∨ x ≥ y) : x ≤ y ∨ x ≥ y := by
+  split_disj h0
+  . left; assumption
+  . right; assumption
+
+
+-- Tactic to split on an exists
+def splitExistsTac (h : Expr) (k : Expr → Expr → TacticM α) : TacticM α := do
+  withMainContext do
+  let goal ←  getMainGoal
+  let hTy ← inferType h
+  if isExists hTy then do
+    let newGoals ← goal.cases h.fvarId! #[]
+    -- There should be exactly one goal
+    match newGoals.toList with
+    | [ newGoal ] =>
+      -- Set the new goal
+      let goals ← getUnsolvedGoals
+      setGoals (newGoal.mvarId :: goals)
+      -- There should be exactly two fields
+      let fields := newGoal.fields
+      withMainContext do
+      k (fields.get! 0) (fields.get! 1)
+    | _ =>
+      throwError "Unreachable"
+  else
+    throwError "Not a conjunction"
+
+partial def splitAllExistsTac [Inhabited α] (h : Expr) (k : Expr → TacticM α) : TacticM α := do
+  try
+    splitExistsTac h (fun _ body => splitAllExistsTac body k)
+  catch _ => k h
+
+-- Tactic to split on a conjunction.
+def splitConjTac (h : Expr) (k : Expr → Expr → TacticM α)  : TacticM α := do
+  withMainContext do
+  let goal ←  getMainGoal
+  let hTy ← inferType h
+  if ← isConj hTy then do
+    let newGoals ← goal.cases h.fvarId! #[]
+    -- There should be exactly one goal
+    match newGoals.toList with
+    | [ newGoal ] =>
+      -- Set the new goal
+      let goals ← getUnsolvedGoals
+      setGoals (newGoal.mvarId :: goals)
+      -- There should be exactly two fields
+      let fields := newGoal.fields
+      withMainContext do
+      k (fields.get! 0) (fields.get! 1)
+    | _ =>
+      throwError "Unreachable"
+  else
+    throwError "Not a conjunction"
+
+elab "split_conj " n:ident : tactic => do
+  withMainContext do
+  let decl ← Lean.Meta.getLocalDeclFromUserName n.getId
+  let fvar := mkFVar decl.fvarId
+  splitConjTac fvar (fun _ _ =>  pure ())
+
+elab "split_all_exists " n:ident : tactic => do
+  withMainContext do
+  let decl ← Lean.Meta.getLocalDeclFromUserName n.getId
+  let fvar := mkFVar decl.fvarId
+  splitAllExistsTac fvar (fun _ =>  pure ())
+
+example (h : a ∧ b) : a := by
+  split_all_exists h
+  split_conj h
+  assumption
+
+example (h : ∃ x y z, x + y + z ≥ 0) : ∃ x, x ≥ 0 := by
+  split_all_exists h
+  rename_i x y z h
+  exists x + y + z
+
+/- Call the simp tactic.
+   The initialization of the context is adapted from Tactic.elabSimpArgs.
+   Something very annoying is that there is no function which allows to
+   initialize a simp context without doing an elaboration - as a consequence
+   we write our own here. -/
+def simpAt (declsToUnfold : List Name) (thms : List Name) (hypsToUse : List FVarId)
+  (loc : Tactic.Location) :
+  Tactic.TacticM Unit := do
+  -- Initialize with the builtin simp theorems
+  let simpThms ← Tactic.simpOnlyBuiltins.foldlM (·.addConst ·) ({} : SimpTheorems)
+  -- Add the equational theorem for the declarations to unfold
+  let simpThms ←
+    declsToUnfold.foldlM (fun thms decl => thms.addDeclToUnfold decl) simpThms
+  -- Add the hypotheses and the rewriting theorems
+  let simpThms ←
+    hypsToUse.foldlM (fun thms fvarId =>
+      -- post: TODO: don't know what that is
+      -- inv: invert the equality
+      thms.add (.fvar fvarId) #[] (mkFVar fvarId) (post := false) (inv := false)
+      -- thms.eraseCore (.fvar fvar)
+      ) simpThms
+  -- Add the rewriting theorems to use
+  let simpThms ←
+    thms.foldlM (fun thms thmName => do
+      let info ← getConstInfo thmName
+      if (← isProp info.type) then
+        -- post: TODO: don't know what that is
+        -- inv: invert the equality
+        thms.addConst thmName (post := false) (inv := false)
+      else
+        throwError "Not a proposition: {thmName}"
+      ) simpThms
+  let congrTheorems ← getSimpCongrTheorems
+  let ctx : Simp.Context := { simpTheorems := #[simpThms], congrTheorems }
+  -- Apply the simplifier
+  let _ ← Tactic.simpLocation ctx (discharge? := .none) loc
 
 end Utils
-- 
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/Utils.lean | 62 +++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 62 insertions(+)

(limited to 'backends/lean/Base/Utils.lean')

diff --git a/backends/lean/Base/Utils.lean b/backends/lean/Base/Utils.lean
index 14feb567..505412b9 100644
--- a/backends/lean/Base/Utils.lean
+++ b/backends/lean/Base/Utils.lean
@@ -2,6 +2,68 @@ import Lean
 import Mathlib.Tactic.Core
 import Mathlib.Tactic.LeftRight
 
+/-
+Mathlib tactics:
+- rcases: https://leanprover-community.github.io/mathlib_docs/tactics.html#rcases
+- split_ifs: https://leanprover-community.github.io/mathlib_docs/tactics.html#split_ifs
+- norm_num: https://leanprover-community.github.io/mathlib_docs/tactics.html#norm_num
+- should we use linarith or omega?
+- hint: https://leanprover-community.github.io/mathlib_docs/tactics.html#hint
+- classical: https://leanprover-community.github.io/mathlib_docs/tactics.html#classical
+-/
+
+/-
+TODO:
+- we want an easier to use cases:
+  - keeps in the goal an equation of the shape: `t = case`
+  - if called on Prop terms, uses Classical.em
+  Actually, the cases from mathlib seems already quite powerful
+  (https://leanprover-community.github.io/mathlib_docs/tactics.html#cases)
+  For instance: cases h : e
+  Also: **casesm**
+- better split tactic
+- we need conversions to operate on the head of applications.
+  Actually, something like this works:
+  ```
+  conv at Hl =>
+    apply congr_fun
+    simp [fix_fuel_P]
+  ```
+  Maybe we need a rpt ... ; focus?
+- simplifier/rewriter have a strange behavior sometimes
+-/
+
+
+namespace List
+
+  -- TODO: I could not find this function??
+  @[simp] def flatten {a : Type u} : List (List a) → List a
+  | [] => []
+  | x :: ls => x ++ flatten ls
+
+end List
+
+namespace Lean
+
+namespace LocalContext
+
+  open Lean Lean.Elab Command Term Lean.Meta
+
+  -- Small utility: return the list of declarations in the context, from
+  -- the last to the first.
+  def getAllDecls (lctx : Lean.LocalContext) : MetaM (List Lean.LocalDecl) :=
+    lctx.foldrM (fun d ls => do let d ← instantiateLocalDeclMVars d; pure (d :: ls)) []
+
+  -- Return the list of declarations in the context, but filter the
+  -- declarations which are considered as implementation details
+  def getDecls (lctx : Lean.LocalContext) : MetaM (List Lean.LocalDecl) := do
+    let ls ← lctx.getAllDecls
+    pure (ls.filter (fun d => not d.isImplementationDetail))
+
+end LocalContext
+
+end Lean
+
 namespace Utils
 
 open Lean Elab Term Meta Tactic
-- 
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/Utils.lean | 47 ++++++++++++++++++++++++++++++++++---------
 1 file changed, 37 insertions(+), 10 deletions(-)

(limited to 'backends/lean/Base/Utils.lean')

diff --git a/backends/lean/Base/Utils.lean b/backends/lean/Base/Utils.lean
index 505412b9..599c3a9f 100644
--- a/backends/lean/Base/Utils.lean
+++ b/backends/lean/Base/Utils.lean
@@ -396,13 +396,21 @@ example (x y : Int) (h0 : x ≤ y ∨ x ≥ y) : x ≤ y ∨ x ≥ y := by
   . right; assumption
 
 
--- Tactic to split on an exists
-def splitExistsTac (h : Expr) (k : Expr → Expr → TacticM α) : TacticM α := do
+-- Tactic to split on an exists.
+-- `h` must be an FVar
+def splitExistsTac (h : Expr) (optId : Option Name) (k : Expr → Expr → TacticM α) : TacticM α := do
   withMainContext do
   let goal ←  getMainGoal
   let hTy ← inferType h
   if isExists hTy then do
-    let newGoals ← goal.cases h.fvarId! #[]
+    -- Try to use the user-provided names
+    let altVarNames ←
+      match optId with
+      | none => pure #[]
+      | some id => do
+        let hDecl ← h.fvarId!.getDecl
+        pure #[{ varNames := [id, hDecl.userName] }]
+    let newGoals ← goal.cases h.fvarId! altVarNames
     -- There should be exactly one goal
     match newGoals.toList with
     | [ newGoal ] =>
@@ -418,18 +426,37 @@ def splitExistsTac (h : Expr) (k : Expr → Expr → TacticM α) : TacticM α :=
   else
     throwError "Not a conjunction"
 
-partial def splitAllExistsTac [Inhabited α] (h : Expr) (k : Expr → TacticM α) : TacticM α := do
+-- TODO: move
+def listTryPopHead (ls : List α) : Option α × List α :=
+  match ls with
+  | [] => (none, ls)
+  | hd :: tl => (some hd, tl)
+
+/- Destruct all the existentials appearing in `h`, and introduce them as variables
+   in the context.
+
+   If `ids` is not empty, we use it to name the introduced variables. We
+   transmit the stripped expression and the remaining ids to the continuation.
+ -/
+partial def splitAllExistsTac [Inhabited α] (h : Expr) (ids : List Name) (k : Expr → List Name → TacticM α) : TacticM α := do
   try
-    splitExistsTac h (fun _ body => splitAllExistsTac body k)
-  catch _ => k h
+    let (optId, ids) := listTryPopHead ids
+    splitExistsTac h optId (fun _ body => splitAllExistsTac body ids k)
+  catch _ => k h ids
 
 -- Tactic to split on a conjunction.
-def splitConjTac (h : Expr) (k : Expr → Expr → TacticM α)  : TacticM α := do
+def splitConjTac (h : Expr) (optIds : Option (Name × Name)) (k : Expr → Expr → TacticM α)  : TacticM α := do
   withMainContext do
   let goal ←  getMainGoal
   let hTy ← inferType h
   if ← isConj hTy then do
-    let newGoals ← goal.cases h.fvarId! #[]
+    -- Try to use the user-provided names
+    let altVarNames ←
+      match optIds with
+      | none => pure #[]
+      | some (id0, id1) => do
+        pure #[{ varNames := [id0, id1] }]
+    let newGoals ← goal.cases h.fvarId! altVarNames
     -- There should be exactly one goal
     match newGoals.toList with
     | [ newGoal ] =>
@@ -449,13 +476,13 @@ elab "split_conj " n:ident : tactic => do
   withMainContext do
   let decl ← Lean.Meta.getLocalDeclFromUserName n.getId
   let fvar := mkFVar decl.fvarId
-  splitConjTac fvar (fun _ _ =>  pure ())
+  splitConjTac fvar none (fun _ _ =>  pure ())
 
 elab "split_all_exists " n:ident : tactic => do
   withMainContext do
   let decl ← Lean.Meta.getLocalDeclFromUserName n.getId
   let fvar := mkFVar decl.fvarId
-  splitAllExistsTac fvar (fun _ =>  pure ())
+  splitAllExistsTac fvar [] (fun _ _ => pure ())
 
 example (h : a ∧ b) : a := by
   split_all_exists h
-- 
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/Utils.lean | 4 ++++
 1 file changed, 4 insertions(+)

(limited to 'backends/lean/Base/Utils.lean')

diff --git a/backends/lean/Base/Utils.lean b/backends/lean/Base/Utils.lean
index 599c3a9f..9cd0db23 100644
--- a/backends/lean/Base/Utils.lean
+++ b/backends/lean/Base/Utils.lean
@@ -43,6 +43,10 @@ namespace List
 
 end List
 
+-- TODO: move?
+@[simp]
+theorem neq_imp {α : Type u} {x y : α} (h : ¬ x = y) : ¬ y = x := by intro; simp_all
+
 namespace Lean
 
 namespace LocalContext
-- 
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/Utils.lean | 19 +++++++++++++++++++
 1 file changed, 19 insertions(+)

(limited to 'backends/lean/Base/Utils.lean')

diff --git a/backends/lean/Base/Utils.lean b/backends/lean/Base/Utils.lean
index 9cd0db23..acaeb26a 100644
--- a/backends/lean/Base/Utils.lean
+++ b/backends/lean/Base/Utils.lean
@@ -142,6 +142,25 @@ private def test2 (x : Nat) : Nat := x
 print_decl test1
 print_decl test2
 
+#check LocalDecl
+
+def printDecls (decls : List LocalDecl) : MetaM Unit := do
+  let decls ← decls.foldrM (λ decl msg => do
+    pure (m!"\n{decl.toExpr} : {← inferType decl.toExpr}" ++ msg)) m!""
+  logInfo m!"# Ctx decls:{decls}"
+
+-- Small utility: print all the declarations in the context (including the "implementation details")
+elab "print_all_ctx_decls" : tactic => do
+  let ctx ← Lean.MonadLCtx.getLCtx
+  let decls ← ctx.getAllDecls
+  printDecls decls
+
+-- Small utility: print all declarations in the context
+elab "print_ctx_decls" : tactic => do
+  let ctx ← Lean.MonadLCtx.getLCtx
+  let decls ← ctx.getDecls
+  printDecls decls
+
 -- A map visitor function for expressions (adapted from `AbstractNestedProofs.visit`)
 -- The continuation takes as parameters:
 -- - the current depth of the expression (useful for printing/debugging)
-- 
cgit v1.2.3


From 985fc7b1c08eaf027ec3a7c1e7ea635f53c00d72 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Wed, 19 Jul 2023 14:49:03 +0200
Subject: Cleanup more

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

(limited to 'backends/lean/Base/Utils.lean')

diff --git a/backends/lean/Base/Utils.lean b/backends/lean/Base/Utils.lean
index acaeb26a..8aa76d8e 100644
--- a/backends/lean/Base/Utils.lean
+++ b/backends/lean/Base/Utils.lean
@@ -138,12 +138,9 @@ open Lean.Elab.Command
 
 private def test1 : Nat := 0
 private def test2 (x : Nat) : Nat := x
-
 print_decl test1
 print_decl test2
 
-#check LocalDecl
-
 def printDecls (decls : List LocalDecl) : MetaM Unit := do
   let decls ← decls.foldrM (λ decl msg => do
     pure (m!"\n{decl.toExpr} : {← inferType decl.toExpr}" ++ msg)) m!""
-- 
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/Utils.lean | 32 ++++++++++++++++++++++++--------
 1 file changed, 24 insertions(+), 8 deletions(-)

(limited to 'backends/lean/Base/Utils.lean')

diff --git a/backends/lean/Base/Utils.lean b/backends/lean/Base/Utils.lean
index 8aa76d8e..44590176 100644
--- a/backends/lean/Base/Utils.lean
+++ b/backends/lean/Base/Utils.lean
@@ -308,8 +308,23 @@ def firstTac (tacl : List (TacticM Unit)) : TacticM Unit := do
   match tacl with
   | [] => pure ()
   | tac :: tacl =>
-    try tac
+    -- Should use try ... catch or Lean.observing?
+    -- Generally speaking we should use Lean.observing? to restore the state,
+    -- but with tactics the try ... catch variant seems to work
+    try do
+      tac
+      -- Check that there are no remaining goals
+      let gl ← Tactic.getUnsolvedGoals
+      if ¬ gl.isEmpty then throwError "tactic failed"
     catch _ => firstTac tacl
+/-    let res ← Lean.observing? do
+      tac
+      -- Check that there are no remaining goals
+      let gl ← Tactic.getUnsolvedGoals
+      if ¬ gl.isEmpty then throwError "tactic failed"
+    match res with
+    | some _ => pure ()
+    | none => firstTac tacl -/
 
 -- Split the goal if it is a conjunction
 def splitConjTarget : TacticM Unit := do
@@ -424,12 +439,13 @@ def splitExistsTac (h : Expr) (optId : Option Name) (k : Expr → Expr → Tacti
   let hTy ← inferType h
   if isExists hTy then do
     -- Try to use the user-provided names
-    let altVarNames ←
-      match optId with
-      | none => pure #[]
-      | some id => do
-        let hDecl ← h.fvarId!.getDecl
-        pure #[{ varNames := [id, hDecl.userName] }]
+    let altVarNames ← do
+      let hDecl ← h.fvarId!.getDecl
+      let id ← do
+        match optId with
+        | none => mkFreshUserName `x
+        | some id => pure id
+      pure #[{ varNames := [id, hDecl.userName] }]
     let newGoals ← goal.cases h.fvarId! altVarNames
     -- There should be exactly one goal
     match newGoals.toList with
@@ -511,7 +527,7 @@ example (h : a ∧ b) : a := by
 
 example (h : ∃ x y z, x + y + z ≥ 0) : ∃ x, x ≥ 0 := by
   split_all_exists h
-  rename_i x y z h
+  rename_i x y z
   exists x + y + z
 
 /- Call the simp tactic.
-- 
cgit v1.2.3


From e58872aa4dc31f0819fe17b13e6b7e4b0d9635c8 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Thu, 20 Jul 2023 15:46:11 +0200
Subject: Make progress on some of the hashmap proofs

---
 backends/lean/Base/Utils.lean | 30 ++++++++++++++++++++++--------
 1 file changed, 22 insertions(+), 8 deletions(-)

(limited to 'backends/lean/Base/Utils.lean')

diff --git a/backends/lean/Base/Utils.lean b/backends/lean/Base/Utils.lean
index 44590176..f014e112 100644
--- a/backends/lean/Base/Utils.lean
+++ b/backends/lean/Base/Utils.lean
@@ -326,14 +326,6 @@ def firstTac (tacl : List (TacticM Unit)) : TacticM Unit := do
     | some _ => pure ()
     | none => firstTac tacl -/
 
--- Split the goal if it is a conjunction
-def splitConjTarget : TacticM Unit := do
-  withMainContext do
-  let and_intro := Expr.const ``And.intro []
-  let mvarIds' ← _root_.Lean.MVarId.apply (← getMainGoal) and_intro
-  Term.synthesizeSyntheticMVarsNoPostponing
-  replaceMainGoal mvarIds'
-
 -- Taken from Lean.Elab.evalAssumption
 def assumptionTac : TacticM Unit :=
   liftMetaTactic fun mvarId => do mvarId.assumption; pure []
@@ -349,6 +341,24 @@ def optSplitConj (e : Expr) : MetaM (Expr × Option Expr) := do
   if f.isConstOf ``And ∧ args.size = 2 then pure (args.get! 0, some (args.get! 1))
   else pure (e, none)
 
+-- Split the goal if it is a conjunction
+def splitConjTarget : TacticM Unit := do
+  withMainContext do
+  let g ← getMainTarget
+  -- The tactic was initially implemened with `_root_.Lean.MVarId.apply`
+  -- but it tended to mess the goal by unfolding terms, even when it failed
+  let (l, r) ← optSplitConj g
+  match r with
+  | none => do throwError "The goal is not a conjunction"
+  | some r => do
+    let lmvar ← mkFreshExprSyntheticOpaqueMVar l
+    let rmvar ← mkFreshExprSyntheticOpaqueMVar r
+    let and_intro ← mkAppM ``And.intro #[lmvar, rmvar]
+    let g ← getMainGoal
+    g.assign and_intro
+    let goals ← getUnsolvedGoals
+    setGoals (lmvar.mvarId! :: rmvar.mvarId! :: goals)
+
 -- Destruct an equaliy and return the two sides
 def destEq (e : Expr) : MetaM (Expr × Expr) := do
   e.withApp fun f args =>
@@ -520,6 +530,10 @@ elab "split_all_exists " n:ident : tactic => do
   let fvar := mkFVar decl.fvarId
   splitAllExistsTac fvar [] (fun _ _ => pure ())
 
+elab "split_target_conjs" : tactic =>
+  withMainContext do
+  repeatTac splitConjTarget
+
 example (h : a ∧ b) : a := by
   split_all_exists h
   split_conj h
-- 
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/Utils.lean | 61 ++++++++++++++++++++++++++++++++++---------
 1 file changed, 48 insertions(+), 13 deletions(-)

(limited to 'backends/lean/Base/Utils.lean')

diff --git a/backends/lean/Base/Utils.lean b/backends/lean/Base/Utils.lean
index f014e112..3b3d4729 100644
--- a/backends/lean/Base/Utils.lean
+++ b/backends/lean/Base/Utils.lean
@@ -499,7 +499,10 @@ def splitConjTac (h : Expr) (optIds : Option (Name × Name)) (k : Expr → Expr
     -- Try to use the user-provided names
     let altVarNames ←
       match optIds with
-      | none => pure #[]
+      | none => do
+        let id0 ← mkFreshUserName `h
+        let id1 ← mkFreshUserName `h
+        pure #[{ varNames := [id0, id1] }]
       | some (id0, id1) => do
         pure #[{ varNames := [id0, id1] }]
     let newGoals ← goal.cases h.fvarId! altVarNames
@@ -518,29 +521,61 @@ def splitConjTac (h : Expr) (optIds : Option (Name × Name)) (k : Expr → Expr
   else
     throwError "Not a conjunction"
 
-elab "split_conj " n:ident : tactic => do
+-- Tactic to fully split a conjunction
+partial def splitFullConjTacAux [Inhabited α] [Nonempty α] (l : List Expr) (h : Expr) (k : List Expr → TacticM α)  : TacticM α := do
+  try
+    splitConjTac h none (λ h1 h2 =>
+      splitFullConjTacAux l h1 (λ l1 =>
+        splitFullConjTacAux l1 h2 (λ l2 =>
+          k l2)))
+  catch _ =>
+    k (h :: l)
+
+-- Tactic to fully split a conjunction
+def splitFullConjTac [Inhabited α] [Nonempty α] (h : Expr) (k : List Expr → TacticM α)  : TacticM α := do
+  splitFullConjTacAux [] h (λ l => k l.reverse)
+
+syntax optAtArgs := ("at" ident)?
+def elabOptAtArgs (args : TSyntax `Utils.optAtArgs) : TacticM (Option Expr) := do
   withMainContext do
-  let decl ← Lean.Meta.getLocalDeclFromUserName n.getId
-  let fvar := mkFVar decl.fvarId
-  splitConjTac fvar none (fun _ _ =>  pure ())
+  let args := (args.raw.getArgs.get! 0).getArgs
+  if args.size > 0 then do
+    let n := (args.get! 1).getId
+    let decl ← Lean.Meta.getLocalDeclFromUserName n
+    let fvar := mkFVar decl.fvarId
+    pure (some fvar)
+  else
+    pure none
 
-elab "split_all_exists " n:ident : tactic => do
+elab "split_conj" args:optAtArgs : tactic => do
+  withMainContext do
+  match ← elabOptAtArgs args with
+  | some fvar =>
+    splitConjTac fvar none (fun _ _ =>  pure ())
+  | none =>
+    splitConjTarget
+
+elab "split_conjs" args:optAtArgs : tactic => do
+  withMainContext do
+  match ← elabOptAtArgs args with
+  | some fvar =>
+    splitFullConjTac fvar (fun _ =>  pure ())
+  | none =>
+    repeatTac splitConjTarget
+
+elab "split_existsl" " at " n:ident : tactic => do
   withMainContext do
   let decl ← Lean.Meta.getLocalDeclFromUserName n.getId
   let fvar := mkFVar decl.fvarId
   splitAllExistsTac fvar [] (fun _ _ => pure ())
 
-elab "split_target_conjs" : tactic =>
-  withMainContext do
-  repeatTac splitConjTarget
-
 example (h : a ∧ b) : a := by
-  split_all_exists h
-  split_conj h
+  split_existsl at h
+  split_conj at h
   assumption
 
 example (h : ∃ x y z, x + y + z ≥ 0) : ∃ x, x ≥ 0 := by
-  split_all_exists h
+  split_existsl at h
   rename_i x y z
   exists x + y + z
 
-- 
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/Utils.lean | 7 +++++--
 1 file changed, 5 insertions(+), 2 deletions(-)

(limited to 'backends/lean/Base/Utils.lean')

diff --git a/backends/lean/Base/Utils.lean b/backends/lean/Base/Utils.lean
index 3b3d4729..66497a49 100644
--- a/backends/lean/Base/Utils.lean
+++ b/backends/lean/Base/Utils.lean
@@ -484,9 +484,12 @@ def listTryPopHead (ls : List α) : Option α × List α :=
    If `ids` is not empty, we use it to name the introduced variables. We
    transmit the stripped expression and the remaining ids to the continuation.
  -/
-partial def splitAllExistsTac [Inhabited α] (h : Expr) (ids : List Name) (k : Expr → List Name → TacticM α) : TacticM α := do
+partial def splitAllExistsTac [Inhabited α] (h : Expr) (ids : List (Option Name)) (k : Expr → List (Option Name) → TacticM α) : TacticM α := do
   try
-    let (optId, ids) := listTryPopHead ids
+    let (optId, ids) :=
+      match ids with
+      | [] => (none, [])
+      | x :: ids => (x, ids)
     splitExistsTac h optId (fun _ body => splitAllExistsTac body ids k)
   catch _ => k h ids
 
-- 
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/Utils.lean | 36 +++++++++++++++++++++++++-----------
 1 file changed, 25 insertions(+), 11 deletions(-)

(limited to 'backends/lean/Base/Utils.lean')

diff --git a/backends/lean/Base/Utils.lean b/backends/lean/Base/Utils.lean
index 66497a49..f6dc45c7 100644
--- a/backends/lean/Base/Utils.lean
+++ b/backends/lean/Base/Utils.lean
@@ -1,6 +1,7 @@
 import Lean
 import Mathlib.Tactic.Core
 import Mathlib.Tactic.LeftRight
+import Base.UtilsBase
 
 /-
 Mathlib tactics:
@@ -331,13 +332,13 @@ def assumptionTac : TacticM Unit :=
   liftMetaTactic fun mvarId => do mvarId.assumption; pure []
 
 def isConj (e : Expr) : MetaM Bool :=
-  e.withApp fun f args => pure (f.isConstOf ``And ∧ args.size = 2)
+  e.consumeMData.withApp fun f args => pure (f.isConstOf ``And ∧ args.size = 2)
 
 -- Return the first conjunct if the expression is a conjunction, or the
 -- expression itself otherwise. Also return the second conjunct if it is a
 -- conjunction.
 def optSplitConj (e : Expr) : MetaM (Expr × Option Expr) := do
-  e.withApp fun f args =>
+  e.consumeMData.withApp fun f args =>
   if f.isConstOf ``And ∧ args.size = 2 then pure (args.get! 0, some (args.get! 1))
   else pure (e, none)
 
@@ -345,6 +346,7 @@ def optSplitConj (e : Expr) : MetaM (Expr × Option Expr) := do
 def splitConjTarget : TacticM Unit := do
   withMainContext do
   let g ← getMainTarget
+  trace[Utils] "splitConjTarget: goal: {g}"
   -- The tactic was initially implemened with `_root_.Lean.MVarId.apply`
   -- but it tended to mess the goal by unfolding terms, even when it failed
   let (l, r) ← optSplitConj g
@@ -525,18 +527,26 @@ def splitConjTac (h : Expr) (optIds : Option (Name × Name)) (k : Expr → Expr
     throwError "Not a conjunction"
 
 -- Tactic to fully split a conjunction
-partial def splitFullConjTacAux [Inhabited α] [Nonempty α] (l : List Expr) (h : Expr) (k : List Expr → TacticM α)  : TacticM α := do
+partial def splitFullConjTacAux [Inhabited α] [Nonempty α] (keepCurrentName : Bool) (l : List Expr) (h : Expr) (k : List Expr → TacticM α)  : TacticM α := do
   try
-    splitConjTac h none (λ h1 h2 =>
-      splitFullConjTacAux l h1 (λ l1 =>
-        splitFullConjTacAux l1 h2 (λ l2 =>
+    let ids ← do
+      if keepCurrentName then do
+        let cur := (← h.fvarId!.getDecl).userName
+        let nid ← mkFreshUserName `h
+        pure (some (cur, nid))
+      else
+        pure none
+    splitConjTac h ids (λ h1 h2 =>
+      splitFullConjTacAux keepCurrentName l h1 (λ l1 =>
+        splitFullConjTacAux keepCurrentName l1 h2 (λ l2 =>
           k l2)))
   catch _ =>
     k (h :: l)
 
 -- Tactic to fully split a conjunction
-def splitFullConjTac [Inhabited α] [Nonempty α] (h : Expr) (k : List Expr → TacticM α)  : TacticM α := do
-  splitFullConjTacAux [] h (λ l => k l.reverse)
+-- `keepCurrentName`: if `true`, then the first conjunct has the name of the original assumption
+def splitFullConjTac [Inhabited α] [Nonempty α] (keepCurrentName : Bool) (h : Expr) (k : List Expr → TacticM α)  : TacticM α := do
+  splitFullConjTacAux keepCurrentName [] h (λ l => k l.reverse)
 
 syntax optAtArgs := ("at" ident)?
 def elabOptAtArgs (args : TSyntax `Utils.optAtArgs) : TacticM (Option Expr) := do
@@ -553,17 +563,21 @@ def elabOptAtArgs (args : TSyntax `Utils.optAtArgs) : TacticM (Option Expr) := d
 elab "split_conj" args:optAtArgs : tactic => do
   withMainContext do
   match ← elabOptAtArgs args with
-  | some fvar =>
+  | some fvar => do
+    trace[Utils] "split at {fvar}"
     splitConjTac fvar none (fun _ _ =>  pure ())
-  | none =>
+  | none => do
+    trace[Utils] "split goal"
     splitConjTarget
 
 elab "split_conjs" args:optAtArgs : tactic => do
   withMainContext do
   match ← elabOptAtArgs args with
   | some fvar =>
-    splitFullConjTac fvar (fun _ =>  pure ())
+    trace[Utils] "split at {fvar}"
+    splitFullConjTac false fvar (fun _ =>  pure ())
   | none =>
+    trace[Utils] "split goal"
     repeatTac splitConjTarget
 
 elab "split_existsl" " at " n:ident : tactic => do
-- 
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/Utils.lean | 12 ++++++++----
 1 file changed, 8 insertions(+), 4 deletions(-)

(limited to 'backends/lean/Base/Utils.lean')

diff --git a/backends/lean/Base/Utils.lean b/backends/lean/Base/Utils.lean
index f6dc45c7..1f8f1455 100644
--- a/backends/lean/Base/Utils.lean
+++ b/backends/lean/Base/Utils.lean
@@ -201,6 +201,10 @@ partial def mapVisit (k : Nat → Expr → MetaM Expr) (e : Expr) : MetaM Expr :
     | .proj _ _ b => return e.updateProj! (← visit (i + 1) b)
   visit 0 e
 
+-- Generate a fresh user name for an anonymous proposition to introduce in the
+-- assumptions
+def mkFreshAnonPropUserName := mkFreshUserName `_
+
 section Methods
   variable [MonadLiftT MetaM m] [MonadControlT MetaM m] [Monad m] [MonadError m]
   variable {a : Type}
@@ -411,7 +415,7 @@ def splitDisjTac (h : Expr) (kleft kright : TacticM Unit) : TacticM Unit := do
   trace[Arith] "left: {inl}: {mleft}"
   trace[Arith] "right: {inr}: {mright}"
   -- Create the match expression
-  withLocalDeclD (← mkFreshUserName `h) hTy fun hVar => do
+  withLocalDeclD (← mkFreshAnonPropUserName) hTy fun hVar => do
   let motive ← mkLambdaFVars #[hVar] goalType
   let casesExpr ← mkAppOptM ``Or.casesOn #[a, b, motive, h, inl, inr]
   let mgoal ← getMainGoal
@@ -505,8 +509,8 @@ def splitConjTac (h : Expr) (optIds : Option (Name × Name)) (k : Expr → Expr
     let altVarNames ←
       match optIds with
       | none => do
-        let id0 ← mkFreshUserName `h
-        let id1 ← mkFreshUserName `h
+        let id0 ← mkFreshAnonPropUserName
+        let id1 ← mkFreshAnonPropUserName
         pure #[{ varNames := [id0, id1] }]
       | some (id0, id1) => do
         pure #[{ varNames := [id0, id1] }]
@@ -532,7 +536,7 @@ partial def splitFullConjTacAux [Inhabited α] [Nonempty α] (keepCurrentName :
     let ids ← do
       if keepCurrentName then do
         let cur := (← h.fvarId!.getDecl).userName
-        let nid ← mkFreshUserName `h
+        let nid ← mkFreshAnonPropUserName
         pure (some (cur, nid))
       else
         pure none
-- 
cgit v1.2.3