項 （term）は 式 （expression）としても知られ、Lean のコア言語における意味の基本単位です。これらは エラボレータ によってユーザが書いた構文から生成されます。Lean の型システムは項をその 型 （type）に関連付けます。型は集合を表し、項は集合の個々の要素を表すと考えることができます。Lean の型理論の規則に従った型を持つ項は well-typed と言います。well-typed である項のみが意味を持ちます。
項は依存型付きラムダ計算です；関数抽象・適用・変数・let 束縛を含みます。束縛変数に加えて、項言語の変数は コンストラクタ ・ 型コンストラクタ ・ 再帰子 ・ defined constants ・不透明な定数を参照することができます。コンストラクタ・型コンストラクタ・再帰子・不透明な定数は置換の対象にはなりませんが、定義された定数はその定義に置き換えることができます。
導出 （derivation）は使用される正確な推論規則を明示的に示すことで項の well-typed さを示します。暗黙的に、well-typed な項は、その well-typed であることを示す導出の代わりにすることができます。Lean の型理論は十分に明示的であるため、well-typed な項から導出を再構築することができ、完全な導出を保存することで発生するオーバーヘッドを大幅に削減することができるにもかかわらず、この理論は現代の研究数学を表現するに足る表現力を保ちます。これは、証明項が定理の真理の十分な根拠となり、独立した検証が可能であることを意味します。
型を持つことに加えて、項は 定義上の等価性 （definitional equality）によっても関連付けられます。これは機械的にチェック可能な関係であり、計算動作に応じて項を等しくします。定義上の等価性には 簡約 （reduction）の以下の形式が含まれます：
束縛された変数への置換によって、引数に関数抽象を適用する
defined constant の出現箇所を定義の値で置き換える
コンストラクタをターゲットとする再帰子の簡約（原始再帰）
let 束縛変数を定義された値に置き換える
定義上の等価性には関数と単一コンストラクタの帰納型についてのη同値が含まれます。つまり、 fun x => f x は f に定義上等しく、 S がフィールド f1 と f2 を持つ構造体である時には S.mk x.f1 x.f2 は x と定義上等価です。また証明の irrelevance も特徴づけ、同じ命題の2つの証明は定義上等価です。これは反射的・対称的・合同です。
定義上の等価性は変換にも用いられます：2つの項が定義上等しく、ある項がその一方を型として持つ場合、その項ももう一方を型として持ちます。定義上の等価性は簡約を含むため、データに対する計算から型が生じることがあります。
自然数を渡すと、関数 LengthList は正確にその数のエントリを持つリストに対応する型を計算します：
def LengthList (α : Type u) : Nat → Type u
| 0 => PUnit
| n + 1 => α × LengthList α n
Lean のタプルは右側にネストしているため、複数のネストした括弧は必要ありません：
example : LengthList Int 0 := ()
example : LengthList String 2 :=
("Hello", "there", ())
長さが項目数と一致しない場合、計算された型はその項と一致しません：
example : LengthList String 5 :=
("Wrong", "number", ())
application type mismatch
("number", ())
argument
()
has type
Unit : Type
but is expected to have type
LengthList String 3 : Type
Lean の基本型は 宇宙 ・ 関数 型・ 帰納型 の 型コンストラクタ です。 Defined constants ・ 再帰子 の適用・関数適用・ axioms ・ 不透明な定数 のいずれかは他の型の項を生じさせることができるのと同様に、さらに型を与えることができます。
関数型は Lean の組み込み機能です。 関数 （function）とはある型の値（ 定義域 、domain）から別の型の値（ 値域 、range）へとマッピングし、 関数型 （function type） は関数の定義域と値域を指定します。
関数型には2種類あります：
依存関数の型はパラメータに明示的に名前を付け、関数の値域はこの名前を明示的に参照することができます。型は値から計算できるため、依存関数はその引数に応じて任意の数の異なる型の値を返すことができます。 依存関数は集合の添字付き積に対応するため、 依存積 （dependent product）と呼ばれることもあります。
非依存関数の型はパラメータの名前を含まず、提供される特定の引数によって値域が変わることはありません。
依存関数の型は明示的な名前を含みます：
term ::= ...
| Explicit binder, like `(x y : A)` or `(x y)`.
Default values can be specified using `(x : A := v)` syntax, and tactics using `(x : A := by tac)`.
非依存関数の型は含みません：
term ::= ... | term → term
関数 two はどの引数で呼び出されるかに応じて異なる型の値を返します：
def two : (b : Bool) → if b then Unit × Unit else String :=
fun b =>
match b with
| true => ((), ())
| false => "two"
関数の本体は if...then...else... と書くことができません。なぜならこの書き方は Lean.Parser.Term.match : termPattern matching. `match e, ... with | p, ... => f | ...` matches each given
term `e` against each pattern `p` of a match alternative. When all patterns
of an alternative match, the `match` term evaluates to the value of the
corresponding right-hand side `f` with the pattern variables bound to the
respective matched values.
If used as `match h : e, ... with | p, ... => f | ...`, `h : e = p` is available
within `f`.
When not constructing a proof, `match` does not automatically substitute variables
matched on in dependent variables' types. Use `match (generalizing := true) ...` to
enforce this.
Syntax quotations can also be used in a pattern match.
This matches a `Syntax` value against quotations, pattern variables, or `_`.
Quoted identifiers only match identical identifiers - custom matching such as by the preresolved
names only should be done explicitly.
`Syntax.atom`s are ignored during matching by default except when part of a built-in literal.
For users introducing new atoms, we recommend wrapping them in dedicated syntax kinds if they
should participate in matching.
For example, in
```lean
syntax "c" ("foo" <|> "bar") ...
```
`foo` and `bar` are indistinguishable during matching, but in
```lean
syntax foo := "foo"
syntax "c" (foo <|> "bar") ...
```
they are not.
match と同じように型を絞り込むわけではないからです。
Lean のコア言語では、すべての関数型は依存的です：非依存関数型はパラメータ名が値域内に存在しない依存関数型のことです。さらに、パラメータ名が異なる2つの依存関数型について、パラメータ名をリネームしたものが等しい場合、これら2つは定義上等しくなります。しかし、Lean のエラボレータは非依存関数のパラメータにローカル束縛を導入しません。
型 (x : Nat) → String と Nat → String は定義上等価です：
example : ((x : Nat) → String) = (Nat → String) := rfl
同様に、型 (n : Nat) → n + 1 = 1 + n と (k : Nat) → k + 1 = 1 + k は定義上等価です：
example : ((n : Nat) → n + 1 = 1 + n) = ((k : Nat) → k + 1 = 1 + k) := rfl
以下の文では、配列のすべての要素が0でないことを示す依存関数が必要です：
def AllNonZero (xs : Array Nat) : Prop :=
(i : Nat) → (lt : i < xs.size) → xs[i] ≠ 0
これは配列アクセスのためのエラボレータが、インデックスが範囲内にあることの証明を必要とするためです。非依存バージョンの文では、この仮定は導入されていません：
def AllNonZero (xs : Array Nat) : Prop :=
(i : Nat) → (i < xs.size) → xs[i] ≠ 0
failed to prove index is valid, possible solutions: - Use `have`-expressions to prove the index is valid - Use `a[i]!` notation instead, runtime check is performed, and 'Panic' error message is produced if index is not valid - Use `a[i]?` notation instead, result is an `Option` type - Use `a[i]'h` notation instead, where `h` is a proof that index is valid xs : Array Nat i : Nat ⊢ i < xs.size
関数型を持つ項は Lean.Parser.Term.fun : termfun キーワードで導入される抽象によって作成することができます。
最も基本的な関数抽象では、関数のパラメータを表す変数を導入します：
term ::= ... | fun ident => term
エラボレーション時において、Lean は関数の定義域を決定できなければなりません。type ascription はこの情報を提供する1つの方法です：
term ::= ... | fun ident : term => term
Lean.Parser.Command.definition : commanddef のようなキーワードで定義された関数定義は Lean.Parser.Term.fun : termfun に脱糖されます。しかし、すべての関数が抽象されたものではありません： 型コンストラクタ ・ コンストラクタ ・ 再帰子 は関数型を持つ場合がありますが、関数抽象だけでは定義できません。
Lean のコア型理論では、すべての関数は定義域の要素をそれぞれ値域の単一の要素にマッピングします。言い換えれば、すべての関数は正確に1つのパラメータを必要とします。複数のパラメータを持つ関数は、高階関数を定義することで実装されます。これは最初のパラメータを与えると、残りのパラメータを持つ新しい関数を返します。このエンコーディングは カリー化 （currying）と呼ばれ、Haskell B. Curry にちなんで命名されました。関数を定義し、型を指定し、それを適用するための Lean の構文は、複数パラメータの関数のような錯覚を引き起こしますが、エラボレーションの結果は単一パラメータの関数のみが含まれます。
依存関数型は同じ型を持つ複数のパラメータを1つの括弧の中に含めることができます：
term ::= ...
| Explicit binder, like `(x y : A)` or `(x y)`.
Default values can be specified using `(x : A := v)` syntax, and tactics using `(x : A := by tac)`.
これはネストされた関数型の各パラメータ名に対して、型注釈を繰り返すことと同じです。
Lean.Parser.Term.fun : termfun の後に複数のパラメータ名を指定することができます：
term ::= ... | fun ident* => term
term ::= ... | fun ident* : term => term
これらは Lean.Parser.Term.fun : termfun 項をネストして書くことと同じです。
Lean は関数への暗黙のパラメータをサポートしています。これはユーザが必要な引数をすべて与えるのではなく、Lean 自身が関数に引数を与えることができることを意味します。暗黙のパラメータには3種類あります：
通常の暗黙のパラメータとは、Lean が単一化によって値を決定すべき関数パラメータのことです。言い換えると、各呼び出し部位は、関数呼び出し全体が well-typed であるような潜在的な引数の値を1つだけ持つべきです。Lean のエラボレータは関数の各呼び出しですべての暗黙引数の値を見つけようとします。通常の暗黙の引数は波括弧（{ と }）で囲んで記述します。
厳格な暗黙のパラメータは通常の暗黙のパラメータと同じですが、Lean は呼び出し先で明示的な引数が指定された場合にのみ引数の値を見つけようとします。厳格な暗黙のパラメータは二重波括弧（⦃ と ⦄ または {{ と }}）で記述します。
インスタンスの暗黙のパラメータの引数は 型クラス合成 を介して見つけられます。インスタンスの暗黙のパラメータは角括弧（[ と ]）で囲まれ、ほとんどの場合パラメータ名は省略されます。というのも、パラメータとして関数に渡されるインスタンス合成は名前を明示的にしなくともすでに関数本体で利用可能であるからです。
f と g の違いは、 f では α が厳密に暗黙であることです：
def f ⦃α : Type⦄ : α → α := fun x => x
def g {α : Type} : α → α := fun x => x
これらの関数は具体的な引数に適用された際には同一のものへエラボレートされます：
example : f 2 = g 2 := rfl
しかし、明示的な引数が与えられない場合、 f の使用は α を解決する必要はありません：
example := f
しかし、g を使う際はこれを解決することが要求され、利用可能な情報が不十分な場合はエラボレートに失敗します：
example := g
don't know how to synthesize implicit argument 'α' @g ?m.6 context: ⊢ Type
Lean.Parser.Term.fun : termfun の最も一般的な構文は束縛子の列を受け入れます：
term ::= ... | fun funBinder* => term
関数の束縛子は以下のいずれかです。識別子：
funBinder ::= ... | ident
type ascription を持つ識別子の列：
funBinder ::= ...
| Type ascription notation: `(0 : Int)` instructs Lean to process `0` as a value of type `Int`.
An empty type ascription `(e :)` elaborates `e` without the expected type.
This is occasionally useful when Lean's heuristics for filling arguments from the expected type
do not yield the right result.
type ascription がある・無い暗黙のパラメータ：
funBinder ::= ...
| Implicit binder, like `{x y : A}` or `{x y}`.
In regular applications, whenever all parameters before it have been specified,
then a `_` placeholder is automatically inserted for this parameter.
Implicit parameters should be able to be determined from the other arguments and the return type
by unification.
In `@` explicit mode, implicit binders behave like explicit binders.
funBinder ::= ...
| Implicit binder, like `{x y : A}` or `{x y}`.
In regular applications, whenever all parameters before it have been specified,
then a `_` placeholder is automatically inserted for this parameter.
Implicit parameters should be able to be determined from the other arguments and the return type
by unification.
In `@` explicit mode, implicit binders behave like explicit binders.
無名・名前付きのインスタンスの暗黙のパラメータ：
funBinder ::= ...
| Instance-implicit binder, like `[C]` or `[inst : C]`.
In regular applications without `@` explicit mode, it is automatically inserted
and solved for by typeclass inference for the specified class `C`.
In `@` explicit mode, if `_` is used for an instance-implicit parameter, then it is still solved for by typeclass inference;
use `(_)` to inhibit this and have it be solved for by unification instead, like an implicit argument.
funBinder ::= ...
| Instance-implicit binder, like `[C]` or `[inst : C]`.
In regular applications without `@` explicit mode, it is automatically inserted
and solved for by typeclass inference for the specified class `C`.
In `@` explicit mode, if `_` is used for an instance-implicit parameter, then it is still solved for by typeclass inference;
use `(_)` to inhibit this and have it be solved for by unification instead, like an implicit argument.
type ascription がある・無い厳格な暗黙のパラメータ：
funBinder ::= ... |⦃(ident |Strict-implicit binder, like `⦃x y : A⦄` or `⦃x y⦄`. In contrast to `{ ... }` implicit binders, strict-implicit binders do not automatically insert a `_` placeholder until at least one subsequent explicit parameter is specified. Do *not* use strict-implicit binders unless there is a subsequent explicit parameter. Assuming this rule is followed, for fully applied expressions implicit and strict-implicit binders have the same behavior. Example: If `h : ∀ ⦃x : A⦄, x ∈ s → p x` and `hs : y ∈ s`, then `h` by itself elaborates to itself without inserting `_` for the `x : A` parameter, and `h hs` has type `p y`. In contrast, if `h' : ∀ {x : A}, x ∈ s → p x`, then `h` by itself elaborates to have type `?m ∈ s → p ?m` with `?m` a fresh metavariable.hole)⦄A *hole* (or *placeholder term*), which stands for an unknown term that is expected to be inferred based on context. For example, in `@id _ Nat.zero`, the `_` must be the type of `Nat.zero`, which is `Nat`. The way this works is that holes create fresh metavariables. The elaborator is allowed to assign terms to metavariables while it is checking definitional equalities. This is often known as *unification*. Normally, all holes must be solved for. However, there are a few contexts where this is not necessary: * In `match` patterns, holes are catch-all patterns. * In some tactics, such as `refine'` and `apply`, unsolved-for placeholders become new goals. Related concept: implicit parameters are automatically filled in with holes during the elaboration process. See also `?m` syntax (synthetic holes).
funBinder ::= ...
| Strict-implicit binder, like `⦃x y : A⦄` or `⦃x y⦄`.
In contrast to `{ ... }` implicit binders, strict-implicit binders do not automatically insert
a `_` placeholder until at least one subsequent explicit parameter is specified.
Do *not* use strict-implicit binders unless there is a subsequent explicit parameter.
Assuming this rule is followed, for fully applied expressions implicit and strict-implicit binders have the same behavior.
Example: If `h : ∀ ⦃x : A⦄, x ∈ s → p x` and `hs : y ∈ s`,
then `h` by itself elaborates to itself without inserting `_` for the `x : A` parameter,
and `h hs` has type `p y`.
In contrast, if `h' : ∀ {x : A}, x ∈ s → p x`, then `h` by itself elaborates to have type `?m ∈ s → p ?m`
with `?m` a fresh metavariable.
Lean のコア言語では暗黙・インスタンス・明示的なパラメータを区別しません：それぞれで書き直された関数とそれらの関数の型は定義上等しいです。これらの違いが観測されるのはエラボレーションの間のみです。
関数は Lean.Parser.Term.fun : termfun の後に、縦棒（|）で始まる一連のパターンを書くことでパターンマッチによって指定することができます。
term ::= ... | fun (| term,* => term)*
これは引数を即座にパターンマッチする関数に脱糖されます。
isZero はパターンマッチ関数を抽象化して定義される一方、 isZero' はパターンマッチ式を使って定義されます：
def isZero : Nat → Bool :=
fun
| 0 => true
| _ => false
def isZero' : Nat → Bool :=
fun n =>
match n with
| 0 => true
| _ => false
前者は後者のための構文糖衣であるため、定義上等しいです：
example : isZero = isZero' := rfl
脱糖結果は Lean.Parser.Command.print : command#print の出力で見ることができます：
#print isZero
上記は以下を出力し、
def isZero : Nat → Bool := fun x => match x with | 0 => true | x => false
一方で、
#print isZero'
は以下を出力します。
def isZero' : Nat → Bool := fun n => match n with | 0 => true | x => false
Lean における関数の定義上の等価性は 内包的 （intensional）です。つまり、この定義上の等価性は、束縛変数のリネームと 簡約 によって 構文上 （syntactically）で定義されます。大まかに言えば、これは2つの関数が同じアルゴリズムを実装していれば定義上等しいということを意味し、定義域の等しい要素を値域の等しい要素にマッピングしていれば等しいという通常の数学的な等値性の概念とは異なります。
Lean の型チェッカは2つの関数が内包的に等しいかどうかを判断できます。外延的な等価性は決定できないため、代わりに2つの関数が等しいという 命題 を証明する時に推論原理として利用できるようにします。
束縛変数の簡約とリネームに加えて、 η同値 （η-equivalence）と呼ばれる外延性の1つの限定された形式をサポートします。これは関数はその本体が引数に適用する抽象と等しいことを指します。 f の型が (x : α) → β x であるとすると、 f は fun x => f x と定義上等価です。
関数について推論するとき、定理 funextいくつかの拡張された型理論とは異なり、 funext は Lean における定理です。これは quotient 型を使って証明できます。 または対応するタクティク ext を使用して、2つの関数が等しい入力を等しい出力にマッピングする場合に等しいことを証明することができます。
funext.{u, v} {α : Sort u} {β : α → Sort v}
{f g : (x : α) → β x}
(h : ∀ (x : α), f x = g x) : f = g
Function extensionality is the statement that if two functions take equal values
every point, then the functions themselves are equal: (∀ x, f x = g x) → f = g.
It is called "extensionality" because it talks about how to prove two objects are equal
based on the properties of the object (compare with set extensionality,
which is (∀ x, x ∈ s ↔ x ∈ t) → s = t).
This is often an axiom in dependent type theory systems, because it cannot be proved
from the core logic alone. However in lean's type theory this follows from the existence
of quotient types (note the Quot.sound in the proof, as well as the show line
which makes use of the definitional equality Quot.lift f h (Quot.mk x) = f x).
関数は Lean.Parser.Command.declaration : commanddef を使って再帰的に定義することができます。Lean の論理の観点から、すべての関数は 全域 （total）です。これは関数が定義域の各要素を値域の要素に有限時間でマッピングすることを意味します。 プログラミング言語のコミュニティによっては、より限定的な意味で 全域 という用語を使用するものもあり、その場合、関数はクラッシュしなければ全域と見なされますが、非停止は無視されます。 全域関数の値はすべての型が正しい引数に対して定義され、パターンマッチでケースが漏れて停止に失敗したりクラッシュしたりすることはありません。
Lean の論理モデルはすべての関数を全域関数と見なしますが、Lean は実用的なプログラミング言語でもあり、ある種の「逃げ道」を用意しています。停止することが証明されていない関数は、その値域が空でないことが証明されている限り Lean の論理で使用することができます。これらの関数は Lean の論理では未解釈の関数として扱われ、その計算動作は無視されます。コンパイルされたコードでは、これらの関数は他の関数と同様に扱われます。そうではない関数は unsafe とマークされることがあります；これらの関数は Lean の論理では全く使用することができません。 partial と unsafe 関数定義 の節で再帰関数を使ったプログラミングの詳細があります。
同様に、配列への範囲外アクセスなど、コンパイルされたコードではランタイムに失敗するはずの操作は、結果の型が inhabited であることが分かっている場合にのみ使用することができます。これらの操作の結果、Lean のロジックでは型の住人が任意に選ばれます（具体的には、その型の Inhabited インスタンスで指定されたもの）。
関数 thirdChar は配列の3番目の要素を取り出します。配列の要素が2個以下の場合はパニックになります：
def thirdChar (xs : Array Char) : Char := xs[2]!
#['!'] と #['-', 'x'] の（存在しない）3番目の要素は等しいです。なぜなら、どちらも同じ任意に選ばれた文字を返すからです：
example : thirdChar #['!'] = thirdChar #['-', 'x'] := rfl
実際、どちらも 'A' に等しく、これは偶然にも Char のデフォルトのフォールバックです：
example : thirdChar #['!'] = 'A' := rfl
example : thirdChar #['-', 'x'] = 'A' := rfl
命題 （propositioin）は証明を認める意味のある文です。 無意味な文は命題ではありませんが、偽の文は命題です。すべての命題は Prop によって分類されます。
命題は以下の性質を持ちます：
同じ命題の2つの証明は完全に交換可能です。
命題はコンパイルされたコードからは消去されます。
命題はあらゆる宇宙からの型に対して量化することができます。
単集合を除いて、命題は非命題型に除去することができません。
論理的に同等な2つの命題は、 propext 公理によって等しいことが証明できます。
propext {a b : Prop} : (a ↔ b) → a = b
The axiom of propositional extensionality. It asserts that if propositions
a and b are logically equivalent (i.e. we can prove a from b and vice versa),
then a and b are equal, meaning that we can replace a with b in all
contexts.
For simple expressions like a ∧ c ∨ d → e we can prove that because all the logical
connectives respect logical equivalence, we can replace a with b in this expression
without using propext. However, for higher order expressions like P a where
P : Prop → Prop is unknown, or indeed for a = b itself, we cannot replace a with b
without an axiom which says exactly this.
This is a relatively uncontroversial axiom, which is intuitionistically valid.
It does however block computation when using #reduce to reduce proofs directly
(which is not recommended), meaning that canonicity,
the property that all closed terms of type Nat normalize to numerals,
fails to hold when this (or any) axiom is used:
set_option pp.proofs true
def foo : Nat := by
have : (True → True) ↔ True := ⟨λ _ => trivial, λ _ _ => trivial⟩
have := propext this ▸ (2 : Nat)
exact this
#reduce foo
-- propext { mp := fun x x => True.intro, mpr := fun x => True.intro } ▸ 2
#eval foo -- 2
#eval can evaluate it to a numeral because the compiler erases casts and
does not evaluate proofs, so propext, whose return type is a proposition,
can never block it.
型は 宇宙 （universe）によって分類されます。 各宇宙には レベル （level）があり、これは自然数です。 Sort 演算子は与えられたレベルから宇宙を構築します。 ある宇宙レベルが他の宇宙レベルよりも小さい場合、その宇宙自体も小さいと言います。命題を除いて（この章で後述）、与えられた宇宙内の型はより小さい宇宙内の型に対してのみ量化することができます。 Sort 0 は命題の型であり、各 Sort (u + 1) はデータを記述する型です。
すべての宇宙はすべての狭義に大きな宇宙の要素なので、 Sort 5 は Sort 4 を含みます。つまり、以下の例が認められます：
example : Sort 5 := Sort 4
example : Sort 2 := Sort 1
一方で、 Sort 3 は Sort 5 の要素ではありません：
example : Sort 5 := Sort 3
type mismatch Type 2 has type Type 3 : Type 4 but is expected to have type Type 4 : Type 5
同様に、 Unit は Sort 1 に存在するため、 Sort 2 には存在しません：
example : Sort 1 := Unit
example : Sort 2 := Unit
type mismatch Unit has type Type : Type 1 but is expected to have type Type 1 : Type 2
命題とデータは異なる使われ方をし、異なる規則に支配されるため、より便利に区別するために Type と Prop という省略形が用意されています。 Type u は Sort (u + 1) の省略形であるため、 Type 0 は Sort 1 で Type 3 は Sort 4 です。 Type 0 は Type と省略することもできるため、 Unit : Type および Type : Type 1 です。 Prop は Sort 0 の省略形です。
各宇宙は依存関数型を含んでおり、それはさらに全称量化子と含意を表します。関数型の宇宙は、引数の型と戻り値の型の宇宙によって決定されます。具体的な規則は、関数の戻り値が命題かどうかに依存します。
命題を返す関数である述語（つまり、関数の結果の型が Prop にある型である場合）は引数の型がどのような宇宙に会っても構いませんが、関数の型自体は Prop に留まります。言い換えると、命題は impredicative な量化子を特徴づけます。というのも、命題はそれ自体、すべての命題（および他のすべての命題）についての文になりうるからです。
証明の irrelevance はすべての命題を量化する命題として書くことができます：
example : Prop := ∀ (P : Prop) (p1 p2 : P), p1 = p2
命題はまた任意のレベルにおいてすべての型を量化することもできます：
example : Prop := ∀ (α : Type), ∀ (x : α), x = x
example : Prop := ∀ (α : Type 5), ∀ (x : α), x = x
レベル 1 以上の宇宙（つまり、Type u の階層）では、量化子は predicative です。 これらの宇宙では、関数型の宇宙は引数の型と戻り値の型の宇宙の最小上界となります。
これらの型はどちらも Type 2 に存在します：
example (α : Type 1) (β : Type 2) : Type 2 := α → β
example (α : Type 2) (β : Type 1) : Type 2 := α → β
Type の Predicativity
α のレベルは 1 より大きいため、この例は許可されません。言い換えると、注釈された宇宙は実際の関数型の宇宙よりも小さいです：
example (α : Type 2) (β : Type 1) : Type 1 := α → β
type mismatch α → β has type Type 2 : Type 3 but is expected to have type Type 1 : Type 2
Lean の宇宙は cumulative ではありません； これは Type u の型が自動的に Type (u + 1) にも存在するようにならないことを意味します。
この例は注釈された宇宙が関数型の宇宙よりも大きいため、許可されません：
example (α : Type 2) (β : Type 1) : Type 3 := α → β
type mismatch α → β has type Type 2 : Type 3 but is expected to have type Type 3 : Type 4
Lean は 宇宙多相 （universe polymorphism）をサポートしており、Lean 環境で定義された定数は 宇宙パラメータ を取ることができます。これらのパラメータは定数が使用されるときに宇宙レベルでインスタンス化されます。宇宙パラメータは定数名の後のドットに続く波括弧で記述します。
完全に明示的な場合、恒等関数は宇宙パラメータ u を取ります。このシグネチャは以下になります：
id.{u} {α : Sort u} (x : α) : α宇宙変数はさらに、定義の中で特定の宇宙レベルを提供する 宇宙レベル式 の中で現れるかもしれません。多相定義が具体的なレベルでインスタンス化されるとき、これらの宇宙レベル式も具体的なレベルをもたらすために評価されます。
この例では、 Codec はそれが含む型の宇宙より1つ大きい宇宙に存在します：
structure Codec.{u} : Type (u + 1) where
type : Type u
encode : Array UInt32 → type → Array UInt32
decode : Array UInt32 → Nat → Option (type × Nat)
Lean はほとんどのレベルパラメータを自動的に推論します。以下の例では、 Char の型は Type 0 であるため、u は 0 でなければならないことから、 Codec.{0} と注釈する必要はありません。
def Codec.char : Codec where
type := Char
encode buf ch := buf.push ch.val
decode buf i := do
let v ← buf[i]?
if h : v.isValidChar then
let ch : Char := ⟨v, h⟩
return (ch, i + 1)
else
failure
宇宙多相な定義は、実際には様々なレベルでインスタンス可能な スキーマ的定義 （schematic definition）を作り出し、宇宙レベルの異なるインスタンス化は互換性のない値を作ります。
これは次の例で見ることができます。 T は不要な宇宙多相定義で、常に true を返します。 Lean.Parser.Command.declaration : commandopaque とマークされているため、Lean は T の定義を展開して等価性をチェックすることができません。 T のインスタンスはどれもパラメータと同じ型を持ちますが、宇宙のインスタンス化が異なるため互換性がありません：
opaque T.{u} (_ : Nat) : Bool := (fun (α : Sort u) => true) PUnit.{u}
set_option pp.universes true
def test.{u, v} : T.{u} 0 = T.{v} 0 := rfl
type mismatch
rfl.{1}
has type
Eq.{1} (T.{u} 0) (T.{u} 0) : Prop
but is expected to have type
Eq.{1} (T.{u} 0) (T.{v} 0) : Prop
自動的に束縛される暗黙の引数は可能な限り宇宙多相となります。恒等関数を次のように定義します：
def id' (x : α) := x
これは以下のシグネチャになります：
id'.{u} {α : Sort u} (x : α) : α
一方、 Nat は Type 0 に存在するため、この関数は自動的に α の具体的な宇宙レベルを求めます。m は Nat と α の両方に適用されるため、どちらも同じ型を持たなければならず、結果として同じ宇宙となります：
partial def count [Monad m] (p : α → Bool) (act : m α) : m Nat := do
if p (← act) then
return 1 + (← count p act)
else
return 0
定義に現れるレベルは変数と定数の和だけに限定されません。より複雑な宇宙間の関係もレベルの表現を使って定義できます。
Level ::= 0 | 1 | 2 | ... -- 具体的なレベル
| u, v -- 変数
| Level + n -- 定数の和
| max Level Level -- 最小上界
| imax Level Level -- Impredicative な最小上界
レベル変数が具体的な数値に割り当てられている場合、これらの式の評価は通常の算術の規則に従います。imax 演算は以下のように定義されます：
\mathtt{imax}\ u\ v = \begin{cases}0 & \mathrm{when\ }v = 0\\\mathtt{max}\ u\ v&\mathrm{otherwise}\end{cases}
imax は Prop の impredicative な量化子を実装するために使用されます。特に、A : Sort u かつ B : Sort v である場合、(x : A) → B : Sort (imax u v) となります。もし B : Prop ならば、その関数型は Prop であり、それ以外ではその関数型のレベルは u と v の最大値になります。
宇宙多相定義は宇宙変数を束縛します。これらの束縛は明示的・暗黙的のどちらも可能です。明示的な宇宙変数の束縛とインスタンス化は定義の名前の接尾辞として行われます。宇宙パラメータは定数名にピリオド（.）を接尾辞として付け、その後に波括弧の間にカンマで区切られた一連の宇宙変数を付けることで定義・提供されます。
map
以下map の宣言では、2つの宇宙パラメータ（u と v）を宣言し、多相型の List を順番にインスタンス化しています：
def map.{u, v} {α : Type u} {β : Type v}
(f : α → β) :
List.{u} α → List.{v} β
| [] => []
| x :: xs => f x :: map f xs
Lean が暗黙のパラメータを自動的にインスタンス化するように、宇宙パラメータも自動的にインスタンス化されます。autoImplicit オプションが true に設定されている場合（これがデフォルトです）、宇宙変数を明示的に束縛する必要はありません。 false に設定すると、明示的に追加するか universe コマンドを使って宣言する必要があります。
autoImplicit が true （デフォルト値）の場合、この定義は宇宙パラメータを束縛していなくても許可されます：
set_option autoImplicit true
def map {α : Type u} {β : Type v} (f : α → β) : List α → List β
| [] => []
| x :: xs => f x :: map f xs
autoImplicit が false の場合、u と v がスコープにないためこの定義は却下されます：
set_option autoImplicit false
def map {α : Type u} {β : Type v} (f : α → β) : List α → List β
| [] => []
| x :: xs => f x :: map f xs
unknown universe level 'u'
unknown universe level 'v'
autoImplicit を使うことに加えて、universe コマンドを使って特定の識別子を特定の section scope 内の宇宙変数として宣言することができます。
command ::= ...
| Declares one or more universe variables.
`universe u v`
`Prop`, `Type`, `Type u` and `Sort u` are types that classify other types, also known as
*universes*. In `Type u` and `Sort u`, the variable `u` stands for the universe's *level*, and a
universe at level `u` can only classify universes that are at levels lower than `u`. For more
details on type universes, please refer to [the relevant chapter of Theorem Proving in Lean][tpil
universes].
Just as type arguments allow polymorphic definitions to be used at many different types, universe
parameters, represented by universe variables, allow a definition to be used at any required level.
While Lean mostly handles universe levels automatically, declaring them explicitly can provide more
control when writing signatures. The `universe` keyword allows the declared universe variables to be
used in a collection of definitions, and Lean will ensure that these definitions use them
consistently.
[tpil universes]: https://lean-lang.org/theorem_proving_in_lean4/dependent_type_theory.html#types-as-objects
(Type universes on Theorem Proving in Lean)
```lean
/- Explicit type-universe parameter. -/
def id₁.{u} (α : Type u) (a : α) := a
/- Implicit type-universe parameter, equivalent to `id₁`.
Requires option `autoImplicit true`, which is the default. -/
def id₂ (α : Type u) (a : α) := a
/- Explicit standalone universe variable declaration, equivalent to `id₁` and `id₂`. -/
universe u
def id₃ (α : Type u) (a : α) := a
```
On a more technical note, using a universe variable only in the right-hand side of a definition
causes an error if the universe has not been declared previously.
```lean
def L₁.{u} := List (Type u)
-- def L₂ := List (Type u) -- error: `unknown universe level 'u'`
universe u
def L₃ := List (Type u)
```
## Examples
```lean
universe u v w
structure Pair (α : Type u) (β : Type v) : Type (max u v) where
a : α
b : β
#check Pair.{v, w}
-- Pair : Type v → Type w → Type (max v w)
```
現在のスコープの範囲において1つ以上の宇宙変数を宣言します。
variable コマンドが特定の識別子を特定の型のパラメータとして扱うように、universe コマンドは autoImplicit オプションが false であっても、それに続く識別子を宇宙パラメータとして暗黙的に量化します。
autoImplicit が false の際の universe コマンドset_option autoImplicit false
universe u
def id₃ (α : Type u) (a : α) := a
自動的な暗黙のパラメータ機能は宣言の ヘッダ で使用されるパラメータのみを挿入するため、定義の右側にのみ現れる宇宙変数は autoImplicit が true の場合でも universe で宣言されていない限り引数として挿入されません。
universe コマンド明示的な宇宙パラメータを伴ったこの定義は許可されます：
def L.{u} := List (Type u)
u が := の前にあるヘッダで言及されていないため、自動的な暗黙のパラメータでもこの定義は却下されます：
set_option autoImplicit true
def L := List (Type u)
unknown universe level 'u'
宇宙宣言では、u は右辺でもパラメータとして許可されます：
universe u
def L := List (Type u)
その結果、L の定義は宇宙パラメータとして u が挿入された宇宙多相となります。
universe コマンドのスコープにある宣言は、その中に宇宙変数が無い場合、または自動的に挿入される他の引数の中に宇宙変数が無い場合、多相にはなりません。
universe u
def L := List (Type 0)
#check L
Rules for unification, properties of algorithm
Lack of injectivity
Universe inference for unannotated inductive types
Tracked at issue #0
帰納型 （inductive type）は Lean に新しい型を導入する主な手段です。 宇宙 と 関数 は組み込みのプリミティブでユーザが追加することはできませんが、Lean の他のすべての型は帰納型であるか、宇宙・関数・帰納型によって定義されたものであるかのどちらかです。帰納型は 型コンストラクタ （type constructor） と コンストラクタ （constructor） によって指定されます；帰納型の性質はこれらから導かれます。各帰納型は1つの型コンストラクタを持ち、 宇宙パラメータ と通常のパラメータの両方を取ることができます。帰納型は任意の数のコンストラクタを持つことができます；これらのコンストラクタは帰納型の型コンストラクタによって型が導かれる新しい値を導入します。
帰納型の型コンストラクタとコンストラクタに基づいて、Lean は 再帰子 （recursor）を導出します。論理的には、再帰子は帰納原理や除去則を表し、計算上は原始再帰計算を表します。再帰関数の停止は、再帰子の使用に変換することで正当化されるため、Lean のカーネルは再帰子の適用の型チェックを行うだけでよく、停止性の分析を別途行う必要はありません。Lean はさらに、システムの他の場所でも使用される再帰子 再帰子 という用語は再帰的でない型でも常に使用されます。 に基づいた数多くの補助的な構成を提供しています。
構造体 （structure）はコンストラクタを1つだけ持つ帰納型の特殊なケースです。構造体が宣言されると、Lean は新しい構造体で追加の言語機能を使用できるようにする補助関数を生成します。
本節では、帰納型と構造体の両方を指定するために使用される構文の具体的な詳細・帰納型の宣言から生じる環境内の新しい定数と定義・コンパイルされたコードにおける帰納型の値のランタイム表現について説明します。
command ::= ... |declModifiers`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.inductiveIn 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.declId`declId` matches `foo` or `foo.{u,v}`: an identifier possibly followed by a list of universe namesoptDeclSig where (|`optDeclSig` matches the signature of a declaration with optional type: a list of binders and then possibly `: type`declModifiers ident`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.optDeclSig)* (deriving ident,*)?`optDeclSig` matches the signature of a declaration with optional type: a list of binders and then possibly `: type`
新しい帰納型を宣言します。 declModifiers の意味は 宣言修飾子について の節で説明した通りです。
帰納型を宣言すると、その型コンストラクタ・コンストラクタ・再帰子が環境に現れます。新しい帰納型は Lean のコア論理を拡張します。それらは既に存在する他のデータによってエンコードされたり表現されたりすることはありません。帰納型の宣言は、論理の一貫性を保つために 多くの適格な要件 を満たす必要があります。
宣言の最初の行にて、 Lean.Parser.Command.inductive : commandinductive から Lean.Parser.Command.inductive : commandwhere までは新しい 型コンストラクタ の名前と型を指定しています。型コンストラクタの型シグネチャが提供されている場合、その結果の型は 宇宙 でなければなりませんが、パラメータは型である必要はありません。シグネチャが提供されない場合、Lean は結果の型を含むのに十分な大きさの宇宙を推論しようとします。状況によってはこのプロセスは最小の宇宙を見つけることができなかったり、全く見つけることができなかったりすることがあり、その場合は注釈が必要です。
コンストラクタの仕様は Lean.Parser.Command.inductive : commandwhere の後に続きます。コンストラクタは必須ではありません。コンストラクタのない帰納型としては False と Empty などがまさに当てはまります。各コンストラクタの指定は、縦棒（'|'、Unicode 'VERTICAL BAR' (U+007c)）・宣言修飾子・名前で始まります。名前は 生識別子 です。宣言シグネチャは名前の後に続きます。シグネチャは帰納的宣言の適格要件に従って任意のパラメータを指定することができますが、シグネチャの戻り型は指定された帰納型の型コンストラクタを完全に適用したものでなければなりません。シグネチャが提供されない場合、コンストラクタの型は適格な戻り値を構成するのに十分な暗黙のパラメータを挿入することによって推測されます。
新しい帰納型の名前は current namespace で定義されます。各コンストラクタの名前は帰納型の名前空間にあります。
型コンストラクタは2種類の引数を取ることができます： パラメータ （parameter）と 添字 （index, indices）です。パラメータは定義全体で一貫して使用されなければなりません；宣言内の各コンストラクタで型コンストラクタが出現する場合は、すべて正確に同じ引数を取る必要があります。添字は型コンストラクタの出現箇所によって異なっていてもかまいません。すべてのパラメータは、型コンストラクタのシグネチャのすべての添字の前にいなければなりません。
型コンストラクタのシグネチャのコロン（':'）より前に現れるパラメータは帰納型宣言全体に対するパラメータと見なされます。これらは常に型の定義全体を通して一様でなければならないパラメータです。一般的に言えば、コロンの後にあるパラメータは型の定義全体を通して変化する可能性のある添字です。しかし、オプション inductive.autoPromoteIndices が true の場合、パラメータになる可能性のある構文としては添字のものがパラメータになります。添字がパラメータである可能性があるのは、その型の依存関係がすべてパラメータであり、帰納型の型コンストラクタのすべてのコンストラクタで一律にインスタンス化されていない変数として使用される場合です。
inductive.autoPromoteIndices
Default value: true
Promote indices to parameters in inductive types whenever possible.
添字は型の 族 （family）を定義していると見なすことができます。添字を選択するごとに、その族から型が選択され、その型は使用可能なコンストラクタのあつまりを持ちます。添字のパラメータを取る型のコンストラクタは 添字族 （indexed family）と呼ばれます、
Vacant は空の帰納型であり、Lean の Empty 型と同値です：
inductive Vacant : Type where
空の帰納型は無用なものではありません；到達不可能なコードを示すために使うことができます。
One は Lean の Unit 型と同値です：
inductive One where
| one
これは型コンストラクタとコンストラクタの両方のシグネチャが省略された帰納型の例です。Lean は One を Type に割り当てます：
#check One
One : Type
コンストラクタ名は型コンストラクタの名前空間にあるため、コンストラクタ名は One.one です。 One は引数を期待しないため、 One.one のシグネチャは次のようになります：
#check One.one
One.one : One
Yes は Lean の True 命題と同値です：
inductive Yes : Prop where
| intro
One と異なり、この新しい帰納型 Yes は Prop 宇宙にあることが指定されています。
#check Yes
Yes : Prop
Yes.intro のシグネチャは以下のように推測されます：
#check Yes.intro
Yes.intro : Yes
EvenOddList α b はリストで、 α はリストに格納されているデータの型、 b はエントリの数が偶数の時に true となります：
inductive EvenOddList (α : Type u) : Bool → Type u where
| nil : EvenOddList α true
| cons : α → EvenOddList α isEven → EvenOddList α (not isEven)
この例では、リストに2つのエントリがあるため、正しく型付けられています：
example : EvenOddList String true :=
.cons "a" (.cons "b" .nil)
この例では、リストに3つのエントリがあるため、型付けは正しくありません：
example : EvenOddList String true :=
.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
この宣言では、 α は パラメータ です。なぜなら、これは EvenOddList のすべての出現で一貫して使用されているからです。 b は index であり、異なる出現で異なる Bool 値が使用されるからです。
この例では、パラメータはどちらも Either のシグネチャにおいてコロンの前に指定されています。
inductive Either (α : Type u) (β : Type v) : Type (max u v) where
| left : α → Either α β
| right : α → Either α β
このバージョンでは α という名前の型が2つあり、同一ではないかもしれません：
inductive Either' (α : Type u) (β : Type v) : Type (max u v) where
| left : {α : Type u} → {β : Type v} → α → Either' α β
| right : α → Either' α β
inductive datatype parameter mismatch α expected α✝
コロンの後にパラメータを置くと、コンストラクタでインスタンス化できるパラメータになります：
inductive Either'' : Type u → Type v → Type (max u v) where
| left : {α : Type u} → {β : Type v} → α → Either'' α β
| right : α → Either'' α β
Either''.right の型パラメータは Lean の automatic implicit パラメータに関する通常の規則によって発見されます。
帰納型がコンストラクタを1つだけ持つ場合、このコンストラクタは 匿名コンストラクタ構文 （anonymous constructor syntax）の対象となります。コンストラクタの名前を引数に適用して書く代わりに、明示的な引数を角括弧（'⟨' と '⟩'、Unicode MATHEMATICAL LEFT ANGLE BRACKET (U+0x27e8) と MATHEMATICAL RIGHT ANGLE BRACKET (U+0x27e9)）で囲み、カンマで区切ることができます。これはパターンと式の両方のコンテキストで動作します。引数を名前で指定したり、すべての暗黙的なパラメータを @ で明示的なものに変換したりするには、通常のコンストラクタ構文を使用する必要があります。
型 AtLeastOne α は List α と似ていますが、少なくとも1つの要素が常に存在します：
inductive AtLeastOne (α : Type u) : Type u where
| mk : α → Option (AtLeastOne α) → AtLeastOne α
匿名コンストラクタ構文を使ってこれを構成することができます：
def oneTwoThree : AtLeastOne Nat :=
⟨1, some ⟨2, some ⟨3, none⟩⟩⟩
また、この型の値にマッチすることができます：
def AtLeastOne.head : AtLeastOne α → α
| ⟨x, _⟩ => x
上記と同等に、通常のコンストラクタ構文も使うことが可能です：
def oneTwoThree' : AtLeastOne Nat :=
.mk 1 (some (.mk 2 (some (.mk 3 none))))
def AtLeastOne.head' : AtLeastOne α → α
| .mk x _ => x
帰納的宣言のオプションとして、 Lean.Parser.Command.inductive : commandderiving 節は、型クラスのインスタンスを導出するために使用することができます。詳細は インスタンス導出についての節 を参照してください。
command ::= ... |declModifiers structure`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.declId bracketedBinder* (extends term,*)? (: term)? where (`declId` matches `foo` or `foo.{u,v}`: an identifier possibly followed by a list of universe namesdeclModifiers ident ::)? structFields (deriving ident,*)?`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.
新しい構造体の型を宣言します。
構造体 （structure）は単一のコンストラクタと添字を持たない帰納型です。これらの制限と引き換えに、Lean は構造体のための数々の便利なコードを生成します：アクセサ関数が各フィールドに対して生成される・位置引数ではなくフィールド名に基づく追加のコンストラクタ構文が利用できる・同様の構文を使用して特定の名前付きフィールドの値を書き換えることができる・構造体は他の構造体を拡張することができる。他の帰納型と同様に、構造体も再帰的です；また strict positivity に関しても同じ制約を受けます。構造体は Lean の表現力を増すものではありません；すべての機能はコード生成の観点から実装されます。
通常の帰納型宣言と同様に、構造体宣言のヘッダにはパラメータと結果の宇宙の両方を指定できるシグネチャが含まれます。構造体は 添字族 を定義することはできません。
構造体宣言の各フィールドは、コンストラクタのパラメータに対応します。自動的な暗黙引数はたとえ名前が一致していても各フィールドに別々に挿入され、フィールドは型を量化するコンストラクタのパラメータになります。
構造体 MyStructure は型が自動的な暗黙のパラメータであるフィールドを含んでいます：
structure MyStructure where
field1 : α
field2 : α
型コンストラクタ MyStructure は2つの宇宙パラメータを取ります：
MyStructure.{u, v} : Type (max u v)
コンストラクタのフィールドは Sort の型に対して量化されるため、結果の型は Type ではなく Sort になります。特に、コンストラクタ MyStructure.mk の両方のフィールドは暗黙の型パラメータを取ります：
MyStructure.mk.{u, v}
(field1 : {α : Sort u} → α)
(field2 : {α : Sort v} → α)
: MyStructure.{u,v}各フィールドに対してベースとなる型のコンストラクタからフィールドの値を抽出する 射影関数 （projection function）が生成されます。この関数は構造体の名前の名前空間に存在します。構造体のフィールドの射影はエラボレータによって特別に処理され（ 構造体の継承についての節 で説明します）、名前空間を検索する以上の余分なステップが実行されます。フィールドの型が先行するフィールドに依存する場合、依存する射影関数の型は、明示的なパターンマッチではなく、先行する射影の観点から記述されます。
構造体 ArraySized は型が構造体のパラメータとそれより前のフィールドの両方に依存するフィールドを含んでいます：
structure ArraySized (α : Type u) (length : Nat) where
array : Array α
size_eq_length : array.size = length
射影関数 size_eq_length のシグネチャは構造体の型のパラメータを暗黙のパラメータとして受け取り、対応する射影を使ってそれより前のフィールドを参照します：
ArraySized.size_eq_length.{u}
{α : Type u} {length : Nat}
(self : ArraySized α length)
: self.array.size = length
構造体のフィールドは := で指定されたデフォルト値を持つことができます。明示的な値が提供されない場合、これらの値が使用されます。
グラフの隣接リスト表現は Nat のリストの配列として表すことができます。配列のサイズは頂点の数を表し、各頂点から出る辺は頂点のインデックスで配列に格納されます。フィールド adjacency にはデフォルト値 #[] が指定されているため、フィールドの値を指定しなくても空のグラフ Graph.empty を作成することができます。
structure Graph where
adjacency : Array (List Nat) := #[]
def Graph.empty : Graph := {}
構造体のフィールドはさらに、ドット記法を使ってインデックスからアクセスすることもできます。フィールドの番号は 1 から始まります。
構造体のコンストラクタは、フィールドの前にコンストラクタ名と :: を指定することで明示的に名前を付けることができます。名前が明示的に与えられない場合、コンストラクタ名は構造体型の名前空間の mk という名前になります。また、明示的なコンストラクタ名と共に、 宣言修飾子 を指定することもできます。
構造体 Palindrome は文字列と、その文字列が反転しても同じであることの証明を含みます：
structure Palindrome where
ofString ::
text : String
is_palindrome : text.data.reverse = text.data
そのコンストラクタ名は Palindrome.mk ではなく Palindrome.ofString です。
構造体 NatStringBimap は自然数と文字列の間の有限な全単射を保持します。これは写像のペアで構成され、それぞれのキーがもう一方の写像の値として一度だけ出現するようになっています。コンストラクタはプライベートであるため、これを定義したモジュールの外のコードは新しいインスタンスを作成できず、提供されたAPIを使用しなければなりません。このAPIではデータ型の不変量を保持します。さらに、デフォルトのコンストラクタ名を明示的に指定することで、コンストラクタに documentation comment を付けることができます。
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))
構造体は単一コンストラクタの帰納型として表現されるため、そのコンストラクタは 匿名コンストラクタ構文 を使用して呼び出したり、マッチしたりすることができます。さらに、構造体はフィールドの名前とフィールドの値を使って構築したり、マッチすることができます。
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 }`.
指定されたフィールドの値が与えられたコンストラクタの型の値を構築します。フィールド指定子には2つの形式があります：
structInstField ::= ... | structInstLVal := term
structInstFieldAbbrev ::= ... | ident
structInstLVal はフィールド名（識別子）・フィールドインデックス（自然数）・角括弧内の項のいずれかで、その後に0個以上のサブフィールドが続きます。サブフィールドはドットで始まるフィールド名・インデックス・角括弧内の項のいずれかです。
この構文は、構造体コンストラクタの適用にエラボレートされます。フィールドに提供される値は名前であり、どのような順序で提供されても構いません。サブフィールドに指定された値は、構造体のコンストラクタのフィールドを初期化するために使用されます。角括弧内の項は構造体を構築する際には使用できません；これらは構造体の更新で用いられます。
:= を含まないフィールド指定子はフィールドの省略形です。この文脈においては、識別子 f は f := f の省略形です；つまり、現在のスコープにおける f の値がフィールド f の初期化に使われます。
デフォルト値を持たないすべてのフィールドは提供されなければなりません。デフォルトの引数としてタクティクが指定された場合、そのタクティクは引数の値を構築するためにエラボレーション時に実行されます。
パターンの文脈では、フィールド名は対応する射影にマッチするパターンにマップされ、フィールドの省略形はフィールド名であるパターン変数を束縛します。デフォルト値を持つフィールドに対してパターンが値を指定しない場合、パターンはデフォルト値のみにマッチします。
オプションで型注釈することによって、構造体型が他に決定されないコンテキストにおいて構造体型を指定することを可能にします。
構造体 AugmentedIntList にはリストといくつかの追加情報がふくまれています。追加情報が省かれた時は空になります：
structure AugmentedIntList where
list : List Int
augmentation : String := ""
リストが空かどうかをテストするとき、関数 isEmpty は augmentation フィールドが空かどうかもテストしています。これは省略されたフィールドのデフォルト値もパターンの文脈で使用されるからです：
def AugmentedIntList.isEmpty : AugmentedIntList → Bool
| {list := []} => true
| _ => false
#eval {list := [], augmentation := "extra" : AugmentedIntList}.isEmpty
false
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 }`.
コンストラクタの型の値を更新します。 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 節の前にある項は構造体型を持つことが期待されます；これが更新される値です。構造体の新しいインスタンスが作成され、指定されていないすべてのフィールドが更新される値からコピーされ、指定されたフィールドは新しい値に置き換えられます。構造体を更新する時、更新するインデックスを角括弧で囲むことで配列の値を置き換えることもできます。この更新では、院デック氏の式が配列の範囲内にある必要はなく、範囲外の更新は破棄されます。
構造体の更新には、射影名だけでなく、配列インデックスも指定できます。範囲外のインデックスでの更新は無視されます：
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}
#eval (one, two, two', two'')
({ array := #[1], augmentation := "" },
{ array := #[1, 2], augmentation := "" },
{ array := #[2, 2], augmentation := "" },
{ array := #[1, 2], augmentation := "" })
構造体型の値は、 Lean.Parser.Command.declValEqns : commandwhere とそれに続く各フィールドの定義を使用して宣言することもできます。これは定義の一部としてのみ使用でき、式の文脈では使用できません。
where
Lean の直積型は Prod という構造体です。直積は射影を使って定義できます：
def location : Float × Float where
fst := 22.807
snd := -13.923
構造体はオプションの Lean.Parser.Command.structure : commandextends 節を使用することで他の構造体を拡張することを宣言できます。結果として得られる構造体型は、すべての親構造体型のすべてのフィールドを持ちます。親構造体型が重複するフィールド名を持つ場合、重複するフィールド名はすべて同じ型を持たなければなりません。重複するフィールド名が異なるデフォルト値を持つ場合、そのフィールドを含む最後の親構造体のデフォルト値が使用されます。子構造体の新しいデフォルト値は、親構造体のデフォルト値よりも優先されます。
新しい構造体が既存の構造体を拡張する場合、新しい構造体のコンストラクタは既存の構造体の情報を追加引数として受け取ります。通常、これは親構造体の型ごとにコンストラクタのパラメータを指定する形になります。しかし、親のフィールドが重複している場合は、フィールド情報の重複を防ぐために、親の1つ以上のフィールドから重複していないフィールドのサブセットが代わりに含まれます。
親構造体とその子構造体の間には部分型の関係はありません。構造体 B が構造体 A を継承していても、A を期待する関数は B を受け付けません。しかし、構造体をそれぞれの親に変換する変換関数が生成されます。これらの変換関数は子構造体の名前空間に存在し、その名前は親構造体の名前の前に to が付いたものになります。
この例では、 Textbook は Book であり、 AcademicWork でもあります：
structure Book where
title : String
author : String
structure AcademicWork where
author : String
discipline : String
structure Textbook extends Book, AcademicWork
#check Textbook.toBook
フィールド author は Book と AcademicWork の両方に存在するため、コンストラクタ Textbook.mk は両方の親を引数に取りません。そのシグネチャは以下のようになります：
Textbook.mk (toBook : Book) (discipline : String) : Textbook変換関数は以下です：
Textbook.toBook (self : Textbook) : BookTextbook.toAcademicWork (self : Textbook) : AcademicWork
後者は含まれる Book の author フィールドとバンドルされていない discipline フィールドを組み合わせたもので、次のものと等価です：
def toAcademicWork (self : Textbook) : AcademicWork :=
let .mk book discipline := self
let .mk _title author := book
.mk author discipline
結果として得られる構造体の射影はそのフィールドが単に親のフィールドの合併であるかのように使うことができます。Lean のエラボレータは射影に遭遇すると、自動的に適切なアクセサを生成します。同様に、フィールドベースの初期化と構造体の更新の表記は、継承のエンコーディングの詳細を隠します。しかし、このエンコーディングはコンストラクタの名前の使用時・ 匿名コンストラクタ構文 の使用時・名前ではなくインデックスでフィールドを参照する時には表示されます。
structure 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}
coords の最初のフィールドインデックスを評価すると、フィールド fst の内容ではなく、そのベースである Pair が得られます：
#eval coords.1
{ fst := 17, snd := 2 }
偶数・偶素数・具体的な偶数素数の定義が与えられている時：
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
printEven を two に直接適用すると型エラーになります：
#check printEven two
application type mismatch printEven two argument two has type EvenPrime : Type but is expected to have type EvenNumber : Type
なぜなら EvenPrime 型の値は EvenNumber 型の値でもないからです。
全ての帰納型は 再帰子 を備えています。再帰子は型コンストラクタとコンストラクタのシグネチャによって完全に決定されます。再帰子は関数型を持ちますが、それはプリミティブであり、fun を使って定義することはできません。
再帰子は以下のパラメータを取ります：
パラメータは一貫しているため、これらは再帰性全体を通して抽象化できます
動機は再帰子の適用の型を決定します。動機は型の添字とこれらの添字をインスタンス化した型のインスタンスを引数とする関数です。動機が決定する型の特定の宇宙は帰納型の宇宙とその特定のコンストラクタに依存します。詳細は subsingleton 除去 の節を参照してください。
それぞれのコンストラクタに対して、再帰子はコンストラクタの任意の適用の動機を満たす関数を期待します。各ケースはコンストラクタのすべてのパラメータを抽象します。コンストラクタのパラメータの型が帰納型そのものである場合、ケースはさらにそのパラメータの値に適用される動機を型とするパラメータを取ります。これは再帰的なパラメータの再帰的な処理結果を受け取ります。
最後に、再帰子は型のインスタンスと添字の値を引数に取ります。
再帰子の結果の型は、これらの添字とターゲットに適用される動機です。
Bool の再帰子
Bool の再帰子 Bool.rec は以下のパラメータを持ちます：
動機は Bool から任意の宇宙における型を計算します。
false と true の両方で動機が満たされる両方のコンストラクタのケースが存在します。
ターゲットはなんらかの Bool です。
戻りの型はターゲットに適用される動機です。
Bool.rec.{u} {motive : Bool → Sort u}
(false : motive false)
(true : motive true)
(t : Bool) : motive tList の再帰子
List の再帰子 List.rec は以下のパラメータを持ちます：
パラメータとケースで参照されるため、パラメータ α が最初に来ます。
動機は List α から任意の宇宙における型を計算します。宇宙レベル u と v の間には何の関連もありません。
それぞれのコンストラクタのためのケースがあります：
この動機は List.nil を満たします。
この動機は後続のリストが満たされているならば List.cons のどの適用でも満たすことができるはずです。追加のパラメータ motive tail は tail の型が List の再帰的な出現であるためです。
ターゲットはなんらかの List です。
繰り返しになりますが、戻りの型はターゲットに適用される動機です。
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
定義 EvenOddList に対して：
inductive EvenOddList (α : Type u) : Bool → Type u where
| nil : EvenOddList α true
| cons : α → EvenOddList α isEven → EvenOddList α (not isEven)
再帰子 EvenOddList.rec は List のものと非常に似たものになります。違う箇所は添字の存在に由来します：
ここでは動機は任意の添字の選択を抽象化します。
nil のケースでは、 nil の添字の値 true に動機を適用しています。
cons のケースでは、再帰的な出現で使用される添字の値を抽象化し、その否定で動機をインスタンス化しています。
ターゲットでは追加で任意の添字の選択を抽象化しています。
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
動機に述語（つまり Prop を返す関数）を使用する場合、再帰子は帰納法を表現します。非再帰コンストラクタのケースは基本ケースであり、再帰引数を持つコンストラクタに供給される追加の引数は帰納法の仮定
Lean において証明は計算上 irrelevant です。言い換えると、ある命題の ある 証明が提供されたとき、プログラムが どの 証明を受け取ったかをチェックすることは不可能でなければなりません。これは帰納的に定義された命題や述語の再帰子の型に反映されています。これらの型では、定理の証明に複数の可能性がある場合、動機は別の Prop を返すだけです。型が高々1つの証明しかないような構造になっている場合、動機はどの宇宙でも型を返すことができます。高々1つしか存在しない命題を subsingleton と呼びます。可能な証明が1つしかないことをユーザに 証明 することを義務付ける代わりに、命題が subsingleton であるかどうかをチェックするための保守的な構文的近似が使われます。
コンストラクタを高々1つ持つ
各コンストラクタのパラメータの型は Prop ・パラメータ・添字のいずれかである
True は subsingleton
True はコンストラクタを1つ持ち、そのコンストラクタにパラメータが無いため subsingleton です。この再帰子は以下のシグネチャを持ちます：
True.rec.{u} {motive : True → Sort u}
(intro : motive True.intro)
(t : True) : motive tFalse は subsingleton
False はコンストラクタが無いため subsingleton です。この再帰子は以下のシグネチャを持ちます：
False.rec.{u} (motive : False → Sort u) (t : False) : motive t動機は明示的なパラメータであることに注意してください。これは動機がそれ以降のパラメータの型において言及されていないため、単一化では解決できなかったからです。
And は subsingleton
True はコンストラクタを1つ持ち、コンストラクタのパラメータの型は両方とも命題であるため subsingleton です。この再帰子は以下のシグネチャを持ちます：
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 tOr は subsingleton ではない
Or は複数のコンストラクタを持つため、subsingleton ではありません。この再帰子は以下のシグネチャを持ちます：
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動機の型は、それが他の命題への再帰にしか使えないことを示しています。選言の証明は何かしらを用いることで証明できますが、2つの選言のうち、どちらが真で証明に使われたかをプログラムが推察する方法はありません。
Eq は subsingleton
Eq はコンストラクタ Eq.refl を1つだけ持つため、subsingleton です。このコンストラクタは Eq の添字をパラメータの値でインスタンス化するため、すべての引数はパラメータです：
Eq.refl.{u} {α : Sort u} (x : α) : Eq x xこの再帰子は以下のシグネチャを持ちます：
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つまり、等号の証明は命題以外の型を書き換えるために使うことができます。
論理に新しい定数が追加されるだけでなく、帰納型宣言には新しい簡約規則も追加されます。これらの規則は再帰子とコンストラクタ、特にコンストラクタをターゲットとする再帰子の相互作用を支配します。この簡約の形式は ι簡約 （iota reduction）と呼ばれます。
再帰子のターゲットが再帰パラメータを持たないコンストラクタである場合、再帰子の適用はコンストラクタの引数へのコンストラクタのケースの適用に簡約されます。再帰パラメータがある場合は、再帰の出現に対して再帰を適用することでケースに対するこれらの引数を見つけることができます。
帰納型の宣言は、多くの適格要件に従います。これらの要件は、Lean が帰納的データ型の新しい規則で拡張された時に、論理としての一貫性が保たれることを保証します。これらの要件は保守的です：一貫性を損なわない帰納型だったとしてもこれらの要件はその帰納型を拒否する可能性があります。
帰納型の型コンストラクタは 宇宙 か戻り値が宇宙である関数型のどちらかに属さなければなりません。各コンストラクタは帰納型の完全な適用を返す関数型に属さなければなりません。もし帰納型の宇宙が Prop であれば、 Prop は impredicative であるため宇宙にはそれ以上の制限はありません。もし宇宙が Prop でない場合、コンストラクタの各パラメータについて以下が成り立つ必要があります：
コンストラクタのパラメータが（パラメータか添字かの意味で）帰納型のパラメータである場合、このパラメータの型は型コンストラクタの宇宙より大きくはできません。
その他のすべてのコンストラクタのパラメータは型コンストラクタの宇宙より小さくなければなりません。
Either はその引数の宇宙がどちらも帰納型のパラメータであるため、それらのうち大きい方の宇宙に存在します：
inductive Either (α : Type u) (β : Type v) : Type (max u v) where
| inl : α → Either α β
| inr : β → Either α β
CanRepr は α が帰納型のパラメータのいずれでもないため、コンストラクタのパラメータ α よりも大きな宇宙に存在します：
inductive CanRepr : Type (u + 1) where
| mk : (α : Type u) → [Repr α] → CanRepr
コンストラクタの無い帰納型はそのパラメータよりも小さな宇宙に存在することができます：
inductive Spurious (α : Type 5) : Type 0 where
しかし、 Spurious のレベルを変えずにコンストラクタを追加することは不可能です。
定義される型がコンストラクタの引数の型に出現する場合は、すべて strictly positive な位置になければなりません。ある位置が strictly positive であるとは、それが関数の引数型になく（その周囲にいくつの関数型がネストしていても同様です）、帰納型の型コンストラクタ以外の式の引数でない場合です。この制限により不健全な帰納型の定義は除外されますが、問題のないものも除外されます。
Bad 型はもし不許可でなければ Lean を矛盾した存在にしてしまいます：
inductive Bad where
| bad : (Bad → Bad) → Bad
(kernel) arg #1 of 'Bad.bad' has a non positive occurrence of the datatypes being declared
これは Bad という仮定の下で False を証明する循環論法を書くことが可能だからです。 Bad.bad はコンストラクタの引数の型が Bad → Bad であり、 Bad が引数の型として出現する関数型であるため却下されます。
Fix は f の引数として出現するため、この不動点演算子の宣言は却下されます：
inductive 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 は f が帰納型の型コンストラクタではなく、Fix 自身がその引数として出現するため却下されます。この場合、Fix も Bad と同等な型を構成するのに十分です：
def Bad : Type := Fix fun t => t → t
Lean は実用上多相的に使うことができない宇宙多相型を拒否します。これは宇宙パラメータの特定のインスタンス化によって型自体が Prop になる場合に発生する可能性があります。この型が subsingleton でない場合、再帰子は命題のみを対象とすることができます（つまり、 動機 は Prop を返さなければなりません）。このような型は Prop そのものとしてしか意味をなさないため、宇宙多相としたことは間違いだと考えられます。これらの型はほとんど役に立たないため、Lean の帰納型エラボレータはこれらの型をサポートするように設計されていません。
このような宇宙多相な帰納型が本当に subsingleton である場合、それらを定義することは意味があります。Lean の標準ライブラリは PUnit と PEmpty を定義しています。 Prop または Type に属することのできる subsingleton を定義するには、オプション bootstrap.inductiveCheckResultingUniverse を false に設定します。
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
Bool
任意の宇宙に存在できるバージョンの Bool の定義は許可されません：
inductive PBool : Sort u where
| true
| false
invalid universe polymorphic type, the resultant universe is not Prop (i.e., 0), but it may be Prop for some parameter values (solution: use 'u+1' or 'max 1 u') u
Lean のコア型理論が帰納型に対して規定している型コンストラクタ・コンストラクタ・再帰子に加えて、Lean は多くの補助構成を構築しています。まず、等式のコンパイラ（パターンマッチによる再帰関数を再帰子の適用に変換する）はこれらの追加のコンストラクタを使用します：
recOn は各コンストラクタのケースよりもターゲットが優先される再帰子のバージョンです。
casesOn は再帰子のバージョンであり、ターゲットが各コンストラクタのケースより前にあり、再帰的な引数は帰納法の仮定を生成しません。これは原始再帰ではなく、ケース分析を表現しています。
below はある動機に対して、ターゲットの部分木である帰納型の すべての 住人がその動機を満たすことを表現する型を計算します。これは、帰納法や原始再帰の動機を強再帰や強帰納法の動機に変換します。
brecOn は below を使用して、直前の再帰パラメータだけでなく、すべての部分木へのアクセスを提供する再帰子のバージョンです。これは強帰納法を表現しています。
noConfusion は一般的な文であり、そこからコンストラクタの単射性と不連結性を導き出すことができます。
noConfusionType は noConfusion に対して用いられ、2つのコンストラクタが等しい場合どうなるかを決定する動機です。別々のコンストラクタの場合、これは False です；両方のコンストラクタが同じであれば、それぞれのパラメータが等しいという結果になります。
整礎再帰 では、サイズの一般的な概念があると便利なことがよくあります。これは SizeOf クラスに含まれています。
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.
SizeOf.mk.{u} {α : Sort u} (sizeOf : α → Nat)
: SizeOf α |
sizeOf | : | α → Nat |
The "size" of an element, a natural number which decreases on fields of each inductive type. | ||
帰納型のランタイム表現は、それがいくつのコンストラクタを持つか・各コンストラクタがいくつの引数を取り、それらの引数が relevant であるかどうかの両方に依存します。
すべての帰納型がここで示されているように表現されるわけではありません。いくつかの帰納型は Lean のコンパイラによって特別にサポートされています：
固定幅整数 UInt8, ..., UInt64 ・ USize は、それぞれ C の uint8_t, ..., uint64_t と size_t 型で表されます。
Char は uint32_t で表現されます。
Float は double で表現されます。
列挙帰納的 （enum inductive）型は少なくとも2個から最大 2^32 個のコンストラクタを持ち、各コンストラクタはパラメータを持ちませんが、 uint8_t ・ uint16_t ・ uint32_t のうち各コンストラクタに一意な値を割り当てるのに十分な最初の型によって表現されます。例えば、 Bool 型は uint8_t で表現され、 false の場合は 0 、 true の場合は 1 になります。
Decidable α は Bool と同じように表現されます。
Nat は lean_object * で表現されます。そのランタイム値は不透明な任意精度整数オブジェクトへのポインタか、または「ポインタ」の最下位ビットが 1 の場合（lean_is_scalar でチェックされます）、ボックス化解除された自然数にエンコードされます（lean_box/lean_unbox）。
型と証明はランタイム表現を持ちません。つまり、帰納型が Prop である場合、その値はコンパイル前に消去されます。同様に、すべての定理文と型は消去されます。ランタイム表現を持つ型を relevant と呼び、ランタイム表現を持たない型を irrelevant と呼びます。
List.cons は以下のように3つのパラメータを持つシグネチャにも関わらず：
List.cons.{u} {α : Type u} : α → List α → List αこのランタイム表現では2つのみのパラメータとなります。なぜなら、型引数はランタイムでは irrelevant だからです。
Fin.mk は以下のように3つのパラメータを持つシグネチャにも関わらず：
Fin.mk {n : Nat} (val : Nat) : val < n → Fin nこのランタイム表現では2つのみのパラメータとなります。なぜなら、証明は消去されるからです。
ほとんどの場合、irrelevant な値は単にコンパイルされたコードから消えるだけです。しかし、何らかの表現が必要な場合（多相コンストラクタの引数など）、自明な値で表現されます。
帰納型が正確に1つのコンストラクタを持ち、そのコンストラクタが正確に1つのランタイムにおいて relevant なパラメータを持つならば、帰納型はそのパラメータと同一のものとして表現されます。
構造体 Subtype はある型の要素と、それがある述語を満たすことの証明を束ねたものです。コンストラクタは4つの引数を取りますが、そのうち3つは irrelevant です：
Subtype.mk.{u} {α : Sort u} {p : α → Prop}
(val : α) (property : p val) : Subtype p
このように、部分型はコンパイルされたコードにおいてランタイムのオーバーヘッドを発生させず、 val フィールドの型と同一のものとして表現されます。
帰納型が上記のカテゴリのいずれにも属さない場合、その表現はコンストラクタによって決定されます。relevant なパラメータを持たないコンストラクタは、コンストラクタのリストへのインデックスによって表現され、ボックス化解除された符号なし機械整数（スカラー）として表現されます。relevant なパラメータを持つコンストラクタは、ヘッダ・コンストラクタのインデックス・他のオブジェクトへのポインタの配列・型の順に並べられたスカラーのフィールドの配列を持つオブジェクトとして表現されます。ヘッダはオブジェクトの参照カウントやその他の必要な記録を追跡します。
再帰関数は帰納型の再帰子を使用するのではなく、ほとんどのプログラミング言語と同じようにコンパイルされます。再帰関数を再帰子にエラボレートするのは、実行ファイルのコードではなく、信頼された停止の根拠を提供するために役立てられます。
C の観点では、これらの帰納型は lean_object * として表現されます。各コンストラクタは lean_ctor_object として格納され、lean_is_ctor は真を返します。lean_ctor_object はコンストラクタのインデックスをヘッダに格納し、フィールドはオブジェクトの m_objs 部分に格納されます。
フィールドのメモリ順序は、宣言のフィールドの型とその並び順から導かれます。フィールドの並び順は以下に従います：
lean_object * として格納される非スカラーのフィールド
USize 型のフィールド
その他のスカラーのフィールドはサイズの降順で並ぶ
各グループ内では、フィールドは宣言順に並んでいます。警告：自明なラッパ型は、この目的のためにフィールドが非スカラーとして扱われます。
最初の種類のフィールドにアクセスするには、 lean_ctor_get(val, i) を使って i 番目の非スカラーフィールドを取得します。
USize フィールドにアクセスするには、lean_ctor_get_usize(val, n+i) を使って i 番目の USize フィールドを取得します。n は最初の種類のフィールドの総数です。
その他のスカラーフィールドにアクセスするには、lean_ctor_get_uintN(vai, off) または lean_ctor_get_usize(val, off) を適切に使用します。ここで off は構造体内のフィールドのバイトオフセットであり、n*sizeof(void*) から始まります。n はその前の2種類のフィールドの数です。
例えば、以下のような構造体があるとして、
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
これは以下のメモリ順序に再ソートされます：
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)
帰納型は相互に再帰することができます。帰納型の相互再帰定義は mutual ... end ブロックの中での型の定義として指定されます。
先の例の型 EvenOddList は真偽値の添字を使用して問題のリストの要素数が偶数か奇数かを選択しました。この区別は、2つの相互帰納型 EvenList と 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" .nil)
invalid dotted identifier notation, unknown identifier `OddList.nil` from expected type OddList String
mutual ブロックで宣言された帰納型は1つのグループとして扱われます；これらはすべて非相互再帰帰納型の適格な基準を一般化したものを満たさなければなりません。これらは実は相互に再帰的ではないため、mutual ブロック無しで定義できた場合でも同様です。
それぞれの型コンストラクタのシグネチャは、mutual グループ内の他の帰納型を参照することなくエラボレートできなければなりません。言い換えると、mutual グループ内の帰納型はお互いを引数として取ることはできません。それぞれの帰納型のコンストラクタは、非相互帰納型における再帰的な出現のための制限を一般化したもので、パラメータ型においてグループ内の他の型コンストラクタに言及することができます。
これらの帰納型は Lean に許容されません：
mutual
inductive FreshList (α : Type) (r : α → α → Prop) : Type where
| nil : FreshList α r
| cons (x : α) (xs : FreshList α r) (fresh : Fresh r x xs)
inductive Fresh (r : α → FreshList α → Prop) : α → 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
型コンストラクタは mutual グループの他の型コンストラクタを参照することはできないため、 FreshList は Fresh の型コンストラクタのスコープにありません：
unknown identifier 'FreshList'
mutual グループ内のすべての帰納型は同じ パラメータ を持たなければなりません。それらの添字は異なっていてもかまいません。
Both と OneOf は相互再帰的ではありませんが、同じ mutual ブロックで宣言されているため、同じパラメータを持たなければなりません：
mutual
inductive Both (α : Type u) (β : Type v) where
| mk : α → β → Both α β
inductive Optional (α : Type u) where
| none
| some : α → Optional α
end
invalid inductive type, number of parameters mismatch in mutually inductive datatypes
Many と OneOf は相互再帰的ではありませんが、同じ mutual ブロックで宣言されているため、同じパラメータを持たなければなりません。両者は正確に1つのパラメータを持っていますが、Many のパラメータは Optional のパラメータと同じ宇宙にあるとは限りません：
mutual
inductive Many (α : Type) : Type u where
| nil : Many α
| cons : α → Many α → Many α
inductive 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
相互グループ内の各帰納型の宇宙レベルは、非相互再帰的な帰納型と同じ要件に従わなければなりません。さらに、相互グループ内のすべての帰納型は同じ宇宙でなければならず、これはそれらのコンストラクタがパラメータの宇宙に関して同様に制限されることを意味します。
これらの相互帰納型はリストの連長圧縮を表すやや複雑な方法です：
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
PrefixRunOf を Prop として指定するほうが感覚的ですが、型が異なる宇宙になるためできません：
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 α → 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
この特殊な性質は、適格条件を個別に定義し、部分型を使用することで表現できます：
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! 🐙
mutual グループで定義される各帰納型は、グループ内のすべての型のコンストラクタのパラメータの型中において strict positively にのみ出現可能です。言い換えると、グループ内のすべての型の各コンストラクタのパラメータの型では、グループ内のどの型コンストラクタも矢印の左側には出現せず、帰納型の型コンストラクタの引き数でない限り引数の位置に出現しません。
以下の相互グループでは、Tm が Binding.scope の引数の negative な位置に出現しています：
mutual
inductive Tm where
| app : Tm → Tm → Tm
| lam : Binding → Tm
inductive Binding where
| scope : (Tm → Tm) → Binding
end
Tm は同じ相互グループの一部であるため、Binding のコンストラクタの引数としては strict positive にのみ出現しなければなりません。しかし、ここでは negative に出現しています：
(kernel) arg #1 of 'Binding.scope' has a non positive occurrence of the datatypes being declared
LocatedStx と Stx の定義は、再帰的な出現がどの矢印の左にもなく、引数である場合は帰納的な型コンストラクタの引数であるため、positivity の条件を満たします。
mutual
inductive LocatedStx where
| mk (line col : Nat) (val : Stx)
inductive Stx where
| atom (str : String)
| node (kind : String) (args : List LocatedStx)
end
相互帰納型には、非相互に定義された帰納型と同様に、原始再帰子が用意されています。これらの再帰子は、グループ内の他の型を処理しなければならないことを考慮し、それぞれの帰納型に対して動機を持つことになります。mutual グループ内のすべての帰納型は同一のパラメータを持つ必要があるため、再帰子はパラメータを最初に受け取り、動機と再帰子の残りの部分を抽象化します。さらに、再帰子はグループの他の型を処理する必要があるため、グループ内の各型コンストラクタについてのケースが必要になります。型の間の実施あの依存構造は考慮されません；相互依存関係が少ないことで追加の動機またはコンストラクタのケースが実際には必要ない場合でも、生成された再帰子はそれらを必要とします。
mutual
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
型 Two と Three はお互いを参照しないにもかかわらず、相互ブロック内で定義されています：
mutual
inductive Two (α : Type) where
| mk : α → α → Two α
inductive Three (α : Type) where
| mk : α → α → α → Three α
end
それにもかかわらず、 Two の再帰子である Two.rec は 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相互帰納型はコンパイルされたコードでもランタイムでも 非相互帰納型 と同一に表現されます。相互帰納型に対する制限は、Lean の論理としての一貫性を保証するために存在し、コンパイルされたコードには影響しません。