同値の証明

あるプログラムを末尾再帰とアキュムレータを使うように書き直すと、元のプログラムとはかなり異なった見た目になることがあります。オリジナルの再帰関数の方が大抵理解しやすいですが、実行時にスタックを使い果たしてしまう危険性があります。両方のバージョンのプログラムをいくつかの例でテストして単純なバグを取り除いた後に、証明を使ってこれらのプログラムが同値であることをはっきりと示すことができます。

`sum` の等価の証明

sum についてこの両方のバージョンが等しいことを証明するには、まずスタブの証明で定理の文を書き始めます：

theorem non_tail_sum_eq_tail_sum : NonTail.sum = Tail.sum := by
  skip

想定されるようにLeanは未解決のゴールを表示します：

unsolved goals
⊢ NonTail.sum = Tail.sum

NonTail.sum と Tail.sum は定義上同値ではないため、ここでは rfl タクティクを使うことはできません。しかし、関数が等しいと言えるのは定義上の同値だけではありません。同じ入力に対して同じ出力を生成することを証明することで、2つの関数が等しいことを証明することも可能です。言い換えると、\( f = g \) はすべての可能な入力 \( x \) に対して \( f(x) = g(x) \) を示すことで証明できます。この原理は 関数の外延性 （function extensionality）と呼ばれます。関数の外延性はまさに NonTail.sum が Tail.sum と等しいことを説明します：どちらも数値のリストを合計を計算するからです。

Leanのタクティク言語では、関数の外延性は funext を使うことで呼び出され、その後に任意の引数に使われる名前が続きます。この任意の引数はコンテキスト中に仮定として追加され、ゴールはこの引数に適用される関数が等しいことの証明を要求するものへと変化します：

theorem non_tail_sum_eq_tail_sum : NonTail.sum = Tail.sum := by
  funext xs

unsolved goals
case h
xs : List Nat
⊢ NonTail.sum xs = Tail.sum xs

このゴールは引数 xs の帰納法によって証明できます。どちらの sum 関数も、空のリストに適用すると基本ケースに対応する 0 を返します。入力リストの先頭に数値を追加すると、両方の関数でその数値を計算結果に加算します。これは帰納法のステップに対応します。induction タクティクを実行すると、2つのゴールが得られます：

theorem non_tail_sum_eq_tail_sum : NonTail.sum = Tail.sum := by
  funext xs
  induction xs with
  | nil => skip
  | cons y ys ih => skip

unsolved goals
case h.nil
⊢ NonTail.sum [] = Tail.sum []

unsolved goals
case h.cons
y : Nat
ys : List Nat
ih : NonTail.sum ys = Tail.sum ys
⊢ NonTail.sum (y :: ys) = Tail.sum (y :: ys)

nil に対応する基本ケースは rfl を使って解決できます。というのも、どちらの関数も空のリストを渡すと 0 を返すからです：

theorem non_tail_sum_eq_tail_sum : NonTail.sum = Tail.sum := by
  funext xs
  induction xs with
  | nil => rfl
  | cons y ys ih => skip

帰納法のステップを解く最初のステップはゴールを単純化することで、simp によって NonTail.sum と Tail.sum を展開します：

theorem non_tail_sum_eq_tail_sum : NonTail.sum = Tail.sum := by
  funext xs
  induction xs with
  | nil => rfl
  | cons y ys ih =>
    simp [NonTail.sum, Tail.sum]

unsolved goals
case h.cons
y : Nat
ys : List Nat
ih : NonTail.sum ys = Tail.sum ys
⊢ y + NonTail.sum ys = Tail.sumHelper 0 (y :: ys)

Tail.sum を展開することで処理が Tail.sumHelper に即座に委譲されていることがわかり、これもまた単純化されるべきです：

theorem non_tail_sum_eq_tail_sum : NonTail.sum = Tail.sum := by
  funext xs
  induction xs with
  | nil => rfl
  | cons y ys ih =>
    simp [NonTail.sum, Tail.sum, Tail.sumHelper]

これらによって、ゴールでは sumHelper の計算のステップが進み、アキュムレータに y が加算されます：

unsolved goals
case h.cons
y : Nat
ys : List Nat
ih : NonTail.sum ys = Tail.sum ys
⊢ y + NonTail.sum ys = Tail.sumHelper y ys

