その他の不等式

arrayMapHelper と findHelper が停止することをチェックするにはLeanの組み込みの証明自動化だけで十分です。必要なものは再帰的に呼び出すたびに値が減少する式を提供することだけです。しかし、Leanの組み込みの自動化は魔法ではないため、しばしば手助けが必要になります。

マージソート

停止証明が自明でない関数の一例として、List のマージソートがあります。マージソートは2つのフェーズから構成されます。まずリストが半分に分割されます。半分になったそれぞれがマージソートでソートされ、その結果を結合してより大きなソート済みリストにする関数を使ってマージされます。基本ケースは空リストと要素が1つのリストで、どちらもすでにソート済みであると見なされます。

2つのソート済みのリストをマージするには2つの基本ケースを考慮する必要があります：

1. どちらかのリストが空であれば、結果はもう片方のリストになります。
2. どちらのリストも空でない場合、それらの先頭を比較します。この関数の結果は2つのリストのどちらか小さい方の先頭に両方のリストの残りの要素をマージした結果が続きます。

これはどちらのリストに対しても構造的に再帰的ではありません。再帰呼び出しのたびに2つのリストのどちらかから1つの要素が削除されるため再帰は終了します。termination_by 節は両方のリストの長さの合計を減少する値として使用します：

def merge [Ord α] (xs : List α) (ys : List α) : List α :=
  match xs, ys with
  | [], _ => ys
  | _, [] => xs
  | x'::xs', y'::ys' =>
    match Ord.compare x' y' with
    | .lt | .eq => x' :: merge xs' (y' :: ys')
    | .gt => y' :: merge (x'::xs') ys'
termination_by merge xs ys => xs.length + ys.length

リストの長さを使うだけでなく、両方のリストを含むペアを提供することもできます：

def merge [Ord α] (xs : List α) (ys : List α) : List α :=
  match xs, ys with
  | [], _ => ys
  | _, [] => xs
  | x'::xs', y'::ys' =>
    match Ord.compare x' y' with
    | .lt | .eq => x' :: merge xs' (y' :: ys')
    | .gt => y' :: merge (x'::xs') ys'
termination_by merge xs ys => (xs, ys)

これはLeanが WellFoundedRelation という型クラスで表現されるデータのサイズに関する概念を組み込んでいるため機能します。この型クラスのペアへのインスタンスでは、ペアの1つ目か2つ目のアイテムのどちらかが縮小すると、自動的に小さくなったと見なされます。

リストを分割する簡単な方法は、入力リストの各要素を2つの出力リストに楮に追加することです：

def splitList (lst : List α) : (List α × List α) :=
  match lst with
  | [] => ([], [])
  | x :: xs =>
    let (a, b) := splitList xs
    (x :: b, a)

マージソートでは基本ケースに到達したかどうかをチェックします。もしそうであれば入力リストを返します。そうでない場合は、入力を分割し、それぞれの半分をソートした結果をマージします：

def mergeSort [Ord α] (xs : List α) : List α :=
  if h : xs.length < 2 then
    match xs with
    | [] => []
    | [x] => [x]
  else
    let halves := splitList xs
    merge (mergeSort halves.fst) (mergeSort halves.snd)

Leanのパターンマッチのコンパイラは xs.length < 2 かどうかをテストする if によって導入された仮定 h が、1つ以上の要素を除外していることを見分けることができます。そのため「場合分けの考慮もれ」エラーは発生しません。しかし、このプログラムは常に終了するにも関わらず、構造的には再帰的ではありません：

fail to show termination for
  mergeSort
with errors
argument #3 was not used for structural recursion
  failed to eliminate recursive application
    mergeSort halves.fst

structural recursion cannot be used

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

これが停止する理由は splitList が常に入力よりも短いリストを返すからです。したがって、halves.fst と halves.snd の長さは xs の長さ未満となります。これは termination_by 節を使って表現することができます：

def mergeSort [Ord α] (xs : List α) : List α :=
  if h : xs.length < 2 then
    match xs with
    | [] => []
    | [x] => [x]
  else
    let halves := splitList xs
    merge (mergeSort halves.fst) (mergeSort halves.snd)
