aesop

[aesop] は aesop タクティクに追加のルールを登録するための属性です。同様の機能を持つコマンドに add_aesop_rules があります。

import Aesop

/-- 自然数 n が正の数であることを表す帰納的述語 -/
inductive Pos : Nat → Prop where
  | succ n : Pos (n + 1)

example : Pos 1 := by
  -- 最初はルールが足りなくて示せない
  fail_if_success aesop

  -- 手動でコンストラクタを `apply` することで証明できる
  apply Pos.succ

-- `Pos` 関連のルールを `aesop` に憶えさせる
attribute [aesop safe constructors] Pos

-- aesop で示せるようになった！
example : Pos 1 := by aesop

なお aesop をカスタマイズしたものを専用のタクティクにまとめることも可能ですが、それについてはここでは詳しく述べません。declare_aesop_rule_sets コマンドのページを参照してください。

[aesop] 属性は、[aesop <phase>? <priority>? <builder_name>? <builder_option>? <rule_sets>?] という構文で使用できます。

phase について

phase は norm と safe と unsafe の３通りです。「ルールを適用した後、ダメそうだとわかったら引き返せ」「常に最初に適用せよ」など試行錯誤のやり方を指示します。

open Lean Parser Category in

-- `Aesop.phase` という構文カテゴリが存在する
#check (Aesop.phase : Category)

norm

norm は正規化(normalisation)ルールを表します。最初に適用されるルール群であり、適用によりゴールが増えないようなルールだけを登録することが推奨されます。[simp] 補題と同様に使用されます。

/-- And を模倣して自作した型 -/
structure MyAnd (a b : Prop) : Prop where
  intro ::
  left : a
  right : b

/-- `P ∧ P ↔ P` に相当するルール -/
theorem erase_duplicate {P : Prop} : MyAnd P P ↔ P := by
  constructor <;> intro h
  · rcases h with ⟨h⟩
    exact h
  · exact MyAnd.intro h h

example (P : Prop) (hp : P) : MyAnd P P := by
  -- 最初は aesop で証明できない
  fail_if_success solve
  | aesop
  sorry

-- aesop に登録する
attribute [aesop norm simp] erase_duplicate

example (P : Prop) (hp : P) : MyAnd P P := by
  -- aesop で証明できるようになった!
  aesop

safe

safe ルールは、norm ルールの実行後に適用されます。あるゴールが証明可能であるとき、それに safe ルールを適用しても生成されるゴールは依然として証明可能であるように、safe ルールを選ぶことが推奨されます。

/-- 自前で定義したリスト -/
inductive MyList (α : Type) where
  | nil
  | cons (head : α) (tail : MyList α)

/-- リストが空ではないことを表す帰納的述語 -/
inductive NonEmpty {α : Type} : MyList α → Prop where
  | cons x xs : NonEmpty (MyList.cons x xs)

example : NonEmpty (MyList.cons 1 MyList.nil) := by
  -- 最初は aesop で証明できない
  fail_if_success aesop
  sorry

attribute [aesop safe apply] NonEmpty.cons

-- aesop で示せるようになった！
example : NonEmpty (MyList.cons 1 MyList.nil) := by aesop

unsafe

unsafe ルールは、すべての safe ルールが失敗した場合に適用されます。失敗したらバックトラックして他の unsafe ルールを試します。priority として成功する確率(%)を指定する必要があります。

variable (a b c d e : Nat)

example (h1 : a ≤ b) (h2 : b ≤ c) (h3 : c ≤ d) (h4 : d ≤ e) : a ≤ e := by
  -- 最初は aesop で証明できない
  fail_if_success aesop
  sorry

-- 推移律を `unsafe` ルールとして登録する
attribute [local aesop unsafe 10% apply] Nat.le_trans

example (h1 : a ≤ b) (h2 : b ≤ c) (h3 : c ≤ d) (h4 : d ≤ e) : a ≤ e := by
  -- aesop で証明できるようになった！
  aesop

safe ルールは適用すると後戻りができないため、特定の状況でのみ適用したいルールは unsafe とすることが推奨されます。誤って safe ルールに登録してしまうと上手く動作しないことがあります。

-- 同じ推移律を今度は `safe` ルールとして登録する
attribute [local aesop safe apply] Nat.le_trans

variable (a b c d e : Nat)

example (h1 : a ≤ b) (h2 : b ≤ c) (h3 : c ≤ d) (h4 : d ≤ e) : a ≤ e := by
  -- aesop で証明できない
  -- 同じ命題を同じように登録したが、safe にしてしまったからダメだった
  fail_if_success aesop

  sorry

builder_name について

builder_name は、登録されるルールに対して「ゴールを分解する」「仮定から推論を進める」といった方向性を決めます。複数の選択肢がありますが、ここではその一部を紹介します。

