Lean 構文早見表

Lean 構文早見表(Lean by Example) は，Lean の基本的な構文や機能を紹介するためのサンプルコード集です．Lean の数多くの機能の全体を概観できる資料となることを目指しています．

本書は逆引きタクティクリストの姉妹編です．mathlibにあるタクティクや，# 付きの対話的コマンドについてはあちらを参照してください．

コメント

多くのプログラミング言語にある機能ですが，Lean でもコメントアウトの構文が存在します．

行コメント

-- はインラインコメントを表します．各行の -- 以降の文字列は無視されます．

-- これはコメントです

ブロックコメント

/- と -/ で囲まれた部分はブロックコメントとして認識され，やはり実行されません．

/-
これはブロックコメントです
複数行を一度にコメントアウトします．
-/

モジュールドキュメントと異なり，import 文より前に書くことができるという性質があります．

ドキュメントコメント

/-- と -/ で囲まれた部分はドキュメントコメントとして認識されます．これは直後に続く関数や変数に対する補足説明として認識されます．ドキュメントコメントとして与えた説明は，エディタ上でその関数や変数にカーソルを合わせることで表示されます．

/-- 挨拶です -/
def foo := "Hello World!"

/-- 1を加える関数 -/
def bar (n : Nat) : Nat := n + 1

モジュールドキュメント

/-! と -/ で囲まれた部分はモジュールドキュメントです．セクショニングコメントと呼ばれることもあります．これは慣習的にファイルやセクション, 名前空間の冒頭でそこで何が行われるかを説明するために使われます．¹

namespace Fibonacci

/-! ### フィボナッチ数列に関する定義 -/

/-- フィボナッチ数列の n 番目の要素 -/
def fib (n : Nat) : Nat :=
  match n with
  | 0 => 0
  | 1 => 1
  | n + 2 => fib (n - 1) + fib (n - 2)

end Fibonacci

なお細かい話として，モジュールドキュメントは import 文より前に書くとエラーになります．

フィールド記法

フィールド記法（ドット記法とも）とは，ある条件の下で関数適用 f x を x.f と書くことができる記法のことです．Nim 言語における Uniform Function Call Syntax に似た機能です．

典型的な使い方

Lean で構造体を定義すると，自動的にその構造体の各フィールドにアクセスするための関数が生成されます．構造体の名前が S で，フィールドの名前が x ならアクセサは S.x という名前になります．

/-- 平面上の点 -/
structure Point where
  x : Int
  y : Int

def p : Point := { x := 10, y := 20 }

-- `Point.x` で構造体の `x` フィールドにアクセスできる．
example : Point.x p = 10 := rfl

このとき，構造体の項 s : S に対して，S.x s を s.x と略記することができます．これが典型的なフィールド記法の使い方です．

example : p.x = 10 := rfl

一般のフィールド記法

構造体を例にしましたが，構造体に限ったことではありません．一般に関数 f があり，項 t : T があったとすると「f の T 型の非暗黙の引数のうち，最初のものに x を代入したもの」を x.f で表すことができます．

例えば，以下は同じことを表現したコードです．

example : List.map (fun x => x + 1) [1, 2, 3] = [2, 3, 4] := rfl

example : [1, 2, 3].map (fun x => x + 1) = [2, 3, 4] := rfl

よくあるエラー

以下のようなエラーが出てフィールド記法が使えないことがあります．このエラーの対処法については _root_ を参照してください．

invalid field 'foo', the environment does not contain 'Bar.foo'

依存型

Lean では型が値に依存することができます．これを依存型と呼びます．他の言語でこれができるものとしては，Idris などがあります．

これにより，たとえば関数 f : A → B の返り値の型が引数 a : A の値に依存することができ，そのような関数の型を (a : A) → B と書きます．これを特に依存関数型といいます．

全称命題と ∀ 記号

典型的なのは全称命題の表現です．

-- 自然数から命題への関数の型
-- `n + 0 = 0` 自体が型であることに注意
#check (n : Nat) → (n + 0 = n : Prop)

/-- 自然数から `n + 0 = n : Prop` への関数.
カリーハワード同型対応により，これは `∀ n, n + 0 = n` の証明であるとみなせる. -/
def add_zero : (n : Nat) → n + 0 = n := fun _n => rfl

-- 通常の書き方をした証明．
-- 返り値の型が `Prop` の項である場合，このように `∀` 記号を使うのが自然
theorem add_zero' : ∀ (n : Nat), n + 0 = n := by
  intro n
  rfl

型の中の条件分岐

「ある b : Bool の値に応じて，真なら自然数，偽なら文字列を返す」という関数も，型の中に if 式を組み込んで次のように表現できます．

def sample (b : Bool) : if b then Nat else String :=
  match b with
  | true => (3 : Nat)
  | false => "three"

ただし，コードの設計としては Nat と String を合成した型を自分で定義したほうがよいでしょう．

-- 自然数と文字列の和集合
inductive NatOrString : Type
  | natVal : Nat → NatOrString
  | strVal : String → NatOrString

-- コンストラクタを省略できるように型強制を定義する
instance : Coe Nat NatOrString := ⟨NatOrString.natVal⟩
instance : Coe String NatOrString := ⟨NatOrString.strVal⟩

def sample' (b : Bool) : NatOrString :=
  match b with
  | true => (3 : Nat)
  | false => "three"

引数のデフォルト値

Python や PHP などの言語と同様に，Lean でも関数の引数にデフォルト値を指定することができます．

たとえば，割り算で「分母がゼロのとき」への安全装置を実装した関数 safeDiv を定義してみましょう．複数のやり方がありますが，ここでは「分母がゼロでないという証明」を引数に取るようにしてみます．

/-- 分母がゼロでないことを要求する割り算 -/
def safeDiv (n m : Nat) (_h : m > 0) : Nat := n / m

-- 分母がゼロでないことの証明を渡す必要がある
#guard safeDiv 10 2 (by decide) = 5

しかし, こうすると割り算を行うたびに毎回引数に証明を渡す必要が生じます．これでは面倒ですね．ここで，引数の証明項にデフォルト値を設定することができます．そうすれば，毎回証明を渡さなくても済みます．

/-- 分母がゼロでないことを自動で証明しようとする割り算 -/
def safeDiv' (n m : Nat) (_h : m > 0 := by decide) : Nat := n / m

-- 分母がゼロでないことの証明を省略できる
#guard safeDiv' 10 2 = 5

