#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)