junghanacs🧠

Backlinks

@정주희 #증명보조기 COQ 강의

ᨒ Sourceᨒ Blameᨒ History ↗

Created: Modified: 7 min read

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

coq 관련 노트

키워드 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 by Compute, 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=,  intros for forall n,  rewrite,  intros for implication

강의동영상 #7 (27m53s)  Basics.v (Part 5/5) --- destruct for nat/bool,

intro pattern and eqn: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 for incr, 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 of  match term_expr where term_expr is 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, Search for 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) --- apply for 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) --- specialize hypotheses and theorems,  generalize dependent for induction variables
  9. [강의 동영상 #23] (29m36s)  Tactics.v (Part 4/4) --- destruct on 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 the Inductive  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 and destruct (classic P),  Falsehood and Negation,  exfalso
  7. [강의 동영상 #30] (24m00s)  Logic.v (Part 7) --- True, apply I, iff, <−> ,  Logical equivalence and setoids, Existential Quantifier, exists tactic, 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 Types by Adam Chlipala (at MIT)

  2. learn-tt by Daniel Gratzer (at Aarhus University), author of Principles 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) by Michael 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.

BIBLIOGRAPHY

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

Comments

Graph View

Backlinks