3. 명제와 증명🔗

지금까지 Lean에서 객체와 함수를 정의하는 몇 가지 방법을 살펴보았습니다. 이 장에서는 의존 타입 이론의 언어로 수학적 명제와 증명을 작성하는 방법도 설명하기 시작하겠습니다.

3.1. 타입으로서의 명제🔗

의존 타입 이론의 언어로 정의된 대상에 대한 단언을 증명하는 한 가지 전략은, 정의 언어 위에 단언 언어와 증명 언어를 층층이 쌓는 것입니다. 하지만 이런 식으로 언어를 늘려야 할 이유는 없습니다. 의존 타입 이론은 유연하고 표현력이 풍부하며, 단언과 증명을 동일한 일반적 프레임워크 안에서 표현하지 못할 이유가 없습니다.

예를 들어, 명제를 나타내는 새로운 타입 Prop을 도입하고, 다른 명제들로부터 새로운 명제를 만들어내는 생성자를 도입할 수 있습니다.

def Implies (p q : Prop) : Prop := p → q

And (a b : Prop) : Prop#check And

And (a b : Prop) : Prop

Or (a b : Prop) : Prop#check Or

Or (a b : Prop) : Prop

Not (a : Prop) : Prop#check Not

Not (a : Prop) : Prop

Implies (p q : Prop) : Prop#check Implies

Implies (p q : Prop) : Prop

variable (p q r : Prop)

p ∧ q : Prop#check And p q

p ∧ q : Prop

p ∧ q ∨ r : Prop#check Or (And p q) r

p ∧ q ∨ r : Prop

Implies (p ∧ q) (q ∧ p) : Prop#check Implies (And p q) (And q p)

Implies (p ∧ q) (q ∧ p) : Prop

그런 다음 각 원소 p : Prop에 대해, p의 증명들의 타입인 또 다른 타입 Proof p를 도입할 수 있습니다. “공리”는 그러한 타입의 상수가 될 것입니다.

def Implies (p q : Prop) : Prop := p → q
structure Proof (p : Prop) : Type where
  proof : p

Proof (p : Prop) : Type#check Proof

Proof (p : Prop) : Type

axiom and_commut (p q : Prop) : Proof (Implies (And p q) (And q p))

variable (p q : Prop)

and_commut p q : Proof (Implies (p ∧ q) (q ∧ p))#check and_commut p q

and_commut p q : Proof (Implies (p ∧ q) (q ∧ p))

하지만 공리 외에도, 기존 증명으로부터 새로운 증명을 만들어내는 규칙 또한 필요합니다. 예를 들어, 명제 논리를 위한 많은 증명 체계에는 modus ponens라는 규칙이 있습니다.

Implies p q의 증명과 p의 증명으로부터 q의 증명을 얻습니다.

이를 다음과 같이 표현할 수 있습니다:

def Implies (p q : Prop) : Prop := p → q
structure Proof (p : Prop) : Type where
  proof : p

axiom modus_ponens (p q : Prop) :
  Proof (Implies p q) → Proof p →
  Proof q

명제 논리를 위한 자연 연역 체계 역시 일반적으로 다음 규칙에 의존합니다.

p를 가정으로 가정했을 때 q의 증명이 있다고 합시다. 그러면 이 가정을 “소거”하여 Implies p q의 증명을 얻을 수 있습니다.

이를 다음과 같이 렌더링할 수 있습니다:

def Implies (p q : Prop) : Prop := p → q
structure Proof (p : Prop) : Type where
  proof : p

axiom implies_intro (p q : Prop) :
  (Proof p → Proof q) → Proof (Implies p q)

이러한 접근 방식은 단언과 증명을 구축하는 합리적인 방법을 제공해 줄 것입니다. 그렇다면 표현식 t가 단언 p의 올바른 증명이라는 것을 판단하는 일은 단순히 t가 Proof p 타입을 갖는지 확인하는 문제가 될 것입니다.

하지만 몇 가지 단순화가 가능합니다. 우선, Proof p를 p 자체와 동일시함으로써 Proof라는 항을 반복해서 쓰지 않을 수 있습니다. 다시 말해, p : Prop이 주어질 때마다 p를 타입, 즉 그 증명들의 타입으로 해석할 수 있습니다. 그러면 t : p를 t가 p의 증명이라는 주장으로 읽을 수 있습니다.

게다가, 일단 이러한 동일시를 하고 나면, 함의에 대한 규칙은 Implies p q와 p → q 사이를 자유롭게 오갈 수 있음을 보여줍니다. 다시 말해, 명제 p와 q 사이의 함의는 p의 임의의 원소를 q의 원소로 보내는 함수를 갖는 것에 대응합니다. 그 결과, 연결사 Implies의 도입은 전적으로 불필요합니다. 우리는 의존 타입 이론에서 나온 통상적인 함수 공간 생성자 p → q를 함의의 개념으로 사용할 수 있습니다.

이는 구성 계산(Calculus of Constructions)에서 따르는 접근법이며, 따라서 Lean에서도 마찬가지입니다. 자연 연역 증명 체계에서 함의를 다루는 규칙이 함수의 추상화 및 적용을 다루는 규칙과 정확히 대응한다는 사실은 커리-하워드 동형(Curry-Howard isomorphism)의 한 사례이며, 이는 때로 명제-타입 대응(propositions-as-types)이라고도 불리는 패러다임입니다. 실제로 Prop 타입은 지난 장에서 설명한 타입 계층의 맨 밑바닥인 Sort 0의 구문 설탕(syntactic sugar)입니다. 게다가 Type u 역시 Sort (u+1)의 구문 설탕일 뿐입니다. Prop은 몇 가지 특별한 특징을 가지고 있지만, 다른 타입 유니버스와 마찬가지로 화살표 생성자에 대해 닫혀 있습니다. 즉, p q : Prop이 있다면 p → q : Prop입니다.

