막간: 명제, 증명, 그리고 인덱싱🔗

많은 언어들이 그렇듯, Lean은 배열과 리스트의 인덱싱에 대괄호를 사용합니다. 예를 들어 woodlandCritters가 다음과 같이 정의되었다면:

def woodlandCritters : List String :=
  ["hedgehog", "deer", "snail"]

그러면 각 구성 요소를 추출할 수 있습니다:

def hedgehog := woodlandCritters[0]
def deer := woodlandCritters[1]
def snail := woodlandCritters[2]

하지만 네 번째 원소를 추출하려고 시도하면 런타임 오류가 아니라 컴파일 타임 오류가 발생합니다:

def oops := failed to prove index is valid, possible solutions:
  - Use `have`-expressions to prove the index is valid
  - Use `a[i]!` notation instead, runtime check is performed, and 'Panic' error message is produced if index is not valid
  - Use `a[i]?` notation instead, result is an `Option` type
  - Use `a[i]'h` notation instead, where `h` is a proof that index is valid
⊢ 3 < woodlandCritters.lengthwoodlandCritters[3]

failed to prove index is valid, possible solutions:
  - Use `have`-expressions to prove the index is valid
  - Use `a[i]!` notation instead, runtime check is performed, and 'Panic' error message is produced if index is not valid
  - Use `a[i]?` notation instead, result is an `Option` type
  - Use `a[i]'h` notation instead, where `h` is a proof that index is valid
⊢ 3 < woodlandCritters.length

이 오류 메시지는 Lean이 3 < woodlandCritters.length(즉 3 < List.length woodlandCritters)라는 것을 자동으로 수학적으로 증명하려 시도했다는 뜻입니다. 이것이 성립하면 조회가 안전함을 의미하겠지만, Lean은 이를 증명할 수 없었습니다. 범위를 벗어난 오류는 흔한 종류의 버그이며, Lean은 프로그래밍 언어이자 정리 증명기라는 이중적 본성을 활용하여 이를 최대한 많이 배제합니다.

이것이 어떻게 작동하는지 이해하려면 명제, 증명, 택틱이라는 세 가지 핵심 개념에 대한 이해가 필요합니다.

명제와 증명🔗

명제는 참이거나 거짓일 수 있는 진술입니다. 다음 영어 문장은 모두 명제입니다:

1 + 1 = 2
덧셈은 교환 법칙이 성립합니다.
소수는 무한히 많습니다.
1 + 1 = 15
파리는 프랑스의 수도입니다.
부에노스아이레스는 대한민국의 수도입니다.
모든 새는 날 수 있습니다.

반면, 무의미한 문장은 명제가 아닙니다. 문법적으로는 옳지만, 다음 중 어느 것도 명제가 아닙니다:

1 + green = ice cream
모든 수도는 소수입니다.
적어도 하나의 gorg는 fleep입니다.

명제에는 두 종류가 있습니다: 오직 개념에 대한 정의에만 의존하는 순수하게 수학적인 명제와, 세계에 대한 사실인 명제입니다. Lean과 같은 정리 증명기는 전자의 범주에 관심을 두며, 펭귄의 비행 능력이나 도시의 법적 지위에 대해서는 아무런 언급도 하지 않습니다.

증명은 명제가 참임을 설득력 있게 보여주는 논증입니다. 수학적 명제의 경우, 이러한 논증은 관련된 개념들의 정의뿐만 아니라 논리적 논증의 규칙도 활용합니다. 대부분의 증명은 사람이 이해할 수 있도록 작성되며, 지루한 세부 사항은 대부분 생략합니다. Lean과 같은 컴퓨터 보조 정리 증명기는 수학자가 많은 세부 사항을 생략한 채 증명을 작성할 수 있도록 설계되었으며, 누락된 명시적 단계를 채우는 것은 소프트웨어의 책임입니다. 이 단계들은 기계적으로 검사할 수 있습니다. 이는 실수나 누락의 가능성을 줄여줍니다.

