막간: 택틱, 귀납법, 그리고 증명🔗

증명과 사용자 인터페이스에 관한 참고 사항🔗

이 책에서는 증명을 작성하는 과정을 마치 증명을 한 번에 작성해 Lean에 제출하면 Lean이 남은 작업을 알려 주는 오류 메시지로 응답하는 것처럼 보여 줍니다. 실제로 Lean과 상호작용하는 과정은 이보다 훨씬 더 쾌적합니다. 증명 안에서 커서를 움직이면 Lean이 증명에 대한 정보를 제공하며, 증명을 더 쉽게 만들어 주는 여러 대화형 기능도 있습니다. 자세한 내용은 사용 중인 Lean 개발 환경의 문서를 참고하십시오.

이 책에서는 증명을 조금씩 쌓아 가면서 그 결과로 나오는 메시지를 보여 주는 방식에 중점을 둡니다. 이 방식은 전문가가 쓰는 과정보다 훨씬 느립니다. 하지만 증명을 작성하는 동안 Lean이 어떤 종류의 대화형 피드백을 제공하는지 보여 줍니다. 동시에 불완전한 증명이 완전한 증명으로 발전해 가는 과정을 지켜보면 증명을 새로운 시각으로 바라볼 수 있어 유용합니다. 증명을 작성하는 실력이 늘수록 Lean의 피드백은 오류라기보다 여러분의 사고 과정을 뒷받침하는 도움처럼 느껴질 것입니다. 대화형 접근 방식을 익히는 것은 매우 중요합니다.

재귀와 귀납법🔗

앞 장에 나온 plusR_succ_left와 plusR_zero_left 함수는 두 가지 관점에서 볼 수 있습니다. 한편으로 이 함수들은 명제에 대한 증거를 쌓아 가는 재귀 함수입니다. 다른 재귀 함수가 리스트나 문자열, 그 밖의 어떤 자료 구조를 만들어 내는 것과 마찬가지입니다. 다른 한편으로 이 함수들은 수학적 귀납법에 의한 증명에도 대응합니다.

수학적 귀납법은 어떤 명제가 모든 자연수에 대해 성립함을 다음 두 단계로 증명하는 증명 기법입니다:

명제가 0에 대해 성립함을 보입니다. 이를 기저 사례라고 합니다.
임의로 선택한 어떤 수 n에 대해 명제가 성립한다는 가정하에, n + 1에 대해서도 성립함을 보입니다. 이를 귀납 단계라고 합니다. n에 대해 명제가 성립한다는 가정을 귀납 가설이라고 합니다.

모든 자연수에 대해 명제를 확인하는 것은 불가능하므로, 귀납법은 원칙적으로 임의의 특정 자연수까지 확장할 수 있는 증명을 작성하는 수단을 제공합니다. 예를 들어 숫자 3에 대한 구체적인 증명이 필요하다면, 먼저 기저 사례를 사용한 다음 귀납 단계를 세 번 사용하여 0, 1, 2, 그리고 마지막으로 3에 대해 명제를 보임으로써 그 증명을 구성할 수 있습니다. 따라서 귀납법은 모든 자연수에 대해 명제를 증명합니다.

귀납 택틱🔗

congrArg와 같은 보조 함수를 사용하는 재귀 함수로 귀납법에 의한 증명을 작성하면 증명에 담긴 의도가 항상 잘 드러나지는 않습니다. 재귀 함수가 실제로 귀납법의 구조를 갖추고 있기는 하지만, 재귀 함수는 증명의 인코딩으로 보는 편이 적절할 것입니다. 게다가 Lean의 택틱 시스템은 재귀 함수를 명시적으로 작성할 때는 활용할 수 없는, 증명 구성을 자동화할 여러 기회를 제공합니다. Lean은 귀납법에 의한 증명 전체를 하나의 택틱 블록 안에서 수행할 수 있는 induction 택틱을 제공합니다. 내부적으로 Lean은 귀납법의 사용에 대응하는 재귀 함수를 구성합니다.

induction 택틱으로 plusR_zero_left를 증명하려면 먼저 시그니처를 작성하십시오(이것은 실제로 증명이므로 theorem을 사용합니다). 그런 다음 정의의 본문으로 by induction k를 사용하십시오:

theorem plusR_zero_left (k : Nat) : k = Nat.plusR 0 k := unsolved goals
zero⊢ 0 = Nat.plusR 0 0

succn✝:Nata✝:n✝ = Nat.plusR 0 n✝⊢ n✝ + 1 = Nat.plusR 0 (n✝ + 1)byk:Nat⊢ k = Nat.plusR 0 k
  induction kzero⊢ 0 = Nat.plusR 0 0succn✝:Nata✝:n✝ = Nat.plusR 0 n✝⊢ n✝ + 1 = Nat.plusR 0 (n✝ + 1)

출력된 메시지는 목표가 두 개 있다고 알려 줍니다:

unsolved goals
zero⊢ 0 = Nat.plusR 0 0

