`inductive` 型¶

inductive は，constructor によって項を作る型を定義するコマンドです．

Sum，Option，List，Or，Exists，Eq は代表的な inductive 型です． Sum α β は左の型 α の値または右の型 β の値を持つ型で，α ⊕ β と書けます．数学の非交和 \(\alpha \sqcup \beta\) に対応します． Option α は値がある場合とない場合を表します． List α は有限列です． Or は命題の選言を表し，P ∨ Q と書けます． Exists は存在命題を表し，∃ x, P x と書けます． Eq は等式命題を表し，a = b と書けます．

実際の定義は，おおよそ次のようになっています． Sum と Exists は Init/Core.lean にあり，α ⊕ β は Sum α β の notation です．

lean4/src/lean/Init/Core.lean

inductive Sum (α : Type u) (β : Type v) where
  | inl (val : α) : Sum α β
  | inr (val : β) : Sum α β

@[inherit_doc] infixr:30 " ⊕ " => Sum

inductive Exists {α : Sort u} (p : α → Prop) : Prop where
  | intro (w : α) (h : p w) : Exists p

Eq，Option，List，Or は Init/Prelude.lean にあります．

lean4/src/lean/Init/Prelude.lean

inductive Eq : α → α → Prop where
  | refl (a : α) : Eq a a

inductive Option (α : Type u) where
  | none : Option α
  | some (val : α) : Option α

export Option (none some)

inductive List (α : Type u) where
  | nil : List α
  | cons (head : α) (tail : List α) : List α

inductive Or (a b : Prop) : Prop where
  | inl (h : a) : Or a b
  | inr (h : b) : Or a b

inductive 型を見るときは，次の 3 つを確認すると読みやすくなります．

型を作る部分: 何を入れると型ができるか．例: List : Type u → Type u
constructor: その型の項をどう作るか．例: List.nil，List.cons
消去・場合分け: match，cases，induction でどう使えるか．

inductive は，型そのものが引数を取る形でも定義できます．たとえば Option α や List α は，型 α を 1 つ受け取って新しい型を作ります．この場合，#check で型名だけを見ると，値の型ではなく「型から型を作る関数」のように見えます．

inductive MyOption (α : Type) where
  | none : MyOption α
  | some (x : α) : MyOption α

#check MyOption
#check (MyOption : Type → Type)
#check MyOption Nat
#check MyOption.none
#check MyOption.some

上の #check MyOption は，おおよそ

MyOption : Type → Type

という意味です． Lean の表示では MyOption (α : Type) : Type のように，引数つきの形で表示されることもあります． #check (MyOption : Type → Type) と型注釈を付けると，Type → Type と見えていることを明示できます．これは MyOption だけではまだ具体的な値の型ではなく， Nat や String などの型を受け取って MyOption Nat，MyOption String という型を作る，という意味です．一方，#check MyOption Nat は

MyOption Nat : Type

となります．つまり MyOption Nat は，「自然数が入っているかもしれない値」の型です．

def myOptionNat : MyOption Nat :=
  MyOption.some 3

def myOptionString : MyOption String :=
  MyOption.none

def myOptionGetD {α : Type} (default : α) : MyOption α → α
  | MyOption.none => default
  | MyOption.some x => x

example : myOptionGetD 0 myOptionNat = 3 := by
  rfl

example : myOptionGetD "empty" myOptionString = "empty" := by
  rfl

このように，引数を取る inductive 型では，まず MyOption Nat のように型引数を与えて具体的な型を作り，その型の項を constructor で作ります． List α や Option α も同じパターンです．

inductive Sign where
  | negative
  | zero
  | positive
deriving Repr, DecidableEq

def signNeg : Sign → Sign
  | Sign.negative => Sign.positive
  | Sign.zero => Sign.zero
  | Sign.positive => Sign.negative

example : signNeg Sign.positive = Sign.negative := by
  rfl

example : signNeg Sign.zero = Sign.zero := by
  rfl


def sumLeft : Nat ⊕ Int :=
  Sum.inl 10

def sumRight : Nat ⊕ Int :=
  Sum.inr (-10)

#check (Sum.inl 10)
#check (Sum.inr (-10))

def sumToInt (x : Nat ⊕ Int) : Int :=
  match x with
  | Sum.inl n => Int.ofNat n
  | Sum.inr z => z

example : sumToInt (Sum.inl 7) = (7 : Int) := by
  rfl

example : sumToInt (Sum.inr (-3)) = (-3 : Int) := by
  rfl

def safePred (n : Nat) : Option Nat :=
  match n with
  | 0 => none
  | m + 1 => some m

example : safePred 0 = none := by
  rfl

example : safePred 4 = some 3 := by
  rfl

def listExample : List Nat :=
  [1, 2, 3].map (fun n => n + 1)

example : listExample = [2, 3, 4] := by
  rfl

def headD {α : Type u} (default : α) : List α → α
  | [] => default
  | x :: _ => x

example : headD 0 [5, 6, 7] = 5 := by
  rfl

example : headD 0 ([] : List Nat) = 0 := by
  rfl

inductive 型は再帰的にも定義できます．次の Tree α は，値をもつ葉と，左右の部分木をもつ節点からなる二分木です．

inductive Tree (α : Type u) where
  | leaf (value : α)
  | node (left right : Tree α)

def Tree.size {α : Type u} : Tree α → Nat
  | Tree.leaf _ => 1
  | Tree.node left right => Tree.size left + Tree.size right

example : Tree.size (Tree.node (Tree.leaf 1) (Tree.leaf 2)) = 2 := by
  rfl

命題の選言 P ∨ Q は Or P Q，存在命題 ∃ x, P x は Exists (fun x => P x) という inductive 型です． Chapter 01 で P ∨ Q の証明に left や right を使ったのは，内部的には Or.inl や Or.inr で項を作っているからです．仮定 h : P ∨ Q に cases h を使うと 2 つのゴールに分かれるのは，Or の constructor が 2 つあるからです．

#check Or
#check Exists
#check Eq

example (P Q : Prop) (hP : P) : P ∨ Q :=
  Or.inl hP

example (P Q R : Prop) (h : P ∨ Q) (hPR : P → R) (hQR : Q → R) : R :=
  Or.elim h hPR hQR

example (n : Nat) : n = n :=
  Eq.refl n

演習¶

また，Or と Exists を notation を使わずに作ってみてください．

example (P Q : Prop) (hP : P) : Or P Q := by
  sorry

example : Exists (fun n : Nat => n = 2) := by
  sorry

inductive 型¶

演習¶

`inductive` 型¶