记录和定义

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）我的第一个定义的rule使用的Definition与另一个使用的Record有什么不同？

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

Answer 1

你两个rule定义是说完全不同的东西

Definition rule := term -> term 

是定义规则的类型（或Prop）函数类型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定义了别名。另一种说法是Definition s是“引用透明的”，你可以（直到变量重命名）始终用定义的右边替换它的名字。

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