Coq (Proof Assistant)를 공부하는 사이트입니다.
Last modified : 2024.08.05
(20m58s) Coq 소개, 윈도즈 PC에 설치, CoqIDE 둘러보기 (20m30s) Coq-Shell 둘러보기, lf.tgz 설치·사용, Inductive, Check, Fail, Type, Set, Prop (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 (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 (31m53s) Basics.v (Part 3/5) — Admitted, Abort, 상수형/함수형 생성자, nat, Fixpoint, even, odd, plus(26m58s) Basics.v (Part 4/5) — unfold, mult, minus, Locate, div, modulo, intros for forall n, rewrite, intros for implication(27m53s) Basics.v (Part 5/5) — destruct for nat/bool, intro pattern and eqn:E, subgoals and bullets(22m32s) Induction.v (Part 1/3) — induction, induction hypothesis, assert (..) as H, replace (..) with (..), redex(outmost-leftmost), rewrite myLemma with (..), 덧셈의 교환법칙과 결합법칙(22m36s) Induction.v (Part 2/3) — repeat, exact, apply, 곱셈의 교환법칙과 결합법칙, 2진법 자연수 타입 bin, commutative diagram for incr, bin_to_nat, S (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 (23m07s) Lists.v (Part 1/4) — natprod, pair, fst, snd,
natlist, nil, cons, repeat, length, app, hd, tl(19m31s) Lists.v (Part 2/4) — alternate, bag, member, remove_one, remove_all, included(25m21s) Lists.v (Part 3/4) — app_assoc, Search for Theorems, app_nil_r, Set Printing Parentheses, involution_injective(23m30s) Lists.v (Part 4/4) — Options, Partial Maps(23m20s) Poly.v (Part 1/5) — Polymorphism, list: Type -> Type, mumble, grumble(18m09s) Poly.v (Part 2/5) — Type Annotation Inference,
Type Argument Synthesis (use [_]),
Implicit Arguments (2 methods: (1) use [Arguments], (2) use {..})(22m15s) Poly.v (Part 3/5) — Polymorphic Pairs, combine, split,
Polymorphic Options, Higher-order Functions, doit3times, filter, Anonymous Functions, let .. in .., partition(25m03s) Poly.v (Part 4/5) — map, map_rev, map_dist, flat_map, fold, fold app, const_fun, fold_length(27m02s) Poly.v (Part 5/5) — fold_map, nth_error_informal, Church Numerals, scc, cplus, cmult, cexp(23m42s) Tactics.v (Part 1/4) — apply for conditionals and universal conditionals, alpha equivalence, transitivity, injection, discriminate(20m32s) Tactics.v (Part 2/4) — admit vs Admitted, inversion, argument and target of tactics, Using Tactics on Hypotheses(20m19s) Tactics.v (Part 3/4) — specialize hypotheses and theorems, generalize dependent for induction variables(29m36s) Tactics.v (Part 4/4) — destruct on compound expressions, left/right inverse of a function, combine_split, split_combine, forallb, existsb(25m25s) Logic.v (Part 1/11) — and, conj, split, destruct H as [H1 H2](19m06s) Logic.v (Part 2/11) — BHK interpretation of intuitionistic logic, proof term for ~ (P /\
~ P)(21m52s) Logic.v (Part 3/11) — Proof terms, representation of empty functions, eq_refl, arguments before/after colon in the Inductive definition of types and constructors (20m51s) Logic.v (Part 4/11) — Conjunction의 inductive 정의와 tactic과의 관계, Proposition의 proof term을 (1) 직접 얻기와, (2) proof script를 먼저 얻은 후에 Show Proof 사용하기. (19m17s) Logic.v (Part 5/11) — eq, eq_refl의 alternative definitions, and, conj의 alternative definitions, implicit argument를 위한 중괄호와 대괄호, forward and backward inference, or_introl, or_intror (25m07s) Logic.v (Part 6/11) — or_introl, or_intror, functional extensionality, or elimination rule, classical logic and destruct (classic P), Falsehood and Negation, exfalso (24m00s) Logic.v (Part 7/11) — True, apply I, iff, <−> , Logical equivalence and setoids, Existential Quantifier, exists tactic, Rule C(22m06s) Logic.v (Part 8/11) — Exercises for [exists], Using Classical Logic, Definition of [ex] and [exists](25m42s) Logic.v (Part 9/11) — apply ex_intro, Programming with Propositions, Applying Theorems to Arguments(24m23s) Logic.v (Part 10/11) — Implicit type arguments in theorems, Working with decidable properties (bool and Prop)| 내용 | |