5.1. 택틱 모드 진입하기🔗

개념적으로, 정리를 진술하거나 have 문을 도입하면 목표가 생성됩니다. 즉, 기대 타입을 갖는 항을 구성해야 한다는 목표입니다. 예를 들어, 다음은 상수 p q : Prop, hp : p, hq : q가 있는 문맥에서 p ∧ q ∧ p 타입의 항을 구성하는 목표를 생성합니다:

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

실제로 위 예제에서 “sorry”를 밑줄로 바꾸면, Lean은 해결되지 않은 채 남아 있는 것이 바로 이 목표라고 보고합니다.

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

흔히 by 키워드를 앞 줄에 두어, 위의 예제를 다음과 같이 작성합니다.

apply 택틱은 표현식을 0개 이상의 인자를 받는 함수로 간주하여 적용합니다. 이 택틱은 표현식의 결론을 현재 목표와 단일화하고, 남은 인자 중 뒤따르는 인자가 의존하지 않는 인자마다 새 목표를 만듭니다. 위 예제에서 apply And.intro 명령은 두 개의 하위 목표를 만듭니다:

첫 번째 목표는 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⟩⟩

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

택틱 명령은 단일 식별자뿐만 아니라 복합 표현식도 인자로 받을 수 있습니다. 다음은 앞의 증명을 더 짧게 작성한 것입니다:

예상대로, 이것은 정확히 같은 증명 항을 생성합니다:

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

여러 택틱 적용은 세미콜론으로 이어 붙여 한 줄에 작성할 수 있습니다.

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

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

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

이를 두고 case가 선택된 목표에 “집중”한다고 말합니다. 또한 case 블록이 끝날 때 선택된 목표가 완전히 해결되지 않았으면 Lean은 오류를 표시합니다.

단순한 하위 목표라면 태그로 하위 목표를 선택할 필요까지는 없겠지만, 그래도 증명을 구조화하고 싶을 수 있습니다. Lean은 증명을 구조화할 수 있도록 “불릿” 표기법 . <tactics>(또는 · <tactics>)도 제공합니다.

5.2. 기본 택틱🔗

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

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

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

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