3.4.Β Inductive TypesπŸ”—

Inductive types are the primary means of introducing new types to Lean. While universes and functions are built-in primitives that could not be added by users, every other type in Lean is either an inductive type or defined in terms of universes, functions, and inductive types. Inductive types are specified by their type constructors and their constructors; their other properties are derived from these. Each inductive type has a single type constructor, which may take both universe parameters and ordinary parameters. Inductive types may have any number of constructors; these constructors introduce new values whose types are headed by the inductive type's type constructor.

Based on the type constructor and the constructors for an inductive type, Lean derives a recursor. Logically, recursors represent induction principles or elimination rules; computationally, they represent primitive recursive computations. The termination of recursive functions is justified by translating them into uses of the recursors, so Lean's kernel only needs to perform type checking of recursor applications, rather than including a separate termination analysis. Lean additionally produces a number of helper constructions based on the recursor,The term recursor is always used, even for non-recursive types. which are used elsewhere in the system.

Structures are a special case of inductive types that have exactly one constructor. When a structure is declared, Lean generates helpers that enable additional language features to be used with the new structure.

This section describes the specific details of the syntax used to specify both inductive types and structures, the new constants and definitions in the environment that result from inductive type declarations, and the run-time representation of inductive types' values in compiled code.

3.4.1.Β Inductive Type DeclarationsπŸ”—

syntax
command ::= ...
    | `declModifiers` is the collection of modifiers on a declaration:
* a doc comment `/-- ... -/`
* a list of attributes `@[attr1, attr2]`
* a visibility specifier, `private` or `protected`
* `noncomputable`
* `unsafe`
* `partial` or `nonrec`

All modifiers are optional, and have to come in the listed order.

`nestedDeclModifiers` is the same as `declModifiers`, but attributes are printed
on the same line as the declaration. It is used for declarations nested inside other syntax,
such as inductive constructors, structure projections, and `let rec` / `where` definitions. declModifiers
      In Lean, every concrete type other than the universes
