정주희 (2024) 콕 증명 도우미 스터디

• (정주희 n.d.) 수리논리전문가로서 coq를 다룬다. 지금 핫하게 작업 중이시라 실용적 측면에서 아주 좋다. 사실 이론은 이론대로 하지만 실제 구현물을 만들어 내야 의미가 있다.
• https://jhjeong.mindconnect.cc/CoqStudy/

coq 관련 노트

• 콕 증명 도우미 이맥스 환경의 시작
• 콕 설치 소개 이맥스 에디터 연동

히스토리

[2024-07-06]

목차 업데이트

Coq Study

[Home]

Coq(Proof Assistant)를 공부하는 사이트입니다.

Last modified : 2024.06.18

설치

• Windows PC에서는 CoqIDE를 사용합니다. 설치방법은 강의 동영상 #1에 나와 있습니다.
• macOS 시스템에서는 VS Code의 익스텐션인 VsCoq을 사용합니다. 설치방법은 강의노트에 나와 있습니다. (CoqIDE, Proof General 등 다른 작업환경도 물론 설치·사용이 가능합니다.)

강의노트

• coq_2024Mar26.pdf(302쪽, 1.4MB)
• 제10장 이후는 오타가 조금 많을 수 있습니다.
• 이 강의노트는 Software Foundations에 바탕을 두었습니다. SF가 제공하는 1~6권 중에 Volume 1 (Logical Foundations)과 Volume 2 (Programming Language Foundations)를 다룰 예정입니다.

강의 동영상

Installation, Basics