succn✝:Nata✝:n✝ = Nat.plusR 0 n✝⊢ n✝ + 1 = Nat.plusR 0 (n✝ + 1)

택틱 블록은 Lean 타입 검사기가 파일을 처리하는 동안 실행되는 프로그램으로, 훨씬 더 강력한 C 전처리기 매크로와 다소 비슷합니다. 실제 프로그램은 택틱이 생성합니다.

택틱 언어에서는 여러 개의 목표가 있을 수 있습니다. 각 목표는 타입과 몇 가지 가정으로 이루어집니다. 이는 밑줄을 자리 표시자로 사용하는 것과 비슷합니다. 목표의 타입은 증명해야 할 대상을 나타내고, 가정은 스코프 안에 있어 사용할 수 있는 것을 나타냅니다. 목표 case zero의 경우, 가정은 없고 타입은 Nat.zero = Nat.plusR 0 Nat.zero입니다. 이는 k 대신 0을 넣은 정리 명제입니다. 목표 case succ에는 n✝과 n_ih✝라는 이름의 가정이 두 개 있습니다. 내부적으로 induction 택틱은 전체 타입을 구체화하는 의존 패턴 매칭을 만들어 내며, n✝은 패턴에서 Nat.succ에 전달되는 인자를 나타냅니다. 가정 n_ih✝는 생성된 함수를 n✝에 대해 재귀적으로 호출한 결과를 나타냅니다. 그 타입은 정리의 전체 타입에서 k 대신 n✝을 넣은 것입니다. 목표 case succ의 일부로 충족해야 하는 타입은 k 대신 Nat.succ n✝을 넣은 전체 정리 명제입니다.

induction 택틱을 사용하면 두 개의 목표가 생기며, 이들은 수학적 귀납법 설명에 나오는 기저 사례와 귀납 단계에 대응합니다. 기저 사례는 case zero입니다. case succ에서 n_ih✝는 귀납 가설에 해당하며, case succ 전체가 귀납 단계입니다.

증명 작성의 다음 단계는 두 목표 각각에 차례로 집중하는 것입니다. do 블록에서 pure ()를 사용해 “아무것도 하지 않음”을 나타낼 수 있는 것처럼, 택틱 언어에도 역시 아무것도 하지 않는 skip 문이 있습니다. 이 문은 Lean의 문법상 택틱이 필요하지만 어떤 택틱을 사용해야 할지 아직 분명하지 않을 때 사용할 수 있습니다. induction 문 끝에 with를 추가하면 패턴 매칭과 비슷한 문법을 사용할 수 있습니다:

theorem plusR_zero_left (k : Nat) : k = Nat.plusR 0 k := byk:Nat⊢ k = Nat.plusR 0 k
  induction k with
  | zero unsolved goals
zero⊢ 0 = Nat.plusR 0 0=> skipzero⊢ 0 = Nat.plusR 0 0
  | succ n ih unsolved goals
succn:Natih:n = Nat.plusR 0 n⊢ n + 1 = Nat.plusR 0 (n + 1)=> skipsuccn:Natih:n = Nat.plusR 0 n⊢ n + 1 = Nat.plusR 0 (n + 1)

두 skip 문에는 각각 메시지가 연결되어 있습니다. 첫 번째 메시지는 기저 사례를 보여 줍니다.

unsolved goals
zero⊢ 0 = Nat.plusR 0 0

두 번째는 귀납 단계를 보여 줍니다:

unsolved goals
succn:Natih:n = Nat.plusR 0 n⊢ n + 1 = Nat.plusR 0 (n + 1)

귀납 단계에서는 단검 기호가 붙은 접근 불가능한 이름들이 succ 뒤에 주어진 이름, 즉 n과 ih로 바뀌었습니다.

induction ...with 뒤에 오는 케이스들은 패턴이 아닙니다. 각 케이스는 목표의 이름과 그 뒤에 오는 0개 이상의 이름으로 이루어집니다. 이 이름들은 목표에서 도입되는 가정의 이름으로 사용되며, 목표가 도입하는 것보다 많은 이름을 제공하면 오류가 발생합니다:

theorem plusR_zero_left (k : Nat) : k = Nat.plusR 0 k := byk:Nat⊢ k = Nat.plusR 0 k
  induction k with
  | zero unsolved goals
zero⊢ 0 = Nat.plusR 0 0=> skipzero⊢ 0 = Nat.plusR 0 0
  Too many variable names provided at alternative `succ`: 5 provided, but 2 expected| succ n ih lots of names unsolved goals
succn:Natih:n = Nat.plusR 0 n⊢ n + 1 = Nat.plusR 0 (n + 1)=> skipsuccn:Natih:n = Nat.plusR 0 n⊢ n + 1 = Nat.plusR 0 (n + 1)

Too many variable names provided at alternative `succ`: 5 provided, but 2 expected

기저 사례에 집중해 보면, rfl 택틱은 재귀 함수에서와 마찬가지로 induction 택틱 안에서도 잘 작동합니다:

