3.4. 帰納型（Inductive Types）🔗

帰納型 （inductive type）は Lean に新しい型を導入する主な手段です。 宇宙 と 関数 は組み込みのプリミティブでユーザが追加することはできませんが、Lean の他のすべての型は帰納型であるか、宇宙・関数・帰納型によって定義されたものであるかのどちらかです。帰納型は 型コンストラクタ （type constructor） と コンストラクタ （constructor） によって指定されます；帰納型の性質はこれらから導かれます。各帰納型は1つの型コンストラクタを持ち、 宇宙パラメータ と通常のパラメータの両方を取ることができます。帰納型は任意の数のコンストラクタを持つことができます；これらのコンストラクタは帰納型の型コンストラクタによってもたらされた型を持つ新しい値を導入します。

帰納型の型コンストラクタとコンストラクタに基づいて、Lean は 再帰子 （recursor）を導出します。論理的には、再帰子は帰納原理や除去則を表し、計算上は原始再帰計算を表します。再帰関数の停止は、再帰子の使用に変換することで正当化されるため、Lean のカーネルは再帰子の適用の型チェックを行うだけでよく、停止性の分析を別途行う必要はありません。Lean はさらに再帰子 再帰子 という用語は再帰的でない型でも常に使用されます。 に基づいた数多くの補助的な構成を提供しており、これはシステムの他の場所でも使用されます。

構造体 （structure）はコンストラクタを1つだけ持つ帰納型の特殊なケースです。構造体が宣言されると、Lean は新しい構造体で追加の言語機能を使用できるようにする補助関数を生成します。

本節では、帰納型と構造体の両方を指定するために使用される構文の具体的な詳細・帰納型の宣言から生じる環境内における新しい定数と定義・コンパイルされたコードにおける帰納型の値のランタイム表現について説明します。

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,*)?

新しい帰納型を宣言します。 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)）・宣言修飾子・名前で始まります。名前は 生識別子 です。名前の後に宣言シグネチャが続きます。このシグネチャは帰納的宣言の適格要件に従って任意のパラメータを指定することができますが、シグネチャの戻り型は指定された帰納型の型コンストラクタを完全に適用したものでなければなりません。シグネチャが提供されない場合、コンストラクタの型は適格な戻り値を構成するのに十分な暗黙のパラメータを挿入することによって推測されます。

新しい帰納型の名前は 現在の名前空間 で定義されます。各コンストラクタの名前は帰納型の名前空間に含まれます。

3.4.1.1. パラメータと添字（Parameters and Indices）🔗

型コンストラクタは2種類の引数を取ることができます： パラメータ （parameter）と 添字 （index, indices）です。パラメータは定義全体で一貫して使用されなければなりません；宣言内の各コンストラクタで型コンストラクタが出現する場合は、すべて正確に同じ引数を取る必要があります。添字は型コンストラクタの出現箇所によって異なっていてもかまいません。すべてのパラメータは、型コンストラクタのシグネチャのすべての添字の前にいなければなりません。

型コンストラクタのシグネチャのコロン（':'）より前に現れるパラメータはその帰納型宣言全体に対するパラメータと見なされます。これらは常にその型の定義全体を通して一様でなければならないパラメータです。一般的に言えば、コロンの後にあるパラメータは添字であり、型の定義全体を通して変化させることができます。しかし、オプション inductive.autoPromoteIndices が true の場合、構文としては添字でありながらパラメータになる可能性のあるものがパラメータとなります。添字がパラメータである可能性があるのは、その型の依存関係がすべてパラメータであり、帰納型の型コンストラクタのすべてのコンストラクタで一律にインスタンス化されていない変数として使用される場合です。

🔗option
inductive.autoPromoteIndices

Default value: true

Promote indices to parameters in inductive types whenever possible.

添字は型の 族 （family）を定義していると見なすことができます。添字を選択するごとに、その族から型が選択され、その型は使用可能なコンストラクタのあつまりを持ちます。添字を持つ型のコンストラクタは 添字付けられた型の族 （indexed family）の型を指定すると言われます。

