[번역] 콕, 빨리빨리 6장 / [Translation] Ch.6, Coq in a Hurry

Coq in a Hurry (Yves Bertot, April 2010)
 - http://cel.archives-ouvertes.fr/docs/00/47/58/07/PDF/coq-hurry.pdf
 - Keyword: Tutorial, Theorem Proving, Prover, Logic, Software Verification, Agda, Nurpl

콕, 빨리빨리 (최광훈, 2014년 7월)

목차
 1. 식과 논리식
 2. 콕으로 프로그래밍하기
 3. 명제와 증명
 4. 숫자 프로그램의 성질을 증명하기
 5. 리스트 프로그램의 성질을 증명하기
 6. 새로운 데이터 타입 정의하기
 7. 콕 시스템의 숫자
 8. 귀납적 성질
 9. 연습문제 (원문 참고)
 10. 해답 (원문 참고)

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

숫자, 부울값, 리스트는 모두 데이터 타입의 예이다. 프로그래밍할때 종종 새로운 데이터 타입이 필요하다. 그 데이터는 어떤 경우들을 모아놓은 것이고 각각의 경우에 해당하는 필드들을 가지고 있음을 표현한다.  콕 시스템은 이런 방식의 데이터 구성을 표현하는데 편리한 방법을 제공한다.

6.1 귀납 타입을 정의하기

여기에 귀납 타입을 정의하는 예가 있다.

Inductive bin : Type :=
   L : bin
| N : bin -> bin -> bin.

이것은 새로운 타입 bin을 만든다. bin의 타입은 Type이다. 이 bin 타입으로 두 가지 경우를 따르는 데이터를 표현한다. 첫번째 경우는 L로 표기하고 필드가 없다. 두번째 경우는 N t1 t2와 같이 쓰고 bin 타입의 두 개의 필드가 있다. 즉, bin 타입의 원소는 상수 L을 취하거나 N을 bin 타입의 두 객체에 적용하는 두가지 다른 방법으로 만들수 있다.

Check N L (N L L)
N L (N L L)
     : bin

이 bin 타입은 내부 노드나 끝 노드에 별도의 정보를 가지고 있지 않는 이진 트리를 포함한다.

데이터 타입 정의에 대한 연습문제

세 가지 경우를 표현하는 데이터 타입을 정의하시오.  상수, 세개의 필드(숫자, 지금 정의하고 있는 데이터 타입의 값 두 개)를 갖는 경우, 네개의 필드(부울값, 지금 정의하는 데이터 타입의 값 세 개)를 갖는 경우를 표현해야한다.

6.2 패턴 매칭

귀납 타입의 원소는 패턴 매칭을 하는 함수로 처리할 수 있다. 예를 들어 인자로 N L L이면 false를 그 외의 형태를 받으면 true를 반환하는 함수를 작성할 수 있다.

Definition example7 (t : bin): bool :=
   match t with N L L => false | _ => true end.

6.3 재귀함수 정의

귀납 데이터 타입이라면 어떠한 것에 대해서도 Fixpoint 명령어를 사용하여 재귀 함수를 정의할 수 있다. 하지만 자연수와 리스트에서 처럼 동일한 구조적 재귀 규칙을 반드시 따라야 한다. 즉, 오직 변수에 대해서만 재귀함수 호출을 할 수 있고 이 변수는 처음 주어진 인자에서 패턴 매칭을 통해 얻는 것이어야 한다. 다음은 우리가 새로 정의한 데이터 타입에 대한 재귀함수의 예제이다.

Fixpoint flatten_aux (t1 t2:bin) : bin :=
   match t1 with
       L => N L t2
   | N t'1 t'2 => flatten_aux t'1 (flatten_aux t'2 t2)
   end.

Fixpoint flatten (t:bin) : bin :=
   match t with
       L => L 
   | N t1 t2 => flatten_aux t1 (flatten t2))
   end.

Fixpoint size (t:bin) : nat :=
   match t with
       L => 1 | N t1 t2 => 1 + size t1 + size t2
   end.

사용자가 정의한 데이터 타입에 대한 구조적 재귀함수를 가지고 계산하는 것은 숫자와 리스트의 경우처럼 비슷하다.

6.4 경우를 나누어 증명

지금까지 우리가 도입한 귀납 타입에 대해 함수들을 정의해보았고, 이제 이 함수들의 성질을 증명할 수 있다. 첫번째 예제에서 bin 타입의 원소에 대한 경우 분석을 한다.

Lemma example7_size :
      forall t, example7 t = false -> size t = 3.

intros t; destruct t.

2 subgoals
  
  ============================
   example7 L = false -> size L = 3

