Lean 4로 정리 증명하기

5. 택틱🔗

이 장에서는 택틱을 사용하여 증명을 구성하는 대안적 접근 방식을 설명합니다. 증명 항은 수학적 증명의 표현이며, 택틱은 그러한 증명을 구성하는 방법을 서술하는 명령 또는 지시입니다. 비형식적으로는, “정방향을 증명하려면 정의를 펼치고, 이전 보조정리를 적용하고, 단순화하라”라고 말하면서 수학적 증명을 시작할 수 있습니다. 이것이 독자에게 관련 증명을 찾는 방법을 알려주는 지시인 것처럼, 택틱은 Lean에게 증명 항을 구성하는 방법을 알려주는 지시입니다. 택틱은 증명을 분해하여 목표를 한 번에 한 단계씩 다루는 점진적인 방식의 증명 작성을 자연스럽게 지원합니다.

택틱들의 나열로 이루어진 증명을 “택틱 스타일” 증명이라 부르며, 지금까지 살펴본 증명항 작성 방식과 대조하여 이를 “항 스타일” 증명이라 부르겠습니다. 각 스타일에는 저마다의 장단점이 있습니다. 예를 들어, 택틱 스타일 증명은 독자가 각 지시문의 결과를 예측하거나 추측해야 하므로 읽기 더 어려울 수 있습니다. 하지만 더 짧고 작성하기 쉬울 수도 있습니다. 게다가 자동화 절차 자체도 택틱이므로, 택틱은 Lean의 자동화를 사용할 수 있는 통로가 되어줍니다.

5.1. 택틱 모드 진입하기🔗

개념적으로, 정리를 명시하거나 have 문을 도입하면 목표가 생성되는데, 이는 예상 타입을 가진 항을 구성하는 목표입니다. 예를 들어, 다음은 상수 p q : Prop, hp : p, hq : q를 가진 맥락에서 타입 p ∧ q ∧ p의 항을 구성하는 목표를 생성합니다:

theorem declaration uses `sorry`test (p q : Prop) (hp : p) (hq : q) : p ∧ q ∧ p := p:Propq:Prophp:phq:q⊢ p ∧ q ∧ p All goals completed! 🐙

이 목표는 다음과 같이 작성할 수 있습니다:

p:Propq:Prophp:phq:q⊢ p ∧ q ∧ p

실제로 위 예제에서 “sorry”를 밑줄(underscore)로 바꾸면, Lean은 정확히 이 목표가 해결되지 않은 채로 남아 있다고 보고할 것입니다.

보통은 명시적인 항을 작성해서 그러한 목표를 만족시킵니다. 하지만 항이 필요한 곳이라면 어디든, Lean은 그 대신 by <tactics> 블록을 삽입할 수 있게 해 주는데, 여기서 <tactics>는 세미콜론이나 줄바꿈으로 구분된 일련의 명령입니다. 위의 정리는 이러한 방식으로 증명할 수 있습니다.

theorem test (p q : Prop) (hp : p) (hq : q) : p ∧ q ∧ p := p:Propq:Prophp:phq:q⊢ p ∧ q ∧ p p:Propq:Prophp:phq:q⊢ pp:Propq:Prophp:phq:q⊢ q ∧ p p:Propq:Prophp:phq:q⊢ q ∧ p p:Propq:Prophp:phq:q⊢ qp:Propq:Prophp:phq:q⊢ p p:Propq:Prophp:phq:q⊢ p All goals completed! 🐙

저희는 종종 by 키워드를 앞 줄에 배치하여, 위 예제를 다음과 같이 작성합니다.

theorem test (p q : Prop) (hp : p) (hq : q) : p ∧ q ∧ p := p:Propq:Prophp:phq:q⊢ p ∧ q ∧ p p:Propq:Prophp:phq:q⊢ pp:Propq:Prophp:phq:q⊢ q ∧ p p:Propq:Prophp:phq:q⊢ q ∧ p p:Propq:Prophp:phq:q⊢ qp:Propq:Prophp:phq:q⊢ p p:Propq:Prophp:phq:q⊢ p All goals completed! 🐙

apply 택틱은 0개 이상의 인자를 갖는 함수를 나타내는 것으로 간주되는 표현식을 적용합니다. 이 택틱은 결론을 현재 목표의 표현식과 통합하고, 이후의 인자들이 해당 인자들에 의존하지 않는 한 나머지 인자들에 대한 새로운 목표를 생성합니다. 위 예제에서 apply And.intro 명령은 두 개의 하위 목표를 만들어 냅니다.

p:Propq:Prophp:phq:q⊢ pp:Propq:Prophp:phq:q⊢ q ∧ p

첫 번째 목표는 exact hp 명령으로 충족됩니다. exact 명령은 apply의 변형일 뿐이며, 주어진 표현식이 목표를 정확히 채워야 함을 나타냅니다. 택틱 증명에서 이 명령을 사용하는 것은 좋은 방식인데, 실패할 경우 무언가 잘못되었음을 알려주기 때문입니다. 또한 정교화기가 표현식을 적용할 때 목표의 대상이 주어지는 예상 타입을 고려하므로, apply보다 더 견고합니다. 다만 이 경우에는 apply도 마찬가지로 잘 작동할 것입니다.

#print 명령으로 결과 증명 항을 확인할 수 있습니다:

theorem test : ∀ (p q : Prop), p → q → p ∧ q ∧ p := fun p q hp hq => ⟨hp, ⟨hq, hp⟩⟩#print test
theorem test : ∀ (p q : Prop), p → q → p ∧ q ∧ p :=
fun p q hp hq => ⟨hp, ⟨hq, hp⟩⟩

택틱 스크립트는 점진적으로 작성할 수 있습니다. VS Code에서는 CtrlShiftEnter를 눌러 메시지를 표시하는 창을 열 수 있으며, 커서가 택틱 블록 안에 있을 때마다 그 창에 현재 목표가 표시됩니다. 증명이 완료되지 않은 경우, by 토큰에는 빨간색 물결 밑줄이 표시되며, 오류 메시지에는 남은 목표가 포함됩니다.

택틱 명령은 단일 식별자뿐만 아니라 복합 표현식도 받을 수 있습니다. 다음은 앞선 증명을 더 짧게 만든 버전입니다.

theorem test (p q : Prop) (hp : p) (hq : q) : p ∧ q ∧ p := p:Propq:Prophp:phq:q⊢ p ∧ q ∧ p p:Propq:Prophp:phq:q⊢ q ∧ p All goals completed! 🐙

예상대로, 이는 정확히 동일한 증명 항을 만들어 냅니다:

theorem test : ∀ (p q : Prop), p → q → p ∧ q ∧ p := fun p q hp hq => ⟨hp, ⟨hq, hp⟩⟩#print test
theorem test : ∀ (p q : Prop), p → q → p ∧ q ∧ p :=
fun p q hp hq => ⟨hp, ⟨hq, hp⟩⟩

여러 택틱 적용은 세미콜론으로 연결하여 한 줄로 작성할 수 있습니다.

theorem test (p q : Prop) (hp : p) (hq : q) : p ∧ q ∧ p := p:Propq:Prophp:phq:q⊢ p ∧ q ∧ p p:Propq:Prophp:phq:q⊢ q ∧ p; All goals completed! 🐙

여러 하위 목표를 생성할 수 있는 택틱은 종종 하위 목표에 태그를 붙입니다. 예를 들어, apply And.intro 택틱은 첫 번째 하위 목표에 leftp:Propq:Prophp:phq:q⊢ p라는 태그를, 두 번째 하위 목표에 rightp:Propq:Prophp:phq:q⊢ q ∧ p라는 태그를 붙였습니다. apply 택틱의 경우, 태그는 And.intro 선언에서 사용된 매개변수의 이름으로부터 추론됩니다. case <tag> => <tactics> 표기법을 사용하여 택틱을 구조화할 수 있습니다. 다음은 이 장의 첫 번째 택틱 증명을 구조화한 버전입니다.

theorem test (p q : Prop) (hp : p) (hq : q) : p ∧ q ∧ p := p:Propq:Prophp:phq:q⊢ p ∧ q ∧ p p:Propq:Prophp:phq:q⊢ pp:Propq:Prophp:phq:q⊢ q ∧ p case left p:Propq:Prophp:phq:q⊢ p All goals completed! 🐙 case right p:Propq:Prophp:phq:q⊢ q ∧ p p:Propq:Prophp:phq:q⊢ qp:Propq:Prophp:phq:q⊢ p case left p:Propq:Prophp:phq:q⊢ q All goals completed! 🐙 case right p:Propq:Prophp:phq:q⊢ p All goals completed! 🐙

case 표기법을 사용하면 leftp:Propq:Prophp:phq:q⊢ p보다 rightp:Propq:Prophp:phq:q⊢ q ∧ p 하위 목표를 먼저 해결할 수 있습니다:

theorem test (p q : Prop) (hp : p) (hq : q) : p ∧ q ∧ p := p:Propq:Prophp:phq:q⊢ p ∧ q ∧ p p:Propq:Prophp:phq:q⊢ pp:Propq:Prophp:phq:q⊢ q ∧ p case right p:Propq:Prophp:phq:q⊢ q ∧ p p:Propq:Prophp:phq:q⊢ qp:Propq:Prophp:phq:q⊢ p case left p:Propq:Prophp:phq:q⊢ q All goals completed! 🐙 case right p:Propq:Prophp:phq:q⊢ p All goals completed! 🐙 case left p:Propq:Prophp:phq:q⊢ p All goals completed! 🐙

Lean이 다른 목표들을 case 블록 안에 숨긴다는 점에 유의하십시오. case left => 이후, 증명 상태는 다음과 같습니다.

p:Propq:Prophp:phq:q⊢ q

case가 선택된 목표에 “집중”한다고 말합니다. 게다가, case 블록의 끝에서 선택된 목표가 완전히 해결되지 않으면 Lean은 오류를 표시합니다.

간단한 하위 목표라면 태그를 사용해 하위 목표를 선택할 만한 가치가 없을 수도 있지만, 그래도 증명을 구조화하고 싶을 수 있습니다. Lean은 또한 증명을 구조화하기 위해 . <tactics> (또는 · <tactics>)라는 “불릿” 표기법을 제공합니다:

theorem test (p q : Prop) (hp : p) (hq : q) : p ∧ q ∧ p := p:Propq:Prophp:phq:q⊢ p ∧ q ∧ p p:Propq:Prophp:phq:q⊢ pp:Propq:Prophp:phq:q⊢ q ∧ p p:Propq:Prophp:phq:q⊢ p All goals completed! 🐙 p:Propq:Prophp:phq:q⊢ q ∧ p p:Propq:Prophp:phq:q⊢ qp:Propq:Prophp:phq:q⊢ p p:Propq:Prophp:phq:q⊢ q All goals completed! 🐙 p:Propq:Prophp:phq:q⊢ p All goals completed! 🐙

5.2. 기본 택틱🔗

apply와 exact에 더하여, 또 다른 유용한 택틱으로 가설을 도입하는 intro가 있습니다. 다음은 이전 장에서 증명했던 명제 논리의 항등식을 예로 들어, 이번에는 택틱을 사용하여 증명한 것입니다.

example (p q r : Prop) : p ∧ (q ∨ r) ↔ (p ∧ q) ∨ (p ∧ r) := p:Propq:Propr:Prop⊢ p ∧ (q ∨ r) ↔ p ∧ q ∨ p ∧ r p:Propq:Propr:Prop⊢ p ∧ (q ∨ r) → p ∧ q ∨ p ∧ rp:Propq:Propr:Prop⊢ p ∧ q ∨ p ∧ r → p ∧ (q ∨ r) p:Propq:Propr:Prop⊢ p ∧ (q ∨ r) → p ∧ q ∨ p ∧ r p:Propq:Propr:Proph:p ∧ (q ∨ r)⊢ p ∧ q ∨ p ∧ r p:Propq:Propr:Proph:p ∧ (q ∨ r)⊢ q → p ∧ q ∨ p ∧ rp:Propq:Propr:Proph:p ∧ (q ∨ r)⊢ r → p ∧ q ∨ p ∧ r p:Propq:Propr:Proph:p ∧ (q ∨ r)⊢ q → p ∧ q ∨ p ∧ r p:Propq:Propr:Proph:p ∧ (q ∨ r)hq:q⊢ p ∧ q ∨ p ∧ r p:Propq:Propr:Proph:p ∧ (q ∨ r)hq:q⊢ p ∧ q p:Propq:Propr:Proph:p ∧ (q ∨ r)hq:q⊢ pp:Propq:Propr:Proph:p ∧ (q ∨ r)hq:q⊢ q p:Propq:Propr:Proph:p ∧ (q ∨ r)hq:q⊢ p All goals completed! 🐙 p:Propq:Propr:Proph:p ∧ (q ∨ r)hq:q⊢ q All goals completed! 🐙 p:Propq:Propr:Proph:p ∧ (q ∨ r)⊢ r → p ∧ q ∨ p ∧ r p:Propq:Propr:Proph:p ∧ (q ∨ r)hr:r⊢ p ∧ q ∨ p ∧ r p:Propq:Propr:Proph:p ∧ (q ∨ r)hr:r⊢ p ∧ r p:Propq:Propr:Proph:p ∧ (q ∨ r)hr:r⊢ pp:Propq:Propr:Proph:p ∧ (q ∨ r)hr:r⊢ r p:Propq:Propr:Proph:p ∧ (q ∨ r)hr:r⊢ p All goals completed! 🐙 p:Propq:Propr:Proph:p ∧ (q ∨ r)hr:r⊢ r All goals completed! 🐙 p:Propq:Propr:Prop⊢ p ∧ q ∨ p ∧ r → p ∧ (q ∨ r) p:Propq:Propr:Proph:p ∧ q ∨ p ∧ r⊢ p ∧ (q ∨ r) p:Propq:Propr:Proph:p ∧ q ∨ p ∧ r⊢ p ∧ q → p ∧ (q ∨ r)p:Propq:Propr:Proph:p ∧ q ∨ p ∧ r⊢ p ∧ r → p ∧ (q ∨ r) p:Propq:Propr:Proph:p ∧ q ∨ p ∧ r⊢ p ∧ q → p ∧ (q ∨ r) p:Propq:Propr:Proph:p ∧ q ∨ p ∧ rhpq:p ∧ q⊢ p ∧ (q ∨ r) p:Propq:Propr:Proph:p ∧ q ∨ p ∧ rhpq:p ∧ q⊢ pp:Propq:Propr:Proph:p ∧ q ∨ p ∧ rhpq:p ∧ q⊢ q ∨ r p:Propq:Propr:Proph:p ∧ q ∨ p ∧ rhpq:p ∧ q⊢ p All goals completed! 🐙 p:Propq:Propr:Proph:p ∧ q ∨ p ∧ rhpq:p ∧ q⊢ q ∨ r p:Propq:Propr:Proph:p ∧ q ∨ p ∧ rhpq:p ∧ q⊢ q All goals completed! 🐙 p:Propq:Propr:Proph:p ∧ q ∨ p ∧ r⊢ p ∧ r → p ∧ (q ∨ r) p:Propq:Propr:Proph:p ∧ q ∨ p ∧ rhpr:p ∧ r⊢ p ∧ (q ∨ r) p:Propq:Propr:Proph:p ∧ q ∨ p ∧ rhpr:p ∧ r⊢ pp:Propq:Propr:Proph:p ∧ q ∨ p ∧ rhpr:p ∧ r⊢ q ∨ r p:Propq:Propr:Proph:p ∧ q ∨ p ∧ rhpr:p ∧ r⊢ p All goals completed! 🐙 p:Propq:Propr:Proph:p ∧ q ∨ p ∧ rhpr:p ∧ r⊢ q ∨ r p:Propq:Propr:Proph:p ∧ q ∨ p ∧ rhpr:p ∧ r⊢ r All goals completed! 🐙

