[Coq 증명기] 콕, 빨리 빨리: 2장 콕으로 프로그래밍하기

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

콕 시스템에서 프로그램은 보통 함수로 표현한다. 프로그램이 간단하면 이 시스템 자체에서 실행할 수 있고, 더 복잡하다면 일반적인 프로그래밍언어로된 프로그램으로 변환하여 시스템 밖에서 실행할 수도 있다.

2.1 상수 정의

키워드 Definition으로 상수를 새로 정의할 수 있다. 예를 보자.

Definition example := fun x : nat => x*x + 2*x + 1.

동일하지만 이렇게도 정의할 수 있다.

Definition example1 ( x : nat) := x*x + 2*x + 1.

이 명령어들을 실행한다음 다른 명령어로 이 함수를 다뤄볼수 있다.

Check example1.

example1 : nat -> nat

Eval compute in example1 1.

= 4 : nat

어떤 경우에는 이전에 만들었던 정의를 없애고 싶을수가 있다. Reset 명령어로 정의한 이름을 주면 가능하다. 정의한 내용을 보고싶으면 Print 명령어를 사용한다. Coqide나 Proof-General 같은 특별한 환경을 사용하고 있다면 작업창 상단의 화살표로 문서의 이곳 저곳으로 실행 포인트를 이동할수 있다.

2.2 부울 조건식

콕에 미리 정의되어있는 타입으로 부울값의 타입이 있다. true와 false 두가지 값을 갖는다. 부울식을 제대로 사용하려면 Bool 라이브러리를 불러야한다. 부울 곱, 합, 부정 등의 정의를 사용할수 있다.

Require Import Bool.

부울값은 if...then...else... 구문으로 검사할수 잇다.

Eval compute in if true then 3 else 5.

= 3 : nat

이 타입과 연관되어 사용할 수 있는 함수로 무엇이 있는지 알고 싶다면 Search나 SearchAbout 명령어를 사용할수 잇다. Search 명령어를 사용한 예를 보자.

Search bool.

false: bool

true: bool

xorb: bool -> bool -> bool

orb: bool -> bool -> bool

negb: bool -> bool

implb: bool -> bool -> bool

ifb: bool -> bool -> bool -> bool

eqb: bool -> bool -> bool

andb: bool -> bool -> bool

2.3 자연수로 계산하기

자연수의 타입도 콕에 준비되어있다. 이 타입을 제대로 사용하려면 역시 Arith 라이브러리를 불러야한다.

Require Import Arith.

자연수는 0부터 무한대까지의 숫자들이다. 자연수 나름의 조건식을 구성하는 방법이 있다. 모든 자연수를 0 또는 어떤 자연수 p의 그 다음 S p로 표현하는 아이디어를 이용한다. 즉, 1은 S 0, 2는 S (S 0)가 된다.

이런 방식에서는 모든 자연수가 0이거나 다른 수의 다음으로 두가지 경우로 나눌수 있다. 이런 구분 방식으로 함수로 작성하면 다음과 같다. 이 함수는 인자가 오직 0인 경우에만 true를 반환한다.

Definition is_zero (n : nat) := 

   match n with

     0 => true

   | S p => false

   end.

match ... with ... end 식을 패턴매칭 구문이라고 부른다. 이 식을 계산한 결과는 n의 패턴에 달려있다. 0의 패턴이면 true이고, S p 패턴에 맞으면 false가 된다. S p 패턴에서 기호 S는 무엇의 다음이라는 개념을 뜻하는데 만일 n이 S p 패턴과 일치하면 다음과 같이 직관적으로 해석할 수 있다. n은 어떤 수의 다음에 위치한 수다. 패턴에 나타난 p는 일종의 지역변수로 그 "어떤 수"를 받는다. 화살표 => 오른편의 식에 p를 자유롭게 사용할 수 있다.

패턴매칭은 자연수로 계산할때 자주 사용한다. 예를 들어, 콕 시스템에서 제공하는 pred 함수는 0보다 큰 자연수를 그 전에 위치하는 수로, 0은 0으로 매핑한다.

Print pred.

pred = fun n : nat =>

   match n with | 0 => n | S u => u end

        : nat -> nat

Argument scope is [nat_scope]

pred 함수는 패턴매칭 구문을 사용해서 S u 형태의 수는 u로, 0은 0으로 매핑하는 것을 표현한다.

