Category: math
-
Lean 6
萩原先生から出題された課題(脳トレ)を解いてみた. import Mathlib.Tactic section variable (A : Prop) example : ¬ (A ↔ ¬ A) := by intro (h : A ↔ ¬ A) have h1 : A → ¬ A := h.mp have h2 : ¬ A → A := h.mpr have h3 : (A → ¬ A) → ¬ A := by intro…
-
LEAN写経 応用情報数理学特論 第11回
千葉大学 萩原先生の 応用情報数理学特論 第11回 の演習をLean4で写経してみる. 演習11-01 — 目標1.data.set — 目標2.関数と集合 — 目標3.型上のinjectiveとsurjective import Mathlib.Tactic — Lean4だとだいたいこれで色々使えるようになる(適当...) variable {X Y : Type} (S : Set X) (P : X → Prop) #check ∀ x ∈ S, P x #check ∃ x ∈ S, P x example (h : ∀ x ∈ S, P x) (x : X)…
-
LEAN写経 応用情報数理学特論 第10回
千葉大学 萩原先生の 応用情報数理学特論 第10回 の演習をLean4で写経してみる. 演習10-01 /- 目標1. ℕ inductive zero : ℕ succ : ℕ → ℕ -/ import Mathlib.Tactic — Lean4だとだいたいこれで色々使えるようになる(適当...) #print Nat — これでNatの定義が見れる. #check Nat.zero — Lean では 0 も自然数 #check Nat.succ — これでNat.succの型が見れる. open Nat #eval zero — 0 #eval succ zero — 1 … 0の次の数 #eval succ (succ zero) –…
-
LEAN写経 応用情報数理学特論 第09回
千葉大学 萩原先生の 応用情報数理学特論 第09回 の演習をLean4で写経してみる. 演習09-01 /- 目標1. set set ⊆ \subseteq ∈ \in ∪ \u ∩ \i \ \ ∅ \empty -/ import Mathlib.Tactic — 目標2. False.elim (h : x ∈ (∅ : set U)) variable {U : Type} — このあと引数が柔軟にとれるように,中括弧にしておく variable (A B : Set U) — U を母集合とする部分集合 A, B variable (x :…
-
Lean 5
「はじめての数理論理学」山田俊行著,森北出版.2018.に記載されている演習問題を Lean で解いてみた. — 「はじめての数理論理学」山田俊行著,森北出版.2018 — p.55 2-5 演習問題 import Mathlib.Tactic — 演習問題 2.1 奇数と平方 — 奇数の平方はみな奇数である. example : ∀ (n : ℤ), Odd (n) → Odd (n * n) := by intro n h — 任意の奇数 n をとってくる. have ⟨k, hk⟩ := h — n = 2 * k + 1 となる k をとってくる.…
-
LEAN写経 応用情報数理学特論 第08回
千葉大学 萩原先生の 応用情報数理学特論 第08回 の演習をLean4で写経してみる. 演習08-01 — 目標1.Nat as ℕ — 目標2.Int as ℤ — 目標3./- -/ /- x + y 足し算 x – y 引き算( ℤ ) x * y 掛け算 -x 加法の逆元( ℤ ) #eval 計算結果の表示 -/ #eval 1 + 1 #eval 3 * 10 #eval (-2 : Int) #eval 1 – 2 –…
-
LEAN写経 応用情報数理学特論 第07回
千葉大学 萩原先生の 応用情報数理学特論 第07回 の演習をLean4で写経してみる. 演習07-01 — 目標1.Exists.elimに慣れる — 目標2.$ ← LEAN4では不要? — 目標3.assume に複数の引数を与える $ ← LEAN4では intro variable (U : Type) variable (A B : U → Prop) — Exists.elim は ∃ を除去する規則 — 逆に Exists.intro は ∃ を導入する規則 example : (∃ x, A x ) → ∃ x, A x ∨ B x…
-
LEAN写経 応用情報数理学特論 第06回
千葉大学 萩原先生の 応用情報数理学特論 第06回 の演習をLean4で写経してみる. 演習06-01 — 目標1.(variable of type) → Prop — 目標2.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)…
-
LEAN写経 応用情報数理学特論 第05回
千葉大学 萩原先生の 応用情報数理学特論 第05回 の演習をLean4で写経してみる. 演習05-01 — 目標1. 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 4
Leanの演習問題をChatGPTに作ってもらい,それを解いてみる. ChatGPTへのプロンプトは以下 #命令書: あなたは、定理証明支援系のプログラミング言語Lean4のプログラマーです. 以下の制約条件に基づき,Lean4の証明問題を3つ出して下さい. #制約条件: ・数理論理の問題であること ・証明問題は example を用いること それでは証明問題を3つ出して下さい. このプロンプトで出てきた問題を解いてみたのが以下. — 論理積(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…