intro 명령은 더 일반적으로 임의의 타입을 가진 변수를 도입하는 데 사용할 수 있습니다:

example (α : Type) : α → α := α:Type⊢ α → α α:Typea:α⊢ α All goals completed! 🐙 example (α : Type) : ∀ x : α, x = x := α:Type⊢ ∀ (x : α), x = x α:Typex:α⊢ x = x All goals completed! 🐙

이를 사용하여 여러 변수를 도입할 수 있습니다:

example : ∀ a b c : Nat, a = b → a = c → c = b := ⊢ ∀ (a b c : Nat), a = b → a = c → c = b a:Natb:Natc:Nath₁:a = bh₂:a = c⊢ c = b All goals completed! 🐙

apply 택틱이 함수 적용을 대화식으로 구성하기 위한 명령인 것처럼, intro 택틱은 함수 추상화(즉, fun x => e 형태의 항)를 대화식으로 구성하기 위한 명령입니다. 람다 추상화 표기법과 마찬가지로, intro 택틱을 사용하면 암묵적 match를 사용할 수 있습니다.

example (p q : α → Prop) : (∃ x, p x ∧ q x) → ∃ x, q x ∧ p x := α:Sort u_1p:α → Propq:α → Prop⊢ (∃ x, p x ∧ q x) → ∃ x, q x ∧ p x α:Sort u_1p:α → Propq:α → Propw:αhpw:p whqw:q w⊢ ∃ x, q x ∧ p x All goals completed! 🐙

match 표현식에서와 같이 여러 대안을 제공할 수도 있습니다.

example (p q : α → Prop) : (∃ x, p x ∨ q x) → ∃ x, q x ∨ p x := α:Sort u_1p:α → Propq:α → Prop⊢ (∃ x, p x ∨ q x) → ∃ x, q x ∨ p x intro α:Sort u_1p:α → Propq:α → Propx✝:∃ x, p x ∨ q xw:αh:p w⊢ ∃ x, q x ∨ p x All goals completed! 🐙 α:Sort u_1p:α → Propq:α → Propx✝:∃ x, p x ∨ q xw:αh:q w⊢ ∃ x, q x ∨ p x All goals completed! 🐙

intros 택틱은 인자 없이 사용할 수도 있으며, 이 경우 이름을 스스로 선택해 가능한 한 많은 변수를 도입합니다. 잠시 후 이에 대한 예제를 보게 될 것입니다.

assumption 택틱은 현재 목표의 맥락에 있는 가정들을 살펴보고, 결론과 일치하는 것이 있으면 이를 적용합니다.

variable (x y z w : Nat) example (h₁ : x = y) (h₂ : y = z) (h₃ : z = w) : x = w := x:Naty:Natz:Natw:Nath₁:x = yh₂:y = zh₃:z = w⊢ x = w x:Naty:Natz:Natw:Nath₁:x = yh₂:y = zh₃:z = w⊢ y = w x:Naty:Natz:Natw:Nath₁:x = yh₂:y = zh₃:z = w⊢ z = w All goals completed! 🐙 -- applied h₃

필요한 경우 결론에 있는 메타변수를 통합합니다:

variable (x y z w : Nat) example (h₁ : x = y) (h₂ : y = z) (h₃ : z = w) : x = w := x:Naty:Natz:Natw:Nath₁:x = yh₂:y = zh₃:z = w⊢ x = w x:Naty:Natz:Natw:Nath₁:x = yh₂:y = zh₃:z = w⊢ x = ?bx:Naty:Natz:Natw:Nath₁:x = yh₂:y = zh₃:z = w⊢ ?b = wx:Naty:Natz:Natw:Nath₁:x = yh₂:y = zh₃:z = w⊢ Nat x:Naty:Natz:Natw:Nath₁:x = yh₂:y = zh₃:z = w⊢ y = w -- solves x = ?b with h₁ x:Naty:Natz:Natw:Nath₁:x = yh₂:y = zh₃:z = w⊢ y = ?h₂.bx:Naty:Natz:Natw:Nath₁:x = yh₂:y = zh₃:z = w⊢ ?h₂.b = wx:Naty:Natz:Natw:Nath₁:x = yh₂:y = zh₃:z = w⊢ Nat x:Naty:Natz:Natw:Nath₁:x = yh₂:y = zh₃:z = w⊢ z = w -- solves y = ?h₂.b with h₂ All goals completed! 🐙 -- solves z = w with h₃

다음 예제는 intros 명령을 사용하여 세 변수와 두 가설을 자동으로 도입합니다:

example : ∀ a b c : Nat, a = b → a = c → c = b := ⊢ ∀ (a b c : Nat), a = b → a = c → c = b a✝²:Natb✝:Natc✝:Nata✝¹:a✝² = b✝a✝:a✝² = c✝⊢ c✝ = b✝ a✝²:Natb✝:Natc✝:Nata✝¹:a✝² = b✝a✝:a✝² = c✝⊢ c✝ = ?ba✝²:Natb✝:Natc✝:Nata✝¹:a✝² = b✝a✝:a✝² = c✝⊢ ?b = b✝a✝²:Natb✝:Natc✝:Nata✝¹:a✝² = b✝a✝:a✝² = c✝⊢ Nat a✝²:Natb✝:Natc✝:Nata✝¹:a✝² = b✝a✝:a✝² = c✝⊢ ?b✝ = c✝a✝²:Natb✝:Natc✝:Nata✝¹:a✝² = b✝a✝:a✝² = c✝⊢ ?b = b✝a✝²:Natb✝:Natc✝:Nata✝¹:a✝² = b✝a✝:a✝² = c✝⊢ Nat a✝²:Natb✝:Natc✝:Nata✝¹:a✝² = b✝a✝:a✝² = c✝⊢ a✝² = b✝ All goals completed! 🐙

Lean이 자동으로 생성한 이름은 기본적으로 접근할 수 없다는 점에 유의하십시오. 그 취지는 여러분의 택틱 증명이 자동으로 생성된 이름에 의존하지 않도록 하여, 결과적으로 더 견고해지도록 하는 것입니다. 하지만 조합자 unhygienic을 사용하면 이 제한을 해제할 수 있습니다.

example : ∀ a b c : Nat, a = b → a = c → c = b := ⊢ ∀ (a b c : Nat), a = b → a = c → c = b unhygienic a:Natb:Natc:Nata_1:a = ba_2:a = c⊢ c = b a:Natb:Natc:Nata_1:a = ba_2:a = c⊢ c = ?ba:Natb:Natc:Nata_1:a = ba_2:a = c⊢ ?b = ba:Natb:Natc:Nata_1:a = ba_2:a = c⊢ Nat a:Natb:Natc:Nata_1:a = ba_2:a = c⊢ ?b✝ = ca:Natb:Natc:Nata_1:a = ba_2:a = c⊢ ?b = ba:Natb:Natc:Nata_1:a = ba_2:a = c⊢ Nat a:Natb:Natc:Nata_1:a = ba_2:a = c⊢ a = b All goals completed! 🐙

또한 rename_i 택틱을 사용하여 맥락에서 가장 최근의 접근 불가능한 이름의 이름을 바꿀 수 있습니다. 다음 예제에서 rename_i h1 _ h2 택틱은 맥락에 있는 마지막 세 가지 가정 중 두 가지의 이름을 바꿉니다.

example : ∀ a b c d : Nat, a = b → a = d → a = c → c = b := ⊢ ∀ (a b c d : Nat), a = b → a = d → a = c → c = b a✝³:Natb✝:Natc✝:Natd✝:Nata✝²:a✝³ = b✝a✝¹:a✝³ = d✝a✝:a✝³ = c✝⊢ c✝ = b✝ a✝¹:Natb✝:Natc✝:Natd✝:Nath1:a✝³ = b✝a✝:a✝³ = d✝h2:a✝³ = c✝⊢ c✝ = b✝ a✝¹:Natb✝:Natc✝:Natd✝:Nath1:a✝³ = b✝a✝:a✝³ = d✝h2:a✝³ = c✝⊢ c✝ = ?ba✝¹:Natb✝:Natc✝:Natd✝:Nath1:a✝³ = b✝a✝:a✝³ = d✝h2:a✝³ = c✝⊢ ?b = b✝a✝¹:Natb✝:Natc✝:Natd✝:Nath1:a✝³ = b✝a✝:a✝³ = d✝h2:a✝³ = c✝⊢ Nat a✝¹:Natb✝:Natc✝:Natd✝:Nath1:a✝³ = b✝a✝:a✝³ = d✝h2:a✝³ = c✝⊢ ?b✝ = c✝a✝¹:Natb✝:Natc✝:Natd✝:Nath1:a✝³ = b✝a✝:a✝³ = d✝h2:a✝³ = c✝⊢ ?b = b✝a✝¹:Natb✝:Natc✝:Natd✝:Nath1:a✝³ = b✝a✝:a✝³ = d✝h2:a✝³ = c✝⊢ Nat a✝¹:Natb✝:Natc✝:Natd✝:Nath1:a✝³ = b✝a✝:a✝³ = d✝h2:a✝³ = c✝⊢ a✝³ = b✝ All goals completed! 🐙

rfl 택틱은 정의적으로 같은 인자에 적용된 반사 관계인 목표를 해결합니다. 동치는 반사적입니다:

example (y : Nat) : (fun Variable name `x` is not explicitly referenced. Hint: The binding can be removed (if unused) or named `_` (if used implicitly). Alternatively, prefix the name with `_` to silence this warning: [apply] _x Note: This linter can be disabled with `set_option linter.unusedVariables false`x : Nat => 0) y = 0 := y:Nat⊢ (fun x => 0) y = 0 All goals completed! 🐙

repeat 조합자는 택틱을 여러 번 적용하는 데 사용할 수 있습니다:

example : ∀ a b c : Nat, a = b → a = c → c = b := ⊢ ∀ (a b c : Nat), a = b → a = c → c = b a✝²:Natb✝:Natc✝:Nata✝¹:a✝² = b✝a✝:a✝² = c✝⊢ c✝ = b✝ a✝²:Natb✝:Natc✝:Nata✝¹:a✝² = b✝a✝:a✝² = c✝⊢ c✝ = ?ba✝²:Natb✝:Natc✝:Nata✝¹:a✝² = b✝a✝:a✝² = c✝⊢ ?b = b✝a✝²:Natb✝:Natc✝:Nata✝¹:a✝² = b✝a✝:a✝² = c✝⊢ Nat a✝²:Natb✝:Natc✝:Nata✝¹:a✝² = b✝a✝:a✝² = c✝⊢ ?b✝ = c✝a✝²:Natb✝:Natc✝:Nata✝¹:a✝² = b✝a✝:a✝² = c✝⊢ ?b = b✝a✝²:Natb✝:Natc✝:Nata✝¹:a✝² = b✝a✝:a✝² = c✝⊢ Nat repeat All goals completed! 🐙

때때로 유용한 또 다른 택틱으로 revert 택틱이 있는데, 이는 어떤 의미에서 intro의 역이라 할 수 있습니다:

example (x : Nat) : x = x := x:Nat⊢ x = x ⊢ ∀ (x : Nat), x = x y:Nat⊢ y = y All goals completed! 🐙

revert x를 실행하면, 증명 상태는 다음과 같습니다:

⊢ ∀ (x : Nat), x = x

intro y를 실행한 후에는 다음과 같습니다:

y:Nat⊢ y = y

가설을 목표로 옮기면 함의가 만들어집니다:

example (x y : Nat) (h : x = y) : y = x := x:Naty:Nath:x = y⊢ y = x x:Naty:Nat⊢ x = y → y = x x:Naty:Nath₁:x = y⊢ y = x -- goal is x y : Nat, h₁ : x = y ⊢ y = x x:Naty:Nath₁:x = y⊢ x = y All goals completed! 🐙

revert h를 실행한 후, 증명 상태는 다음과 같습니다:

x:Naty:Nat⊢ x = y → y = x

intro h₁ 이후에는 다음과 같습니다:

x:Naty:Nath₁:x = y⊢ y = x

하지만 revert는 한층 더 영리해서, 맥락의 한 요소뿐만 아니라 그 요소에 의존하는 맥락의 이후 모든 요소도 되돌립니다. 예를 들어, 위 예시에서 x를 되돌리면 h도 함께 딸려 옵니다.

example (x y : Nat) (h : x = y) : y = x := x:Naty:Nath:x = y⊢ y = x y:Nat⊢ ∀ (x : Nat), x = y → y = x y:Natx✝:Nath✝:x✝ = y⊢ y = x✝ y:Natx✝:Nath✝:x✝ = y⊢ x✝ = y All goals completed! 🐙

revert x를 실행한 후, 목표는 다음과 같습니다:

y:Nat⊢ ∀ (x : Nat), x = y → y = x