termination_by mergeSort xs => xs.length

この節によってエラーメッセージが変化します。Leanは関数が構造的に再帰的でないと文句を言う代わりに、(splitList xs).fst.length < xs.length を自動的に証明できなかった旨を指摘します：

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
xs : List α
h : ¬List.length xs < 2
halves : List α × List α := splitList xs
⊢ List.length (splitList xs).fst < List.length xs

分割によってリストが短くなること

(splitList xs).snd.length < xs.length もまた証明する必要があります。splitList は2つのリストに交互に要素を追加するため、一度に両方の文を証明することが最も簡単であり、そのため証明の構造は splitList 実装に用いられたアルゴリズムに従います。つまり ∀(lst : List), (splitList lst).fst.length < lst.length ∧ (splitList lst).snd.length < lst.length を証明することが最も簡単です。

しかし残念なことに、この文は偽です。特に、splitList [] は ([], []) となります。出力のリストはどちらも長さが 0 で、入力のリストの長さである 0 未満ではありません。同様に、splitList ["basalt"] は (["basalt"], []) に評価され、["basalt"] の長さは ["basalt"] 未満ではありません。しかし、splitList ["basalt", "granite"] は (["basalt"], ["granite"]) に評価され、出力のリストは入力リストよりも短くなります。

したがって出力されるリストの長さは必ず入力リストの長さ以下である一方で、入力リストが2つ以上要素を持つときだけ出力リストの長さが入力リストより短くなることがわかります。前者を証明し、後者に拡張することが簡単です。まず次の定理から始めます：

theorem splitList_shorter_le (lst : List α) :
    (splitList lst).fst.length ≤ lst.length ∧
      (splitList lst).snd.length ≤ lst.length := by
  skip

unsolved goals
α : Type u_1
lst : List α
⊢ List.length (splitList lst).fst ≤ List.length lst ∧ List.length (splitList lst).snd ≤ List.length lst

splitList はリスト上において構造的に再帰的であるため、証明は帰納法を使うべきです。splitList についての構造的な再帰は帰納法による証明に完璧に合致します：帰納法の基本ケースは再帰の基本ケースに、帰納法のステップは再帰呼び出しに一致します。induction タクティクは2つのゴールを与えます：

theorem splitList_shorter_le (lst : List α) :
    (splitList lst).fst.length ≤ lst.length ∧
      (splitList lst).snd.length ≤ lst.length := by
  induction lst with
  | nil => skip
  | cons x xs ih => skip

unsolved goals
case nil
α : Type u_1
⊢ List.length (splitList []).fst ≤ List.length [] ∧ List.length (splitList []).snd ≤ List.length []

unsolved goals
case cons
α : Type u_1
x : α
xs : List α
ih : List.length (splitList xs).fst ≤ List.length xs ∧ List.length (splitList xs).snd ≤ List.length xs
⊢ List.length (splitList (x :: xs)).fst ≤ List.length (x :: xs) ∧
    List.length (splitList (x :: xs)).snd ≤ List.length (x :: xs)

空リストの長さは空リストの長さ以下であるため、nil のケースについてのゴールは単純化器を起動して splitList の定義を展開するよう指示することで証明できます。同様に、cons の場合に splitList を用いて単純化するとゴールの長さを Nat.succ が包みます：

theorem splitList_shorter_le (lst : List α) :
    (splitList lst).fst.length ≤ lst.length ∧
      (splitList lst).snd.length ≤ lst.length := by
  induction lst with
  | nil => simp [splitList]
  | cons x xs ih =>
    simp [splitList]

unsolved goals
case cons
α : Type u_1
x : α
xs : List α
ih : List.length (splitList xs).fst ≤ List.length xs ∧ List.length (splitList xs).snd ≤ List.length xs
⊢ Nat.succ (List.length (splitList xs).snd) ≤ Nat.succ (List.length xs) ∧
    List.length (splitList xs).fst ≤ Nat.succ (List.length xs)