Lean에서 프로그램의 타입은 해당 프로그램과 상호작용할 수 있는 방식을 설명합니다. 예를 들어, Nat → List String 타입의 프로그램은 Nat 인자를 받아 문자열 리스트를 산출하는 함수입니다. 다시 말해, 각 타입은 해당 타입을 가지는 프로그램으로 무엇이 인정되는지를 명시합니다.

Lean에서 명제는 사실상 타입입니다. 이는 해당 명제가 참임을 뒷받침하는 증거로 인정되는 것이 무엇인지를 명시합니다. 명제는 이 증거를 제시함으로써 증명되며, 이는 Lean에 의해 검사됩니다. 반면, 그 명제가 거짓이라면 이 증거를 구성하는 것은 불가능할 것입니다.

예를 들어, 명제 1 + 1 = 2는 Lean에서 직접 작성할 수 있습니다. 이 명제의 증거는 생성자 rfl이며, 이는 reflexivity(반사성)의 줄임말입니다. 수학에서 어떤 관계가 반사적이라는 것은 모든 원소가 자기 자신과 관계를 맺는다는 뜻이며, 이는 타당한 동등성 개념을 갖기 위한 기본 요구 사항입니다. 1 + 1은 2로 계산되므로, 둘은 실제로 같은 것입니다:

Definition `onePlusOneIsTwo` is a proposition; use `theorem` instead of `def`

Note: This linter can be disabled with `set_option linter.defProp false`def onePlusOneIsTwo : 1 + 1 = 2 := rfl

반면에, rfl은 거짓 명제 1 + 1 = 15를 증명하지 않습니다:

def Not a definitional equality: the left-hand side
  1 + 1
is not definitionally equal to the right-hand side
  15onePlusOneIsFifteen : 1 + 1 = 15 := Type mismatch
  rfl
has type
  ?m.16 = ?m.16
but is expected to have type
  1 + 1 = 15rfl

Type mismatch
  rfl
has type
  ?m.16 = ?m.16
but is expected to have type
  1 + 1 = 15

이 오류 메시지는 등식 양변이 이미 같은 숫자일 때 rfl이 두 식이 같음을 증명할 수 있음을 나타냅니다. 1 + 1은 2로 직접 계산되므로 둘은 같은 것으로 간주되며, 이로 인해 onePlusOneIsTwo가 받아들여질 수 있습니다. Type이 데이터 구조와 함수를 나타내는 Nat, String, List (Nat × String × (Int → Float))와 같은 타입들을 서술하는 것처럼, Prop은 명제를 서술합니다.

명제가 증명되면 이를 theorem(정리)이라고 합니다. Lean에서는 정리를 선언할 때 def 대신 theorem 키워드를 사용하는 것이 관례입니다. 이는 독자가 어떤 선언이 수학적 증명으로 읽히도록 의도된 것이고 어떤 선언이 정의인지 구분하는 데 도움이 됩니다. 일반적으로 말해서, 증명에서 중요한 것은 명제가 참임을 뒷받침하는 근거가 존재한다는 사실이지, 어떤 근거가 제시되었는지는 그다지 중요하지 않습니다. 반면 정의에서는 어떤 특정 값이 선택되는지가 매우 중요합니다—결국, 항상 0을 반환하는 덧셈의 정의는 명백히 잘못된 것입니다. 증명의 세부 사항은 이후의 증명들에 영향을 미치지 않기 때문에, theorem 키워드를 사용하면 Lean 컴파일러에서 더 높은 수준의 병렬성을 활용할 수 있습니다.

앞선 예제는 다음과 같이 다시 작성할 수 있습니다.

def OnePlusOneIsTwo : Prop := 1 + 1 = 2

theorem onePlusOneIsTwo : OnePlusOneIsTwo := rfl

택틱🔗

증명은 보통 근거를 직접 제공하기보다는 택틱을 사용하여 작성됩니다. 택틱은 명제에 대한 증거를 구성하는 작은 프로그램입니다. 이 프로그램은 증명해야 할 명제(목표라고 부릅니다)와 이를 증명하는 데 사용할 수 있는 가정을 함께 추적하는 증명 상태에서 실행됩니다. 목표에 대해 택틱을 실행하면 새로운 목표를 포함하는 새로운 증명 상태가 생성됩니다. 모든 목표가 증명되었을 때 증명이 완료됩니다.

