よく使われるタクティクのリストを作る

[Seasawher]

@haruhisa-enomoto @aconite-ac @s-taiga

初学者でもある程度慣れた人でも，タクティクとその説明，使用例が一覧できるリストがあったら便利だと思います．

@haruhisa-enomoto さんが作ってくださった mathlib4 タクティクのリストは良いリソースだと思いますが，日本語ではないですし，仮に訳すとしても「全タクティクのリスト」となると保守が大変ですし，使用例がないところがありますし，また本来 mathlib 側で保守されるべきものでもあると思います．

そうではなくて，Lean 勉強会の Basic/Tactic のような，特に使用頻度が高いものに絞って日本語でリストを作ると有用なのではないかと思いました．「よく使うタクティク 10選」のような感じです．

イメージとしては Lean 勉強会のタクティクリストの部分を独立させて，内容を足し，Webページとして公開するというのを考えています．

いかがでしょうか？ご意見いただければ幸いです．

[aconite-ac]

全タクティクリストと競合しない、というより相補的な資料として、

• 日本語で書かれている
• よく使うタクティクに絞って紹介する
• 各タクティクに対して説明・使用例を載せる

を満たすタクティクリストは非常に有用だと思います！
各タクティクの説明のテンプレートを作るとよさそうですね。

[haruhisa-enomoto]

よいと思います！（自分も欲しいくらいです）
Lean勉強会のBasic/Tacticは自分が適当に書いたものなので、下書き等に使ってもらって結構です。

[Seasawher]

ありがとうございます
作りたい気持ちが強まりました

各タクティクの説明のテンプレートを作るとよさそうですね。

そうですね、将来的に数を増やし、外部からのcontributionも受け入れられるようにしたいので、先にテンプレートを作ろうと思います。

そのときは、お二方にレビューをお願いしようと思います。よろしくお願いします

[Seasawher]

とりあえず気になる点です：

• tactic と tactic? や tactic! を別物として紹介するかどうか．まとめる基準は？

• mathlib4 のタクティクなのかどうか等，由来を区別することは必要か

• · などの一見して読み方が不明なタクティクの名前をどうするか

• 意味を考えて並べるのか，あるいはアルファベット順に並べるのか．

• タクティクの記事にタグをつけて検索できる機能は必要か？

[Seasawher]

とりあえず mdbook でビルドすることにします

記事にタグがつけられないという制約はありますが，コード交じりの文章を書くのに向いていますし，モバイルでも見やすく調整してくれます．シンタックスハイライトも効かせることができます．

[Seasawher]

@aconite-ac @haruhisa-enomoto

1. 辞書のようにアルファベット順でタクティクの記事を作るか、

2. 入門者向けに厳選したタクティクを分類して紹介するか

で迷っていましたが、全タクティクリストは既にあるので、入門者向けテキストとして差別化するのが良さそうに思いました。

[Seasawher]

紹介するタクティクの案です。

モード切り替え

• by
• calc
• conv
• tactic

論理

• apply
• exact
• have
• assumption
• contradiction
• constructor
• left, right
• induction
• cases
• suffices
• intro
• rewrite
• rel
• funext
• ext
• rfl
• exists
• obtain
• rintro

自動化

• simp
• aesop
• ring
• linarith
• nlinarith
• dsimp

補助的なもの

• sorry
• done
• cdot

[haruhisa-enomoto]

tacticというtacticってあるのでしょうか？
あと個人的には以下もよく使います。

• simp_all（やsimpa、ただsimpaは他のものの組み合わせで実現できるので微妙？）
• change
• convert
• congr
  ただ厳選というわけなのでどこまで載せるかは考える必要があるかもしれません。

[haruhisa-enomoto]

rename_iは使う状況がかなり限られる（上に通常の証明では使うことは想定されない気がする）ので微妙かもしれません。

[Seasawher]

rename_i は確かに初心者は知らなくていいタクティクですね。やめておきましょう

あと、15個くらいかなと勝手に予想していたのですが、列挙してみると40個くらいありますね…

[Seasawher]

tacticというtacticってあるのでしょうか？

