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]을 보면 된다. 특히 방대한 연습문제가 있어 훈련하기에 좋다.
참고 문헌
[1] Yves Bertot and Pierre Cast ́eran. Interactive Theorem Proving and Program Devel- opment, Coq’Art:the Calculus of Inductive Constructions. Springer-Verlag, 2004.
[2] The Coq development team. The Coq proof Assistant Reference Manual, Ecole Polytechnique, INRIA, Universit de Paris-Sud, 2004. http://coq.inria.fr/doc/ main.html
목차
1. 식과 논리식
2. 콕으로 프로그래밍하기
3. 명제와 증명
4. 숫자 프로그램의 성질을 증명하기
5. 리스트 프로그램의 성질을 증명하기
6. 새로운 데이터 타입 정의하기
7. 콕 시스템의 숫자
8. 귀납적 성질
9. 연습문제 (원문 참고)
10. 해답 (원문 참고)
콕 시스템은 일종의 언어를 제공한다. 이 언어로 논리식을 다루고, 구문 형태를 살피고, 증명하기도 한다. 논리식은 함수를 사용하여 구성하기도 하고, 제한된 형태지만 이 함수들을 가지고 계산도 한다.
1.1 바른 식 쓰기
먼저 식이 제대로 된 형태인지 검사하는 법을 배울 필요가 있다. 이 명령어는 Check이다. 몇가지 예를 들어보자. 이 시스템의 기초적인 객체와 타입을 두세가지 사용한다. 명령어는 항상 점으로 끝난다. 이제부터 사용자가 콕 시스템에 보내는 글은 이런 스타일이고, 이 시스템에서 응답하는 내용은 이런 스타일이다.
Check True.
True : Prop
Check False.
False : Prop
Check 3.
3 : nat
Check (3+4).
3 + 4 : nat
Check (3=5).
3=5 : Prop
Check (3,4).
(3,4) : nat * nat
Check ((3=5)/\True).
3 = 5 /\ True : Prop
Check nat -> Prop
nat -> Prop : Type
Check (3 <= 6).
3 <= 6 : Prop
두가지 목적으로 A : B 표기법을 사용한다. 식 A의 타입이 식 B이다거나 A는 B의 증명임을 나타낸다. 우리가 입력하는 식에서도 이 표기법을 사용할 수 있다. 보통 어떤 식의 타입을 분명히 드러내고자할때 그렇다.
Check (3,3=5):nat*Prop
(3,3=5):nat * Prop
: nat * Prop
이 식들 중 어떤 것은 논리 명제로 읽고 (즉 Prop 타입을 가지고) 또 어떤 것은 숫자로 읽고(nat 타입을 갖고), 다른 것은 더 복잡한 자료구조의 원소로 읽기도 한다. 물론 제대로 형태를 갖추지 못한 식도도 검사해볼수 있다. 이 경우 콕 시스템은 에러문을 출력해 문제점을 설명해줄것이다.
복잡한 식을 구성하려면 명제들을 논리 연결자들로 조합하거나 덧셈, 곱셈, 쌍만들기 등으로 식들을 구성하면된다. 키워드 fun을 사용해서 새로운 함수도 만들수 있다. 람다계산법과 같은데에서 lambda 기호대신 쓴다. Check 명령어로 함수를 검사하면 nat 타입의 숫자 x를 입력으로 받아 x가 3과 같다는 명제를 리턴한다고 설명해준다. 그 다음 Check 명령어에서 검사하는 논리명제는 모든 자연수 x에 대해 x는 3보다 작거나 또는 자연수 y가 존재해서 x=y+3이다.
Check (fun x:nat => x=3).
fun x : nat => x = 3 : nat -> Prop
Check (forall x:nat, x<3 \/ (exists y:nat, x=y+3)).
forall x:nat, x<3 \/ (exists y:nat, x=y+3) : Prop
이번에는 let을 사용하는 식을 살펴보자. 식에 임시 이름을 부여할 때 유용하다. 예제에서 let으로 이름을 붙인 식은 숫자를 입력받아 숫자의 쌍을 반환하는 함수다. 함수 f를 어떤 값, 예를 들어 3에 적용하는 표기 방법도 보여준다. 단순히 함수 이름 f와 인자 3을 나란히 쓰면된다. 보통 수학에서 하던것과 달리 인자를 감싸는 괄호를 항상 쓰지 않아도 된다.
Check (let f := fun x => (x * 3, x) in f 3).
let f := fun x : nat => (x * 3, x) in f 3 : nat * nat
어떤 표기법은 다용도로 사용된다. 예를 들어, * 기호는 곱셈을 표시하기도 하고 타입에서 곱을 표시하기도 한다. Locate 명령어로 표기법이 의미하는 함수를 찾을 수 있다.
Locate "_ <= _".
Notation Scope
"x <= y" := le x y : nat_scope
(default interpretation)
텀의 형태가 제대로 되려면 두가지 조건을 갖춰야한다. 정해진 구문을 따라야한다. 예를 들어, 열린괄호와 닫힌괄호의 쌍이 맞아야 하고 두개의 피연산자를 요구하는 연산자에게는 그렇게 인자가 주어져야한다. 두번째 조건은 타입에 맞게 식을 구성해야한다. Check 명령어는 식이 제대로 구성되었는지 검사도 하고 식의 타입을 알려주기도한다. 예를 들어 어떤 식이 제대로 되었는지 차근차근 단계별로 확인할 수 있다.
Check True.
True : Prop
Check False.
False : Prop
Check and.
and : Prop -> Prop -> Prop
Check (and True False).
True /\ False : Prop
마지막 예에서 and는 Prop 타입의 인자를 받아 Prop -> Prop 타입의 함수를 반환하는 함수다. 따라서 Prop 타입의 True에 적용할 수 있다. 그 결과 반환되는 함수는 또다른 Prop 타입의 인자를 기대하고 False에 적용할 수 있다. 표기법 a -> b -> c는 사실
a -> (b -> c)이다. 표기법 f a b는 사실 (f a) b 이다.
그리고 /\는 피연산자들 가운데에 연산자를 배치하는 인픽스 표기법을 따른다. Locate 명령어로 확인할 수 있다.
콕 시스템으로 식을 계산할 수도 있다. 기호 계산 방식을 사용하는데, 여러가지 전략이 있다. compute라고 부르는 전략은 다음과 같이 사용한다.
Eval compute in
let f := fun x => (x * 3, x) in f 3.
= (9, 3) : nat * nat
이 명령어를 실행한 뒤에는 함수 f가 사라진다. 이 식을 계산할 때 임시로 정의되고 f 3을 계산할 때 사용될 뿐이다.
함수에 관한 연습문제 (참고문헌 [1]의 연습문제 2.5) 다섯개의 인자를 받아 그 합을 반환하는 함수를 작성하고, Check 명령어로 제대로된 형태로 작성했는지 확인한 다음, Eval 명령어로 샘플 값들을 주어 계산해보시오. 연습문제에 대한 답은 모두 이 글의 마지막에 제공한다.
===
번역
Expressions : 식
Formulas : 식
infix : 인픽스
Logical Formulas : 논리식
Symbolic Computation : 기호 계산
Terms : 텀
Well-formed : 제대로 된 형태
- 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]을 보면 된다. 특히 방대한 연습문제가 있어 훈련하기에 좋다.
참고 문헌
[1] Yves Bertot and Pierre Cast ́eran. Interactive Theorem Proving and Program Devel- opment, Coq’Art:the Calculus of Inductive Constructions. Springer-Verlag, 2004.
[2] The Coq development team. The Coq proof Assistant Reference Manual, Ecole Polytechnique, INRIA, Universit de Paris-Sud, 2004. http://coq.inria.fr/doc/ main.html
목차
1. 식과 논리식
2. 콕으로 프로그래밍하기
3. 명제와 증명
4. 숫자 프로그램의 성질을 증명하기
5. 리스트 프로그램의 성질을 증명하기
6. 새로운 데이터 타입 정의하기
7. 콕 시스템의 숫자
8. 귀납적 성질
9. 연습문제 (원문 참고)
10. 해답 (원문 참고)
1. (계산?)식과 논리식
콕 시스템은 일종의 언어를 제공한다. 이 언어로 논리식을 다루고, 구문 형태를 살피고, 증명하기도 한다. 논리식은 함수를 사용하여 구성하기도 하고, 제한된 형태지만 이 함수들을 가지고 계산도 한다.
1.1 바른 식 쓰기
먼저 식이 제대로 된 형태인지 검사하는 법을 배울 필요가 있다. 이 명령어는 Check이다. 몇가지 예를 들어보자. 이 시스템의 기초적인 객체와 타입을 두세가지 사용한다. 명령어는 항상 점으로 끝난다. 이제부터 사용자가 콕 시스템에 보내는 글은 이런 스타일이고, 이 시스템에서 응답하는 내용은 이런 스타일이다.
Check True.
True : Prop
Check False.
False : Prop
Check 3.
3 : nat
Check (3+4).
3 + 4 : nat
Check (3=5).
3=5 : Prop
Check (3,4).
(3,4) : nat * nat
Check ((3=5)/\True).
3 = 5 /\ True : Prop
Check nat -> Prop
nat -> Prop : Type
Check (3 <= 6).
3 <= 6 : Prop
두가지 목적으로 A : B 표기법을 사용한다. 식 A의 타입이 식 B이다거나 A는 B의 증명임을 나타낸다. 우리가 입력하는 식에서도 이 표기법을 사용할 수 있다. 보통 어떤 식의 타입을 분명히 드러내고자할때 그렇다.
Check (3,3=5):nat*Prop
(3,3=5):nat * Prop
: nat * Prop
이 식들 중 어떤 것은 논리 명제로 읽고 (즉 Prop 타입을 가지고) 또 어떤 것은 숫자로 읽고(nat 타입을 갖고), 다른 것은 더 복잡한 자료구조의 원소로 읽기도 한다. 물론 제대로 형태를 갖추지 못한 식도도 검사해볼수 있다. 이 경우 콕 시스템은 에러문을 출력해 문제점을 설명해줄것이다.
복잡한 식을 구성하려면 명제들을 논리 연결자들로 조합하거나 덧셈, 곱셈, 쌍만들기 등으로 식들을 구성하면된다. 키워드 fun을 사용해서 새로운 함수도 만들수 있다. 람다계산법과 같은데에서 lambda 기호대신 쓴다. Check 명령어로 함수를 검사하면 nat 타입의 숫자 x를 입력으로 받아 x가 3과 같다는 명제를 리턴한다고 설명해준다. 그 다음 Check 명령어에서 검사하는 논리명제는 모든 자연수 x에 대해 x는 3보다 작거나 또는 자연수 y가 존재해서 x=y+3이다.
Check (fun x:nat => x=3).
fun x : nat => x = 3 : nat -> Prop
Check (forall x:nat, x<3 \/ (exists y:nat, x=y+3)).
forall x:nat, x<3 \/ (exists y:nat, x=y+3) : Prop
이번에는 let을 사용하는 식을 살펴보자. 식에 임시 이름을 부여할 때 유용하다. 예제에서 let으로 이름을 붙인 식은 숫자를 입력받아 숫자의 쌍을 반환하는 함수다. 함수 f를 어떤 값, 예를 들어 3에 적용하는 표기 방법도 보여준다. 단순히 함수 이름 f와 인자 3을 나란히 쓰면된다. 보통 수학에서 하던것과 달리 인자를 감싸는 괄호를 항상 쓰지 않아도 된다.
Check (let f := fun x => (x * 3, x) in f 3).
let f := fun x : nat => (x * 3, x) in f 3 : nat * nat
어떤 표기법은 다용도로 사용된다. 예를 들어, * 기호는 곱셈을 표시하기도 하고 타입에서 곱을 표시하기도 한다. Locate 명령어로 표기법이 의미하는 함수를 찾을 수 있다.
Locate "_ <= _".
Notation Scope
"x <= y" := le x y : nat_scope
(default interpretation)
텀의 형태가 제대로 되려면 두가지 조건을 갖춰야한다. 정해진 구문을 따라야한다. 예를 들어, 열린괄호와 닫힌괄호의 쌍이 맞아야 하고 두개의 피연산자를 요구하는 연산자에게는 그렇게 인자가 주어져야한다. 두번째 조건은 타입에 맞게 식을 구성해야한다. Check 명령어는 식이 제대로 구성되었는지 검사도 하고 식의 타입을 알려주기도한다. 예를 들어 어떤 식이 제대로 되었는지 차근차근 단계별로 확인할 수 있다.
Check True.
True : Prop
Check False.
False : Prop
Check and.
and : Prop -> Prop -> Prop
Check (and True False).
True /\ False : Prop
마지막 예에서 and는 Prop 타입의 인자를 받아 Prop -> Prop 타입의 함수를 반환하는 함수다. 따라서 Prop 타입의 True에 적용할 수 있다. 그 결과 반환되는 함수는 또다른 Prop 타입의 인자를 기대하고 False에 적용할 수 있다. 표기법 a -> b -> c는 사실
a -> (b -> c)이다. 표기법 f a b는 사실 (f a) b 이다.
그리고 /\는 피연산자들 가운데에 연산자를 배치하는 인픽스 표기법을 따른다. Locate 명령어로 확인할 수 있다.
2. 식을 계산하기
콕 시스템으로 식을 계산할 수도 있다. 기호 계산 방식을 사용하는데, 여러가지 전략이 있다. compute라고 부르는 전략은 다음과 같이 사용한다.
Eval compute in
let f := fun x => (x * 3, x) in f 3.
= (9, 3) : nat * nat
이 명령어를 실행한 뒤에는 함수 f가 사라진다. 이 식을 계산할 때 임시로 정의되고 f 3을 계산할 때 사용될 뿐이다.
함수에 관한 연습문제 (참고문헌 [1]의 연습문제 2.5) 다섯개의 인자를 받아 그 합을 반환하는 함수를 작성하고, Check 명령어로 제대로된 형태로 작성했는지 확인한 다음, Eval 명령어로 샘플 값들을 주어 계산해보시오. 연습문제에 대한 답은 모두 이 글의 마지막에 제공한다.
===
번역
Expressions : 식
Formulas : 식
infix : 인픽스
Logical Formulas : 논리식
Symbolic Computation : 기호 계산
Terms : 텀
Well-formed : 제대로 된 형태