Lean4でバブルソートを書く

この記事は証明支援系 Advent Calendar 2024 19日目の記事です

https://adventar.org/calendars/10209

Lean4は定理証明支援系かつ純粋関数型プログラミング言語なんですが、今のところ日本語記事は定理証明に焦点を当ててるものがわりかし体感多い気がします(←ゴミみたいな保険かけ)

でもやっぱり依存型を持つプログラミング言語としてのLeanがめちゃんこ好きで、プログラミング言語としても流行ってほしいな～って願望がめちゃくちゃあります。

なのでLeanでのプログラミングの勉強を始めてみたいって人たちとか、関数型プログラミング言語に興味ある人たちに、基本的なアルゴリズムであるバブルソートを通してLeanを知ってもらおうということでこれを書いてます。

対象読者は書かれたコードがなんとなくで読める方です。^[1]

ただのバブルソートといえどLeanの特徴がいろいろ出て奥深いんですよ！覚悟しておけ

2024/11/24にArray.swapのシグネチャを変更するコミットが入った( https://github.com/leanprover/lean4/pull/6194 )のでnightly(2024-12-12)版を使用しています

引用する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、果てには可変変数まで可能です。

https://s-taiga.github.io/fpil-ja/monad-transformers/do.html

これら手続き的な書き方は全て最終的に全て関数呼び出しの形に変換されます。

最終的な関数呼び出しの形

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です。

ただこっからが大変です。気合い入れていきましょう。

この先注意！(開くとネタバレ注意)

(bubbleSort.loop₁.loop₂ arr i 0).size = arr.sizeと設定しているゴールがそもそもよくないです！しかし試行錯誤の過程をそのまま写すためよくないゴールのまま進んでいきます

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がオススメ！日本語のガイド本もいろいろ揃ってます！

https://lean-ja.github.io/lean-by-example/

https://s-taiga.github.io/fpil-ja/

https://aconite-ac.github.io/theorem_proving_in_lean4_ja/

https://s-taiga.github.io/metaprogramming_in_lean4_ja/

https://s-taiga.github.io/MIL_ja/

https://s-taiga.github.io/reference-manual-ja/

ちなみに

余談です

[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の奥深さが出てて面白いですね！

追記₂:decreasing_byをもっと短く証明できます！

(追記:2024-12-24)ebi_chanさんにdecreasing_byのより短い証明についても教えていただきました！

def bubbleSort [Ord α] (arr : Array α) : Array α :=
  let rec loop₁ [Ord α] (arr : Array α) (i : Nat) : Array α :=
    let rec loop₂ [Ord α] (arr : Array α) (i 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
      let rec loop₂_size_eq (arr : Array α) (i j : Nat) : (bubbleSort.loop₁.loop₂ arr i j).size = arr.size := by
        unfold bubbleSort.loop₁.loop₂
        split
        case isTrue hlt =>
          split <;> rw[loop₂_size_eq]
          case h_1 => rw[Array.size_swap]
        case isFalse hnlt => rfl
      rw[loop₂_size_eq]
      rename_i h
      exact Nat.sub_succ_lt_self arr.size i h
  loop₁ arr 0

34行あったdecreasing_byがたった10行で収まっています。

目立つ違いとして、induction無しで証明が完了しています。

あと必要な引数が(arr : Array α) (i j : Nat)となっており、arr'も(h_size : arr'.size = arr.size)も必要なくなってます。

ただこれだと(kernel) declaration has metavariables 'bubbleSort.loop₁._unary'という謎のエラー(おそらくバグ^[15])が出てしまうので、loop₂とloop₂_size_eqを独立させておきましょう。

def loop₂ [Ord α] (arr : Array α) (i 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

theorem loop₂_size_eq [Ord α] (arr : Array α) (i j : Nat) : (loop₂ arr i j).size = arr.size := by
  unfold loop₂
  split
  case isTrue hlt =>
    split <;> rw[loop₂_size_eq]
    case h_1 => rw[Array.size_swap]
  case isFalse hnlt => rfl

def bubbleSort [Ord α] (arr : Array α) : Array α :=
  let rec loop₁ [Ord α] (arr : Array α) (i : Nat) : Array α :=
    if i < arr.size then
      loop₁ (loop₂ arr i 0) (i + 1)
    else
      arr
    termination_by arr.size - i
    decreasing_by
      rw[loop₂_size_eq]
      rename_i h
      exact Nat.sub_succ_lt_self arr.size i h
  loop₁ arr 0

一体何が起こってるんでしょうか。新しくなったloop₂_size_eqの中を追っていきましょう。

この状態の奴を、

⊢ (loop₂ arr i j).size = arr.size

unfold loop₂して、

⊢ (if h_index : j < arr.size - 1 - i then
      match compare arr[j] arr[j + 1] with
      | Ordering.gt => loop₂ (arr.swap j (j + 1) ⋯ ⋯) i (j + 1)
      | Ordering.lt => loop₂ arr i (j + 1)
      | Ordering.eq => loop₂ arr i (j + 1)
    else arr).size =
  arr.size

splitしたやつのisTrue側

⊢ (match compare arr[j] arr[j + 1] with
    | Ordering.gt => loop₂ (arr.swap j (j + 1) ⋯ ⋯) i (j + 1)
    | Ordering.lt => loop₂ arr i (j + 1)
    | Ordering.eq => loop₂ arr i (j + 1)).size =
  arr.size

を、
splitして<;>でrw[loop₂_size_eq]！

case h_1
(省略)
⊢ (arr.swap j (j + 1) ⋯ ⋯).size = arr.size

( ˙ㅿ˙ )え

まどう考えたってrw[loop₂_size_eq]が何かしてますね。loop₂_size_eqを再帰的に利用してます。

ちょっと<;>のおかげで一気にやりすぎなので、一旦ケース分けして考えましょう。

case isTrue hlt =>
  split
  case h_1 => rw[loop₂_size_eq]
  case h_2 => rw[loop₂_size_eq]
  case h_3 => rw[loop₂_size_eq]

でcase h_1について。
これが、

⊢ (loop₂ (arr.swap j (j + 1) ⋯ ⋯) i (j + 1)).size = arr.size

こうなる

⊢ (arr.swap j (j + 1) ⋯ ⋯).size = arr.size

つまり左辺をrwしている訳ですね。

だからあとはrw[Array.size_swap]するだけになる

case h_1 => rw[loop₂_size_eq, Array.size_swap]

これでうまく証明ができたということになります。

ただ疑問なのが、なぜ再帰的にrw[loop₂_size_eq]ができているのでしょう…？

いろいろ試してみたところ、どうやら再帰的にrwを用いることは証明中はとりあえず許されていて、後からその再帰がOKか判断しているみたいです。

なので一応これでもNo goalsとなるのですが、

theorem loop₂_size_eq_bad [Ord α] (arr : Array α) (i j : Nat) : (loop₂ arr i j).size = arr.size := by
  rw[loop₂_size_eq_bad]

その宣言に対してエラーが出ます。

fail to show termination for
  loop₂_size_eq_bad
with errors
failed to infer structural recursion:
Not considering parameter α of loop₂_size_eq_bad:
  it is unchanged in the recursive calls
...(省略)

well-founded recursion cannot be used, 'loop₂_size_eq_bad' does not take any (non-fixed) arguments

「変わってる変数が無いから整礎再帰が使えないよ」と言ってますね。

とはいえこれは関数の再帰的定義でも同じで、とりあえず再帰的に利用すること自体は関数でも証明でも許されていて、それが許される利用方法かはあとからチェックされます。

となると問題は「なぜ構造的再帰でもないrw[loop₂_size_eq]を使った証明が許されるのか？」ということになりますが、これはloop₂を定義したときと同じように整礎再帰していることがLean側で自動的に証明されているからです(set_option trace.Elab.definition.wf trueを置いてみると分かります)。

ここでもomegaがぶちかまされてます。最強すぎ

追記₃:decreasing_byをもっと短く証明できます！₂

(追記:2024-12-27)

Zulipにて"Functional induction"なるものを教えていただきました！

再帰している関数には.inductが自動で生えてきて、これがinductionに使えるようです。

詳しい説明は以下にあります

https://lean-lang.org/blog/2024-5-17-functional-induction/

そしてFunctional Inductionを使った結果がこちら

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 : Array α) (i j : Nat) : (bubbleSort.loop₁.loop₂ arr i j).size = arr.size := by
      induction arr, i, j using bubbleSort.loop₁.loop₂.induct
      <;> unfold bubbleSort.loop₁.loop₂ <;> simp[*]
    rw[loop₂_size_eq]
    rename_i h
    exact Nat.sub_succ_lt_self arr.size i h
  loop₁ arr 0

simp[*]が全部やりました。

このbubbleSort.loop₁.loop₂.inductは何をしたのかというと...

case case1
α : Type u_1
inst✝ : Ord α
arr✝ : Array α
i✝ j✝ : Nat
h✝ : j✝ < arr✝.size - 1 - i✝
x✝ : compare arr✝[j✝] arr✝[j✝ + 1] = Ordering.gt
ih1✝ : (bubbleSort.loop₁.loop₂ (arr✝.swap j✝ (j✝ + 1) ⋯ ⋯) i✝ (j✝ + 1)).size = (arr✝.swap j✝ (j✝ + 1) ⋯ ⋯).size
⊢ (bubbleSort.loop₁.loop₂ arr✝ i✝ j✝).size = arr✝.size

case case2
α : Type u_1
inst✝ : Ord α
arr✝ : Array α
i✝ j✝ : Nat
h✝ : j✝ < arr✝.size - 1 - i✝
x✝ : compare arr✝[j✝] arr✝[j✝ + 1] = Ordering.lt
ih1✝ : (bubbleSort.loop₁.loop₂ arr✝ i✝ (j✝ + 1)).size = arr✝.size
⊢ (bubbleSort.loop₁.loop₂ arr✝ i✝ j✝).size = arr✝.size

case case3
α : Type u_1
inst✝ : Ord α
arr✝ : Array α
i✝ j✝ : Nat
h✝ : j✝ < arr✝.size - 1 - i✝
x✝ : compare arr✝[j✝] arr✝[j✝ + 1] = Ordering.eq
ih1✝ : (bubbleSort.loop₁.loop₂ arr✝ i✝ (j✝ + 1)).size = arr✝.size
⊢ (bubbleSort.loop₁.loop₂ arr✝ i✝ j✝).size = arr✝.size

case case4
α : Type u_1
inst✝ : Ord α
arr✝ : Array α
i✝ j✝ : Nat
h✝ : ¬j✝ < arr✝.size - 1 - i✝
⊢ (bubbleSort.loop₁.loop₂ arr✝ i✝ j✝).size = arr✝.size

と発生する分岐全てについて仮定を網羅し、しかも必要としていた帰納ケースの仮定(ih1✝)までもらえる状態にしてくれます。だからあとはsimp[*]が勝手に、持っている仮定なり[simp]属性が付いた定理なりを使って全部自動で証明できたんですね。

どうやらこのやり方こそがLean4の(証明自動化としての)能力を最大限に発揮した書き方っぽいですね。

小ネタ

VSCodeの拡張機能のError LensはLeanと相性抜群だと思います。

特に#evalや#checkは書いた行と同じところに結果が出力されるのですぐに確認できます

戯言

まだLeanのシンタックスハイライトが効かないのでStandardMLのシンタックスハイライトで無理に代用してます……

Prism.jsさんお願いします(https://github.com/PrismJS/prism/pull/3765)
と思ったけど、10ヶ月前から更新止まってる……？

Zenn上で投稿するためにMarkdownで記事書いているけどLeanはコード面だけじゃ伝わりにくいことが多いから個人サイトでverso使う方がいいってのは、ある　ただ個人サイト持っていないからversoが使えるサイトが欲しいよ～

脚注

1. Leanがある程度分かってたり、全く知らなくてもこれまでの経験から読めたりするくらいの感じです

2. 四苦八苦した挙句諦めました……

3. LeanはコードにASCII文字だけでなくUnicode文字も多用します。簡単に入力できるようになっているのでそこまで不自然さも無く慣れます

4. Vectorはそれはそれで別であります

5. 代償?として[Inhabited α]が必要
   forを使った関数の方はこっちを使ってた

6. 多分厳密には「Leanのエラボレータ」だと思うのですが、聞きなじみのない言葉でごちゃごちゃしちゃいそうなので「Lean」にしておいてます！ごめん

7. なぜ停止することが必要なのかの詳細は、ここに書いてあります:https://lean-lang.org/blog/2024-1-11-recursive-definitions-in-lean/

8. 「今持っているもの」の用語が分からないので「仮定」と呼んじゃってます…誰か正確な名前があれば教えてください

9. 別にプログラムを書いてる時点でif h : i < arr.size thenと書けばrename_iは無しでもいけます

10. dsimpタクティクはなぜか何も展開してくれませんでした……

11. ちなみにarrもgeneralizingしてもいいですしiは別にgeneralizingしなくてもいいです。あと「使えない！」って騒いでた時も実はjだけはgeneralizingできます

12. でもpartialはkokaのdivエフェクトみたいに伝播しないからミスリーディング味ある

13. ※他の依存型持ってる言語に触れたことが無いだけ

14. 伝わらなさそうな言い方しか思いつかなくてハゲ

15. Zulipに書いたけどこれでいいのかな……