[번역] 콕, 빨리빨리 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 : 술어

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

7. 콕 시스템의 숫자

콕 시스템에서 대부분의 데이터 타입을 귀납 타입으로 표현한다. 콕 패키지는 이 데이터 타입에 대한 다양한 성질, 함수, 정리를 제공한다. Arith 패키지는 자연수(0부터 무한대)에 대한 많은 정리들을 포함하고 있다. 자연수는 O(0을 표현하는)과 S를 컨스트럭터로 하는 귀납 타입으로 기술한다.

Print nat.

Inductive nat : Set :=  O : nat | S : nat -> nat

덧셈, 곱셈, 뺄셈 (x - y에서 x가 y보다 작으면 0)도 제공한다. 이 패키지는 ring 전술을 제공하는데, 덧셈과 곱셈의 결합 규칙과 교환 법칙과 배분 법칙 하에 자연수 식들 간의 등식이 성립하는지 증명한다. 이 전술은 뺄셈은 처리하지 않는다. 그 이유는 자연수에 대한 뺄셈의 특별한 정의(역주: 위의 괄호 내용) 때문이다. 앞에서 이미 설명한바와 같이 자연수 구문에 대한 편리 기능이 있다. 예를 들어, 3은 S (S (S O))이다.

자연수를 귀납 타입으로 정의하면 자연수를 받는 재귀 함수를 정의할 수 있다. 재귀 함수 호출에 대한 제약이 있다. 주어진 인자의 바로 앞 숫자를 재귀함수 호출의 인자로 사용하는 그러한 함수를 쉽게 정의할 수 있을 것이다. 예를 들어, 팩토리얼 함수이다.

Fixpoint nat_fact (n:nat) : nat :=
    match n with O => 1 | S p => S p * nat_fact p end.

피보나치 함수의 정의다.

Fixpoint fib (n:nat) : nat :=
    match n with
       O => 0
    | S q => 
       match q with 
           O => 1
       |   S p => fib p + fib q
       end
    end.

ZArith 패키지는 정수를 표현하는 두 가지 데이터 타입을 제공한다. 양의 정수 (1부터 무한대)를 모델하는 이진 표현의 positive 귀납 타입과 세 개의 컨스트럭터(양의 정수, 음의 정수, 0을 구분하는)를 갖는 타입 Z이다. 이 패키지는 순서 개념과 덧셈, 뺄셈, 곱셈, 나눗셈, 루트와 같은 기본 연산을 제공한다. ring 전술은 정수에 대해서도 적용할 수 있다. 이번에는 뺄셈도 잘 지원한다. omega 전술은 nat 타입에 대한 선형식과 Z 타입의 선형식에 대해서도 잘 적용된다.

자연수가 아니라 정수를 가지고 작업하려면, 콕 시스템에게 모든 수에 관한 표기법을 정수에 관련된 표기법으로 해석하도록 요청하는 것이 편리하다. 다음 명령어를 사용한다.

Open Scope Z_scope.

타입 Z는 구조적 재귀에 적합하지 않다. 그래서 입력으로 양의 정수나 음의 정수를 받는 재귀 함수를 정의하는 것은 쉽지 않다. 이 문제를 해결하는 주요 방법은 [1]에서 설명한 기초가 튼튼한 재귀를 사용하는 것이다. 또다른 해결 방법은 반복자에 의존하는 것이다. 반복자는 동일한 연산을 주어진 횟수만큼 반복하는 연산이다. 횟수는 정수로 지정한다. 이 방법은 앞의 방법에 비해 강력하지는 않지만 이해하기 쉬운 장점이 있다. 이 반복자를 iter라 한다.

Check iter.
iter : Z -> forall A : Type, (A -> A) -> A -> A    

예를 들어, 팩토리얼 함수를 다시 정의해서 테스트해보자. 입력으로 한 쌍의 숫자를 받아 다시 한 쌍의 숫자를 반환하는 보조 함수를 사용한다. n과 n!을 입력하면 출력은 n+1과 (n+1)!이다. 이 함수를 iter의 입력으로 준다.

Definition fact_aux (n:Z) :=
  iter n (Z*Z) (fun p => (fst p + 1, snd p * (fst p + 1))) (0, 1).

Definition Z_fact (n:Z) := snd (fact_aux n).

Eval vm_compute in Z_fact 100.
93326...

