[Coq 증명기] 콕, 빨리 빨리: 4장 숫자 프로그램의 성질을 증명하기

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

자연수에 대해 계산하는 프로그램의 성질을 증명하기위해 보통 여러 계산과정이 어떤 방식으로 연관되어 있음을 보일수 있다. 주어진 함수가 재귀방식이면 대개 귀납적 방식으로  증명한다. 이때 알아야할 전술은 다음과 같다.

• induction 전술은 자연수 n에 대한 귀납적 증명을 한다. 증명을 두 부분으로 나누어, 우선 n이 0일때 증명하고자하는 성질이 성립함을 확인한다. 그 다음 p에 대한 성질로부터 S p에 대한 성질을 증명한다. p에 대한 가정을 귀납적 가정이라 부르고 IH로 시작하는 이름을 보통 붙인다. 이 전술은 0에 대한 목적 명제와 S p에 대한 목적 명제 두 개를 만든다. 
• simpl 전술은 복잡한 인자를 갖는 재귀함수 호출을 해당하는 값으로 대체한다. 함수의 정의에 의해 이 값을 결정한다. 
• discriminate 전술은 0 = S ...이나 true = false와 같이 선언하는 가정이 있을때 유용하다.
• injection 전술은 S x = S y 모양의 가정에서 x = y를 알아내는데 도움이 된다. 

4.1 귀납적 증명

증명 예제를 살펴보자. 0부터 n개의 자연수들의 합이 잘 알려진 다항식을 이룬다는 것을 증명해보자.

Lemma sum_n_p : forall n, 2 * sum_n n + n = n * n.

induction n.

2 subgoals

  

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

   2 * sum_n 0 + 0 = 0 * 0

subgoal 2 is:

 2 * sum_n (S n) + S n = S n * S n

새로 생성된 두 목적 명제에서, 첫번째 것은 n을 0으로 바꾸었고, 두번째는 n을 S n으로 바꾼것이다.  두번째 목적 명제에서 n에 대해 성립한다는 가정은 표시되어 있지 않다. 

첫번째 목적 명제는 매우 쉽다. sum_n, 덧셈, 곱셈의 정의에 의하면 등식의 양쪽이 모두 0이기 때문이다. reflexivity 전술로 해결한다. 

reflexivity.

이 전술을 쓰면 두번째 목적 명제만 남았고 콕 시스템에서 전체를 보여준다. 이제 귀납적 가정을 볼 수 있다. 

1 subgoal

  

  n : nat

  IHn : 2 * sum_n n + n = n * n

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

   2 * sum_n (S n) + S n = S n * S n

여기에서 조금 생각할 필요가 있다. S n * S n을 n * n이 나타나는 식으로 펼칠수 있다. 그 다음 IHn으로 오른편에서 왼쪽 방향으로 다시 쓸 수 있다. assert  전술을 사용해 S n * S n과 새로운 값이 같다고 임시로 선언하고, ring 전술로 이 동등 선언이 사실 성립함을 보인다. 

assert (SnSn : S n * S n = n * n + 2 * n + 1).

2 subgoals

  

  n : nat

  IHn : 2 * sum_n n + n = n * n

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

   S n * S n = n * n + 2 * n + 1

subgoal 2 is:

 2 * sum_n (S n) + S n = S n * S n

ring.

1 subgoal

  

  n : nat

  IHn : 2 * sum_n n + n = n * n

  SnSn : S n * S n = n * n + 2 * n + 1

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

   2 * sum_n (S n) + S n = S n * S n

rewrite SnSn.

1 subgoal

  

  n : nat

  IHn : 2 * sum_n n + n = n * n

  SnSn : S n * S n = n * n + 2 * n + 1

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

   2 * sum_n (S n) + S n = n * n + 2 * n + 1

이번에는 귀납적 가정을 이용해서 n * n을 2 * sum_n n + n으로 다시 쓴다. 

rewrite <- IHn.

1 subgoal

  

  n : nat

  IHn : 2 * sum_n n + n = n * n

  SnSn : S n * S n = n * n + 2 * n + 1

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

   2 * sum_n (S n) + S n = 2 * sum_n n + n + 2 * n + 1

다음 단계에서 sum_n (S n)을 정의에 따라 펼쳐서 그 값을 sum_n n으로 표현해본다. simpl 전술을 사용하는데, 이것은 sum_n 뿐만 아니라 곱셈도 그 정의에 따라 펼치는 것을 시도한다.

sumpl.

1 subgoal

  

  n : nat

  IHn : 2 * sum_n n + n = n * n

  SnSn : S n * S n = n * n + 2 * n + 1

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

   n + sum_n n + (n + sum_n n + 0) + S n =

   sum_n n + (sum_n n + 0) + n + (n + (n + 0)) + 1

그 다음 단계에서 ring 전술을 사용해서 목적 명제의 등식이 덧셈의 결합성과 교환 규칙에 의해 성립함을 보인다.