subgoal 2 is:
 example7 (N t1 t2) = false -> size (N t1 t2) = 3

전술 destruct t는 t에 대한 귀납 타입의 정의에 따라 다양한 경우를 따져본다. 식 t는 L로 만든 것일 수도 있고, N을 다른 트리 t1과 t2에 적용한 결과일 가능성도 있다. 따라서 이 전술을 쓰면 두 가지 목적 명제가 나온다. 

트리 L에 대해서 example7과 size의 결과 값을 알고 있다. 콕 시스템에게 요청해서 그것을 계산한다. 

simpl.

2 subgoals

  

  ============================

   true = false -> 1 = 3

subgoal 2 is:

 example7 (N t1 t2) = false -> size (N t1 t2) = 3

이 계산을 하면 example7 L이 true이므로 false이기를 기대하는 것과 다름을 발견한다. 아래의 전술로 이런 비일관성을 다룬다. 

intros H.

2 subgoals

  

  H : true = false

  ============================

   1 = 3

subgoal 2 is:

 example7 (N t1 t2) = false -> size (N t1 t2) = 3

discriminate H.

1 subgoal

  

  t1 : bin

  t2 : bin

  ============================

   example7 (N t1 t2) = false -> size (N t1 t2) = 3

그 결과 첫번째 목적 명제를 증명했다. discriminate H 전술은, 가정 H가 귀납 타입에서 두 개의 다른 컨스트럭터[역주: bin 타입의 컨스트럭터는 L과 N이다.]가 같은 값을 반환한다고 선언할 때 사용할 수 있다. 그런 가정은 일관성이 없고, 이 전술은 이 일관성을 직접 이용해서 이러한 경우는 결코 일어날 수 없음을 표현한다. 

귀납 타입의 컨스트럭터는 단사적이다는 또다른 중요한 성질이 있다. 이것에 대해서는 나중에 6.6절에서 설명한다. 

두번째 목적 명제에 대해서도 t1과 t2의 값에 대해 경우 분석을 해야 한다. 자세한 증명은 생략한다. 다음에 나열한 전술들을 사용하여 완료할 수 있다. 

destruct t1.

2 subgoals

  

  t2 : bin

  ============================

   example7 (N L t2) = false -> size (N L t2) = 3

subgoal 2 is:

 example7 (N (N t1_1 t1_2) t2) = false -> size (N (N t1_1 t1_2) t2) = 3

destruct t2.

3 subgoals

  

  ============================

   example7 (N L L) = false -> size (N L L) = 3

subgoal 2 is:

 example7 (N L (N t2_1 t2_2)) = false -> size (N L (N t2_1 t2_2)) = 3

subgoal 3 is:

 example7 (N (N t1_1 t1_2) t2) = false -> size (N (N t1_1 t1_2) t2) = 3

첫번째 목적 명제에 있는 함수를 계산하도록 콕 시스템에 요청한다.

simpl.

3 subgoals

  

  ============================

   false = false -> 3 = 3

subgoal 2 is:

 example7 (N L (N t2_1 t2_2)) = false -> size (N L (N t2_1 t2_2)) = 3

subgoal 3 is:

 example7 (N (N t1_1 t1_2) t2) = false -> size (N (N t1_1 t1_2) t2) = 3

함축의 오른편이 참이므로 콕 시스템은 자동으로 이것을 증명할 수 있다. 전술 테이블을 참조해서 더 기초적인 방법으로 증명하려면 intro와 reflexivity 전술을 차례로 사용할 수 있다.

auto.

2 subgoals

  

  t2_1 : bin

  t2_2 : bin

  ============================

   example7 (N L (N t2_1 t2_2)) = false -> size (N L (N t2_1 t2_2)) = 3

subgoal 2 is:

 example7 (N (N t1_1 t1_2) t2) = false -> size (N (N t1_1 t1_2) t2) = 3

intros H; discriminate H.

intros H; discriminate H.

Qed.

6.5 귀납적 증명

귀납 타입에 대한 가장 일반적인 증명이 귀납적 증명이다. 이 방법으로 귀납 타입 원소에 대한 성질을 증명할때 사실 우리는 각 컨스트럭터로 분류되는 경우를 따지고 있는 것이다. 마치 경우 분석에서 했던 것 처럼 말이다. 물론 변형된 부분도 있다. 귀납 타입의 인자를 갖는 컨스트럭터를 다룰때 이러한 인자에 대해서 증명하려고 하는 성질이 성립한다고 가정할 수 있다.

목적 지향적인 증명을 할때 elim 전술로 귀납 원리를 사용한다. 이 전술을 설명하기 위해 flatten_aux와 size 함수에 대한 간단한 사실 명제를 증명할 것이다.

