feat: interval_cases tactic (#1155)

Implements the `interval_cases` tactic from mathlib. This is a from scratch implementation, which should be a lot faster and give better goals than the original. I also tried to make a reasonable MetaM version of the tactic.

The original tactic was very generic and used typeclass inference to find most of the structure on the type. The new one is still somewhat type-generic but relies on meta-instances which implement the required functionality for supported types. Currently only `Nat` and `Int` are supported; `PNat` is more difficult because `norm_num` doesn't work on it.

Co-authored-by: Heather Macbeth <25316162+hrmacbeth@users.noreply.github.com>

Mathlib.lean

@@ -635,6 +635,7 @@ import Mathlib.Tactic.Have
 import Mathlib.Tactic.HelpCmd
 import Mathlib.Tactic.InferParam
 import Mathlib.Tactic.Inhabit
+import Mathlib.Tactic.IntervalCases
 import Mathlib.Tactic.IrreducibleDef
 import Mathlib.Tactic.LeftRight
 import Mathlib.Tactic.LibrarySearch

Mathlib/Control/Basic.lean

@@ -193,6 +193,10 @@ def tryM {α} (x : F α) : F Unit :=
   Functor.mapConst () x <|> pure ()
 #align mtry tryM
 
+/-- Attempts to perform the computation, and returns `none` if it doesn't succeed. -/
+def try? {α} (x : F α) : F (Option α) :=
+  some <$> x <|> pure none
+
 @[simp]
 theorem guard_true {h : Decidable True} : @guard F _ True h = pure () := by simp [guard, if_pos]
 #align guard_true guard_true

Mathlib/Mathport/Syntax.lean

@@ -31,6 +31,7 @@ import Mathlib.Tactic.Find
 import Mathlib.Tactic.GeneralizeProofs
 import Mathlib.Tactic.GuardHypNums
 import Mathlib.Tactic.InferParam
+import Mathlib.Tactic.IntervalCases
 import Mathlib.Tactic.Inhabit
 import Mathlib.Tactic.IrreducibleDef
 import Mathlib.Tactic.LeftRight
@@ -230,9 +231,6 @@ syntax mono.side := &"left" <|> &"right" <|> &"both"
 /- B -/ syntax (name := acMono) "ac_mono" ("*" <|> ("^" num))?
   (config)? ((" : " term) <|> (" := " term))? : tactic
 
-/- M -/ syntax (name := intervalCases) "interval_cases" (ppSpace (colGt term))?
-  (" using " term ", " term)? (" with " ident)? : tactic
-
 /- M -/ syntax (name := reassoc) "reassoc" (ppSpace (colGt ident))* : tactic
 /- M -/ syntax (name := reassoc!) "reassoc!" (ppSpace (colGt ident))* : tactic
 /- M -/ syntax (name := deriveReassocProof) "derive_reassoc_proof" : tactic

Mathlib/Tactic/FinCases.lean

@@ -43,35 +43,30 @@ This is useful for hypotheses of the form `h : a ∈ [l₁, l₂, ...]`,
 which will be transformed into a sequence of goals with hypotheses `h : a = l₁`, `h : a = l₂`,
 and so on.
 -/
-partial def unfoldCases (h : FVarId) (g : MVarId) : MetaM (List MVarId) := do
+partial def unfoldCases (g : MVarId) (h : FVarId) : MetaM (List MVarId) := do
   let gs ← g.cases h
   try
     let #[g₁, g₂] := gs | throwError "unexpected number of cases"
-    let gs ← unfoldCases g₂.fields[2]!.fvarId! g₂.mvarId
+    let gs ← unfoldCases g₂.mvarId g₂.fields[2]!.fvarId!
     return g₁.mvarId :: gs
   catch _ => return []
 
 /-- Implementation of the `fin_cases` tactic. -/
-partial def finCasesAt (hyp : FVarId) : TacticM Unit := do
-  withMainContext do
-    let lDecl ←
-      match (← getLCtx).find? hyp with
-      | none => throwError m!"hypothesis not found"
-      | some lDecl => pure lDecl
-    match ← getMemType lDecl.type with
-    | some _ => liftMetaTactic (unfoldCases hyp)
-    | none =>
-      -- Deal with `x : A`, where `[Fintype A]` is available:
-      let inst ← synthInstance (← mkAppM ``Fintype #[lDecl.type])
-      let elems ← mkAppOptM ``Fintype.elems #[lDecl.type, inst]
-      let t ← mkAppM ``Membership.mem #[lDecl.toExpr, elems]
-      let v ← mkAppOptM ``Fintype.complete #[lDecl.type, inst, lDecl.toExpr]
-
-      let hyp ← liftMetaTacticAux fun mvarId ↦ do
-        let (fvar, mvarId) ← (← mvarId.assert `this t v).intro1P
-        pure (fvar, [mvarId])
-
-      finCasesAt hyp
+partial def finCasesAt (g : MVarId) (hyp : FVarId) : MetaM (List MVarId) := g.withContext do
+  let lDecl ←
+    match (← getLCtx).find? hyp with
+    | none => throwError m!"hypothesis not found"
+    | some lDecl => pure lDecl
+  match ← getMemType lDecl.type with
+  | some _ => unfoldCases g hyp
+  | none =>
+    -- Deal with `x : A`, where `[Fintype A]` is available:
+    let inst ← synthInstance (← mkAppM ``Fintype #[lDecl.type])
+    let elems ← mkAppOptM ``Fintype.elems #[lDecl.type, inst]
+    let t ← mkAppM ``Membership.mem #[lDecl.toExpr, elems]
+    let v ← mkAppOptM ``Fintype.complete #[lDecl.type, inst, lDecl.toExpr]
+    let (fvar, g) ← (← g.assert `this t v).intro1P
+    finCasesAt g fvar
 
 /--
 `fin_cases h` performs case analysis on a hypothesis of the form
@@ -128,7 +123,6 @@ produces three goals with hypotheses
    rather than `tail.tail.tail.head`? -/
 
 @[tactic finCases] elab_rules : tactic
-  | `(tactic| fin_cases $[$hyps:ident],*) => withMainContext do
-  focus
+  | `(tactic| fin_cases $[$hyps:ident],*) => withMainContext <| focus do
     for h in hyps do
-      allGoals (finCasesAt (← getFVarId h))
+      allGoals <| liftMetaTactic (finCasesAt · (← getFVarId h))