From c0fbcc76c43b196c366eb29d43d2d26887a55cb4 Mon Sep 17 00:00:00 2001
From: Joachim Breitner <mail@joachim-breitner.de>
Date: Tue, 16 Apr 2024 13:59:40 +0200
Subject: [PATCH] feat: FunInd: reserve name `.mutual_induct` (#3898)

---
 src/Lean/Meta/Tactic/FunInd.lean | 15 +++++---
 tests/lean/run/funind_tests.lean | 62 ++++++++++++++++++++++++++++++++
 2 files changed, 73 insertions(+), 4 deletions(-)

diff --git a/src/Lean/Meta/Tactic/FunInd.lean b/src/Lean/Meta/Tactic/FunInd.lean
index 3a94bcf9bb..0c6c431618 100644
--- a/src/Lean/Meta/Tactic/FunInd.lean
+++ b/src/Lean/Meta/Tactic/FunInd.lean
@@ -943,10 +943,17 @@ def deriveInduction (name : Name) : MetaM Unit := do
 
 def isFunInductName (env : Environment) (name : Name) : Bool := Id.run do
   let .str p s := name | return false
-  unless s = "induct" do return false
-  if (WF.eqnInfoExt.find? env p).isSome then return true
-  if (Structural.eqnInfoExt.find? env p).isSome then return true
-  return false
+  match s with
+  | "induct" =>
+    if (WF.eqnInfoExt.find? env p).isSome then return true
+    if (Structural.eqnInfoExt.find? env p).isSome then return true
+    return false
+  | "mutual_induct" =>
+    if let some eqnInfo := WF.eqnInfoExt.find? env p then
+      if h : eqnInfo.declNames.size > 1 then
+        return eqnInfo.declNames[0] = p
+    return false
+  | _ => return false
 
 builtin_initialize
   registerReservedNamePredicate isFunInductName
diff --git a/tests/lean/run/funind_tests.lean b/tests/lean/run/funind_tests.lean
index 92f8e29a58..062e42c593 100644
--- a/tests/lean/run/funind_tests.lean
+++ b/tests/lean/run/funind_tests.lean
@@ -1,3 +1,7 @@
+import Lean.Elab.Command
+import Lean.Elab.PreDefinition.WF.Eqns
+import Lean.Meta.Tactic.FunInd
+
 namespace Unary
 
 def ackermann : (Nat × Nat) → Nat
@@ -739,3 +743,61 @@ info: PreserveParams.foo.induct (a : Nat) (motive : Nat → Prop) (case1 : motiv
 
 
 end PreserveParams
+
+namespace Mutual_Induct
+
+/-! Tests that `mutual_induct` is properly reserved. -/
+
+mutual
+def even : Nat → Bool
+  | 0 => true
+  | n+1 => odd n
+termination_by n => n
+def odd : Nat → Bool
+  | 0 => false
+  | n+1 => even n
+termination_by n => n
+end
+
+-- The following tests uses that guard_msgs reverts the environment,
+-- so they all test that the mutual induct is really generated by these commands
+
+/--
+info: Mutual_Induct.even.mutual_induct (motive1 motive2 : Nat → Prop) (case1 : motive1 0)
+  (case2 : ∀ (n : Nat), motive2 n → motive1 n.succ) (case3 : motive2 0)
+  (case4 : ∀ (n : Nat), motive1 n → motive2 n.succ) : (∀ (a : Nat), motive1 a) ∧ ∀ (a : Nat), motive2 a
+-/
+#guard_msgs in
+#check even.mutual_induct
+
+-- The .mutual_induct only exists on the first declaration:
+
+/-- error: unknown constant 'Mutual_Induct.odd.mutual_induct' -/
+#guard_msgs in
+#check odd.mutual_induct
+
+/-- info: false -/
+#guard_msgs in
+open Lean Lean.Elab in
+run_meta
+  logInfo m!"{Lean.Tactic.FunInd.isFunInductName (← getEnv) `Mutual_Induct.odd.mutual_induct}"
+
+def nonmutual : Nat → Bool
+  | 0 => true
+  | n+1 => nonmutual n
+
+/-- error: unknown constant 'Mutual_Induct.nonmutual.mutual_induct' -/
+#guard_msgs in
+#check nonmutual.mutual_induct
+
+/--
+error: invalid field notation, type is not of the form (C ...) where C is a constant
+  id
+has type
+  ?_ → ?_
+-/
+#guard_msgs in
+set_option pp.mvars false in
+#check id.mutual_induct
+
+end Mutual_Induct