명제를 타입으로 생각하는 방식에는 적어도 두 가지가 있습니다. 논리학과 수학을 구성주의적 관점에서 바라보는 이들에게는 이것이 명제가 의미하는 바를 충실히 표현한 것입니다: 명제 p는 일종의 데이터 타입, 즉 증명을 구성하는 데이터의 타입에 대한 명세를 나타냅니다. 이때 p의 증명이란 단순히 올바른 타입을 가진 객체 t : p입니다.

이 이념에 끌리지 않는 사람은 오히려 이를 단순한 코딩 기법으로 볼 수 있습니다. 각 명제 p에 대해, p가 거짓이면 비어 있고 p가 참이면 *라는 단일 원소를 가지는 타입을 대응시킵니다. 후자의 경우, (p에 대응하는 타입)이 inhabited하다고 말합시다. 함수 적용 및 추상화 규칙은 마침 Prop의 어떤 원소들이 inhabited한지 편리하게 추적하는 데 도움을 줍니다. 따라서 원소 t : p를 구성한다는 것은 p가 실제로 참임을 알려줍니다. p의 inhabitant는 “p가 참이라는 사실”이라고 생각할 수 있습니다. p → q의 증명은 “p가 참이라는 사실”을 사용해 “q가 참이라는 사실”을 얻어냅니다.

실제로 p : Prop이 임의의 명제라면, Lean의 커널은 두 원소 t1 t2 : p를 마치 (fun x => t) s와 t[s/x]를 정의적으로 같다고 취급하는 것과 마찬가지 방식으로, 정의적으로 같다고 취급합니다. 이는 증명 무관성이라고 알려져 있으며, 앞 문단의 해석과도 일치합니다. 이는 증명 t : p를 의존 타입 이론의 언어에서 일반적인 객체로 취급할 수 있다 하더라도, 그것들이 p가 참이라는 사실 이상의 어떠한 정보도 담고 있지 않음을 의미합니다.

우리가 propositions-as-types 패러다임에 대해 생각하도록 제안한 두 가지 방식은 근본적인 면에서 다릅니다. 구성주의적 관점에서 보면, 증명은 의존 타입 이론에서 적절한 표현식에 의해 표시되는 추상적인 수학적 대상입니다. 이와 대조적으로, 앞서 설명한 코딩 트릭의 관점에서 생각한다면, 표현식 자체는 흥미로운 어떤 것도 표시하지 않습니다. 오히려, 우리가 그것들을 적어 내려가고 그것들의 타입이 올바른지 확인할 수 있다는 사실이야말로 해당 명제가 참임을 보장합니다. 다시 말해, 표현식 자체가 증명입니다.

아래 설명에서는 이 두 가지 표현 방식을 오가며 사용할 것인데, 어떤 때는 어떤 식이 명제의 증명을 “구성한다” 또는 “만들어 낸다” 또는 “반환한다”고 말하고, 다른 때는 그것이 단순히 그러한 증명“이다”라고 말할 것입니다. 이는 컴퓨터 과학자들이 때때로 구문과 의미론의 구별을 흐릿하게 하여, 어떤 때는 프로그램이 특정 함수를 “계산한다”고 말하고, 다른 때는 마치 그 프로그램이 문제의 함수“인” 것처럼 말하는 방식과 비슷합니다.

어쨌든 정말로 중요한 것은 결론입니다. 수학적 주장을 의존 타입 이론의 언어로 형식적으로 표현하려면, 항 p : Prop을 제시해야 합니다. 그 주장을 증명하려면, 항 t : p를 제시해야 합니다. 정리 증명기로서 Lean의 역할은, 우리가 그러한 항 t를 구성하도록 돕고, 그것이 올바른 형식이며 올바른 타입을 가지는지 검증하는 것입니다.

3.2. 명제로서의 타입 다루기🔗

propositions-as-types 패러다임에서 →만 포함하는 정리는 람다 추상화와 적용을 사용하여 증명할 수 있습니다. Lean에서 theorem 명령은 새로운 정리를 도입합니다:

                set_option linter.unusedVariables false
---
variable {p : Prop}
variable {q : Prop}

theorem t1 : p → q → p := fun hp : p => fun hq : q => hp

이 증명을 자료형인 α와 β에 대한 타입 α → β → α의 표현식 fun x : α => fun y : β => x와 비교해 보십시오. 이는 각각 α와 β 타입의 인자 x와 y를 받아 x를 반환하는 함수를 나타냅니다. t1의 증명은 동일한 형태를 가지며, 유일한 차이점은 p와 q가 Type이 아닌 Prop의 원소라는 점입니다. 직관적으로, p → q → p에 대한 우리의 증명은 p와 q가 참이라고 가정하며, 첫 번째 가설을 (자명하게) 이용하여 결론인 p가 참임을 증명합니다.

theorem 명령은 사실 def 명령의 한 형태라는 점에 유의하십시오. 명제와 타입의 대응 관계에 따르면, 정리 p → q → p를 증명하는 것은 실제로 연관된 타입의 원소를 정의하는 것과 같습니다. 커널 타입 검사기의 입장에서는 이 둘 사이에 아무런 차이가 없습니다.