-- 分母をゼロにするとエラー
#check_failure safeDiv' 10 0

デフォルト値を上書きするには，普通に値を渡せばよいです．

-- `contradiction` では示せないので失敗する
#check_failure safeDiv' (12) 3 (by contradiction)

正格評価

Lean は Haskell と同様に純粋関数型言語ですが，Haskell とは異なり 正格評価 です．つまり，関数を評価する前に引数をすべて評価します．これは純粋関数型ではない Python や Rust, Julia などと同様です．

次のコード例の selectFst は cond として true を渡されれば，単に fst を返します．つまり trace 20 は返り値には必要ないので，もし遅延評価なら評価されません. しかし実際には評価されるので，Lean は正格評価だとわかります．

/-- 条件 `cond` が true なら最初の引数を，
false なら2番目の引数を返す関数 -/
def selectFst (cond : Bool) (fst snd : Nat) :=
  if cond then
    fst
  else
    snd

/-- 与えられた自然数をそのまま返す関数.
実行されると infoview に表示が出る. -/
def trace (n : Nat) : Nat :=
  dbg_trace "trace is called"
  n

/--
info: trace is called
10
-/
#eval selectFst true 10 (trace 20)

なお if 式を直接評価した場合は，必要のない枝は評価されません．

/-- info: 10 -/
#eval (if true then 10 else trace 20)

無名コンストラクタ

無名コンストラクタは，構造体 T に対して T 型の項を構成する方法のひとつです．

これは以下に示すように，⟨x1, x2, ...⟩ という構文により使うことができます．

/-- 2つのフィールドを持つ構造体 -/
structure Hoge where
  foo : Nat
  bar : Nat

def hoge : Hoge := ⟨1, 2⟩

コンストラクタが入れ子になっていても平坦化することができます．例えば，以下の2つの定義は同じことをしています．

def foo : Nat × (Int × String) := ⟨1, ⟨2, "foo"⟩⟩

def foo' : Nat × (Int × String) := ⟨1, 2, "foo"⟩

一般の帰納型に対しては使用できません．

inductive Sample where
  | fst (foo bar : Nat) : Sample
  | snd (foo bar : String) : Sample

-- 「コンストラクタが一つしかない型でなければ使用できない」というエラーになる
#check_failure (⟨"foo", "bar"⟩ : Sample)

-- コンストラクタを指定しても使用できない
#check_failure (Sample.snd ⟨"foo", "bar"⟩ : Sample)

名前付き引数

Lean では，関数に引数を渡すときに順序ではなく名前で引数を指定することができます．

/-- 足したり掛けたりする関数 -/
def addMul (n m : Nat) := n + m * m

-- 通常, 引数は順序で指定されるが
#guard addMul 2 3 = 11

-- 名前付き引数を使うと，引数の順序を変えることができる
#guard addMul (m := 3) (n := 2) = 11

Functional but in-place

参照透過性

Lean は 純粋関数型言語 です．これはすべての関数が純粋で 参照透過性(referential transparency) を持つことを意味します．ここで関数 f が参照透過であるとは，次を意味します．

• 引数として同じ値を与えると毎回同じ値を返し，
• 式の値の評価以外の 副作用(side effect) を生まない

特に変数 a の値を参照する関数を考えると，関数の値が変わらないことから，変数 a の値は変更できないということがわかります．実際に Lean ではすべての変数は一度値を束縛すると値を変更できません．参照透過性を守るために，Lean は必要に応じて変数の値のコピーを行います．

-- foo という変数を定義する
def foo := "hello"

-- 再定義しようとするとエラーになる
/-- error: 'foo' has already been declared -/
#guard_msgs in def foo := "hello world"

-- 関数の内部で同名の `foo` という変数を定義することはできる
#eval show IO Unit from do
  let foo := foo ++ " world"
  IO.println foo

-- しかしグローバル変数としての `foo` の値は "hello" のまま変わっていない
#guard foo = "hello"

値の破壊的変更

しかし，Lean で変数の値の破壊的変更ができないわけではありません．できないどころか，容易に変数の値の破壊的変更を行うことができます．ここで破壊的変更とは，変数の値をコピーすることなく，in-place に値が変更されることを指します．次の例では，配列の値の変更が in-place に行われていることを確かめることができます．

-- Lean のオブジェクトのメモリ上でのアドレスを取得する関数
-- 参照透過性を壊すため，unsafe である
#eval ptrAddrUnsafe #[1, 2, 3]

/-- フィボナッチ数列を計算する -/
unsafe def fibonacci (n : Nat) : Array Nat := Id.run do
  -- 可変な配列 `fib` を宣言している
  let mut fib : Array Nat := Array.mkEmpty n
  fib := fib.push 0
  fib := fib.push 1
  for i in [2:n] do
    -- ここで配列 `fib` のメモリアドレスを表示させている
    dbg_trace ptrAddrUnsafe fib
    fib := fib.push (fib[i-1]! + fib[i-2]!)
  return fib

-- 値がコピーされていれば異なるメモリアドレスが表示されるはずだが...?
#eval fibonacci 15

Functional but in-place

なぜこのような現象が起こるのでしょうか？答えは，Lean が値の不要なコピーを行わないためです．具体的には，Lean は参照カウントがちょうど 1 であるような値を更新する際に，コピーして新しい値を生成する代わりに破壊的変更を行います．参照カウントが 1 の値はグローバル変数ではありませんし，その値を束縛している変数がその値を参照しているだけであるため，その値を変更しても参照透過性は保たれます．これを指して，Lean 言語のパラダイムのことを Functional but in-place と呼びます．¹

変数の参照カウントを調べるための関数も用意されており，次の例のようなコードで検証を行うことができます．

-- `α` は型で，`α` の要素の大小比較ができる
variable {α : Type} [Ord α]

-- コンパイラによる最適化が行われないようにし，
-- `dbgTraceIfShared` の直観的でない挙動を防ぐために `noinline` 属性を付与
@[noinline]
def Array.checkedSwap (a : Array α) (i j : Fin a.size) : Array α :=
  -- `dbgTraceIfShared` 関数は，引数の参照カウントが 1 より大きいときにメッセージを表示する
  -- これは，破壊的変更ができない場合に警告を出すと言ってもよい
  dbgTraceIfShared "array shared!" a |>.swap i j

