8.4.1. 병합 정렬🔗

종료 증명이 자명하지 않은 함수의 한 예로 List에 대한 병합 정렬이 있습니다. 병합 정렬은 두 단계로 구성됩니다. 먼저 리스트를 절반으로 나눕니다. 각 절반은 병합 정렬(merge sort)을 사용하여 정렬된 후, 두 개의 정렬된 리스트를 더 큰 정렬된 리스트로 합치는 함수를 사용하여 결과가 병합됩니다. 기저 사례는 빈 리스트와 단일 원소 리스트이며, 둘 다 이미 정렬된 것으로 간주됩니다.

정렬된 두 리스트를 병합하려면 고려해야 할 두 가지 기본 경우가 있습니다:

1. 입력 목록 중 하나가 비어 있으면, 결과는 다른 목록이 됩니다.

2. 두 리스트가 모두 비어 있지 않다면, 두 리스트의 머리를 비교해야 합니다. 함수의 결과는 두 머리 중 더 작은 것 다음에 두 리스트의 나머지 항목들을 병합한 결과가 이어진 것입니다.

이것은 두 리스트 중 어느 쪽에 대해서도 구조적으로 재귀적이지 않습니다. 이 재귀는 각 재귀 호출마다 두 리스트 중 하나에서 항목이 제거되기 때문에 종료되지만, 어느 리스트에서 제거될지는 정해져 있지 않습니다. 내부적으로 Lean은 이 사실을 이용해 종료함을 증명합니다:

리스트를 분할하는 간단한 방법은 입력 리스트의 각 항목을 두 개의 출력 리스트에 번갈아 추가하는 것입니다:

이 분할 함수는 구조적 재귀 함수입니다.

병합 정렬은 기저 사례에 도달했는지 확인합니다. 만약 그렇다면, 입력 리스트를 반환합니다. 그렇지 않다면, 입력을 분할하고 각 절반을 정렬한 결과를 병합합니다.

Lean의 패턴 매칭 컴파일러는 xs.length < 2인지 검사하는 if가 도입한 가정 h가 항목이 하나보다 긴 리스트를 배제한다는 것을 알아낼 수 있으므로, "누락된 경우" 오류가 발생하지 않습니다. 하지만 이 프로그램이 항상 종료하더라도, 이는 구조적 재귀가 아니며 Lean은 감소하는 척도를 자동으로 찾아낼 수 없습니다:

fail to show termination for
  mergeSort
with errors
failed to infer structural recursion:
Not considering parameter α of mergeSort:
  it is unchanged in the recursive calls
Not considering parameter #2 of mergeSort:
  it is unchanged in the recursive calls
Cannot use parameter xs:
  failed to eliminate recursive application
    mergeSort halves.fst


Could not find a decreasing measure.
The basic measures relate at each recursive call as follows:
(<, ≤, =: relation proved, ? all proofs failed, _: no proof attempted)
            xs #1
1) 70:11-31  ?  ?
2) 70:34-54  _  _

#1: xs.length

Please use `termination_by` to specify a decreasing measure.

이것이 종료되는 이유는 splitList가 항상 입력보다 짧은 리스트를 반환하기 때문이며, 이는 적어도 원소가 두 개 이상인 리스트에 적용될 때 성립합니다. 따라서 halves.fst와 halves.snd의 길이는 xs의 길이보다 작습니다. 이는 termination_by 절을 사용하여 표현할 수 있습니다:

이 절을 사용하면 오류 메시지가 달라집니다. 함수가 구조적으로 재귀적이지 않다고 불평하는 대신, 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_1xs:List αh:¬xs.length < 2halves:List α × List α := splitList xs⊢ (splitList xs).fst.length < xs.length

8.4.2. 리스트를 나누면 더 짧아집니다🔗

또한 (splitList xs).snd.length < xs.length임을 증명해야 합니다. splitList는 두 리스트에 항목을 번갈아 추가하기 때문에, 두 명제를 한꺼번에 증명하는 것이 가장 쉬우며, 따라서 증명의 구조는 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"])로 평가되며, 이 두 출력 리스트는 모두 입력 리스트보다 짧습니다.

출력 목록의 길이는 항상 입력 목록의 길이보다 작거나 같지만, 입력 목록이 최소 두 개의 항목을 포함할 때만 엄밀하게 더 짧아진다는 사실이 밝혀졌습니다. 전자의 명제를 증명한 다음 이를 후자의 명제로 확장하는 것이 가장 쉬운 것으로 밝혀졌습니다. 정리 서술로 시작합니다:

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