3.4.1.2. 帰納型の例（Example Inductive Types）🔗

コンストラクタの無い型

Vacant は空の帰納型であり、Lean の Empty 型と同値です：

inductive Vacant : Type where

空の帰納型は無用なものではありません；到達不可能なコードを示すために使うことができます。

コンストラクタの無い命題

No は偽の 命題 であり、Lean の False と同値です：

inductive No : Prop where
ユニット型

One は Lean の Unit 型と同値です：

inductive One where | one

これは型コンストラクタとコンストラクタの両方のシグネチャが省略された帰納型の例です。Lean は One を Type に割り当てます：

One : Type#check One 
One : Type

コンストラクタ名は型コンストラクタの名前空間にあるため、コンストラクタ名は One.one です。 One は引数を期待しないため、 One.one のシグネチャは次のようになります：

One.one : One#check One.one 
One.one : One
真である命題

Yes は Lean の True 命題と同値です：

inductive Yes : Prop where | intro

One と異なり、この新しい帰納型 Yes は Prop 宇宙にあることが指定されています。

Yes : Prop#check Yes 
Yes : Prop

Yes.intro のシグネチャは以下のように推測されます：

Yes.intro : Yes#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 := 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

この宣言では、 α は パラメータ です。なぜなら、これは EvenOddList のすべての出現で一貫して使用されているからです。 b は 添字 であり、異なる出現で異なる 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 inductive datatype parameter mismatch α expected α✝| 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 パラメータに関する通常の規則によって発見されます。

3.4.1.3. 匿名コンストラクタ構文（Anonymous Constructor Syntax）🔗

帰納型がコンストラクタを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

3.4.1.4. インスタンスの導出（Deriving Instances）🔗

帰納的宣言のオプションとして、 Lean.Parser.Command.inductive : commandderiving 句は、型クラスのインスタンスを導出するために使用することができます。詳細は インスタンス導出についての節 を参照してください。

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,*)?

新しい構造体の型を宣言します。

構造体 （structure）は単一のコンストラクタを持ち、添字を持たない帰納型です。これらの制限と引き換えに、Lean は構造体のための数々の便利なコードを生成します：各フィールドに対して生成される射影関数・位置引数ではなくフィールド名に基づく追加のコンストラクタ構文が利用できる・同様の構文を使用して特定の名前付きフィールドの値を書き換えることができる・構造体は他の構造体を拡張することができる。他の帰納型と同様に、構造体も再帰的にすることができます；また strict positivity に関しても同じ制約を受けます。構造体は Lean の表現力を増すものではありません；構造体のすべての機能はコード生成によって実装されています。

3.4.2.1. 構造体のパラメータ（Structure Parameters）🔗

通常の帰納型宣言と同様に、構造体宣言のヘッダにはパラメータと結果の宇宙の両方を指定できるシグネチャが含まれます。構造体は 添字付けられた型の族 を定義することはできません。

3.4.2.2. フィールド（Fields）🔗

構造体宣言の各フィールドは、コンストラクタのパラメータに対応します。自動的な暗黙引数はたとえ名前が一致していても各フィールドに別々に挿入され、フィールドは型を量化するコンストラクタのパラメータになります。

構造体のフィールドの自動的な暗黙のパラメータ

構造体 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 から始まります。

3.4.2.3. 構造体のコンストラクタ（Structure Constructors）🔗

構造体のコンストラクタは、フィールドの前にコンストラクタ名と :: を指定することで明示的に名前を付けることができます。名前が明示的に与えられない場合、コンストラクタ名は構造体型の名前空間の 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))

構造体は単一コンストラクタの帰納型として表現されるため、そのコンストラクタは 匿名コンストラクタ構文 を使用して呼び出したり、マッチしたりすることができます。さらに、構造体は 構造体インスタンス （structure instance）の記法を用いて構築したり、マッチすることができます。構造体インスタンスの記法ではフィールド名とそれに紐づく値を含みます。

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)? }

指定されたフィールドの値が与えられたコンストラクタの型の値を構築します。フィールド指定子には2つの形式があります：

