Lean4でバブルソートを書く
この記事は証明支援系 Advent Calendar 2024 19日目の記事です
Lean4は定理証明支援系かつ純粋関数型プログラミング言語なんですが、今のところ日本語記事は定理証明に焦点を当ててるものがわりかし体感多い気がします(←ゴミみたいな保険かけ)
でもやっぱり依存型を持つプログラミング言語としてのLeanがめちゃんこ好きで、プログラミング言語としても流行ってほしいな～って願望がめちゃくちゃあります。
なのでLeanでのプログラミングの勉強を始めてみたいって人たちとか、関数型プログラミング言語に興味ある人たちに、基本的なアルゴリズムであるバブルソートを通してLeanを知ってもらおうということでこれを書いてます。
対象読者は書かれたコードがなんとなくで読める方です。[1]
ただのバブルソートといえどLeanの特徴がいろいろ出て奥深いんですよ！覚悟しておけ
書く
なんと普通にforで書けます！
def bubbleSort [Inhabited α] [Ord α] (arr : Array α) : Array α := Id.run do
let mut arr := arr
for i in [0:arr.size] do
for j in [0:arr.size - 1 - i] do
match Ord.compare arr[j]! arr[j + 1]! with
|.gt => arr := arr.swapIfInBounds j (j + 1)
|.lt |.eq => pure ()
arr
驚いただろ
Leanは純粋関数型言語ではあれどdo記法の中ならかなり手続き的に書くことができます！
具体的にはelseのないif、早期リターン、for、while、果てには可変変数まで可能です。
これら手続き的な書き方は全て最終的に全て関数呼び出しの形に変換されます。
最終的な関数呼び出しの形
def bubbleSort : {α : Type} → [inst : Inhabited α] → [inst : Ord α] → Array α → Array α :=
fun {α} [Inhabited α] [Ord α] arr =>
(let arr := arr;
bind
(let col := { start := 0, stop := arr.size, step := 1 };
forIn col arr fun i r =>
let arr := r;
bind
(let col := { start := 0, stop := HSub.hSub (HSub.hSub arr.size 1) i, step := 1 };
forIn col arr fun j r =>
let arr := r;
bubbleSort.match_1 (fun x => Id (ForInStep (Array α)))
(compare (getElem! arr j) (getElem! arr (HAdd.hAdd j 1)))
(fun _ =>
let arr := arr.swapIfInBounds j (HAdd.hAdd j 1);
bind (pure PUnit.unit) fun x => pure (ForInStep.yield arr))
(fun _ => bind (pure Unit.unit) fun x => pure (ForInStep.yield arr)) fun _ =>
bind (pure Unit.unit) fun x => pure (ForInStep.yield arr))
fun r =>
let arr := r;
bind (pure PUnit.unit) fun x => pure (ForInStep.yield arr))
fun r =>
let arr := r;
arr).run
モナドで付け足したい効果が特にない場合であってもIdモナドを使えばいつでもこの記法が使えます。
――――――まあこれは茶番だ
甘えるな
さっきの説明は「Leanは純粋関数型言語だけどかなり手続き的に書ける」ってことしか伝わってこないし、Leanのメインの強みである境界チェックもできてないし[2]。
これはLeanでのプログラミング初心者に対して「構えることないよ！」ってことを伝えたかったってわけなんですが、これだけじゃ物足りないですよね^^
というわけでね、さっきの関数をほぼそのまま末尾再帰で書き直します。
さっきのは茶番なので軽く説明をすっ飛ばしましたがここからは一つ一つ解説します。冗長かも。
まずシグネチャを考えます。型α[3]は比較できて、そのα型の要素の配列を受け取り、ソートした配列を返すので、こう
def bubbleSort [Ord α] (arr : Array α) : Array α := _
Array αは固定長配列というよりかはRustのVec<T>のようなもので大きさは動的に変化します[4]
次に外側のループを回すので、こう
def bubbleSort [Ord α] (arr : Array α) : Array α :=
let rec loop₁ [Ord α] (arr : Array α) (i : Nat) : Array α := _
loop₁ arr 0
外側のループは、iを増やしながら内側のループを回すので、こう
def bubbleSort [Ord α] (arr : Array α) : Array α :=
let rec loop₁ [Ord α] (arr : Array α) (i : Nat) : Array α :=
let rec loop₂ [Ord α] (arr : Array α) (i : Nat) (j : Nat) : Array α := _
if i < arr.size then
loop₁ (loop₂ arr i 0) (i + 1)
else
arr
loop₁ arr 0
内側のループを書いて、こう
def bubbleSort [Ord α] (arr : Array α) : Array α :=
let rec loop₁ [Ord α] (arr : Array α) (i : Nat) : Array α :=
let rec loop₂ [Ord α] (arr : Array α) (i : Nat) (j : Nat) : Array α :=
if j < arr.size - 1 - i then
match Ord.compare arr[j] arr[j + 1] with
|.gt => loop₂ (arr.swap j (j + 1)) i (j + 1)
|.lt |.eq => loop₂ arr i (j + 1)
else
arr
if i < arr.size then
loop₁ (loop₂ arr i 0) (i + 1)
else
arr
loop₁ arr 0
これで完成！……って言いたいじゃないですか。ここからが本番だ
この時点で4箇所エラーが出てます
一旦loop₁にあるエラーは無視してindexアクセスとarr.swapのエラーを気にします。
indexが範囲内にあることを証明する
Infoviewに表示されているエラーはこちら
failed to prove index is valid, possible solutions:
- Use `have`-expressions to prove the index is valid
- Use `a[i]!` notation instead, runtime check is performed, and 'Panic' error message is produced if index is not valid
- Use `a[i]?` notation instead, result is an `Option` type
- Use `a[i]'h` notation instead, where `h` is a proof that index is valid
α : Type ?u.19884
inst✝² : Ord α
arr✝¹ : Array α
inst✝¹ : Ord α
arr✝ : Array α
i✝ : Nat
inst✝ : Ord α
arr : Array α
i j : Nat
⊢ j < arr.size
failed to prove index is valid, possible solutions:
......(中略)
⊢ j + 1 < arr.size
これらのエラーが言ってる通り、配列への普通のindexアクセスにはindexが配列の範囲内であることの証明が必要になります。
エラーにも書いてありますがarr[j]!と書けば範囲外の時にパニックさせたり[5]arr[j]?と書けばOption αとして取り出したりすることもできますが、ここは証明で行きましょう！Leanの強みの見せどころです！
まずなぜjとj + 1が範囲内にあると確信できるのかと言えば、ifの条件j < arr.size - 1 - iを通ったからですね。
じゃあこいつをそのまま証明として取れればいいんだけどな～ってことなんですが、取れます。
if h_index : j < arr.size - 1 - i then
このように書けばh_indexという名前でj < arr.size - 1 - iの証明が取れます。
さらにさらに、Leanはめちゃくちゃ賢い[6]のでこの証明があるだけでjもj + 1も配列の範囲内だと認めてくれちゃいます！
arr.swapも同じ問題なのでこっちのエラーも解決してくれます
なので"証明"といってもLeanの賢さによって解決されちゃうんですね
現状のエラー状況はこうなります
loop₁が停止することを証明する
さてloop₁のエラーはこうなっています
fail to show termination for
bubbleSort.loop₁
with errors
failed to infer structural recursion:
Not considering parameter α of bubbleSort.loop₁:
it is unchanged in the recursive calls
Not considering parameter #2 of bubbleSort.loop₁:
it is unchanged in the recursive calls
Cannot use parameter arr:
the type Array α does not have a `.brecOn` recursor
Cannot use parameter i:
failed to eliminate recursive application
bubbleSort.loop₁ (bubbleSort.loop₁.loop₂ arr i 0) (i + 1)
Could not find a decreasing measure.
The arguments relate at each recursive call as follows:
(<, ≤, =: relation proved, ? all proofs failed, _: no proof attempted)
arr i #1
1) 103:6-35 ? ? ?
#1: arr.size - i
Please use `termination_by` to specify a decreasing measure.
Leanでは(partial defでもunsafe defでもなく)defで定義された関数は関数が停止することを保証しなければなりません。[7]このエラーは「loop₁が停止することを証明できなかった」と言っているのでこちら側で停止することを証明する必要があります。
停止することの証明にはtermination_byを使います。このtermination_byに「再帰することで減少するもの」を指定してあげればよいです。
再帰がいつ止まるかと言えばi < arr.sizeの条件に通らなかった場合なので、arr.size - iが0に向かって減少する関係と言えます。
実際Leanも「arr.size - iかなー?」って言って諦めてます
Could not find a decreasing measure. The arguments relate at each recursive call as follows: (<, ≤, =: relation proved, ? all proofs failed, _: no proof attempted) arr i #1 1) 11:6-35 ? ? ? #1: arr.size - i
我々もtermination_by arr.size - iと指示しましょう
def bubbleSort [Ord α] (arr : Array α) : Array α :=
let rec loop₁ [Ord α] (arr : Array α) (i : Nat) : Array α :=
let rec loop₂ [Ord α] (arr : Array α) (i : Nat) (j : Nat) : Array α :=
if h_index : j < arr.size - 1 - i then
match Ord.compare arr[j] arr[j + 1] with
|.gt => loop₂ (arr.swap j (j + 1)) i (j + 1)
|.lt |.eq => loop₂ arr i (j + 1)
else
arr
if i < arr.size then
loop₁ (loop₂ arr i 0) (i + 1)
else
arr
termination_by arr.size - i
loop₁ arr 0
するとエラー内容が変わります
failed to prove termination, possible solutions:
- Use `have`-expressions to prove the remaining goals
- Use `termination_by` to specify a different well-founded relation
- Use `decreasing_by` to specify your own tactic for discharging this kind of goal
α : Type u_1
inst✝ : Ord α
arr : Array α
i : Nat
h✝ : i < arr.size
⊢ (bubbleSort.loop₁.loop₂ arr i 0).size - (i + 1) < arr.size - i
「(bubbleSort.loop₁.loop₂ arr i 0).size - (i + 1) < arr.size - iの証明をしなさいよ」と言われていますね。Leanはこの証明を諦めたわけです。
これの証明にはdecreasing_byを使います。
さてarr.size - (i + 1) < arr.size - iなのは当然なのですが、今回示さなければならないのは(bubbleSort.loop₁.loop₂ arr i 0).size - (i + 1) < arr.size - iです。loop₂がarrの大きさを変えることは無いからarr.sizeに書き換えたいんだけどなぁ……
とここでrwタクティクが使えます。loop₂によってarrの大きさが変わらないこと((bubbleSort.loop₁.loop₂ arr i 0).size = arr.size)を示せば、このrwタクティクによってゴールをarr.size - (i + 1) < arr.size - iに書き換えて簡単に証明できます。
いったんここまででこういう下書きになります
def bubbleSort [Ord α] (arr : Array α) : Array α :=
-- ......(中略)
termination_by arr.size - i
decreasing_by
have loop₂_size_eq : (bubbleSort.loop₁.loop₂ arr i 0).size = arr.size := by sorry
rw[loop₂_size_eq]
sorry
loop₁ arr 0
haveはletとほぼ同じです。使い分けはあんまり考えてなく、証明だったらとりあえずhave、値だったらとりあえずletにしてます。
んーさきにrwより下のsorryを無くしましょう。
arr.size - (i + 1) < arr.size - iを証明する
この時点でのゴールと持っている仮定[8]は以下のとおりです
α : Type u_1
inst✝ : Ord α
arr : Array α
i : Nat
h✝ : i < arr.size
loop₂_size_eq : (bubbleSort.loop₁.loop₂ arr i 0).size = arr.size
⊢ arr.size - (i + 1) < arr.size - i
「いや簡単に証明できそうだけど何の定理がすでに証明されていて使えるのか知らない……！さすがにn - (m + 1) < n - mくらいならあるんじゃないか……？！」ってなりますよね。そんなときに使えるのがapply?タクティクです。apply?タクティクは証明のために何の定理が使えるのかを探し出してくれます。使ってみましょう
decreasing_by
have loop₂_size_eq : (bubbleSort.loop₁.loop₂ arr i 0).size = arr.size := by sorry
rw[loop₂_size_eq]
apply?
loop₁ arr 0
するとInfoviewにこのような表示が出ます
Try this: exact Nat.sub_succ_lt_self arr.size i h✝
Nat.sub_succ_lt_self (a i : Nat) (h : i < a) : a - (i + 1) < a - iという定理が使えるようですね。しかもapplyではなくexactで行けるようです。ありがたく使わせていただきましょう
decreasing_by
have loop₂_size_eq : (bubbleSort.loop₁.loop₂ arr i 0).size = arr.size := by sorry
rw[loop₂_size_eq]
exact Nat.sub_succ_lt_self arr.size i h✝
▼ Basic.lean:18:43
expected line break or token
▼ Basic.lean:18:42
unknown identifier 'h'
え？( `-´ #)せっかく使ったのになめとんのか
このhとやらはh✝ : i < arr.sizeのhですね。Infoview上で変数名に✝が付いたものはアクセス不能になってしまったものです。rename_iタクティクを使えば名前を付けて復帰できます。[9]
decreasing_by
have loop₂_size_eq : (bubbleSort.loop₁.loop₂ arr i 0).size = arr.size := by sorry
rw[loop₂_size_eq]
rename_i h
exact Nat.sub_succ_lt_self arr.size i h
これでrw以後は解決しました。あとは(bubbleSort.loop₁.loop₂ arr i 0).size = arr.sizeを証明すればOKです。
ただこっからが大変です。気合い入れていきましょう。
この先注意！(開くとネタバレ注意)
loop₂が配列の大きさを変えないことを証明する
まずとりあえずloop₂を定義に展開しましょう。unfoldタクティク[10]を使います
decreasing_by
have loop₂_size_eq : (bubbleSort.loop₁.loop₂ arr i 0).size = arr.size := by
unfold bubbleSort.loop₁.loop₂
rw[loop₂_size_eq]
rename_i h
exact Nat.sub_succ_lt_self arr.size i h
ゴールはこうなります
⊢ (if h_index : 0 < arr.size - 1 - i then
match compare arr[0] arr[0 + 1] with
| Ordering.gt => bubbleSort.loop₁.loop₂ (arr.swap 0 (0 + 1) ⋯ ⋯) i (0 + 1)
| Ordering.lt => bubbleSort.loop₁.loop₂ arr i (0 + 1)
| Ordering.eq => bubbleSort.loop₁.loop₂ arr i (0 + 1)
else arr).size =
arr.size
ifが邪魔ですね。ifのとおり条件分岐をしたい場合はsplitタクティクを使います。
decreasing_by
have loop₂_size_eq : (bubbleSort.loop₁.loop₂ arr i 0).size = arr.size := by
unfold bubbleSort.loop₁.loop₂
split
case isTrue hlt => sorry
case isFalse hnlt => sorry
rw[loop₂_size_eq]
rename_i h
exact Nat.sub_succ_lt_self arr.size i h
case isTrueとcase isFalseでhlt : j < arr.size - 1 - iとhnlt : ¬j < arr.size - 1 - iがそれぞれ取れます。
case isTrueのゴールはこれ
⊢ (match compare arr[0] arr[0 + 1] with
| Ordering.gt => bubbleSort.loop₁.loop₂ (arr.swap 0 (0 + 1) ⋯ ⋯) i (0 + 1)
| Ordering.lt => bubbleSort.loop₁.loop₂ arr i (0 + 1)
| Ordering.eq => bubbleSort.loop₁.loop₂ arr i (0 + 1)).size =
arr.size
case isFalseのゴールはこれ
⊢ arr.size = arr.size
case isFalseのゴールは簡単ですね。rflを使って一発です
case isFalse => rfl
case isTrueが問題ですね。Ordering.gtの場合とそれ以外とで挙動が違います。
というわけでもう一回split
case isTrue =>
split
case h_1 => sorry
case h_2 => sorry
case h_3 => sorry
case h_1のゴールを見てみると……
⊢ (bubbleSort.loop₁.loop₂ (arr.swap 0 (0 + 1) ⋯ ⋯) i (0 + 1)).size = arr.size
うーん……なんか振り出しに戻った感じがする……
またunfoldする……?いやいや、帰納法を使いましょう。
振り出しに戻ったのは再帰しているからで、再帰しているなら帰納法を使って証明するものです。inductionタクティクを使った方法で証明をやり直しましょう。
loop₂が配列の大きさを変えないことを証明する₂
……いやしかし！loop₂は再帰のたびにiは変わんないしjは増えていきます。つまり引数の中に減るものがないので単純にinductionを使うことが出来ません。induction iでもinduction jでもないんです。
じゃあなんなのか。そもそもloop₂はどうやって停止する再帰になっているかを考えましょう。
loop₂はj < arr.size - 1 - iを通らなかった場合に止まる再帰でありarr.size - 1 - i - jが減少するわけです。だから
have loop₂_size_eq : (bubbleSort.loop₁.loop₂ arr i 0).size = arr.size := by
induction (arr.size - i - 1 - j)
と書きたいんですが、「jって何？」とコンパイラに言われてしまいます。仕方ないので(j : Nat)として引数にしときますか。でもこれじゃjがなんのためにあるのか分かんないので、jの役割からしてゴールの0をjに書き換えておきましょう
have loop₂_size_eq (j : Nat) : (bubbleSort.loop₁.loop₂ arr i j).size = arr.size := by
induction (arr.size - i - 1 - j)
でこうなるんですが、残念ながらこう書いたところで都合よくarr.size - 1 - i - j = 0やarr.size - 1 - i - j = n + 1のような仮定をもらうことができません！
じゃあどうすればこの仮定がもらえるのか……というと、generalizeタクティクを使えばいけます
have loop₂_size_eq (j : Nat) : (bubbleSort.loop₁.loop₂ arr i j).size = arr.size := by
generalize hk : arr.size - i - 1 - j = k
induction k
このように書けばhkという名前でarr.size - 1 - i - j = 0やarr.size - 1 - i - j = n + 1が仮定として使えるようになります。
現状こうなります
have loop₂_size_eq (j : Nat) : (bubbleSort.loop₁.loop₂ arr i j).size = arr.size := by
generalize hk : arr.size - i - 1 - j = k
induction k <;> unfold bubbleSort.loop₁.loop₂
case zero => sorry
case succ n ih => sorry
<;>を使ってinductionによって生まれる2つのゴールの両方にunfoldをあてています。どちらもunfoldすることには変わりないので。
まずcase zeroから
case zero =>
split
case isTrue hlt => sorry
case isFalse hnlt => rfl
case isFalseはさっきと同じなのでパパっとrflしときましょう。
case isTrueなんですが、仮定に
hk : arr.size - 1 - i - j = 0
hlt : j < arr.size - 1 - i
の二つがあります。arr.size - 1 - i - j = 0なのにj < arr.size - 1 - iなのはおかしな話です。矛盾を示しましょう。
ただ単にcontradictionタクティクを使おうとしても何かしらの真逆の仮定は持ち合わせていないので失敗しちゃいます。arr.size - 1 - i - j ≠ 0を作ってからcontradictionしましょう。
case isTrue hlt =>
have h_ne_z : arr.size - 1 - i - j ≠ 0 := by sorry
contradiction
さてh_ne_zをどうするかなんですが、まあ分かんなかったらとりあえずapply?しとけばいいんですよ
case isTrue hlt =>
have h_ne_z : arr.size - 1 - i - j ≠ 0 := by apply?
contradiction
Try this: exact Nat.sub_ne_zero_iff_lt.mpr hlt
定理Nat.sub_ne_zero_iff_lt {n m : Nat} : n - m ≠ 0 ↔ m < nありますね。使います
case isTrue hlt =>
have h_ne_z : arr.size - 1 - i - j ≠ 0 := by exact Nat.sub_ne_zero_iff_lt.mpr hlt
contradiction
これでcase isTrueの証明が完了したのでcase zeroは証明完了です！うまくいっていますね
case zero =>
split
case isTrue hlt =>
have h_ne_z : arr.size - 1 - i - j ≠ 0 := by exact Nat.sub_ne_zero_iff_lt.mpr hlt
contradiction
case isFalse hnlt => rfl
残るはcase succですね
case succ n ih =>
split
case isTrue hlt => sorry
case isFalse hnlt => rfl
case isFalseは一応hk : arr'.size - 1 - i - j = n + 1でhnlt : ¬j < arr'.size - 1 - iとなっていてこれは矛盾しているのですが、rflって言った方が簡単なのでrflって言ってます
今回のcase isTrueは別に持っている仮定に矛盾がないので前回と同じようにsplit
case isTrue hlt =>
split
case h_1 => sorry
case h_2 => sorry
case h_3 => sorry
問題のcase h_1は……
⊢ (bubbleSort.loop₁.loop₂ (arr.swap j (j + 1) ⋯ ⋯) i (j + 1)).size = arr.size
ふむ。まあまあまあ今回は帰納法でやってるんで帰納ケースの仮定が――――――
ih : arr.size - 1 - i - j = n → (bubbleSort.loop₁.loop₂ arr i j).size = arr.size
hk : arr.size - 1 - i - j = n + 1
……使えない！！！！ 使えないんだが！？
まずihを使うのに必要な前提も満たせないしihの結論が(arr.swap j (j + 1) ⋯ ⋯)じゃなくてarrに対してしか使えない！
困った……一体どうすれば…………
うーーーーーーーーーーーーーーーーーーーーーーーーーーん
はい。
ネタバレ注意！のところに書いたとおり問題なのはゴールが具体的すぎることです。
出てくる変数をもう少し一般化して帰納法の仮定として使えるようにしておきましょう。
でも特に当然だけど大事なのは、再帰によって次に引数として渡される配列は Array.swapによって変化している可能性がある ということです。これが原因でさっきは失敗していたわけです。よって左辺((bubbleSort.loop₁.loop₂ arr i j).size)のarrと右辺(arr.size)のarrは別物として扱わなければなりません。ここからは左辺の配列をarr'としておきましょう。
ただし、引数として渡されるarr'の大きさともともとのarrの大きさが違うことはないということ抜きには証明できません。
よって新しく考える定理はこうなります:「任意のarr'.size = arr.sizeなarr', arrと自然数i,jについて、(bubbleSort.loop₁.loop₂ arr' i j).size = arr.size」
というわけで書き直したゴールはこうなります
have loop₂_size_eq (arr' arr : Array α) (i j : Nat) (h_size : arr'.size = arr.size) :
(bubbleSort.loop₁.loop₂ arr' i j).size = arr.size := by sorry
また証明やり直しです(^-^)/
loop₂が配列の大きさを変えないことを証明する₃
ただちょっと待って！このままでは帰納ケースで得られる仮定がih : arr'.size - 1 - i - j = n → (bubbleSort.loop₁.loop₂ arr' i j).size = arr.sizeであり、さっきから躓いているcase h_1のときの
⊢ (bubbleSort.loop₁.loop₂ (arr'.swap j (j + 1) ⋯ ⋯) i (j + 1)).size = arr.size
というゴールはarr'は(arr'.swap j (j + 1) ⋯ ⋯)ですしjはj + 1になってるので仮定を使って対応できません。
これに対応するため、inductionにはgeneralizing構文を使ってもう少し強力な仮定にします。
とりあえずarr'とiとjを、generalizingを使って一般化しておきましょう[11]
have loop₂_size_eq (arr' arr : Array α) (i j : Nat) (h_size : arr'.size = arr.size) :
(bubbleSort.loop₁.loop₂ arr' i j).size = arr.size := by
generalize hk : arr'.size - 1 - i - j = k
induction k generalizing arr' i j <;> unfold bubbleSort.loop₁.loop₂
case zero => sorry
case succ n ih => sorry
これで帰納ケースで得られる仮定がih : ∀ (arr' : Array α) (i j : Nat), arr'.size = arr.size → arr'.size - 1 - i - j = n → (bubbleSort.loop₁.loop₂ arr' i j).size = arr.sizeになってくれました！
またやり直しか…はあ……と思ってるかもしれませんが安心してください！今までやってきた証明を多少変えるだけです
まずcase zeroですが、case isFalseの際のゴールがarr'.size = arr.sizeと少し変わっています。仮定h_sizeを持っているのでexactしましょう
case zero =>
split
case isTrue hlt =>
have h_ne_z : arr'.size - 1 - i - j ≠ 0 := by exact Nat.sub_ne_zero_iff_lt.mpr hlt
contradiction
case isFalse hnlt => exact h_size
さてcase succ
case succ n ih =>
split
case isTrue hlt => sorry
case isFalse hnlt => sorry
case isFalseはさっきrflで解決したようにexact h_sizeでも解決できますが、一応矛盾してるしやっぱり矛盾を示しません…?
定理Nat.lt_of_sub_eq_succ {m n l : Nat} (h : m - n = l.succ) : n < mもあるので、簡単です
case isFalse hnlt =>
have : j < arr'.size - 1 - i := by exact Nat.lt_of_sub_eq_succ hk
contradiction
問題はcase isTrueです。とりあえずsplit
case isTrue hlt =>
split
case h_1 => sorry
case h_2 => sorry
case h_3 => sorry
さて……問題のcase h_1
⊢ (bubbleSort.loop₁.loop₂ (arr'.swap j (j + 1) ⋯ ⋯) i (j + 1)).size = arr.size
あの時とは違って、今の我々には仮定ih : ∀ (arr' : Array α) (i j : Nat), arr'.size = arr.size → arr'.size - 1 - i - j = n → (bubbleSort.loop₁.loop₂ arr' i j).size = arr.sizeを持っています！これを使って解決しましょう！
今の仮定ihは"任意の"arr'とiとjについて言える話なので、これらは何にするか自分で決められるわけです。今回の場合はarr'は(arr'.swap j (j + 1))、iはi、jは(j + 1)になります。
ただ少し面倒くさくなっている所があって、その自分で決めたarr'、i、j(今回の場合arr'.swap j (j + 1)、i、(j + 1))がarr'.size = arr.sizeやarr'.size - 1 - i - j = nを満たすことも証明しとかなければいけません。
ihの結論と今回のゴールが一致しているのでapply ihができます
case h_1 =>
apply ih
case h_size => sorry
case hk => sorry
case h_sizeのゴール
⊢ (arr'.swap j (j + 1) ⋯ ⋯).size = arr.size
とcase hkのゴール
⊢ (arr'.swap j (j + 1) ⋯ ⋯).size - 1 - i - (j + 1) = n
が現れました。めんどっち～
ただどっちも(arr'.swap j (j + 1) ⋯ ⋯).sizeが出ているけどこれってarr'.sizeと変わりませんよね。Array.size_swapという定理もあるので、先に持っておきましょう
case h_1 =>
apply ih
have h_size_swap : (arr'.swap j (j + 1)).size = arr'.size := arr'.size_swap j (j + 1)
case h_size => sorry
case hk => sorry
case h_sizeの方はEq.trans(推移律)で証明できます。case hkの方は一旦rwしておきましょう
case h_1 =>
have h_size_swap : (arr'.swap j (j + 1)).size = arr'.size := arr'.size_swap j (j + 1)
apply ih
case h_size => exact h_size_swap.trans h_size
case hk =>
rw[h_size_swap]
さてcase hkのゴールは⊢ arr'.size - 1 - i - (j + 1) = nとなりましたが、ここで最強タクティクomegaが使えます！omegaは自然数や整数の計算なら結構なんでもありに自動で証明してくれるタクティクです。今回はhk : arr'.size - 1 - i - j = n + 1があるのでこれくらいの証明ならomegaぶっぱで解決します
case h_1 =>
have h_size_swap : (arr'.swap j (j + 1)).size = arr'.size := arr'.size_swap j (j + 1)
apply ih
case h_size => exact h_size_swap.trans h_size
case hk =>
rw[h_size_swap]
omega
……いやーせっかくだし手で証明しません？^^;
calcを使って=で繋いでいきます。
まず証明したい等式の左辺から
case hk =>
rw[h_size_swap]
calc arr'.size - 1 - i - (j + 1)
hk : arr'.size - 1 - i - j = n + 1があるのでそれにあわせて変形し、
case hk =>
rw[h_size_swap]
calc arr'.size - 1 - i - (j + 1)
_ = (arr'.size - 1 - i - j) - 1 := rfl
Nat.sub_eq_of_eq_add {a b c : Nat} (h : a = c + b) : a - b = cがあるのでこれで証明完了です
case hk =>
rw[h_size_swap]
calc arr'.size - 1 - i - (j + 1)
_ = (arr'.size - 1 - i - j) - 1 := rfl
_ = n := Nat.sub_eq_of_eq_add hk
これでようやくcase h_1を乗り越えました！
あとはcase h_2とcase h_3です
ゴールはどちらも
⊢ (bubbleSort.loop₁.loop₂ arr' i (j + 1)).size = arr.size
なんですが、結局同じようにarr'.size - 1 - i - (j + 1) = nの証明が必要になりそうですね。
といわけでさっきcalcで証明したのをh_eq_nとしてsplitの前にとっておきましょう。
これさえとれればあとは簡単なので説明も省きます
case isTrue hlt =>
have h_eq_n : arr'.size - 1 - i - (j + 1) = n := by
calc arr'.size - 1 - i - (j + 1)
_ = (arr'.size - 1 - i - j) - 1 := rfl
_ = n := Nat.sub_eq_of_eq_add hk
split
case h_1 =>
have h_size_swap : (arr'.swap j (j + 1)).size = arr'.size := arr'.size_swap j (j + 1)
apply ih
case h_size => exact h_size_swap.trans h_size
case hk =>
rw[h_size_swap]
exact h_eq_n
case h_2 =>
apply ih
case h_size => exact h_size
case hk => exact h_eq_n
case h_3 =>
apply ih
case h_size => exact h_size
case hk => exact h_eq_n
これでcase isTrueを乗り越えたのでようやくloop₂_size_eqの証明が完了しました……！
これでdecreasing_byの証明が……！？まだ終わりませ～ん^^
loop₂_size_eqのシグネチャがだいぶ変わったので何のarr'とarrとiとjでrwしたいのか指定しなければいけません。
もともと(bubbleSort.loop₁.loop₂ arr i 0).size = arr.sizeを証明したかったわけなので、引数arr',arrにはarrを、引数iにはiを、引数jには0を、そしてh_sizeにはrflを指定します。
decreasing_by
have loop₂_size_eq (arr' arr : Array α) (i j : Nat) (h_size : arr'.size = arr.size) :
(bubbleSort.loop₁.loop₂ arr' i j).size = arr.size := /- 省略 -/
rw[loop₂_size_eq arr arr i 0 rfl]
rename_i h
exact Nat.sub_succ_lt_self arr.size i h
これで本当にdecreasing_byの証明が完了しました！
そしてこれにより……！bubbleSortの定義が……！完了しました！！！！！
まとめ・コード全体を見る
では完成したバブルソートのコード全体を見てみましょう
def bubbleSort [Ord α] (arr : Array α) : Array α :=
let rec loop₁ [Ord α] (arr : Array α) (i : Nat) : Array α :=
let rec loop₂ [Ord α] (arr : Array α) (i : Nat) (j : Nat) : Array α :=
if h_index : j < arr.size - 1 - i then
match Ord.compare arr[j] arr[j + 1] with
|.gt => loop₂ (arr.swap j (j + 1)) i (j + 1)
|.lt |.eq => loop₂ arr i (j + 1)
else
arr
if i < arr.size then
loop₁ (loop₂ arr i 0) (i + 1)
else
arr
termination_by arr.size - i
decreasing_by
have loop₂_size_eq (arr' arr : Array α) (i j : Nat) (h_size : arr'.size = arr.size) :
(bubbleSort.loop₁.loop₂ arr' i j).size = arr.size := by
generalize hk : arr'.size - 1 - i - j = k
induction k generalizing arr' i j <;> unfold bubbleSort.loop₁.loop₂
case zero =>
split
case isTrue hlt =>
have h_ne_z : arr'.size - 1 - i - j ≠ 0 := by exact Nat.sub_ne_zero_iff_lt.mpr hlt
contradiction
case isFalse hnlt => exact h_size
case succ n ih =>
split
case isTrue hlt =>
have h_eq_n : arr'.size - 1 - i - (j + 1) = n := by
calc arr'.size - 1 - i - (j + 1)
_ = (arr'.size - 1 - i - j) - 1 := rfl
_ = n := Nat.sub_eq_of_eq_add hk
split
case h_1 =>
have h_size_swap : (arr'.swap j (j + 1)).size = arr'.size := arr'.size_swap j (j + 1)
apply ih
case h_size => exact h_size_swap.trans h_size
case hk =>
rw[h_size_swap]
exact h_eq_n
case h_2 =>
apply ih
case h_size => exact h_size
case hk => exact h_eq_n
case h_3 =>
apply ih
case h_size => exact h_size
case hk => exact h_eq_n
case isFalse hnlt =>
have : j < arr'.size - 1 - i := by exact Nat.lt_of_sub_eq_succ hk
contradiction
rw[loop₂_size_eq arr arr i 0 rfl]
rename_i h
exact Nat.sub_succ_lt_self arr.size i h
loop₁ arr 0
全体で55行！バブルソート1つで55行！頑張りましたね！まあ2/3ほど証明に使ってますが
ただ見誤らないで！55行もするのは甘えずに証明付きで書くことを頑張ったからであって、「Leanだとバブルソートに55行も書かされる」のではありません！
別に甘えてもいいんです。証明がだるかったらdefにpartial付けたっていいし、何ならforで書いたっていいんです。arr[i]!だって使っていいんです。(✝甘えるな✝とか言ってたら流行らせられない)
他の大体の言語だと実行時エラーだったり未定義動作だったりOptionを返したりするindexアクセスを「必ずindexが範囲内にある」って保証したりとか、他の大体の言語だと無限ループする関数と必ず停止する関数の区別がつかないのを「この関数は必ず停止する」って言いきったりとか[12]、頑張ればLeanでそういうことができるんです。だからLeanが好きなんです。[13]
それ以外にもLeanの好きなところはいろいろあるんですけども(メタプログラミングとそれに伴う書き方の自由さとかInfoviewとか)
とりあえずこれでバブルソートの解説は以上です！
最後に
今関数型言語を学び始めるならLeanがオススメ！日本語のガイド本もいろいろ揃ってます！
ちなみに
余談です
[Inhabited α]と[Ord α]って何?
instance implicit と呼ばれる、Leanがインスタンス探索の仕事をする引数です(Theorem Proving in Lean 4の日本語訳では"インスタンス暗黙引数"、Functional Programming in Leanの日本語訳では"暗黙のインスタンス"と呼ばれる)
役割は型クラス制約と同じです
[Ord α]は見てきた通りOrd.compareができるようにするための型クラスです。
[Inhabited α]はただ「デフォルト値がある」ことを示すだけの型クラスなんですが、なぜarr[i]!の時には必要になるかというと「arr[i]!が必ずαを返す」という取り決めの論理的整合性を保つためです。範囲外エラーの際は、実際の挙動はエラーメッセージが出ることですが、コードの見かけ上はdefaultが返されます
ifで書かないの?
普通if arr[j] > arr[j + 1] thenって書くところをなんでわざわざOrd.compare arr[j] arr[j + 1]にしてんの？って話なんですが、ifで書くと必要な型クラス制約がちょっと変わってきます。まずa < bの書き方を許すために[LT α]が必要です。そしてifの条件部分は命題(Prop)を書くのですがこの命題が決定可能である必要があります。今回の場合だと「任意のαの値a,bについて、a > bが決定可能」が要求されるので[∀(a b : α), Decidable (a > b)]が必要になります。
具体的なコード
def bubbleSortif [LT α] [∀(a b : α), Decidable (a > b)] (arr : Array α) : Array α :=
let rec loop₁ [LT α] [∀(a b : α), Decidable (a > b)] (arr : Array α) (i : Nat) : Array α :=
let rec loop₂ [LT α] [∀(a b : α), Decidable (a > b)] (arr : Array α) (i : Nat) (j : Nat) : Array α :=
if h_index : j < arr.size - 1 - i then
if arr[j] > arr[j + 1] then
loop₂ (arr.swap j (j + 1)) i (j + 1)
else
loop₂ arr i (j + 1)
else
arr
if i < arr.size then
loop₁ (loop₂ arr i 0) (i + 1)
else
arr
termination_by arr.size - i
decreasing_by
/- 省略 (証明できます！) -/
loop₁ arr 0
結局indexアクセスとarr.swapの証明ってどうなってるの?
get_elem_tacticが自動で使われています。まず欲しいゴールと一致する仮定があるかどうか探してから、そのあとtirivialやsimpとかを試して、それでも失敗した場合はomegaをぶちかましてます
loop₂はなんで停止することの証明が要らなかったの?
decreasing_tacticが自動で使われています。decreasing_tacticの方もいろいろできないか試しますが結局最後にomegaをかまします
どうやってそうなってることを知ったの?
Leanにはset_optionというコマンドがあり、この中のtrace.Elab.stepやtrace.Elab.definition.wfをtrueにすると確認できます。trace系オプションはLeanがどうエラボレーションするのか知るのに重宝します
for版でindexが範囲内にあることを証明しようとした
一応for版でも以下のように書けば証明項が取れます
def bubbleSort [Inhabited α] [Ord α] (arr : Array α) : Array α := Id.run do
let mut arr := arr
for h₁ : i in [0:arr.size] do
for h₂ : j in [0:arr.size - 1 - i] do
match Ord.compare arr[j] arr[j + 1] with
|.gt => arr := arr.swap j (j + 1)
|.lt |.eq => pure ()
arr
これでh₁ : i ∈ col✝¹とh₂ : j ∈ col✝という2つの証明項が取れ、この証明からMembership.mem.upper {i : Nat} {r : Std.Range} (h : i ∈ r) : i < r.stopという定理が使えるのでいけそうに見えるのですが、厄介なことになっています。持っている仮定は
arr✝² : Array α
arr✝¹ : Array α := arr✝²
col✝¹ : Std.Range := { start := 0, stop := arr✝¹.size, step := 1 }
i : Nat
h₁ : i ∈ col✝¹
r✝¹ : Array α
arr✝ : Array α := r✝¹
col✝ : Std.Range := { start := 0, stop := arr✝.size - 1 - i, step := 1 }
j : Nat
h₂ : j ∈ col✝
r✝ : Array α
arr : Array α := r✝
となっており、forを経るごとにarrが別のものとして認識されてしまいます。特にarr✝².sizeとr✝¹.sizeが一致すること、r✝¹.sizeとr✝.sizeが一致することの証明がどう持てばいいかが分からなくて断念しています……助けてください
追記:for版でもindexが範囲内にあることを証明できます！
(追記:2024-12-22)
LEAN JA Discordサーバー(https://discord.gg/RnPdWctrSU)にてpandaman64さんに、この記事のコメントにてebi_chanさんにfor版でもindexが範囲内にあることの証明方法を教えていただきました！
def bubbleSort [Ord α] (arr : Array α) : Array α := Id.run do
let mut size := arr.size
let mut arr : { arr : Array α // arr.size = size } := ⟨arr, rfl⟩
for h₁ : i in [0:size] do
for h₂ : j in [0:size - 1 - i] do
have : j < size - 1 - i := h₂.upper
match Ord.compare arr.val[j] arr.val[j + 1] with
|.gt => arr := ⟨arr.val.swap j (j + 1), by rw[Array.size_swap, arr.property]⟩
|.lt |.eq => pure ()
arr.val
一旦arr.sizeをsizeとして取り、それをSubtypeでarrの中に情報を入れこんでおいて、forの中で使えるようにするようにした感じですね。あと他にforの範囲指定の部分がarr.sizeからsizeに変わっています
j < size - 1 - iの証明(前述したMembership.mem.upperで簡単に取れる)さえ取ってしまえばあとは境界チェックの証明はget_elem_tactic内のomegaが勝手に解決してくれます。境界チェックにはj < arr.val.sizeの証明が必要なはずですが、j < size - 1 - iを取るだけで解決されています。どうやらomegaはSubtypeの言明まで見てかましてくれるみたいですね。強すぎだろ
境界チェックの証明(←最初からそう言えばよかった…)ができたので、これで[Inhabited α]を付ける必要も無くなります！
ちなみにforの範囲をsizeじゃなくてarr.val.sizeとしても多少の手間が加わるだけで境界チェックの証明はできます。(これもebi_chanさんから指摘していただいて気づきました)
forの範囲をsizeからarr.val.sizeにした場合
def bubbleSort [Ord α] (arr : Array α) : Array α := Id.run do
let size := arr.size
let mut arr : { arr : Array α // arr.size = size } := ⟨arr, rfl⟩
for h₁ : i in [0:arr.val.size] do
for h₂ : j in [0:arr.val.size - 1 - i] do
have : j < size - 1 - i := by
rename_i col _
have h_jind := h₂.upper
dsimp[col] at h_jind
omega
match Ord.compare arr.val[j] arr.val[j + 1] with
|.gt => arr := ⟨arr.val.swap j (j + 1), by rw[Array.size_swap, arr.property]⟩
|.lt |.eq => pure ()
arr.val
なのでキーとなるのは「Subtypeにarrのsizeに関する情報を命題として入れこむ」ところにあります。
この方法を教えてもらった(チラ見だけした)とき、「ならば命題もmutにすれば(マクロ展開後は直積になるため)for内で使えるんじゃ…？」と思ったのですが、これは見当違いで、重要なのは「そのarrがarr.size = sizeであること」なんです。[14]
つまり自分が考えていたのは
def bubbleSort [Ord α] (arr : Array α) : Array α := Id.run do
let size := arr.size
let mut arr := arr
let mut size_prop : arr.size = size := rfl
なんですが、これじゃ意味無いんです。size_propは結局ついさっき1行前のarrの「arr.sizeがsizeと等しい」としか言えておらず、forの中の境界チェックの時は(一回断念したように)違うarrのsizeに対して証明を要求されて無様に撃沈します。
なのでこれはSubtypeとして、「値とその値の性質を表す命題」をペアにすることが必要なんです。このペアは"依存和型"(とか"依存直積型"とか"シグマ型"とか"依存ペア型"とか)と言われています。これはLeanで存在の命題を表すときのExistsと中身は同じで、違うのはそれが命題(Prop)か型(Sort (max 1 u))かくらいです。
この"依存和型"は依存型を代表する2つの型(依存積型と依存和型)の1つで、それを直に使っているわけです。
ここにもLeanの奥深さが出てて面白いですね！
小ネタ
VSCodeの拡張機能のError LensはLeanと相性抜群だと思います。
特に#evalや#checkは書いた行と同じところに結果が出力されるのですぐに確認できます
戯言
まだLeanのシンタックスハイライトが効かないのでStandardMLのシンタックスハイライトで無理に代用してます……
Prism.jsさんお願いします(https://github.com/PrismJS/prism/pull/3765)
と思ったけど、10ヶ月前から更新止まってる……？
Zenn上で投稿するためにMarkdownで記事書いているけどLeanはコード面だけじゃ伝わりにくいことが多いから個人サイトでverso使う方がいいってのは、ある ただ個人サイト持っていないからversoが使えるサイトが欲しいよ～
-
Leanがある程度分かってたり、全く知らなくてもこれまでの経験から読めたりするくらいの感じです ↩︎
-
四苦八苦した挙句諦めました…… ↩︎
-
LeanはコードにASCII文字だけでなくUnicode文字も多用します。簡単に入力できるようになっているのでそこまで不自然さも無く慣れます ↩︎
-
代償?として
[Inhabited α]が必要
forを使った関数の方はこっちを使ってた ↩︎ -
多分厳密には「Leanのエラボレータ」だと思うのですが、聞きなじみのない言葉でごちゃごちゃしちゃいそうなので「Lean」にしておいてます！ごめん ↩︎
-
なぜ停止することが必要なのかの詳細は、ここに書いてあります:https://lean-lang.org/blog/2024-1-11-recursive-definitions-in-lean/ ↩︎
-
「今持っているもの」の用語が分からないので「仮定」と呼んじゃってます…誰か正確な名前があれば教えてください ↩︎
-
別にプログラムを書いてる時点で
if h : i < arr.size thenと書けばrename_iは無しでもいけます ↩︎ -
dsimpタクティクはなぜか何も展開してくれませんでした…… ↩︎ -
ちなみに
arrもgeneralizingしてもいいですしiは別にgeneralizingしなくてもいいです。あと「使えない！」って騒いでた時も実はjだけはgeneralizingできます ↩︎ -
でも
partialはkokaのdivエフェクトみたいに伝播しないからミスリーディング味ある ↩︎ -
※他の依存型持ってる言語に触れたことが無いだけ ↩︎
-
伝わらなさそうな言い方しか思いつかなくてハゲ ↩︎
Discussion
for版はSubtypeを使ってArrayのsizeに関する情報を入れておくとうまくいきました。