feat: subsections for obligations_by

Author: Sebastian Graf

src/Lean/Elab/Obligations.lean

@@ -24,7 +24,10 @@ def mkObligations {m} [Monad m] [MonadError m] (stx : TSyntax ``Parser.Term.obli
     return { ref := stx, tactic := ⟨.missing⟩ }
   if let some ob := stx.raw.getOptional? then
     match ob with
-    | `(Parser.Term.obligationsBy| obligations_by $tactic) => do
+    | `(Parser.Term.obligationsBy| obligations_by $tactic) =>
       return { ref := stx, tactic }
-    | _ => throwErrorAt stx s!"Unexpected obligationsBy syntax: {stx} of kind {stx.raw.getKind}"
+    | `(Parser.Term.obligationsBy| obligations_by) =>
+      return { ref := stx, tactic := ⟨.missing⟩ }
+    | `(Parser.Term.obligationsBy| $_) =>
+      throwErrorAt stx "`obligations_by` does not currently support any named sub-sections `| sectionName => ...`"
   else return .none

src/Lean/Parser/Term.lean

@@ -810,12 +810,19 @@ Termination hints are `termination_by` and `decreasing_by`, in that order.
 end Termination
 namespace Term
 
+/--
+A named subsection of `obligations_by`. In the future, sections such as `decreasing_by` might become
+syntactic sugar for an `obligations_by` subsection `| decreasing => ...`.
+-/
+def obligationsBySubSection := leading_parser
+  ppLine >> "| " >> ident >> darrow >> Tactic.tacticSeq
+
 /--
 `obligations_by` opens a tactic block to discharge proof obligations introduced by
 use of `?hole`s in the definition body.
 -/
 @[builtin_doc] def obligationsBy := leading_parser
-  ppDedent ppLine >> "obligations_by " >> Tactic.tacticSeqIndentGt
+  ppDedent ppLine >> withPosition ("obligations_by " >> optional Tactic.tacticSeqIndentGt >> manyIndent obligationsBySubSection)
 
 /-- `letRecDecl` matches the body of a let-rec declaration: a doc comment, attributes, and then
 a let declaration without the `let` keyword, such as `/-- foo -/ @[simp] bar := 1`. -/

tests/lean/obligations.lean

@@ -62,3 +62,13 @@ def obligation_in_rec_let_and_def (i : Nat) (xs : Array Nat) (h : i < xs.size) :
   f i + xs[i]'?hole₂
 obligations_by
   case hole₂ => exact h
+
+/--
+error: `obligations_by` does not currently support any named sub-sections `| sectionName => ...`
+-/
+#guard_msgs in
+def obligation_decreasing_does_not_exist (i : Nat) (xs : Array Nat) (h : i < xs.size) : Nat :=
+  xs[i]'?hole
+obligations_by
+  case hole => exact h
+| decreasing => skip