fix: make casesm and constructorm fail if no matches are found (#1552)

The main thing I want to fix here is that `tauto` on master currently never fails *quickly*. E.g. this takes many seconds to fail:
```lean
example (p : Prop) : p := by tauto
```
The reason is that the final step of `tauto` repeats until it sees a failure, and `constructorMatching` never fails, so we end up going until a timeout is hit.
https://github.com/leanprover-community/mathlib4/blob/e78a2694fd2c5b00c16b4139f4a45faa17d2718d/Mathlib/Tactic/Tauto.lean#L150-L153

When I originally wrote this code, I had expected that `constructorMatching` would fail when it finds no match, similar to how the mathlib3 tactic `constructor_matching` fails when it finds no match.

To fix the problem, this PR adds a `throwOnNoMatch` optional parameter to the `casesMatching` and `constructorMatching` functions, with default value set to `!recursive`. This means that the `casesm` and `constructorm` tactics will fail on no match, but the `casesm*` and `constructorm*` tactics will succeed on no match. That corresponds exactly to how the analogous tactics work in mathlib3.

According to some [zulip discussion](https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/casesm.20.2F.20constructorm.20on.20no.20match.3A.20error.20or.20not.3F), other folks agree that the mathlib3 behavior was better.

This PR also explicitly sets `(throwOnNoMatch := false)` on the other calls to `constructorMatching` and `casesMatching` in `tautoCore`, because in those cases we don't want a failure. Technically, to exactly match the mathlib3 behavior there, we should be setting `(recursive := true)`, as I do in #1507, but if I do that here without the other performance fixes in that PR, then the proof of `Preorder.toCircularPreorder` gets pushed over the default `maxHeartbeats` timeout.

Mathlib/Control/Basic.lean

@@ -219,7 +219,8 @@ instance : Monad (Sum.{v, u} e) where
   pure := @Sum.inr e
   bind := @Sum.bind e
 
-instance : LawfulFunctor (Sum.{v, u} e) := by refine' { .. } <;> intros <;> casesm Sum _ _ <;> rfl
+instance : LawfulFunctor (Sum.{v, u} e) := by
+  refine' { .. } <;> intros <;> (try casesm Sum _ _) <;> rfl
 
 instance : LawfulMonad (Sum.{v, u} e) where
   seqRight_eq := by

Mathlib/Tactic/CasesM.lean

@@ -19,9 +19,17 @@ Core tactic for `casesm` and `cases_type`. Calls `cases` on all fvars in `g` for
 `matcher ldecl.type` returns true.
 * `recursive`: if true, it calls itself repeatedly on the resulting subgoals
 * `allowSplit`: if false, it will skip any hypotheses where `cases` returns more than one subgoal.
+* `throwOnNoMatch`: if true, then throws an error if no match is found
 -/
 partial def casesMatching (g : MVarId) (matcher : Expr → MetaM Bool)
-    (recursive := false) (allowSplit := true) : MetaM (List MVarId) := return (← go g).toList where
+    (recursive := false) (allowSplit := true) (throwOnNoMatch := !recursive) :
+    MetaM (List MVarId) := do
+  let result := (← go g).toList
+  if throwOnNoMatch && result == [g] then
+    throwError "no match"
+  else
+    return result
+  where
   /-- Auxiliary for `casesMatching`. Accumulates generated subgoals in `acc`. -/
   go (g : MVarId) (acc : Array MVarId := #[]) : MetaM (Array MVarId) :=
     g.withContext do
@@ -107,14 +115,21 @@ elab (name := casesType!) "cases_type!" recursive:"*"? ppSpace heads:(colGt iden
 Core tactic for `constructorm`. Calls `constructor` on all subgoals for which
 `matcher ldecl.type` returns true.
 * `recursive`: if true, it calls itself repeatedly on the resulting subgoals
+* `throwOnNoMatch`: if true, throws an error if no match is found
 -/
 partial def constructorMatching (g : MVarId) (matcher : Expr → MetaM Bool)
-    (recursive := false) : MetaM (List MVarId) :=
-  if recursive then
-    return (← go g).toList
+    (recursive := false) (throwOnNoMatch := !recursive): MetaM (List MVarId) := do
+  let result ←
+    (if recursive then (do
+      let result ← go g
+      pure result.toList)
+     else
+      (g.withContext do
+          if ← matcher (← g.getType) then g.constructor else pure [g]))
+  if throwOnNoMatch && [g] == result then
+    throwError "no match"
   else
-    g.withContext do
-      if ← matcher (← g.getType) then g.constructor else pure [g]
+    return result
 where
   /-- Auxiliary for `constructorMatching`. Accumulates generated subgoals in `acc`. -/
   go (g : MVarId) (acc : Array MVarId := #[]) : MetaM (Array MVarId) :=

Mathlib/Tactic/Tauto.lean

@@ -124,11 +124,11 @@ def tautoCore : TacticM Unit := do
     allGoals (
       liftMetaTactic (fun m => do pure [(← m.intros!).2]) <;>
       distribNot <;>
-      liftMetaTactic (casesMatching · casesMatcher) <;>
+      liftMetaTactic (casesMatching · casesMatcher (throwOnNoMatch := false)) <;>
       (do _ ← tryTactic (evalTactic (← `(tactic| contradiction)))) <;>
       (do _ ← tryTactic (evalTactic (←`(tactic| refine or_iff_not_imp_left.mpr ?_)))) <;>
       liftMetaTactic (fun m => do pure [(← m.intros!).2]) <;>
-      liftMetaTactic (constructorMatching · coreConstructorMatcher) <;>
+      liftMetaTactic (constructorMatching · coreConstructorMatcher (throwOnNoMatch := false)) <;>
       do _ ← tryTactic (evalTactic (← `(tactic| assumption))))
     let gs' ← getUnsolvedGoals
     if gs == gs' then failure -- no progress

test/casesm.lean

@@ -27,7 +27,7 @@ example (h : a ∧ b ∨ c ∨ d) : True := by
   · clear ‹c ∨ d›; trivial
 
 example (h : a ∧ b ∨ c ∨ d) : True := by
-  cases_type And
+  cases_type* And -- no match expected
   · clear ‹a ∧ b ∨ c ∨ d›; trivial
 
 example (h : a ∧ b ∨ c ∨ d) : True := by
@@ -42,7 +42,7 @@ example (h : a ∧ b ∨ c ∨ d) : True := by
   · clear ‹d›; trivial
 
 example (h : a ∧ b ∨ c ∨ d) : True := by
-  cases_type! And Or
+  cases_type!* And Or -- no match expected
   · clear ‹a ∧ b ∨ c ∨ d›; trivial
 
 example (h : a ∧ b ∧ (c ∨ d)) : True := by
@@ -72,7 +72,7 @@ example (_ : Test n) (h2 : Test (m + 1)) : True := by
   · clear ‹False›; clear ‹False›; trivial
 
 example : True ∧ True ∧ True := by
-  constructorm True, _∨_
+  constructorm* True, _∨_ -- no match expected
   guard_target = True ∧ True ∧ True
   constructorm _∧_
   · guard_target = True; constructorm True