Elaborator framework for (mutual) inductives

This module defines the framework for elaborating (mutually recursive) inductive types. Commands such as inductive and structure plug into this framework, and the framework orchestrates their mutual elaboration.

The main entry point for new inductive commands are the @[builtin_inductive_elab]/@[inductive_elab] attributes, which register a handler for a given decl syntax.

The main entry point to elaboration are the functions

• Lean.Elab.Command.isInductiveCommand to determine whether syntax has a registered inductive elaborator.
• Lean.Elab.Command.elabInductives to elaborate a list of syntaxes as mutually inductive types.
• Lean.Elab.Command.elabInductive to elaborate a single inductive command.

For mutual ... end in particular:

• Lean.Elab.Command.isMutualInductive to check whether each syntax element of a mutual ... end block has a registered inductive elaborator.
• Lean.Elab.Command.elabMutualInductive to elaborate a list of syntaxes satisfying isMutualInductive as a mutually inductive block.

See the docstring on Lean.Elab.Command.InductiveElabDescr for an overview of the framework.

opaque Lean.Elab.Command.inductive.autoPromoteIndices : Lean.Option Bool

opaque Lean.Elab.Command.bootstrap.inductiveCheckResultingUniverse : Lean.Option Bool

structure Lean.Elab.Command.CtorView : Type

View of a constructor. Only ref, modifiers, declName, and declId are required by the mutual inductive elaborator itself.

• ref : Syntax

  Syntax for the whole constructor.

• modifiers : Modifiers
• declName : Name

  Fully qualified name of the constructor.

• declId : Syntax

  Syntax for the name of the constructor, used to apply terminfo. If the source is synthetic, terminfo is not applied.

• binders : Syntax

  For handler use. The inductive uses it for the binders to the constructor.

• type? : Option Syntax

  For handler use. The inductive command uses it for the resulting type for the constructor.

def Lean.Elab.Command.instInhabitedCtorView.default : CtorView

Equations

• Lean.Elab.Command.instInhabitedCtorView.default = { ref := default, modifiers := default, declName := default, declId := default, binders := default, type? := default }

@[implicit_reducible]

instance Lean.Elab.Command.instInhabitedCtorView : Inhabited CtorView

Equations

• Lean.Elab.Command.instInhabitedCtorView = { default := Lean.Elab.Command.instInhabitedCtorView.default }

structure Lean.Elab.Command.ComputedFieldView : Type

• ref : Syntax
• modifiers : Syntax
• fieldId : Name
• type : Term
• matchAlts : TSyntax `Lean.Parser.Term.matchAlts

structure Lean.Elab.Command.InductiveView : Type

A view for generic inductive types.

• ref : Syntax
• declId : Syntax
• modifiers : Modifiers
• isClass : Bool
• allowIndices : Bool

  Whether the command should allow indices (like inductive) or not (like structure).

• allowSortPolymorphism : Bool

  Whether the command supports creating inductive types that can be polymorphic across both Prop and Type _. If false, then either the universe must be Prop or it must be of the form Type _.

• shortDeclName : Name
• declName : Name
• levelNames : List Name
• binders : Syntax
• type? : Option Syntax
• ctors : Array CtorView
• computedFields : Array ComputedFieldView
• derivingClasses : Array DerivingClassView
• docString? : Option (TSyntax `Lean.Parser.Command.docComment × Bool)

  The declaration docstring, and whether it's Verso

• isCoinductive : Bool

@[implicit_reducible]

instance Lean.Elab.Command.instInhabitedInductiveView : Inhabited InductiveView

Equations

• Lean.Elab.Command.instInhabitedInductiveView = { default := Lean.Elab.Command.instInhabitedInductiveView.default }

def Lean.Elab.Command.instInhabitedInductiveView.default : InductiveView

Equations

• One or more equations did not get rendered due to their size.

structure Lean.Elab.Command.PreElabHeaderResult : Type

Elaborated header for an inductive type before fvars for each inductive are added to the local context.

• view : InductiveView
• levelNames : List Name
• numParams : Nat
• type : Expr
• origParams : Array Expr

  The parameters in the header's initial local context. Used for adding fvar alias terminfo.

@[implicit_reducible]

instance Lean.Elab.Command.instInhabitedPreElabHeaderResult : Inhabited PreElabHeaderResult

Equations

