ushumpei’s blog

生活で気になったことを随時調べて書いていきます。

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: 64 := h_nash (Fin.ofNat 0) (Strategy.pure ⟨PrisonersDilemmaStrategies.confess⟩)
        let nh_64: ¬ (64) := 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 や関数型言語をしっかりやっていないからかもしれない
    • 型クラスの気持ちもわかっていないし
  • 6 ≤ 4 とか偽なのが自明なんだけどうまく書くことができなくてもどかしい
  • 自白x2 がナッシュ均衡であることを示したい
  • 混合戦略も面白そう

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 : 515 := 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 : 315 := 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 : 315 := 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 アイテムのリスト
        • でもそんなに面白くないな...
    • そもそも証明が必要になるプログラムはどんなものか?
      • 簡単なプロトコルでも実装してみる?
        • 具体的にどう役に立つ?
      • 証明が必要なもの、必要じゃないものはある
      • 日付の変換、単位の読み替え、何らかのちゃんとした (式等で記述可能な) 定義があるもの?

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 α nFin 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 → Yf ∘ _: (Fin n → X) → (Fin n → Y) に移すことからわかる (: 関数の合成)
    • Vector α n へ関手であることは、f: X → Y_.map f: Vector X n → Vector Y n に移すことからわかる
    • fin_fun_to_vecFin n → α から Vector α n への自然変換であることは、f: X → Ya: 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 を定義しました。

追記: もっといい方法があった

ushumpei.hatenablog.com

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' にした方が良い。VectorMathlib にあるようですが、何が起こっているか分かりにくかったので一旦自前で用意しました。

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 は関手だとして、その間の自然同型とかいうやつ?
  • そろそろ体系的に学ぶべき時が来た気がします
  • ライブラリを探す能力が不足している
    • 新しめな言語を触ることが減っているので、ググれば何かしらのコードがある状況に慣れてしまっている
  • ゲーム理論的な話を Lean4 でやりたくて、プレイヤーが n 人いて、戦略が m 個あって、みたいなことを議論するための道具として Fin n → α をいじった
    • 単に Vector を使えば事足りたのだろうか?
      • 各プレイヤーが戦略を決めた場合のプレイヤーごとの点数は (Fin n → Fin m) → Fin n → ℝ で与えられる感じで良いか?
        • これを Vector で書く場合は?
  • 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 のコンストラクタに渡せばいいということがわかり、これを使えば具体的な値に関して話を進められるかもしれない。

モナドは自己関手の圏 (で自然変換を射、関手の合成を演算と見た場合) におけるモノイド対象

概要

自然変換の垂直合成、関手との合成がわかった結果

モナドは自己関手の圏 (で自然変換を射、関手の合成を演算と見た場合) におけるモノイド対象

だと言葉の意味を理解した。「自己関手の圏って言ったら射、演算は決まりきっているだろう」と言われたらそれまでだけど、知らなかったので。

まとめ

 Cモナドは関手  T: C \rightarrow C、自然変換  \eta : 1_C \Rightarrow T \mu : TT \Rightarrow T で次を満たすもの:

  •  \mu \circ T\mu = \mu \circ \mu T
  •  \mu \circ T \eta = \mu \circ \eta T

これを自己関手の圏 (自己関手を対象、自然変換を射、関手の合成を演算) と見た場合以下の図が可換なので、モナドは自己関手の圏におけるモノイド対象

モノイド対象 - Wikipedia

補足

自然変換の演算

http://alg-d.com/math/kan_extension/nat.pdf

そもそも自然変換の演算の種類を知らないとモナドの定義が読めない、上のサイトがとてもわかりやすかった。対象や射をある程度忘れて図を見ていくと、自分は議論を進められる程度にはわかった。必要な合成の種類は、垂直合成と関手との合成の 2 つ。

垂直合成

  • 圏:  C,  D
  • 関手:  F, G, H: C \rightarrow D
  • 自然変換:  \theta: F \Rightarrow G,  \sigma: G \Rightarrow H

とする、この時  \sigma \circ \theta: F \Rightarrow H a \in C に対し  ( \sigma \circ \theta )_a := \sigma_a \circ \theta_a と定義すれば、これは自然変換になる。

この合成は割と自然な感覚で理解できた。

関手との合成

  • 圏:  B,  C,  D,  E
  • 関手:  F, G: C \rightarrow D
  • 自然変換:  \theta: F \Rightarrow G

関手  H: D \rightarrow E が与えられた時、 H\theta: HF \Rightarrow HG a \in C に対し  (H\theta)_a := H(\theta_a) と定義すれば、これは自然変換になる (自然変換の型に出てくる  HF,  HG は関手の合成)

関手  H': B \rightarrow C が与えられた時、 \theta H': FH' \Rightarrow GH' a \in C に対し  (\theta H')_a := \theta_{H'(a)} と定義すれば、これは自然変換になる。

自然変換は関手によって "延長" できる。他に水平合成というものもあるが、一旦おいておく。

モナドの定義を眺める

モナドの定義は wiki から モナド (圏論) - Wikipedia

圏:  C 上のモナドは 関手:  T: C \rightarrow C と 2 つの自然変換  \eta : 1_C \Rightarrow T ( 1_C C 上の恒等関手) と  \mu : TT \Rightarrow T ( TT T を自分自身に合成した関手) で次を満たすもの:

  •  \mu \circ T\mu = \mu \circ \mu T
  •  \mu \circ T \eta = \mu \circ \eta T

