Skip to content

courses-at-nju-by-hfwei/problem-solving-class-coq

Folders and files

NameName
Last commit message
Last commit date

Latest commit

 

History

46 Commits
 
 
 
 
 
 
 
 
 
 
 
 

Repository files navigation

problem-solving-class-coq

Rock on Coq for the Problem Solving Class at Nanjing University

内容

Coq 是什么?

Coq 是辅助定理证明器。

借助 Coq, 你可以开发机器可检验的证明,大大提高证明的可靠性。

(要不是发现了一个反例,再给我三天的时间,我就能"证明"那个猜想中的定理了。)

为什么要引入 Coq?

  • 作为 Open Topics 素材
  • 配合课程内容,加深理解
  • 培养学生做严格证明的意识、习惯与能力
  • 介绍形式化方法,阅读并撰写课程/学术论文

如何使用 Coq?

如何学习 Coq?

以本仓库里的教程为主。

  • 关注 2019-1-coq 中的"通知"。
  • 学习相关 .v 文件并尽可能完成里面的练习
  • .v 文件相应的 .html 文件可以在本地浏览器中打开 (目前部分显示格式有误)

Coq 官方文档:

如何学好 Coq?

  • 练习,练习,再练习
  • 由于章节之间有依赖性,所以如果想做与 Coq 相关的 OT 报告,练习不能中断。

如何使用本仓库?

  • Clone 或者下载本仓库 (注意保持同步更新)
  • 在本地完成练习
  • 请不要公开发布练习答案。如果想放在个人 GitHub 仓库里,请设置为私有。
  • 有问题请在 ProblemOverflow 与QQ群讨论

如何向本仓库提交贡献?

  • 解决 Issues 中提到的问题
  • 贡献练习题
  • 配合教学内容,贡献相关 Coq 形式化框架与证明
  • 反馈意见与建议、交流学习经验等