택틱으로 증명을 작성하려면 정의를 by로 시작하십시오. by를 작성하면 다음 들여쓰기 블록이 끝날 때까지 Lean을 택틱 모드로 전환합니다. 택틱 모드에 있는 동안, Lean은 현재 증명 상태에 대한 지속적인 피드백을 제공합니다. 택틱으로 작성하면, onePlusOneIsTwo는 여전히 상당히 짧습니다:

theorem onePlusOneIsTwo : 1 + 1 = 2 := by⊢ 1 + 1 = 2
  decideAll goals completed! 🐙

decide 택틱은 결정 절차를 호출하는데, 이는 명제가 참인지 거짓인지 검사하여 어느 경우든 적절한 증명을 반환할 수 있는 프로그램입니다. 이는 주로 1과 2와 같은 구체적인 값을 다룰 때 사용됩니다. 이 책에서 다루는 그 밖의 중요한 택틱으로는 “simplify”의 줄임말인 simp와, 여러 정리를 자동으로 증명할 수 있는 grind가 있습니다.

택틱은 여러 가지 이유로 유용합니다:

많은 증명은 아주 세세한 부분까지 다 작성하면 복잡하고 지루해지는데, 택틱은 이런 흥미롭지 않은 부분들을 자동화할 수 있습니다.
택틱으로 작성된 증명은 유연한 자동화가 정의의 작은 변경 사항을 감추어 줄 수 있기 때문에 시간이 지나도 유지 관리하기가 더 쉽습니다.
하나의 택틱이 여러 다른 정리를 증명할 수 있기 때문에, Lean은 사용자가 직접 증명을 작성하지 않아도 되도록 배후에서 택틱을 사용할 수 있습니다. 예를 들어, 배열 조회에는 인덱스가 범위 내에 있다는 증명이 필요한데, 택틱은 일반적으로 사용자가 이를 신경 쓸 필요 없이 그 증명을 구성할 수 있습니다.

내부적으로 인덱싱 표기법은 택틱을 사용하여 사용자의 조회 연산이 안전함을 증명합니다. 이 택틱은 산술에 관한 여러 사실을 고려하며, 이를 지역적으로 알려진 사실들과 결합하여 인덱스가 범위 내에 있음을 증명하려고 시도합니다.

simp 택틱은 Lean 증명의 주력입니다. 이는 목표를 가능한 한 단순한 형태로 재작성합니다. 많은 경우, 이러한 재작성은 명제를 크게 단순화하여 자동으로 증명될 수 있게 만듭니다. 뒤에서는 상세한 형식적 증명이 구성되지만, simp 택틱을 사용하면 이러한 복잡성이 감춰집니다.

decide와 마찬가지로, grind 택틱은 증명을 완료하는 데 사용됩니다. 이 택틱은 SMT 솔버에서 사용되는 여러 기법을 조합하여 다양한 정리를 증명할 수 있습니다. simp와 달리, grind 택틱은 증명을 완전히 끝내지 않고서는 결코 진전을 이룰 수 없습니다. 즉, 완전히 성공하거나 실패하거나 둘 중 하나입니다. grind 택틱은 매우 강력하며 커스터마이즈 및 확장이 가능합니다. 이러한 힘과 유연성 때문에, 정리 증명에 실패했을 때의 출력에는 숙련된 Lean 사용자가 실패 원인을 진단하는 데 도움이 될 수 있는 많은 정보가 담겨 있습니다. 이는 처음에는 압도적으로 느껴질 수 있으므로, 이 장에서는 decide와 simp 택틱만 사용합니다.

논리 연결사🔗

