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
1. 식과 논리식
2. 콕으로 프로그래밍하기
3. 명제와 증명
4. 숫자 프로그램의 성질을 증명하기
5. 리스트 프로그램의 성질을 증명하기
6. 새로운 데이터 타입 정의하기
7. 콕 시스템의 숫자
8. 귀납적 성질
9. 연습문제 (원문 참고)
10. 해답 (원문 참고)
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 : 반복자
- 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 : 반복자
No comments:
Post a Comment