#guard
#guard
は与えられた Bool 値が true であることを確かめます。
-- 階乗関数
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
but is expected to have type
Bool
---
error: cannot evaluate code because 'sorryAx' uses 'sorry' and/or contains errors
-/
#guard ((α : Type) → ∀ (l : List α), [] ⊆ l : Prop)
しかし、 1 + 1 = 2
等も #check
で確かめてみると型は Prop
です。にも関わらず #guard
に渡してもエラーになりません。これは不思議に思えますが、理由は 1 + 1 = 2
が Decidable
型クラスのインスタンスであり、決定可能だからです。
-- 型は Prop
/- info: 1 + 1 = 2 : Prop -/
#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 -/
#check decide (1 + 1 = 2)
DIY: 差分の表示
#guard
コマンドを使って A = B
という式を評価して false
だったとき、デフォルトでは A
と B
がそれぞれどんな値であるかは表示されません。単に「等しくない」というメッセージが出るだけです。
/-
error: Expression
decide (1 + 1 = 3)
did not evaluate to `true`
-/
#guard 1 + 1 = 3
この挙動は少し不便です。#guard
に渡された等式が false
だったときに左辺と右辺の値を表示するようなコマンドが欲しいですね。これは、以下のように自作することができます。1
import Lean
import Qq
open Lean Meta Elab Command Qq
private def failGenerically (e : Expr) : TermElabM Unit := do
throwError "Expression{indentExpr e}\ndid not evaluate to `true`"
private def fail (e : Expr) : TermElabM Unit := do
let_expr Decidable.decide p _ := e | failGenerically e
let_expr Eq _ lhs rhs := p | failGenerically e
let lhs_fmt_expr : Q(Format) ← mkAppM ``repr #[lhs]
let rhs_fmt_expr : Q(Format) ← mkAppM ``repr #[rhs]
let lhs_fmt ← unsafe evalExpr Format q(Format) lhs_fmt_expr
let rhs_fmt ← unsafe evalExpr Format q(Format) rhs_fmt_expr
throwError
"Expression{indentExpr e}\n\
did not evaluate to `true`\n\
---\n\
{lhs} = {lhs_fmt}\n\
{rhs} = {rhs_fmt}"
/-- 等式を評価して不成立だったときに、左辺と右辺の値を表示するような
`#guard` コマンドの派生コマンド -/
elab "#guard_diff" e:term : command => liftTermElabM do
let e ← Term.elabTermEnsuringType e q(Bool)
Term.synthesizeSyntheticMVarsNoPostponing
let e ← instantiateMVars e
let mvars ← getMVars e
if mvars.isEmpty then
let v ← unsafe evalExpr Bool q(Bool) e
unless v do fail e
else
_ ← Term.logUnassignedUsingErrorInfos mvars
/-
error: Expression
decide (3 * 4 = 2 + 2)
did not evaluate to `true`
---
3 * 4 = 12
2 + 2 = 4
-/
#guard_diff 3 * 4 = 2 + 2
-
こちらのコードは Zulip の #guard with diff というトピックで Marcus Rossel さんによって提案されたコードを参考にしています。 ↩