feat: use reserved name infrastructure for functional induction

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