theorem plusR_zero_left (k : Nat) : k = Nat.plusR 0 k := byk:Nat⊢ k = Nat.plusR 0 k
  induction k with
  | zero =>zero⊢ 0 = Nat.plusR 0 0 rflAll goals completed! 🐙
  | succ n ih unsolved goals
succn:Natih:n = Nat.plusR 0 n⊢ n + 1 = Nat.plusR 0 (n + 1)=> skipsuccn:Natih:n = Nat.plusR 0 n⊢ n + 1 = Nat.plusR 0 (n + 1)

증명의 재귀 함수 버전에서는 타입 표기 덕분에 기대 타입을 더 이해하기 쉬운 형태로 만들 수 있었습니다. 택틱 언어에는 목표를 더 쉽게 풀 수 있도록 변형하는 구체적인 방법이 여러 가지 있습니다. unfold 택틱은 정의된 이름을 그 정의로 대체합니다:

theorem plusR_zero_left (k : Nat) : k = Nat.plusR 0 k := byk:Nat⊢ k = Nat.plusR 0 k
  induction k with
  | zero =>zero⊢ 0 = Nat.plusR 0 0 rflAll goals completed! 🐙
  | succ n ih unsolved goals
succn:Natih:n = Nat.plusR 0 n⊢ n + 1 = Nat.plusR 0 n + 1=>
    unfold Nat.plusRsuccn:Natih:n = Nat.plusR 0 n⊢ n + 1 = Nat.plusR 0 n + 1succn:Natih:n = Nat.plusR 0 n⊢ n + 1 = Nat.plusR 0 (n + 1)

이제 목표에 있는 등식의 우변은 Nat.plusR 0 (Nat.succ n) 대신 Nat.plusR 0 n + 1이 되었습니다:

unsolved goals
succn:Natih:n = Nat.plusR 0 n⊢ n + 1 = Nat.plusR 0 n + 1

congrArg 같은 함수나 ▸ 같은 연산자에 의존하는 대신, 동등성 증명을 사용하여 증명 목표를 변환할 수 있게 해 주는 택틱들이 있습니다. 그중 가장 중요한 것 하나는 rw로, 동등성 증명의 리스트를 받아 목표에서 좌변을 우변으로 바꿉니다. 이 택틱은 plusR_zero_left에서 거의 올바르게 동작합니다:

theorem plusR_zero_left (k : Nat) : k = Nat.plusR 0 k := byk:Nat⊢ k = Nat.plusR 0 k
  induction k with
  | zero =>zero⊢ 0 = Nat.plusR 0 0 rflAll goals completed! 🐙
  | succ n ih unsolved goals
succn:Natih:n = Nat.plusR 0 n⊢ Nat.plusR 0 n + 1 = Nat.plusR 0 (Nat.plusR 0 n) + 1=>
    unfold Nat.plusRsuccn:Natih:n = Nat.plusR 0 n⊢ n + 1 = Nat.plusR 0 n + 1
    rw [ihsuccn:Natih:n = Nat.plusR 0 n⊢ Nat.plusR 0 n + 1 = Nat.plusR 0 (Nat.plusR 0 n) + 1]succn:Natih:n = Nat.plusR 0 n⊢ Nat.plusR 0 n + 1 = Nat.plusR 0 (Nat.plusR 0 n) + 1succn:Natih:n = Nat.plusR 0 n⊢ n + 1 = Nat.plusR 0 (n + 1)

하지만 재작성의 방향이 잘못되었습니다. n을 Nat.plusR 0 n으로 바꾸자 목표가 단순해지기는커녕 오히려 더 복잡해졌습니다:

unsolved goals
succn:Natih:n = Nat.plusR 0 n⊢ Nat.plusR 0 n + 1 = Nat.plusR 0 (Nat.plusR 0 n) + 1

이 문제는 rw 호출에서 ih 앞에 왼쪽 화살표를 붙여 해결할 수 있습니다. 이렇게 하면 등식의 우변을 좌변으로 치환하도록 지시하게 됩니다:

theorem plusR_zero_left (k : Nat) : k = Nat.plusR 0 k := byk:Nat⊢ k = Nat.plusR 0 k
  induction k with
  | zero =>zero⊢ 0 = Nat.plusR 0 0 rflAll goals completed! 🐙
  | succ n ih =>succn:Natih:n = Nat.plusR 0 n⊢ n + 1 = Nat.plusR 0 (n + 1)
    unfold Nat.plusRsuccn:Natih:n = Nat.plusR 0 n⊢ n + 1 = Nat.plusR 0 n + 1
    rw [←ihsuccn:Natih:n = Nat.plusR 0 n⊢ n + 1 = n + 1]All goals completed! 🐙

이렇게 다시 쓰면 등식의 양변이 똑같아지고, rfl은 Lean이 알아서 처리합니다. 증명이 완료되었습니다.

택틱 골프🔗

