feat: exfalso in grind

This PR ensures that `grind` can be used as a more powerful `contradiction` tactic, sparing the user from having to type `exfalso; grind` or `intros; exfalso; grind`.

src/Init/Grind/Lemmas.lean

@@ -15,7 +15,7 @@ namespace Lean.Grind
 theorem rfl_true : true = true :=
   rfl
 
-theorem intro_with_eq (p p' q : Prop) (he : p = p') (h : p' → q) : p → q :=
+def intro_with_eq (p p' : Prop) (q : Sort u) (he : p = p') (h : p' → q) : p → q :=
   fun hp => h (he.mp hp)
 
 /-! And -/

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

@@ -119,7 +119,8 @@ private def introNext (goal : Goal) (generation : Nat) : GrindM IntroResult := d
           let h ← mkLambdaFVars #[mkFVar fvarId] mvarNew
           match r.proof? with
           | some he =>
-            let hNew := mkAppN (mkConst ``Lean.Grind.intro_with_eq) #[p, r.expr, q, he, h]
+            let u ← getLevel q
+            let hNew := mkAppN (mkConst ``Lean.Grind.intro_with_eq [u]) #[p, r.expr, q, he, h]
             mvarId.assign hNew
             return .newHyp fvarId { (← get) with mvarId := mvarIdNew }
           | none =>
@@ -170,6 +171,12 @@ private def applyInjection? (goal : Goal) (fvarId : FVarId) : MetaM (Option Goal
   else
     return none
 
+private def exfalsoIfNotProp (goal : Goal) : MetaM Goal := goal.mvarId.withContext do
+  if (← isProp (← goal.mvarId.getType)) then
+    return goal
+  else
+    return { goal with mvarId := (← goal.mvarId.exfalso) }
+
 /-- Introduce new hypotheses (and apply `by_contra`) until goal is of the form `... ⊢ False` -/
 partial def intros  (generation : Nat) : GrindTactic' := fun goal => do
   let rec go (goal : Goal) : StateRefT (Array Goal) GrindM Unit := do
@@ -177,6 +184,7 @@ partial def intros  (generation : Nat) : GrindTactic' := fun goal => do
       return ()
     match (← introNext goal generation) with
     | .done =>
+      let goal ← exfalsoIfNotProp goal
       if let some mvarId ← goal.mvarId.byContra? then
         go { goal with mvarId }
       else

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

@@ -94,7 +94,6 @@ private def mkGoal (mvarId : MVarId) (params : Params) : GrindM Goal := do
       activateTheorem thm 0
 
 private def initCore (mvarId : MVarId) (params : Params) : GrindM (List Goal) := do
-  mvarId.ensureProp
   -- TODO: abstract metavars
   mvarId.ensureNoMVar
   let mvarId ← mvarId.clearAuxDecls

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

@@ -20,14 +20,6 @@ def _root_.Lean.MVarId.ensureNoMVar (mvarId : MVarId) : MetaM Unit := do
   if type.hasExprMVar then
     throwTacticEx `grind mvarId "goal contains metavariables"
 
-/--
-Throws an exception if target is not a proposition.
--/
-def _root_.Lean.MVarId.ensureProp (mvarId : MVarId) : MetaM Unit := do
-  let type ← mvarId.getType
-  unless (← isProp type) do
-    throwTacticEx `grind mvarId "goal is not a proposition"
-
 def _root_.Lean.MVarId.transformTarget (mvarId : MVarId) (f : Expr → MetaM Expr) : MetaM MVarId := mvarId.withContext do
   mvarId.checkNotAssigned `grind
   let tag ← mvarId.getTag

tests/lean/run/grind_exfalso.lean

@@ -0,0 +1,13 @@
+set_option grind.warning false
+
+example (x : Nat) (h : x < 0) : Nat → Nat := by
+  grind
+
+example : False → Nat := by
+  grind
+
+example : (x : Nat) → x < 0 → Nat := by
+  grind
+
+example : (x : Nat) → x < 3 → x > 4 → Nat := by
+  grind