作业
- 使用课程主页提供的英文教材最新版本
- 平时作业独立完成，和其他同学讨论的部分需在提交时说明
- 作业周四上课前提交(如果slides之中有特殊标注，以slides为准)，发送到助教的邮箱（willhuang@stu.pku.edu.cn），邮件标题请以“
学号-姓名”的格式书写 - 作业提交要求：只需提交
.v文件，并且请勿修改文件名
-
2025/02/20
课程介绍[不需要提交]
- 下载教科书及相关Coq代码 ：https://softwarefoundations.cis.upenn.edu
- 安装Coq系统和至少一个开发环境 ：https://coq.inria.fr/download
-
2025/02/25
Basics: Functional Programming in Coq[2025/03/06 13:00 截止]
- 完成Bascis.v中standard非optional的11道习题,More Exercise下的习题除外
-
2025/02/27
Induction: Proof by Induction 等[2025/03/10 13:00 截止]
- 完成Induction.v中standard非optional的6道习题
- 完成Lists.v中standard非optional的11道习题
-
2025/03/06
Poly: Polymorphism and Higher-Order Functions[2025/03/13 13:00 截止]
- 完成Poly.v中standard非optional且不属于Additional Exercises的7道习题
- （可选，不评分）如果之前没有接触过函数式语言，可以尝试Poly中Additional Exercises中的习题
-
2025/03/11
Tactics: More Tactics[2025/03/20 13:00 截止]
- 完成Tactics.v中standard非optional且不属于Additional Exercises的8道习题
-
2025/03/13
Logic: Logic in Coq[2025/03/27 13:00 截止]
- 完成Logic.v中standard非optional且不在下面列表中的17道习题
- tr_rev_correct、even_double_conv、eqb_list
-
2025/03/20
Logic: Logic in Coq 等[2025/03/27 13:00 截止]
- 完成Logic.v中standard非optional且不在下面列表中的17道习题
- tr_rev_correct、even_double_conv、eqb_list
-
2025/03/25
IndProp: Inductively Defined Propositions[2025/04/03 13:00 截止]
- 见03/27课程内容
-
2025/03/27
IndProp: Inductively Defined Propositions 等[2025/04/03 13:00 截止]
- 完成IndProp中standard非optional截止到case study（不含）之前且不包括如下题目的8道习题：le_facts, plus_le_facts1, plus_le_facts2
- 完成IndPrinciples中standard非optional的3道习题