Coq初学者在这里，如何理解语法？

Posted 2023-05-08

【中文标题】Coq初学者在这里，如何理解语法？

【英文标题】：Coq begginer here, how to understand the syntax?

【发布时间】：2021-06-19 06:55:31

【问题描述】：

我最近在我的大学开设了一门课，我们用 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。 orb true false 也是如此。

现在，这段代码

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.

是我的教授写的证明这两个功能相等的证明。 我的问题是：intros、destruct、simpl、reflexivity 有什么作用？ 在 Coq 中做证明时你应该记住的一般概念是什么？ 另外，我在哪里可以找到一些有用、易于理解的 Coq 教程或文献？

【参考方案1】：

这个问题有点开放式；这就像在用某种编程语言编程时问你应该记住什么！互联网上有大量关于如何使用 Coq 的资料，其中解释了 intros、destruct 等策略的作用。我特别推荐软件基础系列，可在here 获得。它很长，但“逻辑基础”卷的前几章应该已经让您对正在发生的事情有一个基本的了解。