계정: 로그인
AA 📝
Coq /
입문서

2003년 초에 한국어로 번역한 증명 보조 도구 Coq의 입문서입니다. Gérard Huet과 Gilles Kahn, Christine Paulin-Mohring이 쓴 영어 원문의 제목은 “The Coq Proof Assistant: A Tutorial”이며, 저작권은 INRIA에 있습니다. 원 저작권 문구에 번역에 관한 세부 사항이 없기에 이 번역문의 저작권도 정해진 바 없으며, 만일 저작권 상의 문제가 발생하면 이 문서는 온라인 상에서 사라지게됩니다.

Version 7.31

Gérard Huet, Gilles Kahn and Christine Paulin-Mohring

LogiCal Project

V7.3, (c) INRIA 1999–2002

시작하며

Coq은 Calculus of Inductive Constructions라고 알려진 논리적 프레임워크를 위한 증명 보조기(proof assistant)입니다. 대화식으로 정형적 증명을 만들 수 있으며, 모순 없이 명세 그대로의 함수형 프로그램을 만들 수도 있습니다. Coq은 수많은 아키텍쳐 상에서 컴퓨터 프로그램으로서 수행되며, 특히 UNIX 기계상에서 작동합니다. 다양한 사용자 인터페이스를 제공합니다. 현재 문서는 Coq으로 가능한 모든 영역을 다 보여주지는 않을 것입니다. 대신, 정형적 공리를 개발하는 기본 명세 언어 Gallina와 메인 증명 도구에 대한 초보적인 입문서가 될 것입니다.

사용자가 자신의 워크스테이션에 Coq을 설치했고 표준 문자입출력 쉘에서 Coq을 호출하며, 이 때 Emacs나 Centaur 같은 특별한 인터페이스는 사용하지 않는다고 가정하겠습니다. 설치 안내문이나 더 상세한 문서는 Coq 표준 배포본에 들어있으며, 익명 FTP 사이트 ftp.inria.frINRIA/coq/V7.3 디렉토리에서 찾으실 수 있습니다.

지금부터, 프롬프트 Coq <  뒤에 따라 나오는 모든 예문들은 사용자의 입력을 의미하며 마침표로 끝납니다. 그 아래에 나오는 줄들은 대체로 Coq의 응답을 사용자 화면에 보이는 대로 나타내는 부분입니다. 이런 예제들은 특별히 따로 언급하지 않는 한 올바른 Coq 세션입니다. 이 입문서는 Linux로 운영하는 PC 워크스테이션에서 만들었습니다. 표준적인 방법으로 Coq를 시동하면 다음과 같은 메세지가 나타납니다:

user@host:~> coqtop
Welcome to Coq 7.3 (May 2002)

Coq <

첫번째 줄에는 현재 사용중인 Coq의 정확한 버전을 나타내는 배너가 표시됩니다. 저희 핫라인 <coq@pauillac.inria.fr>로 오류를 보고할 때에는 반드시 이 배너를 함께 보내주셔야 합니다.

제 1 장 : 술어 논리

1.1 명세 언어 Gallina 개괄

Gallina로 만든 정형 명세는 선언(declarations)정의(definitions)의 나열입니다. 정형 명세의 진정한 일부분은 아니지만 비정형적인 요청이나 서비스 루틴 시동에 관련되는 명령(commands)을 Coq에 전달할 수도 있습니다. 예를 들어, 다음과 같은 명령:

Coq < Quit.

은 현재 세션을 끝냅니다.

1.1.1 선언(declarations)