하지만 정의와 정리 사이에는 몇 가지 실용적인 차이점이 있습니다. 일반적인 경우 정리의 “정의”를 펼쳐 볼 필요는 전혀 없습니다. 증명 무관성에 의해, 그 정리에 대한 어떤 두 증명이든 정의적으로 같기 때문입니다. 정리의 증명이 완료되면, 일반적으로 우리는 그 증명이 존재한다는 사실만 알면 되며, 증명이 무엇인지는 중요하지 않습니다. 이러한 사실에 비추어, Lean은 증명을 환원 불가능으로 표시하는데, 이는 파일을 처리할 때 일반적으로 이를 펼칠 필요가 없다는 것을 파서(더 정확히는 정교화기)에게 알려주는 힌트 역할을 합니다. 실제로 Lean은 일반적으로 증명을 병렬로 처리하고 검사할 수 있는데, 한 증명의 정확성을 평가하는 데 다른 증명의 세부 사항을 알 필요가 없기 때문입니다. 또한, 정의의 본문에서 참조되는 섹션 변수는 자동으로 매개변수로 추가되지만, 정리의 타입에서 참조되는 변수만 추가됩니다. 이는 명제가 증명되는 방식이 증명 대상이 되는 명제 자체에 영향을 미쳐서는 안 되기 때문입니다.

정의와 마찬가지로, #print 명령을 사용하면 정리의 증명을 확인할 수 있습니다:

set_option linter.unusedVariables false
variable {p : Prop}
variable {q : Prop}

theorem t1 : p → q → p := fun hp : p => fun hq : q => hp

theorem t1 : ∀ {p q : Prop}, p → q → p :=
fun {p q} hp hq => hp#print t1

theorem t1 : ∀ {p q : Prop}, p → q → p :=
fun {p q} hp hq => hp

람다 추상화 hp : p와 hq : q는 t1의 증명에서 임시 가정으로 볼 수 있다는 점에 유의하십시오. Lean에서는 또한 show 문을 사용하여 최종 항 hp의 타입을 명시적으로 지정할 수도 있습니다.

set_option linter.unusedVariables false
variable {p : Prop}
variable {q : Prop}

theorem t1 : p → q → p :=
  fun hp : p =>
  fun hq : q =>
  show p from hp

이러한 추가 정보를 더하면 증명의 명확성을 높일 수 있으며, 증명을 작성할 때 오류를 발견하는 데 도움이 됩니다. show 명령은 타입을 표시하는 것 이상의 일을 하지 않으며, 내부적으로 지금까지 살펴본 t1의 모든 표현은 동일한 항을 만들어 냅니다.

일반적인 정의와 마찬가지로, 람다 추상화된 변수를 콜론 왼쪽으로 옮길 수 있습니다:

set_option linter.unusedVariables false
variable {p : Prop}
variable {q : Prop}

theorem t1 (hp : p) (hq : q) : p := hp

theorem t1 : ∀ {p q : Prop}, p → q → p :=
fun {p q} hp hq => hp#print t1

theorem t1 : ∀ {p q : Prop}, p → q → p :=
fun {p q} hp hq => hp

정리 t1을 함수 적용처럼 사용할 수 있습니다:

set_option linter.unusedVariables false
variable {p : Prop}
variable {q : Prop}

theorem t1 (hp : p) (hq : q) : p := hp

axiom hp : p

theorem t2 : q → p := t1 hp

axiom 선언은 주어진 타입의 원소가 존재한다고 가정하며, 논리적 일관성을 훼손할 수 있습니다. 예를 들어, 이를 이용해 공집합 타입 False에 원소가 있다고 가정할 수 있습니다:

                axiom unsound : False
-- Everything follows from false
theorem ex : 1 = 0 :=
  False.elim unsound

“axiom” hp : p를 선언하는 것은 hp가 증거가 되어 p가 참이라고 선언하는 것과 다름없습니다. 정리 t1 : p → q → p를 p가 참이라는 사실 hp : p에 적용하면 정리 t1 hp : q → p가 산출됩니다.

정리 t1을 다음과 같이 작성할 수도 있다는 점을 상기하십시오:

set_option linter.unusedVariables false

theorem t1 {p q : Prop} (hp : p) (hq : q) : p := hp

theorem t1 : ∀ {p q : Prop}, p → q → p :=
fun {p q} hp hq => hp#print t1

theorem t1 : ∀ {p q : Prop}, p → q → p :=
fun {p q} hp hq => hp

t1의 타입은 이제 ∀ {p q : Prop}, p → q → p입니다. 이는 “모든 명제 쌍 p q에 대해 p → q → p가 성립한다”라는 주장으로 읽을 수 있습니다. 예를 들어, 모든 매개변수를 콜론 오른쪽으로 옮길 수도 있습니다:

set_option linter.unusedVariables false

theorem t1 : ∀ {p q : Prop}, p → q → p :=
  fun {p q : Prop} (hp : p) (hq : q) => hp

p와 q가 변수로 선언되어 있다면, Lean은 이들을 자동으로 일반화해 줍니다:

                variable {p q : Prop}

theorem t1 : p → q → p := fun (hp : p) (Variable name `hq` 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] _hq

Note: This linter can be disabled with `set_option linter.unusedVariables false`hq : q) => hp

이런 방식으로 t1을 일반화하면, 서로 다른 명제 쌍에 이를 적용하여 일반 정리의 다양한 인스턴스를 얻을 수 있습니다.

set_option linter.unusedVariables false

theorem t1 (p q : Prop) (hp : p) (hq : q) : p := hp

variable (p q r s : Prop)

t1 p q : p → q → p#check t1 p q

t1 p q : p → q → p

t1 r s : r → s → r#check t1 r s

t1 r s : r → s → r

t1 (r → s) (s → r) : (r → s) → (s → r) → r → s#check t1 (r → s) (s → r)

t1 (r → s) (s → r) : (r → s) → (s → r) → r → s

variable (h : r → s)

t1 (r → s) (s → r) h : (s → r) → r → s#check t1 (r → s) (s → r) h

t1 (r → s) (s → r) h : (s → r) → r → s