https://aconite-ac.github.io/theorem_proving_in_lean4_ja/conv.html#other-tactics-inside-conversion-mode-%E5%A4%89%E6%8F%9B%E3%83%A2%E3%83%BC%E3%83%89%E3%81%AB%E3%81%8A%E3%81%91%E3%82%8B%E4%BB%96%E3%81%AE%E3%82%BF%E3%82%AF%E3%83%86%E3%82%A3%E3%82%AF これを指してます

conv モードの中でほかのタクティクを呼ぶときのやつです

[Seasawher]

@haruhisa-enomoto

https://github.com/lean-ja/tactic-tutorial

ちょっと試作してみました．ご確認ください．

mdbook を使って，Lean ファイルを include しながら書くという方針は問題なさそうですが，本としての構成は問題ありです．行き当たりばったりではなくてしっかり紹介する順序と内容を考え抜いてから書き始めるべきという感じがします．

[Seasawher]

mathlib 依存の例をいったん忘れて，厳選して再構成してみました

これでも結構多いですね

公理

• 証明したことにする: sorry

論理系

• 証明を直接与える： exact
• 仮定より明らか：assumption
• 含意を適用する: apply
• 含意を示す等: intro
• 論理積を示す: constructor
• 論理和を示す: left, right
• 存在を示す: exists
• 存在を適用する: obtain have があるのでまだ要らない

証明の構造化

• 矛盾: contradiction
• 帰納法: induction
• 場合分け: by_cases
• ～を示せば十分: suffices
• 補題を用意する: have

等式・同値

• 定義から明らか: rfl
• 言い換え: rewrite, rw

モード切替

• 計算モードに入る: calc
• 変換モードに入る: conv
• タクティクモードに入る: by

追記： funext, ext も入れるかどうか迷いますね

[haruhisa-enomoto]

いくつかコメントします。
あったほうがいいと思うやつ

• simpはmathlib無しでも使える、Leanの強みのような強力なtacticなのでぜひあったほうがいいです。
• 同様にmathlib依存ではありますがapply?はあったほうがいいと思っています。
• funextはextで代用できますが、extは集合の包含や写像の等しいことを示すときに必須なので、入れたほうがいいと思います。

なくてもいいと思うやつ

• assumption contradictionはexact（とexfalsoもしくはFalse.elim）で書けるのでいらないと思います（自分も短くリファクタリングする以外の目的ではあまり使いません）
• convはtacticとして紹介するにはちょっと長くなって独自モードの機能の説明も必要なので、TPIL4の該当箇所に投げるのがいいと思います。
• obtainはhaveでいちおう代用できるので（若干振る舞いは違いますが）、まとめてもいいかもしれません。
• rewriteを使うことは無い気がしてrwのみでいい気がします。

[Seasawher]

simpはmathlib無しでも使える、Leanの強みのような強力なtacticなのでぜひあったほうがいいです。

そうですね. mathlib 依存組と間違えてました．入れましょう！

同様にmathlib依存ではありますがapply?はあったほうがいいと思っています。

入れたいですね．ただ mathlib 依存のタクティクは，後で追記する形で入れていけたらと思っています．mathlib を許可するとまた量がぐんと多くなって公開が遠のくので，後からアップデートする形で入れたい…．

assumption contradictionはexact（とexfalsoもしくはFalse.elim）で書けるのでいらないと思います（自分も短くリファクタリングする以外の目的ではあまり使いません）

個人的には両方好きなので入れています．

• assumption は exact で書き直せますが，専門のタクティクがあるならそれを使うべきだと思っています. そもそも exact も apply で書き直せますよね．仮定からあきらかであるときはそれを明示したいという気がしています．

• contradiction は矛盾系のタクティクで最も直感的に使いやすいので入れたいですね．exfalso や False.elim は結構わかりにくいと思っています．なぜかというと，普段の数学の発想では「ゴールをFalseにしよう」という考えになかなか至らないからです．実際，Lean 勉強会で False.elim がわかりにくいという質問がありました．コードの記述量も contradiction を使うと短くなるので，良いと思います．

funextはextで代用できますが、extは集合の包含や写像の等しいことを示すときに必須なので、入れたほうがいいと思います。

