sdgoij/lean4
1
0
Fork 0
mirror of https://github.com/leanprover/lean4.git synced 2026-03-17 18:34:06 +00:00
Code Issues Packages Projects Releases Wiki Activity

chore: use terminology "non-recursive structure" instead of "struct-like" (#12749)

Browse Source 
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
This commit is contained in:
Kyle Miller
2026-03-08 20:44:38 -07:00
committed by GitHub
parent 530842e843
commit d8accf47b3
14 changed files with 52 additions and 46 deletions
Download Patch File Download Diff File Expand all files Collapse all files

13
src/Lean/Elab/App.lean
View File

@@ -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}"}"

18
src/Lean/Expr.lean
View File

@@ -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

2
src/Lean/Meta/Basic.lean
View File

@@ -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`.
-/

10
src/Lean/Meta/ExprDefEq.lean
View File

@@ -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

2
src/Lean/Meta/Tactic/Grind/Internalize.lean
View File

@@ -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

4
src/Lean/Meta/WHNF.lean
View File

@@ -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

8
src/Lean/MonadEnv.lean
View File

@@ -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

13
src/Lean/Structure.lean
View File

@@ -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

6
src/kernel/inductive.cpp
View File

@@ -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();

8
src/kernel/inductive.h
View File

@@ -19,8 +19,8 @@ bool is_recursor(environment const & env, name const & n);
Otherwise, return none. */
optional<name> 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<expr> 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<typename WHNF, typename INFER>
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))

4
src/kernel/type_checker.cpp
View File

@@ -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<expr> 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();

4
tests/elab/9312.lean
View File

@@ -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.
-/

4
tests/elab/invalidProjection.lean
View File

@@ -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

2
tests/elab/structure_recursive.lean
View File

@@ -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)