作业
- 使用课程主页提供的英文教材最新版本；
- 平时作业独立完成，和其他同学讨论的部分需在提交时说明；
- 当周作业需于下周四上课前提交至教学网（如果 slides 之中有特殊标注，以 slides 为准）；
- 作业提交要求：只需提交当次作业涉及到的 Rocq 源文件（
.v），无需压缩，且不要修改文件名。
-
2026/03/05
课程介绍[不需要提交]
- 下载教科书及相关 Rocq 代码 ：https://softwarefoundations.cis.upenn.edu
- 安装 Rocq 系统和至少一个开发环境 ：https://rocq-prover.org/install
- 祝大家学习愉快！
-
2026/03/10
Basics: Functional Programming in Rocq[2026/03/19 13:00 截止]
- 完成 Bascis.v 中 standard 非 optional 的习题，More Exercise 下的 Course Late Policies 除外，共 11 道。
-
2026/03/12
Induction: Proof by Induction 等[2026/03/19 13:00 截止]
- 完成 Induction.v 中 standard 非 optional 的 6 道习题。
- 完成 Lists.v 中 standard 非 optional 的 10 道习题。
- 本周作业量较大，请尽早动手完成。
-
2026/03/19
Poly: Polymorphism and Higher-Order Functions[2026/03/26 13:00 截止]
- 完成 Poly.v 中 standard 非 optional 且不属于 Additional Exercises 的 7 道习题。
- （可选）如果之前没有接触过函数式语言，可以考虑做一下 Additional Exercises 中的习题，其中第二部分是关于丘奇数的习题。
-
2026/03/24
Tactics: More Tactics[2026/04/02 13:00 截止]
- 完成 Tactics.v 中 standard 非 optional 且不属于 Additional Exercises 的 9 道习题。
-
2026/03/26
Logic: Logic in Rocq[2026/04/09 13:00 截止]
- 完成 Logic.v 中 standard 非 optional 且不在下面列表中的 17 道习题。
- tr_rev_correct, even_double_conv, eqb_list
-
2026/04/02
Logic: Logic in Rocq[2026/04/09 13:00 截止]
- 完成 Logic.v 中 standard 非 optional 且不在下面列表中的 17 道习题。
- tr_rev_correct, even_double_conv, eqb_list
-
2026/04/07
ProofObjects: The Curry-Howard Correspondence[2026/04/16 13:00 截止]
- 完成 ProofObject.v 中 standard 非 optional 的 10 道习题。
-
2026/04/09
IndProp: Inductively Defined Propositions 等[2026/04/16 13:00 截止]
- 完成 IndProp 中 standard 非 optional 截止到 Case Study（不含）之前且不包括如下题目的 8 道习题。
- le_facts, plus_le_facts1, plus_le_facts2