4.1. 전칭 기호🔗

α가 임의의 타입이라면, α에 대한 단항 술어 p를 α → Prop 타입의 객체로 나타낼 수 있음에 주목하십시오. 이 경우, x : α가 주어지면, p x는 x에 대해 p가 성립한다는 주장을 나타냅니다. 마찬가지로, 객체 r : α → α → Prop은 α에 대한 이항 관계를 나타냅니다. x y : α가 주어지면, r x y는 x가 y와 관계가 있다는 주장을 나타냅니다.

전칭 기호(universal quantifier) ∀ x : α, p x는 “모든 x : α에 대해 p x가 성립한다”라는 주장을 나타내는 것으로 이해됩니다. 명제 연결사와 마찬가지로, 자연 연역 체계에서 “forall” 역시 도입 규칙과 소거 규칙에 의해 지배됩니다. 비형식적으로 도입 규칙은 다음과 같이 서술됩니다:

x : α가 임의로 주어진 맥락에서 p x의 증명이 주어지면, ∀ x : α, p x의 증명을 얻습니다.

소거 규칙은 다음과 같습니다:

∀ x : α, p x의 증명과 임의의 항 t : α가 주어지면, p t의 증명을 얻습니다.

함의의 경우와 마찬가지로, 여기서 명제-타입 대응(propositions-as-types) 해석이 작동합니다. 의존 화살표 타입에 대한 도입 규칙과 소거 규칙을 기억해 봅시다.

x : α가 임의인 문맥에서 β x 타입을 갖는 항 t가 주어지면, (fun x : α => t) : (x : α) → β x가 성립합니다.

소거 규칙은 다음과 같이 명시됩니다:

항 s : (x : α) → β x와 임의의 항 t : α가 주어지면, s t : β t가 성립합니다.

p x가 Prop 타입을 가지는 경우, (x : α) → β x를 ∀ x : α, p x로 바꾸면 이를 전칭 기호를 포함하는 증명을 구성하기 위한 올바른 규칙으로 읽을 수 있습니다.

따라서 구성 계산법(Calculus of Constructions)은 이러한 방식으로 의존 화살표 타입을 forall-표현식과 동일시합니다. p가 임의의 표현식이라면, ∀ x : α, p는 (x : α) → p에 대한 대안적 표기법에 지나지 않으며, p가 명제인 경우에는 전자가 후자보다 더 자연스럽다는 발상에서 비롯된 것입니다. 일반적으로 표현식 p는 x : α에 의존하게 됩니다. 일반적인 함수 공간의 경우, α → β를 β가 x에 의존하지 않는 (x : α) → β의 특수한 경우로 해석할 수 있었다는 점을 상기하십시오. 마찬가지로, 명제 사이의 함의 p → q도 표현식 q가 x에 의존하지 않는 ∀ x : p, q의 특수한 경우로 생각할 수 있습니다.

다음은 propositions-as-types 대응이 실제로 어떻게 적용되는지 보여주는 예시입니다.

표기 관례상, 우리는 전칭 기호에 가능한 한 가장 넓은 범위를 부여하므로, 위 예시에서 x에 대한 전칭 기호를 가설로 한정하려면 괄호가 필요합니다. ∀ y : α, p y를 증명하는 정형적인 방법은 임의의 y를 취하여 p y를 증명하는 것입니다. 이것이 도입 규칙입니다. 이제 h가 ∀ x : α, p x ∧ q x 타입을 갖는다고 할 때, 식 h y는 p y ∧ q y 타입을 갖습니다. 이것이 소거 규칙입니다. 좌측 연언지를 취하면 원하는 결론인 p y를 얻습니다.

묶인 변수의 이름을 바꾸는 정도로만 차이가 나는 표현은 동치로 간주된다는 점을 기억하십시오. 예를 들어, 가설과 결론 모두에서 동일한 변수 x를 사용했다가, 증명에서는 이를 다른 변수 z로 인스턴스화할 수도 있습니다.

또 다른 예로, 관계 r이 전이적(transitive)이라는 사실을 어떻게 표현할 수 있는지 살펴보겠습니다:

