fix: check that funind-reserved names are available (#4135)

I did not introduce `inductTheoremSuffix` etc, it seems more direct to
just spell out the suffix here. If we ever change it there are many
occurrences where they need to be changed anyways, so the definition
doesn't seem to save much work or add that much robustness.

src/Lean/Elab/PreDefinition/Main.lean

@@ -90,6 +90,11 @@ private def addAsAxioms (preDefs : Array PreDefinition) : TermElabM Unit := do
     applyAttributesOf #[preDef] AttributeApplicationTime.afterTypeChecking
     applyAttributesOf #[preDef] AttributeApplicationTime.afterCompilation
 
+def ensureFunIndReservedNamesAvailable (preDefs : Array PreDefinition) : MetaM Unit := do
+  preDefs.forM fun preDef =>
+    withRef preDef.ref <| ensureReservedNameAvailable preDef.declName "induct"
+  withRef preDefs[0]!.ref <| ensureReservedNameAvailable preDefs[0]!.declName "mutual_induct"
+
 def addPreDefinitions (preDefs : Array PreDefinition) : TermElabM Unit := withLCtx {} {} do
   for preDef in preDefs do
     trace[Elab.definition.body] "{preDef.declName} : {preDef.type} :=\n{preDef.value}"
@@ -121,6 +126,7 @@ def addPreDefinitions (preDefs : Array PreDefinition) : TermElabM Unit := withLC
       addAndCompilePartial preDefs
       preDefs.forM (·.termination.ensureNone "partial")
     else
+      ensureFunIndReservedNamesAvailable preDefs
       try
         let hasHints := preDefs.any fun preDef => preDef.termination.isNotNone
         if hasHints then

tests/lean/funind_reserved.lean

@@ -0,0 +1,96 @@
+
+-- Test that the reserved name availability is checked at function definition time
+
+namespace Nonrec
+
+def foo.induct := 1
+
+def foo : (n : Nat) → Nat -- no error (yet)
+  | 0 => 0
+  | n+1 => n
+
+end Nonrec
+
+namespace Structural
+
+def foo.induct := 1
+
+def foo : (n : Nat) → Nat -- error
+  | 0 => 0
+  | n+1 => foo n
+
+end Structural
+
+namespace WF
+
+def foo.induct := 1
+
+def foo : (n : Nat) → Nat -- error
+  | 0 => 0
+  | n+1 => foo n
+termination_by n => n
+
+end WF
+
+namespace Mutual1
+
+def foo.induct := 1
+
+mutual
+def foo : (n : Nat) → Nat -- error
+  | 0 => 0
+  | n+1 => bar n
+termination_by n => n
+
+def bar : (n : Nat) → Nat -- error
+  | 0 => 0
+  | n+1 => foo n
+termination_by n => n
+end
+
+end Mutual1
+
+namespace Mutual2
+
+def bar.induct := 1
+
+mutual
+def foo : (n : Nat) → Nat -- error
+  | 0 => 0
+  | n+1 => bar n
+termination_by n => n
+
+def bar : (n : Nat) → Nat
+  | 0 => 0
+  | n+1 => foo n
+termination_by n => n
+end
+
+end Mutual2
+
+namespace Mutual3
+
+def foo.mutual_induct := 1
+
+mutual
+def foo : (n : Nat) → Nat -- error
+  | 0 => 0
+  | n+1 => bar n
+termination_by n => n
+
+def bar : (n : Nat) → Nat
+  | 0 => 0
+  | n+1 => foo n
+termination_by n => n
+end
+
+end Mutual3
+
+namespace Nested
+
+def foo : (n : Nat) → Nat -- error
+  | 0 => 0
+  | n+1 => foo n
+  where induct := 1
+
+end Nested

tests/lean/funind_reserved.lean.expected.out

@@ -0,0 +1,6 @@
+funind_reserved.lean:18:4-18:7: error: failed to declare `Structural.foo` because `Structural.foo.induct` has already been declared
+funind_reserved.lean:28:4-28:7: error: failed to declare `WF.foo` because `WF.foo.induct` has already been declared
+funind_reserved.lean:40:4-40:7: error: failed to declare `Mutual1.foo` because `Mutual1.foo.induct` has already been declared
+funind_reserved.lean:63:4-63:7: error: failed to declare `Mutual2.bar` because `Mutual2.bar.induct` has already been declared
+funind_reserved.lean:76:4-76:7: error: failed to declare `Mutual3.foo` because `Mutual3.foo.mutual_induct` has already been declared
+funind_reserved.lean:91:4-91:7: error: failed to declare `Nested.foo` because `Nested.foo.induct` has already been declared