feat: grind.cases tactic

src/Lean/Meta/Tactic/Grind.lean

@@ -9,3 +9,4 @@ import Lean.Meta.Tactic.Grind.RevertAll
 import Lean.Meta.Tactic.Grind.Types
 import Lean.Meta.Tactic.Grind.Preprocessor
 import Lean.Meta.Tactic.Grind.Util
+import Lean.Meta.Tactic.Grind.Cases

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

@@ -0,0 +1,62 @@
+/-
+Copyright (c) 2024 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.Cases
+
+namespace Lean.Meta.Grind
+/--
+The `grind` tactic includes an auxiliary `cases` tactic that is not intended for direct use by users.
+This method implements it.
+This tactic is automatically applied when introducing local declarations with a type tagged with `[grind_cases]`.
+It differs from the user-facing Lean `cases` tactic in the following ways:
+
+- It avoids unnecessary `revert` and `intro` operations.
+
+- It does not introduce new local declarations for each minor premise. Instead, the `grind` tactic preprocessor is responsible for introducing them.
+
+- It assumes that the major premise (i.e., the parameter `fvarId`) is the latest local declaration in the current goal.
+
+- If the major premise type is an indexed family, auxiliary declarations and (heterogeneous) equalities are introduced.
+  However, these equalities are not resolved using `unifyEqs`. Instead, the `grind` tactic employs union-find and
+  congruence closure to process these auxiliary equalities. This approach avoids applying substitution to propositions
+  that have already been internalized by `grind`.
+-/
+def cases (mvarId : MVarId) (fvarId : FVarId) : MetaM (List MVarId) := mvarId.withContext do
+  let tag ← mvarId.getTag
+  let type ← whnf (← fvarId.getType)
+  let .const declName _ := type.getAppFn | throwInductiveExpected type
+  let .inductInfo _ ← getConstInfo declName | throwInductiveExpected type
+  let recursorInfo ← mkRecursorInfo (mkCasesOnName declName)
+  let k (mvarId : MVarId) (fvarId : FVarId) (indices : Array Expr) (clearMajor : Bool) : MetaM (List MVarId) := do
+    let recursor ← mkRecursorAppPrefix mvarId `grind.cases fvarId recursorInfo indices
+    let mut recursor := mkApp (mkAppN recursor indices) (mkFVar fvarId)
+    let mut recursorType ← inferType recursor
+    let mut mvarIdsNew := #[]
+    for _ in [:recursorInfo.numMinors] do
+      let .forallE _ targetNew recursorTypeNew _ ← whnf recursorType
+        | throwTacticEx `grind.cases mvarId "unexpected recursor type"
+      recursorType := recursorTypeNew
+      let mvar ← mkFreshExprSyntheticOpaqueMVar targetNew tag
+      recursor := mkApp recursor mvar
+      let mvarIdNew ← if clearMajor then
+        mvar.mvarId!.clear fvarId
+      else
+        pure mvar.mvarId!
+      mvarIdsNew := mvarIdsNew.push mvarIdNew
+    mvarId.assign recursor
+    return mvarIdsNew.toList
+  if recursorInfo.numIndices > 0 then
+    let s ← generalizeIndices mvarId fvarId
+    s.mvarId.withContext do
+      k s.mvarId s.fvarId (s.indicesFVarIds.map mkFVar) (clearMajor := false)
+  else
+    let indices ← getMajorTypeIndices mvarId `grind.cases recursorInfo type
+    k mvarId fvarId indices (clearMajor := true)
+where
+  throwInductiveExpected {α} (type : Expr) : MetaM α := do
+    throwTacticEx `grind.cases mvarId m!"(non-recursive) inductive type expected at {mkFVar fvarId}{indentExpr type}"
+
+end Lean.Meta.Grind

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

@@ -13,6 +13,7 @@ import Lean.Meta.Tactic.Grind.Attr
 import Lean.Meta.Tactic.Grind.RevertAll
 import Lean.Meta.Tactic.Grind.Types
 import Lean.Meta.Tactic.Grind.Util
+import Lean.Meta.Tactic.Grind.Cases
 
 namespace Lean.Meta.Grind
 namespace Preprocessor
@@ -104,6 +105,18 @@ def introNext (goal : Goal) : PreM IntroResult := do
 def pushResult (goal : Goal) : PreM Unit :=
   modifyThe Grind.State fun s => { s with goals := s.goals.push goal }
 