trans_r : ∀ (x y z : α), r x y → r y z → r x z

trans_r a b c : r a b → r b c → r a c

trans_r a b c hab : r b c → r a c

trans_r a b c hab hbc : r a c

여기서 무슨 일이 일어나고 있는지 생각해 봅시다. trans_r를 값 a b c에 인스턴스화하면, 결국 r a b → r b c → r a c의 증명을 얻게 됩니다. 이를 “가설” hab : r a b에 적용하면, 함의 r b c → r a c의 증명을 얻습니다. 마지막으로, 이를 가설 hbc에 적용하면 결론 r a c의 증명이 산출됩니다.

이와 같은 상황에서는 인자 hab hbc로부터 추론될 수 있는 인자 a b c를 매번 제공하는 것이 번거로울 수 있습니다. 그런 이유로, 이러한 인자들을 암시적으로 만드는 것이 일반적입니다.

trans_r : r ?m.4 ?m.5 → r ?m.5 ?m.6 → r ?m.4 ?m.6

trans_r hab : r b ?m.6 → r a ?m.6

trans_r hab hbc : r a c

장점은 r a c의 증명으로 단순히 trans_r hab hbc라고 쓸 수 있다는 것입니다. 단점은 Lean이 trans_r와 trans_r hab 표현식에서 인자의 타입을 추론하기에 충분한 정보를 가지고 있지 않다는 것입니다. 첫 번째 #check 명령의 출력은 r ?m.1 ?m.2 → r ?m.2 ?m.3 → r ?m.1 ?m.3이며, 이는 이 경우 암시적 인자가 지정되지 않았음을 나타냅니다.

다음은 동치 관계를 사용하여 기본적인 추론을 수행하는 방법을 보여주는 예시입니다:

전칭 양화사를 사용하는 데 익숙해지려면, 이 절 끝에 있는 연습문제 중 몇 가지를 풀어 보아야 합니다.

Prop을 다른 타입들과 구별 짓는 것은 바로 의존 화살표 타입, 특히 전칭 한정자에 대한 타이핑 규칙입니다. α : Sort i와 β : Sort j가 있다고 가정합시다. 여기서 표현식 β는 변수 x : α에 의존할 수 있습니다. 그러면 (x : α) → β는 Sort (imax i j)의 원소이며, 여기서 imax i j는 j가 0이 아닐 경우 i와 j의 최댓값이고, 그렇지 않을 경우 0입니다.

아이디어는 다음과 같습니다. j가 0이 아니라면, (x : α) → β는 Sort (max i j)의 원소입니다. 다시 말해, α에서 β로 가는 의존 함수의 타입은 색인이 i와 j의 최댓값인 유니버스에 “존재”합니다. 그러나 β가 Sort 0에 속한다고, 즉 Prop의 원소라고 가정해 봅시다. 이 경우, α가 어떤 타입 유니버스에 속하든 상관없이 (x : α) → β 또한 Sort 0의 원소입니다. 다시 말해, β가 α에 의존하는 명제라면, ∀ x : α, β 역시 명제입니다. 이는 Prop을 데이터가 아닌 명제들의 타입으로 해석함을 반영하며, 바로 이 점이 Prop을 impredicative하게 만듭니다.

“술어적”이라는 용어는 20세기 전환기 무렵의 기초론적 발전에서 유래합니다. 당시 푸앵카레와 러셀 같은 논리학자들은 집합론적 역설의 원인을, 정의되고 있는 바로 그 속성을 포함하는 모음에 대해 양화함으로써 어떤 속성을 정의할 때 발생하는 “악순환”에 있다고 보았습니다. α가 임의의 타입이라면, α에 대한 모든 술어의 타입인 α → Prop(“α의 거듭제곱 타입”)을 구성할 수 있다는 점에 유의하십시오. Prop의 비술어성은 α → Prop에 대해 양화하는 명제를 구성할 수 있음을 의미합니다. 특히, α에 대한 모든 술어에 대해 양화함으로써 α에 대한 술어를 정의할 수 있는데, 이는 한때 문제로 여겨졌던 바로 그 순환의 유형입니다.

