From d8accf47b39c107e53336744376a7ffff4d7ec98 Mon Sep 17 00:00:00 2001 From: Kyle Miller Date: Sun, 8 Mar 2026 20:44:38 -0700 Subject: [PATCH] chore: use terminology "non-recursive structure" instead of "struct-like" (#12749) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit This PR changes "structure-like" terminology to "non-recursive structure" across internal documentation, error messages, the metaprogramming API, and the kernel, to clarify Lean's type theory. A *structure* is a one-constructor inductive type with no indices — these can be created by either the `structure` or `inductive` commands — and are supported by the primitive `Expr.proj` projections. Only *non-recursive* structures have an eta conversion rule. The PR description contains the APIs that were renamed. Addresses RFC #5891, which proposed this rename. The change is motivated by the need to distinguish between `structure`-defined structures, structures, and non-recursive structures. Especially since #5783, which enabled the `structure` command to define recursive structures, "structure-like" has been easy to misunderstand. Changes: - Kernel: `is_structure_like()` -> `is_non_rec_structure()` - `Lean.isStructureLike` -> `Lean.isNonRecStructure` - `Lean.matchConstStructLike` -> `Lean.matchConstNonRecStructure` - `Lean.getStructureLikeCtor?` -> `Lean.getNonRecStructureCtor?` - `Lean.getStructureLikeNumFields` -> `Lean.getNonRecStructureNumFields` - `Lean.Expr.proj`: extended and corrected documentation (note: despite the fact that not every projection can be written as a recursor application, I left in this claim since it seems good to document a more-restrictive specification, and some users have requested the kernel be more restrictive in this way) Closes #5891 --- src/Lean/Elab/App.lean | 13 +++++++------ src/Lean/Expr.lean | 18 ++++++++++++------ src/Lean/Meta/Basic.lean | 2 +- src/Lean/Meta/ExprDefEq.lean | 10 +++++----- src/Lean/Meta/Tactic/Grind/Internalize.lean | 2 +- src/Lean/Meta/WHNF.lean | 4 ++-- src/Lean/MonadEnv.lean | 8 ++++---- src/Lean/Structure.lean | 13 ++++++------- src/kernel/inductive.cpp | 6 +++--- src/kernel/inductive.h | 8 ++++---- src/kernel/type_checker.cpp | 4 ++-- tests/elab/9312.lean | 4 ++-- tests/elab/invalidProjection.lean | 4 ++-- tests/elab/structure_recursive.lean | 2 +- 14 files changed, 52 insertions(+), 46 deletions(-) diff --git a/src/Lean/Elab/App.lean b/src/Lean/Elab/App.lean index 2c34fe0e83..cdafba20be 100644 --- a/src/Lean/Elab/App.lean +++ b/src/Lean/Elab/App.lean @@ -1247,7 +1247,7 @@ inductive LValResolution where /-- When applied to `f`, effectively expands to `BaseStruct.fieldName (self := Struct.toBase f)`. This is a special named argument where it suppresses any explicit arguments depending on it so that type parameters don't need to be supplied. -/ | projFn (baseStructName : Name) (structName : Name) (fieldName : Name) - /-- Similar to `projFn`, but for extracting field indexed by `idx`. Works for structure-like inductive types in general. -/ + /-- Similar to `projFn`, but for extracting field indexed by `idx`. Works for one-constructor inductive types in general. -/ | projIdx (structName : Name) (idx : Nat) /-- When applied to `f`, effectively expands to `constName ... (Struct.toBase f)`, with the argument placed in the correct positional argument if possible, or otherwise as a named argument. The `Struct.toBase` is not present if `baseStructName == structName`, @@ -1331,9 +1331,9 @@ private def resolveLValAux (e : Expr) (eType : Expr) (lval : LVal) : TermElabM L if idx == 0 then throwError "Invalid projection: Index must be greater than 0" let env ← getEnv - let failK _ := throwError "Invalid projection: Projection operates on structure-like types \ - with fields. The expression{indentExpr e}\nhas type{inlineExpr eType}which does not \ - have fields." + let failK _ := throwError "Invalid projection: Projections extract constructor fields for \ + one-constructor inductive types. \ + The expression{indentExpr e}\nhas type{inlineExpr eType}which is not a one-constructor inductive type." matchConstStructure eType.getAppFn failK fun _ _ ctorVal => do let numFields := ctorVal.numFields @@ -1347,8 +1347,9 @@ private def resolveLValAux (e : Expr) (eType : Expr) (lval : LVal) : TermElabM L return LValResolution.projIdx structName (idx - 1) else if numFields == 0 then - throwError m!"Invalid projection: Projection operates on structure-like types with \ - fields. The expression{indentExpr e}\nhas type{inlineExpr eType}which has no fields." + throwError m!"Invalid projection: Projections extract constructor fields for \ + one-constructor inductive types. \ + The expression{indentExpr e}\nhas type{inlineExpr eType}which has no fields." let tupleHint ← mkTupleHint eType idx ref throwError m!"Invalid projection: Index `{idx}` is invalid for this structure; \ {numFields.plural "the only valid index is 1" s!"it must be between 1 and {numFields}"}" diff --git a/src/Lean/Expr.lean b/src/Lean/Expr.lean index 1e1969a15d..7224cbd086 100644 --- a/src/Lean/Expr.lean +++ b/src/Lean/Expr.lean @@ -447,18 +447,24 @@ inductive Expr where /-- Projection-expressions. They are redundant, but are used to create more compact - terms, speedup reduction, and implement eta for structures. - The type of `struct` must be an structure-like inductive type. That is, it has only one - constructor, is not recursive, and it is not an inductive predicate. The kernel and elaborators - check whether the `typeName` matches the type of `struct`, and whether the (zero-based) index - is valid (i.e., it is smaller than the number of constructor fields). - When exporting Lean developments to other systems, `proj` can be replaced with `typeName`.`rec` + terms, speed up reduction, and implement eta for structures. + The type of `struct` must be a one-constructor inductive type. + If `I.mk` is the constructor of an `m`-parameter inductive type `I`, + then ``.proj `I k (@I.mk p1 ... pm f0 f1 ...)`` is definitionally equal to `fk`. + + The kernel and elaborator check whether the `typeName` matches the type of `struct`, + whether the zero-based index is valid (it must be smaller than the number of constructor fields), + and whether the projection itself is valid (for inductive predicates, the fields must be propositions). + When exporting Lean developments to other systems, `proj` can be replaced with `typeName.rec` applications. + Non-recursive structures (one-constructor inductive types with no indices) have an eta rule: + if `e : I p1 ... pm`, then `e` and `@I.mk p1 ... pm e.1 e.2 ... e.n` are definitionally equal. Example, given `a : Nat × Bool`, `a.1` is represented as ``` .proj `Prod 0 a ``` + and `a` is definitionally equal to `@Prod.mk Nat Bool a.1 a.2` by the structure eta rule. -/ | proj (typeName : Name) (idx : Nat) (struct : Expr) with diff --git a/src/Lean/Meta/Basic.lean b/src/Lean/Meta/Basic.lean index 9ff01fbc71..cce9a11aca 100644 --- a/src/Lean/Meta/Basic.lean +++ b/src/Lean/Meta/Basic.lean @@ -742,7 +742,7 @@ def setPostponed (postponed : PersistentArray PostponedEntry) : MetaM Unit := for the inductive datatype `inductName`. Recall we have three different settings: `.none` (never use it), `.all` (always use it), `.notClasses` - (enabled only for structure-like inductive types that are not classes). + (enabled only for non-recursive structure types that are not classes). The parameter `inductName` affects the result only if the current setting is `.notClasses`. -/ diff --git a/src/Lean/Meta/ExprDefEq.lean b/src/Lean/Meta/ExprDefEq.lean index 389e114b92..790ed93784 100644 --- a/src/Lean/Meta/ExprDefEq.lean +++ b/src/Lean/Meta/ExprDefEq.lean @@ -120,8 +120,8 @@ where trace[Meta.isDefEq.eta.struct] "failed, insufficient number of arguments at{indentExpr b}" return false else - if !isStructureLike (← getEnv) ctorVal.induct then - trace[Meta.isDefEq.eta.struct] "failed, type is not a structure{indentExpr b}" + if !isNonRecStructure (← getEnv) ctorVal.induct then + trace[Meta.isDefEq.eta.struct] "failed, type is not a non-recursive structure{indentExpr b}" return false else if (← isDefEq (← inferType a) (← inferType b)) then checkpointDefEq do @@ -2095,9 +2095,9 @@ where assign `?m`. -/ return false - let some ctorVal := getStructureLikeCtor? (← getEnv) structName | return false + let some ctorVal := getNonRecStructureCtor? (← getEnv) structName | return false if ctorVal.numFields != 1 then - return false -- It is not a structure with a single field. + return false -- It is not a non-recursive structure with a single field. let sType ← whnf (← inferType s) let sTypeFn := sType.getAppFn if !sTypeFn.isConstOf structName then @@ -2133,7 +2133,7 @@ private def isDefEqApp (t s : Expr) : MetaM Bool := do /-- Return `true` if the type of the given expression is an inductive datatype with a single constructor with no fields. -/ private def isDefEqUnitLike (t : Expr) (s : Expr) : MetaM Bool := do let tType ← whnf (← inferType t) - matchConstStructureLike tType.getAppFn (fun _ => return false) fun _ _ ctorVal => do + matchConstNonRecStructure tType.getAppFn (fun _ => return false) fun _ _ ctorVal => do if ctorVal.numFields != 0 then return false else if (← useEtaStruct ctorVal.induct) then diff --git a/src/Lean/Meta/Tactic/Grind/Internalize.lean b/src/Lean/Meta/Tactic/Grind/Internalize.lean index b0dc390326..7f0412a92f 100644 --- a/src/Lean/Meta/Tactic/Grind/Internalize.lean +++ b/src/Lean/Meta/Tactic/Grind/Internalize.lean @@ -346,7 +346,7 @@ these facts. private def propagateEtaStruct (a : Expr) (generation : Nat) : GoalM Unit := do unless (← getConfig).etaStruct do return () let aType ← whnf (← inferType a) - matchConstStructureLike aType.getAppFn (fun _ => return ()) fun inductVal us ctorVal => do + matchConstNonRecStructure aType.getAppFn (fun _ => return ()) fun inductVal us ctorVal => do unless a.isAppOf ctorVal.name do -- TODO: remove ctorVal.numFields after update stage0 if (← isExtTheorem inductVal.name) || ctorVal.numFields == 0 then diff --git a/src/Lean/Meta/WHNF.lean b/src/Lean/Meta/WHNF.lean index 62bc98613b..c2924e0cda 100644 --- a/src/Lean/Meta/WHNF.lean +++ b/src/Lean/Meta/WHNF.lean @@ -169,7 +169,7 @@ def mkProjFn (ctorVal : ConstructorVal) (us : List Level) (params : Array Expr) | some projFn => return mkApp (mkAppN (mkConst projFn us) params) major /-- - If `major` is not a constructor application, and its type is a structure `C ...`, then return `C.mk major.1 ... major.n` + If `major` is not a constructor application, and its type is a non-recursive structure `C ...`, then return `C.mk major.1 ... major.n` \pre `inductName` is `C`. @@ -178,7 +178,7 @@ private def toCtorWhenStructure (inductName : Name) (major : Expr) : MetaM Expr unless (← useEtaStruct inductName) do return major let env ← getEnv - if !isStructureLike env inductName then + if !isNonRecStructure env inductName then return major else if let some _ ← isConstructorApp? major then return major diff --git a/src/Lean/MonadEnv.lean b/src/Lean/MonadEnv.lean index c24b3d6038..a76026a5ba 100644 --- a/src/Lean/MonadEnv.lean +++ b/src/Lean/MonadEnv.lean @@ -147,7 +147,7 @@ def getConstInfoRec [Monad m] [MonadEnv m] [MonadError m] (constName : Name) : m /-- Matches if `e` is a constant that is an inductive type with one constructor. Such types can be used with primitive projections. -See also `Lean.matchConstStructLike` for a more restrictive version. +See also `Lean.matchConstNonRecStructure` for a more restrictive version. -/ @[inline] def matchConstStructure [Monad m] [MonadEnv m] [MonadError m] (e : Expr) (failK : Unit → m α) (k : InductiveVal → List Level → ConstructorVal → m α) : m α := matchConstInduct e failK fun ival us => do @@ -159,11 +159,11 @@ See also `Lean.matchConstStructLike` for a more restrictive version. | _ => failK () /-- -Matches if `e` is a constant that is an non-recursive inductive type with no indices and with one constructor. -Such a type satisfies `Lean.isStructureLike`. +Matches if `e` is a constant that is a non-recursive inductive type with no indices and with one constructor. +Such a type satisfies `Lean.isNonRecStructure`. See also `Lean.matchConstStructure` for a less restrictive version. -/ -@[inline] def matchConstStructureLike [Monad m] [MonadEnv m] [MonadError m] (e : Expr) (failK : Unit → m α) (k : InductiveVal → List Level → ConstructorVal → m α) : m α := +@[inline] def matchConstNonRecStructure [Monad m] [MonadEnv m] [MonadError m] (e : Expr) (failK : Unit → m α) (k : InductiveVal → List Level → ConstructorVal → m α) : m α := matchConstInduct e failK fun ival us => do if ival.isRec || ival.numIndices != 0 then failK () else match ival.ctors with diff --git a/src/Lean/Structure.lean b/src/Lean/Structure.lean index 878d16e73f..77e580c4e5 100644 --- a/src/Lean/Structure.lean +++ b/src/Lean/Structure.lean @@ -143,8 +143,7 @@ Gets the constructor of an inductive type that has exactly one constructor. This is meant to be used with types that have had been registered as a structure by `registerStructure`, but this is not checked. -Warning: these do *not* need to be "structure-likes". A structure-like is non-recursive, -and structure-likes have special kernel support. +Warning: this does not check that the type has no indices. -/ def getStructureCtor (env : Environment) (constName : Name) : ConstructorVal := match env.find? constName with @@ -357,9 +356,9 @@ where /-- Returns true iff `constName` is a non-recursive inductive datatype that has only one constructor and no indices. -Such types have special kernel support. This must be in sync with `is_structure_like`. +Such types have special kernel support (e.g. the eta rule). This must be in sync with `is_non_rec_structure()`. -/ -def isStructureLike (env : Environment) (constName : Name) : Bool := +def isNonRecStructure (env : Environment) (constName : Name) : Bool := match env.find? constName with | some (.inductInfo { isRec := false, ctors := [_], numIndices := 0, .. }) => true | _ => false @@ -367,7 +366,7 @@ def isStructureLike (env : Environment) (constName : Name) : Bool := /-- Returns the constructor of the structure named `constName` if it is a non-recursive single-constructor inductive type with no indices. -/ -def getStructureLikeCtor? (env : Environment) (constName : Name) : Option ConstructorVal := +def getNonRecStructureCtor? (env : Environment) (constName : Name) : Option ConstructorVal := match env.find? constName with | some (.inductInfo { isRec := false, ctors := [ctorName], numIndices := 0, .. }) => match env.find? ctorName with @@ -375,8 +374,8 @@ def getStructureLikeCtor? (env : Environment) (constName : Name) : Option Constr | _ => panic! "ill-formed environment" | _ => none -/-- Returns the number of fields for a structure-like type -/ -def getStructureLikeNumFields (env : Environment) (constName : Name) : Nat := +/-- Returns the number of fields for a non-recursive structure type. -/ +def getNonRecStructureNumFields (env : Environment) (constName : Name) : Nat := match env.find? constName with | some (.inductInfo { isRec := false, ctors := [ctor], numIndices := 0, .. }) => match env.find? ctor with diff --git a/src/kernel/inductive.cpp b/src/kernel/inductive.cpp index b09b45204c..7a09077a76 100644 --- a/src/kernel/inductive.cpp +++ b/src/kernel/inductive.cpp @@ -18,13 +18,13 @@ Author: Leonardo de Moura namespace lean { static name * g_ind_fresh = nullptr; -/**\ brief Return recursor name for the given inductive datatype name */ +/** \brief Return recursor name for the given inductive datatype name */ name mk_rec_name(name const & I) { return I + name("rec"); } -/** \brief Return true if the given declaration is a structure */ -bool is_structure_like(environment const & env, name const & decl_name) { +/** \brief Return true if the given declaration is a non-recursive structure (an inductive type with one constructor and no indices). */ +bool is_non_rec_structure(environment const & env, name const & decl_name) { constant_info I = env.get(decl_name); if (!I.is_inductive()) return false; inductive_val I_val = I.to_inductive_val(); diff --git a/src/kernel/inductive.h b/src/kernel/inductive.h index 307c828f45..ace7545869 100644 --- a/src/kernel/inductive.h +++ b/src/kernel/inductive.h @@ -19,8 +19,8 @@ bool is_recursor(environment const & env, name const & n); Otherwise, return none. */ optional is_constructor_app(environment const & env, expr const & e); -/** \brief Return true if the given declaration is a structure */ -bool is_structure_like(environment const & env, name const & decl_name); +/** \brief Return true if the given declaration is a non-recursive structure (an inductive type with one constructor and no indices). */ +bool is_non_rec_structure(environment const & env, name const & decl_name); /* Auxiliary function for to_cnstr_when_K */ optional mk_nullary_cnstr(environment const & env, expr const & type, unsigned num_params); @@ -57,12 +57,12 @@ expr string_lit_to_constructor(expr const & e); /* Auxiliary method for \c to_cnstr_when_structure, convert `e` into `mk e.1 ... e.n` */ expr expand_eta_struct(environment const & env, expr const & e_type, expr const & e); -/* If `e` is not a constructor application and its type `C ...` is a structure, return `C.mk e.1 ... e.n`, +/* If `e` is not a constructor application and its type `C ...` is a non-recursive structure, return `C.mk e.1 ... e.n`, where `C.mk` is `C`s constructor. */ template inline expr to_cnstr_when_structure(environment const & env, name const & induct_name, expr const & e, WHNF const & whnf, INFER const & infer_type) { - if (!is_structure_like(env, induct_name) || is_constructor_app(env, e)) + if (!is_non_rec_structure(env, induct_name) || is_constructor_app(env, e)) return e; expr e_type = whnf(infer_type(e)); if (!is_constant(get_app_fn(e_type), induct_name)) diff --git a/src/kernel/type_checker.cpp b/src/kernel/type_checker.cpp index 964bb19a85..dd3741a339 100644 --- a/src/kernel/type_checker.cpp +++ b/src/kernel/type_checker.cpp @@ -797,7 +797,7 @@ bool type_checker::try_eta_struct_core(expr const & t, expr const & s) { if (!f_info.is_constructor()) return false; constructor_val f_val = f_info.to_constructor_val(); if (get_app_num_args(s) != f_val.get_nparams() + f_val.get_nfields()) return false; - if (!is_structure_like(env(), f_val.get_induct())) return false; + if (!is_non_rec_structure(env(), f_val.get_induct())) return false; if (!is_def_eq(infer_type(t), infer_type(s))) return false; buffer s_args; get_app_args(s, s_args); @@ -1044,7 +1044,7 @@ lbool type_checker::try_string_lit_expansion(expr const & t, expr const & s) { bool type_checker::is_def_eq_unit_like(expr const & t, expr const & s) { expr t_type = whnf(infer_type(t)); expr I = get_app_fn(t_type); - if (!is_constant(I) || !is_structure_like(env(), const_name(I))) + if (!is_constant(I) || !is_non_rec_structure(env(), const_name(I))) return false; name ctor_name = head(env().get(const_name(I)).to_inductive_val().get_cnstrs()); constructor_val ctor_val = env().get(ctor_name).to_constructor_val(); diff --git a/tests/elab/9312.lean b/tests/elab/9312.lean index 386c72cbaa..17ead9a578 100644 --- a/tests/elab/9312.lean +++ b/tests/elab/9312.lean @@ -10,7 +10,7 @@ no fields. structure MyEmpty where /-- -error: Invalid projection: Projection operates on structure-like types with fields. The expression +error: Invalid projection: Projections extract constructor fields for one-constructor inductive types. The expression { } has type `MyEmpty` which has no fields. -/ @@ -21,7 +21,7 @@ inductive T where | a /-- -error: Invalid projection: Projection operates on structure-like types with fields. The expression +error: Invalid projection: Projections extract constructor fields for one-constructor inductive types. The expression T.a has type `T` which has no fields. -/ diff --git a/tests/elab/invalidProjection.lean b/tests/elab/invalidProjection.lean index 485d453175..1802349430 100644 --- a/tests/elab/invalidProjection.lean +++ b/tests/elab/invalidProjection.lean @@ -41,9 +41,9 @@ Hint: n-tuples in Lean are actually nested pairs. To access the third component example (x : Nat × Nat × Nat) := x.3 /-- -error: Invalid projection: Projection operates on structure-like types with fields. The expression +error: Invalid projection: Projections extract constructor fields for one-constructor inductive types. The expression h -has type `Nat` which does not have fields. +has type `Nat` which is not a one-constructor inductive type. -/ #guard_msgs in example (h : Nat) := h.2 diff --git a/tests/elab/structure_recursive.lean b/tests/elab/structure_recursive.lean index 423cb9a23c..a6183d3cd4 100644 --- a/tests/elab/structure_recursive.lean +++ b/tests/elab/structure_recursive.lean @@ -133,7 +133,7 @@ structure Exists' {α : Sort _} (p : α → Prop) : Prop where h : p x /-! -Testing numeric projections on recursive inductive types now that the elaborator isn't restricted to structure-likes. +Testing numeric projections on recursive inductive types now that the elaborator isn't restricted to non-recursive structures. -/ inductive I1 where | mk (x : Nat) (xs : I1)