chore: two BitVec lemmas that help simp confluence

This PR adds infrastructure for the `grind?` tactic. It also adds the
new modifier `usr` which allows users to write `grind only [usr
thmName]` to instruct `grind` to only use theorem `thmName`, but using
the patterns specified with the command `grind_pattern`.

src/Init/Data/BitVec/Lemmas.lean

@@ -378,6 +378,16 @@ theorem getElem_ofBool {b : Bool} : (ofBool b)[0] = b := by simp
 @[simp] theorem msb_ofBool (b : Bool) : (ofBool b).msb = b := by
   cases b <;> simp [BitVec.msb]
 
+@[simp] theorem one_eq_zero_iff : 1#w = 0#w ↔ w = 0 := by
+  constructor
+  · intro h
+    cases w
+    · rfl
+    · replace h := congrArg BitVec.toNat h
+      simp at h
+  · rintro rfl
+    simp
+
 /-! ### msb -/
 
 @[simp] theorem msb_zero : (0#w).msb = false := by simp [BitVec.msb, getMsbD]
@@ -1164,6 +1174,10 @@ theorem not_not {b : BitVec w} : ~~~(~~~b) = b := by
   ext i h
   simp [h]
 
+@[simp] theorem and_not_self (x : BitVec n) : x &&& ~~~x = 0 := by
+   ext i
+   simp_all
+
 theorem not_eq_comm {x y : BitVec w} : ~~~ x = y ↔ x = ~~~ y := by
   constructor
   · intro h
@@ -3429,7 +3443,7 @@ theorem shiftLeft_eq_mul_twoPow (x : BitVec w) (n : Nat) :
   simp [getLsbD_shiftLeft, Fin.is_lt, decide_true, Bool.true_and, mul_twoPow_eq_shiftLeft]
 
 /-- 2^i * 2^j = 2^(i + j) with bitvectors as well -/
-theorem twoPow_mul_twoPow_eq {w : Nat} (i j : Nat) : twoPow w i * twoPow w j = twoPow w (i + j) := by 
+theorem twoPow_mul_twoPow_eq {w : Nat} (i j : Nat) : twoPow w i * twoPow w j = twoPow w (i + j) := by
   apply BitVec.eq_of_toNat_eq
   simp only [toNat_mul, toNat_twoPow]
   rw [← Nat.mul_mod, Nat.pow_add]

src/Init/Grind/Tactics.lean

@@ -14,10 +14,11 @@ syntax grindEqRhs  := atomic("=" "_")
 syntax grindEqBwd  := atomic("←" "=")
 syntax grindBwd    := "←"
 syntax grindFwd    := "→"
+syntax grindUsr    := &"usr"
 syntax grindCases  := &"cases"
 syntax grindCasesEager := atomic(&"cases" &"eager")
 
-syntax grindMod := grindEqBoth <|> grindEqRhs <|> grindEq <|> grindEqBwd <|> grindBwd <|> grindFwd <|> grindCasesEager <|> grindCases
+syntax grindMod := grindEqBoth <|> grindEqRhs <|> grindEq <|> grindEqBwd <|> grindBwd <|> grindFwd <|> grindUsr <|> grindCasesEager <|> grindCases
 
 syntax (name := grind) "grind" (grindMod)? : attr
 
@@ -75,4 +76,10 @@ syntax (name := grind)
   (" [" withoutPosition(grindParam,*) "]")?
   ("on_failure " term)? : tactic
 
+
+syntax (name := grindTrace)
+  "grind?" optConfig (&" only")?
+  (" [" withoutPosition(grindParam,*) "]")?
+  ("on_failure " term)? : tactic
+
 end Lean.Parser.Tactic

src/Init/Grind/Util.lean

@@ -12,11 +12,10 @@ namespace Lean.Grind
 def nestedProof (p : Prop) {h : p} : p := h
 
 /--
-Gadget for marking terms that should not be normalized by `grind`s simplifier.
-`grind` uses a simproc to implement this feature.
+Gadget for marking `match`-expressions that should not be reduced by the `grind` simplifier, but the discriminants should be normalized.
 We use it when adding instances of `match`-equations to prevent them from being simplified to true.
 -/
-def doNotSimp {α : Sort u} (a : α) : α := a
+def simpMatchDiscrsOnly {α : Sort u} (a : α) : α := a
 
 /-- Gadget for representing offsets `t+k` in patterns. -/
 def offset (a b : Nat) : Nat := a + b

src/Lean/Compiler/LCNF/ToLCNF.lean

@@ -7,6 +7,7 @@ prelude
 import Lean.ProjFns
 import Lean.Meta.CtorRecognizer
 import Lean.Compiler.BorrowedAnnotation
+import Lean.Compiler.CSimpAttr
 import Lean.Compiler.LCNF.Types
 import Lean.Compiler.LCNF.Bind
 import Lean.Compiler.LCNF.InferType
@@ -472,7 +473,7 @@ where
 
   /-- Giving `f` a constant `.const declName us`, convert `args` into `args'`, and return `.const declName us args'` -/
   visitAppDefaultConst (f : Expr) (args : Array Expr) : M Arg := do
-    let .const declName us := f | unreachable!
+    let .const declName us := CSimp.replaceConstants (← getEnv) f | unreachable!
     let args ← args.mapM visitAppArg
     letValueToArg <| .const declName us args
 
@@ -670,7 +671,7 @@ where
   visitApp (e : Expr) : M Arg := do
     if let some (args, n, t, v, b) := e.letFunAppArgs? then
       visitCore <| mkAppN (.letE n t v b (nonDep := true)) args
-    else if let .const declName _ := e.getAppFn then
+    else if let .const declName _ := CSimp.replaceConstants (← getEnv) e.getAppFn then
       if declName == ``Quot.lift then
         visitQuotLift e
       else if declName == ``Quot.mk then

src/Lean/Elab/Tactic/Grind.lean

@@ -31,7 +31,7 @@ def elabGrindPattern : CommandElab := fun stx => do
           let pattern ← instantiateMVars pattern
           let pattern ← Grind.preprocessPattern pattern
           return pattern.abstract xs
-        Grind.addEMatchTheorem declName xs.size patterns.toList
+        Grind.addEMatchTheorem declName xs.size patterns.toList .user
   | _ => throwUnsupportedSyntax
 
 open Command Term in
@@ -45,7 +45,7 @@ def elabInitGrindNorm : CommandElab := fun stx =>
       Grind.registerNormTheorems pre post
   | _ => throwUnsupportedSyntax
 
-def elabGrindParams (params : Grind.Params) (ps :  TSyntaxArray ``Parser.Tactic.grindParam) : MetaM Grind.Params := do
+def elabGrindParams (params : Grind.Params) (ps :  TSyntaxArray ``Parser.Tactic.grindParam) (only : Bool) : MetaM Grind.Params := do
   let mut params := params
   for p in ps do
     match p with
@@ -59,6 +59,16 @@ def elabGrindParams (params : Grind.Params) (ps :  TSyntaxArray ``Parser.Tactic.
       let declName ← realizeGlobalConstNoOverloadWithInfo id
       let kind ← if let some mod := mod? then Grind.getAttrKindCore mod else pure .infer
       match kind with
+      | .ematch .user =>
+        unless only do
+          withRef p <| Grind.throwInvalidUsrModifier
+        let s ← Grind.getEMatchTheorems
+        let thms := s.find (.decl declName)
+        let thms := thms.filter fun thm => thm.kind == .user
+        if thms.isEmpty then
+          throwErrorAt p "invalid use of `usr` modifier, `{declName}` does not have patterns specified with the command `grind_pattern`"
+        for thm in thms do
+          params := { params with extra := params.extra.push thm }
       | .ematch kind =>
         params ← withRef p <| addEMatchTheorem params declName kind
       | .cases eager =>
@@ -97,7 +107,7 @@ def mkGrindParams (config : Grind.Config) (only : Bool) (ps :  TSyntaxArray ``Pa
   let ematch ← if only then pure {} else Grind.getEMatchTheorems
   let casesTypes ← if only then pure {} else Grind.getCasesTypes
   let params := { params with ematch, casesTypes }
-  elabGrindParams params ps
+  elabGrindParams params ps only
 
 def grind
     (mvarId : MVarId) (config : Grind.Config)
@@ -126,16 +136,32 @@ private def elabFallback (fallback? : Option Term) : TermElabM (Grind.GoalM Unit
     pure auxDeclName
   unsafe evalConst (Grind.GoalM Unit) auxDeclName
 
+private def evalGrindCore
+    (ref : Syntax)
+    (config : TSyntax `Lean.Parser.Tactic.optConfig)
+    (only : Option Syntax)
+    (params : Option (Syntax.TSepArray `Lean.Parser.Tactic.grindParam ","))
+    (fallback? : Option Term)
+    (_trace : Bool) -- TODO
+    : TacticM Unit := do
+  let fallback ← elabFallback fallback?
+  let only := only.isSome
+  let params := if let some params := params then params.getElems else #[]
+  logWarningAt ref "The `grind` tactic is experimental and still under development. Avoid using it in production projects"
+  let declName := (← Term.getDeclName?).getD `_grind
+  let config ← elabGrindConfig config
+  withMainContext do liftMetaFinishingTactic (grind · config only params declName fallback)
+
 @[builtin_tactic Lean.Parser.Tactic.grind] def evalGrind : Tactic := fun stx => do
   match stx with
   | `(tactic| grind $config:optConfig $[only%$only]?  $[ [$params:grindParam,*] ]? $[on_failure $fallback?]?) =>
-    let fallback ← elabFallback fallback?
-    let only := only.isSome
-    let params := if let some params := params then params.getElems else #[]
-    logWarningAt stx "The `grind` tactic is experimental and still under development. Avoid using it in production projects"
-    let declName := (← Term.getDeclName?).getD `_grind
-    let config ← elabGrindConfig config
-    withMainContext do liftMetaFinishingTactic (grind · config only params declName fallback)
+    evalGrindCore stx config only params fallback? false
+  | _ => throwUnsupportedSyntax
+
+@[builtin_tactic Lean.Parser.Tactic.grindTrace] def evalGrindTrace : Tactic := fun stx => do
+  match stx with
+  | `(tactic| grind? $config:optConfig $[only%$only]?  $[ [$params:grindParam,*] ]? $[on_failure $fallback?]?) =>
+    evalGrindCore stx config only params fallback? true
   | _ => throwUnsupportedSyntax
 
 end Lean.Elab.Tactic

src/Lean/Meta/ExprDefEq.lean

@@ -1634,11 +1634,18 @@ private partial def consumeLet : Expr → Expr
     else
       e
 
+private partial def consumeLetIfZeta (e : Expr) : MetaM Expr := do
+  let cfg ← getConfig
+  if cfg.zeta || cfg.zetaUnused then
+    return consumeLet e
+  else
+    return e
+
 mutual
 
-private partial def isDefEqQuick (t s : Expr) : MetaM LBool :=
-  let t := consumeLet t
-  let s := consumeLet s
+private partial def isDefEqQuick (t s : Expr) : MetaM LBool := do
+  let t ← consumeLetIfZeta t
+  let s ← consumeLetIfZeta s
   match t, s with
   | .lit  l₁,      .lit l₂     => return (l₁ == l₂).toLBool
   | .sort u,       .sort v     => toLBoolM <| isLevelDefEqAux u v

src/Lean/Meta/Tactic/Contradiction.lean

@@ -96,12 +96,12 @@ private abbrev isGenDiseq (e : Expr) : Bool :=
 
   See `processGenDiseq`
 -/
-private def mkGenDiseqMask (e : Expr) : Array Bool :=
+def mkGenDiseqMask (e : Expr) : Array Bool :=
   go e #[]
 where
   go (e : Expr) (acc : Array Bool) : Array Bool :=
     match e with
-    | Expr.forallE _ d b _ => go b (acc.push (!b.hasLooseBVar 0 && (d.isEq || d.isHEq)))
+    | .forallE _ d b _ => go b (acc.push (!b.hasLooseBVar 0 && (d.isEq || d.isHEq)))
     | _ => acc
 
 /--

src/Lean/Meta/Tactic/Grind.lean

@@ -27,7 +27,7 @@ import Lean.Meta.Tactic.Grind.CasesMatch
 import Lean.Meta.Tactic.Grind.Arith
 import Lean.Meta.Tactic.Grind.Ext
 import Lean.Meta.Tactic.Grind.MatchCond
-import Lean.Meta.Tactic.Grind.DoNotSimp
+import Lean.Meta.Tactic.Grind.MatchDiscrOnly
 
 namespace Lean
 
@@ -72,7 +72,9 @@ builtin_initialize registerTraceClass `grind.debug.offset
 builtin_initialize registerTraceClass `grind.debug.offset.proof
 builtin_initialize registerTraceClass `grind.debug.ematch.pattern
 builtin_initialize registerTraceClass `grind.debug.beta
+builtin_initialize registerTraceClass `grind.debug.internalize
 builtin_initialize registerTraceClass `grind.debug.matchCond
 builtin_initialize registerTraceClass `grind.debug.matchCond.lambda
+builtin_initialize registerTraceClass `grind.debug.matchCond.proveFalse
 
 end Lean

src/Lean/Meta/Tactic/Grind/Arith/Model.lean

@@ -9,37 +9,70 @@ import Lean.Meta.Tactic.Grind.Types
 import Lean.Meta.Tactic.Grind.Util
 
 namespace Lean.Meta.Grind.Arith.Offset
+
+
 /-- Construct a model that statisfies all offset constraints -/
 def mkModel (goal : Goal) : MetaM (Array (Expr × Nat)) := do
   let s := goal.arith.offset
+  let dbg := grind.debug.get (← getOptions)
   let nodes := s.nodes
+  let isInterpreted (u : Nat) : Bool := isNatNum s.nodes[u]!
   let mut pre : Array (Option Int) := mkArray nodes.size none
+  /-
+  `needAdjust[u]` is true if `u` assignment is not connected to an interpreted value in the graph.
+  That is, its assignment may be negative.
+  -/
+  let mut needAdjust : Array Bool := mkArray nodes.size true
+  -- Initialize `needAdjust`
+  for u in [: nodes.size] do
+    if isInterpreted u then
+      -- Interpreted values have a fixed value.
+      needAdjust := needAdjust.set! u false
+    else if s.sources[u]!.any fun v _ => isInterpreted v then
+      needAdjust := needAdjust.set! u false
+    else if s.targets[u]!.any fun v _ => isInterpreted v then
+      needAdjust := needAdjust.set! u false
+  -- Set interpreted values
+  for h : u in [:nodes.size] do
+    let e := nodes[u]
+    if let some v ← getNatValue? e then
+      pre := pre.set! u (Int.ofNat v)
+  -- Set remaining values
   for u in [:nodes.size] do
-    let val? := s.sources[u]!.foldl (init := @none Int) fun val? v k => Id.run do
+    let lower? := s.sources[u]!.foldl (init := none) fun val? v k => Id.run do
       let some va := pre[v]! | return val?
       let val' := va - k
       let some val := val? | return val'
       if val' > val then return val' else val?
-    let val? := s.targets[u]!.foldl (init := val?) fun val? v k => Id.run do
+    let upper? := s.targets[u]!.foldl (init := none) fun val? v k => Id.run do
       let some va := pre[v]! | return val?
       let val' := va + k
       let some val := val? | return val'
       if val' < val then return val' else val?
-    let val := val?.getD 0
-    pre := pre.set! u (some val)
+    if dbg then
+      let some upper := upper? | pure ()
+      let some lower := lower? | pure ()
+      assert! lower ≤ upper
+      let some val := pre[u]! | pure ()
+      assert! lower ≤ val
+      assert! val ≤ upper
+    unless pre[u]!.isSome do
+      let val := lower?.getD (upper?.getD 0)
+      pre := pre.set! u (some val)
   let min := pre.foldl (init := 0) fun min val? => Id.run do
     let some val := val? | return min
     if val < min then val else min
   let mut r := {}
   for u in [:nodes.size] do
     let some val := pre[u]! | unreachable!
-    let val := (val - min).toNat
+    let val := if needAdjust[u]! then (val - min).toNat else val.toNat
     let e := nodes[u]!
     /-
     We should not include the assignment for auxiliary offset terms since
     they do not provide any additional information.
+    That said, the information is relevant for debugging `grind`.
     -/
-    if !(← isLitValue e) && (isNatOffset? e).isNone && isNatNum? e != some 0 then
+    if (!(← isLitValue e) && (isNatOffset? e).isNone && isNatNum? e != some 0) || grind.debug.get (← getOptions) then
       r := r.push (e, val)
   return r
 

src/Lean/Meta/Tactic/Grind/Arith/Offset.lean

@@ -270,7 +270,13 @@ private def isEqParent (parent? : Option Expr) : Bool := Id.run do
   let some parent := parent? | return false
   return parent.isEq
 
+private def alreadyInternalized (e : Expr) : GoalM Bool := do
+  let s ← get'
+  return s.cnstrs.contains { expr := e } || s.nodeMap.contains { expr := e }
+
 def internalize (e : Expr) (parent? : Option Expr) : GoalM Unit := do
+  if (← alreadyInternalized e) then
+    return ()
   let z ← getNatZeroExpr
   if let some c := isNatOffsetCnstr? e z then
     internalizeCnstr e c

src/Lean/Meta/Tactic/Grind/Attr.lean

@@ -23,6 +23,7 @@ def getAttrKindCore (stx : Syntax) : CoreM AttrKind := do
   | `(Parser.Attr.grindMod| =_) => return .ematch .eqRhs
   | `(Parser.Attr.grindMod| _=_) => return .ematch .eqBoth
   | `(Parser.Attr.grindMod| ←=) => return .ematch .eqBwd
+  | `(Parser.Attr.grindMod| usr) => return .ematch .user
   | `(Parser.Attr.grindMod| cases) => return .cases false
   | `(Parser.Attr.grindMod| cases eager) => return .cases true
   | _ => throwError "unexpected `grind` theorem kind: `{stx}`"
@@ -34,6 +35,9 @@ def getAttrKindFromOpt (stx : Syntax) : CoreM AttrKind := do
   else
     getAttrKindCore stx[1][0]
 
+def throwInvalidUsrModifier : CoreM α :=
+  throwError "the modifier `usr` is only relevant in parameters for `grind only`"
+
 builtin_initialize
   registerBuiltinAttribute {
     name := `grind
@@ -57,6 +61,7 @@ builtin_initialize
     applicationTime := .afterCompilation
     add := fun declName stx attrKind => MetaM.run' do
       match (← getAttrKindFromOpt stx) with
+      | .ematch .user => throwInvalidUsrModifier
       | .ematch k => addEMatchAttr declName attrKind k
       | .cases eager => addCasesAttr declName eager attrKind
       | .infer =>

src/Lean/Meta/Tactic/Grind/Beta.lean

@@ -44,7 +44,7 @@ def propagateBetaEqs (lams : Array Expr) (f : Expr) (args : Array Expr) : GoalM
           gen := Nat.max gen (← getGeneration arg)
           h ← mkCongrFun h arg
         let eq ← mkEq lhs rhs
-        trace[grind.beta] "{eq}, using {lam}"
+        trace_goal[grind.beta] "{eq}, using {lam}"
         addNewFact h eq (gen+1)
 
 private def isPropagateBetaTarget (e : Expr) : GoalM Bool := do

src/Lean/Meta/Tactic/Grind/Canon.lean

@@ -86,15 +86,15 @@ def canonElemCore (parent : Expr) (f : Expr) (i : Nat) (e : Expr) (useIsDefEqBou
         -- Moreover, we store the canonicalizer state in the `Goal` because we case-split
         -- and different locals are added in different branches.
         modify' fun s => { s with canon := s.canon.insert e c }
-        trace[grind.debugn.canon] "found {e} ===> {c}"
+        trace_goal[grind.debugn.canon] "found {e} ===> {c}"
         return c
       if useIsDefEqBounded then
         -- If `e` and `c` are not types, we use `isDefEqBounded`
         if (← isDefEqBounded e c parent) then
           modify' fun s => { s with canon := s.canon.insert e c }
-          trace[grind.debugn.canon] "found using `isDefEqBounded`: {e} ===> {c}"
+          trace_goal[grind.debugn.canon] "found using `isDefEqBounded`: {e} ===> {c}"
           return c
-  trace[grind.debug.canon] "({f}, {i}) ↦ {e}"
+  trace_goal[grind.debug.canon] "({f}, {i}) ↦ {e}"
   modify' fun s => { s with canon := s.canon.insert e e, argMap := s.argMap.insert key ((e, eType)::cs) }
   return e
 
@@ -173,7 +173,7 @@ where
           let mut args := args.toVector
           for h : i in [:args.size] do
             let arg := args[i]
-            trace[grind.debug.canon] "[{repr (← shouldCanon pinfos i arg)}]: {arg} : {← inferType arg}"
+            trace_goal[grind.debug.canon] "[{repr (← shouldCanon pinfos i arg)}]: {arg} : {← inferType arg}"
             let arg' ← match (← shouldCanon pinfos i arg) with
             | .canonType  => canonType e f i arg
             | .canonInst  => canonInst e f i arg
@@ -197,7 +197,7 @@ end Canon
 
 /-- Canonicalizes nested types, type formers, and instances in `e`. -/
 def canon (e : Expr) : GoalM Expr := do
-  trace[grind.debug.canon] "{e}"
+  trace_goal[grind.debug.canon] "{e}"
   unsafe Canon.canonImpl e
 
 end Lean.Meta.Grind

src/Lean/Meta/Tactic/Grind/Cases.lean

@@ -85,6 +85,20 @@ def eraseCasesAttr (declName : Name) : CoreM Unit := do
   let s ← s.eraseDecl declName
   modifyEnv fun env => casesExt.modifyState env fun _ => s
 
+/--
+We say a free variable is "simple" to be processed by the cases tactic IF:
+- It is the latest and consequently there are no forward dependencies, OR
+- It is not a proposion.
+-/
+private def isSimpleFVar (e : Expr) : MetaM Bool := do
+  let .fvar fvarId := e | return false
+  let decl ← fvarId.getDecl
+  if decl.index == (← getLCtx).numIndices - 1 then
+    -- It is the latest free variable, so there are no forward dependencies
+    return true
+  else
+    -- It is pointless to add an auxiliary equality if `e`s type is a proposition
+    isProp decl.type
 
 /--
 The `grind` tactic includes an auxiliary `cases` tactic that is not intended for direct use by users.
@@ -132,12 +146,17 @@ def cases (mvarId : MVarId) (e : Expr) : MetaM (List MVarId) := mvarId.withConte
     let s ← generalizeIndices' mvarId e
     s.mvarId.withContext do
       k s.mvarId s.fvarId s.indicesFVarIds
-  else if let .fvar fvarId := e then
-    k mvarId fvarId #[]
+  else if (← isSimpleFVar e) then
+    -- We don't need to revert anything.
+    k mvarId e.fvarId! #[]
   else
-    let mvarId ← mvarId.assert (← mkFreshUserName `x) type e
+    let mvarId ← if (← isProof e) then
+      mvarId.assert (← mkFreshUserName `x) type e
+    else
+      mvarId.assertExt (← mkFreshUserName `x) type e
     let (fvarId, mvarId) ← mvarId.intro1
     mvarId.withContext do k mvarId fvarId #[]
+
 where
   throwInductiveExpected {α} (type : Expr) : MetaM α := do
     throwTacticEx `grind.cases mvarId m!"(non-recursive) inductive type expected at {e}{indentExpr type}"

src/Lean/Meta/Tactic/Grind/Core.lean

@@ -116,15 +116,15 @@ the lambda expressions in `lams`.
 def propagateBeta (lams : Array Expr) (fns : Array Expr) : GoalM Unit := do
   if lams.isEmpty then return ()
   let lamRoot ← getRoot lams.back!
-  trace[grind.debug.beta] "fns: {fns}, lams: {lams}"
+  trace_goal[grind.debug.beta] "fns: {fns}, lams: {lams}"
   for fn in fns do
-    trace[grind.debug.beta] "fn: {fn}, parents: {(← getParents fn).toArray}"
+    trace_goal[grind.debug.beta] "fn: {fn}, parents: {(← getParents fn).toArray}"
     for parent in (← getParents fn) do
       let mut args := #[]
       let mut curr := parent
-      trace[grind.debug.beta] "parent: {parent}"
+      trace_goal[grind.debug.beta] "parent: {parent}"
       repeat
-        trace[grind.debug.beta] "curr: {curr}"
+        trace_goal[grind.debug.beta] "curr: {curr}"
         if (← isEqv curr lamRoot) then
           propagateBetaEqs lams curr args.reverse
         let .app f arg := curr
@@ -234,7 +234,8 @@ private def popNextEq? : GoalM (Option NewEq) := do
     modify fun s => { s with newEqs := s.newEqs.pop }
   return r
 
-private def processNewEqs : GoalM Unit := do
+@[export lean_grind_process_new_eqs]
+private def processNewEqsImpl : GoalM Unit := do
   repeat
     if (← isInconsistent) then
       resetNewEqs
@@ -246,7 +247,7 @@ private def processNewEqs : GoalM Unit := do
 
 private def addEqCore (lhs rhs proof : Expr) (isHEq : Bool) : GoalM Unit := do
   addEqStep lhs rhs proof isHEq
-  processNewEqs
+  processNewEqsImpl
 
 /-- Adds a new equality `lhs = rhs`. It assumes `lhs` and `rhs` have already been internalized. -/
 private def addEq (lhs rhs proof : Expr) : GoalM Unit := do
@@ -311,56 +312,4 @@ where
 def addHypothesis (fvarId : FVarId) (generation := 0) : GoalM Unit := do
   add (← fvarId.getType) (mkFVar fvarId) generation
 
-/--
-Helper function for executing `x` with a fresh `newEqs` and without modifying
-the goal state.
- -/
-private def withoutModifyingState (x : GoalM α) : GoalM α := do
-  let saved ← get
-  modify fun goal => { goal with newEqs := {} }
-  try
-    x
-  finally
-    set saved
-
-/--
-If `e` has not been internalized yet, simplify it, and internalize the result.
--/
-private def simpAndInternalize (e : Expr) (gen : Nat := 0) : GoalM Simp.Result := do
-  if (← alreadyInternalized e) then
-    return { expr := e }
-  else
-    let r ← simp e
-    internalize r.expr gen
-    return r
-
-/--
-Try to construct a proof that `lhs = rhs` using the information in the
-goal state. If `lhs` and `rhs` have not been internalized, this function
-will internalize then, process propagated equalities, and then check
-whether they are in the same equivalence class or not.
-The goal state is not modified by this function.
-This function mainly relies on congruence closure, and constraint
-propagation. It will not perform case analysis.
--/
-def proveEq? (lhs rhs : Expr) : GoalM (Option Expr) := do
-  if (← alreadyInternalized lhs <&&> alreadyInternalized rhs) then
-    if (← isEqv lhs rhs) then
-      return some (← mkEqProof lhs rhs)
-    else
-      return none
-  else withoutModifyingState do
-    let lhs ← simpAndInternalize lhs
-    let rhs ← simpAndInternalize rhs
-    processNewEqs
-    unless (← isEqv lhs.expr rhs.expr) do return none
-    unless (← hasSameType lhs.expr rhs.expr) do return none
-    let h ← mkEqProof lhs.expr rhs.expr
-    let h ← match lhs.proof?, rhs.proof? with
-      | none,    none    => pure h
-      | none,    some h₂ => mkEqTrans h (← mkEqSymm h₂)
-      | some h₁, none    => mkEqTrans h₁ h
-      | some h₁, some h₂ => mkEqTrans (← mkEqTrans h₁ h) (← mkEqSymm h₂)
-    return some h
-
 end Lean.Meta.Grind

src/Lean/Meta/Tactic/Grind/DoNotSimp.lean

@@ -1,35 +0,0 @@
-/-
-Copyright (c) 2025 Amazon.com, Inc. or its affiliates. All Rights Reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Leonardo de Moura
--/
-prelude
-import Init.Grind.Util
-import Init.Simproc
-import Lean.Meta.Tactic.Simp.Simproc
-
-namespace Lean.Meta.Grind
-
-/--
-Returns `Grind.doNotSimp e`.
-Recall that `Grind.doNotSimp` is an identity function, but the following simproc is used to prevent the term `e` from being simplified.
--/
-def markAsDoNotSimp (e : Expr) : MetaM Expr :=
-  mkAppM ``Grind.doNotSimp #[e]
-
-builtin_dsimproc_decl reduceDoNotSimp (Grind.doNotSimp _) := fun e => do
-  let_expr Grind.doNotSimp _ _ ← e | return .continue
-  return .done e
-
-/-- Adds `reduceDoNotSimp` to `s` -/
-def addDoNotSimp (s : Simprocs) : CoreM Simprocs := do
-  s.add ``reduceDoNotSimp (post := false)
-
-/-- Erases `Grind.doNotSimp` annotations. -/
-def eraseDoNotSimp (e : Expr) : CoreM Expr := do
-  let pre (e : Expr) := do
-    let_expr Grind.doNotSimp _ a := e | return .continue e
-    return .continue a
-  Core.transform e (pre := pre)
-
-end Lean.Meta.Grind

src/Lean/Meta/Tactic/Grind/EMatch.lean

@@ -6,7 +6,7 @@ Authors: Leonardo de Moura
 prelude
 import Lean.Meta.Tactic.Grind.Types
 import Lean.Meta.Tactic.Grind.Intro
-import Lean.Meta.Tactic.Grind.DoNotSimp
+import Lean.Meta.Tactic.Grind.MatchDiscrOnly
 import Lean.Meta.Tactic.Grind.MatchCond
 import Lean.Meta.Tactic.Grind.Core
 
@@ -235,7 +235,8 @@ private def annotateMatchEqnType (prop : Expr) (initApp : Expr) : M Expr := do
   annotateEqnTypeConds prop fun prop => do
     let_expr f@Eq α lhs rhs := prop | return prop
     -- See comment at `Grind.EqMatch`
-    return mkApp4 (mkConst ``Grind.EqMatch f.constLevels!) α (← markAsDoNotSimp lhs) rhs initApp
+    let lhs ← markAsSimpMatchDiscrsOnly lhs
+    return mkApp4 (mkConst ``Grind.EqMatch f.constLevels!) α lhs rhs initApp
 
 /--
 Stores new theorem instance in the state.
@@ -282,6 +283,11 @@ private partial def instantiateTheorem (c : Choice) : M Unit := withDefault do w
         let some heq ← proveEq? vType mvarIdType
           | report
             return ()
+        /-
+        Some of the `cast`s will appear inside the `Grind.MatchCond` binders, and
+        we want their proofs to be properly wrapped.
+        -/
+        let heq := mkApp2 (mkConst ``Grind.nestedProof) (← mkEq vType mvarIdType) heq
         v ← mkAppM ``cast #[heq, v]
       unless (← mvarId.checkedAssign v) do
         report

src/Lean/Meta/Tactic/Grind/EMatchTheorem.lean

@@ -92,6 +92,30 @@ instance : BEq Origin where
 instance : Hashable Origin where
   hash a := hash a.key
 
+inductive TheoremKind where
+  | eqLhs | eqRhs | eqBoth | eqBwd | fwd | bwd | default | user /- pattern specified using `grind_pattern` command -/
+  deriving Inhabited, BEq, Repr
+
+private def TheoremKind.toAttribute : TheoremKind → String
+  | .eqLhs   => "[grind =]"
+  | .eqRhs   => "[grind =_]"
+  | .eqBoth  => "[grind _=_]"
+  | .eqBwd   => "[grind ←=]"
+  | .fwd     => "[grind →]"
+  | .bwd     => "[grind ←]"
+  | .default => "[grind]"
+  | .user    => "[grind]"
+
+private def TheoremKind.explainFailure : TheoremKind → String
+  | .eqLhs   => "failed to find pattern in the left-hand side of the theorem's conclusion"
+  | .eqRhs   => "failed to find pattern in the right-hand side of the theorem's conclusion"
+  | .eqBoth  => unreachable! -- eqBoth is a macro
+  | .eqBwd   => "failed to use theorem's conclusion as a pattern"
+  | .fwd     => "failed to find patterns in the antecedents of the theorem"
+  | .bwd     => "failed to find patterns in the theorem's conclusion"
+  | .default => "failed to find patterns"
+  | .user    => unreachable!
+
 /-- A theorem for heuristic instantiation based on E-matching. -/
 structure EMatchTheorem where
   /--
@@ -106,16 +130,20 @@ structure EMatchTheorem where
   /-- Contains all symbols used in `pattterns`. -/
   symbols     : List HeadIndex
   origin      : Origin
+  /-- The `kind` is used for generating the `patterns`. We save it here to implement `grind?`. -/
+  kind        : TheoremKind
   deriving Inhabited
 
 /-- Set of E-matching theorems. -/
 structure EMatchTheorems where
   /-- The key is a symbol from `EMatchTheorem.symbols`. -/
-  private map : PHashMap Name (List EMatchTheorem) := {}
+  private smap : PHashMap Name (List EMatchTheorem) := {}
   /-- Set of theorem ids that have been inserted using `insert`. -/
   private origins : PHashSet Origin := {}
   /-- Theorems that have been marked as erased -/
   private erased  : PHashSet Origin := {}
+  /-- Mapping from origin to E-matching theorems associated with this origin. -/
+  private omap : PHashMap Origin (List EMatchTheorem) := {}
   deriving Inhabited
 
 /--
@@ -130,13 +158,19 @@ def EMatchTheorems.insert (s : EMatchTheorems) (thm : EMatchTheorem) : EMatchThe
   let .const declName :: syms := thm.symbols
     | unreachable!
   let thm := { thm with symbols := syms }
-  let { map, origins, erased } := s
-  let origins := origins.insert thm.origin
-  let erased := erased.erase thm.origin
-  if let some thms := map.find? declName then
-    return { map := map.insert declName (thm::thms), origins, erased }
+  let { smap, origins, erased, omap } := s
+  let origin := thm.origin
+  let origins := origins.insert origin
+  let erased := erased.erase origin
+  let smap := if let some thms := smap.find? declName then
+    smap.insert declName (thm::thms)
   else
-    return { map := map.insert declName [thm], origins, erased }
+    smap.insert declName [thm]
+  let omap := if let some thms := omap.find? origin then
+    omap.insert origin (thm::thms)
+  else
+    omap.insert origin [thm]
+  return { smap, origins, erased, omap }
 
 /-- Returns `true` if `s` contains a theorem with the given origin. -/
 def EMatchTheorems.contains (s : EMatchTheorems) (origin : Origin) : Bool :=
@@ -156,11 +190,20 @@ The theorems are removed from `s`.
 -/
 @[inline]
 def EMatchTheorems.retrieve? (s : EMatchTheorems) (sym : Name) : Option (List EMatchTheorem × EMatchTheorems) :=
-  if let some thms := s.map.find? sym then
-    some (thms, { s with map := s.map.erase sym })
+  if let some thms := s.smap.find? sym then
+    some (thms, { s with smap := s.smap.erase sym })
   else
     none
 
+/--
+Returns theorems associated with the given origin.
+-/
+def EMatchTheorems.find (s : EMatchTheorems) (origin : Origin) : List EMatchTheorem :=
+  if let some thms := s.omap.find? origin then
+    thms
+  else
+    []
+
 def EMatchTheorem.getProofWithFreshMVarLevels (thm : EMatchTheorem) : MetaM Expr := do
   if thm.proof.isConst && thm.levelParams.isEmpty then
     let declName := thm.proof.constName!
@@ -491,7 +534,7 @@ private def ppParamsAt (proof : Expr) (numParams : Nat) (paramPos : List Nat) :
 Creates an E-matching theorem for a theorem with proof `proof`, `numParams` parameters, and the given set of patterns.
 Pattern variables are represented using de Bruijn indices.
 -/
-def mkEMatchTheoremCore (origin : Origin) (levelParams : Array Name) (numParams : Nat) (proof : Expr) (patterns : List Expr) : MetaM EMatchTheorem := do
+def mkEMatchTheoremCore (origin : Origin) (levelParams : Array Name) (numParams : Nat) (proof : Expr) (patterns : List Expr) (kind : TheoremKind): MetaM EMatchTheorem := do
   let (patterns, symbols, bvarFound) ← NormalizePattern.main patterns
   if symbols.isEmpty then
     throwError "invalid pattern for `{← origin.pp}`{indentD (patterns.map ppPattern)}\nthe pattern does not contain constant symbols for indexing"
@@ -501,7 +544,7 @@ def mkEMatchTheoremCore (origin : Origin) (levelParams : Array Name) (numParams
      throwError "invalid pattern(s) for `{← origin.pp}`{indentD pats}\nthe following theorem parameters cannot be instantiated:{indentD (← ppParamsAt proof numParams pos)}"
   return {
     proof, patterns, numParams, symbols
-    levelParams, origin
+    levelParams, origin, kind
   }
 
 private def getProofFor (declName : Name) : CoreM Expr := do
@@ -514,8 +557,8 @@ private def getProofFor (declName : Name) : CoreM Expr := do
 Creates an E-matching theorem for `declName` with `numParams` parameters, and the given set of patterns.
 Pattern variables are represented using de Bruijn indices.
 -/
-def mkEMatchTheorem (declName : Name) (numParams : Nat) (patterns : List Expr) : MetaM EMatchTheorem := do
-  mkEMatchTheoremCore (.decl declName) #[] numParams (← getProofFor declName) patterns
+def mkEMatchTheorem (declName : Name) (numParams : Nat) (patterns : List Expr) (kind : TheoremKind) : MetaM EMatchTheorem := do
+  mkEMatchTheoremCore (.decl declName) #[] numParams (← getProofFor declName) patterns kind
 
 /--
 Given a theorem with proof `proof` and type of the form `∀ (a_1 ... a_n), lhs = rhs`,
@@ -535,15 +578,15 @@ def mkEMatchEqTheoremCore (origin : Origin) (levelParams : Array Name) (proof :
     trace[grind.debug.ematch.pattern] "mkEMatchEqTheoremCore: after preprocessing: {pat}, {← normalize pat}"
     let pats := splitWhileForbidden (pat.abstract xs)
     return (xs.size, pats)
-  mkEMatchTheoremCore origin levelParams numParams proof patterns
+  mkEMatchTheoremCore origin levelParams numParams proof patterns (if useLhs then .eqLhs else .eqRhs)
 
 def mkEMatchEqBwdTheoremCore (origin : Origin) (levelParams : Array Name) (proof : Expr) : MetaM EMatchTheorem := do
   let (numParams, patterns) ← forallTelescopeReducing (← inferType proof) fun xs type => do
     let_expr f@Eq α lhs rhs := type
-      | throwError "invalid E-matching `≠` theorem, conclusion must be an equality{indentExpr type}"
+      | throwError "invalid E-matching `←=` theorem, conclusion must be an equality{indentExpr type}"
     let pat ← preprocessPattern (mkEqBwdPattern f.constLevels! α lhs rhs)
     return (xs.size, [pat.abstract xs])
-  mkEMatchTheoremCore origin levelParams numParams proof patterns
+  mkEMatchTheoremCore origin levelParams numParams proof patterns .eqBwd
 
 /--
 Given theorem with name `declName` and type of the form `∀ (a_1 ... a_n), lhs = rhs`,
@@ -559,8 +602,8 @@ def mkEMatchEqTheorem (declName : Name) (normalizePattern := true) (useLhs : Boo
 Adds an E-matching theorem to the environment.
 See `mkEMatchTheorem`.
 -/
-def addEMatchTheorem (declName : Name) (numParams : Nat) (patterns : List Expr) : MetaM Unit := do
-  ematchTheoremsExt.add (← mkEMatchTheorem declName numParams patterns)
+def addEMatchTheorem (declName : Name) (numParams : Nat) (patterns : List Expr) (kind : TheoremKind) : MetaM Unit := do
+  ematchTheoremsExt.add (← mkEMatchTheorem declName numParams patterns kind)
 
 /--
 Adds an E-matching equality theorem to the environment.
@@ -573,28 +616,6 @@ def addEMatchEqTheorem (declName : Name) : MetaM Unit := do
 def getEMatchTheorems : CoreM EMatchTheorems :=
   return ematchTheoremsExt.getState (← getEnv)
 
-inductive TheoremKind where
-  | eqLhs | eqRhs | eqBoth | eqBwd | fwd | bwd | default
-  deriving Inhabited, BEq, Repr
-
-private def TheoremKind.toAttribute : TheoremKind → String
-  | .eqLhs   => "[grind =]"
-  | .eqRhs   => "[grind =_]"
-  | .eqBoth  => "[grind _=_]"
-  | .eqBwd   => "[grind ←=]"
-  | .fwd     => "[grind →]"
-  | .bwd     => "[grind ←]"
-  | .default => "[grind]"
-
-private def TheoremKind.explainFailure : TheoremKind → String
-  | .eqLhs   => "failed to find pattern in the left-hand side of the theorem's conclusion"
-  | .eqRhs   => "failed to find pattern in the right-hand side of the theorem's conclusion"
-  | .eqBoth  => unreachable! -- eqBoth is a macro
-  | .eqBwd   => "failed to use theorem's conclusion as a pattern"
-  | .fwd     => "failed to find patterns in the antecedents of the theorem"
-  | .bwd     => "failed to find patterns in the theorem's conclusion"
-  | .default => "failed to find patterns"
-
 /-- Returns the types of `xs` that are propositions. -/
 private def getPropTypes (xs : Array Expr) : MetaM (Array Expr) :=
   xs.filterMapM fun x => do
@@ -702,7 +723,7 @@ where
     trace[grind.ematch.pattern] "{← origin.pp}: {patterns.map ppPattern}"
     return some {
       proof, patterns, numParams, symbols
-      levelParams, origin
+      levelParams, origin, kind
     }
 
 def mkEMatchTheoremForDecl (declName : Name) (thmKind : TheoremKind) : MetaM EMatchTheorem := do

src/Lean/Meta/Tactic/Grind/ForallProp.lean

@@ -98,7 +98,7 @@ def propagateForallPropDown (e : Expr) : GoalM Unit := do
       pushEqFalse b <| mkApp3 (mkConst ``Grind.eq_false_of_imp_eq_false) a b h
   else if (← isEqTrue e) then
     if let some (e', h') ← eqResolution e then
-      trace[grind.eqResolution] "{e}, {e'}"
+      trace_goal[grind.eqResolution] "{e}, {e'}"
       let h := mkOfEqTrueCore e (← mkEqTrueProof e)
       let h' := mkApp h' h
       addNewFact h' e' (← getGeneration e)

src/Lean/Meta/Tactic/Grind/Internalize.lean

@@ -90,7 +90,7 @@ private def checkAndAddSplitCandidate (e : Expr) : GoalM Unit := do
       else if (← getConfig).splitIndPred then
         addSplitCandidate e
   | .fvar .. =>
-    let .const declName _ := (← inferType e).getAppFn | return ()
+    let .const declName _ := (← whnfD (← inferType e)).getAppFn | return ()
     if (← get).casesTypes.isSplit declName then
       addSplitCandidate e
   | _ => pure ()
@@ -114,7 +114,6 @@ private def preprocessGroundPattern (e : Expr) : GoalM Expr := do
 private def mkENode' (e : Expr) (generation : Nat) : GoalM Unit :=
   mkENodeCore e (ctor := false) (interpreted := false) (generation := generation)
 
-mutual
 /-- Internalizes the nested ground terms in the given pattern. -/
 private partial def internalizePattern (pattern : Expr) (generation : Nat) : GoalM Expr := do
   if pattern.isBVar || isPatternDontCare pattern then
@@ -127,17 +126,17 @@ private partial def internalizePattern (pattern : Expr) (generation : Nat) : Goa
     return mkAppN f (← args.mapM (internalizePattern · generation))
 
 /-- Internalizes the `MatchCond` gadget. -/
-private partial def internalizeMatchCond (matchCond : Expr) (generation : Nat) : GoalM Unit := do
+private def internalizeMatchCond (matchCond : Expr) (generation : Nat) : GoalM Unit := do
   mkENode' matchCond generation
   let (lhss, e') ← collectMatchCondLhssAndAbstract matchCond
   lhss.forM fun lhs => do internalize lhs generation; registerParent matchCond lhs
   propagateUp matchCond
   internalize e' generation
-  trace[grind.debug.matchCond.lambda] "(idx := {(← getENode e'.getAppFn).idx}) {e'.getAppFn}"
-  trace[grind.debug.matchCond.lambda] "auxiliary application{indentExpr e'}"
+  trace_goal[grind.debug.matchCond.lambda] "(idx := {(← getENode e'.getAppFn).idx}) {e'.getAppFn}"
+  trace_goal[grind.debug.matchCond.lambda] "auxiliary application{indentExpr e'}"
   pushEq matchCond e' (← mkEqRefl matchCond)
 
-partial def activateTheorem (thm : EMatchTheorem) (generation : Nat) : GoalM Unit := do
+def activateTheorem (thm : EMatchTheorem) (generation : Nat) : GoalM Unit := do
   -- Recall that we use the proof as part of the key for a set of instances found so far.
   -- We don't want to use structural equality when comparing keys.
   let proof ← shareCommon thm.proof
@@ -149,7 +148,7 @@ partial def activateTheorem (thm : EMatchTheorem) (generation : Nat) : GoalM Uni
 If `Config.matchEqs` is set to `true`, and `f` is `match`-auxiliary function,
 adds its equations to `newThms`.
 -/
-private partial def addMatchEqns (f : Expr) (generation : Nat) : GoalM Unit := do
+private def addMatchEqns (f : Expr) (generation : Nat) : GoalM Unit := do
   if !(← getConfig).matchEqs then return ()
   let .const declName _ := f | return ()
   if !(← isMatcher declName) then return ()
@@ -159,7 +158,7 @@ private partial def addMatchEqns (f : Expr) (generation : Nat) : GoalM Unit := d
     -- We disable pattern normalization to prevent the `match`-expression to be reduced.
     activateTheorem (← mkEMatchEqTheorem eqn (normalizePattern := false)) generation
 
-private partial def activateTheoremPatterns (fName : Name) (generation : Nat) : GoalM Unit := do
+private def activateTheoremPatterns (fName : Name) (generation : Nat) : GoalM Unit := do
   if let some (thms, thmMap) := (← get).thmMap.retrieve? fName then
     modify fun s => { s with thmMap }
     let appMap := (← get).appMap
@@ -173,20 +172,37 @@ private partial def activateTheoremPatterns (fName : Name) (generation : Nat) :
           trace_goal[grind.ematch] "reinsert `{thm.origin.key}`"
           modify fun s => { s with thmMap := s.thmMap.insert thm }
 
-partial def internalize (e : Expr) (generation : Nat) (parent? : Option Expr := none) : GoalM Unit := do
-  if (← alreadyInternalized e) then return ()
+
+@[export lean_grind_internalize]
+private partial def internalizeImpl (e : Expr) (generation : Nat) (parent? : Option Expr := none) : GoalM Unit := do
+  if (← alreadyInternalized e) then
+    trace_goal[grind.debug.internalize] "already internalized: {e}"
+    /-
+    Even if `e` has already been internalized, we must check whether it has also been internalized in
+    the satellite solvers. For example, suppose we have already internalized the term `f (a + 1)`.
+    The `1` in this term is treated as an offset for the offset term `a + 1` by the arithmetic module, and
+    only nodes for `a` and `a+1` are created. However, an ENode for `1` is created here.
+    Later, if we try to internalize `f 1`, the arithmetic module must create a node for `1`.
+    Otherwise, it will not be able to propagate that `a + 1 = 1` when `a = 0`
+    -/
+    Arith.internalize e parent?
+    return ()
   trace_goal[grind.internalize] "{e}"
   match e with
   | .bvar .. => unreachable!
   | .sort .. => return ()
-  | .fvar .. | .letE .. | .lam .. => mkENode' e generation
+  | .fvar .. =>
+    mkENode' e generation
+    checkAndAddSplitCandidate e
+  | .letE .. | .lam .. =>
+    mkENode' e generation
   | .forallE _ d b _ =>
     mkENode' e generation
     if (← isProp d <&&> isProp e) then
-      internalize d generation e
+      internalizeImpl d generation e
       registerParent e d
       unless b.hasLooseBVars do
-        internalize b generation e
+        internalizeImpl b generation e
         registerParent e b
       propagateUp e
   | .lit .. | .const .. =>
@@ -215,17 +231,17 @@ partial def internalize (e : Expr) (generation : Nat) (parent? : Option Expr :=
         -- We only internalize the proposition. We can skip the proof because of
         -- proof irrelevance
         let c := args[0]!
-        internalize c generation e
+        internalizeImpl c generation e
         registerParent e c
       else if f.isConstOf ``ite && args.size == 5 then
         let c := args[1]!
-        internalize c generation e
+        internalizeImpl c generation e
         registerParent e c
       else
         if let .const fName _ := f then
           activateTheoremPatterns fName generation
         else
-          internalize f generation e
+          internalizeImpl f generation e
         registerParent e f
         for h : i in [: args.size] do
           let arg := args[i]
@@ -238,6 +254,4 @@ partial def internalize (e : Expr) (generation : Nat) (parent? : Option Expr :=
       propagateUp e
       propagateBetaForNewApp e
 
-end
-
 end Lean.Meta.Grind

src/Lean/Meta/Tactic/Grind/MatchCond.lean

@@ -6,7 +6,9 @@ Authors: Leonardo de Moura
 prelude
 import Init.Grind
 import Init.Simproc
+import Lean.Meta.Tactic.Contradiction
 import Lean.Meta.Tactic.Simp.Simproc
+import Lean.Meta.Tactic.Grind.ProveEq
 import Lean.Meta.Tactic.Grind.PropagatorAttr
 
 namespace Lean.Meta.Grind
@@ -267,7 +269,7 @@ private partial def isStatisfied (e : Expr) : GoalM Bool := do
   repeat
     let .forallE _ d b _ := e | break
     if (← isMatchCondFalseHyp d) then
-      trace[grind.debug.matchCond] "satifised{indentExpr e}\nthe following equality is false{indentExpr d}"
+      trace_goal[grind.debug.matchCond] "satifised{indentExpr e}\nthe following equality is false{indentExpr d}"
       return true
     e := b
   return false
@@ -279,13 +281,13 @@ private partial def mkMatchCondProof? (e : Expr) : GoalM (Option Expr) := do
     for x in xs do
       let type ← inferType x
       if (← isMatchCondFalseHyp type) then
-        trace[grind.debug.matchCond] ">>> {type}"
+        trace_goal[grind.debug.matchCond] ">>> {type}"
         let some h ← go? x | pure ()
         return some (← mkLambdaFVars xs h)
     return none
 where
   go? (h : Expr) : GoalM (Option Expr) := do
-    trace[grind.debug.matchCond] "go?: {← inferType h}"
+    trace_goal[grind.debug.matchCond] "go?: {← inferType h}"
     let some (α?, lhs, rhs) := isEqHEq? (← inferType h)
       | return none
     let target ← (← get).mvarId.getType
@@ -318,13 +320,112 @@ where
     else
       return none
 
+/--
+Given a `match`-expression condition `e` that is known to be equal to `True`,
+try to close the goal by proving `False`. We use the following to example to illustrate
+the purpose of this function.
+```
+def f : List Nat → List Nat → Nat
+  | _, 1 :: _ :: _ => 1
+  | _, _ :: _ => 2
+  | _, _  => 0
+
+example : z = a :: as → y = z → f x y > 0 := by
+  grind [f.eq_def]
+```
+After `grind` unfolds `f`, it case splits on the `match`-expression producing
+three subgoals. The first two are easily closed by it. In the third one,
+we have the following two `match`-expression conditions stating that we
+are **not** in the first and second cases.
+```
+Lean.Grind.MatchCond (∀ (head : Nat) (tail : List Nat), x✝² = 1 :: head :: tail → False)
+Lean.Grind.MatchCond (∀ (head : Nat) (tail : List Nat), x✝² = head :: tail → False)
+```
+Moreover, we have the following equivalence class.
+```
+{z, y, x✝², a :: as}
+```
+Thus, we can close the goal by using the second `match`-expression condition,
+we just have to instantiate `head` and `tail` with `a` and `as` respectively,
+and use the fact that `x✝²` is equal to `a :: as`.
+-/
+partial def tryToProveFalse (e : Expr) : GoalM Unit := do
+  trace_goal[grind.debug.matchCond.proveFalse] "{e}"
+  let_expr Grind.MatchCond body ← e | return ()
+  let proof? ← withNewMCtxDepth do
+    let (args, _, _) ← forallMetaTelescope body
+    let mask := mkGenDiseqMask body
+    for arg in args, target in mask do
+      if target then
+        let some (α?, lhs, rhs) := isEqHEq? (← inferType arg)
+          | return none
+        let lhs' ← go lhs
+        trace[grind.debug.matchCond.proveFalse] "{lhs'} =?= {rhs}"
+        unless (← withDefault <| isDefEq lhs' rhs) do
+          return none
+        let isHEq := α?.isSome
+        let some lhsEqLhs' ← if isHEq then proveHEq? lhs lhs' else proveEq? lhs lhs'
+          | return none
+        unless (← isDefEq arg lhsEqLhs') do
+          return none
+    let he := mkOfEqTrueCore e (← mkEqTrueProof e)
+    let falseProof ← instantiateMVars (mkAppN he args)
+    if (← hasAssignableMVar falseProof) then
+      return none
+    trace[grind.debug.matchCond.proveFalse] "{falseProof} : {← inferType falseProof}"
+    return some falseProof
+  let some proof := proof? | return ()
+  closeGoal proof
+where
+  /--
+  Returns a term that is equal to `e`, but containing constructor applications
+  and literal values. `e` is the left-hand side of the equations in a `match`-expression
+  condition.
+  Remark: we could use the right-hand side to interrupt the recursion. For example,
+  suppose the equation is `x = ?head :: ?tail`. We only need to show that `x` is equal to
+  some term of the form `a :: as` to satisfy it. This function may return `a₁ :: b :: bs`,
+  which still allows us to satisfy the equation, but may have a bigger proof (e.g.,
+  a proof that `as` is equal to `b::bs`)
+  -/
+  go (e : Expr) : GoalM Expr := do
+    let root ← getRootENode e
+    if root.ctor then
+      let ctor := root.self
+      let some ctorInfo ← isConstructorApp? ctor | return ctor
+      let mut ctorArgs := ctor.getAppArgs
+      let mut modified := false
+      for i in [ctorInfo.numParams : ctorInfo.numParams + ctorInfo.numFields] do
+        let arg  := ctorArgs[i]!
+        let arg' ← go arg
+        unless isSameExpr arg arg' do
+          ctorArgs := ctorArgs.set! i arg'
+          modified := true
+      if modified then
+        shareCommon <| mkAppN ctor.getAppFn ctorArgs
+      else
+        return root.self
+    else if root.interpreted then
+      return root.self
+    else
+      return e
+
 /-- Propagates `MatchCond` upwards -/
-builtin_grind_propagator propagateMatchCond ↑Grind.MatchCond := fun e => do
-  trace[grind.debug.matchCond] "visiting{indentExpr e}"
-  if !(← isStatisfied e) then return ()
-  let some h ← mkMatchCondProof? e
-     | reportIssue m!"failed to construct proof for{indentExpr e}"; return ()
-  trace[grind.debug.matchCond] "{← inferType h}"
-  pushEqTrue e <| mkEqTrueCore e h
+builtin_grind_propagator propagateMatchCondUp ↑Grind.MatchCond := fun e => do
+  trace_goal[grind.debug.matchCond] "visiting{indentExpr e}"
+  if (← isEqTrue e) then
+    unless (← isStatisfied e) do
+      tryToProveFalse e
+  else
+    if !(← isStatisfied e) then return ()
+    let some h ← mkMatchCondProof? e
+       | reportIssue m!"failed to construct proof for{indentExpr e}"; return ()
+    trace_goal[grind.debug.matchCond] "{← inferType h}"
+    pushEqTrue e <| mkEqTrueCore e h
+
+/-- Propagates `MatchCond` downwards -/
+builtin_grind_propagator propagateMatchCondDown ↓Grind.MatchCond := fun e => do
+  if (← isEqTrue e) then
+    unless (← isStatisfied e) do
+      tryToProveFalse e
 
 end Lean.Meta.Grind

src/Lean/Meta/Tactic/Grind/MatchDiscrOnly.lean

@@ -0,0 +1,42 @@
+/-
+Copyright (c) 2025 Amazon.com, Inc. or its affiliates. All Rights Reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+-/
+prelude
+import Init.Grind.Util
+import Init.Simproc
+import Lean.Meta.Tactic.Simp.Simproc
+import Lean.Meta.Tactic.Simp.Rewrite
+
+namespace Lean.Meta.Grind
+/--
+Returns `Grind.simpMatchDiscrsOnly e`. Recall that `Grind.simpMatchDiscrsOnly` is
+a gadget for instructing the `grind` simplifier to only normalize/simplify
+the discriminants of a `match`-expression. See `reduceSimpMatchDiscrsOnly`.
+-/
+def markAsSimpMatchDiscrsOnly (e : Expr) : MetaM Expr :=
+  mkAppM ``Grind.simpMatchDiscrsOnly #[e]
+
+builtin_simproc_decl reduceSimpMatchDiscrsOnly (Grind.simpMatchDiscrsOnly _) := fun e => do
+  let_expr Grind.simpMatchDiscrsOnly _ m ← e | return .continue
+  let .const declName _ := m.getAppFn
+    | return .done { expr := e }
+  let some info ← getMatcherInfo? declName
+    | return .done { expr := e }
+  if let some r ← Simp.simpMatchDiscrs? info m then
+    return .done { r with expr := (← markAsSimpMatchDiscrsOnly r.expr) }
+  return .done { expr := e }
+
+/-- Adds `reduceSimpMatchDiscrsOnly` to `s` -/
+def addSimpMatchDiscrsOnly (s : Simprocs) : CoreM Simprocs := do
+  s.add ``reduceSimpMatchDiscrsOnly (post := false)
+
+/-- Erases `Grind.simpMatchDiscrsOnly` annotations. -/
+def eraseSimpMatchDiscrsOnly (e : Expr) : CoreM Expr := do
+  let pre (e : Expr) := do
+    let_expr Grind.simpMatchDiscrsOnly _ a := e | return .continue e
+    return .continue a
+  Core.transform e (pre := pre)
+
+end Lean.Meta.Grind

src/Lean/Meta/Tactic/Grind/ProveEq.lean

@@ -0,0 +1,85 @@
+/-
+Copyright (c) 2025 Amazon.com, Inc. or its affiliates. All Rights Reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+-/
+prelude
+import Lean.Meta.Tactic.Grind.Types
+import Lean.Meta.Tactic.Grind.Simp
+
+namespace Lean.Meta.Grind
+
+/--
+Helper function for executing `x` with a fresh `newEqs` and without modifying
+the goal state.
+ -/
+private def withoutModifyingState (x : GoalM α) : GoalM α := do
+  let saved ← get
+  modify fun goal => { goal with newEqs := {} }
+  try
+    x
+  finally
+    set saved
+
+/--
+If `e` has not been internalized yet, simplify it, and internalize the result.
+-/
+private def simpAndInternalize (e : Expr) (gen : Nat := 0) : GoalM Simp.Result := do
+  if (← alreadyInternalized e) then
+    return { expr := e }
+  else
+    let r ← simp e
+    internalize r.expr gen
+    return r
+
+/--
+Try to construct a proof that `lhs = rhs` using the information in the
+goal state. If `lhs` and `rhs` have not been internalized, this function
+will internalize then, process propagated equalities, and then check
+whether they are in the same equivalence class or not.
+The goal state is not modified by this function.
+This function mainly relies on congruence closure, and constraint
+propagation. It will not perform case analysis.
+-/
+def proveEq? (lhs rhs : Expr) : GoalM (Option Expr) := do
+  if (← alreadyInternalized lhs <&&> alreadyInternalized rhs) then
+    if (← isEqv lhs rhs) then
+      return some (← mkEqProof lhs rhs)
+    else
+      return none
+  else withoutModifyingState do
+    let lhs ← simpAndInternalize lhs
+    let rhs ← simpAndInternalize rhs
+    processNewEqs
+    unless (← isEqv lhs.expr rhs.expr) do return none
+    unless (← hasSameType lhs.expr rhs.expr) do return none
+    let h ← mkEqProof lhs.expr rhs.expr
+    let h ← match lhs.proof?, rhs.proof? with
+      | none,    none    => pure h
+      | none,    some h₂ => mkEqTrans h (← mkEqSymm h₂)
+      | some h₁, none    => mkEqTrans h₁ h
+      | some h₁, some h₂ => mkEqTrans (← mkEqTrans h₁ h) (← mkEqSymm h₂)
+    return some h
+
+/-- Similiar to `proveEq?`, but for heterogeneous equality. -/
+def proveHEq? (lhs rhs : Expr) : GoalM (Option Expr) := do
+  if (← alreadyInternalized lhs <&&> alreadyInternalized rhs) then
+    if (← isEqv lhs rhs) then
+      return some (← mkHEqProof lhs rhs)
+    else
+      return none
+  else withoutModifyingState do
+    let lhs ← simpAndInternalize lhs
+    let rhs ← simpAndInternalize rhs
+    processNewEqs
+    unless (← isEqv lhs.expr rhs.expr) do return none
+    let h ← mkHEqProof lhs.expr rhs.expr
+    let h ← match lhs.proof?, rhs.proof? with
+      | none,    none    => pure h
+      | none,    some h₂ => mkHEqTrans h (← mkHEqSymm h₂)
+      | some h₁, none    => mkHEqTrans h₁ h
+      | some h₁, some h₂ => mkHEqTrans (← mkHEqTrans h₁ h) (← mkHEqSymm h₂)
+    return some h
+
+
+end Lean.Meta.Grind

src/Lean/Meta/Tactic/Grind/Simp.lean

@@ -9,7 +9,7 @@ import Lean.Meta.Tactic.Assert
 import Lean.Meta.Tactic.Simp.Main
 import Lean.Meta.Tactic.Grind.Util
 import Lean.Meta.Tactic.Grind.Types
-import Lean.Meta.Tactic.Grind.DoNotSimp
+import Lean.Meta.Tactic.Grind.MatchDiscrOnly
 import Lean.Meta.Tactic.Grind.MarkNestedProofs
 import Lean.Meta.Tactic.Grind.Canon
 
@@ -35,10 +35,10 @@ def simp (e : Expr) : GoalM Simp.Result := do
   let e' ← eraseIrrelevantMData e'
   let e' ← foldProjs e'
   let e' ← normalizeLevels e'
-  let e' ← eraseDoNotSimp e'
+  let e' ← eraseSimpMatchDiscrsOnly e'
   let e' ← canon e'
   let e' ← shareCommon e'
-  trace[grind.simp] "{e}\n===>\n{e'}"
+  trace_goal[grind.simp] "{e}\n===>\n{e'}"
   return { r with expr := e' }
 
 end Lean.Meta.Grind

src/Lean/Meta/Tactic/Grind/SimpUtil.lean

@@ -6,7 +6,7 @@ Authors: Leonardo de Moura
 prelude
 import Lean.Meta.Tactic.Simp.Simproc
 import Lean.Meta.Tactic.Grind.Simp
-import Lean.Meta.Tactic.Grind.DoNotSimp
+import Lean.Meta.Tactic.Grind.MatchDiscrOnly
 import Lean.Meta.Tactic.Grind.MatchCond
 import Lean.Meta.Tactic.Simp.BuiltinSimprocs.List
 
@@ -40,7 +40,7 @@ protected def getSimprocs : MetaM (Array Simprocs) := do
   We don't want it to be simplified to `[] = []`.
   -/
   let s := s.erase ``List.reduceReplicate
-  let s ← addDoNotSimp s
+  let s ← addSimpMatchDiscrsOnly s
   let s ← addMatchCond s
   return #[s]
 

src/Lean/Meta/Tactic/Grind/Split.lean

@@ -91,22 +91,25 @@ private def checkCaseSplitStatus (e : Expr) : GoalM CaseSplitStatus := do
   | dite _ c _ _ _ => checkIteCondStatus c
   | _ =>
     if (← isResolvedCaseSplit e) then
-      trace[grind.debug.split] "split resolved: {e}"
+      trace_goal[grind.debug.split] "split resolved: {e}"
       return .resolved
     if (← isCongrToPrevSplit e) then
       return .resolved
     if let some info := isMatcherAppCore? (← getEnv) e then
       return .ready info.numAlts
-    let .const declName .. := e.getAppFn | unreachable!
-    if let some info ← isInductivePredicate? declName then
-      if (← isEqTrue e) then
-        return .ready info.ctors.length info.isRec
+    if let .const declName .. := e.getAppFn then
+      if let some info ← isInductivePredicate? declName then
+        if (← isEqTrue e) then
+          return .ready info.ctors.length info.isRec
     if e.isFVar then
       let type ← whnfD (← inferType e)
+      trace[Meta.debug] "1. {e}"
       let report : GoalM Unit := do
         reportIssue "cannot perform case-split on {e}, unexpected type{indentExpr type}"
       let .const declName _ := type.getAppFn | report; return .resolved
+      trace[Meta.debug] "2. {e}"
       let .inductInfo info ← getConstInfo declName | report; return .resolved
+      trace[Meta.debug] "3. {e}"
       return .ready info.ctors.length info.isRec
     return .notReady
 
@@ -162,7 +165,11 @@ private def mkCasesMajor (c : Expr) : GoalM Expr := do
       return mkApp3 (mkConst ``Grind.of_eq_eq_true) a b (← mkEqTrueProof c)
     else
       return mkApp3 (mkConst ``Grind.of_eq_eq_false) a b (← mkEqFalseProof c)
-  | _ => return mkOfEqTrueCore c (← mkEqTrueProof c)
+  | _ =>
+    if (← isEqTrue c) then
+      return mkOfEqTrueCore c (← mkEqTrueProof c)
+    else
+      return c
 
 /-- Introduces new hypotheses in each goal. -/
 private def introNewHyp (goals : List Goal) (acc : List Goal) (generation : Nat) : GrindM (List Goal) := do

src/Lean/Meta/Tactic/Grind/Types.lean

@@ -740,6 +740,14 @@ It assumes `a` and `b` are in the same equivalence class.
 @[extern "lean_grind_mk_heq_proof"]
 opaque mkHEqProof (a b : Expr) : GoalM Expr
 
+-- Forward definition
+@[extern "lean_grind_internalize"]
+opaque internalize (e : Expr) (generation : Nat) (parent? : Option Expr := none) : GoalM Unit
+
+-- Forward definition
+@[extern "lean_grind_process_new_eqs"]
+opaque processNewEqs : GoalM Unit
+
 /--
 Returns a proof that `a = b` if they have the same type. Otherwise, returns a proof of `HEq a b`.
 It assumes `a` and `b` are in the same equivalence class.

src/Lean/Meta/Tactic/Simp/Main.lean

@@ -465,7 +465,7 @@ private partial def dsimpImpl (e : Expr) : SimpM Expr := do
   let pre := m.dpre >> doNotVisitOfNat >> doNotVisitOfScientific >> doNotVisitCharLit
   let post := m.dpost >> dsimpReduce
   withInDSimp do
-  transform (usedLetOnly := cfg.zeta) e (pre := pre) (post := post)
+  transform (usedLetOnly := cfg.zeta || cfg.zetaUnused) e (pre := pre) (post := post)
 
 def visitFn (e : Expr) : SimpM Result := do
   let f := e.getAppFn
@@ -623,6 +623,7 @@ It attempts to minimize the quadratic overhead imposed by
 the locally nameless discipline.
 -/
 partial def simpNonDepLetFun (e : Expr) : SimpM Result := do
+  let cfg ← getConfig
   let rec go (xs : Array Expr) (e : Expr) : SimpM SimpLetFunResult := do
     /-
     Helper function applied when `e` is not a `let_fun` or
@@ -648,9 +649,9 @@ partial def simpNonDepLetFun (e : Expr) : SimpM Result := do
     -/
     if alpha.hasLooseBVars || !betaFun.isLambda || !body.isLambda || betaFun.bindingBody!.hasLooseBVars then
       stop
-    else if !body.bindingBody!.hasLooseBVar 0 then
+    else if (cfg.zeta || cfg.zetaUnused) && !body.bindingBody!.hasLooseBVar 0 then
       /-
-      Redundant `let_fun`. The simplifier will remove it.
+      Redundant `let_fun`. The simplifier will remove it when `zetaUnused := true`.
       Remark: the `hasLooseBVar` check here may introduce a quadratic overhead in the worst case.
       If observe that in practice, we may use a separate step for removing unused variables.
 

src/lake/Lake/Build/Facets.lean

@@ -53,7 +53,7 @@ The facet which builds all of a module's dependencies
 Returns the list of shared libraries to load along with their search path.
 -/
 abbrev Module.depsFacet := `deps
-module_data deps : Job (SearchPath × Array FilePath)
+module_data deps : SearchPath × Array FilePath
 
 /--
 The core build facet of a Lean file.
@@ -62,42 +62,42 @@ of the module (i.e., `olean`, `ilean`, `c`).
 Its trace just includes its dependencies.
 -/
 abbrev Module.leanArtsFacet := `leanArts
-module_data leanArts : Job Unit
+module_data leanArts : Unit
 
 /-- The `olean` file produced by `lean`. -/
 abbrev Module.oleanFacet := `olean
-module_data olean : Job FilePath
+module_data olean : FilePath
 
 /-- The `ilean` file produced by `lean`. -/
 abbrev Module.ileanFacet := `ilean
-module_data ilean : Job FilePath
+module_data ilean : FilePath
 
 /-- The C file built from the Lean file via `lean`. -/
 abbrev Module.cFacet := `c
-module_data c : Job FilePath
+module_data c : FilePath
 
 /-- The LLVM BC file built from the Lean file via `lean`. -/
 abbrev Module.bcFacet := `bc
-module_data bc : Job FilePath
+module_data bc : FilePath
 
 /--
 The object file `.c.o` built from `c`.
 On Windows, this is `c.o.noexport`, on other systems it is `c.o.export`).
 -/
 abbrev Module.coFacet := `c.o
-module_data c.o : Job FilePath
+module_data c.o : FilePath
 
 /-- The object file `.c.o.export` built from `c` (with `-DLEAN_EXPORTING`). -/
 abbrev Module.coExportFacet := `c.o.export
-module_data c.o.export : Job FilePath
+module_data c.o.export : FilePath
 
 /-- The object file `.c.o.noexport` built from `c` (without `-DLEAN_EXPORTING`). -/
 abbrev Module.coNoExportFacet := `c.o.noexport
-module_data c.o.noexport : Job FilePath
+module_data c.o.noexport : FilePath
 
 /-- The object file `.bc.o` built from `bc`. -/
 abbrev Module.bcoFacet := `bc.o
-module_data bc.o : Job FilePath
+module_data bc.o : FilePath
 
 /--
 The object file built from `c`/`bc`.
@@ -105,15 +105,15 @@ On Windows with the C backend, no Lean symbols are exported.
 On every other configuration, symbols are exported.
 -/
 abbrev Module.oFacet := `o
-module_data o : Job FilePath
+module_data o : FilePath
 
 /-- The object file built from `c`/`bc` (with Lean symbols exported). -/
 abbrev Module.oExportFacet := `o.export
-module_data o.export : Job FilePath
+module_data o.export : FilePath
 
 /-- The object file built from `c`/`bc` (without Lean symbols exported). -/
 abbrev Module.oNoExportFacet := `o.noexport
-module_data o.noexport : Job FilePath
+module_data o.noexport : FilePath
 
 
 /-! ## Package Facets -/
@@ -123,35 +123,35 @@ A package's *optional* cached build archive (e.g., from Reservoir or GitHub).
 Will NOT cause the whole build to fail if the archive cannot be fetched.
 -/
 abbrev Package.optBuildCacheFacet := `optCache
-package_data optCache : Job Bool
+package_data optCache : Bool
 
 /--
 A package's cached build archive (e.g., from Reservoir or GitHub).
 Will cause the whole build to fail if the archive cannot be fetched.
 -/
 abbrev Package.buildCacheFacet := `cache
-package_data cache : Job Unit
+package_data cache : Unit
 
 /--
 A package's *optional* build archive from Reservoir.
 Will NOT cause the whole build to fail if the barrel cannot be fetched.
 -/
 abbrev Package.optReservoirBarrelFacet := `optBarrel
-package_data optBarrel : Job Bool
+package_data optBarrel : Bool
 
 /--
 A package's Reservoir build archive from Reservoir.
 Will cause the whole build to fail if the barrel cannot be fetched.
 -/
 abbrev Package.reservoirBarrelFacet := `barrel
-package_data barrel : Job Unit
+package_data barrel : Unit
 
 /--
 A package's *optional* build archive from a GitHub release.
 Will NOT cause the whole build to fail if the release cannot be fetched.
 -/
 abbrev Package.optGitHubReleaseFacet := `optRelease
-package_data optRelease : Job Bool
+package_data optRelease : Bool
 
 @[deprecated optGitHubReleaseFacet (since := "2024-09-27")]
 abbrev Package.optReleaseFacet := optGitHubReleaseFacet
@@ -161,49 +161,49 @@ A package's build archive from a GitHub release.
 Will cause the whole build to fail if the release cannot be fetched.
 -/
 abbrev Package.gitHubReleaseFacet := `release
-package_data release : Job Unit
+package_data release : Unit
 
 @[deprecated gitHubReleaseFacet (since := "2024-09-27")]
 abbrev Package.releaseFacet := gitHubReleaseFacet
 
 /-- A package's `extraDepTargets` mixed with its transitive dependencies'. -/
 abbrev Package.extraDepFacet := `extraDep
-package_data extraDep : Job Unit
+package_data extraDep : Unit
 
 /-! ## Target Facets -/
 
 /-- A Lean library's Lean artifacts (i.e., `olean`, `ilean`, `c`). -/
 abbrev LeanLib.leanArtsFacet := `leanArts
-library_data leanArts : Job Unit
+library_data leanArts : Unit
 
 /-- A Lean library's static artifact. -/
 abbrev LeanLib.staticFacet := `static
-library_data static : Job FilePath
+library_data static : FilePath
 
 /-- A Lean library's static artifact (with exported symbols). -/
 abbrev LeanLib.staticExportFacet := `static.export
-library_data static.export : Job FilePath
+library_data static.export : FilePath
 
 /-- A Lean library's shared artifact. -/
 abbrev LeanLib.sharedFacet := `shared
-library_data shared : Job FilePath
+library_data shared : FilePath
 
 /-- A Lean library's `extraDepTargets` mixed with its package's. -/
 abbrev LeanLib.extraDepFacet := `extraDep
-library_data extraDep : Job Unit
+library_data extraDep : Unit
 
 /-- A Lean binary executable. -/
 abbrev LeanExe.exeFacet := `leanExe
-target_data leanExe : Job FilePath
+target_data leanExe : FilePath
 
 /-- A external library's static binary. -/
 abbrev ExternLib.staticFacet := `externLib.static
-target_data externLib.static : Job FilePath
+target_data externLib.static : FilePath
 
 /-- A external library's shared binary. -/
 abbrev ExternLib.sharedFacet := `externLib.shared
-target_data externLib.shared : Job FilePath
+target_data externLib.shared : FilePath
 
 /-- A external library's dynlib. -/
 abbrev ExternLib.dynlibFacet := `externLib.dynlib
-target_data externLib.dynlib : Job Dynlib
+target_data externLib.dynlib : Dynlib

src/lake/Lake/Build/Fetch.lean

@@ -59,8 +59,8 @@ abbrev RecBuildM := RecBuildT LogIO
 
 /-- A build function for any element of the Lake build index. -/
 abbrev IndexBuildFn (m : Type → Type v) :=
-  -- `DFetchFn BuildInfo (BuildData ·.key) m` with less imports
-  (info : BuildInfo) → m (BuildData info.key)
+  -- `DFetchFn BuildInfo (Job <| BuildData ·.key) m` with less imports
+  (info : BuildInfo) → m (Job (BuildData info.key))
 
 /-- A transformer to equip a monad with a build function for the Lake index. -/
 abbrev IndexT (m : Type → Type v) := EquipT (IndexBuildFn RecBuildM) m
@@ -78,7 +78,7 @@ abbrev FetchM := FetchT LogIO
 @[deprecated FetchM (since := "2024-04-30")] abbrev BuildM := BuildT LogIO
 
 /-- Fetch the result associated with the info using the Lake build index. -/
-@[inline] def BuildInfo.fetch (self : BuildInfo) [FamilyOut BuildData self.key α] : FetchM α :=
+@[inline] def BuildInfo.fetch (self : BuildInfo) [FamilyOut BuildData self.key α] : FetchM (Job α) :=
   fun build => cast (by simp) <| build self
 
 export BuildInfo (fetch)

src/lake/Lake/Build/Index.lean

@@ -26,13 +26,13 @@ dynamically-typed equivalent.
 -/
 @[macro_inline] def mkTargetFacetBuild
   (facet : Name) (build : FetchM (Job α))
-  [h : FamilyOut TargetData facet (Job α)]
-: FetchM (TargetData facet) :=
+  [h : FamilyOut TargetData facet α]
+: FetchM (Job (TargetData facet)) :=
   cast (by rw [← h.family_key_eq_type]) build
 
 def ExternLib.recBuildStatic (lib : ExternLib) : FetchM (Job FilePath) :=
   withRegisterJob s!"{lib.staticTargetName.toString}:static" do
-  lib.config.getJob <$> fetch (lib.pkg.target lib.staticTargetName)
+  lib.config.getPath <$> fetch (lib.pkg.target lib.staticTargetName)
 
 def ExternLib.recBuildShared (lib : ExternLib) : FetchM (Job FilePath) :=
   withRegisterJob s!"{lib.staticTargetName.toString}:shared" do
@@ -47,7 +47,7 @@ def ExternLib.recComputeDynlib (lib : ExternLib) : FetchM (Job Dynlib) := do
 -/
 
 /-- Recursive build function for anything in the Lake build index. -/
-def recBuildWithIndex : (info : BuildInfo) → FetchM (BuildData info.key)
+def recBuildWithIndex : (info : BuildInfo) → FetchM (Job (BuildData info.key))
 | .moduleFacet mod facet => do
   if let some config := (← getWorkspace).findModuleFacetConfig? facet then
     config.build mod
@@ -82,4 +82,5 @@ Run a recursive Lake build using the Lake build index
 and a topological / suspending scheduler.
 -/
 def FetchM.run (x : FetchM α) : RecBuildM α :=
-  x (inline <| recFetchMemoize BuildInfo.key recBuildWithIndex)
+  x <| inline <|
+    recFetchMemoize (β := (Job <| BuildData ·)) BuildInfo.key recBuildWithIndex

src/lake/Lake/Build/Info.lean

@@ -125,27 +125,27 @@ definitions.
 
 /-- The direct local imports of the Lean module. -/
 abbrev Module.importsFacet := `lean.imports
-module_data lean.imports : Job (Array Module)
+module_data lean.imports : Array Module
 
 /-- The transitive local imports of the Lean module. -/
 abbrev Module.transImportsFacet := `lean.transImports
-module_data lean.transImports : Job (Array Module)
+module_data lean.transImports : Array Module
 
 /-- The transitive local imports of the Lean module. -/
 abbrev Module.precompileImportsFacet := `lean.precompileImports
-module_data lean.precompileImports : Job (Array Module)
+module_data lean.precompileImports : Array Module
 
 /-- Shared library for `--load-dynlib`. -/
 abbrev Module.dynlibFacet := `dynlib
-module_data dynlib : Job Dynlib
+module_data dynlib : Dynlib
 
 /-- A Lean library's Lean modules. -/
 abbrev LeanLib.modulesFacet := `modules
-library_data modules : Job (Array Module)
+library_data modules : Array Module
 
 /-- The package's complete array of transitive dependencies. -/
 abbrev Package.depsFacet := `deps
-package_data deps : Job (Array Package)
+package_data deps : Array Package
 
 
 /-!

src/lake/Lake/Build/Package.lean

@@ -147,7 +147,7 @@ def Package.fetchBuildArchive
 private def Package.mkOptBuildArchiveFacetConfig
   {facet : Name} (archiveFile : Package → FilePath)
   (getUrl : Package → JobM String) (headers : Array String := #[])
-  [FamilyDef PackageData facet (Job Bool)]
+  [FamilyDef PackageData facet Bool]
 : PackageFacetConfig facet := mkFacetJobConfig fun pkg =>
   withRegisterJob s!"{pkg.name}:{facet}" (optional := true) <| Job.async do
   try
@@ -161,8 +161,8 @@ private def Package.mkOptBuildArchiveFacetConfig
 @[inline]
 private def Package.mkBuildArchiveFacetConfig
   {facet : Name} (optFacet : Name) (what : String)
-  [FamilyDef PackageData facet (Job Unit)]
-  [FamilyDef PackageData optFacet (Job Bool)]
+  [FamilyDef PackageData facet Unit]
+  [FamilyDef PackageData optFacet Bool]
 : PackageFacetConfig facet :=
   mkFacetJobConfig fun pkg =>
     withRegisterJob s!"{pkg.name}:{facet}" do

src/lake/Lake/Build/Store.lean

@@ -5,6 +5,7 @@ Authors: Mac Malone
 -/
 prelude
 import Lake.Build.Data
+import Lake.Build.Job.Basic
 import Lake.Util.StoreInsts
 
 /-!
@@ -19,23 +20,21 @@ namespace Lake
 open Lean (Name NameMap)
 
 /-- A monad equipped with a Lake build store. -/
-abbrev MonadBuildStore (m) := MonadDStore BuildKey BuildData m
+abbrev MonadBuildStore (m) := MonadDStore BuildKey (Job <| BuildData ·) m
 
 /-- The type of the Lake build store. -/
 abbrev BuildStore :=
-  DRBMap BuildKey BuildData BuildKey.quickCmp
+  DRBMap BuildKey (Job <| BuildData ·) BuildKey.quickCmp
 
 @[inline] def BuildStore.empty : BuildStore := DRBMap.empty
 
 namespace BuildStore
 
--- Linter reports false positives on the `v` variables below
-set_option linter.unusedVariables false
-
 /-- Derive an array of built module facets from the store. -/
-def collectModuleFacetArray (self : BuildStore)
-(facet : Name) [FamilyOut ModuleData facet α] : Array α := Id.run do
-  let mut res : Array α := #[]
+def collectModuleFacetArray
+  (self : BuildStore) (facet : Name) [FamilyOut ModuleData facet α]
+: Array (Job α) := Id.run do
+  let mut res : Array (Job α) := #[]
   for ⟨k, v⟩ in self do
     match k with
     | .moduleFacet m f =>
@@ -46,9 +45,10 @@ def collectModuleFacetArray (self : BuildStore)
   return res
 
 /-- Derive a map of module names to built facets from the store. -/
-def collectModuleFacetMap (self : BuildStore)
-(facet : Name) [FamilyOut ModuleData facet α] : NameMap α := Id.run do
-  let mut res := Lean.mkNameMap α
+def collectModuleFacetMap
+  (self : BuildStore) (facet : Name) [FamilyOut ModuleData facet α]
+: NameMap (Job α) := Id.run do
+  let mut res := Lean.mkNameMap (Job α)
   for ⟨k, v⟩ in self do
     match k with
     | .moduleFacet m f =>
@@ -59,9 +59,10 @@ def collectModuleFacetMap (self : BuildStore)
   return res
 
 /-- Derive an array of built package facets from the store. -/
-def collectPackageFacetArray (self : BuildStore)
-(facet : Name) [FamilyOut PackageData facet α] : Array α := Id.run do
-  let mut res : Array α := #[]
+def collectPackageFacetArray
+  (self : BuildStore) (facet : Name) [FamilyOut PackageData facet α]
+: Array (Job α) := Id.run do
+  let mut res : Array (Job α) := #[]
   for ⟨k, v⟩ in self do
     match k with
     | .packageFacet _ f =>
@@ -72,9 +73,10 @@ def collectPackageFacetArray (self : BuildStore)
   return res
 
 /-- Derive an array of built target facets from the store. -/
-def collectTargetFacetArray (self : BuildStore)
-(facet : Name) [FamilyOut TargetData facet α] : Array α := Id.run do
-  let mut res : Array α := #[]
+def collectTargetFacetArray
+  (self : BuildStore) (facet : Name) [FamilyOut TargetData facet α]
+: Array (Job α) := Id.run do
+  let mut res : Array (Job α) := #[]
   for ⟨k, v⟩ in self do
     match k with
     | .targetFacet _ _ f =>
@@ -85,6 +87,6 @@ def collectTargetFacetArray (self : BuildStore)
   return res
 
 /-- Derive an array of built external shared libraries from the store. -/
-def collectSharedExternLibs (self : BuildStore)
-[FamilyOut TargetData `externLib.shared α] : Array α :=
-  self.collectTargetFacetArray `externLib.shared
+def collectSharedExternLibs
+  (self : BuildStore) [FamilyOut TargetData `externLib.shared α]
+: Array (Job α) := self.collectTargetFacetArray `externLib.shared

src/lake/Lake/Build/Targets.lean

@@ -19,16 +19,14 @@ open System (FilePath)
 /-- Fetch the build job of the specified package target. -/
 def Package.fetchTargetJob
   (self : Package) (target : Name)
-: FetchM OpaqueJob :=  do
-  let some config := self.findTargetConfig? target
-    | error s!"package '{self.name}' has no target '{target}'"
-  return config.getJob (← fetch <| self.target target)
+: FetchM OpaqueJob := do
+  return (← fetch <| self.target target).toOpaque
 
 /-- Fetch the build result of a target. -/
 protected def TargetDecl.fetch
   (self : TargetDecl)
   [FamilyOut CustomData (self.pkg, self.name) α]
-: FetchM α := do
+: FetchM (Job α) := do
   let some pkg ← findPackage? self.pkg
     | error s!"package '{self.pkg}' of target '{self.name}' does not exist in workspace"
   fetch <| pkg.target self.name
@@ -37,51 +35,43 @@ protected def TargetDecl.fetch
 def TargetDecl.fetchJob (self : TargetDecl) : FetchM OpaqueJob :=  do
   let some pkg ← findPackage? self.pkg
     | error s!"package '{self.pkg}' of target '{self.name}' does not exist in workspace"
-  return self.config.getJob (← fetch <| pkg.target self.name)
+  return (← fetch <| pkg.target self.name).toOpaque
 
 /-- Fetch the build result of a package facet. -/
 @[inline] protected def PackageFacetDecl.fetch
   (pkg : Package) (self : PackageFacetDecl) [FamilyOut PackageData self.name α]
-: FetchM α := fetch <| pkg.facet self.name
+: FetchM (Job α) := fetch <| pkg.facet self.name
 
 /-- Fetch the build job of a package facet. -/
 def PackageFacetConfig.fetchJob
   (pkg : Package) (self : PackageFacetConfig name)
-: FetchM OpaqueJob :=  do
-  let some getJob := self.getJob?
-    | error s!"package facet '{name}' has no associated build job"
-  return getJob <| ← fetch <| pkg.facet self.name
+: FetchM OpaqueJob := do
+  return  (← fetch <| pkg.facet self.name).toOpaque
 
 /-- Fetch the build job of a library facet. -/
 def Package.fetchFacetJob
   (name : Name) (self : Package)
-: FetchM OpaqueJob :=  do
-  let some config := (← getWorkspace).packageFacetConfigs.find? name
-    | error s!"package facet '{name}' does not exist in workspace"
-  inline <| config.fetchJob self
+: FetchM OpaqueJob := do
+  return  (← fetch <| self.facet name).toOpaque
 
 /-! ## Module Facets -/
 
 /-- Fetch the build result of a module facet. -/
 @[inline] protected def ModuleFacetDecl.fetch
   (mod : Module) (self : ModuleFacetDecl) [FamilyOut ModuleData self.name α]
-: FetchM α := fetch <| mod.facet self.name
+: FetchM (Job α) := fetch <| mod.facet self.name
 
 /-- Fetch the build job of a module facet. -/
 def ModuleFacetConfig.fetchJob
   (mod : Module) (self : ModuleFacetConfig name)
-: FetchM OpaqueJob :=  do
-  let some getJob := self.getJob?
-    | error s!"module facet '{self.name}' has no associated build job"
-  return getJob <| ← fetch <| mod.facet self.name
+: FetchM OpaqueJob := do
+  return (← fetch <| mod.facet self.name).toOpaque
 
 /-- Fetch the build job of a module facet. -/
 def Module.fetchFacetJob
   (name : Name) (self : Module)
-: FetchM OpaqueJob :=  do
-  let some config := (← getWorkspace).moduleFacetConfigs.find? name
-    | error s!"library facet '{name}' does not exist in workspace"
-  inline <| config.fetchJob self
+: FetchM OpaqueJob := do
+  return (← fetch <| self.facet name).toOpaque
 
 /-! ## Lean Library Facets -/
 
@@ -95,23 +85,19 @@ def Module.fetchFacetJob
 /-- Fetch the build result of a library facet. -/
 @[inline] protected def LibraryFacetDecl.fetch
   (lib : LeanLib) (self : LibraryFacetDecl) [FamilyOut LibraryData self.name α]
-: FetchM α := fetch <| lib.facet self.name
+: FetchM (Job α) := fetch <| lib.facet self.name
 
 /-- Fetch the build job of a library facet. -/
 def LibraryFacetConfig.fetchJob
   (lib : LeanLib) (self : LibraryFacetConfig name)
-: FetchM OpaqueJob :=  do
-  let some getJob := self.getJob?
-    | error s!"library facet '{self.name}' has no associated build job"
-  return getJob <| ← fetch <| lib.facet self.name
+: FetchM OpaqueJob := do
+  return (← fetch <| lib.facet self.name).toOpaque
 
 /-- Fetch the build job of a library facet. -/
 def LeanLib.fetchFacetJob
   (name : Name) (self : LeanLib)
-: FetchM OpaqueJob :=  do
-  let some config := (← getWorkspace).libraryFacetConfigs.find? name
-    | error s!"library facet '{name}' does not exist in workspace"
-  inline <| config.fetchJob self
+: FetchM OpaqueJob := do
+  return (← fetch <| self.facet name).toOpaque
 
 /-! ## Lean Executable Target -/
 

src/lake/Lake/CLI/Build.lean

@@ -15,7 +15,6 @@ open Lean (Name)
 
 structure BuildSpec where
   info : BuildInfo
-  getBuildJob : BuildData info.key → OpaqueJob
 
 @[inline] def BuildData.toJob
   [FamilyOut BuildData k (Job α)] (data : BuildData k)
@@ -23,21 +22,18 @@ structure BuildSpec where
   ofFamily data |>.toOpaque
 
 @[inline] def mkBuildSpec
-  (info : BuildInfo) [FamilyOut BuildData info.key (Job α)]
-: BuildSpec :=
-  {info, getBuildJob := BuildData.toJob}
+  (info : BuildInfo) [FamilyOut BuildData info.key α]
+: BuildSpec := {info}
 
 @[inline] def mkConfigBuildSpec
-  (facetType : String) (info : BuildInfo)
-  (config : FacetConfig Fam ι facet) (h : BuildData info.key = Fam facet)
+  (facetType : String) (info : BuildInfo) (config : FacetConfig Fam ι facet)
 : Except CliError BuildSpec := do
-  let some getBuildJob := config.getJob?
-    | throw <| CliError.nonCliFacet facetType facet
-  return {info, getBuildJob := h ▸ getBuildJob}
+  unless config.cli do
+    throw <| CliError.nonCliFacet facetType facet
+  return {info}
 
 @[inline] protected def BuildSpec.fetch (self : BuildSpec) : FetchM OpaqueJob := do
-  maybeRegisterJob (self.info.key.toSimpleString) <| ← do
-    self.getBuildJob <$> self.info.fetch
+  maybeRegisterJob (self.info.key.toSimpleString) (← self.info.fetch)
 
 def buildSpecs (specs : Array BuildSpec) : FetchM (Job Unit) := do
   return .mixArray (← specs.mapM (·.fetch))
@@ -59,7 +55,7 @@ def resolveModuleTarget
   if facet.isAnonymous then
     return mkBuildSpec <| mod.facet leanArtsFacet
   else if let some config := ws.findModuleFacetConfig? facet then do
-    mkConfigBuildSpec "module" (mod.facet facet) config rfl
+    mkConfigBuildSpec "module" (mod.facet facet) config
   else
     throw <| CliError.unknownFacet "module" facet
 
@@ -73,7 +69,7 @@ def resolveLibTarget
 where
   resolveFacet facet :=
     if let some config := ws.findLibraryFacetConfig? facet then do
-      mkConfigBuildSpec "library" (lib.facet facet) config rfl
+      mkConfigBuildSpec "library" (lib.facet facet) config
     else
       throw <| CliError.unknownFacet "library" facet
 
@@ -91,14 +87,14 @@ def resolveExternLibTarget (lib : ExternLib) (facet : Name) : Except CliError Bu
   else
     throw <| CliError.unknownFacet "external library" facet
 
-def resolveCustomTarget (pkg : Package)
-(name facet : Name) (config : TargetConfig pkg.name name) : Except CliError BuildSpec :=
+set_option linter.unusedVariables false in
+def resolveCustomTarget
+  (pkg : Package) (name facet : Name) (config : TargetConfig pkg.name name)
+: Except CliError BuildSpec :=
   if !facet.isAnonymous then
     throw <| CliError.invalidFacet name facet
   else do
-    let info := pkg.target name
-    have h : BuildData info.key = CustomData (pkg.name, name) := rfl
-    return {info, getBuildJob := h ▸ config.getJob}
+    return {info := pkg.target name}
 
 def resolveTargetInPackage (ws : Workspace)
 (pkg : Package) (target facet : Name) : Except CliError (Array BuildSpec) :=
@@ -122,7 +118,7 @@ def resolvePackageTarget (ws : Workspace) (pkg : Package) (facet : Name) : Excep
   if facet.isAnonymous then
     resolveDefaultPackageTarget ws pkg
   else if let some config := ws.findPackageFacetConfig? facet then do
-    Array.singleton <$> mkConfigBuildSpec "package" (pkg.facet facet) config rfl
+    Array.singleton <$> mkConfigBuildSpec "package" (pkg.facet facet) config
   else
     throw <| CliError.unknownFacet "package" facet
 

src/lake/Lake/Config/ExternLibConfig.lean

@@ -13,7 +13,7 @@ open Lean System
 /-- A external library's declarative configuration. -/
 structure ExternLibConfig (pkgName name : Name) where
   /-- The library's build data. -/
-  getJob : CustomData (pkgName, .str name "static") → Job FilePath
+  getPath : Job (CustomData (pkgName, .str name "static")) → Job FilePath
   deriving Inhabited
 
 /-- A dependently typed configuration based on its registered package and name. -/

src/lake/Lake/Config/FacetConfig.lean

@@ -11,25 +11,19 @@ open Lean (Name)
 
 /-- A facet's declarative configuration. -/
 structure FacetConfig (DataFam : Name → Type) (ι : Type) (name : Name) : Type where
-  /-- The facet's build (function). -/
-  build : ι → FetchM (DataFam name)
-  /-- Does this facet produce an associated asynchronous job? -/
-  getJob? : Option (DataFam name → OpaqueJob)
+  /-- The facet's build function. -/
+  build : ι → FetchM (Job (DataFam name))
+  /-- Does this facet  compatible with the `lake build` CLI? -/
+  cli : Bool := true
   deriving Inhabited
 
 protected abbrev FacetConfig.name (_ : FacetConfig DataFam ι name) := name
 
-/-- A smart constructor for facet configurations that are not known to generate targets. -/
-@[inline] def mkFacetConfig (build : ι → FetchM α)
-[h : FamilyOut Fam facet α] : FacetConfig Fam ι facet where
-  build := cast (by rw [← h.family_key_eq_type]) build
-  getJob? := none
-
 /-- A smart constructor for facet configurations that generate jobs for the CLI. -/
-@[inline] def mkFacetJobConfig (build : ι → FetchM (Job α))
-[h : FamilyOut Fam facet (Job α)] : FacetConfig Fam ι facet where
+@[inline] def mkFacetJobConfig
+  (build : ι → FetchM (Job α)) [h : FamilyOut Fam facet α]
+: FacetConfig Fam ι facet  where
   build := cast (by rw [← h.family_key_eq_type]) build
-  getJob? := some fun data => ofFamily data |>.toOpaque
 
 /-- A dependently typed configuration based on its registered name. -/
 structure NamedConfigDecl (β : Name → Type u) where

src/lake/Lake/Config/LeanExeConfig.lean

@@ -71,7 +71,7 @@ structure LeanExeConfig extends LeanConfig where
   `Module.oFacet`. That is, the  object file compiled from the Lean source,
   potentially with exported Lean symbols.
   -/
-  nativeFacets (shouldExport : Bool) : Array (ModuleFacet (Job FilePath)) :=
+  nativeFacets (shouldExport : Bool) : Array (ModuleFacet FilePath) :=
     #[if shouldExport then Module.oExportFacet else Module.oFacet]
 
 deriving Inhabited

src/lake/Lake/Config/LeanLib.lean

@@ -97,7 +97,7 @@ Otherwise, falls back to the package's.
   self.config.defaultFacets
 
 /-- The library's `nativeFacets` configuration. -/
-@[inline] def nativeFacets (self : LeanLib) (shouldExport : Bool) : Array (ModuleFacet (Job FilePath)) :=
+@[inline] def nativeFacets (self : LeanLib) (shouldExport : Bool) : Array (ModuleFacet FilePath) :=
   self.config.nativeFacets shouldExport
 
 /--

src/lake/Lake/Config/LeanLibConfig.lean

@@ -79,7 +79,7 @@ structure LeanLibConfig extends LeanConfig where
   `Module.oFacet`. That is, the  object files compiled from the Lean sources,
   potentially with exported Lean symbols.
   -/
-  nativeFacets (shouldExport : Bool) : Array (ModuleFacet (Job FilePath)) :=
+  nativeFacets (shouldExport : Bool) : Array (ModuleFacet FilePath) :=
     #[if shouldExport then Module.oExportFacet else Module.oFacet]
 
 deriving Inhabited

src/lake/Lake/Config/Module.lean

@@ -148,7 +148,7 @@ def dynlibSuffix := "-1"
 @[inline] def shouldPrecompile (self : Module) : Bool :=
   self.lib.precompileModules
 
-@[inline] def nativeFacets (self : Module) (shouldExport : Bool) : Array (ModuleFacet (Job FilePath)) :=
+@[inline] def nativeFacets (self : Module) (shouldExport : Bool) : Array (ModuleFacet FilePath) :=
   self.lib.nativeFacets shouldExport
 
 /-! ## Trace Helpers -/

src/lake/Lake/Config/TargetConfig.lean

@@ -12,17 +12,15 @@ open Lean (Name)
 /-- A custom target's declarative configuration. -/
 structure TargetConfig (pkgName name : Name) : Type where
   /-- The target's build function. -/
-  build : (pkg : NPackage pkgName) → FetchM (CustomData (pkgName, name))
-  /-- The target's resulting build job. -/
-  getJob : CustomData (pkgName, name) → OpaqueJob
+  build : (pkg : NPackage pkgName) → FetchM (Job (CustomData (pkgName, name)))
   deriving Inhabited
 
 /-- A smart constructor for target configurations that generate CLI targets. -/
 @[inline] def mkTargetJobConfig
-(build : (pkg : NPackage pkgName) → FetchM (Job α))
-[h : FamilyOut CustomData (pkgName, name) (Job α)] : TargetConfig pkgName name where
+  (build : (pkg : NPackage pkgName) → FetchM (Job α))
+  [h : FamilyOut CustomData (pkgName, name) α]
+: TargetConfig pkgName name where
   build := cast (by rw [← h.family_key_eq_type]) build
-  getJob := fun data => ofFamily data |>.toOpaque
 
 /-- A dependently typed configuration based on its registered package and name. -/
 structure TargetDecl where

src/lake/Lake/DSL/Targets.lean

@@ -24,7 +24,7 @@ syntax buildDeclSig :=
 
 abbrev mkModuleFacetDecl
   (α) (facet : Name)
-  [FamilyDef ModuleData facet (Job α)]
+  [FamilyDef ModuleData facet α]
   (f : Module → FetchM (Job α))
 : ModuleFacetDecl := .mk facet <| mkFacetJobConfig fun mod => do
   withRegisterJob (mod.facet facet |>.key.toSimpleString)
@@ -51,7 +51,7 @@ kw:"module_facet " sig:buildDeclSig : command => withRef kw do
     let facet := Name.quoteFrom id id.getId
     let declId := mkIdentFrom id <| id.getId.modifyBase (.str · "_modFacet")
     let mod ← expandOptSimpleBinder mod?
-    `(module_data $id : Job $ty
+    `(module_data $id : $ty
       $[$doc?:docComment]? @[$attrs,*] abbrev $declId :=
         Lake.DSL.mkModuleFacetDecl $ty $facet (fun $mod => $defn)
       $[$wds?:whereDecls]?)
@@ -59,7 +59,7 @@ kw:"module_facet " sig:buildDeclSig : command => withRef kw do
 
 abbrev mkPackageFacetDecl
   (α) (facet : Name)
-  [FamilyDef PackageData facet (Job α)]
+  [FamilyDef PackageData facet α]
   (f : Package → FetchM (Job α))
 : PackageFacetDecl := .mk facet <| mkFacetJobConfig fun pkg => do
   withRegisterJob (pkg.facet facet |>.key.toSimpleString)
@@ -86,7 +86,7 @@ kw:"package_facet " sig:buildDeclSig : command => withRef kw do
     let facet := Name.quoteFrom id id.getId
     let declId := mkIdentFrom id <| id.getId.modifyBase (.str · "_pkgFacet")
     let pkg ← expandOptSimpleBinder pkg?
-    `(package_data $id : Job $ty
+    `(package_data $id : $ty
       $[$doc?]? @[$attrs,*] abbrev $declId :=
         Lake.DSL.mkPackageFacetDecl $ty $facet (fun $pkg => $defn)
       $[$wds?:whereDecls]?)
@@ -94,7 +94,7 @@ kw:"package_facet " sig:buildDeclSig : command => withRef kw do
 
 abbrev mkLibraryFacetDecl
   (α) (facet : Name)
-  [FamilyDef LibraryData facet (Job α)]
+  [FamilyDef LibraryData facet α]
   (f : LeanLib → FetchM (Job α))
 : LibraryFacetDecl := .mk facet <| mkFacetJobConfig fun lib => do
   withRegisterJob (lib.facet facet |>.key.toSimpleString)
@@ -121,7 +121,7 @@ kw:"library_facet " sig:buildDeclSig : command => withRef kw do
     let facet := Name.quoteFrom id id.getId
     let declId := mkIdentFrom id <| id.getId.modifyBase (.str · "_libFacet")
     let lib ← expandOptSimpleBinder lib?
-    `(library_data $id : Job $ty
+    `(library_data $id : $ty
       $[$doc?]? @[$attrs,*] abbrev $declId : LibraryFacetDecl :=
         Lake.DSL.mkLibraryFacetDecl $ty $facet (fun $lib => $defn)
       $[$wds?:whereDecls]?)
@@ -133,7 +133,7 @@ kw:"library_facet " sig:buildDeclSig : command => withRef kw do
 
 abbrev mkTargetDecl
   (α) (pkgName target : Name)
-  [FamilyDef CustomData (pkgName, target) (Job α)]
+  [FamilyDef CustomData (pkgName, target) α]
   (f : NPackage pkgName → FetchM (Job α))
 : TargetDecl := .mk pkgName target <| mkTargetJobConfig fun pkg => do
   withRegisterJob (pkg.target target |>.key.toSimpleString)
@@ -161,7 +161,7 @@ kw:"target " sig:buildDeclSig : command => do
     let name := Name.quoteFrom id id.getId
     let pkgName := mkIdentFrom id `_package.name
     let pkg ← expandOptSimpleBinder pkg?
-    `(family_def $id : CustomData ($pkgName, $name) := Job $ty
+    `(family_def $id : CustomData ($pkgName, $name) := $ty
       $[$doc?]? @[$attrs,*] abbrev $id :=
         Lake.DSL.mkTargetDecl $ty $pkgName $name (fun $pkg => $defn)
       $[$wds?:whereDecls]?)
@@ -222,6 +222,11 @@ instance : Coe LeanExeDecl Command where
 /-! ## External Library Target Declaration                                    -/
 --------------------------------------------------------------------------------
 
+abbrev mkExternLibDecl
+  (pkgName name : Name)
+  [FamilyDef CustomData (pkgName, .str name "static")  FilePath]
+: ExternLibDecl := .mk pkgName name {getPath := cast (by simp)}
+
 syntax externLibDeclSpec :=
   identOrStr (ppSpace simpleBinder)? declValSimple
 
@@ -251,9 +256,6 @@ kw:"extern_lib " spec:externLibDeclSpec : command => withRef kw do
     let targetId := mkIdentFrom id <| id.getId.modifyBase (· ++ `static)
     let name := Name.quoteFrom id id.getId
     `(target $targetId:ident $[$pkg?]? : FilePath := $defn $[$wds?:whereDecls]?
-      $[$doc?:docComment]? @[$attrs,*] def $id : ExternLibDecl := {
-        pkg := $pkgName
-        name := $name
-        config := {getJob := ofFamily}
-      })
+      $[$doc?:docComment]? @[$attrs,*] def $id : ExternLibDecl :=
+        Lake.DSL.mkExternLibDecl $pkgName $name)
   | stx => Macro.throwErrorAt stx "ill-formed external library declaration"

tests/lean/run/grind_match_cond_contra.lean

@@ -0,0 +1,7 @@
+def f : List Nat → List Nat → Nat
+  | _, 1 :: _ :: _ => 1
+  | _, _ :: _ => 2
+  | _, _  => 0
+
+example : z = a :: as → y = z → f x y > 0 := by
+  grind [f.eq_def]

tests/lean/run/grind_offset_model.lean

@@ -0,0 +1,119 @@
+def g (i : Nat) (j : Nat) := i + j
+
+set_option grind.debug true
+set_option grind.debug.proofs true
+
+/--
+error: `grind` failed
+case grind
+i j : Nat
+h : j + 1 ≤ i
+x✝ : ¬g (i + 1) j = i + 1
+⊢ False
+[grind] Diagnostics
+  [facts] Asserted facts
+    [prop] j + 1 ≤ i
+    [prop] ¬g (i + 1) j = i + 1
+  [eqc] True propositions
+    [prop] j + 1 ≤ i
+  [eqc] False propositions
+    [prop] g (i + 1) j = i + 1
+  [offset] Assignment satisfying offset contraints
+    [assign] j := 0
+    [assign] i := 1
+    [assign] i + 1 := 2
+    [assign] 0 := 0
+-/
+#guard_msgs (error) in
+example (i j : Nat) (h : i + 1 > j + 1) : g (i+1) j = i + 1 := by
+  grind
+
+/--
+error: `grind` failed
+case grind
+i : Nat
+x✝ : 101 ≤ i
+⊢ False
+[grind] Diagnostics
+  [facts] Asserted facts
+    [prop] 101 ≤ i
+  [eqc] True propositions
+    [prop] 101 ≤ i
+  [offset] Assignment satisfying offset contraints
+    [assign] 0 := 0
+    [assign] i := 101
+-/
+#guard_msgs (error) in
+example (i : Nat) : i ≤ 100 := by
+  grind
+
+/--
+error: `grind` failed
+case grind
+i : Nat
+x✝ : i ≤ 99
+⊢ False
+[grind] Diagnostics
+  [facts] Asserted facts
+    [prop] i ≤ 99
+  [eqc] True propositions
+    [prop] i ≤ 99
+  [offset] Assignment satisfying offset contraints
+    [assign] i := 99
+    [assign] 0 := 0
+-/
+#guard_msgs (error) in
+example (i : Nat) : 100 ≤ i := by
+  grind
+
+/--
+error: `grind` failed
+case grind
+n m a j i : Nat
+a✝ : g (n + 1) m = a
+x✝ : i ≤ j + 99
+⊢ False
+[grind] Diagnostics
+  [facts] Asserted facts
+    [prop] g (n + 1) m = a
+    [prop] i ≤ j + 99
+  [eqc] True propositions
+    [prop] i ≤ j + 99
+  [eqc] Equivalence classes
+    [eqc] {g (n + 1) m, a}
+  [offset] Assignment satisfying offset contraints
+    [assign] n + 1 := 1
+    [assign] n := 0
+    [assign] 0 := 0
+    [assign] i := 99
+    [assign] j := 0
+-/
+#guard_msgs (error) in
+example (i : Nat) : g (n + 1) m = a → 100 + j ≤ i := by
+  grind
+
+/--
+error: `grind` failed
+case grind
+n m a j i : Nat
+a✝ : g (n + 1) m = a
+x✝ : i + 101 ≤ j
+⊢ False
+[grind] Diagnostics
+  [facts] Asserted facts
+    [prop] g (n + 1) m = a
+    [prop] i + 101 ≤ j
+  [eqc] True propositions
+    [prop] i + 101 ≤ j
+  [eqc] Equivalence classes
+    [eqc] {g (n + 1) m, a}
+  [offset] Assignment satisfying offset contraints
+    [assign] n + 1 := 1
+    [assign] n := 0
+    [assign] 0 := 0
+    [assign] i := 0
+    [assign] j := 101
+-/
+#guard_msgs (error) in
+example (i : Nat) : g (n + 1) m = a → j ≤ i + 100 := by
+  grind

tests/lean/run/grind_pre.lean

@@ -94,7 +94,10 @@ x✝ : ¬g (i + 1) j ⋯ = i + j + 1
   [offset] Assignment satisfying offset contraints
     [assign] j := 0
     [assign] i := 1
-    [assign] i + j := 1
+    [assign] i + 1 := 2
+    [assign] 0 := 0
+    [assign] i + j + 1 := 1
+    [assign] i + j := 0
 -/
 #guard_msgs (error) in
 example (i j : Nat) (h : i + 1 > j + 1) : g (i+1) j = f ((fun x => x) i) + f j + 1 := by
@@ -192,10 +195,8 @@ info: [grind.issues] found congruence between
     and
       f a
     but functions have different types
----
-warning: declaration uses 'sorry'
 -/
-#guard_msgs in
+#guard_msgs (info) in
 set_option trace.grind.issues true in
 set_option trace.grind.debug.proof false in
 example (f : Nat → Bool) (g : Int → Bool) (a : Nat) (b : Int) : HEq f g → HEq a b → f a = g b := by

tests/lean/run/grind_split_data.lean

@@ -0,0 +1,13 @@
+inductive C where
+  | a | b | c
+
+def f : C → Nat
+  | .a => 2
+  | .b => 3
+  | .c => 4
+
+example : f .a > 1 := by
+  grind [f]
+
+example : f x > 1 := by
+  grind [f, C]

tests/lean/run/grind_t1.lean

@@ -357,3 +357,6 @@ set_option trace.grind.issues true in
 example : (if n + 2 < m then a else b) = (if n + 1 < m then c else d) := by
   fail_if_success grind (splits := 0)
   sorry
+
+example (f : Nat → Nat) : f (a + 1) = 1 → a = 0 → f 1 = 1 := by
+  grind

tests/lean/run/grind_usr.lean

@@ -0,0 +1,75 @@
+opaque f : Nat → Nat
+
+/--
+error: the modifier `usr` is only relevant in parameters for `grind only`
+-/
+#guard_msgs (error) in
+@[grind usr]
+theorem fthm : f (f x) = f x := sorry
+
+/--
+info: [grind.ematch.pattern] fthm: [f (f #0)]
+-/
+#guard_msgs (info) in
+set_option trace.grind.ematch.pattern true in
+example : f (f (f x)) = f x := by
+  grind only [fthm]
+
+/--
+info: [grind.ematch.instance] fthm: f (f (f x)) = f (f x)
+[grind.ematch.instance] fthm: f (f x) = f x
+-/
+#guard_msgs (info) in
+set_option trace.grind.ematch.instance true in
+example : f (f (f x)) = f x := by
+  grind only [fthm]
+
+#guard_msgs (info) in
+-- should not instantiate anything using pattern `f (f #0)`
+set_option trace.grind.ematch.instance true in
+example : f x = x := by
+  fail_if_success grind only [fthm]
+  sorry
+
+/--
+error: the modifier `usr` is only relevant in parameters for `grind only`
+-/
+#guard_msgs (error) in
+example : f (f (f x)) = f x := by
+  grind [usr fthm]
+
+/--
+error: invalid use of `usr` modifier, `fthm` does not have patterns specified with the command `grind_pattern`
+-/
+#guard_msgs (error) in
+example : f (f (f x)) = f x := by
+  grind only [usr fthm]
+
+grind_pattern fthm => f x
+
+example : f (f (f x)) = f x := by
+  grind only [usr fthm]
+
+#guard_msgs (info) in
+-- should not instantiate anything using pattern `f (f #0)`
+set_option trace.grind.ematch.instance true in
+example : f x = x := by
+  fail_if_success grind only [fthm]
+  sorry
+
+/--
+info: [grind.ematch.instance] fthm: f (f x) = f x
+[grind.ematch.instance] fthm: f (f (f x)) = f (f x)
+-/
+#guard_msgs (info) in
+set_option trace.grind.ematch.instance true in
+example : f x = x := by
+  fail_if_success grind only [usr fthm]
+  sorry
+
+/--
+error: the modifier `usr` is only relevant in parameters for `grind only`
+-/
+#guard_msgs (error) in
+example : f (f (f x)) = f x := by
+  grind [usr fthm]

tests/lean/run/zetaUnused.lean

@@ -0,0 +1,80 @@
+
+/--
+info: b : Bool
+⊢ if b = true then
+    let_fun unused := ();
+    True
+  else False
+---
+warning: declaration uses 'sorry'
+-/
+#guard_msgs in
+example (b : Bool) : if b then have unused := (); True else False := by
+  trace_state; sorry
+
+/--
+info: b : Bool
+⊢ b = true
+---
+warning: declaration uses 'sorry'
+-/
+#guard_msgs in
+example (b : Bool) : if b then have unused := (); True else False := by
+  simp; trace_state; sorry
+
+/--
+info: b : Bool
+⊢ b = true ∧
+    let_fun unused := ();
+    True
+---
+warning: declaration uses 'sorry'
+-/
+#guard_msgs in
+example (b : Bool) : if b then have unused := (); True else False := by
+  simp (config := Lean.Meta.Simp.neutralConfig); trace_state; sorry
+
+/-- error: simp made no progress -/
+#guard_msgs in
+example (b : Bool) : if b then have unused := (); True else False := by
+  simp (config := Lean.Meta.Simp.neutralConfig) only; trace_state; sorry
+
+/--
+info: b : Bool
+⊢ if b = true then True else False
+---
+warning: declaration uses 'sorry'
+-/
+#guard_msgs in
+example (b : Bool) : if b then have unused := (); True else False := by
+  simp (config := Lean.Meta.Simp.neutralConfig) +zeta only; trace_state; sorry
+
+
+/--
+info: b : Bool
+⊢ if b = true then True else False
+---
+warning: declaration uses 'sorry'
+-/
+#guard_msgs in
+example (b : Bool) : if b then have unused := (); True else False := by
+  simp (config := Lean.Meta.Simp.neutralConfig) +zetaUnused only; trace_state; sorry
+
+
+-- Before the introduction of zetaUnused, split would do collateral damage to unused letFuns.
+-- Now they are preserved:
+
+/--
+info: case isTrue
+b : Bool
+h✝ : b = true
+⊢ let_fun unused := ();
+  True
+---
+warning: declaration uses 'sorry'
+-/
+#guard_msgs in
+example (b : Bool) : if b then have unused := (); True else False := by
+  split
+  · trace_state; sorry
+  · sorry