Запись и определение - PullRequest
Новая
       6

Запись и определение

2 голосов
/ 06 марта 2012

У меня есть вопрос о: 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).

Myвопрос в том, что:

1) В чем разница между моим первым определенным rule использованным Definition и другим использованным Record?

2) Если я хочу определить правило с помощью Definition могу ли я дать псевдоним lhs и rhs лайков в Record определении?

1 Ответ

9 голосов
/ 06 марта 2012

Ваши два определения 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), перечисляя набор конструкторов. В более логичном мышлении Inductive определяет логическое суждение в терминах правил исключения / введения таким образом, чтобы обеспечить «гармонию».

...