まだ小学生の頃に習ったことで印象に残っているのは3の倍数の確認方法でした。各桁を足した数が3の倍数ならば元の数も3の倍数、というアレです。 倍数とか約数とかがLean4で扱えるようになり、この3の倍数の確認方法の証明を書き下してみようと思いました。自分で定理を形式化して証明を与えることを一通りやるには良いのではないかと思ったのです。 任意桁数の3の倍数で証明しようとすると、その数の10進数展開がk桁あるとして各桁を$a_n$とすると$\sum_{n=0}^{k-1} a_n\,10^n$と表すことができるところから始める必要があります。まだ$\sum$記号を勉強していないこともあり、えいやで3…
-数学- Lean4のお勉強 $\sqrt{2}$が無理数であること
Mathematics in Lean 4で進めてきているLean4の勉強も第4章となり、初等整数論が扱えるところまで来ました。 最初の節では$\sqrt{2}$が無理数であることを示します。とはいってもこの段階で示すことは$\sqrt{2}$が有理数であるとして矛盾を導くことまでです。$\sqrt{2}$が実数の中に存在することまで示すわけではありません。 証明は古代ギリシャから知られているものです。$\sqrt{2}=\frac{m}{n}$となる互いに素な自然数$m,n$が存在するとします。すると $$m^2=2\,n^2$$ です。ここから$m$が偶数であることがわかります。$m=2\…
-数学- Lean4のお勉強 シュレーダー＝ベルンシュタインの定理
第4章「集合と関数」の最後のセクションはシュレーダー＝ベルンシュタインの定理のLean4による証明です。 初めてこの定理をきちんとした形で知りました。集合論の濃度に関する基本的な定理です。 定理：$\alpha, \beta$を集合、$f:\alpha \rightarrow\beta, g:\beta\rightarrow\alpha$が両方とも単射である時、$\alpha$から$\beta$への全単射がある。 集合の濃度に関して$ \alpha \ge \beta , \beta \ge \alpha $のとき$ \alpha = \beta $が成り立つということで確かに基本的です…
Mathematics in Leanの第4章「集合と関数」の中の2つ目のセクションである「関数」を読みながら練習問題を解いています。その問題の中で集合族の積集合の写像と集合族の写像の積集合に関する問題がありました。全称量化子と存在量化子が絡み、なかなか手強かったので、紹介したいと思います。 練習問題とその証明は下記のとおりです。 example (i : I) (injf : Injective f) : (⋂ i, f '' A i) ⊆ f '' ⋂ i, A i := by01 intro y h102 simp at h103 simp04 have : (∃ x, (∀ (j : …
「ブログリーダー」を活用して、jurupapaさんをフォローしませんか？
少し事情があって?Lean4での確率の取り扱いについて勉強をしています。とは言っても決して本格的な確率論(測度論をベースにした確率密度関数や確率分布など)ではなく、算数や中学校で習うレベルの確率の話です。いわゆるコイントスの確率やサイコロの確率などです。 これらは離散的な事象の確率として確率質量関数という形でまとめられており、Lean4ではPMF (Probability Mass Function)という形で形式化されています。確率質量関数などと言われるとやはり専門用語にしか見えませんが、ようは離散的な確率事象に確率を割り当てる仕組みです。例えばコイントスでは確率事象は「表が出る」「裏が出る…
Mathematics in Leanを読んできましたが、今回を最終回とします。11.1. Elementary Differential Calculusと12.1. Elementary Integrationの内容の紹介です。 import Mathlib open Real-- サイン関数を微分するとコサイン関数example : deriv sin = cos := by exact Real.deriv_sin example {x:ℝ}: HasDerivAt sin (cos x) x := by exact hasDerivAt_sin x -- サイン関数の0での微分係数は…
今日は3月14日、毎年恒例の円周率の日です。 今年はなんと満月なんです。今、まだ今夜の満月を見ていない人、すぐに外に出てください。関東地方は晴れていて見られます。 記念に今夜のお月様を撮って見ました。次に円周率の日に満月が見られるのはいつのことでしょうか。 EOS 70D, EF-S 55-250mm, SS1/160, ISO 400, F8
少し複雑な関数の極限として $$\lim_{x\to 0}x\,\sin{\frac1{x}}=0$$ を証明します。$x$が$\sin$の引数の分母にあるので$x=0$では定義されませんが$x\to 0$での極限は存在して$0$になる、という命題です。 今回は関数の絶対値を取ってから挟み撃ち論法で証明する方針です。そのための道具として$x\to 0$で、関数の極限が0になることと関数の絶対値の極限が0になることが同値であることを示しておきます。 $$\lim_{x\to 0}f(x)=0 \iff \lim_{x\to 0} f(x) =0\hspace{20cm}$$ theorem re…
今回は関数の極限の証明を見ていきます。 $$\lim_{x\to 2} 2\,x = 4\hspace{20cm}$$ example : Tendsto (fun x:ℝ => 2*x) (𝓝 2) (𝓝 4) := by have cont_two_mul : Continuous (fun x : ℝ => 2 * x) := by exact continuous_const.mul continuous_id refine Continuous.tendsto' cont_two_mul 2 4 ?h -- ⊢ 2 * 2 = 4 linarith 証明するべきことは引数を2倍にする…
まずは数列の極限の証明を見て見ましょう。 $$\lim_{n\to\infty}n = \infty\hspace{20cm}$$ example : Tendsto (fun n:ℕ => n) atTop atTop := by exact tendsto_id exact一発で終わるということは全く同じか、より一般化された証明があるということです。この場合は少し一般化された定理tendsto_idがすでにmathlib4にあり、それが使われました。 tendsto_idという定理はFilter.tendsto_id.{u_1} {α : Type u_1} {x : Filter α} …
Mathematics in Lean 4も最後の方に辿り着きつつあります。これから数回にわたってLean4による解析学の証明を見ていきます。Mathematics In Lean 4の章立てで言えば10.1 Filtersあたりなのですが、そこでの扱いはもっとはるかに抽象的です。この記事では具体例を中心に説明します。 まずは極限ですよね。普通の数学では$\varepsilon - \delta$論法が証明の中心です。一方Lean 4では定義域や値域での極限操作をフィルタという概念で統一的に表現しています。フィルタの概念のレベルで証明が完結する場合もあれば、それを不等式や集合に展開して個別のケ…
久しぶりに（このブログのタイトルにもなっている）Maximaの話題です。 Maximaをブラウザの中でローカルに動かすことに成功しているようです。 https://maxima-on-wasm.pages.dev/ にChromeなどのブラウザでアクセスするとMaximaが起動した画面が表示されます。入力プロンプトの後ろをクリックするとMaximaのコマンドを入力できてきちんと処理が実行されます。こんな感じです。 さらにブラウザの中でgnuplotも動いており、それと組み合わさって2Dや3Dのグラフ生成も動作します。 そしてその動作は全てブラウザ側で動作しており、サーバはWebサーバとしてファ…
前回の記事 -数学- Lean4のお勉強 ラグランジュの定理の続き - Maxima で綴る数学の旅 は色々と修正するべき点や補おう点があり、ここに書き直すことにしました。 前回はGを群、G'をその部分群としてG ≃ (G ⧸ G') × G'という定理の証明について解説しようとしました。まずはこの定理の意味の理解が間違っていたのでそこから始めます。前回の記事では≃は群同型を表すと書きましたが、これは集合の同型でした。つまり、Gと(G ⧸ G') × G'の間には双射がある、すなわちGから(G ⧸ G') × G'への写像toFunと(G ⧸ G') × G'からGへの写像invFunがあり、…
今回もMathematics In Lean 4の第8章 群と環 から8.1.3 部分群を読んでいます。前回の記事でラグランジュの定理「有限群の元の個数は部分群の源の個数で割り切れる」をLean4で形式証明しました。 maxima.hatenablog.jp 証明の肝はSubgroup.groupEquivQuotientProdSubgroupという長い名前の定理です。定理の内容は次の式です。 G ≃ (G ⧸ G') × G' ここでGは群、G'はその部分群です。G⧸G'はGをG'で割った商集合（同値類の集合）です。×は群の直積、≃は群同型です。 意味は群はその部分群で割った商集合と部分群…
今回もMathematics In Lean 4の第8章 群と環 から8.1.3 部分群を読んでいます。 8.1.3のハイライトはラグランジュの定理です。 ラグランジュの定理：有限群の部分群の位数はもとの群の位数の約数である。 G =[G:G'] G' 、あるいは同じことだが、 G = G/G' G' ここにGはある有限群、G'はその部分群、 は群の位数（集合の要素数）、[G:G']はGにおけるG'の指数、G/G'はG'によるGの左剰余類の集合。 多分高校生の頃にこの定理は知っていたと思うのですが、腹落ちして感動したのは大学に入ってからだったと思います。抽象的な代数構造に見える…
Mathematics In Lean 4の第8章 群と環 に進みます。今回は8.1.3 部分群を読んでみます。 あるタイプAの元の集合が群をなすことを示すにはGroup A、Aの元の集合の部分集合がAの演算で群をなす（部分群になる）ことを示すにはSubgroup Aと書きます。演算が加法である場合にはAddSubgroup Aと書けば良いです。 Mathematics In Lean 4では例として整数のなす群が有理数のなす群の加法に関する部分群であることを示します。このためには4つのことを示す必要があります。 1. 整数の集合が有理数の集合の部分集合であること2. 整数の集合が加法で閉じて…
Mathematics In Lean 4の第8章 群と環 に進みます。第8章ではこれらの代数構造について部分集合や代数構造間の写像をLean4で表現する方法を学びます。代数構造としてはより単純なモノイドも扱います。演算の言葉として加法や乗法が出てきますが、主に記号の違いと思ってください。 今回は8.1 モノイドと群を読んでいきます。 以下の代数構造はすでにLean4 / Mathlibに定義されていてすぐに使えます。 Monoid, addMonoid, addCommMonoid Group, addGroup, addCommGroup Commがつけば可換、addがつけば加法群です。加…
Mathematics in Lean4を読んでいます。第7章1節で環の定義のあたりを勉強しています。前回は半群、モノイド、群などを定義し、また環の定義に備えて、乗法モノイドの性質を加法群に自動変換する方法なども説明しました。 ここまでくれば環を定義することができます。 class Ring₃ (R : Type) extends AddGroup₃ R, Monoid₃ R, MulZeroClass R where /-- Multiplication is left distributive over addition -/ left_distrib : ∀ a b c : R, a *…
Mathematics In Leanから第7章 階層 7.1 基礎の勉強を続けます。 "At this stage we would like to move on to define rings"というあたりで、ここから環を定義していきます。 環を定義するにあたっての課題意識は環の2つの演算である加法群と乗法モノイドでは全ての乗法モノイドの定理は加法群でも成り立つことです。この部分を自動的に行う仕組みが必要になります。 使う道具立てはAdd, AddZero, Mul, MulOne, Neg, InvというLean標準定義済みのクラスです。ちなみに明示的には登場しませんが、これらのクラス…
群にあってモノイドにないものは、、、そう、逆元です。モノイドにはすでに演算があり単位元があり演算は結合的でした。そこに全ての元に逆元があれば群になるわけです。 一旦前回までに定義した道具立てを再掲しておきます。 class Semigroup₂ (α : Type) extends Dia₁ α where /-- Diamond is associative -/ dia_assoc : ∀ a b c : α, a ⋄ b ⋄ c = a ⋄ (b ⋄ c) class DiaOneClass₁ (α : Type) extends One₁ α, Dia₁ α where /-- One…
Mathematics In Leanから第7章 階層 7.1 基礎を勉強中です。 ここでは代数構造の階層を構成する方法を知ります。目的はその仕組みの概要を知ることで階層を使えるようになることだそうです。なので完全な理解というよりも主要な言葉や考え方などが理解できれば良いと思います。 実は夏前に7.1 基礎を読んだ時には何をやっているのかいまいちわからず、ちょっと困っていました。夏の暑い間はLean 4はお休みしていたのですが、最近勉強を復活しつつあります。まだ理解が足りていないところが多そうなのですが、まあそこは上記のように割り切って進めることにします。 具体的には7.1では半群、モノイド、…
お久しぶりになってしまいました。 暑い夏の間ちょっと数学系の話題から離れていたこともありこのブログもしばらく放置してしまいました。ぼちぼち復活していきたいと思います。 今回はすこしリハビリも兼ねて最近の私の開発環境の話です。Lean4をM1 iMac, VSCodeで使っています。M1 iMacにOSメジャーアップデートである macOS 15.0 Sequoia が降ってきましたのでそれに合わせて必要なソフトウェアを全て更新してみました。その環境でとりあえず目立った不具合はなくLean4が使えています。 アップデートした開発環境は以下のとおりです。 M1 iMac 16GB + 1TB ma…
前回の記事では普通の証明としてEuclideanDomainには零因子がないことを示しました。こんな感じでした。 $a, b$を零因子、すなわち$a\ne 0, b\ne 0, a * b=0$とします。$a * b = 0$及び$r\; 0\; a$から$r\; (a*b)\; a$。これはmul_left_not_lt a bに矛盾します。これで無事に任意のEuclideanDomainには零因子がないこと、すなわち整域であることが証明できました。 まあいいんですけど、この証明を見て細かいことを言えば$r\; 0\; a$は自明でしょうか。そういうことをきちんと詰めるための道具が形式的証明…
前回疑問に思ったことはまだ解決していません。なので今回は疑問となぜそう思ったのかだけを書いておきます。 前回までの記事でgaussIntは可換環であることを示しました。またgaussIntにquotientやremainderを定義し除法の原理を示すことでEuclideanDomainという型であることも示しました。しかし特に後者の証明ではガウス整数用の（いわゆる）ユークリッド関数を構成してそれが除法の原理を満たすことを示しただけでした。 ガウス整数が整域であること（零因子がないこと）は別途示す必要があると思っていたので、それなしで証明が終わったことが疑問だったのです。 もちろんその証明は普通…
Mathematics in Lean4 もいよいよ第6章まできました。「6.1 構造の定義」は今までの知識があればとても簡単に読み進むことができました。いわゆるレコード型のような構造およびそのレコード型に付随する関数（演算）、そしてレコード型の各フィールドあるいは各フィールド間で成り立つ命題（一種の制約ですね）をまとめて定義できるわけです。 そのレコード型のインスタンスを生成する関数を定義する場合、新たに生成されたインスタンスで制約が成り立つ必要があります。実際にその生成関数が正しくインスタンスを生成できていることを証明する必要があります。つまりインスタンスを生成するにあたり生成関数として各…
連休直前の4月29日より、イギリスでは消費者向けの様々なIoT機器（みなさんがよく使っているスマホ・スマートテレビ・スマートスピーカーを含むおよそ全てのネット接続機器）に一定のセキュリティ対策が施されて販売されています。 非常に大雑把に言うと、1. 対象機器での適切な既定パスワードの設定、2. 機器製造業者による脆弱性報告窓口の設置、3. 対象機器ごとのセキュリティサポート期間の明示がされているはずです。 例えばアマゾンUKで販売されているエコー のページの中ほどにこんな感じでセキュリティアップデートがいつまで受けられるのかの記載があります。Learn moreのリンクをクリックすれば具体的に…
Mathematics in Lean4の数論の章の3つ目のセクションではいよいよ「自然数には素数が無限個ある」ことを形式化して証明します。 証明方法として3つのやり方が説明されています。それぞれの形式化も異なるので下記に記載してみました。 ある自然数nに対して必ずnよりも大きな素数が存在する（作れる）ことを示す。theorem primes_infinite : ∀ n, ∃ p > n, Nat.Prime p := by... 素数が有限個しかないとして、それらの積に1を足した数を考えるとその素因数が元の素数の集合に含まれることから矛盾を導く（ユークリッド）。theorem primes…
有限の場合の総和記号について勉強したことで任意桁数の場合の3の倍数の確認方法について形式化して証明することが出来そうです。ということでやってみました。 まず与えられた自然数が3の倍数かどうかの確認方法と普通の証明をざっと述べてみます。 3の倍数の確認方法：$N, i, a_i$を自然数として$a_i$は各桁の数を表します。従って$\sum_{i=0}^{N-1} a_i\cdot 10^i$が与えられた自然数です。確認方法は、$$3 \sum_{i=0}^{N-1} a_i\cdot 10^i \iff 3 \sum_{i=0}^{N-1} a_i$$が成り立つので、右辺の和（各桁の数…
Mathmatics In Lean4の第5章 初等数論の2つ目の話題は帰納法と再帰です。自然数では定義が帰納的であること（自然数型は帰納型であること）を知ります。 inductive Nat zero : Nat succ (n : Nat) : Nat この意味は、0はNat型、Nat型の要素を1つとってnとするとsucc nもNat型です。そしてsucc n=0となるようなnはありません。ちなみにsucc nはn+1とも書かれます。 次にこの型の上で階乗関数を再帰的に定義します。 def fac : ℕ → ℕ 0 => 1 n + 1 => (n + 1) * fac …
まだ小学生の頃に習ったことで印象に残っているのは3の倍数の確認方法でした。各桁を足した数が3の倍数ならば元の数も3の倍数、というアレです。 倍数とか約数とかがLean4で扱えるようになり、この3の倍数の確認方法の証明を書き下してみようと思いました。自分で定理を形式化して証明を与えることを一通りやるには良いのではないかと思ったのです。 任意桁数の3の倍数で証明しようとすると、その数の10進数展開がk桁あるとして各桁を$a_n$とすると$\sum_{n=0}^{k-1} a_n\,10^n$と表すことができるところから始める必要があります。まだ$\sum$記号を勉強していないこともあり、えいやで3…
Mathematics in Lean 4で進めてきているLean4の勉強も第4章となり、初等整数論が扱えるところまで来ました。 最初の節では$\sqrt{2}$が無理数であることを示します。とはいってもこの段階で示すことは$\sqrt{2}$が有理数であるとして矛盾を導くことまでです。$\sqrt{2}$が実数の中に存在することまで示すわけではありません。 証明は古代ギリシャから知られているものです。$\sqrt{2}=\frac{m}{n}$となる互いに素な自然数$m,n$が存在するとします。すると $$m^2=2\,n^2$$ です。ここから$m$が偶数であることがわかります。$m=2\…
第4章「集合と関数」の最後のセクションはシュレーダー＝ベルンシュタインの定理のLean4による証明です。 初めてこの定理をきちんとした形で知りました。集合論の濃度に関する基本的な定理です。 定理：$\alpha, \beta$を集合、$f:\alpha \rightarrow\beta, g:\beta\rightarrow\alpha$が両方とも単射である時、$\alpha$から$\beta$への全単射がある。 集合の濃度に関して$ \alpha \ge \beta , \beta \ge \alpha $のとき$ \alpha = \beta $が成り立つということで確かに基本的です…
Mathematics in Leanの第4章「集合と関数」の中の2つ目のセクションである「関数」を読みながら練習問題を解いています。その問題の中で集合族の積集合の写像と集合族の写像の積集合に関する問題がありました。全称量化子と存在量化子が絡み、なかなか手強かったので、紹介したいと思います。 練習問題とその証明は下記のとおりです。 example (i : I) (injf : Injective f) : (⋂ i, f '' A i) ⊆ f '' ⋂ i, A i := by01 intro y h102 simp at h103 simp04 have : (∃ x, (∀ (j : …
しばらく前のmacOSではbluetoothイヤフォンで音楽を楽しむ際、コーデック選択の問題で音質が悪い状況がありました。私もiMacとソニーのWF-1000MX4 の組み合わせでこの辺について色々と試してきています。 最近知ったのですが、この状況は少なくともmacOS Sonomaでは大きく改善された面もあり改善されていない面もあります。 以前のmacOSではbluetoothイヤフォンの(正確にはA2DPプロファイルで使う)デフォルトのコーデックがSBCでした。このためたとえイヤフォンがAACをサポートしていてもSBCで繋がってしまい、音が悪い、ということが発生していました。よく知られた改…
Mathematics in LeanもC04 Sets and Functionsの最初の章である集合まで辿り着きました。ここでは集合に関する性質の証明方法のLean4での実現の仕方を知ります。 集合が等しいこと(A=B)を示す場合、ゴールをA=Bとして方法として、AがBの部分集合であり、かつBがAの部分集合であることを示すこと AがBの部分集合であることを示すにはAの任意の要素がBの要素であることを示すこと 空集合と全体集合の性質 和集合と積集合をメンバーシップの論理和と論理積 集合族の積集合と和集合 のようなことがここでは解説されています。ここでは上記の初めの2つについて簡単な命題を示し…
Lean4を証明支援系として使っていても、型と証明の対応や関数型言語が突然現れることがあります。このことを知っていないと証明が読めないことがありました。 具体的には例えばある定理がこんな形だったとします。 def P (x:ℕ) : Prop := sorrytheorem theoA : ∀ x > 3, P x := sorry P xを命題としてxが3より大きい場合はP xが成り立つ、というのがtheoAという定理です。 当然P 4は4>3なので成り立つはずです。証明は普通はこんなふうにやると思うのです。 example : P 4 := by apply theoA -- ⊢ 4 > …
Lean4での論理記号の取り扱いの勉強も後半です。今回は論理積と論理和の扱いを見ていきます。この辺はあまり難しい話は出てきません。 ゴールが論理積A ∧ Bの形の場合にはconstructorタクティクを使うとAとBが両方ともゴールとなり両方証明するとA ∧ Bの証明が終わります。 仮定にh:A ∧ Bがある場合には仮定としてAとBが成り立つのですからバラしてそれぞれを仮定としたいですよね。仮定にh1:Aとh2:Bを入れるにはrcases h with <h1,h2>とかhave <h1,h2>:=hなどとすれば良いです。 ゴールが論理和A∨ Bの形の場合にはAかBのどちらかを証明できれば良い…
否定が論理式に含まれているとき使えるタクティクを勉強しました。 introタクティク：ゴールがある命題の否定¬ Aである場合、intro hとすると仮定h: Aが導入されて、ゴールがFalse (矛盾)に変わります。仮定の集まりの中で適当な命題Bについてhb:Bとhbn:¬ Bを両方含むようにできれば最後にapply hb hbnで矛盾を導いて証明が終わります。 by_contraタクティク：ゴールが特に否定の形ではない場合でも、by_contra hとすることでゴールの否定を仮定hとして導入するとともに、ゴールをFlase(矛盾)にすることができます。仮定の中で矛盾を導くことで証明を終了させ…
現役で最高の数学者のお一人で情報発信にも熱心なテレンスタオ教授のブログがあります。 terrytao.wordpress.com 残念ながら難しすぎて普段はほとんど見ない数学ブログですが、Lean4の勉強をしていたら検索で記事が1つヒットしました！ A slightly longer Lean 4 proof tour What's new 実数の2つの無限数列に関するある補題の証明をLean4を使って形式化して確認する、というものです。証明自体は望遠鏡和(telescoping sum)という手法を使ったものです。有限和をうまく作ると、実は隣り合った項が打ち消しあって最初と最後の項だけが…
ゴールに存在量化子が入っている場合、存在量化子がついた変数に値を入ることでゴールの論理式を証明することができます。useタクティクを使うと、「この値を使え」ということができます。例えばこんな感じです。 example : ∃ x : ℝ, 2 < x ∧ x < 3 := by use 5 / 2 -- ⊢ 2 < 5 / 2 ∧ 5 / 2 < 3 norm_num -- No goals ゴールの論理式の意味は「2より大きくて3より小さい実数xが存在する」です。まあ当たり前ですがどうやって証明するかです。この場合xが$\frac{5}{2}$であればこの不等式は確かに成立するので、xが存在…
今勉強しているMILの第3章「論理」では仮定の論理式やゴールの論理式に登場する論理記号をタクティクでどのように取り扱えば良いのかを説明しています。 この章の最初の方で説明されるのは全称量化子 ∀ です。ゴールの論理式にこの論理記号がついている場合、その変数や中身の式を証明することができません。そこで多くの場合には全称量化子 ∀を外してその中身にアクセスできるようにすることが証明の第一歩となります。 全称量化子 ∀がゴールの論理式に登場している場合、introタクティクを使うとその変数がラベル付きで導入されて、以降の証明で使えるようになります。 例えば前回見たcalcモードの説明の記事では偶関数…
前の記事でcalcモードがわかっていないと書きました。calcは便利そうなのでとりあえず簡単なユースケースを勉強しました。理解できたと思うのでメモを残しておきます。 Quantifiers and Equality - Theorem Proving in Lean 4にある説明を中心にして理解しました。最も典型的なユースケースは等式A=Bを証明する場合です。式Aから始めてタクティクを使って変形し、式Bを導ければ等式証明が成功します。等式変形なので使うタクティクはrwで、仮定や既知の定理を使って式変形します。 現在勉強中の第3章「論理」の中ので分かり易い例があったので紹介します。偶関数と奇関数…
数学の記事では普通は環境について書かないのですが、Lean4はプログラミング環境でもあるし、一応概要を記しておきます。 パソコン：M1 iMac (主記憶16GB), macOS 14.2.1 Lean (version 4.5.0-rc1) VS Code バージョン1.85.1 VS Code機能拡張Lean4 v0.0.124 起動中のVSCodeの様子はこんな感じです。縦分割の左から、フォルダ階層、Mathematics In Lean、練習ファイル、証明ゴール が表示されています。 MILの「2章 基本」の最後の練習問題である「距離関数は常にゼロ以上」の証明が終わったところが練習ファ…
"Mathematics In Lean"に沿ってLean4の証明支援系の勉強を進めています。まだ基本編で、今やっているのはmin, maxの性質の証明です。具体的には全順序集合上の関数min a b （a, bの小さい方を返す）について次の性質の証明です。 min a (min b c) = min (min a b) c 直感的には結局両辺ともa,b,cのうち最小の値を返しますから等しくなるのは納得です。一方この学習では以下の4つの性質だけから上記の性質を示すことが課題です。 le_antisymm : a $\le$ b $\land$ b $\le$ a $\iff$ a=b min_…
