Propositions and Proofs🔗

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

• 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에 직접 쓸 수 있다. 이 명제의 증거는 반사성(reflexivity)의 줄임말인 rfl 생성자다. 수학에서 모든 원소가 자기 자신과 관계를 맺으면 관계가 반사적이라고 한다. 이는 타당한 동등성 개념을 갖기 위한 기본 요구 사항이다. 1 + 1은 2로 계산되므로 실제로 같은 것이다.

반면 rfl은 거짓 명제 1 + 1 = 15를 증명하지 못한다.

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은 명제를 설명한다.

명제가 증명되면 이를 정리라고 부른다. Lean에서는 정리를 def 대신 theorem 키워드로 선언하는 것이 관례다. 이렇게 하면 독자가 어떤 선언을 수학적 증명으로 읽어야 하고 어떤 선언을 정의로 읽어야 하는지 알 수 있다. 일반적으로 증명에서는 명제가 참이라는 증거가 있다는 점이 중요하고, 어떤 증거를 제공했는지는 특별히 중요하지 않다. 반면 정의에서는 어떤 특정 값을 선택하는지가 매우 중요하다. 항상 0을 반환하는 덧셈 정의는 분명히 잘못되었기 때문이다. 증명의 세부 사항은 이후 증명에 중요하지 않으므로 theorem 키워드를 사용하면 Lean 컴파일러가 더 큰 병렬성을 활용할 수 있다.

앞의 예제는 다음과 같이 다시 쓸 수 있다.

Tactics🔗

증명은 보통 증거를 직접 제공하기보다 전술을 사용해 작성한다. 전술은 명제의 증거를 구성하는 작은 프로그램이다. 이 프로그램은 증명할 문장(목표라고 부른다)과 이를 증명하는 데 사용할 수 있는 가정을 추적하는 증명 상태에서 실행된다. 목표에 전술을 실행하면 새로운 목표가 들어 있는 새 증명 상태가 나온다. 모든 목표가 증명되면 증명이 완성된다.

전술로 증명을 작성하려면 정의를 by로 시작하라. by를 쓰면 Lean은 다음 들여쓰기 블록이 끝날 때까지 전술 모드로 들어간다. 전술 모드에서 Lean은 현재 증명 상태에 관한 피드백을 계속 제공한다. 전술로 작성한 onePlusOneIsTwo는 여전히 매우 짧다.

decide 전술은 문장이 참인지 거짓인지 검사하고 어느 경우든 적절한 증명을 반환하는 프로그램인 결정 절차를 호출한다. 주로 1, 2 같은 구체적인 값을 다룰 때 사용한다. 이 책의 다른 중요한 전술은 “단순화”를 뜻하는 simp와 많은 정리를 자동으로 증명할 수 있는 grind다.

전술은 여러 이유로 유용하다.

1. 많은 증명은 가장 작은 세부 사항까지 직접 쓰면 복잡하고 지루하지만, 전술은 이런 흥미롭지 않은 부분을 자동화할 수 있다.

2. 유연한 자동화가 정의의 작은 변경을 가려 줄 수 있으므로 전술로 작성한 증명은 시간이 지나도 유지하기 쉽다.

3. 하나의 전술로 여러 정리를 증명할 수 있으므로 Lean은 내부적으로 전술을 사용해 사용자가 손으로 증명을 작성하지 않아도 되게 한다. 예를 들어 배열 조회에는 인덱스가 범위 안에 있다는 증명이 필요하지만, 전술은 보통 사용자가 신경 쓰지 않아도 그 증명을 구성할 수 있다.

내부적으로 인덱싱 표기법은 전술을 사용해 사용자의 조회 연산이 안전함을 증명한다. 이 전술은 산술에 관한 많은 사실을 고려하고 현재 범위에서 알려진 사실과 결합해 인덱스가 범위 안에 있음을 증명하려 한다.

simp 전술은 Lean 증명의 일꾼이다. 목표를 가능한 한 단순한 형태로 다시 쓴다. 많은 경우 이렇게 다시 쓰면 문장이 충분히 단순해져 자동으로 증명할 수 있다. 내부적으로는 자세한 형식 증명이 구성되지만 simp를 사용하면 이 복잡성이 가려진다.

decide처럼 grind 전술은 증명을 마무리하는 데 사용한다. 다양한 정리를 증명할 수 있는 SMT 솔버의 기법 모음을 사용한다. simp와 달리 grind는 증명을 완전히 끝내지 않고는 증명을 향해 조금도 나아갈 수 없으며, 완전히 성공하거나 실패한다. grind 전술은 매우 강력하고 사용자화할 수 있으며 확장 가능하다. 이 힘과 유연성 때문에 정리를 증명하지 못했을 때의 출력에는 숙련된 Lean 사용자가 실패 이유를 진단하는 데 도움이 되는 정보가 많이 담긴다. 이는 처음에는 벅찰 수 있으므로 이 장에서는 decide와 simp만 사용한다.

