8.4.1. Merge Sort🔗

종료 증명이 간단하지 않은 함수의 한 예는 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. Splitting a List Makes it Shorter🔗

(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