/-- 挿入ソートのヘルパ関数.
要素 `arr[i]` を `arr[i-1]` と比較して，
`arr[i-1] ≤ arr[i]` となるように要素を入れ替える -/
def insertSorted (arr : Array α) (i : Fin arr.size) : Array α :=
  match i with
  | ⟨0, _⟩ => arr
  | ⟨i' + 1, _⟩ =>
    have : i' < arr.size := by
      simp [Nat.lt_of_succ_lt, *]
    match Ord.compare arr[i'] arr[i] with
    | .lt | .eq => arr
    | .gt =>
      -- 再帰呼び出しのたびに "called swap" を表示させる
      dbg_trace "called swap"

      -- 上で定義した `checkedSwap` を呼んで配列の値の swap を行う
      insertSorted
        (arr.checkedSwap ⟨i', by assumption⟩ i)
        ⟨i', by simp [Array.checkedSwap, dbgTraceIfShared, *]⟩

/-- 挿入ソートのヘルパ関数 -/
partial def insertionSortLoop (arr : Array α) (i : Nat) : Array α :=
  if h : i < arr.size then
    insertionSortLoop (insertSorted arr ⟨i, h⟩) (i + 1)
  else
    arr

/-- 挿入ソート -/
def insertionSort (arr : Array α) : Array α :=
  insertionSortLoop arr 0

def sample_array := #[1, 3, 2, 8, 10, 1, 1, 15, 2]

-- `swap` は何度も実行されているが，最初の一回だけ `shared RC ...` メッセージが表示される
-- 最初の一回はグローバル変数 `sample_array` が引数として与えられているので，破壊的変更は許されない
-- 後の呼び出しでは参照カウントが 1 になっていて，破壊的変更が許される状況
/--
info: called swap
shared RC array shared!
called swap
called swap
called swap
called swap
called swap
called swap
called swap
called swap
called swap
called swap
called swap
called swap
#[1, 1, 1, 2, 2, 3, 8, 10, 15]
-/
#guard_msgs in #eval insertionSort sample_array

_root_

_root_ は名前空間のルートを表します．主に名前空間を一時的に抜けるために使います．名前空間 Hoge の中で foo を定義すると Hoge.foo という名前になりますが，_root_.foo と定義すればこの挙動を避けて foo という名前にすることができます．

たとえば以下のように名前空間の中で List 配下の関数を定義し，フィールド記法を使おうとしてもうまくいきません．こういう場合に _root_ を使用すると，名前空間を閉じることなくエラーを解消できます．

namespace Root

variable {α : Type}

def List.unpack (l : List (List α)) : List α :=
  match l with
  | [] => []
  | x :: xs => x ++ unpack xs

/--
error: invalid field 'unpack', the environment does not contain 'List.unpack'
  [[1, 2], [3]]
has type
  List (List Nat)
-/
#check ([[1, 2], [3]] : List (List Nat)).unpack

-- エラーになる原因は，名前空間 `Root` の中で宣言したので
-- 関数名が `Root.List.unpack` になってしまっているから
#check Root.List.unpack

-- `_root_` を頭につけて再度定義する
def _root_.List.unpack (l : List (List α)) : List α :=
  match l with
  | [] => []
  | x :: xs => x ++ unpack xs

-- 今度は成功する
#eval [[1, 2], [3]].unpack

end Root

abbrev

abbrev は，別名を宣言する構文です．

たとえば，Nat 型に別の名前を与えたかったとしましょう．Lean では型も他の項と同様に宣言できるので，次のように書いて問題がないように見えます．

def NaturalNumber : Type := Nat

しかし，ここで定義した Nat の別名を項に対して使用するとエラーになります．これは，Lean が NaturalNumber を定義に簡約(reduce)するよりも先に，42 : NaturalNumber という表記が定義されているか OfNat のインスタンスを探そうとするためです．¹

/--
error: failed to synthesize instance
  OfNat NaturalNumber 42
-/
#check (42 : NaturalNumber)

ここでエラーを修正する方法の一つが，def の代わりに abbrev を使用することです．

abbrev NaturalNumber : Type := Nat

#check (42 : NaturalNumber)

舞台裏

abbrev は @[reducible] 属性のついた def と同じである²ため，定義に reducible という属性を与えても機能します．

@[reducible]
def NaturalNumber : Type := Nat

#check (42 : NaturalNumber)

attribute

attribute は，属性(attribute)を付与するためのコマンドです．

次の例では，命題に simp 属性を付与しています．これは simp タクティクで利用される命題を増やすことを意味します．

theorem foo {P Q : Prop} : (P → Q) ∧ P ↔ Q ∧ P := by
  constructor <;> intro h
  · obtain ⟨hPQ, hP⟩ := h
    constructor
    · apply hPQ
      assumption
    · assumption
  · obtain ⟨hP, hQ⟩ := h
    constructor
    · intro _
      assumption
    · assumption

-- `simp` では示せない
example {P Q : Prop} : (P → Q) ∧ P ↔ Q ∧ P := by
  simp
  sorry

-- `attribute` で属性を付与
attribute [simp] foo

-- `simp` で示せるようになった
example {P Q : Prop} : (P → Q) ∧ P ↔ Q ∧ P := by
  simp

与えた属性を削除することもできます．削除するには - を属性の頭に付けます．

-- `simp` 属性を削除
attribute [-simp] foo

example {P Q : Prop} : (P → Q) ∧ P ↔ Q ∧ P := by
  simp
  sorry

attribute コマンドを使用すると定義の後から属性を付与することができますが，定義した直後に属性を付与する場合は @[..] という書き方が使えます．

@[simp]
theorem bar {P Q : Prop} : (P → Q) ∧ P ↔ Q ∧ P := by
  constructor <;> intro h
  · obtain ⟨hPQ, hP⟩ := h
    constructor
    · apply hPQ
      assumption
    · assumption
  · obtain ⟨hP, hQ⟩ := h
    constructor
    · intro _
      assumption
    · assumption

example {P Q : Prop} : (P → Q) ∧ P ↔ Q ∧ P := by
  simp

class

class は型クラスを定義するための構文です．型クラスを用いると，複数の型に対して定義され，型ごとに異なる実装を持つような関数を定義することができます．例えば「和を取る操作」のような，Nat や Int や Rat など複数の型に対して同じ名前で定義したい関数を作りたいとき，型クラスが適しています．

/-- 証明なしのバージョンのモノイド -/
class Monoid (α : Type) where
  /-- 単位元 -/
  e : α

  /-- 二項演算 -/
  op : α → α → α

/-- 自然数はモノイド -/
instance : Monoid Nat where
  -- ゼロを単位元とする
  e := 0

  -- 加算を二項演算とする
  op := Nat.add

/-- 連結リストはモノイド -/
instance {α : Type} : Monoid (List α) where
  -- 空リストを単位元とする
  e := []

  -- リストの連結を二項演算とする
  op := List.append

-- `Nat` に対してモノイドの演算が使える
#guard Monoid.op 0 0 = 0

-- `List Nat` に対してモノイドの演算が使える
#guard Monoid.op [1] [2, 3] = [1, 2, 3]

-- `Nat` に対して単位元を取得する関数が使える
#guard (Monoid.e : Nat) = 0

-- `List Int` に対しても単位元を取得する関数が使える
#guard (Monoid.e : List Int) = []

舞台裏

構造体による型クラスの模倣

型クラスが行っていることを class を使わずにDIYしてみると，型クラスの理解が深まるでしょう．class として上で定義したものを，もう一度 structure として定義してみます．

/-- 構造体でモノイドクラスを真似たもの -/
structure Monoid' (α : Type) where
  e : α
  op : α → α → α

/-- 自然数がモノイドのインスタンスであるという主張を再現したもの -/
def instMonoid'Nat : Monoid' Nat where
  e := 0
  op := Nat.add

このとき構造体 Monoid' のフィールド Monoid'.e は，「Monoid' の項に対して α の要素を返す」関数なので，次のような型を持ちます．

/-- info: Monoid'.e {α : Type} (self : Monoid' α) : α -/
#check Monoid'.e

self : Monoid' α が暗黙の引数ではなく明示的な引数なので, 型クラスのように書くことはできません．

#check_failure (Monoid'.e : Nat)

しかし，インスタンスを引数として渡せば，型クラスのように Nat の要素を取り出すことができます．

#check (Monoid'.e instMonoid'Nat : Nat)

構造体による模倣と本物の型クラスの違いがどこにあるのかおわかりいただけたでしょうか．最大の違いは，引数の instMonoid'Nat が省略できるかどうかです．

インスタンス暗黙引数と型クラス解決

ここで(本物の)型クラスにおける単位元関数 e の型を調べてみると, self : Monoid' α が角括弧 [ .. ] で囲われていることがわかります．

/-- info: Monoid.e {α : Type} [self : Monoid α] : α -/
#check Monoid.e

これはインスタンス暗黙引数と呼ばれるもので，この場合 Lean に対して Monoid' α 型の項を自動的に合成するよう指示することを意味します．また，型クラスのインスタンス暗黙引数を自動的に合成する手続きのことを，型クラス解決と呼びます．

def

def は，関数や項を定義するための基本的な構文です．

def foo := "hello"

/-- 1を足す -/
def addOne (n : Nat) : Nat := n + 1

/-- 階乗関数 -/
def factorial (n : Nat) : Nat :=
  match n with
  | 0 => 1
  | n + 1 => (n + 1) * factorial n

#guard factorial 7 = 5040

なお関数を定義するとき，隣接する同じ型の引数に対しては : を使いまわすことができます．

def add (n m : Nat) : Nat := n + m

def threeAdd (n m l : Nat) : Nat := n + m + l

where

where キーワードを使うと，定義をする前に変数を使用することができます．主に，ヘルパー関数を宣言するために使用されます．

/-- 整数 `m, n` が与えられたときに `m` 以上 `n` 以下の整数のリストを返す -/
def range (m n : Int) : List Int :=
  loop m (n - m + 1).toNat
where
  loop (start : Int) (length : Nat) : List Int :=
    match length with
    | 0 => []
    | l + 1 => loop start l ++ [start + l]

deriving

deriving は，型クラスのインスタンスを自動的に生成します．

以下に示すように, deriving instance C for T とすると型 T に対して型クラス C のインスタンスを生成します．

inductive Color : Type where
  | red
  | green
  | blue

deriving instance Repr for Color

#eval Color.red

対象の型の直後であれば，省略して deriving C だけ書けば十分です．また複数の型クラスに対してインスタンスを生成するには，クラス名をカンマで続けます．

structure People where
  name : String
  age : Nat

deriving Inhabited, Repr

#eval (default : People)

よくあるエラー

なお，deriving で実装を生成できるのは，決まりきったやり方で実装できて，実装方法が指定されている型クラスのみです．実装方法が指定されていなければ使うことはできません．

/-- 自前で定義した型クラス -/
class Callable (α : Type) where
  call : α → String

/--
error: default handlers have not been implemented yet, class: 'Deriving.Callable' types: [Deriving.People]
-/
deriving instance Callable for People

example

example は名前を付けずに命題の証明をすることができるコマンドです．

より正確には，example : T := t は t が型 T を持っていることを確かめます．特に T の型が Prop であるときには，最初に述べた通り t は T の証明だとみなすことができます．

-- `1 + 1 = 2` は `rfl` で証明できる
example : 1 + 1 = 2 := rfl

-- `rfl` という項の型が `1 + 1 = 2` であると言っても同じこと
#check (rfl : 1 + 1 = 2)

-- `n + 0 = n` は `rfl` で証明できる
example {n : Nat} : n + 0 = n := rfl

-- `{n : Nat} → n + 0 = n` という依存関数型の項を `rfl` で構成できる, と言い換えられる
#check (rfl : {n : Nat} → n + 0 = n)

-- `[1, 2, 3]` は `List Nat` 型の項
example : List Nat := [1, 2, 3]

-- `#[1, 2, 3]` は `Array Nat` 型の項
example : Array Nat := #[1, 2, 3]

-- `true` は `Bool` 型の項
example : Bool := true

inductive

inductive コマンドは，帰納型(inductive type)を定義することができます．Lean でユーザが新しい型を定義する主要な方法です．

列挙型

帰納型の最も基本的な例は，次のような列挙型です．列挙型とは，固定された値のどれかを取るような型です．

/-- 真か偽のどちらかの値をとる型 -/
inductive Bool : Type where
  | true
  | false

#check (Bool.true : Bool)

列挙型は，帰納型の中でもすべてのコンストラクタが引数を持たないような特別な場合といえます．

一般の帰納型

一般には，帰納型のコンストラクタは引数を持つことができます．

universe u v

/-- `α` と `β` の直和型 -/
inductive Sum (α : Type u) (β : Type v) where
  | inl (a : α) : Sum α β
  | inr (b : β) : Sum α β

コンストラクタの引数の型が定義しようとしているその帰納型自身であっても構いません．

/-- ペアノの公理によって定義された自然数 -/
inductive Nat : Type where
  | zero : Nat
  | succ (n : Nat) : Nat

instance

instance は，型クラスのインスタンスを定義するための構文です．

/-- 平面 -/
structure Point (α : Type) where
  x : α
  y : α

/-- 原点 -/
def origin : Point Int := { x := 0, y := 0 }

-- 数値のように足し算をすることはできない
#check_failure (origin + origin)

/-- 平面上の点の足し算ができるようにする -/
instance {α : Type} [Add α] : Add (Point α) where
  add p q := { x := p.x + q.x, y := p.y + q.y }

-- 足し算ができるようになった
#check (origin + origin)

舞台裏

instance は @[instance] タグが付けられた def と同じように振る舞います．

-- `List` 同士を足すことはできない
#check_failure [1] + [2]

-- インスタンスを宣言する
@[instance]
def instListAdd {α : Type} : Add (List α) where
  add := List.append

-- リスト同士を足すことができるようになった
-- 実装としては，上で指定した通り `List.append` が使われる
#check [1] + [2]

namespace

namespace は，定義に階層構造を与えて整理するための構文です．名前空間 Foo の中で bar を定義すると，それは Foo.bar という名前になり，名前空間 Foo の中では短い名前 bar でアクセスできますが，名前空間を出るとアクセスにフルネームが必要になります．

なおここでは説明のために namespace の中をインデントしていますが，これは一般的なコード規約ではありません．

namespace Nat

  def isEven (n : Nat) : Bool := n % 2 == 0

  -- 同じ名前空間の中なら短い名前でアクセスできる
  #check isEven

end Nat

-- 名前空間の外に出ると，短い名前ではアクセスできない
#check_failure isEven

-- フルネームならアクセスできる
#check Nat.isEven

名前空間は入れ子にすることができます．

namespace Nat

  namespace Even

    def thirty := 30

  end Even

  #check Even.thirty

end Nat

#check Nat.Even.thirty

open

open は名前空間を開くためのコマンドです．

名前空間 N の中にある定義 S を使いたいとき，通常はフルネームの N.S を使う必要がありますが，open N とすることで短い別名 S でアクセスできるようになります．

namespace Hoge

  def foo := "hello"

end Hoge

-- 名前空間の外からだと `foo` という短い名前が使えない
#check_failure foo

section
  -- 名前空間 `Hoge` をオープン
  open Hoge

  -- `open` することで `foo` という短い名前が使えるようになる
  #check foo
end

-- セクションが終わると再び短い名前は使えなくなる
#check_failure foo

入れ子になった名前空間

名前空間 N₁ と N₂ が入れ子になっているとき，その下にある定義に短い名前でアクセスするには，open N₁ N₂ とすればよいです．

namespace Foo

  namespace Bar

    def baz := "world"

  end Bar

end Foo

-- 入れ子の名前空間を開く
-- `Foo` の後に `Bar` を開く必要がある
open Foo Bar

#check baz

名前空間と公理

また名前空間 Foo 内に bar という公理(axiom で宣言されたもの)が存在する場合，Foo を開くと同時に公理 Foo.bar もインポートされます．

open Classical

-- 選択原理
#print choice

variable (P : Prop)

-- 選択原理が仮定された状態になっているため，
-- 任意の命題が決定可能になっている
#synth Decidable P

section

section は，variable で宣言された引数のスコープを区切ることができます．

section
  variable (a : Type)

  -- 宣言したので有効
  #check a
end

-- `section` の外に出ると無効になる
#check_failure a

なお上記の例ではセクションの中をインデントしていますが，インデントする必要はありません．

また，セクションに名前を付けることもできます．名前を付けた場合は，閉じるときにも名前を指定する必要があります．

section hoge
  variable (a : Type)

  #check a
end hoge

セクションは入れ子にすることもできます．

section parent
  variable (a : Type)

  section child
    variable (b : Type)

    -- 親セクションで定義された引数は子セクション内でも有効
    #check a
  end child

  -- child セクションの外なので無効
  #check_failure b
end parent

-- parent セクションの外なので無効
#check_failure a

structure

structure は構造体を定義するためのコマンドです．構造体とは，複数のデータをまとめて一つの型として扱えるようにしたものです．

structure Point (α : Type) : Type where
  x : α
  y : α

構造体を定義すると，自動的に作られる関数があります．代表的なものは

• フィールドにアクセスするための関数．
• コンストラクタ.

の2つです．フィールドへのアクセサはフィールドの名前で，コンストラクタは mk という名前で作られます．

-- アクセサ
#check (Point.x : {α : Type} → (Point α) → α)
#check (Point.y : {α : Type} → (Point α) → α)

def origin : Point Int := { x := 0, y := 0 }

/-- フィールド記法でアクセサを使用する -/
example : origin.x = 0 := by rfl

-- コンストラクタ
#check (Point.mk : {α : Type} → α → α → Point α)

コンストラクタに mk 以外の名前を使いたい場合，:: を使って次のようにします．

structure Prod (α : Type) (β : Type) where
  gen ::
  fst : α
  snd : β

-- コンストラクタ
#check Prod.gen

項を定義する

構造体の項を定義したい場合，複数の方法があります．波括弧記法が好まれますが，フィールド名が明らかな状況であれば無名コンストラクタを使用することもあります．

-- コンストラクタを使う
def sample0 : Point Int := Point.mk 1 2

-- 波括弧記法を使う
def sample1 : Point Int := { x := 1, y := 2 }

-- 無名コンストラクタを使う
def sample2 : Point Int := ⟨1, 2⟩

-- `where` を使う
def sample : Point Int where
  x := 1
  y := 2

値の更新

Lean は純粋関数型言語なので「構造体のフィールドを更新する」ことはできませんが，既存の構造体のフィールドの一部だけを変更した新しい構造体の項を作ることはできます．

variable {α : Type} [Add α]

/-- `p : Point` の x 座標を 2 倍にする -/
def Point.doubleX (p : Point α) : Point α :=
  { p with x := p.x + p.x}

#check Point.doubleX origin

継承

既存の構造体に新しいフィールドを追加した新しい構造体を定義することができます．多重継承(複数の親を持つ構造体を作ること)も行うことができます．

structure Point3D (α : Type) extends Point α where
  z : α

structure RGBValue where
  red : Nat
  green : Nat
  blue : Nat

structure ColorPoint3D (α : Type) extends Point α, RGBValue where
  z : α

舞台裏

構造体は，帰納型の特別な場合であり，コンストラクタが一つしかないケースに対応します．上記の Point は以下のように定義しても同じことです．ただしこの場合，アクセサ関数が自動的に作られないため，フィールド記法は自分で実装しないと使用できないほか，波括弧記法が使えません．

inductive Point' (α : Type) : Type where
  | mk : (x : α) → (y : α) → Point' α

-- フィールド記法が利用できない
#check_failure Point'.x

-- 無名コンストラクタは使用できる
def origin' : Point Int := ⟨0, 0⟩

-- 波括弧記法は使用できない
#check_failure ({ x := 1, y := 2 } : Point' Int)

theorem

theorem は名前付きで命題を証明するための構文です．より正確には，theorem は証明項を定義するための構文だといえます．

/-- 自然数に右から0を足しても変わらない -/
theorem add_zero {n : Nat} : n + 0 = n := by simp

-- `add_zero` という項の型が，命題の内容になっている
#check (add_zero : ∀ {n : Nat}, n + 0 = n)

def との違い

theorem コマンドは特定の型を持つ項を定義するという意味で，def と同じです．実際，def を使っても証明項を定義することは可能です. しかし theorem を使っても関数などを定義することはできません．theorem で宣言できる項は命題のみです．

def add_zero' {n : Nat} : n + 0 = n := by simp

/--
error: type of theorem 'Theorem.frac' is not a proposition
  Nat → Nat
-/
theorem frac (n : Nat) : Nat :=
  match n with
  | 0 => 1
  | n + 1 => (n + 1) * frac n

variable

variable は，定理や関数の引数を宣言するための構文です．

たとえば以下の関数と命題に対して，引数の α : Type と l : List α は共通です．

/-- 連結リストの最後の要素を取り出す -/
def last? {α : Type} (l : List α) : Option α :=
  match l with
  | [] => none
  | [a] => some a
  | _ :: xs => last? xs

theorem nng_list_length {α : Type} (l : List α) : l.length >= 0 := by simp

variable コマンドを利用すると，共通の引数を宣言してまとめておくことができます．

variable {α : Type} (l : List α)

/-- 連結リストの最後の要素を取り出す -/
def last? (l : List α) : Option α :=
  match l with
  | [] => none
  | [a] => some a
  | _ :: xs =>last? xs

theorem nng_list_length : l.length >= 0 := by simp

上記の２つの例で引数の l : List α を省略できるかどうかに違いがありますが，これは返り値の型に現れているかどうかに依ります．

partial

partial は部分関数(partial function)を定義するための構文です．

Lean では再帰関数も再帰的でない関数と同様に定義できますが，扱いは異なります．再帰的な関数 f を定義すると，Lean は f がすべての入力に対して必ず有限回の再帰で停止することを証明しようとします．自動的な証明が失敗すると，エラーになってしまいます．エラーを消すには，

• 停止することを手動で証明するか
• 停止性は保証しないと明示的にマークするか

どちらかの対応が必要です．関数の定義に partial とマークすると, 停止性は保証しないとマークしたことになります．

/--
error: fail to show termination for
  WithoutPartial.alternate
with errors
argument #2 was not used for structural recursion
  failed to eliminate recursive application
    alternate ys xs

argument #3 was not used for structural recursion
  failed to eliminate recursive application
    alternate ys xs

structural recursion cannot be used

Could not find a decreasing measure.
The arguments relate at each recursive call as follows:
(<, ≤, =: relation proved, ? all proofs failed, _: no proof attempted)
            xs ys
1) 38:24-39  ?  ?
Please use `termination_by` to specify a decreasing measure.
-/
#guard_msgs (whitespace := lax) in
def alternate {α : Type} (xs ys : List α) : List α :=
  match xs, ys with
  | [], ys => ys
  | x :: xs, ys => x :: alternate ys xs