지금까지는 택틱 언어가 진정한 가치를 보여 주지 못했습니다. 위 증명은 재귀 함수보다 짧지 않습니다. 단지 완전한 Lean 언어 대신 도메인 특화 언어로 작성되었을 뿐입니다. 하지만 택틱을 사용한 증명은 더 짧고, 더 쉬우며, 유지 보수하기도 더 좋을 수 있습니다. 골프에서 점수가 낮을수록 좋은 것처럼, 택틱 골프에서는 증명이 짧을수록 좋습니다.

plusR_zero_left의 귀납 단계는 단순화 택틱 simp를 사용하여 증명할 수 있습니다. simp만 단독으로 사용해서는 도움이 되지 않습니다:

theorem plusR_zero_left (k : Nat) : k = Nat.plusR 0 k := byk:Nat⊢ k = Nat.plusR 0 k
  induction k with
  | zero =>zero⊢ 0 = Nat.plusR 0 0 rflAll goals completed! 🐙
  | succ n ih =>succn:Natih:n = Nat.plusR 0 n⊢ n + 1 = Nat.plusR 0 (n + 1)
    `simp` made no progresssimpsuccn:Natih:n = Nat.plusR 0 n⊢ n + 1 = Nat.plusR 0 (n + 1)

`simp` made no progress

하지만 simp가 여러 정의를 활용하도록 설정할 수 있습니다. rw와 마찬가지로 이 인자들은 리스트로 전달합니다. simp가 Nat.plusR의 정의를 고려하도록 하면 더 단순한 목표를 얻습니다:

theorem plusR_zero_left (k : Nat) : k = Nat.plusR 0 k := byk:Nat⊢ k = Nat.plusR 0 k
  induction k with
  | zero =>zero⊢ 0 = Nat.plusR 0 0 rflAll goals completed! 🐙
  | succ n ih unsolved goals
succn:Natih:n = Nat.plusR 0 n⊢ n = Nat.plusR 0 n=>
    simp [Nat.plusR]succn:Natih:n = Nat.plusR 0 n⊢ n = Nat.plusR 0 nsuccn:Natih:n = Nat.plusR 0 n⊢ n + 1 = Nat.plusR 0 (n + 1)

unsolved goals
succn:Natih:n = Nat.plusR 0 n⊢ n = Nat.plusR 0 n

특히, 이제 목표는 귀납 가설과 동일합니다. 단순화기는 간단한 등식 명제를 자동으로 증명할 뿐만 아니라, Nat.succ A = Nat.succ B와 같은 목표를 A = B로 자동으로 바꿉니다. 귀납 가설 ih가 정확히 알맞은 타입을 가지므로, exact 택틱으로 이 가설을 사용하도록 지시할 수 있습니다:

theorem plusR_zero_left (k : Nat) : k = Nat.plusR 0 k := byk:Nat⊢ k = Nat.plusR 0 k
  induction k with
  | zero =>zero⊢ 0 = Nat.plusR 0 0 rflAll goals completed! 🐙
  | succ n ih =>succn:Natih:n = Nat.plusR 0 n⊢ n + 1 = Nat.plusR 0 (n + 1)
    simp [Nat.plusR]succn:Natih:n = Nat.plusR 0 n⊢ n = Nat.plusR 0 n
    exact ihAll goals completed! 🐙

하지만 exact를 사용하는 방식은 다소 취약합니다. 증명을 “골프”하는 과정에서 귀납 가설의 이름이 바뀔 수 있는데, 그러면 이 증명은 더 이상 작동하지 않게 됩니다. assumption 택틱은 가정 중 어느 하나라도 현재 목표와 일치하면 그 목표를 해결합니다:

theorem plusR_zero_left (k : Nat) : k = Nat.plusR 0 k := byk:Nat⊢ k = Nat.plusR 0 k
  induction k with
  | zero =>zero⊢ 0 = Nat.plusR 0 0 rflAll goals completed! 🐙
  | succ n ih =>succn:Natih:n = Nat.plusR 0 n⊢ n + 1 = Nat.plusR 0 (n + 1)
    simp [Nat.plusR]succn:Natih:n = Nat.plusR 0 n⊢ n = Nat.plusR 0 n
    assumptionAll goals completed! 🐙

이 증명은 펼치기와 명시적 재작성을 사용했던 이전 증명보다 짧지 않습니다. 하지만 simp가 여러 종류의 목표를 풀 수 있다는 점을 활용하면, 일련의 변환을 거쳐 증명을 훨씬 짧게 만들 수 있습니다. 첫 번째 단계는 induction 끝에 있는 with를 없애는 것입니다. 구조적이고 읽기 쉬운 증명에는 with 문법이 편리합니다. 이 문법은 빠진 경우가 있으면 오류를 알려 주고, 귀납의 구조를 명확하게 보여 줍니다. 하지만 증명을 짧게 줄이려면 흔히 좀 더 느슨한 접근 방식이 필요합니다.

with 없이 induction을 사용하면 단순히 목표가 두 개인 증명 상태가 됩니다. induction ...with 택틱의 분기에서와 마찬가지로, case 택틱을 사용하여 그중 하나를 선택할 수 있습니다. 다시 말해, 다음 증명은 앞의 증명과 동등합니다:

