Coq 증명기(http://coq.inria.fr/)는 수학과 알고리즘을 형식화해서 표현하고 여러 성질을 증명하는 도구입니다. 


Coq 증명기가 무엇인지 궁금하거나 배워보고 싶은 분들이 참고 할 수 있는 Yves Bertot의 "Coq in a Hurry"를 번역했습니다. 1장~8장까지 별도의 글로 나누어 올려놓았고, 9장과 10장은 연습문제와 해답으로 번역에서 제외했습니다.


특히, 프로그래밍언어, 정형기법, 논리, 컴파일러를 전공하거나 관심을 두신 분들이 이 글의 독자가 될 수 있을 것으로 생각합니다.


새로운 프로그래밍언어를 배울때 가장 좋은 방법은 자신만의 문제를 하나 선택해서 스스로 풀어보는 것이지요. 저도 이 글을 읽고 번역한 다음, 텍스트 패턴 매칭에 대한 어떤 성질을 증명해보고 있습니다. 좌충우돌... 그럼에도 불구하고 Coq에 조금씩 적응하고 있구나 하는 생각이 듭니다. Coq을 처음 배운다면 구문이 생각나지 않을 수 있고, 증명하는데 적절한 전술이 무었일까 답답할 수도 있습니다. 이런 경우 1장~8장을 뒤적이면 유용한 답을 찾을 수 있을 것입니다. 특히 초보자에게 가장 도움이 되는 부분은 3장이 아닐까 생각합니다.


마지막으로, 글쓰기도 어렵지만 번역은 더 어렵네요. 글을 읽으시다 잘 이해가 가지 않는 문장이 있으면 틀림없이 번역에 문제가 있을 것으로 추측됩니다. 잘못된 번역, 더 매끄러운 번역이 생각나시면 언제든지 댓글을 달아주세요. 


2014년 7월, 최광훈.



[원문]

Coq in a Hurry (Yves Bertot, April 2010)

 - http://cel.archives-ouvertes.fr/docs/00/47/58/07/PDF/coq-hurry.pdf




콕, 빨리 빨리 - 이브 베르토


이 글에서 콕 시스템을 간단히 소개하고 논리적 개념과 함수를 정의하고 추론하는 법을 일러준다. 일종의 튜토리얼이고, 독자들은 이 시스템의 몇가지만을 배워 하고싶은 것을 빨리 실험해볼 수 있다. 더욱 자세히 배우고 싶다면 참고문헌 [1]을 보면 된다. 특히 방대한 연습문제가 있어 훈련하기에 좋다.



 참고 문헌



[1] Yves Bertot and Pierre Cast ́eran. Interactive Theorem Proving and Program Devel- opment, Coq’Art:the Calculus of Inductive Constructions. Springer-Verlag, 2004.


[2] The Coq development team. The Coq proof Assistant Reference Manual, Ecole Polytechnique, INRIA, Universit de Paris-Sud, 2004. http://coq.inria.fr/doc/ main.html 


목차

 1. 식과 논리식

 2. 콕으로 프로그래밍하기

 3. 명제와 증명

 4. 숫자 프로그램의 성질을 증명하기

 5. 리스트 프로그램의 성질을 증명하기

 6. 새로운 데이터 타입 정의하기

 7. 콕 시스템의 숫자

 8. 귀납적 성질

 9. 연습문제 (원문 참고)

 10. 해답 (원문 참고)



1. (계산?)식과 논리식


콕 시스템은 일종의 언어를 제공한다. 이 언어로 논리식을 다루고, 구문 형태를 살피고, 증명하기도 한다. 논리식은 함수를 사용하여 구성하기도 하고, 제한된 형태지만 이 함수들을 가지고 계산도 한다.


1.1 바른 식 쓰기


먼저 식이 제대로 된 형태인지 검사하는 법을 배울 필요가 있다. 이 명령어는 Check이다. 몇가지 예를 들어보자. 이 시스템의 기초적인 객체와 타입을 두세가지 사용한다. 명령어는 항상 점으로 끝난다. 이제부터 사용자가 콕 시스템에 보내는 글은 이런 스타일이고, 이 시스템에서 응답하는 내용은 이런 스타일이다. 


Check True.

True : Prop


Check False.

False : Prop


Check 3.

3 : nat


Check (3+4).

3 + 4 : nat


Check (3=5).

3=5 : Prop


Check (3,4).

(3,4) : nat * nat


Check ((3=5)/\True).

3 = 5 /\ True : Prop


Check nat -> Prop

nat -> Prop : Type


Check (3 <= 6).

3 <= 6 : Prop


두가지 목적으로 A : B 표기법을 사용한다. 식 A의 타입이 식 B이다거나 A는 B의 증명임을 나타낸다. 우리가 입력하는 식에서도 이 표기법을 사용할 수 있다. 보통 어떤 식의 타입을 분명히 드러내고자할때 그렇다. 


Check (3,3=5):nat*Prop

(3,3=5):nat * Prop

       : nat * Prop


이 식들 중 어떤 것은 논리 명제로 읽고 (즉  Prop 타입을 가지고) 또 어떤 것은 숫자로 읽고(nat 타입을 갖고), 다른 것은 더 복잡한 자료구조의 원소로 읽기도 한다. 물론 제대로 형태를 갖추지 못한 식도도 검사해볼수 있다. 이 경우 콕 시스템은 에러문을 출력해 문제점을 설명해줄것이다.


복잡한 식을 구성하려면 명제들을 논리 연결자들로 조합하거나 덧셈, 곱셈, 쌍만들기 등으로 식들을 구성하면된다. 키워드 fun을 사용해서 새로운 함수도 만들수 있다. 람다계산법과 같은데에서 lambda 기호대신 쓴다. Check 명령어로 함수를 검사하면 nat 타입의 숫자 x를 입력으로 받아 x가 3과 같다는 명제를 리턴한다고 설명해준다. 그 다음 Check 명령어에서 검사하는 논리명제는 모든 자연수 x에 대해 x는 3보다 작거나 또는 자연수 y가 존재해서 x=y+3이다.


Check (fun x:nat => x=3).

fun x : nat => x = 3 : nat -> Prop


Check (forall x:nat, x<3 \/ (exists y:nat, x=y+3)).

forall x:nat, x<3 \/ (exists y:nat, x=y+3) : Prop


이번에는 let을 사용하는 식을 살펴보자. 식에 임시 이름을 부여할 때 유용하다. 예제에서 let으로 이름을 붙인 식은 숫자를 입력받아 숫자의 쌍을 반환하는 함수다. 함수 f를 어떤 값, 예를 들어 3에 적용하는 표기 방법도 보여준다. 단순히 함수 이름 f와 인자 3을 나란히 쓰면된다. 보통 수학에서 하던것과 달리 인자를 감싸는 괄호를 항상 쓰지 않아도 된다. 


Check (let f := fun x => (x * 3, x) in f 3).

let f := fun x : nat => (x * 3, x) in f 3 : nat * nat 


어떤 표기법은 다용도로 사용된다. 예를 들어, * 기호는 곱셈을 표시하기도 하고 타입에서 곱을 표시하기도 한다. Locate 명령어로 표기법이 의미하는 함수를 찾을 수 있다.


Locate "_ <= _".

Notation Scope

"x <= y" := le x y : nat_scope

                    (default interpretation)


텀의 형태가 제대로 되려면 두가지 조건을 갖춰야한다. 정해진 구문을 따라야한다. 예를 들어, 열린괄호와 닫힌괄호의 쌍이 맞아야 하고 두개의 피연산자를 요구하는 연산자에게는 그렇게 인자가 주어져야한다. 두번째 조건은 타입에 맞게 식을 구성해야한다. Check 명령어는 식이 제대로 구성되었는지 검사도 하고 식의 타입을 알려주기도한다. 예를 들어 어떤 식이 제대로 되었는지 차근차근 단계별로 확인할 수 있다.


Check True.

True : Prop


Check False.

False : Prop


Check and.

and : Prop -> Prop -> Prop


Check (and True False).

True /\ False : Prop


마지막 예에서 and는 Prop 타입의 인자를 받아 Prop -> Prop 타입의 함수를 반환하는 함수다. 따라서 Prop 타입의 True에 적용할 수 있다. 그 결과 반환되는 함수는 또다른 Prop 타입의 인자를 기대하고 False에 적용할 수 있다. 표기법 a -> b -> c는 사실

a -> (b -> c)이다. 표기법 f a b는 사실 (f a) b 이다.


그리고 /\는 피연산자들 가운데에 연산자를 배치하는 인픽스 표기법을 따른다. Locate 명령어로 확인할 수 있다.



2. 식을 계산하기


콕 시스템으로 식을 계산할 수도 있다. 기호 계산 방식을 사용하는데, 여러가지 전략이 있다. compute라고 부르는 전략은 다음과 같이 사용한다.


Eval compute in 

   let f := fun x => (x * 3, x) in f 3.

= (9, 3) : nat * nat


이 명령어를 실행한 뒤에는 함수 f가 사라진다. 이 식을 계산할 때 임시로 정의되고 f 3을 계산할 때 사용될 뿐이다.


함수에 관한 연습문제 (참고문헌 [1]의 연습문제 2.5) 다섯개의 인자를 받아 그 합을 반환하는 함수를 작성하고, Check 명령어로 제대로된 형태로 작성했는지 확인한 다음, Eval 명령어로 샘플 값들을 주어 계산해보시오.  연습문제에 대한 답은 모두 이 글의 마지막에 제공한다.




===

번역


Expressions : 식

Formulas : 식

infix : 인픽스

Logical Formulas : 논리식

Symbolic Computation : 기호 계산

Terms : 텀

Well-formed : 제대로 된 형태



Posted by lazyswamp :