Category: math

Lean による定理証明に関する素振り． 今回は次の命題を証明する． ⊢ の右側に表示されている現在証明すべき命題は Q ．まず，仮定 h : P → Q を適用すると， ⊢ の右側に P が表示される． 続けて，仮定 hP : P を適用すると， No goals となる．これで証明完了． なお，2つの仮定の適用は次のように1行にまとめることもできる． example (h : P → Q) (hP : P) : Q := by apply h hP

Lean による定理証明に関する素振り． vscode上でLeanをインストールすれば，下記のように拡張子が .lean のファイルを開くとvscodeがLeanモードになる． Leanモードでは，サイドビューに定理証明の状況が表示される． 以下のように証明したい命題を example として定義し，by 以降に証明を書く．このモードを tactic mode という． この状態で exampleの次の行へカーソルを移動させると，サイドビューに証明の状況が表示され，現在証明すべき命題が ⊢ の右側に表示される．P である． 命題 P の証明 hP があるので，apply hP とすれば証明完了． サイドビューの Tactic state が変化し，No goals となる．これで証明完了（らしい）．

千葉大学 萩原先生の 応用情報数理学特論　第０１回 の演習をLean4で写経してみる． 演習01-01 割愛 m(_ _)m 演習01-02 variable (A : Type) variable (B C D: Type) variable (a : A) variable (b₁ b₂ : B) variable (c : C) variable (f : A → B) variable (g : B → C) variable (h : A → B → C → D) variable (i…