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

Rock on Coq for the Problem Solving Class at Nanjing University

problem-solving-class-coq

Rock on Coq for the Problem Solving Class at Nanjing University

内容

• 2019-1-coq
• 2019-2-coq
• 2019-3-coq
• 2019-4-coq

Coq 是什么?

Coq 是辅助定理证明器。

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

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

为什么要引入 Coq?

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

如何使用 Coq?

• CoqIDE 安装指南:
  • coq-install-linux
  • coq-install-windows
• CoqIDE 使用指南:
  • 极简指南:
    • 使用 CoqIDE [File => Open] 打开 2019-1-coq 中的 Basics.v 文件
    • 尝试 [Navigation] 菜单里的命令，观察 CoqIDE 的变化
  • 正经指南:
    • coqide-config

如何学习 Coq?

以本仓库里的教程为主。

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

Coq 官方文档:

• The Coq Standard Library
• The Coq Reference Manual

如何学好 Coq?

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

如何使用本仓库?

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

如何向本仓库提交贡献?

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