挿入ソートと配列の更新

挿入ソートはソートアルゴリズムとしては最悪計算時間の複雑性において最適ではありませんが、それでもいくつもの有用な性質を持ちます：

• 実装および理屈がシンプルで直観的であること
• in-placeアルゴリズムであり、実行時に追加の領域を必要としないこと
• 安定ソートである
• 入力がソート済みである場合は高速

特にin-placeアルゴリズムである点はLeanにおいてメモリ管理の方法から有用です。いくつかのケースでは、通常では配列のコピーの操作は更新に最適化されます。これは配列内の要素の交換も含みます。

JavaScriptやJVM、.NETを含むメモリを動的に管理するほとんどの言語とランタイムでは、ガベージコレクションの追跡を用います。メモリを再要求する必要がある場合、システムはいくつかの ルート （コールスタックやグローバル値など）から開始し、再帰的にポインタを追いかけることで到達できる値を決定します。到達できない値はすべて割り当て解除され、メモリが解放されます。

ガベージコレクションの追跡の代替手段として、Python・Swift・Leanを含む多くの言語では参照カウントが用いられます。参照カウントを持つシステムでは、メモリ内のオブジェクトはそれへの参照がいくつあるかを追跡するフィールドを持ちます。新しい参照が確立されるとカウントが1増えます。参照が存在しなくなるとカウントが1減ります。カウントが0になると、オブジェクトは直ちに解放されます。

参照カウントはガベージコレクションの追跡に対して1つの大きな欠点があります：循環参照によるメモリーリークです。あるオブジェクト \( A \) がオブジェクト \( B \) を参照し、オブジェクト \( B \) がオブジェクト \( A \) を参照している場合、たとえそのプログラム内で \( A \) と \( B \) に対して他に参照が無くてもこれらは決して解放されません。循環参照は制御されていない再帰か、変更可能な参照のどちらかに起因します。Leanはどちらもサポートしていないため、循環参照を構築することは不可能です。

参照カウントによってLeanのランタイムシステムのデータ構造の割り当て・解放のプリミティブが、あるオブジェクトの参照カウントが0になるかどうか、既存のオブジェクトを新しく割り当てることなく再利用するかをチェックできるようになります。これは大きな配列を扱う際には特に重要になります。

Leanの配列についての挿入ソートの実装は以下の性質を満たさなければなりません：

1. Leanがこの関数を partial 注釈無しで許容するべきである
2. 他に参照がない配列が渡された場合、新しい配列を確保するのではなく、in-placeで配列を変更すること

最初の性質は簡単にチェックできます：もしLeanがその定義を受け入れるならば満足します。しかし2つ目は検証方法が必要になります。Leanには下記のシグネチャを持つ dbgTraceIfShared という関数が組み込まれています：

#check dbgTraceIfShared

dbgTraceIfShared.{u} {α : Type u} (s : String) (a : α) : α

これは引数として文字列と値を受け取り、もしその値に複数の参照があれば渡された文字列を使用したメッセージを標準エラーに出力し、値を返します。これは厳密には純粋関数ではありません。しかし、これは関数が実際にメモリを割り当てたりコピーしたりせずにメモリを再利用できるかどうかをチェックするために、開発中にのみ使用することを意図しています。

dbgTraceIfShared の使い方を学ぶにあたって、#eval がコンパイルされたコード中のものよりも多くの値が共有されていると報告することを知ることが大事です。これは混乱を招く恐れがあります。エディタで実験するよりも、lake を使って実行ファイルをビルドすることが重要です。

挿入ソートは2つのループから構成されます。外側のループはポインタをソート対象の配列中で左から右に動かします。各繰り返しの後に、配列内のポインタの左側はソートされる一方で右側は未ソートとなります。内側のループはポインタが指す要素を受け取り、それを適切な場所が見つかりループの不変条件が復元するまで左へと移動させます。言い換えると、各繰り返しは配列の次の要素をソート済み領域の適切な位置に挿入します。

内側のループ

挿入ソートの内側のループは配列と挿入する要素を引数として受け取る末尾再帰関数として実装することができます。挿入されるこの要素は、左側の要素の方が小さいときか配列の先頭にたどり着くまで繰り返し左の要素と入れ替えられ続けます。内側のループは配列のインデックスとして使われる Fin の中の Nat に対して構造的に再帰的です：

