From b8f2f28e0dc93dff65c5715bc041804d49560f59 Mon Sep 17 00:00:00 2001
From: Joachim Breitner <mail@joachim-breitner.de>
Date: Sun, 12 May 2024 22:39:14 +0200
Subject: [PATCH] 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        |  6 ++
 tests/lean/funind_reserved.lean              | 96 ++++++++++++++++++++
 tests/lean/funind_reserved.lean.expected.out |  6 ++
 3 files changed, 108 insertions(+)
 create mode 100644 tests/lean/funind_reserved.lean
 create mode 100644 tests/lean/funind_reserved.lean.expected.out

diff --git a/src/Lean/Elab/PreDefinition/Main.lean b/src/Lean/Elab/PreDefinition/Main.lean
index 200fa29f5c..d65b178aaf 100644
--- a/src/Lean/Elab/PreDefinition/Main.lean
+++ b/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
diff --git a/tests/lean/funind_reserved.lean b/tests/lean/funind_reserved.lean
new file mode 100644
index 0000000000..d822a60ef7
--- /dev/null
+++ b/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
diff --git a/tests/lean/funind_reserved.lean.expected.out b/tests/lean/funind_reserved.lean.expected.out
new file mode 100644
index 0000000000..36e3a5ca52
--- /dev/null
+++ b/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