• Lean.Elab.Command.instInhabitedPreElabHeaderResult = { default := Lean.Elab.Command.instInhabitedPreElabHeaderResult.default }

def Lean.Elab.Command.instInhabitedPreElabHeaderResult.default : PreElabHeaderResult

Equations

• Lean.Elab.Command.instInhabitedPreElabHeaderResult.default = { view := default, levelNames := default, numParams := default, type := default, origParams := default }

structure Lean.Elab.Command.ElabHeaderResultextends Lean.Elab.Command.PreElabHeaderResult : Type

The elaborated header with the indFVar registered for this inductive type.

• view : InductiveView
• levelNames : List Name
• numParams : Nat
• type : Expr
• origParams : Array Expr
• indFVar : Expr

def Lean.Elab.Command.instInhabitedElabHeaderResult.default : ElabHeaderResult

Equations

• Lean.Elab.Command.instInhabitedElabHeaderResult.default = { toPreElabHeaderResult := default, indFVar := default }

@[implicit_reducible]

instance Lean.Elab.Command.instInhabitedElabHeaderResult : Inhabited ElabHeaderResult

Equations

• Lean.Elab.Command.instInhabitedElabHeaderResult = { default := Lean.Elab.Command.instInhabitedElabHeaderResult.default }

structure Lean.Elab.Command.InductiveElabStep3 : Type

An intermediate step for mutual inductive elaboration. See InductiveElabDescr

• finalize : TermElabM Unit

  Finalize the inductive type, after they are all added to the environment, after auxiliary definitions are added, and after computed fields are registered. The levelParams, params, and replaceIndFVars arguments of prefinalize are still valid here.

structure Lean.Elab.Command.InductiveElabStep2 : Type

An intermediate step for mutual inductive elaboration. See InductiveElabDescr.

• ctors : List Constructor

  The constructors produced by InductiveElabStep1.

• collectUsedFVars : StateRefT' IO.RealWorld CollectFVars.State MetaM Unit

  Function to collect additional fvars that might be missed by the constructors. It is permissible to include fvars that do not exist in the local context (structure for example includes its field fvars).

• collectExtraHeaderLMVars : StateRefT' IO.RealWorld CollectLevelMVars.State MetaM Unit

  Function to collect additional level metavariables that are header-like (e.g. in extends clauses in structure). Header-like level metavariables can be promoted to be level parameters.

• checkUniverses (numParams : Nat) (u : Level) : TermElabM Unit

  Function to check universes and provide a custom error. (structure uses this to do checks per field to give nicer messages.)

• finalizeTermElab : TermElabM Unit

  Step to do final term elaboration error reporting, done immediately after universe levels are fully elaborated, but before the final level checks.

• prefinalize (levelParams : List Name) (params : Array Expr) (replaceIndFVars : Expr → MetaM Expr) : TermElabM InductiveElabStep3

  Like finalize, but occurs before afterTypeChecking attributes.

def Lean.Elab.Command.instInhabitedInductiveElabStep2.default : InductiveElabStep2

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

instance Lean.Elab.Command.instInhabitedInductiveElabStep2 : Inhabited InductiveElabStep2

Equations

• Lean.Elab.Command.instInhabitedInductiveElabStep2 = { default := Lean.Elab.Command.instInhabitedInductiveElabStep2.default }

structure Lean.Elab.Command.InductiveElabStep1 : Type

An intermediate step for mutual inductive elaboration. See InductiveElabDescr.

• view : InductiveView
• elabCtors (rs : Array ElabHeaderResult) (r : ElabHeaderResult) (params : Array Expr) : TermElabM InductiveElabStep2

def Lean.Elab.Command.instInhabitedInductiveElabStep1.default : InductiveElabStep1

Equations

• Lean.Elab.Command.instInhabitedInductiveElabStep1.default = { view := default, elabCtors := default }

@[implicit_reducible]

instance Lean.Elab.Command.instInhabitedInductiveElabStep1 : Inhabited InductiveElabStep1

Equations

• Lean.Elab.Command.instInhabitedInductiveElabStep1 = { default := Lean.Elab.Command.instInhabitedInductiveElabStep1.default }

structure Lean.Elab.Command.InductiveElabDescr : Type

Descriptor for a command processor that elaborates an inductive type.

Elaboration occurs in the following steps:

• Every command has its mkInductiveView evaluated, producing InductiveViews and callbacks for the next steps (all recorded in InductiveElabStep1).
• Each InductiveView gets elaborated, creating ElabHeaderResults, and the local contexts are unified into a single one with a consistent set of parameters between each inductive.
• Each callback is called to elaborate each inductives' constructors and some additional callbacks (all recorded in InductiveElabStep2).
• Fvars are collected from the constructors and from the InductiveStep2.collectUsedFVars callbacks. This is used to compute the final set of scoped variables that should be used as additional parameters.
• Universe levels are checked. Commands can give custom errors using InductiveStep2.checkUniverses.
• Elaboration of constructors is finalized, with additional tasks done by each InductiveStep2.finalizeTermElab.
• The inductive family is added to the environment and is checked by the kernel.
• Attributes and other finalization activities are performed, including those defined by InductiveStep2.prefinalize and InductiveStep3.finalize.

• mkInductiveView : Modifiers → Syntax → TermElabM InductiveElabStep1

def Lean.Elab.Command.instInhabitedInductiveElabDescr.default : InductiveElabDescr

Equations

• Lean.Elab.Command.instInhabitedInductiveElabDescr.default = { mkInductiveView := default }

@[implicit_reducible]

instance Lean.Elab.Command.instInhabitedInductiveElabDescr : Inhabited InductiveElabDescr

Equations

• Lean.Elab.Command.instInhabitedInductiveElabDescr = { default := Lean.Elab.Command.instInhabitedInductiveElabDescr.default }

opaque Lean.Elab.Command.inductiveElabAttr : KeyedDeclsAttribute InductiveElabDescr

Registers an inductive type elaborator for the given syntax node kind.

Commands registered using this attribute are allowed to be used together in mutual blocks with other inductive type commands. This attribute is mostly used internally for inductive and structure.

An inductive type elaborator should have type Lean.Elab.Command.InductiveElabDescr.

def Lean.Elab.Command.isInductiveCommand {m : Type → Type} [Monad m] [MonadEnv m] (stx : Syntax) : m Bool

Returns true if the syntax participates in the mutual inductive elaborator. These do not need to be commands. In fact inductive and structure are registered on the Lean.Parser.Command.inductive and Lean.Parser.Command.structure syntaxes.

Equations

• Lean.Elab.Command.isInductiveCommand stx = do let env ← Lean.getEnv pure !(Lean.Elab.Command.inductiveElabAttr.getEntries env stx.getKind).isEmpty

def Lean.Elab.Command.mkInductiveView (modifiers : Modifiers) (stx : Syntax) : TermElabM InductiveElabStep1

Initializes the elaborator associated to the given syntax.

Equations

• One or more equations did not get rendered due to their size.

def Lean.Elab.Command.checkValidInductiveModifier {m : Type → Type} [Monad m] [MonadError m] (modifiers : Modifiers) : m Unit

Equations

• One or more equations did not get rendered due to their size.

def Lean.Elab.Command.checkValidCtorModifier {m : Type → Type} [Monad m] [MonadError m] (modifiers : Modifiers) : m Unit

Equations

• One or more equations did not get rendered due to their size.

def Lean.Elab.Command.withCtorRef {m : Type → Type} {α : Type} [Monad m] [MonadRef m] (views : Array InductiveView) (ctorName : Name) (k : m α) : m α

Executes k using the Syntax reference associated with constructor ctorName.

Equations

• One or more equations did not get rendered due to their size.

def Lean.Elab.Command.InductiveView.withTypeRef {m : Type → Type} {α : Type} [Monad m] [MonadRef m] (view : InductiveView) (k : m α) : m α

Runs k with the resulting type as the ref or, if that's not available, with the view's ref.

Equations

• view.withTypeRef k = Lean.withRef view.ref (Lean.withRef? view.type? k)

def Lean.Elab.Command.withViewTypeRef {m : Type → Type} {α : Type} [Monad m] [MonadRef m] (views : Array InductiveView) (k : m α) : m α

Equations

• One or more equations did not get rendered due to their size.

def Lean.Elab.Command.withExplicitToImplicit {α : Type} (xs : Array Expr) (k : TermElabM α) : TermElabM α

Execute k with updated binder information for xs. Any x that is explicit becomes implicit.

Equations

• One or more equations did not get rendered due to their size.