+-- TODO: use `[grind_cases]` attribute
+def isCasesCandidate (fvarId : FVarId) : MetaM Bool := do
+  let type ← fvarId.getType
+  return type.isAppOf ``And
+
+def applyCases? (goal : Goal) (fvarId : FVarId) : MetaM (Option (List Goal)) := goal.mvarId.withContext do
+  if (← isCasesCandidate fvarId) then
+    let mvarIds ← cases goal.mvarId fvarId
+    return mvarIds.map fun mvarId => { goal with mvarId }
+  else
+    return none
+
 partial def preprocess (goal : Goal) : PreM Unit := do
   trace[Meta.debug] "{goal.mvarId}"
   match (← introNext goal) with
@@ -113,12 +126,16 @@ partial def preprocess (goal : Goal) : PreM Unit := do
     else
       pushResult goal
   | .newHyp fvarId goal =>
-    -- TODO: apply eliminators
-    let clause ← goal.mvarId.withContext do mkInputClause fvarId
-    preprocess { goal with clauses := goal.clauses.push clause }
-  | .newLocal _ goal =>
-    -- TODO: apply eliminators
-    preprocess goal
+    if let some goals ← applyCases? goal fvarId then
+      goals.forM preprocess
+    else
+      let clause ← goal.mvarId.withContext do mkInputClause fvarId
+      preprocess { goal with clauses := goal.clauses.push clause }
+  | .newLocal fvarId goal =>
+    if let some goals ← applyCases? goal fvarId then
+      goals.forM preprocess
+    else
+      preprocess goal
 
 end Preprocessor
 

src/Lean/Meta/Tactic/Induction.lean

@@ -120,8 +120,75 @@ private partial def finalize
       pure subgoals
   loop (recursorInfo.paramsPos.length + 1) 0 recursor recursorType false #[]
 