컨텍스트의 여러 요소를 한 번에 되돌릴 수도 있습니다:

example (x y : Nat) (h : x = y) : y = x := x:Naty:Nath:x = y⊢ y = x ⊢ ∀ (x y : Nat), x = y → y = x x✝:Naty✝:Nath✝:x✝ = y✝⊢ y✝ = x✝ x✝:Naty✝:Nath✝:x✝ = y✝⊢ x✝ = y✝ All goals completed! 🐙

revert x y를 실행한 후, 목표는 다음과 같습니다:

⊢ ∀ (x y : Nat), x = y → y = x

로컬 컨텍스트의 요소, 즉 로컬 변수나 가설만 revert할 수 있습니다. 하지만 generalize 택틱을 사용하면 목표 안의 임의의 식을 새로운 변수로 치환할 수 있습니다.

example : 3 = 3 := ⊢ 3 = 3 x:Nat⊢ x = x ⊢ ∀ (x : Nat), x = x y:Nat⊢ y = y All goals completed! 🐙

특히, generalize를 사용한 후 목표는 다음과 같습니다.

x:Nat⊢ x = x

위 표기법의 기억법은 목표에서 3을 임의의 변수 x로 설정하여 일반화한다는 것입니다. 주의하십시오: 모든 일반화가 목표의 타당성을 보존하는 것은 아닙니다. 여기서 generalize는 rfl을 사용해 증명할 수 있었던 목표를 증명할 수 없는 목표로 바꿉니다:

declaration uses `sorry`example : 2 + 3 = 5 := ⊢ 2 + 3 = 5 x:Nat⊢ 2 + x = 5 All goals completed! 🐙

이 예제에서 sorry 택틱은 sorry 증명 항의 대응물입니다. 이는 현재 목표를 닫으며, sorry가 사용되었다는 통상적인 경고를 발생시킵니다. 이전 목표의 유효성을 보존하기 위해, generalize 택틱을 사용하면 3이 x로 대체되었다는 사실을 기록할 수 있습니다. 필요한 작업은 레이블을 하나 제공하는 것뿐이며, generalize는 이를 사용하여 로컬 컨텍스트에 그 대입을 저장합니다:

example : 2 + 3 = 5 := ⊢ 2 + 3 = 5 x:Nath:3 = x⊢ 2 + x = 5 All goals completed! 🐙

generalize h : 3 = x를 실행한 후, h는 3 = x라는 명제의 증명입니다:

x:Nath:3 = x⊢ 2 + x = 5

여기서 재작성 택틱 rw는 h를 사용하여 x를 다시 3으로 치환합니다. rw 택틱은 아래에서 다룰 것입니다.

5.3. 더 많은 택틱🔗

명제와 데이터를 구성하거나 분해하는 데 유용한 몇 가지 추가 택틱이 있습니다. 예를 들어, p ∨ q 형태의 목표에 적용할 때는 apply Or.inl이나 apply Or.inr과 같은 택틱을 사용합니다. 반대로, cases 택틱은 논리합을 분해하는 데 사용할 수 있습니다.

example (p q : Prop) : p ∨ q → q ∨ p := p:Propq:Prop⊢ p ∨ q → q ∨ p p:Propq:Proph:p ∨ q⊢ q ∨ p cases h with p:Propq:Prophp:p⊢ q ∨ p p:Propq:Prophp:p⊢ p; All goals completed! 🐙 p:Propq:Prophq:q⊢ q ∨ p p:Propq:Prophq:q⊢ q; All goals completed! 🐙

이 구문은 match 표현식에서 사용되는 구문과 유사하다는 점에 유의하십시오. 새로 생긴 하위 목표는 어떤 순서로든 해결할 수 있습니다.

example (p q : Prop) : p ∨ q → q ∨ p := p:Propq:Prop⊢ p ∨ q → q ∨ p p:Propq:Proph:p ∨ q⊢ q ∨ p cases h with p:Propq:Prophq:q⊢ q ∨ p p:Propq:Prophq:q⊢ q; All goals completed! 🐙 p:Propq:Prophp:p⊢ q ∨ p p:Propq:Prophp:p⊢ p; All goals completed! 🐙

with와 각 경우에 대한 택틱 없이 (비구조적) cases를 사용할 수도 있습니다:

example (p q : Prop) : p ∨ q → q ∨ p := p:Propq:Prop⊢ p ∨ q → q ∨ p p:Propq:Proph:p ∨ q⊢ q ∨ p p:Propq:Proph✝:p⊢ q ∨ pp:Propq:Proph✝:q⊢ q ∨ p p:Propq:Proph✝:p⊢ pp:Propq:Proph✝:q⊢ q ∨ p p:Propq:Proph✝:q⊢ q ∨ p p:Propq:Proph✝:q⊢ q All goals completed! 🐙

(구조화되지 않은) cases는 동일한 택틱을 사용하여 여러 하위 목표를 닫을 수 있는 경우 특히 유용합니다:

example (p : Prop) : p ∨ p → p := p:Prop⊢ p ∨ p → p p:Proph:p ∨ p⊢ p p:Proph✝:p⊢ pp:Proph✝:p⊢ p repeat All goals completed! 🐙

또한 tac1 <;> tac2 조합기를 사용하여 택틱 tac1이 생성하는 각 하위 목표에 tac2를 적용할 수도 있습니다:

example (p : Prop) : p ∨ p → p := p:Prop⊢ p ∨ p → p p:Proph:p ∨ p⊢ p p:Proph✝:p⊢ pp:Proph✝:p⊢ p p:Proph✝:p⊢ pp:Proph✝:p⊢ p All goals completed! 🐙

구조화되지 않은 cases 택틱을 case와 . 표기법과 결합할 수 있습니다:

example (p q : Prop) : p ∨ q → q ∨ p := p:Propq:Prop⊢ p ∨ q → q ∨ p p:Propq:Proph:p ∨ q⊢ q ∨ p p:Propq:Proph✝:p⊢ q ∨ pp:Propq:Proph✝:q⊢ q ∨ p p:Propq:Proph✝:p⊢ q ∨ p p:Propq:Proph✝:p⊢ p All goals completed! 🐙 p:Propq:Proph✝:q⊢ q ∨ p p:Propq:Proph✝:q⊢ q All goals completed! 🐙 example (p q : Prop) : p ∨ q → q ∨ p := p:Propq:Prop⊢ p ∨ q → q ∨ p p:Propq:Proph:p ∨ q⊢ q ∨ p p:Propq:Proph✝:p⊢ q ∨ pp:Propq:Proph✝:q⊢ q ∨ p case inr h p:Propq:Proph:q⊢ q ∨ p p:Propq:Proph:q⊢ q All goals completed! 🐙 case inl h p:Propq:Proph:p⊢ q ∨ p p:Propq:Proph:p⊢ p All goals completed! 🐙 example (p q : Prop) : p ∨ q → q ∨ p := p:Propq:Prop⊢ p ∨ q → q ∨ p p:Propq:Proph:p ∨ q⊢ q ∨ p p:Propq:Proph✝:p⊢ q ∨ pp:Propq:Proph✝:q⊢ q ∨ p case inr h p:Propq:Proph:q⊢ q ∨ p p:Propq:Proph:q⊢ q All goals completed! 🐙 p:Propq:Proph✝:p⊢ q ∨ p p:Propq:Proph✝:p⊢ p All goals completed! 🐙

cases 택틱은 논리곱을 분해하는 데에도 사용할 수 있습니다:

example (p q : Prop) : p ∧ q → q ∧ p := p:Propq:Prop⊢ p ∧ q → q ∧ p p:Propq:Proph:p ∧ q⊢ q ∧ p cases h with p:Propq:Prophp:phq:q⊢ q ∧ p p:Propq:Prophp:phq:q⊢ qp:Propq:Prophp:phq:q⊢ p; p:Propq:Prophp:phq:q⊢ p; All goals completed! 🐙

이 예제에서는 cases 택틱을 적용한 후 목표가 하나만 남으며, h : p ∧ q는 hp : p와 hq : q라는 한 쌍의 가정으로 대체됩니다:

p:Propq:Prophp:phq:q⊢ q ∧ p

constructor 택틱은 논리곱(conjunction)에 대한 유일한 생성자인 And.intro를 적용합니다.

이러한 택틱들을 사용하면 이전 절의 예제를 다음과 같이 다시 작성할 수 있습니다.

example (p q r : Prop) : p ∧ (q ∨ r) ↔ (p ∧ q) ∨ (p ∧ r) := p:Propq:Propr:Prop⊢ p ∧ (q ∨ r) ↔ p ∧ q ∨ p ∧ r p:Propq:Propr:Prop⊢ p ∧ (q ∨ r) → p ∧ q ∨ p ∧ rp:Propq:Propr:Prop⊢ p ∧ q ∨ p ∧ r → p ∧ (q ∨ r) p:Propq:Propr:Prop⊢ p ∧ (q ∨ r) → p ∧ q ∨ p ∧ r p:Propq:Propr:Proph:p ∧ (q ∨ r)⊢ p ∧ q ∨ p ∧ r cases h with p:Propq:Propr:Prophp:phqr:q ∨ r⊢ p ∧ q ∨ p ∧ r p:Propq:Propr:Prophp:ph✝:q⊢ p ∧ q ∨ p ∧ rp:Propq:Propr:Prophp:ph✝:r⊢ p ∧ q ∨ p ∧ r p:Propq:Propr:Prophp:ph✝:q⊢ p ∧ q ∨ p ∧ r p:Propq:Propr:Prophp:ph✝:q⊢ p ∧ q; p:Propq:Propr:Prophp:ph✝:q⊢ pp:Propq:Propr:Prophp:ph✝:q⊢ q p:Propq:Propr:Prophp:ph✝:q⊢ pp:Propq:Propr:Prophp:ph✝:q⊢ q All goals completed! 🐙 p:Propq:Propr:Prophp:ph✝:r⊢ p ∧ q ∨ p ∧ r p:Propq:Propr:Prophp:ph✝:r⊢ p ∧ r; p:Propq:Propr:Prophp:ph✝:r⊢ pp:Propq:Propr:Prophp:ph✝:r⊢ r p:Propq:Propr:Prophp:ph✝:r⊢ pp:Propq:Propr:Prophp:ph✝:r⊢ r All goals completed! 🐙 p:Propq:Propr:Prop⊢ p ∧ q ∨ p ∧ r → p ∧ (q ∨ r) p:Propq:Propr:Proph:p ∧ q ∨ p ∧ r⊢ p ∧ (q ∨ r) cases h with p:Propq:Propr:Prophpq:p ∧ q⊢ p ∧ (q ∨ r) cases hpq with p:Propq:Propr:Prophp:phq:q⊢ p ∧ (q ∨ r) p:Propq:Propr:Prophp:phq:q⊢ pp:Propq:Propr:Prophp:phq:q⊢ q ∨ r; p:Propq:Propr:Prophp:phq:q⊢ q ∨ r; p:Propq:Propr:Prophp:phq:q⊢ q; All goals completed! 🐙 p:Propq:Propr:Prophpr:p ∧ r⊢ p ∧ (q ∨ r) cases hpr with p:Propq:Propr:Prophp:phr:r⊢ p ∧ (q ∨ r) p:Propq:Propr:Prophp:phr:r⊢ pp:Propq:Propr:Prophp:phr:r⊢ q ∨ r; p:Propq:Propr:Prophp:phr:r⊢ q ∨ r; p:Propq:Propr:Prophp:phr:r⊢ r; All goals completed! 🐙

귀납적 타입에서 이러한 택틱들이 상당히 일반적이라는 사실을 보게 될 것입니다. cases 택틱은 귀납적으로 정의된 타입의 어떤 원소든 분해하는 데 사용할 수 있으며, constructor는 귀납적으로 정의된 타입에서 적용 가능한 첫 번째 생성자를 항상 적용합니다. 예를 들어, 존재 한정사에 대해 cases와 constructor를 사용할 수 있습니다.

example (p q : Nat → Prop) : (∃ x, p x) → ∃ x, p x ∨ q x := p:Nat → Propq:Nat → Prop⊢ (∃ x, p x) → ∃ x, p x ∨ q x p:Nat → Propq:Nat → Proph:∃ x, p x⊢ ∃ x, p x ∨ q x cases h with p:Nat → Propq:Nat → Propx:Natpx:p x⊢ ∃ x, p x ∨ q x p:Nat → Propq:Nat → Propx:Natpx:p x⊢ p ?intro.w ∨ q ?intro.wp:Nat → Propq:Nat → Propx:Natpx:p x⊢ Nat; p:Nat → Propq:Nat → Propx:Natpx:p x⊢ p ?intro.wp:Nat → Propq:Nat → Propx:Natpx:p x⊢ Nat; All goals completed! 🐙

여기서 constructor 택틱은 존재 명제의 첫 번째 구성 요소인 x의 값을 암시적인 상태로 남겨 둡니다. 이 값은 메타변수로 표현되며, 나중에 구체적인 값이 채워져야 합니다. 앞선 예제에서 메타변수의 적절한 값은 exact px 택틱에 의해 결정되는데, 이는 px가 p x 타입을 가지기 때문입니다. 존재 한정사에 대한 증인을 명시적으로 지정하고 싶다면, 대신 exists 택틱을 사용할 수 있습니다.

example (p q : Nat → Prop) : (∃ x, p x) → ∃ x, p x ∨ q x := p:Nat → Propq:Nat → Prop⊢ (∃ x, p x) → ∃ x, p x ∨ q x p:Nat → Propq:Nat → Proph:∃ x, p x⊢ ∃ x, p x ∨ q x cases h with p:Nat → Propq:Nat → Propx:Natpx:p x⊢ ∃ x, p x ∨ q x p:Nat → Propq:Nat → Propx:Natpx:p x⊢ p x ∨ q x; p:Nat → Propq:Nat → Propx:Natpx:p x⊢ p x; All goals completed! 🐙

또 다른 예시는 다음과 같습니다:

example (p q : Nat → Prop) : (∃ x, p x ∧ q x) → ∃ x, q x ∧ p x := p:Nat → Propq:Nat → Prop⊢ (∃ x, p x ∧ q x) → ∃ x, q x ∧ p x p:Nat → Propq:Nat → Proph:∃ x, p x ∧ q x⊢ ∃ x, q x ∧ p x cases h with p:Nat → Propq:Nat → Propx:Nathpq:p x ∧ q x⊢ ∃ x, q x ∧ p x cases hpq with p:Nat → Propq:Nat → Propx:Nathp:p xhq:q x⊢ ∃ x, q x ∧ p x All goals completed! 🐙

