Lean4 でゲーム理論
MixedMatched/formalizing-game-theory というリポジトリでゲーム理論を Lean4 で形式化している人がいて、自分がやりたかったことはこうやればいいのか、と勉強になった。読んだ内容をメモとしてまとめておく、ファイルはこれ: https://github.com/MixedMatched/formalizing-game-theory/blob/0b35fc377f76a5b143bd3f2e6fd36027cdf1ee43/FormalizingGameTheory/Basic.lean
また、囚人のジレンマで両者黙秘はナッシュ均衡にならないことを示せたのでそれも書いておく。
用語はわかっていないため、wiki を参照しながら読んだ。
定義
効用 (Utility)
実数を val として持つ
戦略 (Strategy)
純粋戦略 (pure) と混合戦略 (mixed) を持つ帰納型で、戦略の集合として型を引数に取る
戦略の型を取るためゲームごとに自由に戦略を与えることができる、戦略と戦略の型は違うので注意。
例としてスタグハントゲームの戦略が与えられている
inductive StagHuntStrategies | stag | hare
もう一つの例としてはナッシュの要求ゲーム、実数の値を持つ、持てる値として 0 < で < 1 の条件がついている。
structure NashDemandStrategies := (demand : Real) (above_0: demand > 0) (below_1: demand < 1)
(構造体を値とその証明を持つものとして使うのが勉強になった)
プロファイル (Profile)
ゲーム理論では効用、戦略などの「一覧」をプロファイルと呼ぶ?
- 戦略プロファイル: プレイヤーごとに異なる戦略を取れるような型になっている
- 効用プロファイル:
- (L: List Type) という戦略型のリストをパラメータとしてとっている
- (utilities: List Utility) というフィールドも持ち、L と utitilies の長さが一致する
効用関数 (UtilityFunction)
効用関数は戦略プロファイルを受け取って、効用プロファイルを返す関数。
ゲーム (Game)
効用関数とプレイヤー数を受け取り、ゲームが定義できる、プレイヤーは少なくとも一人いるという条件がある
ナッシュ均衡 (NashEquilibrium)
ナッシュ均衡は戦略プロファイルから Prop への関数として与えられていて、そのプロファイルがナッシュ均衡であることを示す。
内容としては任意のプレイヤーの戦略を任意に変更した場合、そのプレイヤーの効用が低下することを、旧戦略プロファイルを一部書き換えて新戦略プロファイルを作り、新旧効用プロファイルのそのプレイヤーの値を比較することで示している。
具体例を眺める
混乱してきたので、具体例を見てみる。
- 囚人のジレンマの戦略は自白と黙秘の2つで、これは帰納型で定義されている。
- PL という変数を定義している、これはプレイヤーごとの戦略の型のリスト。
- 今回は同じだが、先行後攻で異なる戦略を取ることが可能
- 効用関数を定義している、中でやっていることは、
- 純粋/混合戦略の場合わけ
- 次にマッチしたプロファイルの要素を既知の値として扱っていいことを示す (これいる?)
- 最後にその組み合わせに応じて効用を返す
裏切り合いの原因
囚人のジレンマのよく知られている話として、両者が黙秘することは (パレート最適だが) ナッシュ均衡ではない、というものがある。
このことが案外簡単に示せたのでここに書いておく (リポジトリにも証明があったが途中だった)
theorem MyNotNashEquilibriumSilent : ¬ NashEquilibrium PL 2 PrisonersDilemmaGame PrisonersDilemmaSilentProfile := fun h_nash => let h_64: 6 ≤ 4 := h_nash (Fin.ofNat 0) (Strategy.pure ⟨PrisonersDilemmaStrategies.confess⟩) let nh_64: ¬ (6 ≤ 4) := not_le_of_gt ( (@Real.ratCast_lt 4 6).mpr ( by exact rfl ) ) absurd h_64 nh_64
両者黙秘でナッシュ均衡が成り立っていると仮定すると False になることを示せばいい。 プレイヤー0が自白すれば 6 、黙秘すれば 4 ということがわかっていて、ナッシュ均衡は任意のプレイヤーと戦略を取るので、 プレイヤー0と自白をわたすと 6 ≤ 4 が得られる。 そんなことはないということを愚直に示した。
感想
Lean4 学習10
Lean4 を数学の証明以外で使ってみたい気持ちがあり、しかし現実にある複雑なプログラムを検証する方法がわかっていないため、とりあえず FizzBuzz
の証明を書いてみました。
import Std def fizz_buzz : Nat → String := fun n => if n % 15 = 0 then "FizzBuzz" else if n % 3 = 0 then "Fizz" else if n % 5 = 0 then "Buzz" else toString n -- 15 の倍数で FizzBuzz になることを証明する theorem fizz_buzz_mul_15 (n : Nat) : n % 15 = 0 → fizz_buzz n = "FizzBuzz" := fun mod_15 => by simp [fizz_buzz, mod_15] -- 3 の倍数で 5 の倍数じゃないものは Fizz になることを証明する theorem fizz_buzz_mul_3 (n : Nat) : n % 3 = 0 ∧ (¬ n % 5 = 0) → fizz_buzz n = "Fizz" := fun ⟨mod_3, not_mod_5⟩ => have not_mod_15 : ¬ n % 15 = 0 := fun mod_15 => have mod_5 : n % 5 = 0 := have h : 5 ∣ 15 := by simp -- 書きたくない have dvd_15 : 15 ∣ n := (Nat.dvd_iff_mod_eq_zero 15 n).mpr mod_15 (Nat.dvd_iff_mod_eq_zero 5 n).mp (Nat.dvd_trans h dvd_15) absurd mod_5 not_mod_5 by simp [fizz_buzz, not_mod_15, mod_3] -- 5 の倍数で 3 の倍数じゃないものは Buzz になることを証明する theorem fizz_buzz_mul_5 (n : Nat) : n % 5 = 0 ∧ (¬ n % 3 = 0) → fizz_buzz n = "Buzz" := fun ⟨mod_5, not_mod_3⟩ => have not_mod_15 : ¬ n % 15 = 0 := fun mod_15 => have mod_3 : n % 3 = 0 := have h : 3 ∣ 15 := by simp -- 書きたくない have dvd_15 : 15 ∣ n := (Nat.dvd_iff_mod_eq_zero 15 n).mpr mod_15 (Nat.dvd_iff_mod_eq_zero 3 n).mp (Nat.dvd_trans h dvd_15) absurd mod_3 not_mod_3 by simp [fizz_buzz, not_mod_15, not_mod_3, mod_5] -- 3 の倍数でも 5 の倍数でもないものはそのままの数になることを証明する theorem fizz_buzz_n (n: Nat) : (¬ n % 3 = 0) ∧ (¬ n % 5 = 0) → fizz_buzz n = toString n := fun ⟨not_mod_3, not_mod_5⟩ => have not_mod_15 : ¬ n % 15 = 0 := fun mod_15 => have mod_3 : n % 3 = 0 := have h : 3 ∣ 15 := by simp -- 書きたくない have dvd_15 : 15 ∣ n := (Nat.dvd_iff_mod_eq_zero 15 n).mpr mod_15 (Nat.dvd_iff_mod_eq_zero 3 n).mp (Nat.dvd_trans h dvd_15) absurd mod_3 not_mod_3 by simp [fizz_buzz, not_mod_15, not_mod_3, not_mod_5] def main: IO Unit := let fizz_buzz_list := List.map fizz_buzz (List.range 100) IO.println fizz_buzz_list #eval main
感想
- 色々と課題がある
- Std は勝手にインポートされたりしないのか
- 自明な式を示すために使っている by simp を書かない方法、実はありそう
%
だけで書きたかったが (FizzBuzz 書く時大体は%
で書くと思うので)∣
の方が定理が証明されていて楽だったので使った、敗北感ある- IO わかっていない
- if に式 (Prop) を渡しているので、型レベルでのパターンマッチ?みたいなことをしている?依存型がわかっていない
- 状態を型で定義すれば何らかの証明が書けそう?
- 基本的なプログラムである TODO リストとか書けるだろうか?
- 状態として考えられるのは有限の TODO アイテムのリスト
- でもそんなに面白くないな...
- 状態として考えられるのは有限の TODO アイテムのリスト
- そもそも証明が必要になるプログラムはどんなものか?
- 簡単なプロトコルでも実装してみる?
- 具体的にどう役に立つ?
- 証明が必要なもの、必要じゃないものはある
- 日付の変換、単位の読み替え、何らかのちゃんとした (式等で記述可能な) 定義があるもの?
- 簡単なプロトコルでも実装してみる?
- 基本的なプログラムである TODO リストとか書けるだろうか?
Lean4 学習9'
Lean4 学習9 - ushumpei’s blog こちらで定義した range' : (n : Nat) → Vector (Fin n) n
という関数、もっと簡単に定義できた。
range を定義してから型の対応関係を考えるというのが逆で、型の対応関係を考えたら自然と range に相当するものが出てきた感じ。
Fin n → α
から Vector α n
への自然変換から range 関数 (n ⊢> [0, 1, ..., n-1]
) を得る話
対応関係
以下を定義する。fin_fun_to_vec
は複雑に考えていたがそんなに難しいものではなかった。
fin_fun_to_vec
:f: Fin n → α
をVector α n
に[f 0, f 1, ..., f (n-1)]
という感じで対応させる関数vec_to_fin_fun
:v: Vector α n
をFin n → α
にi ⊢> v[i]
という感じで対応させる関数
def Vector (α: Type) (n: Nat) := { l : List α // l.length = n } def fin_fun_to_vec {n: Nat} {α : Type} (f: Fin n → α): Vector α n := match n with | 0 => ⟨[], rfl⟩ | m+1 => let a: α := f ⟨0, Nat.zero_lt_succ m⟩ let as: Vector α m := fin_fun_to_vec (fun j : Fin m => have hj: j.val + 1 < m + 1 := Nat.add_lt_add_right j.isLt 1 f ⟨j.val + 1, hj⟩) have h : (a::as.val).length = m + 1 := calc (a::as.val).length = as.val.length + 1 := rfl _ = m + 1 := congrArg (· + 1) as.property ⟨a::as.val, h⟩ def vec_to_fin_fun {n: Nat} {α : Type} (v: Vector α n): Fin n → α := fun i => have h : i.val < v.val.length := calc i.val < n := i.isLt _ = v.val.length := Eq.symm v.property v.val.get ⟨i.val, h⟩
定義
fin_fun_to_vec
により Fin n → Fin n
の恒等写像が range n
に変換される
def range (n: Nat) : Vector (Fin n) n := fin_fun_to_vec id #eval range 3 -- [0, 1, 2] #check range 3 -- range 3 : Vector (Fin 3) 3
感想
- まじか
- すごい圏論っぽい話だと思うので時間がある時に考えてみる
- 圏は Hask 圏 (とかいうやつ)、n は固定
Fin n → α
が関手であることは、f: X → Y
をf ∘ _: (Fin n → X) → (Fin n → Y)
に移すことからわかる (∘
: 関数の合成)Vector α n
へ関手であることは、f: X → Y
を_.map f: Vector X n → Vector Y n
に移すことからわかるfin_fun_to_vec
がFin n → α
からVector α n
への自然変換であることは、f: X → Y
、a: Fin n → X
として可換図式の2経路を計算すると[f ∘ a 0, f ∘ a 1, ..., f ∘ a n-1]
で一致することからわかる
- 多分関手とか自然変換とかそれ用のクラスとかがあるはず (だけど一旦放置)
Lean4 学習9
Lean4 で有限個の要素をいい感じに扱いたくてどうすればいいか悩んでいて、Fin n → α
がそれに当たるかなーとか考えたのですが、プログラミングにおいては Vector α n
(長さ固定の List α
) が使いやすいのでその間を埋めることができないかなと色々しています。
とりあえずなんかに使えそうなので range' : (n : Nat) → Vector (Fin n) n
を定義しました。
追記: もっといい方法があった
range
定義
まずは List.range
を真似て、行き先が List (Fin n)
の range
を定義します。range n
は [0, 1, ..., n-1]
を返します。適当に実装したら逆順 [n-1, n-2, ..., 0]
となってしまったり、一個不足した [0, 1, ..., n-2]
となってしまったりして苦労しました。
-- Fin n := {i: ℕ | i < n} = {0, 1, ..., n-1} def range (n: Nat): List (Fin n) := match n with | 0 => [] | i+1 => let fin := ⟨i, (Nat.lt_succ_self i)⟩ loop fin (fin::[]) where loop {n: Nat} : Fin n → List (Fin n) → List (Fin n) | ⟨0, _⟩, ns => ns | ⟨i+1, h⟩, ns => have hh : i < n := calc i < i + 1 := Nat.lt_succ_self i _ < n := h loop ⟨i, hh⟩ (⟨i, hh⟩ :: ns) #eval range 4 -- [0, 1, 2, 3] #check range 4 -- range 4 : List (Fin 4)
証明1
次に長さに関する定理を証明します。range
内部の再帰関数 loop
に関する補題 loop_length
という名前で range.loop nn (nn:nns)
の長さが nn.val + nns.length + 1
と等しいことを示します。ここで最初に躓いたのが n = 0
の時ですが Fin 0
は要素を持たないことに気がつき absurd
で解決できました。他の部分は気合いでいきました。
theorem loop_length: ∀ n, ∀ nn: Fin n, ∀ nns: List (Fin n), (range.loop nn (nn::nns)).length = nn.val + nns.length + 1 | 0, nn , nns => absurd nn.isLt (Nat.not_lt_zero _) | _, ⟨0, h⟩ , nns => calc (range.loop ⟨0, h⟩ (⟨0, h⟩::nns)).length = (⟨0, h⟩::nns).length := rfl _ = nns.length + 1 := rfl _ = 0 + nns.length + 1 := Eq.symm (Nat.zero_add (nns.length + 1)) | n, ⟨i+1, h⟩, nns => let nn' := ⟨i+1, h⟩ have hh : i < n := calc i < i + 1 := Nat.lt_succ_self i _ < n := h let nn := ⟨i, hh⟩ calc (range.loop nn' (nn'::nns)).length = (range.loop nn (nn::nn'::nns)).length := rfl _ = nn.val + (nn'::nns).length + 1 := loop_length n nn (nn'::nns) _ = nn.val + 1 + (nn'::nns).length := Nat.add_right_comm nn.val (nn'::nns).length 1 _ = nn.val + 1 + nns.length + 1 := rfl _ = nn'.val + nns.length + 1 := rfl
証明2
この補題を使用して range n
の長さが n
であることを証明します。congrArg
とか忘れかけています、Eq.refl
の部分は勘で書きました。そろそろ体系的に学ぶべき時が来た気がします。
theorem range_length: ∀ n, (range n).length = n | 0 => rfl | i+1 => let fin := ⟨i, (Nat.lt_succ_self i)⟩ calc (range (i+1)).length = (range.loop fin (fin::[])).length := congrArg List.length (Eq.refl (range (i+1))) _ = fin.val + 1 := loop_length (i+1) fin [] _ = i+1 := rfl
range'
定義
range' : (n : Nat) → Vector (Fin n) n
を定義します。多分この関数を range
にして、前のやつを range'
にした方が良い。Vector
は Mathlib
にあるようですが、何が起こっているか分かりにくかったので一旦自前で用意しました。
def Vector (α: Type) (n: Nat) := { l : List α // l.length = n } def range' (n: Nat): Vector (Fin n) n := ⟨range n, range_length n⟩
感想
range'
を使用してFin n → α
とVector α n
の双方向の変換を書くことができる- もしかしたらもっと簡単で使いやすくかける方法があるかもしれない
- 準同型的なことを示したいが全然分からない、関数や部分集合の等値性はどのように示す?
- そもそも何の同型?α は型、
Fin n → α
とVector α n
は関手だとして、その間の自然同型とかいうやつ?
- そもそも何の同型?α は型、
- そろそろ体系的に学ぶべき時が来た気がします
- 公式のプログラミング側のドキュメント、の日本語訳があり大変助かりました: Theorem Proving in Lean 4 日本語訳 - Theorem Proving in Lean 4 日本語訳
- ライブラリを探す能力が不足している
- 新しめな言語を触ることが減っているので、ググれば何かしらのコードがある状況に慣れてしまっている
- ゲーム理論的な話を Lean4 でやりたくて、プレイヤーが n 人いて、戦略が m 個あって、みたいなことを議論するための道具として
Fin n → α
をいじった - calc がインデントの位置によって失敗するようになった?
_
を行頭の方に寄せて書くことで回避できたが、何が何だか分からなくて混乱した
Lean4 学習8
Lean4 で証明とプログラムをうまく組み合わせたものが書けないか色々試している。証明を書いて、その具体的な値を使って何かするといったことがなかなかうまく出来ず、何となくこれでいいんじゃないかな、という方法が少しわかったのでメモしておく。単体を定義して具体的な点を取得してみた。本当は Vector で書きたかったが、sum
メソッドがないということなので一旦 List
で書いた。by simp
の部分は脳死で書いている。
import Mathlib def pos := { x : List Nat // (∀ i : Fin 3, x[i]! ≥ 0) ∧ x.sum = 1 } theorem h : ∀ i: Fin 3, [1, 0, 0][i]! ≥ 0 := fun i => let l := [1, 0, 0] match i with | 0 => calc l[0] = 1 := by simp _ ≥ 0 := by simp | 1 => calc l[1] = 0 := by simp _ ≥ 0 := by simp | 2 => calc l[2] = 0 := by simp _ ≥ 0 := by simp theorem g : [1, 0, 0].sum = 1 := by simp def l : pos := ⟨[1, 0, 0], ⟨h, g⟩⟩ def ll : pos := ⟨[1, 0, 0], And.intro h g⟩ def lll : pos := Subtype.mk [1, 0, 0] (And.intro h g) -- def llll : pos := ⟨[1, 0, 0], h ∧ g⟩ -- error (なんか間違っている?) #eval l #eval ll
感想
最初、具体的な def l : List Nat := [1, 0, 0]
が l ∈ pos
であることを示そうと思ったが、pos
は型なのでうまくいかず、かといってキャストなどができるかと言えば情報が見つからず悩んでいた。しかし、証明付きで Subtype
のコンストラクタに渡せばいいということがわかり、これを使えば具体的な値に関して話を進められるかもしれない。
モナドは自己関手の圏 (で自然変換を射、関手の合成を演算と見た場合) におけるモノイド対象
概要
自然変換の垂直合成、関手との合成がわかった結果
モナドは自己関手の圏 (で自然変換を射、関手の合成を演算と見た場合) におけるモノイド対象
だと言葉の意味を理解した。「自己関手の圏って言ったら射、演算は決まりきっているだろう」と言われたらそれまでだけど、知らなかったので。
まとめ
圏 のモナドは関手 、自然変換 と で次を満たすもの:
これを自己関手の圏 (自己関手を対象、自然変換を射、関手の合成を演算) と見た場合以下の図が可換なので、モナドは自己関手の圏におけるモノイド対象
補足
自然変換の演算
http://alg-d.com/math/kan_extension/nat.pdf
そもそも自然変換の演算の種類を知らないとモナドの定義が読めない、上のサイトがとてもわかりやすかった。対象や射をある程度忘れて図を見ていくと、自分は議論を進められる程度にはわかった。必要な合成の種類は、垂直合成と関手との合成の 2 つ。
垂直合成
- 圏: ,
- 関手:
- 自然変換: ,
とする、この時 を に対し と定義すれば、これは自然変換になる。
この合成は割と自然な感覚で理解できた。
関手との合成
- 圏: , , ,
- 関手:
- 自然変換:
関手 が与えられた時、 を に対し と定義すれば、これは自然変換になる (自然変換の型に出てくる , は関手の合成)
関手 が与えられた時、 を に対し と定義すれば、これは自然変換になる。
自然変換は関手によって "延長" できる。他に水平合成というものもあるが、一旦おいておく。
モナドの定義を眺める
モナドの定義は wiki から モナド (圏論) - Wikipedia
圏: 上のモナドは 関手: と 2 つの自然変換 ( は 上の恒等関手) と ( は を自分自身に合成した関手) で次を満たすもの:
ここで合成された自然変換の型を見てみる、まずは各関手による合成の型を括弧を省略せずにかく
は垂直合成で、結局以下になる
注意として、関手の合成は結合的なのと恒等関手の性質から、 と はちゃんと意味がある (括弧を書いておくと後々わかりやすいので書いている)
この型を元に、自己関手の圏で眺めてみるとブログ冒頭のまとめの図式が得られる。
感想
- 圏、関手、自然変換の定義はここ: 圏, 関手, 自然変換 - ushumpei’s blog
- 自然変換が具体的になんなのかわかってなかったのだけど、結合法則とか恒等関手の性質も自然変換ってことだろうか
- で何がわかったの?という気持ちにはなる
- モノイド対象だから
(>>=) :: IO a -> (a -> IO b) -> IO b
みたいな二重のIO
になりそうな部分で一つのIO
にできる?
- モノイド対象だから
- Haskell でいうと
return
か?- は なので
>>= : : m a -> (a -> m b) -> m b
でm a -> m m b
とした後m m b
をm b
にするのに使えそう、flatten みたいなものか?
- は なので
- 圏論を自然変換までやらなかったのかなり勿体無かったという気持ちになった
- 垂直合成だと言い切ってしまったが今回の状況だと垂直合成と水平合成は一致する?
Lean4 学習7
ヤングアニマル Web に数学ゴールデンがあった (https://younganimal.com/series/a2c408d4be5da/) ので読んだら鳩の巣原理が出てきて、証明できそうだったのでやってみた。有限集合の濃度の不等号を仮定に単射が存在しないことを示す方針、本質は単射から濃度の不等号を導く部分っぽい (A.card ≤ B.card
を証明する部分)。Classical.choice
が混ざってしまっている。
import Mathlib.Data.Finset.Card open Finset theorem pigeonhole { α : Type u } { β : Type v } [DecidableEq β]: ∀ (A : Finset α) (B : Finset β), A.card > B.card → ¬ (∃ (f : α → β), A.image f ⊆ B ∧ Set.InjOn f A) := fun A B h_card_gt h_exists => have h_card_le : A.card ≤ B.card := h_exists.elim fun f h_inj => calc A.card _ = (A.image f).card := Eq.symm (card_image_of_injOn h_inj.right) _ ≤ B.card := card_le_of_subset h_inj.left absurd h_card_le (by simp [h_card_gt]) /- 'pigeonhole' depends on axioms: [propext, Quot.sound, Classical.choice] -/ #print axioms pigeonhole
感想
- 最初関数を
f : A -> B
と書こうとしたが、それでは像A.image f
の型が合わなかった - 証明済みの定理を探すのが辛く
Mathlib.Tactic.LibrarySearch
もあまり助けてくれない - 次はプログラミング的な側面を実験していきたい、日付型とかで面白い証明考えられないだろうか
DecidableEq
は当然わかっていない、わからないことが多い- ヤングアニマル Web は読み込み遅い?
Lean4 学習6
パターンマッチを書いている時、
match xs with | [] => [] | y::ys => _
としたときに二番目にマッチしたケースでは 0 < xs.length
が成り立っていて欲しいけどそれはダメみたい?そう言う場合はどうすればいいか?素直に if h : 0 < xs.length then ... else ...
で書くか?こうすれば補題 h を後続で使用できるらしい。しかしその場合 y::ys
が使えないので要素にアクセスできない。let で書いてしまえばいいか?if 内で let で分解した場合、補題 h も 0 < (y::ys).length
に分解されるようだ。
List をインデックス付きの List にする zipIndices 関数を書いてみた
def zipIndices {α : Type} (xs : List α) : List ((Fin xs.length) × α) := let rec f (ys : List α) (hx : 0 < xs.length) : List ((Fin xs.length) × α) := if hy : 0 < ys.length then let y::ys := ys ({ val := xs.length - (y::ys).length, isLt := (Nat.sub_lt hx hy) }, y)::(f ys hx) else [] if h : 0 < xs.length then f xs h else []
なんか条件分岐が多くて醜い。再帰のローカル関数必要だろうか? h : 0 < xs.length
を与えてあげれば単純な再帰で直せるか?しかしインデックスを計算するためには大元の xs にアクセスする必要があるのでそれは難しいかもしれない。zip
関数を定義して、0 ~ n までのリストを返す seq n
みたいな関数を定義してやるのが本来なのかもしれない。
本来やりたかったことは以下の定理を示すことだった。時系列の状態をもったデータが並んでいる時に状態が遷移したことの証明として、状態 A の最小値と状態 B の最大値が発生時刻を前後して現れていればいい、と言うもの。(なんかこれ自明じゃない?とか示せると嬉しいの?みたいな疑問が湧いているけど)
theorem exists_iff_min_lt_max (xs : List Status) (s1 : Status) (s2 : Status) : min xs s1 < max xs s2 ↔ ∃ i j : Fin xs.length, i < j ∧ xs.get i = s1 ∧ xs.get j = s2 := sorry
そのために条件を満たす最小/最大のインデックスを返す min
/max
を定義したいが、その前に色々必要で zipIndices
を定義することにした。
感想
Lean4 学習5
Inductive Types の Exercises の exponentiation の実装。
色々感じが掴めてきて rw、simp を使わないでかけるようになってきた
Eq.refl
に何か渡すことで何か = 何かの評価
の等式が得られるEq.refl
は自動的に解決されるので calc のEq.refl
の行は本来不要 (不安だから自分は書いている)- 関数定義で変な場合わけを書くと
Eq.refl
で機能しなくなるEq.refl
は帰納型の定義に基づいてなんかしているのだろうか?- まずは自分が定義した性質を rfl で証明できることを確かめると良さそう、今回でいう
pow_succ
、pow_zero
- 式を部分的に変更したい場合は congrArg を使えばよくて、第一引数に無名関数、第二引数に Eq を渡す
:= fun n => match n with
は省略可能な時があるっぽいa < b
はb > a
と同じっぽい (定義を見にいくと reducible が付いていたからそれのおかげ?)- 数学的帰納法は明示しなくても使えるっぽい? (
pow_le_pow_of_le_left
の証明)
open Nat def my_pow (n : Nat): Nat → Nat | 0 => 1 -- | 1 => n -- ここに変な定義を入れてしまうと `Eq.refl` が機能しなくなる | succ m => (my_pow n m) * n def instPow : Pow Nat Nat := { pow := my_pow } attribute [local instance] instPow theorem pow_succ (n m : Nat) : n^(succ m) = n^m * n := Eq.refl (n^(succ m)) theorem pow_zero (n : Nat) : n^0 = 1 := Eq.refl (n^0) theorem pow_le_pow_of_le_left {n m : Nat} (h : n ≤ m) : ∀ (i : Nat), n^i ≤ m^i := fun i => match i with | 0 => calc n^0 _ = 1 := Eq.refl (n^0) _ ≤ 1 := Nat.le_refl 1 _ = m^0 := Eq.symm (Eq.refl (m^0)) | i + 1 => calc n^(i+1) _ = n^i * n := Eq.refl (n^(i+1)) _ ≤ m^i * m := Nat.mul_le_mul (pow_le_pow_of_le_left h i) h theorem pow_le_pow_of_le_right {n : Nat} (hx : n > 0) {i : Nat} : ∀ {j}, i ≤ j → n^i ≤ n^j | 0, h => have _ : i = 0 := (Nat.le_zero_eq i).mp h calc n^i _ = n^0 := congrArg (n^·) ‹i = 0› _ ≤ n^0 := Nat.le_refl (n^0) | j + 1, h => match Nat.le_or_eq_of_le_succ h with | Or.inr h => calc n^i _ = n^(j+1) := congrArg (n^·) h _ ≤ n^(j+1) := Nat.le_refl (n^(j+1)) | Or.inl h => -- n > 0 は 0 < n と同じ、というルールがある have _ : 1 ≤ n := Nat.succ_le_of_lt hx calc n^i _ = (n^i) * 1 := Eq.symm (Nat.mul_one (n^i)) _ ≤ (n^j) * n := Nat.mul_le_mul (pow_le_pow_of_le_right hx h) ‹1 ≤ n› _ = n^(j+1) := Eq.symm (Eq.refl (n^(j+1))) theorem pos_pow_of_pos {n : Nat} (m : Nat) (h : 0 < n) : 0 < n^m := match m with | 0 => calc 0 _ < 1 := Nat.zero_lt_one _ = n^0 := Eq.refl (n^0) | m+1 => calc 0 _ < (n^m) := pos_pow_of_pos m h _ = (n^m) * 1 := Eq.symm (Nat.mul_one (n^m)) _ ≤ (n^m) * n := Nat.mul_le_mul_left (n^m) (Nat.succ_le_of_lt h) _ = n^(m+1) := Eq.symm (Eq.refl (n^(m+1)))
感想
- 慣れてきたのでそろそろ以下のことがしてみたい
- Mathlib を使って微分幾何とかやってみる
- 世の中にありそうなプログラムの検証を行う
- 定理証明支援系で証明した関数を他のプログラム言語に抽出する、という利用方法があるらしい: https://onct.oita-ct.ac.jp/seigyo/nishimura_hp/pdf/2017watanabe.pdf
- Lean4 だとどうか、とか自分の書ける各言語と相性のいい定理証明支援系はなんだ?とか調べたい
- rfl とか rw とか simp とかはなくても書けることがわかったので、使ってもいいような気もしてきた
- シンタックスシュガーがありすぎて使うべきかどうか迷う
- コードのシンタックスハイライト見つからなかったので haskell のやつ使っている
Lean4 学習4
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 12 -- 144 ok
fib2 は末尾再帰関数を用いて無駄な計算を省く実装
def fib_inner (n0 n1 n : Nat) := match n with | 0 => n0 | n + 1 => fib_inner n1 (n0 + n1) n def fib2 (n : Nat) := fib_inner 0 1 n #eval fib2 12 -- 144 ok
(雑に挙動を確かめる時に 12 を入れて 144 を確かめがち、12 x 12 = 144 で 12th fibonacci = 144 なのが印象的だったので)
末尾再帰関数に関する補題を示す (theorem って書いちゃってるけど)
theorem fib_inner_rule : ∀ n n0 n1 : Nat, fib_inner (n0 + n1) (n0 + n1 + n1) n = (fib_inner n0 n1 n) + (fib_inner n1 (n0 + n1) n) := fun n : Nat => Nat.recOn ( motive := fun n => ∀ n0 n1 : Nat, fib_inner (n0 + n1) (n0 + n1 + n1) n = (fib_inner n0 n1 n) + (fib_inner n1 (n0 + n1) n) ) n ( fun n0 n1 => calc fib_inner (n0 + n1) (n0 + n1 + n1) 0 = n0 + n1 := by simp [fib_inner] _ = fib_inner n0 n1 0 + n1 := by simp [fib_inner] _ = (fib_inner n0 n1 0) + (fib_inner n1 (n0 + n1) 0) := by simp [fib_inner] ) ( fun n ih n0 n1 => calc fib_inner (n0 + n1) (n0 + n1 + n1) (n + 1) = fib_inner (n0 + n1 + n1) (n0 + n1 + (n0 + n1 + n1)) n := by rw [fib_inner] _ = fib_inner (n1 + (n0 + n1)) (n1 + (n0 + n1) + (n0 + n1)) n := by simp [Nat.add_assoc, Nat.add_comm] _ = (fib_inner n1 (n0 + n1) n) + (fib_inner (n0 + n1) (n1 + (n0 + n1)) n) := by rw [(ih n1 (n0 + n1))] _ = (fib_inner n0 n1 (n + 1)) + (fib_inner n1 (n0 + n1) (n + 1)) := by simp [fib_inner] )
fib1、fib2 が等しいことの証明を行う。強い数学的帰納法を使った。この辺全然正しいやり方がわかっていない。
theorem fib1_eq_fib2 : ∀ n : Nat, fib1 n = fib2 n := fun n => Nat.strongInductionOn (motive := fun n => fib1 n = fib2 n) n ( fun n H => match n with | 0 => rfl | 1 => rfl | n + 2 => have _ : fib1 n = fib2 n := have _ : n < n + 1 := lt_succ_of_le (Nat.le_refl n) have _ : n < n + 2 := Nat.lt_trans ‹n < n + 1› (lt_succ_of_le (Nat.le_refl (n + 1))) H n ‹n < n + 2› have _ : fib1 (n + 1) = fib2 (n + 1) := H (n + 1) (lt_succ_of_le (Nat.le_refl (n + 1))) calc fib1 (n + 2) = fib1 n + fib1 (n + 1) := by simp [fib1] _ = fib2 n + fib1 (n + 1) := by rw [‹fib1 n = fib2 n›] _ = fib2 n + fib2 (n + 1) := by rw [‹fib1 (n + 1) = fib2 (n + 1)›] _ = fib_inner 0 1 n + fib_inner 0 1 (n + 1) := by simp [fib2] _ = fib_inner 0 1 n + fib_inner 1 1 n := by simp [fib_inner] _ = fib_inner 1 2 n := by simp [fib_inner_rule n 0 1] _ = fib_inner 0 1 (n + 2) := by simp [fib_inner] _ = fib2 (n + 2) := by simp [fib2] )
ひとまず証明できた。
感想
- by simp, by rw は何が起こっているかわからなくなるので使いたくなかったが、無いと全然進まないので使った。Eq の理解が曖昧なのが原因っぽい。
- 証明した後に書き直そうと思ったがうまくいかない
- fib_inner を証明しているときに、証明しやすい実装を書かないといけないことに気がつき、ある既存の実装と新しい実装が同じことを数学的に証明する、といったことが結構困難なことだと分かった
- recOn も match も calc も by simp も by rw もだいぶ曖昧にやってる
- calc は have と this のシンタックスシュガー?
- とはいえ関数の等号を示せた経験は、どう使っていくかのイメージが湧いてと思う
- n < n + 2 くらい証明なしで使いたい、多分方法ある?見つけるのが難しい
lake のパッケージの置き方
Lean4 では lake コマンドを使用してプロジェクトを作成する、作成したプロジェクトでパッケージの整理をする際に、少し詰まったのでメモしておく。結論はプロジェクト名のディレクトリを作成してそこにファイルを作るとインポートできる。
lake init
を使用して作成したプロジェクトの Main.lean
から、適当に作った Hoge/Fuga.lean
を import Hoge.Fuga
でインポートしようとしたがうまくいかなかった。
そこで自分のプロジェクト名 (ここでは Playground
) のディレクトリを作成し、その中に Hoge/Fuga.lean
を移動し import Playground.Hoge.Fuga
でインポートするとうまくいった。
いちいちプロジェクト名のディレクトリを作成しないといけないのだろうか?そういえば既存のライブラリとかは src
ディレクトリを置いているのを見たことがある、ということで調べると lakefile.lean
に srcDir
という設定をかけることがわかった。しかしこれもあまり意味がなかった、単に src/Playground/Hoge/Fuga.lean
が import Playground.Hoge.Fuga
でインポートできるようになるだった。
この辺りのコード を見てみても import する場所の指定はなさそうだった。名前が衝突するなどの理由から無理なのだろうか?
感想
- ドキュメントの不足
Lean4 学習3
Quantifiers and Equality の演習にて、床屋のパラドックスを示す問題があった。これは排中律を使用すればすぐに解けるのだが、検索してみると構成的証明があるとのことで、やってみると解けた。
variable (men : Type) (barber : men) variable (shaves : men → men → Prop) example (h : ∀ x : men, shaves barber x ↔ ¬ shaves x x) : False := let p := shaves barber barber have _ : p ↔ ¬p := h barber have _ : ¬p := fun _ : p => ((‹p ↔ ¬p›).mp ‹p›) ‹p› have _ : p := (‹p ↔ ¬p›).mpr ‹¬p› ‹¬p› ‹p›
新たに覚えた french quotation marks を使った書き方で解いていくと、どこかで見た命題を証明していることに気がついた。前章 Propositions and Proofs の最後の一文に Prove ¬(p ↔ ¬p) without using classical logic.
とあるのを見つけた、自分は without using classical logic
の部分を見落としていたようだった。
感想
- 排中律は
¬p ∨ p
- 無闇に必要だと決めつけてはいけない
- French quotation marks を使った証明は読みやすい気もするが、入力しにくい問題がある
- 数学記号で書いたコードは検索しにくい問題もある
- 数学用キーボードがあるといい?
- 他の言語と違い、型を明示して変数名を隠す方が読みやすい?
- 証明以外まだ書いていないのでなんとも言えないけど
Lean4 学習2
Quantifiers and Equality の The Existential Quantifier セクションにある問題を解いた。
変数名を気にして書いてみたけど一向に読みやすくならない、たとえばこんなやつ (シンタックスハイライトないのでさらに読みにくい)
example : (¬ ∀ x, p x) ↔ (∃ x, ¬ p x) := Iff.intro (fun h_not_all_p : ¬ ∀ x, p x => (em (∃ x, ¬ p x )).elim (id) (fun h_not_exists_not_p : ¬ ∃ x, ¬ p x => have h_all_p : ∀ x, p x := fun w => (em (p w)).elim (id) (fun hw : ¬ p w => have h_exists_not_p : ∃ x, ¬ p x := Exists.intro w hw absurd h_exists_not_p h_not_exists_not_p) absurd h_all_p h_not_all_p)) (fun h_exists_not_p : ∃ x, ¬ p x => fun h_all_p : ∀ x, p x => h_exists_not_p.elim fun (w : α) (h_not_p : ¬ p w) => absurd (h_all_p w) h_not_p)
byContradiction
は (em h).elim (id) (fun hn =>)
を書き換えられるようだが、宣言以降 False を示すことを覚えておかなければいけないのがちょっと嫌な感じがする。結局 absurd するし。
だが absurd に関しても曖昧な部分が多い、関数が implicit な変数をどうやって見つけているか理解できていないので、無関係な h, not h を渡したら示したかった命題が証明された、という感じがする
byContradiction ... show False from h hn
の方が見やすいのだろうか?証明として読みやすいことと、プログラムとして読みやすいことはどうバランスを取ればいいのだろうか?というか現時点だとどちらとしても読みやすくない書き方になっている。コメントをちゃんとつけるのがいいのだろうか?
変えてみた
example : (¬ ∀ x, p x) ↔ (∃ x, ¬ p x) := Iff.intro ( -- Not「任意の x に対し p x が真」と仮定する fun h_not_all_p : ¬ ∀ x, p x => -- Not「ある x が存在し p x が偽」と仮定して、背理法を用いて証明する byContradiction (fun h_not_exists_not_p : ¬ ∃ x, ¬ p x => -- 補題「任意の x に対し p x が真」が成り立つ have h_all_p : ∀ x, p x := fun x => -- 「p x が偽」 を仮定して、背理法を用いて証明する byContradiction (fun hx : ¬ p x => -- 背理法の仮定より、補題「ある x が存在し p x が偽」が成り立つ have h_exists_not_p : ∃ x, ¬ p x := Exists.intro x hx -- 一つ目の背理法の仮定と補題より矛盾が示された show False from h_not_exists_not_p h_exists_not_p) -- 仮定と補題より矛盾が示された show False from h_not_all_p h_all_p) ) ( -- 「ある x が存在し p x が偽」を仮定する fun h_exists_not_p : ∃ x, ¬ p x => -- 仮定より「p x が偽」な x が得られる h_exists_not_p.elim fun (x : α) (h_not_p : ¬ p x) => -- 「任意の x に対し p x が真」を仮定する fun h_all_p : ∀ x, p x => -- x は「p x が偽」であるが、上記の仮定より「p x が真」になるため、Not「任意の x に対し p x が真」が示された show False from h_not_p (h_all_p x) )
コードとコメントを一対一で書くのは無駄なことしている感がある、ただ数学の証明として意味のあるものを1行に収めることはわかりやすくなるかもしれない。
コメントの方は若干日本語が怪しい (Not とか。~ が偽、というのが偽、を表現するのが難しい)、だいぶブランクがあるか、元々そんなもんだったかわからないが。
感想
- 1行を意味のある単位で改行するのはアリかもしれない
- 変数名をどうするべきかはあまり考えられていない、数学のノリだと lem1 とか数字振っちゃうでもいいけど、もっと読みやすくできないだろうか?しかし文字だけで表現するのは限界があるし、定義元へジャンプできるのだからいいのかもしれない。
h_∃x¬px
とそのまんま記号入りで変数名考えたけど普通にダメ - インデントも悩む
- とはいえ証明っぽくなってきてなかなか楽しい
- byContradiction は脳に悪いということを誰かが言っていたのを思い出した
- 調べたら普通にスタイルガイドあるっぽい?: https://leanprover-community.github.io/contribute/style.html
Lean4 学習
Lean が気になっているので Theorem Proving in Lean 4 の Propositions and Proofs にある演習問題を解いた。プログラムによる定理証明に触れるのは初なので、時々型を定理だと認識できなくなって迷走してしまうなど苦労した。
Lean4 が気になっている理由としては
- 定理証明支援系で堅牢なソフトウェアかけるんじゃないかなという期待
- Lean4 が関数型言語 + 定理証明支援系 という部分
定理証明支援系の使用例を調べてみたが、今回の学習からどう繋がっていくかイメージがまだついていない
- Hyper-V, Ironclad (契約管理?), ... など: https://leanprover.github.io/presentations/20150717_CICM/#/sec-6
- 自動運転の安全性: https://www.nii.ac.jp/news/release/2022/0707.html
- 例としてC言語コンパイラCompCert、オペレーティングシステムseL4が紹介されている: https://note.com/morikita/n/nf45b6e44964f
- seL4 の開発で定理証明支援系によりコスト削減できたみたいな記事をどこかで見たが見失った...
問題を載せることに関しては Apache License 2.0 のため大丈夫な認識
以下
variable (p q r : Prop) -- commutativity of ∧ and ∨ example : p ∧ q ↔ q ∧ p := Iff.intro (fun hpq => ⟨hpq.right, hpq.left⟩) (fun hqp => ⟨hqp.right, hqp.left⟩) example : p ∨ q ↔ q ∨ p := Iff.intro (fun hpq => hpq.elim (fun hp => Or.inr hp) (fun hq => Or.inl hq)) (fun hqp => hqp.elim (fun hq => Or.inr hq) (fun hp => Or.inl hp)) -- associativity of ∧ and ∨ example : (p ∧ q) ∧ r ↔ p ∧ (q ∧ r) := Iff.intro (fun h => ⟨h.left.left, ⟨h.left.right, h.right⟩⟩) (fun h => ⟨⟨h.left, h.right.left⟩, h.right.right⟩) example : (p ∨ q) ∨ r ↔ p ∨ (q ∨ r) := Iff.intro (fun h => h.elim (fun hpq => hpq.elim (fun hp => Or.inl hp) (fun hq => Or.inr (Or.inl hq))) (fun hr => Or.inr (Or.inr hr))) (fun h => h.elim (fun hp => Or.inl (Or.inl hp)) (fun hqr => hqr.elim (fun hq => Or.inl (Or.inr hq)) (fun hr => Or.inr hr))) -- distributivity example : p ∧ (q ∨ r) ↔ (p ∧ q) ∨ (p ∧ r) := Iff.intro (fun h => have hp := h.left h.right.elim (fun hq => Or.inl (And.intro hp hq)) (fun hr => Or.inr (And.intro hp hr))) (fun h => h.elim (fun hpq => And.intro hpq.left (Or.inl hpq.right)) (fun hpr => And.intro hpr.left (Or.inr hpr.right))) example : p ∨ (q ∧ r) ↔ (p ∨ q) ∧ (p ∨ r) := Iff.intro (fun h => h.elim (fun hp => And.intro (Or.inl hp) (Or.inl hp)) (fun hqr => And.intro (Or.inr hqr.left) (Or.inr hqr.right))) (fun h => have hpq := h.left have hpr := h.right hpq.elim (fun hp => Or.inl hp) (fun hq => hpr.elim (fun hp => Or.inl hp) (fun hr => Or.inr (And.intro hq hr)))) -- other properties example : (p → (q → r)) ↔ (p ∧ q → r) := Iff.intro (fun hpqr => fun hpq => hpqr hpq.left hpq.right) (fun h => fun hp => fun hq => h (And.intro hp hq)) example : ((p ∨ q) → r) ↔ (p → r) ∧ (q → r) := Iff.intro (fun h => And.intro (fun hp => h (Or.inl hp)) (fun hq => h (Or.inr hq))) (fun h => fun hpq => hpq.elim (h.left) (h.right)) example : ¬(p ∨ q) ↔ ¬p ∧ ¬q := Iff.intro (fun hnpq => And.intro (fun hp => hnpq (Or.inl hp)) (fun hq => hnpq (Or.inr hq))) (fun h => have hnp := h.left have hnq := h.right fun hpq => hpq.elim hnp hnq) example : ¬p ∨ ¬q → ¬(p ∧ q) := fun h => fun hpq => h.elim (fun hnp => hnp hpq.left) (fun hnq => hnq hpq.right) example : ¬(p ∧ ¬p) := fun h => h.right h.left example : p ∧ ¬q → ¬(p → q) := fun h₁ => fun h₂ => h₁.right (h₂ h₁.left) example : ¬p → (p → q) := fun hnp => fun hp => absurd hp hnp example : (¬p ∨ q) → (p → q) := fun h => fun hp => h.elim (fun hnp => absurd hp hnp) (fun hq => hq) example : p ∨ False ↔ p := Iff.intro (fun h => h.elim (fun hp => hp) (fun hf => hf.elim)) (fun hp => Or.inl hp) example : p ∧ False ↔ False := Iff.intro (fun h => h.right.elim) (fun h => h.elim) example : (p → q) → (¬q → ¬p) := fun hpq => fun hnq => fun hp => hnq (hpq hp) open Classical variable (p q r : Prop) example : (p → q ∨ r) → ((p → q) ∨ (p → r)) := fun h => (em p).elim (fun hp => (h hp).elim (fun hq => Or.inl fun _ => hq) (fun hr => Or.inr fun _ => hr)) (fun hnp => Or.inl (fun hp => absurd hp hnp)) example : ¬(p ∧ q) → ¬p ∨ ¬q := fun h => (em p).elim (fun hp => (em q).elim (fun hq => (h (And.intro hp hq)).elim) (fun hnq => Or.inr hnq)) (fun hnp => Or.inl hnp) example : ¬(p → q) → p ∧ ¬q := fun hn => (em p).elim (fun hp => have hnq : ¬q := fun hq => have h : p → q := fun _ => hq absurd h hn And.intro hp hnq) (fun hnp => have h : p → q := fun hp => absurd hp hnp absurd h hn) example : (p → q) → (¬p ∨ q) := fun hpq => (em p).elim (fun hp => Or.inr (hpq hp)) (fun hnp => Or.inl hnp) example : (¬q → ¬p) → (p → q) := fun h => fun hp => (em q).elim (id) (fun hnq => absurd hp (h hnq)) example : p ∨ ¬p := em p example : (((p → q) → p) → p) := (em p).elim (fun hp => fun _ => hp) (fun hnp => fun h => have hpq : p → q := fun hp => absurd hp hnp absurd (h hpq) hnp)
感想
- 排中律を使った証明が難しい
- have ... absurd で補題を示していく感じにしているがもっと良い書き方ありそう
- And.intro の方がカッコを使った書き方より見やすそう
- フォーマッター欲しい、ちゃんと読んでないけど話はある?(https://github.com/leanprover/lean4/issues/369)
- 関数型言語の側面をうまく使えていないかもしれない
- 依存型がわかってない
- Type と Prop の差異が曖昧、Prop : Type?
- そういえば定理証明支援系って言葉あまり意味を理解していないで使っている
- 定理証明支援系を使って書かれたコードは証明?証明を使ったソフトウェア開発とかいうべき?
Litestream 入りの Dockerfile 作る
Litestream を Dockerfile に同梱して node のなんか動かすやつです。ここでは Next.js & Prisma 構成のサーバー動かします。
主な必要なファイル
- Dockerfile
- litestream.yml
- entrypoint.sh
1. Dockerfile
FROM node:18-alpine as builder ADD . /app WORKDIR /app ADD https://github.com/benbjohnson/litestream/releases/download/v0.3.9/litestream-v0.3.9-linux-amd64-static.tar.gz litestream.tar.gz RUN tar -xzf litestream.tar.gz -C ./ RUN npm install RUN npx prisma generate RUN npm run build FROM node:18-alpine COPY --from=builder /app/next.config.js /next.config.js COPY --from=builder /app/public /public COPY --from=builder /app/package.json /package.json COPY --from=builder /app/.next/static /.next/static COPY --from=builder /app/.next/standalone / COPY --from=builder /app/litestream /usr/local/bin/litestream COPY --from=builder /app/litestream.yml /etc/litestream.yml COPY --from=builder /app/entrypoint.sh /entrypoint.sh ENTRYPOINT ["/entrypoint.sh"]
- litestream のバイナリダウンロードして解凍して、COPY で実行できる場所におきます
- restore したかったので entrypoint.sh にいろいろ書きます
- builder や COPY の部分は物によっていろいろ違いがあると思います
- npx prisma generate で node:18-alpine 用の sqlite3 入ります、後述の schema.prisma の設定が必要
2. litestream.yml
dbs: - path: /tmp/db.sqlite # Database to replicate from replicas: - url: s3://mybkt/litestream # S3-based replication endpoint: http://172.17.0.2:9000 sync-interval: 1s
- ここでは minio を使う想定です、endpoint は minio 起動した時に表示されたものを入れました
3. entrypoint.sh
#!/bin/sh set -e if [ -f /tmp/db.sqlite ]; then rm /tmp/db* fi litestream restore /tmp/db.sqlite litestream replicate -exec "node ./server.js"
- /tmp/db.sqlite にある想定、あったら一旦削除して restore します
- exec で replicate しつつスクリプトを実行できるようです
- /bin/sh と/bin/bash 間違えてハマりました
という感じです。まだ何も作っていない状態だったら以下の感じで諸々入れていけばいいかなと思います。
諸々の入れ方
Next.js
$ npx create-next-app next-prisma-litestream --typescript $ cd next-prisma-litestream
next.config.js 作成
module.exports = { output: 'standalone', }
Prisma
$ npm install --save-dev prisma
$ npx prisma init
.env を修正して sqlite の db を指定 (/tmp/db.sqlite にした)
DATABASE_URL="file:/tmp/db.sqlite"
generator client { provider = "prisma-client-js" binaryTargets = ["native", "linux-musl-openssl-3.0.x"] } datasource db { provider = "sqlite" url = env("DATABASE_URL") } // 動作確認のための適当なテーブル model test { id Int @id @default(autoincrement()) value String }
node:alpine-18
を使う場合 binaryTargets にlinux-musl-openssl-3.0.x
を入れろとエラーで言われたので入れました
マイグレーション実行
$ npx prisma migrate dev
適当なエンドポイント作る
pages/api/hello.ts
import type { NextApiRequest, NextApiResponse } from "next"; import { PrismaClient } from "@prisma/client"; const prisma = new PrismaClient(); type Data = { id: number; value: string; }; const Hello = (req: NextApiRequest, res: NextApiResponse<Data[]>) => { prisma.test .create({ data: { value: new Date().toISOString() }, }) .then(() => prisma.test.findMany()) .then((v) => res.status(200).json(v)); }; export default Hello;
動作確認
minio 起動して Web 画面からバケット作っておきます (mybkt にしました)
$ docker run --rm -p 9000:9000 -p 9001:9001 -v /tmp/minio:/data minio/minio:latest server /data --console-address ":9001"
Dockerfile をビルドして実行します
$ docker build -t ushumpei/next-prisma-litestream:latest . $ docker run --tty --interactive --rm -p3000:3000 --env LITESTREAM_ACCESS_KEY_ID=minioadmin --env LITESTREAM_SECRET_ACCESS_KEY=minioadmin ushumpei/next-prisma-litestream:latest
$ open http://localhost:3000/api/hello
データ表示されてる感じです、再起動しても残る
感想
- litestream は複数の writer 対応していないことを結構調べてから知った
- Lambda & container では無理そう
- ECS on EC2 なら大丈夫そうだけどインスタンス料金はかかる、同時起動制御とかも
- Fargate?
- Cloud Run はどんな感じなんだろう?
- Dockerfile のマルチビルド初めて書いた
- docker のネットワーク全然わからない、雰囲気で書いている
- node:slim-18 とかで書きたかったけどちょっとやってダメだったのでやめました
- litefs は consul server (?) を常時起動する必要がある?