"그리고", "또는", "참", "거짓", "아님"과 같은 논리의 기본 구성 요소를 논리 연결사라고 합니다. 각 연결사는 그 참임을 나타내는 증거가 무엇인지를 정의합니다. 예를 들어, “A이고 B이다”라는 명제를 증명하려면 A와 B를 모두 증명해야 합니다. 즉, "A이고 B"에 대한 근거는 A에 대한 근거와 B에 대한 근거를 모두 포함하는 쌍이라는 것을 의미합니다. 마찬가지로, "A 또는 B"에 대한 증거는 A에 대한 증거이거나 B에 대한 증거로 구성됩니다.

특히 이러한 연결사 대부분은 데이터 타입처럼 정의되며, 생성자를 가지고 있습니다. A와 B가 명제라면, “A 그리고 B”(A ∧ B라고 씀)는 명제입니다. A ∧ B에 대한 증거는 생성자 And.intro로 구성되며, 이 생성자는 A → B → A ∧ B 타입을 가집니다. A와 B를 구체적인 명제로 바꾸면, And.intro rfl rfl로 1 + 1 = 2 ∧ "Str".append "ing" = "String"을 증명할 수 있습니다. 물론 decide도 이 증명을 찾을 만큼 충분히 강력합니다:

theorem addAndAppend : 1 + 1 = 2 ∧ "Str".append "ing" = "String" := by⊢ 1 + 1 = 2 ∧ "Str".append "ing" = "String"
  decideAll goals completed! 🐙

마찬가지로, “A 또는 B”(A ∨ B로 표기)는 생성자가 두 개 있습니다. 이는 “A 또는 B”의 증명이 기저의 두 명제 중 하나만 참이면 되기 때문입니다. 생성자는 두 개가 있습니다. 타입이 A → A ∨ B인 Or.inl과, 타입이 B → A ∨ B인 Or.inr입니다.

함의(만약 A이면 B)는 함수를 사용하여 표현됩니다. 특히, A에 대한 증거를 B에 대한 증거로 변환하는 함수는 그 자체로 A가 B를 함의한다는 증거입니다. 이는 A → B가 ¬A ∨ B의 축약형인 함의에 대한 일반적인 설명과는 다르지만, 두 공식화는 동등합니다.

"그리고(and)"에 대한 증거는 생성자이므로, 패턴 매칭에 사용할 수 있습니다. 예를 들어, A와 B가 A 또는 B를 함의한다는 증명은, A와 B에 대한 증거로부터 A(또는 B)의 증거를 꺼낸 다음, 이 증거를 사용하여 A 또는 B의 증거를 만들어 내는 함수입니다:

theorem andImpliesOr : A ∧ B → A ∨ B :=
  fun andEvidence =>
    match andEvidence with
    | And.intro a b => Or.inl a

논리 연결사	Lean 구문	증거
참	`True`	`True.intro : True`
False	`False`	증거 없음
`A`와 `B`	`A ∧ B`	`And.intro : A → B → A ∧ B`
`A` 또는 `B`	`A ∨ B`	`Or.inl : A → A ∨ B` 또는 `Or.inr : B → A ∨ B` 중 하나
`A`는 `B`를 함의합니다	`A → B`	`A`의 증거를 `B`의 증거로 변환하는 함수입니다
not `A`	`¬A`	`A`의 증거를 `False`의 증거로 변환하는 함수

decide 택틱은 이러한 연결사를 사용하는 정리를 증명할 수 있습니다. 예를 들어:

theorem onePlusOneOrLessThan : 1 + 1 = 2 ∨ 3 < 5 := by⊢ 1 + 1 = 2 ∨ 3 < 5 decideAll goals completed! 🐙
theorem notTwoEqualFive : ¬(1 + 1 = 5) := by⊢ ¬1 + 1 = 5 decideAll goals completed! 🐙
theorem trueIsTrue : True := by⊢ True decideAll goals completed! 🐙
theorem trueOrFalse : True ∨ False := by⊢ True ∨ False decideAll goals completed! 🐙
theorem falseImpliesTrue : False → True := by⊢ False → True decideAll goals completed! 🐙

논거로서의 증거🔗

