MixedMatched/formalizing-game-theory というリポジトリでゲーム理論を Lean4 で形式化している人がいて、自分がやりたかったことはこうやればいいのか、と勉強になった。読んだ内容をメモとしてまとめておく、ファイルはこれ: https://github.com/MixedMat…

Lean4 を数学の証明以外で使ってみたい気持ちがあり、しかし現実にある複雑なプログラムを検証する方法がわかっていないため、とりあえず FizzBuzz の証明を書いてみました。 import Std def fizz_buzz : Nat → String := fun n => if n % 15 = 0 then "Fizz…

Lean4 学習9 - ushumpei’s blog こちらで定義した range' : (n : Nat) → Vector (Fin n) n という関数、もっと簡単に定義できた。 range を定義してから型の対応関係を考えるというのが逆で、型の対応関係を考えたら自然と range に相当するものが出てきた感…

Lean4 で有限個の要素をいい感じに扱いたくてどうすればいいか悩んでいて、Fin n → α がそれに当たるかなーとか考えたのですが、プログラミングにおいては Vector α n (長さ固定の List α) が使いやすいのでその間を埋めることができないかなと色々していま…

Lean4 で証明とプログラムをうまく組み合わせたものが書けないか色々試している。証明を書いて、その具体的な値を使って何かするといったことがなかなかうまく出来ず、何となくこれでいいんじゃないかな、という方法が少しわかったのでメモしておく。単体を…

概要 自然変換の垂直合成、関手との合成がわかった結果 モナドは自己関手の圏 (で自然変換を射、関手の合成を演算と見た場合) におけるモノイド対象 だと言葉の意味を理解した。「自己関手の圏って言ったら射、演算は決まりきっているだろう」と言われたらそ…

ヤングアニマル 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 が気になっている理由…

Litestream を Dockerfile に同梱して node のなんか動かすやつです。ここでは Next.js & Prisma 構成のサーバー動かします。 主な必要なファイル Dockerfile litestream.yml entrypoint.sh 1. Dockerfile FROM node:18-alpine as builder ADD . /app WORKDI…