制御構文

Lean の制御構文は，通常のプログラミング言語の構文に似ています． ただし Lean では，これらもすべて型をもつ式です．

if ... then ... else ...

if は条件分岐です． 条件には，Bool または Lean が真偽を判定できる命題が入ります． n < 10 は命題ですが，自然数の大小比較には判定手続きがあるため if の条件として使えます． 一般の命題 P : Prop を条件にするには，Lean が [Decidable P] を見つけられる必要があります．

def minWithTen (n : Nat) : Nat :=
  if n < 10 then n else 10

example : minWithTen 3 = 3 := by
  rfl

example : minWithTen 20 = 10 := by
  rfl

match

match は inductive 型やデータ構造を場合分けする式です． Option，List，自分で定義した inductive などを分解できます． 各分岐は同じ型の式を返す必要があります． 証明で使う cases はゴールを場合分けする tactic ですが，match は式の中で場合分けして値を作る構文です．

def optionToNat : Option Nat → Nat
  | none => 0
  | some n => n

example : optionToNat none = 0 := by
  rfl

example : optionToNat (some 8) = 8 := by
  rfl

def listLength : List Nat → Nat
  | [] => 0
  | _ :: xs => 1 + listLength xs

example : listLength [10, 20, 30] = 3 := by
  rfl

let

let は局所的な名前をつける構文です． 長い式を読みやすくするために使います． let で導入した名前は，その式の残りの部分だけで使えます． 定義を環境に追加する def とは異なり，let は局所的な束縛です．

def squareSum (x y : Nat) : Nat :=
  let x2 := x * x
  let y2 := y * y
  x2 + y2

example : squareSum 3 4 = 25 := by
  rfl

do

do notation は，モナド的な計算を順番に書くための構文です． 最初は，失敗するかもしれない計算を Option でつなぐ例として見るとよいです． do ブロックの各行も式を組み立てるための notation であり，最終的には bind や pure を使う式に展開されます．

def addOptions (x y : Option Nat) : Option Nat := do
  let a ← x
  let b ← y
  pure (a + b)

example : addOptions (some 2) (some 5) = some 7 := by
  rfl

example : addOptions none (some 5) = none := by
  rfl

let a ← x は，x が some a なら中身を取り出して続行し，none なら全体を none にする，という動きをします． 同様に let b ← y で y が none なら，以降の pure (a + b) は実行されず，結果は none になります． 証明では do notation を頻繁に使うわけではありませんが，Lean でプログラムを書くときには重要です．