帰納法の仮定で書き換えを行うことで、ゴールから NonTail.sum のすべての言及が削除されます：

theorem non_tail_sum_eq_tail_sum : NonTail.sum = Tail.sum := by
  funext xs
  induction xs with
  | nil => rfl
  | cons y ys ih =>
    simp [NonTail.sum, Tail.sum, Tail.sumHelper]
    rw [ih]

unsolved goals
case h.cons
y : Nat
ys : List Nat
ih : NonTail.sum ys = Tail.sum ys
⊢ y + Tail.sum ys = Tail.sumHelper y ys

この新しいゴールは、あるリストの和にある数を加えることは、sumHelper の最初のアキュムレータとしてその数を使うことと同じであるということを述べています。わかりやすくするために、この新しいゴールは別の定理として証明することができます：

theorem helper_add_sum_accum (xs : List Nat) (n : Nat) :
    n + Tail.sum xs = Tail.sumHelper n xs := by
  skip

unsolved goals
xs : List Nat
n : Nat
⊢ n + Tail.sum xs = Tail.sumHelper n xs

繰り返しになりますが、これは帰納法による証明であり、基本ケースは rfl を使っています：

theorem helper_add_sum_accum (xs : List Nat) (n : Nat) :
    n + Tail.sum xs = Tail.sumHelper n xs := by
  induction xs with
  | nil => rfl
  | cons y ys ih => skip

unsolved goals
case cons
n y : Nat
ys : List Nat
ih : n + Tail.sum ys = Tail.sumHelper n ys
⊢ n + Tail.sum (y :: ys) = Tail.sumHelper n (y :: ys)

これは帰納法のステップであるため、ゴールは帰納法の仮定 ih と一致するまで単純化する必要があります。Tail.sum と Tail.sumHelper の定義を使って単純化すると、以下のようになります：

theorem helper_add_sum_accum (xs : List Nat) (n : Nat) :
    n + Tail.sum xs = Tail.sumHelper n xs := by
  induction xs with
  | nil => rfl
  | cons y ys ih =>
    simp [Tail.sum, Tail.sumHelper]

unsolved goals
case cons
n y : Nat
ys : List Nat
ih : n + Tail.sum ys = Tail.sumHelper n ys
⊢ n + Tail.sumHelper y ys = Tail.sumHelper (y + n) ys

理想的には、帰納法の仮定を使って Tail.sumHelper (y + n) ys を置き換えることができますが、両者は一致しません。この帰納法の仮定は Tail.sumHelper n ys には使えますが、Tail.sumHelper (y + n) ys には使えません。つまり、この証明は行き詰ってしまいます。

再挑戦

この方針でなんとか頑張る代わりに、ここで一歩引いて考えてみましょう。なぜこの関数の末尾再帰バージョンと非末尾再帰バージョンは等しいのでしょうか？根本的に言えばリストの各要素について、再帰版の結果に加算されるのと同じ量だけアキュムレータが増えます。この洞察によってエレガントな証明を書くことができます。重要なのは、帰納法による証明は帰納法の仮定を 任意の アキュムレータ値に適用できるように設定しなければならないということです。

先ほどの試みは置いておいて、上記の洞察は次の文にエンコードされます：

theorem non_tail_sum_eq_helper_accum (xs : List Nat) :
    (n : Nat) → n + NonTail.sum xs = Tail.sumHelper n xs := by
  skip

この文において、n がコロンの後にある型の一部であることが非常に重要です。この結果、ゴールは「全ての n について～」の略である ∀ (n : Nat) で始まります。

unsolved goals
xs : List Nat
⊢ ∀ (n : Nat), n + NonTail.sum xs = Tail.sumHelper n xs

帰納法のタクティクを用いると、この「全ての～について～」という文を含んだゴールができます：

theorem non_tail_sum_eq_helper_accum (xs : List Nat) :
    (n : Nat) → n + NonTail.sum xs = Tail.sumHelper n xs := by
  induction xs with
  | nil => skip
  | cons y ys ih => skip

nil のケースでは、ゴールは次のようになります：

unsolved goals
case nil
⊢ ∀ (n : Nat), n + NonTail.sum [] = Tail.sumHelper n []

cons の帰納法のステップでは、帰納法の仮定と具体的なゴールの両方に「全ての n について～」が含まれます：

