From e833667cf8e0682479c097d11b16c42ba5df27e7 Mon Sep 17 00:00:00 2001 From: Joachim Breitner Date: Mon, 21 Oct 2024 10:45:18 +0200 Subject: [PATCH] =?UTF-8?q?fix:=20RecursorVal.getInduct=20to=20return=20na?= =?UTF-8?q?me=20of=20major=20argument=E2=80=99s=20type=20(#5679)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit 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. Also, to avoid confusion, renames the function to ``getMajorInduct`. --- src/Lean/Declaration.lean | 9 ++++- src/Lean/Meta/WHNF.lean | 4 +- src/kernel/declaration.cpp | 13 ++++++- src/kernel/declaration.h | 2 +- src/kernel/inductive.h | 4 +- tests/lean/run/issue5661.lean | 73 +++++++++++++++++++++++++++++++++++ 6 files changed, 97 insertions(+), 8 deletions(-) create mode 100644 tests/lean/run/issue5661.lean diff --git a/src/Lean/Declaration.lean b/src/Lean/Declaration.lean index 6cac5cd3edf1..4be29c41349c 100644 --- a/src/Lean/Declaration.lean +++ b/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` diff --git a/src/Lean/Meta/WHNF.lean b/src/Lean/Meta/WHNF.lean index f2bb450582df..c7b5ce4e36df 100644 --- a/src/Lean/Meta/WHNF.lean +++ b/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 diff --git a/src/kernel/declaration.cpp b/src/kernel/declaration.cpp index 489a134c1258..492d3942c88b 100644 --- a/src/kernel/declaration.cpp +++ b/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()); } diff --git a/src/kernel/declaration.h b/src/kernel/declaration.h index 9b636ae0a8f6..398d4e1f8967 100644 --- a/src/kernel/declaration.h +++ b/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(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(cnstr_get_ref(*this, 1)); } unsigned get_nparams() const { return static_cast(cnstr_get_ref(*this, 2)).get_small_value(); } unsigned get_nindices() const { return static_cast(cnstr_get_ref(*this, 3)).get_small_value(); } diff --git a/src/kernel/inductive.h b/src/kernel/inductive.h index dd6b2671b2bf..a7b2864624ac 100644 --- a/src/kernel/inductive.h +++ b/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 app_type_args; get_app_args(app_type, app_type_args); @@ -94,7 +94,7 @@ inline optional 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 rule = get_rec_rule_for(rec_val, major); if (!rule) return none_expr(); buffer major_args; diff --git a/tests/lean/run/issue5661.lean b/tests/lean/run/issue5661.lean new file mode 100644 index 000000000000..c3d747d5a1f3 --- /dev/null +++ b/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