ヤングアニマル Web に数学ゴールデンがあった (https://younganimal.com/series/a2c408d4be5da/) ので読んだら鳩の巣原理が出てきて、証明できそうだったのでやってみた。有限集合の濃度の不等号を仮定に単射が存在しないことを示す方針、本質は単射から濃…

パターンマッチを書いている時、 match xs with | [] => [] | y::ys => _ としたときに二番目にマッチしたケースでは 0 < xs.length が成り立っていて欲しいけどそれはダメみたい？そう言う場合はどうすればいいか？素直に if h : 0 < xs.length then ... el…

Inductive Types の Exercises の exponentiation の実装。 色々感じが掴めてきて rw、simp を使わないでかけるようになってきた Eq.refl に何か渡すことで 何か = 何かの評価 の等式が得られる Eq.refl は自動的に解決されるので calc の Eq.refl の行は本…

n 番目の fibonacci 数を求める 2 つの関数が等しいこと (全ての引数に対し等しい戻り値を返すか) を証明してみた。 まず fib1 は素朴な実装 open Nat def fib1 (n : Nat) := match n with | 0 => 0 | 1 => 1 | n + 2 => fib1 n + fib1 (n + 1) #eval fib1 1…

Lean4 では lake コマンドを使用してプロジェクトを作成する、作成したプロジェクトでパッケージの整理をする際に、少し詰まったのでメモしておく。結論はプロジェクト名のディレクトリを作成してそこにファイルを作るとインポートできる。 lake init を使用…

Quantifiers and Equality の演習にて、床屋のパラドックスを示す問題があった。これは排中律を使用すればすぐに解けるのだが、検索してみると構成的証明があるとのことで、やってみると解けた。 variable (men : Type) (barber : men) variable (shaves : m…

Quantifiers and Equality の The Existential Quantifier セクションにある問題を解いた。 変数名を気にして書いてみたけど一向に読みやすくならない、たとえばこんなやつ (シンタックスハイライトないのでさらに読みにくい) example : (¬ ∀ x, p x) ↔ (∃ x…

Lean が気になっているので Theorem Proving in Lean 4 の Propositions and Proofs にある演習問題を解いた。プログラムによる定理証明に触れるのは初なので、時々型を定理だと認識できなくなって迷走してしまうなど苦労した。 Lean4 が気になっている理由…