structInstField ::= ...
    | structInstLVal := term
structInstField ::= ...
    | 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 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)?}

コンストラクタの型の値を更新します。 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} ({ 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 := "" })

構造体型の値は、 Lean.Parser.Command.declValEqns : commandwhere とそれに続く各フィールドの定義を使用して宣言することもできます。これは定義の一部としてのみ使用でき、式の文脈では使用できません。

構造体での where

Lean の直積型は Prod という構造体です。直積は射影を使って定義できます：

def location : Float × Float where fst := 22.807 snd := -13.923

3.4.2.4. 構造体の継承（Structure Inheritance）🔗

構造体はオプションの 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 Textbook.toBook (self : Textbook) : Book#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 が得られます：

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

エラボレータは coords.fst を coords.toPair.fst に変換します。

構造体に部分型が無いこと

偶数・偶素数・具体的な偶数素数の定義が与えられている時：

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 に直接適用すると型エラーになります：

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

なぜなら EvenPrime 型の値は EvenNumber 型の値でもないからです。

3.4.3. 論理モデル（Logical Model）🔗

3.4.3.1. 再帰子（Recursors）🔗

全ての帰納型は 再帰子 を備えています。再帰子は型コンストラクタとコンストラクタのシグネチャによって完全に決定されます。再帰子は関数型を持ちますが、それはプリミティブであり、fun を使って定義することはできません。

3.4.3.1.1. 再帰子の型（Recursor Types）🔗

再帰子は以下のパラメータを取ります：

帰納型の パラメータ

パラメータは一貫しているため、これらは再帰子全体に対して抽象化することができます

動機 （motive）

動機は再帰子の適用の型を決定します。動機は型の添字とこれらの添字をインスタンス化した型のインスタンスを引数とする関数です。動機に決定される型の特定の宇宙は帰納型の宇宙とその特定のコンストラクタに依存します。詳細は 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 t
List の再帰子

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 を返す関数）を使用する場合、再帰子は帰納法を表現します。非再帰コンストラクタのケースは基本ケースであり、再帰引数を持つコンストラクタに供給される追加の引数は帰納法の仮定です。

3.4.3.1.1.1. Subsingleton 除去（Subsingleton Elimination）🔗

Lean において証明は計算上 irrelevant です。言い換えると、ある命題の ある 証明が提供されたとき、プログラムが どの 証明を受け取ったかをチェックすることは不可能でなければなりません。これは帰納的に定義された命題や述語の再帰子の型に反映されます。これらの型では、定理の証明に複数の可能性がある場合、動機はどれか1つの Prop を返すだけです。型が高々1つの証明しかないような構造になっている場合、動機はどの宇宙でも型を返すことができます。高々1つしか存在しない命題を subsingleton と呼びます。可能な証明が1つしかないことをユーザに 証明 することを義務付ける代わりに、命題が subsingleton であるかどうかをチェックするための保守的な構文的近似が使われます。命題は以下の要件をどちらも満たす場合に subsingleton であると考えられます：

  • コンストラクタを高々1つ持つ

  • コンストラクタのパラメータの各型は Prop ・パラメータ・添字のいずれかである

True は subsingleton

True はコンストラクタを1つ持ち、そのコンストラクタにパラメータが無いため subsingleton です。この再帰子は以下のシグネチャを持ちます：

True.rec.{u} {motive : True → Sort u} (intro : motive True.intro) (t : True) : motive t
False は 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 t
Or は 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

動機の型は、 Or.rec が証明を作成するためにのみ使用できることを示しています。選言の証明は何かしらを証明するために使うことができますが、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

つまり、等号の証明は命題以外の型を書き換えるために使うことができます。

3.4.3.1.2. 簡約（Reduction）🔗

論理に新しい定数が追加されるだけでなく、帰納型宣言には新しい簡約規則も追加されます。これらの規則は再帰子とコンストラクタ、特にコンストラクタをターゲットとする再帰子の相互作用を支配します。この簡約の形式は ι簡約 （iota reduction）と呼ばれます。

