From ed9facba07fd8d2b2d35150a31f87f7e2be1e3f1 Mon Sep 17 00:00:00 2001 From: Joachim Breitner Date: Sat, 12 Oct 2024 13:40:42 +0200 Subject: [PATCH] =?UTF-8?q?fix:=20RecursorVal.getInduct=20to=20return=20na?= =?UTF-8?q?me=20of=20major=20argument=E2=80=99s=20type?= 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. (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 | 7 +++- src/kernel/declaration.cpp | 13 ++++++- src/kernel/declaration.h | 2 +- tests/lean/run/issue5661.lean | 66 +++++++++++++++++++++++++++++++++++ 4 files changed, 85 insertions(+), 3 deletions(-) create mode 100644 tests/lean/run/issue5661.lean diff --git a/src/Lean/Declaration.lean b/src/Lean/Declaration.lean index 6cac5cd3edf1..f24b9ae8ff8a 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 +/-- 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` diff --git a/src/kernel/declaration.cpp b/src/kernel/declaration.cpp index 489a134c1258..0e0ee6778a91 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_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..c6b4ee46ea6c 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_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/tests/lean/run/issue5661.lean b/tests/lean/run/issue5661.lean new file mode 100644 index 000000000000..d25112128104 --- /dev/null +++ b/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