====== 증명 보조도구 Coq 입문서 ====== Version 7.3((This research was partly supported by ESPRIT Basic Research Action "Types".)) 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://ftp.inria.fr/|ftp.inria.fr]]''의 디렉토리 ''[[ftp://ftp.inria.fr/INRIA/coq/V7.3|INRIA/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 문자가 따라나오는 문자열입니다. 대소문자를 가리므로 ''A''와 ''a''는 서로 다른 명칭입니다. 몇몇 문자열들은 Coq의 키워드로 예약되어있어서 사용자가 인식명으로 쓸 수 없습니다. 명세란 지금 선언하고있는 개념을 분류해주는 정형적인 표현식입니다. 기본적으로 세 종류의 명세가 있으며, **logical propositions**, **mathematical collections**, 그리고 **abstract types**입니다. 이들은 각각 ''Prop'', ''Set'', ''Type''이라고 불리는 기본적인 시스템 종류에 따라 분류되며, 이들 자신은 원소(atomic) 추상자료형(abstract types)입니다. Gallina에서 모든 유효한 표현식 //e//는 그 표현식의 **타입** τ(//E//)라고 불리는 (그리고 그 자신도 다시 유효한 표현식인) 명세와 연관됩니다. //e//가 //E// 타입이라는 것을 우리는 //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 이로써 ''gt''가 ''nat'' 타입의 인수 두 개를 받아서 논리적 명제를 만드는 함수라는 것을 알 수 있습니다. 여기서 일어난 일은 함수형 프로그래밍 언어에서 익히 일어나는 일과 같은 것입니다: (명세) 타입 ''nat''과 logical propositions의 (추상) 타입 ''Prop''을 함수 형성자인 화살표로 연결해서 ''nat''->''Prop''이라는 함수 타입을 만들 수 있습니다: Coq < Check nat->Prop. nat->Prop : Type 그리고 이 타입을 다시 ''nat''과 연결하여 자연수에 관한 이항 관계 타입인 ''nat''->''nat''->''Prop''을 얻습니다. 사실 ''nat''->''nat''->''Prop''은 ''nat''->(''nat''->''Prop'')의 축약형입니다. 함수 개념에 대해서는 그저 일반적으로 생각하시면 됩니다. //A//->//B// 타입의 표현식 //f//는 //A// 타입의 표현식 //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 대괄호에 대해서 설명하겠습니다. //x//가 //A// 타입이라고 선언하고 있는 문맥 안에서 //e//가 올바른 //B// 타입의 표현식이라면 [//x//://A//]//e//라는 표현식은 그 문맥 안에서 올바른 //A//->//B// 타입입니다.((람다 함수 λ//x////A//.//e//를 생각하시면 됩니다 --- 역자 주)) 표현식 [//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 //A//->//B// 같은 간단한 논리적 함축에 대해서 생각해봅시다. //A//->//B//는 "//A// implies //B//."라고 읽습니다. 지금까지 함수 형성자로 써오던 화살표 기호를 명제 연산자로도 사용하도록 오버로드한다는 점에 주목하시기 바랍니다: Coq < Check A->B. A->B : Prop 이제 간단한 증명을 시작해봅시다. 쉽게 이해할 수 있는 항진명제 (//A//->(//B//->//C//%%))%%->(//A//->//B//)->(//A//->//C//)를 증명해보겠습니다. 검증하고자하는 추측과 함께 ''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 여러 개의 소개((Natural deduction 과정상 이 전략은 결국 함축 연산자를 소개하는 규칙, 즉, implication introduction rule에 해당합니다 --- 역자 주))를 한 번에 수행할 수 있습니다: Unnamed_thm < Intros H' HA. 1 subgoal A : Prop B : Prop C : Prop H : A->B->C H' : A->B HA : A ============================ C 현재 골이 된 ''C''는, ''A''와 ''B''를 증명할 수 있다는 가정 하에 가설 ''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**를 써서 몇 개의 전략들을 직렬 혹은 병렬로 조합할 수 있습니다. 주요 구성은 다음과 같습니다: * //T//1; //T//2는 현재 골에 //T//1을 적용한 후 //T//1에 의해 만들어진 서브골들 모두에 //T//2를 적용합니다. ( "//T//1 then //T//2."라고 읽습니다.) * //T//; [//T//1 | //T//2 | ... | //T//n]은 현재 골에 //T//를 적용한 후 새로 만들어진 서브골 중 첫번째 서브골에 //T//1, 두번째 서브골에 //T//2, ..., n번째 서브골에 //T//n을 적용합니다. 따라서 ''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'' 명령에 인수로 넣어서 이 명칭을 덮어쓸 수도 있습니다. 사실은, ''Intro''나 ''Apply'', ''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) === 지금까지 함축문을 증명하기 위해서 ''Intro''와 ''Apply'' 전략이 조합되는 것을 보았습니다. 좀 더 일반적으로 말해서, 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 연어 가설 ''H''를 ''Elim'' 전략을 써서 그 구성 요소들로 분해합니다: 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 이접 접속사에는 두 개의 소개 규칙이 있습니다. //P//∨//Q//는 //P//로부터 얻을 수도 있고 //Q//로부터 얻을 수도 있기 때문이죠. 이런 두 가지 증명 형성자는 각각 ''or_introl''과 ''or_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''에 해당합니다. 추가 인수 ''B''와 ''A''는 ''or_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의 정리는 불리언 논리체계에서는 참입니다. 즉, 이 정리는 ''A''와 ''B''에 대응되는 모든 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이라는 것이 있습니다. 회원제 클럽에 다음과 같은 규칙이 있습니다: - 스코틀랜드인이 아닌 모든 회원은 빨간 양말을 신는다 - 모든 회원들은 킬트를 입던가 혹은 빨간 양말을 안 신는다 - 결혼한 회원은 일요일에 싸돌아다니지 않는다 - 스코틀랜드인 회원이라면, 그리고 스코틀랜드인 회원인 경우에만 일요일에 싸돌아다닌다. - 킬트를 입는 회원은 모두 결혼한 스코틀랜드인이다 - 모든 스코틀랜드인 회원은 킬트를 입는다 자, 이런 규칙은 아무도 따를 수 없는 불가능한 규칙임을 보여드리겠습니다. 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'' 위의 두 빈위기호 ''P''와 ''R''을 생각해보겠습니다. 이런 추상 요소는 문맥 속에 전역 변수로 포함됩니다. 하지만, 우리의 전역 환경을 이런 선언들로 오염시킬 때에는 항상 주의해야합니다. 예를 들어, 우리는 이미 ''n'', ''Pos_n'', ''A'', ''B'', ''C''등의 변수를 선언함으로써 우리의 Coq 세션을 오염시켜 놓았습니다. 초기 세션의 깨끗한 상태로 돌아가려면 ''Reset'' 명령을 써야하며, 이 명령은 구획을 지우기 전에 했던 전역 개념이 만들어지기 이전 상태로 돌아가게합니다. 혹은, 다음 명령으로 완전히 초기 상태로 돌아갈 수도 있습니다: Coq < Reset Initial. 이제 새로운 구획(section)을 선언하여 지역적으로 잘 경계지어진 구역 안에서 개념들을 정의할 수 있도록 합니다. 추론의 정의구역인 ''D''와 ''D''에 대한 이항 관계인 ''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)''라는 구문은 전체한정 ∀//x////D//를 의미함을 상기하시기 바랍니다. === 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)함으로써 ''P''에 ''a:D''라는 증명이 제공되며, 이 때 실제로 ''a''가 ''P''를 만족시킨다는 가설 ''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) 이제 ''x''의 R-successor인 ''y''를 내도록 존재 가설 ''x_Rlinked''를 사용합시다. 이 과정은 ''Elim''과 ''Intros''의 두 단계로 진행됩니다. 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'' 전략은 어떻게 ''x''를 ''x''에 대응시키고 ''z''를 ''x''에 대응시킬지 알고 있습니다만, ''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_if''는 ''Predicate_calcaulus''라는 구획 안에 선언된 일계언어의 일반적인 정리가 되었다는 일종의 경고입니다. 위 예제에서 ''R_sym_trans'' 구획을 사용한 것은 사실은 그다지 꼭 필요한 것은 아니었습니다. ''R_symmetric''과 ''R_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''가 존재한다는 가설 하에서 관계 ''R''은 ''refl_if''에 대해서만 해제되었으며, ''P''는 ''weird''와 ''drinker''에 대해서만 해제되었습니다. 마지막으로, excluded middle 가설은 ''drinker''에 대해서만 해제되었습니다. ''weird''와 ''drinker'' 문장에서 ''d''라는 명칭도 사라졌음에 주의하십시오. Coq의 pretty-printer는 ''d''가 ''E'' 속에 등장하지 않는 ''(d:D)E'' 같은 한정을 함수형 표현법인 ''%%D->E%%''로 체계적으로 바꿔주기 때문입니다. 마찬가지로 ''drinker'' 속에 ''EM''이라는 명칭은 나타나지 않습니다. 실제로, 전체한정, 함축(implication), 그리고 함수 형성은 모두 타입 이론상의 한 가지 일반화된 생성자인 **dependent product**의 특수한 경우들일 뿐입니다. 이것은 인덱스된 함수 계열에 해당하는 수학적 생성법입니다. 함수 //f// ∈ Π//x////D//.//C// //x//는 자신의 정의역의 원소인 //x//를 (인덱스된) 공변역 //C// //x//에 대응시킵니다. 따라서 ∀//x////D//.//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 동치이며, //x//와 //y//가 같은 Set의 타입일 때 중위 표현법으로 //x//=//y//라고 씁니다. 어떤 텀에서든 //x//를 //y//로 대체(replacement)하는 것은 ''Rewrite''나 ''Replace'' 같은 다양한 전략들에 의해 나타납니다. 동치 대체의 몇가지 예를 보겠습니다. 어떤 산술 함수 //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) 이렇게 해서 두 개의 ''k''를 ''0''으로 바꿨습니다. 이제 ''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)가 핵심적인 방법으로 사용됩니다. A formal development proceeds by a dual process of abstraction, where one proves abstract statements in predicate calculus, and use of definitions, which in the contrary one instantiates general statements with particular notions in order to use the structure of mathematical values for the proof of more specialised properties. === 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)**가 ''true''와 ''false''라는 이름으로 선언됩니다. 이는 새로운 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'' 전략을 써서 ''b''가 ''bool''이라는 점을 사용합니다. 이 경우, ''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! 사실, 이 경우에 전체 증명 과정은 ''Intro''와 ''Elim''을 결합시켜주는 ''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'' 모듈에 생성자 ''S''와 ''O''로 정의되어 있습니다: 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_rec''은 ''nat''의 원소를 균일하게 계산합니다. ''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 === 원시 재귀를 써서 새로운 명제를 정의하는 것도 가능합니다. 예를 들어, 형성자 ''O''와 ''S''를 식별(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의 공리 중 하나인, ''O''와 ''S''는 서로 다른 값을 형성(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_n''과 ''le_S''를 소개합니다. 즉, "공리" ''le_n''과 ''le_S'' 뿐만 아니라, 이와 상통하는 성질인 '이들 정의 구절들의 귀결로서 얻어지면, 그리고 얻어질 때에만 ''(le n m)''이다'라는 사실도 얻게되는 것입니다. 즉, ''le''는 구절 ''le_n''과 ''le_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) 이 원리로 증명을 이끌어내는 방법을 보여드리겠습니다. 우선 //n// ≤ //m// => //n//+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! 정의 구절을 힌트로 주는 것은 좋은 생각입니다. 이렇게 하면 ''Induction''과 ''Auto''의 간단한 조합만으로도 증명을 진행할 수 있게됩니다. 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// 속에서 요청하고있는 모듈 //M//을 //N//이 요청될 때 자동적으로 보이게끔 하고싶으면, 모듈 //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와 함께 배포된 이미 증명된 이론의 라이브러리들을 들여다봐야할 것입니다.