Blog

千葉大学 萩原先生の 応用情報数理学特論　第０７回 の演習をLean4で写経してみる． 演習07-01 — 目標１．Exists.elimに慣れる — 目標２．$ ← LEAN4では不要？ — 目標３．assume に複数の引数を与える $ ← LEAN4では intro variable (U : Type) variable (A B : U → Prop) — Exists.elim は ∃ を除去する規則 — 逆に Exists.intro は ∃ を導入する規則 example : (∃ x, A x ) → ∃ x, A x ∨ B x…

千葉大学 萩原先生の 応用情報数理学特論　第０６回 の演習をLean4で写経してみる． 演習06-01 — 目標１．(variable of type) → Prop — 目標２．Nat variable (U : Type) variable (u : U) variable (A : U → Prop) — A は U から Prop への関数なので A u は Prop である． #check A u — B は Prop から Prop への関数 variable (B : Prop → Prop)…

千葉大学 萩原先生の 応用情報数理学特論　第０５回 の演習をLean4で写経してみる． 演習05-01 — 目標１． def def mpPropDef (A B : Prop) : Prop := A → (A → B) → B — 命題が定義されている def mpProofDef (A B : Prop) : A → (A → B) → B := by intro (a : A) intro (f : A → B) exact f a…

Leanの演習問題をChatGPTに作ってもらい，それを解いてみる． ChatGPTへのプロンプトは以下 #命令書: あなたは、定理証明支援系のプログラミング言語Lean4のプログラマーです． 以下の制約条件に基づき，Lean4の証明問題を3つ出して下さい． #制約条件: ・数理論理の問題であること ・証明問題は example を用いること それでは証明問題を３つ出して下さい． このプロンプトで出てきた問題を解いてみたのが以下． — 論理積（AND）の交換法則を示す定理を証明してください。 example (P Q : Prop) : P ∧ Q ↔ Q ∧ P := Iff.intro (fun hPQ : P ∧ Q => And.intro hPQ.right hPQ.left) (fun hQP : Q ∧ P => And.intro hQP.right hQP.left) — 論理和（OR）の分配法則を示す定理を証明してください。 example (P Q R…

千葉大学 萩原先生の 応用情報数理学特論　第０４回 の演習をLean4で写経してみる． 演習04-01 — 目標1. Or.elim #print Or.elim variable (A B C: Prop) example (f : A → C) (g : B → C) : A ∨ B → C := fun (h : A ∨ B) => Or.elim h (fun (ha : A) => f ha) (fun (hb : B) => g…

数学系のためのLean勉強会の教材 Tutorial/Basic/Lecture4 を解いてみた． Basic/Lecture4.lean import Mathlib.Tactic /- # 単射と全射についての演習問題 このファイルでは、学部数学の集合論の演習問題でよくある、写像の単射と全射についての問題を通して、 `∀`や`∃`についてのより細かい扱いを学ぶ。また、`have`についても復習する。 -/ namespace Tutorial — 以下、`X` `Y` `Z`を集合とする。 variable {X Y Z : Type} /- ## 単射 写像`f : X → Y`が単射であることを`Injective f`で表す。 これは以下のように定義できる。 -/ def Injective (f : X → Y) : Prop := ∀ {x₁ x₂ : X}, f x₁ = f x₂…

数学系のためのLean勉強会の教材 Tutorial/Basic/Lecture3 を解いてみた． Basic/Lecture3.lean import Mathlib.Tactic.Linarith namespace Tutorial /- # 存在 命題`∃ x : X, P x`は`P x`を満たす`x : X`が存在することを表す。 -/ example (n : ℤ) : ∃ m : ℤ, n < m := by — 存在命題は`exists` tacticで証明できる exists n + 1 linarith example (n : ℤ) : ∃ m : ℤ, m < n…

数学系のためのLean勉強会の教材 Tutorial/Basic/Lecture2 を解いてみた． Basic/Lecture2.lean import Mathlib.Tactic.Linarith /- # mathlib mathlibは有志のコミュニテイーによって開発されている数学ライブラリである。 https://leanprover-community.github.io/ mathlibは現在も活発に発展しているライブラリであるが、既に基本的な数学の かなりの部分をカバーしている。 -/ /- # apply? 現在のゴールに適用可能なmathlibの定理(もしくは定義)を探すtactic -/ example [Group G] [Group H] (f : G →* H) (a b : G) : f (a * b) = f a * f b := by — ヒント: `apply?`を使う exact MonoidHom.map_mul f a b –…

Leanには強力な数学用ライブラリ Mathlib がありますが，これを利用するためには，プロジェクトディレクトリを作成する必要があります．この記事では，Lean 4における数学用ライブラリ Mathlib を使った証明プログラムを書くためのプロジェクトディレクトリの作成方法を述べます．Leanプロジェクトの作り方のページに書かれている手順に従い，プロジェクトを作成した記録を以下に述べます．また，すでにLean4をインストールされていることを想定していますので，Lean4自体のインストール手順については触れません． 作業は M1 Mac 上で実施しました．Lean のインストールはvscodeの拡張機能である lean4 を用いて行っています． 参考リンクに従い作業を進めてみる．．． vscode をインストールすると，Leanプロジェクト管理ツールである，elan が ~/.elan/bin/にインストールされていますので，以下のコマンドでツールをアップデートします． $ elan update info: syncing channel updates for ‘stable’ info: latest update on stable, lean version v4.0.0-m5 info: downloading component ‘lean’ Total: 124.9 MiB Speed: 1.5 MiB/s info: installing component ‘lean’ info: syncing channel updates for ‘nightly’…

数学系のためのLean勉強会の教材 Tutorial/Basic/Lecture1 を解いてみた． Basic/Lecture1.lean import Std /- # 遊び方 -/ — 証明があるべき場所に`sorry`と書いてあるので… example : 1 + 1 = 2 := by sorry — 正しい証明に書き直そう！ example : 1 + 1 = 2 := by triv /- # Leanにおける論理 数学的に意味のある文を**命題**と呼ぶ。例えば、「1 + 1 = 2」「3は偶数である」「リーマン予想」などが 命題である。命題は真である場合もあれば偽である場合もあるし、真偽がわかっていない場合もある。数学の 教科書などでは「命題」という単語は「定理」という単語の別名として使われることもあるが、ここでは違う 意味で使われていることに注意しよう。 `P`が命題であることをLeanでは`P : Prop`と書く。また、`h : P`と書けば`h`が`P`の証明であることを 意味する。別の言い方をすると、`h : P`は`P`が真であり、その事実に`h`と名前を付けているという こともできる。 -/…