coq - 记录和定义

Question

我有一个问题:Record和 Definition

我有这样的定义:

Definition rule := term -> term.

然后我为它写了一个 bool 函数。

Definition beq_rule a b := beq_term a && beq_term b.

哪里beq_term : term -> term -> bool.

所以我对 beq_rule 的定义实际上返回 beq_term 的类型这不是我想要的。我希望它为我返回一个类型:rule -> rule -> bool.

所以我通过 Record 更改了规则的定义:

Record rule := mkRule {lhs : term; rhs : term}.

和

Definition beq_rule (a b : rule) : bool :=
 beq_term (lhs a) (lhs b) && beq_term (rhs a) (rhs b).

我的问题是:

1) 我的第一个定义 rule 有什么不同？二手 Definition另一个用过Record ？

2) 如果我想通过 Definition 定义规则我可以给个别名吗 lhs和 rhs喜欢 Record定义？

Answer 1

rule 的两个定义说的是完全不同的事情

Definition rule := term -> term

将规则定义为函数类型 term -> term 的类型(或 Prop)别名。因此

Definition not_what_you_meant : rule := fun t => t.

将愉快地编译。

关于Record和Definition的关系。 Record 只是一个转换为 Inductive 的宏。所以

Record rule := mkRule {lhs : term; rhs : term}.

与

相同

Inductive rule := mkRule : term -> term -> rule.

加上访问函数

Definition lhs (r : rule) : term := 
 match r with
  mkRule l _ => l
 end.

etc.

您应该认为 Inductive 与 Definition 有根本的不同。 Definition 定义一个别名。另一种说法是 Definition 是“引用透明的”，您可以(直到变量重命名)始终用定义的右侧替换其名称的任何出现。

另一方面，

Inductive 通过列出一组构造函数来定义类型(Coqs 域的元素)。在更合乎逻辑的思维方式中，Inductive 以确保“和谐”的方式根据其消除/引入规则定义逻辑命题。