2

以下について質問があります 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).

私の質問は次のとおりです。

rule1) 最初に定義したusedDefinitionと別の usedの違いは何Recordですか?

2) ルールを定義したい場合Definition、エイリアスlhsとrhs好きなものをRecord定義できますか?

4

1 に答える 1

9

あなたの2つの定義は、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を定義します。これが「参照透過的」であると言う別の方法では、(変数の名前変更まで) 常に定義の右側をその名前の出現に置き換えることができます。Definition

Inductive一方、一連のコンストラクターをリストすることにより、タイプ (Coqs ユニバースの要素) を定義します。より論理的な考え方でInductiveは、「調和」を保証する方法で、排除/導入規則の観点から論理命題を定義します。

于 2012-03-06T04:17:13.610 に答える