Blog
-
Lean 2
Lean による定理証明に関する素振り． 今回は次の命題を証明する． ⊢ の右側に表示されている現在証明すべき命題は Q ．まず，仮定 h : P → Q を適用すると， ⊢ の右側に P が表示される． 続けて，仮定 hP : P を適用すると， No goals となる．これで証明完了． なお，2つの仮定の適用は次のように1行にまとめることもできる． example (h : P → Q) (hP : P) : Q := by apply h hP
-
Lean 1
Lean による定理証明に関する素振り． vscode上でLeanをインストールすれば，下記のように拡張子が .lean のファイルを開くとvscodeがLeanモードになる． Leanモードでは，サイドビューに定理証明の状況が表示される． 以下のように証明したい命題を example として定義し，by 以降に証明を書く．このモードを tactic mode という． この状態で exampleの次の行へカーソルを移動させると，サイドビューに証明の状況が表示され，現在証明すべき命題が ⊢ の右側に表示される．P である． 命題 P の証明 hP があるので，apply hP とすれば証明完了． サイドビューの Tactic state が変化し，No goals となる．これで証明完了（らしい）．
-
Lean写経 応用情報数理学特論 第０１回
千葉大学 萩原先生の 応用情報数理学特論 第０１回 の演習を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…
-
WordPressに移行
これまでの個人サイトをWordPressに移行しました． 従来のサイトはMacのホームページ作成ソフト Rapid Weaver を使って作っていました．Rapid Weaverはプラグインが豊富で，特に Stacks というプラグインを使うと部品を組み上げるようにホームページが作れて非常に使い勝手がよかったのですが，ライセンスモデルがサブスクに移行してしまったため，年に数回使用するためだけに毎年支払うのは抵抗があり，やめました． WordPressは，Rapid Weaver と Stacks でホームページをデザインしていたのとほとんど同じようにサイトが制作できるので，移行にもほとんど時間がかかりませんでした． これだけの機能が無料で使えるというのは，本当に素晴らしい．
投稿されている内容や意見は私個人の見解に基づくものであり，
所属組織・部門見解を代表するものではありません．