[번역] 콕, 빨리빨리 5장 / [Translation] Ch.5, 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. 해답 (원문 참고)

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

리스트에 대해 계산하는 프로그램의 성질을 증명할때도 귀납적 증명을 사용할 수 있다. 귀납 인자로 리스트를 취한다. 이번에도 두 가지 목적 명제를 증명할 것이다. 처음은 비어있는 리스트의 경우이고 다음은 a::l 형태의 일반적인 리스트를 다룬다. 여기서 l은 귀납적 가정에서 사용된다.

예제 증명을 살펴보자. 앞에서 소개했던 insert와 sort 함수를 사용하는 리스트 정렬은 리스트에 나타난 원소의 수를 변경하지 않음을 증명하겠다. 리스트에 어떤 숫자가 몇번 나타나는지 그 수를 세는 함수는 다음과 같다.

Fixpoint count n l := 
   match l with
       nil => 0
    | a::tl =>
       let r := count n tl in if beq_nat n a then 1+r else r
    end.

리스트에 원소를 추가하면 이 숫자가 출현하는 빈도는 항상 증가함을 먼저 증명한다.

Lemma insert_incr : forall n l, count n (insert n l) = 1 + count n l.

intros n l; induction l.

2 subgoals
  
  n : nat
  ============================
   count n (insert n nil) = 1 + count n nil

subgoal 2 is:
 count n (insert n (a :: l)) = 1 + count n (a :: l)

simpl 전략으로 콕 시스템은 여러 함수들을 계산한다. 

simpl.

2 subgoals

  

  n : nat

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

   (if beq_nat n n then 1 else 0) = 1

subgoal 2 is:

 count n (insert n (a :: l)) = 1 + count n (a :: l)

여기에서 beq_nat에 대한 정리를 찾을 필요가 있다.

SearchAbout beq_nat.
beq_nat_refl: forall n : nat, true = beq_nat n n
beq_nat_eq: forall x y : nat, true = beq_nat x y -> x = y
beq_nat_true: forall x y : nat, beq_nat x y = true -> x = y
beq_nat_false: forall x y : nat, beq_nat x y = false -> x <> y
beq_nat_true_iff: forall x y : nat, beq_nat x y = true <-> x = y
beq_nat_false_iff: forall x y : nat, beq_nat x y = false <-> x <> y
NatOrderedType.Nat_as_DT.eqb_eq:
  forall x y : nat, beq_nat x y = true <-> x = y
NatOrderedType.Nat_as_OT.eqb_eq:
  forall x y : nat, beq_nat x y = true <-> x = y
NatOrderedType.Nat_as_UBE.eqb_eq:
  forall x y : nat, beq_nat x y = true <-> x = y

이미 존재하는 beq_nat_refl 정리가 유용하다. rewrite 전술로 이 정리를 적용한다.

rewrite <- beq_nat_refl.

2 subgoals
  
  n : nat
  ============================
   1 = 1

subgoal 2 is:
 count n (insert n (a :: l)) = 1 + count n (a :: l)

현재 목적 명제의 형태는 reflexivity 전술로 쉽게 해결할 수 있다. 그 다음 목적 명제는 리스트에 대한 귀납적 증명의 귀납적인 경우이다.

reflexivity.

1 subgoal
  
  n : nat
  a : nat
  l : list nat
  IHl : count n (insert n l) = 1 + count n l
  ============================
   count n (insert n (a :: l)) = 1 + count n (a :: l)

다시 한 번 콕 시스템에 요청해 여러 함수들을 계산한다. 

simpl. 

1 subgoal

  

  n : nat

  a : nat

  l : list nat

  IHl : count n (insert n l) = 1 + count n l

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

   count n (if leb n a then n :: a :: l else a :: insert n l) =

   S (if beq_nat n a then S (count n l) else count n l)

leb n a 식의 경우들을 먼저 각각 살펴보고, 그 다음 beq_nat n a의 경우들을 따져본다. case (leb n a) 전술을 처음 부분에 사용한다. 그 결과 두 개의 목적 명제를 만난다. 하나는 leb n a를 true로 바꾸고 다른 하나는 false로 바꾼 것이다.

case (leb n a).

2 subgoals
  
  n : nat
  a : nat
  l : list nat
  IHl : count n (insert n l) = 1 + count n l
  ============================
   count n (n :: a :: l) =
   S (if beq_nat n a then S (count n l) else count n l)

subgoal 2 is:
 count n (a :: insert n l) =
 S (if beq_nat n a then S (count n l) else count n l)

이제 이 식을 간단하게 만들 수 있다. 그 다음 beq_nat이 다시 나타나는데 beq_nat_refl 정리를 다시 쓸 수 있다.

simpl.

2 subgoals
  
  n : nat
  a : nat
  l : list nat
  IHl : count n (insert n l) = 1 + count n l
  ============================
   (if beq_nat n n
    then S (if beq_nat n a then S (count n l) else count n l)
    else if beq_nat n a then S (count n l) else count n l) =
   S (if beq_nat n a then S (count n l) else count n l)

subgoal 2 is:
 count n (a :: insert n l) =
 S (if beq_nat n a then S (count n l) else count n l)

rewrite <- beq_nat_refl.

2 subgoals
  
  n : nat
  a : nat
  l : list nat
  IHl : count n (insert n l) = 1 + count n l
  ============================
   S (if beq_nat n a then S (count n l) else count n l) =
   S (if beq_nat n a then S (count n l) else count n l)

subgoal 2 is:
 count n (a :: insert n l) =
 S (if beq_nat n a then S (count n l) else count n l)

reflexivity.

1 subgoal

  

  n : nat

  a : nat

  l : list nat

  IHl : count n (insert n l) = 1 + count n l

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

   count n (a :: insert n l) =

   S (if beq_nat n a then S (count n l) else count n l)

마지막 목적 명제에서 이 식을 먼저 간단하게 변환한다.

simpl.

1 subgoal

  n : nat
  a : nat
  l : list nat
  IHl : count n (insert n l) = 1 + count n l
  ============================
   (if beq_nat n a then S (count n (insert n l)) else count n (insert n l)) =
   S (if beq_nat n a then S (count n l) else count n l)

이제 beq_nat n a의 값에 대한 경우를 나누어 따져봐야 한다. 

case (beq_nat n a).

2 subgoals

  

  n : nat

  a : nat

  l : list nat

  IHl : count n (insert n l) = 1 + count n l

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

   S (count n (insert n l)) = S (S (count n l))

subgoal 2 is:

 count n (insert n l) = S (count n l)

그 결과로 얻은 나머지 두 목적 명제들을 보면 가정 IHl을 가지고 다시 쓰면 등식의 양쪽이 분명하게 같아질 것이다. 다음 명령어들로 이 증명을 결론짓는다. 

rewrite IHl; reflexivity.

rewrite IHl; reflexivity.
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 : 귀납적 증명의 귀납적 경우