8.2. 동치성 증명하기
꼬리 재귀와 누산기를 사용하도록 다시 작성된 프로그램은 원래 프로그램과 상당히 다르게 보일 수 있습니다. 원래의 재귀 함수는 이해하기가 훨씬 쉬운 경우가 많지만, 실행 시점에 스택을 소진할 위험이 있습니다. 프로그램의 두 버전을 예제로 테스트하여 단순한 버그를 배제한 후에는, 증명을 사용하여 두 프로그램이 동등하다는 것을 한 번에 완전히 보일 수 있습니다.
8.2.1. sum이 같음을 증명하기
sum의 두 버전이 동일함을 증명하려면, 먼저 스텁 증명과 함께 정리 명제를 작성하는 것으로 시작합니다.
theorem non_tail_sum_eq_tail_sum : NonTail.sum = Tail.sum := ⊢ NonTail.sum = Tail.sum
⊢ NonTail.sum = Tail.sum예상대로 Lean은 해결되지 않은 목표를 설명합니다:
NonTail.sum과 Tail.sum은 정의적으로 동일하지 않기 때문에 여기서는 rfl 택틱을 적용할 수 없습니다. 하지만 함수는 정의적 동등성 외에도 더 다양한 방식으로 같을 수 있습니다. 두 함수가 동일한 입력에 대해 동일한 출력을 산출한다는 것을 증명함으로써 두 함수가 같다는 것을 증명하는 것도 가능합니다. 다시 말해, 가능한 모든 입력 x에 대해 f(x) = g(x)임을 증명함으로써 f = g를 증명할 수 있습니다. 이 원칙을 함수 외연성이라고 부릅니다. 함수 외연성은 NonTail.sum이 Tail.sum과 같은 이유를 정확히 설명해 줍니다. 둘 다 숫자 리스트의 합을 구하기 때문입니다.
Lean의 택틱 언어에서 함수 외연성은 funext를 사용하여 호출하며, 그 뒤에는 임의의 인자에 사용할 이름을 붙입니다. 임의의 인자는 컨텍스트에 가정으로 추가되며, 목표는 이 인자에 적용된 함수들이 서로 같다는 증명을 요구하도록 바뀝니다:
theorem non_tail_sum_eq_tail_sum : NonTail.sum = Tail.sum := ⊢ NonTail.sum = Tail.sum
xs:List Nat⊢ NonTail.sum xs = Tail.sum xs
이 목표는 인자 xs에 대한 귀납법으로 증명할 수 있습니다. sum 함수는 둘 다 빈 리스트에 적용되면 기저 사례 역할을 하는 0을 반환합니다. 입력 목록의 맨 앞에 숫자를 추가하면 두 함수 모두 결과에 그 숫자를 더하게 되며, 이는 귀납 단계 역할을 합니다. induction 택틱을 호출하면 두 개의 목표가 생성됩니다:
theorem non_tail_sum_eq_tail_sum : NonTail.sum = Tail.sum := ⊢ NonTail.sum = Tail.sum
xs:List Nat⊢ NonTail.sum xs = Tail.sum xs
induction xs with
⊢ NonTail.sum [] = Tail.sum []
y:Natys:List Natih:NonTail.sum ys = Tail.sum ys⊢ NonTail.sum (y :: ys) = Tail.sum (y :: ys)
nil에 대한 기저 사례(base case)는 rfl을 사용하여 해결할 수 있습니다. 두 함수 모두 빈 리스트가 주어졌을 때 0을 반환하기 때문입니다:
theorem non_tail_sum_eq_tail_sum : NonTail.sum = Tail.sum := ⊢ NonTail.sum = Tail.sum
xs:List Nat⊢ NonTail.sum xs = Tail.sum xs
induction xs with
⊢ NonTail.sum [] = Tail.sum [] All goals completed! 🐙
y:Natys:List Natih:NonTail.sum ys = Tail.sum ys⊢ NonTail.sum (y :: ys) = Tail.sum (y :: ys)
귀납 단계를 해결하는 첫 단계는 목표를 단순화하는 것으로, simp에게 NonTail.sum과 Tail.sum을 펼치도록 요청합니다:
theorem non_tail_sum_eq_tail_sum : NonTail.sum = Tail.sum := ⊢ NonTail.sum = Tail.sum
xs:List Nat⊢ NonTail.sum xs = Tail.sum xs
induction xs with
⊢ NonTail.sum [] = Tail.sum [] All goals completed! 🐙
y:Natys:List Natih:NonTail.sum ys = Tail.sum ys⊢ NonTail.sum (y :: ys) = Tail.sum (y :: ys)
Tail.sum을 펼쳐 보면 즉시 Tail.sumHelper에 위임함을 알 수 있는데, 이 또한 단순화해야 합니다.
theorem non_tail_sum_eq_tail_sum : NonTail.sum = Tail.sum := ⊢ NonTail.sum = Tail.sum
xs:List Nat⊢ NonTail.sum xs = Tail.sum xs
induction xs with
⊢ NonTail.sum [] = Tail.sum [] All goals completed! 🐙
y:Natys:List Natih:NonTail.sum ys = Tail.sum ys⊢ NonTail.sum (y :: ys) = Tail.sum (y :: ys)
결과 목표에서, sumHelper는 계산을 한 단계 진행하여 y를 누산기에 더했습니다:
귀납 가설을 이용해 다시 쓰면 목표에서 NonTail.sum에 대한 언급이 모두 제거됩니다:
theorem non_tail_sum_eq_tail_sum : NonTail.sum = Tail.sum := ⊢ NonTail.sum = Tail.sum
xs:List Nat⊢ NonTail.sum xs = Tail.sum xs
induction xs with
⊢ NonTail.sum [] = Tail.sum [] All goals completed! 🐙
y:Natys:List Natih:NonTail.sum ys = Tail.sum ys⊢ NonTail.sum (y :: ys) = Tail.sum (y :: ys)
이 새로운 목표는 리스트의 합에 어떤 수를 더하는 것이 그 수를 sumHelper의 초기 누산기로 사용하는 것과 같다는 것을 나타냅니다. 명확성을 위해, 이 새로운 목표는 별도의 정리로 증명할 수 있습니다:
theorem helper_add_sum_accum (xs : List Nat) (n : Nat) :
n + Tail.sum xs = Tail.sumHelper n xs := xs:List Natn:Nat⊢ n + Tail.sum xs = Tail.sumHelper n xs
xs:List Natn: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 := xs:List Natn:Nat⊢ n + Tail.sum xs = Tail.sumHelper n xs
induction xs with
n:Nat⊢ n + Tail.sum [] = Tail.sumHelper n [] All goals completed! 🐙
n:Naty:Natys:List Natih: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 := xs:List Natn:Nat⊢ n + Tail.sum xs = Tail.sumHelper n xs
induction xs with
n:Nat⊢ n + Tail.sum [] = Tail.sumHelper n [] All goals completed! 🐙
n:Naty:Natys:List Natih:n + Tail.sum ys = Tail.sumHelper n ys⊢ n + Tail.sum (y :: ys) = Tail.sumHelper n (y :: ys)
이상적으로는 귀납 가설을 사용하여 Tail.sumHelper (y + n) ys를 대체할 수 있어야 하지만, 둘은 일치하지 않습니다. 귀납 가설은 Tail.sumHelper (y + n) ys가 아니라 Tail.sumHelper n ys에 대해 사용할 수 있습니다. 다시 말해, 이 증명은 막혀 있습니다.
8.2.2. 두 번째 시도
증명을 억지로 헤쳐 나가려 하기보다는, 한 걸음 물러나 생각해 볼 시점입니다. 왜 이 함수의 꼬리 재귀 버전이 꼬리 재귀가 아닌 버전과 같은 것일까요? 근본적으로 말하면, 리스트의 각 항목에서 누산기는 재귀의 결과에 더해졌을 양만큼 증가합니다. 이 통찰을 사용하면 우아한 증명을 작성할 수 있습니다. 결정적으로, 귀납법에 의한 증명은 귀납 가설이 어떤 누산기 값에도 적용될 수 있도록 설정되어야 합니다.
이전 시도를 버리고, 이 통찰을 다음과 같은 명제로 표현할 수 있습니다:
theorem non_tail_sum_eq_helper_accum (xs : List Nat) :
(n : Nat) → n + NonTail.sum xs = Tail.sumHelper n xs := xs:List Nat⊢ ∀ (n : Nat), n + NonTail.sum xs = Tail.sumHelper n xs
xs:List Nat⊢ ∀ (n : Nat), n + NonTail.sum xs = Tail.sumHelper n xs
이 명제에서 n이 콜론 뒤에 오는 타입의 일부라는 점이 매우 중요합니다. 결과 목표는 “모든 n에 대해”의 줄임말인 ∀ (n : Nat)로 시작합니다:
induction 택틱을 사용하면 이 "모든 ~에 대하여" 문장을 포함하는 목표가 생성됩니다:
theorem non_tail_sum_eq_helper_accum (xs : List Nat) :
(n : Nat) → n + NonTail.sum xs = Tail.sumHelper n xs := xs:List Nat⊢ ∀ (n : Nat), n + NonTail.sum xs = Tail.sumHelper n xs
induction xs with
⊢ ∀ (n : Nat), n + NonTail.sum [] = Tail.sumHelper n []
y:Natys:List Natih:∀ (n : Nat), n + NonTail.sum ys = Tail.sumHelper n ys⊢ ∀ (n : Nat), n + NonTail.sum (y :: ys) = Tail.sumHelper n (y :: ys)
nil 경우, 목표는 다음과 같습니다:
cons에 대한 귀납 단계에서, 귀납 가설과 특정 목표 모두 "모든 n에 대해"를 포함합니다:
다시 말해, 목표는 증명하기 더 어려워졌지만, 귀납 가설은 그에 상응하여 더 유용해졌습니다.
"모든 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 := xs:List Nat⊢ ∀ (n : Nat), n + NonTail.sum xs = Tail.sumHelper n xs
induction xs with
⊢ ∀ (n : Nat), n + NonTail.sum [] = Tail.sumHelper n []
y:Natys:List Natih:∀ (n : Nat), n + NonTail.sum ys = Tail.sumHelper n ys⊢ ∀ (n : Nat), n + NonTail.sum (y :: ys) = Tail.sumHelper n (y :: ys)
이 명제적 동등성의 양변은 정의상 n과 동일하므로, rfl이면 충분합니다:
theorem non_tail_sum_eq_helper_accum (xs : List Nat) :
(n : Nat) → n + NonTail.sum xs = Tail.sumHelper n xs := xs:List Nat⊢ ∀ (n : Nat), n + NonTail.sum xs = Tail.sumHelper n xs
induction xs with
⊢ ∀ (n : Nat), n + NonTail.sum [] = Tail.sumHelper n []
n:Nat⊢ n + NonTail.sum [] = Tail.sumHelper n []
All goals completed! 🐙
y:Natys:List Natih:∀ (n : Nat), n + NonTail.sum ys = Tail.sumHelper n ys⊢ ∀ (n : Nat), n + NonTail.sum (y :: ys) = Tail.sumHelper n (y :: ys)
cons 목표에도 "모든 ~에 대해"가 포함되어 있습니다:
이는 intro의 사용을 제안합니다.
theorem non_tail_sum_eq_helper_accum (xs : List Nat) :
(n : Nat) → n + NonTail.sum xs = Tail.sumHelper n xs := xs:List Nat⊢ ∀ (n : Nat), n + NonTail.sum xs = Tail.sumHelper n xs
induction xs with
⊢ ∀ (n : Nat), n + NonTail.sum [] = Tail.sumHelper n []
n:Nat⊢ n + NonTail.sum [] = Tail.sumHelper n []
All goals completed! 🐙
y:Natys:List Natih:∀ (n : Nat), n + NonTail.sum ys = Tail.sumHelper n ys⊢ ∀ (n : Nat), n + NonTail.sum (y :: ys) = Tail.sumHelper n (y :: ys)
이제 증명 목표에는 y :: ys에 적용된 NonTail.sum과 Tail.sumHelper가 모두 포함되어 있습니다. 단순화기(simplifier)를 사용하면 다음 단계를 더 명확하게 만들 수 있습니다:
theorem non_tail_sum_eq_helper_accum (xs : List Nat) :
(n : Nat) → n + NonTail.sum xs = Tail.sumHelper n xs := xs:List Nat⊢ ∀ (n : Nat), n + NonTail.sum xs = Tail.sumHelper n xs
induction xs with
⊢ ∀ (n : Nat), n + NonTail.sum [] = Tail.sumHelper n []
n:Nat⊢ n + NonTail.sum [] = Tail.sumHelper n []
All goals completed! 🐙
y:Natys:List Natih:∀ (n : Nat), n + NonTail.sum ys = Tail.sumHelper n ys⊢ ∀ (n : Nat), n + NonTail.sum (y :: ys) = Tail.sumHelper n (y :: ys)이 목표는 귀납 가정과 일치하는 것에 매우 가깝습니다. 일치하지 않는 경우는 두 가지가 있습니다:
-
등식의 좌변은
n + (y + NonTail.sum ys)이지만, 귀납 가정은 좌변이NonTail.sum ys에 어떤 수를 더한 형태일 것을 필요로 합니다. 다시 말해, 이 목표는(n + y) + NonTail.sum ys로 다시 써야 하는데, 자연수 덧셈은 결합 법칙을 만족하므로 이는 타당합니다. -
왼쪽이
(y + n) + 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 택틱에는 그 타입이 등식인 표현식이 제공됩니다. 하지만 인자가 반환 타입이 동등성인 의존 함수인 경우에는, 그 동등성이 목표에 있는 무언가와 일치하도록 만들 수 있는 함수의 인자를 찾으려 시도합니다. 결합법칙을 적용할 기회는 단 한 번뿐이지만, (n + m) + k = n + (m + k)에서 등식의 오른쪽이 증명 목표와 일치하는 쪽이기 때문에 재작성의 방향을 반대로 해야 합니다.
theorem non_tail_sum_eq_helper_accum (xs : List Nat) :
(n : Nat) → n + NonTail.sum xs = Tail.sumHelper n xs := xs:List Nat⊢ ∀ (n : Nat), n + NonTail.sum xs = Tail.sumHelper n xs
induction xs with
⊢ ∀ (n : Nat), n + NonTail.sum [] = Tail.sumHelper n []
n:Nat⊢ n + NonTail.sum [] = Tail.sumHelper n []
All goals completed! 🐙
y:Natys:List Natih:∀ (n : Nat), n + NonTail.sum ys = Tail.sumHelper n ys⊢ ∀ (n : Nat), n + NonTail.sum (y :: ys) = Tail.sumHelper n (y :: ys)
하지만 rw [Nat.add_comm]로 직접 다시 쓰면 잘못된 결과로 이어집니다. rw 택틱은 재작성 위치를 잘못 추측하여, 의도하지 않은 목표로 이어집니다:
theorem non_tail_sum_eq_helper_accum (xs : List Nat) :
(n : Nat) → n + NonTail.sum xs = Tail.sumHelper n xs := xs:List Nat⊢ ∀ (n : Nat), n + NonTail.sum xs = Tail.sumHelper n xs
induction xs with
⊢ ∀ (n : Nat), n + NonTail.sum [] = Tail.sumHelper n []
n:Nat⊢ n + NonTail.sum [] = Tail.sumHelper n []
All goals completed! 🐙
y:Natys:List Natih:∀ (n : Nat), n + NonTail.sum ys = Tail.sumHelper n ys⊢ ∀ (n : Nat), n + NonTail.sum (y :: ys) = Tail.sumHelper n (y :: 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 := xs:List Nat⊢ ∀ (n : Nat), n + NonTail.sum xs = Tail.sumHelper n xs
induction xs with
⊢ ∀ (n : Nat), n + NonTail.sum [] = Tail.sumHelper n []
n:Nat⊢ n + NonTail.sum [] = Tail.sumHelper n []
All goals completed! 🐙
y:Natys:List Natih:∀ (n : Nat), n + NonTail.sum ys = Tail.sumHelper n ys⊢ ∀ (n : Nat), n + NonTail.sum (y :: 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 := xs:List Nat⊢ ∀ (n : Nat), n + NonTail.sum xs = Tail.sumHelper n xs
induction xs with
⊢ ∀ (n : Nat), n + NonTail.sum [] = Tail.sumHelper n [] n:Nat⊢ n + NonTail.sum [] = Tail.sumHelper n []; All goals completed! 🐙
y:Natys:List Natih:∀ (n : Nat), n + NonTail.sum ys = Tail.sumHelper n ys⊢ ∀ (n : Nat), n + NonTail.sum (y :: ys) = Tail.sumHelper n (y :: ys)
y:Natys:List Natih:∀ (n : Nat), n + NonTail.sum ys = Tail.sumHelper n ysn:Nat⊢ n + NonTail.sum (y :: ys) = Tail.sumHelper n (y :: ys)
y:Natys:List Natih:∀ (n : Nat), n + NonTail.sum ys = Tail.sumHelper n ysn:Nat⊢ n + (y + NonTail.sum ys) = Tail.sumHelper (y + n) ys
y:Natys:List Natih:∀ (n : Nat), n + NonTail.sum ys = Tail.sumHelper n ysn:Nat⊢ n + y + NonTail.sum ys = Tail.sumHelper (y + n) ys
y:Natys:List Natih:∀ (n : Nat), n + NonTail.sum ys = Tail.sumHelper n ysn:Nat⊢ n + y + NonTail.sum ys = Tail.sumHelper (n + y) ys
All goals completed! 🐙실제 증명은 목표가 헬퍼의 타입과 일치하도록 만드는 데 약간의 추가 작업만 필요합니다. 첫 번째 단계는 여전히 함수 외연성을 사용하는 것입니다:
theorem non_tail_sum_eq_tail_sum : NonTail.sum = Tail.sum := ⊢ NonTail.sum = Tail.sum
xs:List Nat⊢ NonTail.sum xs = Tail.sum xs
다음 단계는 Tail.sum을 펼쳐서 Tail.sumHelper를 드러내는 것입니다:
theorem non_tail_sum_eq_tail_sum : NonTail.sum = Tail.sum := ⊢ NonTail.sum = Tail.sum
xs:List Nat⊢ NonTail.sum xs = Tail.sum xs
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 타입이 산출됩니다. 표준 라이브러리의 또 다른 증명인 Nat.zero_add는 (n : Nat) → 0 + n = n 타입을 가집니다. NonTail.sum xs에 이 함수를 적용하면 0 + NonTail.sum xs = NonTail.sum xs 타입의 식이 나오므로, 오른쪽에서 왼쪽으로 다시 쓰면 원하는 목표에 도달합니다.
theorem non_tail_sum_eq_tail_sum : NonTail.sum = Tail.sum := ⊢ NonTail.sum = Tail.sum
xs:List Nat⊢ NonTail.sum xs = Tail.sum xs
xs:List Nat⊢ NonTail.sum xs = Tail.sumHelper 0 xs
xs:List Nat⊢ 0 + NonTail.sum xs = Tail.sumHelper 0 xs마지막으로, 이 보조 정리를 사용하여 증명을 완성할 수 있습니다:
theorem non_tail_sum_eq_tail_sum : NonTail.sum = Tail.sum := ⊢ NonTail.sum = Tail.sum
xs:List Nat⊢ NonTail.sum xs = Tail.sum xs
xs:List Nat⊢ NonTail.sum xs = Tail.sumHelper 0 xs
xs:List Nat⊢ 0 + NonTail.sum xs = Tail.sumHelper 0 xs
All goals completed! 🐙
이 증명은 누산기를 전달하는 꼬리 재귀 함수가 꼬리 재귀가 아닌 버전과 같음을 증명할 때 사용할 수 있는 일반적인 패턴을 보여줍니다. 첫 번째 단계는 시작 누산기 인자와 최종 결과 사이의 관계를 발견하는 것입니다. 예를 들어, Tail.sumHelper를 n이라는 누산기로 시작하면 최종 합계가 n에 더해지는 결과가 나오고, Tail.reverseHelper를 ys라는 누산기로 시작하면 최종적으로 뒤집힌 목록이 ys 앞에 붙는 결과가 나옵니다. 두 번째 단계는 이 관계를 정리 명제로 작성하고 귀납법으로 증명하는 것입니다. 실제로는 누산기가 항상 0 또는 []와 같은 중립적인 값으로 초기화되지만, 시작 누산기가 임의의 값이 될 수 있도록 허용하는 이 더 일반적인 진술이 충분히 강력한 귀납 가설을 얻는 데 필요한 것입니다. 마지막으로, 이 보조 정리를 실제 초기 누산기 값과 함께 사용하면 원하는 증명을 얻을 수 있습니다. 예를 들어, non_tail_sum_eq_tail_sum에서는 누산기가 0으로 지정되어 있습니다. 이는 중립적인 초기 누산기 값이 올바른 위치에 오도록 목표를 다시 작성해야 할 수도 있습니다.
8.2.3. 함수적 귀납법
non_tail_sum_eq_helper_accum의 증명은 Tail.sumHelper의 구현을 그대로 따릅니다. 그러나 구현과 수학적 귀납법이 기대하는 구조가 완벽하게 일치하지는 않으므로, 가정 n을 신중하게 관리해야 합니다. non_tail_sum_eq_helper_accum의 경우에는 이것이 적은 양의 작업이지만, 정의가 induction이 기대하는 구조에서 더 멀리 떨어진 함수에 대한 증명은 더 많은 부기 작업을 필요로 합니다.
인자 중 하나에 대한 귀납법으로 재귀 함수에 대한 정리를 증명하는 것 외에도, Lean은 함수의 재귀 호출 구조에 대한 귀납법을 이용한 증명을 지원합니다. 이 함수형 귀납은 재귀 호출을 포함하지 않는 함수의 제어 흐름의 각 분기에 대해서는 기저 사례를, 재귀 호출을 포함하는 각 분기에 대해서는 귀납 단계를 만들어냅니다. 함수적 귀납법을 이용한 증명은 재귀가 아닌 분기에 대해 정리가 성립함을 보여야 하며, 각 재귀 호출의 결과에 대해 정리가 성립한다면 재귀 분기의 결과에 대해서도 정리가 성립함을 보여야 합니다.
함수적 귀납법을 사용하면 non_tail_sum_eq_helper_accum을 단순화할 수 있습니다:
theorem non_tail_sum_eq_helper_accum (xs : List Nat) (n : Nat) :
n + NonTail.sum xs = Tail.sumHelper n xs := xs:List Natn:Nat⊢ n + NonTail.sum xs = Tail.sumHelper n xs
fun_induction Tail.sumHelper with
n:Nat⊢ n + NonTail.sum [] = n
n:Naty:Natys:List Natih:y + n + NonTail.sum ys = Tail.sumHelper (y + n) ys⊢ n + NonTail.sum (y :: ys) = Tail.sumHelper (y + n) ys
증명의 각 분기는 Tail.sumHelper의 해당 분기와 일치합니다:
def Tail.sumHelper (soFar : Nat) : List Nat → Nat
| [] => soFar
| x :: xs => sumHelper (x + soFar) xs
첫 번째인 case1에서 등식의 우변은 누산기 값이며, 증명에서는 n이라고 부릅니다:
두 번째, case2에서 등식의 오른쪽 변은 꼬리 재귀 루프의 다음 단계입니다:
그 결과로 얻어지는 증명은 더 단순할 수 있습니다. 사용된 덧셈의 성질을 포함하여 논증의 근본은 동일하지만, 부기 작업은 제거되었습니다. 이제 누산기 값을 수동으로 다룰 필요가 없으며, 귀납 가설을 인스턴스화할 필요 없이 직접 사용할 수 있습니다:
theorem non_tail_sum_eq_helper_accum (xs : List Nat) (n : Nat) :
n + NonTail.sum xs = Tail.sumHelper n xs := xs:List Natn:Nat⊢ n + NonTail.sum xs = Tail.sumHelper n xs
fun_induction Tail.sumHelper with
n:Nat⊢ n + NonTail.sum [] = n All goals completed! 🐙
n:Naty:Natys:List Natih:y + n + NonTail.sum ys = Tail.sumHelper (y + n) ys⊢ n + NonTail.sum (y :: ys) = Tail.sumHelper (y + n) ys
n:Naty:Natys:List Natih:y + n + NonTail.sum ys = Tail.sumHelper (y + n) ys⊢ n + (y + NonTail.sum ys) = Tail.sumHelper (y + n) ys
n:Naty:Natys:List Natih:y + n + NonTail.sum ys = Tail.sumHelper (y + n) ys⊢ n + y + NonTail.sum ys = Tail.sumHelper (y + n) ys
n:Naty:Natys:List Natih:y + n + NonTail.sum ys = Tail.sumHelper (y + n) ys⊢ y + n + NonTail.sum ys = Tail.sumHelper (y + n) ys
All goals completed! 🐙
grind 택틱은 이런 종류의 목표에 매우 잘 어울립니다. simp나 rw와 달리, 이 택틱은 방향성을 가지지 않습니다. 내부적으로는 목표를 완전히 증명하거나 증명에 실패할 때까지 사실들의 모음을 누적합니다. 이는 덧셈의 결합법칙과 교환법칙 같은 산술에 관한 기본 사실을 사용하도록 미리 구성되어 있으며, 귀납 가설과 같은 지역 가정을 자동으로 사용합니다. grind를 사용하면, 이 증명은 짧고 요점만 담게 됩니다:
theorem non_tail_sum_eq_helper_accum (xs : List Nat) (n : Nat) :
n + NonTail.sum xs = Tail.sumHelper n xs := xs:List Natn:Nat⊢ n + NonTail.sum xs = Tail.sumHelper n xs
soFar✝:Nat⊢ soFar✝ + NonTail.sum [] = soFar✝soFar✝:Natx✝:Natxs✝:List Natih1✝:x✝ + soFar✝ + NonTail.sum xs✝ = Tail.sumHelper (x✝ + soFar✝) xs✝⊢ soFar✝ + NonTail.sum (x✝ :: xs✝) = Tail.sumHelper (x✝ + soFar✝) xs✝ soFar✝:Nat⊢ soFar✝ + NonTail.sum [] = soFar✝soFar✝:Natx✝:Natxs✝:List Natih1✝:x✝ + soFar✝ + NonTail.sum xs✝ = Tail.sumHelper (x✝ + soFar✝) xs✝⊢ soFar✝ + NonTail.sum (x✝ :: xs✝) = Tail.sumHelper (x✝ + soFar✝) xs✝ All goals completed! 🐙
이 증명은 또한 숙련된 프로그래머에게 증명을 설명하는 방식과도 일치합니다: "그냥 Tail.sumHelper의 두 분기를 모두 확인하면 됩니다!"
8.2.4. 연습문제
8.2.4.1. 준비 운동
induction 택틱을 사용하여 Nat.zero_add, Nat.add_assoc, Nat.add_comm에 대한 증명을 직접 작성하십시오.
8.2.4.2. 더 많은 누산기 증명
8.2.4.2.1. 리스트 뒤집기
sum에 대한 증명을 NonTail.reverse와 Tail.reverse에 대한 증명으로 응용하십시오. 첫 번째 단계는 Tail.reverseHelper에 전달되는 누산기 값과 꼬리 재귀가 아닌 reverse 사이의 관계에 대해 생각해 보는 것입니다. Tail.sumHelper에서 누산기에 숫자를 더하는 것이 전체 합계에 숫자를 더하는 것과 마찬가지로, Tail.reverseHelper에서 List.cons를 사용하여 누산기에 새 항목을 추가하는 것은 전체 결과에 대한 어떤 변경과 동등합니다. 관계가 명확해질 때까지 연필과 종이로 서너 가지 다른 누산기 값을 시도해 보십시오. 이 관계를 사용하여 적절한 보조 정리를 증명하십시오. 이 보조 정리를 리스트에 대한 귀납법과 함수형 귀납법을 모두 사용하여 증명해 보십시오. 그런 다음, 전체 정리를 작성합니다. NonTail.reverse와 Tail.reverse는 다형적이므로, 이들의 동등성을 서술하려면 Lean이 α에 어떤 타입을 사용할지 알아내려는 것을 막기 위해 @를 사용해야 합니다. α를 일반 인자로 취급하고 나면, funext는 α와 xs 둘 다에 대해 호출되어야 합니다:
theorem non_tail_reverse_eq_tail_reverse :
@NonTail.reverse = @Tail.reverse := ⊢ @NonTail.reverse = @Tail.reverse
α:Type u_1xs:List α⊢ NonTail.reverse xs = Tail.reverse xs이렇게 하면 적절한 목표가 만들어집니다:
8.2.4.2.2. 팩토리얼
이전 절의 연습문제에 등장한 NonTail.factorial이 여러분의 꼬리 재귀 풀이와 동일함을, 누산기와 결과 사이의 관계를 찾고 적절한 보조 정리를 증명함으로써 증명하십시오.