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 : 술어
'Coq 증명기' 카테고리의 다른 글
소프트웨어 기초(Software Foundations) (0) | 2017.09.11 |
---|---|
타입이 다른 원소들의 리스트 (Heterogeneous Lists) (0) | 2014.08.26 |
[Coq 증명기] 콕, 빨리 빨리: 7장 콕 시스템의 숫자 (0) | 2014.08.09 |
[Coq 증명기] 콕, 빨리 빨리: 6장 새로운 데이터 타입 정의하기 (0) | 2014.08.09 |
[Coq 증명기] 콕, 빨리 빨리: 5장 리스트 프로그램의 성질을 증명하기 (0) | 2014.08.09 |