선언은 명칭(name) 하나를 명세(specification) 하나에 연관시켜줍니다. 명칭이란 대략적으로 프로그래밍 언어에서 말하는 인식명(identifier)에 해당합니다. 즉, 명칭은 문자로 시작하고 그 뒤에 문자, 숫자, 그리고 밑줄(_)이나 프라임(') 등의 몇가지 ASCII 문자가 따라나오는 문자열입니다. 대소문자를 가리므로 Aa는 서로 다른 명칭입니다. 몇몇 문자열들은 Coq의 키워드로 예약되어있어서 사용자가 인식명으로 쓸 수 없습니다.

명세란 지금 선언하고있는 개념을 분류해주는 정형적인 표현식입니다. 기본적으로 세 종류의 명세가 있으며, logical propositions, mathematical collections, 그리고 abstract types입니다. 이들은 각각 Prop, Set, Type이라고 불리는 기본적인 시스템 종류에 따라 분류되며, 이들 자신은 원소(atomic) 추상자료형(abstract types)입니다.

Gallina에서 모든 유효한 표현식 e는 그 표현식의 타입 τ(E)라고 불리는 (그리고 그 자신도 다시 유효한 표현식인) 명세와 연관됩니다. eE 타입이라는 것을 우리는 e:τ(E)라고 적습니다. Check라는 명령을 써서 Coq에게 어떤 유효한 표현식의 타입을 알려달라고 요청할 수 있습니다:

Coq < Check O.
O
     : nat

이렇게 해서, O라는 인식명이 (명칭 'O'입니다. 올바른 인식명이 아닌 숫자 '0'과 헛갈리지 마시기 바랍니다!) 현재 문맥 속에 알려져있고 그 타입은 nat이라는 명세임을 알 수 있습니다. 이 명세 자신은 mathematical collection으로 분류되며, 즉시 확인해볼 수 있습니다:

Coq < Check nat.
nat
     : Set

Set이라는 명세는 Gallina 언어의 기본 요소 중 하나인 추상타입(abstract type)인 반면, nat이나 O 같은 개념들은 Coq 시스템을 시작할 때 자동적으로 적재되는 산술적 기반 안에 정의되어 있는 공리화된 개념입니다.

이른바 구획(section) 명칭이라는 것부터 소개하겠습니다. 구획의 역할은 매개변수와 가설과 정의들의 유효범위(scope)를 제한함으로써 모형화 과정을 구조적으로 만들어주는 것입니다. 개발중인 대상 중의 일부분을 초기화하는 간단한 방법도 제공해줍니다.

Coq < Section Declaration.

이제 우리가 알고있는 것들을 가지고 "n을 자연수라고 하자"라는 비정형적 수학에 해당하는 선언을 입력해보겠습니다.

Coq < Variable n:nat.
n is assumed

"n을 양의 자연수라고 하자"와 같은 좀 더 자세한 문장을 만들려면 또다른 선언을 추가해야하며, 이는 logical proposition 명세를 갖는 Pos_n이라는 가설(hypothesis)을 명시적으로 선언합니다:

Coq < Hypothesis Pos_n : (gt n O).
Pos_n is assumed

현재 문맥 속에서 gt라는 관계가 올바른 타입으로 알려져있는지 확인해볼 수 있습니다:

Coq < Check gt.
gt
     : nat->nat->Prop

이로써 gtnat 타입의 인수 두 개를 받아서 논리적 명제를 만드는 함수라는 것을 알 수 있습니다. 여기서 일어난 일은 함수형 프로그래밍 언어에서 익히 일어나는 일과 같은 것입니다: (명세) 타입 nat과 logical propositions의 (추상) 타입 Prop을 함수 형성자인 화살표로 연결해서 nat->Prop이라는 함수 타입을 만들 수 있습니다:

Coq < Check nat->Prop.
nat->Prop
     : Type

그리고 이 타입을 다시 nat과 연결하여 자연수에 관한 이항 관계 타입인 nat->nat->Prop을 얻습니다. 사실 nat->nat->Propnat->(nat->Prop)의 축약형입니다.

함수 개념에 대해서는 그저 일반적으로 생각하시면 됩니다. AB 타입의 표현식 fA 타입의 표현식 e에 적용되어 B 타입의 표현식 (f e)를 생성합니다. 이로써, 표현식 (gt n)은 올바른 nat->Prop 타입이며, 따라서 표현식 ((gt n) O)의 축약형인 (gt n O)는 올바른 명제 타입임을 알 수 있습니다.

Coq < Check (gt n O).
(gt n O)
     : Prop

1.1.2 정의(definitions)

초기 환경에는 약간의 산술 정의들이 들어있습니다: nat은 수리계열 (Set 타입)로서 정의되어 있고, 상수 O, S, plus는 각각 nat, nat->nat, nat->nat->nat 타입의 실체로서 정의되어 있습니다. 올바른 타입의 값을 하나의 명칭에 연결시키는 새로운 정의를 내릴 수 있습니다. 예를 들어, 상수 one을 영(zero)의 계승(successor)과 같다고 정의할 수 있습니다:

Coq < Definition one := (S O).
one is defined

선택사양으로서, 필요한 타입을 지정해줄 수도 있습니다:

Coq < Definition two : nat := (S one).
two is defined

실제로 Coq는 몇가지 다른 구문을 허용합니다:

Coq < Definition three := (S two) : nat.
three is defined

다음은 nat 타입의 인수 m 하나를 받아서 (plus m m)을 결과로 만들어내는 doubling 함수를 정의하는 방법입니다:

Coq < Definition double := [m:nat](plus m m).
double is defined

대괄호에 대해서 설명하겠습니다. xA 타입이라고 선언하고 있는 문맥 안에서 e가 올바른 B 타입의 표현식이라면 [x:A]e라는 표현식은 그 문맥 안에서 올바른 AB 타입입니다.2 표현식 [x:A]e 속에서 x는 종속(bound) 변수, 혹은 멍텅구리(dummy) 변수라고 합니다. 예를 들어, 위에서 double[n:nat](plus n n)으로 정의할 수도 있었습니다.

종속(지역) 변수와 자유(전역) 변수는 섞일 수 있습니다. 예를 들어, 받아들인 인수에 상수 n을 더하는 함수를 다음과 같이 정의할 수 있습니다:

Coq < Definition add_n := [m:nat](plus m n).
add_n is defined

하지만, n의 자유출몰(free occurrence)을 캡춰하지 않은 채로 인수 m의 이름을 n으로 바꾸면 정의하고자 하는 개념의 의미가 바뀌어버리므로 안됩니다.

바인딩 연산은 논리학에서 한정사(quantifier)라는 이름으로 잘 알려져 있습니다. m>0 같은 명제를 전체 한정하여 명제 ∀m.m>0를 얻을 수 있습니다. 실은 Coq에서도 (m:nat)(gt m O)라는 구문을 써서 이런 연산을 사용할 수 있습니다. 함수 합성에서의 바인딩의 경우처럼, 한정되는 변수의 타입을 명시적으로 선언해야만 합니다. 다음과 같이 확인해봅니다:

Coq < Check (m:nat)(gt m O).
(m:nat)(gt m O)
     : Prop

현재 구획의 내용을 지워서 만들던 내용을 비울 수 있습니다:

Coq < Reset Declaration.

1.2 증명 엔진 소개 : Minimal Logic

지금부터 원소 명제 A, B, C로부터 만들어지는 여러가지 명제들에 대해서 생각해보겠습니다. 이 원소들을 Prop 타입으로 선언된 전역 변수로 소개함으로써 간단히 만들 수 있습니다. 같은 명세로 여러개의 명칭들을 선언하는 것도 간단합니다:

Coq < Section Minimal_Logic.

Coq < Variables A,B,C:Prop.
A is assumed
B is assumed
C is assumed

AB 같은 간단한 논리적 함축에 대해서 생각해봅시다. AB는 "A implies B."라고 읽습니다. 지금까지 함수 형성자로 써오던 화살표 기호를 명제 연산자로도 사용하도록 오버로드한다는 점에 주목하시기 바랍니다:

Coq < Check A->B.
A->B
     : Prop

이제 간단한 증명을 시작해봅시다. 쉽게 이해할 수 있는 항진명제 (A→(BC))→(AB)→(AC)를 증명해보겠습니다. 검증하고자하는 추측과 함께 Goal 명령을 써서 증명 엔진으로 들어갑니다:

Coq < Goal (A->(B->C))->(A->B)->(A->C).
1 subgoal

  A : Prop
  B : Prop
  C : Prop
  ============================
   (A->B->C)->(A->B)->A->C

Unnamed_thm <

현재 골은 이중선 아래에 나타나고 지역 가설들(처음에는 없습니다)은 선 위에 나타납니다. 지역 가설들과 골의 조합을 judgment라고 합니다. 새로운 프롬프트 'Unnamed_thm < '은 지금 우리가 시스템의 내부 루프인 증명 모드에 있다는 것을 의미합니다. 이 모드에서는 증명을 조합해주는 원시요소인 전략(tactics) 같은 새로운 명령들을 쓸 수 있습니다. 전략은 현재 골에 대해 작동하여 몇몇 가설격 judgment들의 증명으로부터 현재 골에 해당하는 judgment의 증명을 구성하며, 이는 다시 현재 추정하고 있는 judgment들의 목록에 추가됩니다. 예를 들어, Intro 전략은 증명하고자 하는 목표(goal)가 함축(implication)인 어떠한 judgment에도 적용될 수 있으며, 함축 연산자(->)의 좌항에 해당하는 명제를 지역 가설 목록으로 이동시킵니다:

Unnamed_thm < Intro H.
1 subgoal

  A : Prop
  B : Prop
  C : Prop
  H : A->B->C
  ============================
   (A->B)->A->C

여러 개의 소개3를 한 번에 수행할 수 있습니다:

Unnamed_thm < Intros H' HA.
1 subgoal

  A : Prop
  B : Prop
  C : Prop
  H : A->B->C
  H' : A->B
  HA : A
  ============================
   C

현재 골이 된 C는, AB를 증명할 수 있다는 가정 하에 가설 H로부터 얻을 수 있음을 알 수 있습니다. 이런 추론 과정은 Apply 전략이 구현해줍니다:

Unnamed_thm < Apply H.
2 subgoals

  A : Prop
  B : Prop
  C : Prop
  H : A->B->C
  H' : A->B
  HA : A
  ============================
   A
subgoal 2 is:
 B

이제 증명해야할 추정물로서의 judgment가 두 개가 되어버렸습니다. 이 중 첫번째 judgment만 전체를 다 보여주며, 나머지들은 지역 가설 목록 없이 해당되는 서브골만 달랑 보여줍니다. Apply는 이전 judgment의 지역 가설들을 유지해주며, 따라서 Apply가 만들어낸 새로운 judgment들에서도 여전히 이 가설들을 쓸 수 있습니다.

현재 골을 해결하기 위해서는 단지 현재 골이 가설 HA에 정확히 그대로 들어있음을 알려주기만하면 됩니다:

Coq < Exact HA.
1 subgoal

  A : Prop
  B : Prop
  C : Prop
  H : A->B->C
  H' : A->B
  HA : A
  ============================
   B

이제 H'를 적용합니다:

Coq < Apply H'.
1 subgoal

  A : Prop
  B : Prop
  C : Prop
  H : A->B->C
  H' : A->B
  HA : A
  ============================
   A

이제 바로 위에서 했던 것처럼 Exact HA로 증명을 결론지을 수 있습니다. 사실은, HA라는 명칭에 구애될 필요 없이, 그저 현재 골이 현재 지역 가정들로부터 해결 가능하다고 말해주기만하면 됩니다:

Coq < Assumption.
Subtree proved!

이제 증명이 끝났습니다. 군소리 없이 표준 Coq toplevel 루프로 돌아가게해주는 Abort 명령을 써서 이 증명을 버릴 수도 있고, 아니면 현재 문맥 속에 trivial_lemma 같은 명칭으로 보조정리(lemma)로서 저장해둘 수도 있습니다:

Coq < Save trivial_lemma.
Intro H.
Intros H' HA.
Apply H.
Exact HA.
Apply H'.
Assumption.
trivial_lemma is defined

일종의 주석 격으로, 시스템은 증명 과정에서 사용된 모든 전략 명령들을 나열한 증명 스크립트를 보여줍니다.

같은 증명을 몇가지 다른 방식으로 다시 해봅시다. 우선, 골을 처음 지정할 때 아예 (그러리라 추정되는) 보조정리로 이름지을 수 있습니다:

Coq < Lemma distr_impl : (A->(B->C))->(A->B)->(A->C).
1 subgoal

  A : Prop
  B : Prop
  C : Prop
  ============================
   (A->B->C)->(A->B)->A->C

다음으로, 소개 전략이 만드는 지역 가정들의 이름을 생략할 수 있습니다. 증명 엔진이 충돌 없는 새로운 명칭을 자동으로 붙여줍니다.

Coq < Intros.
1 subgoal

  A : Prop
  B : Prop
  C : Prop
  H : A->B->C
  H0 : A->B
  H1 : A
  ============================
   C

인수 없이 Intros 전략을 사용하면, Intro 전략을 합법적인 한 계속 적용한 것과 같은 효과를 냅니다.

다음으로, 전략들을 조합해주는 tacticals를 써서 몇 개의 전략들을 직렬 혹은 병렬로 조합할 수 있습니다. 주요 구성은 다음과 같습니다:

따라서 distr_impl의 증명을 복합전략 한 번으로 끝낼 수 있습니다:

Coq < Apply H; [Assumption | Apply H0; Assumption].
Subtree proved!

이제 보조정리 distr_impl를 저장합시다:

Coq < Save.
Intros.
Apply H; [ Assumption | Apply H0; Assumption ].
distr_impl is defined

여기서 Save에는 인수가 필요 없는데, 이미 distr_impl이라는 명칭을 줬기 때문입니다. 하지만 주어진 명칭과는 다른 새로운 명칭을 Save 명령에 인수로 넣어서 이 명칭을 덮어쓸 수도 있습니다.

사실은, IntroApply, Assumption 같은 쉬운 전략들의 조합은 사용자의 안내 없이도 Auto라 불리는 자동 전략에 의해 완전 자동으로 이루어질 수 있습니다:

Coq < Lemma distr_imp : (A->(B->C))->(A->B)->(A->C).
1 subgoal

  A : Prop
  B : Prop
  C : Prop
  ============================
   (A->B->C)->(A->B)->A->C

Coq < Auto.
Subtree proved!

이번에는 증명을 저장하지 않고 Abort 명령으로 버리도록 합니다:

Coq < Abort.
Current goal aborted

증명 과정 중의 어느 곳에서도 Abort 명령으로 증명 모드를 끝내고 Coq의 메인 루프로 탈출할 수 있습니다. 혹은 Restart 명령으로 같은 보조정리의 증명을 scratch로부터 다시 시작할 수도 있습니다. 한 단계 되돌아가기 위해서 Undo를 쓸 수도 있고, 좀 더 일반적으로는 Undo n 명령으로 n 단계를 되돌아갈 수 있습니다.

Inspect n이라는 유용한 명령을 소개하면서 이번 장을 마칠까합니다. 이 명령은 Coq의 전역 환경을 추적해서 마지막 n번째로 선언된 개념을 보여줍니다.

Coq < Inspect 3.
distr_impl : (A->B->C)->(A->B)->A->C

선언은 전역 매개변수든 공리든 간에 그 앞에 ***를 달고 나타납니다. 정의(definitions)와 보조정리(lemmas)들은 자신들의 명세와 함께 나타나지만, 그들의 값(혹은 증거)은 생략됩니다.

1.3 명제 논리

1.3.1 연어 명제 (Conjunction)

지금까지 함축문을 증명하기 위해서 IntroApply 전략이 조합되는 것을 보았습니다. 좀 더 일반적으로 말해서, Coq는 Natural Deduction이라 불리는 추론 형태를 지원합니다. 이것은 메인 연산자가 어떤 접속사인 골을 어떻게 증명하는가를 말해주는 소개 규칙(introduction rules)과, 메인 연산자가 어떤 접속사인 가설을 어떻게 사용하는가를 말해주는 삭제 규칙(elimination rules)으로 추론 과정을 분석합니다. 명제 접속사인 ∧와 ∨에 대해서 이런 발상을 어떻게 이용하는지 보여드리겠습니다.

Coq < Lemma and_commutative : A /\ B -> B /\ A.
1 subgoal

  A : Prop
  B : Prop
  C : Prop
  ============================
   A/\B->B/\A

Coq < Intro.
1 subgoal

  A : Prop
  B : Prop
  C : Prop
  H : A/\B
  ============================
   B/\A

연어 가설 HElim 전략을 써서 그 구성 요소들로 분해합니다:

Coq < Elim H.
1 subgoal

  A : Prop
  B : Prop
  C : Prop
  H : A/\B
  ============================
   A->B->B/\A

이제 연어 소개 전략인 Split를 써서 연어 형태의 골을 두 개의 서브골로 나눕니다:

Coq < Split.
2 subgoals

  A : Prop
  B : Prop
  C : Prop
  H : A/\B
  H0 : A
  H1 : B
  ============================
   B
subgoal 2 is:
 A

이제 증명은 명백해졌습니다. 사실, 전체 증명은 다음과 같이 얻을 수 있습니다:

Coq < Restart.
1 subgoal

  A : Prop
  B : Prop
  C : Prop
  ============================
   A/\B->B/\A

Coq < Intro H; Elim H; Auto.
Subtree proved!

Coq < Save.
Intro H; Elim H; Auto.
and_commutative is defined

여기서 Auto 전략이 성공한 것은, 일종의 힌트로서 연어 소개 연산자인 conj를 알고있었기 때문입니다.

Coq < Check conj.
conj
     : (A,B:Prop)A->B->A/\B

사실, Split 전략은 Apply conj.의 축약형일 뿐입니다.

방금 우리는 단순히 지역 가설을 적용하는 것보다 Auto 전략을 쓰는 것이 더 강력하다는 것을 보았습니다. Auto는 힌트로 주어진 모든 보조정리들을 적용해봅니다. Hints Resolve 명령으로 지금부터 Auto 전략이 힌트로 사용할 보조정리를 등록할 수 있으며, 이렇게해서 Auto의 힘이 더 강화됩니다.

1.3.2 이접 명제 (Disjunction)

비슷한 방식으로 이접 명제에 대해서 생각해봅니다:

Coq < Lemma or_commutative : A \/ B -> B \/ A.
1 subgoal

  A : Prop
  B : Prop
  C : Prop
  ============================
   A\/B->B\/A

Coq < Intro H; Elim H.
2 subgoals

  A : Prop
  B : Prop
  C : Prop
  H : A\/B
  ============================
   A->B\/A
subgoal 2 is:
 B->B\/A

첫번째 서브골을 자세히 증명해봅시다. A로부터 B\/A를 증명하기 위해서 Intro를 사용합니다:

Coq < Intro HA.
2 subgoals

  A : Prop
  B : Prop
  C : Prop
  H : A\/B
  HA : A
  ============================
   B\/A
subgoal 2 is:
 B->B\/A

여기서 가설 H는 이제 더이상 필요하지 않습니다. Clear 전략으로 이것을 선택해서 지울 수 있습니다. 이런 간단한 증명에서는 별 문제가 되지 않지만, 훨씬 더 큰 증명 과정에서는 화면을 어지럽히는 불필요한 가설들을 지우는 데에 유용합니다.

Coq < Clear H.
2 subgoals

  A : Prop
  B : Prop
  C : Prop
  HA : A
  ============================
   B\/A
subgoal 2 is:
 B->B\/A

이접 접속사에는 두 개의 소개 규칙이 있습니다. PQP로부터 얻을 수도 있고 Q로부터 얻을 수도 있기 때문이죠. 이런 두 가지 증명 형성자는 각각 or_introlor_intror이라고 불립니다. 이들은 각각 Left 전략과 Right 전략으로 현재 골에 적용됩니다. 예를 들어:

Coq < Right.
2 subgoals

  A : Prop
  B : Prop
  C : Prop
  HA : A
  ============================
   A
subgoal 2 is:
 B->B\/A

Coq < Trivial.
1 subgoal

  A : Prop
  B : Prop
  C : Prop
  H : A\/B
  ============================
   B->B\/A

Trivial 전략은 힌트 데이터베이스를 기반으로 Auto와 비슷하게 동작하지만, 대신 골을 한 단계로 해결할 수 있는 전략만을 시도합니다.

방금 수행했던 지루한 기본적 작업들은 두 번째의 대칭적인 경우에 대해서는 자동적으로 수행될 수 있습니다:

Coq < Auto.
Subtree proved!

그러나, Auto 혼자만으로는 삭제(elimination) 과정을 전혀 시도하지 않기 때문에 전체 보조정리를 증명하지 못합니다. Auto로 이런 간단한 항진명제를 자동적으로 증명하지 못한다는 것이 조금 실망스러울 것입니다. 그 이유는 Auto를 언제나 효율적으로 사용할 수 있도록 그 효율성을 유지하기 위함입니다.

1.3.3 Tauto

Coq에서 항진명제를 위한 궁극의 전략은 Tauto 전략입니다.

Coq < Restart.
1 subgoal

  A : Prop
  B : Prop
  C : Prop
  ============================
   A\/B->B\/A

Coq < Tauto.
Subtree proved!

Coq < Save.
Tauto.
or_commutative is defined

문맥 속에 현재 정의되어있는 개념들의 값을 출력해주는 표준 명령을 써서, Tauto가 구성한 실제 증명 트리를 탐색해볼 수 있습니다:

Coq < Print or_commutative.
or_commutative =
[H:(A\/B)]
 (or_ind A B B\/A [H0:A](or_intror B A H0) [H0:B](or_introl B A H0) H)
     : A\/B->B\/A

아무 설명 없이 이 증명 텀의 표기를 이해하기는 좀 어려울겁니다. [H:A\/B] 같은 대괄호는 Intro H에 해당하는 반면 (or_intror B A H0) 같은 서브텀은 Apply or_intror; Exact H0에 해당합니다. 추가 인수 BAor_intror의 기동 요소에 해당하며, 이들은 Apply 전략이 골에 패턴 매칭을 수행할 때 자동적으로 영향을 받는 부분입니다. 물론, 전문가라면 이런 증명 텀을 Curry-Howard isomorphism을 통해 natural deduction 증명 텀의 표기법으로 사용되는 λ 텀으로서 받아들일 수 있을겁니다. Coq를 처음 사용하시는 분들은 이런 정형적인 세부 사항들은 무시해도 괜찮습니다.

좀 더 복잡한 예제를 통해 Tauto 전략을 연습해봅시다:

Coq < Lemma distr_and : A->(B/\C) -> (A->B /\ A->C).
1 subgoal

  A : Prop
  B : Prop
  C : Prop
  ============================
   A->B/\C->A->B/\A->C

Coq < Tauto.
Subtree proved!

Coq < Save.
Tauto.
distr_and is defined

1.3.4 전통적 추론법 (Classical reasoning)

Tauto는 항상 뭔가 답을 해줍니다. 아래 예제는 Tauto가 실패하는 경우입니다:

Coq < Lemma Peirce : ((A->B)->A)->A.
1 subgoal

  A : Prop
  B : Prop
  C : Prop
  ============================
   ((A->B)->A)->A

Coq < Try Tauto.
1 subgoal

  A : Prop
  B : Prop
  C : Prop
  ============================
   ((A->B)->A)->A

전략 제어 구문인 Try의 용법에 주목하십시오. Try는 인수로 들어온 전략이 실패하면 아무것도 하지 않습니다.

전통적인 추론 방식에 익숙한 분들에게 있어서 이것은 당황스러운 현상일겁니다. Peirce의 정리는 불리언 논리체계에서는 참입니다. 즉, 이 정리는 AB에 대응되는 모든 truth-assignment에 대해서 항상 참으로 평가됩니다. 사실, Peirce 법칙의 이중부정은 Coq에서도 Tauto를 써서 증명할 수 있습니다:

Coq < Abort.
Current goal aborted

Coq < Lemma NNPeirce : ~~(((A->B)->A)->A).
1 subgoal

  A : Prop
  B : Prop
  C : Prop
  ============================
   ~~(((A->B)->A)->A)

Coq < Tauto.
Subtree proved!

Coq < Save.
Tauto.
NNPeirce is defined

전통적 논리 체계에서 어떤 명제의 이중부정은 그 명제 자신과 동치입니다만, Coq의 직관주의 논리 체계에서는 그렇지 않습니다. 만일 Coq에서 전통적인 논리 체계를 쓰고싶으시다면 명시적으로 Classical 모듈을 적재해야합니다. 이 모듈은 excluded middle 공리(axiom)인 classic과, de Morgan 법칙 같은 전통적인 항진명제들을 선언하고 있습니다. Coq의 라이브러리로부터 모듈을 불러오기 위해서는 Require 명령을 사용합니다:

Coq < Require Classical.

Coq < Check NNPP.
NNPP
     : (p:Prop)~~p->p

이제 Peirce 법칙 같은 전통적인 법칙들을 (비록 완전히 직접적인 방법을 쓸 수는 없지만) 쉽게 증명할 수 있습니다:

Coq < Lemma Peirce : ((A->B)->A)->A.
1 subgoal

  A : Prop
  B : Prop
  C : Prop
  ============================
   ((A->B)->A)->A

Coq < Apply NNPP; Tauto.
Subtree proved!

Coq < Save.
Apply NNPP; Tauto.
Peirce is defined

명제 논리 추론의 또 한 가지 예로서 Scottish puzzle이라는 것이 있습니다. 회원제 클럽에 다음과 같은 규칙이 있습니다:

  1. 스코틀랜드인이 아닌 모든 회원은 빨간 양말을 신는다
  2. 모든 회원들은 킬트를 입던가 혹은 빨간 양말을 안 신는다
  3. 결혼한 회원은 일요일에 싸돌아다니지 않는다
  4. 스코틀랜드인 회원이라면, 그리고 스코틀랜드인 회원인 경우에만 일요일에 싸돌아다닌다.
  5. 킬트를 입는 회원은 모두 결혼한 스코틀랜드인이다
  6. 모든 스코틀랜드인 회원은 킬트를 입는다

자, 이런 규칙은 아무도 따를 수 없는 불가능한 규칙임을 보여드리겠습니다.

Coq < Section club.

Coq < Variable Scottish, RedSocks, WearKilt, Married, GoOutSunday : Prop.
Scottish is assumed
RedSocks is assumed
WearKilt is assumed
Married is assumed
GoOutSunday is assumed

Coq < Hypothesis rule1 : ~Scottish -> RedSocks.
rule1 is assumed

Coq < Hypothesis rule2 : WearKilt \/ ~RedSocks.
rule2 is assumed

Coq < Hypothesis rule3 : Married -> ~GoOutSunday.
rule3 is assumed

Coq < Hypothesis rule4 : GoOutSunday <-> Scottish.
rule4 is assumed

Coq < Hypothesis rule5 : WearKilt -> (Scottish /\ Married).
rule5 is assumed

Coq < Hypothesis rule6 : Scottish -> WearKilt.
rule6 is assumed

Coq < Lemma NoMember : False.
1 subgoal

  A : Prop
  B : Prop
  C : Prop
  Scottish : Prop
  RedSocks : Prop
  WearKilt : Prop
  Married : Prop
  GoOutSunday : Prop
  rule1 : ~Scottish->RedSocks
  rule2 : WearKilt\/~RedSocks
  rule3 : Married->~GoOutSunday
  rule4 : GoOutSunday<->Scottish
  rule5 : WearKilt->Scottish/\Married
  rule6 : Scottish->WearKilt
  ============================
   False

Coq < Tauto.
Subtree proved!

Coq < Save.
Tauto.
NoMember is defined

NoMember는 주어진 가설들이 말도 안됨을 보여주는 증거입니다. 이 구획(section)을 여기서 끝낼 수 있는데, 이 경우 변수들과 가설들은 해제(discharge)되고 NoMember의 타입은 일반화됩니다.

Coq < End club.
NoMember is discharged.

Coq < Check NoMember.
NoMember
     : (Scottish,RedSocks,WearKilt,Married,GoOutSunday:Prop)
        (~Scottish->RedSocks)
        ->WearKilt\/~RedSocks
        ->(Married->~GoOutSunday)
        ->(GoOutSunday<->Scottish)
        ->(WearKilt->Scottish/\Married)
        ->(Scottish->WearKilt)
        ->False

1.4 술어 논리

이제 술어논리, 그 중에서도 일단은 일계(first-order) 술어논리의 세계로 들어가보겠습니다. 술어논리의 요점은 수리적인 개념 정의를 사용하는 대신 해석되지 않은 함수와 빈위기호(predicate symbols)를 정형적으로 조작하여 최대한 추상적인 방법으로 증명을 시도한다는 점입니다.

1.4.1 Sections and signatures

대개의 경우 개별 변수들과 함수 기호들이 의미를 갖는 어떤 사고 범위 (정의 구역) 내에서 작업하게 됩니다. Coq에서는 다양한 타입을 갖는 언어를 사용하기 때문에 몇 개의 도메인들을 섞을 수 있습니다. 우선, Set으로서 공리화된 정의역 D 위에서 몇 가지 연습을 해본 후, 각각 단항, 이항인 D 위의 두 빈위기호 PR을 생각해보겠습니다. 이런 추상 요소는 문맥 속에 전역 변수로 포함됩니다. 하지만, 우리의 전역 환경을 이런 선언들로 오염시킬 때에는 항상 주의해야합니다. 예를 들어, 우리는 이미 n, Pos_n, A, B, C등의 변수를 선언함으로써 우리의 Coq 세션을 오염시켜 놓았습니다. 초기 세션의 깨끗한 상태로 돌아가려면 Reset 명령을 써야하며, 이 명령은 구획을 지우기 전에 했던 전역 개념이 만들어지기 이전 상태로 돌아가게합니다. 혹은, 다음 명령으로 완전히 초기 상태로 돌아갈 수도 있습니다:

Coq < Reset Initial.

이제 새로운 구획(section)을 선언하여 지역적으로 잘 경계지어진 구역 안에서 개념들을 정의할 수 있도록 합니다. 추론의 정의구역인 DD에 대한 이항 관계인 R을 가정하는 것으로 시작해보겠습니다:

Coq < Section Predicate_calculus.

Coq < Variable D:Set.
D is assumed

Coq < Variable R: D -> D -> Prop.
R is assumed

술어 논리 추론의 간단한 예로서, 관계 R은 symmetric하고 transitive하다고 가정하고, R에 대한 대응점을 갖는 모든 점 x에 대해서 R은 reflexive하다는 것을 보이기로 하겠습니다. R에 관한 가정들은 전역 공리로 등록되는게 아니라 지금 증명해보이려는 정리를 위한 지역가설이어야 하기 때문에, 이런 효과를 위한 특정 구획을 열도록 합니다.

Coq < Section R_sym_trans.

Coq < Hypothesis R_symmetric : (x,y:D) (R x y) -> (R y x).
R_symmetric is assumed

Coq < Hypothesis R_transitive : (x,y,z:D) (R x y) -> (R y z) -> (R x z).
R_transitive is assumed

(x:D)라는 구문은 전체한정 ∀xD를 의미함을 상기하시기 바랍니다.

1.4.2 존재 한정 (Existential quantification)

이제 우리의 보조정리를 말하고 증명 모드로 들어갑니다.

Coq < Lemma refl_if : (x:D)(EX y | (R x y)) -> (R x x).
1 subgoal

  D : Set
  R : D->D->Prop
  R_symmetric : (x,y:D)(R x y)->(R y x)
  R_transitive : (x,y,z:D)(R x y)->(R y z)->(R x z)
  ============================
   (x:D)(EX y:D | (R x y))->(R x x)

현재 열려있는 구획에 대해 지역적인 가설들이 현재 골에 대한 지역가설로서 나열되어있는 점을 주시하시기 바랍니다. 그 근거는, 앞으로 보시게 되겠지만, 나중에 해당 구획을 닫을 때 이 가설들은 해제(discharge)된다는 것입니다.

존재 한정의 함수형 구문에 주목하십시오. 존재한정사는 술어 하나를 인수로 받는 연산자 ex로부터 만들어집니다:

refl_if < Check ex.
ex
     : (A:Set)(A->Prop)->Prop

(EX x | (P x))라는 표현은 (ex D [x:D](P x))의 명확한 표현일 뿐입니다. Coq에서 존재 한정은 ∧나 ∨ 같은 접속사와 비슷한 방식으로 처리됩니다: 존재 한정은 ex_intro라는 proof combinator를 이용해서 소개되는데, 이는 Exists라는 특정 전략에 의해 기동됩니다. 그리고 존재 한정을 삭제(eliminate)함으로써 Pa:D라는 증명이 제공되며, 이 때 실제로 aP를 만족시킨다는 가설 h:(P a)도 함께 제공됩니다. 간단한 예제를 통해 이것이 어떻게 작동하는지 확인해보겠습니다.

refl_if < Intros x x_Rlinked.
1 subgoal

  D : Set
  R : D->D->Prop
  R_symmetric : (x,y:D)(R x y)->(R y x)
  R_transitive : (x,y,z:D)(R x y)->(R y z)->(R x z)
  x : D
  x_Rlinked : (EX y:D | (R x y))
  ============================
   (R x x)

Intro는 전체한정을 함축(implication)의 전제와 마찬가지로 취급한다는 점을 기억하시기 바랍니다. 필요한 경우에는 종속변수의 이름이 바뀝니다. 예를 들어, 만일 위의 과정 대신 Intro y라는 명령으로 시작했더라면 골은 다음과 같이 바뀌었을 것입니다:

refl_if < Intro y.
1 subgoal

  D : Set
  R : D->D->Prop
  R_symmetric : (x,y:D)(R x y)->(R y x)
  R_transitive : (x,y,z:D)(R x y)->(R y z)->(R x z)
  y : D
  ============================
   (EX y0:D | (R y y0))->(R y y)

이제 xR-successor인 y를 내도록 존재 가설 x_Rlinked를 사용합시다. 이 과정은 ElimIntros의 두 단계로 진행됩니다.

refl_if < Elim x_Rlinked.
1 subgoal

  D : Set
  R : D->D->Prop
  R_symmetric : (x,y:D)(R x y)->(R y x)
  R_transitive : (x,y,z:D)(R x y)->(R y z)->(R x z)
  x : D
  x_Rlinked : (EX y:D | (R x y))
  ============================
   (x0:D)(R x x0)->(R x x)

refl_if < Intros y Rxy.
1 subgoal

  D : Set
  R : D->D->Prop
  R_symmetric : (x,y:D)(R x y)->(R y x)
  R_transitive : (x,y,z:D)(R x y)->(R y z)->(R x z)
  x : D
  x_Rlinked : (EX y:D | (R x y))
  y : D
  Rxy : (R x y)
  ============================
   (R x x)

이제 R_transitive를 사용하고 싶습니다. Apply 전략은 어떻게 xx에 대응시키고 zx에 대응시킬지 알고 있습니다만, R_transitive의 가설에는 등장하고 결론에는 나타나지 않는 y를 어떻게 초기화할지에 대해서는 약간의 도움이 필요합니다. 다음과 같이 with 절을 써서 Apply에게 올바른 힌트를 줍니다:

refl_if < Apply R_transitive with y.
2 subgoals

  D : Set
  R : D->D->Prop
  R_symmetric : (x,y:D)(R x y)->(R y x)
  R_transitive : (x,y,z:D)(R x y)->(R y z)->(R x z)
  x : D
  x_Rlinked : (EX y:D | (R x y))
  y : D
  Rxy : (R x y)
  ============================
   (R x y)
subgoal 2 is:
 (R y x)

나머지 증명 과정은 늘상 하던 대로입니다:

refl_if < Assumption.
1 subgoal

  D : Set
  R : D->D->Prop
  R_symmetric : (x,y:D)(R x y)->(R y x)
  R_transitive : (x,y,z:D)(R x y)->(R y z)->(R x z)
  x : D
  x_Rlinked : (EX y:D | (R x y))
  y : D
  Rxy : (R x y)
  ============================
   (R y x)

refl_if < Apply R_symmetric; Assumption.
Subtree proved!

refl_if < Save.

이제 현재 구획을 닫읍시다.

Coq < End R_sym_trans.
refl_if is discharged.

여기서 Coq가 말하는 것은, 모든 지역 가설들이 refl_if 문에 대해 해제되었고, 이제 refl_ifPredicate_calcaulus라는 구획 안에 선언된 일계언어의 일반적인 정리가 되었다는 일종의 경고입니다. 위 예제에서 R_sym_trans 구획을 사용한 것은 사실은 그다지 꼭 필요한 것은 아니었습니다. R_symmetricR_transitive를 문맥 속의 전역 가설로 설정하는 대신, 정리 refl_if를 일반적인 형태로 말해놓고 처음 단계에서 Intros를 써서 지역가설로 뽑아냄으로써 같은 증명을 할 수 있었기 때문이죠. 하지만, 만일 관계 R에 대한 더 많은 정리들을 증명하려했다면, 구획을 닫을 때 대칭성과 전의성에 대한 의존도를 최소화하는 일반화된 형태의 모든 문들을 다 얻게됐을 것입니다.

1.4.3 전통적인 술어논리의 모순

Predicate_calculus 구획을 계속하여 이런 면을 살펴봅시다. 단항 술어 P와 상수 d를 선언합니다:

Coq < Variable P:D->Prop.
P is assumed

Coq < Variable d:D.
d is assumed

이제 일계술어논리의 잘 알려진 사실 하나를 증명해봅니다: 즉, 전체 한정된 술어는 비어있지 않다, 혹은 존재 한정은 전체 한정으로부터 함축된다는 사실입니다.

Coq < Lemma weird : ((x:D)(P x)) -> (EX a | (P a)).
1 subgoal

  D : Set
  R : D->D->Prop
  P : D->Prop
  d : D
  ============================
   ((x:D)(P x))->(EX a:D | (P a))

weird < Intro UnivP.
1 subgoal

  D : Set
  R : D->D->Prop
  P : D->Prop
  d : D
  UnivP : (x:D)(P x)
  ============================
   (EX a:D | (P a))

일단, 보조정리 weird의 문장 속의 (x:D)(P x) 를 감싸는 괄호에 주목하십시오. 만일 이 괄호를 빠트리면, (P x)를 검증하는 x를 공리로 간주할 수 있기 때문에, Coq의 파서는 이 문장을 완전히 자명한 사실로 해석할 것입니다. 이 예에서는 문제의 소지가 조금 더 있습니다. 만일 D라는 Set 속에 원소가 있다면 이 원소에 UnivP를 적용하여 결론을 얻을 수 있을것이고, 그렇지 않다면 막히게됩니다. 사실 이런 원소인 d가 있지만, 이것은 우리의 새로운 시그너춰 덕분일 뿐입니다. 바로 이 부분이 표준적인 술어논리와 Coq의 미묘한 차이점입니다. 표준 일계술어논리에서는 보조정리 weird와 동치인 문장은 항상 만족됩니다. 한정사의 추정 규칙 상, 해석하는 정의역은 비어있지 않다고 가정하는 의미론적 규칙 때문이죠. 반면 타입이 systematic하게 존재한다고 가정하지 않는 Coq에서는, 술어의 정의역에서 명시적으로 원소를 생성하도록 하는 시그너춰가 있을 때에만 보조정리 weird가 만족됩니다.

Exists 전략의 사용법을 보기 위해 증명을 결론지어봅시다:

weird < Exists d; Trivial.
Subtree proved!

weird < Save.
Intro UnivP.
Split with d; Trivial.
weird is defined

전통적인 술어논리의 법칙들 중 때때로 사람을 당황스럽게 만드는 부분을 보여주는 또다른 예가 바로 Smullyan의 술꾼 모순입니다: "비어있지 않은 모든 술집에는, 만일 그가 술을 마시면 모든 사람이 술을 마시는 그런 사람이 반드시 있다"라는 것이죠. 술집을 Set D로, 음주를 술어 P로 놓습니다. 전통적인 추론 방식이 필요할 것입니다. 전에 했던 것처럼 Classical 모듈을 적재하는 대신, excluded middle 법칙을 지금 이곳에서의 지역 가설로 말해줍니다:

Coq < Hypothesis EM : (A:Prop) A \/ ~A.
EM is assumed

Coq < Lemma drinker : (EX x | (P x) -> (x:D)(P x)).
1 subgoal

  D : Set
  R : D->D->Prop
  P : D->Prop
  d : D
  EM : (A:Prop)A\/~A
  ============================
   (EX x:D | (P x)->(x0:D)(P x0))

술을 마시지 않는 사람이 있는가 없는가 하는 경우에 따라 증명을 진행합니다. 이렇게 경우에 따라 나누는 추론 방식은 EM의 적절한 실체를 Elim하여 excluded middle 원리를 가동함으로써 진행됩니다:

drinker < Elim (EM  (EX x | ~(P x))).
2 subgoals

  D : Set
  R : D->D->Prop
  P : D->Prop
  d : D
  EM : (A:Prop)A\/~A
  ============================
   (EX x:D | ~(P x))->(EX x:D | (P x)->(x0:D)(P x0))
subgoal 2 is:
 ~(EX x:D | ~(P x))->(EX x:D | (P x)->(x0:D)(P x0))

먼저 첫번째 경우를 보겠습니다. 술을 마시지 않는 사람을 Tom이라고 합시다:

drinker < Intro Non_drinker; Elim Non_drinker; Intros Tom Tom_does_not_drink.
2 subgoals

  D : Set
  R : D->D->Prop
  P : D->Prop
  d : D
  EM : (A:Prop)A\/~A
  Non_drinker : (EX x:D | ~(P x))
  Tom : D
  Tom_does_not_drink : ~(P Tom)
  ============================
   (EX x:D | (P x)->(x0:D)(P x0))
subgoal 2 is:
 ~(EX x:D | ~(P x))->(EX x:D | (P x)->(x0:D)(P x0))

이 경우에는 Tom을 고려하여 결론짓습니다. Tom이 술을 마시면 모순이 생기기 때문이죠:

drinker < Exists Tom; Intro Tom_drinks.
2 subgoals

  D : Set
  R : D->D->Prop
  P : D->Prop
  d : D
  EM : (A:Prop)A\/~A
  Non_drinker : (EX x:D | ~(P x))
  Tom : D
  Tom_does_not_drink : ~(P Tom)
  Tom_drinks : (P Tom)
  ============================
   (x:D)(P x)
subgoal 2 is:
 ~(EX x:D | ~(P x))->(EX x:D | (P x)->(x0:D)(P x0))

모순을 일으키는 경우를 제거하는 몇가지 방법이 있습니다. 간단한 한 가지 방법은 다음과 같이 Absurd 전략을 쓰는 것입니다:

drinker < Absurd (P Tom); Trivial.
1 subgoal

  D : Set
  R : D->D->Prop
  P : D->Prop
  d : D
  EM : (A:Prop)A\/~A
  ============================
   ~(EX x:D | ~(P x))->(EX x:D | (P x)->(x0:D)(P x0))

이제 두 번째 경우를 생각합니다. 여기서는 어느 누구라도 다 상관 없습니다: 비어있지 않다는 증거 d에 의해서 아무개를 얻을 수 있습니다:

drinker < Intro No_nondrinker; Exists d; Intro d_drinks.
1 subgoal

  D : Set
  R : D->D->Prop
  P : D->Prop
  d : D
  EM : (A:Prop)A\/~A
  No_nondrinker : ~(EX x:D | ~(P x))
  d_drinks : (P d)
  ============================
   (x:D)(P x)

이제 술집에 있는 아무개 Dick을 하나 상정해서, 그가 술을 마시는지 마시지 않는지에 따라 경우를 나누어 추론합니다:

drinker < Intro Dick; Elim (EM (P Dick)); Trivial.
1 subgoal

  D : Set
  R : D->D->Prop
  P : D->Prop
  d : D
  EM : (A:Prop)A\/~A
  No_nondrinker : ~(EX x:D | ~(P x))
  d_drinks : (P d)
  Dick : D
  ============================
   ~(P Dick)->(P Dick)

자명(trivial)하지 않은 유일한 경우는 다시 모순으로 취급합니다:

drinker < Intro Dick_does_not_drink; Absurd (EX x | ~(P x)); Trivial.
1 subgoal

  D : Set
  R : D->D->Prop
  P : D->Prop
  d : D
  EM : (A:Prop)A\/~A
  No_nondrinker : ~(EX x:D | ~(P x))
  d_drinks : (P d)
  Dick : D
  Dick_does_not_drink : ~(P Dick)
  ============================
   (EX x:D | ~(P x))

drinker < Exists Dick; Trivial.
Subtree proved!

drinker < Save.
Elim (EM (EX x:? | ~(P x))).
Intro Non_drinker; Elim Non_drinker; Intros Tom Tom_does_not_drink.
Split with Tom; Intro Tom_drinks.
Absurd (P Tom); Trivial.
Intro No_nondrinker; Split with d; Intro d_drinks.
Intro Dick; Elim (EM (P Dick)); Trivial.
Intro Dick_does_not_drink; Absurd (EX x:? | ~(P x)); Trivial.
Split with Dick; Trivial.
drinker is defined

이제 메인 구획을 닫읍시다:

Coq < End Predicate_calculus.
refl_if is discharged.
weird is discharged.
drinker is discharged.

세 가지 정리들이 가장 일반적인 방식으로 완벽하게 일반화되는 과정에 주목하시기 바랍니다. 정의역 D는 세 가지 정리 모두에 대해서 해제되었고, D가 존재한다는 가설 하에서 관계 Rrefl_if에 대해서만 해제되었으며, Pweirddrinker에 대해서만 해제되었습니다. 마지막으로, excluded middle 가설은 drinker에 대해서만 해제되었습니다.

weirddrinker 문장에서 d라는 명칭도 사라졌음에 주의하십시오. Coq의 pretty-printer는 dE 속에 등장하지 않는 (d:D)E 같은 한정을 함수형 표현법인 D->E로 체계적으로 바꿔주기 때문입니다. 마찬가지로 drinker 속에 EM이라는 명칭은 나타나지 않습니다.

실제로, 전체한정, 함축(implication), 그리고 함수 형성은 모두 타입 이론상의 한 가지 일반화된 생성자인 dependent product의 특수한 경우들일 뿐입니다. 이것은 인덱스된 함수 계열에 해당하는 수학적 생성법입니다. 함수 f ∈ ΠxD.C x자신의 정의역의 원소인 x를 (인덱스된) 공변역 C x에 대응시킵니다. 따라서 ∀xD.P x의 증거는 D의 원소 x를 명제 P x의 증거에 대응시키는 함수입니다.

1.4.4 지역 가정의 유연한 사용법

예를 들어 좀 더 일반화된 귀납 가설을 얻기 위해, 증명 과정에서 지역 가정을 추출해서 골에 다시 명시적으로 소개해 넣고싶은 경우가 자주 있습니다. 이런 경우에 필요한 것이 Generalize 전략입니다:

Coq < Section Predicate_Calculus.

Coq < Variable P,Q:nat->Prop. Variable R: nat->nat->Prop.
P is assumed
Q is assumed
R is assumed

Coq < Lemma PQR : (x,y:nat)((R x x)->(P x)->(Q x))->(P x)->(R x y)->(Q x).
1 subgoal

  P : nat->Prop
  Q : nat->Prop
  R : nat->nat->Prop
  ============================
   (x,y:nat)((R x x)->(P x)->(Q x))->(P x)->(R x y)->(Q x)

PQR < Intros.
1 subgoal

  P : nat->Prop
  Q : nat->Prop
  R : nat->nat->Prop
  x : nat
  y : nat
  H : (R x x)->(P x)->(Q x)
  H0 : (P x)
  H1 : (R x y)
  ============================
   (Q x)

PQR < Generalize H0.
1 subgoal

  P : nat->Prop
  Q : nat->Prop
  R : nat->nat->Prop
  x : nat
  y : nat
  H : (R x x)->(P x)->(Q x)
  H0 : (P x)
  H1 : (R x y)
  ============================
   (P x)->(Q x)

가끔은 보조정리를 쓰는 것이 편리할 때가 있습니다. 비록 이렇게 이미 증면된 사실을 호소할 직접적인 방법은 없지만 말이죠. Cut 전략을 쓰면 해당하는 증명 예정 대상을 새로운 서브골로 남겨두면서 보조정리를 쓸 수 있습니다:

Coq < Cut (R x x); Trivial.
1 subgoal

  P : nat->Prop
  Q : nat->Prop
  R : nat->nat->Prop
  x : nat
  y : nat
  H : (R x x)->(P x)->(Q x)
  H0 : (P x)
  H1 : (R x y)
  ============================
   (R x x)

1.4.5 동치(Equality)

Coq가 제공하는 기본적인 동치는 Leibniz 동치이며, xy가 같은 Set의 타입일 때 중위 표현법으로 x=y라고 씁니다. 어떤 텀에서든 xy로 대체(replacement)하는 것은 RewriteReplace 같은 다양한 전략들에 의해 나타납니다.

동치 대체의 몇가지 예를 보겠습니다. 어떤 산술 함수 f가 영(zero)에 대해서는 null 함수라고 가정합시다:

PQR < Variable f:nat->nat.
Warning: Variable f is not visible from current goals
f is assumed

PQR < Hypothesis foo : (f O)=O.
Warning: Variable foo is not visible from current goals
foo is assumed

다음과 같은 조건부 동치성을 증명하려합니다:

PQR < Lemma L1 : (k:nat)k=O->(f k)=k.

늘 그렇듯이, 우선 Intro를 써서 지역 가정들을 제거합니다:

L1 < Intros k E.
1 subgoal

  P : nat->Prop
  Q : nat->Prop
  R : nat->nat->Prop
  f : nat->nat
  foo : (f (0))=(0)
  k : nat
  E : k=(0)
  ============================
   (f k)=k

이제 left-to-right rewriting으로서 등식 E를 사용합시다:

L1 < Rewrite E.
1 subgoal

  P : nat->Prop
  Q : nat->Prop
  R : nat->nat->Prop
  f : nat->nat
  foo : (f (0))=(0)
  k : nat
  E : k=(0)
  ============================
   (f (0))=(0)

이렇게 해서 두 개의 k0으로 바꿨습니다. 이제 Apply foo를 하면 증명이 끝날겁니다:

L1 < Apply foo.
Subtree proved!

L1 < Save.
Intros k E.
Rewrite E.
Apply foo.
L1 is defined

만일 오른쪽에서 왼쪽으로 바꾸고싶은 경우에는, Rewrite E나 그와 동치인 Rewrite -> E를 쓰는 대신 Rewrite <- E를 써야합니다. 이제 Replace 전략을 살펴봅시다.

PQR < Hypothesis f10 : (f (S O))=(f O).
Warning: Variable f10 is not visible from current goals
f10 is assumed

PQR < Lemma L2 : (f (f (S O)))=O.
1 subgoal

  P : nat->Prop
  Q : nat->Prop
  R : nat->nat->Prop
  f : nat->nat
  foo : (f (0))=(0)
  f10 : (f (1))=(f (0))
  ============================
   (f (f (1)))=(0)

L2 < Replace (f (S O)) with O.
2 subgoals

  P : nat->Prop
  Q : nat->Prop
  R : nat->nat->Prop
  f : nat->nat
  foo : (f (0))=(0)
  f10 : (f (1))=(f (0))
  ============================
   (f (0))=(0)
subgoal 2 is:
 (0)=(f (1))

이 교환에 의해 첫번째 서브골은 증명될 수 있는 형태가 되었지만, Replace 전략에 의해 또다른 증명 예정물이 두번째 서브골로서 만들어졌습니다. 첫번째 서브골은 보조정리 foo를 적용하여 즉시 해결할 수 있습니다. 두번째 서브골은 Transitivity 전략과 Symmetry 전략을 이용해서 동치의 추이성과 대칭성을 통해 해결합니다:

L2 < Apply foo.
1 subgoal

  P : nat->Prop
  Q : nat->Prop
  R : nat->nat->Prop
  f : nat->nat
  foo : (f (0))=(0)
  f10 : (f (1))=(f (0))
  ============================
   (0)=(f (1))

L2 < Transitivity (f O); Symmetry; Trivial.
Subtree proved!

Replace u with t에 의해 생성된 동치 t=u가 가정(modulo symmetry 등)일 경우, 이것은 자동적으로 증명되며 이에 따르는 해당 골은 나타나지 않습니다. 예를 들어:

L2 < Restart.
1 subgoal

  P : nat->Prop
  Q : nat->Prop
  R : nat->nat->Prop
  f : nat->nat
  foo : (f (0))=(0)
  f10 : (f (1))=(f (0))
  ============================
   (f (f (1)))=(0)

L2 < Replace (f O) with O.
1 subgoal

  P : nat->Prop
  Q : nat->Prop
  R : nat->nat->Prop
  f : nat->nat
  foo : (f (0))=(0)
  f10 : (f (1))=(f (0))
  ============================
   (f (f (1)))=(0)

L2 < Rewrite f10; Rewrite foo; Trivial.
Subtree proved!

L2 < Save.
Replace (f O) with O.
Rewrite f10; Rewrite foo; Trivial.
L2 is defined

1.4.6 타입에 대한 술어 논리

지금까지 수리적 Set 세계에서의 일계 추론(first-order reasoning)의 개괄에 대해 설명했습니다. 추상 타입의 수준에서도 비슷한 추론을 할 수 있습니다. 이런 추상 추론을 하려면 Logic_Type 라이브러리를 적재해야합니다.

Coq < Require Logic_Type.

이제 (EXT x | (P x))라는 구문으로 사용하는, 타입에 대한 존재한정사 exT 같은 새로운 증명 형성자를 사용할 수 있습니다. 이에 상응하는 소개 형성자는 위에서처럼 Exists 전략으로 가동시킬 수 있습니다.

Coq < Check exT_intro.
exT_intro
     : (A:Type; P:(A->Prop); x:A)(P x)->(exT A P)

마찬가지로, 타입에 대한 동치성도 M==N이라는 표현법으로 사용할 수 있습니다. 동치성에 관한 전략들은 ===에서와 같은 방식으로 처리합니다.

1.5 정의 사용하기

수학적인 개념을 형성하는 것은 단순히 첫번째 이론으로부터 논리적으로 뻗어나가 진행되는 것이 아니며, 정의(definition)가 핵심적인 방법으로 사용됩니다. 정형적인 증명 과정은 추상화 과정에 상반되는 과정입니다. 술어논리의 추상화된 문장들을 증명하고 정의를 사용하는 것에 비교할 때, 보다 구체적인 속성을 증명하는 데에 수학적인 값들의 내부 구조를 이용하기 위해서는 일반적인 문장에 특정 개념을 결합시켜 실체화시키곤 합니다.

1.5.1 정의 전개하기 (unfolding)

어떤 전체집합 U에 대한 특정 술어(predicate)로 나타나는 집합론을 만들고자한다고 가정합시다. 예를 들어:

Coq < Reset Initial.  Section Unfolding.


Coq < Variable U:Type.
U is assumed

Coq < Definition set := U->Prop.
set is defined

Coq < Definition element := [x:U][S:set](S x).
element is defined

Coq < Definition subset := [A,B:set](x:U)(element x A)->(element x B).
subset is defined

이제, 예를 들어 추이성(transitivity)처럼, 어떤 추상 타입 T에 관한 관계에 대한 일반적인 성질들의 모듈을 적재했다고 가정합니다:

Coq < Definition transitive := [T:Type][R:T->T->Prop]
Coq <                  (x,y,z:T)(R x y)->(R y z)->(R x z).
transitive is defined

subset은 추이성(transitivity)이 있는 관계임을 증명해 보겠습니다.

Coq < Lemma subset_transitive : (transitive set subset).
1 subgoal

  U : Type
  ============================
   (transitive set subset)

여기서 뭔가 더 진행하려면 transitive의 정의를 써야합니다. 현재 골에 있는 모든 정의된 개념을 그 정의 내용으로 교체해주는 전략인 Unfold를 여기서 사용합니다.

subset_transitive < Unfold transitive.
1 subgoal

  U : Type
  ============================
   (x,y,z:set)(subset x y)->(subset y z)->(subset x z)

이제 subset을 전개(unfold)해야합니다:

subset_transitive < Unfold subset.
1 subgoal

  U : Type
  ============================
   (x,y,z:set)
    ((x0:U)(element x0 x)->(element x0 y))
    ->((x:U)(element x y)->(element x z))
      ->(x0:U)(element x0 x)->(element x0 z)

여기서 element를 전개하는 것은 실책입니다. element를 그대로 추상 술어인 채로 두고도 Auto로 간단히 증거를 찾을 수 있기 때문입니다:

subset_transitive < Auto.
Subtree proved!

Coq는 Unfold를 다양하게 변형시킬 수 있게합니다. 예를 들어, 선택적으로 특정 대상 하나만을 지목하여 전개할 수도 있습니다:

subset_transitive < Undo 2.
1 subgoal

  U : Type
  ============================
   (x,y,z:set)(subset x y)->(subset y z)->(subset x z)

subset_transitive < Unfold 2 subset.
1 subgoal

  U : Type
  ============================
   (x,y,z:set)
    (subset x y)->((x:U)(element x y)->(element x z))->(subset x z)

지역 가설 속에 들어있는 정의도 in 표현법을 써서 전개할 수 있습니다:

subset_transitive < Intros.
1 subgoal

  U : Type
  x : set
  y : set
  z : set
  H : (subset x y)
  H0 : (x:U)(element x y)->(element x z)
  ============================
   (subset x z)

subset_transitive < Unfold subset in H.
1 subgoal

  U : Type
  x : set
  y : set
  z : set
  H : (x0:U)(element x0 x)->(element x0 y)
  H0 : (x:U)(element x y)->(element x z)
  ============================
   (subset x z)

마지막으로, Red 전략은 현재 골의 맨 앞에 출현하는 정의만을 전개합니다:

subset_transitive < Red.
1 subgoal

  U : Type
  x : set
  y : set
  z : set
  H : (x0:U)(element x0 x)->(element x0 y)
  H0 : (x:U)(element x y)->(element x z)
  ============================
   (x0:U)(element x0 x)->(element x0 z)

subset_transitive < Auto. Save.
Subtree proved!
Unfold transitive.
Unfold 2 subset.
Intros.
Unfold subset in H.
Red.
Auto.
subset_transitive is defined

1.5.2 Principle of proof irrelevance

비록 이론적으로는 어떤 검증된 보조정리(lemma)에 대한 증명 텀이 어떤 명세에 따라 정의된 값에 대응하긴 하지만, Coq에서 이런 정의는 전개할 수 없습니다: 보조정리는 불투명한(opaque) 정의이기 때문입니다. 이는 proof irrelevance라는 수학적 전통에 따른 것입니다: 논리 명제의 증명은 문제가 되지 않으며, 논리적인 개념 형성의 수학적 조정은 어디까지나 정형 증명에 사용되는 보조정리의 provability에만 의존합니다.

반대로, 평범한 수학적 정의들은 마음먹은 대로 전개시킬 수 있으며, 이들은 투명(transparent)합니다. 정의를 불투명하게 선언하거나 보조정리를 투명하게 선언함으로써 이와는 반대되는 관례를 강제로 만들 수도 있습니다.

제 2 장 : 귀납법

2.1 귀납적으로 정의된 수학적 집합물로서의 자료형

지금까지 공부한 모든 개념들은 전통적인 수리 논리를 따르고 있었습니다. 객체의 명세는 다소 구성주의적인 방법으로 추론하는 데에 사용되는 추상적인 특질이었습니다. 이제 수학적으로 견고하게 구성할 수 있는 존재를 명세하는 귀납적 타입의 영역으로 들어가겠습니다.

2.1.1 Booleans

Coq의 Prelude 모듈에 명세되어 있는 불리언 타입으로 시작해보겠습니다:

Coq < Inductive bool : Set := true : bool | false : bool.
bool is defined
bool_rect is defined
bool_ind is defined
bool_rec is defined

이런 선언은 몇 가지 대상을 한꺼번에 정의합니다. 먼저 bool이라는 이름의 새로운 Set이 선언됩니다. 다음, 이 Set구성자(constructor)truefalse라는 이름으로 선언됩니다. 이는 새로운 Set bool의 소개 규칙과 유사합니다. 마지막으로, bool 값에 따라 경우를 나눠 추론할 수 있게 해주는 bool만의 특정한 제거 규칙들이 만들어집니다. 전역 문맥 속에 세 가지 실체들이 새로운 조합자(combinator)로서 실제로 정의됩니다: 경우에 따라 추론하는 데에 해당하는 증명 조합자인 bool_ind과 if-then-else 프로그래밍 재료인 bool_rec, 그리고 타입 수준에서 이와 비슷한 조합자로 작동하는 bool_rect입니다. 실제로 확인해보면:

Coq < Check bool_ind.
bool_ind
     : (P:(bool->Prop))(P true)->(P false)->(b:bool)(P b)

Coq < Check bool_rec.
bool_rec
     : (P:(bool->Set))(P true)->(P false)->(b:bool)(P b)

Coq < Check bool_rect.
bool_rect
     : (P:(bool->Type))(P true)->(P false)->(b:bool)(P b)

예를 들 겸, 모든 불리언들은 참이거나 거짓임을 증명해봅시다.

Coq < Lemma duality : (b:bool)(b=true \/ b=false).
1 subgoal

  ============================
   (b:bool)b=true\/b=false

duality < Intro b.
1 subgoal

  b : bool
  ============================
   b=true\/b=false

Elim 전략을 써서 bbool이라는 점을 사용합니다. 이 경우, Elim은 증명 과정을 두 가지 경우에 따라 나누기 위해 bool_ind 구성자를 적용합니다:

duality < Elim b.
2 subgoals

  b : bool
  ============================
   true=true\/true=false
subgoal 2 is:
 false=true\/false=false

각각의 경우마다 결론을 쉽게 내릴 수 있습니다:

duality < Left; Trivial.
1 subgoal

  b : bool
  ============================
   false=true\/false=false

duality < Right; Trivial.
Subtree proved!

사실, 이 경우에 전체 증명 과정은 IntroElim을 결합시켜주는 Induction전략과 예전부터 써 오던 Auto 전략으로 해결할 수 있습니다:

duality < Restart.
1 subgoal

  ============================
   (b:bool)b=true\/b=false

duality < Induction b; Auto.
Subtree proved!

duality < Save.
Induction b; Auto.
duality is defined

2.1.2 자연수

불리언과 마찬가지로, 자연수도 Prelude 모듈에 생성자 SO로 정의되어 있습니다:

Coq < Inductive nat : Set := O : nat | S : nat->nat.
nat is defined
nat_rect is defined
nat_ind is defined
nat_rec is defined

자동 생성되는 제거 원리는 Peano 귀납법과 재귀 연산자입니다:

Coq < Check nat_ind.
nat_ind
     : (P:(nat->Prop))(P O)->((n:nat)(P n)->(P (S n)))->(n:nat)(P n)

Coq < Check nat_rec.
nat_rec
     : (P:(nat->Set))(P O)->((n:nat)(P n)->(P (S n)))->(n:nat)(P n)

좀더 일반적인 nat_rec으로부터 어떻게 표준 원시 재귀 연산자 prim_rec을 프로그램하는지 보겠습니다:

Coq < Definition prim_rec := (nat_rec [i:nat]nat).
prim_rec is defined

즉, 인덱스된 Set(P i)의 원소를 자연수 i에 대해서 계산하는 대신, prim_recnat의 원소를 균일하게 계산합니다. prim_rec의 타입을 검사해봅시다:

Coq < Check prim_rec.
prim_rec
     : ([_:nat]nat O)
       ->((n:nat)([_:nat]nat n)->([_:nat]nat (S n)))
         ->(n:nat)([_:nat]nat n)

이런! 기대했던 타입 nat->(nat->nat->nat)->nat->nat 대신 훨씬 복잡한 표현식이 나왔습니다. 사실 prim_rec의 타입은 기대했던 타입과 β 규칙에 의해서 동치입니다. 표현식을 자신의 normal form으로 β-reduce시켜주는 명령인 Eval Cbv Beta로 이런 사실을 확인해볼 수 있습니다:

Coq < Eval Cbv Beta in
Coq <      ([_:nat]nat O)
Coq <         ->((y:nat)([_:nat]nat y)->([_:nat]nat (S y)))
Coq <            ->(n:nat)([_:nat]nat n).
     = nat->(nat->nat->nat)->nat->nat
     : Set

이제 원시 재귀를 써서 덧셈을 프로그램하는 방법을 보겠습니다:

Coq < Definition addition := [n,m:nat](prim_rec m [p:nat][rec:nat](S rec) n).
addition is defined

즉, (addition n m)n의 주 형성자(main constructor)의 경우에 따라 나눠서 계산한다고 명세한 것입니다: n=O일 경우에는 m을 얻고, n=(S p)일 경우에는 (S rec)을 얻게되며, 여기서 rec은 재귀적으로 계산된 (addition p m)의 결과입니다. 2+3을 계산하게하여 이 점을 확인해봅시다:

Coq < Eval Compute in (addition (S (S O)) (S (S (S O)))).
     = (S (S (S (S (S O)))))
     : ([_:nat]nat (S (S O)))

사실, 명시적으로 이 모든 것들은 해줄 필요는 없었습니다. Coq는 일반적인 원시 재귀를 위해서 Fixpoint/Cases라는 특수 구문을 제공하며, 덧셈을 다음과 같이 직접 정의할 수 있었던 것입니다:

Coq < Fixpoint plus [n:nat] : nat -> nat :=
Coq <    [m:nat]Cases n of
Coq <              O    => m
Coq <           | (S p) => (S (plus p m))
Coq <           end.
plus is recursively defined

앞으로는, Coq의 Prelude 모듈이 제공하는 초기 정의를 사용하고 우리가 방금 했던 재정의에 의한 에러 메세지들을 받지 않기 위해서, bool 타입과 nat 타입을 가지고 지금까지 했던 것들을 지우겠습니다. Reset 명령으로 우리가 bool을 정의하기 이전 상태로 되돌아갑니다:

Coq < Reset bool.

2.1.3 귀납법에 의한 증명

이제 structural induction을 통해 증명하는 방법을 보여드리겠습니다. 방금 정의한 plus 함수의 간단한 특성 하나를 보도록 합니다. 먼저 n = n + 0을 확인합니다.

Coq < Lemma plus_n_O : (n:nat)n=(plus n O).
1 subgoal

  ============================
   (n:nat)n=(plus n (0))

plus_n_O < Intro n; Elim n.
2 subgoals

  n : nat
  ============================
   (0)=(plus (0) (0))

subgoal 2 is:
 (n0:nat)n0=(plus n0 (0))->(S n0)=(plus (S n0) (0))

nat 타입의 n으로부터 원래 골의 타입인 Prop을 만들기 위해서 Elim n을 수행했고, 이는 대응하는 귀납 원리이자 사실상 Peano의 귀납 체계임을 이미 보았던 nat_ind에 의존합니다. 패턴 매칭에 의해 [n:nat]n=(plus n O)에 해당하는 술어 P의 실체가 만들어지고, 기준 경우인 (P O)와 귀납 단계인 (y:nat)(P y)->(P (S y))에 각각 해당하는 서브골을 얻게됩니다. 각각의 경우마다 두 번째 인수가 형성자(constructor)로 시작하는 plus 함수의 실체를 얻게되고, 따라서 원시재귀를 써서 간략화시킬 수 있습니다. Coq의 Simpl 전략을 이런 용도로 쓸 수 있습니다:

plus_n_O < Simpl.
2 subgoals

  n : nat
  ============================
   (0)=(0)
subgoal 2 is:
 (n0:nat)n0=(plus n0 (0))->(S n0)=(plus (S n0) (0))

plus_n_O < Auto.
1 subgoal

  n : nat
  ============================
   (n0:nat)n0=(plus n0 (0))->(S n0)=(plus (S n0) (0))

기본 단계에서와 마찬가지 과정을 거칩니다:

plus_n_O < Simpl; Auto.
Subtree proved!

plus_n_O < Save.
Intro n; Elim n.
Simpl.
Auto.
Simpl; Auto.
plus_n_O is defined

여기서 Auto가 성공한 것은, 계승(successor)은 동치성을 유지한다는 보조정리인 eq_S를 힌트로서 사용했기 때문입니다:

Coq < Check eq_S.
eq_S
     : (x,y:nat)x=y->(S x)=(S y)

실제로, Auto로 하여금 우리의 보조정리 plus_n_O를 힌트로서 사용할 수 있도록 선언하는 방법을 알아봅시다:

Coq < Hints Resolve plus_n_O.

이제 또다른 형성자인 S에 관한 비슷한 성질을 가지고 진행하겠습니다:

Coq < Lemma plus_n_S : (n,m:nat)(S (plus n m))=(plus n (S m)).
1 subgoal

  ============================
   (n,m:nat)(S (plus n m))=(plus n (S m))

이번에는 Induction 전략이 Elim을 적용하기 전에 필요한 Intros를 실행해준다는 사실을 기억하면서 좀 더 빨리 진행해봅시다. 간략화와 자동화 전략을 조합하는 기능 덕분에, 이 보조정리를 한 줄로 증명할 수 있습니다:

plus_n_S < Induction n; Simpl; Auto.
Subtree proved!

plus_n_S < Save.
Induction n; Simpl; Auto.
plus_n_S is defined

Coq < Hints Resolve plus_n_S.

마지막 연습으로 plus의 교환 법칙을 생각해봅시다:

Coq < Lemma plus_com : (n,m:nat)(plus n m)=(plus m n).
1 subgoal

  ============================
   (n,m:nat)(plus n m)=(plus m n)

대칭적 상황이기 때문에, 여기서 귀납법을 n에 대해서 수행할지 m에 대해서 수행할지 선택할 수 있습니다. 예를 들어:

plus_com < Induction m; Simpl; Auto.
1 subgoal

  n : nat
  m : nat
  ============================
   (n0:nat)(plus n n0)=(plus n0 n)->(plus n (S n0))=(S (plus n0 n))

우리가 준 힌트 plus_n_O 덕분에 기준 단계에 대해서는 Auto가 성공했지만, 재귀 단계에 대해서는 Auto가 다룰 수 없는 rewriting이 필요합니다:

plus_com < Intros m' E; Rewrite <- E; Auto.
Subtree proved!

plus_com < Save.
Induction m; Simpl; Auto.
Intros m' E; Rewrite <- E; Auto.
plus_com is defined

2.1.4 Discriminate

원시 재귀를 써서 새로운 명제를 정의하는 것도 가능합니다. 예를 들어, 형성자 OS를 식별(discriminate)하는 술어를 정의해봅시다: 이 술어는 인수가 O일 경우 False로, 인수가 (S n) 형태일 경우 True로 계산됩니다:

Coq < Definition Is_S
Coq <       := [n:nat]Cases n of O => False | (S p) => True end.
Is_S is defined

이제 (Is_S (S n))를 증명하기 위해서 Is_S의 계산 능력을 사용할 수 있습니다:

Coq < Lemma S_Is_S : (n:nat)(Is_S (S n)).
1 subgoal

  ============================
   (n:nat)(Is_S (S n))

S_Is_S < Simpl; Trivial.
Subtree proved!

S_Is_S < Save.
Simpl; Trivial.
S_Is_S is defined

이것을 False 골을 (Is_S O)로 변형시키기 위해서 사용할 수도 있습니다. 이 기능의 특히 중요한 사용법을 보여드리겠습니다. Peano의 공리 중 하나인, OS는 서로 다른 값을 형성(construct)한다는 사실을 증명하고자 합니다:

Coq < Lemma no_confusion : (n:nat)~(O=(S n)).
1 subgoal

  ============================
   (n:nat)~(0)=(S n)

우선, 골을 Red 전략으로 reduce하여 부정(negation)을 그 정의에 따라 치환합니다. 그 다음, 몇 번의 Intros를 통해 모순을 얻게됩니다:

no_confusion < Red; Intros n H.
1 subgoal

  n : nat
  H : (0)=(S n)
  ============================
   False

이제, 아까 말했던 트릭을 사용합니다:

no_confusion < Change (Is_S O).
1 subgoal

  n : nat
  H : (0)=(S n)
  ============================
   (Is_S (0))

True로 계산되어 증명을 끝마치게 해주는 서브골을 얻기 위해 동치성을 사용합니다:

no_confusion < Rewrite H; Trivial.
1 subgoal

  n : nat
  H : (0)=(S n)
  ============================
   (Is_S (S n))

no_confusion < Simpl; Trivial.
Subtree proved!

사실, Discriminate 전략은 사용자로 하여금 명시적으로 적절한 식별 술어를 정의할 필요가 없도록 하면서 기계적으로 이런 증명을 만들기 위해 제공되는 것입니다:

no_confusion < Restart.
1 subgoal

  ============================
   (n:nat)~(0)=(S n)

no_confusion < Intro n; Discriminate.
Subtree proved!

no_confusion < Save.
Intro n; Discriminate.
no_confusion is defined

2.2 논리 프로그래밍

위에서 표준 자료형을 정의했던 것과 같은 방식으로, 예를 들어 귀납적 술어 같은 귀납적 대상들도 정의할 수 있습니다. 아래에 보이는 정의는 Coq의 Prelude 모듈에 나와있는, nat 타입에 대한 술어 ≤의 정의입니다:

Coq < Inductive le [n:nat] : nat -> Prop
Coq <    := le_n : (le n n)
Coq <     | le_S : (m:nat)(le n m)->(le n (S m)).

이 정의는 새로운 술어 le:nat->nat->Prop과, le의 정의 구절인 두 형성자 le_nle_S를 소개합니다. 즉, "공리" le_nle_S 뿐만 아니라, 이와 상통하는 성질인 '이들 정의 구절들의 귀결로서 얻어지면, 그리고 얻어질 때에만 (le n m)이다'라는 사실도 얻게되는 것입니다. 즉, le는 구절 le_nle_S를 검증하는 가장 작은 술어입니다. 이런 사실은 귀납적 자료형의 경우에서처럼 이 최소성을 설명해주는 제거(elimination) 원리에 의해 보증되며, 여기서 이 제거 원리는 결국 le_ind라는 귀납 원리에 해당합니다:

Coq < Check le.
le
     : nat->nat->Prop

Coq < Check le_ind.
le_ind
     : (n:nat; P:(nat->Prop))
        (P n)
        ->((m:nat)(le n m)->(P m)->(P (S m)))
        ->(n0:nat)(le n n0)->(P n0)

이 원리로 증명을 이끌어내는 방법을 보여드리겠습니다. 우선 nmn+1 ≤ m+1임을 보여드립니다:

Coq < Lemma le_n_S : (n,m:nat)(le n m)->(le (S n) (S m)).
1 subgoal

  ============================
   (n,m:nat)(le n m)->(le (S n) (S m))

le_n_S < Intros n m n_le_m.
1 subgoal

  n : nat
  m : nat
  n_le_m : (le n m)
  ============================
   (le (S n) (S m))

le_n_S < Elim n_le_m.
2 subgoals

  n : nat
  m : nat
  n_le_m : (le n m)
  ============================
   (le (S n) (S n))
subgoal 2 is:
 (m0:nat)(le n m0)->(le (S n) (S m0))->(le (S n) (S (S m0)))

여기서 일어난 일은 자연수에 대한 Elim의 동작과 비슷합니다. Elim은 해당 귀납 원리(여기서는 le_ind)에 문의하게 되고, 이 귀납 원리는 두 개의 서브골을 만들며, 이 서브골들은 le의 정의 구절의 도움으로 쉽게 해결될 수 있습니다.

le_n_S < Apply le_n; Trivial.
1 subgoal

  n : nat
  m : nat
  n_le_m : (le n m)
  ============================
   (m0:nat)(le n m0)->(le (S n) (S m0))->(le (S n) (S (S m0)))

le_n_S < Intros; Apply le_S; Trivial.
Subtree proved!

정의 구절을 힌트로 주는 것은 좋은 생각입니다. 이렇게 하면 InductionAuto의 간단한 조합만으로도 증명을 진행할 수 있게됩니다.

le_n_S < Restart.
1 subgoal

  ============================
   (n,m:nat)(le n m)->(le (S n) (S m))

le_n_S < Hints Resolve le_n le_S.

하지만, 약간의 문제가 있습니다. "가설 (le n m)에 대해서 귀납법을 수행하라"라고 말하고 싶은건데, 이 가설에 적절한 이름이 없습니다. 이런 경우에는 다음과 같이 "이름이 없는 첫번째 가설에 대해서 귀납법을 수행하라"라고 말해야합니다.

le_n_S < Induction 1; Auto.
Subtree proved!

le_n_S < Save.
Induction 1; Auto.
le_n_S is defined

다음은 좀 더 미묘한 문제입니다. n ≤ 0 ⇒ n = 0임을 보이려한다고 가정합시다. 이런 추론은 le의 오직 첫번째 정의 구절만 적용한다는 사실로부터 나와야합니다.

Coq < Lemma tricky : (n:nat)(le n O)->n=O.
1 subgoal

  ============================
   (n:nat)(le n (0))->n=(0)

하지만, 여기서 Induction 1 같은 것을 시도해도 아무것도 얻을 수 없습니다. (실제로 한 번 해보고 무슨 일이 일어나는지 확인하시기 바랍니다.) n에 대한 귀납법도 역시 별로 편하지 않습니다. 지금 해야하는 일은, 가설 (le n (0))를 정의구절과 매치시키기 위해 le의 정의를 분석하고, le_n만 적용하여 결론이 도출됨을 찾는 것입니다. 다음과 같이 '여환법(戾換法, inversion)' 전략인 Inversion_clear를 통해 이 분석을 수행합니다:

tricky < Intros n H; Inversion_clear H.
1 subgoal

  n : nat
  ============================
   (0)=(0)

tricky < Trivial.
Subtree proved!

tricky < Save.
Intros n H; Inversion_clear H.
Trivial.
tricky is defined

제 3 장 : 모듈

3.1 라이브러리 모듈 열기

명령행에서 별다른 추가 요구 없이 Coq를 시작하면, 극히 일부 라이브러리들만 적재된 빈털털이 시스템이 나타납니다. 지금까지 살펴봤듯이 표준 prelude 모듈은 표준 논리 연산과 산술 명칭들만 제공합니다. 라이브러리의 모듈을 적재하고 열려면 이전에 수리논리 부분에서 본 것처럼 Require 명령을 써야합니다. 예를 들어, 산술 연산이 더 필요하다면 다음과 같이 해야합니다:

Coq < Require Arith.

이런 명령은 Coq가 등록한 라이브러리에서 (컴파일된) 모듈 파일인 Arith.vo를 찾습니다. 라이브러리는 운영체제의 파일 시스템 구조를 상속받으며 Add LoadPath 명령으로 등록합니다. 물리적 디렉토리는 논리적 디렉토리에 대응됩니다. 특히 Coq의 표준 라이브러리는 Coq라는 이름의 라이브러리로 기등록(pre-registered)되어 있습니다. 모듈들은 Coq의 라이브러리 속에서 자신의 위치를 알려주는 절대적인 고유 명칭을 갖습니다. 절대 명칭은 마침표로 구분된 단일 인식명들의 나열입니다. 예를 들어, Arith 모듈의 전체 이름은 Coq.Arith.Arith이며, 표준 라이브러리 중 Arith라는 원조 하위디렉토리에 들어있기 때문에 다음과 같은 명령으로도 불러올 수 있습니다:

Coq < Require Coq.Arith.Arith.

Coq가 알고 있는 어떤 다른 라이브러리 줄기 속에서 또다른 모듈도 Arith라고 불리고있을 경우, 모호함을 피하는 데에 위와 같은 방식이 유용합니다. 라이브러리가 등록되면, 기본적으로 그 라이브러리의 모든 내용물과 그 (재귀적으로 모든) 하위 디렉토리들의 내용물까지 전부 보이게 되며, Arith 같은 짧은 (상대) 명칭으로 접근할 수 있음을 알아두십시오. 또한, 라이브러리에 명시적으로 등록되지 않은 모듈이나 정의들은 Scratch라고 불리는 디폴트 라이브러리에 들어간다는 점에도 주의하시기 바랍니다.

컴파일된 파일은 빠르게 적재되며, 이것은 이에 수반되는 개발 과정에서 타입 검사를 다시 하지 않기 때문입니다.

경고: Coq는 아직 parametric module을 제공하지 않습니다.

3.2 자신의 모듈 만들기

my_module.v 같은 파일에 Coq 명령들을 적어서 당신 자신의 모듈을 만들 수도 있습니다. Load my_module 명령으로 이런 모듈을 현재 문맥 속에 간단히 적재할 수 있습니다. 이런 모듈을 컴파일할 수도 있으며, Compile Module my_module 명령을 Coq toplevel에서 직접 써도 되고, 혹은 coqc라는 UNIX 명령으로 "batch" 모드에서 할 수도 있습니다. 모듈 my_module.v를 컴파일하면 Require my_module 명령으로 적재할 수 있는 파일 my_module.vo가 만들어집니다.

만일 요청한 모듈이 또다른 모듈들에 의존하고 있다면 이런 또다른 모듈들은 먼저 자동적으로 요청(require)됩니다. 하지만 그 내용물은 자동으로 보이지(visible) 않습니다. 만일 모듈 N 속에서 요청하고있는 모듈 MN이 요청될 때 자동적으로 보이게끔 하고싶으면, 모듈 N 속에서 Require Export M이라고 해야합니다.

3.3 문맥 다루기

현재 문맥 속에서 사용 가능한 모든 보조정리들과 정의들의 이름을 모두 외우는 것은 어려운 일이며, 특히 커다란 라이브러리가 적재됐을 경우에는 심각한 문제입니다. 주어진 술어(predicate)가 관여하는 모든 알려진 사실들을 알아보기 위해 Search라는 편리한 명령을 사용할 수 있습니다. 예를 들어, 작거나 같은 관계에 대해 알려진 모든 보조정리들을 보고싶으면 다음과 같이 물어보면 됩니다:

Coq < Search le.
Top.le_n_S: (n,m:nat)(le n m)->(le (S n) (S m))
le_n: (n:nat)(le n n)
le_S: (n,m:nat)(le n m)->(le n (S m))

Yves Bertot가 개발한 SearchPattern이라는 더 편리한 새 검색 도구가 있습니다. 주어진 패턴과 결론이 대응되는 정리를을 찾을 수 있으며, 패턴 속에서 임의의 term 자리에 ?를 사용할 수 있습니다.

Coq < SearchPattern (plus ? ?)=?.
le_plus_minus_r: (n,m:nat)(Peano.le n m)->(plus n (minus m n))=m
mult_acc_aux: (n,s,m:nat)(plus s (mult n m))=(mult_acc s m n)
plus_sym: (n,m:nat)(plus n m)=(plus m n)
plus_Snm_nSm: (n,m:nat)(plus (S n) m)=(plus n (S m))
plus_assoc_l: (n,m,p:nat)(plus n (plus m p))=(plus (plus n m) p)
plus_permute: (n,m,p:nat)(plus n (plus m p))=(plus m (plus n p))
plus_assoc_r: (n,m,p:nat)(plus (plus n m) p)=(plus n (plus m p))
plus_permute_2_in_4:
  (a,b,c,d:nat)
   (plus (plus a b) (plus c d))=(plus (plus a c) (plus b d))
plus_tail_plus: (n,m:nat)(plus n m)=(tail_plus n m)
plus_O_n: (n:nat)(plus (0) n)=n
plus_Sn_m: (n,m:nat)(plus (S n) m)=(S (plus n m))
mult_n_Sm: (n,m:nat)(plus (mult n m) n)=(mult n (S m))
plus_com: (n,m:nat)(plus n m)=(plus m n)

3.4 이제 알아서 하시죠

이 튜토리얼은 불완전할 수밖에 없습니다. Coq로 심각한 증명을 하고자한다면 지금부터는 Coq's Reference Manual을 참조하셔야합니다. 여기에는 지금까지 보아온 모든 tactic들과 그 외의 많은 것들에 대한 완전한 설명이 들어있습니다. 또한, 다양한 증명 기법들에 정통하기 위해서는 Coq와 함께 배포된 이미 증명된 이론의 라이브러리들을 들여다봐야할 것입니다.


  1. This research was partly supported by ESPRIT Basic Research Action "Types". (1)

  2. 람다 함수 λxA.e를 생각하시면 됩니다 — 역자 주 (2)

  3. Natural deduction 과정상 이 전략은 결국 함축 연산자를 소개하는 규칙, 즉, implication introduction rule에 해당합니다 — 역자 주 (3)