iter로 정의한 함수의 성질을 증명하기 위해서 이 튜토리얼에서 설명한 내용으로 부족하다. 튜토리얼의 마지막에 관련 연습문제와 해를 제공한다.

이제부터 다시 자연수만 다루도록 돌아간다. 콕 시스템에게 다음 명령어를 주어 정수 표기법에 대한 규정을 해제한다.

Close Scope Z_scope.



===
번역

(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 : 반복자

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

6. 새로운 데이터 타입 정의하기

숫자, 부울값, 리스트는 모두 데이터 타입의 예이다. 프로그래밍할때 종종 새로운 데이터 타입이 필요하다. 그 데이터는 어떤 경우들을 모아놓은 것이고 각각의 경우에 해당하는 필드들을 가지고 있음을 표현한다.  콕 시스템은 이런 방식의 데이터 구성을 표현하는데 편리한 방법을 제공한다.

6.1 귀납 타입을 정의하기

여기에 귀납 타입을 정의하는 예가 있다.

Inductive bin : Type :=
   L : bin
| N : bin -> bin -> bin.

이것은 새로운 타입 bin을 만든다. bin의 타입은 Type이다. 이 bin 타입으로 두 가지 경우를 따르는 데이터를 표현한다. 첫번째 경우는 L로 표기하고 필드가 없다. 두번째 경우는 N t1 t2와 같이 쓰고 bin 타입의 두 개의 필드가 있다. 즉, bin 타입의 원소는 상수 L을 취하거나 N을 bin 타입의 두 객체에 적용하는 두가지 다른 방법으로 만들수 있다.

Check N L (N L L)
N L (N L L)
     : bin

이 bin 타입은 내부 노드나 끝 노드에 별도의 정보를 가지고 있지 않는 이진 트리를 포함한다.

데이터 타입 정의에 대한 연습문제

세 가지 경우를 표현하는 데이터 타입을 정의하시오.  상수, 세개의 필드(숫자, 지금 정의하고 있는 데이터 타입의 값 두 개)를 갖는 경우, 네개의 필드(부울값, 지금 정의하는 데이터 타입의 값 세 개)를 갖는 경우를 표현해야한다.

6.2 패턴 매칭

귀납 타입의 원소는 패턴 매칭을 하는 함수로 처리할 수 있다. 예를 들어 인자로 N L L이면 false를 그 외의 형태를 받으면 true를 반환하는 함수를 작성할 수 있다.

Definition example7 (t : bin): bool :=
   match t with N L L => false | _ => true end.

6.3 재귀함수 정의

귀납 데이터 타입이라면 어떠한 것에 대해서도 Fixpoint 명령어를 사용하여 재귀 함수를 정의할 수 있다. 하지만 자연수와 리스트에서 처럼 동일한 구조적 재귀 규칙을 반드시 따라야 한다. 즉, 오직 변수에 대해서만 재귀함수 호출을 할 수 있고 이 변수는 처음 주어진 인자에서 패턴 매칭을 통해 얻는 것이어야 한다. 다음은 우리가 새로 정의한 데이터 타입에 대한 재귀함수의 예제이다.

Fixpoint flatten_aux (t1 t2:bin) : bin :=
   match t1 with
       L => N L t2
   | N t'1 t'2 => flatten_aux t'1 (flatten_aux t'2 t2)
   end.

Fixpoint flatten (t:bin) : bin :=
   match t with
       L => L 
   | N t1 t2 => flatten_aux t1 (flatten t2))
   end.

Fixpoint size (t:bin) : nat :=
   match t with
       L => 1 | N t1 t2 => 1 + size t1 + size t2
   end.

사용자가 정의한 데이터 타입에 대한 구조적 재귀함수를 가지고 계산하는 것은 숫자와 리스트의 경우처럼 비슷하다.

6.4 경우를 나누어 증명

지금까지 우리가 도입한 귀납 타입에 대해 함수들을 정의해보았고, 이제 이 함수들의 성질을 증명할 수 있다. 첫번째 예제에서 bin 타입의 원소에 대한 경우 분석을 한다.

Lemma example7_size :
      forall t, example7 t = false -> size t = 3.

intros t; destruct t.

2 subgoals
  
  ============================
   example7 L = false -> size L = 3

subgoal 2 is:
 example7 (N t1 t2) = false -> size (N t1 t2) = 3