이러한 택틱은 명제뿐만 아니라 데이터에도 마찬가지로 사용할 수 있습니다. 다음 예제에서는 이를 사용하여 곱 타입과 합 타입의 구성 요소를 교환하는 함수를 정의합니다.

def swap_pair : α × β → β × α := α:Type ?u.6β:Type ?u.5⊢ α × β → β × α α:Type ?u.6β:Type ?u.5p:α × β⊢ β × α α:Type ?u.6β:Type ?u.5fst✝:αsnd✝:β⊢ β × α α:Type ?u.6β:Type ?u.5fst✝:αsnd✝:β⊢ βα:Type ?u.6β:Type ?u.5fst✝:αsnd✝:β⊢ α α:Type ?u.6β:Type ?u.5fst✝:αsnd✝:β⊢ βα:Type ?u.6β:Type ?u.5fst✝:αsnd✝:β⊢ α All goals completed! 🐙 def swap_sum : Sum α β → Sum β α := α:Type ?u.6β:Type ?u.5⊢ α ⊕ β → β ⊕ α α:Type ?u.6β:Type ?u.5p:α ⊕ β⊢ β ⊕ α α:Type ?u.6β:Type ?u.5val✝:α⊢ β ⊕ αα:Type ?u.6β:Type ?u.5val✝:β⊢ β ⊕ α α:Type ?u.6β:Type ?u.5val✝:α⊢ β ⊕ α α:Type ?u.6β:Type ?u.5val✝:α⊢ α; All goals completed! 🐙 α:Type ?u.6β:Type ?u.5val✝:β⊢ β ⊕ α α:Type ?u.6β:Type ?u.5val✝:β⊢ β; All goals completed! 🐙

변수에 대해 선택한 이름을 제외하면, 이 정의들은 논리곱과 논리합에 대한 유사한 명제들의 증명과 동일하다는 점에 유의하십시오. cases 택틱은 자연수에 대한 경우 구분도 수행합니다.

open Nat example (P : Nat → Prop) (h₀ : P 0) (h₁ : ∀ n, P (succ n)) (m : Nat) : P m := P:Nat → Proph₀:P 0h₁:∀ (n : Nat), P n.succm:Nat⊢ P m cases m with P:Nat → Proph₀:P 0h₁:∀ (n : Nat), P n.succ⊢ P 0 All goals completed! 🐙 P:Nat → Proph₀:P 0h₁:∀ (n : Nat), P n.succm':Nat⊢ P (m' + 1) All goals completed! 🐙

cases 택틱과 그 동반 택틱인 induction 택틱은 귀납적 타입을 위한 택틱 절에서 더 자세히 다룹니다.

contradiction 택틱은 현재 목표의 가설 중에서 모순을 찾습니다.

example (p q : Prop) : p ∧ ¬ p → q := p:Propq:Prop⊢ p ∧ ¬p → q p:Propq:Proph:p ∧ ¬p⊢ q p:Propq:Propleft✝:pright✝:¬p⊢ q All goals completed! 🐙

택틱 블록에서도 match를 사용할 수 있습니다.

example (p q r : Prop) : p ∧ (q ∨ r) ↔ (p ∧ q) ∨ (p ∧ r) := p:Propq:Propr:Prop⊢ p ∧ (q ∨ r) ↔ p ∧ q ∨ p ∧ r p:Propq:Propr:Prop⊢ p ∧ (q ∨ r) → p ∧ q ∨ p ∧ rp:Propq:Propr:Prop⊢ p ∧ q ∨ p ∧ r → p ∧ (q ∨ r) p:Propq:Propr:Prop⊢ p ∧ (q ∨ r) → p ∧ q ∨ p ∧ r p:Propq:Propr:Proph:p ∧ (q ∨ r)⊢ p ∧ q ∨ p ∧ r match h with p:Propq:Propr:Proph:p ∧ (q ∨ r)left✝:ph✝:q⊢ p ∧ q ∨ p ∧ r p:Propq:Propr:Proph:p ∧ (q ∨ r)left✝:ph✝:q⊢ p ∧ q; p:Propq:Propr:Proph:p ∧ (q ∨ r)left✝:ph✝:q⊢ pp:Propq:Propr:Proph:p ∧ (q ∨ r)left✝:ph✝:q⊢ q p:Propq:Propr:Proph:p ∧ (q ∨ r)left✝:ph✝:q⊢ pp:Propq:Propr:Proph:p ∧ (q ∨ r)left✝:ph✝:q⊢ q All goals completed! 🐙 p:Propq:Propr:Proph:p ∧ (q ∨ r)left✝:ph✝:r⊢ p ∧ q ∨ p ∧ r p:Propq:Propr:Proph:p ∧ (q ∨ r)left✝:ph✝:r⊢ p ∧ r; p:Propq:Propr:Proph:p ∧ (q ∨ r)left✝:ph✝:r⊢ pp:Propq:Propr:Proph:p ∧ (q ∨ r)left✝:ph✝:r⊢ r p:Propq:Propr:Proph:p ∧ (q ∨ r)left✝:ph✝:r⊢ pp:Propq:Propr:Proph:p ∧ (q ∨ r)left✝:ph✝:r⊢ r All goals completed! 🐙 p:Propq:Propr:Prop⊢ p ∧ q ∨ p ∧ r → p ∧ (q ∨ r) p:Propq:Propr:Proph:p ∧ q ∨ p ∧ r⊢ p ∧ (q ∨ r) match h with p:Propq:Propr:Proph:p ∧ q ∨ p ∧ rhp:phq:q⊢ p ∧ (q ∨ r) p:Propq:Propr:Proph:p ∧ q ∨ p ∧ rhp:phq:q⊢ pp:Propq:Propr:Proph:p ∧ q ∨ p ∧ rhp:phq:q⊢ q ∨ r; p:Propq:Propr:Proph:p ∧ q ∨ p ∧ rhp:phq:q⊢ q ∨ r; p:Propq:Propr:Proph:p ∧ q ∨ p ∧ rhp:phq:q⊢ q; All goals completed! 🐙 p:Propq:Propr:Proph:p ∧ q ∨ p ∧ rhp:phr:r⊢ p ∧ (q ∨ r) p:Propq:Propr:Proph:p ∧ q ∨ p ∧ rhp:phr:r⊢ pp:Propq:Propr:Proph:p ∧ q ∨ p ∧ rhp:phr:r⊢ q ∨ r; p:Propq:Propr:Proph:p ∧ q ∨ p ∧ rhp:phr:r⊢ q ∨ r; p:Propq:Propr:Proph:p ∧ q ∨ p ∧ rhp:phr:r⊢ r; All goals completed! 🐙

intro와 match를 “결합”하여 앞선 예제들을 다음과 같이 작성할 수 있습니다:

example (p q r : Prop) : p ∧ (q ∨ r) ↔ (p ∧ q) ∨ (p ∧ r) := p:Propq:Propr:Prop⊢ p ∧ (q ∨ r) ↔ p ∧ q ∨ p ∧ r p:Propq:Propr:Prop⊢ p ∧ (q ∨ r) → p ∧ q ∨ p ∧ rp:Propq:Propr:Prop⊢ p ∧ q ∨ p ∧ r → p ∧ (q ∨ r) p:Propq:Propr:Prop⊢ p ∧ (q ∨ r) → p ∧ q ∨ p ∧ r intro p:Propq:Propr:Propx✝:p ∧ (q ∨ r)hp:phq:q⊢ p ∧ q ∨ p ∧ r p:Propq:Propr:Propx✝:p ∧ (q ∨ r)hp:phq:q⊢ p ∧ q; p:Propq:Propr:Propx✝:p ∧ (q ∨ r)hp:phq:q⊢ pp:Propq:Propr:Propx✝:p ∧ (q ∨ r)hp:phq:q⊢ q p:Propq:Propr:Propx✝:p ∧ (q ∨ r)hp:phq:q⊢ pp:Propq:Propr:Propx✝:p ∧ (q ∨ r)hp:phq:q⊢ q All goals completed! 🐙 p:Propq:Propr:Propx✝:p ∧ (q ∨ r)hp:phr:r⊢ p ∧ q ∨ p ∧ r p:Propq:Propr:Propx✝:p ∧ (q ∨ r)hp:phr:r⊢ p ∧ r; p:Propq:Propr:Propx✝:p ∧ (q ∨ r)hp:phr:r⊢ pp:Propq:Propr:Propx✝:p ∧ (q ∨ r)hp:phr:r⊢ r p:Propq:Propr:Propx✝:p ∧ (q ∨ r)hp:phr:r⊢ pp:Propq:Propr:Propx✝:p ∧ (q ∨ r)hp:phr:r⊢ r All goals completed! 🐙 p:Propq:Propr:Prop⊢ p ∧ q ∨ p ∧ r → p ∧ (q ∨ r) intro p:Propq:Propr:Propx✝:p ∧ q ∨ p ∧ rhp:phq:q⊢ p ∧ (q ∨ r) p:Propq:Propr:Propx✝:p ∧ q ∨ p ∧ rhp:phq:q⊢ pp:Propq:Propr:Propx✝:p ∧ q ∨ p ∧ rhp:phq:q⊢ q ∨ r; p:Propq:Propr:Propx✝:p ∧ q ∨ p ∧ rhp:phq:q⊢ q ∨ r; p:Propq:Propr:Propx✝:p ∧ q ∨ p ∧ rhp:phq:q⊢ q; All goals completed! 🐙 p:Propq:Propr:Propx✝:p ∧ q ∨ p ∧ rhp:phr:r⊢ p ∧ (q ∨ r) p:Propq:Propr:Propx✝:p ∧ q ∨ p ∧ rhp:phr:r⊢ pp:Propq:Propr:Propx✝:p ∧ q ∨ p ∧ rhp:phr:r⊢ q ∨ r; p:Propq:Propr:Propx✝:p ∧ q ∨ p ∧ rhp:phr:r⊢ q ∨ r; p:Propq:Propr:Propx✝:p ∧ q ∨ p ∧ rhp:phr:r⊢ r; All goals completed! 🐙

5.4. 택틱 증명 구조화🔗

택틱은 종종 증명을 구성하는 효율적인 방법을 제공하지만, 명령어가 길게 이어지면 논증의 구조가 불명확해질 수 있습니다. 이 절에서는 택틱 스타일 증명에 구조를 부여하는 데 도움이 되는 몇 가지 수단을 설명하며, 이를 통해 그러한 증명을 더 읽기 쉽고 견고하게 만듭니다.

Lean의 증명 작성 구문에서 좋은 점 하나는 항 스타일 증명과 택틱 스타일 증명을 섞어서 사용하고, 둘 사이를 자유롭게 오갈 수 있다는 것입니다. 예를 들어, apply와 exact 택틱은 임의의 항을 기대하는데, 이는 have, show 등을 사용하여 작성할 수 있습니다. 반대로, 임의의 Lean 항을 작성할 때는 by 블록을 삽입하여 언제든지 택틱 모드를 호출할 수 있습니다. 다음은 다소 장난감 같은 예시입니다:

example (p q r : Prop) : p ∧ (q ∨ r) → (p ∧ q) ∨ (p ∧ r) := p:Propq:Propr:Prop⊢ p ∧ (q ∨ r) → p ∧ q ∨ p ∧ r p:Propq:Propr:Proph:p ∧ (q ∨ r)⊢ p ∧ q ∨ p ∧ r exact have hp : p := h.left have hqr : q ∨ r := h.right show (p ∧ q) ∨ (p ∧ r) p:Propq:Propr:Prop⊢ p ∧ (q ∨ r) → p ∧ q ∨ p ∧ r cases hqr with p:Propq:Propr:Proph:p ∧ (q ∨ r)hp:phq:q⊢ p ∧ q ∨ p ∧ r All goals completed! 🐙 p:Propq:Propr:Proph:p ∧ (q ∨ r)hp:phr:r⊢ p ∧ q ∨ p ∧ r All goals completed! 🐙

다음은 더 자연스러운 예시입니다:

example (p q r : Prop) : p ∧ (q ∨ r) ↔ (p ∧ q) ∨ (p ∧ r) := p:Propq:Propr:Prop⊢ p ∧ (q ∨ r) ↔ p ∧ q ∨ p ∧ r p:Propq:Propr:Prop⊢ p ∧ (q ∨ r) → p ∧ q ∨ p ∧ rp:Propq:Propr:Prop⊢ p ∧ q ∨ p ∧ r → p ∧ (q ∨ r) p:Propq:Propr:Prop⊢ p ∧ (q ∨ r) → p ∧ q ∨ p ∧ r p:Propq:Propr:Proph:p ∧ (q ∨ r)⊢ p ∧ q ∨ p ∧ r cases h.right with p:Propq:Propr:Proph:p ∧ (q ∨ r)hq:q⊢ p ∧ q ∨ p ∧ r All goals completed! 🐙 p:Propq:Propr:Proph:p ∧ (q ∨ r)hr:r⊢ p ∧ q ∨ p ∧ r All goals completed! 🐙 p:Propq:Propr:Prop⊢ p ∧ q ∨ p ∧ r → p ∧ (q ∨ r) p:Propq:Propr:Proph:p ∧ q ∨ p ∧ r⊢ p ∧ (q ∨ r) cases h with p:Propq:Propr:Prophpq:p ∧ q⊢ p ∧ (q ∨ r) All goals completed! 🐙 p:Propq:Propr:Prophpr:p ∧ r⊢ p ∧ (q ∨ r) All goals completed! 🐙

실제로 증명 항의 show 표현식과 유사한 show 택틱이 있습니다. 이는 택틱 모드를 유지한 채로, 곧 해결할 목표의 타입을 단순히 선언합니다.