다시 한번 명제-타입 대응을 사용하면, r → s 타입의 변수 h는 r → s가 성립한다는 가설, 즉 전제로 볼 수 있습니다.

또 다른 예시로, 이전 장에서 다루었던 합성 함수를 이번에는 타입 대신 명제를 사용하여 살펴봅시다.

                variable (p q r s : Prop)

theorem t2 (h₁ : q → r) (h₂ : p → q) : p → r :=
  fun h₃ : p =>
  show r from h₁ (h₂ h₃)

명제 논리의 정리로서, t2는 무엇을 말하고 있습니까?

이 예제에서와 같이, 가설을 나타낼 때 \0, \1, \2, ... 등으로 입력하는 숫자 유니코드 아래첨자를 사용하는 것이 흔히 유용하다는 점에 유의하십시오.

3.3. 명제 논리🔗

Lean은 모든 표준 논리 연결사와 표기법을 정의합니다. 명제 연결사에는 다음과 같은 표기법이 있습니다.

ASCII	유니코드	에디터 단축키	정의
`True`			`True`
`False`			`False`
`Not`	`¬`	`\not`, `\neg`	`Not`
`/\`	`∧`	`\and`	`And`
`\/`	`∨`	`\or`	`Or`
`->`	`→`	`\to`, `\r`, `\imp`
`<->`	`↔`	`\iff`, `\lr`	`Iff`

이들은 모두 Prop의 값을 취합니다.

variable (p q : Prop)

p → q → p ∧ q : Prop#check p → q → p ∧ q

p → q → p ∧ q : Prop

¬p → p ↔ False : Prop#check ¬p → p ↔ False

¬p → p ↔ False : Prop

p ∨ q → q ∨ p : Prop#check p ∨ q → q ∨ p

p ∨ q → q ∨ p : Prop

연산 순서는 다음과 같습니다. 단항 부정 ¬이 가장 강하게 결합하고, 그다음 ∧, 그다음 ∨, 그다음 →, 마지막으로 ↔ 순입니다. 예를 들어, a ∧ b → c ∨ d ∧ e는 (a ∧ b) → (c ∨ (d ∧ e))를 의미합니다. →는 다른 이항 연결사들과 마찬가지로 오른쪽으로 결합한다는 점을 기억하십시오(인자들이 다른 Type 대신 Prop의 원소가 되었다고 해서 달라지는 것은 없습니다). 따라서 p q r : Prop이 있을 때, 식 p → q → r은 “만약 p라면, q일 때 r이다”라고 읽습니다. 이는 단지 p ∧ q → r을 “커리(curried)” 형태로 쓴 것일 뿐입니다.

지난 장에서 우리는 람다 추상화가 →에 대한 “도입 규칙”으로 간주될 수 있음을 살펴보았습니다. 현재의 맥락에서, 이는 함의를 “도입”하거나 확립하는 방법을 보여줍니다. 함수 적용은 “소거 규칙”으로 간주될 수 있으며, 이는 증명에서 함의를 “소거”하거나 사용하는 방법을 보여줍니다. 그 밖의 명제 연결사들은 Lean의 라이브러리에 정의되어 있으며, 자동으로 불러와집니다. 각 연결사에는 고유한 도입 규칙과 소거 규칙이 함께 제공됩니다.

3.3.1. 논리곱🔗

And.intro h1 h2 표현식은 증명 h1 : p와 h2 : q를 사용하여 p ∧ q의 증명을 구성합니다. And.intro를 and-introduction 규칙이라고 설명하는 것이 일반적입니다. 다음 예제에서는 And.intro를 사용하여 p → q → p ∧ q의 증명을 만듭니다.

variable (p q : Prop)

example (hp : p) (hq : q) : p ∧ q := And.intro hp hq

fun hp hq => ⟨hp, hq⟩ : p → q → p ∧ q#check fun (hp : p) (hq : q) => And.intro hp hq

fun hp hq => ⟨hp, hq⟩ : p → q → p ∧ q

example 명령은 정리에 이름을 붙이거나 영구 컨텍스트에 저장하지 않고 정리를 서술합니다. 본질적으로 이 명령은 주어진 항이 명시된 타입을 가지는지 확인할 뿐입니다. 이는 예시를 보이는 데 편리하므로, 앞으로 자주 사용하겠습니다.

표현식 And.left h는 증명 h : p ∧ q로부터 p의 증명을 만듭니다. 마찬가지로, And.right h는 q의 증명입니다. 이들은 흔히 좌측 및 우측 and-elimination 규칙으로 알려져 있습니다.

                  variable (p q : Prop)

example (h : p ∧ q) : p := And.left h
example (h : p ∧ q) : q := And.right h

이제 다음 증명 항을 사용하여 p ∧ q → q ∧ p를 증명할 수 있습니다.

                  variable (p q : Prop)

example (h : p ∧ q) : q ∧ p :=
  And.intro (And.right h) (And.left h)

and-도입과 and-소거가 데카르트 곱의 페어링 및 사영 연산과 유사하다는 점에 주목하십시오. 차이점은 hp : p와 hq : q가 주어졌을 때 And.intro hp hq는 p ∧ q : Prop 타입을 가지는 반면, a : α와 b : β가 주어졌을 때 Prod.mk a b는 α × β : Type 타입을 가진다는 것입니다. Prod는 Prop과 함께 사용할 수 없으며, And는 Type과 함께 사용할 수 없습니다. ∧와 × 사이의 유사성은 커리-하워드 동형사상의 또 다른 사례이지만, 함의 및 함수 공간 생성자와는 달리 ∧와 ×는 Lean에서 별도로 다루어집니다. 그러나 이 유비를 통해 보면, 방금 우리가 구성한 증명은 쌍의 원소를 뒤바꾸는 함수와 유사합니다.

Lean의 특정 타입들이 구조체라는 것을 구조체와 레코드에서 살펴보겠습니다. 즉, 해당 타입은 적절한 인자들의 나열로부터 그 타입의 원소를 만들어내는 단 하나의 표준적인 생성자로 정의됩니다. 모든 p q : Prop에 대해, p ∧ q가 그 예입니다. 원소를 구성하는 표준적인 방법은 And.intro를 적절한 인자 hp : p와 hq : q에 적용하는 것입니다. Lean은 이러한 상황, 즉 관련 타입이 귀납적 타입이고 문맥으로부터 추론될 수 있는 경우, 익명 생성자 표기 ⟨arg1, arg2, ...⟩를 사용할 수 있게 해 줍니다. 특히 우리는 종종 And.intro hp hq 대신 ⟨hp, hq⟩를 쓸 수 있습니다.

variable (p q : Prop)

variable (hp : p) (hq : q)

⟨hp, hq⟩ : p ∧ q#check (⟨hp, hq⟩ : p ∧ q)

⟨hp, hq⟩ : p ∧ q

이 꺾쇠 괄호는 각각 \<와 \>를 입력하여 얻을 수 있습니다.

Lean은 또 다른 유용한 구문적 장치를 제공합니다. 귀납적 타입 Foo(인자가 적용되어 있을 수도 있음)의 표현식 e가 주어졌을 때, 표기법 e.bar는 Foo.bar e의 축약형입니다. 이는 네임스페이스를 열지 않고도 함수에 접근할 수 있는 편리한 방법을 제공합니다. 예를 들어, 다음 두 표현식은 같은 것을 의미합니다.

variable (xs : List Nat)

xs.length : Nat#check List.length xs

xs.length : Nat

xs.length : Nat#check xs.length

xs.length : Nat

그 결과, h : p ∧ q가 주어졌을 때 And.left h를 h.left로, And.right h를 h.right로 쓸 수 있습니다. 따라서 위의 예제 증명을 다음과 같이 간편하게 다시 쓸 수 있습니다.

                  variable (p q : Prop)

example (h : p ∧ q) : q ∧ p :=
  ⟨h.right, h.left⟩

간결함과 모호함 사이에는 미묘한 경계가 있으며, 이런 식으로 정보를 생략하면 때로는 증명을 더 읽기 어렵게 만들 수 있습니다. 하지만 위와 같이 단순한 구성에서는 h의 타입과 구성의 목표가 명확할 때, 이 표기법은 깔끔하고 효과적입니다.

“And”와 같은 구성을 반복하는 것은 흔한 일입니다. Lean은 또한 오른쪽으로 결합하는 중첩된 생성자를 평탄화할 수 있도록 허용하므로, 다음 두 증명은 동등합니다.

                  variable (p q : Prop)

example (h : p ∧ q) : q ∧ p ∧ q :=
  ⟨h.right, ⟨h.left, h.right⟩⟩

example (h : p ∧ q) : q ∧ p ∧ q :=
  ⟨h.right, h.left, h.right⟩

이 또한 종종 유용합니다.

3.3.2. 논리합🔗

표현식 Or.intro_left q hp는 증명 hp : p로부터 p ∨ q의 증명을 만듭니다. 마찬가지로, Or.intro_right p hq는 증명 hq : q를 사용하여 p ∨ q에 대한 증명을 만듭니다. 이들은 각각 좌측과 우측 or-introduction(선언 도입) 규칙입니다.

                  variable (p q : Prop)
example (hp : p) : p ∨ q := Or.intro_left q hp
example (hq : q) : p ∨ q := Or.intro_right p hq

or-elimination 규칙은 조금 더 복잡합니다. 그 발상은 p ∨ q로부터 r을 증명하되, r이 p로부터 따라 나옴을 보이고 r이 q로부터 따라 나옴을 보임으로써 증명한다는 것입니다. 다시 말해, 이는 경우를 나누어 하는 증명입니다. Or.elim hpq hpr hqr 표현식에서 Or.elim은 hpq : p ∨ q, hpr : p → r, hqr : q → r이라는 세 개의 인자를 받아 r의 증명을 만들어 냅니다. 다음 예제에서는 Or.elim을 사용하여 p ∨ q → q ∨ p를 증명합니다.

                  variable (p q r : Prop)

example (h : p ∨ q) : q ∨ p :=
  Or.elim h
    (fun hp : p =>
      show q ∨ p from Or.intro_right q hp)
    (fun hq : q =>
      show q ∨ p from Or.intro_left p hq)

대부분의 경우, Or.intro_right와 Or.intro_left의 첫 번째 인자는 Lean에 의해 자동으로 추론될 수 있습니다. 따라서 Lean은 Or.intro_right _와 Or.intro_left _의 축약형으로 볼 수 있는 Or.inr과 Or.inl을 제공합니다. 따라서 위의 증명 항은 더 간결하게 작성될 수 있습니다:

                  variable (p q r : Prop)

example (h : p ∨ q) : q ∨ p :=
  Or.elim h (fun hp => Or.inr hp) (fun hq => Or.inl hq)

전체 표현식에는 Lean이 hp와 hq의 타입까지도 추론할 수 있을 만큼 충분한 정보가 담겨 있다는 점에 주목하십시오. 그러나 더 긴 버전에서 타입 주석을 사용하면 증명을 더 읽기 쉽게 만들 수 있으며, 오류를 발견하고 디버깅하는 데에도 도움이 됩니다.

Or는 생성자가 두 개이므로, 익명 생성자 표기법을 사용할 수 없습니다. 하지만 Or.elim h 대신 h.elim이라고 여전히 쓸 수 있습니다:

                  variable (p q r : Prop)

example (h : p ∨ q) : q ∨ p :=
  h.elim (fun hp => Or.inr hp) (fun hq => Or.inl hq)

이번에도 이러한 축약이 가독성을 높이는지 저해하는지 판단력을 발휘해야 합니다.

3.3.3. 부정과 거짓🔗

부정 ¬p는 실제로 p → False로 정의되므로, p로부터 모순을 이끌어냄으로써 ¬p를 얻습니다. 마찬가지로 표현식 hnp hp는 hp : p와 hnp : ¬p로부터 False의 증명을 만들어냅니다. 다음 예제는 이 두 규칙을 모두 사용하여 (p → q) → ¬q → ¬p의 증명을 만들어냅니다. (기호 ¬는 \not 또는 \neg를 입력하여 만들 수 있습니다.)

                  variable (p q : Prop)

example (hpq : p → q) (hnq : ¬q) : ¬p :=
  fun hp : p =>
  show False from hnq (hpq hp)

연결사 False는 단일한 소거 규칙 False.elim을 가지는데, 이는 모순으로부터 무엇이든 도출된다는 사실을 표현합니다. 이 규칙은 때때로 ex falso(ex falso sequitur quodlibet의 줄임말)라 불리거나, 폭발 원리라 불립니다.

                  variable (p q : Prop)

example (hp : p) (hnp : ¬p) : q := False.elim (hnp hp)

거짓으로부터 도출되는 임의의 사실 q는 False.elim의 암묵적 인자이며, 자동으로 추론됩니다. 모순된 가설로부터 임의의 사실을 도출하는 이러한 패턴은 상당히 흔하며, absurd로 표현됩니다.

                  variable (p q : Prop)

example (hp : p) (hnp : ¬p) : q := absurd hp hnp

예를 들어, 다음은 ¬p → q → (q → p) → r의 증명입니다:

                  variable (p q r : Prop)

example (hnp : ¬p) (hq : q) (hqp : q → p) : r :=
  absurd (hqp hq) hnp

그런데 False가 소거 규칙만 가지는 것처럼, True는 도입 규칙만 가지며, 이는 True.intro : True입니다. 다시 말해, True는 그저 참이며, 표준적인 증명인 True.intro를 가집니다.

3.3.4. 논리적 동치🔗

Iff.intro h1 h2 표현식은 h1 : p → q와 h2 : q → p로부터 p ↔ q의 증명을 만들어 냅니다. Iff.mp h 표현식은 h : p ↔ q로부터 p → q의 증명을 만들어 냅니다. 마찬가지로, Iff.mpr h는 h : p ↔ q로부터 q → p의 증명을 만들어 냅니다. 다음은 p ∧ q ↔ q ∧ p의 증명입니다:

variable (p q : Prop)

theorem and_swap : p ∧ q ↔ q ∧ p :=
  Iff.intro
    (fun h : p ∧ q =>
     show q ∧ p from And.intro (And.right h) (And.left h))
    (fun h : q ∧ p =>
     show p ∧ q from And.intro (And.right h) (And.left h))

and_swap p q : p ∧ q ↔ q ∧ p#check and_swap p q

and_swap p q : p ∧ q ↔ q ∧ p

variable (h : p ∧ q)

example : q ∧ p := Iff.mp (and_swap p q) h

익명 생성자 표기법을 사용하여 정방향과 역방향 증명으로부터 p ↔ q의 증명을 구성할 수 있으며, mp와 mpr에 대해 . 표기법을 사용할 수도 있습니다. 따라서 앞선 예제들은 다음과 같이 간결하게 작성할 수 있습니다.

                  variable (p q : Prop)

theorem and_swap : p ∧ q ↔ q ∧ p :=
  ⟨ fun h => ⟨h.right, h.left⟩, fun h => ⟨h.right, h.left⟩ ⟩

example (h : p ∧ q) : q ∧ p := (and_swap p q).mp h

3.4. 보조 하위 목표 도입하기🔗

여기서 Lean이 긴 증명을 구조화하는 데 도움을 주기 위해 제공하는 또 다른 장치, 즉 증명에서 보조 하위 목표를 도입하는 have 구성을 소개하기에 좋습니다. 다음은 이전 절에서 가져와 수정한 작은 예제입니다:

                variable (p q : Prop)

example (h : p ∧ q) : q ∧ p :=
  have hp : p := h.left
  have hq : q := h.right
  show q ∧ p from And.intro hq hp

내부적으로, have h : p := s; t라는 표현식은 (fun (h : p) => t) s라는 항을 만들어 냅니다. 다시 말해, s는 p의 증명이고, t는 h : p를 가정했을 때 원하는 결론의 증명이며, 이 둘은 람다 추상화와 적용을 통해 결합됩니다. 이 간단한 장치는 긴 증명을 구조화할 때 매우 유용한데, 중간의 have들을 최종 목표로 이어지는 디딤돌로 사용할 수 있기 때문입니다.

Lean은 또한 목표로부터 거꾸로 추론하는 구조화된 방법도 지원하는데, 이는 일반 수학에서 “보이기만 하면 충분하다”라는 구성을 본뜬 것입니다. 다음 예제는 앞선 증명의 마지막 두 줄을 단순히 뒤바꾼 것입니다.

                variable (p q : Prop)

example (h : p ∧ q) : q ∧ p :=
  have hp : p := h.left
  suffices hq : q from And.intro hq hp
  show q from And.right h

suffices hq : q를 작성하면 두 개의 목표가 남습니다. 첫째, 추가 가설 hq : q를 사용하여 원래 목표 q ∧ p를 증명함으로써, q를 보이는 것으로 실제로 충분함을 보여야 합니다. 마지막으로, q를 보여야 합니다.

3.5. 고전 논리🔗

지금까지 살펴본 도입 규칙과 소거 규칙은 모두 구성적이며, 이는 곧 propositions-as-types 대응에 기반하여 논리 연결사에 대한 계산적 이해를 반영한다는 것을 의미합니다. 일반적인 고전 논리는 여기에 배중률, 즉 p ∨ ¬p를 추가합니다. 이 원리를 사용하려면 classical 네임스페이스를 열어야 합니다.

open Classical

variable (p : Prop)

em p : p ∨ ¬p#check em p

em p : p ∨ ¬p

직관적으로 볼 때, 구성적 “또는(Or)”은 매우 강력합니다. p ∨ q를 주장한다는 것은 둘 중 어느 쪽이 성립하는지를 안다는 것과 마찬가지입니다. RH가 리만 가설을 나타낸다면, 고전 수학자는 두 선언지 중 어느 쪽도 아직 주장할 수 없음에도 불구하고 RH ∨ ¬RH를 기꺼이 주장합니다.

배중률의 한 가지 결과는 이중 부정 소거의 원리입니다:

                open Classical

theorem dne {p : Prop} (h : ¬¬p) : p :=
  Or.elim (em p)
    (fun hp : p => hp)
    (fun hnp : ¬p => absurd hnp h)

이중 부정 제거는 ¬p를 가정하고 False를 도출함으로써 임의의 명제 p를 증명할 수 있게 해주는데, 이는 ¬¬p를 증명하는 것과 마찬가지이기 때문입니다. 다시 말해, 이중 부정 제거는 귀류법에 의한 증명을 수행할 수 있게 해주는데, 이는 구성적 논리에서는 일반적으로 불가능한 것입니다. 연습 문제로, 그 역, 즉 dne로부터 em을 증명할 수 있음을 보이는 것을 시도해 볼 수 있습니다.

고전 공리는 em을 통해 정당화할 수 있는 추가적인 증명 패턴에도 접근할 수 있게 해 줍니다. 예를 들어, 다음과 같이 경우 나누기(case) 증명을 수행할 수 있습니다.

                open Classical
variable (p : Prop)

example (h : ¬¬p) : p :=
  byCases
    (fun h1 : p => h1)
    (fun h1 : ¬p => absurd h1 h)

또는 귀류법으로 증명을 진행할 수도 있습니다:

                open Classical
variable (p : Prop)

example (h : ¬¬p) : p :=
  byContradiction
    (fun h1 : ¬p =>
     show False from h h1)

구성적으로 사고하는 데 익숙하지 않다면, 고전적 추론이 어디에서 사용되는지 감을 잡는 데 다소 시간이 걸릴 수 있습니다. 구성적인 관점에서는 p와 q가 둘 다 참인 것은 아니라는 사실을 안다고 해서 반드시 어느 쪽이 거짓인지 알 수 있는 것은 아니므로, 다음 예제에서는 고전적 추론이 필요합니다.

open Classical
variable (p q : Prop)

example (h : ¬(p ∧ q)) : ¬p ∨ ¬q :=
  Or.elim (em p)
    (fun hp : p =>
      Or.inr
        (show ¬q from
          fun hq : q =>
          h ⟨hp, hq⟩))
    (fun hp : ¬p =>
      Or.inl hp)

구성적 논리에는 배중률이나 이중 부정 제거와 같은 원리가 허용되는 상황이 있다는 것을 나중에 살펴볼 것이며, Lean은 배중률에 의존하지 않고도 그러한 맥락에서 고전적 추론을 사용하는 것을 지원합니다.

Lean에서 고전적 추론을 지원하기 위해 사용되는 공리의 전체 목록은 공리와 계산에서 다룹니다.

3.6. 명제적 타당성의 예시🔗

Lean의 표준 라이브러리에는 명제 논리의 여러 유효한 명제에 대한 증명이 포함되어 있으며, 여러분은 이들을 자유롭게 자신의 증명에 사용할 수 있습니다. 다음 목록에는 흔히 쓰이는 여러 항등식이 포함되어 있습니다.

교환 법칙:

p ∧ q ↔ q ∧ p
p ∨ q ↔ q ∨ p

결합법칙:

(p ∧ q) ∧ r ↔ p ∧ (q ∧ r)
(p ∨ q) ∨ r ↔ p ∨ (q ∨ r)

분배 법칙:

p ∧ (q ∨ r) ↔ (p ∧ q) ∨ (p ∧ r)
p ∨ (q ∧ r) ↔ (p ∨ q) ∧ (p ∨ r)

그 외 속성:

(p → (q → r)) ↔ (p ∧ q → r)
((p ∨ q) → r) ↔ (p → r) ∧ (q → r)
¬(p ∨ q) ↔ ¬p ∧ ¬q
¬p ∨ ¬q → ¬(p ∧ q)
¬(p ∧ ¬p)
p ∧ ¬q → ¬(p → q)
¬p → (p → q)
(¬p ∨ q) → (p → q)
p ∨ False ↔ p
p ∧ False ↔ False
¬(p ↔ ¬p)
(p → q) → (¬q → ¬p)

이는 고전적 추론을 필요로 합니다:

(p → r ∨ s) → ((p → r) ∨ (p → s))
¬(p ∧ q) → ¬p ∨ ¬q
¬(p → q) → p ∧ ¬q
(p → q) → (¬p ∨ q)
(¬q → ¬p) → (p → q)
p ∨ ¬p
(((p → q) → p) → p)

sorry 식별자는 마법처럼 무엇이든 증명해내거나 어떤 데이터 타입의 객체든 제공합니다. 물론 이는 증명 방법으로서는 건전하지 않습니다—예를 들어 이를 사용하여 False를 증명할 수도 있습니다—그리고 Lean은 이에 의존하는 정리를 사용하거나 임포트하는 파일에 대해 심각한 경고를 발생시킵니다. 하지만 이는 긴 증명을 점진적으로 구축하는 데 매우 유용합니다. 위에서 아래로 증명을 작성하기 시작하면서, sorry를 사용하여 하위 증명을 채워 넣으십시오. Lean이 모든 sorry가 포함된 항을 받아들이는지 확인하십시오. 그렇지 않다면 수정해야 할 오류가 있는 것입니다. 그런 다음 다시 돌아가서 각 sorry를 실제 증명으로 대체하여, 더 이상 남지 않을 때까지 계속하십시오.

여기 또 다른 유용한 요령이 있습니다. sorry를 사용하는 대신, 밑줄 _를 자리표시자로 사용할 수 있습니다. 이는 해당 인자가 암시적이며 자동으로 채워져야 함을 Lean에게 알려준다는 점을 기억하십시오. Lean이 이를 시도했으나 실패하면, “자리표시자를 합성하는 방법을 모릅니다”라는 오류 메시지와 함께, 기대하는 항의 타입, 그리고 그 맥락에서 사용 가능한 모든 객체와 가설을 반환합니다. 다시 말해, 해결되지 않은 각 자리표시자에 대해 Lean은 그 지점에서 채워져야 할 하위 목표를 보고합니다. 그런 다음 이러한 자리표시자들을 점진적으로 채워 나감으로써 증명을 구성할 수 있습니다.

참고로, 위 목록에서 가져온 타당성 증명의 예시 두 가지는 다음과 같습니다.

                open Classical

-- distributivity
example (p q r : Prop) : p ∧ (q ∨ r) ↔ (p ∧ q) ∨ (p ∧ r) :=
  Iff.intro
    (fun h : p ∧ (q ∨ r) =>
      have hp : p := h.left
      Or.elim (h.right)
        (fun hq : q =>
          show (p ∧ q) ∨ (p ∧ r) from Or.inl ⟨hp, hq⟩)
        (fun hr : r =>
          show (p ∧ q) ∨ (p ∧ r) from Or.inr ⟨hp, hr⟩))
    (fun h : (p ∧ q) ∨ (p ∧ r) =>
      Or.elim h
        (fun hpq : p ∧ q =>
          have hp : p := hpq.left
          have hq : q := hpq.right
          show p ∧ (q ∨ r) from ⟨hp, Or.inl hq⟩)
        (fun hpr : p ∧ r =>
          have hp : p := hpr.left
          have hr : r := hpr.right
          show p ∧ (q ∨ r) from ⟨hp, Or.inr hr⟩))

-- an example that requires classical reasoning
example (p q : Prop) : ¬(p ∧ ¬q) → (p → q) :=
  fun h : ¬(p ∧ ¬q) =>
  fun hp : p =>
  show q from
    Or.elim (em q)
      (fun hq : q => hq)
      (fun hnq : ¬q => absurd (And.intro hp hnq) h)

3.7. 연습문제🔗

다음 항등식들을 증명하되, sorry 자리 표시자를 실제 증명으로 대체하십시오.

                variable (p q r : Prop)

-- commutativity of ∧ and ∨
declaration uses `sorry`example : p ∧ q ↔ q ∧ p := sorry
declaration uses `sorry`example : p ∨ q ↔ q ∨ p := sorry

-- associativity of ∧ and ∨
declaration uses `sorry`example : (p ∧ q) ∧ r ↔ p ∧ (q ∧ r) := sorry
declaration uses `sorry`example : (p ∨ q) ∨ r ↔ p ∨ (q ∨ r) := sorry

-- distributivity
declaration uses `sorry`example : p ∧ (q ∨ r) ↔ (p ∧ q) ∨ (p ∧ r) := sorry
declaration uses `sorry`example : p ∨ (q ∧ r) ↔ (p ∨ q) ∧ (p ∨ r) := sorry

-- other properties
declaration uses `sorry`example : (p → (q → r)) ↔ (p ∧ q → r) := sorry
declaration uses `sorry`example : ((p ∨ q) → r) ↔ (p → r) ∧ (q → r) := sorry
declaration uses `sorry`example : ¬(p ∨ q) ↔ ¬p ∧ ¬q := sorry
declaration uses `sorry`example : ¬p ∨ ¬q → ¬(p ∧ q) := sorry
declaration uses `sorry`example : ¬(p ∧ ¬p) := sorry
declaration uses `sorry`example : p ∧ ¬q → ¬(p → q) := sorry
declaration uses `sorry`example : ¬p → (p → q) := sorry
declaration uses `sorry`example : (¬p ∨ q) → (p → q) := sorry
declaration uses `sorry`example : p ∨ False ↔ p := sorry
declaration uses `sorry`example : p ∧ False ↔ False := sorry
declaration uses `sorry`example : (p → q) → (¬q → ¬p) := sorry

다음 항등식들을 증명하되, sorry 자리표시자를 실제 증명으로 대체하십시오. 이들은 고전적 추론을 필요로 합니다.

                open Classical

variable (p q r : Prop)

declaration uses `sorry`example : (p → q ∨ r) → ((p → q) ∨ (p → r)) := sorry
declaration uses `sorry`example : ¬(p ∧ q) → ¬p ∨ ¬q := sorry
declaration uses `sorry`example : ¬(p → q) → p ∧ ¬q := sorry
declaration uses `sorry`example : (p → q) → (¬p ∨ q) := sorry
declaration uses `sorry`example : (¬q → ¬p) → (p → q) := sorry
declaration uses `sorry`example : p ∨ ¬p := sorry
declaration uses `sorry`example : (((p → q) → p) → p) := sorry

고전 논리를 사용하지 않고 ¬(p ↔ ¬p)를 증명하십시오.