전술 destruct t는 t에 대한 귀납 타입의 정의에 따라 다양한 경우를 따져본다. 식 t는 L로 만든 것일 수도 있고, N을 다른 트리 t1과 t2에 적용한 결과일 가능성도 있다. 따라서 이 전술을 쓰면 두 가지 목적 명제가 나온다. 

트리 L에 대해서 example7과 size의 결과 값을 알고 있다. 콕 시스템에게 요청해서 그것을 계산한다. 

simpl.

2 subgoals

  

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

   true = false -> 1 = 3

subgoal 2 is:

 example7 (N t1 t2) = false -> size (N t1 t2) = 3

이 계산을 하면 example7 L이 true이므로 false이기를 기대하는 것과 다름을 발견한다. 아래의 전술로 이런 비일관성을 다룬다. 

intros H.

2 subgoals

  

  H : true = false

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

   1 = 3

subgoal 2 is:

 example7 (N t1 t2) = false -> size (N t1 t2) = 3

discriminate H.

1 subgoal

  

  t1 : bin

  t2 : bin

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

   example7 (N t1 t2) = false -> size (N t1 t2) = 3

그 결과 첫번째 목적 명제를 증명했다. discriminate H 전술은, 가정 H가 귀납 타입에서 두 개의 다른 컨스트럭터[역주: bin 타입의 컨스트럭터는 L과 N이다.]가 같은 값을 반환한다고 선언할 때 사용할 수 있다. 그런 가정은 일관성이 없고, 이 전술은 이 일관성을 직접 이용해서 이러한 경우는 결코 일어날 수 없음을 표현한다. 

귀납 타입의 컨스트럭터는 단사적이다는 또다른 중요한 성질이 있다. 이것에 대해서는 나중에 6.6절에서 설명한다. 

두번째 목적 명제에 대해서도 t1과 t2의 값에 대해 경우 분석을 해야 한다. 자세한 증명은 생략한다. 다음에 나열한 전술들을 사용하여 완료할 수 있다. 

destruct t1.

2 subgoals

  

  t2 : bin

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

   example7 (N L t2) = false -> size (N L t2) = 3

subgoal 2 is:

 example7 (N (N t1_1 t1_2) t2) = false -> size (N (N t1_1 t1_2) t2) = 3

destruct t2.

3 subgoals

  

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

   example7 (N L L) = false -> size (N L L) = 3

subgoal 2 is:

 example7 (N L (N t2_1 t2_2)) = false -> size (N L (N t2_1 t2_2)) = 3

subgoal 3 is:

 example7 (N (N t1_1 t1_2) t2) = false -> size (N (N t1_1 t1_2) t2) = 3

첫번째 목적 명제에 있는 함수를 계산하도록 콕 시스템에 요청한다.

simpl.

3 subgoals

  

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

   false = false -> 3 = 3

subgoal 2 is:

 example7 (N L (N t2_1 t2_2)) = false -> size (N L (N t2_1 t2_2)) = 3

subgoal 3 is:

 example7 (N (N t1_1 t1_2) t2) = false -> size (N (N t1_1 t1_2) t2) = 3

함축의 오른편이 참이므로 콕 시스템은 자동으로 이것을 증명할 수 있다. 전술 테이블을 참조해서 더 기초적인 방법으로 증명하려면 intro와 reflexivity 전술을 차례로 사용할 수 있다.

auto.

2 subgoals

  

  t2_1 : bin

  t2_2 : bin

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

   example7 (N L (N t2_1 t2_2)) = false -> size (N L (N t2_1 t2_2)) = 3

subgoal 2 is:

 example7 (N (N t1_1 t1_2) t2) = false -> size (N (N t1_1 t1_2) t2) = 3

intros H; discriminate H.

intros H; discriminate H.

Qed.

6.5 귀납적 증명

귀납 타입에 대한 가장 일반적인 증명이 귀납적 증명이다. 이 방법으로 귀납 타입 원소에 대한 성질을 증명할때 사실 우리는 각 컨스트럭터로 분류되는 경우를 따지고 있는 것이다. 마치 경우 분석에서 했던 것 처럼 말이다. 물론 변형된 부분도 있다. 귀납 타입의 인자를 갖는 컨스트럭터를 다룰때 이러한 인자에 대해서 증명하려고 하는 성질이 성립한다고 가정할 수 있다.

목적 지향적인 증명을 할때 elim 전술로 귀납 원리를 사용한다. 이 전술을 설명하기 위해 flatten_aux와 size 함수에 대한 간단한 사실 명제를 증명할 것이다.