Connectives🔗

“그리고”, “또는”, “참”, “거짓”, “아니다”와 같은 논리의 기본 구성 요소를 논리 연결사라고 한다. 각 연결사는 그 연결사가 참이라는 증거로 인정되는 것을 정의한다. 예를 들어 “A 그리고 B”라는 문장을 증명하려면 A와 B를 모두 증명해야 한다. 따라서 “A 그리고 B”의 증거는 A의 증거와 B의 증거를 모두 담은 쌍이다. 마찬가지로 “A 또는 B”의 증거는 A의 증거나 B의 증거 중 하나다.

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

마찬가지로 “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의 줄임말로 보는 일반적인 설명과 다르지만 두 표현은 동등하다.

“그리고”의 증거는 생성자이므로 패턴 매칭과 함께 사용할 수 있다. 예를 들어 A 그리고 B가 A 또는 B를 함의한다는 증명은, A 그리고 B의 증거에서 A의 증거(또는 B의 증거)를 꺼내 그 증거로 A 또는 B의 증거를 만드는 함수다.

decide 전술은 이러한 연결사를 사용하는 정리를 증명할 수 있다. 예를 들어 다음과 같다.

Evidence as Arguments🔗

어떤 경우에는 목록을 안전하게 인덱싱하려면 목록에 최소 크기가 있어야 하지만 목록 자체는 구체적인 값이 아니라 변수다. 이 조회가 안전하려면 목록이 충분히 길다는 증거가 있어야 한다. 인덱싱을 안전하게 만드는 가장 쉬운 방법 중 하나는 자료구조를 조회하는 함수가 안전성에 필요한 증거를 인수로 받게 하는 것이다. 예를 들어 목록의 세 번째 항목을 반환하는 함수는 목록에 원소가 0개, 1개, 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

하지만 인덱싱 연산이 안전하다는 증거로 이루어진 인수를 추가하면 목록에 항목이 적어도 세 개 있음을 보이는 의무를 호출자에게 부과할 수 있다.

이 예제에서 xs.length > 2는 xs에 항목이 2개보다 많은지 검사하는 프로그램이 아니다. 참일 수도 거짓일 수도 있는 명제이며, ok 인수는 이 명제가 참이라는 증거여야 한다.

함수를 구체적인 목록에 호출하면 목록의 길이를 안다. 이 경우 by decide가 증거를 자동으로 구성할 수 있다.

"snail"

Indexing Without Evidence🔗

인덱싱 연산이 범위 안에 있음을 증명하기가 현실적이지 않은 경우에는 다른 방법이 있다. 물음표를 붙이면 Option이 되며, 인덱스가 범위 안이면 결과는 some이고 그렇지 않으면 none이다. 예를 들어 다음과 같다.

some "snail"

none

"deer"

Messages You May Meet🔗

decide 전술은 문장이 참임을 증명할 뿐 아니라 거짓임도 증명할 수 있다. 원소가 하나인 목록에 원소가 두 개보다 많다고 증명하라고 하면, 문장이 실제로 거짓임을 나타내는 오류를 반환한다.

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

simp와 decide 전술은 def로 정의한 것을 자동으로 펼치지 않는다. simp를 사용해 OnePlusOneIsTwo를 증명하려 하면 실패한다.

오류 메시지는 OnePlusOneIsTwo를 펼치지 않으면 진전할 수 없으므로 아무것도 할 수 없다고 단순히 말한다.

`simp` made no progress

decide를 사용해도 실패한다.

이 역시 OnePlusOneIsTwo를 펼치지 않기 때문이다.

failed to synthesize
  Decidable OnePlusOneIsTwo

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

abbrev로 OnePlusOneIsTwo를 정의하면 펼칠 정의로 표시되므로 문제가 해결된다.

인덱싱 연산이 안전하다는 컴파일 타임 증거를 Lean이 찾지 못할 때 발생하는 오류 외에도, 안전하지 않은 인덱싱을 사용하는 다형 함수는 다음 메시지를 낼 수 있다.

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 같은 함수를 성공적으로 작성하는 방법을 설명한다.

목록과 조회에 사용하는 대괄호 사이에 공백을 넣으면 또 다른 메시지가 나올 수 있다.

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를 함수로 취급하려 하기 때문에 나온다.