如何解决Coq初学者在这里,如何理解语法?
我最近在我的大学开设了一门课,我们用 Coq 解决逻辑问题。我在理解 Coq 中的编程原理、语法和遇到问题时大脑中的“构建”想法时遇到了问题。例如,
Definition orb_3 (x y : bool) : bool :=
match x,y with
| false,false => false
| _,_ => true
end.
这是定义析取的第一个函数,并且
Definition orb (x y : bool) : bool :=
match x with
| true => true
| false => y
end.
是定义析取的第二个函数。 它们应该给出相同的结果,例如 orb3 true false 应该给出结果为 true。球体真假也是如此。
现在,这个代码
Goal forall x y : bool,orb x y = orb_3 x y.
Proof.
intros x y. destruct x.
- destruct y.
-- simpl. reflexivity.
-- simpl. reflexivity.
- destruct y ; simpl ; reflexivity.
Qed.
是我的教授写的证明这两个函数相等的证明。 我的问题是:介绍、破坏、简化、反身有什么作用? 在 Coq 中做证明时你应该记住的一般想法是什么? 另外,在哪里可以找到一些有用且易于理解的 Coq 教程或文献?
解决方法
这个问题有点开放;这就像问你在用某种编程语言编程时应该注意什么!互联网上有大量关于如何使用 Coq 的材料,其中解释了 intros
、destruct
等策略的作用。我特别推荐软件基础系列,可用 here。它很长,但“逻辑基础”卷的前几章应该已经让您对正在发生的事情有一个基本的了解。
版权声明:本文内容由互联网用户自发贡献,该文观点与技术仅代表作者本人。本站仅提供信息存储空间服务,不拥有所有权,不承担相关法律责任。如发现本站有涉嫌侵权/违法违规的内容, 请发送邮件至 dio@foxmail.com 举报,一经查实,本站将立刻删除。