#guard

#guard は与えられた Bool 値が true であることを確かめます．

import Batteries.Data.List.Lemmas -- リストに対して `⊆` が使えるようにする


-- 階乗関数
def fac : Nat → Nat
| 0 => 1
| n + 1 => (n + 1) * fac n

#guard fac 5 == 120

舞台裏

#guard に Bool ではなく Prop 型の項を与えた場合，エラーになることがあります．次の命題は証明があるので真ですが， #guard は通りません.

example (α : Type) (l : List α) : [] ⊆ l := by simp

-- Prop 型を持つ
#check ((α : Type) → ∀ (l : List α), [] ⊆ l : Prop)

/--
error: type mismatch
  ∀ (α : Type) (l : List α), [] ⊆ l
has type
  Prop : Type
but is expected to have type
  Bool : Type
---
error: cannot evaluate code because 'sorryAx' uses 'sorry' and/or contains errors
-/
#guard_msgs (whitespace := lax) in
#guard ((α : Type) → ∀ (l : List α), [] ⊆ l : Prop)

しかし， 1 + 1 = 2 等も #check で確かめてみると型は Prop です．にも関わらず #guard に渡してもエラーになりません．これは不思議に思えますが，理由は 1 + 1 = 2 が Decidable 型クラスのインスタンスであり, 決定可能だからです．

-- 型は Prop
/-- info: 1 + 1 = 2 : Prop -/
#guard_msgs in #check 1 + 1 = 2

#guard 1 + 1 = 2

-- 1 + 1 = 2 は決定可能
#synth Decidable (1 + 1 = 2)

Prop 型であっても，Decidable クラスのインスタンスであれば Bool に変換できます．それを自動で行っているので，Prop 型の項でも #guard に通せるというわけです．

-- 決定可能な Prop 型の項を Bool に変換する関数
#check (decide : (p : Prop) → [_h : Decidable p] → Bool)

-- Bool 型になっている
/-- info: decide (1 + 1 = 2) : Bool -/
#guard_msgs in #check decide (1 + 1 = 2)