open Lean Parser Category in

-- `Aesop.builder_name` という構文カテゴリが存在する
#check (Aesop.builder_name : Category)

apply

apply タクティクと同様にはたらくルールを登録します。

variable (a b c d e : Nat)

example (h1 : a < b) (h2 : b < c) (h3 : c < d) (h4 : d < e) : a < e := by
  -- 最初は aesop で示せない
  fail_if_success aesop

  -- 手動で示すならこのように apply を繰り返すことになる
  apply Nat.lt_trans (m := d) <;> try assumption
  apply Nat.lt_trans (m := c) <;> try assumption
  apply Nat.lt_trans (m := b) <;> try assumption

-- 推移律を登録する
attribute [aesop unsafe 10% apply] Nat.lt_trans

example (h1 : a < b) (h2 : b < c) (h3 : c < d) (h4 : d < e) : a < e := by
  -- aesop で証明できるようになった!
  aesop

constructors

constructors ビルダーは、帰納型 T の形をしたゴールに遭遇した際に、コンストラクタを適用するように指示します。

/-- 自前で定義した偶数を表す帰納的述語 -/
inductive Even : Nat → Prop where
  | zero : Even 0
  | succ m : Even m → Even (m + 2)

example : Even 2 := by
  -- 最初は aesop で証明できない
  fail_if_success aesop

  -- 手動でコンストラクタを適用することで示せる
  apply Even.succ
  apply Even.zero

-- aesop にルールを登録する
attribute [aesop safe constructors] Even

example : Even 2 := by
  -- aesop で証明できるようになった!
  aesop

cases

cases ビルダーは、帰納型 T の形をした仮定がローカルコンテキストにある場合に、それに対して再帰的に cases タクティクを使用して分解するように指示します。

/-- 自前で定義した奇数を表す帰納的述語 -/
inductive Odd : Nat → Prop where
  | one : Odd 1
  | succ m : Odd m → Odd (m + 2)

example (n : Nat) (h : Odd (n + 2)) : Odd n := by
  -- 最初は aesop で証明できない
  fail_if_success aesop

  -- 手動で cases を使って分解することで証明できる
  cases h
  assumption

-- aesop にルールを登録する
attribute [aesop safe cases] Odd

example (n : Nat) (h : Odd (n + 2)) : Odd n := by
  -- aesop で証明できるようになった
  aesop

destruct

destruct ビルダーは、A₁ → ⋯ → Aₙ → B という形の命題を登録することで、仮定に A₁, ..., Aₙ が含まれている場合に、元の仮定を消去して B を仮定に追加します。

/-- 自前で定義した偶数を表す帰納的述語 -/
inductive Even : Nat → Prop where
  | zero : Even 0
  | succ m : Even m → Even (m + 2)

/-- 任意の数 n について、n か n + 1 のどちらかは偶数 -/
theorem even_or_even_succ (n : Nat) : Even n ∨ Even (n + 1) := by
  induction n with
  | zero => left; apply Even.zero
  | succ n ih =>
    rcases ih with ih | ih
    · right
      apply Even.succ
      assumption
    · left
      assumption

example {n : Nat} (h0 : ¬ Even n) (h1 : ¬ Even (n + 1)) : False := by
  -- 最初は aesop で証明できない
  fail_if_success aesop

  -- 手動で補題を示すことで証明する
  have := even_or_even_succ n
  simp_all

attribute [aesop unsafe 30% destruct] even_or_even_succ

example {n : Nat} (h0 : ¬ Even n) (h1 : ¬ Even (n + 1)) : False := by
  -- aesop で示せるようになった！
  aesop

tactic

tactic ビルダーは、タクティクを追加のルールとして直接利用できるようにします。

example (a b : Nat) (h : 3 ∣ (10 * a + b)) : 3 ∣ (a + b) := by
  -- aesop で証明できない
  fail_if_success aesop

  -- omega を使えば証明できる
  omega

open Lean Elab Tactic in

-- aesop にルールを登録する
attribute [aesop safe tactic] Omega.omegaDefault

example (a b : Nat) (h : 3 ∣ (10 * a + b)) : 3 ∣ (a + b) := by
  -- aesop で証明できるようになった!
  aesop

ただし tactic ビルダーは受け入れる型が少し特殊で、TacticM Unit などの少数の型の項しか受け入れません。正確にどの型の項を受け入れるかは、エラーメッセージで確認できます。

/--
error: aesop: tactic builder: expected foo to be a tactic, i.e. to have one of these types:
  TacticM Unit
  SimpleRuleTac
  RuleTac
  TacGen
However, it has type
  String
-/
#guard_msgs in
  @[aesop safe tactic] def foo := "hello"