Leanタクティク 1

Lean

過去記事：

「Leanタクティク」は、実際のLeanのタクティクを話題にする。

参考URL：

ケビン・バザードのチートシート（不適切語を修正、順序変更）：

Form of proposition In the target? Hypothesis named h?
P → Q intro hP で分解 apply h で利用
true trivial で分解 (can’t be used)
false (can’t be used) exfalso, exact h or cases h を使用
￢P intro hP で分解 apply h (if goal is false) を使用
P ∧ Q split ☓ cases h with hP hQ ？
P ↔ Q split ☓ cases h or rw h で利用
P ∨ Q left or right で分解 cases h with hP hQ で使用
∀ (a : X), ... intro x で分解 specialize h x
∃ (a : X), ... use x で分解 cases h with x hx

Lean 4で変わってしまい使えないものがある。ハッキリしているのは☓が付いている。

  • P∧Q は、apply And.intro で分解
  • P ↔ Q は、apply Iff.intro で分解

あるパターンの論理式がターゲットに出現したときにタクティクで分解する。分解した後の質問シーケントでは、論理記号が消えているので、導入規則の逆を実行している。

あるパターンの論理式がコンテキストに出現したときは名前を持っている。名前を特定して利用する。apply h で、h を使ったモーダスポネンスを逆行する。P → Q ... |-? Q ～(-)⇒ P → Q ... |-? P 順行なら P → Q ... |-! P ～(+)⇒ P → Q ..., P |! ～(-)⇒ P → Q ..., P |-! Q 。

intro

引数なしの intro でコンテキスト側に自動命名された宣言〈仮説〉が出現する。自動の名前は、英字＋ラテンクロス＋上付き番号。

simp [f]

関数 f の定義を使って展開〈フォールド〉する。定義は、項の simplification rule / unfolding rule として使える。定義の右辺式を右辺式で置き換えるだけ。simpしたら複雑になることもある。