def insertSorted [Ord α] (arr : Array α) (i : Fin arr.size) : Array α :=
  match i with
  | ⟨0, _⟩ => arr
  | ⟨i' + 1, _⟩ =>
    have : i' < arr.size := by
      simp [Nat.lt_of_succ_lt, *]
    match Ord.compare arr[i'] arr[i] with
    | .lt | .eq => arr
    | .gt =>
      insertSorted (arr.swap ⟨i', by assumption⟩ i) ⟨i', by simp [*]⟩

インデックス i が 0 ならば、ソート済み領域に挿入されるこの要素はすでに領域の先頭であり最小の値です。インデックスが i' + 1 ならば、i' 番目の要素は i 番目の要素と比較されるべきです。ここで i は Fin arr.size 型ですが、i' は i の val フィールドから得られたものなのでただの Nat であることに注意してください。したがって i' を arr のインデックスとして使う前に i' < arr.size を証明する必要があります。

i' < arr.size の証明から have 式を取り除くと以下のゴールが現れます：

unsolved goals
α : Type ?u.7
inst✝ : Ord α
arr : Array α
i : Fin (Array.size arr)
i' : Nat
isLt✝ : i' + 1 < Array.size arr
⊢ i' < Array.size arr

Nat.lt_of_succ_lt はLeanの標準ライブラリにある定理です。このシグネチャは #check Nat.lt_of_succ_lt で確認でき、以下のようになります：

Nat.lt_of_succ_lt {n m : Nat} (a✝ : Nat.succ n < m) : n < m

言い換えると、これは n + 1 < m ならば n < m であるということを述べています。simp に * を渡すことで最終的な証明を得るために Nat.lt_of_succ_lt に i の isLt フィールドが組み合わせられます。

i' が挿入される要素の左の要素を調べるために使えるようになったため、これら2つの要素を調べて比較します。左の要素が挿入される要素以下であれば、ループは終了し、ループ不変条件が復元されます。もし左の要素が挿入される要素より大きければ、要素が入れ替わり内側のループが再び始まります。Array.swap は Fin である両方のインデックスと、have で成立した i' < arr.size を利用している by assumption を受け取ります。次のループで調べるインデックスも i' ですが、この場合 by assumption だけでは不十分です。なぜなら、この証明は2つの要素を入れ替えた結果ではなく、もとの配列 arr に対して書かれたものだからです。simp タクティクのデータベースには、配列の2つの要素を入れ替えてもサイズが変わらないという事実が含まれており、[*] 引数は have によって導入された仮定を追加で使用するように指示します。

外側のループ

挿入ソートの外側のループでは、ポインタを左から右へ動かし、各繰り返しで insertSorted を呼び出してポインタの要素を配列の正しい位置に挿入します。このループの基本形は Array.map の実装に似ています：

def insertionSortLoop [Ord α] (arr : Array α) (i : Nat) : Array α :=
  if h : i < arr.size then
    insertionSortLoop (insertSorted arr ⟨i, h⟩) (i + 1)
  else
    arr

その結果生じるエラーも termination_by 節を Array.map に指定しない場合に生じるものと同じです。というのも再帰呼び出しのたびに減少する引数がないからです：

fail to show termination for
  insertionSortLoop
with errors
argument #4 was not used for structural recursion
  failed to eliminate recursive application
    insertionSortLoop (insertSorted arr { val := i, isLt := h }) (i + 1)

structural recursion cannot be used

failed to prove termination, use `termination_by` to specify a well-founded relation

停止についての証明を構築する前に、partial 修飾子を使って定義をテストし、これが期待される答えを返すことを確認しておくと便利です：

partial def insertionSortLoop [Ord α] (arr : Array α) (i : Nat) : Array α :=
  if h : i < arr.size then
    insertionSortLoop (insertSorted arr ⟨i, h⟩) (i + 1)
  else
    arr

#eval insertionSortLoop #[5, 17, 3, 8] 0

#[3, 5, 8, 17]

#eval insertionSortLoop #["metamorphic", "igneous", "sedentary"] 0

#["igneous", "metamorphic", "sedentary"]

停止性

ここでもまた、インデックスと配列のサイズの差が各再帰呼び出しのたびに小さくなっていくため関数は停止します。しかし、今回Leanはこの termination_by を受理しません：

def insertionSortLoop [Ord α] (arr : Array α) (i : Nat) : Array α :=
  if h : i < arr.size then
    insertionSortLoop (insertSorted arr ⟨i, h⟩) (i + 1)
  else
    arr
termination_by insertionSortLoop arr i => arr.size - i

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 < Array.size arr
⊢ Array.size (insertSorted arr { val := i, isLt := h }) - (i + 1) < Array.size arr - i

問題はLeanが insertSorted が渡された配列と同じサイズの配列を返すことを知る方法がないことです。insertionSortLoop が停止することを証明するには、まず insertSorted が配列のサイズを変更しないことを証明する必要があります。エラーメッセージから証明されていない停止条件を関数にコピーし、sorry で「証明」することで、この関数を一時的に受け入れることができます：

def insertionSortLoop [Ord α] (arr : Array α) (i : Nat) : Array α :=
  if h : i < arr.size then
    have : (insertSorted arr ⟨i, h⟩).size - (i + 1) < arr.size - i := by
      sorry
    insertionSortLoop (insertSorted arr ⟨i, h⟩) (i + 1)
  else
    arr
termination_by insertionSortLoop arr i => arr.size - i

declaration uses 'sorry'

insertSorted は挿入される要素のインデックスに対して構造的に再帰的であるため、証明はインデックスに対する帰納法で行う必要があります。基本ケースでは配列は変更されずに返されるので、その長さは確かに変化しません。帰納法のステップでは、次の小さいインデックスで再帰的に呼び出しても配列の長さは変わらないという帰納法の仮定が成り立ちます。ここでは2つのケースを考慮します：要素がソート済みの領域に完全に挿入され、配列が変更されずに返される場合と、再帰呼び出しの前に要素が次の要素と交換される場合です。しかし、配列の2つの要素を入れ替えてもサイズは変わらないため、帰納法の仮定によれば次のインデックスによる再帰呼び出しは、引数と同じサイズの配列を返します。したがってサイズは変わりません。

この自然言語の定理文をLeanに翻訳し、本章のテクニックを使って進めば、基本ケースの証明と帰納法のステップを進めるには十分です：

theorem insert_sorted_size_eq [Ord α] (arr : Array α) (i : Fin arr.size) :
    (insertSorted arr i).size = arr.size := by
  match i with
  | ⟨j, isLt⟩ =>
    induction j with
    | zero => simp [insertSorted]
    | succ j' ih =>
      simp [insertSorted]

帰納法のステップ中で insertSorted を使って単純化することで insertSorted 内のパターンマッチが現れます：

unsolved goals
case succ
α : Type u_1
inst✝ : Ord α
arr : Array α
i : Fin (Array.size arr)
j' : Nat
ih : ∀ (isLt : j' < Array.size arr), Array.size (insertSorted arr { val := j', isLt := isLt }) = Array.size arr
isLt : Nat.succ j' < Array.size arr
⊢ Array.size
      (match compare arr[j'] arr[{ val := Nat.succ j', isLt := isLt }] with
      | Ordering.lt => arr
      | Ordering.eq => arr
      | Ordering.gt =>
        insertSorted
          (Array.swap arr { val := j', isLt := (_ : j' < Array.size arr) } { val := Nat.succ j', isLt := isLt })
          { val := j',
            isLt :=
              (_ :
                j' <
                  Array.size
                    (Array.swap arr { val := j', isLt := (_ : j' < Array.size arr) }
                      { val := Nat.succ j', isLt := isLt })) }) =
    Array.size arr

if や match を含むゴールに直面した時、split タクティク（マージソートの定義で使われている split 関数と混同しないように）は制御フローのパスごとにゴールを新しいゴールに置き換えます：

theorem insert_sorted_size_eq [Ord α] (arr : Array α) (i : Fin arr.size) :
    (insertSorted arr i).size = arr.size := by
  match i with
  | ⟨j, isLt⟩ =>
    induction j with
    | zero => simp [insertSorted]
    | succ j' ih =>
      simp [insertSorted]
      split

さらに、それぞれの新しいゴールにはどのブランチがそのゴールにつながったかを示す仮定があり、この場合では heq✝ と名付けられます：

unsolved goals
case succ.h_1
α : Type u_1
inst✝ : Ord α
arr : Array α
i : Fin (Array.size arr)
j' : Nat
ih : ∀ (isLt : j' < Array.size arr), Array.size (insertSorted arr { val := j', isLt := isLt }) = Array.size arr
isLt : Nat.succ j' < Array.size arr
x✝ : Ordering
heq✝ : compare arr[j'] arr[{ val := Nat.succ j', isLt := isLt }] = Ordering.lt
⊢ Array.size arr = Array.size arr

case succ.h_2
α : Type u_1
inst✝ : Ord α
arr : Array α
i : Fin (Array.size arr)
j' : Nat
ih : ∀ (isLt : j' < Array.size arr), Array.size (insertSorted arr { val := j', isLt := isLt }) = Array.size arr
isLt : Nat.succ j' < Array.size arr
x✝ : Ordering
heq✝ : compare arr[j'] arr[{ val := Nat.succ j', isLt := isLt }] = Ordering.eq
⊢ Array.size arr = Array.size arr

case succ.h_3
α : Type u_1
inst✝ : Ord α
arr : Array α
i : Fin (Array.size arr)
j' : Nat
ih : ∀ (isLt : j' < Array.size arr), Array.size (insertSorted arr { val := j', isLt := isLt }) = Array.size arr
isLt : Nat.succ j' < Array.size arr
x✝ : Ordering
heq✝ : compare arr[j'] arr[{ val := Nat.succ j', isLt := isLt }] = Ordering.gt
⊢ Array.size
      (insertSorted
        (Array.swap arr { val := j', isLt := (_ : j' < Array.size arr) } { val := Nat.succ j', isLt := isLt })
        { val := j',
          isLt :=
            (_ :
              j' <
                Array.size
                  (Array.swap arr { val := j', isLt := (_ : j' < Array.size arr) }
                    { val := Nat.succ j', isLt := isLt })) }) =
    Array.size arr

両方のケースに対して単純な証明を書くよりも、split の後に <;> try rfl を加えることで2つの単純なケースはたちまち消え、1つのゴールだけが残ります：

theorem insert_sorted_size_eq [Ord α] (arr : Array α) (i : Fin arr.size) :
    (insertSorted arr i).size = arr.size := by
  match i with
  | ⟨j, isLt⟩ =>
    induction j with
    | zero => simp [insertSorted]
    | succ j' ih =>
      simp [insertSorted]
      split <;> try rfl

unsolved goals
case succ.h_3
α : Type u_1
inst✝ : Ord α
arr : Array α
i : Fin (Array.size arr)
j' : Nat
ih : ∀ (isLt : j' < Array.size arr), Array.size (insertSorted arr { val := j', isLt := isLt }) = Array.size arr
isLt : Nat.succ j' < Array.size arr
x✝ : Ordering
heq✝ : compare arr[j'] arr[{ val := Nat.succ j', isLt := isLt }] = Ordering.gt
⊢ Array.size
      (insertSorted
        (Array.swap arr { val := j', isLt := (_ : j' < Array.size arr) } { val := Nat.succ j', isLt := isLt })
        { val := j',
          isLt :=
            (_ :
              j' <
                Array.size
                  (Array.swap arr { val := j', isLt := (_ : j' < Array.size arr) }
                    { val := Nat.succ j', isLt := isLt })) }) =
    Array.size arr

残念なことに、帰納法の仮定はこのゴールを証明するには不十分です。帰納法の仮定は arr に対して insertSorted を呼び出すとサイズが変わらないことを述べていますが、証明のゴールは再帰的な呼び出しの結果と置換の結果がサイズを変えないことを示すことです。証明を成功させるには、小さい方のインデックスを引数として insertSorted に渡す 任意の 配列に対して機能する帰納法の仮定が必要です。

induction タクティクに generalizing オプションを使用することで強力な帰納法の仮定を得ることができます。このオプションは、基本ケース、帰納法の仮定、および帰納法のステップで示されるゴールを生成するために使用される文にコンテキストから追加の仮定をもたらします。arr を一般化することで、より強力な仮定を導くことができます：

theorem insert_sorted_size_eq [Ord α] (arr : Array α) (i : Fin arr.size) :
    (insertSorted arr i).size = arr.size := by
  match i with
  | ⟨j, isLt⟩ =>
    induction j generalizing arr with
    | zero => simp [insertSorted]
    | succ j' ih =>
      simp [insertSorted]
      split <;> try rfl

その結果、arr は帰納法の仮定の「全ての～について～」文の一部となります：

unsolved goals
case succ.h_3
α : Type u_1
inst✝ : Ord α
j' : Nat
ih :
  ∀ (arr : Array α),
    Fin (Array.size arr) →
      ∀ (isLt : j' < Array.size arr), Array.size (insertSorted arr { val := j', isLt := isLt }) = Array.size arr
arr : Array α
i : Fin (Array.size arr)
isLt : Nat.succ j' < Array.size arr
x✝ : Ordering
heq✝ : compare arr[j'] arr[{ val := Nat.succ j', isLt := isLt }] = Ordering.gt
⊢ Array.size
      (insertSorted
        (Array.swap arr { val := j', isLt := (_ : j' < Array.size arr) } { val := Nat.succ j', isLt := isLt })
        { val := j',
          isLt :=
            (_ :
              j' <
                Array.size
                  (Array.swap arr { val := j', isLt := (_ : j' < Array.size arr) }
                    { val := Nat.succ j', isLt := isLt })) }) =
    Array.size arr

しかし、この証明全体は手に負えなくなっていきます。次のステップは置換結果の長さを表す変数を導入し、それが arr.size と等しいことを示し、この変数が再帰呼び出しの結果得られる配列の長さとも等しいことを示すことです。これらの等式を連鎖させて、ゴールを証明することができます。しかし、帰納法の仮定が自動的に十分強く、変数もすでに導入されるように定理文を注意深く再定式化する方がはるかに簡単です。再定式化された文は次のようになります：

theorem insert_sorted_size_eq [Ord α] (len : Nat) (i : Nat) :
    (arr : Array α) → (isLt : i < arr.size) → arr.size = len →
    (insertSorted arr ⟨i, isLt⟩).size = len := by
  skip

このバージョンの定理文はいくつかの理由から証明が容易です：

1. インデックスとその有効性の証明を Fin にまとめるのではなく、インデックスを配列の前に持ってくる。これにより帰納法の仮定が配列と i が範囲内にあることの証明に対して自然に一般化されます。
2. 抽象的な長さ len が array.size の略として導入されました。証明の自動化は明示的な等号を扱う方が得意な場合が多いです。

結果として得られる証明状態は、帰納法の仮定を生成するために使用される文と、基本ケースと帰納法のステップのゴールを示します：

unsolved goals
α : Type u_1
inst✝ : Ord α
len i : Nat
⊢ ∀ (arr : Array α) (isLt : i < Array.size arr),
    Array.size arr = len → Array.size (insertSorted arr { val := i, isLt := isLt }) = len

この文と induction タクティクの結果として得られるゴールを比べてみてください：

theorem insert_sorted_size_eq [Ord α] (len : Nat) (i : Nat) :
    (arr : Array α) → (isLt : i < arr.size) → arr.size = len →
    (insertSorted arr ⟨i, isLt⟩).size = len := by
  induction i with
  | zero => skip
  | succ i' ih => skip

基本ケースでは、i のそれぞれの出現が 0 に置き換えられています。各仮定の導入に intro を使用し、次に insertSorted を使用して単純化するとインデックス zero での insertSorted はその引数を変更せずに返すため、ゴールが証明されます：

unsolved goals
case zero
α : Type u_1
inst✝ : Ord α
len : Nat
⊢ ∀ (arr : Array α) (isLt : Nat.zero < Array.size arr),
    Array.size arr = len → Array.size (insertSorted arr { val := Nat.zero, isLt := isLt }) = len

帰納法のステップにおいて、帰納法の仮定は実にちょうど良い強さを持ちます。これは配列の長さが len である限り どのような 配列に対しても有効です：

unsolved goals
case succ
α : Type u_1
inst✝ : Ord α
len i' : Nat
ih :
  ∀ (arr : Array α) (isLt : i' < Array.size arr),
    Array.size arr = len → Array.size (insertSorted arr { val := i', isLt := isLt }) = len
⊢ ∀ (arr : Array α) (isLt : Nat.succ i' < Array.size arr),
    Array.size arr = len → Array.size (insertSorted arr { val := Nat.succ i', isLt := isLt }) = len

基本ケースでは、simp によってゴールが arr.size = len へと簡約されます：

theorem insert_sorted_size_eq [Ord α] (len : Nat) (i : Nat) :
    (arr : Array α) → (isLt : i < arr.size) → arr.size = len →
    (insertSorted arr ⟨i, isLt⟩).size = len := by
  induction i with
  | zero =>
    intro arr isLt hLen
    simp [insertSorted]
  | succ i' ih => skip

unsolved goals
case zero
α : Type u_1
inst✝ : Ord α
len : Nat
arr : Array α
isLt : Nat.zero < Array.size arr
hLen : Array.size arr = len
⊢ Array.size arr = len

これは仮定 hLen を使って証明できます。simp に * パラメータを追加することで仮定を追加で使用するように指示することができます：

theorem insert_sorted_size_eq [Ord α] (len : Nat) (i : Nat) :
    (arr : Array α) → (isLt : i < arr.size) → arr.size = len →
    (insertSorted arr ⟨i, isLt⟩).size = len := by
  induction i with
  | zero =>
    intro arr isLt hLen
    simp [insertSorted, *]
  | succ i' ih => skip

帰納法のステップにおいて、仮定の導入とゴールの単純化によってゴールはふたたびパターンマッチを含んだものとなります：

theorem insert_sorted_size_eq [Ord α] (len : Nat) (i : Nat) :
    (arr : Array α) → (isLt : i < arr.size) → (arr.size = len) →
    (insertSorted arr ⟨i, isLt⟩).size = len := by
  induction i with
  | zero =>
    intro arr isLt hLen
    simp [insertSorted, *]
  | succ i' ih =>
    intro arr isLt hLen
    simp [insertSorted]

unsolved goals
case succ
α : Type u_1
inst✝ : Ord α
len i' : Nat
ih :
  ∀ (arr : Array α) (isLt : i' < Array.size arr),
    Array.size arr = len → Array.size (insertSorted arr { val := i', isLt := isLt }) = len
arr : Array α
isLt : Nat.succ i' < Array.size arr
hLen : Array.size arr = len
⊢ Array.size
      (match compare arr[i'] arr[{ val := Nat.succ i', isLt := isLt }] with
      | Ordering.lt => arr
      | Ordering.eq => arr
      | Ordering.gt =>
        insertSorted
          (Array.swap arr { val := i', isLt := (_ : i' < Array.size arr) } { val := Nat.succ i', isLt := isLt })
          { val := i',
            isLt :=
              (_ :
                i' <
                  Array.size
                    (Array.swap arr { val := i', isLt := (_ : i' < Array.size arr) }
                      { val := Nat.succ i', isLt := isLt })) }) =
    len

split タクティクを使うことで各パターンそれぞれに1つずつゴールが割り当てられます。繰り返しになりますが、最初の2つのゴールは再帰呼び出しのない分岐から得られるため帰納法の仮定は必要ありません：

theorem insert_sorted_size_eq [Ord α] (len : Nat) (i : Nat) :
    (arr : Array α) → (isLt : i < arr.size) → (arr.size = len) →
    (insertSorted arr ⟨i, isLt⟩).size = len := by
  induction i with
  | zero =>
    intro arr isLt hLen
    simp [insertSorted, *]
  | succ i' ih =>
    intro arr isLt hLen
    simp [insertSorted]
    split

unsolved goals
case succ.h_1
α : Type u_1
inst✝ : Ord α
len i' : Nat
ih :
  ∀ (arr : Array α) (isLt : i' < Array.size arr),
    Array.size arr = len → Array.size (insertSorted arr { val := i', isLt := isLt }) = len
arr : Array α
isLt : Nat.succ i' < Array.size arr
hLen : Array.size arr = len
x✝ : Ordering
heq✝ : compare arr[i'] arr[{ val := Nat.succ i', isLt := isLt }] = Ordering.lt
⊢ Array.size arr = len

case succ.h_2
α : Type u_1
inst✝ : Ord α
len i' : Nat
ih :
  ∀ (arr : Array α) (isLt : i' < Array.size arr),
    Array.size arr = len → Array.size (insertSorted arr { val := i', isLt := isLt }) = len
arr : Array α
isLt : Nat.succ i' < Array.size arr
hLen : Array.size arr = len
x✝ : Ordering
heq✝ : compare arr[i'] arr[{ val := Nat.succ i', isLt := isLt }] = Ordering.eq
⊢ Array.size arr = len

case succ.h_3
α : Type u_1
inst✝ : Ord α
len i' : Nat
ih :
  ∀ (arr : Array α) (isLt : i' < Array.size arr),
    Array.size arr = len → Array.size (insertSorted arr { val := i', isLt := isLt }) = len
arr : Array α
isLt : Nat.succ i' < Array.size arr
hLen : Array.size arr = len
x✝ : Ordering
heq✝ : compare arr[i'] arr[{ val := Nat.succ i', isLt := isLt }] = Ordering.gt
⊢ Array.size
      (insertSorted
        (Array.swap arr { val := i', isLt := (_ : i' < Array.size arr) } { val := Nat.succ i', isLt := isLt })
        { val := i',
          isLt :=
            (_ :
              i' <
                Array.size
                  (Array.swap arr { val := i', isLt := (_ : i' < Array.size arr) }
                    { val := Nat.succ i', isLt := isLt })) }) =
    len

split で得られる各ゴールで try assumption を実行すると非再帰的なゴールは両方とも無くなります：

theorem insert_sorted_size_eq [Ord α] (len : Nat) (i : Nat) :
    (arr : Array α) → (isLt : i < arr.size) → (arr.size = len) →
    (insertSorted arr ⟨i, isLt⟩).size = len := by
  induction i with
  | zero =>
    intro arr isLt hLen
    simp [insertSorted, *]
  | succ i' ih =>
    intro arr isLt hLen
    simp [insertSorted]
    split <;> try assumption

unsolved goals
case succ.h_3
α : Type u_1
inst✝ : Ord α
len i' : Nat
ih :
  ∀ (arr : Array α) (isLt : i' < Array.size arr),
    Array.size arr = len → Array.size (insertSorted arr { val := i', isLt := isLt }) = len
arr : Array α
isLt : Nat.succ i' < Array.size arr
hLen : Array.size arr = len
x✝ : Ordering
heq✝ : compare arr[i'] arr[{ val := Nat.succ i', isLt := isLt }] = Ordering.gt
⊢ Array.size
      (insertSorted
        (Array.swap arr { val := i', isLt := (_ : i' < Array.size arr) } { val := Nat.succ i', isLt := isLt })
        { val := i',
          isLt :=
            (_ :
              i' <
                Array.size
                  (Array.swap arr { val := i', isLt := (_ : i' < Array.size arr) }
                    { val := Nat.succ i', isLt := isLt })) }) =
    len

再帰関数に関係するすべての配列の長さに定数 len を使用するという新しい証明のゴールについての形式化は simp が解決できる類の問題にうまく当てはまります。配列の長さを len に関連付ける仮定が重要であるため、この証明の最終的なゴールは simp [*] で解くことができます：

theorem insert_sorted_size_eq [Ord α] (len : Nat) (i : Nat) :
    (arr : Array α) → (isLt : i < arr.size) → (arr.size = len) →
    (insertSorted arr ⟨i, isLt⟩).size = len := by
  induction i with
  | zero =>
    intro arr isLt hLen
    simp [insertSorted, *]
  | succ i' ih =>
    intro arr isLt hLen
    simp [insertSorted]
    split <;> try assumption
    simp [*]

最後に、simp [*] は仮定を使うことができるため、try assumption の行は simp [*] に置き換えることができ、証明を短くできます：

theorem insert_sorted_size_eq [Ord α] (len : Nat) (i : Nat) :
    (arr : Array α) → (isLt : i < arr.size) → (arr.size = len) →
    (insertSorted arr ⟨i, isLt⟩).size = len := by
  induction i with
  | zero =>
    intro arr isLt hLen
    simp [insertSorted, *]
  | succ i' ih =>
    intro arr isLt hLen
    simp [insertSorted]
    split <;> simp [*]

これでこの証明を使って insertionSortLoop の sorry を置き換えることができます。定理の len 引数に arr.size を与えることで最終的な結論は (insertSorted arr ⟨i, isLt⟩).size = arr.size となるため、非常に扱いやすい証明のゴールへと書き換えることができます：

  def insertionSortLoop [Ord α] (arr : Array α) (i : Nat) : Array α :=
    if h : i < arr.size then
      have : (insertSorted arr ⟨i, h⟩).size - (i + 1) < arr.size - i := by
        rw [insert_sorted_size_eq arr.size i arr h rfl]
      insertionSortLoop (insertSorted arr ⟨i, h⟩) (i + 1)
    else
      arr
termination_by insertionSortLoop arr i => arr.size - i

unsolved goals
α : Type ?u.22173
inst✝ : Ord α
arr : Array α
i : Nat
h : i < Array.size arr
⊢ Array.size arr - (i + 1) < Array.size arr - i

証明 Nat.sub_succ_lt_self はLeanの標準ライブラリの一部です。この型は ∀ (a i : Nat), i < a → a - (i + 1) < a - i であり、これはまさに必要だったものです：

def insertionSortLoop [Ord α] (arr : Array α) (i : Nat) : Array α :=
  if h : i < arr.size then
    have : (insertSorted arr ⟨i, h⟩).size - (i + 1) < arr.size - i := by
      rw [insert_sorted_size_eq arr.size i arr h rfl]
      simp [Nat.sub_succ_lt_self, *]
    insertionSortLoop (insertSorted arr ⟨i, h⟩) (i + 1)
  else
    arr
termination_by insertionSortLoop arr i => arr.size - i

ドライバ関数

挿入ソート自体は insertionSortLoop を呼び出し、配列のソート済み領域と未ソート領域を区切るインデックスを 0 に初期化します：

def insertionSort [Ord α] (arr : Array α) : Array α :=
   insertionSortLoop arr 0

簡単なテストをいくつかやってみると、この関数は少なくともあからさまに間違ってはいません：

#eval insertionSort #[3, 1, 7, 4]

#[1, 3, 4, 7]

#eval insertionSort #[ "quartz", "marble", "granite", "hematite"]

#["granite", "hematite", "marble", "quartz"]

これは本当に挿入ソート？

挿入ソートはin-placeのソートアルゴリズムとして 定義されています 。最悪実行時間が2倍になるにも関わらず挿入ソートが有用であるのは、余分な領域を割り当てず、ほぼソート済みのデータを効率的に扱う安定したソートアルゴリズムであるからです。もし内部ループの各繰り返しが新しい配列を割り当てるのであれば、このアルゴリズムは 本物の 挿入ソートではありません。

Array.set や Array.swap などのLeanの配列操作は対象の配列の参照カウントが1より大きいかどうかをチェックします。もし大きければ、その配列はコードの複数の個所から見えることになり、コピーしなければならないことになります。そうでなければLeanはもはや純粋関数型言語ではなくなってしまいます。しかし、参照カウントがちょうど1の場合、その値に対する潜在的な観測者はほかに存在しません。このような場合、配列のプリミティブはその場で配列を変更します。ここ以外のプログラムが知り得ないことはそれ等自身を傷つけることはありません。

Leanの証明論理は純粋関数型プログラムのレベルで機能するのであって、その下にある実装に対しては機能しません。つまりプログラムが不必要にデータをコピーしているかどうかを発見する最善の方法は、それをテストすることです。更新が必要な各ポイントで dbgTraceIfShared の呼び出しを追加すると、問題の値が複数の参照を持つ場合に提供されたメッセージが stderr に出力されます。

挿入ソートは変更ではなくコピーをしてしまう恐れのある箇所がまさに一か所あります：Array.swapの呼び出しです。arr.swap ⟨i', by assumption⟩ i を ((dbgTraceIfShared "array to swap" arr).swap ⟨i', by assumption⟩ i) に置き換えることで、プログラムはプログラムを変更できない時は必ず shared RC array to swap を出力するようになります。しかし、追加の関数呼び出しが加わることの変化によって証明も変わってしまいます。dbgTraceIfShared は第2引数を直接返すため、simp の呼び出しに追加するだけで証明は修正されます。

挿入ソートの計装用の完全なコードは以下の通りです：

def insertSorted [Ord α] (arr : Array α) (i : Fin arr.size) : Array α :=
  match i with
  | ⟨0, _⟩ => arr
  | ⟨i' + 1, _⟩ =>
    have : i' < arr.size := by
      simp [Nat.lt_of_succ_lt, *]
    match Ord.compare arr[i'] arr[i] with
    | .lt | .eq => arr
    | .gt =>
      insertSorted
        ((dbgTraceIfShared "array to swap" arr).swap ⟨i', by assumption⟩ i)
        ⟨i', by simp [dbgTraceIfShared, *]⟩

theorem insert_sorted_size_eq [Ord α] (len : Nat) (i : Nat) :
    (arr : Array α) → (isLt : i < arr.size) → (arr.size = len) →
    (insertSorted arr ⟨i, isLt⟩).size = len := by
  induction i with
  | zero =>
    intro arr isLt hLen
    simp [insertSorted, *]
  | succ i' ih =>
    intro arr isLt hLen
    simp [insertSorted, dbgTraceIfShared]
    split <;> simp [*]

def insertionSortLoop [Ord α] (arr : Array α) (i : Nat) : Array α :=
  if h : i < arr.size then
    have : (insertSorted arr ⟨i, h⟩).size - (i + 1) < arr.size - i := by
      rw [insert_sorted_size_eq arr.size i arr h rfl]
      simp [Nat.sub_succ_lt_self, *]
    insertionSortLoop (insertSorted arr ⟨i, h⟩) (i + 1)
  else
    arr
termination_by insertionSortLoop arr i => arr.size - i

def insertionSort [Ord α] (arr : Array α) : Array α :=
  insertionSortLoop arr 0

計装が実際に機能するかどうかをチェックするにはちょっとした工夫が必要です。まずLeanのコンパイラはコンパイル時にすべての引数が分かっている場合、関数呼び出しを積極的に最適化します。そのため計装のために大きな配列に insertionSort を適用するプログラムを書くだけでは不十分です。というのもコンパイル結果のコードはソート済みの配列だけが定数として含まれる可能性があるからです。コンパイラがソートルーチンを最適化しないようにする最も簡単な方法は stdin から配列を読み込むことです。次に、コンパイラはデッドコードの除去を行います。もし let に束縛された変数が使われることがなければ、プログラムへの余分な let を追加しても実行中のコードの参照が増えるとは限りません。余分な参照が完全に除去されないようにするためには、余分な参照が何らかの形で使われるようにすることが重要です。

計装をテストする最初のステップは標準入力から行の配列を読み込む getLines を書くことです：

def getLines : IO (Array String) := do
  let stdin ← IO.getStdin
  let mut lines : Array String := #[]
  let mut currLine ← stdin.getLine
  while !currLine.isEmpty do
     -- Drop trailing newline:
    lines := lines.push (currLine.dropRight 1)
    currLine ← stdin.getLine
  pure lines

IO.FS.Stream.getLine は末尾の開業を含む完全なテキスト行を返します。ファイル終端記号に到達した場合は "" を返します。

次に、2つの別々の main ルーチンが必要です。どちらも標準入力からソート対象の配列を読み込み、これによってコンパイル時に insertionSort の呼び出しが戻り値に置き換えられないようにします。どちらもコンソールに出力し、これにより insertionSort の呼び出しが完全に最適化されることはありません。一方はソートされた配列のみを表示し、もう一方はソートされた配列と元の配列を両方表示します。2番目の関数は Array.swap が新しい配列を確保しなければならなかったという警告を表示します：

def mainUnique : IO Unit := do
  let lines ← getLines
  for line in insertionSort lines do
    IO.println line

def mainShared : IO Unit := do
  let lines ← getLines
  IO.println "--- Sorted lines: ---"
  for line in insertionSort lines do
    IO.println line

  IO.println ""
  IO.println "--- Original data: ---"
  for line in lines do
    IO.println line

実際の main は与えらえたコマンドライン引数に基づいて2つのメインアクションのうち1つを選択するだけです：

def main (args : List String) : IO UInt32 := do
  match args with
  | ["--shared"] => mainShared; pure 0
  | ["--unique"] => mainUnique; pure 0
  | _ =>
    IO.println "Expected single argument, either \"--shared\" or \"--unique\""
    pure 1

引数無しで実行すると、期待通りの使用情報が得られます：

$ sort
Expected single argument, either "--shared" or "--unique"

ファイル test-data は以下の岩についての情報を保持します：

schist
feldspar
diorite
pumice
obsidian
shale
gneiss
marble
flint

これらの岩石に計装用の挿入ソートを使うとアルファベット順に印字されます：

$ sort --unique < test-data
diorite
feldspar
flint
gneiss
marble
obsidian
pumice
schist
shale

しかし、元の配列への参照が保持されるバージョンでは、最初に Array.swap を呼び出した時から stderr （つまり shared RC array to swap ）に通知が行われます：

$ sort --shared < test-data
shared RC array to swap
--- Sorted lines: ---
diorite
feldspar
flint
gneiss
marble
obsidian
pumice
schist
shale

--- Original data: ---
schist
feldspar
diorite
pumice
obsidian
shale
gneiss
marble
flint

shared RC が1つしか表示されないということは、配列が1度だけコピーされることを意味します。これは、Array.swap を呼び出した結果のコピー自体が一意であるためであり、それ以上コピーする必要はありません。命令型言語では、配列を参照渡しする前に明示的にコピーすることを忘れると微妙なバグが発生することがあります。sort --shared を実行すると、Leanのプログラムの純粋関数的な意味を保つために必要な分だけ配列がコピーされますが、それ以上はコピーされません。

その他の更新の機会

参照が一意である場合にコピーの代わりに更新を使用するのは配列更新演算子に限ったことではありません。Leanは参照カウントが0になりそうなコンストラクタを「リサイクル」し、新しいデータを割り当てる代わりに再利用しようとします。これは例えば、Let.map が連結リストをその場で更新することを意味します。Leanのコードでホット・ループを最適化する最も重要なステップの1つは、変更されるデータが複数の場所から参照されないようにすることです。

演習問題

• 配列を反転させる関数を書いてください。入力配列の参照カウントが1の場合、関数が新しい配列を確保しないことをテストしてください。

• 配列に対してマージソートかクイックソートのどちらかを実装してください。読者の実装が停止することを証明し、期待以上の配列を確保しないことをテストしてください。これは難しい練習問題です！