-- `partial` を使うと，停止性の証明が不要になる
partial def alternate {α : Type} (xs ys : List α) : List α :=
  match xs, ys with
  | [], ys => ys
  | x :: xs, ys => x :: alternate ys xs

#guard alternate [1, 3, 5] [2, 4, 6] = [1, 2, 3, 4, 5, 6]

なお，partial とマークされた定義を元に新たに関数を定義するとき，再度 partial とマークする必要はありません．

def more_alternate := @alternate

private

private は，その定義があるファイルの中でだけ参照可能になるようにする修飾子です．他のファイルからはアクセス不能になります．

不安定なAPIなど，外部に公開したくないものに対して使うのが主な用途です．

なお private コマンドでセクションや名前空間にスコープを制限することはできません．

namespace Hoge
  section
    -- private とマークした定義
    private def addOne (n : Nat) : Nat := n + 1
  end
end Hoge

open Hoge

-- アクセスできる
#check addOne

以下の例 ¹ のように，変数のスコープを制限するようなセクションの変種を自作することは可能です．

open Lean Elab Command

elab "private section" ppLine cmd:command* ppLine "end private section": command => do
  let old ← get
  try
    for cmd in cmd do
      elabCommandTopLevel cmd
    throwAbortCommand
  finally
    set old

private section
  def foo := "hello!!"

  -- セクションの中なら当然アクセスできる
  #check foo
