junghanacs🧠

Backlinks

#콕 #이맥스 #에디터 연동

ᨒ Sourceᨒ Blameᨒ History ↗

Created: Modified: 9 min read

이 노트에 대하여

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

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

[강의 동영상 #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.)에 대해서 다룬다.

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

[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}

자연수 집합은 보통 으로 표기됩니다.

\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 -> 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

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.

Comments

Backlinks