そうですね．入れましょう．不等式の rel も欲しい気がしてきました．

convはtacticとして紹介するにはちょっと長くなって独自モードの機能の説明も必要なので、TPIL4の該当箇所に投げるのがいいと思います。

そうですね．

obtainはhaveでいちおう代用できるので（若干振る舞いは違いますが）、まとめてもいいかもしれません。

うーん．時間さえあれば…という感じです．

rewriteを使うことは無い気がしてrwのみでいい気がします。

rewrite と rw を別にするのではなくて，rewrite という見出し名で rw を紹介しようかなと思っていました．

[Seasawher]

全体的に，導入するタクティクをできるだけ少なくするという NNG のような発想ではなくて，

自然にタクティク逆引き辞書ができる程度に，代用可能なタクティクも紹介したいという気持ちです．（労力はかかりますが…）

https://github.com/orgs/lean-ja/discussions/25#discussioncomment-7017369 には対応する日本語も載せていますが，日本語の方を見出しにして逆引きリストにすると結構わかりやすいのでは？とひそかに思っていて，逆引きにするには多義的なタクティクを紹介するより，専門のタクティクを紹介していく方が見やすくなるという意図があります．

[Seasawher]

ローカルコンテキストに hpq: P ∨ Q があってゴールが R のときに，

P ⊢ R と Q ⊢ R の２つのゴールを生成してどちらかを両方示せばいい，みたいにするタクティクってありましたっけ？

[Seasawher]

追記：cases ですね．失礼しました

[haruhisa-enomoto]

（厳密に言うと、どちらかを示せばいいのではなく、どちらも示す必要がありますね）

[Seasawher]

そういえば勉強会のタクティク紹介のこの部分間違ってますね

cases でも，case を使わずに名前をつけることができます

example : P ∨ Q → (P → R) → (Q → R) → R := by
  intro h hPR hQR
  -- `rcases`という`cases`の別バージョンがある。ひとつの違いとして、こちらは`case`を使わなくても
  -- 分岐した仮定に名前を付けられる。箇条書きを使いたい人はこちらを使おう。
  rcases h with hP | hQ
  · sorry
  · sorry

たとえば

example : P ∨ Q → (P → R) → (Q → R) → R := by
  intro h hpr hqr
  cases h with
  | inl hp =>
    exact hpr hp
  | inr hq =>
    exact hqr hq

inl inr を使わなくても～だったら正しそう

[haruhisa-enomoto]

たぶんwith |の構文やinlについての説明を省略したかったのだと思います。

[Seasawher]

@haruhisa-enomoto

下書きを作りました．大筋が問題なさそうか確認してもらませんか？

• 要らないタクティクが入ってるのは今は無視でお願いします
• カテゴリの分け方や日本語のラベルが間違ってるのは指摘してください
• 必要そうなタクティクが入ってないのは指摘して下さい．ただし mathlib 依存のものは後回しです
• 以前挙げてくださっていた，change, convert, congr は私はあまり使ったことがなくてわからないので，できれば PR ください

https://github.com/lean-ja/tactic-tutorial

追記：

• mathlib がないと left right さえ使えないので，mathlib 解禁しました．

[Seasawher]

@haruhisa-enomoto ローカルコンテキストに P : Prop があるかどうか確認するタクティクってありましたっけ？

[Seasawher]

@haruhisa-enomoto

下書きが終わりました．ご確認お願いします．mdbook serve --open でプレビューできます．

https://github.com/lean-ja/tactic-tutorial

追記：提案などあったら PR を出してください．

[haruhisa-enomoto]

お疲れ様です。Rustをインストールしていないのと、空き容量があまりないのと、少し忙しいので、時間がかかるかもしれません。

[Seasawher]

tutorial ではないなと思ったのでリポジトリの名前を変えました．
https://github.com/lean-ja/tactic-cheetsheet

[Seasawher]

@haruhisa-enomoto

こちらで欠けているタクティクを最低限補って公開して，そのあとに確認していただいて，OK ならリリースという流れにしますか？

そうすればローカルでプレビューする必要はありませんし，多少レビューが楽なのではないかと思います

[Seasawher]

β版として公開しました．