Blog
-
LEAN写経 応用情報数理学特論 第０２回
千葉大学 萩原先生の 応用情報数理学特論 第０２回 の演習をLean4で写経してみる． 演習02-01 — 目標１．example — 目標２．show, from variable (A B : Prop) variable (h : A ∧ B) — example : 証明を与えられる命題 := 証明の具体例 example : A := And.left h — A の証明を与えているイメージ example : B := h.right — B の証明を与えているイメージ example : B ∧ A := And.intro (h.right) (h.left) example :…
-
論理 1
Lean による定理証明は，証明したいステートメントを論理式に落としてプログラミングするわけだが，それには数理論理に関する知識が必要になる．そこで「はじめての数理論理学」山田俊行著，森北出版．2018．を使って数理論理を勉強することにした． ナルホドと思った演習問題に関して，ここに備忘録を残す． 演習問題 1.1 論理同値性の判定 (5) $A \Rightarrow (B \Rightarrow C)$ と $(A \Rightarrow B) \Rightarrow C$ は論理同値か？ 演習問題は真理値表を使って判定することになっているが，式変形で判定する． まず $A \Rightarrow (B \Rightarrow C)$ について $$ \begin{aligned} & \ A \Rightarrow (B \Rightarrow C) \\ \Leftrightarrow & \ \lnot A \lor (\lnot B \lor C) \\ \Leftrightarrow & \ \lnot A \lor \lnot…
-
Lean 3
Lean による定理証明に関する素振り． 今回は次の命題を証明する． 命題 P → R を証明するための仮定として h : P → Q と，h’ : Q → R が与えられているが，命題 P の証明は仮定として与えられていない． この状態で h’ : Q → R を適用すると， このようなエラー表示が出てしまい，証明が進まない． 命題 P の証明が足りていないので，intro を使って apply h’ より前に仮定を追加する． intro (hP : P) は intro hP だけでもよい（Leanが忖度してくれる）． 続けて順に仮定を適用することで No goals となる．これで証明完了． なお，短く書くと次のようにも書ける． example (h : P → Q)…
-
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 でホームページをデザインしていたのとほとんど同じようにサイトが制作できるので，移行にもほとんど時間がかかりませんでした． これだけの機能が無料で使えるというのは，本当に素晴らしい．
投稿されている内容や意見は私個人の見解に基づくものであり，
所属組織・部門見解を代表するものではありません．