4.2. 동치🔗

이제 Lean의 라이브러리에 정의된 가장 근본적인 관계 중 하나, 즉 동치 관계로 눈을 돌려 봅시다. 귀납적 타입에 관한 장에서는 Lean의 논리적 프레임워크의 기본 요소들로부터 동치가 어떻게 정의되는지를 설명하겠습니다. 그동안 여기서는 그것을 사용하는 방법을 설명합니다.

물론, 동치의 근본적인 속성은 그것이 동치 관계라는 것입니다:

Eq.refl.{u_1} {α : Sort u_1} (a : α) : a = a

Eq.symm.{u} {α : Sort u} {a b : α} (h : a = b) : b = a

Eq.trans.{u} {α : Sort u} {a b c : α} (h₁ : a = b) (h₂ : b = c) : a = c

Lean에게 암시적 인자(여기서는 메타변수로 표시됨)를 삽입하지 말라고 지시하면 출력을 더 읽기 쉽게 만들 수 있습니다.

@Eq.refl : ∀ {α : Sort u} (a : α), a = a

@Eq.symm : ∀ {α : Sort u} {a b : α}, a = b → b = a

@Eq.trans : ∀ {α : Sort u} {a b c : α}, a = b → b = c → a = c

.{u} 표기는 Lean에게 상수들을 유니버스 u에서 인스턴스화하도록 지시합니다.

따라서 예를 들어, 이전 절의 예제를 동치 관계에 특수화할 수 있습니다:

프로젝션(projection) 표기법을 사용할 수도 있습니다:

반사성(reflexivity)은 겉보기보다 강력합니다. 구성 계산법(Calculus of Constructions)의 항들은 계산적 해석을 가지며, 논리적 프레임워크는 공통된 축약형(reduct)을 갖는 항들을 동일한 것으로 취급한다는 점을 상기하십시오. 그 결과, 일부 자명하지 않은 항등식들도 반사성으로 증명될 수 있습니다:

이 프레임워크의 이러한 기능은 매우 중요하기 때문에, 라이브러리는 Eq.refl _에 대한 표기법으로 rfl을 정의합니다:

하지만 동치는 동치 관계보다 훨씬 더 많은 것을 담고 있습니다. 모든 단언이 이 동치를 존중한다는 중요한 성질을 가지고 있는데, 이는 진리값을 바꾸지 않고도 같은 값을 갖는 식들을 서로 치환할 수 있다는 의미입니다. 즉, h1 : a = b와 h2 : p a가 주어지면, 치환을 이용하여 p b에 대한 증명을 구성할 수 있습니다: Eq.subst h1 h2.

두 번째 표기법에 나오는 삼각형은 Eq.subst와 Eq.symm 위에 구축된 매크로이며, \t를 입력하여 입력할 수 있습니다.

Eq.subst 규칙은 더 명시적인 치환을 수행하는 다음 보조 규칙들을 정의하는 데 사용됩니다. 이 규칙들은 적용 항, 즉 s t 형태의 항을 다루도록 설계되었습니다. 구체적으로, congrArg는 인자를 대체하는 데, congrFun은 적용되고 있는 항을 대체하는 데, congr는 둘 다를 한꺼번에 대체하는 데 사용될 수 있습니다.

Lean의 라이브러리에는 다음과 같은 다수의 일반적인 항등식이 포함되어 있습니다:

Nat.mul_add와 Nat.add_mul은 각각 Nat.left_distrib와 Nat.right_distrib의 대체 이름임에 유의하십시오. 위의 속성들은 자연수(타입 Nat)에 대해 서술된 것입니다.

다음은 결합법칙과 분배법칙을 대입과 함께 사용하는 자연수 계산의 예입니다.