unsolved goals
case cons
y : Nat
ys : List Nat
ih : ∀ (n : Nat), n + NonTail.sum ys = Tail.sumHelper n ys
⊢ ∀ (n : Nat), n + NonTail.sum (y :: ys) = Tail.sumHelper n (y :: ys)

言い換えると、ゴールの証明はより難しくなりましたが、これに応じて帰納法の仮定はより有用なものになったということです。

「全ての \( x \) について～」で始まる文の数学的な証明はある任意の \( x \) を仮定してその文を証明します。ここで「任意」という言葉は \( x \) について追加の性質を何も仮定しないことを意味し、これによって文は どんな \( x \) について成立します。Leanでは、「全ての～について～」文は依存型の関数です：これに適用されるどんな値に対しても、この命題の根拠を返します。同様に、任意の \( x \) を選ぶプロセスは fun x => ... を使うことと同じです。タクティク言語においては、任意の \( x \) を選ぶこの処理は intro タクティクを使って実行されます。これは裏ではタクティクのスクリプトが完成したタイミングで関数を生成します。intro タクティクにはこの任意の値に使用する名前を指定します。

nil のケースで intro タクティクを使うことでゴールから ∀ (n : Nat), が取り除かれ、仮定 n : Nat が追加されます：

theorem non_tail_sum_eq_helper_accum (xs : List Nat) :
    (n : Nat) → n + NonTail.sum xs = Tail.sumHelper n xs := by
  induction xs with
  | nil => intro n
  | cons y ys ih => skip

unsolved goals
case nil
n : Nat
⊢ n + NonTail.sum [] = Tail.sumHelper n []

この命題の同値の両辺は、定義上 n に同値であるため、rfl で十分です：

theorem non_tail_sum_eq_helper_accum (xs : List Nat) :
    (n : Nat) → n + NonTail.sum xs = Tail.sumHelper n xs := by
  induction xs with
  | nil =>
    intro n
    rfl
  | cons y ys ih => skip

cons のゴールにも「全ての～について～」が含まれます：

unsolved goals
case cons
y : Nat
ys : List Nat
ih : ∀ (n : Nat), n + NonTail.sum ys = Tail.sumHelper n ys
⊢ ∀ (n : Nat), n + NonTail.sum (y :: ys) = Tail.sumHelper n (y :: ys)

このことから intro を使う必要があります。

theorem non_tail_sum_eq_helper_accum (xs : List Nat) :
    (n : Nat) → n + NonTail.sum xs = Tail.sumHelper n xs := by
  induction xs with
  | nil =>
    intro n
    rfl
  | cons y ys ih =>
    intro n

unsolved goals
case cons
y : Nat
ys : List Nat
ih : ∀ (n : Nat), n + NonTail.sum ys = Tail.sumHelper n ys
n : Nat
⊢ n + NonTail.sum (y :: ys) = Tail.sumHelper n (y :: ys)

これでこの証明のゴールは NonTail.sum と Tail.sumHelper の両方を y :: ys に適用したものとなります。単純化することで次のステップをより明確にすることができます。

theorem non_tail_sum_eq_helper_accum (xs : List Nat) :
    (n : Nat) → n + NonTail.sum xs = Tail.sumHelper n xs := by
  induction xs with
  | nil =>
    intro n
    rfl
  | cons y ys ih =>
    intro n
    simp [NonTail.sum, Tail.sumHelper]

unsolved goals
case cons
y : Nat
ys : List Nat
ih : ∀ (n : Nat), n + NonTail.sum ys = Tail.sumHelper n ys
n : Nat
⊢ n + (y + NonTail.sum ys) = Tail.sumHelper (y + n) ys

このゴールは帰納法の仮定に非常に近いです。一致しない点は2つです：

この等式の左辺は n + (y + NonTail.sum ys) ですが、帰納法の仮定では左辺は NonTail.sum ys に何かしらの数値を足した数であることが求められています。言い換えれば、このゴールは (n + y) + NonTail.sum ys と書き直されるべきで、これは自然数の足し算が結合的であることから成り立ちます。
左辺を (n + y) + NonTail.sum ys と書き換えた¹場合、右辺のアキュムレータの引数は y + n ではなく n + y とする必要があります。足し算は可換でもあるため、この書き換えも成り立ちます。