これは List.length の呼び出しがリストの先頭 x :: xs を消費し、入力リストの長さと最初の出力リストの長さの両方で Nat.succ に変換するからです。

Leanにおいて A ∧ B は And A B の略記です。And は Prop 宇宙での構造体型です。

structure And (a b : Prop) : Prop where
  intro ::
  left : a
  right : b

言いかえれば、A ∧ B の証明は And.intro コンストラクタを left フィールドの A の証明と right フィールドの B の証明に適用したものです。

cases タクティクを使うと、証明をデータ型の各コンストラクタや命題の各証明に対して順番に考慮することができます。これは再帰のない match 式に相当します。構造体に対して cases を使用すると、プログラムで使用するためにパターンマッチ式が構造体のフィールドを展開するのと同じように、構造体が分解され構造体の各フィールドに対して仮定が追加されます。構造体にはコンストラクタが1つしかないため、構造体に対して cases を使用してもゴールが追加されることはありません。

ih は List.length (splitList xs).fst ≤ List.length xs ∧ List.length (splitList xs).snd ≤ List.length xs の証明であるため、cases ih を使うと仮定 List.length (splitList xs).fst ≤ List.length xs と仮定 List.length (splitList xs).snd ≤ List.length xs が得られます：

theorem splitList_shorter_le (lst : List α) :
    (splitList lst).fst.length ≤ lst.length ∧
      (splitList lst).snd.length ≤ lst.length := by
  induction lst with
  | nil => simp [splitList]
  | cons x xs ih =>
    simp [splitList]
    cases ih

unsolved goals
case cons.intro
α : Type u_1
x : α
xs : List α
left✝ : List.length (splitList xs).fst ≤ List.length xs
right✝ : List.length (splitList xs).snd ≤ List.length xs
⊢ Nat.succ (List.length (splitList xs).snd) ≤ Nat.succ (List.length xs) ∧
    List.length (splitList xs).fst ≤ Nat.succ (List.length xs)

証明のゴールも And であるため、constructor タクティクを使って And.intro を適用し、各引数のゴールを得ることができます：

theorem splitList_shorter_le (lst : List α) :
    (splitList lst).fst.length ≤ lst.length ∧
      (splitList lst).snd.length ≤ lst.length := by
  induction lst with
  | nil => simp [splitList]
  | cons x xs ih =>
    simp [splitList]
    cases ih
    constructor

unsolved goals
case cons.intro.left
α : Type u_1
x : α
xs : List α
left✝ : List.length (splitList xs).fst ≤ List.length xs
right✝ : List.length (splitList xs).snd ≤ List.length xs
⊢ Nat.succ (List.length (splitList xs).snd) ≤ Nat.succ (List.length xs)

case cons.intro.right
α : Type u_1
x : α
xs : List α
left✝ : List.length (splitList xs).fst ≤ List.length xs
right✝ : List.length (splitList xs).snd ≤ List.length xs
⊢ List.length (splitList xs).fst ≤ Nat.succ (List.length xs)

left のゴールは left の仮定にとてもよく似ていますが、ゴールでは不等式の両辺を Nat.succ が包んでいます。同様に、right のゴールは right に似ていますが、Nat.succ が入力リストの長さにのみ追加されています。これらの Nat.succ のラッピングが文の正しさを保持することを証明する時がきました。

両辺に1を足す

left ゴールの場合、証明すべき文は Nat.succ_le_succ : n ≤ m → Nat.succ n ≤ Nat.succ m です。言い換えると、もし n ≤ m ならば両辺に1を足してもこの事実は変わらないということです。なぜそうなるのでしょうか？n ≤ m ということの証明は Nat.le.refl コンストラクタに Nat.le.step コンストラクタを m - n 個のインスタンスでくるんだものです。両辺に1を足すことは単純に refl が以前より1だけ大きい数に適用され、同じ数の step コンストラクタを持つことを意味します。

より形式的には、この証明は n ≤ m という根拠に対する帰納法で示されます。もし根拠が refl ならば、n = m であるため Nat.succ n = Nat.succ m となり、再び refl を使うことができます。もし根拠が step ならば、帰納法の仮定からは Nat.succ n ≤ Nat.succ m という根拠が提供され、ゴールは Nat.succ n ≤ Nat.succ (Nat.succ m) を示すことになります。これは step と帰納法の仮定を併用することで可能です。