theorem plusR_zero_left (k : Nat) : k = Nat.plusR 0 k := byk:Nat⊢ k = Nat.plusR 0 k
  induction kzero⊢ 0 = Nat.plusR 0 0succn✝:Nata✝:n✝ = Nat.plusR 0 n✝⊢ n✝ + 1 = Nat.plusR 0 (n✝ + 1)
  case zero =>⊢ 0 = Nat.plusR 0 0 rflAll goals completed! 🐙
  case succ n ih =>n:Natih:n✝ = Nat.plusR 0 n✝⊢ n✝ + 1 = Nat.plusR 0 (n✝ + 1)
    simp [Nat.plusR]n:Natih:n✝ = Nat.plusR 0 n✝⊢ n✝ = Nat.plusR 0 n✝
    assumptionAll goals completed! 🐙

목표가 하나뿐인 맥락(즉, k = Nat.plusR 0 k)에서 induction k 택틱은 두 개의 목표를 만들어 냅니다. 일반적으로 택틱은 오류를 내며 실패하거나, 목표 하나를 받아 이를 0개 이상의 새로운 목표로 변환합니다. 각각의 새로운 목표는 아직 증명해야 할 남은 부분을 나타냅니다. 결과로 남은 목표가 0개라면 택틱이 성공한 것이며, 증명의 해당 부분은 완료된 것입니다.

<;> 연산자는 두 택틱을 인자로 받아 새로운 택틱을 만듭니다. T1 <;> T2는 현재 목표에 T1을 적용한 다음, T1이 만든 모든 목표에 T2를 적용합니다. 다시 말해, <;>를 사용하면 여러 종류의 목표를 풀 수 있는 범용 택틱을 새로 생긴 여러 목표에 한꺼번에 사용할 수 있습니다. 그러한 범용 택틱 중 하나가 simp입니다.

simp는 기저 사례의 증명을 완료할 수 있을 뿐만 아니라 귀납 단계의 증명도 진척시킬 수 있으므로, 이를 induction 및 <;>와 함께 사용하면 증명이 짧아집니다:

theorem plusR_zero_left (k : Nat) : k = Nat.plusR 0 k := unsolved goals
succn✝:Nata✝:n✝ = Nat.plusR 0 n✝⊢ n✝ = Nat.plusR 0 n✝byk:Nat⊢ k = Nat.plusR 0 k
  induction kzero⊢ 0 = Nat.plusR 0 0succn✝:Nata✝:n✝ = Nat.plusR 0 n✝⊢ n✝ + 1 = Nat.plusR 0 (n✝ + 1) <;>zero⊢ 0 = Nat.plusR 0 0succn✝:Nata✝:n✝ = Nat.plusR 0 n✝⊢ n✝ + 1 = Nat.plusR 0 (n✝ + 1) simp [Nat.plusR]succn✝:Nata✝:n✝ = Nat.plusR 0 n✝⊢ n✝ = Nat.plusR 0 n✝

그 결과 변환된 귀납 단계 하나만 목표로 남습니다:

unsolved goals
succn✝:Nata✝:n✝ = Nat.plusR 0 n✝⊢ n✝ = Nat.plusR 0 n✝

이 목표에서 assumption을 실행하면 증명이 완료됩니다:

theorem plusR_zero_left (k : Nat) : k = Nat.plusR 0 k := byk:Nat⊢ k = Nat.plusR 0 k
  induction kzero⊢ 0 = Nat.plusR 0 0succn✝:Nata✝:n✝ = Nat.plusR 0 n✝⊢ n✝ + 1 = Nat.plusR 0 (n✝ + 1) <;>zero⊢ 0 = Nat.plusR 0 0succn✝:Nata✝:n✝ = Nat.plusR 0 n✝⊢ n✝ + 1 = Nat.plusR 0 (n✝ + 1) simp [Nat.plusR]succn✝:Nata✝:n✝ = Nat.plusR 0 n✝⊢ n✝ = Nat.plusR 0 n✝ <;>succn✝:Nata✝:n✝ = Nat.plusR 0 n✝⊢ n✝ = Nat.plusR 0 n✝ assumptionAll goals completed! 🐙

여기서는 exact를 사용할 수 없었을 것입니다. ih에 명시적으로 이름을 붙인 적이 없기 때문입니다.

초보자에게는 이 증명이 더 읽기 쉽지 않습니다. 하지만 숙련된 사용자들이 흔히 쓰는 패턴은 simp처럼 강력한 택틱으로 여러 간단한 경우를 처리하고, 증명의 본문은 흥미로운 경우에 집중하는 것입니다. 또한 이러한 증명은 증명에 관련된 함수와 데이터 타입이 조금 바뀌어도 잘 깨지지 않는 경향이 있습니다. 택틱 골프 놀이는 증명을 작성할 때 좋은 감각과 스타일을 기르는 데 도움이 됩니다.

다른 데이터 타입에 대한 귀납법🔗

