8.2. Proving Equivalence
꼬리 재귀와 누산기를 사용하도록 다시 작성한 프로그램은 원래 프로그램과 상당히 달라 보일 수 있다. 원래 재귀 함수가 이해하기 훨씬 쉬운 경우가 많지만 실행 중 스택을 소진할 위험이 있다. 두 프로그램 버전을 예제로 시험해 간단한 버그를 배제한 뒤, 증명을 사용해 두 프로그램이 동치임을 확정적으로 보일 수 있다.
8.2.1. Proving sum Equal
sum의 두 버전이 같음을 증명하려면 먼저 임시 증명을 넣어 정리 명제를 작성한다.
theorem non_tail_sum_eq_tail_sum : NonTail.sum = Tail.sum := ⊢ NonTail.sum = Tail.sum
⊢ NonTail.sum = Tail.sum예상대로 Lean은 미해결 목표를 보여 준다.
rfl 전술은 여기서 적용할 수 없다. NonTail.sum과 Tail.sum이 정의적으로 동등하지 않기 때문이다.
그러나 함수가 같은 방식은 정의적 동등성만 있는 것이 아니다.
같은 입력에 대해 같은 출력을 만든다는 것을 증명해 두 함수가 같음을 보일 수도 있다.
다시 말해 모든 가능한 입력 x에 대해 f(x) = g(x)임을 증명해 f = g를 증명할 수 있다.
이 원리를 함수 외연성(function extensionality)이라고 한다.
함수 외연성이 바로 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 n ys에는 사용할 수 있지만 Tail.sumHelper (y + n) ys에는 사용할 수 없다.
다시 말해 이 증명은 막혔다.
8.2.2. A Second Attempt
증명을 억지로 진행하려 하기보다 한 걸음 물러나 생각해 볼 때다. 꼬리 재귀 버전의 함수가 비꼬리 재귀 버전과 같은 이유는 무엇인가? 근본적으로 리스트의 각 원소에서 누산기는 재귀 결과에 더할 양만큼 똑같이 증가한다. 이 통찰을 사용하면 우아한 증명을 작성할 수 있다. 중요한 점은 귀납 가설을 어떤 누산기 값에도 적용할 수 있도록 귀납 증명을 설정해야 한다는 것이다.
앞의 시도를 버리고 이 통찰을 다음 명제로 표현할 수 있다.
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)으로 시작한다.
귀납 전술을 사용하면 이 “모든 경우” 명제를 포함하는 목표가 생긴다.
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 => ...를 사용하는 것과 같다.
전술 언어에서는 intro 전술로 임의의 x를 선택하며, 전술 스크립트가 끝나면 내부에서 함수를 만들어 낸다.
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가 모두 들어 있다.
단순화기를 사용하면 다음 단계를 더 분명히 볼 수 있다.
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로 다시 써야 하며, 이는 자연수 덧셈이 결합법칙을 따르므로 올바르다. -
왼쪽 항을
(n + y) + NonTail.sum ys로 다시 썼다면 오른쪽 누산기 인자도 일치하도록n + y여야 하며, 원래의y + n과는 다르다. 덧셈도 교환법칙을 따르므로 이 다시 쓰기가 유효하다.
덧셈의 결합법칙과 교환법칙은 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)
y와 n을 Nat.add_comm의 인자로 명시하면 고칠 수 있다.
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. Functional Induction
non_tail_sum_eq_helper_accum의 증명은 Tail.sumHelper 구현을 밀접하게 따른다.
그러나 구현과 수학적 귀납법이 기대하는 구조가 완전히 일치하지 않으므로 n 가정을 주의 깊게 관리해야 한다.
non_tail_sum_eq_helper_accum의 경우에는 작은 작업이지만, 정의가 induction이 기대하는 구조에서 더 멀리 떨어진 함수에 관한 증명은 더 많은 장부 작업이 필요하다.
Lean은 인자 중 하나에 대해 귀납법으로 재귀 함수에 관한 정리를 증명하는 것 외에도 함수의 재귀 호출 구조에 대한 귀납 증명을 지원한다. 이 함수 귀납법(functional induction)은 재귀 호출이 없는 함수 제어 흐름의 각 분기에 기본 경우를, 재귀 호출이 있는 각 분기에 귀납 단계를 만든다. 함수 귀납법에 의한 증명은 비재귀 분기에서 정리가 성립하고, 각 재귀 호출 결과에서 정리가 성립하면 재귀 분기 결과에서도 성립함을 보여야 한다.
함수 귀납법을 사용하면 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. Exercise
8.2.4.1. Warming Up
induction 전술을 사용하여 Nat.zero_add, Nat.add_assoc, Nat.add_comm의 증명을 직접 작성하라.
8.2.4.2. More Accumulator Proofs
8.2.4.2.1. Reversing Lists
sum에 대한 증명을 NonTail.reverse와 Tail.reverse에 대한 증명으로 바꾸어 작성하라.
첫 단계는 Tail.reverseHelper에 전달하는 누산기 값과 비꼬리 재귀 뒤집기의 관계를 생각하는 것이다.
Tail.sumHelper에서 누산기에 수를 더하는 것이 전체 합에 그 수를 더하는 것과 같듯이, Tail.reverseHelper에서 List.cons로 누산기에 새 원소를 추가하는 것은 전체 결과를 어떤 방식으로 바꾸는 것과 같다.
관계가 분명해질 때까지 연습장에 세네 가지 누산기 값을 대입해 보라.
이 관계를 사용하여 적절한 보조 정리를 증명하라.
이 보조 정리를 리스트에 대한 귀납법과 함수 귀납법으로 각각 증명해 보라.
그 다음 전체 정리를 적어라.
NonTail.reverse와 Tail.reverse는 다형적이므로 두 함수의 동등성을 명시할 때 α에 어떤 타입을 사용할지 Lean이 추론하지 못하게 @를 사용해야 한다.
α를 일반 인자로 다루게 한 뒤에는 α와 xs 모두에 대해 funext를 호출해야 한다.
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. Factorial
이전 절의 연습문제에 나온 NonTail.factorial이 자신의 꼬리 재귀 해와 같음을, 누산기와 결과 사이의 관계를 찾아 적절한 보조 정리를 증명하여 보이라.