Leanにおいて、この定理は以下のように表現されます：

theorem Nat.succ_le_succ : n ≤ m → Nat.succ n ≤ Nat.succ m := by
  skip

そしてエラーメッセージがこの内容を要約しています：

unsolved goals
n m : Nat
⊢ n ≤ m → Nat.succ n ≤ Nat.succ m

最初のステップは intro タクティクを使うことで、これにより n ≤ m という仮定をスコープ内に導入し、名前を付けます：

theorem Nat.succ_le_succ : n ≤ m → Nat.succ n ≤ Nat.succ m := by
  intro h

unsolved goals
n m : Nat
h : n ≤ m
⊢ Nat.succ n ≤ Nat.succ m

この証明は n ≤ m についての根拠に対しての帰納法であるため、次に使うタクティクは induction h です：

theorem Nat.succ_le_succ : n ≤ m → Nat.succ n ≤ Nat.succ m := by
  intro h
  induction h

これによりゴールが Nat.le の各コンストラクタそれぞれに1つずつ、合計2つ作られます：

unsolved goals
case refl
n m : Nat
⊢ Nat.succ n ≤ Nat.succ n

case step
n m m✝ : Nat
a✝ : Nat.le n m✝
a_ih✝ : Nat.succ n ≤ Nat.succ m✝
⊢ Nat.succ n ≤ Nat.succ (Nat.succ m✝)

refl についてのゴールは refl を使って解くことができ、これは constructor タクティクによっても選ばれます。step についてのゴールも step コンストラクタを使用する必要があります：

theorem Nat.succ_le_succ : n ≤ m → Nat.succ n ≤ Nat.succ m := by
  intro h
  induction h with
  | refl => constructor
  | step h' ih => constructor

unsolved goals
case step.a
n m m✝ : Nat
h' : Nat.le n m✝
ih : Nat.succ n ≤ Nat.succ m✝
⊢ Nat.le (Nat.succ n) (m✝ + 1)

このゴールはもはや ≤ 演算子を用いた表示でありませんが、これは帰納法の仮定 ih と等価です。assumption タクティクはゴールを埋める仮定を自動で選択し、これで証明が完了します：

theorem Nat.succ_le_succ : n ≤ m → Nat.succ n ≤ Nat.succ m := by
  intro h
  induction h with
  | refl => constructor
  | step h' ih =>
    constructor
    assumption

この証明を再帰関数として書くと以下のようになります：

theorem Nat.succ_le_succ : n ≤ m → Nat.succ n ≤ Nat.succ m
  | .refl => .refl
  | .step h' => .step (Nat.succ_le_succ h')

帰納法によるタクティクベースの証明とこの再帰関数を比較することは学びになるでしょう。どの証明ステップがこの定義のどの部分に対応するでしょうか？

大きい辺に1を足す

splitList_shorter_le の証明に必要な2つめの不等式は ∀(n m : Nat), n ≤ m → n ≤ Nat.succ m です。この証明はほとんど Nat.succ_le_succ と同じです。繰り返しになりますが、n ≤ m という仮定が導入されることで Nat.le.step コンストラクタの数によって n と m の差を本質的に追跡することができます。したがって、この証明は基本ケースに Nat.le.step を足す必要があります。この証明は次のように書かれます：

theorem Nat.le_succ_of_le : n ≤ m → n ≤ Nat.succ m := by
  intro h
  induction h with
  | refl => constructor; constructor
  | step => constructor; assumption

裏で何が起こっているかを明らかにするために、apply と exact タクティクを使用してどちらのコンストラクタが適用されているかを正確に示すことができます。apply タクティクは戻り値の型が現在のゴールに一致するような関数やコンストラクタを適用することで現在のゴールを解きます。もし関数などに引数を与えなかった場合は exact では失敗してしまいますが、apply では新たなゴールが作られます。：

