리스트: 구조적 데이터를 가지고 작업하기

숫자들의 쌍들

Inductive 정의에서 각 생성자는 어떤 개수의 인자들을 받을 수 있다. true와 O와 같이 인자를 받지 않는 생성자, S와 같이 하나의 인자를 받는 생성자가 있고, 다음 예에서 하나 이상을 받는 생성자를 보여준다.

이 선언을 읽는 법은 "숫자들 쌍을 만드는 단 한 가지 방법이 있는데, 생성자 pair를 nat 타입의 두 인자들에 적용하는 것이다."

쌍에서 첫 번째와 두 번째 요소들을 꺼내는 두 개의 간단한 함수들이 있다. 이 정의들은 또한 두 개의 인자를 받은 생성자들에 대해 패턴 매치를 하는 법도 보여준다.

쌍들은 상당히 자주 사용되기 때문에 pair x y 대신에 표준 수학 표기법 (x,y)으로 쓸 수 있으면 좋을 것이다. 콕에서 Notation 선언으로 가능하다.

쌍에 대한 새로운 표기법은 식과 패턴 매치에서 모두 사용될 수 있다. (Basics 장의 minus 함수의 정의에서 사실 이미 보았다. 표준 라이브러리 일부로 쌍에 대한 표기법도 제공하기 때문에 동작한 것이다.

쌍들에 대한 몇 가지 간단한 사실들을 증명해보자. 특별한 방법으로 이 명제들을 서술하면 reflexivity (와 그리고 내장된 간략화) 만으로 증명들을 완성할 수 있다.

하지만 만일 보조 정리를 더 자연스러운 방법으로 서술하면 reflexivity만으로 충분하지 않다.

p의 구조를 드러내서 simpl로 fst와 snd에서의 패턴 매치를 수행할 수 있어야 한다. 이것은 destruct를 가지고 할 수 있다.

nat 타입의 값들을 가지고 다룰 때와 달리 destruct는 단 하나의 부분 목적 만을 만든다는 것을 주목하시오. natprod 타입의 값들은 한 가지 방법으로만 생성할 수 있기 때문이다.

연습문제: 별 하나 (snd_fst_is_swap)

☐

연습문제: 별 하나, 선택사항 (fst_swap_is_snd)

☐

숫자 리스트

쌍에 대한 정의를 일반화하면 다음과 같이 숫자 _리스트_의 타입을 기술할 수 있다. "리스트는 비어있는 리스트이거나 숫자와 또 다른 리스트의 쌍이다."

예를 들어, 세 개의 원소를 갖는 리스트가 여기 있다.

쌍들을 다룰 때와 같이 익숙한 프로그래밍 표기법으로 리스트를 쓰는 것이 더 편리하다. 다음 선언들로 ::을 중위 표기 cons로 사용하고 대괄호를 리스트를 만드는 "바깥쪽을 감싸는" 표기법으로 사용할 수 있다.

이 선언들을 자세하게 이해할 필요는 없지만 관심이 있다면 여기 대강 설명한다. right associativity 주석을 달아 콕으로 하여금 ::을 여러 번 사용한 식 들에서 괄호를 어떻게 씌울지 정한다. 예를 들어 다음 세 가지 선언들은 모두 동일한 의미를 갖는다.

at level 60은 ::과 다른 중위 연산자를 함께 사용한 식들에서 괄호를 어떻게 매길지 정한다. 예를 들어, +를 plus 함수에 대한 중위 표기법으로 50 레벨로 정의하였기 때문에, Notation "x + y" := (plus x y) (at level 50, left associativity). + 연산자는 ::보다 더 빨리 묶인다. 그래서 1 + 2 :: [3]은 콕이 우리가 기대한 대로 (1 + 2) :: [3]으로 해석하고, 1 + (2 :: [3])으로 해석하지 않는다. (.v 파일에서 "1 + 2 :: [3]"와 같은 식을 읽을 때 조금 혼동스러울 수 있다. 3을 감싸는 안쪽 괄호는 리스트를 표시하지만, 바깥쪽 괄호(HTML에서 보이지 않는)는 "coqdoc" 도구가 텍스트가 아니라 콕 코드로 표시해야 한다는 명령어이다.) 위에서 두 번째와 세 번째 Notation 선언들은 리스트에 대한 표준 대괄호 표기법을 도입한다. 세 번째 선언의 오른편은 콕에서 n개를 나열하는 표기법을 사용하는 예시를 보여주고 이진 생성자들의 반복해서 내포된 형태로 변환되는 예를 설명한다.

Repeat

많은 함수들이 리스트를 다루기에 유용하다. 예를 들어, repeat 함수는 n과 count를 받아 모든 원소가 n이고 길이가 count인 리스트를 반환한다.

Length

length 함수는 리스트의 길이를 계산한다.

Append

app 함수는 두 리스트들을 붙여 하나의 리스트를 만든다.

사실 app은 뒤이어 나올 어떤 부분에서 많이 사용될 것이다. 그래서 중위 표기법을 도입하는 것이 편리하다.

(기본 값을 지정한) Head와 Tail

리스트 프로그래밍의 두 가지 작은 예제가 있다. hd 함수는 인자로 주어진 리스트의 첫 번째 원소 ("head")를 반환하고 tl 함수는 첫 번째 원소를 제외한 모든 것 ("tail")을 리턴한다. 물론 비어 있는 리스트는 첫 번째 원소가 없기 때문에 그런 경우에 리턴할 기본 값을 지정해야 한다.

연습문제들

연습문제: 별 두 개, 추천 (list_funs)

아래의 nonzero, oddmembers, countoddmembers 정의를 완성하시오. 이 함수들이 하는 일을 이해하기 위해 테스트들을 살펴 보시오.

☐

연습문제: 별 세 개, 고급 (alternate)

두 리스트를 "지퍼로 잠그는 방식"으로 첫 번째 리스트에서 취한 원소들과 두 번째 리스트에서 취한 원소들 사이를 번갈아 가며 하나의 리스트로 만들도록 alternate를 완성하시오. alternate를 자연스럽고 우아하게 작성하려면 콕에서 요구하는 모든 Fixpoint 정의들이 "분명하게 종료해야 한다"는 점을 만족시키지 못할 것이다. 그 대신 두 리스트들의 원소들을 동시에 고려하는 조금 더 긴 해법을 찾아보시오. (한 가지 가능한 해는 새로운 종류의 쌍들을 정의하는 것인데 이 것이 유일한 방법은 아니다.

☐

리스트로 표현한 가방(bags) 자료 구조

bag (또는 multiset)은 집합과 같다. 다만, 각 원소가 단 한 번이 아니라 여러 번 나타날 수 있다는 점이 다르다. 숫자들을 담은 가방 자료 구조를 표현하는 한 가지 가능한 구현은 리스트를 사용하는 것이다.

연습문제: 별 세 개, 추천 (bag_functions)

가방 자료 구조를 다루는 count, sum, add, member 함수들의 정의를 완성하시오.

아래 증명들은 모두 reflexivity만 사용해도 증명할 수 있다.

중복 집합 sum은 집합 union과 유사하다. sum a b는 a와 b의 모든 원소들을 포함한다. (수학자들은 대개 중복 집합에 대한 union을 sum 대신 max를 사용하여 조금 다르게 정의한다. 이 연산에 대해 union이라고 부르지 않는 이유이다. sum의 정의에서 인자 이름을 명시적으로 주지 않고 작성하고 있다. 더욱이 Fixpoint 대신 Definion 키워드를 사용한다. 따라서 그 인자들 이름을 지었더라도 재귀 방식으로 다룰 수 없을 것이다. 이런 식으로 문제를 제시하는 의도는 스스로 sum이 다른 방식으로 구현될 수 있는지 생각해보라는 것이다. 아마도 이미 정의했던 함수들을 사용할 수 있다.

☐

연습문제: 별 세 개, 선택사항 (bag_more_functions)

여기 가방 자료 구조를 다루는 함수들이 있으니 연습해보시오. remove_one을 제거할 숫자를 포함하지 않는 가방 자료 구조에 적용하면 동일한 가방을 변경하지 않고 반환해야 한다.

☐

연습문제: 별 세 개, 추천 (bag_theorem)

함수 count와 add와 관련된 가방 자료 구조에 대한 흥미로운 정리 bag_theorem를 작성하고 증명하시오. 이 것은 열린 문제이기 때문에 참인 정리이지만 증명하기 위해서 아직 배우지 않은 방법이 필요할 수도 있다. 막히면 자유롭게 질문하시오!

☐

리스트에 대한 추론

숫자들을 다루었을 때처럼 리스트 처리 함수들에 대한 간단한 사실들은 종종 간략화를 통해 완전히 증명할 수 있다. 예를 들어, reflexivity로 간략화를 수행하면 아래 정리를 충분히 증명할 수 있다...

... 왜냐하면 []을 app 정의에서 match로 조사할 식으로 대체해서 그 매치 자체가 간략화되기 때문이다. 그리고 숫자들에 대해서와 같이 알려지지 않은 리스트의 가능한 형태에 관해 경우 별로 분석하는 것이 도움이 될 수 있다.

여기 nil의 경우 tl nil = nil로 정의하였기 때문에 증명할 수 있다. destruct 전술에 as 주석으로 n과 l' 이름들을 여기 도입한다. 리스트에 대한 cons 생성자의 두 인자들(리스트의 머리와 꼬리)에 이 이름들을 붙인다. 비록 리스트에 대한 흥미로운 정리들을 증명하려면 대개 귀납법이 필요하다.

짧은 설교

예제 증명 스크립트들을 읽기만 하면 제대로 이해하지 못할 것이다! 콕을 사용하고 각 단계가 얻는 바를 생각하면서 각 증명의 상세 내용을 따라가는 것이 중요하다. 그렇지 않으면 증명들을 시작할 때 연습문제들은 아무런 의미가 없을 것이 분명하다. 충분히 얘기했다.

리스트에 대한 귀납법

natlist 같은 자료형들에 대한 귀납법으로 증명하는 것은 자연수에 대한 귀납법 보다 조금 덜 익숙 할 수 있지만 아이디어는 똑같이 간단하다. 각 Inductive 선언은 선언한 생성자들을 사용하여 만들 수 있는 데이터 값들의 집합을 정의한다. 부울형은 true 또는 false이고 숫자는 O와 S를 다른 숫자에 적용한 것이고, 리스트는 nil 또는 숫자와 리스트에 적용한 cons이다. 더욱이 선언한 생성자들을 다른 것에 적용하는 것만이 유일하게 귀납적으로 정의한 집합의 원소들이 가질 수 있는 _유일하게_ 가능한 모양이다. 그리고 이러한 사실을 통해 귀납적으로 정의된 집합들에 대해 유추하는 방법을 직접적으로 제공한다. 숫자는 O이거나 그렇지 않으면 S를 _더 작은_ 숫자에 적용한 것이고, 리스트는 nil이거나 그렇지 않으면 cons를 어떤 숫자와 어떤 _더 작은_ 리스트에 적용한 것이며, 등등. 그래서 리스트 l을 언급하는 어떤 명제 P가 있고, _모든_ 리스트에 대해 P가 성립한다고 주장하고 싶다면 다음과 같이 추론할 수 있다.

• 첫째, l이 nil 일 때 P가 참이라고 증명하시오.
• 그런 다음 l이 어떤 숫자 n과 어떤 작은 리스트 l'에 대한 cons n l' 일 때, P가 l'에 대해 참이라고 가정하에 P가 참임을 보이시오.

더 큰 리스트는 오직 더 작은 리스트들 (궁극적으로 nil에 도달할 것인)로 만들기 때문에 이 두 주장들을 합하면 P가 모든 리스트 l에 대해 참이라는 것을 증명한다. 여기 구체적인 예가 있다.

자연수에 대한 귀납법을 적용할 때처럼 induction 전술에서 cons 경우에 as... 절로 더 작은 리스트 l1'에 해당하는 귀납 가정에 이름을 붙인다. 다시 한번 반복하면, 이 콕 증명은 고정된 형태로 작성한 문서로 보아서는 더욱 안된다. 대화식 콕 세션에서 증명을 읽고 있다면 무엇이 진행되고 있는지 쉽게 알 수 있고 현재 목적과 문맥을 각 지점에서 볼 수 있다. 하지만 이러한 상태는 콕 증명으로 작성한 부분에서는 드러나 있지 않다. 그래서 사람을 위해서 작성한 자연어로 서술된 증명은 더 명백한 이정표를 포함할 필요가 있을 것이다. 특히 두 번째 경우에 귀납적 가정이 무엇인지 독자들에게 정확히 환기시킨다면 증명의 흐름을 잃지 않도록 유지하는데 도움이 될 것이다. 비교를 위해 여기 동일한 정리를 비형식적으로 증명해본다. _정리_: 모든 리스트 l1, l2, l3에 대하여, (l1 ++ l2) ++ l3 = l1 ++ (l2 ++ l3). _증명_: l1에 관한 귀납법에 의하여.

• 첫째, l1 = []라 가정하자. 다음을 증명해야 한다.
  (☐ ++ l2) ++ l3 = ☐ ++ (l2 ++ l3),
  ++ 정의에 의해 바로 성립한다.
• 다음은, 아래 등식이 성립하는 l1 = n::l1'을 가정하자.
  (l1' ++ l2) ++ l3 = l1' ++ (l2 ++ l3)
  (귀납 가정). 다음 등식이 성립함을 보여야 한다.
  ((n :: l1') ++ l2) ++ l3 = (n :: l1') ++ (l2 ++ l3).
  ++ 정의와 아래 등식에 의해 성립한다.
  n :: ((l1' ++ l2) ++ l3) = n :: (l1' ++ (l2 ++ l3)),
  위 등식은 귀납 가정에 의해 바로 성립한다. ☐

리스트 뒤집기

리스트에 대한 조금 더 어려운 귀납 증명의 예에 대해 리스트 뒤집는 함수 rev를 app를 사용해서 정의한다고 가정하자.

rev의 성질들

새롭게 정의한 rev에 대한 몇 가지 정리들을 이제 증명해보자. 지금까지 본 것보다 조금 더 도전적인 증명으로 리스트를 뒤집으면 그 길이가 달라지지 않는다는 것을 증명하자. 처음 귀납법으로 증명해보면 비어있지 않는 리스트의 경우에서 막힌다...

++와 length를 연관 짓는 등식을 취하자. 이 등식으로 증명을 진행할 수도 있고 별도의 보조 정리로 증명할 수도 있을 것이다.

이 보조 정리를 가능한 일반화시키기 위해, rev 적용 결과에 대한 것이 아닌 _모든_ natlist들에 대해 한정사를 두었다. 이 목적이 참인지 여부는 분명히 뒤집을 리스트에 의존하지 않기 때문에 이렇게 한정사를 두는 것이 자연스럽다. 더욱이 더 일반적인 성질을 증명하기 더 쉽다. 이제 원래 증명을 완성할 수 있다.

비교를 위해 두 정리들을 비형식적으로 증명한 것이 여기 있다. _정리_: 모든 리스트 l1과 l2에 대해 length (l1 ++ l2) = length l1 + length l2. _증명_: l1에 대한 귀납법에 의해.

• 첫째, l1 = []을 가정하자. 다음을 증명하자.
  length (☐ ++ l2) = length ☐ + length l2,
  length와 ++의 정의들로 부터 바로 보일 수 있다.
• 다음으로, 아래 등식과 함께 l1 = n::l1'을 가정하자.
  length (l1' ++ l2) = length l1' + length l2.
  다음을 증명해야 한다.
  length ((n::l1') ++ l2) = length (n::l1') + length l2).
  length와 ++ 정의들과 귀납 가정과 함께 바로 보일 수 있다. ☐

_정리_: 모든 리스트 l에 대해, length (rev l) = length l. _증명_: l에 관한 귀납법에 의해.

• 첫째, l = []를 가정하자. 다음 등식을 증명해야 한다.
  length (rev ☐) = length ☐,
  이 등식은 length와 rev 정의들에서 직접 유도할 수 있다.
• 다음으로, 아래 등식과 함께 l = n::l'를 가정하자
  length (rev l') = length l'.
  다음 등식을 증명해야 한다.
  length (rev (n :: l')) = length (n :: l').
  rev 정의에 의해, 위 등식은 아래 등식으로 증명할 수 있는데,
  length ((rev l') ++ n) = S (length l')
  이전 보조 정리에 의해 이 등식은 아래 등식과 동일하다.
  length (rev l') + length n = S (length l').
  동일한 이 등식은 귀납 가정과 length 정의에 의해 바로 보일 수 있다.

이 증명들 스타일은 꽤 지루하고 현학적이다. 이 증명들 처음 두 세 개를 살펴보면, 상세한 내용이 적은 (머리 속으로 또는 필요하다면 메모 용지에 쉽게 작성할 수 있는) 그리고 중요한 단계들만 강조하는 증명들을 따라가기가 더 쉽다는 것을 발견할 수 있다. 이런 더 압축된 스타일로 위 증명을 다시 작성하면 다음과 같이 보일 것이다. _정리_: 모든 리스트 l, length (rev l) = length l에 대해. _증명_: 첫째, 어떤 l에 대해 length (l ++ [n]) = S (length l)이다. (l에 대한 직접적인 귀납 증명으로 보일 수 있다.) 그 주요 성질은, l = n'::l' 경우의 귀납 가정과 함께 위 등식을 사용하여 l에 대한 귀납법으로 다시 보일 수 있다. 주어진 상황에서 어느 스타일이 더 좋은지는 기대하는 독자의 교육 정도와 독자가 이미 익숙한 증명과 얼마나 비슷한지에 따라 다르다. 더 현학적인 스타일이 현재 목적을 위한 좋은 초기 설정이다.

Search

예를 들어 rewrite를 사용하여, 이미 증명한 다른 정리들을 이용하여 증명하는 것을 보았다. 그러나 어떤 정리를 참조하기 위해 이름을 알 필요가 있다! 정말로 이전에 증명한 정리들을 기억하는 것 조차 종종 어렵고 또한 그 정리들의 이름들은 더 기억하기 어렵다. 콕의 Search 명령은 이럴 때 꽤 도움이 된다. Search foo를 치면 콕은 foo가 포함된 모든 정리들의 목록을 보여줄 것이다. 예를 들어, rev에 대해 증명했던 정리들의 목록을 보기 위해서 다음 주석을 제거해보라.

다음 연습문제들을 풀 때 그리고 이 책을 읽는 동안 Search를 기억하라. 왜냐하면 많은 시간을 절약하게 해줄 것이기 때문이다! 프룹제너럴(ProofGeneral)을 사용하면 C-C C-a C-a를 가지고 Search를 실행할 수 있다. C-c C-; 명령어로 그 결과를 버퍼로 옮겨올 수 있다.

리스트 연습문제들, 파트 1

연습문제: 별 세 개 (list_exercises)

리스트에 대한 추가 연습:

다음 연습문제에 대한 짧은 해가 있다. 증명이 엉키면 뒤로 물러나서 더 간단한 방법을 찾아보려고 노력해보라.

nonzeros의 구현에 대한 연습문제:

☐

연습문제: 별 두 개 (beq_natlist)

beq_natlist 정의를 채우시오. 이 함수는 두 리스트의 숫자들이 같은 지 비교한다. 모든 리스트 l에 대해 beq_natlist l l는 true를 냄을 증명하시오.

☐

리스트 연습문제들, 파트 2

연습문제: 별 세 개, 고급 (bag_proofs)

위의 가방 자료구조에 대해 정의들에 관하여 증명하는 한 두 가지 작은 정리들이 있다.

leb에 대한 다음 보조 정리는 다음 증명에 도움이 될 수도 있다.

☐

연습문제: 별 세 개, 선택사항 (bag_count_sum)

함수 count와 sum을 사용하는 가방 자료 구조에 대한 정리 bag_count_sum을 흥미롭게 작성하고 증명해보시오. (count를 정의하는 법에 따라 그 증명이 어려울 수도 있다!)

☐

연습문제: 별 네 개, 고급 (rev_injective)

rev 함수가 단사 함수임을 증명하시오. 즉, forall (l1 l2 : natlist), rev l1 = rev l2 -> l1 = l2. (어렵게 증명하는 방법과 쉽게 증명하는 방법이 있다.)

☐

선택사항들

어떤 리스트의 n번째 원소를 반환하는 함수를 작성한다고 가정하자. 그 함수의 타입을 nat → natlist → nat로 하면 리스트가 너무 짧을 때 리턴할 어떤 숫자를 선택해야 할 것이다...

위 정의는 그다지 좋지 않다. 왜냐하면 nth_bad가 42를 반환하면 입력 리스트에 값이 실제로 나타나는지 추가 처리 없이 구분할 수 없기 때문이다. 더 나은 대응 방법은 nth_bad의 반환 타입을 변경해서 가능한 결과 중 하나로 에러 값을 포함시키는 것이다. 이러한 타입을 natoption이라고 부른다.

위 nth_bad 정의를 변경해서 리스트가 너무 짧을 때 None를 반환하고 리스트가 충분한 원소들로 구성되어 n 위치에 a가 나타날 때 Some a를 리턴할 수 있다. 이 새로운 함수를 nth_error으로 이름 지어 에러를 결과로 낼 수 있음을 나타낸다.

(In the HTML version, the boilerplate proofs of these examples are elided. Click on a box if you want to see one.) This example is also an opportunity to introduce one more small feature of Coq's programming language: conditional expressions...

콕의 조건식은 다른 언어의 조건식과 한 가지 작은 일반화를 제외하고 정확히 똑같다. 부울이 기본으로 제공되는 타입이 아니기 때문에 실제로 콕은 정확히 두 가지 생성자들을 가지고 _어떤_ 귀납적으로 정의한 타입에 대한 조건식을 지원한다. 조건식을 계산해서 Inductive 정의의 첫 번째 생성자가 나오면 참이고, 두 번째 생성자가 나오면 거짓이라고 간주한다. 아래 함수는 natopion에서 nat을 꺼내고 None 경우에 제공된 기본 값을 반환한다.

연습문제: 별 두 개 (hd_error)

동일한 아이디어를 사용하여 초기 hd 함수를 nil 경우에 기본 원소를 전달하지 않아도 되도록 수정하시오.

☐

연습문제: 별 하나, 선택사항 (option_elim_hd)

이 연습문제는 새로운 함수 hd_error를 예전 함수 hd와 연관짓는다.

☐

부분 맵

콕에서 어떤 자료 구조를 정의할 수 있는지 설명하는 마지막 예로 간단한 _부분 맵_ 자료 타입이 있다. 대부분의 프로그래밍언어에 있는 맵이나 딕셔너리 자료 구조와 유사하다. 첫째, 새로운 귀납적 자료형 id를 정의해서 부분 맵의 "키"로 사용한다.

내부적으로 id는 단지 숫자이다. 각 숫자를 Id 태그로 감싸 별도의 타입을 도입하면 정의들이 더 읽기 좋고 나중에 우리가 원하면 표현을 변경시킬 수 있는 유연성을 제공한다. id들이 똑같은지 테스트할 필요가 있을 것이다.

Exercise: 1 star (beq_id_refl)

☐ 이제 부분 맵의 타입을 정의한다:

이 선언을 다음과 같이 읽을 수 있다. "partial_map을 만드는 두 가지 방법이 있다. empty 생성자를 사용하여 비어 있는 부분 맵을 표현하거나 record 생성자를 키와 값과 다른 partial_map에 적용하여 기존 부분 맵에 키와 값 매핑을 추가하여 partial_map을 만든다." update 함수는 부분 맵에서 주어진 키에 대한 내용을 바꾸거나 주어진 키가 아직 없으면 새로운 내용을 추가한다.

마지막으로 find 함수는 partial_map에서 주어진 키를 탐색한다. 그 키를 찾지 못하면 None를 반환하고, 그 키와 val이 연관되어 있다면 Some val을 리턴한다. 만일 같은 키가 여러 값들에 매핑되어 있으면 find는 첫 번째로 만나는 것을 반환할 것이다.

연습문제: 별 하나 (update_eq)

☐

연습문제: 별 하나 (update_neq)

☐

연습문제: 별 두 개 (baz_num_elts)

아래의 귀납적 정의를 고려하자:

baz 타입은 _몇 개_의 원소들을 가지고 있는가? (영어로 답하거나 당신의 언어로 답하시오.) ☐