ushumpei’s blog (original) (raw)

最初

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", ), ); ...

感想

仕事で

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))

感想

だいぶ忘れている。

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)

ゲーム理論では効用、戦略などの「一覧」をプロファイルと呼ぶ？

効用関数 (UtilityFunction)

効用関数は戦略プロファイルを受け取って、効用プロファイルを返す関数。

ゲーム (Game)

効用関数とプレイヤー数を受け取り、ゲームが定義できる、プレイヤーは少なくとも一人いるという条件がある

ナッシュ均衡 (NashEquilibrium)

ナッシュ均衡は戦略プロファイルから Prop への関数として与えられていて、そのプロファイルがナッシュ均衡であることを示す。

内容としては任意のプレイヤーの戦略を任意に変更した場合、そのプレイヤーの効用が低下することを、旧戦略プロファイルを一部書き換えて新戦略プロファイルを作り、新旧効用プロファイルのそのプレイヤーの値を比較することで示している。

具体例を眺める

混乱してきたので、具体例を見てみる。

囚人のジレンマ

裏切り合いの原因

囚人のジレンマのよく知られている話として、両者が黙秘することは (パレート最適だが) ナッシュ均衡ではない、というものがある。

このことが案外簡単に示せたのでここに書いておく (リポジトリにも証明があったが途中だった)

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 を数学の証明以外で使ってみたい気持ちがあり、しかし現実にある複雑なプログラムを検証する方法がわかっていないため、とりあえず 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

theorem fizz_buzz_mul_15 (n : Nat) : n % 15 = 0 → fizz_buzz n = "FizzBuzz" := fun mod_15 => by simp [fizz_buzz, mod_15]

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]

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]

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

感想

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 は複雑に考えていたがそんなに難しいものではなかった。

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

感想

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] となってしまったりして苦労しました。

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⟩

感想

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)

#eval l #eval ll

感想

最初、具体的な def l : List Nat := [1, 0, 0] が l ∈ pos であることを示そうと思ったが、pos は型なのでうまくいかず、かといってキャストなどができるかと言えば情報が見つからず悩んでいた。しかし、証明付きで Subtype のコンストラクタに渡せばいいということがわかり、これを使えば具体的な値に関して話を進められるかもしれない。

ヤングアニマル 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

感想

パターンマッチを書いている時、

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

感想

Inductive Types の Exercises の exponentiation の実装。

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

感想

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]

)

ひとまず証明できた。

感想

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 する場所の指定はなさそうだった。名前が衝突するなどの理由から無理なのだろうか？

感想

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 の部分を見落としていたようだった。

感想

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 (

fun h_not_all_p : ¬ ∀ x, p x =>

byContradiction (fun h_not_exists_not_p : ¬ ∃ x, ¬ p x =>
  
  have h_all_p : ∀ x, p x := fun x =>
    
    byContradiction (fun hx : ¬ 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)

) (

fun h_exists_not_p : ∃ x, ¬ p x =>

h_exists_not_p.elim fun (x : α) (h_not_p : ¬ p x) =>

fun h_all_p : ∀ x, p x =>

show False from h_not_p (h_all_p x)

)

コードとコメントを一対一で書くのは無駄なことしている感がある、ただ数学の証明として意味のあるものを１行に収めることはわかりやすくなるかもしれない。

コメントの方は若干日本語が怪しい (Not とか。~ が偽、というのが偽、を表現するのが難しい)、だいぶブランクがあるか、元々そんなもんだったかわからないが。

感想