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

8. 귀납적 성질

귀납적 정의로 새로운 술어를 기술할 수도 있다. 타입 A에 대한 술어는 A 타입의 원소를 입력 받아 명제 타입 Prop의 원소를 반환하는 함수로 간단히 기술할 수 있다. 귀납적 명제의 컨스트럭터는 술어로 규정하는 정리들이다. 이 술어에 기반한 문장에 대한 증명은 오직 이 컨스트럭터의 조합으로만 얻을 수 있다.

8.1 귀납적 술어 정의하기

짝수 자연수 집합을 뜻하는 술어를 다음과 같이 귀납적 정의를 쓸 수 있다.

Inductive even : nat -> Prop :=
   even0 : even 0
| evenS : forall x:nat, even x -> even (S (S x)).


x가 자연수라면 even x는 명제이다. 정리 even0는 even 0 명제를 증명할 때 사용하고, 정리 evenS는 명제 even 0로 부터 명제 even 2를 추론할 때 쓸 수 있다. evenS를 반복해서 사용하면 나머지 숫자들도 even 술어를 만족함을 증명하는데 이용할 수 있다.

귀납 타입처럼 case, elim, destruct 전술들을 사용해서 귀납 명제에 관련된 가정에 대해 추론할 수 있다. 이 전술들을 쓰면 귀납 정의의 각 컨스트럭터 별로 하나씩 목적 명제를 다시 만들어 낼 것이다. 덧붙이자면 컨스트럭터가 전제로 귀납 명제를 사용하면 elim과 induction 전술은 귀납 가정을 만든다.

8.2 귀납적 술어에 대한 귀납 증명

변수 x가 귀납적 성질을 만족한다면 그 변수 자체에 대한 귀납을 사용하는 것 보다 귀납적 성질에 대한 귀납을 사용해서 그 변수에 대한 성질을 증명하는 것이 종종 더 효율적이다. 다음 증명의 예를 보자.

Lemma even_mult : forall x, even x -> exists y, x = 2 * y.
intros x H; elim H.

2 subgoals
  
  x : nat
  H : even x
  ============================
   exists y : nat, 0 = 2 * y

subgoal 2 is:
 forall x0 : nat,
 even x0 -> (exists y : nat, x0 = 2 * y) -> exists y : nat, S (S x0) = 2 * y

첫번째 목적 명제는 even의 첫번째 컨스트럭터를 사용해주 even x를 증명하는 경우이다. 이때 변수 x는 0으로 바꾸어 이 목적 명제를 표시한다. y를 0으로 놓고 증명할 수 있다.

exists 0; ring.

1 subgoal

  

  x : nat

  H : even x

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

   forall x0 : nat,

   even x0 ->

   (exists y : nat, x0 = 2 * y) -> exists y : nat, S (S x0) = 2 * y

그 다음 목적 명제는 even의 두번째 컨스트럭터를 가지고 even x를 증명하는 경우에 대한 것이다. 이때 x가 S (S x0)인 변수 x0가 반드시 존재해야 한다. 그리고 elim 전술은 even x0에 대한 귀납 가정을 도입한다. 이렇게 x0는 S (S x0)에 대해 증명할 성질을 만족할 것으로 가정한다. 이런 점에서 elim 전술은 귀납 가정을 생성한다. 이는 마치 induction 전술에서와 정확히 같다. 사실 elim대신 induction 전술을 쓸 수 있다. 두 전술은 거의 똑같다. 

intros x0 Hevenx0 IHx.

1 subgoal

  

  x : nat

  H : even x

  x0 : nat

  Hevenx0 : even x0

  IHx : exists y : nat, x0 = 2 * y

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

   exists y : nat, S (S x0) = 2 * y

이제 IHx는 귀납 가정이다. x가 x0의 다음 다음이라면 x0의 반이되는 값 y가 존재함을 이미 알고 있음을 뜻한다. 이 값을 S (S x0)의 반을 구하기 위해 이용한다. 다음의 전술을 사용해서 증명을 완료한다.

destruct IHx as [y Heq].

rewrite Heq.

exists (S y).

ring.

destruct 전술을 이전과 다르게 사용했다. 이 전술로 원소를 새로 만들어 이름을 붙이고, 이 이름을 문맥에 도입한다. 

8.3 inversion 전술

inversion 전술은 귀납적 명제에 관한 문장을 증명하는 다양한 방법에서 쓰일 수 있다. 이 전술은 귀납적 명제의 모든 컨스트럭터를 분석하고, 적용할 수 없는 것은 버리며, 적용가능한 컨스트럭터에 대해서 새로운 목적 명제를 만들고 이 컨스트럭터의 전제들을 문맥에 불러들인다. 예를 들어, 1이 짝수가 아님을 증명하는데 매우 적합하다. 왜냐하면 어떤한 컨스트럭터도 명제 even 1로 결론짓지 않기 때문이다. evenS는1 = S (S x)를 증명해야하고, even0는 1=0을 증명해야하는데 모두 거짓이다.

Lemma not_even_1 : ~even 1.

intros even1.

1 subgoal

  

  even1 : even 1

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

   False

inversion even1.

Qed.

inversion 전술을 사용하는 다른 예로, 짝수의 이전 이전 수는 짝수임을 증명해보자. 이 문장에서 주어진 수를 S (S x)로 놓고 이전 이전 수를 x로 놓자.

Lemma even_inv : forall x, even (S (S x)) -> even x.

intros x H.

1 subgoal

  

  x : nat

  H : even (S (S x))

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

   even x

이 전술에서 even 술어의 컨스트럭터들을 분석하면 even0를 사용해서 가정 H를 증명할 수 없음을 인식한다. 오직 evenS만 사용될 수 있다. 그러므로 even x0와 S (S x) = S (S x0)가 성립하는 x0가 반드시 존재해야 한다. 즉, even x가 성립한다.

inversion H.

1 subgoal

  

  x : nat

  H : even (S (S x))

  x0 : nat

  H1 : even x

  H0 : x0 = x

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

   even x

assumption.

Qed.

even_inv의 문장은 evenS 문장의 반대임을 참고하시오. 이 전술의 이름을 이렇게 붙이 이유이다. 

귀납적 성질은 매우 복잡한 개념을 표현하는데 사용할 수 있다. 프로그래밍 언어의 의미를 귀납적 정의로 정의할 수 있다. 기본적인 계산 단계에 각각 해당하는 컨스트럭터들을 도입할 수 있다. 

===
번역

(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 : 단사적

(7장)
Well-founded : 기초가 튼튼한(?)
Iterator : 반복자

(8장)

Predicate : 술어