Lemma flatten_aux_size : 
   forall t1 t2, size (flatten_aux t1 t2) = size t1 + size t2 + 1.

induction t1.

2 subgoals
  
  ============================
   forall t2 : bin, size (flatten_aux L t2) = size L + size t2 + 1

subgoal 2 is:
 forall t2 : bin,
 size (flatten_aux (N t1_1 t1_2) t2) = size (N t1_1 t1_2) + size t2 + 1

두 개의 목적 명제가 생기는데, 첫번째는 flatten_aux의 첫번째 인자가 L일때, 두번째는 N t1_1 t1_2일때 보조 정리의 명제를 증명하는 것이다. 두 함수의 정의를 사용하면 증명을 쉽게 진행할 수 있다. 콕 시스템에서 simple 전술을 사용한다. 얻은 결과는 ring 전술로 해결한다.

intros t2.

simpl.

2 subgoals

  

  t2 : bin

  ============================

   S (S (size t2)) = S (size t2 + 1)

subgoal 2 is:

 forall t2 : bin,

 size (flatten_aux (N t1_1 t1_2) t2) = size (N t1_1 t1_2) + size t2 + 1

ring.

1 subgoal

  

  t1_1 : bin

  t1_2 : bin

  IHt1_1 : forall t2 : bin,

           size (flatten_aux t1_1 t2) = size t1_1 + size t2 + 1

  IHt1_2 : forall t2 : bin,

           size (flatten_aux t1_2 t2) = size t1_2 + size t2 + 1

  ============================

   forall t2 : bin,

   size (flatten_aux (N t1_1 t1_2) t2) = size (N t1_1 t1_2) + size t2 + 1

두번째 목적 명제를 증명할때, t1_1과 t1_2에 대한 귀납 가정을 사용할 수 있다. 다시 한번 size와 flatten_aux 함수를 호출한 결과 값을 콕 시스템으로 하여금 계산하도록 명령을 내릴 수 있다. 그 다음 귀납 가정을 사용할 수 있다.

intros t2; simpl.

1 subgoal

  

  t1_1 : bin

  t1_2 : bin

  IHt1_1 : forall t2 : bin,

           size (flatten_aux t1_1 t2) = size t1_1 + size t2 + 1

  IHt1_2 : forall t2 : bin,

           size (flatten_aux t1_2 t2) = size t1_2 + size t2 + 1

  t2 : bin

  ============================

   size (flatten_aux t1_1 (flatten_aux t1_2 t2)) =

   S (size t1_1 + size t1_2 + size t2 + 1)

rewrite IHt1_1

1 subgoal

  

  t1_1 : bin

  t1_2 : bin

  IHt1_1 : forall t2 : bin,

           size (flatten_aux t1_1 t2) = size t1_1 + size t2 + 1

  IHt1_2 : forall t2 : bin,

           size (flatten_aux t1_2 t2) = size t1_2 + size t2 + 1

  t2 : bin

  ============================

   size t1_1 + size (flatten_aux t1_2 t2) + 1 =

   S (size t1_1 + size t1_2 + size t2 + 1)

rewrite IHt1_2

1 subgoal

  

  t1_1 : bin

  t1_2 : bin

  IHt1_1 : forall t2 : bin,

           size (flatten_aux t1_1 t2) = size t1_1 + size t2 + 1

  IHt1_2 : forall t2 : bin,

           size (flatten_aux t1_2 t2) = size t1_2 + size t2 + 1

  t2 : bin

  ============================

   size t1_1 + (size t1_2 + size t2 + 1) + 1 =

   S (size t1_1 + size t1_2 + size t2 + 1)

ring.

Proof completed.

Qed.

flatten과 size에 대한 연습문제

Lemma flatten_size : forall t, size (flatten t) = size t.

flatten_aux_size 보조 정리를 사용하되 apply 전술이나 rewrite 전술을 함께 고려해야 한다.

6.6 injection 전술을 사용하는 예제

이번에는 injection 전술을 사용하는 증명의 예를 설명한다. 어떠한 트리도 자신의 부분을 구성할 수 없음을 증명한다.

Lemma not_subterm_self_l : forall x y, ~ x = N x y.

1 subgoal
  
  ============================
   forall x y : bin, x <> N x y

이 목적 명제에 등식의 부정을 _ <> _로 표시함을 볼 수 있다. x에 대한 귀납적 증명을 한다.

induction x.

2 subgoals

  

  ============================

   forall y : bin, L <> N L y

subgoal 2 is:

 forall y : bin, N x1 x2 <> N (N x1 x2) y

첫번째 목적 명제는 이 귀납 타입의 두 컨스트럭터가 다르다는 것이다. discriminate 전술을 사용한다. 첫번째를 해결하고 두번째 목적 명제를 보자.