theorem Nat.le_succ_of_le : n ≤ m → n ≤ Nat.succ m := by
  intro h
  induction h with
  | refl => apply Nat.le.step; exact Nat.le.refl
  | step _ ih => apply Nat.le.step; exact ih

この証明をゴルフすることができます：

theorem Nat.le_succ_of_le (h : n ≤ m) : n ≤ Nat.succ m := by
  induction h <;> repeat (first | constructor | assumption)

この短いタクティクのスクリプトでは、induction によって導入された両方のゴールに repeat (first | constructor | assumption) を使って対処しています。タクティク first | T1 | T2 | ... | Tn は T1 から Tn まで順番に試してみて、最初に成功したタクティクを使うことを意味します。つまり、repeat (first | constructor | assumption) はできる限りコンストラクタを適用し、その後仮定を使ってゴールを解こうとします。

最後に、この証明は再帰関数を使っても書くことができます：

theorem Nat.le_succ_of_le : n ≤ m → n ≤ Nat.succ m
  | .refl => .step .refl
  | .step h => .step (Nat.le_succ_of_le h)

証明についての各スタイルは適材適所です。詳細な証明のスクリプトは初心者がコードを読む場合や、証明のステップから何らかの洞察が得られるような場合に有用です。短く、高度に自動化された証明スクリプトは一般的に保守が容易です。なぜなら、自動化は定義やデータ型の小さな変更を柔軟に吸収し、かつロバストであることが多いからです。再帰関数は一般的に数学的証明の観点からは理解しにくく、保守もしづらいですが、対話型定理証明に取り組み始めたばかりのプログラマにとっては有用な橋渡しになります。

証明を完成させる

これで補助定理が両方とも証明されたため、splitList_shorter_le の残りの部分はすぐに完了します。現在の証明状態には、And の左辺と右辺の2つのゴールがあります：

unsolved goals
case cons.intro.left
α : Type u_1
x : α
xs : List α
left✝ : List.length (splitList xs).fst ≤ List.length xs
right✝ : List.length (splitList xs).snd ≤ List.length xs
⊢ Nat.succ (List.length (splitList xs).snd) ≤ Nat.succ (List.length xs)

case cons.intro.right
α : Type u_1
x : α
xs : List α
left✝ : List.length (splitList xs).fst ≤ List.length xs
right✝ : List.length (splitList xs).snd ≤ List.length xs
⊢ List.length (splitList xs).fst ≤ Nat.succ (List.length xs)

これらのゴールは And 構造体のフィールド名が付けられています。つまり case タクティク（cases と混同しないように）を使ってそれぞれ順番に焦点を当てることができます：

theorem splitList_shorter_le (lst : List α) :
    (splitList lst).fst.length ≤ lst.length ∧ (splitList lst).snd.length ≤ lst.length := by
  induction lst with
  | nil => simp [splitList]
  | cons x xs ih =>
    simp [splitList]
    cases ih
    constructor
    case left => skip
    case right => skip

両方の未解決ゴールを並べた1つのエラーから、それぞれ skip による2つのメッセージが表示されるようになります。left のゴールでは Nat.succ_le_succ を使うことができます：

unsolved goals
α : Type u_1
x : α
xs : List α
left✝ : List.length (splitList xs).fst ≤ List.length xs
right✝ : List.length (splitList xs).snd ≤ List.length xs
⊢ Nat.succ (List.length (splitList xs).snd) ≤ Nat.succ (List.length xs)

右のゴールでは Nat.le_suc_of_le が合致します：

unsolved goals
α : Type u_1
x : α
xs : List α
left✝ : List.length (splitList xs).fst ≤ List.length xs
right✝ : List.length (splitList xs).snd ≤ List.length xs
⊢ List.length (splitList xs).fst ≤ Nat.succ (List.length xs)

どちらの定理も前提条件に n ≤ m を含みます。これは left✝ と right✝ という仮定として見つけることができ、assumption タクティクによって最終的なゴールが対処されることを意味します：

