---
title: "#콕 #이맥스 #에디터 연동"
url: "https://notes.junghanacs.com/notes/20240708T053516"
author: "Junghan Kim"
date: "2024-07-08T05:35:00+09:00"
lastmod: "2024-12-01T06:30:00+09:00"
tags: ["coq","emacs","install"]
description: "강의 예제를 따라가며 Coq를 이맥스 에디터와 연동하고 자동완성까지 확인한 학습 기록."
---

> [!abstract] 이 노트에 대하여
> 
> 강의 영상을 따라가며 Coq를 Emacs에서 어떻게 다룰지 실습한 기록이다. 온라인 에디터와 이맥스 연동, 수식 입력, 자동완성 같은 실제 사용 감각이 단계적으로 이어진다.

-   [정주희 (2024) #콕 #증명보조기](https://notes.junghanacs.com/notes/20240705T220648)의 시작

기본을 해보는 것. 기본은 배워야 한다. 여태 이렇다 생각 없이 그냥 해보는 것이다. 그래야 배운다. 이제 들어가 보자.

-   [콕 증명 도우미 이맥스 환경의 시작](https://notes.junghanacs.com/notes/20240705T221508) 여기에서 일단 시작은 한 바 있다. 보다 디테일하게 나아가자.

## [[강의 동영상 #1](https://youtu.be/zPsYXjJv5Ew)] `(20m58s)`  Coq 소개, 윈도즈 PC에 설치, CoqIDE 둘러보기

근데 IDE를 설치해야 할까? 모르겠다. 다만 영상을 보면서 해보자.

5분 경에 바로 간단한 예시를 해본다. 이맥스로 해보려면 준비가 필요할 것 같은데?! 아. 일단 온라인 에디터로 예시를 작업해 본다.

N 을 어떻게 쓰는거지? nat 란 것은 알았다. 자연수라는 말이다. 정리 좀 해둬야지.

-   [이맥스: 레이텍: 수식: 입력: 스니펫: 활용법](https://notes.junghanacs.com/notes/20240315T075956)
-   [조직모드: 논리 기호 심볼 활용](https://notes.junghanacs.com/notes/20240614T142704)

스니펫 좀 보자. 자연수를 어떻게 입력하는가? 위와 관계 없이 바로 물어보자.

오케이. 알았다. 이제 다음으로 진행하자. 물어보면 된다.

좋아. 간단한 예제이다. 근데 자동완성은?! 되게 해야 한다. coq-company를 활용하여 추가하였다. 완벽하게 커버된다.

```coq

Theorem mytheorem : forall n : nat, n = n.
Proof.
  intros.
  reflexivity.
Qed.
```

코그 IDE를 다루는 이야기를 한다. 좋아. 설치와 기본 사용을 다루었다.

소프트웨어파운데이션 ([정주희 n.d.](https://notes.junghanacs.com/notes/20240708T053516#citeproc_bib_item_1))에 대해서 다룬다.

-   "ProofGeneral/PG: This repo is the new home of Proof General" ([“Proofgeneral/Pg: This Repo Is the New Home of Proof General” n.d.](https://notes.junghanacs.com/notes/20240708T053516#citeproc_bib_item_2)) 이 녀석한테 가보자. 여기에서 찾아야 겠다. 메뉴얼을 보려면 인포로 가자.

-   스니펫 입력 관련 : vscoq 패키지가 굉장히 유용하더라. LSP는 사용하지 않는다.

-   coq-lookup.el 을 위한 Coq PDF 메뉴얼을 다운 받자 <https://github.com/coq/coq/releases?page=2>

## #chatgpt 스니펫 좀 보자. 자연수를 어떻게 입력하는가? 위와 관계 없이 바로 물어보자.

<div class="ai">

[SYS]: You are a helpful assistant. Please write in Korean language.

@user 자연수 심볼을 어떻게 latex 심볼로 입력하는거야?

@assistant 자연수(Natural Numbers)의 심볼은 보통 'ℕ'으로 나타냅니다. LaTeX에서 자연수를 나타내려면 다음과 같이 입력하면 됩니다:

\`\`\`latex \documentclass{article} \usepackage{amsmath} \usepackage{amssymb}

\begin{document}

자연수 집합은 보통 $\mathbb{N}$으로 표기됩니다.

\end{document}

\`\`\`

위 코드에서 \`\mathbb{N}\`이 자연수 심볼을 나타냅니다. 이 코드를 사용하기 위해서는 \`amsmath\`와 \`amssymb\` 패키지를 포함시켜야 합니다.

@user coq 에서는 자연수를 어떻게 입력하는거야?

@assistant 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\` 타입을 사용하여 자연수를 다루고, 다양한 연산자나 함수들을 쓸 수 있습니다.

@user nat 이외에 coq에서 주로 사용하는 것들을 알려줄래?

@assistant Coq은 강력한 정리 증명 도구로 다양한 데이터 타입과 구조를 광범위하게 사용합니다. \`nat\` 외에도 Coq에서 주로 사용되는 몇 가지 중요한 데이터 타입과 구조는 다음과 같습니다:

1.  **Bool (참/거짓)**:
    -   Coq에서 논리적 참(\`true\`)과 거짓(\`false\`)을 나타내는 타입입니다.
    -   \`andb\`, \`orb\`, \`negb\`와 같은 기본 논리 연산이 포함됩니다. \`\`\`coq Definition b : bool := true. \`\`\`

2.  **List (리스트)**:
    -   동일한 타입의 요소들의 유한한 시퀀스를 나타냅니다.
    -   \`cons\` (리스트의 머리에 요소를 추가), \`nil\` (빈 리스트) 등의 연산이 포함됩니다. \`\`\`coq Require Import List. Import ListNotations.
        
        Definition l : list nat := [1; 2; 3]. \`\`\`

3.  **Option (옵션 타입)**:
    -   값이 있을 수도 있고 없을 수도 있는 타입입니다.
    -   \`Some\` (값이 있는 경우)과 \`None\` (값이 없는 경우)으로 구성됩니다. \`\`\`coq Definition maybe_number : option nat := Some 42. \`\`\`

4.  **Sum (합 타입 / 공집합)**:
    -   두 타입의 합집합을 나타내며, \`inl\` (왼쪽 값)과 \`inr\` (오른쪽 값)으로 구성됩니다. \`\`\`coq Definition example_sum : sum nat bool := inl 5. \`\`\`

5.  **Product (곱 타입 / 튜플)**:
    -   두 타입의 카르테시안 곱을 나타내며, 보통 \`(x, y)\` 형식을 사용합니다. \`\`\`coq Definition example_pair : nat \* bool := (3, true). \`\`\`

6.  **Inductive Types (귀납적 타입)**:
    -   사용자가 정의할 수 있는 새로운 데이터 타입으로 다양한 데이터 구조를 생성하는 데 사용됩니다.
    -   예를 들어, Coq 표준 라이브러리의 \`nat\` 타입은 귀납적으로 정의됩니다. \`\`\`coq Inductive nat : Type :=
        
        | O : nat            |
        |--------------------|
        | S : nat -&gt; nat. |
        
        \`\`\`

7.  **Prop (명제)**:
    -   논리적 명제를 나타내는 타입입니다. 증명과 논리에 관련된 연산을 수행할 때 사용됩니다. \`\`\`coq Definition example_proposition : Prop := 2 + 2 = 4. \`\`\`

8.  **Function (함수)**:
    -   함수 정의와 응용은 Coq의 핵심 특징 중 하나입니다. \`\`\`coq Definition add (x y : nat) : nat := x + y. \`\`\`

9.  **Vectors (벡터)**:
    -   고정된 길이를 가진 리스트로, 종종 길이가 타입의 일부로 포함된 리스트로 쓰입니다. \`\`\`coq Require Import Coq.Vectors.Vector. Import VectorNotations.
        
        Definition v : Vector.t nat 3 := [1; 2; 3]. \`\`\`

이 외에도 Coq은 다양한 탑재된 라이브러리와 사용자 정의 타입을 통해 매우 다양한 범위의 수학적, 논리적 문제를 다룰 수 있습니다.

@user

</div>

## 관련노트

## BIBLIOGRAPHY

- 정주희. 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>.