어떤 경우에는 리스트에 안전하게 인덱싱하려면 리스트가 최소 크기를 가져야 하지만, 리스트 자체는 구체적인 값이 아니라 변수인 경우가 있습니다. 이 조회가 안전하려면 리스트가 충분히 길다는 증거가 있어야 합니다. 인덱싱을 안전하게 만드는 가장 쉬운 방법 중 하나는, 자료 구조를 조회하는 함수가 안전성에 대해 필요한 증거를 인자로 받도록 하는 것입니다. 예를 들어, 리스트의 세 번째 항목을 반환하는 함수는 일반적으로 안전하지 않은데, 리스트에는 0개, 1개, 또는 2개의 항목만 있을 수도 있기 때문입니다:

def third (xs : List α) : α := failed to prove index is valid, possible solutions:
  - Use `have`-expressions to prove the index is valid
  - Use `a[i]!` notation instead, runtime check is performed, and 'Panic' error message is produced if index is not valid
  - Use `a[i]?` notation instead, result is an `Option` type
  - Use `a[i]'h` notation instead, where `h` is a proof that index is valid
α:Type ?u.3xs:List α⊢ 2 < xs.lengthxs[2]

failed to prove index is valid, possible solutions:
  - Use `have`-expressions to prove the index is valid
  - Use `a[i]!` notation instead, runtime check is performed, and 'Panic' error message is produced if index is not valid
  - Use `a[i]?` notation instead, result is an `Option` type
  - Use `a[i]'h` notation instead, where `h` is a proof that index is valid
α:Type ?u.3xs:List α⊢ 2 < xs.length

하지만 리스트에 최소 세 개의 항목이 있음을 보여야 하는 의무는, 인덱싱 연산이 안전하다는 증거로 이루어진 인자를 추가함으로써 호출자에게 부과할 수 있습니다.

def third (xs : List α) (ok : xs.length > 2) : α := xs[2]

이 예시에서 xs.length > 2는 xs가 2개보다 많은 항목을 갖고 있는지를 검사하는 프로그램이 아닙니다. 이는 참이거나 거짓일 수 있는 명제이며, 인자 ok는 그것이 참이라는 증거여야 합니다.

함수가 구체적인 리스트에 대해 호출되면, 그 리스트의 길이는 알려져 있습니다. 이런 경우, by decide가 자동으로 증거를 구성할 수 있습니다:

"snail"#eval third woodlandCritters (by⊢ woodlandCritters.length > 2 decideAll goals completed! 🐙)

"snail"

증거 없는 인덱싱🔗

인덱싱 연산이 범위 내에 있음을 증명하는 것이 실용적이지 않은 경우, 다른 대안들이 있습니다. 물음표를 추가하면 Option이 결과로 나오는데, 인덱스가 범위 안에 있으면 some이, 그렇지 않으면 none이 됩니다. 예를 들어:

def thirdOption (xs : List α) : Option α := xs[2]?some "snail"#eval thirdOption woodlandCritters

some "snail"

none#eval thirdOption ["only", "two"]

none

인덱스가 범위를 벗어났을 때 Option을 반환하는 대신 프로그램을 크래시시키는 버전도 있습니다:

"deer"#eval woodlandCritters[1]!

"deer"

만날 수 있는 메시지들🔗

어떤 명제가 참임을 증명하는 것 외에도, decide 택틱은 그것이 거짓임을 증명할 수도 있습니다. 원소가 하나뿐인 리스트가 원소를 두 개 넘게 갖는다는 것을 증명하라고 요청하면, 해당 명제가 실제로 거짓임을 나타내는 오류를 반환합니다:

#eval third ["rabbit"] (by⊢ ["rabbit"].length > 2 Tactic `decide` proved that the proposition
  ["rabbit"].length > 2
is falsedecide⊢ ["rabbit"].length > 2)

Tactic `decide` proved that the proposition
  ["rabbit"].length > 2
is false

simp와 decide 택틱은 def로 작성된 정의를 자동으로 펼치지 않습니다. OnePlusOneIsTwo를 simp를 사용해 증명하려고 하면 실패합니다:

theorem onePlusOneIsStillTwo : OnePlusOneIsTwo := by⊢ OnePlusOneIsTwo `simp` made no progresssimp⊢ OnePlusOneIsTwo

