8.4.1. 병합 정렬🔗

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

정렬된 두 리스트를 병합할 때 고려해야 할 기본적인 경우는 두 가지입니다.

1. 입력 리스트 중 하나가 비어 있으면, 결과는 나머지 리스트입니다.

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

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

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

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

병합 정렬은 기저 사례에 도달했는지 확인합니다. 도달했다면 입력 리스트를 반환합니다. 도달하지 않았다면 입력을 나누고, 각 절반을 정렬한 결과를 병합합니다:

Lean의 패턴 매칭 컴파일러는 xs.length < 2인지 검사하는 if가 도입한 가정 h가 원소가 둘 이상인 리스트를 배제한다는 것을 알아낼 수 있으므로, “누락된 경우(missing cases)” 오류가 발생하지 않습니다. 그러나 이 프로그램은 항상 종료하지만 구조적 재귀가 아니며, 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