fix: RecursorVal.getInduct to return name of major argument’s type

Previously `RecursorVal.getInduct` would return the prefix of the
recursor’s name, which is unlikely the right value for the “derived”
recursors in nested recursion. The code using `RecursorVal.getInduct`
seems to expect the name of the inductive type of major argument here.

If we return that name, this fixes #5661.

This bug becomes more visible now that we have structural mutual
recursion.

(The implementation is still up for discussion; let’s first agree on
whether this is the right semantics.)

(Also likely worth renaming this function to `getMajorInduct` for
clarity.)

src/Lean/Declaration.lean

@@ -369,8 +369,13 @@ def RecursorVal.getFirstIndexIdx (v : RecursorVal) : Nat :=
 def RecursorVal.getFirstMinorIdx (v : RecursorVal) : Nat :=
   v.numParams + v.numMotives
 
+/-- The inductive type of the major argument of the recursor. -/
 def RecursorVal.getInduct (v : RecursorVal) : Name :=
-  v.name.getPrefix
+  go v.getMajorIdx v.type
+where -- TODO: Turn into a helper function on Lean.Expr
+  go
+  | 0, e => e.bindingDomain!.getAppFn.constName!
+  | n+1, e => go n e.bindingBody!
 
 inductive QuotKind where
   | type  -- `Quot`

src/kernel/declaration.cpp

@@ -126,7 +126,6 @@ constructor_val::constructor_val(name const & n, names const & lparams, expr con
     object_ref(lean_mk_constructor_val(n.to_obj_arg(), lparams.to_obj_arg(), type.to_obj_arg(), induct.to_obj_arg(),
                                        nat(cidx).to_obj_arg(), nat(nparams).to_obj_arg(), nat(nfields).to_obj_arg(), is_unsafe)) {
 }
-
 bool constructor_val::is_unsafe() const { return lean_constructor_val_is_unsafe(to_obj_arg()); }
 
 extern "C" object * lean_mk_recursor_val(object * n, object * lparams, object * type, object * all,
@@ -143,6 +142,18 @@ recursor_val::recursor_val(name const & n, names const & lparams, expr const & t
                                     nat(nminors).to_obj_arg(), rules.to_obj_arg(), k, is_unsafe)) {
 }
 
+name const & recursor_val::get_induct() const {
+    unsigned int n = get_major_idx();
+    expr const * t = &(to_constant_val().get_type());
+    for (unsigned int i = 0; i < n; i++) {
+        t = &(binding_body(*t));
+    }
+    t = &(binding_domain(*t));
+    t = &(get_app_fn(*t));
+    return const_name(*t);
+}
+
+
 bool recursor_val::is_k() const { return lean_recursor_k(to_obj_arg()); }
 bool recursor_val::is_unsafe() const { return lean_recursor_is_unsafe(to_obj_arg()); }
 

src/kernel/declaration.h

@@ -370,7 +370,7 @@ class recursor_val : public object_ref {
     recursor_val & operator=(recursor_val && other) { object_ref::operator=(std::move(other)); return *this; }
     constant_val const & to_constant_val() const { return static_cast<constant_val const &>(cnstr_get_ref(*this, 0)); }
     name const & get_name() const { return to_constant_val().get_name(); }
-    name const & get_induct() const { return get_name().get_prefix(); }
+    name const & get_induct() const;
     names const & get_all() const { return static_cast<names const &>(cnstr_get_ref(*this, 1)); }
     unsigned get_nparams() const { return static_cast<nat const &>(cnstr_get_ref(*this, 2)).get_small_value(); }
     unsigned get_nindices() const { return static_cast<nat const &>(cnstr_get_ref(*this, 3)).get_small_value(); }

tests/lean/run/issue5661.lean

@@ -0,0 +1,66 @@
+import Lean.Meta.Basic
+
+inductive StructLike α where
+  | mk : α → StructLike α
+
+inductive Nested where
+  | nest : StructLike Nested → Nested
+  | other
+
+/-- info: StructLike -/
+#guard_msgs in
+open Lean Meta in
+run_meta do
+  let i ← getConstInfoRec ``Nested.rec_1
+  logInfo m!"{i.getInduct}"
+
+theorem works (x : StructLike Nested) : StructLike.rec
+  (motive := fun _ => Bool)
+  (mk := fun _ => true)
+  x = true
+  := rfl
+
+theorem failed_before (x : StructLike Nested) : Nested.rec_1
+  (motive_1 := fun _ => Bool) (motive_2 := fun _ => Bool)
+  (nest := fun _ _ => true)
+  (other := true)
+  (mk := fun _ _ => true)
+  x = true
+  := rfl
+
+
+-- The original surface bug
+
+inductive Set (α : Type u) where
+  | mk (l : List α)
+
+inductive Value where
+  | prim
+  | set (s : Set Value)
+
+instance : DecidableEq Value := sorry
+
+mutual
+
+def Value.lt : Value → Value → Bool
+  | .prim, .prim => false
+  | .set (.mk vs₁), .set (.mk vs₂) => Values.lt vs₁ vs₂
+  | .prim, .set _ => true
+  | .set _, .prim => false
+
+def Values.lt : List Value → List Value → Bool
+  | [], [] => false
+  | [], _ => true
+  | _, [] => false
+  | v₁ :: vs₁, v₂ :: vs₂ => Value.lt v₁ v₂ || (v₁ = v₂ && Values.lt vs₁ vs₂)
+
+end
+
+theorem Value.lt_irrefl (v : Value) :
+  ¬ Value.lt v v
+:= by
+  cases v
+  case set a =>
+    show ¬Values.lt a.1 a.1 = true
+    sorry
+  all_goals sorry