Index-to-parameter promotion

The basic convention for inductive is that the binders before the colon in a type former correspond to the type parameters, and the pi types after the colon correspond to the indices.

Indices that are fixed across all occurrences of the type former can potentially be promoted to be parameters instead. Motivations:

• The recursor is more efficient (though the induction principle might be more rigid than expected; this is solved by generalizing variables)
• The inferred universe level of the inductive type might decrease.

Recall that when an inductive type declaration Declaration.inductDecl is sent to the kernel, every constructor is provided its full type, including the inductive parameters. The inductDecl declaration itself specifies how many parameters there are (nparams), and the first nparams parameters of a constructor are the parameters for the inductive type.

The function fixedIndicesToParams determines by how much nparams can be increased without resulting in an invalid inductive type declaration. We say the indices that become parameters this way are promoted. Only a prefix of indices can be promoted because of this.

Note that it currently does not do any constructor parameter reordering. If the parameter for an index does not appear in the correct position in a constructor for it to be an inductive type parameter, it is not promoted. That said, the inductive command itself has some capacity for reordering in Lean.Elab.Command.reorderCtorArgs.

Promotion can be disabled with set_option inductive.autoPromoteIndices false.

Level metavariable inference

Terminology: Given the inductive type former I : ... -> Sort u, we call Sort u the resulting universe of I and u the resulting universe level of I.

After constructor elaboration, inductive type declarations still often have universe level metavariables. They may appear anywhere:

• in types of inductive parameters/indices
• in the resulting universe level of the type former
• and in constructor fields (i.e. those parameters after inductive parameters).

The resulting universe has a strong bearing on what sort of inference we can do:

• If it is Prop, the type is an inductive predicate, and it is impredicative, meaning fields can come from any universe.
• Otherwise, fields are subject to the universe level inequality (described further below).

There are certain cases where we choose to infer Prop for the resulting universe. Recall that an inductive type is a syntactic subsingleton if any two terms of that type are definitionally equal. Syntactic subsingletons can eliminate into Type, hence can be pattern matched. This justifies setting the resulting universe Prop if a type is "obviously" meant to be an inductive predicate. Roughly, we say an inductive type is "obviously" meant to be an inductive predicate if the type is not recursive, has exactly one constructor, the constructor has at least one field, and every field is Prop. See isPropCandidate for further explanation.

From now on, we will talk only about inductive types in Type or above.

There are a number of considerations for inference:

• The universe level inequality. If u is the resulting universe level, then for every field f : fty of every constructor, we must have v ≤ u, where fty : Sort v.

• Avoiding Sort polymorphism. We say a type is Sort-polymorphic if, depending on the values of level parameters, the resulting universe can be both Prop and Type _. These usually cannot eliminate into Prop unless they are syntactic subsingletons, so we wish to avoid Sort polymorphism to avoid users' unpleasant surprises. We do this by adding the constraint 1 ≤ u.

• Using the minimal resulting universe if it exists. If u has metavariables, then we do not want u to be unnecessarily large. We want to find the minimal levels to assign to the metavariables subject to the above constraints. However: we only entertain unique solutions. We report ambiguous situations to the user. Furthermore, this is best-effort. Users can always provide an explicit resulting universe. (We can also detect certain situations where this procedure computes a universe that is likely larger than what could be if it had been explicitly provided before constructor elaboration.)

• Avoiding inferring proof fields. If v is the universe level for a constructor field, then we avoid assigning metavariable in v to anything that could potentially give Prop fields or Sort polymorphism. To do this, we use the weak constraint 1 ≤w v. Definition:

  • 1 ≤w p and 1 ≤w k for all parameters p and constants k.
  • 1 ≤w succ v for all levels v
  • 1 ≤w max a b and 1 ≤w imax a b iff 1 ≤w a and 1 ≤w b
  • 1 ≤w ?v iff 1 ≤ ?v. The effect is that 1 ≤w v resolves to a set of 1 ≤ ?v metavariable constraints. This is more conservative than it needs to be, but it is uniform and avoids SAT-like reasoning; effectively, inference analyzes each metavariable, independently from one another.