-private def throwUnexpectedMajorType {α} (mvarId : MVarId) (majorType : Expr) : MetaM α :=
-  throwTacticEx `induction mvarId m!"unexpected major premise type{indentExpr majorType}"
+private def throwUnexpectedMajorType (tacticName : Name) (mvarId : MVarId) (majorType : Expr) : MetaM α :=
+  throwTacticEx tacticName mvarId m!"unexpected major premise type{indentExpr majorType}"
+
+/--
+Auxiliary method for implementing `induction`-like tactics.
+It retrieves indices from `majorType` using `recursorInfo`.
+Remark: `mvarId` and `tacticName` are used to generate error messages.
+-/
+def getMajorTypeIndices (mvarId : MVarId) (tacticName : Name) (recursorInfo : RecursorInfo) (majorType : Expr) : MetaM (Array Expr) := do
+  let majorTypeArgs := majorType.getAppArgs
+  recursorInfo.indicesPos.toArray.mapM fun idxPos => do
+    if idxPos ≥ majorTypeArgs.size then throwTacticEx tacticName mvarId m!"major premise type is ill-formed{indentExpr majorType}"
+    let idx := majorTypeArgs.get! idxPos
+    unless idx.isFVar do throwTacticEx tacticName mvarId m!"major premise type index {idx} is not a variable{indentExpr majorType}"
+    majorTypeArgs.size.forM fun i => do
+      let arg := majorTypeArgs[i]!
+      if i != idxPos && arg == idx then
+        throwTacticEx tacticName mvarId m!"'{idx}' is an index in major premise, but it occurs more than once{indentExpr majorType}"
+      if i < idxPos then
+        if (← exprDependsOn arg idx.fvarId!) then
+          throwTacticEx tacticName mvarId m!"'{idx}' is an index in major premise, but it occurs in previous arguments{indentExpr majorType}"
+      -- If arg is also and index and a variable occurring after `idx`, we need to make sure it doesn't depend on `idx`.
+      -- Note that if `arg` is not a variable, we will fail anyway when we visit it.
+      if i > idxPos && recursorInfo.indicesPos.contains i && arg.isFVar then
+        let idxDecl ← idx.fvarId!.getDecl
+        if (← localDeclDependsOn idxDecl arg.fvarId!) then
+          throwTacticEx tacticName mvarId m!"'{idx}' is an index in major premise, but it depends on index occurring at position #{i+1}"
+    return idx
+
+/--
+Auxiliary method for implementing `induction`-like tactics.
+It creates the prefix of a recursor application up-to `motive`.
+The motive is computed by abstracting `major` and `indices` at `mvarId.getType`.
+It retrieves indices from `majorType` using `recursorInfo`.
+Remark: `mvarId` and `tacticName` are used to generate error messages.
+-/
+def mkRecursorAppPrefix (mvarId : MVarId) (tacticName : Name) (majorFVarId : FVarId) (recursorInfo : RecursorInfo) (indices : Array Expr) : MetaM Expr := do
+  let major := mkFVar majorFVarId
+  let target ← mvarId.getType
+  let targetLevel ← getLevel target
+  let targetLevel ← normalizeLevel targetLevel
+  let majorLocalDecl ← majorFVarId.getDecl
+  let some majorType ← whnfUntil majorLocalDecl.type recursorInfo.typeName
+    | throwUnexpectedMajorType tacticName mvarId majorLocalDecl.type
+  majorType.withApp fun majorTypeFn majorTypeArgs => do
+    match majorTypeFn with
+    | .const _ majorTypeFnLevels => do
+      let majorTypeFnLevels := majorTypeFnLevels.toArray
+      let (recursorLevels, foundTargetLevel) ← recursorInfo.univLevelPos.foldlM (init := (#[], false))
+          fun (recursorLevels, foundTargetLevel) (univPos : RecursorUnivLevelPos) => do
+            match univPos with
+            | RecursorUnivLevelPos.motive => pure (recursorLevels.push targetLevel, true)
+            | RecursorUnivLevelPos.majorType idx =>
+              if idx ≥ majorTypeFnLevels.size then throwTacticEx tacticName mvarId "ill-formed recursor"
+              pure (recursorLevels.push (majorTypeFnLevels.get! idx), foundTargetLevel)
+      if !foundTargetLevel && !targetLevel.isZero then
+        throwTacticEx tacticName mvarId m!"recursor '{recursorInfo.recursorName}' can only eliminate into Prop"
+      let recursor := mkConst recursorInfo.recursorName recursorLevels.toList
+      let recursor ← addRecParams mvarId majorTypeArgs recursorInfo.paramsPos recursor
+      -- Compute motive
+      let motive := target
+      let motive ← if recursorInfo.depElim then
+        pure <| mkLambda `x BinderInfo.default (← inferType major) (← motive.abstractM #[major])
+      else
+        pure motive
+      let motive ← mkLambdaFVars indices motive
+      return mkApp recursor motive
+    | _ =>
+      throwTacticEx tacticName mvarId "major premise is not of the form (C ...)"
 
 def _root_.Lean.MVarId.induction (mvarId : MVarId) (majorFVarId : FVarId) (recursorName : Name) (givenNames : Array AltVarNames := #[]) : MetaM (Array InductionSubgoal) :=
   mvarId.withContext do
@@ -129,30 +196,14 @@ def _root_.Lean.MVarId.induction (mvarId : MVarId) (majorFVarId : FVarId) (recur
     mvarId.checkNotAssigned `induction
     let majorLocalDecl ← majorFVarId.getDecl
     let recursorInfo ← mkRecursorInfo recursorName
-    let some majorType ← whnfUntil majorLocalDecl.type recursorInfo.typeName | throwUnexpectedMajorType mvarId majorLocalDecl.type
+    let some majorType ← whnfUntil majorLocalDecl.type recursorInfo.typeName
+      | throwUnexpectedMajorType `induction mvarId majorLocalDecl.type
     majorType.withApp fun _ majorTypeArgs => do
       recursorInfo.paramsPos.forM fun paramPos? => do
         match paramPos? with
         | none          => pure ()
         | some paramPos => if paramPos ≥ majorTypeArgs.size then throwTacticEx `induction mvarId m!"major premise type is ill-formed{indentExpr majorType}"
-      let indices ← recursorInfo.indicesPos.toArray.mapM fun idxPos => do
-        if idxPos ≥ majorTypeArgs.size then throwTacticEx `induction mvarId m!"major premise type is ill-formed{indentExpr majorType}"
-        let idx := majorTypeArgs.get! idxPos
-        unless idx.isFVar do throwTacticEx `induction mvarId m!"major premise type index {idx} is not a variable{indentExpr majorType}"
-        majorTypeArgs.size.forM fun i => do
-          let arg := majorTypeArgs[i]!
-          if i != idxPos && arg == idx then
-            throwTacticEx `induction mvarId m!"'{idx}' is an index in major premise, but it occurs more than once{indentExpr majorType}"
-          if i < idxPos then
-            if (← exprDependsOn arg idx.fvarId!) then
-              throwTacticEx `induction mvarId m!"'{idx}' is an index in major premise, but it occurs in previous arguments{indentExpr majorType}"
-          -- If arg is also and index and a variable occurring after `idx`, we need to make sure it doesn't depend on `idx`.
-          -- Note that if `arg` is not a variable, we will fail anyway when we visit it.
-          if i > idxPos && recursorInfo.indicesPos.contains i && arg.isFVar then
-            let idxDecl ← idx.fvarId!.getDecl
-            if (← localDeclDependsOn idxDecl arg.fvarId!) then
-              throwTacticEx `induction mvarId m!"'{idx}' is an index in major premise, but it depends on index occurring at position #{i+1}"
-        pure idx
+      let indices ← getMajorTypeIndices mvarId `induction recursorInfo majorType
       let target ← mvarId.getType
       if (← pure !recursorInfo.depElim <&&> exprDependsOn target majorFVarId) then
         throwTacticEx `induction mvarId m!"recursor '{recursorName}' does not support dependent elimination, but conclusion depends on major premise"
@@ -175,37 +226,8 @@ def _root_.Lean.MVarId.induction (mvarId : MVarId) (majorFVarId : FVarId) (recur
       let majorFVarId := majorFVarId'
       let major := mkFVar majorFVarId
       mvarId.withContext do
-        let target ← mvarId.getType
-        let targetLevel ← getLevel target
-        let targetLevel ← normalizeLevel targetLevel
-        let majorLocalDecl ← majorFVarId.getDecl
-        let some majorType ← whnfUntil majorLocalDecl.type recursorInfo.typeName | throwUnexpectedMajorType mvarId majorLocalDecl.type
-        majorType.withApp fun majorTypeFn majorTypeArgs => do
-          match majorTypeFn with
-          | Expr.const _ majorTypeFnLevels => do
-            let majorTypeFnLevels := majorTypeFnLevels.toArray
-            let (recursorLevels, foundTargetLevel) ← recursorInfo.univLevelPos.foldlM (init := (#[], false))
-                fun (recursorLevels, foundTargetLevel) (univPos : RecursorUnivLevelPos) => do
-                  match univPos with
-                  | RecursorUnivLevelPos.motive => pure (recursorLevels.push targetLevel, true)
-                  | RecursorUnivLevelPos.majorType idx =>
-                    if idx ≥ majorTypeFnLevels.size then throwTacticEx `induction mvarId "ill-formed recursor"
-                    pure (recursorLevels.push (majorTypeFnLevels.get! idx), foundTargetLevel)
-            if !foundTargetLevel && !targetLevel.isZero then
-              throwTacticEx `induction mvarId m!"recursor '{recursorName}' can only eliminate into Prop"
-            let recursor := mkConst recursorName recursorLevels.toList
-            let recursor ← addRecParams mvarId majorTypeArgs recursorInfo.paramsPos recursor
-            -- Compute motive
-            let motive := target
-            let motive ← if recursorInfo.depElim then
-              pure <| mkLambda `x BinderInfo.default (← inferType major) (← motive.abstractM #[major])
-            else
-              pure motive
-            let motive ← mkLambdaFVars indices motive
-            let recursor := mkApp recursor motive
-            finalize mvarId givenNames recursorInfo reverted major indices baseSubst recursor
-          | _ =>
-           throwTacticEx `induction mvarId "major premise is not of the form (C ...)"
+        let recursor ← mkRecursorAppPrefix mvarId `induction majorFVarId recursorInfo indices
+        finalize mvarId givenNames recursorInfo reverted major indices baseSubst recursor
 
 @[deprecated MVarId.induction (since := "2022-07-15")]
 def induction (mvarId : MVarId) (majorFVarId : FVarId) (recursorName : Name) (givenNames : Array AltVarNames := #[]) : MetaM (Array InductionSubgoal) :=

tests/lean/run/grind_pre.lean

@@ -14,8 +14,10 @@ warning: declaration uses 'sorry'
 ---
 info: a b c : Bool
 p q : Prop
-h : a = true ∧ (b = true ∨ c = true)
-h' : p ∧ q
+left✝ : a = true
+right✝ : b = true ∨ c = true
+left : p
+right : q
 x✝ : b = false ∨ a = false
 ⊢ False
 -/