🧠Junghanacs

Recent Notes

정주희: #콕 #증명보조기

Jul 05, 20247 min read

  • (정주희 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

정주희. n.d. “Coq 스터디 가이드 문서.” Accessed July 5, 2024. https://jhjeong.mindconnect.cc/CoqStudy/.

Backlinks