수학적 귀납법은 Nat.zero에 대한 기저 사례와 Nat.succ에 대한 귀납 단계를 제시하여 자연수에 관한 명제를 증명합니다. 귀납법의 원리는 다른 데이터 타입에도 똑같이 적용됩니다. 재귀 인자가 없는 생성자는 기저 사례를 이루고, 재귀 인자가 있는 생성자는 귀납 단계를 이룹니다. 귀납법으로 증명할 수 있다는 점이야말로 이러한 데이터 타입을 귀납적 데이터 타입이라고 부르는 이유입니다.

이에 대한 한 가지 예는 이진 트리에 대한 귀납법입니다. 이진 트리에 대한 귀납법은 어떤 명제를 모든 이진 트리에 대해 다음 두 단계로 증명하는 증명 기법입니다:

BinTree.leaf에 대해 명제가 성립함을 보입니다. 이를 기저 사례라고 합니다.
임의로 선택한 트리 l과 r에 대해 명제가 성립한다고 가정하고, BinTree.branch l x r에 대해서도 명제가 성립함을 보입니다. 여기서 x는 임의로 선택한 새 데이터 포인트입니다. 이를 귀납 단계라고 합니다. l과 r에 대해 명제가 성립한다는 가정들을 귀납 가설이라고 합니다.

BinTree.count는 트리에 있는 가지의 개수를 셉니다:

def BinTree.count : BinTree α → Nat
  | .leaf => 0
  | .branch l _ r =>
    1 + l.count + r.count

트리를 좌우로 뒤집어도 트리에 있는 가지의 개수는 변하지 않습니다. 이는 트리에 대한 귀납법으로 증명할 수 있습니다. 첫 번째 단계는 정리를 기술하고 induction을 호출하는 것입니다:

theorem BinTree.mirror_count (t : BinTree α) :
    t.mirror.count = t.count := byα:Typet:BinTree α⊢ t.mirror.count = t.count
  induction t with
  | leaf unsolved goals
leafα:Type⊢ leaf.mirror.count = leaf.count=> skipleafα:Type⊢ leaf.mirror.count = leaf.count
  | branch l x r ihl ihr unsolved goals
branchα:Typel:BinTree αx:αr:BinTree αihl:l.mirror.count = l.countihr:r.mirror.count = r.count⊢ (l.branch x r).mirror.count = (l.branch x r).count=> skipbranchα:Typel:BinTree αx:αr:BinTree αihl:l.mirror.count = l.countihr:r.mirror.count = r.count⊢ (l.branch x r).mirror.count = (l.branch x r).count

기저 사례는 잎의 거울상을 세는 것이 그 잎을 세는 것과 같다는 것을 나타냅니다:

unsolved goals
leafα:Type⊢ leaf.mirror.count = leaf.count

귀납 단계에서는 왼쪽과 오른쪽 서브트리를 좌우 반전해도 각각의 가지 수가 달라지지 않는다는 가정을 사용할 수 있으며, 이 서브트리들로 이루어진 가지를 좌우 반전해도 전체 가지 수가 보존된다는 증명을 요구합니다:

unsolved goals
branchα:Typel:BinTree αx:αr:BinTree αihl:l.mirror.count = l.countihr:r.mirror.count = r.count⊢ (l.branch x r).mirror.count = (l.branch x r).count

leaf를 좌우 반전하면 leaf가 되므로 좌변과 우변이 정의상 같습니다. 따라서 기저 사례는 참입니다. 이는 simp에 BinTree.mirror를 펼치라고 지시하여 표현할 수 있습니다:

theorem BinTree.mirror_count (t : BinTree α) :
    t.mirror.count = t.count := byα:Typet:BinTree α⊢ t.mirror.count = t.count
  induction t with
  | leaf =>leafα:Type⊢ leaf.mirror.count = leaf.count simp [BinTree.mirror]All goals completed! 🐙
  | branch l x r ihl ihr unsolved goals
branchα:Typel:BinTree αx:αr:BinTree αihl:l.mirror.count = l.countihr:r.mirror.count = r.count⊢ (l.branch x r).mirror.count = (l.branch x r).count=> skipbranchα:Typel:BinTree αx:αr:BinTree αihl:l.mirror.count = l.countihr:r.mirror.count = r.count⊢ (l.branch x r).mirror.count = (l.branch x r).count

귀납 단계에서는 목표의 어떤 부분도 귀납 가설과 바로 일치하지 않습니다. BinTree.count와 BinTree.mirror의 정의를 사용해 단순화하면 둘 사이의 관계가 드러납니다:

theorem BinTree.mirror_count (t : BinTree α) :
    t.mirror.count = t.count := byα:Typet:BinTree α⊢ t.mirror.count = t.count
  induction t with
  | leaf =>leafα:Type⊢ leaf.mirror.count = leaf.count simp [BinTree.mirror]All goals completed! 🐙
  | branch l x r ihl ihr unsolved goals