example (p q r : Prop) : p ∧ (q ∨ r) ↔ (p ∧ q) ∨ (p ∧ r) := p:Propq:Propr:Prop⊢ p ∧ (q ∨ r) ↔ p ∧ q ∨ p ∧ r p:Propq:Propr:Prop⊢ p ∧ (q ∨ r) → p ∧ q ∨ p ∧ rp:Propq:Propr:Prop⊢ p ∧ q ∨ p ∧ r → p ∧ (q ∨ r) p:Propq:Propr:Prop⊢ p ∧ (q ∨ r) → p ∧ q ∨ p ∧ r p:Propq:Propr:Proph:p ∧ (q ∨ r)⊢ p ∧ q ∨ p ∧ r cases h.right with p:Propq:Propr:Proph:p ∧ (q ∨ r)hq:q⊢ p ∧ q ∨ p ∧ r p:Propq:Propr:Proph:p ∧ (q ∨ r)hq:q⊢ p ∧ q ∨ p ∧ r All goals completed! 🐙 p:Propq:Propr:Proph:p ∧ (q ∨ r)hr:r⊢ p ∧ q ∨ p ∧ r p:Propq:Propr:Proph:p ∧ (q ∨ r)hr:r⊢ p ∧ q ∨ p ∧ r All goals completed! 🐙 p:Propq:Propr:Prop⊢ p ∧ q ∨ p ∧ r → p ∧ (q ∨ r) p:Propq:Propr:Proph:p ∧ q ∨ p ∧ r⊢ p ∧ (q ∨ r) cases h with p:Propq:Propr:Prophpq:p ∧ q⊢ p ∧ (q ∨ r) p:Propq:Propr:Prophpq:p ∧ q⊢ p ∧ (q ∨ r) All goals completed! 🐙 p:Propq:Propr:Prophpr:p ∧ r⊢ p ∧ (q ∨ r) p:Propq:Propr:Prophpr:p ∧ r⊢ p ∧ (q ∨ r) All goals completed! 🐙

사실 show 택틱을 사용하면 목표를 정의적으로 동치인 다른 것으로 다시 쓸 수 있습니다:

example (n : Nat) : n + 1 = Nat.succ n := n:Nat⊢ n + 1 = n.succ n:Nat⊢ n.succ = n.succ All goals completed! 🐙

또한 have 택틱도 있는데, 이는 증명 항을 작성할 때와 마찬가지로 새로운 하위 목표를 도입합니다.

example (p q r : Prop) : p ∧ (q ∨ r) → (p ∧ q) ∨ (p ∧ r) := p:Propq:Propr:Prop⊢ p ∧ (q ∨ r) → p ∧ q ∨ p ∧ r p:Propq:Propr:Prophp:phqr:q ∨ r⊢ p ∧ q ∨ p ∧ r p:Propq:Propr:Prophp:phqr:q ∨ r⊢ p ∧ q ∨ p ∧ r cases hqr with p:Propq:Propr:Prophp:phq:q⊢ p ∧ q ∨ p ∧ r p:Propq:Propr:Prophp:phq:qhpq:p ∧ q⊢ p ∧ q ∨ p ∧ r p:Propq:Propr:Prophp:phq:qhpq:p ∧ q⊢ p ∧ q All goals completed! 🐙 p:Propq:Propr:Prophp:phr:r⊢ p ∧ q ∨ p ∧ r p:Propq:Propr:Prophp:phr:rhpr:p ∧ r⊢ p ∧ q ∨ p ∧ r p:Propq:Propr:Prophp:phr:rhpr:p ∧ r⊢ p ∧ r All goals completed! 🐙

증명 항에서와 마찬가지로, have 택틱에서도 레이블을 생략할 수 있으며, 이 경우 기본 레이블 this가 사용됩니다:

example (p q r : Prop) : p ∧ (q ∨ r) → (p ∧ q) ∨ (p ∧ r) := p:Propq:Propr:Prop⊢ p ∧ (q ∨ r) → p ∧ q ∨ p ∧ r p:Propq:Propr:Prophp:phqr:q ∨ r⊢ p ∧ q ∨ p ∧ r p:Propq:Propr:Prophp:phqr:q ∨ r⊢ p ∧ q ∨ p ∧ r cases hqr with p:Propq:Propr:Prophp:phq:q⊢ p ∧ q ∨ p ∧ r p:Propq:Propr:Prophp:phq:qthis:p ∧ q⊢ p ∧ q ∨ p ∧ r p:Propq:Propr:Prophp:phq:qthis:p ∧ q⊢ p ∧ q All goals completed! 🐙 p:Propq:Propr:Prophp:phr:r⊢ p ∧ q ∨ p ∧ r p:Propq:Propr:Prophp:phr:rthis:p ∧ r⊢ p ∧ q ∨ p ∧ r p:Propq:Propr:Prophp:phr:rthis:p ∧ r⊢ p ∧ r All goals completed! 🐙

have 택틱에서는 타입을 생략할 수 있으므로, have hp := h.left와 have hqr := h.right처럼 작성할 수 있습니다. 실제로 이 표기법을 사용하면 타입과 레이블을 모두 생략할 수도 있는데, 이 경우 새로운 사실은 this라는 레이블로 도입됩니다.

example (p q r : Prop) : p ∧ (q ∨ r) → (p ∧ q) ∨ (p ∧ r) := p:Propq:Propr:Prop⊢ p ∧ (q ∨ r) → p ∧ q ∨ p ∧ r p:Propq:Propr:Prophp:phqr:q ∨ r⊢ p ∧ q ∨ p ∧ r cases hqr with p:Propq:Propr:Prophp:phq:q⊢ p ∧ q ∨ p ∧ r p:Propq:Propr:Prophp:phq:qthis:p ∧ q⊢ p ∧ q ∨ p ∧ r p:Propq:Propr:Prophp:phq:qthis:p ∧ q⊢ p ∧ q; All goals completed! 🐙 p:Propq:Propr:Prophp:phr:r⊢ p ∧ q ∨ p ∧ r p:Propq:Propr:Prophp:phr:rthis:p ∧ r⊢ p ∧ q ∨ p ∧ r p:Propq:Propr:Prophp:phr:rthis:p ∧ r⊢ p ∧ r; All goals completed! 🐙

Lean에는 have 택틱과 비슷하지만 보조 사실 대신 지역 정의를 도입하는 데 사용되는 let 택틱도 있습니다. 이는 증명 항에서의 let에 대응하는 택틱입니다:

example : ∃ x, x + 2 = 8 := ⊢ ∃ x, x + 2 = 8 a:Nat := 3 * 2⊢ ∃ x, x + 2 = 8 All goals completed! 🐙

have와 마찬가지로, let a := 3 * 2처럼 작성하여 타입을 암묵적으로 남겨둘 수 있습니다. let와 have의 차이는, let이 맥락에 지역 정의를 도입하여 증명에서 해당 지역 선언의 정의를 펼칠 수 있다는 것입니다.

우리는 중첩된 택틱 블록을 만들기 위해 .을 사용했습니다. 중첩된 블록에서 Lean은 첫 번째 목표에 집중하며, 블록이 끝날 때까지 해당 목표가 완전히 해결되지 않았다면 오류를 생성합니다. 이는 택틱에 의해 도입된 여러 하위 목표에 대한 개별 증명을 구분하여 나타내는 데 유용할 수 있습니다. . 표기법은 공백에 민감하며, 택틱 블록이 끝나는지 여부를 감지하기 위해 들여쓰기에 의존합니다. 또는, 중괄호와 세미콜론을 사용하여 택틱 블록을 정의할 수도 있습니다.

example (p q r : Prop) : p ∧ (q ∨ r) ↔ (p ∧ q) ∨ (p ∧ r) := p:Propq:Propr:Prop⊢ p ∧ (q ∨ r) ↔ p ∧ q ∨ p ∧ r p:Propq:Propr:Prop⊢ p ∧ (q ∨ r) → p ∧ q ∨ p ∧ rp:Propq:Propr:Prop⊢ p ∧ q ∨ p ∧ r → p ∧ (q ∨ r) p:Propq:Propr:Prop⊢ p ∧ (q ∨ r) → p ∧ q ∨ p ∧ r p:Propq:Propr:Proph:p ∧ (q ∨ r)⊢ p ∧ q ∨ p ∧ r; p:Propq:Propr:Proph:p ∧ (q ∨ r)h✝:q⊢ p ∧ q ∨ p ∧ rp:Propq:Propr:Proph:p ∧ (q ∨ r)h✝:r⊢ p ∧ q ∨ p ∧ r; p:Propq:Propr:Proph:p ∧ (q ∨ r)h✝:q⊢ p ∧ q ∨ p ∧ r p:Propq:Propr:Proph:p ∧ (q ∨ r)h✝:q⊢ p ∧ q ∨ p ∧ r; All goals completed! 🐙 } p:Propq:Propr:Proph:p ∧ (q ∨ r)h✝:r⊢ p ∧ q ∨ p ∧ r p:Propq:Propr:Proph:p ∧ (q ∨ r)h✝:r⊢ p ∧ q ∨ p ∧ r; All goals completed! 🐙 } } p:Propq:Propr:Prop⊢ p ∧ q ∨ p ∧ r → p ∧ (q ∨ r) p:Propq:Propr:Proph:p ∧ q ∨ p ∧ r⊢ p ∧ (q ∨ r); p:Propq:Propr:Proph✝:p ∧ q⊢ p ∧ (q ∨ r)p:Propq:Propr:Proph✝:p ∧ r⊢ p ∧ (q ∨ r); p:Propq:Propr:Proph✝:p ∧ q⊢ p ∧ (q ∨ r) p:Propq:Propr:Proph✝:p ∧ q⊢ p ∧ (q ∨ r); p:Propq:Propr:Prophpq:p ∧ q⊢ p ∧ (q ∨ r); All goals completed! 🐙 } p:Propq:Propr:Proph✝:p ∧ r⊢ p ∧ (q ∨ r) p:Propq:Propr:Proph✝:p ∧ r⊢ p ∧ (q ∨ r); p:Propq:Propr:Prophpr:p ∧ r⊢ p ∧ (q ∨ r); All goals completed! 🐙 } }

증명을 구조화하는 데는 들여쓰기를 사용하는 것이 유용합니다. 택틱이 두 개 이상의 하위 목표를 남길 때마다, 남은 하위 목표들을 블록으로 감싸고 들여쓰기하여 구분합니다. 따라서 정리 foo를 단일 목표에 적용하여 네 개의 하위 목표가 생성된다면, 증명은 다음과 같은 모습일 것이라 예상할 수 있습니다.

  apply foo
  . <proof of first goal>
  . <proof of second goal>
  . <proof of third goal>
  . <proof of final goal>

또는

  apply foo
  case <tag of first goal>  => <proof of first goal>
  case <tag of second goal> => <proof of second goal>
  case <tag of third goal>  => <proof of third goal>
  case <tag of final goal>  => <proof of final goal>

또는

  apply foo
  { <proof of first goal>  }
  { <proof of second goal> }
  { <proof of third goal>  }
  { <proof of final goal>  }

5.5. 택틱 조합자🔗

택틱 조합자는 기존 택틱으로부터 새로운 택틱을 만드는 연산입니다. 순차 조합자는 by 블록에 이미 암묵적으로 포함되어 있습니다.

example (p q : Prop) (hp : p) : p ∨ q := p:Propq:Prophp:p⊢ p ∨ q p:Propq:Prophp:p⊢ p; All goals completed! 🐙

여기서 apply Or.inl; assumption은 먼저 apply Or.inl을 적용한 다음 assumption을 적용하는 단일 택틱과 기능적으로 동등합니다.

t₁ <;> t₂에서 <;> 연산자는 순차 결합 연산의 병렬 버전을 제공합니다. t₁이 현재 목표에 적용된 다음, 그 결과로 생긴 모든 하위 목표에 t₂가 적용됩니다.

example (p q : Prop) (hp : p) (hq : q) : p ∧ q := p:Propq:Prophp:phq:q⊢ p ∧ q p:Propq:Prophp:phq:q⊢ pp:Propq:Prophp:phq:q⊢ q p:Propq:Prophp:phq:q⊢ pp:Propq:Prophp:phq:q⊢ q All goals completed! 🐙

이는 결과로 생성된 목표들을 통일된 방식으로 마무리할 수 있을 때, 또는 적어도 모든 목표에 대해 균일하게 진행할 수 있을 때 특히 유용합니다.

first | t₁ | t₂ | ... | tₙ는 하나가 성공할 때까지 각 tᵢ를 적용하며, 그렇지 않으면 실패합니다:

example (p q : Prop) (hp : p) : p ∨ q := p:Propq:Prophp:p⊢ p ∨ q first | p:Propq:Prophp:p⊢ p; All goals completed! 🐙 | apply Or.inr; assumption example (p q : Prop) (hq : q) : p ∨ q := p:Propq:Prophq:q⊢ p ∨ q first | p:Propq:Prophq:q⊢ p; p:Propq:Prophq:q⊢ p | p:Propq:Prophq:q⊢ q; All goals completed! 🐙

첫 번째 예시에서는 왼쪽 분기가 성공하는 반면, 두 번째 예시에서는 오른쪽 분기가 성공합니다. 다음 세 예시에서는 동일한 복합 택틱이 각 경우 모두 성공합니다:

example (p q r : Prop) (hp : p) : p ∨ q ∨ r := p:Propq:Propr:Prophp:p⊢ p ∨ q ∨ r repeat (first | p:Propq:Propr:Prophp:p⊢ p; All goals completed! 🐙 | apply Or.inr | assumption) example (p q r : Prop) (hq : q) : p ∨ q ∨ r := p:Propq:Propr:Prophq:q⊢ p ∨ q ∨ r repeat (first | p:Propq:Propr:Prophq:q⊢ q; All goals completed! 🐙 | p:Propq:Propr:Prophq:q⊢ q ∨ r | assumption) example (p q r : Prop) (hr : r) : p ∨ q ∨ r := p:Propq:Propr:Prophr:r⊢ p ∨ q ∨ r repeat (first | p:Propq:Propr:Prophr:r⊢ r; p:Propq:Propr:Prophr:r⊢ q | p:Propq:Propr:Prophr:r⊢ r | All goals completed! 🐙)

이 택틱은 assumption을 통해 왼쪽 논리합 항을 즉시 해결하려 시도합니다. 그것이 실패하면 오른쪽 논리합 항에 초점을 맞추려 시도하며, 그마저 통하지 않으면 assumption 택틱을 호출합니다.

