feat: use reserved name infrastructure for functional induction (#3776)

no need to enter `derive_functional_induction` anymore.

(Will remove the support for `derive_functional_induction` after the
next stage0 update, since we are already using it in Init.)

RELEASES.md

@@ -21,16 +21,16 @@ v4.8.0 (development in progress)
 
 * Importing two different files containing proofs of the same theorem is no longer considered an error. This feature is particularly useful for theorems that are automatically generated on demand (e.g., equational theorems).
 
-* New command `derive_functional_induction`:
+* Funcitonal induction principles.
 
-  Derived from the definition of a (possibly mutually) recursive function, a **functional induction
-  principle** is created that is tailored to proofs about that function. For example from:
+  Derived from the definition of a (possibly mutually) recursive function, a **functional induction principle** is created that is tailored to proofs about that function.
+
+  For example from:
   ```
   def ackermann : Nat → Nat → Nat
     | 0, m => m + 1
     | n+1, 0 => ackermann n 1
     | n+1, m+1 => ackermann n (ackermann (n + 1) m)
-  derive_functional_induction ackermann
   ```
   we get
   ```

src/Lean/Meta/Tactic/FunInd.lean

@@ -13,6 +13,7 @@ import Lean.Meta.Tactic.Subst
 import Lean.Meta.Injective -- for elimOptParam
 import Lean.Meta.ArgsPacker
 import Lean.Elab.PreDefinition.WF.Eqns
+import Lean.Elab.PreDefinition.Structural.Eqns
 import Lean.Elab.Command
 import Lean.Meta.Tactic.ElimInfo
 
@@ -947,4 +948,22 @@ def elabDeriveInduction : Command.CommandElab := fun stx => Command.runTermElabM
   let name ← realizeGlobalConstNoOverloadWithInfo ident
   deriveInduction name
 
+
+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
+
+builtin_initialize
+  registerReservedNamePredicate isFunInductName
+
+  registerReservedNameAction fun name => do
+    if isFunInductName (← getEnv) name then
+      let .str p _ := name | return false
+      MetaM.run' <| deriveInduction p
+      return true
+    return false
+
 end Lean.Tactic.FunInd

tests/lean/funind_errors.lean

@@ -0,0 +1,45 @@
+-- Some of these tests made more sense when we had a
+-- derive_functional_induction command.
+
+#check doesNotExist.induct
+
+def takeWhile (p : α → Bool) (as : Array α) : Array α :=
+  foo 0 #[]
+where
+  foo (i : Nat) (r : Array α) : Array α :=
+    if h : i < as.size then
+      let a := as.get ⟨i, h⟩
+      if p a then
+        foo (i+1) (r.push a)
+      else
+        r
+    else
+      r
+  termination_by as.size - i
+
+-- Checks the error message when the users tries to access the induct rule for the wrong function
+-- (before we used reserved names for this feature we did give a more helpful error message here)
+#check takeWhile.induct
+
+#check takeWhile.foo.induct
+
+
+-- this tests the error we get when trying to access the induct rules for
+-- a function that recurses over an inductive *predicate* (not yet supported)
+
+inductive Even : Nat → Prop where
+| zero : Even 0
+| plus2 : Even n → Even (n + 2)
+
+def idEven : Even n → Even n
+| .zero => .zero
+| .plus2 p => .plus2 (idEven p)
+
+#check idEven.induct
+
+-- this tests the error we get when trying to access the induct rules for
+-- a function that recurses over `Acc`
+
+def idAcc : Acc p x → Acc p x
+  | Acc.intro x f => Acc.intro x (fun y h => idAcc (f y h))
+#check idAcc.induct

tests/lean/funind_errors.lean.expected.out

@@ -0,0 +1,23 @@
+funind_errors.lean:4:7-4:26: error: unknown identifier 'doesNotExist.induct'
+funind_errors.lean:22:7-22:23: error: invalid field notation, type is not of the form (C ...) where C is a constant
+  takeWhile
+has type
+  (?m → Bool) → Array ?m → Array ?m
+takeWhile.foo.induct.{u_1} {α : Type u_1} (p : α → Bool) (as : Array α) (motive : Nat → Array α → Prop)
+  (case1 :
+    ∀ (i : Nat) (r : Array α) (h : i < as.size),
+      let a := as.get ⟨i, h⟩;
+      p a = true → motive (i + 1) (r.push a) → motive i r)
+  (case2 :
+    ∀ (i : Nat) (r : Array α) (h : i < as.size),
+      let a := as.get ⟨i, h⟩;
+      ¬p a = true → motive i r)
+  (case3 : ∀ (i : Nat) (r : Array α), ¬i < as.size → motive i r) (i : Nat) (r : Array α) : motive i r
+funind_errors.lean:38:7-38:20: error: invalid field notation, type is not of the form (C ...) where C is a constant
+  idEven
+has type
+  Even ?m → Even ?m
+funind_errors.lean:45:7-45:19: error: invalid field notation, type is not of the form (C ...) where C is a constant
+  idAcc
+has type
+  Acc ?m ?m → Acc ?m ?m

tests/lean/run/funind_demo.lean

@@ -4,7 +4,6 @@ def ackermann : Nat → Nat → Nat
   | 0, m => m + 1
   | n+1, 0 => ackermann n 1
   | n+1, m+1 => ackermann n (ackermann (n + 1) m)
-derive_functional_induction ackermann
 
 /--
 info: ackermann.induct (motive : Nat → Nat → Prop) (case1 : ∀ (m : Nat), motive 0 m)
@@ -23,8 +22,6 @@ def List.attach {α} : (l : List α) → List {x // x ∈ l}
 inductive Tree | node : List Tree → Tree
 def Tree.rev : Tree → Tree | node ts => .node (ts.attach.map (fun ⟨t, _ht⟩ => t.rev) |>.reverse)
 
-derive_functional_induction Tree.rev
-
 /--
 info: Tree.rev.induct (motive : Tree → Prop)
   (case1 : ∀ (ts : List Tree), (∀ (t : Tree), t ∈ ts → motive t) → motive (Tree.node ts)) : ∀ (a : Tree), motive a

tests/lean/run/funind_expr.lean

@@ -47,8 +47,6 @@ theorem Expr.typeCheck_correct (h₁ : HasType e ty) (h₂ : e.typeCheck ≠ .un
   | found ty' h' => intro; have := HasType.det h₁ h'; subst this; rfl
   | unknown => intros; contradiction
 
-derive_functional_induction Expr.typeCheck
-
 /--
 info: Expr.typeCheck.induct (motive : Expr → Prop) (case1 : ∀ (a : Nat), motive (Expr.nat a))
   (case2 : ∀ (a : Bool), motive (Expr.bool a))

tests/lean/run/funind_fewer_levels.lean

@@ -9,16 +9,15 @@ def foo.{u} : Nat → PUnit.{u}
 | 0 => .unit
 | n+1 => foo n
 
-derive_functional_induction foo
 /--
 info: Structural.foo.induct (motive : Nat → Prop) (case1 : motive 0) (case2 : ∀ (n : Nat), motive n → motive n.succ) :
   ∀ (a : Nat), motive a
 -/
 #guard_msgs in
-#check foo.induct
+#check Structural.foo.induct
 
 example : foo n = .unit := by
-  induction n using foo.induct with
+  induction n using Structural.foo.induct with
   | case1 => unfold foo; rfl
   | case2 n ih => unfold foo; exact ih
 
@@ -30,16 +29,15 @@ def foo.{u,v} {α : Type v} : List α  → PUnit.{u}
 | _ :: xs => foo xs
 termination_by xs => xs
 
-derive_functional_induction foo
 /--
 info: WellFounded.foo.induct.{v} {α : Type v} (motive : List α → Prop) (case1 : motive [])
   (case2 : ∀ (head : α) (xs : List α), motive xs → motive (head :: xs)) : ∀ (a : List α), motive a
 -/
 #guard_msgs in
-#check foo.induct
+#check WellFounded.foo.induct
 
 example : foo xs = .unit := by
-  induction xs using foo.induct with
+  induction xs using WellFounded.foo.induct with
   | case1 => unfold foo; rfl
   | case2 _ xs ih => unfold foo; exact ih
 
@@ -58,16 +56,15 @@ def bar.{u} : Nat → PUnit.{u}
 termination_by n => n
 end
 
-derive_functional_induction foo
 /--
 info: Mutual.foo.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
 -/
 #guard_msgs in
-#check foo.induct
+#check Mutual.foo.induct
 
 example : foo n = .unit := by
-  induction n using foo.induct (motive2 := fun n => bar n = .unit) with
+  induction n using Mutual.foo.induct (motive2 := fun n => bar n = .unit) with
   | case1 => unfold foo; rfl
   | case2 n ih => unfold foo; exact ih
   | case3 => unfold bar; rfl

tests/lean/run/funind_mutual_dep.lean

@@ -45,8 +45,6 @@ def Finite.functions (t : Finite) (results : List α) : List (t.asType → α) :
         fun (f : t1.asType → t2.asType) => more (f arg) f
 end
 
-derive_functional_induction Finite.functions
-
 /--
 info: Finite.functions.induct (motive1 : Finite → Prop) (motive2 : (α : Type) → Finite → List α → Prop)
   (case1 : motive1 Finite.unit) (case2 : motive1 Finite.bool)

tests/lean/run/funind_proof.lean

@@ -24,7 +24,6 @@ mutual
     | c :: cs => replaceConst a b c :: replaceConstLst a b cs
 end
 
-derive_functional_induction replaceConst
 
 /--
 info: Term.replaceConst.induct (a b : String) (motive1 : Term → Prop) (motive2 : List Term → Prop)
@@ -34,10 +33,10 @@ info: Term.replaceConst.induct (a b : String) (motive1 : Term → Prop) (motive2
   (case5 : ∀ (c : Term) (cs : List Term), motive1 c → motive2 cs → motive2 (c :: cs)) : ∀ (a : Term), motive1 a
 -/
 #guard_msgs in
-#check replaceConst.induct
+#check Term.replaceConst.induct
 
 theorem numConsts_replaceConst (a b : String) (e : Term) : numConsts (replaceConst a b e) = numConsts e := by
-  apply replaceConst.induct
+  apply Term.replaceConst.induct
     (motive1 := fun e => numConsts (replaceConst a b e) = numConsts e)
     (motive2 := fun es =>  numConstsLst (replaceConstLst a b es) = numConstsLst es)
   case case1 => intro c h; guard_hyp h :ₛ (a == c) = true; simp [replaceConst, numConsts, *]

tests/lean/run/funind_structural.lean

@@ -1,4 +1,5 @@
 import Lean.Elab.Command
+import Lean.Elab.PreDefinition.Structural.Eqns
 
 /-!
 This module tests functional induction principles on *structurally* recursive functions.
@@ -8,7 +9,6 @@ def fib : Nat → Nat
   | 0 | 1 => 0
   | n+2 => fib n + fib (n+1)
 
-derive_functional_induction fib
 /--
 info: fib.induct (motive : Nat → Prop) (case1 : motive 0) (case2 : motive 1)
   (case3 : ∀ (n : Nat), motive n → motive (n + 1) → motive n.succ.succ) : ∀ (a : Nat), motive a
@@ -21,7 +21,6 @@ def binary : Nat → Nat → Nat
   | 0, acc | 1, acc => 1 + acc
   | n+2, acc => binary n (binary (n+1) acc)
 
-derive_functional_induction binary
 /--
 info: binary.induct (motive : Nat → Nat → Prop) (case1 : ∀ (acc : Nat), motive 0 acc) (case2 : ∀ (acc : Nat), motive 1 acc)
   (case3 : ∀ (n acc : Nat), motive (n + 1) acc → motive n (binary (n + 1) acc) → motive n.succ.succ acc) :
@@ -36,7 +35,6 @@ def binary' : Bool → Nat → Bool
   | acc, 0 | acc , 1 => not acc
   | acc, n+2 => binary' (binary' acc (n+1)) n
 
-derive_functional_induction binary'
 /--
 info: binary'.induct (motive : Bool → Nat → Prop) (case1 : ∀ (acc : Bool), motive acc 0)
   (case2 : ∀ (acc : Bool), motive acc 1)
@@ -51,7 +49,6 @@ def zip {α β} : List α → List β → List (α × β)
   | _, [] => []
   | x::xs, y::ys => (x, y) :: zip xs ys
 
-derive_functional_induction zip
 /--
 info: zip.induct.{u_1, u_2} {α : Type u_1} {β : Type u_2} (motive : List α → List β → Prop)
   (case1 : ∀ (x : List β), motive [] x) (case2 : ∀ (x : List α), (x = [] → False) → motive x [])
@@ -88,7 +85,6 @@ def Finn.min (x : Bool) {n : Nat} (m : Nat) : Finn n → (f : Finn n) → Finn n
   | _, fzero => fzero
   | fsucc i, fsucc j => fsucc (Finn.min (not x) (m + 1) i j)
 
-derive_functional_induction Finn.min
 /--
 info: Finn.min.induct (motive : Bool → {n : Nat} → Nat → Finn n → Finn n → Prop)
   (case1 : ∀ (x : Bool) (m n : Nat) (x_1 : Finn n), motive x m Finn.fzero x_1)
@@ -100,29 +96,6 @@ info: Finn.min.induct (motive : Bool → {n : Nat} → Nat → Finn n → Finn n
 #check Finn.min.induct
 
 
-inductive Even : Nat → Prop where
-| zero : Even 0
-| plus2 : Even n → Even (n + 2)
-
-def idEven : Even n → Even n
-| .zero => .zero
-| .plus2 p => .plus2 (idEven p)
-/--
-error: Function idEven is defined in a way not supported by functional induction, for example by recursion over an inductive predicate.
--/
-#guard_msgs in
-derive_functional_induction idEven
-
-
--- Acc.brecOn is not recognized by isBRecOnRecursor:
--- run_meta Lean.logInfo m!"{Lean.isBRecOnRecursor (← Lean.getEnv) ``Acc.brecOn}"
-def idAcc : Acc p x → Acc p x
-  | Acc.intro x f => Acc.intro x (fun y h => idAcc (f y h))
-/--
-error: Function idAcc is defined in a way not supported by functional induction, for example by recursion over an inductive predicate.
--/
-#guard_msgs in
-derive_functional_induction idAcc
 
 namespace TreeExample
 
@@ -141,8 +114,6 @@ def Tree.insert (t : Tree β) (k : Nat) (v : β) : Tree β :=
     else
       node left k v right
 
-derive_functional_induction Tree.insert
-
 /--
 info: TreeExample.Tree.insert.induct.{u_1} {β : Type u_1} (motive : Tree β → Nat → β → Prop)
   (case1 : ∀ (k : Nat) (v : β), motive Tree.leaf k v)
@@ -158,11 +129,11 @@ info: TreeExample.Tree.insert.induct.{u_1} {β : Type u_1} (motive : Tree β →
   (t : Tree β) (k : Nat) (v : β) : motive t k v
 -/
 #guard_msgs in
-#check Tree.insert.induct
+#check TreeExample.Tree.insert.induct
 
 end TreeExample
 
-namespace Term
+namespace TermDenote
 
 inductive HList {α : Type v} (β : α → Type u) : List α → Type (max u v)
   | nil  : HList β []
@@ -204,10 +175,8 @@ def Term.denote : Term ctx ty → HList Ty.denote ctx → ty.denote
   | .lam b,     env => fun x => b.denote (.cons x env)
   | .let a b,   env => b.denote (.cons (a.denote env) env)
 
-derive_functional_induction Term.denote
-
 /--
-info: Term.Term.denote.induct (motive : {ctx : List Ty} → {ty : Ty} → Term ctx ty → HList Ty.denote ctx → Prop)
+info: TermDenote.Term.denote.induct (motive : {ctx : List Ty} → {ty : Ty} → Term ctx ty → HList Ty.denote ctx → Prop)
   (case1 : ∀ (a : List Ty) (ty : Ty) (h : Member ty a) (env : HList Ty.denote a), motive (Term.var h) env)
   (case2 : ∀ (a : List Ty) (n : Nat) (x : HList Ty.denote a), motive (Term.const n) x)
   (case3 :
@@ -225,6 +194,6 @@ info: Term.Term.denote.induct (motive : {ctx : List Ty} → {ty : Ty} → Term c
   {ctx : List Ty} {ty : Ty} : ∀ (a : Term ctx ty) (a_1 : HList Ty.denote ctx), motive a a_1
 -/
 #guard_msgs in
-#check Term.denote.induct
+#check TermDenote.Term.denote.induct
 
-end Term
+end TermDenote

tests/lean/run/funind_tests.lean

@@ -6,8 +6,6 @@ def ackermann : (Nat × Nat) → Nat
   | (n+1, m+1) => ackermann (n, ackermann (n + 1, m))
 termination_by p => p
 
-derive_functional_induction ackermann
-
 /--
 info: Unary.ackermann.induct (motive : Nat × Nat → Prop) (case1 : ∀ (m : Nat), motive (0, m))
   (case2 : ∀ (n : Nat), motive (n, 1) → motive (n.succ, 0))
@@ -15,7 +13,7 @@ info: Unary.ackermann.induct (motive : Nat × Nat → Prop) (case1 : ∀ (m : Na
   ∀ (a : Nat × Nat), motive a
 -/
 #guard_msgs in
-#check ackermann.induct
+#check Unary.ackermann.induct
 
 end Unary
 
@@ -26,7 +24,6 @@ def ackermann : Nat → Nat → Nat
   | n+1, 0 => ackermann n 1
   | n+1, m+1 => ackermann n (ackermann (n + 1) m)
 termination_by n m => (n, m)
-derive_functional_induction ackermann
 
 /--
 info: Binary.ackermann.induct (motive : Nat → Nat → Prop) (case1 : ∀ (m : Nat), motive 0 m)
@@ -35,7 +32,7 @@ info: Binary.ackermann.induct (motive : Nat → Nat → Prop) (case1 : ∀ (m :
   ∀ (a a_1 : Nat), motive a a_1
 -/
 #guard_msgs in
-#check ackermann.induct
+#check Binary.ackermann.induct
 
 end Binary
 
@@ -45,7 +42,6 @@ opaque _root_.List.attach : {α : Type u} → (l : List α) → List { x // x
 inductive Tree | node : List Tree → Tree
 def Tree.rev : Tree → Tree
   | node ts => .node (ts.attach.map (fun ⟨t, _ht⟩ => t.rev) |>.reverse)
-derive_functional_induction Tree.rev
 
 /--
 info: Tree.rev.induct (motive : Tree → Prop)
@@ -61,7 +57,6 @@ def fib : Nat → Nat
   | n+2 => fib n + fib (n+1)
 termination_by n => n
 
-derive_functional_induction fib
 /--
 info: fib.induct (motive : Nat → Prop) (case1 : motive 0) (case2 : motive 1)
   (case3 : ∀ (n : Nat), motive n → motive (n + 1) → motive n.succ.succ) : ∀ (a : Nat), motive a
@@ -76,7 +71,6 @@ def have_tailrec : Nat → Nat
     have h2 : n < n+1 := Nat.lt_succ_self n
     have_tailrec n
 termination_by n => n
-derive_functional_induction have_tailrec
 
 /--
 info: have_tailrec.induct (motive : Nat → Prop) (case1 : motive 0)
@@ -93,7 +87,6 @@ def have_non_tailrec : Nat → Nat
       have h2 : n < n+1 := Nat.lt_succ_self n
       have_non_tailrec n
 termination_by n => n
-derive_functional_induction have_non_tailrec
 
 /--
 info: have_non_tailrec.induct (motive : Nat → Prop) (case1 : motive 0) (case2 : ∀ (n : Nat), motive n → motive n.succ) :
@@ -109,7 +102,6 @@ def let_tailrec : Nat → Nat
     let h2 : n < n+1 := Nat.lt_succ_self n
     let_tailrec n
 termination_by n => n
-derive_functional_induction let_tailrec
 
 /--
 info: let_tailrec.induct (motive : Nat → Prop) (case1 : motive 0)
@@ -130,7 +122,6 @@ def let_non_tailrec : Nat → Nat
       let h2 : n < n+1 := Nat.lt_succ_self n
       let_non_tailrec n
 termination_by n => n
-derive_functional_induction let_non_tailrec
 
 /--
 info: let_non_tailrec.induct (motive : Nat → Prop) (case1 : motive 0) (case2 : ∀ (n : Nat), motive n → motive n.succ) :
@@ -149,7 +140,6 @@ def with_ite_tailrec : Nat → Nat
     else
       with_ite_tailrec n
 termination_by n => n
-derive_functional_induction with_ite_tailrec
 
 /--
 info: with_ite_tailrec.induct (motive : Nat → Prop) (case1 : motive 0)
@@ -171,7 +161,6 @@ def with_ite_non_tailrec : Nat → Nat
       else
         with_ite_non_tailrec n
 termination_by n => n
-derive_functional_induction with_ite_non_tailrec
 
 /--
 info: with_ite_non_tailrec.induct (motive : Nat → Prop) (case1 : motive 0) (case2 : motive 1)
@@ -188,7 +177,6 @@ def with_dite_non_tailrec (n : Nat) : Nat :=
     else
       0
 termination_by n
-derive_functional_induction with_dite_non_tailrec
 
 /--
 info: with_dite_non_tailrec.induct (motive : Nat → Prop) (case1 : ∀ (x : Nat), (x - 1 < x → motive (x - 1)) → motive x)
@@ -204,7 +192,6 @@ def with_dite_tailrec (n : Nat) : Nat :=
     else
       0
 termination_by n
-derive_functional_induction with_dite_tailrec
 
 /--
 info: with_dite_tailrec.induct (motive : Nat → Prop) (case1 : ∀ (x : Nat), x - 1 < x → motive (x - 1) → motive x)
@@ -221,7 +208,6 @@ def with_match_refining_tailrec : Nat → Nat
     | 0 => with_match_refining_tailrec 0
     | m => with_match_refining_tailrec m
 termination_by n => n
-derive_functional_induction with_match_refining_tailrec
 
 /--
 info: with_match_refining_tailrec.induct (motive : Nat → Prop) (case1 : motive 0) (case2 : motive 0 → motive (Nat.succ 0))
@@ -237,7 +223,6 @@ def with_arg_refining_match1 (i : Nat) : Nat → Nat
   | n+1 =>
     if h : i = 0 then 0 else with_arg_refining_match1 (i - 1) n
 termination_by i
-derive_functional_induction with_arg_refining_match1
 
 /--
 info: with_arg_refining_match1.induct (motive : Nat → Nat → Prop) (case1 : ∀ (i : Nat), motive i 0)
@@ -252,7 +237,6 @@ def with_arg_refining_match2 (i : Nat) (n : Nat) : Nat :=
   | 0 => 0
   | n+1 => with_arg_refining_match2 (i - 1) n
 termination_by i
-derive_functional_induction with_arg_refining_match2
 
 /--
 info: with_arg_refining_match2.induct (motive : Nat → Nat → Prop) (case1 : ∀ (n : Nat), motive 0 n)
@@ -271,7 +255,6 @@ def with_other_match_tailrec : Nat → Nat
     | 0 => with_other_match_tailrec n
     | _ => with_other_match_tailrec n
 termination_by n => n
-derive_functional_induction with_other_match_tailrec
 
 /--
 info: with_other_match_tailrec.induct (motive : Nat → Prop) (case1 : motive 0)
@@ -287,7 +270,6 @@ def with_mixed_match_tailrec : Nat → Nat → Nat → Nat → Nat := fun a b c
   | 0, _, _, _ => 0
   | a+1, x, y, z => with_mixed_match_tailrec a x y z
 termination_by n => n
-derive_functional_induction with_mixed_match_tailrec
 
 /--
 info: with_mixed_match_tailrec.induct (motive : Nat → Nat → Nat → Nat → Prop) (case1 : ∀ (a a_1 x : Nat), motive 0 x a a_1)
@@ -306,7 +288,6 @@ def with_mixed_match_tailrec2 : Nat → Nat → Nat → Nat → Nat → Nat := f
     | 0, _, _, _ => 0
     | a+1, x, y, z => with_mixed_match_tailrec2 n a x y z
 termination_by n => n
-derive_functional_induction with_mixed_match_tailrec2
 
 /--
 info: with_mixed_match_tailrec2.induct (motive : Nat → Nat → Nat → Nat → Nat → Prop)
@@ -326,7 +307,6 @@ def with_match_non_tailrec : Nat → Nat
     | 0 => with_match_non_tailrec n
     | _ => with_match_non_tailrec n
 termination_by n => n
-derive_functional_induction with_match_non_tailrec
 
 /--
 info: with_match_non_tailrec.induct (motive : Nat → Prop) (case1 : motive 0) (case2 : ∀ (n : Nat), motive n → motive n.succ) :
@@ -344,7 +324,6 @@ def with_match_non_tailrec_refining : Nat → Nat
     | 0 => with_match_non_tailrec_refining 0
     | m => with_match_non_tailrec_refining m
 termination_by n => n
-derive_functional_induction with_match_non_tailrec_refining
 
 /--
 info: with_match_non_tailrec_refining.induct (motive : Nat → Prop) (case1 : motive 0)
@@ -367,7 +346,6 @@ def with_overlap : Nat → Nat
   | 3 => 3
   | n+1 => with_overlap n
 termination_by n => n
-derive_functional_induction with_overlap
 
 /--
 info: with_overlap.induct (motive : Nat → Prop) (case1 : motive 0) (case2 : motive 1) (case3 : motive 2) (case4 : motive 3)
@@ -386,27 +364,25 @@ def unary (base : Nat) : Nat → Nat
   | 0 => base
   | n+1 => unary base n
 termination_by n => n
-derive_functional_induction unary
 
 /--
 info: UnusedExtraParams.unary.induct (base : Nat) (motive : Nat → Prop) (case1 : motive 0)
   (case2 : ∀ (n : Nat), motive n → motive n.succ) : ∀ (a : Nat), motive a
 -/
 #guard_msgs in
-#check unary.induct
+#check UnusedExtraParams.unary.induct
 
 def binary (base : Nat) : Nat → Nat → Nat
   | 0, m => base + m
   | n+1, m => binary base n m
 termination_by n => n
-derive_functional_induction binary
 
 /--
 info: UnusedExtraParams.binary.induct (base : Nat) (motive : Nat → Nat → Prop) (case1 : ∀ (m : Nat), motive 0 m)
   (case2 : ∀ (n m : Nat), motive n m → motive n.succ m) : ∀ (a a_1 : Nat), motive a a_1
 -/
 #guard_msgs in
-#check binary.induct
+#check UnusedExtraParams.binary.induct
 
 end UnusedExtraParams
 
@@ -430,7 +406,6 @@ def match_non_tail_induct
       case1 (n+1) (IH n (Nat.lt_succ_self _))
   ) n
 
-derive_functional_induction match_non_tail
 
 /--
 info: NonTailrecMatch.match_non_tail.induct (motive : Nat → Prop)
@@ -444,11 +419,11 @@ info: NonTailrecMatch.match_non_tail.induct (motive : Nat → Prop)
   (n : Nat) : motive n
 -/
 #guard_msgs in
-#check match_non_tail.induct
+#check NonTailrecMatch.match_non_tail.induct
 
 
 theorem match_non_tail_eq_true (n : Nat) : match_non_tail n = true := by
-  induction n using match_non_tail.induct
+  induction n using NonTailrecMatch.match_non_tail.induct
   case case1 n IH =>
     unfold match_non_tail
     split <;> dsimp at IH <;> simp [IH]
@@ -463,16 +438,13 @@ def foo (n : Nat) :=
   | 0 => 0
   | x@(n+1) => x + foo n
 termination_by n
-derive_functional_induction foo
 
 /--
 info: AsPattern.foo.induct (motive : Nat → Prop) (case1 : motive 0) (case2 : ∀ (n : Nat), motive n → motive n.succ)
   (n : Nat) : motive n
 -/
 #guard_msgs in
-#check foo.induct
-
-
+#check AsPattern.foo.induct
 
 def bar (n : Nat) :=
   1 +
@@ -480,7 +452,6 @@ def bar (n : Nat) :=
   | 0 => 0
   | x@(n+1) => x + bar n
 termination_by n
-derive_functional_induction bar
 
 /--
 info: AsPattern.bar.induct (motive : Nat → Prop)
@@ -493,7 +464,7 @@ info: AsPattern.bar.induct (motive : Nat → Prop)
   (n : Nat) : motive n
 -/
 #guard_msgs in
-#check bar.induct
+#check AsPattern.bar.induct
 
 end AsPattern
 
@@ -521,13 +492,12 @@ decreasing_by
   simp_wf
   simp [below_lt, *]
 
-derive_functional_induction foo
 /--
 info: GramSchmidt.foo.induct (motive : Nat → Prop) (case1 : ∀ (x : Nat), (∀ (i : Nat), below x i → motive i) → motive x)
   (n : Nat) : motive n
 -/
 #guard_msgs in
-#check foo.induct
+#check GramSchmidt.foo.induct
 
 end GramSchmidt
 
@@ -539,13 +509,12 @@ def foo {α} (x : α) : List α → Nat
       let this := foo x ys
       this
 termination_by xs => xs
-derive_functional_induction foo
 /--
 info: LetFun.foo.induct.{u_1} {α : Type u_1} (x : α) (motive : List α → Prop) (case1 : motive [])
   (case2 : ∀ (_y : α) (ys : List α), motive ys → motive (_y :: ys)) : ∀ (a : List α), motive a
 -/
 #guard_msgs in
-#check foo.induct
+#check LetFun.foo.induct
 
 
 def bar {α} (x : α) : List α → Nat
@@ -555,13 +524,12 @@ def bar {α} (x : α) : List α → Nat
       this
 termination_by xs => xs
 
-derive_functional_induction bar
 /--
 info: LetFun.bar.induct.{u_1} {α : Type u_1} (x : α) (motive : List α → Prop) (case1 : motive [])
   (case2 : ∀ (_y : α) (ys : List α), motive ys → motive (_y :: ys)) : ∀ (a : List α), motive a
 -/
 #guard_msgs in
-#check bar.induct
+#check LetFun.bar.induct
 
 end LetFun
 
@@ -572,7 +540,6 @@ def foo : Nat → Nat
   | 0 => 0
   | n+1 => if foo n = 0 then 1 else 0
 termination_by n => n
-derive_functional_induction foo
 
 /--
 info: RecCallInDisrs.foo.induct (motive : Nat → Prop) (case1 : motive 0)
@@ -580,7 +547,7 @@ info: RecCallInDisrs.foo.induct (motive : Nat → Prop) (case1 : motive 0)
   (case3 : ∀ (n : Nat), ¬foo n = 0 → motive n → motive n.succ) : ∀ (a : Nat), motive a
 -/
 #guard_msgs in
-#check foo.induct
+#check RecCallInDisrs.foo.induct
 
 
 set_option linter.unusedVariables false in
@@ -591,7 +558,6 @@ def bar : Nat → Nat
     | 0, _ => 1
     | m+1, _ => bar m
 termination_by n => n
-derive_functional_induction bar
 
 /--
 info: RecCallInDisrs.bar.induct (motive : Nat → Prop) (case1 : motive 0) (case2 : bar 0 = 0 → motive 0 → motive (Nat.succ 0))
@@ -599,7 +565,7 @@ info: RecCallInDisrs.bar.induct (motive : Nat → Prop) (case1 : motive 0) (case
   (case4 : ∀ (m : Nat), motive m.succ → motive m → motive m.succ.succ) : ∀ (a : Nat), motive a
 -/
 #guard_msgs in
-#check bar.induct
+#check RecCallInDisrs.bar.induct
 
 end RecCallInDisrs
 
@@ -615,21 +581,20 @@ def odd : Nat → Bool
   | n+1 => even n
 termination_by n => n
 end
-derive_functional_induction even
 
 /--
 info: EvenOdd.even.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
 -/
 #guard_msgs in
-#check even.induct
+#check EvenOdd.even.induct
 
 /--
 info: EvenOdd.odd.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), motive2 a
 -/
 #guard_msgs in
-#check odd.induct
+#check EvenOdd.odd.induct
 
 end EvenOdd
 
@@ -645,7 +610,6 @@ def Tree.map (f : Tree → Tree) : Tree → Tree
 def Tree.map_forest (f : Tree → Tree) (ts : List Tree) : List Tree :=
   ts.attach.map (fun ⟨t, _ht⟩ => Tree.map f t)
 end
-derive_functional_induction Tree.map
 
 /--
 info: Tree.Tree.map.induct (f : Tree → Tree) (motive1 : Tree → Prop) (motive2 : List Tree → Prop)
@@ -653,7 +617,7 @@ info: Tree.Tree.map.induct (f : Tree → Tree) (motive1 : Tree → Prop) (motive
   (case2 : ∀ (ts : List Tree), (∀ (t : Tree), t ∈ ts → motive1 t) → motive2 ts) : ∀ (a : Tree), motive1 a
 -/
 #guard_msgs in
-#check Tree.map.induct
+#check Tree.Tree.map.induct
 
 /--
 info: Tree.Tree.map_forest.induct (f : Tree → Tree) (motive1 : Tree → Prop) (motive2 : List Tree → Prop)
@@ -661,7 +625,7 @@ info: Tree.Tree.map_forest.induct (f : Tree → Tree) (motive1 : Tree → Prop)
   (case2 : ∀ (ts : List Tree), (∀ (t : Tree), t ∈ ts → motive1 t) → motive2 ts) (ts : List Tree) : motive2 ts
 -/
 #guard_msgs in
-#check Tree.map_forest.induct
+#check Tree.Tree.map_forest.induct
 
 end Tree
 
@@ -674,28 +638,26 @@ def unary (fixed : Bool := false) (n : Nat := 0)  : Nat :=
   | 0 => 0
   | n+1 => unary fixed n
 termination_by n
-derive_functional_induction unary
 
 /--
 info: DefaultArgument.unary.induct (fixed : Bool) (motive : Nat → Prop) (case1 : motive 0)
   (case2 : ∀ (n : Nat), motive n → motive n.succ) (n : Nat) : motive n
 -/
 #guard_msgs in
-#check unary.induct
+#check DefaultArgument.unary.induct
 
 def foo (fixed : Bool := false) (n : Nat) (m : Nat := 0) : Nat :=
   match n with
   | 0 => m
   | n+1 => foo fixed n m
 termination_by n
-derive_functional_induction foo
 
 /--
 info: DefaultArgument.foo.induct (fixed : Bool) (motive : Nat → Nat → Prop) (case1 : ∀ (m : Nat), motive 0 m)
   (case2 : ∀ (m n : Nat), motive n m → motive n.succ m) (n m : Nat) : motive n m
 -/
 #guard_msgs in
-#check foo.induct
+#check DefaultArgument.foo.induct
 
 end DefaultArgument
 
@@ -708,7 +670,6 @@ def foo : Nat → Nat → (k : Nat) → Fin k → Nat
   | _, _, 1, _ => 0
   | n+1, m+1, k+2, _ => foo n m (k+1) ⟨0, Nat.zero_lt_succ _⟩
 termination_by n => n
-derive_functional_induction foo
 
 /--
 info: Nary.foo.induct (motive : Nat → Nat → (k : Nat) → Fin k → Prop)
@@ -720,7 +681,7 @@ info: Nary.foo.induct (motive : Nat → Nat → (k : Nat) → Fin k → Prop)
   ∀ (a a_1 k : Nat) (a_2 : Fin k), motive a a_1 k a_2
 -/
 #guard_msgs in
-#check foo.induct
+#check Nary.foo.induct
 
 end Nary
 
@@ -732,7 +693,6 @@ def foo (n : Nat) : Nat :=
     foo j
   else
     42
-derive_functional_induction foo
 
 /--
 info: Dite.foo.induct (motive : Nat → Prop)
@@ -747,91 +707,10 @@ info: Dite.foo.induct (motive : Nat → Prop)
   (n : Nat) : motive n
 -/
 #guard_msgs in
-#check foo.induct
+#check Dite.foo.induct
 
 end Dite
 
-namespace CommandIdempotence
-
--- This checks that the `derive_functional_induction` command gracefully handles being called twice
-
-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
-
-derive_functional_induction even._mutual
-
-/--
-info: CommandIdempotence.even._mutual.induct (motive : Nat ⊕' Nat → Prop) (case1 : motive (PSum.inl 0))
-  (case2 : ∀ (n : Nat), motive (PSum.inr n) → motive (PSum.inl n.succ)) (case3 : motive (PSum.inr 0))
-  (case4 : ∀ (n : Nat), motive (PSum.inl n) → motive (PSum.inr n.succ)) (x : Nat ⊕' Nat) : motive x
--/
-#guard_msgs in
-#check even._mutual.induct
-
-/-- error: unknown constant 'CommandIdempotence.even.induct' -/
-#guard_msgs in
-#check even.induct
-
-derive_functional_induction even
-
-/--
-info: CommandIdempotence.even._mutual.induct (motive : Nat ⊕' Nat → Prop) (case1 : motive (PSum.inl 0))
-  (case2 : ∀ (n : Nat), motive (PSum.inr n) → motive (PSum.inl n.succ)) (case3 : motive (PSum.inr 0))
-  (case4 : ∀ (n : Nat), motive (PSum.inl n) → motive (PSum.inr n.succ)) (x : Nat ⊕' Nat) : motive x
--/
-#guard_msgs in
-#check even._mutual.induct
-
-/--
-info: CommandIdempotence.even.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
--/
-#guard_msgs in
-#check even.induct
-
-derive_functional_induction even
-
-end CommandIdempotence
-
-namespace Errors
-
-/-- error: unknown constant 'doesNotExist' -/
-#guard_msgs in
-derive_functional_induction doesNotExist
-
-def takeWhile (p : α → Bool) (as : Array α) : Array α :=
-  foo 0 #[]
-where
-  foo (i : Nat) (r : Array α) : Array α :=
-    if h : i < as.size then
-      let a := as.get ⟨i, h⟩
-      if p a then
-        foo (i+1) (r.push a)
-      else
-        r
-    else
-      r
-  termination_by as.size - i
-
-/--
-error: Function Errors.takeWhile does not look like a function defined by recursion.
-NB: If Errors.takeWhile is not itself recursive, but contains an inner recursive function (via `let rec` or `where`), try `Errors.takeWhile.go` where `go` is name of the inner function.
--/
-#guard_msgs in
-derive_functional_induction takeWhile
-
-derive_functional_induction takeWhile.foo
-
-end Errors
 
 namespace PreserveParams
 
@@ -847,7 +726,6 @@ def foo (a : Nat) : Nat → Nat
     if a = n then 42 else
     foo a n
 termination_by n => n
-derive_functional_induction foo
 
 /--
 info: PreserveParams.foo.induct (a : Nat) (motive : Nat → Prop) (case1 : motive 0)
@@ -855,7 +733,7 @@ info: PreserveParams.foo.induct (a : Nat) (motive : Nat → Prop) (case1 : motiv
   (case4 : ∀ (n : Nat), ¬a = 23 → ¬a = n → motive n → motive n.succ) : ∀ (a : Nat), motive a
 -/
 #guard_msgs in
-#check foo.induct
+#check PreserveParams.foo.induct
 
 
 end PreserveParams