branchα:Typel:BinTree αx:αr:BinTree αihl:l.mirror.count = l.countihr:r.mirror.count = r.count⊢ 1 + r.mirror.count + l.mirror.count = 1 + l.count + r.count=>
    simp [BinTree.mirror, BinTree.count]branchα:Typel:BinTree αx:αr:BinTree αihl:l.mirror.count = l.countihr:r.mirror.count = r.count⊢ 1 + r.mirror.count + l.mirror.count = 1 + l.count + r.countbranchα:Typel:BinTree αx:αr:BinTree αihl:l.mirror.count = l.countihr:r.mirror.count = r.count⊢ (l.branch x r).mirror.count = (l.branch x r).count

unsolved goals
branchα:Typel:BinTree αx:αr:BinTree αihl:l.mirror.count = l.countihr:r.mirror.count = r.count⊢ 1 + r.mirror.count + l.mirror.count = 1 + l.count + r.count

두 귀납 가설을 모두 사용하면 목표의 좌변을 우변과 거의 같은 형태로 다시 쓸 수 있습니다:

theorem BinTree.mirror_count (t : BinTree α) :
    t.mirror.count = t.count := byα:Typet:BinTree α⊢ t.mirror.count = t.count
  induction t with
  | leaf =>leafα:Type⊢ leaf.mirror.count = leaf.count simp [BinTree.mirror]All goals completed! 🐙
  | branch l x r ihl ihr unsolved goals
branchα:Typel:BinTree αx:αr:BinTree αihl:l.mirror.count = l.countihr:r.mirror.count = r.count⊢ 1 + r.count + l.count = 1 + l.count + r.count=>
    simp [BinTree.mirror, BinTree.count]branchα:Typel:BinTree αx:αr:BinTree αihl:l.mirror.count = l.countihr:r.mirror.count = r.count⊢ 1 + r.mirror.count + l.mirror.count = 1 + l.count + r.count
    rw [ihl,branchα:Typel:BinTree αx:αr:BinTree αihl:l.mirror.count = l.countihr:r.mirror.count = r.count⊢ 1 + r.mirror.count + l.count = 1 + l.count + r.count ihrbranchα:Typel:BinTree αx:αr:BinTree αihl:l.mirror.count = l.countihr:r.mirror.count = r.count⊢ 1 + r.count + l.count = 1 + l.count + r.count]branchα:Typel:BinTree αx:αr:BinTree αihl:l.mirror.count = l.countihr:r.mirror.count = r.count⊢ 1 + r.count + l.count = 1 + l.count + r.countbranchα:Typel:BinTree αx:αr:BinTree αihl:l.mirror.count = l.countihr:r.mirror.count = r.count⊢ (l.branch x r).mirror.count = (l.branch x r).count

unsolved goals
branchα:Typel:BinTree αx:αr:BinTree αihl:l.mirror.count = l.countihr:r.mirror.count = r.count⊢ 1 + r.count + l.count = 1 + l.count + r.count

simp 택틱에 +arith 옵션을 전달하면 추가적인 산술 항등식을 사용할 수 있습니다. 이것만으로 이 목표를 증명하기에 충분하며, 결과는 다음과 같습니다:

theorem BinTree.mirror_count (t : BinTree α) :
    t.mirror.count = t.count := byα:Typet:BinTree α⊢ t.mirror.count = t.count
  induction t with
  | leaf =>leafα:Type⊢ leaf.mirror.count = leaf.count simp [BinTree.mirror]All goals completed! 🐙
  | branch l x r ihl ihr =>branchα:Typel:BinTree αx:αr:BinTree αihl:l.mirror.count = l.countihr:r.mirror.count = r.count⊢ (l.branch x r).mirror.count = (l.branch x r).count
    simp [BinTree.mirror, BinTree.count]branchα:Typel:BinTree αx:αr:BinTree αihl:l.mirror.count = l.countihr:r.mirror.count = r.count⊢ 1 + r.mirror.count + l.mirror.count = 1 + l.count + r.count
    rw [ihl,branchα:Typel:BinTree αx:αr:BinTree αihl:l.mirror.count = l.countihr:r.mirror.count = r.count⊢ 1 + r.mirror.count + l.count = 1 + l.count + r.count ihrbranchα:Typel:BinTree αx:αr:BinTree αihl:l.mirror.count = l.countihr:r.mirror.count = r.count⊢ 1 + r.count + l.count = 1 + l.count + r.count]branchα:Typel:BinTree αx:αr:BinTree αihl:l.mirror.count = l.countihr:r.mirror.count = r.count⊢ 1 + r.count + l.count = 1 + l.count + r.count
    simp +arithAll goals completed! 🐙

단순화기에는 펼칠 정의뿐만 아니라, 증명 목표를 단순화하는 동안 재작성에 사용할 동등성 증명의 이름도 전달할 수 있습니다. BinTree.mirror_count는 다음과 같이 작성할 수도 있습니다:

