用于教育的证明检查器 Deduce
Deduce 是一个为教育设计的自动化证明检查器，旨在帮助学生学习函数式程序正确性证明。它面向具备基本编程和逻辑知识的学生，提供入门指南、编程练习和证明教程。文章介绍了 Deduce 的使用方法，包括编写代码和证明程序，并提供了参考手册和速查表。此外，文章还展示了线性搜索算法的实现及其证明示例。
用于教育的证明检查器
用于向学生教授函数式程序正确性证明。
什么是 Deduce?
Deduce 是一个自动化的证明检查器，旨在用于教育，以帮助学生：
- 轻松入门程序正确性的证明。
- 加深他们对逻辑的理解。
- 提高他们编写数学证明的能力。
function search(List<Nat>, Nat) -> Nat {
search(empty, y) = 0
search(node(x, xs), y) =
if x = y then 0
else suc(search(xs, y))
}
theorem less_implies_not_equal:
all x:Nat, y:Nat.
if x < y then not (x = y)
proof
arbitrary x:Nat, y:Nat
assume: x < y
assume xy: x = y
have: y < y by rewrite xy in recall x < y
conclude false by apply less_irreflexive
to recall y < y
end
谁可以使用 Deduce?
目标受众是具有（大致）以下背景知识和技能的学生：
- 具备主流编程语言（如 Java、Python 或 C++）的基本编程技能。
- 接触过一些逻辑知识，例如在离散数学课程中所学到的。
开始使用
通过安装必要的先决条件和下载 Deduce 源代码开始使用。您还可以找到有关设置 Deduce 工作区的有用信息。
编写 Deduce 代码
通过一系列示例来熟悉 Deduce 函数式编程。 通过练习检查您的理解，以测试您对该语言的掌握程度。
证明你的程序
按照详细的教程学习如何有效地使用 Deduce 编写逻辑证明。 在这本全面的指南中，探索 Deduce 证明语言的所有功能。
需要帮助？
Deduce Reference 手册提供了 Deduce 中所有功能的字母列表。 Cheat Sheet 提供了一些关于证明策略的建议，以及在证明中接下来使用哪个 Deduce 关键字。
示例证明
为了让您了解在 Deduce 中编写程序和证明是什么样的，以下是 线性搜索算法的实现，以及一个证明，即项目 y 不在列表 xs 中出现在 search(xs, y) 返回的索引之前的任何位置。
function search(List<Nat>, Nat) -> Nat {
search(empty, y) = 0
search(node(x, xs), y) =
if x = y then 0
else suc(search(xs, y))
}
theorem search_take: all xs: List<Nat>. all y:Nat.
not (y ∈ set_of(take(search(xs, y), xs)))
proof
induction List<Nat>
case [] {
arbitrary y:Nat
suffices not (y ∈ ∅) by evaluate
empty_no_members<Nat>
}
case node(x, xs')
assume IH: all y:Nat. not (y ∈ set_of(take(search(xs', y), xs')))
{
arbitrary y:Nat
switch x = y for search {
case true {
suffices not (y ∈ ∅) by evaluate
empty_no_members<Nat>
}
case false assume xy_false: (x = y) = false {
suffices not (x = y or y ∈ set_of(take(search(xs', y), xs')))
by evaluate
assume prem: x = y or y ∈ set_of(take(search(xs', y), xs'))
cases prem
case: x = y {
conclude false by rewrite xy_false in (recall x = y)
}
case y_in_rest: y ∈ set_of(take(search(xs', y), xs')) {
conclude false by apply IH to y_in_rest
}
}
}
}
end
贡献者
这个开源软件是由以下人员的志愿工作带给你的。
- Matei Cloteaux
- Shulin Gonsalves
- Calvin Josenhans
- Jeremy Siek
Get Started Live Code Source Code VS-Code deduce-mode Emacs deduce-mode Reference Cheat sheet Programming in deduce Proofs in deduce Standard library Syntax/Grammar Statements Proofs Terms Types Deduce unicode