4.1. 전칭 한정자🔗

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

전칭 한정자 ∀ 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의 특수한 경우로 생각할 수 있습니다.

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

표기법상의 관례로, 전칭 한정자에는 가능한 한 가장 넓은 범위를 부여합니다. 따라서 위 예제에서 x에 대한 한정자의 범위를 가설로 제한하려면 괄호가 필요합니다. ∀ y : α, p y를 증명하는 표준적인 방법은 임의의 y를 취하여 p y를 증명하는 것입니다. 이것이 도입 규칙입니다. 이제 h가 ∀ x : α, p x ∧ q x 타입을 가진다고 하면, 표현식 h y는 p y ∧ q y 타입을 가집니다. 이것이 제거 규칙입니다. 왼쪽 연언지를 취하면 원하는 결론인 p y를 얻습니다.

속박 변수의 이름을 바꾼 것만 다른 표현식들은 동치로 간주된다는 점을 기억하십시오. 따라서 예를 들어, 가설과 결론 모두에 같은 변수 x를 사용하고, 증명에서는 이를 다른 변수 z로 인스턴스화할 수도 있었습니다:

또 다른 예로, 관계 r이 추이적이라는 사실은 다음과 같이 표현할 수 있습니다:

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의 증명을 얻습니다.

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

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라고 간단히 쓸 수 있다는 것입니다. 단점은 trans_r와 trans_r hab 표현식에서 인자의 타입을 추론하는 데 필요한 정보가 Lean에 충분하지 않다는 것입니다. 첫 번째 #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)으로 만드는 것이 바로 이 성질입니다.

“서술적(predicative)”이라는 용어는 20세기로 넘어갈 무렵의 기초론적 발전에서 유래합니다. 당시 푸앵카레와 러셀 같은 논리학자들은 집합론의 역설이 “악순환”에서 비롯된다고 보았습니다. 이 악순환은 정의하려는 바로 그 성질을 항목으로 포함하는 모임에 대해 한정하여 그 성질을 정의할 때 생깁니다. α가 임의의 타입이면 α 위의 모든 술어로 이루어진 타입 α → Prop(“α의 멱타입”)을 만들 수 있다는 점에 주목하십시오. Prop이 비술어적(impredicative)이라는 것은 α → 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에서 인스턴스화하도록 지시합니다.

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

사영 표기법을 사용할 수도 있습니다:

반사성(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이라는 점에 주목하십시오. 따라서 이 술어를 추론하려면 고차 단일화(higher-order unification)의 한 사례를 풀어야 합니다. 가장 일반적인 경우에 고차 단일자가 존재하는지 판정하는 문제는 결정 불가능하며, Lean은 기껏해야 이 문제에 대해 불완전하고 근사적인 해만을 제공할 수 있습니다. 그 결과, Eq.subst가 항상 원하는 대로 동작하지는 않습니다. 매크로 h ▸ e는 이 암시적 매개변수를 계산하는 데 더 효과적인 휴리스틱을 사용하며, Eq.subst를 적용하면 실패하는 상황에서도 성공하는 경우가 많습니다.

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

4.3. 계산적 증명🔗

계산적 증명은 상등의 추이성과 같은 기본 원리에 의해 합성되도록 의도된 중간 결과들의 사슬일 뿐입니다. 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로 환원되면, 택틱은 반사성을 적용하여 이를 증명합니다.

재작성은 순차적으로 적용할 수 있으므로 위의 증명을 다음과 같이 줄일 수 있습니다.

혹은 이렇게 쓸 수도 있습니다:

반면 simp 택틱은 주어진 항등식들을 항 안에서 적용할 수 있는 곳이면 어디에서든 순서에 상관없이 반복적으로 적용하여 목표를 다시 씁니다. 또한 이 택틱은 시스템에 미리 선언되어 있던 다른 규칙들도 사용하며, 무한 루프에 빠지지 않도록 교환법칙을 적절히 적용합니다. 그 결과, 이 정리를 다음과 같이 증명할 수도 있습니다:

다음 장에서는 rw와 simp의 여러 변형을 다루겠습니다.

calc 명령은 어떤 형태로든 추이성을 지원하는 관계라면 무엇이든 사용할 수 있도록 설정할 수 있습니다. 심지어 서로 다른 관계를 조합할 수도 있습니다.