ここで合成された自然変換の型を見てみる、まずは各関手による合成の型を括弧を省略せずにかく

  •  T \mu: T(TT) \Rightarrow TT
  •  \mu T: (TT)T \Rightarrow TT
  •  T \eta: TI \Rightarrow TT
  •  \eta T: IT \Rightarrow TT

 \mu \circ hoge は垂直合成で、結局以下になる

  •  \mu \circ T \mu: T(TT) \Rightarrow T
  •  \mu \circ \mu T: (TT)T \Rightarrow T
  •  \mu \circ T \eta: TI \Rightarrow T
  •  \mu \circ \eta T: IT \Rightarrow T

注意として、関手の合成は結合的なのと恒等関手の性質から、 \mu \circ T\mu = \mu \circ \mu T \mu \circ T \eta = \mu \circ \eta T はちゃんと意味がある (括弧を書いておくと後々わかりやすいので書いている)

この型を元に、自己関手の圏で眺めてみるとブログ冒頭のまとめの図式が得られる。

感想

  • 圏、関手、自然変換の定義はここ: 圏, 関手, 自然変換 - ushumpei’s blog
  • 自然変換が具体的になんなのかわかってなかったのだけど、結合法則とか恒等関手の性質も自然変換ってことだろうか
  • で何がわかったの?という気持ちにはなる
    • モノイド対象だから (>>=) :: IO a -> (a -> IO b) -> IO b みたいな二重の IO になりそうな部分で一つの IO にできる?
  • Haskell でいうと  \eta return か?
    •  \mu TT \rightarrow T なので >>= : : m a -> (a -> m b) -> m bm a -> m m b とした後 m m bm 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 を定義することにした。

感想

  • 定理は SQL 書いている時に思いついて、条件を満たす SQL を生成する、とかの用途で定理証明が活躍する?
  • そろそろ書籍にあたるべきだろうか
  • そもそも実例をもっと調べるべきか
  • ライブラリが充実して欲しい
  • 実装した関数が証明で使いやすいか自信がない
  • 慣れていないせいかちょっとした思いつきを試すのにも時間がかかる

Lean4 学習5

Inductive Types の Exercises の exponentiation の実装。

色々感じが掴めてきて rw、simp を使わないでかけるようになってきた

  • Eq.refl に何か渡すことで 何か = 何かの評価 の等式が得られる
  • Eq.refl は自動的に解決されるので calc の Eq.refl の行は本来不要 (不安だから自分は書いている)
  • 関数定義で変な場合わけを書くと Eq.refl で機能しなくなる
    • Eq.refl帰納型の定義に基づいてなんかしているのだろうか?
    • まずは自分が定義した性質を rfl で証明できることを確かめると良さそう、今回でいう pow_succpow_zero
  • 式を部分的に変更したい場合は congrArg を使えばよくて、第一引数に無名関数、第二引数に Eq を渡す
  • := fun n => match n with は省略可能な時があるっぽい
  • a < bb > 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 を証明しているときに、証明しやすい実装を書かないといけないことに気がつき、ある既存の実装と新しい実装が同じことを数学的に証明する、といったことが結構困難なことだと分かった
    • 例えば fib_inner が内部に隠蔽されていたら?とか、そういったことは文法上不可能になっているのだろうか?(let rec で定義した場合は fib2.fib_inner でアクセスできたので大丈夫だが)
    • 証明を行う対象をどういったものにすべきか考えなければいけない
    • リファクタリングの際に証明毎回行うのヤバそう
    • 逆に証明されている定理に基づいて安全に行える?
      • 安全って何?
      • 今回は関数に対して証明を行ったが、型に対して証明がされている場合、その型を壊さない限りリファクタリングは自由に行える、とか良い面がある?
        • 型を壊すって何?
  • recOn も match も calc も by simp も by rw もだいぶ曖昧にやってる
  • とはいえ関数の等号を示せた経験は、どう使っていくかのイメージが湧いてと思う
  • n < n + 2 くらい証明なしで使いたい、多分方法ある?見つけるのが難しい

lake のパッケージの置き方

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

lake init を使用して作成したプロジェクトの Main.lean から、適当に作った Hoge/Fuga.leanimport Hoge.Fuga でインポートしようとしたがうまくいかなかった。

そこで自分のプロジェクト名 (ここでは Playground) のディレクトリを作成し、その中に Hoge/Fuga.lean を移動し import Playground.Hoge.Fuga でインポートするとうまくいった。

いちいちプロジェクト名のディレクトリを作成しないといけないのだろうか?そういえば既存のライブラリとかは src ディレクトリを置いているのを見たことがある、ということで調べると lakefile.leansrcDir という設定をかけることがわかった。しかしこれもあまり意味がなかった、単に src/Playground/Hoge/Fuga.leanimport 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 が関数型言語 + 定理証明支援系 という部分

定理証明支援系の使用例を調べてみたが、今回の学習からどう繋がっていくかイメージがまだついていない

問題を載せることに関しては 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 構成のサーバー動かします。

主な必要なファイル

  1. Dockerfile
  2. litestream.yml
  3. 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"

prisma/schema.prisma も修正

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
  • LITESTREAM_ACCESS_KEY_ID, LITESTREAM_SECRET_ACCESS_KEY に minio の認証渡します、実際の s3 使う場合は AWS の認証渡します
$ open http://localhost:3000/api/hello

データ表示されてる感じです、再起動しても残る

感想

  • litestream は複数の writer 対応していないことを結構調べてから知った
  • Lambda & container では無理そう
  • ECS on EC2 なら大丈夫そうだけどインスタンス料金はかかる、同時起動制御とかも
  • Fargate?
  • Cloud Run はどんな感じなんだろう?
  • Dockerfile のマルチビルド初めて書いた
  • docker のネットワーク全然わからない、雰囲気で書いている
  • node:slim-18 とかで書きたかったけどちょっとやってダメだったのでやめました
  • litefs は consul server (?) を常時起動する必要がある?