theorem BinTree.mirror_count (t : BinTree α) :
    t.mirror.count = t.count := byα:Typet:BinTree α⊢ t.mirror.count = t.count
  induction t with
  | leaf =>leafα:Type⊢ BinTree.leaf.mirror.count = BinTree.leaf.count simp [BinTree.mirror]All goals completed! 🐙
  | branch l x r ihl ihr =>branchα:Typel:BinTree αx:αr:BinTree αihl:l.mirror.count = l.countihr:r.mirror.count = r.count⊢ (l.branch x r).mirror.count = (l.branch x r).count
    simp +arith [BinTree.mirror, BinTree.count, ihl, ihr]All goals completed! 🐙

증명이 복잡해질수록 가정을 일일이 나열하는 일은 번거로워질 수 있습니다. 게다가 가정 이름을 직접 적으면 같은 증명 단계를 여러 하위 목표에 재사용하기가 더 어려워질 수 있습니다. simp나 simp +arith에 인자 *를 주면 목표를 단순화하거나 해결할 때 모든 가정을 사용합니다. 다시 말해, 이 증명은 다음과 같이 작성할 수도 있습니다.

theorem BinTree.mirror_count (t : BinTree α) :
    t.mirror.count = t.count := byα:Typet:BinTree α⊢ t.mirror.count = t.count
  induction t with
  | leaf =>leafα:Type⊢ BinTree.leaf.mirror.count = BinTree.leaf.count simp [BinTree.mirror]All goals completed! 🐙
  | branch l x r ihl ihr =>branchα:Typel:BinTree αx:αr:BinTree αihl:l.mirror.count = l.countihr:r.mirror.count = r.count⊢ (l.branch x r).mirror.count = (l.branch x r).count
    simp +arith [BinTree.mirror, BinTree.count, *]All goals completed! 🐙

두 분기 모두 단순화기(simplifier)를 사용하므로 증명을 다음과 같이 줄일 수 있습니다:

theorem BinTree.mirror_count (t : BinTree α) :
    t.mirror.count = t.count := byα:Typet:BinTree α⊢ t.mirror.count = t.count
  induction tleafα:Type⊢ BinTree.leaf.mirror.count = BinTree.leaf.countbranchα:Typea✝²:BinTree αa✝¹:αa✝:BinTree αa_ih✝¹:a✝².mirror.count = a✝².counta_ih✝:a✝.mirror.count = a✝.count⊢ (a✝².branch a✝¹ a✝).mirror.count = (a✝².branch a✝¹ a✝).count <;>leafα:Type⊢ BinTree.leaf.mirror.count = BinTree.leaf.countbranchα:Typea✝²:BinTree αa✝¹:αa✝:BinTree αa_ih✝¹:a✝².mirror.count = a✝².counta_ih✝:a✝.mirror.count = a✝.count⊢ (a✝².branch a✝¹ a✝).mirror.count = (a✝².branch a✝¹ a✝).count simp +arith [BinTree.mirror, BinTree.count, *]All goals completed! 🐙

`grind` 택틱🔗

grind 택틱은 많은 정리를 자동으로 증명할 수 있습니다. simp와 마찬가지로 고려할 추가 사실이나 펼칠 함수의 목록을 선택적으로 받습니다. simp와 달리 지역 가설을 자동으로 고려합니다. 또한 특정 수학 영역에 대한 추론을 지원하는 grind의 기능은 simp의 산술 지원보다 훨씬 강력합니다. BinTree.mirror_count의 증명은 grind를 사용하도록 다시 작성할 수 있습니다:

theorem BinTree.mirror_count (t : BinTree α) :
    t.mirror.count = t.count := byα:Typet:BinTree α⊢ t.mirror.count = t.count
  induction tleafα:Type⊢ BinTree.leaf.mirror.count = BinTree.leaf.countbranchα:Typea✝²:BinTree αa✝¹:αa✝:BinTree αa_ih✝¹:a✝².mirror.count = a✝².counta_ih✝:a✝.mirror.count = a✝.count⊢ (a✝².branch a✝¹ a✝).mirror.count = (a✝².branch a✝¹ a✝).count <;>leafα:Type⊢ BinTree.leaf.mirror.count = BinTree.leaf.countbranchα:Typea✝²:BinTree αa✝¹:αa✝:BinTree αa_ih✝¹:a✝².mirror.count = a✝².counta_ih✝:a✝.mirror.count = a✝.count⊢ (a✝².branch a✝¹ a✝).mirror.count = (a✝².branch a✝¹ a✝).count grind [BinTree.mirror, BinTree.count]All goals completed! 🐙

이 책의 증명들은 상당히 간단한 편이므로, 대부분의 증명에서는 grind가 진가를 온전히 발휘할 기회가 없습니다. 하지만 이 책 후반부의 몇몇 증명에서는 매우 편리합니다.

연습 문제🔗

induction ...with 택틱을 사용하여 plusR_succ_left를 증명하십시오.
plusR_succ_left의 증명을 <;>를 사용하여 한 줄로 다시 작성하십시오.
리스트에 대한 귀납법을 사용하여 리스트 이어 붙이기가 결합법칙을 만족함을 증명하십시오:
theorem List.append_assoc (xs ys zs : List α) : xs ++ (ys ++ zs) = (xs ++ ys) ++ zs