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에 대한 기저 사례는 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 : Nat)로 시작하며, 이는 “모든 n에 대하여”를 줄여 쓴 것입니다:
귀납(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 목표에도 “모든 ~에 대하여(for all)”가 들어 있습니다:
따라서 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가 모두 들어 있습니다. 단순화기를 사용하면 다음 단계를 더 분명하게 알 수 있습니다:
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이 여러분의 꼬리 재귀 풀이와 같음을 증명하십시오.