diff --git a/Examples/Command/Declarative/AddAesopRules.lean b/Examples/Command/Declarative/AddAesopRules.lean new file mode 100644 index 00000000..889109ac --- /dev/null +++ b/Examples/Command/Declarative/AddAesopRules.lean @@ -0,0 +1,192 @@ +/- # add_aesop_rules +`add_aesop_rules` は [`aesop`](../../Tactic/Aesop.md) タクティクに追加のルールを登録するためのコマンドです。-/ +import Aesop + +/-- 自然数 n が正の数であることを表す命題 -/ +inductive Pos : Nat → Prop + | succ n : Pos (n + 1) + +example : Pos 1 := by + -- 最初はルールが足りなくて示せない + fail_if_success aesop + + -- 手動でコンストラクタを `apply` することで証明できる + apply Pos.succ + +-- `Pos` 関連のルールを `aesop` に憶えさせる +add_aesop_rules safe constructors [Pos] + +-- aesop で示せる +example : Pos 1 := by aesop + +/- +`add_aesop_rules` は、`add_aesop_rules (phase)? (priority)? (builder)? [(rule_sets)?]` という構文で使用できます。 + +## phase について + +`phase` は `norm` と `safe` と `unsafe` の３通りです。ルールが適用される順番などに影響します。 + +### 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 + +-- aesop に登録する +add_aesop_rules norm simp [erase_duplicate] + +example (P : Prop) (hp : P) : MyAnd P P := by + -- aesop で証明できるようになった! + aesop + +/- ### safe + +`safe` ルールは、`norm` ルールの実行後に適用されます。あるゴールが証明可能であるとき、それに `safe` ルールを適用しても生成されるゴールは依然として証明可能であるように、`safe` ルールを選ぶことが推奨されます。 +-/ +section --# + +/-- 自前で定義したリスト -/ +inductive MyList (α : Type) + | nil + | cons (head : α) (tail : MyList α) + +/-- リストが空ではないことを表す述語 -/ +inductive NonEmpty {α : Type} : MyList α → Prop + | cons x xs : NonEmpty (MyList.cons x xs) + +local add_aesop_rules safe apply [NonEmpty.cons] + +-- aesop で `NonEmpty _` という形のゴールを示せる +example : NonEmpty (MyList.cons 1 MyList.nil) := by aesop + +end --# +/- ### unsafe +`unsafe` ルールは、すべての `safe` ルールが失敗した場合に適用されます。失敗したらバックトラックして他の `unsafe` ルールを試します。`priority` として成功する確率(%)を指定する必要があります。 +-/ +section --# + +-- 推移律を `unsafe` ルールとして登録する +local add_aesop_rules unsafe 10% apply [Nat.le_trans] + +example (a b c d e : Nat) + (h1 : a ≤ b) (h2 : b ≤ c) (h3 : c ≤ d) (h4 : d ≤ e) : a ≤ e := by + -- aesop で証明できるようになった！ + aesop + +end --# +/- `safe` ルールは常に適用されてしまうため、特定の状況でのみ適用したいルールは `unsafe` とすることが推奨されます。誤って `safe` ルールに登録してしまうと上手く動作しないことがあります。 -/ +section --# + +-- safe ルールとして推移律を登録する +local add_aesop_rules safe apply [Nat.le_trans] + +example (a b c d e : Nat) + (h1 : a ≤ b) (h2 : b ≤ c) (h3 : c ≤ d) (h4 : d ≤ e) : a ≤ e := by + -- aesop で証明できない + fail_if_success aesop + + calc + a ≤ b := by assumption + _ ≤ c := by assumption + _ ≤ d := by assumption + _ ≤ e := by assumption + +end --# +/- ## builder について +`builder` には多くの選択肢があります。ここではその一部を紹介します。 + +### apply + +`apply` タクティクと同様にはたらくルールを登録します。 +-/ +section --# +example (a b c d e : Nat) + (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 + +-- 推移律を登録する +local add_aesop_rules unsafe 10% apply [Nat.lt_trans] + +example (a b c d e : Nat) + (h1 : a < b) (h2 : b < c) (h3 : c < d) (h4 : d < e) : a < e := by + -- aesop で証明できるようになった + aesop +end --# +/- ### 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 にルールを登録する +add_aesop_rules safe constructors [Even] + +example : Even 2 := by + -- aesop で証明できるようになった + aesop + +/- ### cases +`cases` ビルダーは、帰納型 `T` の形をした仮定がローカルコンテキストにある場合に、それに対して再帰的に `cases` タクティクを使用して分解するように指示します。 +-/ + +example (n : Nat) (h : Even (n + 2)) : Even n := by + -- 最初は aesop で証明できない + fail_if_success aesop + + -- 手動で cases を使って分解することで証明できる + cases h + assumption + +-- aesop にルールを登録する +add_aesop_rules safe cases [Even] + +example (n : Nat) (h : Even (n + 2)) : Even n := 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 + +-- aesop にルールを登録する +add_aesop_rules safe tactic [(by omega)] + +example (a b : Nat) (h : 3 ∣ (10 * a + b)) : 3 ∣ (a + b) := by + -- aesop で証明できるようになった! + aesop diff --git a/Examples/Solution/HeytingAndBooleanAlgebra.lean b/Examples/Solution/HeytingAndBooleanAlgebra.lean index aaa7bc17..663bd5d6 100644 --- a/Examples/Solution/HeytingAndBooleanAlgebra.lean +++ b/Examples/Solution/HeytingAndBooleanAlgebra.lean @@ -136,23 +136,7 @@ end HeytingAlgebra しかし、今回は証明の `sorry` の部分を埋めていただくという問題ではありません。逆に、こちらで用意した証明が通るようにしていただくのが問題です。 -こちらで用意した証明は、すべて `aesop` という単一のタクティクで完結しています。`aesop` は補題やタクティクを登録することにより、ユーザがカスタマイズ可能なタクティクですので、うまくカスタマイズして用意された証明が通るようにしてください。 - -### aesop ルールの記述方法 - -`add_aesop_rules` コマンドで `aesop` をカスタマイズすることができます。`add_aesop_rules` は構文的には `add_aesop_rules (phase) [(rule builder) (rule)]` という構成になっています。 - -* `phase` は `norm` と `safe` と `unsafe` の３通りです。 - * `norm`: 正規化ルールを表します。 - * `safe`: 正規化ルールの後に実行されます。`safe` ルールは「適用しても証明可能性が変わらない」ことを前提にしているため、適用後に同じゴールが再検討されることはありません。 - * `unsafe`: すべての `safe` ルールが失敗した場合に適用されます。直後に成功する確率(%)も指定します。 - -* `rule builder` には多くの選択肢がありますが、この演習問題では以下のものだけ使用すれば解くことができます。 - * `tactic`: タクティクを指定します。たとえば `add_aesop_rules safe [tacitc (by simp_all)]` などのように使います。 - * `cases`: 帰納型 `T` に対して使用することで、仮定に `t : T` がある場合に `cases` を再帰的に適用して分解します。 - * `simp`: `simp` 補題を登録します。 - -`aesop` タクティクのカスタマイズ方法については、最も詳しい資料は [leanprover-community/aesop](https://github.com/leanprover-community/aesop) の README です。必要に応じて参考にしてください。 +こちらで用意した証明は、すべて `aesop` という単一のタクティクで完結しています。`aesop` は補題やタクティクを登録することにより、ユーザがカスタマイズ可能なタクティクですので、うまくカスタマイズして用意された証明が通るようにしてください。[`add_aesop_rules`](../Command/Declarative/AddAesopRules.md) の記事が参考になると思います。 ### 問1.1 半順序集合であること -/ diff --git a/Examples/Tactic/Aesop.lean b/Examples/Tactic/Aesop.lean index 51902772..03ae2a51 100644 --- a/Examples/Tactic/Aesop.lean +++ b/Examples/Tactic/Aesop.lean @@ -1,14 +1,20 @@ /- # aesop -`aesop` は、Automated Extensible Search for Obvious Proofs (自明な証明の拡張可能な自動探索)からその名があるタクティクです。`aesop` は `intro` や `simp` を使用してルーチンな証明を自動で行ってくれます。 +`aesop` は汎用的かつ強力な自動証明のためのタクティクです。 + +Automated Extensible Search for Obvious Proofs (自明な証明の拡張可能な自動探索)からその名があります。様々なタクティクやルールを使用しながら最良優先探索を行い、ルーチンな証明を自動で終わらせます。 + -/ import Aesop -- `aesop` を使用するため -import Mathlib.Logic.Function.Defs -- `Injective` を使用するため +import Mathlib.Tactic.Says -- 以下 `X` `Y` `Z`を集合とする variable {X Y Z : Type} +/-- 関数の単射性 -/ +def Function.Injective (f : X → Y) : Prop := ∀ ⦃a₁ a₂ : X⦄, f a₁ = f a₂ → a₁ = a₂ + open Function -- 合成 `g ∘ f` が単射なら、`f` も単射 @@ -19,7 +25,7 @@ example {f : X → Y} {g : Y → Z} (hgfinj : Injective (g ∘ f)) : Injective f -- 示すべきことがまだまだあるように見えるが、一発で証明が終わる aesop -/-! +/- ## aesop? `aesop` が成功するとき、`aesop?` に置き換えるとゴールを達成するのにどんなタクティクを使用したか教えてくれます。 @@ -27,22 +33,51 @@ example {f : X → Y} {g : Y → Z} (hgfinj : Injective (g ∘ f)) : Injective f example {f : X → Y} {g : Y → Z} (hgfinj : Injective (g ∘ f)) : Injective f := by rw [Injective] + aesop? says + intro a₁ a₂ a + apply hgfinj + simp_all only [comp_apply] + +/- なお上記の例により、`aesop` が組み込みのルールとして `simp` 補題や `intro` タクティク等を使用することがわかります。-/ + +/- ## カスタマイズ +`aesop` はユーザがカスタマイズ可能です。補題やタクティクを登録することで、証明可能な命題を増やすことができます。 +-/ + +/-- 自然数 n が正の数であることを表す命題 -/ +inductive Pos : Nat → Prop + | succ n : Pos (n + 1) - /- - Try this: - intro a₁ a₂ a - apply hgfinj - simp_all only [comp_apply] - -/ - aesop? +example : Pos 1 := by + -- ルールが登録されていないので、`aesop` で示すことはできない + fail_if_success aesop -/-! ## 補足 -より詳細には `aesop` は下記のような性質を持ちます: + -- 手動でコンストラクタを `apply` することで証明できる + apply Pos.succ -* `simp` と同様に、`@[aesop]` という属性(attribute)を付けることで補題や定義を登録し、`aesop` に使用させることができます。 -* `aesop` は登録されたルールを最初のゴールに適用しようとします。成功してサブゴールが生成されたら、`aesop` はサブゴールにも再帰的にルールを適用し、探索ツリーを構築します。 -* 探索ツリーは最良優先探索(best-first search)により探索されます。ルールには有用である可能性が高いか低いかもマークすることができ、`aesop` は探索ツリー内のより有望そうなゴールを先に調べます。 -* `aesop` はまず `simp_all` を用いてゴールを正規化するため、`simp` が使用する補題は `aesop` にも使用されます。 +-- `Pos` 関連のルールを `aesop` に憶えさせる +attribute [aesop safe constructors] Pos -もっと詳しいことが知りたい方は、[aesopのリポジトリ](https://github.com/leanprover-community/aesop)をご参照ください。 +-- `aesop` で証明できるようになった！ +example : Pos 1 := by aesop + +/- 上記の例のように `[aesop]` 属性によってルールを追加することもできますし、[`add_aesop_rules`](../Command/Declarative/AddAesopRules.md) というコマンドでルールを追加することもできます。-/ + +example (n : Nat) (h : Pos n) : 0 < n := by + -- ルールが足りないので、`aesop` で示すことはできない + fail_if_success aesop + + -- 手動で `h : Pos n` を分解して証明する + rcases h with ⟨h⟩ + simp + +-- `Pos` 関連のルールを `aesop` に追加 +add_aesop_rules safe [cases Pos] + +-- `aesop` で証明できるようになった！ +example (n : Nat) (h : Pos n) : 0 < n := by + aesop + +/- +カスタマイズ方法の詳細を知りたい方は[aesopのリポジトリ](https://github.com/leanprover-community/aesop)をご参照ください。また、内部のロジックの詳細については論文 [Aesop: White-Box Best-First Proof Search for Lean](https://dl.acm.org/doi/pdf/10.1145/3573105.3575671) で説明されています。 -/ diff --git a/Exercise/HeytingAndBooleanAlgebra.lean b/Exercise/HeytingAndBooleanAlgebra.lean index a491f428..948cebd3 100644 --- a/Exercise/HeytingAndBooleanAlgebra.lean +++ b/Exercise/HeytingAndBooleanAlgebra.lean @@ -136,23 +136,7 @@ end HeytingAlgebra しかし、今回は証明の `sorry` の部分を埋めていただくという問題ではありません。逆に、こちらで用意した証明が通るようにしていただくのが問題です。 -こちらで用意した証明は、すべて `aesop` という単一のタクティクで完結しています。`aesop` は補題やタクティクを登録することにより、ユーザがカスタマイズ可能なタクティクですので、うまくカスタマイズして用意された証明が通るようにしてください。 - -### aesop ルールの記述方法 - -`add_aesop_rules` コマンドで `aesop` をカスタマイズすることができます。`add_aesop_rules` は構文的には `add_aesop_rules (phase) [(rule builder) (rule)]` という構成になっています。 - -* `phase` は `norm` と `safe` と `unsafe` の３通りです。 - * `norm`: 正規化ルールを表します。 - * `safe`: 正規化ルールの後に実行されます。`safe` ルールは「適用しても証明可能性が変わらない」ことを前提にしているため、適用後に同じゴールが再検討されることはありません。 - * `unsafe`: すべての `safe` ルールが失敗した場合に適用されます。直後に成功する確率(%)も指定します。 - -* `rule builder` には多くの選択肢がありますが、この演習問題では以下のものだけ使用すれば解くことができます。 - * `tactic`: タクティクを指定します。たとえば `add_aesop_rules safe [tacitc (by simp_all)]` などのように使います。 - * `cases`: 帰納型 `T` に対して使用することで、仮定に `t : T` がある場合に `cases` を再帰的に適用して分解します。 - * `simp`: `simp` 補題を登録します。 - -`aesop` タクティクのカスタマイズ方法については、最も詳しい資料は [leanprover-community/aesop](https://github.com/leanprover-community/aesop) の README です。必要に応じて参考にしてください。 +こちらで用意した証明は、すべて `aesop` という単一のタクティクで完結しています。`aesop` は補題やタクティクを登録することにより、ユーザがカスタマイズ可能なタクティクですので、うまくカスタマイズして用意された証明が通るようにしてください。[`add_aesop_rules`](../Command/Declarative/AddAesopRules.md) の記事が参考になると思います。 ### 問1.1 半順序集合であること -/ diff --git a/src/SUMMARY.md b/src/SUMMARY.md index 921f819c..fed23bfe 100644 --- a/src/SUMMARY.md +++ b/src/SUMMARY.md @@ -23,6 +23,7 @@ - [#whnf: 式を弱頭正規形に](./Command/Diagnostic/Whnf.md) - [宣言的コマンド](./Command/Declarative/README.md) - [abbrev: 略称を定義する](./Command/Declarative/Abbrev.md) + - [add_aesop_rules: aesop 改造](./Command/Declarative/AddAesopRules.md) - [attribute: 属性を付与する](./Command/Declarative/Attribute.md) - [axiom: 公理を宣言する](./Command/Declarative/Axiom.md) - [class: 型クラスを定義する](./Command/Declarative/Class.md)