지금쯤이면 택틱이 실패할 수 있다는 것을 분명히 눈치채셨을 것입니다. 실제로 first 조합자가 백트래킹하여 다음 택틱을 시도하도록 만드는 것이 바로 이 “실패” 상태입니다. try 조합자는 비록 사소한 방식일지라도 항상 성공하는 택틱을 만듭니다. try t는 t를 실행하고, t가 실패하더라도 성공을 보고합니다. 이는 first| t |skip과 동등하며, 여기서 skip은 아무 일도 하지 않는 (그리고 그렇게 함으로써 성공하는) 택틱입니다. 다음 예제에서 두 번째 constructor는 오른쪽 논리곱 q ∧ r에 대해서는 성공하지만(논리합과 논리곱은 오른쪽으로 결합한다는 것을 기억하십시오) 첫 번째에 대해서는 실패합니다. try 택틱은 순차 합성이 성공하도록 보장합니다.

example (p q r : Prop) (hp : p) (hq : q) (hr : r) : p ∧ q ∧ r := p:Propq:Propr:Prophp:phq:qhr:r⊢ p ∧ q ∧ r p:Propq:Propr:Prophp:phq:qhr:r⊢ pp:Propq:Propr:Prophp:phq:qhr:r⊢ q ∧ r p:Propq:Propr:Prophp:phq:qhr:r⊢ pp:Propq:Propr:Prophp:phq:qhr:r⊢ q ∧ r (try p:Propq:Propr:Prophp:phq:qhr:r⊢ qp:Propq:Propr:Prophp:phq:qhr:r⊢ r) p:Propq:Propr:Prophp:phq:qhr:r⊢ pp:Propq:Propr:Prophp:phq:qhr:r⊢ qp:Propq:Propr:Prophp:phq:qhr:r⊢ r All goals completed! 🐙

주의하십시오: repeat (try t)는 내부 택틱이 결코 실패하지 않기 때문에 무한히 반복됩니다.

증명에서는 미해결 목표가 여러 개 남아 있는 경우가 흔합니다. 병렬 순차 결합은 하나의 택틱을 여러 목표에 적용하도록 구성하는 한 가지 방법이지만, 이를 수행하는 다른 방법도 있습니다. 예를 들어, all_goals t는 t를 열려 있는 모든 목표에 적용합니다:

example (p q r : Prop) (hp : p) (hq : q) (hr : r) : p ∧ q ∧ r := p:Propq:Propr:Prophp:phq:qhr:r⊢ p ∧ q ∧ r p:Propq:Propr:Prophp:phq:qhr:r⊢ pp:Propq:Propr:Prophp:phq:qhr:r⊢ q ∧ r all_goals (try p:Propq:Propr:Prophp:phq:qhr:r⊢ qp:Propq:Propr:Prophp:phq:qhr:r⊢ r) all_goals All goals completed! 🐙

이 경우에는 any_goals 택틱이 더 견고한 해결책을 제공합니다. 이는 all_goals와 유사하지만, 인자가 적어도 하나의 목표에서 성공하면 성공한다는 점이 다릅니다.

example (p q r : Prop) (hp : p) (hq : q) (hr : r) : p ∧ q ∧ r := p:Propq:Propr:Prophp:phq:qhr:r⊢ p ∧ q ∧ r p:Propq:Propr:Prophp:phq:qhr:r⊢ pp:Propq:Propr:Prophp:phq:qhr:r⊢ q ∧ r any_goals p:Propq:Propr:Prophp:phq:qhr:r⊢ qp:Propq:Propr:Prophp:phq:qhr:r⊢ r any_goals All goals completed! 🐙

아래 by 블록의 첫 번째 택틱은 논리곱을 반복적으로 분해합니다:

example (p q r : Prop) (hp : p) (hq : q) (hr : r) : p ∧ ((p ∧ q) ∧ r) ∧ (q ∧ r ∧ p) := p:Propq:Propr:Prophp:phq:qhr:r⊢ p ∧ ((p ∧ q) ∧ r) ∧ q ∧ r ∧ p repeat (any_goals p:Propq:Propr:Prophp:phq:qhr:r⊢ p) all_goals All goals completed! 🐙

사실, 전체 택틱을 한 줄로 압축할 수 있습니다:

example (p q r : Prop) (hp : p) (hq : q) (hr : r) : p ∧ ((p ∧ q) ∧ r) ∧ (q ∧ r ∧ p) := p:Propq:Propr:Prophp:phq:qhr:r⊢ p ∧ ((p ∧ q) ∧ r) ∧ q ∧ r ∧ p repeat (any_goals (first | p:Propq:Propr:Prophp:phq:qhr:r⊢ p | All goals completed! 🐙))

조합자 focus t는 t가 현재 목표에만 영향을 미치도록 보장하며, 나머지 목표는 일시적으로 범위에서 숨깁니다. 따라서 t가 원래 현재 목표에만 영향을 미친다면, focus (all_goals t)는 t와 동일한 효과를 갖습니다.

5.6. 재작성🔗

rw 택틱과 simp 택틱은 계산적 증명에서 간략히 소개되었습니다. 이 절과 다음 절에서는 이들을 더 자세히 다룹니다.

rw 택틱은 목표와 가설에 치환을 적용하는 기본적인 메커니즘을 제공하며, 동치를 다루는 편리하고 효율적인 방법을 제공합니다. 이 택틱의 가장 기본적인 형태는 rw [t]이며, 여기서 t는 그 타입이 동치를 나타내는 항입니다. 예를 들어, t는 문맥 내의 가설 h : x = y일 수도 있고, add_comm : ∀ x y, x + y = y + x와 같은 일반적인 보조정리일 수도 있는데, 이 경우 rewrite 택틱은 x와 y에 적절한 대입을 찾으려 시도합니다. 또는 구체적이거나 일반적인 방정식을 나타내는 임의의 복합 항일 수도 있습니다. 다음 예제에서는 이 기본 형태를 사용하여 가설을 이용해 목표를 다시 씁니다.

variable (k : Nat) (f : Nat → Nat) example (h₁ : f 0 = 0) (h₂ : k = 0) : f k = 0 := k:Natf:Nat → Nath₁:f 0 = 0h₂:k = 0⊢ f k = 0 k:Natf:Nat → Nath₁:f 0 = 0h₂:k = 0⊢ f 0 = 0 -- replace k with 0 All goals completed! 🐙 -- replace f 0 with 0

위 예제에서 rw의 첫 번째 사용은 목표 f k = 0에서 k를 0으로 치환합니다. 그다음, 두 번째 사용은 f 0을 0으로 치환합니다. 이 택틱은 t = t 형태의 목표를 자동으로 닫습니다. 다음은 복합 표현식을 사용한 재작성 예제입니다:

