记录和定义

Quy*_*yen 2 coq

我有一个问题: RecordDefinition

我有这个定义:

Definition rule := term -> term.
Run Code Online (Sandbox Code Playgroud)

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

Definition beq_rule a b := beq_term a && beq_term b.
Run Code Online (Sandbox Code Playgroud)

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

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

所以我改变了规则的定义Record:

Record rule := mkRule {lhs : term; rhs : term}.
Run Code Online (Sandbox Code Playgroud)

Definition beq_rule (a b : rule) : bool :=
 beq_term (lhs a) (lhs b) && beq_term (rhs a) (rhs b).
Run Code Online (Sandbox Code Playgroud)

我的问题是:

1)我的第一次rule使用Definition和另一次使用之间有什么不同Record

2)如果我想定义规则,Definition我可以在定义中给出别名lhsrhs喜欢Record吗?

Phi*_* JF 9

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

Definition rule := term -> term
Run Code Online (Sandbox Code Playgroud)

将规则定义为Prop函数类型的类型(或)别名term -> term.于是

Definition not_what_you_meant : rule := fun t => t.
Run Code Online (Sandbox Code Playgroud)

很乐意编译.

至于Record和之间的关系Definition. Record只是一个转换成一个宏的宏Inductive.所以

Record rule := mkRule {lhs : term; rhs : term}.
Run Code Online (Sandbox Code Playgroud)

是相同的

Inductive rule := mkRule : term -> term -> rule.
Run Code Online (Sandbox Code Playgroud)

加上访问者功能

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

etc.
Run Code Online (Sandbox Code Playgroud)

你应该认为它与Inductive根本不同Definition. Definition定义别名.另一种说法Definition是"引用透明"的方式,你可以(最多可变重命名)总是用定义的右边替换其名称的任何出现.

Inductive另一方面,通过列出一组构造函数来定义类型(Coqs Universe的元素).以更合乎逻辑的思维Inductive方式,以确保"和谐"的方式根据其消除/引入规则定义逻辑命题.