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 : 술어



Posted by lazyswamp :