fun

fun x => t は無名関数を作る式です． 数学の notation では（関数名を明記しない） \(x \mapsto t\) に対応します． def が名前つきの関数を環境に追加するコマンドであるのに対して，fun はその場で関数という項を作る式です．

Lean の多引数関数は基本的にカリー化されています． たとえば Nat → Nat → Nat は，自然数を 1 つ受け取って，さらに Nat → Nat 型の関数を返す型として読めます． fun x y => t は，おおよそ fun x => fun y => t の短い書き方です．

#check (fun n : Nat => n + 1)
#check (fun m n : Nat => m + n)
#check (fun (P Q : Prop) (hP : P) (_hQ : Q) => hP)

def addByFun : Nat → Nat → Nat :=
  fun m n => m + n

example : addByFun 2 5 = 7 := by
  rfl

def addConst (k : Nat) : Nat → Nat :=
  fun n => n + k

example : addConst 4 3 = 7 := by
  rfl

関数を引数に取る関数へ，その場で関数を渡すときにも fun がよく使われます． これは後で tactic を読むときにも重要です． たとえば含意 P → Q の証明は，P の証明を受け取って Q の証明を返す関数です．

def applyTwice (f : Nat → Nat) (n : Nat) : Nat :=
  f (f n)

example : applyTwice (fun n => n + 1) 10 = 12 := by
  rfl

def composeNat (f g : Nat → Nat) : Nat → Nat :=
  fun n => f (g n)

example : composeNat (fun n => n + 1) (fun n => 2 * n) 5 = 11 := by
  rfl

example (P Q : Prop) : P → Q → P :=
  fun hP _hQ => hP

fun は tactic ではなく式です． したがって，exact fun hP => ... のように書けば，「関数を証明項として直接与える」ことにもなります． この見方は Chapter 03 で tactic と証明項の対応を見るときに使います．

演習

fun を使って，次の関数と証明項を書いてください．

def squareByFunExercise : Nat → Nat :=
  -- `n ↦ n * n`
  sorry

example : squareByFunExercise 5 = 25 := by
  sorry

def applyToThreeExercise (f : Nat → Nat) : Nat :=
  -- `f` を `3` に適用する．
  sorry

example : applyToThreeExercise (fun n => n + 4) = 7 := by
  sorry

example (P Q : Prop) : P → Q → Q :=
  -- `fun` で証明項を書く．
  sorry