#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 だったときに左辺と右辺の値を表示するようなコマンドが欲しいですね。これは、以下のように自作することができます。¹

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 さんによって提案されたコードを参考にしています。 ↩

Lean by Example

#guard

決定可能性

DIY: 差分の表示