Eq.subst의 두 번째 암묵적 매개변수는 치환이 일어날 문맥을 제공하는 것으로, α → Prop 타입을 가진다는 점에 주목하십시오. 따라서 이 술어를 추론하려면 고차 단일화의 인스턴스가 필요합니다. 완전히 일반적인 경우, 고차 단일자가 존재하는지 판정하는 문제는 결정 불가능하며, Lean은 기껏해야 불완전하고 근사적인 해법만을 제공할 수 있습니다. 그 결과 Eq.subst가 항상 원하는 대로 동작하지는 않습니다. 매크로 h ▸ e는 이 암묵적 매개변수를 계산하는 데 더 효과적인 휴리스틱을 사용하며, Eq.subst를 적용했을 때 실패하는 상황에서도 종종 성공합니다.

등식 추론은 매우 흔하고 중요하기 때문에, Lean은 이를 더 효과적으로 수행할 수 있는 여러 메커니즘을 제공합니다. 다음 절에서는 더 자연스럽고 명료한 방식으로 계산적 증명을 작성할 수 있는 구문을 소개합니다. 하지만 더 중요한 것은, 등식 추론이 항 재작성기(term rewriter), 단순화기(simplifier), 그리고 다른 종류의 자동화에 의해 지원된다는 점입니다. 항 재작성기와 단순화기는 다음 절에서 간략히 설명하고, 이어서 다음 장에서 더 자세히 설명합니다.

4.3. 계산적 증명🔗

계산적 증명(calculational proof)이란 등식의 추이성(transitivity)과 같은 기본 원리에 의해 결합되도록 되어 있는 중간 결과들의 연쇄에 불과합니다. Lean에서 계산적 증명은 키워드 calc로 시작하며, 다음과 같은 문법을 가집니다:

calc
  <expr>_0  'op_1'  <expr>_1  ':='  <proof>_1
  '_'       'op_2'  <expr>_2  ':='  <proof>_2
  ...
  '_'       'op_n'  <expr>_n  ':='  <proof>_n

calc 관계들이 모두 동일한 들여쓰기를 가진다는 점에 유의하십시오. 각 <proof>_i는 <expr>_{i-1} op_i <expr>_i에 대한 증명입니다.

첫 번째 관계식(즉 <expr>_0 바로 다음)에서도 _를 사용할 수 있으며, 이는 관계식/증명 쌍의 나열을 정렬하는 데 유용합니다:

calc <expr>_0
    '_' 'op_1' <expr>_1 ':=' <proof>_1
    '_' 'op_2' <expr>_2 ':=' <proof>_2
    ...
    '_' 'op_n' <expr>_n ':=' <proof>_n

다음은 예시입니다:

이러한 증명 작성 방식은 simp와 rw 택틱과 함께 사용할 때 가장 효과적이며, 이 택틱들은 다음 장에서 더 자세히 다룹니다. 예를 들어, rewrite를 위한 rw를 사용하면 위의 증명을 다음과 같이 작성할 수 있습니다.

본질적으로 rw 택틱은 주어진 동치(가설, 정리 이름, 또는 복합 항일 수 있음)를 사용하여 목표를 “다시 씁니다”. 그렇게 하여 목표가 항등식 t = t로 축소되면, 이 택틱은 이를 증명하기 위해 반사성을 적용합니다.

재작성(rewrite)은 순차적으로 적용할 수 있으므로, 위의 증명은 다음과 같이 줄일 수 있습니다:

아니면 심지어 이렇게도:

대신 simp 택틱은 주어진 항등식을 반복적으로, 임의의 순서로, 항 안에서 적용 가능한 모든 곳에 적용하여 목표를 다시 씁니다. 또한 이 택틱은 시스템에 미리 선언되어 있던 다른 규칙들도 사용하며, 무한 반복을 피하기 위해 교환법칙을 현명하게 적용합니다. 그 결과, 다음과 같은 방식으로도 이 정리를 증명할 수 있습니다.

다음 장에서는 rw와 simp의 변형들에 대해 다루겠습니다.

calc 명령은 어떤 형태로든 추이성을 지원하는 모든 관계에 대해 설정될 수 있습니다. 심지어 서로 다른 관계들을 조합할 수도 있습니다.