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

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

이 책에서는 증명을 작성하는 과정을 마치 한 번에 작성하여 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 전처리기 매크로와 다소 비슷합니다. 택틱이 실제 프로그램을 생성합니다.

택틱 언어에서는 여러 개의 목표가 존재할 수 있습니다. 각 목표(goal)는 타입과 몇 가지 가정으로 구성됩니다. 이는 밑줄을 자리 표시자로 사용하는 것과 유사합니다—목표의 타입은 증명해야 할 대상을 나타내고, 가정은 범위 안에 있어 사용할 수 있는 것을 나타냅니다. 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 전체는 귀납 단계입니다.

증명을 작성하는 다음 단계는 두 목표 각각에 차례로 집중하는 것입니다. pure ()가 do 블록에서 “아무것도 하지 않음”을 나타내는 데 사용될 수 있는 것과 마찬가지로, 택틱 언어에도 마찬가지로 아무것도 하지 않는 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)

증명의 재귀 함수 버전에서는 타입 표기 덕분에 예상 타입이 더 이해하기 쉬운 것이 되었습니다. 택틱 언어에는 목표(goal)를 더 쉽게 해결할 수 있도록 변형하는 다양한 특정 방법들이 있습니다. 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! 🐙

이 재작성은 등식의 양변을 동일하게 만들며, Lean이 rfl을 알아서 처리합니다. 증명이 완료되었습니다.

택틱 골프🔗

지금까지는 택틱 언어가 진정한 가치를 보여주지 못했습니다. 위 증명은 재귀 함수보다 짧지 않으며, 단지 완전한 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을 사용하면 단순히 두 개의 목표가 있는 증명 상태가 됩니다. case 택틱을 사용하면 induction ...with 택틱의 분기에서와 마찬가지로 이들 중 하나를 선택할 수 있습니다. 다시 말해, 다음 증명은 이전 증명과 동등합니다:

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에 대한 귀납 단계를 제공함으로써 자연수에 대한 명제를 증명합니다. 귀납법의 원리는 다른 데이터 타입에 대해서도 유효합니다. 재귀 인자가 없는 생성자는 기저 사례를 이루며, 재귀 인자가 있는 생성자는 귀납 단계를 이룹니다. 귀납법으로 증명을 수행할 수 있는 능력이야말로 이들이 inductive(귀납적) 데이터 타입이라 불리는 바로 그 이유입니다.

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

BinTree.leaf에 대해 이 명제가 성립함이 보입니다. 이를 기저 사례(base case)라고 합니다.
임의로 선택된 트리 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

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

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가 되므로, 좌변과 우변이 정의상 동일하기 때문입니다. 이는 BinTree.mirror를 펼치라는 지시와 함께 simp를 사용하여 표현할 수 있습니다:

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