足し算の結合性と可換性はLeanの標準ライブラリですでに証明されています。結合性の証明は Nat.add_assoc という名前で (n m k : Nat) → (n + m) + k = n + (m + k) という型を持ち、可換性の証明は Nat.add_comm という名前で (n m : Nat) → n + m = m + n という型を持ちます。通常、rw タクティクには型が同値である式を指定します。しかし、引数が等式を返す依存型の関数である場合、等式がゴールの何かとマッチするようにその関数の引数を見つけようとします。ここでは結合性が適用できる可能性のある個所はただ1つですが、等式 Nat.add_assoc の右辺が証明のゴールにマッチするため、書き換えの方向は逆にしなければなりません：

theorem non_tail_sum_eq_helper_accum (xs : List Nat) :
    (n : Nat) → n + NonTail.sum xs = Tail.sumHelper n xs := by
  induction xs with
  | nil =>
    intro n
    rfl
  | cons y ys ih =>
    intro n
    simp [NonTail.sum, Tail.sumHelper]
    rw [←Nat.add_assoc]

unsolved goals
case cons
y : Nat
ys : List Nat
ih : ∀ (n : Nat), n + NonTail.sum ys = Tail.sumHelper n ys
n : Nat
⊢ n + y + NonTail.sum ys = Tail.sumHelper (y + n) ys

しかし、Nat.add_comm で直接書き換えすると間違った結果になります。ここでの rw タクティクは間違った書き換え場所を推測しており、意図しないゴールに導きます：

theorem non_tail_sum_eq_helper_accum (xs : List Nat) :
    (n : Nat) → n + NonTail.sum xs = Tail.sumHelper n xs := by
  induction xs with
  | nil =>
    intro n
    rfl
  | cons y ys ih =>
    intro n
    simp [NonTail.sum, Tail.sumHelper]
    rw [←Nat.add_assoc]
    rw [Nat.add_comm]

unsolved goals
case cons
y : Nat
ys : List Nat
ih : ∀ (n : Nat), n + NonTail.sum ys = Tail.sumHelper n ys
n : Nat
⊢ NonTail.sum ys + (n + y) = Tail.sumHelper (y + n) ys

これは Nat.add_comm の引数として y と n を明示的に提示することで解決します：

theorem non_tail_sum_eq_helper_accum (xs : List Nat) :
    (n : Nat) → n + NonTail.sum xs = Tail.sumHelper n xs := by
  induction xs with
  | nil =>
    intro n
    rfl
  | cons y ys ih =>
    intro n
    simp [NonTail.sum, Tail.sumHelper]
    rw [←Nat.add_assoc]
    rw [Nat.add_comm y n]

unsolved goals
case cons
y : Nat
ys : List Nat
ih : ∀ (n : Nat), n + NonTail.sum ys = Tail.sumHelper n ys
n : Nat
⊢ n + y + NonTail.sum ys = Tail.sumHelper (n + y) ys

これでゴールは帰納法の仮定にマッチするようになりました。特に、帰納法の仮定の型は依存型の関数型です。ih を n + y に適用すると、期待していた型そのものになります。exact タクティクはその引数が正確に望みの型である場合、証明のゴールを完成させます：

theorem non_tail_sum_eq_helper_accum (xs : List Nat) :
    (n : Nat) → n + NonTail.sum xs = Tail.sumHelper n xs := by
  induction xs with
  | nil => intro n; rfl
  | cons y ys ih =>
    intro n
    simp [NonTail.sum, Tail.sumHelper]
    rw [←Nat.add_assoc]
    rw [Nat.add_comm y n]
    exact ih (n + y)

実際の証明では、ゴールをこのような補助的な定義の型と一致させるためにはさらにほんの少しだけ追加作業が必要になります。最初のステップは、ここでも関数の外延性を呼び出すことです：

theorem non_tail_sum_eq_tail_sum : NonTail.sum = Tail.sum := by
  funext xs

unsolved goals
case h
xs : List Nat
⊢ NonTail.sum xs = Tail.sum xs

次のステップは Tail.sum を展開し、Tail.sumHelper を公開することです：

theorem non_tail_sum_eq_tail_sum : NonTail.sum = Tail.sum := by
  funext xs
  simp [Tail.sum]

