Coq (Proof Assistant)를 공부하는 사이트입니다.
Last modified : 2024.05.02
(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) — and, conj, split, destruct H as [H1 H2]
(19m06s)
Logic.v (Part 2) — BHK interpretation of intuitionistic logic, proof term for ~ (P /\
~ P)(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 내용 | |