• 使用课程主页提供的英文教材最新版本；
  • 平时作业独立完成，和其他同学讨论的部分需在提交时说明；
  • 当周作业需于下周四上课前提交至教学网（如果 slides 之中有特殊标注，以 slides 为准）；
  • 作业提交要求：只需提交当次作业涉及到的 Rocq 源文件（.v），无需压缩，且不要修改文件名。
  • 2026/03/05
    课程介绍
    [不需要提交]
  • 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.v 中 standard 非 optional 截止到 Case Study（不含）之前且不包括如下题目的 8 道习题。
    • le_facts, plus_le_facts1, plus_le_facts2
  • 2026/04/16
    IndPrinciples: Induction Principles 等
    [2026/04/23 13:00 截止]
    • 完成 IndPrinciples.v 中 standard 非 optional 的 3 道习题。
    • 完成 Maps.v 中 standard 非 optional 的 2 道习题。
  • 2026/04/21
    Imp: Simple Imperative Programs 等
    [2026/04/30 13:00 截止]
    • 完成 Imp.v 中 standard 非 optional 并不属于 Additional Exercises 的 6 道习题。
    • 从本章起证明长度有显著增加，请尽早动手。
  • 2026/04/23
    EQUIV: Program Equivalence
    [2026/05/07 13:00 截止]
    • 完成 Equiv.v 中 standard 非 optional 并不属于 Extended/Additional Exercises 的 8 道习题。
    • （可选）推荐也完成 Nondeterministic Imp 部分的两道习题。
  • 2026/04/30
    EQUIV: Program Equivalence 等
    [2026/05/07 13:00 截止]
    • 完成 Equiv.v 中 standard 非 optional 并不属于 Extended/Additional Exercises 的 8 道习题。
    • （可选）推荐也完成 Nondeterministic Imp 部分的两道习题。
    • 祝大家五一快乐！