기본을 해보는 것. 기본은 배워야 한다. 여태 이렇다 생각 없이 그냥 해보는 것이다. 그래야 배운다. 이제 들어가 보자.
콕 증명 도우미 이맥스 환경의 시작 여기에서 일단 시작은 한 바 있다. 보다 디테일하게 나아가자.
[강의 동영상 #1](20m58s) Coq 소개, 윈도즈 PC에 설치, CoqIDE 둘러보기
근데 IDE를 설치해야 할까? 모르겠다. 다만 영상을 보면서 해보자.
5분 경에 바로 간단한 예시를 해본다. 이맥스로 해보려면 준비가 필요할 것 같은데?! 아. 일단 온라인 에디터로 예시를 작업해 본다.
N 을 어떻게 쓰는거지? nat 란 것은 알았다. 자연수라는 말이다. 정리 좀 해둬야지.
스니펫 좀 보자. 자연수를 어떻게 입력하는가? 위와 관계 없이 바로 물어보자.
오케이. 알았다. 이제 다음으로 진행하자. 물어보면 된다.
좋아. 간단한 예제이다. 근데 자동완성은?! 되게 해야 한다. coq-company를 활용하여 추가하였다. 완벽하게 커버된다.
Theorem mytheorem : forall n : nat, n = n.
Proof.
intros.
reflexivity.
Qed.코그 IDE를 다루는 이야기를 한다. 좋아. 설치와 기본 사용을 다루었다.
소프트웨어파운데이션 (정주희 n.d.)에 대해서 다룬다.
-
"ProofGeneral/PG: This repo is the new home of Proof General" (“ProofGeneral/PG: This Repo Is the New Home of Proof General” n.d.) 이 녀석한테 가보자. 여기에서 찾아야 겠다. 메뉴얼을 보려면 인포로 가자.
-
스니펫 입력 관련 : vscoq 패키지가 굉장히 유용하더라. LSP는 사용하지 않는다.
-
coq-lookup.el 을 위한 Coq PDF 메뉴얼을 다운 받자 https://github.com/coq/coq/releases?page=2
#chatgpt 스니펫 좀 보자. 자연수를 어떻게 입력하는가? 위와 관계 없이 바로 물어보자.
[SYS]: You are a helpful assistant. Please write in Korean language.
[ME]: 자연수 심볼을 어떻게 latex 심볼로 입력하는거야?
[AI]: 자연수(Natural Numbers)의 심볼은 보통 'ℕ'으로 나타냅니다. LaTeX에서 자연수를 나타내려면 다음과 같이 입력하면 됩니다:
```latex \documentclass{article} \usepackage{amsmath} \usepackage{amssymb}
\begin{document}
자연수 집합은 보통 으로 표기됩니다.
\end{document}
```
위 코드에서 `\mathbb{N}`이 자연수 심볼을 나타냅니다. 이 코드를 사용하기 위해서는 `amsmath`와 `amssymb` 패키지를 포함시켜야 합니다.
[ME]: coq 에서는 자연수를 어떻게 입력하는거야?
[AI]: Coq에서는 자연수를 나타내는 데 `nat` 타입을 사용합니다. Coq 표준 라이브러리는 이미 자연수와 관련된 많은 정의와 함수들을 포함하고 있습니다. 예를 들어, 자연수를 정의하고 사용하려면 다음과 같이 할 수 있습니다:
```coq Require Import Arith.
(* 자연수 n 을 정의합니다. *) Definition n : nat := 5.
(* 두 자연수의 합을 계산하는 예제 *) Definition add_example : nat := 3 + 4.
(* 자연수의 간단한 증명을 예제 *) Theorem add_comm : forall n m : nat, n + m = m + n. Proof. intros n m. apply Nat.add_comm. Qed. ```
이 예제에서:
- `Require Import Arith.` 구문을 사용하여 수학적 도구들을 가져옵니다.
- `Definition n : nat := 5.`는 `n`이라는 자연수를 정의합니다.
- `Definition add_example : nat := 3 + 4.`는 두 자연수의 합을 계산하여 `add_example`에 저장합니다.
- `Theorem add_comm`은 덧셈의 교환 법칙을 증명하는 예제입니다.
Coq에서는 `nat` 타입을 사용하여 자연수를 다루고, 다양한 연산자나 함수들을 쓸 수 있습니다.
[ME]: nat 이외에 coq에서 주로 사용하는 것들을 알려줄래?
[AI]: Coq은 강력한 정리 증명 도구로 다양한 데이터 타입과 구조를 광범위하게 사용합니다. `nat` 외에도 Coq에서 주로 사용되는 몇 가지 중요한 데이터 타입과 구조는 다음과 같습니다:
-
Bool (참/거짓):
- Coq에서 논리적 참(`true`)과 거짓(`false`)을 나타내는 타입입니다.
- `andb`, `orb`, `negb`와 같은 기본 논리 연산이 포함됩니다. ```coq Definition b : bool := true. ```
-
List (리스트):
-
동일한 타입의 요소들의 유한한 시퀀스를 나타냅니다.
-
`cons` (리스트의 머리에 요소를 추가), `nil` (빈 리스트) 등의 연산이 포함됩니다. ```coq Require Import List. Import ListNotations.
Definition l : list nat := [1; 2; 3]. ```
-
-
Option (옵션 타입):
- 값이 있을 수도 있고 없을 수도 있는 타입입니다.
- `Some` (값이 있는 경우)과 `None` (값이 없는 경우)으로 구성됩니다. ```coq Definition maybe_number : option nat := Some 42. ```
-
Sum (합 타입 / 공집합):
- 두 타입의 합집합을 나타내며, `inl` (왼쪽 값)과 `inr` (오른쪽 값)으로 구성됩니다. ```coq Definition example_sum : sum nat bool := inl 5. ```
-
Product (곱 타입 / 튜플):
- 두 타입의 카르테시안 곱을 나타내며, 보통 `(x, y)` 형식을 사용합니다. ```coq Definition example_pair : nat * bool := (3, true). ```
-
Inductive Types (귀납적 타입):
-
사용자가 정의할 수 있는 새로운 데이터 타입으로 다양한 데이터 구조를 생성하는 데 사용됩니다.
-
예를 들어, Coq 표준 라이브러리의 `nat` 타입은 귀납적으로 정의됩니다. ```coq Inductive nat : Type :=
| O : nat | |--------------------| | S : nat -> nat. |
```
-
-
Prop (명제):
- 논리적 명제를 나타내는 타입입니다. 증명과 논리에 관련된 연산을 수행할 때 사용됩니다. ```coq Definition example_proposition : Prop := 2 + 2 = 4. ```
-
Function (함수):
- 함수 정의와 응용은 Coq의 핵심 특징 중 하나입니다. ```coq Definition add (x y : nat) : nat := x + y. ```
-
Vectors (벡터):
-
고정된 길이를 가진 리스트로, 종종 길이가 타입의 일부로 포함된 리스트로 쓰입니다. ```coq Require Import Coq.Vectors.Vector. Import VectorNotations.
Definition v : Vector.t nat 3 := [1; 2; 3]. ```
-
이 외에도 Coq은 다양한 탑재된 라이브러리와 사용자 정의 타입을 통해 매우 다양한 범위의 수학적, 논리적 문제를 다룰 수 있습니다.
[ME]:
Related-Notes
References
정주희. n.d. “Software Foundations.” Accessed July 5, 2024. https://softwarefoundations.cis.upenn.edu/.
“ProofGeneral/PG: This Repo Is the New Home of Proof General.” n.d. Accessed July 5, 2024. https://github.com/ProofGeneral/PG.