자연수로 계산할때 재귀 형태가 흔히 나타난다. 패턴매칭을 사용하는 함수를 정의할때 이 함수에 인자의 이전 숫자를 주어 사용하는 것이 가능하다. 콕은 재귀 방식으로 정의된 것을 매우 조심스럽게 다루기 때문에 특별한 키워드를 함께 사용해야한다. Fixpoint 키워드이다. 두 자연수를 더하는 재귀함수의 예를 보자.

Fixpoint sum_n n :=

   match n with

       0 => 0

   | S p => p + sum_n p

   end.

재귀함수를 정의할때 구조적 재귀라는 제약을 고려해야한다. 재귀함수를 호출하려면 원래 인자의 부분식만을 인자로 취할수 있다. 더 정확히 말하자면, 재귀함수의 인자는 반드시 변수이고 패턴매칭을 통해서 원래 인자로부터 얻은 것이어야 한다. 이런 제약을 지키면 모든 계산이, 설사 재귀함수를 쓰더라도, 종료함을 보장할 수 있다. sum_n의 정의는 제대로된 형태를 갖추고 있다. 왜냐하면 원래 인자 n과 매치되는 S p 패턴의 변수 p만 사용하기 때문이다.

예를 들어, 구조적 재귀 제약을 지키지 않은 다음 정의는 사용할수 없다.

Fixpoint rec_bad n :=

   match n with 0 => 0 | S p => rec_bad (S p) end.

Error:

Recursive definition of rec_bad is ill-formed.

In environment

rec_bad : nat -> nat

n : nat

p : nat

Recursive call to rec_bad has principal argument equal to "S p" instead of

"p".

Recursive definition is:

"fun n : nat => match n with

                | 0 => 0

                | S p => rec_bad (S p)

                end".

여러개의 인자를 받는 재귀함수를 정의할수 있다. 이런 경우 이 인자들중 하나는 구조적 재귀 제약을 따라야 한다. 예를 들어 아래 함수는 합의 중간결과를 인자로 받아 첫번째 인자인 자연수를 누적해서 더한다. 첫번째 인자에 대해서 구조적 재귀 제약을 만족한다. 왜냐하면 재귀함수를 호출할 때 첫번째 인자 p는 원래 첫번째 인자 n을 패턴매칭해서 얻은 것이기 때문이다.

Fixpoint sum_n2 n s :=

   match n with

       0 => s

   | S p => sum_n2 p (p + s)

   end.

재귀함수를 정의할 때 부울 타입과 같이 다른 타입의 값을 반환하도록 정의할수도 있다. 자연수로 주어진 인자가 짝수인지 검사하는 함수가 그러한 예이다.

Fixpoint evenb n :=

   match n with

      0 => true

    | 1 => false

    | S (S p) => evenb p

   end.

이 예제에서 깊은 패턴매칭을 사용했고, 두가지 이상의 경우를 나열했다. 콕 시스템은 모든 경우를 커버하는지 검사하고 재귀함수호출에서 패턴매칭을 통해서 얻은 변수들을 인자를 사용하는지를 검사할 것이다.

2.4 리스트로 계산하기

같은 타입의 데이터를 리스트로 모아 다룰 수 있다. 물론 리스트를 사용하기 위해 필요한 라이브러리를 불러야한다.

Require Import List.

여러 원소를 모아 하나의 리스트를 만드려면 두개의 콜론 ::으로 구분해서 차례로 나열하고 맨끝에 ::nil을 둔다.

Check 1::2::3::nil.

1 :: 2 :: 3 :: nil

      : list nat

:: 표기법은 어떤 리스트 앞에 요소를 추가함을 뜻한다. nil은 원소가 없는 리스트이고, 3::nil은 원소가 오직 3을 가지고 있고, 2::3::nil은 3만 포함하는 리스트 앞에 2를 붙인 리스트다.

nil은 콕 시스템에서 특별하게 사용된다. 왜냐하면 사용되는 문맥에 따라 다르게 사용될 수 있기 때문이다. 요소를 포함하는 리스트에서는 이 원소와 동일한 타입에 대한 비어있는 리스트를 표현한다. 하지만 nil을 그 자체로만 쓰면 콕 시스템은 문맥을 판단하지 못해 적절히 해석하는데 어려움에 처하게 된다(콕 시스템의 버전에 따라 다름).

