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를 함의의 개념으로 사용할 수 있습니다.

이것이 구성 계산법이 따르는 접근 방식이며, 따라서 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(에 대응하는 타입)가 거주되어 있다고 합시다. 마침 함수 적용과 추상화 규칙을 이용하면 Prop의 어떤 원소가 거주되어 있는지 편리하게 추적할 수 있습니다. 따라서 원소 t : p를 구성하면 p가 실제로 참이라는 것을 알 수 있습니다. p의 거주자를 “p가 참이라는 사실”로 생각할 수 있습니다. p → q의 증명은 “p가 참이라는 사실”을 사용하여 “q가 참이라는 사실”을 얻습니다.

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

앞서 제안한 명제-타입 대응 패러다임에 대한 두 가지 사고방식은 근본적으로 다릅니다. 구성적 관점에서 보면, 증명은 의존 타입 이론의 적절한 표현식이 나타내는 추상적인 수학적 대상입니다. 반면, 위에서 설명한 코딩 기법의 관점에서 생각한다면, 표현식(항) 자체는 아무런 흥미로운 것도 나타내지 않습니다. 오히려 해당 명제가 참임을 보장하는 것은 우리가 그 표현식을 적어 내려가고 그것이 올바른 타입을 갖는지 검사할 수 있다는 사실입니다. 다시 말해, 표현식 그 자체가 증명입니다.

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

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

3.2. 명제를 타입으로 다루기🔗

명제-타입 대응 패러다임에서 →만 포함하는 정리는 람다 추상화와 적용을 사용하여 증명할 수 있습니다. 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

“공리” 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의 “커리된” 형태일 뿐입니다.

지난 장에서 우리는 람다 추상화를 →에 대한 “도입 규칙”으로 볼 수 있음을 살펴보았습니다. 지금의 맥락에서 람다 추상화는 함의를 “도입”하는 방법, 곧 함의를 성립시키는 방법을 보여 줍니다. 적용은 증명에서 함의를 어떻게 "제거"하는지, 즉 사용하는지를 보여 주는 "제거 규칙"으로 볼 수 있습니다. 그 밖의 명제 연결사들은 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-introduction)과 논리곱 제거(and-elimination)가 데카르트 곱의 쌍 만들기 및 사영 연산과 비슷하다는 점에 주목하십시오. 차이점은 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가 그 예입니다. 원소를 구성하는 표준적인 방법은 적절한 인수 hp : p와 hq : q에 And.intro를 적용하는 것입니다. 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-도입(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로부터 r이 따라 나오고 q로부터도 r이 따라 나온다는 것을 보임으로써 p ∨ q로부터 r을 증명할 수 있다는 것입니다. 다시 말해, 이것은 경우에 따른 증명입니다. 표현식 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.inr과 Or.inl을 제공하며, 이들은 Or.intro_right _와 Or.intro_left _의 축약형으로 볼 수 있습니다. 따라서 위의 증명 항은 다음과 같이 더 간결하게 쓸 수 있습니다:

                  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. 고전 논리🔗

지금까지 살펴본 도입 규칙과 제거 규칙은 모두 구성적입니다. 즉, 이 규칙들은 명제-타입 대응에 기반하여 논리 연결사를 계산적으로 이해하는 방식을 반영합니다. 일반적인 고전 논리는 여기에 배중률 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에 근거하여 정당화할 수 있는 추가적인 증명 패턴도 쓸 수 있습니다. 예를 들어, 경우에 따른 증명을 수행할 수 있습니다:

                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이 이를 시도했는데 실패하면 “don't know how to synthesize placeholder”(자리 표시자를 합성하는 방법을 모릅니다)라는 오류 메시지를 반환합니다. 이어서 기대하는 항의 타입과 컨텍스트에서 사용할 수 있는 모든 객체와 가설을 함께 보여 줍니다. 다시 말해, 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)를 증명하십시오.