ring.

Qed.

4.2 귀납에서 더 강력한 문장

재귀 함수가 몇 단계의 패턴 매칭을 사용한다면 연속적인 여러 개의 숫자들에 대해 성질을 기술하는 문장을 증명하는 것이 낫다. evenb 함수에 대한 증명의 예로 살펴보자.

Lemma evenb_p : forall n, evenb n = true -> exists x, n = 2 * x.

assert (Main: forall n, (evenb n = true -> exists x, n = 2 * x) /\

                    (evenb (S n) = true -> exists x, S n = 2 * x)).

여기에서 원래 목적 명제보다 더 강력한 문장을 증명해본다. 즉, n 뿐만 아니라 S n에 대해서도 성립함을 증명한다. 그 다음 이전처럼 귀납 방식으로 진행한다. 더 강력한 문장을 귀납 방식으로 증명하는 것은 재귀함수 증명에서 흔히 볼 수 있다.

induction n.

3 subgoals

  

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

   (evenb 0 = true -> exists x : nat, 0 = 2 * x) /\

   (evenb 1 = true -> exists x : nat, 1 = 2 * x)

subgoal 2 is:

 (evenb (S n) = true -> exists x : nat, S n = 2 * x) /\

 (evenb (S (S n)) = true -> exists x : nat, S (S n) = 2 * x)

subgoal 3 is:

 forall n : nat, evenb n = true -> exists x : nat, n = 2 * x

첫번째 목적 명제는 두 부분으로 나뉜다. 처음 부분은 결론에 나타난 존재 한정이 있는 문장이다. 전술 테이블을 보면 exists 전술로 어떤 값을 주면 된다. 이 경우 x의 값을 0으로 놓으면 0 = 2 * 0이 성립함을 쉽게 알 수 있다. 두번째 부분은 다르다. x의 값으로 놓을 수 있는 것이 없다. 하지만 evenb 1 = true는 성립하지 않는다. 왜냐하면 evenb 1은 false이고 false = true는 불가능하기 때문이다. 일관성이 없는 경우는 discriminate 전술을 사용한다.

split.

   exists 0; ring.

simpl; intros H; discriminate H.

나머지 증명에 대해 자세히 설명하지 않는다. 독자 스스로 증명해볼 것을 권한다. 

  split.

    destruct IHn as [_ IHn'].

    exact IHn'.

  simpl.

  intros H.

  destruct IHn as [IHn' _].

  assert (H' : exists x, n = 2 * x).

    apply IHn'.

    exact H.

  destruct H' as [x q].

  exists (x + 1).

  rewrite q.

  ring.

가정 Main을 일단 증명하면 원래 증명하려고 했던 명제로 돌아갈수 있다. 이때 firstorder 전술로 증명을 마무리할 수 있다. 설명을 위해 다른 방법을 보여줄 것이다.

1 subgoal

  

  Main : forall n : nat,

         (evenb n = true -> exists x : nat, n = 2 * x) /\

         (evenb (S n) = true -> exists x : nat, S n = 2 * x)

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

   forall n : nat, evenb n = true -> exists x : nat, n = 2 * x

intros n ev.

1 subgoal

  

  Main : forall n : nat,

         (evenb n = true -> exists x : nat, n = 2 * x) /\

         (evenb (S n) = true -> exists x : nat, S n = 2 * x)

  n : nat

  ev : evenb n = true

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

   exists x : nat, n = 2 * x

여기서 지금까지 언급하지 않았던 콕 시스템의 한가지 편의 기능을 사용할 수 있다. 정리의 문장이 전칭 한정이거나 함축의 형태이면 이 정리를 마치 함수인 것 처럼 쓸 수 있다. 어떤 식에 적용하면 이것으로 사례화된 새로운 정리를 얻을 수 있다. 위의 예에서 Main 가정을 사용해서 n에 대해 사례화시킬수 있다. 

  destruct (Main n) as [H _].

  apply H.

  exact ev.

Qed.

덧셈에 다른 정의에 관한 연습문제

자연수에 대한 덧셈을 새롭게 정의할 수 있다.

Fixpoint add n m := match n with 0 => m | S p => add p (S m) end.

다음을 증명하시오.

forall n m, add n (S m) = S (add n m)

forall n m, add (S n) m = S (add n m)

forall n m, add n m = n + m

새로운 연습문제를 증명할때 이전에 증명한 보조 정리를 사용할 수 있다.

홀수의 합에 대한 연습문제

앞에서부터 n개의 홀수를 모두 더한 합은 다음 함수로 정의한다.

Fixpoint sum_odd_n (n:nat) : nat :=

   match n with 0 => 0 | S p => 1 + 2 * p + sum_odd_n p end.

다음 문장을 증명하시오.

forall n:nat, sum_odd_n n = n * n

===

번역

(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 : 보조 정리