Check nil.

Error: Cannot infer the implicit parameter A of nil.

또는

nil

      : list ?1

이런 문제가 발생하면 nil을 사용할때 의도하는 문맥을 타입으로 콕 시스템에게 알려주어 해결할 수 있다.

Check (nil : list nat).

nil:list nat

    : list nat

리스트를 다루는 몇가지 함수들을 콕 시스템에서 제공한다. 리스트 붙이기 함수 app (보통 ++로 사용), 함수를 받아 리스트의 각각의 원소에 적용하는 함수 map 등이 있다.

Eval compute in map (fun x => x + 3) (1::3::2::nil).

= 4 :: 6 :: 5 :: nil : list nat

Eval compute in map S (1::22::3::nil).

= 2 :: 23 :: 4 :: nil : list nat

Eval compute in

   let l := (1::2::3::nil) in l ++ map (fun x => x + 3) l.

= 1 :: 2 :: 3 :: 4 :: 5 :: 6 :: nil : list nat

리스트, map, app에 대한 연습문제

숫자 n을 입력받아 0부터 n-1까지 n개의 원소로 된 리스트를 반환하는 함수를 정의하시오.

리스트의 원소를 다룰때 패턴매칭 식을 사용한다. 자연수에 대한 패턴매칭과 유사하다. 리스트는 비어있거나 다른 리스트 앞에 원소를 갖는 두가지 경우로 분류할 수 있다. 두번째의 경우에 패턴매칭 식으로 리스트의 첫번째 원소와 나머지 리스트에 이름을 붙일 수 있다. 다음 예를 살펴보자. 인자로 주어진 리스트가 적어도 원소를 하나 포함하고 있고 첫번째 원소가 짝수이면 true를 반환하는 함수이다.

Definition head_evb l :=

   match l with nil => false | a::tl => evenb a end.

리스트에 대한 재귀함수를 정의할 수도 있다. 자연수를 다룰때와 동일하게 구조적 재귀 제약을 따라야 한다. 재귀함수 호출은 인자 리스트에서 직접적으로 얻은 부분리스트만 인자로 취할 수 있다. 리스트의 원소를 모두 더하는 예를 보자.

Fixpoint sum_list l :=

   match l with nil => 0 | n::tl => n + sum_list tl end.

마지막 예로, 자연수 리스트를 정렬하는 함수를 작성해보자. 두 자연수를 비교해서 부울값을 반환하는 함수 leb를 사용한다. 콕 시스템에서 제공한다.

Fixpoint insert n l :=

   match l with

       nil => n :: nil

   | a::tl => if leb n a then n::l else a ::insert n tl

   end.

Fixpoint sort l :=

   match l with

       nil => nil

   | a::tl => insert a (sort tl)

   end.

간단하게 테스트해보자.

Eval compute in sort (1::4::3::22::5::16::7::nil).

= 1 :: 3 :: 4 :: 5 :: 7 :: 16 :: 22 :: nil

     : list nat

정렬에 대한 연습문제

리스트를 인자로 받아 원소의 수가 2미만이거나 첫번째 원소가 두번째 원소보다 작을 때 true를 반환하는 함수를 작성하시오. 그 다음 역시 리스트를 인자로 받아 정렬되었는지 검사해서 true를 반환하는 함수를 작성하시오.

카운팅에 대한 연습문제

콕 시스템에서 제공하는 함수 beq_nat으로 두 자연수를 비교할수 있다. 이 함수를 이용하여 count_list를 작성하시오. 인자로 자연수와 리스트를 받아 이 자연수가 리스트 원소로 몇번 나타나는지 세어 그 횟수를 반환한다.

===

번역

(1장)

Expressions : 식

Formulas : 식

infix : 인픽스

Logical Formulas : 논리식

Symbolic Computation : 기호 계산

Terms : 텀

Well-formed : 제대로 된 형태

(2장)

Keyword : 키워드

Boolean : 부울

Conjunction : 곱

Disjunction : 합

Negation : 부정

Construct : 구문

Pattern-matching : 패턴 매칭

Recursivity : 재귀 형태

Structural Recursion : 구조적 재귀

Subterm : 부분식

Sublist : 부분리스트