splitList는 리스트에 대해 구조적으로 재귀적이므로, 증명은 귀납법을 사용해야 합니다. splitList의 구조적 재귀는 귀납법에 의한 증명에 완벽히 들어맞습니다: 귀납의 기본 단계는 재귀의 기본 단계와 일치하고, 귀납적 단계는 재귀 호출과 일치합니다. induction 택틱은 두 개의 목표를 제시합니다:

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

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

nil 경우의 목표는 단순화기를 호출하고 splitList의 정의를 펼치도록 지시함으로써 증명할 수 있습니다. 빈 리스트의 길이는 빈 리스트의 길이보다 작거나 같기 때문입니다. 마찬가지로, cons 경우에서 splitList로 단순화하면 목표의 길이들 주위에 Nat.succ가 놓입니다:

unsolved goals
consα:Type u_1x:αxs:List αih:(splitList xs).fst.length ≤ xs.length ∧ (splitList xs).snd.length ≤ xs.length⊢ (splitList xs).snd.length ≤ xs.length ∧ (splitList xs).fst.length ≤ xs.length + 1

이는 List.length 호출이 리스트 x :: xs의 머리를 소비하여 입력 리스트의 길이와 첫 번째 출력 리스트의 길이 모두에서 이를 Nat.succ로 변환하기 때문입니다.

Lean에서 A ∧ B를 작성하는 것은 And A B의 축약형입니다. And는 Prop 유니버스에 있는 구조체 타입입니다:

다시 말해, A ∧ B의 증명은 left 필드에 있는 A의 증명과 right 필드에 있는 B의 증명에 적용된 And.intro 생성자로 구성됩니다.

cases 택틱은 증명에서 데이터타입의 각 생성자 또는 명제의 각 잠재적 증명을 차례로 고려할 수 있게 해 줍니다. 이는 재귀가 없는 match 표현식에 해당합니다. 구조체에 cases를 사용하면, 마치 패턴 매칭 표현식이 프로그램에서 사용할 구조체의 필드를 추출하는 것처럼, 구조체가 분해되어 구조체의 각 필드에 대한 가정이 추가됩니다. 구조체는 생성자가 하나뿐이므로, 구조체에 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라는 가정이 생성됩니다:

unsolved goals
cons.introα:Type u_1x:αxs:List αleft✝:(splitList xs).fst.length ≤ xs.lengthright✝:(splitList xs).snd.length ≤ xs.length⊢ (splitList xs).snd.length ≤ xs.length ∧ (splitList xs).fst.length ≤ xs.length + 1

증명의 목표 또한 And이므로, constructor 택틱을 사용하여 And.intro를 적용할 수 있으며, 이는 각 인자에 대한 목표를 생성합니다:

unsolved goals
cons.intro.leftα:Type u_1x:αxs:List αleft✝:(splitList xs).fst.length ≤ xs.lengthright✝:(splitList xs).snd.length ≤ xs.length⊢ (splitList xs).snd.length ≤ xs.length

cons.intro.rightα:Type u_1x:αxs:List αleft✝:(splitList xs).fst.length ≤ xs.lengthright✝:(splitList xs).snd.length ≤ xs.length⊢ (splitList xs).fst.length ≤ xs.length + 1

left 목표는 left✝ 가정과 동일하므로, assumption 택틱이 이를 해소합니다:

unsolved goals
cons.intro.rightα:Type u_1x:αxs:List αleft✝:(splitList xs).fst.length ≤ xs.lengthright✝:(splitList xs).snd.length ≤ xs.length⊢ (splitList xs).fst.length ≤ xs.length + 1

right 목표는 right✝ 가정과 유사하지만, 목표는 입력 목록의 길이에만 + 1을 더한다는 점이 다릅니다. 이제 부등식이 성립함을 증명할 차례입니다.

unsolved goals
n m:Nat⊢ n ≤ m → n ≤ m + 1

unsolved goals
n m:Nath:n ≤ m⊢ n ≤ m + 1

unsolved goals
refln m:Nat⊢ n ≤ n + 1

unsolved goals
stepn m m✝:Nata✝:n.le m✝ih:n ≤ m✝ + 1⊢ n ≤ m✝.succ + 1