coq - 记录和定义

Question

我有一个问题： Record和Definition

我有这个定义：

Definition rule := term -> term.

我为它写了一个布尔函数。

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）我第一个定义的ruleusedDefinition和另一个 used有什么不同Record？

2）如果我想定义规则，Definition我可以在定义中给出别名lhs和rhs喜欢Record吗？

score 9 · Accepted Answer

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

Definition rule := term -> term

将 rule 定义为Prop函数 type 的类型（或）别名term -> term。因此

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定义一个别名。f 说这是Definitions 的另一种方式是“引用透明”，您可以（直到变量重命名）总是用定义的右侧替换其名称的任何出现。

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

1 回答 1