再帰子のターゲットが再帰パラメータを持たないコンストラクタである場合、再帰子の適用はコンストラクタの引数へのコンストラクタのケースの適用に簡約されます。再帰パラメータがある場合は、再帰の出現に対して再帰を適用することでケースに対するこれらの引数を見つけることができます。

3.4.3.2. 適格要件（Well-Formedness Requirements）🔗

帰納型の宣言は、多くの適格要件に従います。これらの要件によって、Lean が帰納的データ型の新しい規則で拡張された時に、論理としての一貫性が保たれることが保証されます。これらの要件は保守的です：一貫性を損なわない帰納型だったとしてもこれらの要件はその帰納型を拒否する可能性があります。

3.4.3.2.1. 宇宙レベル（Universe Levels）

帰納型の型コンストラクタは 宇宙 か戻り値が宇宙である関数型のどちらかに属さなければなりません。各コンストラクタは帰納型の完全な適用を返す関数型に属さなければなりません。もし帰納型の宇宙が Prop であれば、 Prop は 非可述 であるため宇宙にはそれ以上の制限はありません。もし宇宙が 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 のレベルを変えずにコンストラクタを追加することは不可能です。

3.4.3.2.2. Strict Positivity🔗

定義される型がコンストラクタの引数の型に出現する場合は、すべて strictly positive な位置になければなりません。ある位置が strictly positive であるとは、それが関数の引数型になく（その周囲にいくつの関数型がネストしていても同様です）、帰納型の型コンストラクタ以外の式の引数でない場合です。この制限により不健全な帰納型の定義は除外されますが、問題のないものも一定数除外されてしまいます。

非 strictly-positive な帰納型

Bad 型がもし不許可でなければ、Lean は矛盾した存在になってしまいます：

