Skip to content

fix: more consistent terminology for inductive types #504

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
merged 1 commit into from
Jun 30, 2025
Merged

fix: more consistent terminology for inductive types #504

Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
40 changes: 20 additions & 20 deletions Manual/Language/InductiveTypes/LogicalModel.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -38,7 +38,7 @@ tag := "recursor-types"
The recursor takes the following parameters:
: The inductive type's {tech}[parameters]

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

: The {deftech}_motive_

Expand All @@ -48,23 +48,23 @@ The recursor takes the following parameters:

For each constructor, the recursor expects a function that satisfies the motive for an arbitrary application of the constructor.
Each minor premise 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.
If the constructor's parameter's type is the inductive type itself, then the minor premise 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 {deftech}_major premise_, or 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 result type of the recursor is the motive applied to these indices and the major premise.
:::

:::example "The recursor for {lean}`Bool`"
{lean}`Bool`'s recursor {name}`Bool.rec` has the following parameters:

* The motive computes a type in any universe, given a {lean}`Bool`.
* There are cases for both constructors, in which the motive is satisfied for both {lean}`false` and {lean}`true`.
* The target is some {lean}`Bool`.
* There are minor premises for both constructors, in which the motive is satisfied for both {lean}`false` and {lean}`true`.
* The major premise is some {lean}`Bool`.

The return type is the motive applied to the target.
The return type is the motive applied to the major premise.

```signature
Bool.rec.{u} {motive : Bool → Sort u}
Expand All @@ -82,15 +82,15 @@ Bool.rec.{u} {motive : Bool → Sort u}
axiom α.{u} : Type u
```

* The parameter {lean}`α` comes first, because the parameter and the cases need to refer to it
* The parameter {lean}`α` comes first, because the motive, minor premises, and major premise need to refer to it.
* The motive computes a type in any universe, given a {lean}`List α`. There is no connection between the universe levels `u` and `v`.
* There are cases for both constructors:
* There are minor premises for both constructors:
- The motive is satisfied for {name}`List.nil`
- The motive should be satisfiable for any application of {name}`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 {name}`List`.
* The target is some {lean}`List α`.
* The major premise is some {lean}`List α`.
:::

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

```signature
List.rec.{u, v} {α : Type v} {motive : List α → Sort u}
Expand All @@ -114,9 +114,9 @@ inductive EvenOddList (α : Type u) : Bool → Type u where
The recursor {name}`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 {name EvenOddList.nil}`nil` applies the motive to {name EvenOddList.nil}`nil`'s index value `true`.
* The case for {name EvenOddList.cons}`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.
* The minor premise for {name EvenOddList.nil}`nil` applies the motive to {name EvenOddList.nil}`nil`'s index value `true`.
* The minor premise {name EvenOddList.cons}`cons` abstracts over the index value used in its recursive occurrence, and instantiates the motive with its negation.
* The major premise additionally abstracts over an arbitrary choice of index.

```signature
EvenOddList.rec.{u, v} {α : Type v}
Expand All @@ -132,7 +132,7 @@ EvenOddList.rec.{u, v} {α : Type v}
:::::

When using a predicate (that is, a function that returns a {lean}`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.
The minor premises for non-recursive constructors are the base cases, and the additional arguments supplied to minor premises for constructors with recursive arguments are the induction hypotheses.

### Subsingleton Elimination
%%%
Expand Down Expand Up @@ -218,11 +218,11 @@ tag := "iota-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.
These rules govern the interaction between recursors and constructors; specifically recursors that have constructors as their major premise.
This form of reduction is called {deftech}_ι-reduction_ (iota reduction){index}[ι-reduction]{index (subterm:="ι (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.
When the recursor's major premise is a constructor with no recursive parameters, the recursor application reduces to an application of the constructor's minor premise to the constructor's arguments.
If there are recursive parameters, then these arguments to the minor premise are found by applying the recursor to the recursive occurrence.

# Well-Formedness Requirements
%%%
Expand Down Expand Up @@ -367,9 +367,9 @@ tag := "recursor-elaboration-helpers"

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.
* `recOn` is a version of the recursor in which the major premise is prior to the minor premise for each constructor.
* `casesOn` is a version of the recursor in which the major premise is prior to the minor premise 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 major premise 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 {lean}`False`; if both constructors are the same, then the consequence is the equality of their respective parameters.
Expand Down