intros y; discriminate.

1 subgoal

  

  x1 : bin

  x2 : bin

  IHx1 : forall y : bin, x1 <> N x1 y

  IHx2 : forall y : bin, x2 <> N x2 y

  ============================

   forall y : bin, N x1 x2 <> N (N x1 x2) y

이 목적 명제의 결론이 부정 형태이므로 전술 테이블을 참고해서 해당하는 전술을 선택할 수 있다. 이 예에서, 사실 명제의 부정은 이 사실 명제는 False를 함축한다라는 함수로 표현할 수도 있음을 보여준다. 

intros y abs.

1 subgoal

  

  x1 : bin

  x2 : bin

  IHx1 : forall y : bin, x1 <> N x1 y

  IHx2 : forall y : bin, x2 <> N x2 y

  y : bin

  abs : N x1 x2 = N (N x1 x2) y

  ============================

   False

가정 abs는 N x1 x2와 N (N x1 x2) y가 동등함을 표현한다. 컨스트럭터 N은 두 인자에 대해 단사적이어서 x1이 N x1 x2와 같다는 것을 함축한다. 이러한 유추 과정을 injection 전술로 표현한다.

injection abs.

1 subgoal

  

  x1 : bin

  x2 : bin

  IHx1 : forall y : bin, x1 <> N x1 y

  IHx2 : forall y : bin, x2 <> N x2 y

  y : bin

  abs : N x1 x2 = N (N x1 x2) y

  ============================

   x2 = y -> x1 = N x1 x2 -> False

그 결과 두 개의 등식이 함축의 전제로 이 목적 명제의 결론에 도입되었다. 이 등식들을 새로운 가정으로 도입할 수 있다. 

intros h2 h1.

1 subgoal

  

  x1 : bin

  x2 : bin

  IHx1 : forall y : bin, x1 <> N x1 y

  IHx2 : forall y : bin, x2 <> N x2 y

  y : bin

  abs : N x1 x2 = N (N x1 x2) y

  h2 : x2 = y

  h1 : x1 = N x1 x2

  ============================

   False

가정 h1과 IHx1(을 사례화 시킨 명제)는 서로 모순이다. 다음 전술로 이것을 표현한다.

assert (IHx1' : x1 <> N x1 x2).

2 subgoals

  

  x1 : bin

  x2 : bin

  IHx1 : forall y : bin, x1 <> N x1 y

  IHx2 : forall y : bin, x2 <> N x2 y

  y : bin

  abs : N x1 x2 = N (N x1 x2) y

  h2 : x2 = y

  h1 : x1 = N x1 x2

  ============================

   x1 <> N x1 x2

subgoal 2 is:

 False

   apply IHx1.

1 subgoal

  

  x1 : bin

  x2 : bin

  IHx1 : forall y : bin, x1 <> N x1 y

  IHx2 : forall y : bin, x2 <> N x2 y

  y : bin

  abs : N x1 x2 = N (N x1 x2) y

  h2 : x2 = y

  h1 : x1 = N x1 x2

  IHx1' : x1 <> N x1 x2

  ============================

   False

case IHx1'.

[역주: IHx1'이 true와 false 경우 분석. true 경우는 False 결론을 낼 수없으므로 쉽게 배제. 남은 경우는 IHx1' = false.] 

1 subgoal

  

  x1 : bin

  x2 : bin

  IHx1 : forall y : bin, x1 <> N x1 y

  IHx2 : forall y : bin, x2 <> N x2 y

  y : bin

  abs : N x1 x2 = N (N x1 x2) y

  h2 : x2 = y

  h1 : x1 = N x1 x2

  IHx1' : x1 <> N x1 x2

  ============================

   x1 = N x1 x2

exact h1.

Proof completed.

Qed.

===
번역

(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 : 부분리스트

(3장)
Fact: 사실 명제
Theorem: 정리
Implication : 함축
Predicate : (술어) 명제
Rewriting : 다시쓰기
Equality : 등식
Goal : 목적 명제
Tactic : 전술
Hypothesis : 가정
Universal Quantification : 전칭 한정
Transitive : 추이적
Instantiation : 사례화
Associativity : 결합성

(4장)
Proof by induction : 귀납적 증명
Existential : 존재
Lemma : 보조 정리

(5장)
the step case of the proof by induction : 귀납적 증명의 귀납적 경우

(6장)
datatype : 타입, 데이터 타입
Binary tree : 이진 트리
Internal Node : 내부 노드
Leaf : 끝 노드
Proof by Cases : 경우를 나누어 증명
Constructor : 컨스트럭터
Injective : 단사적