lean-ja / tactic-cheatsheet Goto Github PK

現状では lean4:v4.3.0-rc2 ですが，最新は /lean4:v4.4.0-rc1 です

TPiL を紹介するのを忘れていたので，追加する．

sorry を使わない非自明な例にしたい。

find
eval
check
print
guard
time
check_failure （優先度低い）
guard_msgs （要らないかも）
help

プルリクエストに対してデプロイは行うことができない．しかし，mdbook のビルドが通るかチェックはできるし，生成されたアーティファクトを確認することもできる．

この設定がないと，GitHub Pages の見た目を変えるための PR の結果をテストするのに，main ブランチにいったんマージする必要が生じてしまう．

統一するか、きちんと違いを説明するべき

トップの、全タクティクリストのところの説明に誤字が残ってる

GitHub Pages へのリンクは修正し，リダイレクトも行ったが，リポジトリ自体へのリンクが古いままになってしまっている．

wlog を使うありがたみを感じさせる例に変更したい

コード例がコンパイルできることを、git hub action を用いて確かめる

main へのプッシュと pull request ごとに走らせる

TPiL は初心者にとっては読みづらい文献．

重要なキーワードである calc 構文の使い方を雑でいいので紹介しておくべきだと思う．

現在の記述 https://lean-ja.github.io/tactic-cheetsheet/rfl.html ではrflは項のdefinitional equalityを証明するもののように書かれていますが, ドキュメント https://leanprover-community.github.io/mathlib4_docs//Mathlib/Tactic/Relation/Rfl.html によるとこれは refl attributeのついた定理を用いて関係の反射性を示すといったほうが正確ではないかと思います。例えば以下のように順序の反射性を証明することが可能です.

example (n : ℕ) : n ≤ n := by rfl

tauto は古典論理に依存するものも示せるが、aesopでは示せないようだ。これは偶然ではなさそう

この部分が古い．lake-packages はもう使わない．

      - name: Cache dependencies
        uses: actions/cache@v3
        with:
          path: |
            ./lake-packages
          key: deps-${{ runner.os }}-${{ hashFiles('lean-toolchain') }}-${{ hashFiles('lake-manifest.json') }}
          restore-keys: |
            deps-${{ runner.os }}-${{ hashFiles('lean-toolchain') }}

デバッグに便利なので紹介する価値はある

タクティクではあるけど、証明と関係がないので紹介しない方が良いかもしれない。「数学に役立つ」リストとしては要らないはず

普通は ∃ x P x を示すとき，先に x を具体的に渡す．

しかし，P を変形してから x を考えることもできる．

example {c : ℝ} (h : c ≠ 0) : Surjective fun x ↦ c * x := by
  intro y
  use ?term
  simp
  show c * ?term = y

  case term =>
    exact c⁻¹ * y

  case h =>
    rw [mul_inv_cancel_left₀ h y]

メリット

• 今までは md ファイルと lean ファイルの両方を作成していたが，mdgen で一本化できる （既にかなりのタクティクを紹介済みなのでメリットは薄いが…）
• 一つの大きなコードブロックに説明を書くと，読みづらくなってしまう．今まで特にコマンド紹介欄でそれが顕著だった．（コマンド紹介欄はもう対応済み）

デメリット

• 作業が大変．残り 55 個のタクティクに対して行わないといけない．

作業内容

1. Examples/Tactic ディレクトリに lean ファイルを移し，そこからビルドした md ファイルを src ディレクトリに配置するように変更する．
2. 従来 md ファイルと lean ファイルに分かれている内容を，lean ファイルに一本化する
3. 1-2 を 55 タクティクに対して繰り返す

どう考えても rel より先に gcongr を紹介すべきだったと思う

rwは書き換え可能な箇所をすべて書き換えるタクティックですが、これに対して式中で書き換え可能な箇所のうちn番目のみ書き換えるnth_rewriteというタクティックがあります。
https://leanprover-community.github.io/mathlib_docs/tactic/nth_rewrite/default.html
例えば以下のように用いることができます。
https://github.com/s-taiga/lean-math-workshop-my-solution/blob/d58278dc98ac95129c3ce7d7627dec70110dc2f4/Tutorial/Advanced/Algebra/Lecture1.lean#L262
個人的には先日の勉強会時にはかなりお世話になったタクティックだったので、言及があると良いのではないかと思います。

rw のページに追記する

cheat sheet が正しい.

GitHub Page の URLが変わってしまうため、リダイレクトも設定する必要がある

当初は「便利なタクティクを集めて，早見表を作る」のが目的でしたが，紹介するタクティクが多くなってきて辞書のようになりつつあります．早見表としての利便性は確保できているのでしょうか…？

個人的には日本語検索が可能になった時点で十分だと感じていましたが，まだ足りないかもしれません．

Lean 初心者の意見を聞きたいところです．

直接 Action からデプロイする方式に変更する

unfold と rw, dsimp 等がどう違うのかについても，できれば説明したい

any_goals に比べて使う機会も多そうに思えるので，all_goals 単体でまず紹介する

Theorem Proving をちょうど読んでいて，そこで触れられているもので載っていないものを探してみました

• let
• intros (introでも特に触れられていない)
• rename_i
• revert
• match
• simp_arith
• generalize

コンビネータ寄り？

• #35
• #36
• all_goals/any_goals

コンビネータも入れたい？（別 Issue にすべきであればそうします，セクションをそもそも分けたほうがいいかもしれません)

• ;
• <;>
• first| tac| ...

また，以下細かい点

• (目次に) rwはあるがrewriteはない
• (目次に) sorryはあるがadmitはない

あくまでも good first issue として役立てばと思い列挙させていただきました，私も取り組めそうなとこから触ってみようかなと思います

現在は racses と cases が同じページだったり，simp と dsimp が同じページだったりしている．

派生タクティクは，一言説明を考えるのが難しいので同じページにまとめたくなってしまい，このようにしていた．

しかし，紹介するタクティクが多くなってきて，（当初の想定の早見表としてだけでなく）辞書のような使われ方をすることも今後想定される．そうなった場合，一ページあたり一タクティクの方が統一感がある．

import Mathlib.Tactic

theorem T (x y : Nat) (h: x ≤ y) : 2 ^ x ≤ 2 ^ y := by
  apply?

  -- なぜ subgoal が残ってるのに done が通るのか
  done

#explode T

出力の中に sorryAx がある．勝手に sorry しているし，警告も出ない

コード例の中で使用したいこともあるので

以下のタクティクを追加する：

• nlinarith
• replace

mdgen でleanからmdファイルを生成するようになったことで、リンク切れが多くなっているようだ

MIL を参考に例を取るとよいかもしれない

leanprover/std4#463

show のドキュメントとしての使い道しか紹介しないのはまずい

hint は証明に残さない

コード例にはフィボナッチ数列の例を使えばいいかな

guard_hyp のところ

simp_arith, norm_num, linarith はどれも 1 < 2 のようなゴールを閉じることができるタクティクですが，このうち linarith だけ紹介されています．しかし linarith は重めのタクティクです．linarith が必要でない場面では，機能は制限されていてもより軽量なタクティクを使った方が良いように思います．

上記のような注意書きを付け加えるのはいかがでしょうか？

コード例の案. apply? と少し挙動が異なる

import Mathlib.Tactic

variable (P Q : Prop)

example (hPQ : P → Q) (hQR : Q → R) (hQ : P) : R := by
  -- `Try this: exact hQR (hPQ hQ)` と出力される
  exact?

  -- 証明は `exact?` だけで終わっている!
  done