Interlude: Tactics, Induction, and Proofs🔗

A Note on Proofs and User Interfaces🔗

이 책은 증명을 한 번에 작성하여 Lean에 제출하고, Lean이 아직 해야 할 일을 설명하는 오류 메시지로 답하는 것처럼 증명 작성 과정을 제시한다. 실제로 Lean과 상호작용하는 과정은 훨씬 즐겁다. Lean은 커서를 증명 안에서 움직일 때 증명에 관한 정보를 제공하며, 증명을 쉽게 해 주는 여러 상호작용 기능도 제공한다. 자세한 내용은 사용 중인 Lean 개발 환경의 문서를 참고하라.

증명을 점진적으로 만들고 그 결과로 나오는 메시지를 보여 주는 이 책의 접근법은 전문가가 사용하는 과정보다 훨씬 느리지만, 증명을 작성하는 동안 Lean이 제공하는 상호작용 피드백의 종류를 보여 준다. 동시에 불완전한 증명이 완전한 증명으로 발전하는 과정을 보는 것은 증명을 바라보는 유용한 관점이다. 증명 작성 능력이 향상되면 Lean의 피드백은 오류라기보다 자신의 사고 과정을 돕는 지원처럼 느껴질 것이다. 상호작용 방식의 학습은 매우 중요하다.

Recursion and Induction🔗

앞 장의 함수 plusR_succ_left와 plusR_zero_left는 두 가지 관점에서 볼 수 있다. 한편으로 이 함수들은 다른 재귀 함수가 리스트, 문자열 또는 다른 자료 구조를 만들 수 있는 것처럼 명제에 대한 증거를 쌓아 가는 재귀 함수다. 다른 한편으로 이 함수들은 수학적 귀납법(mathematical induction), 즉 귀납법에 의한 증명에도 대응한다.

수학적 귀납법은 다음 두 단계로 명제가 모든(all) 자연수에 대해 성립함을 증명하는 기법이다.

명제가 0에 대해 성립함을 보인다. 이를 ‘기저 사례(base case)’라고 한다.
임의로 선택한 어떤 수 n에 대해 명제가 성립한다고 가정하고, n + 1에 대해서도 성립함을 보인다. 이를 ‘귀납 단계(induction step)’라고 한다. n에 대해 명제가 성립한다는 가정을 ‘귀납 가설(induction hypothesis)’이라고 한다.

모든(every) 자연수에 대해 명제를 직접 확인하는 것은 불가능하므로, 귀납법은 원칙적으로 특정 자연수까지 펼칠 수 있는 증명을 작성하는 방법을 제공한다. 예를 들어 3에 대한 구체적인 증명이 필요하다면, 먼저 기저 사례를 사용한 다음 귀납 단계를 세 번 사용하여 0, 1, 2, 마지막으로 3에 대해 명제가 성립함을 보일 수 있다. 이렇게 하여 모든 자연수에 대한 명제를 증명한다.

The Induction Tactic🔗

congrArg 같은 보조 함수를 사용하는 귀납 증명을 재귀 함수로 작성하는 방식은 증명 이면의 의도를 항상 잘 표현하지는 못한다. 재귀 함수가 실제로 귀납법의 구조를 갖기는 하지만, 재귀 함수는 증명의 인코딩(encoding), 즉 증명의 표현으로 보는 편이 좋다. 더구나 Lean의 전술 시스템은 재귀 함수를 명시적으로 작성할 때는 사용할 수 없는, 증명 작성을 자동화할 여러 기회를 제공한다. Lean은 하나의 전술 블록에서 귀납에 의한 증명 전체를 수행할 수 있는 귀납 전술(tactic), 즉 이 전술을 제공한다. 내부적으로 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 뒤의 case 절은 패턴이 아니다. 목표 이름 뒤에 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! 🐙

이 다시 쓰기는 등식의 양변을 같게 만들며, Lean이 rfl을 자동으로 처리한다. 증명이 완성되었다.

Tactic Golf🔗

지금까지 전술 언어는 진정한 가치를 보여 주지 못했다. 위의 증명은 재귀 함수보다 짧지 않으며, 단지 완전한 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 전술은 가정 어떤 것(any), 즉 어느 하나라도 현재 목표와 일치하면 현재 목표를 해결한다.

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 문법이 편리하다. 누락된 경우(case)가 있으면 알려 주고 귀납의 구조도 명확히 보여 준다. 하지만 증명을 짧게 하려면 더 자유로운 접근이 필요한 경우가 많다.

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이 만든 모든(all) 목표에 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! 🐙

여기서는 ih에 명시적으로 이름을 붙이지 않았으므로 exact를 사용할 수 없다.

초보자에게는 이 증명이 더 읽기 쉽지 않다. 그러나 숙련자는 simp 같은 강력한 전술로 여러 단순한 경우(case)를 처리하고, 증명 본문을 흥미로운 경우(case)에 집중시키는 패턴을 흔히 사용한다. 또한 이런 증명은 증명에 관여하는 함수와 데이터 타입이 조금 바뀌어도 더 견고한 경향이 있다. 전술 골프는 증명을 작성할 때 좋은 감각과 스타일을 기르는 데 유용한 부분이다.

Induction on Other Datatypes🔗

수학적 귀납법은 Nat.zero에 대한 기저 사례와 Nat.succ에 대한 귀납 단계를 제공하여 자연수에 대한 명제를 증명한다. 귀납의 원리는 다른 데이터 타입에도 유효하다. 재귀 인자가 없는 생성자는 기저 사례를 이루고, 재귀 인자가 있는 생성자는 귀납 단계를 이룬다. 귀납으로 증명을 수행할 수 있다는 점이 바로 이 데이터 타입들을 귀납적(inductive) 데이터 타입이라고 부르는 이유다.

그 예로 이진 트리에 대한 귀납을 들 수 있다. 이진 트리에 대한 귀납은 다음 두 단계로 모든(all) 이진 트리에 대해 명제를 증명하는 기법이다.

명제가 BinTree.leaf에 대해 성립함을 보인다. 이를 기저 사례라고 한다.
임의로 선택한 트리 l과 r에 대해 명제가 성립한다고 가정하고, x가 임의로 선택한 새 데이터인 BinTree.branch l x r에 대해서도 성립함을 보인다. 이를 ‘귀납 단계(induction step)’라고 한다. l과 r에 대해 명제가 성립한다는 가정을 ‘귀납 가설(induction hypotheses)’이라고 한다.

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의 미러를 센 결과가 leaf를 센 결과와 같다는 것을 나타낸다.

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

귀납 단계에서는 왼쪽과 오른쪽 서브트리의 미러링이 각각의 가지 수에 영향을 주지 않는다고 가정하고, 이 서브트리를 가진 branch를 미러링해도 전체 가지 수가 보존됨을 증명해야 한다.

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의 인자 *는 목표를 단순화하거나 해결할 때 모든(all) 가정을 사용하라고 지시한다. 즉 증명을 다음과 같이 작성할 수도 있다.

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! 🐙

두 분기 모두 단순화기를 사용하므로 증명을 다음처럼 줄일 수 있다.

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! 🐙

The `grind` Tactic🔗

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가 모든 능력을 보여 줄 기회를 제공하지 않는다. 그러나 책 뒤쪽의 일부 증명에서는 매우 편리하다.

Exercises🔗

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