theorem splitList_shorter_le (lst : List α) :
    (splitList lst).fst.length ≤ lst.length ∧ (splitList lst).snd.length ≤ lst.length := by
  induction lst with
  | nil => simp [splitList]
  | cons x xs ih =>
    simp [splitList]
    cases ih
    constructor
    case left => apply Nat.succ_le_succ; assumption
    case right => apply Nat.le_succ_of_le; assumption

次のステップはマージソートが終了することを証明するために必要な実際の定理に戻ることです：すなわち、リストが少なくとも2つの要素を持つ限り、それを分割した結果の長さは両方とももとのリスト未満という定理です。

theorem splitList_shorter (lst : List α) (_ : lst.length ≥ 2) :
    (splitList lst).fst.length < lst.length ∧
      (splitList lst).snd.length < lst.length := by
  skip

unsolved goals
α : Type u_1
lst : List α
x✝ : List.length lst ≥ 2
⊢ List.length (splitList lst).fst < List.length lst ∧ List.length (splitList lst).snd < List.length lst

パターンマッチは通常のプログラムと同様にタクティクスクリプトでもうまく機能します。lst には少なくとも2つの要素があるため、match をつかって展開することができます。同時に依存パターンマッチによって型も絞り込まれます：

theorem splitList_shorter (lst : List α) (_ : lst.length ≥ 2) :
    (splitList lst).fst.length < lst.length ∧
      (splitList lst).snd.length < lst.length := by
  match lst with
  | x :: y :: xs =>
    skip

unsolved goals
α : Type u_1
lst : List α
x y : α
xs : List α
x✝ : List.length (x :: y :: xs) ≥ 2
⊢ List.length (splitList (x :: y :: xs)).fst < List.length (x :: y :: xs) ∧
    List.length (splitList (x :: y :: xs)).snd < List.length (x :: y :: xs)

splitList を使って単純化すると、x と y が取り除かれ、それぞれ Nat.succ が増えたリストの長さが計算されます：

theorem splitList_shorter (lst : List α) (_ : lst.length ≥ 2) :
    (splitList lst).fst.length < lst.length ∧
      (splitList lst).snd.length < lst.length := by
  match lst with
  | x :: y :: xs =>
    simp [splitList]

unsolved goals
α : Type u_1
lst : List α
x y : α
xs : List α
x✝ : List.length (x :: y :: xs) ≥ 2
⊢ Nat.succ (List.length (splitList xs).fst) < Nat.succ (Nat.succ (List.length xs)) ∧
    Nat.succ (List.length (splitList xs).snd) < Nat.succ (Nat.succ (List.length xs))

simp を simp_arith に置き換えると、これらの Nat.succ コンストラクタは削除されます。なぜなら、simp_arith は n + 1 < m + 1 が n < m を意味することを利用するからです：

theorem splitList_shorter (lst : List α) (_ : lst.length ≥ 2) :
    (splitList lst).fst.length < lst.length ∧
      (splitList lst).snd.length < lst.length := by
  match lst with
  | x :: y :: xs =>
    simp_arith [splitList]

unsolved goals
α : Type u_1
lst : List α
x y : α
xs : List α
x✝ : List.length (x :: y :: xs) ≥ 2
⊢ List.length (splitList xs).fst ≤ List.length xs ∧ List.length (splitList xs).snd ≤ List.length xs

これでこのゴールは splitList_shorter_le にマッチし、証明が完結します：

theorem splitList_shorter (lst : List α) (_ : lst.length ≥ 2) :
    (splitList lst).fst.length < lst.length ∧
      (splitList lst).snd.length < lst.length := by
  match lst with
  | x :: y :: xs =>
    simp_arith [splitList]
    apply splitList_shorter_le

mergeSort が停止することを証明するために必要な事実は、結果として得られる And から引き出すことができます：

theorem splitList_shorter_fst (lst : List α) (h : lst.length ≥ 2) :
    (splitList lst).fst.length < lst.length :=
  splitList_shorter lst h |>.left

theorem splitList_shorter_snd (lst : List α) (h : lst.length ≥ 2) :
    (splitList lst).snd.length < lst.length :=
  splitList_shorter lst h |>.right

マージソートが停止すること