[강의 동영상 #1](20m58s) Coq 소개, 윈도즈 PC에 설치, CoqIDE 둘러보기

[강의 동영상 #2](20m30s) Coq-Shell 둘러보기

lf.tgz 설치·사용,Inductive, Check, Fail, Type, Set, Prop

[강의 동영상 #3](28m34s) Basics.v (Part 1/5) —=Module .. End,

Definition, match .. with .. end, Compute, Print, Example, Theorem, Lemma, Proof, Qed, simpl, reflexivity=, 과제 제출 및 채점 요령, Basics.v를 컴파일 하여 Basics.vo를 얻기,From LF Require Export Basics

[강의 동영상 #4](18m46s) Basics.v (Part 2/5) —=bool, true, false,

negb, andb, orb=, Currying (all Coq functions are unary), left/right-associativity, infix notation, precedence of operators, unit test byCompute,if .. then .. else

강의동영상 #5(31m53s) Basics.v (Part 3/5) —Admitted, Abort,

상수형/함수형 생성자,nat, Fixpoint, even, odd, plus

강의동영상 #6(26m58s) Basics.v (Part 4/5) —unfold,=mult, minus,

Locate, div, modulo=,introsforforall n,rewrite,introsfor implication

강의동영상 #7(27m53s) Basics.v (Part 5/5) —destructfornat/bool,

intro pattern andeqn:E, subgoals and bullets

Induction, Lists

1. [강의 동영상 #8](22m32s) Induction.v (Part 1/3) —induction, induction hypothesis,assert (..) as H, replace (..) with (..), redex(outmost-leftmost), rewrite myLemma with (..), 덧셈의 교환법칙과 결합법칙
2. [강의 동영상 #9](22m36s) Induction.v (Part 2/3) —repeat, exact, apply, 곱셈의 교환법칙과 결합법칙, 2진법 자연수 타입bin, commutative diagram forincr, bin_to_nat, S
3. [강의 동영상 #10](24m59s) Induction.v (Part 3/3) — Nat to Bin and Back to Nat,nat_bin_nat, Bin to Nat and Back to Bin (Advanced),bin_nat_bin, use ofmatch term_exprwhereterm_expris not a variable
4. [강의 동영상 #11](23m07s) Lists.v (Part 1/4) —natprod, pair, fst, snd, natlist, nil, cons, repeat, length, app, hd, tl
5. [강의 동영상 #12](19m31s) Lists.v (Part 2/4) —alternate, bag, member, remove_one, remove_all, included
6. [강의 동영상 #13](25m21s) Lists.v (Part 3/4) —app_assoc, Searchfor Theorems,app_nil_r, Set Printing Parentheses, involution_injective
7. [강의 동영상 #14](23m30s) Lists.v (Part 4/4) — Options, Partial Maps

Polymorphism, Tactics

1. [강의 동영상 #15](23m20s) Poly.v (Part 1/5) — Polymorphism,list: Type -> Type, mumble, grumble
2. [강의 동영상 #16](18m09s) Poly.v (Part 2/5) — Type Annotation Inference, Type Argument Synthesis (use [_]), Implicit Arguments (2 methods: (1) use [Arguments], (2) use {..})
3. [강의 동영상 #17](22m15s) Poly.v (Part 3/5) — Polymorphic Pairs,combine, split, Polymorphic Options, Higher-order Functions,doit3times, filter, Anonymous Functions,let .. in .., partition
4. [강의 동영상 #18](25m03s) Poly.v (Part 4/5) —map, map_rev, map_dist, flat_map, fold, fold app, const_fun, fold_length
5. [강의 동영상 #19](27m02s) Poly.v (Part 5/5) —fold_map, nth_error_informal, Church Numerals,scc, cplus, cmult, cexp
6. [강의 동영상 #20](23m42s) Tactics.v (Part 1/4) —applyfor conditionals and universal conditionals, alpha equivalence,transitivity, injection, discriminate
7. [강의 동영상 #21](20m32s) Tactics.v (Part 2/4) —admit vs Admitted, inversion, argument and target of tactics, Using Tactics on Hypotheses
8. [강의 동영상 #22](20m19s) Tactics.v (Part 3/4) —specializehypotheses and theorems,generalize dependentfor induction variables
9. [강의 동영상 #23](29m36s) Tactics.v (Part 4/4) —destructon compound expressions, left/right inverse of a function,combine_split, split_combine, forallb, existsb

Logic, Inductive Predicates

1. [강의 동영상 #24](25m25s) Logic.v (Part 1) —and, conj, split, destruct H as [H1 H2]
2. [강의 동영상 #25](19m06s) Logic.v (Part 2) — BHK interpretation of intuitionistic logic, proof term for ~ (P /~ P)
3. [강의 동영상 #26](21m52s) Logic.v (Part 3) — Proof terms, representation of empty functions,eq_refl, arguments before/after colon in theInductive definition of types and constructors
4. [강의 동영상 #27](20m51s) Logic.v (Part 4) — Conjunction의 inductive 정의와 tactic과의 관계, Proposition의 proof term을 (1) 직접 얻기와, (2) proof script를 먼저 얻은 후에Show Proof사용하기.
5. [강의 동영상 #28](19m17s) Logic.v (Part 5) —eq, eq_refl=의 alternative definitions,=and, conj=의 alternative definitions, implicit argument를 위한 중괄호와 대괄호, forward and backward inference,=or_introl, or_intror
6. [강의 동영상 #29](25m07s) Logic.v (Part 6) —or_introl, or_intror, functional extensionality, or elimination rule, classical logic anddestruct (classic P), Falsehood and Negation,exfalso
7. [강의 동영상 #30](24m00s) Logic.v (Part 7) —True, apply I, iff, <−>, Logical equivalence and setoids, Existential Quantifier,existstactic, Rule C
8. [강의 동영상 #31] 또는 [강의동영상 #31 new] (두 번째 링크는 첫 번째 동영상의 자막 스타일을 개선된 버전으로 바꾸고, 음성 녹음이 잘못된 부분 한 곳을 수정한 버전입니다.)(22m06s) Logic.v (Part 8) — Exercises for [exists], Using Classical Logic, Definition of [ex] and [exists]
9. [강의 동영상 #32](25m42s) Logic.v (Part 9) —apply ex_intro, Programming with Propositions, Applying Theorems to Arguments

외부 링크

1. Certified Programming with Dependent TypesbyAdam Chlipala(at MIT)

2. learn-ttbyDaniel Gratzer(at Aarhus University), author ofPrinciples of Dependent Type Theory

3. Oregon Programming Languages Summer School

4. DeepSpec Summer School — July 13−28, 2017

5. Software Foundations in Coq(YouTube Lecture) byMichael Ryan Clarkson(at Cornell University), one of the authors of SF, Volume 1 and 2

6. Formalising Mathematics(based on Lean)

7. Copyright ©2024,Joohee Jeong.

Related-Notes

References