• Using the unique universe for fields if it exists, preferring non-constant solutions. Uniqueness is with respect to the set of universe level expressions, not universe levels. Examples:

  • ?a ≤ 0 ~~~> ?a = 0 is the unique solution. (Note: this can lead to unpleasant surprises, where a field unexpectedly becomes a proof. We currently do nothing about this. It would require more careful global analysis.)
  • ?a ≤ 1 ~~~> either ?a = 0 or ?a = 1, so underconstrained unless we have 1 ≤ ?a, in which case ?a = 1 is the unique solution.
  • ?a ≤ v with v a level parameter ~~~> syntactically have ?a = 0 and ?a = v as solutions, but prefer ?a = v since it is non-constant, and is the unique solution.
  • ?a ≤ v + 1 with v a level parameter ~~~> syntactically have ?a = 0, ?a = 1, ?a = v, and ?a = v + 1 as solutions, with ?a = v and ?a = v + 1 preferred. This is underconstrained, unless we have 1 ≤ ?a, in which case ?a = v + 1 is the unique solution.
  • ?a ≤ max v₁ v₂ with v₁ and v₂ level parameters ~~~> syntactically have ?a = 0, ?a = v₁, ?a = v₂, and ?a = max v₁ v₂ as solutions, with the latter three preferred. This is underconstrained.

  The heuristic for preferring non-constant solutions comes from user examples.

Collecting the constraints, these rules imply the only assignments considered are:

• if 0 ≤ ?a ≤ k and k = 0 then assign ?a := 0
• if 0 ≤ ?a ≤ p + k and k = 0 then assign ?a := p
• if 1 ≤ ?a ≤ k and k = 1 then assign ?a := 1
• if 1 ≤ ?a ≤ p + k and k = 1 then assign ?a := p + 1

Otherwise we do not assign ?a, and we leave it to the "declaration has metavariables" error to report it.

There are also other considerations to make the inference more effective. If the resulting universe is of the form max ?m 1, we want to isolate ?m as the metavariable to solve for. The simplifyResultingUniverse u procedure is a heavy hammer to reliably extract the "generic part" of the resulting universe level that is suitable for the inference procedures, without the fragility of matching on specific patterns. It gives a universe level u' ≤ u such that u' and u are equivalent "at infinity", which means u' = u for all sufficiently high assignments of the parameters or metavariables. In general, we only attempt solving for any universe levels at each stage if u' is of the form r + k where r is a parameter, metavariable, or zero, since in other cases solutions are not unique.

High-level inference algorithm:

• Solve for the metavariable in the resulting universe level.
• Solve for metavariables in constructor fields, if possible.
• Turn level metavariables in the type former (and from collectExtraHeaderLMVars) into level parameters.
• Report unsolved level metavariables.

Examples are in tests/lean/run/inductive_univ.lean.

def Lean.Elab.Command.replaceIndFVars (numParams : Nat) (oldFVars calls : Array Expr) : Expr → Expr

Equations

• One or more equations did not get rendered due to their size.

def Lean.Elab.Command.updateViewWithFunctorName (view : InductiveView) : InductiveView

Equations

• One or more equations did not get rendered due to their size.

def Lean.Elab.Command.InductiveViewToCoinductiveElab (e : InductiveElabStep1) : CoinductiveElabData

Equations

• One or more equations did not get rendered due to their size.

def Lean.Elab.Command.elabInductives (inductives : Array (Modifiers × Syntax)) : CommandElabM Unit

Equations

• One or more equations did not get rendered due to their size.

def Lean.Elab.Command.elabInductive (modifiers : Modifiers) (stx : Syntax) : CommandElabM Unit

Equations

• Lean.Elab.Command.elabInductive modifiers stx = Lean.Elab.Command.elabInductives #[(modifiers, stx)]

def Lean.Elab.Command.isMutualInductive {m : Type → Type} [Monad m] [MonadEnv m] (stx : Syntax) : m Bool

Returns true if all elements of the mutual block (Lean.Parser.Command.mutual) are inductive declarations.

Equations

• Lean.Elab.Command.isMutualInductive stx = Array.allM (fun (elem : Lean.Syntax) => Lean.Elab.Command.isInductiveCommand elem[1]) stx[1].getArgs

def Lean.Elab.Command.elabMutualInductive (elems : Array Syntax) : CommandElabM Unit

Elaborates a mutual block, assuming the commands satisfy Lean.Elab.Command.isMutualInductive.

Equations

• One or more equations did not get rendered due to their size.