오류 메시지는 단순히 아무것도 할 수 없었다고 알립니다. OnePlusOneIsTwo를 펼치지 않고서는 아무런 진전도 이룰 수 없기 때문입니다:

`simp` made no progress

decide를 사용해도 실패합니다:

theorem onePlusOneIsStillTwo : OnePlusOneIsTwo := by⊢ OnePlusOneIsTwo failed to synthesize
  Decidable OnePlusOneIsTwo

Hint: Additional diagnostic information may be available using the `set_option diagnostics true` command.decide⊢ OnePlusOneIsTwo

이는 또한 OnePlusOneIsTwo를 펼치지 않기 때문이기도 합니다:

failed to synthesize
  Decidable OnePlusOneIsTwo

Hint: Additional diagnostic information may be available using the `set_option diagnostics true` command.

OnePlusOneIsTwo를 abbrev로 정의하면 문제가 해결되는데, 이는 정의를 펼침 대상으로 표시하기 때문입니다.

Lean이 인덱싱 연산이 안전하다는 컴파일 시점 증거를 찾지 못했을 때 발생하는 오류 외에도, 안전하지 않은 인덱싱을 사용하는 다형 함수는 다음과 같은 메시지를 낼 수 있습니다:

def unsafeThird (xs : List α) : α := failed to synthesize instance of type class
  Inhabited α

Hint: Type class instance resolution failures can be inspected with the `set_option trace.Meta.synthInstance true` command.xs[2]!

failed to synthesize instance of type class
  Inhabited α

Hint: Type class instance resolution failures can be inspected with the `set_option trace.Meta.synthInstance true` command.

이는 Lean을 정리 증명을 위한 논리이자 프로그래밍 언어로서 모두 사용 가능하게 유지하는 것의 일부인 기술적 제약 때문입니다. 특히, 타입에 값이 하나 이상 포함된 프로그램만이 크래시가 허용됩니다. 이는 Lean에서 명제란 그 참임을 나타내는 증거를 분류하는 일종의 타입이기 때문입니다. 거짓 명제에는 그러한 증거가 없습니다. 만약 빈 타입을 가진 프로그램이 크래시될 수 있다면, 그 크래시되는 프로그램은 거짓 명제에 대한 일종의 가짜 증거로 사용될 수 있습니다.

내부적으로 Lean은 적어도 하나의 값을 가지는 것으로 알려진 타입들의 테이블을 포함합니다. 이 오류는 임의의 타입 α가 반드시 그 표에 있는 것은 아니라는 것을 의미합니다. 다음 장에서는 이 표에 항목을 추가하는 방법과, unsafeThird와 같은 함수를 성공적으로 작성하는 방법을 설명합니다.

목록과 조회에 사용되는 대괄호 사이에 공백을 추가하면 다른 메시지가 발생할 수 있습니다:

#eval Function expected at
  woodlandCritters
but this term has type
  List String

Note: Expected a function because this term is being applied to the argument
  [1]woodlandCritters [1]

Function expected at
  woodlandCritters
but this term has type
  List String

Note: Expected a function because this term is being applied to the argument
  [1]

공백을 추가하면 Lean은 이 표현식을 함수 적용으로 취급하고, 인덱스를 단일 숫자를 포함하는 리스트로 취급합니다. 이 오류 메시지는 Lean이 woodlandCritters를 함수로 취급하려 시도한 결과로 발생합니다.

연습 문제🔗

다음 정리들을 rfl을 사용하여 증명하십시오: 2 + 3 = 5, 15 - 8 = 7, "Hello, ".append "world" = "Hello, world". 5 < 18을 증명하는 데 rfl을 사용하면 어떻게 됩니까? 그 이유는 무엇입니까?
by decide를 사용하여 다음 정리를 증명하십시오: 2 + 3 = 5, 15 - 8 = 7, "Hello, ".append "world" = "Hello, world", 5 < 18.
리스트에서 다섯 번째 항목을 조회하는 함수를 작성하십시오. 이 조회가 안전하다는 증거를 함수의 인자로 전달하십시오.