Lemma flatten_aux_size : 
   forall t1 t2, size (flatten_aux t1 t2) = size t1 + size t2 + 1.

induction t1.

2 subgoals
  
  ============================
   forall t2 : bin, size (flatten_aux L t2) = size L + size t2 + 1

subgoal 2 is:
 forall t2 : bin,
 size (flatten_aux (N t1_1 t1_2) t2) = size (N t1_1 t1_2) + size t2 + 1

두 개의 목적 명제가 생기는데, 첫번째는 flatten_aux의 첫번째 인자가 L일때, 두번째는 N t1_1 t1_2일때 보조 정리의 명제를 증명하는 것이다. 두 함수의 정의를 사용하면 증명을 쉽게 진행할 수 있다. 콕 시스템에서 simple 전술을 사용한다. 얻은 결과는 ring 전술로 해결한다.

intros t2.

simpl.

2 subgoals

  

  t2 : bin

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

   S (S (size t2)) = S (size t2 + 1)

subgoal 2 is:

 forall t2 : bin,

 size (flatten_aux (N t1_1 t1_2) t2) = size (N t1_1 t1_2) + size t2 + 1

ring.

1 subgoal

  

  t1_1 : bin

  t1_2 : bin

  IHt1_1 : forall t2 : bin,

           size (flatten_aux t1_1 t2) = size t1_1 + size t2 + 1

  IHt1_2 : forall t2 : bin,

           size (flatten_aux t1_2 t2) = size t1_2 + size t2 + 1

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

   forall t2 : bin,

   size (flatten_aux (N t1_1 t1_2) t2) = size (N t1_1 t1_2) + size t2 + 1

두번째 목적 명제를 증명할때, t1_1과 t1_2에 대한 귀납 가정을 사용할 수 있다. 다시 한번 size와 flatten_aux 함수를 호출한 결과 값을 콕 시스템으로 하여금 계산하도록 명령을 내릴 수 있다. 그 다음 귀납 가정을 사용할 수 있다.

intros t2; simpl.

1 subgoal

  

  t1_1 : bin

  t1_2 : bin

  IHt1_1 : forall t2 : bin,

           size (flatten_aux t1_1 t2) = size t1_1 + size t2 + 1

  IHt1_2 : forall t2 : bin,

           size (flatten_aux t1_2 t2) = size t1_2 + size t2 + 1

  t2 : bin

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

   size (flatten_aux t1_1 (flatten_aux t1_2 t2)) =

   S (size t1_1 + size t1_2 + size t2 + 1)

rewrite IHt1_1

1 subgoal

  

  t1_1 : bin

  t1_2 : bin

  IHt1_1 : forall t2 : bin,

           size (flatten_aux t1_1 t2) = size t1_1 + size t2 + 1

  IHt1_2 : forall t2 : bin,

           size (flatten_aux t1_2 t2) = size t1_2 + size t2 + 1

  t2 : bin

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

   size t1_1 + size (flatten_aux t1_2 t2) + 1 =

   S (size t1_1 + size t1_2 + size t2 + 1)

rewrite IHt1_2

1 subgoal

  

  t1_1 : bin

  t1_2 : bin

  IHt1_1 : forall t2 : bin,

           size (flatten_aux t1_1 t2) = size t1_1 + size t2 + 1

  IHt1_2 : forall t2 : bin,

           size (flatten_aux t1_2 t2) = size t1_2 + size t2 + 1

  t2 : bin

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

   size t1_1 + (size t1_2 + size t2 + 1) + 1 =

   S (size t1_1 + size t1_2 + size t2 + 1)

ring.

Proof completed.

Qed.

flatten과 size에 대한 연습문제

Lemma flatten_size : forall t, size (flatten t) = size t.

flatten_aux_size 보조 정리를 사용하되 apply 전술이나 rewrite 전술을 함께 고려해야 한다.

6.6 injection 전술을 사용하는 예제

이번에는 injection 전술을 사용하는 증명의 예를 설명한다. 어떠한 트리도 자신의 부분을 구성할 수 없음을 증명한다.

Lemma not_subterm_self_l : forall x y, ~ x = N x y.

1 subgoal
  
  ============================
   forall x y : bin, x <> N x y

이 목적 명제에 등식의 부정을 _ <> _로 표시함을 볼 수 있다. x에 대한 귀납적 증명을 한다.

induction x.

2 subgoals

  

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

   forall y : bin, L <> N L y