unsolved goals
case h
xs : List Nat
⊢ NonTail.sum xs = Tail.sumHelper 0 xs

こうすることで、型はほとんど一致します。しかし、補助定理では左辺に追加で加算を行っています。言い換えると、証明のゴールは NonTail.sum xs = Tail.sumHelper 0 xs ですが、non_tail_sum_eq_helper_accum を xs と 0 に適用すると 0 + NonTail.sum xs = Tail.sumHelper 0 xs という型が得られます。ここで標準ライブラリには (n : Nat) → 0 + n = n という型を持つ Nat.zero_add という証明があります。この関数を NonTail.sum xs に適用すると式は 0 + NonTail.sum xs = NonTail.sum xs という型になり、これで右辺から左辺への書き換えによって望みの型が得られます：

theorem non_tail_sum_eq_tail_sum : NonTail.sum = Tail.sum := by
  funext xs
  simp [Tail.sum]
  rw [←Nat.zero_add (NonTail.sum xs)]

unsolved goals
case h
xs : List Nat
⊢ 0 + NonTail.sum xs = Tail.sumHelper 0 xs

最終的に、この補助定理によって証明が完成します：

theorem non_tail_sum_eq_tail_sum : NonTail.sum = Tail.sum := by
  funext xs
  simp [Tail.sum]
  rw [←Nat.zero_add (NonTail.sum xs)]
  exact non_tail_sum_eq_helper_accum xs 0

この証明はアキュムレータを渡す版の末尾再帰関数が非末尾再帰版と等しいことを証明する時に使用できる一般的なパターンを示しています。最初のステップでは、開始時のアキュムレータの引数と最終結果の関係を発見することです。例えば、Tail.sumHelper を n のアキュムレータで開始すると、最終的な合計に n が加算され、Tail.reverseHelper を ys のアキュムレータで開始すると、最終的な反転されたリストが ys の前に追加されます。2つ目のステップは、この関係を定理として書き出し、帰納法によって証明することです。実際にはアキュムレータは常に 0 や [] などの中立な値で初期化されますが、開始時のアキュムレータを任意の値にすることができるこの一般的な文は、十分に強力な帰納法の仮定を得るために必要なものです。最後に、この補助定理を実際のアキュムレータの初期値で使用すると望ましい証明が得られます。例えば、non_tail_sum_eq_tail_sum ではアキュムレータは 0 が指定されます。この場合、中立的なアキュムレータの初期値が適切な場所で発生するようにゴールを書き換える必要があるかもしれません。

演習問題

準備運動

Nat.zero_add ・Nat.add_assoc ・Nat.add_comm の証明を induction タクティクを使って自分で書いてみましょう。

アキュムレータについて他の証明

リストの反転

sum についての証明を NonTail.reverse と Tail.reverse の証明に適用してください。最初のステップは Tail.reverseHelper に渡されるアキュムレータの値と非末尾再帰的な反転の間の関係を考えることです。ちょうど Tail.sumHelper でアキュムレータに数値を追加することが全体の合計に追加することと同じように、Tail.reverseHelper でアキュムレータに新しい要素を追加するために List.cons を使用することは全体の結果に何らかの変更を加えることと同じです。関係性がはっきりするまで、紙と鉛筆を使って3，4例の異なるアキュムレータの値を試してください。この関係を使って適切な補助定理を証明してください。それから全体の証明を書き下してください。NonTail.reverse と Tail.reverse は多相であるため、両者が等価であることを示すにはLeanが α にどのような型を使うべきかを考えさせないために @ を使う必要があります。いったん α が通常の引数として扱われると、funext は α と xs の両方で呼び出されるようになります：

theorem non_tail_reverse_eq_tail_reverse : @NonTail.reverse = @Tail.reverse := by
  funext α xs

これによって適切なゴールが生まれます：

unsolved goals
case h.h
α : Type u_1
xs : List α
⊢ NonTail.reverse xs = Tail.reverse xs

階乗

アキュムレータと結果の関係を見つけ、適切な補助定理を証明することによって、前の節の練習問題で出てきた NonTail.factorial が読者の末尾再帰版の解答と等しいことを証明してください。

原文では(y + n) + NonTail.sum ysとなっているが、おそらくyとnの位置が逆になっている

Functional Programming in Lean 日本語訳