end private section

-- `foo` にアクセスできない
#check_failure foo

protected

protected は，ある名前空間 Hoge にある定義 foo に対して，必ずフルネームの Hoge.foo でアクセスすることを強要するものです．

structure Point where
  x : Nat
  y : Nat

namespace Point

  protected def sub (p q : Point) : Point :=
    { x := p.x - q.x, y := p.y - q.y }

  -- 名前空間の中にいても，短い名前ではアクセスできない
  #check_failure sub

  -- フルネームならアクセスできる
  #check Point.sub

end Point

open Point

-- 名前空間を開いていても，短い名前でアクセスできない
#check_failure sub

-- フルネームならアクセスできる
#check Point.sub

noncomputable

noncomputable は，宣言された関数が計算可能でないことを Lean に伝えるために使われます．

Lean は，def で定義された関数はすべて計算可能であると想定しています．したがって，計算可能でない関数を定義すると，エラーが発生します．

計算可能でない関数が生じるのは，選択原理 Classical.choice を使用したときです．選択原理は，型が「空ではない」という証明だけから，その型の項を魔法のように構成できると主張している公理です．空ではないという情報から具体的な項の情報は得られないため，選択原理を使用した関数は計算不能になります．

variable {X Y : Type}

-- 写像 `f : X → Y` が全射であること
def Surjective (f : X → Y) : Prop := ∀ y, ∃ x, f x = y