and every type constructor other than dependent arrows
is an instance of a general family of type constructions known as inductive types.
It is remarkable that it is possible to construct a substantial edifice of mathematics
based on nothing more than the type universes, dependent arrow types, and inductive types;
everything else follows from those.
Intuitively, an inductive type is built up from a specified list of constructors.
For example, `List Ξ±` is the list of elements of type `Ξ±`, and is defined as follows:
```
inductive List (Ξ± : Type u) where
| nil
| cons (head : Ξ±) (tail : List Ξ±)
```
A list of elements of type `Ξ±` is either the empty list, `nil`,
or an element `head : Ξ±` followed by a list `tail : List Ξ±`.
See [Inductive types](https://lean-lang.org/theorem_proving_in_lean4/inductive_types.html)
for more information.
inductive `declId` matches `foo` or `foo.{u,v}`: an identifier possibly followed by a list of universe names declId `optDeclSig` matches the signature of a declaration with optional type: a list of binders and then possibly `: type` optDeclSig where
        (| `declModifiers` is the collection of modifiers on a declaration:
* a doc comment `/-- ... -/`
* a list of attributes `@[attr1, attr2]`
* a visibility specifier, `private` or `protected`
* `noncomputable`
* `unsafe`
* `partial` or `nonrec`

All modifiers are optional, and have to come in the listed order.

`nestedDeclModifiers` is the same as `declModifiers`, but attributes are printed
on the same line as the declaration. It is used for declarations nested inside other syntax,
such as inductive constructors, structure projections, and `let rec` / `where` definitions. declModifiers ident `optDeclSig` matches the signature of a declaration with optional type: a list of binders and then possibly `: type` optDeclSig)*
      (deriving ident,*)?

Declares a new inductive type. The meaning of the declModifiers is as described in the section on declaration modifiers.

After declaring an inductive type, its type constructor, constructors, and recursor are present in the environment. New inductive types extend Lean's core logicβ€”they are not encoded or represented by some other already-present data. Inductive type declarations must satisfy a number of well-formedness requirements to ensure that the logic remains consistent.

The first line of the declaration, from Lean.Parser.Command.inductive : commandinductive to Lean.Parser.Command.inductive : commandwhere, specifies the new type constructor's name and type. If a type signature for the type constructor is provided, then its result type must be a universe, but the parameters do not need to be types. If no signature is provided, then Lean will attempt to infer a universe that's just big enough to contain the resulting type. In some situations, this process may fail to find a minimal universe or fail to find one at all, necessitating an annotation.

The constructor specifications follow Lean.Parser.Command.inductive : commandwhere. Constructors are not mandatory, as constructorless inductive types such as False and Empty are perfectly sensible. Each constructor specification begins with a vertical bar ('|', Unicode 'VERTICAL BAR' (U+007c)), declaration modifiers, and a name. The name is a raw identifier. A declaration signature follows the name. The signature may specify any parameters, modulo the well-formedness requirements for inductive type declarations, but the return type in the signature must be a saturated application of the type constructor of the inductive type being specified. If no signature is provided, then the constructor's type is inferred by inserting sufficient implicit parameters to construct a well-formed return type.

The new inductive type's name is defined in the current namespace. Each constructor's name is in the inductive type's namespace.

3.4.1.1.Β Parameters and IndicesπŸ”—

Type constructors may take two kinds of arguments: parameters and indices. Parameters must be used consistently in the entire definition; all occurrences of the type constructor in each constructor in the declaration must take precisely the same argument. Indices may vary among the occurrences of the type constructor. All parameters must precede all indices in the type constructor's signature.

Parameters that occur prior to the colon (':') in the type constructor's signature are considered parameters to the entire inductive type declaration. They are always parameters that must be uniform throughout the type's definition. Generally speaking, parameters that occur after the colon are indices that may vary throughout the definition of the type. However, if the option inductive.autoPromoteIndices is true, then syntactic indices that could have been parameters are made into parameters. An index could have been a parameter if all of its type dependencies are themselves parameters and it is used uniformly as an uninstantiated variable in all occurrences of the inductive type's type constructor in all constructors.

πŸ”—option
inductive.autoPromoteIndices

Default value: true

Promote indices to parameters in inductive types whenever possible.

Indices can be seen as defining a family of types. Each choice of indices selects a type from the family, which has its own set of available constructors. Type constructors with indices are said to specify indexed families of types.

3.4.1.2.Β Example Inductive TypesπŸ”—

A constructorless type

Vacant is an empty inductive type, equivalent to Lean's Empty type:

inductive Vacant : Type where

Empty inductive types are not useless; they can be used to indicate unreachable code.

A constructorless proposition

No is a false proposition, equivalent to Lean's False:

inductive No : Prop where
A unit type

One is equivalent to Lean's Unit type:

inductive One where | one

It is an example of an inductive type in which the signatures have been omitted for both the type constructor and the constructor. Lean assigns One to Type:

One : Type#check One 
One : Type

The constructor is named One.one, because constructor names are the type constructor's namespace. Because One expects no arguments, the signature inferred for One.one is:

One.one : One#check One.one 
One.one : One
A true proposition

Yes is equivalent to Lean's True proposition:

inductive Yes : Prop where | intro

Unlike One, the new inductive type Yes is specified to be in the Prop universe.

Yes : Prop#check Yes 
Yes : Prop

The signature inferred for Yes.intro is:

Yes.intro : Yes#check Yes.intro 
Yes.intro : Yes
A type with parameter and index

An EvenOddList Ξ± b is a list where Ξ± is the type of the data stored in the list and b is true when there are an even number of entries:

inductive EvenOddList (Ξ± : Type u) : Bool β†’ Type u where | nil : EvenOddList Ξ± true | cons : Ξ± β†’ EvenOddList Ξ± isEven β†’ EvenOddList Ξ± (not isEven)

This example is well typed because there are two entries in the list:

example : EvenOddList String true := .cons "a" (.cons "b" .nil)

This example is not well typed because there are three entries in the list:

example : EvenOddList String true := type mismatch EvenOddList.cons "a" (EvenOddList.cons "b" (EvenOddList.cons "c" EvenOddList.nil)) has type EvenOddList String !!!true : Type but is expected to have type EvenOddList String true : Type.cons "a" (.cons "b" (.cons "c" .nil)) 
type mismatch
  EvenOddList.cons "a" (EvenOddList.cons "b" (EvenOddList.cons "c" EvenOddList.nil))
has type
  EvenOddList String !!!true : Type
but is expected to have type
  EvenOddList String true : Type

In this declaration, Ξ± is a parameter, because it is used consistently in all occurrences of EvenOddList. b is an index, because different Bool values are used for it at different occurrences.

Parameters before and after the colon

In this example, both parameters are specified before the colon in Either's signature.

inductive Either (Ξ± : Type u) (Ξ² : Type v) : Type (max u v) where | left : Ξ± β†’ Either Ξ± Ξ² | right : Ξ± β†’ Either Ξ± Ξ²

In this version, there are two types named Ξ± that might not be identical:

inductive Either' (Ξ± : Type u) (Ξ² : Type v) : Type (max u v) where inductive datatype parameter mismatch Ξ± expected α✝| left : {Ξ± : Type u} β†’ {Ξ² : Type v} β†’ Ξ± β†’ Either' Ξ± Ξ² | right : Ξ± β†’ Either' Ξ± Ξ² 
inductive datatype parameter mismatch
  Ξ±
expected
  α✝

Placing the parameters after the colon results in parameters that can be instantiated by the constructors:

inductive Either'' : Type u β†’ Type v β†’ Type (max u v) where | left : {Ξ± : Type u} β†’ {Ξ² : Type v} β†’ Ξ± β†’ Either'' Ξ± Ξ² | right : Ξ± β†’ Either'' Ξ± Ξ²

Either''.right's type parameters are discovered via Lean's ordinary rules for automatic implicit parameters.

3.4.1.3.Β Anonymous Constructor SyntaxπŸ”—

If an inductive type has just one constructor, then this constructor is eligible for anonymous constructor syntax. Instead of writing the constructor's name applied to its arguments, the explicit arguments can be enclosed in angle brackets ('⟨' and '⟩', Unicode MATHEMATICAL LEFT ANGLE BRACKET (U+0x27e8) and MATHEMATICAL RIGHT ANGLE BRACKET (U+0x27e9)) and separated with commas. This works in both pattern and expression contexts. Providing arguments by name or converting all implicit parameters to explicit parameters with @ requires using the ordinary constructor syntax.

Anonymous constructors

The type AtLeastOne Ξ± is similar to List Ξ±, except there's always at least one element present:

inductive AtLeastOne (Ξ± : Type u) : Type u where | mk : Ξ± β†’ Option (AtLeastOne Ξ±) β†’ AtLeastOne Ξ±

Anonymous constructor syntax can be used to construct them:

def oneTwoThree : AtLeastOne Nat := ⟨1, some ⟨2, some ⟨3, none⟩⟩⟩

and to match against them:

def AtLeastOne.head : AtLeastOne Ξ± β†’ Ξ± | ⟨x, _⟩ => x

Equivalently, traditional constructor syntax could have been used:

def oneTwoThree' : AtLeastOne Nat := .mk 1 (some (.mk 2 (some (.mk 3 none)))) def AtLeastOne.head' : AtLeastOne Ξ± β†’ Ξ± | .mk x _ => x

3.4.1.4.Β Deriving InstancesπŸ”—

The optional Lean.Parser.Command.inductive : commandderiving clause of an inductive type declaration can be used to derive instances of type classes. Please refer to the section on instance deriving for more information.

3.4.2.Β Structure DeclarationsπŸ”—

syntax
command ::= ...
    | `declModifiers` is the collection of modifiers on a declaration:
* a doc comment `/-- ... -/`
* a list of attributes `@[attr1, attr2]`
* a visibility specifier, `private` or `protected`
* `noncomputable`
* `unsafe`
* `partial` or `nonrec`

All modifiers are optional, and have to come in the listed order.

`nestedDeclModifiers` is the same as `declModifiers`, but attributes are printed
on the same line as the declaration. It is used for declarations nested inside other syntax,
such as inductive constructors, structure projections, and `let rec` / `where` definitions. declModifiers
      structure `declId` matches `foo` or `foo.{u,v}`: an identifier possibly followed by a list of universe names declId bracketedBinder*
          (extends term,*)? (: term)? where
        (`declModifiers` is the collection of modifiers on a declaration:
* a doc comment `/-- ... -/`
* a list of attributes `@[attr1, attr2]`
* a visibility specifier, `private` or `protected`
* `noncomputable`
* `unsafe`
* `partial` or `nonrec`

All modifiers are optional, and have to come in the listed order.

`nestedDeclModifiers` is the same as `declModifiers`, but attributes are printed
on the same line as the declaration. It is used for declarations nested inside other syntax,
such as inductive constructors, structure projections, and `let rec` / `where` definitions. declModifiers ident ::)?
        structFields
      (deriving ident,*)?

Declares a new structure type.

Structures are inductive types that have only a single constructor and no indices. In exchange for these restrictions, Lean generates code for structures that offers a number of conveniences: projection functions are generated for each field, an additional constructor syntax based on field names rather than positional arguments is available, a similar syntax may be used to replace the values of certain named fields, and structures may extend other structures. Just like other inductive types, structures may be recursive; they are subject to the same restrictions regarding strict positivity. Structures do not add any expressive power to Lean; all of their features are implemented in terms of code generation.

3.4.2.1.Β Structure ParametersπŸ”—

Just like ordinary inductive type declarations, the header of the structure declaration contains a signature that may specify both parameters and a resulting universe. Structures may not define indexed families.

3.4.2.2.Β FieldsπŸ”—

Each field of a structure declaration corresponds to a parameter of the constructor. Auto-implicit arguments are inserted in each field separately, even if their names coincide, and the fields become constructor parameters that quantify over types.

Auto-implicit parameters in structure fields

The structure MyStructure contains a field whose type is an auto-implicit parameter:

structure MyStructure where field1 : Ξ± field2 : Ξ±

The type constructor MyStructure takes two universe parameters:

MyStructure.{u, v} : Type (max u v)

The resulting type is in Type rather than Sort because the constructor fields quantify over types in Sort. In particular, both fields in its constructor MyStructure.mk take an implicit type parameter:

MyStructure.mk.{u, v} (field1 : {Ξ± : Sort u} β†’ Ξ±) (field2 : {Ξ± : Sort v} β†’ Ξ±) : MyStructure.{u,v}

For each field, a projection function is generated that extracts the field's value from the underlying type's constructor. This function is in the structure's name's namespace. Structure field projections are handled specially by the elaborator (as described in the section on structure inheritance), which performs extra steps beyond looking up a namespace. When field types depend on prior fields, the types of the dependent projection functions are written in terms of earlier projections, rather than explicit pattern matching.

Dependent projection types

The structure ArraySized contains a field whose type depends on both a structure parameter and an earlier field:

structure ArraySized (Ξ± : Type u) (length : Nat) where array : Array Ξ± size_eq_length : array.size = length

The signature of the projection function size_eq_length takes the structure type's parameter as an implicit parameter and refers to the earlier field using the corresponding projection:

ArraySized.size_eq_length.{u} {Ξ± : Type u} {length : Nat} (self : ArraySized Ξ± length) : self.array.size = length

Structure fields may have default values, specified with :=. These values are used if no explicit value is provided.

Default values

An adjacency list representation of a graph can be represented as an array of lists of Nat. The size of the array indicates the number of vertices, and the outgoing edges from each vertex are stored in the array at the vertex's index. Because the default value #[] is provided for the field adjacency, the empty graph Graph.empty can be constructed without providing any field values.

structure Graph where adjacency : Array (List Nat) := #[] def Graph.empty : Graph := {}

Structure fields may additionally be accessed via their index, using dot notation. Fields are numbered beginning with 1.

3.4.2.3.Β Structure ConstructorsπŸ”—

Structure constructors may be explicitly named by providing the constructor name and :: prior to the fields. If no name is explicitly provided, then the constructor is named mk in the structure type's namespace. Declaration modifiers may additionally be provided along with an explicit constructor name.

Non-default constructor name

The structure Palindrome contains a string and a proof that the string is the same when reversed:

structure Palindrome where ofString :: text : String is_palindrome : text.data.reverse = text.data

Its constructor is named Palindrome.ofString, rather than Palindrome.mk.

Modifiers on structure constructor

The structure NatStringBimap maintains a finite bijection between natural numbers and strings. It consists of a pair of maps, such that the keys each occur as values exactly once in the other map. Because the constructor is private, code outside the defining module can't construct new instances and must use the provided API, which maintains the invariants of the type. Additionally, providing the default constructor name explicitly is an opportunity to attach a documentation comment to the constructor.

structure NatStringBimap where /-- Build a finite bijection between some natural numbers and strings -/ private mk :: natToString : Std.HashMap Nat String stringToNat : Std.HashMap String Nat def NatStringBimap.empty : NatStringBimap := ⟨{}, {}⟩ def NatStringBimap.insert (nat : Nat) (string : String) (map : NatStringBimap) : Option NatStringBimap := if map.natToString.contains nat || map.stringToNat.contains string then none else some (NatStringBimap.mk (map.natToString.insert nat string) (map.stringToNat.insert string nat))

Because structures are represented by single-constructor inductive types, their constructors can be invoked or matched against using anonymous constructor syntax. Additionally, structures may be constructed or matched against using structure instance notation, which includes the names of the fields together with values for them.

syntaxStructure Instances
term ::= ...
    | Structure instance. `{ x := e, ... }` assigns `e` to field `x`, which may be
inherited. If `e` is itself a variable called `x`, it can be elided:
`fun y => { x := 1, y }`.
A *structure update* of an existing value can be given via `with`:
`{ point with x := 1 }`.
The structure type can be specified if not inferable:
`{ x := 1, y := 2 : Point }`.
{ structInstField,*
        (: term)? }

Constructs a value of a constructor type given values for named fields. Field specifiers may take two forms:

structInstField ::= ...
    | structInstLVal := term
structInstField ::= ...
    | ident

A structInstLVal is a field name (an identifier), a field index (a natural number), or a term in square brackets, followed by a sequence of zero or more subfields. Subfields are either a field name or index preceded by a dot, or a term in square brackets.

This syntax is elaborated to applications of structure constructors. The values provided for fields are by name, and they may be provided in any order. The values provided for subfields are used to initialize fields of constructors of structures that are themselves found in fields. Terms in square brackets are not allowed when constructing a structure; they are used in structure updates.

Field specifiers that do not contain := are field abbreviations. In this context, the identifier f is an abbreviation for f := f; that is, the value of f in the current scope is used to initialize the field f.

Every field that does not have a default value must be provided. If a tactic is specified as the default argument, then it is run at elaboration time to construct the argument's value.

In a pattern context, field names are mapped to patterns that match the corresponding projection, and field abbreviations bind a pattern variable that is the field's name. Default arguments are still present in patterns; if a pattern does not specify a value for a field with a default value, then the pattern only matches the default.

The optional type annotation allows the structure type to be specified in contexts where it is not otherwise determined.

Patterns and default values

The structure AugmentedIntList contains a list together with some extra information, which is empty if omitted:

structure AugmentedIntList where list : List Int augmentation : String := ""

When testing whether the list is empty, the function isEmpty is also testing whether the augmentation field is empty, because the omitted field's default value is also used in pattern contexts:

def AugmentedIntList.isEmpty : AugmentedIntList β†’ Bool | {list := []} => true | _ => false false#eval {list := [], augmentation := "extra" : AugmentedIntList}.isEmpty 
false
syntax
term ::= ...
    | Structure instance. `{ x := e, ... }` assigns `e` to field `x`, which may be
inherited. If `e` is itself a variable called `x`, it can be elided:
`fun y => { x := 1, y }`.
A *structure update* of an existing value can be given via `with`:
`{ point with x := 1 }`.
The structure type can be specified if not inferable:
`{ x := 1, y := 2 : Point }`.
{term with
        structInstField,*
        (: term)?}

Updates a value of a constructor type. The term that precedes the Lean.Parser.Term.structInst : termStructure instance. `{ x := e, ... }` assigns `e` to field `x`, which may be inherited. If `e` is itself a variable called `x`, it can be elided: `fun y => { x := 1, y }`. A *structure update* of an existing value can be given via `with`: `{ point with x := 1 }`. The structure type can be specified if not inferable: `{ x := 1, y := 2 : Point }`. with clause is expected to have a structure type; it is the value that is being updated. A new instance of the structure is created in which every field not specified is copied from the value that is being updated, and the specified fields are replaced with their new values. When updating a structure, array values may also be replaced by including the index to be updated in square brackets. This updating does not require that the index expression be in bounds for the array, and out-of-bounds updates are discarded.

Updating arrays

Updating structures may use array indices as well as projection names. Updates at indices that are out of bounds are ignored:

structure AugmentedIntArray where array : Array Int augmentation : String := "" deriving Repr def one : AugmentedIntArray := {array := #[1]} def two : AugmentedIntArray := {one with array := #[1, 2]} def two' : AugmentedIntArray := {two with array[0] := 2} def two'' : AugmentedIntArray := {two with array[99] := 3} ({ array := #[1], augmentation := "" }, { array := #[1, 2], augmentation := "" }, { array := #[2, 2], augmentation := "" }, { array := #[1, 2], augmentation := "" })#eval (one, two, two', two'') 
({ array := #[1], augmentation := "" },
 { array := #[1, 2], augmentation := "" },
 { array := #[2, 2], augmentation := "" },
 { array := #[1, 2], augmentation := "" })

Values of structure types may also be declared using Lean.Parser.Command.declValEqns : commandwhere, followed by definitions for each field. This may only be used as part of a definition, not in an expression context.

where for structures

The product type in Lean is a structure named Prod. Products can be defined using their projections:

def location : Float Γ— Float where fst := 22.807 snd := -13.923

3.4.2.4.Β Structure InheritanceπŸ”—

Structures may be declared as extending other structures using the optional Lean.Parser.Command.structure : commandextends clause. The resulting structure type has all of the fields of all of the parent structure types. If the parent structure types have overlapping field names, then all overlapping field names must have the same type. If the overlapping fields have different default values, then the default value from the last parent structure that includes the field is used. New default values in the child structure take precedence over default values from the parent structures.

When the new structure extends existing structures, the new structure's constructor takes the existing structure's information as additional arguments. Typically, this is in the form of a constructor parameter for each parent structure type. If the parents' fields overlap, however, then the subset of non-overlapping fields from one or more of the parents is included instead to prevent duplicating field information.

There is no subtyping relation between a parent structure type and its children. Even if structure B extends structure A, a function expecting an A will not accept a B. However, conversion functions are generated that convert a structure into each of its parents. These conversion functions are in the child structure's namespace, and their name is the parent structure's name preceded by to.

Structure type inheritance with overlapping fields

In this example, a Textbook is a Book that is also an AcademicWork:

structure Book where title : String author : String structure AcademicWork where author : String discipline : String structure Textbook extends Book, AcademicWork Textbook.toBook (self : Textbook) : Book#check Textbook.toBook

Because the field author occurs in both Book and AcademicWork, the constructor Textbook.mk does not take both parents as arguments. Its signature is:

Textbook.mk (toBook : Book) (discipline : String) : Textbook

The conversion functions are:

Textbook.toBook (self : Textbook) : BookTextbook.toAcademicWork (self : Textbook) : AcademicWork

The latter combines the author field of the included Book with the unbundled Discipline field, and is equivalent to:

def toAcademicWork (self : Textbook) : AcademicWork := let .mk book discipline := self let .mk _title author := book .mk author discipline

The resulting structure's projections can be used as if its fields are simply the union of the parents' fields. The Lean elaborator automatically generates an appropriate projection when fields are used. Likewise, the field-based initialization and structure update notations hide the details of the encoding of inheritance. The encoding is, however, visible when using the constructor's name, when using anonymous constructor syntax, or when referring to fields by their index rather than their name.

Field Indices and Structure Inheritancestructure Pair (Ξ± : Type u) where fst : Ξ± snd : Ξ± deriving Repr structure Triple (Ξ± : Type u) extends Pair Ξ± where thd : Ξ± deriving Repr def coords : Triple Nat := {fst := 17, snd := 2, thd := 95}

Evaluating the first field index of coords yields the underlying Pair, rather than the contents of the field fst:

{ fst := 17, snd := 2 }#eval coords.1 
{ fst := 17, snd := 2 }

The elaborator translates coords.fst into coords.toPair.fst.

No structure subtyping

Given these definitions of even numbers, even prime numbers, and a concrete even prime:

structure EvenNumber where val : Nat isEven : 2 ∣ val := by decide structure EvenPrime extends EvenNumber where notOne : val β‰  1 := by decide isPrime : βˆ€ n, n ≀ val β†’ n ∣ val β†’ n = 1 ∨ n = val def two : EvenPrime where val := 2 isPrime := ⊒ βˆ€ (n : Nat), n ≀ { val := 2, isEven := β‹― }.val β†’ n ∣ { val := 2, isEven := β‹― }.val β†’ n = 1 ∨ n = { val := 2, isEven := β‹― }.val n✝:Nata✝¹:n✝ ≀ { val := 2, isEven := β‹― }.vala✝:n✝ ∣ { val := 2, isEven := β‹― }.val⊒ n✝ = 1 ∨ n✝ = { val := 2, isEven := β‹― }.val n✝:Nata✝¹:n✝ ≀ 2a✝:n✝ ∣ 2⊒ n✝ = 1 ∨ n✝ = 2 repeat' (a✝:0 ∣ 2⊒ 0 = 1 ∨ 0 = 2) all_goals All goals completed! πŸ™ def printEven (num : EvenNumber) : IO Unit := IO.print num.val

it is a type error to apply printEven directly to two:

printEven sorry : IO Unit#check printEven application type mismatch printEven two argument two has type EvenPrime : Type but is expected to have type EvenNumber : Typetwo 
application type mismatch
  printEven two
argument
  two
has type
  EvenPrime : Type
but is expected to have type
  EvenNumber : Type

because values of type EvenPrime are not also values of type EvenNumber.

3.4.3.Β Logical ModelπŸ”—

3.4.3.1.Β RecursorsπŸ”—

Every inductive type is equipped with a recursor. The recursor is completely determined by the signatures of the type constructor and the constructors. Recursors have function types, but they are primitive and are not definable using fun.

3.4.3.1.1.Β Recursor TypesπŸ”—

The recursor takes the following parameters:

The inductive type's parameters

Because parameters are consistent, they can be abstracted over the entire recursor

The motive

The motive determines the type of an application of the recursor. The motive is a function whose arguments are the type's indices and an instance of the type with these indices instantiated. The specific universe for the type that the motive determines depends on the inductive type's universe and the specific constructorsβ€”see the section on subsingleton elimination for details.

A case for each constructor

For each constructor, the recursor expects a function that satisfies the motive for an arbitrary application of the constructor. Each case abstracts over all of the constructor's parameters. If the constructor's parameter's type is the inductive type itself, then the case additionally takes a parameter whose type is the motive applied to that parameter's valueβ€”this will receive the result of recursively processing the recursive parameter.

The target

Finally, the recursor takes an instance of the type as an argument, along with any index values.

The result type of the recursor is the motive applied to these indices and the target.

The recursor for Bool

Bool's recursor Bool.rec has the following parameters:

  • The motive computes a type in any universe, given a Bool.

  • There are cases for both constructors, in which the motive is satisfied for both false and true.

  • The target is some Bool.

The return type is the motive applied to the target.

Bool.rec.{u} {motive : Bool β†’ Sort u} (false : motive false) (true : motive true) (t : Bool) : motive t
The recursor for List

List's recursor List.rec has the following parameters:

  • The parameter Ξ± comes first, because the parameter and the cases need to refer to it

  • The motive computes a type in any universe, given a List Ξ±. There is no connection between the universe levels u and v.

  • There are cases for both constructors:

    • The motive is satisfied for List.nil

    • The motive should be satisfiable for any application of List.cons, given that it is satisfiable for the tail. The extra parameter motive tail is because tail's type is a recursive occurrence of List.

  • The target is some List Ξ±.

Once again, the return type is the motive applied to the target.

List.rec.{u, v} {Ξ± : Type v} {motive : List Ξ± β†’ Sort u} (nil : motive []) (cons : (head : Ξ±) β†’ (tail : List Ξ±) β†’ motive tail β†’ motive (head :: tail)) (t : List Ξ±) : motive t
Recursor with parameters and indices

Given the definition of EvenOddList:

inductive EvenOddList (Ξ± : Type u) : Bool β†’ Type u where | nil : EvenOddList Ξ± true | cons : Ξ± β†’ EvenOddList Ξ± isEven β†’ EvenOddList Ξ± (not isEven)

The recursor EvenOddList.rec is very similar to that for List. The difference comes from the presence of the index:

  • The motive now abstracts over any arbitrary choice of index.

  • The case for nil applies the motive to nil's index value true.

  • The case for cons abstracts over the index value used in its recursive occurrence, and instantiates the motive with its negation.

  • The target additionally abstracts over an arbitrary choice of index.

EvenOddList.rec.{u, v} {Ξ± : Type v} {motive : (isEven : Bool) β†’ EvenOddList Ξ± isEven β†’ Sort u} (nil : motive true EvenOddList.nil) (cons : {isEven : Bool} β†’ (head : Ξ±) β†’ (tail : EvenOddList Ξ± isEven) β†’ motive isEven tail β†’ motive (!isEven) (EvenOddList.cons head tail)) : {isEven : Bool} β†’ (t : EvenOddList Ξ± isEven) β†’ motive isEven t

When using a predicate (that is, a function that returns a Prop) for the motive, recursors express induction. The cases for non-recursive constructors are the base cases, and the additional arguments supplied to constructors with recursive arguments are the induction hypotheses.

3.4.3.1.1.1.Β Subsingleton EliminationπŸ”—

Proofs in Lean are computationally irrelevant. In other words, having been provided with some proof of a proposition, it should be impossible for a program to check which proof it has received. This is reflected in the types of recursors for inductively defined propositions or predicates. For these types, if there's more than one potential proof of the theorem then the motive may only return another Prop. If the type is structured such that there's only at most one proof anyway, then the motive may return a type in any universe. A proposition that has at most one inhabitant is called a subsingleton. Rather than obligating users to prove that there's only one possible proof, a conservative syntactic approximation is used to check whether a proposition is a subsingleton. Propositions that fulfill both of the following requirements are considered to be subsingletons:

  • There is at most one constructor.

  • Each of the constructor's parameter types is either a Prop, a parameter, or an index.

True is a subsingleton

True is a subsingleton because it has one constructor, and this constructor has no parameters. Its recursor has the following signature:

True.rec.{u} {motive : True β†’ Sort u} (intro : motive True.intro) (t : True) : motive t
False is a subsingleton

False is a subsingleton because it has no constructors. Its recursor has the following signature:

False.rec.{u} (motive : False β†’ Sort u) (t : False) : motive t

Note that the motive is an explicit parameter. This is because it is not mentioned in any further parameters' types, so it could not be solved by unification.

And is a subsingleton

And is a subsingleton because it has one constructor, and both of the constructor's parameters' types are propositions. Its recursor has the following signature:

And.rec.{u} {a b : Prop} {motive : a ∧ b β†’ Sort u} (intro : (left : a) β†’ (right : b) β†’ motive (And.intro left right)) (t : a ∧ b) : motive t
Or is not a subsingleton

Or is not a subsingleton because it has more than one constructor. Its recursor has the following signature:

Or.rec {a b : Prop} {motive : a ∨ b β†’ Prop} (inl : βˆ€ (h : a), motive (.inl h)) (inr : βˆ€ (h : b), motive (.inr h)) (t : a ∨ b) : motive t

The motive's type indicates that Or.rec can only be used to produce proofs. A proof of a disjunction can be used to prove something else, but there's no way for a program to inspect which of the two disjuncts was true and used for the proof.

Eq is a subsingleton

Eq is a subsingleton because it has just one constructor, Eq.refl. This constructor instantiates Eq's index with a parameter value, so all arguments are parameters:

Eq.refl.{u} {Ξ± : Sort u} (x : Ξ±) : Eq x x

Its recursor has the following signature:

Eq.rec.{u, v} {Ξ± : Sort v} {x : Ξ±} {motive : (y : Ξ±) β†’ x = y β†’ Sort u} (refl : motive x (.refl x)) {y : Ξ±} (t : x = y) : motive y t

This means that proofs of equality can be used to rewrite the types of non-propositions.

3.4.3.1.2.Β ReductionπŸ”—

In addition to adding new constants to the logic, inductive type declarations also add new reduction rules. These rules govern the interaction between recursors and constructors; specifically recursors that have constructors as their targets. This form of reduction is called ΞΉ-reduction (iota reduction).

When the recursor's target is a constructor with no recursive parameters, the recursor application reduces to an application of the constructor's case to the constructor's arguments. If there are recursive parameters, then these arguments to the case are found by applying the recursor to the recursive occurrence.

3.4.3.2.Β Well-Formedness RequirementsπŸ”—

Inductive type declarations are subject to a number of well-formedness requirements. These requirements ensure that Lean remains consistent as a logic when it is extended with the inductive type's new rules. They are conservative: there exist potential inductive types that do not undermine consistency, but that these requirements nonetheless reject.

3.4.3.2.1.Β Universe Levels

Type constructors of inductive types must either inhabit a universe or a function type whose return type is a universe. Each constructor must inhabit a function type that returns a saturated application of the inductive type. If the inductive type's universe is Prop, then there are no further restrictions on universes, because Prop is impredicative. If the universe is not Prop, then the following must hold for each parameter to the constructor:

  • If the constructor's parameter is a parameter (in the sense of parameters vs indices) of the inductive type, then this parameter's type may be no larger than the type constructor's universe.

  • All other constructor parameters must be smaller than the type constructor's universe.

Universes, constructors, and parameters

Either is in the greater of its arguments' universes, because both are parameters to the inductive type:

inductive Either (Ξ± : Type u) (Ξ² : Type v) : Type (max u v) where | inl : Ξ± β†’ Either Ξ± Ξ² | inr : Ξ² β†’ Either Ξ± Ξ²

CanRepr is in a larger universe than the constructor parameter Ξ±, because Ξ± is not one of the inductive type's parameters:

inductive CanRepr : Type (u + 1) where | mk : (Ξ± : Type u) β†’ [Repr Ξ±] β†’ CanRepr

Constructorless inductive types may be in universes smaller than their parameters:

inductive Spurious (Ξ± : Type 5) : Type 0 where

It would, however, be impossible to add a constructor to Spurious without changing its levels.

3.4.3.2.2.Β Strict PositivityπŸ”—

All occurrences of the type being defined in the types of the parameters of the constructors must be in strictly positive positions. A position is strictly positive if it is not in a function's argument type (no matter how many function types are nested around it) and it is not an argument of any expression other than type constructors of inductive types. This restriction rules out unsound inductive type definitions, at the cost of also ruling out some unproblematic ones.

Non-strictly-positive inductive types

The type Bad would make Lean inconsistent if it were not rejected:

(kernel) arg #1 of 'Bad.bad' has a non positive occurrence of the datatypes being declaredinductive Bad where | bad : (Bad β†’ Bad) β†’ Bad 
(kernel) arg #1 of 'Bad.bad' has a non positive occurrence of the datatypes being declared

This is because it would be possible to write a circular argument that proves False under the assumption Bad. Bad.bad is rejected because the constructor's parameter has type Bad β†’ Bad, which is a function type in which Bad occurs as an argument type.

This declaration of a fixed point operator is rejected, because Fix occurs as an argument to f:

(kernel) arg #2 of 'Fix.fix' contains a non valid occurrence of the datatypes being declaredinductive Fix (f : Type u β†’ Type u) where | fix : f (Fix f) β†’ Fix f 
(kernel) arg #2 of 'Fix.fix' contains a non valid occurrence of the datatypes being declared

Fix.fix is rejected because f is not a type constructor of an inductive type, but Fix itself occurs as an argument to it. In this case, Fix is also sufficient to construct a type equivalent to Bad:

def Bad : Type := Fix fun t => t β†’ t

3.4.3.2.3.Β Prop vs TypeπŸ”—

Lean rejects universe-polymorphic types that could not, in practice, be used polymorphically. This could arise if certain instantiations of the universe parameters would cause the type itself to be a Prop. If this type is not a subsingleton, then is recursor can only target propositions (that is, the motive must return a Prop). These types only really make sense as Props themselves, so the universe polymorphism is probably a mistake. Because they are largely useless, Lean's inductive type elaborator has not been designed to support these types.

When such universe-polymorphic inductive types are indeed subsingletons, it can make sense to define them. Lean's standard library defines PUnit and PEmpty. To define a subsingleton that can inhabit Prop or a Type, set the option bootstrap.inductiveCheckResultingUniverse to false.

πŸ”—option
bootstrap.inductiveCheckResultingUniverse

Default value: true

by default the inductive/structure commands report an error if the resulting universe is not zero, but may be zero for some universe parameters. Reason: unless this type is a subsingleton, it is hardly what the user wants since it can only eliminate into Prop. In the Init package, we define subsingletons, and we use this option to disable the check. This option may be deleted in the future after we improve the validator

Overly-universe-polymorphic Bool

Defining a version of Bool that can be in any universe is not allowed:

inductive PBool : invalid universe polymorphic resulting type, the resulting universe is not 'Prop', but it may be 'Prop' for some parameter values: Sort u Possible solution: use levels of the form 'max 1 _' or '_ + 1' to ensure the universe is of the form 'Type _'.Sort u where | true | false 
invalid universe polymorphic resulting type, the resulting universe is not 'Prop', but it may be 'Prop' for some parameter values:
  Sort u
Possible solution: use levels of the form 'max 1 _' or '_ + 1' to ensure the universe is of the form 'Type _'.

3.4.3.3.Β Constructions for Termination CheckingπŸ”—

In addition to the type constructor, constructors, and recursors that Lean's core type theory prescribes for inductive types, Lean constructs a number of useful helpers. First, the equation compiler (which translates recursive functions with pattern matching in to applications of recursors) makes use of these additional constructs:

  • recOn is a version of the recursor in which the target is prior to the cases for each constructor.

  • casesOn is a version of the recursor in which the target is prior to the cases for each constructor, and recursive arguments do not yield induction hypotheses. It expresses case analysis rather than primitive recursion.

  • below computes a type that, for some motive, expresses that all inhabitants of the inductive type that are subtrees of the target satisfy the motive. It transforms a motive for induction or primitive recursion into a motive for strong recursion or strong induction.

  • brecOn is a version of the recursor in which below is used to provide access to all subtrees, rather than just immediate recursive parameters. It represents strong induction.

  • noConfusion is a general statement from which injectivity and disjointness of constructors can be derived.

  • noConfusionType is the motive used for noConfusion that determines what the consequences of two constructors being equal would be. For separate constructors, this is False; if both constructors are the same, then the consequence is the equality of their respective parameters.

For well-founded recursion, it is frequently useful to have a generic notion of size available. This is captured in the SizeOf class.

πŸ”—type class
SizeOf.{u} (Ξ± : Sort u) : Sort (max 1 u)

SizeOf is a typeclass automatically derived for every inductive type, which equips the type with a "size" function to Nat. The default instance defines each constructor to be 1 plus the sum of the sizes of all the constructor fields.

This is used for proofs by well-founded induction, since every field of the constructor has a smaller size than the constructor itself, and in many cases this will suffice to do the proof that a recursive function is only called on smaller values. If the default proof strategy fails, it is recommended to supply a custom size measure using the termination_by argument on the function definition.

Instance Constructor

SizeOf.mk.{u}

Methods

sizeOf : Ξ± β†’ Nat

The "size" of an element, a natural number which decreases on fields of each inductive type.

3.4.4.Β Run-Time RepresentationπŸ”—

An inductive type's run-time representation depends both on how many constructors it has, how many arguments each constructor takes, and whether these arguments are relevant.

3.4.4.1.Β ExceptionsπŸ”—

Not every inductive type is represented as indicated hereβ€”some inductive types have special support from the Lean compiler:

  • The fixed-width integer types UInt8, ..., UInt64, and USize are represented by the C types uint8_t, ..., uint64_t, and size_t, respectively.

  • Char is represented by uint32_t

  • Float is represented by double

  • An enum inductive type of at least 2 and at most 2^{32} constructors, each of which has no parameters, is represented by the first type of uint8_t, uint16_t, uint32_t that is sufficient to assign a unique value to each constructor. For example, the type Bool is represented by uint8_t, with values 0 for false and 1 for true.

  • Decidable Ξ± is represented the same way as Bool

  • Nat is represented by lean_object *. Its run-time value is either a pointer to an opaque arbitrary-precision integer object or, if the lowest bit of the β€œpointer” is 1 (checked by lean_is_scalar), an encoded unboxed natural number (lean_box/lean_unbox).

3.4.4.2.Β RelevanceπŸ”—

Types and proofs have no run-time representation. That is, if an inductive type is a Prop, then its values are erased prior to compilation. Similarly, all theorem statements and types are erased. Types with run-time representations are called relevant, while types without run-time representations are called irrelevant.

Types are irrelevant

Even though List.cons has the following signature, which indicates three parameters:

List.cons.{u} {Ξ± : Type u} : Ξ± β†’ List Ξ± β†’ List Ξ±

its run-time representation has only two, because the type argument is run-time irrelevant.

Proofs are irrelevant

Even though Fin.mk has the following signature, which indicates three parameters:

Fin.mk {n : Nat} (val : Nat) : val < n β†’ Fin n

its run-time representation has only two, because the proof is erased.

In most cases, irrelevant values simply disappear from compiled code. However, in cases where some representation is required (such as when they are arguments to polymorphic constructors), they are represented by a trivial value.

3.4.4.3.Β Trivial WrappersπŸ”—

If an inductive type has exactly one constructor, and that constructor has exactly one run-time relevant parameter, then the inductive type is represented identically to its parameter.

Zero-Overhead Subtypes

The structure Subtype bundles an element of some type with a proof that it satisfies a predicate. Its constructor takes four arguments, but three of them are irrelevant:

Subtype.mk.{u} {Ξ± : Sort u} {p : Ξ± β†’ Prop} (val : Ξ±) (property : p val) : Subtype p

Thus, subtypes impose no runtime overhead in compiled code, and are represented identically to the type of the val field.

3.4.4.4.Β Other Inductive TypesπŸ”—

If an inductive type doesn't fall into one of the categories above, then its representation is determined by its constructors. Constructors without relevant parameters are represented by their index into the list of constructors, as unboxed unsigned machine integers (scalars). Constructors with relevant parameters are represented as an object with a header, the constructor's index, an array of pointers to other objects, and then arrays of scalar fields sorted by their types. The header tracks the object's reference count and other necessary bookkeeping.

Recursive functions are compiled as they are in most programming languages, rather than by using the inductive type's recursor. Elaborating recursive functions to recursors serves to provide reliable termination evidence, not executable code.

3.4.4.4.1.Β FFIπŸ”—

From the perspective of C, these other inductive types are represented by lean_object *. Each constructor is stored as a lean_ctor_object, and lean_is_ctor will return true. A lean_ctor_object stores the constructor index in its header, and the fields are stored in the m_objs portion of the object. Lean assumes that sizeof(size_t) == sizeof(void*)β€”while this is not guaranteed by C, the Lean run-time system contains an assertion that fails if this is not the case.

The memory order of the fields is derived from the types and order of the fields in the declaration. They are ordered as follows:

  • Non-scalar fields stored as lean_object *

  • Fields of type USize

  • Other scalar fields, in decreasing order by size

Within each group the fields are ordered in declaration order. Warning: Trivial wrapper types still count toward a field being treated as non-scalar for this purpose.

  • To access fields of the first kind, use lean_ctor_get(val, i) to get the ith non-scalar field.

  • To access USize fields, use lean_ctor_get_usize(val, n+i) to get the ith USize field and n is the total number of fields of the first kind.

  • To access other scalar fields, use lean_ctor_get_uintN(val, off) or lean_ctor_get_usize(val, off) as appropriate. Here off is the byte offset of the field in the structure, starting at n*sizeof(void*) where n is the number of fields of the first two kinds.

For example, a structure such as

structure S where ptr_1 : Array Nat usize_1 : USize sc64_1 : UInt64 ptr_2 : { x : UInt64 // x > 0 } -- wrappers don't count as scalars sc64_2 : Float -- `Float` is 64 bit sc8_1 : Bool sc16_1 : UInt16 sc8_2 : UInt8 sc64_3 : UInt64 usize_2 : USize ptr_3 : Char -- trivial wrapper around `UInt32` sc32_1 : UInt32 sc16_2 : UInt16

would get re-sorted into the following memory order:

  • S.ptr_1 - lean_ctor_get(val, 0)

  • S.ptr_2 - lean_ctor_get(val, 1)

  • S.ptr_3 - lean_ctor_get(val, 2)

  • S.usize_1 - lean_ctor_get_usize(val, 3)

  • S.usize_2 - lean_ctor_get_usize(val, 4)

  • S.sc64_1 - lean_ctor_get_uint64(val, sizeof(void*)*5)

  • S.sc64_2 - lean_ctor_get_float(val, sizeof(void*)*5 + 8)

  • S.sc64_3 - lean_ctor_get_uint64(val, sizeof(void*)*5 + 16)

  • S.sc32_1 - lean_ctor_get_uint32(val, sizeof(void*)*5 + 24)

  • S.sc16_1 - lean_ctor_get_uint16(val, sizeof(void*)*5 + 28)

  • S.sc16_2 - lean_ctor_get_uint16(val, sizeof(void*)*5 + 30)

  • S.sc8_1 - lean_ctor_get_uint8(val, sizeof(void*)*5 + 32)

  • S.sc8_2 - lean_ctor_get_uint8(val, sizeof(void*)*5 + 33)

3.4.5.Β Mutual Inductive TypesπŸ”—

Inductive types may be mutually recursive. Mutually recursive definitions of inductive types are specified by defining the types in a mutual ... end block.

Mutually Defined Inductive Types

The type EvenOddList in a prior example used a Boolean index to select whether the list in question should have an even or odd number of elements. This distinction can also be expressed by the choice of one of two mutually inductive types EvenList and OddList:

mutual inductive EvenList (Ξ± : Type u) : Type u where | nil : EvenList Ξ± | cons : Ξ± β†’ OddList Ξ± β†’ EvenList Ξ± inductive OddList (Ξ± : Type u) : Type u where | cons : Ξ± β†’ EvenList Ξ± β†’ OddList Ξ± end example : EvenList String := .cons "x" (.cons "y" .nil) example : OddList String := .cons "x" (.cons "y" (.cons "z" .nil)) example : OddList String := .cons "x" (.cons "y" invalid dotted identifier notation, unknown identifier `OddList.nil` from expected type OddList String.nil) 
invalid dotted identifier notation, unknown identifier `OddList.nil` from expected type
  OddList String

3.4.5.1.Β RequirementsπŸ”—

The inductive types declared in a mutual block are considered as a group; they must collectively satisfy generalized versions of the well-formedness criteria for non-mutually-recursive inductive types. This is true even if they could be defined without the mutual block, because they are not in fact mutually recursive.

3.4.5.1.1.Β Mutual DependenciesπŸ”—

Each type constructor's signature must be able to be elaborated without reference to the other inductive types in the mutual group. In other words, the inductive types in the mutual group may not take each other as arguments. The constructors of each inductive type may mention the other type constructors in the group in their parameter types, with restrictions that are a generalization of those for recursive occurrences in non-mutual inductive types.

Mutual inductive type constructors may not mention each other

These inductive types are not accepted by Lean:

mutual inductive FreshList (Ξ± : Type) (r : Ξ± β†’ Ξ± β†’ Prop) : Type where | nil : FreshList Ξ± r | cons (x : Ξ±) (xs : FreshList Ξ± r) (fresh : Fresh r x xs) invalid mutually inductive types, binder annotation mismatch at parameter 'Ξ±'inductive Fresh (r : Ξ± β†’ unknown identifier 'FreshList'FreshList Ξ± β†’ Prop) : Ξ± β†’ unknown identifier 'FreshList'FreshList Ξ± r β†’ Prop where | nil : Fresh r x .nil | cons : r x y β†’ (f : Fresh r x ys) β†’ Fresh r x (.cons y ys f) end

The type constructors may not refer to the other type constructors in the mutual group, so FreshList is not in scope in the type constructor of Fresh:

unknown identifier 'FreshList'

3.4.5.1.2.Β Parameters Must MatchπŸ”—

All inductive types in the mutual group must have the same parameters. Their indices may differ.

Differing numbers of parameters

Even though Both and OneOf are not mutually recursive, they are declared in the same mutual block and must therefore have identical parameters:

mutual inductive Both (Ξ± : Type u) (Ξ² : Type v) where | mk : Ξ± β†’ Ξ² β†’ Both Ξ± Ξ² invalid inductive type, number of parameters mismatch in mutually inductive datatypesinductive Optional (Ξ± : Type u) where | none | some : Ξ± β†’ Optional Ξ± end 
invalid inductive type, number of parameters mismatch in mutually inductive datatypes
Differing parameter types

Even though Many and OneOf are not mutually recursive, they are declared in the same mutual block and must therefore have identical parameters. They both have exactly one parameter, but Many's parameter is not necessarily in the same universe as Optional's:

mutual inductive Many (Ξ± : Type) : Type u where | nil : Many Ξ± | cons : Ξ± β†’ Many Ξ± β†’ Many Ξ± invalid mutually inductive types, parameter 'Ξ±' has type Type u : Type (u + 1) but is expected to have type Type : Type 1inductive Optional (Ξ± : Type u) where | none | some : Ξ± β†’ Optional Ξ± end 
invalid mutually inductive types, parameter 'Ξ±' has type
  Type u : Type (u + 1)
but is expected to have type
  Type : Type 1

3.4.5.1.3.Β Universe LevelsπŸ”—

The universe levels of each inductive type in a mutual group must obey the same requirements as non-mutually-recursive inductive types. Additionally, all the inductive types in a mutual group must be in the same universe, which implies that their constructors are similarly limited with respect to their parameters' universes.

Universe mismatch

These mutually-inductive types are a somewhat complicated way to represent run-length encoding of a list:

mutual inductive RLE : List Ξ± β†’ Type where | nil : RLE [] | run (x : Ξ±) (n : Nat) : n β‰  0 β†’ PrefixRunOf n x xs ys β†’ RLE ys β†’ RLE xs inductive PrefixRunOf : Nat β†’ Ξ± β†’ List Ξ± β†’ List Ξ± β†’ Type where | zero (noMore : Β¬βˆƒzs, xs = x :: zs := by simp) : PrefixRunOf 0 x xs xs | succ : PrefixRunOf n x xs ys β†’ PrefixRunOf (n + 1) x (x :: xs) ys end example : RLE [1, 1, 2, 2, 3, 1, 1, 1] := .run 1 2 (⊒ 2 β‰  0 All goals completed! πŸ™) (.succ (.succ .zero)) <| .run 2 2 (⊒ 2 β‰  0 All goals completed! πŸ™) (.succ (.succ .zero)) <| .run 3 1 (⊒ 1 β‰  0 All goals completed! πŸ™) (.succ .zero) <| .run 1 3 (⊒ 3 β‰  0 All goals completed! πŸ™) (.succ (.succ (.succ (.zero)))) <| .nil

Specifying PrefixRunOf as a Prop would be sensible, but it cannot be done because the types would be in different universes:

mutual inductive RLE : List Ξ± β†’ Type where | nil : RLE [] | run (x : Ξ±) (n : Nat) : n β‰  0 β†’ PrefixRunOf n x xs ys β†’ RLE ys β†’ RLE xs invalid mutually inductive types, resulting universe mismatch, given Prop expected type Typeinductive PrefixRunOf : Nat β†’ Ξ± β†’ List Ξ± β†’ List Ξ± β†’ Prop where | zero (noMore : Β¬βˆƒzs, xs = x :: zs := by simp) : PrefixRunOf 0 x xs xs | succ : PrefixRunOf n x xs ys β†’ PrefixRunOf (n + 1) x (x :: xs) ys end 
invalid mutually inductive types, resulting universe mismatch, given
  Prop
expected type
  Type

This particular property can be expressed by separately defining the well-formedness condition and using a subtype:

def RunLengths Ξ± := List (Ξ± Γ— Nat) def NoRepeats : RunLengths Ξ± β†’ Prop | [] => True | [_] => True | (x, _) :: ((y, n) :: xs) => x β‰  y ∧ NoRepeats ((y, n) :: xs) def RunsMatch : RunLengths Ξ± β†’ List Ξ± β†’ Prop | [], [] => True | (x, n) :: xs, ys => ys.take n = List.replicate n x ∧ RunsMatch xs (ys.drop n) | _, _ => False def NonZero : RunLengths Ξ± β†’ Prop | [] => True | (_, n) :: xs => n β‰  0 ∧ NonZero xs structure RLE (xs : List Ξ±) where rle : RunLengths Ξ± noRepeats : NoRepeats rle runsMatch : RunsMatch rle xs nonZero : NonZero rle example : RLE [1, 1, 2, 2, 3, 1, 1, 1] where rle := [(1, 2), (2, 2), (3, 1), (1, 3)] noRepeats := ⊒ NoRepeats [(1, 2), (2, 2), (3, 1), (1, 3)] All goals completed! πŸ™ runsMatch := ⊒ RunsMatch [(1, 2), (2, 2), (3, 1), (1, 3)] [1, 1, 2, 2, 3, 1, 1, 1] All goals completed! πŸ™ nonZero := ⊒ NonZero [(1, 2), (2, 2), (3, 1), (1, 3)] All goals completed! πŸ™

3.4.5.1.4.Β PositivityπŸ”—

Each inductive type that is defined in the mutual group may occur only strictly positively in the types of the parameters of the constructors of all the types in the group. In other words, in the type of each parameter to each constructor in all the types of the group, none of the type constructors in the group occur to the left of any arrows, and none of them occur in argument positions unless they are an argument to an inductive type's type constructor.

Mutual strict positivity

In the following mutual group, Tm occurs in a negative position in the argument to Binding.scope:

mutual (kernel) arg #1 of 'Binding.scope' has a non positive occurrence of the datatypes being declaredinductive Tm where | app : Tm β†’ Tm β†’ Tm | lam : Binding β†’ Tm inductive Binding where | scope : (Tm β†’ Tm) β†’ Binding end

Because Tm is part of the same mutual group, it must occur only strictly positively in the arguments to the constructors of Binding. It occurs, however, negatively:

(kernel) arg #1 of 'Binding.scope' has a non positive occurrence of the datatypes being declared
Nested positions

The definitions of LocatedStx and Stx satisfy the positivity condition because the recursive occurrences are not to the left of any arrows and, when they are arguments, they are arguments to inductive type constructors.

mutual inductive LocatedStx where | mk (line col : Nat) (val : Stx) inductive Stx where | atom (str : String) | node (kind : String) (args : List LocatedStx) end

3.4.5.2.Β RecursorsπŸ”—

Mutual inductive types are provided with primitive recursors, just like non-mutually-defined inductive types. These recursors take into account that they must process the other types in the group, and thus will have a motive for each inductive type. Because all inductive types in the mutual group are required to have identical parameters, the recursors still take the parameters first, abstracting them over the motives and the rest of the recursor. Additionally, because the recursor must process the group's other types, it will require cases for each constructor of each of the types in the group. The actual dependency structure between the types is not taken into account; even if an additional motive or constructor case is not really required due to there being fewer mutual dependencies than there could be, the generated recursor still requires them.

Even and oddmutual inductive Even : Nat β†’ Prop where | zero : Even 0 | succ : Odd n β†’ Even (n + 1) inductive Odd : Nat β†’ Prop where | succ : Even n β†’ Odd (n + 1) end Even.rec {motive_1 : (a : Nat) β†’ Even a β†’ Prop} {motive_2 : (a : Nat) β†’ Odd a β†’ Prop} (zero : motive_1 0 Even.zero) (succ : {n : Nat} β†’ (a : Odd n) β†’ motive_2 n a β†’ motive_1 (n + 1) (Even.succ a)) : (βˆ€ {n : Nat} (a : Even n), motive_1 n a β†’ motive_2 (n + 1) (Odd.succ a)) β†’ βˆ€ {a : Nat} (t : Even a), motive_1 a tOdd.rec {motive_1 : (a : Nat) β†’ Even a β†’ Prop} {motive_2 : (a : Nat) β†’ Odd a β†’ Prop} (zero : motive_1 0 Even.zero) (succ : βˆ€ {n : Nat} (a : Odd n), motive_2 n a β†’ motive_1 (n + 1) (Even.succ a)) : (βˆ€ {n : Nat} (a : Even n), motive_1 n a β†’ motive_2 (n + 1) (Odd.succ a)) β†’ βˆ€ {a : Nat} (t : Odd a), motive_2 a t
Spuriously mutual types

The types Two and Three are defined in a mutual block, even though they do not refer to each other:

mutual inductive Two (Ξ± : Type) where | mk : Ξ± β†’ Ξ± β†’ Two Ξ± inductive Three (Ξ± : Type) where | mk : Ξ± β†’ Ξ± β†’ Ξ± β†’ Three Ξ± end

Two's recursor, Two.rec, nonetheless requires a motive and a case for Three:

Two.rec.{u} {Ξ± : Type} {motive_1 : Two Ξ± β†’ Sort u} {motive_2 : Three Ξ± β†’ Sort u} (mk : (a a_1 : Ξ±) β†’ motive_1 (Two.mk a a_1)) : ((a a_1 a_2 : Ξ±) β†’ motive_2 (Three.mk a a_1 a_2)) β†’ (t : Two Ξ±) β†’ motive_1 t

3.4.5.3.Β Run-Time RepresentationπŸ”—

Mutual inductive types are represented identically to non-mutual inductive types in compiled code and in the runtime. The restrictions on mutual inductive types exist to ensure Lean's consistency as a logic, and do not impact compiled code.