マージソートは2つの再帰呼び出しを持ち、それぞれ splitList が返すサブリストに対して呼び出されます。それぞれの再帰呼び出しでは渡されるリストの長さが入力リストの長さよりも短いことを証明する必要があります。停止性の証明は通常2つのステップで書くと便利です：まずLeanが停止を検証できる命題を書き出し、それを証明します。そうでないと、命題の証明に多くの労力を費やした結果、それが再帰呼び出しの入力が小さくなることの証明に全く必要ないということだけが判明するということにもなりかねません。

sorry タクティクはどのようなゴール、それこそ偽のものであっても証明することができます。これは本番のコードや最終的な証明に使うことは意図されていませんが、証明やプログラムを前もって「下書き」する便利な方法です。sorry を使った定義や定理には警告が付きます。

sorry を使った mergeSort の停止引数についての最初のスケッチは、Leanが証明できなかったゴールを have 式にコピーすることから書き始められます。Leanにおいて、have は let に似ています。have を使う場合、名前を省略することができます。一般的に、let は興味の対象の値を参照する名前の定義のために使用され、have はLeanが何かしらの根拠を検索した際に見つかる命題を局所的に証明するために使用されます。この根拠は配列の検索が範囲内であることや関数が停止することなどです。

def mergeSort [Ord α] (xs : List α) : List α :=
  if h : xs.length < 2 then
    match xs with
    | [] => []
    | [x] => [x]
  else
    let halves := splitList xs
    have : halves.fst.length < xs.length := by
      sorry
    have : halves.snd.length < xs.length := by
      sorry
    merge (mergeSort halves.fst) (mergeSort halves.snd)
termination_by mergeSort xs => xs.length

名前 mergeSort に対して警告が現れます：

declaration uses 'sorry'

エラーは無いため、この命題の方向性は停止性の証明に十分です。

この証明はまず補助定理の適用からはじまります：

def mergeSort [Ord α] (xs : List α) : List α :=
  if h : xs.length < 2 then
    match xs with
    | [] => []
    | [x] => [x]
  else
    let halves := splitList xs
    have : halves.fst.length < xs.length := by
      apply splitList_shorter_fst
    have : halves.snd.length < xs.length := by
      apply splitList_shorter_snd
    merge (mergeSort halves.fst) (mergeSort halves.snd)
termination_by mergeSort xs => xs.length

splitList_shorter_fst と splitList_shorter_snd はどちらも xs.length ≥ 2 の証明を必要とするため、どちらの証明も失敗します：

unsolved goals
case h
α : Type ?u.37732
inst✝ : Ord α
xs : List α
h : ¬List.length xs < 2
halves : List α × List α := splitList xs
⊢ List.length xs ≥ 2

これが証明を完成させることを確認するために、sorry を使いエラーになるかチェックします：

def mergeSort [Ord α] (xs : List α) : List α :=
  if h : xs.length < 2 then
    match xs with
    | [] => []
    | [x] => [x]
  else
    let halves := splitList xs
    have : xs.length ≥ 2 := by sorry
    have : halves.fst.length < xs.length := by
      apply splitList_shorter_fst
      assumption
    have : halves.snd.length < xs.length := by
      apply splitList_shorter_snd
      assumption
    merge (mergeSort halves.fst) (mergeSort halves.snd)
termination_by mergeSort xs => xs.length

ここでも警告のみとなります。

declaration uses 'sorry'

ここで有力な仮定が1つあります：if によって得られる h : ¬List.length xs < 2 です。明らかに、xs.length < 2 でなければ xs.length ≥ 2 となります。Leanのライブラリにはこの定理を Nat.ge_of_not_lt という名前で提供しています。これでプログラムが完成します：

def mergeSort [Ord α] (xs : List α) : List α :=
  if h : xs.length < 2 then
    match xs with
    | [] => []
    | [x] => [x]
  else
    let halves := splitList xs
    have : xs.length ≥ 2 := by
      apply Nat.ge_of_not_lt
      assumption
    have : halves.fst.length < xs.length := by
      apply splitList_shorter_fst
      assumption
    have : halves.snd.length < xs.length := by
      apply splitList_shorter_snd
      assumption
    merge (mergeSort halves.fst) (mergeSort halves.snd)
