Jev と StopHook で構築する自動ループ

箇条書きを Gemini でまとめた記事です

背景・モチベーション

• 家事と育児でまとまった開発時間が取れない
• AI Agent 使って隙間時間でアプリとか作れようになってきた(nutrate)
• もっと活用できないか？と考えた
  • Discord に入れたら、コミュニケーションの仲介として良い働きをすることがわかった
  • 「事業検証→LP作成→Google Ads出稿→計測」を自動化した。検証自体は失敗したが手応えは得た

自動で回し続けるやつ面白そう

---

言ったことやらない問題

• CLAUDE.md や SKILL に書いても割とやらない解決策はスクリプトによる判定
  1. タスクの定義 ＝ 終了条件の定義
  2. 終了条件をスクリプトにして、人間と AI の契約書（っぽいもの）とする
  3. スクリプトが exit 0 を出すまでフックでループさせ続ける
• Jev
  • 手軽に定性的な評価を定量化
  • スクリプトでかける条件が広がった

---

ループに与えている「事業の要件と評価観点」

実際に AI（Opus 5.5）に書かせている README.md のフォーマットと、Jev で判定させている閾値

1. 記述項目（フォーマット）

1. 背景・既知の事実 — 現状・変化・市場の動き（出典URL必須）
2. 課題 — 誰のどんな「負」か
3. 独自仮説（構造・法則） — なぜ既存ではダメで、何に置き換えれば成り立つか
4. 事業内容（解決策） — 誰に・何を・どう提供するか
5. 仮説検証方法 — 手軽・短期間で確かめる方法（月10万円からの逆算）

2. Jev による定性評価の観点と合格ライン

deno run -A scripts/jev-check.ts で判定し、全観点が閾値以上なら合格。

• 独自仮説の筋が良いか（0.8） — 原因を人の怠慢や値段ではなく、制度やサービスの構造（収益モデル・インセンティブ等）に求めているか
• 話がつながっているか（0.9） — 事実→課題→仮説→事業内容が一貫しているか
• 誰の課題かが具体的か（0.9） — 「みんな」ではなく絞られているか
• 検証が小さく早いか（0.9） — システムをいきなり作らず、手順・期間・費用まで小さく設計されているか
• 事業として成り立つか（0.5） — 自分たちで実行でき、対価が発生する形か

---

システムの仕組みとフロー

• 自作の「ループプラグイン」に SKILL と StopHook を設定
• StopHook で終了条件スクリプトを呼ぶ構成

実際の動き:

1. タスクを投げると、AI（Opus 5.5）が自ら終了条件スクリプトを書く
2. AI が「この終了条件（スクリプト）でいいですか？」と人間に確認する
3. 人間がフィードバックして合意（OK）を出す
4. ループ開始: スクリプトが exit 0 になるまで放置
   • 機械チェック：README の数、評価や絵が最新の README から作られているか、ディレクトリ構造、PR が出ているか
   • 定性チェック：Jev（Noul）で上記の観点・閾値を判定
   • Opus 5.5 が条件を満たすまで修正ループを回し続ける

---

実験: 「フレイル予防の事業アイディア100個」

• 上記の条件スクリプトを握らせて放置
• 途中でセッション上限に達した。コミットの記録では、最初の12案から100案まで約6時間（解除待ちを含む）で完走
• 100個のアイディアが出力されたが、テキストのままだとレビューがだるいので、ビューアーを作ってもらった
  • 生成された事業アイディア＆ビューアー
• 結構面白い
• ポリファーマシーなど知らなかったことが知れたり
• 本当か？みたいな記述は結構ある

---

その後: エンタメ50案

• 同じ仕組みで「エンタメの事業アイディア50個」
• ほぼ全案の仮説が「〜は、〜の設計のせいである」という同じ書き出しだった
• 微妙
• 課題解決系の方が向いてる評価設定だからそうなるよなーって感じ

---

感想

• 終了条件定めるところが自動ではないし割と面倒な作業だと思う
• 可読性のためdeno にしたのは良い判断した
• マネタイズの視点強めると同じようなものばかりでつまらなくなるけど、ないとそれ行政の仕事では？って感じになる

SQL の `IS NOT DISTINCT FROM` で真偽値を比較した結果

SQL の IS NOT DISTINCT FROM で真偽値を比較した結果をメモしておく。 IS NOT DISTINCT FROM は値に null が入る可能性があっても "正しく" 比較できる (どう正しいかは以下の実行結果を参照)

  SELECT
    a, b, a IS NOT DISTINCT FROM b
  FROM (VALUES
    (true, true),
    (true, false),
    (true, null),
    (false, true),
    (false, false),
    (false, null),
    (null, true),
    (null, false),
    (null, null)
  ) as t(a, b);
┌─────────┬─────────┬────────────────────────────┐
│    a    │    b    │ (a IS NOT DISTINCT FROM b) │
│ boolean │ boolean │          boolean           │
├─────────┼─────────┼────────────────────────────┤
│ true    │ true    │ true                       │
│ true    │ false   │ false                      │
│ true    │ NULL    │ false                      │
│ false   │ true    │ false                      │
│ false   │ false   │ true                       │
│ false   │ NULL    │ false                      │
│ NULL    │ true    │ false                      │
│ NULL    │ false   │ false                      │
│ NULL    │ NULL    │ true                       │
└─────────┴─────────┴────────────────────────────┘

Option[Boolean] 値の等値比較みたいな感じ。

macOS 15 (Sequoia) の Window > Move & Resize 以下の項目に、新たなショートカットを割り当てる

状況