subgoal 2 is:

 forall y : bin, N x1 x2 <> N (N x1 x2) y

첫번째 목적 명제는 이 귀납 타입의 두 컨스트럭터가 다르다는 것이다. discriminate 전술을 사용한다. 첫번째를 해결하고 두번째 목적 명제를 보자.

intros y; discriminate.

1 subgoal

  

  x1 : bin

  x2 : bin

  IHx1 : forall y : bin, x1 <> N x1 y

  IHx2 : forall y : bin, x2 <> N x2 y

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

   forall y : bin, N x1 x2 <> N (N x1 x2) y

이 목적 명제의 결론이 부정 형태이므로 전술 테이블을 참고해서 해당하는 전술을 선택할 수 있다. 이 예에서, 사실 명제의 부정은 이 사실 명제는 False를 함축한다라는 함수로 표현할 수도 있음을 보여준다. 

intros y abs.

1 subgoal

  

  x1 : bin

  x2 : bin

  IHx1 : forall y : bin, x1 <> N x1 y

  IHx2 : forall y : bin, x2 <> N x2 y

  y : bin

  abs : N x1 x2 = N (N x1 x2) y

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

   False

가정 abs는 N x1 x2와 N (N x1 x2) y가 동등함을 표현한다. 컨스트럭터 N은 두 인자에 대해 단사적이어서 x1이 N x1 x2와 같다는 것을 함축한다. 이러한 유추 과정을 injection 전술로 표현한다.

injection abs.

1 subgoal

  

  x1 : bin

  x2 : bin

  IHx1 : forall y : bin, x1 <> N x1 y

  IHx2 : forall y : bin, x2 <> N x2 y

  y : bin

  abs : N x1 x2 = N (N x1 x2) y

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

   x2 = y -> x1 = N x1 x2 -> False

그 결과 두 개의 등식이 함축의 전제로 이 목적 명제의 결론에 도입되었다. 이 등식들을 새로운 가정으로 도입할 수 있다. 

intros h2 h1.

1 subgoal

  

  x1 : bin

  x2 : bin

  IHx1 : forall y : bin, x1 <> N x1 y

  IHx2 : forall y : bin, x2 <> N x2 y

  y : bin

  abs : N x1 x2 = N (N x1 x2) y

  h2 : x2 = y

  h1 : x1 = N x1 x2

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

   False

가정 h1과 IHx1(을 사례화 시킨 명제)는 서로 모순이다. 다음 전술로 이것을 표현한다.

assert (IHx1' : x1 <> N x1 x2).

2 subgoals

  

  x1 : bin

  x2 : bin

  IHx1 : forall y : bin, x1 <> N x1 y

  IHx2 : forall y : bin, x2 <> N x2 y

  y : bin

  abs : N x1 x2 = N (N x1 x2) y

  h2 : x2 = y

  h1 : x1 = N x1 x2

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

   x1 <> N x1 x2

subgoal 2 is:

 False

   apply IHx1.

1 subgoal

  

  x1 : bin

  x2 : bin

  IHx1 : forall y : bin, x1 <> N x1 y

  IHx2 : forall y : bin, x2 <> N x2 y

  y : bin

  abs : N x1 x2 = N (N x1 x2) y

  h2 : x2 = y

  h1 : x1 = N x1 x2

  IHx1' : x1 <> N x1 x2

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

   False

case IHx1'.

[역주: IHx1'이 true와 false 경우 분석. true 경우는 False 결론을 낼 수없으므로 쉽게 배제. 남은 경우는 IHx1' = false.] 

1 subgoal

  

  x1 : bin

  x2 : bin

  IHx1 : forall y : bin, x1 <> N x1 y

  IHx2 : forall y : bin, x2 <> N x2 y

  y : bin

  abs : N x1 x2 = N (N x1 x2) y

  h2 : x2 = y

  h1 : x1 = N x1 x2

  IHx1' : x1 <> N x1 x2

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

   x1 = N x1 x2

exact h1.

Proof completed.

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 : 귀납적 증명의 귀납적 경우

(6장)
datatype : 타입, 데이터 타입
Binary tree : 이진 트리
Internal Node : 내부 노드
Leaf : 끝 노드
Proof by Cases : 경우를 나누어 증명
Constructor : 컨스트럭터
Injective : 단사적

[번역] 콕, 빨리빨리 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 : 귀납적 증명의 귀납적 경우

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

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