今勉強しているMILの第3章「論理」では仮定の論理式やゴールの論理式に登場する論理記号をタクティクでどのように取り扱えば良いのかを説明しています。 この章の最初の方で説明されるのは全称量化子 ∀ です。ゴールの論理式にこの論理記号がついている場合…

前の記事でcalcモードがわかっていないと書きました。calcは便利そうなのでとりあえず簡単なユースケースを勉強しました。理解できたと思うのでメモを残しておきます。 Quantifiers and Equality - Theorem Proving in Lean 4にある説明を中心にして理解しま…

数学の記事では普通は環境について書かないのですが、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 …

"Mathematics In Lean"に沿ってLean4の証明支援系の勉強を進めています。まだ基本編で、今やっているのはmin, maxの性質の証明です。具体的には全順序集合上の関数min a b （a, bの小さい方を返す）について次の性質の証明です。 min a (min b c) = min (min…

これからしばらくの間はLean4の証明支援系の勉強の話をシリーズ的に記事にします。相変わらず自分の勉強メモのような感じです。つまづいたところや感動したところを中心に書いていきます。 使用するテキストはMathematics In Lean(通称MIL)にしました。 Math…

年末は帰省していたのですが、有休含めて1/8までお休みにしたこともあり時間ができました。そこでLean 4を勉強してみることにしました。 Lean 4は以前このブログで紹介したLean 3と呼ばれる定理証明支援システムの後継システムです。 Lean 4からは関数型プロ…

今年もこのブログをよろしくお願いします。 昨年の12月に最初は数日おきに、途中から毎日CISSPの練習問題を作成して投稿する、という企画を実行してみました。 CISSP資格試験の問題は巨大なテスト問題のバンクからほぼランダムに選んで各受験者に対して出題…