(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

これは Bad という仮定の下で False を証明する循環論法を書くことが可能だからです。 Bad.bad はコンストラクタの引数の型が Bad → Bad であり、 Bad が引数の型として出現する関数型であるため却下されます。

Fix は 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 は f が帰納型の型コンストラクタではなく、Fix 自身がその引数として出現するため却下されます。この場合、Fix も Bad と同等な型を構成するのに十分です：

def Bad : Type := Fix fun t => t → t

3.4.3.2.3. Prop vs Type🔗

Lean は実用上多相的に使うことができない宇宙多相型を拒否します。これは宇宙パラメータの特定のインスタンス化によって型自体が Prop になる場合に発生する可能性があります。この型が subsingleton でない場合、再帰子は命題のみを対象とすることができます（つまり、 動機 は Prop を返さなければなりません）。このような型は Prop そのものとしてしか意味をなさないため、宇宙多相としたことは間違いだと考えられます。これらの型はほとんど役に立たないため、Lean の帰納型エラボレータはこれらの型をサポートするように設計されていません。

このような宇宙多相な帰納型が本当に subsingleton である場合、それらを定義することは意味があります。Lean の標準ライブラリは PUnit と PEmpty を定義しています。 Prop または Type に属することのできる subsingleton を定義するには、オプション bootstrap.inductiveCheckResultingUniverse を 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

過剰に宇宙多相な Bool

任意の宇宙に存在できるバージョンの Bool の定義は許可されません：

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）🔗

Lean のコア型理論が帰納型に対して規定している型コンストラクタ・コンストラクタ・再帰子に加えて、Lean は多くの補助構成を構築しています。まず、等式のコンパイラ（パターンマッチによる再帰関数を再帰子の適用に変換する）はこれらの追加のコンストラクタを使用します：

  • recOn は各コンストラクタのケースよりもターゲットが先に来る再帰子のバージョンです。

  • casesOn は再帰子のバージョンであり、ターゲットが各コンストラクタのケースより前にあり、再帰的な引数は帰納法の仮定を生成しません。これは原始再帰ではなく、ケース分析を表現しています。

  • below はある動機に対して、ターゲットの部分木である帰納型の すべての 住人がその動機を満たすことを表現する型を計算します。これは、帰納法や原始再帰の動機を強再帰や強帰納法の動機に変換します。

  • brecOn は below を使用して、直前の再帰パラメータだけでなく、すべての部分木へのアクセスを提供する再帰子のバージョンです。これは強帰納法を表現しています。

  • noConfusion は一般的な文であり、そこからコンストラクタの単射性と不連結性を導き出すことができます。

  • noConfusionType は noConfusion に対して用いられ、2つのコンストラクタが等しい場合どうなるかを決定する動機です。別々のコンストラクタの場合、これは False です；両方のコンストラクタが同じであれば、それぞれのパラメータが等しいという結果になります。

整礎再帰 では、サイズの一般的な概念があると便利なことがよくあります。これは SizeOf クラスに含まれています。

🔗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）🔗

帰納型のランタイム表現は、それがいくつのコンストラクタを持つか・各コンストラクタがいくつの引数を取り、それらの引数が relevant であるかどうかの両方に依存します。

3.4.4.1. 例外（Exceptions）🔗

すべての帰納型がここで示されているように表現されるわけではありません。いくつかの帰納型は 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）。

3.4.4.2. Relevance🔗

型と証明はランタイム表現を持ちません。つまり、帰納型が Prop である場合、その値はコンパイル前に消去されます。同様に、すべての定理文と型は消去されます。ランタイム表現を持つ型を relevant と呼び、ランタイム表現を持たない型を irrelevant と呼びます。

型は irrelevant である

List.cons は以下のように3つのパラメータを持つシグネチャにも関わらず：

List.cons.{u} {α : Type u} : α → List α → List α

このランタイム表現では2つのみのパラメータとなります。なぜなら、型引数はランタイムでは irrelevant だからです。

証明は irrelevant である

Fin.mk は以下のように3つのパラメータを持つシグネチャにも関わらず：

Fin.mk {n : Nat} (val : Nat) : val < n → Fin n

このランタイム表現では2つのみのパラメータとなります。なぜなら、証明は消去されるからです。

ほとんどの場合、irrelevant な値は単にコンパイルされたコードから消えるだけです。しかし、何らかの表現が必要な場合（多相コンストラクタの引数など）、自明な値で表現されます。

3.4.4.3. 自明なラッパ（Trivial Wrappers）🔗

帰納型が正確に1つのコンストラクタを持ち、そのコンストラクタが正確に1つのランタイムにおいて relevant なパラメータを持つならば、帰納型はそのパラメータと同一のものとして表現されます。

オーバーヘッドのない部分型

構造体 Subtype はある型の要素と、それがある述語を満たすことの証明を束ねたものです。コンストラクタは4つの引数を取りますが、そのうち3つは irrelevant です：

Subtype.mk.{u} {α : Sort u} {p : α → Prop} (val : α) (property : p val) : Subtype p

このように、部分型はコンパイルされたコードにおいてランタイムのオーバーヘッドを発生させず、 val フィールドの型と同一のものとして表現されます。

3.4.4.4. その他の帰納型（Other Inductive Types）🔗

帰納型が上記のカテゴリのいずれにも属さない場合、その表現はコンストラクタによって決定されます。relevant なパラメータを持たないコンストラクタは、コンストラクタのリストへのインデックスによって表現され、ボックス化解除された符号なし機械整数（スカラー）として表現されます。relevant なパラメータを持つコンストラクタは、ヘッダ・コンストラクタのインデックス・他のオブジェクトへのポインタの配列・型の順に並べられたスカラーのフィールドの配列を持つオブジェクトとして表現されます。ヘッダはオブジェクトの参照カウントやその他の必要な記録を追跡します。

再帰関数は帰納型の再帰子を使用するのではなく、ほとんどのプログラミング言語と同じようにコンパイルされます。再帰関数の再帰子へのエラボレートは、実行ファイルのコードではなく、信頼された停止の根拠を提供するために役立てられます。

3.4.4.4.1. FFI🔗

C の観点では、これらの帰納型は lean_object * として表現されます。各コンストラクタは lean_ctor_object として格納され、lean_is_ctor は真を返します。lean_ctor_object はコンストラクタのインデックスをヘッダに格納し、フィールドはオブジェクトの m_objs 部分に格納されます。Lean は sizeof(size_t) == sizeof(void*) を仮定しています。これは C では保証されていませんが、Lean のランタイムシステムには、これが当てはまらない場合に失敗するアサートが含まれています。

フィールドのメモリ順序は、宣言のフィールドの型とその並び順から導かれます。フィールドの並び順は以下に従います：

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

3.4.5. 相互帰納型（Mutual Inductive Types）🔗

帰納型は相互に再帰することができます。帰納型の相互再帰定義は 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" 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）🔗

mutual ブロックで宣言された帰納型は1つのグループとして扱われます；これらはすべて非相互再帰帰納型の適格な基準を一般化したものを満たさなければなりません。これらは実際には相互に再帰的ではないため、mutual ブロック無しで定義できた場合でも同様です。

3.4.5.1.1. 相互依存（Mutual Dependencies）🔗

それぞれの型コンストラクタのシグネチャは、mutual グループ内の他の帰納型を参照することなくエラボレートできなければなりません。言い換えると、mutual グループ内の帰納型はお互いを引数として取ることはできません。非相互帰納型における再帰的な出現のための制限を一般化したものによって、それぞれの帰納型のコンストラクタはそれらのパラメータの型においてグループ内の他の型コンストラクタに言及することができます。

お互いに言及しない相互帰納型コンストラクタ

これらの帰納型は 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

型コンストラクタは mutual グループの他の型コンストラクタを参照することはできないため、 FreshList は Fresh の型コンストラクタのスコープにありません：

unknown identifier 'FreshList'

3.4.5.1.2. マッチすべきパラメータ（Parameters Must Match）🔗

mutual グループ内のすべての帰納型は同じ パラメータ を持たなければなりません。それらの添字は異なっていてもかまいません。

パラメータ数が異なる場合

Both と OneOf は相互再帰的ではありませんが、同じ mutual ブロックで宣言されているため、同一のパラメータを持たなければなりません：

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
パラメータの型が異なる場合

Many と OneOf は相互再帰的ではありませんが、同じ mutual ブロックで宣言されているため、同一のパラメータを持たなければなりません。両者は正確に1つのパラメータを持っていますが、Many のパラメータは Optional のパラメータと同じ宇宙にあるとは限りません：

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）🔗

相互グループ内の各帰納型の宇宙レベルは、非相互再帰的な帰納型と同じ要件に従わなければなりません。さらに、相互グループ内のすべての帰納型は同じ宇宙でなければならず、これはそれらのコンストラクタがパラメータの宇宙に関して同様に制限されることを意味します。

宇宙のミスマッチ

これらの相互帰納型はリストの連長圧縮を表すやや複雑な方法です：

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

この特殊な性質は、適格条件を個別に定義し、部分型を使用することで表現できます：

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🔗

mutual グループで定義される各帰納型は、グループ内のすべての型のコンストラクタのパラメータの型中において strict positively にのみ出現可能です。言い換えると、グループ内のすべての型の各コンストラクタのパラメータの型では、グループ内のどの型コンストラクタも矢印の左側には出現せず、帰納型の型コンストラクタの引き数でない限り引数の位置に出現しません。

相互 strict positivity

以下の相互グループでは、Tm が Binding.scope の引数の negative な位置に出現しています：

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

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

3.4.5.2. 再帰子（Recursors）🔗

相互帰納型には、非相互に定義された帰納型と同様に、原始再帰子が用意されています。これらの再帰子は、グループ内の他の型を処理しなければならないことを考慮し、それぞれの帰納型に対して動機を持つことになります。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

3.4.5.3. ランタイム表現（Run-Time Representation）🔗

相互帰納型はコンパイルされたコードでもランタイムでも 非相互帰納型 と同一に表現されます。相互帰納型に対する制限は、Lean の論理としての一貫性を保証するために存在し、コンパイルされたコードには影響しません。

3.4.5.4. Nested inductive types🔗

Planned Content

TODO

Tracked at issue #235