在Coq的入门阶段，我主要是参阅的《Software fundations》这册书的第一卷。第一卷整体来说，对于初学者，做起来还是有些吃力的。完成进度如下：
- Basics (100%)
- Induction (90%)
- Lists (100%)
- Poly (100%)
- Tactics(100%)
- Logic(100%)
- IndProp(90%)
- Maps(100%)
- ProofObjects(100%)
- IndPrinciples(100%)
- Rel(100%)
- Imp (100%)
- ImpParser(Skip main part)
- ImpCEvalFun(100%)
- Extraction (100%)
- Auto(100%)