termination_by mergeSort xs => xs.length

この関数は以下のような例でテストできます：

#eval mergeSort ["soapstone", "geode", "mica", "limestone"]

["geode", "limestone", "mica", "soapstone"]

#eval mergeSort [5, 3, 22, 15]

[3, 5, 15, 22]

割り算が引き算の繰り返しであること

掛け算が足し算の繰り返しであり、累乗が掛け算の繰り返しであるように、割り算は引き算の繰り返しとして理解することができます。本書における再帰関数の最初の説明 では、除数が0でないときに停止する割り算を紹介していますが、Leanはこれを受け入れません。割り算が終了することを証明するためには、不等式に関する事実を使用する必要があります。

最初のステップは割り算についての定義を改めることで、これによって除数が0でないことの根拠が求められます：

def div (n k : Nat) (ok : k > 0) : Nat :=
  if n < k then
    0
  else
    1 + div (n - k) k ok

このエラーメッセージは追加の引数によっていくぶん長いですが、本質的には以下と同じ内容です：

fail to show termination for
  div
with errors
argument #1 was not used for structural recursion
  failed to eliminate recursive application
    div (n - k) k ok

argument #2 was not used for structural recursion
  failed to eliminate recursive application
    div (n - k) k ok

argument #3 was not used for structural recursion
  application type mismatch
    @Nat.le.brecOn (Nat.succ 0) fun k ok => Nat → Nat
  argument
    fun k ok => Nat → Nat
  has type
    (k : Nat) → k > 0 → Type : Type 1
  but is expected to have type
    (a : Nat) → Nat.le (Nat.succ 0) a → Prop : Type

structural recursion cannot be used

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

この div の定義は最初の引数 n が再帰呼び出しのたびに小さくなることから停止します。これは termination_by 節を使うことで表現されます：

def div (n k : Nat) (ok : k > 0) : Nat :=
  if h : n < k then
    0
  else
    1 + div (n - k) k ok
termination_by div n k ok => n

これで、エラーは再帰呼び出しに限定されるようになります：

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
n k : Nat
ok : k > 0
h : ¬n < k
⊢ n - k < n

これは標準ライブラリの定理 Nat.sub_lt を使って証明することができます。この定理は ∀ {n k : Nat}, 0 < n → 0 < k → n - k < n ということを述べています（波括弧は n と k が暗黙の引数であることを示しています）。この定理を使うには n と k の両方が0よりも大きいことを証明する必要があります。k > 0 は 0 < k の糖衣構文であるため、必要なのは 0 < n を示すことだけです。これには2つの場合があります：n が 0 であるか、ある他の Nat n' に対して n' + 1 であるかです。しかし n は 0 ではありえません。if による2つ目の分岐は ¬ n < k を意味しますが、もし n = 0 で k > 0 であれば n は k よりも小さいはずであり、これは矛盾になります。これにより n = Nat.succ n' であり、Nat.succ n' は明らかに 0 より大きくなります。

停止についての証明も含めた div の完全な定義は以下になります：

def div (n k : Nat) (ok : k > 0) : Nat :=
  if h : n < k then
    0
  else
    have : 0 < n := by
      cases n with
      | zero => contradiction
      | succ n' => simp_arith
    have : n - k < n := by
      apply Nat.sub_lt <;> assumption
    1 + div (n - k) k ok
termination_by div n k ok => n

演習問題

以下の定理を証明してください：

• 全ての整数 \( n \) について \( 0 < n + 1 \) である。
• 全ての整数 \( n \) について \( 0 \leq n \) である。
• 全ての整数 \( n \) と \( k \) について \( (n + 1) - (k + 1) = n - k \) である。
• 全ての整数 \( n \) と \( k \) について、もし \( k < n \) ならば \( n \neq 0 \) である。
• 全ての整数 \( n \) について \( n - n = 0 \) である。
• 全ての整数 \( n \) と \( k \) について、もし \( n + 1 < k \) ならば \( n < k \) である。