example (x y : Nat) (p : Nat → Prop) (q : Prop) (h : q → x = y) (h' : p y) (hq : q) : p x := x:Naty:Natp:Nat → Propq:Proph:q → x = yh':p yhq:q⊢ p x x:Naty:Natp:Nat → Propq:Proph:q → x = yh':p yhq:q⊢ p y; All goals completed! 🐙

여기서 h hq는 방정식 x = y를 성립시킵니다.

rw [t_1, ..., t_n] 표기법을 사용하면 여러 재작성을 결합할 수 있으며, 이는 rw[t_1]; ...;rw [t_n]의 축약형일 뿐입니다. 앞의 예제는 다음과 같이 작성할 수 있습니다.

variable (k : Nat) (f : Nat → Nat) example (h₁ : f 0 = 0) (h₂ : k = 0) : f k = 0 := k:Natf:Nat → Nath₁:f 0 = 0h₂:k = 0⊢ f k = 0 All goals completed! 🐙

기본적으로 rw는 등식을 정방향으로 사용하여, 좌변을 어떤 식과 매칭한 후 우변으로 치환합니다. ←t 표기법을 사용하면 택틱이 등식 t를 역방향으로 사용하도록 지시할 수 있습니다.

variable (a b : Nat) (f : Nat → Nat) example (h₁ : a = b) (h₂ : f a = 0) : f b = 0 := a:Natb:Natf:Nat → Nath₁:a = bh₂:f a = 0⊢ f b = 0 All goals completed! 🐙

이 예제에서 ←h₁이라는 항은 재작성기에게 b를 a로 바꾸도록 지시합니다. 편집기에서는 역방향 화살표를 \l로 입력할 수 있습니다. ASCII로 대응되는 <-를 사용할 수도 있습니다.

때로는 항등식의 좌변이 패턴 내에서 둘 이상의 부분식과 일치할 수 있는데, 이 경우 rw 택틱은 항을 순회하면서 찾은 첫 번째 일치를 선택합니다. 그것이 원하는 것이 아니라면, 추가 인자를 사용하여 적절한 부분식을 지정할 수 있습니다.

example (a b c : Nat) : a + b + c = a + c + b := a:Natb:Natc:Nat⊢ a + b + c = a + c + b All goals completed! 🐙 example (a b c : Nat) : a + b + c = a + c + b := a:Natb:Natc:Nat⊢ a + b + c = a + c + b All goals completed! 🐙 example (a b c : Nat) : a + b + c = a + c + b := a:Natb:Natc:Nat⊢ a + b + c = a + c + b All goals completed! 🐙

위의 첫 번째 예제에서 첫 단계는 a + b + c를 a + (b + c)로 재작성합니다. 다음 단계는 항 b + c에 교환법칙을 적용합니다. 인자를 지정하지 않으면, 이 택틱은 대신 a + (b + c)를 (b + c) + a로 재작성할 것입니다. 마지막으로, 마지막 단계는 결합법칙을 반대 방향으로 적용하여 a + (c + b)를 a + c + b로 재작성합니다. 다음 두 예제는 대신 결합법칙을 적용해 양변에서 괄호를 오른쪽으로 옮긴 다음, b와 c를 서로 바꿉니다. 마지막 예제는 Nat.add_comm의 두 번째 인자를 지정함으로써 재작성이 우변에서 이루어지도록 지정한다는 점에 유의하십시오.

기본적으로, rw 택틱은 목표에만 영향을 줍니다. rw [t] at h 표기법은 재작성을

example (f : Nat → Nat) (a : Nat) (h : a + 0 = 0) : f a = f 0 := f:Nat → Nata:Nath:a + 0 = 0⊢ f a = f 0 f:Nat → Nata:Nath:a = 0⊢ f a = f 0 All goals completed! 🐙

첫 번째 단계인 rw [Nat.add_zero] at h는 가설 a + 0 = 0을 a = 0으로 다시 씁니다. 그런 다음 새로운 가설 a = 0을 사용하여 목표를 f 0 = f 0로 다시 씁니다.

rw 택틱은 명제에만 국한되지 않습니다. 다음 예제에서는 rw [h] at t를 사용하여 가설 t : Tuple α n을 t : Tuple α 0으로 재작성합니다.

def Tuple (α : Type) (n : Nat) := { as : List α // as.length = n } example (n : Nat) (h : n = 0) (t : Tuple α n) : Tuple α 0 := α:Typen:Nath:n = 0t:Tuple α n⊢ Tuple α 0 α:Typen:Nath:n = 0t:Tuple α 0⊢ Tuple α 0 All goals completed! 🐙

5.7. 단순화기 사용하기🔗

rw가 목표(goal)를 조작하기 위한 정밀한 도구로 설계된 반면, 단순화기(simplifier)는 더 강력한 형태의 자동화를 제공합니다. Lean 라이브러리의 여러 항등식에는 [simp] 속성이 태그되어 있으며, simp 택틱은 이를 사용하여 식 안의 부분항을 반복적으로 다시 씁니다.

example (x y z : Nat) : (x + 0) * (0 + y * 1 + z * 0) = x * y := x:Naty:Natz:Nat⊢ (x + 0) * (0 + y * 1 + z * 0) = x * y All goals completed! 🐙 example (x y z : Nat) (p : Nat → Prop) (h : p (x * y)) : p ((x + 0) * (0 + y * 1 + z * 0)) := x:Naty:Natz:Natp:Nat → Proph:p (x * y)⊢ p ((x + 0) * (0 + y * 1 + z * 0)) x:Naty:Natz:Natp:Nat → Proph:p (x * y)⊢ p (x * y); All goals completed! 🐙

첫 번째 예제에서는 목표에 있는 등식의 좌변이 0과 1이 관련된 일반적인 항등식을 사용해 단순화되어, 목표가 x * y = x * y로 축소됩니다. 이 지점에서 simp는 반사성을 적용해 이를 마무리합니다. 두 번째 예제에서는 simp가 목표를 p (x * y)로 축소시키며, 이 지점에서 가정 h가 이를 마무리합니다. 다음은 리스트를 사용하는 몇 가지 예제입니다:

open List example (xs : List Nat) : reverse (xs ++ [1, 2, 3]) = [3, 2, 1] ++ reverse xs := xs:List Nat⊢ (xs ++ [1, 2, 3]).reverse = [3, 2, 1] ++ xs.reverse All goals completed! 🐙 example (xs ys : List α) : length (reverse (xs ++ ys)) = length xs + length ys := α:Type u_1xs:List αys:List α⊢ (xs ++ ys).reverse.length = xs.length + ys.length All goals completed! 🐙

rw와 마찬가지로, at 키워드를 사용하여 가설을 단순화할 수 있습니다:

example (x y z : Nat) (p : Nat → Prop) (h : p ((x + 0) * (0 + y * 1 + z * 0))) : p (x * y) := x:Naty:Natz:Natp:Nat → Proph:p ((x + 0) * (0 + y * 1 + z * 0))⊢ p (x * y) x:Naty:Natz:Natp:Nat → Proph:p (x * y)⊢ p (x * y); All goals completed! 🐙

또한, “와일드카드” 애스터리스크(asterisk)를 사용하여 모든 가정과 목표를 단순화할 수 있습니다.

attribute [local simp] Nat.mul_comm Nat.mul_assoc Nat.mul_left_comm attribute [local simp] Nat.add_assoc Nat.add_comm Nat.add_left_comm example (w x y z : Nat) (p : Nat → Prop) (h : p (x * y + z * w * x)) : p (x * w * z + y * x) := w:Natx:Naty:Natz:Natp:Nat → Proph:p (x * y + z * w * x)⊢ p (x * w * z + y * x) w:Natx:Naty:Natz:Natp:Nat → Proph:p (x * y + w * (x * z))⊢ p (x * y + w * (x * z)); All goals completed! 🐙 example (x y z : Nat) (p : Nat → Prop) (h₁ : p (1 * x + y)) (h₂ : p (x * z * 1)) : p (y + 0 + x) ∧ p (z * x) := x:Naty:Natz:Natp:Nat → Proph₁:p (1 * x + y)h₂:p (x * z * 1)⊢ p (y + 0 + x) ∧ p (z * x) x:Naty:Natz:Natp:Nat → Proph₁:p (x + y)h₂:p (x * z)⊢ p (x + y) ∧ p (x * z) x:Naty:Natz:Natp:Nat → Proph₁:p (x + y)h₂:p (x * z)⊢ p (x + y) ∧ p (x * z) x:Naty:Natz:Natp:Nat → Proph₁:p (x + y)h₂:p (x * z)⊢ p (x + y)x:Naty:Natz:Natp:Nat → Proph₁:p (x + y)h₂:p (x * z)⊢ p (x * z) x:Naty:Natz:Natp:Nat → Proph₁:p (x + y)h₂:p (x * z)⊢ p (x + y)x:Naty:Natz:Natp:Nat → Proph₁:p (x + y)h₂:p (x * z)⊢ p (x * z) All goals completed! 🐙

자연수에서의 곱셈처럼 교환법칙과 결합법칙이 성립하는 연산에 대해서는, 단순화기가 이 두 사실뿐만 아니라 좌교환성도 사용하여 식을 재작성합니다. 곱셈의 경우 후자는 다음과 같이 표현됩니다: x * (y * z) = y * (x * z). local 수정자는 현재 파일(또는 경우에 따라 절이나 네임스페이스)에서 이 규칙들을 사용하도록 단순화기에 지시합니다. 교환법칙과 좌교환성을 반복적으로 적용하면 순환이 발생한다는 점에서, 이 둘이 문제가 되는 것처럼 보일 수 있습니다. 하지만 단순화기는 인자를 치환하는 항등식을 감지하며, 순서화된 재작성이라고 알려진 기법을 사용합니다. 이는 시스템이 항들에 대한 내부 순서를 유지하며, 항등식을 적용했을 때 순서가 감소하는 경우에만 그 항등식을 적용한다는 것을 의미합니다. 위에서 언급한 세 가지 항등식으로 인해, 식 안의 모든 괄호가 오른쪽으로 결합되고, 식들이 (다소 임의적이기는 하지만) 정규적인 방식으로 정렬되는 효과가 나타납니다. 그러면 결합법칙과 교환법칙까지 고려했을 때 동치인 두 식은 동일한 정규 형태로 재작성됩니다.

example (w x y z : Nat) (Variable name `p` is not explicitly referenced. Hint: The binding can be removed (if unused) or named `_` (if used implicitly). Alternatively, prefix the name with `_` to silence this warning: [apply] _p Note: This linter can be disabled with `set_option linter.unusedVariables false`p : Nat → Prop) : x * y + z * w * x = x * w * z + y * x := w:Natx:Naty:Natz:Natp:Nat → Prop⊢ x * y + z * w * x = x * w * z + y * x All goals completed! 🐙 example (w x y z : Nat) (p : Nat → Prop) (h : p (x * y + z * w * x)) : p (x * w * z + y * x) := w:Natx:Naty:Natz:Natp:Nat → Proph:p (x * y + z * w * x)⊢ p (x * w * z + y * x) w:Natx:Naty:Natz:Natp:Nat → Proph:p (x * y + z * w * x)⊢ p (x * y + w * (x * z)); w:Natx:Naty:Natz:Natp:Nat → Proph:p (x * y + w * (x * z))⊢ p (x * y + w * (x * z)); All goals completed! 🐙

rw와 마찬가지로, simp에도 일반 보조정리, 지역 가정, 펼칠 정의, 복합 표현식 등 사용할 사실들의 목록을 전달할 수 있습니다. simp 택틱은 rewrite가 인식하는 ←t 구문도 인식합니다. 어느 경우든, 추가된 규칙들은 항을 단순화하는 데 사용되는 항등식 모음에 더해집니다.

def f (m n : Nat) : Nat := m + n + m example {m n : Nat} (h : n = 1) (h' : 0 = m) : (f m n) = n := m:Natn:Nath:n = 1h':0 = m⊢ f m n = n All goals completed! 🐙

로컬 가정을 사용하여 목표를 단순화하는 것은 흔한 관용구입니다:

variable (k : Nat) (f : Nat → Nat) example (h₁ : f 0 = 0) (h₂ : k = 0) : f k = 0 := k:Natf:Nat → Nath₁:f 0 = 0h₂:k = 0⊢ f k = 0 All goals completed! 🐙

단순화 시 로컬 컨텍스트에 있는 모든 가설을 사용하려면, 와일드카드 기호인 *를 사용할 수 있습니다:

variable (k : Nat) (f : Nat → Nat) example (h₁ : f 0 = 0) (h₂ : k = 0) : f k = 0 := k:Natf:Nat → Nath₁:f 0 = 0h₂:k = 0⊢ f k = 0 All goals completed! 🐙

또 다른 예를 살펴보겠습니다:

example (u w x y z : Nat) (h₁ : x = y + z) (h₂ : w = u + x) : w = z + y + u := u:Natw:Natx:Naty:Natz:Nath₁:x = y + zh₂:w = u + x⊢ w = z + y + u All goals completed! 🐙

단순화기(simplifier)는 명제 재작성(propositional rewriting)도 수행합니다. 예를 들어, 가설 p를 사용하여 p ∧ q를 q로, p ∨ q를 True로 재작성하며, 이는 곧바로 자명하게 증명됩니다. 이러한 재작성을 반복하면 자명하지 않은 명제 추론이 만들어집니다.

example (p q : Prop) (hp : p) : p ∧ q ↔ q := p:Propq:Prophp:p⊢ p ∧ q ↔ q All goals completed! 🐙 example (p q : Prop) (hp : p) : p ∨ q := p:Propq:Prophp:p⊢ p ∨ q All goals completed! 🐙 example (p q r : Prop) (hp : p) (hq : q) : p ∧ (q ∨ r) := p:Propq:Propr:Prophp:phq:q⊢ p ∧ (q ∨ r) All goals completed! 🐙

다음 예제는 모든 가설을 단순화한 다음, 이를 사용하여 목표를 증명합니다.

example (u w x x' y y' z : Nat) (p : Nat → Prop) (h₁ : x + 0 = x') (h₂ : y + 0 = y') : x + y + 0 = x' + y' := u:Natw:Natx:Natx':Naty:Naty':Natz:Natp:Nat → Proph₁:x + 0 = x'h₂:y + 0 = y'⊢ x + y + 0 = x' + y' u:Natw:Natx:Natx':Naty:Naty':Natz:Natp:Nat → Proph₁:x = x'h₂:y = y'⊢ x + y = x' + y' All goals completed! 🐙

단순화기(simplifier)를 특히 유용하게 만드는 한 가지 요소는, 라이브러리가 발전함에 따라 그 능력도 함께 성장할 수 있다는 점입니다. 예를 들어, 입력값에 그 역순을 이어붙여 대칭으로 만드는 리스트 연산을 정의한다고 가정해 봅시다.

def mk_symm (xs : List α) := xs ++ xs.reverse

그러면 임의의 리스트 xs에 대해, (mk_symm xs).reverse는 mk_symm xs와 같으며, 이는 정의를 펼쳐 보면 쉽게 증명할 수 있습니다:

theorem reverse_mk_symm (xs : List α) : (mk_symm xs).reverse = mk_symm xs := α:Type u_1xs:List α⊢ (mk_symm xs).reverse = mk_symm xs All goals completed! 🐙

이제 이 정리를 사용하여 새로운 결과를 증명할 수 있습니다:

example (xs ys : List Nat) : (xs ++ mk_symm ys).reverse = mk_symm ys ++ xs.reverse := xs:List Natys:List Nat⊢ (xs ++ mk_symm ys).reverse = mk_symm ys ++ xs.reverse All goals completed! 🐙 example (xs ys : List Nat) (p : List Nat → Prop) (h : p (xs ++ mk_symm ys).reverse) : p (mk_symm ys ++ xs.reverse) := xs:List Natys:List Natp:List Nat → Proph:p (xs ++ mk_symm ys).reverse⊢ p (mk_symm ys ++ xs.reverse) xs:List Natys:List Natp:List Nat → Proph:p (mk_symm ys ++ xs.reverse)⊢ p (mk_symm ys ++ xs.reverse); All goals completed! 🐙

하지만 reverse_mk_symm을 사용하는 것이 일반적으로 옳은 방법이며, 사용자가 이를 명시적으로 호출할 필요가 없다면 좋을 것입니다. 정리를 정의할 때 이를 단순화 규칙으로 표시함으로써 그렇게 할 수 있습니다:

@[simp] theorem reverse_mk_symm (xs : List α) : (mk_symm xs).reverse = mk_symm xs := α:Type u_1xs:List α⊢ (mk_symm xs).reverse = mk_symm xs All goals completed! 🐙 example (xs ys : List Nat) : (xs ++ mk_symm ys).reverse = mk_symm ys ++ xs.reverse := xs:List Natys:List Nat⊢ (xs ++ mk_symm ys).reverse = mk_symm ys ++ xs.reverse All goals completed! 🐙 example (xs ys : List Nat) (p : List Nat → Prop) (h : p (xs ++ mk_symm ys).reverse) : p (mk_symm ys ++ xs.reverse) := xs:List Natys:List Natp:List Nat → Proph:p (xs ++ mk_symm ys).reverse⊢ p (mk_symm ys ++ xs.reverse) xs:List Natys:List Natp:List Nat → Proph:p (mk_symm ys ++ xs.reverse)⊢ p (mk_symm ys ++ xs.reverse); All goals completed! 🐙

@[simp] 표기법은 reverse_mk_symm이 [simp] 속성을 가지도록 선언하며, 다음과 같이 더 명시적으로 풀어 쓸 수도 있습니다.

theorem reverse_mk_symm (xs : List α) : (mk_symm xs).reverse = mk_symm xs := α:Type u_1xs:List α⊢ (mk_symm xs).reverse = mk_symm xs All goals completed! 🐙 attribute [simp] reverse_mk_symm example (xs ys : List Nat) : (xs ++ mk_symm ys).reverse = mk_symm ys ++ xs.reverse := xs:List Natys:List Nat⊢ (xs ++ mk_symm ys).reverse = mk_symm ys ++ xs.reverse All goals completed! 🐙 example (xs ys : List Nat) (p : List Nat → Prop) (h : p (xs ++ mk_symm ys).reverse) : p (mk_symm ys ++ xs.reverse) := xs:List Natys:List Natp:List Nat → Proph:p (xs ++ mk_symm ys).reverse⊢ p (mk_symm ys ++ xs.reverse) xs:List Natys:List Natp:List Nat → Proph:p (mk_symm ys ++ xs.reverse)⊢ p (mk_symm ys ++ xs.reverse); All goals completed! 🐙

이 속성은 정리가 선언된 이후 언제든지 적용할 수도 있습니다:

theorem reverse_mk_symm (xs : List α) : (mk_symm xs).reverse = mk_symm xs := α:Type u_1xs:List α⊢ (mk_symm xs).reverse = mk_symm xs All goals completed! 🐙 example (xs ys : List Nat) : (xs ++ mk_symm ys).reverse = mk_symm ys ++ xs.reverse := xs:List Natys:List Nat⊢ (xs ++ mk_symm ys).reverse = mk_symm ys ++ xs.reverse All goals completed! 🐙 attribute [simp] reverse_mk_symm example (xs ys : List Nat) (p : List Nat → Prop) (h : p (xs ++ mk_symm ys).reverse) : p (mk_symm ys ++ xs.reverse) := xs:List Natys:List Natp:List Nat → Proph:p (xs ++ mk_symm ys).reverse⊢ p (mk_symm ys ++ xs.reverse) xs:List Natys:List Natp:List Nat → Proph:p (mk_symm ys ++ xs.reverse)⊢ p (mk_symm ys ++ xs.reverse); All goals completed! 🐙

그러나 속성이 한번 적용되고 나면 이를 영구적으로 제거할 방법은 없습니다. 이 속성은 해당 속성이 지정된 파일을 가져오는 모든 파일에서 지속됩니다. 속성에서 더 자세히 다룰 것처럼, local 수정자를 사용하면 속성의 범위를 현재 파일이나 섹션으로 제한할 수 있습니다.

theorem reverse_mk_symm (xs : List α) : (mk_symm xs).reverse = mk_symm xs := α:Type u_1xs:List α⊢ (mk_symm xs).reverse = mk_symm xs All goals completed! 🐙 section attribute [local simp] reverse_mk_symm example (xs ys : List Nat) : (xs ++ mk_symm ys).reverse = mk_symm ys ++ xs.reverse := xs:List Natys:List Nat⊢ (xs ++ mk_symm ys).reverse = mk_symm ys ++ xs.reverse All goals completed! 🐙 example (xs ys : List Nat) (p : List Nat → Prop) (h : p (xs ++ mk_symm ys).reverse) : p (mk_symm ys ++ xs.reverse) := xs:List Natys:List Natp:List Nat → Proph:p (xs ++ mk_symm ys).reverse⊢ p (mk_symm ys ++ xs.reverse) xs:List Natys:List Natp:List Nat → Proph:p (mk_symm ys ++ xs.reverse)⊢ p (mk_symm ys ++ xs.reverse); All goals completed! 🐙 end

섹션 밖에서는 단순화기(simplifier)가 더 이상 기본적으로 reverse_mk_symm을 사용하지 않습니다.

지금까지 살펴본 다양한 simp 옵션들—규칙의 명시적 목록을 지정하는 것과 위치를 지정하기 위해 at을 사용하는 것—은 서로 결합할 수 있지만, 나열되는 순서는 고정되어 있다는 점에 유의하십시오. 편집기에서 simp 식별자에 커서를 놓으면 이와 연관된 문서 문자열을 확인하여 올바른 순서를 볼 수 있습니다.

유용한 추가 수정자가 두 가지 있습니다. 기본적으로 simp는 [simp] 속성이 표시된 모든 정리를 포함합니다. simp only라고 작성하면 이러한 기본값이 제외되므로, 더 명시적으로 작성된 규칙 목록을 사용할 수 있습니다. 아래 예제에서는 마이너스 기호와 only를 사용하여 reverse_mk_symm의 적용을 막습니다.

def mk_symm (xs : List α) := xs ++ xs.reverse @[simp] theorem reverse_mk_symm (xs : List α) : (mk_symm xs).reverse = mk_symm xs := α:Type u_1xs:List α⊢ (mk_symm xs).reverse = mk_symm xs All goals completed! 🐙 example (xs ys : List Nat) (p : List Nat → Prop) (h : p (xs ++ mk_symm ys).reverse) : p (mk_symm ys ++ xs.reverse) := xs:List Natys:List Natp:List Nat → Proph:p (xs ++ mk_symm ys).reverse⊢ p (mk_symm ys ++ xs.reverse) xs:List Natys:List Natp:List Nat → Proph:p (mk_symm ys ++ xs.reverse)⊢ p (mk_symm ys ++ xs.reverse); All goals completed! 🐙 example (xs ys : List Nat) (p : List Nat → Prop) (h : p (xs ++ mk_symm ys).reverse) : p ((mk_symm ys).reverse ++ xs.reverse) := xs:List Natys:List Natp:List Nat → Proph:p (xs ++ mk_symm ys).reverse⊢ p ((mk_symm ys).reverse ++ xs.reverse) xs:List Natys:List Natp:List Nat → Proph:p ((mk_symm ys).reverse ++ xs.reverse)⊢ p ((mk_symm ys).reverse ++ xs.reverse); All goals completed! 🐙 example (xs ys : List Nat) (p : List Nat → Prop) (h : p (xs ++ mk_symm ys).reverse) : p ((mk_symm ys).reverse ++ xs.reverse) := xs:List Natys:List Natp:List Nat → Proph:p (xs ++ mk_symm ys).reverse⊢ p ((mk_symm ys).reverse ++ xs.reverse) xs:List Natys:List Natp:List Nat → Proph:p ((mk_symm ys).reverse ++ xs.reverse)⊢ p ((mk_symm ys).reverse ++ xs.reverse); All goals completed! 🐙

simp 택틱에는 많은 설정 옵션이 있습니다. 예를 들어, 다음과 같이 문맥적 단순화를 활성화할 수 있습니다.

example : if x = 0 then y + x = y else x ≠ 0 := x:Naty:Nat⊢ if x = 0 then y + x = y else x ≠ 0 All goals completed! 🐙

+contextual을 사용하면, simp 택틱은 y + x = y를 단순화할 때는 x = 0이라는 사실을, 다른 분기를 단순화할 때는 x ≠ 0이라는 사실을 사용합니다. 다음은 또 다른 예시입니다.

example : ∀ (x : Nat) (Variable name `h` is not explicitly referenced. Hint: The binding can be removed (if unused) or named `_` (if used implicitly). Alternatively, prefix the name with `_` to silence this warning: [apply] _h Note: This linter can be disabled with `set_option linter.unusedVariables false`h : x = 0), y + x = y := y:Nat⊢ ∀ (x : Nat), x = 0 → y + x = y All goals completed! 🐙

또 하나의 유용한 설정 옵션으로는 산술적 단순화를 활성화하는 +arith가 있습니다.

example : 0 < 1 + x ∧ x + y + 2 ≥ y + 1 := x:Naty:Nat⊢ 0 < 1 + x ∧ x + y + 2 ≥ y + 1 All goals completed! 🐙

5.8. Split 택틱🔗

split 택틱은 중첩된 if-then-else 및 match 표현식을 여러 경우로 나누는 데 유용합니다. n개의 경우를 가진 match 표현식에 대해, split 택틱은 최대 n개의 하위 목표를 생성합니다. 예시는 다음과 같습니다:

def f (x y z : Nat) : Nat := match x, y, z with | 5, _, _ => y | _, 5, _ => y | _, _, 5 => y | _, _, _ => 1 example (x y z : Nat) : x ≠ 5 → y ≠ 5 → z ≠ 5 → z = w → f x y w = 1 := w:Natx:Naty:Natz:Nat⊢ x ≠ 5 → y ≠ 5 → z ≠ 5 → z = w → f x y w = 1 w:Natx:Naty:Natz:Nata✝³:x ≠ 5a✝²:y ≠ 5a✝¹:z ≠ 5a✝:z = w⊢ f x y w = 1 w:Natx:Naty:Natz:Nata✝³:x ≠ 5a✝²:y ≠ 5a✝¹:z ≠ 5a✝:z = w⊢ (match x, y, w with | 5, x, x_1 => y | x, 5, x_1 => y | x, x_1, 5 => y | x, x_1, x_2 => 1) = 1 w:Naty:Natz:Nata✝³:y ≠ 5a✝²:z ≠ 5a✝¹:z = wx✝:Naty✝:Natz✝:Nata✝:5 ≠ 5⊢ y = 1w:Natx:Natz:Nata✝³:x ≠ 5a✝²:z ≠ 5a✝¹:z = wx✝¹:Naty✝:Natz✝:Natx✝:x = 5 → Falsea✝:5 ≠ 5⊢ 5 = 1x:Naty:Natz:Nata✝³:x ≠ 5a✝²:y ≠ 5a✝¹:z ≠ 5x✝²:Naty✝:Natz✝:Natx✝¹:x = 5 → Falsex✝:y = 5 → Falsea✝:z = 5⊢ y = 1w:Natx:Naty:Natz:Nata✝³:x ≠ 5a✝²:y ≠ 5a✝¹:z ≠ 5a✝:z = wx✝³:Naty✝:Natz✝:Natx✝²:x = 5 → Falsex✝¹:y = 5 → Falsex✝:w = 5 → False⊢ 1 = 1 w:Naty:Natz:Nata✝³:y ≠ 5a✝²:z ≠ 5a✝¹:z = wx✝:Naty✝:Natz✝:Nata✝:5 ≠ 5⊢ y = 1 All goals completed! 🐙 w:Natx:Natz:Nata✝³:x ≠ 5a✝²:z ≠ 5a✝¹:z = wx✝¹:Naty✝:Natz✝:Natx✝:x = 5 → Falsea✝:5 ≠ 5⊢ 5 = 1 All goals completed! 🐙 x:Naty:Natz:Nata✝³:x ≠ 5a✝²:y ≠ 5a✝¹:z ≠ 5x✝²:Naty✝:Natz✝:Natx✝¹:x = 5 → Falsex✝:y = 5 → Falsea✝:z = 5⊢ y = 1 All goals completed! 🐙 w:Natx:Naty:Natz:Nata✝³:x ≠ 5a✝²:y ≠ 5a✝¹:z ≠ 5a✝:z = wx✝³:Naty✝:Natz✝:Natx✝²:x = 5 → Falsex✝¹:y = 5 → Falsex✝:w = 5 → False⊢ 1 = 1 All goals completed! 🐙

위의 택틱 증명은 다음과 같이 축약할 수 있습니다.

example (x y z : Nat) : x ≠ 5 → y ≠ 5 → z ≠ 5 → z = w → f x y w = 1 := w:Natx:Naty:Natz:Nat⊢ x ≠ 5 → y ≠ 5 → z ≠ 5 → z = w → f x y w = 1 w:Natx:Naty:Natz:Nata✝³:x ≠ 5a✝²:y ≠ 5a✝¹:z ≠ 5a✝:z = w⊢ f x y w = 1; w:Natx:Naty:Natz:Nata✝³:x ≠ 5a✝²:y ≠ 5a✝¹:z ≠ 5a✝:z = w⊢ (match x, y, w with | 5, x, x_1 => y | x, 5, x_1 => y | x, x_1, 5 => y | x, x_1, x_2 => 1) = 1; w:Naty:Natz:Nata✝³:y ≠ 5a✝²:z ≠ 5a✝¹:z = wx✝:Naty✝:Natz✝:Nata✝:5 ≠ 5⊢ y = 1w:Natx:Natz:Nata✝³:x ≠ 5a✝²:z ≠ 5a✝¹:z = wx✝¹:Naty✝:Natz✝:Natx✝:x = 5 → Falsea✝:5 ≠ 5⊢ 5 = 1x:Naty:Natz:Nata✝³:x ≠ 5a✝²:y ≠ 5a✝¹:z ≠ 5x✝²:Naty✝:Natz✝:Natx✝¹:x = 5 → Falsex✝:y = 5 → Falsea✝:z = 5⊢ y = 1w:Natx:Naty:Natz:Nata✝³:x ≠ 5a✝²:y ≠ 5a✝¹:z ≠ 5a✝:z = wx✝³:Naty✝:Natz✝:Natx✝²:x = 5 → Falsex✝¹:y = 5 → Falsex✝:w = 5 → False⊢ 1 = 1 w:Naty:Natz:Nata✝³:y ≠ 5a✝²:z ≠ 5a✝¹:z = wx✝:Naty✝:Natz✝:Nata✝:5 ≠ 5⊢ y = 1w:Natx:Natz:Nata✝³:x ≠ 5a✝²:z ≠ 5a✝¹:z = wx✝¹:Naty✝:Natz✝:Natx✝:x = 5 → Falsea✝:5 ≠ 5⊢ 5 = 1x:Naty:Natz:Nata✝³:x ≠ 5a✝²:y ≠ 5a✝¹:z ≠ 5x✝²:Naty✝:Natz✝:Natx✝¹:x = 5 → Falsex✝:y = 5 → Falsea✝:z = 5⊢ y = 1w:Natx:Naty:Natz:Nata✝³:x ≠ 5a✝²:y ≠ 5a✝¹:z ≠ 5a✝:z = wx✝³:Naty✝:Natz✝:Natx✝²:x = 5 → Falsex✝¹:y = 5 → Falsex✝:w = 5 → False⊢ 1 = 1 first | w:Natx:Naty:Natz:Nata✝³:x ≠ 5a✝²:y ≠ 5a✝¹:z ≠ 5a✝:z = wx✝³:Naty✝:Natz✝:Natx✝²:x = 5 → Falsex✝¹:y = 5 → Falsex✝:w = 5 → False⊢ 1 = 1 | All goals completed! 🐙

split <;> first | contradiction | rfl 택틱은 먼저 split 택틱을 적용한 다음, 생성된 각 목표에 대해 contradiction을 시도하고, contradiction이 실패하면 rfl을 시도합니다. simp와 마찬가지로, split을 특정 가설에 적용할 수 있습니다:

def g (xs ys : List Nat) : Nat := match xs, ys with | [a, b], _ => a+b+1 | _, [b, _] => b+1 | _, _ => 1 example (xs ys : List Nat) (h : g xs ys = 0) : False := xs:List Natys:List Nath:g xs ys = 0⊢ False xs:List Natys:List Nath:(match xs, ys with | [a, b], x => a + b + 1 | x, [b, head] => b + 1 | x, x_1 => 1) = 0⊢ False; ys:List Natxs✝:List Natys✝:List Nata✝:Natb✝:Nath:a✝ + b✝ + 1 = 0⊢ Falsexs:List Natxs✝:List Natys✝:List Natb✝:Nathead✝:Natx✝:∀ (a b : Nat), xs = [a, b] → Falseh:b✝ + 1 = 0⊢ Falsexs:List Natys:List Natxs✝:List Natys✝:List Natx✝¹:∀ (a b : Nat), xs = [a, b] → Falsex✝:∀ (b head : Nat), ys = [b, head] → Falseh:1 = 0⊢ False ys:List Natxs✝:List Natys✝:List Nata✝:Natb✝:Nath:a✝ + b✝ + 1 = 0⊢ Falsexs:List Natxs✝:List Natys✝:List Natb✝:Nathead✝:Natx✝:∀ (a b : Nat), xs = [a, b] → Falseh:b✝ + 1 = 0⊢ Falsexs:List Natys:List Natxs✝:List Natys✝:List Natx✝¹:∀ (a b : Nat), xs = [a, b] → Falsex✝:∀ (b head : Nat), ys = [b, head] → Falseh:1 = 0⊢ False All goals completed! 🐙

5.9. 확장 가능한 택틱🔗

다음 예제에서는 syntax 명령을 사용하여 표기법 triv를 정의합니다. 그런 다음, macro_rules 명령을 사용하여 triv가 사용될 때 수행되어야 하는 작업을 지정합니다. 서로 다른 확장을 여러 개 제공할 수 있으며, 택틱 인터프리터는 그중 하나가 성공할 때까지 모두 시도합니다.

-- Define a new tactic notation syntax "triv" : tactic macro_rules | `(tactic| triv) => `(tactic| assumption) example (h : p) : p := p:Sort ?u.2h:p⊢ p All goals completed! 🐙 -- You cannot prove the following theorem using `triv` -- example (x : α) : x = x := by -- triv -- Let's extend `triv`. The tactic interpreter -- tries all possible macro extensions for `triv` until one succeeds macro_rules | `(tactic| triv) => `(tactic| rfl) example (x : α) : x = x := α:Sort u_1x:α⊢ x = x All goals completed! 🐙 example (x : α) (h : p) : x = x ∧ p := α:Sort u_1p:Propx:αh:p⊢ x = x ∧ p α:Sort u_1p:Propx:αh:p⊢ x = xα:Sort u_1p:Propx:αh:p⊢ p α:Sort u_1p:Propx:αh:p⊢ x = xα:Sort u_1p:Propx:αh:p⊢ p All goals completed! 🐙 -- We now add a (recursive) extension macro_rules | `(tactic| triv) => `(tactic| apply And.intro <;> triv) example (x : α) (h : p) : x = x ∧ p := α:Sort u_1p:Propx:αh:p⊢ x = x ∧ p All goals completed! 🐙

5.10. 연습문제🔗

  1. 명제와 증명과 정량자와 동치의 연습문제로 돌아가서, 필요에 따라 rw와 simp도 사용하면서 택틱 증명으로 다시 풀 수 있는 만큼 풀어 보십시오.

  2. 택틱 조합자를 사용하여 다음에 대한 한 줄짜리 증명을 얻으십시오.

declaration uses `sorry`example (p q r : Prop) (hp : p) : (p ∨ q ∨ r) ∧ (q ∨ p ∨ r) ∧ (q ∨ r ∨ p) := p:Propq:Propr:Prophp:p⊢ (p ∨ q ∨ r) ∧ (q ∨ p ∨ r) ∧ (q ∨ r ∨ p) All goals completed! 🐙