macOS 15 でウィンドウの並び替え等の Windows っぽい機能が追加*1されて、便利なので活用したい。しかし自分の使っている HHKB HYBRID では fn キー (ショートカット上では地球マークのユニバーサルキーで表される) と矢印キーの組み合わせのショートカットがうまく動作しないようなので、新たなショートカットを割り当てることで対応した。

*1 実は macOS 15 前も Move Window to Right Side of Screen などの Window の項目はあった

この記事が参考になった。 https://www.sungrove.co.jp/mac-shortcut-key/#toc_7

はまりポイントは mac でメニューの項目をショートカットとして設定する方法の書式が特徴的で、 メニュー名->子メニュー名->...->項目名 というふうに -> を使ってネストを表現していく部分。

実際の手順



「System Settings」 > 「Keyboard」 > 「Keyboard Shorcuts...」 を選択

「App Shortcuts」 > (「All Applications」 >) 「plus アイコン」を選択



メニュータイトルに前述のルールで項目名を入力 (Window->Move & Resize->Left 等)、好きなショートカットキーを割り当てる

これでいけるはず。設定後もなぜか動作しない状態だったが再起動したり再設定したりごちゃごちゃしているうちに動作するようになった。

感想

• 便利
• 心情的に未設定を保ちたいけどこれに関しては HHKB 由来の問題であることと便利なので設定変更した

Cloudflare Workers + Hono で jwt を扱うときにハマった

最初

jsonwebtoken (https://www.npmjs.com/package/jsonwebtoken) で ES256 を使って生成/検証しようとしたけどエラーでうまくいかなかった。

調査

https://github.com/auth0/node-jsonwebtoken/blob/v9.0.2/sign.js#L117

createPrivateKey がエラーを発生させているので、createSecretKey が使われている模様、なので type == 'secret' になってしまってエラー (https://github.com/auth0/node-jsonwebtoken/blob/v9.0.2/sign.js#L130) が出ている。

node_modules/jsonwebtoken/sign.js をいじってエラーを出力すると createPrivateKey が定義されていないようだった。

node_compat_v2 は設定していたが、リストを見ると createPrivateKey は対応していない模様。

https://developers.cloudflare.com/workers/runtime-apis/nodejs/crypto/#keys

解決

https://hono.dev/docs/helpers/jwt#jwt-authentication-helper

どうしたものかと調べていたら hono のドキュメントに行き当たり、ヘルパー関数があるとのことなのでそれを使うことにしたらうまく行った。

メモ

ES256 の鍵の作り方

https://blog.authlib.org/2023/openssl-ec-keys

openssl ecparam -name prime256v1 -genkey -noout -out test.key
openssl ec -in test.key -pubout -out test.pem 

base64 エンコードして環境変数にいれた (とりあえず .dev.vars に書いた)

cat test.key | base64 | pbcopy
cat test.pem | base64 | pbcopy

コード

import { sign, verify } from "hono/jwt";
...
const token = await sign(
    { ...payload, exp: Math.floor(Date.now() / 1000) + 60 * 60 * 24 },
    Buffer.from(c.env.PRIVATE_KEY, "base64").toString("ascii"),
    "ES256",
);
console.log(
    await verify(
        token,
        Buffer.from(c.env.PUBLIC_KEY, "base64").toString("ascii"),
        "ES256",
    ),
);
...

感想

• 消耗した
• hono/jwt では payload にごちゃごちゃ入れちゃっているけどいいのだろうか？
• 多分 RS256 も同じハマりポイントある？

ふとした時の検証

仕事で

a > c * n または b > c * m

みたいな条件を判定する必要があり、

b / m > a / n

の関係が成り立っているので

b > c * m

だけ確かめればいい、みたいなことを考えました。

ふと、本当にそうだっけ？と思ったので Lean4 で証明してみました。

variable (p q: Prop)

example : (p ∨ q) ∧ (p → q) ↔ q := Iff.intro
  (fun ⟨h1, h2⟩ => h1.elim (fun h3 => h2 h3) (fun h3 => h3))
  (fun h => And.intro (Or.inr h) (fun _hp => h))

感想

だいぶ忘れている。

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

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 として可換図式の２経路を計算すると [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' にした方が良い。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 → α をいじった
  • 単に 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 のコンストラクタに渡せばいいということがわかり、これを使えば具体的な値に関して話を進められるかもしれない。

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

概要

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

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

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

まとめ

圏 のモナドは関手 、自然変換 と で次を満たすもの:

• 
• 

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

モノイド対象 - Wikipedia

補足

自然変換の演算

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 を定義することにした。

感想

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

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 を証明しているときに、証明しやすい実装を書かないといけないことに気がつき、ある既存の実装と新しい実装が同じことを数学的に証明する、といったことが結構困難なことだと分かった
  • 例えば fib_inner が内部に隠蔽されていたら？とか、そういったことは文法上不可能になっているのだろうか？(let rec で定義した場合は fib2.fib_inner でアクセスできたので大丈夫だが)
  • 証明を行う対象をどういったものにすべきか考えなければいけない
  • リファクタリングの際に証明毎回行うのヤバそう
  • 逆に証明されている定理に基づいて安全に行える？
    • 安全って何？
    • 今回は関数に対して証明を行ったが、型に対して証明がされている場合、その型を壊さない限りリファクタリングは自由に行える、とか良い面がある？
      • 型を壊すって何？
• recOn も match も calc も by simp も by rw もだいぶ曖昧にやってる
  • calc は have と this のシンタックスシュガー？
• とはいえ関数の等号を示せた経験は、どう使っていくかのイメージが湧いてと思う
• n < n + 2 くらい証明なしで使いたい、多分方法ある？見つけるのが難しい