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

…eanprover#5679)

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 leanprover#5661.

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

Also, to avoid confusion, renames the function to ``getMajorInduct`.

src/Lean/Declaration.lean

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

src/Lean/Meta/WHNF.lean

@@ -95,7 +95,7 @@ private def toCtorWhenK (recVal : RecursorVal) (major : Expr) : MetaM Expr := do
   let majorType ← inferType major
   let majorType ← instantiateMVars (← whnf majorType)
   let majorTypeI := majorType.getAppFn
-  if !majorTypeI.isConstOf recVal.getInduct then
+  if !majorTypeI.isConstOf recVal.getMajorInduct then
     return major
   else if majorType.hasExprMVar && majorType.getAppArgs[recVal.numParams:].any Expr.hasExprMVar then
     return major
@@ -197,7 +197,7 @@ private def reduceRec (recVal : RecursorVal) (recLvls : List Level) (recArgs : A
       major ← toCtorWhenK recVal major
     major := major.toCtorIfLit
     major ← cleanupNatOffsetMajor major
-    major ← toCtorWhenStructure recVal.getInduct major
+    major ← toCtorWhenStructure recVal.getMajorInduct major
     match getRecRuleFor recVal major with
     | some rule =>
       let majorArgs := major.getAppArgs

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_major_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_major_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(); }

src/kernel/inductive.h

@@ -33,7 +33,7 @@ inline expr to_cnstr_when_K(environment const & env, recursor_val const & rval,
     lean_assert(rval.is_k());
     expr app_type    = whnf(infer_type(e));
     expr const & app_type_I = get_app_fn(app_type);
-    if (!is_constant(app_type_I) || const_name(app_type_I) != rval.get_induct()) return e; // type incorrect
+    if (!is_constant(app_type_I) || const_name(app_type_I) != rval.get_major_induct()) return e; // type incorrect
     if (has_expr_mvar(app_type)) {
         buffer<expr> app_type_args;
         get_app_args(app_type, app_type_args);
@@ -94,7 +94,7 @@ inline optional<expr> inductive_reduce_rec(environment const & env, expr const &
     else if (is_string_lit(major))
         major = string_lit_to_constructor(major);
     else
-        major = to_cnstr_when_structure(env, rec_val.get_induct(), major, whnf, infer_type);
+        major = to_cnstr_when_structure(env, rec_val.get_major_induct(), major, whnf, infer_type);
     optional<recursor_rule> rule = get_rec_rule_for(rec_val, major);
     if (!rule) return none_expr();
     buffer<expr> major_args;

tests/lean/run/issue5661.lean

@@ -0,0 +1,73 @@
+import Lean.Meta.Basic
+
+inductive StructLike α where
+  | mk : α → StructLike α
+
+inductive Nested where
+  | nest : StructLike Nested → Nested
+  | other
+
+/--
+info: theorem Nested.nest.sizeOf_spec : ∀ (a : StructLike Nested), sizeOf (Nested.nest a) = 1 + sizeOf a :=
+fun a => Eq.refl (1 + sizeOf a)
+-/
+#guard_msgs in
+#print Nested.nest.sizeOf_spec
+
+/-- info: StructLike -/
+#guard_msgs in
+open Lean Meta in
+run_meta do
+  let i ← getConstInfoRec ``Nested.rec_1
+  logInfo m!"{i.getMajorInduct}"
+
+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