-- 全射な関数の逆写像を構成する
-- しかし，全射という情報だけからは逆写像を具体的に作ることはできないので，
-- 計算不能になりエラーになってしまう
/--
error: failed to compile definition, consider marking it as 'noncomputable'
because it depends on 'Classical.choice', and it does not have executable code
-/
#guard_msgs in def inverse' (f : X → Y) (hf : Surjective f) : Y → X := by
  -- `y : Y` が与えられたとする
  intro y

  -- `f` は全射なので `{x // f x = y}` は空ではない
  have : Nonempty {x // f x = y} := by
    let ⟨x, hx⟩ := hf y
    exact ⟨⟨x, hx⟩⟩

  -- 選択原理を用いて，`f x = y` なる `x : X` を構成する
  have x := Classical.choice this
  exact x.val

-- `noncomputable` という修飾子を付ければ，エラーは回避できる
noncomputable def inverse (f : X → Y) (hf : Surjective f) : Y → X := by
  intro y

  have : Nonempty {x // f x = y} := by
    let ⟨x, hx⟩ := hf y
    exact ⟨⟨x, hx⟩⟩

  have x := Classical.choice this
  exact x.val

noncomputable とマークされた式を含む式は文字通り評価不能になり，#eval に渡すことができなくなります．

-- 補助として `id` という恒等写像が全射であることを示しておく
theorem id_surjective : Surjective (id : Nat → Nat) := by
  intro y
  exists y

-- `id` の逆写像を構成する
noncomputable def id_inverse := inverse (id : Nat → Nat) id_surjective

-- 逆写像の `3` での値を評価しようとするとエラーになる
/--
error: failed to compile definition, consider marking it as 'noncomputable'
because it depends on 'id_inverse', and it does not have executable code
-/
#guard_msgs in #eval id_inverse 3

Fin

Fin は，ある数 i : Nat とそれがある数 n : Nat 未満であるという情報を組にしたものです．Fin n は n 未満の自然数全体の集合を表します．

/--
info: structure Fin : Nat → Type
number of parameters: 1
constructor:
Fin.mk : {n : Nat} → (val : Nat) → val < n → Fin n
fields:
val : Nat
isLt : ↑self < n
-/
#guard_msgs in #print Fin

variable (n : Nat)

-- 自然数 `n : Nat` と，`n` より小さい自然数 `val : Nat` から，`Fin n` の項が得られる
-- つまり `Fin n` は `n` 未満の自然数全体の集合
#check (Fin.mk : (val : Nat) → val < n → Fin n)

パイプライン演算子

関数型言語らしく，Lean にもパイプライン演算子があります．

|> 演算子

関数 f : α → β と x : α に対して x |> f は f x と同じです．

def pipe₁ := [1, 2, 3, 4, 5]
  |> List.map (· + 10)
  |> List.filter (· % 2 == 0)

#guard pipe₁ = [12, 14]

|>. を使用すればフィールド記法が利用できます．

def pipe₂ := [1, 2, 3, 4, 5]
  |>.map (· + 10)
  |>.filter (· % 2 == 0)

#guard pipe₂ = [12, 14]

<| 演算子

関数 f : α → β と x : α に対して f <| x は f x と同じです．関数適用と変わらないようですが，パイプラインを使うと括弧が要らなくなるという利点があります．

#check ([[]] : List <| List Nat)

#check ([[[]]] : List <| List <| List Nat)

<| は $ で書くこともできます．同じ意味になりますが，<| を使うべきであるとされています．¹

#check ([[]] : List $ List Nat)

#check ([[[]]] : List $ List $ List Nat)

Coe

Coe は，型強制(coercion)と呼ばれる仕組みをユーザが定義するための型クラスです．

ある型 T が期待される場所に別の型の項 s : S を見つけると，Lean は型エラーにする前に自動的に型変換を行うことができないか試します．ここで行われる「自動的な型変換」が型強制です．型強制を明示的に指定するには，↑ 記号をつけて ↑x などのようにします．

具体的には Coe S T という型クラスのインスタンスが定義されているとき，型 S の項が型 T に変換されます．

例えば，正の自然数からなる型 Pos を定義したとします．包含関係から Pos → Nat という変換ができるはずです．この変換を関数として定義するだけでは，必要になるごとに毎回書かなければなりませんが，型強制を使うと自動化することができます．

inductive Pos where
  | one : Pos
  | succ : Pos → Pos

def one : Pos := Pos.one

-- `List.drop` の引数は `Nat` なのに，`Pos` を渡したのでエラーになっている
#check_failure [1, 2, 3].drop one

/-- `Pos` から `Nat` へ変換する -/
def Pos.toNat : Pos → Nat
  | one => 1
  | succ n => n.toNat + 1

instance : Coe Pos Nat where
  coe n := n.toNat

-- 自動的に `Pos` から `Nat` への変換が行われてエラーにならない
#check [1, 2, 3].drop one

-- 明示的に型強制を行った例
#check [1, 2, 3].drop (↑one)

CoeDep

CoeDep は型強制を行うための型クラスですが，Coe と異なり「項に依存する型強制」(dependent coercion)を行うことができます．

たとえば空でないリストからなる型 NonEmptyList を定義したとします．空リストを変換する方法がないため，List α → NonEmptyList α という変換を定義する自然な方法はありません．しかし CoeDep を使えば空でないリストに限って NonEmptyList に変換するという型強制を定義することができます．

structure NonEmptyList (α : Type) : Type where
  head : α
  tail : List α

-- リストから `NonEmptyList` に変換することができない
#check_failure ([1, 2] : NonEmptyList Nat)

variable {α : Type}

instance (x : α) (xs : List α) : CoeDep (List α) (x :: xs) (NonEmptyList α) where
  coe := {
    head := x
    tail := xs
  }

-- 変換できるようになる
#check ([1, 2] : NonEmptyList Nat)

CoeFun

CoeFun は，関数型を持たない項を関数型に強制することができる型クラスです．

/-- 加法的な関数 -/
structure AdditiveFunction : Type where
  /-- 関数部分 -/
  func : Nat → Nat

  /-- 加法を保つ -/
  additive : ∀ x y, func (x + y) = func x + func y

/-- 恒等写像 -/
def identity : AdditiveFunction := ⟨id, by intro x y; rfl⟩

#check (identity : AdditiveFunction)

-- `identity` の型は `AdditiveFunction` であって，関数ではないのでこれはエラーになる
#check_failure (identity 1)

-- `CoeFun` を使って `AdditiveFunction` の項を関数型 `Nat → Nat` に強制する
instance : CoeFun AdditiveFunction (fun _ => Nat → Nat) where
  coe f := f.func

-- まるで関数のように使えるようになる
#check (identity 1)

上記の例ではどんな t : AdditiveFunction も同じ型 Nat → Nat に強制していますが，実際には依存関数型に強制することができます．

CoeSort

CorSort は Coe と同じく型強制を定義するための型クラスですが，項ではなく型に対して適用されるところが違います．

たとえば，モノイドという数学的対象をどう形式化するか考えてみましょう．モノイドとは，集合 M とその上の二項演算 * : M → M → M であって，結合律を満たし，単位元を持つものです．インフォーマルには，「くっつける」演算が定義されている集合と考えても良いでしょう．たとえば自然数は加法に対してモノイドですし，文字列は連結に対してモノイドです．

ここでは以下のように形式化します．¹

structure Monoid where
  /-- 台集合 -/
  Carrier : Type

  /-- 単位元 -/
  neutral : Carrier

  /-- 二項演算 -/
  op : Carrier → Carrier → Carrier

自然数やリストがモノイドであることを，上記の定義に基づいて形式化すると次のようになります．

def natAddMonoid : Monoid :=
  {
    Carrier := Nat,
    neutral := 0,
    op := (· + ·)
  }

def listMonoid (α : Type) : Monoid :=
  {
    Carrier := List α,
    neutral := [],
    op := (· ++ ·)
  }

ここでこの2つのモノイドの間の関数として，リストの長さを与える関数を考えてみます．

def length {α : Type} (xs : (listMonoid α).Carrier) : (natAddMonoid).Carrier :=
  List.length xs

型アノテーションの中で Carrier が繰り返し現れています．上記でモノイドを「集合と演算の組」として定義したため，モノイドを集合とみなすことができないためです．毎回 Carrier を補うのは面倒に感じますね．CoeSort を使えば，このようなルーティンな型変換を自動で行うことができます．

instance : CoeSort Monoid Type where
  coe m := m.Carrier

-- 単に `listMonoid α` と書いただけで，`Carrier` への変換が暗黙的に行われる
def length' {α : Type} (xs : listMonoid α) : natAddMonoid :=
  List.length xs

Inhabited

Inhabited は，ある型にデフォルトの項があることを示す型クラスです．

Inhabited のインスタンスである型は，default という項を持ちます．

variable {α : Type} [Inhabited α]

#check (default : α)

Inhabited の注意すべき使われ方として，クラッシュする関数の返り値として呼ばれるというものがあります．

たとえば a : Array に対して i 番目の要素を取り出す処理を考えます．i 番目の要素が存在するとは限らないので，例外の処理が必要です．一つの方法は，「i 番目の要素がなければエラーにする」というものです．

def get (a : Array α) (i : Nat) : α :=
  if h : i < a.size then
    a.get ⟨i, h⟩
  else
    panic! "index out of bounds"

何気ない定義のように見えますが，この定義には Inhabited α が必要です．panic! でプログラムをクラッシュさせているのですが，このときに α が空でないことが要求されています．

これは Lean が定理証明支援系としてもプログラミング言語としても使えるようにするための技術的な制約からくる仕様です．もし空の型を返してプログラムがクラッシュすることが許されたとすると，「空の型は False に等しい」ので，クラッシュするプログラムを False の証明として扱える可能性が生じてしまいます．

Repr

Repr は，その型の項をどのように表示するかを指示する型クラスです．

たとえば，以下のように新しく構造体 Point を定義したとき，特に何も指定しなければ Point の項を #eval で表示することはできません．

-- 平面上の点を表す構造体
structure Point (α : Type) : Type where
  x : α
  y : α

-- 原点
def origin : Point Nat := ⟨0, 0⟩

/--
error: expression
  origin
has type
  Point Nat
but instance
  Lean.Eval (Point Nat)
failed to be synthesized, this instance instructs Lean on how to display the resulting value, recall that any type implementing the `Repr` class also implements the `Lean.Eval` class
-/
#eval origin

エラーメッセージが示すように，これは Point が型クラス Lean.Eval のインスタンスではないからです．エラーメッセージには，Repr クラスのインスタンスであれば自動的に Lean.Eval のインスタンスにもなることが書かれています．通常，Lean.Eval のインスタンスを手で登録することはなく，Repr インスタンスによって自動生成させます．

Repr インスタンスの登録方法ですが，通り一遍の表示で構わなければ deriving コマンドで Lean に自動生成させることができます．

deriving instance Repr for Point

#eval origin

あるいは，Point の定義時に以下のようにしても構いません．

structure Point (α : Type) : Type where
  x : α
  y : α
deriving Repr

def origin : Point Nat := ⟨0, 0⟩

#eval origin

ToString

ToString は，文字列への変換を行う型クラスです．

structure Point (α : Type) where
  x : α
  y : α

def origin : Point Int := ⟨0, 0⟩

-- 文字列補完により文字列に変換しようとしても，
-- 最初はどう変換したらいいのかわからないのでエラーになる
#check_failure s!"{origin}"

/-- `ToString` のインスタンスを登録する -/
instance : ToString (Point Int) where
  toString p := s!"Point: ({p.x}, {p.y})"

-- これで文字列に変換できる
#eval s!"{origin}"

なお，Repr のインスタンスがないが，ToString のインスタンスはある状態で #eval しようとすると，Repr の代わりに ToString のインスタンスが使用されます．Repr のインスタンスを与えればそちらが優先して使用されます．

/-- info: Point: (0, 0) -/
#eval origin

-- `Repr` のインスタンスを自動生成して登録する
-- 以降は，`#eval` 時には `Repr` のインスタンスが使用される
deriving instance Repr for Point

/-- info: { x := 0, y := 0 } -/
#eval origin

notation

notation は，新しい記法を導入するためのコマンドです．

/-- 各 `k` に対して，二項関係 `a ≃ b mod k` を返す -/
def modulo (k a b : Int) : Prop :=
  k ∣ (a - b)

notation a " ≃ " b " mod " k => modulo k a b

#check (3 ≃ 7 mod 4)

次のような例も作ることができます．

notation "[" x " ... " y "]" => List.range y |> List.drop x

example : [1 ... 10] = [1, 2, 3, 4, 5, 6, 7, 8, 9] := by rfl