feat: add grind.injection

Recall that we create a (non-dependent) copy.

src/Lean/Meta/CtorRecognizer.lean

@@ -14,13 +14,11 @@ private def getConstructorVal? (env : Environment) (ctorName : Name) : Option Co
   | some (.ctorInfo v) => v
   | _                  => none
 
-
 /--
-If `e` is a constructor application or a builtin literal defeq to a constructor application,
+If `e` is a constructor application,
 then return the corresponding `ConstructorVal`.
 -/
-def isConstructorApp? (e : Expr) : MetaM (Option ConstructorVal) := do
-  let e ← litToCtor e
+def isConstructorAppCore? (e : Expr) : MetaM (Option ConstructorVal) := do
   let .const n _ := e.getAppFn | return none
   let some v := getConstructorVal? (← getEnv) n | return none
   if v.numParams + v.numFields == e.getAppNumArgs then
@@ -28,6 +26,13 @@ def isConstructorApp? (e : Expr) : MetaM (Option ConstructorVal) := do
   else
     return none
 
+/--
+If `e` is a constructor application or a builtin literal defeq to a constructor application,
+then return the corresponding `ConstructorVal`.
+-/
+def isConstructorApp? (e : Expr) : MetaM (Option ConstructorVal) := do
+  isConstructorAppCore? (← litToCtor e)
+
 /--
 Similar to `isConstructorApp?`, but uses `whnf`.
 -/

src/Lean/Meta/Tactic/Grind.lean

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

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

@@ -0,0 +1,39 @@
+/-
+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.CtorRecognizer
+import Lean.Meta.Tactic.Util
+import Lean.Meta.Tactic.Clear
+
+namespace Lean.Meta.Grind
+/--
+The `grind` tactic includes an auxiliary `injection?` tactic that is not intended for direct use by users.
+This tactic is automatically applied when introducing non-dependent propositions.
+It differs from the user-facing Lean `injection` tactic in the following ways:
+
+- It does not introduce new propositions. Instead, the `grind` tactic preprocessor is responsible for introducing them.
+- It assumes that `fvarId` is the latest local declaration in the current goal.
+- It does not handle cases where the constructors are different because the simplifier already reduces such equalities to `False`.
+- It does not have support for heterogeneous equality. Recall that the simplifier already reduces them to `Eq` if
+  the types are definitionally equal.
+-/
+def injection? (mvarId : MVarId) (fvarId : FVarId) : MetaM (Option MVarId) := mvarId.withContext do
+  let decl ← fvarId.getDecl
+  let_expr Eq _ a b := decl.type | return none
+  match (← isConstructorAppCore? a), (← isConstructorAppCore? b) with
+  | some aCtor, some bCtor =>
+    if aCtor.name != bCtor.name then return none -- Simplifier handles this case
+    let target ← mvarId.getType
+    let val ← mkNoConfusion target (mkFVar fvarId)
+    let .forallE _ targetNew _ _ ← whnfD (← inferType val) | return none
+    let targetNew := targetNew.headBeta
+    let tag ← mvarId.getTag
+    let mvarNew ← mkFreshExprSyntheticOpaqueMVar targetNew tag
+    mvarId.assign (mkApp val mvarNew)
+    return some (← mvarNew.mvarId!.clear fvarId)
+  | _, _ => return none
+
+end Lean.Meta.Grind

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

@@ -14,6 +14,7 @@ import Lean.Meta.Tactic.Grind.RevertAll
 import Lean.Meta.Tactic.Grind.Types
 import Lean.Meta.Tactic.Grind.Util
 import Lean.Meta.Tactic.Grind.Cases
+import Lean.Meta.Tactic.Grind.Injection
 
 namespace Lean.Meta.Grind
 namespace Preprocessor
@@ -57,6 +58,7 @@ def simpHyp? (mvarId : MVarId) (fvarId : FVarId) : PreM (Option (FVarId × MVarI
 inductive IntroResult where
   | done
   | newHyp (fvarId : FVarId) (goal : Goal)
+  | newDepHyp (goal : Goal)
   | newLocal (fvarId : FVarId) (goal : Goal)
 
 def introNext (goal : Goal) : PreM IntroResult := do
@@ -96,7 +98,7 @@ def introNext (goal : Goal) : PreM IntroResult := do
       if (← isProp localDecl.type) then
         -- Add a non-dependent copy
         let mvarId ← mvarId.assert localDecl.userName localDecl.type (mkFVar fvarId)
-        return .newLocal fvarId { goal with mvarId }
+        return .newDepHyp { goal with mvarId }
       else
         return .newLocal fvarId { goal with mvarId }
   else
@@ -117,8 +119,13 @@ def applyCases? (goal : Goal) (fvarId : FVarId) : MetaM (Option (List Goal)) :=
   else
     return none
 
+def applyInjection? (goal : Goal) (fvarId : FVarId) : MetaM (Option Goal) := do
+  if let some mvarId ← injection? goal.mvarId fvarId then
+    return some { goal with mvarId }
+  else
+    return none
+
 partial def preprocess (goal : Goal) : PreM Unit := do
-  trace[Meta.debug] "{goal.mvarId}"
   match (← introNext goal) with
   | .done =>
     if let some mvarId ← goal.mvarId.byContra? then
@@ -128,9 +135,13 @@ partial def preprocess (goal : Goal) : PreM Unit := do
   | .newHyp fvarId goal =>
     if let some goals ← applyCases? goal fvarId then
       goals.forM preprocess
+    else if let some goal ← applyInjection? goal fvarId then
+      preprocess goal
     else
       let clause ← goal.mvarId.withContext do mkInputClause fvarId
       preprocess { goal with clauses := goal.clauses.push clause }
+  | .newDepHyp goal =>
+    preprocess goal
   | .newLocal fvarId goal =>
     if let some goals ← applyCases? goal fvarId then
       goals.forM preprocess

tests/lean/run/grind_pre.lean

@@ -35,3 +35,28 @@ example (i j : Nat) (h : i + 1 > j + 1) : g (i+1) j = f ((fun x => x) i) + f j +
   next hn =>
   guard_hyp hn : ¬g (i + 1) j _ = i + j + 1
   simp_arith [g] at hn
+
+/--
+warning: declaration uses 'sorry'
+---
+info: α✝ : Type ?u.1908
+β✝ : Type ?u.1907
+a₁ : α✝ × β✝
+a₂ : α✝
+a₃ : β✝
+as : List (α✝ × β✝)
+b₁ : α✝ × β✝
+b₂ : α✝
+b₃ : β✝
+bs : List (α✝ × β✝)
+head_eq : a₁ = b₁
+fst_eq : a₂ = b₂
+snd_eq : a₃ = b₃
+tail_eq : as = bs
+⊢ False
+-/
+#guard_msgs in
+example (h : a₁ :: (a₂, a₃) :: as = b₁ :: (b₂, b₃) :: bs) : False := by
+  grind_pre
+  trace_state
+  sorry