記録と定義

Question

は、私は疑問を持っています。 beq_term : term -> term -> bool.

のでbeq_ruleの私の定義は実際に私がここに欲しいものではありませんbeq_termの正確型を返す

Definition beq_rule a b := beq_term a && beq_term b. 

。

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). 

私の質問は、その次のとおりです：だから私は、ルールの定義を変更し

rule -> rule -> bool.Recordによって：私はそれが私のために型を返すたい

1）最初に定義したruleとDefinitionとを使用した場合とRecordを使用した場合の違いは何ですか？私はDefinitionてルールを定義する場合

2）私はRecord定義でlhsとrhs同類エイリアスを与えることができますか？ ruleの

Answer 1

あなたの二つの定義は、関数型term -> termの別名

Definition rule := term -> term 

がタイプ（またはProp）などのルールを定義して全く別の事を言っています。したがって

Definition not_what_you_meant : rule := fun t => t. 

はうれしくコンパイルされます。

RecordとDefinitionの関係については、 Recordは、Inductiveに変換する単なるマクロです。だから、

Record rule := mkRule {lhs : term; rhs : term}. 

はあなたがDefinitionとは根本的に異なるものとしてInductiveと考えるべきで

Inductive rule := mkRule : term -> term -> rule. 

プラスアクセサ関数

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

etc. 

と同じです。 Definitionは、エイリアスを定義します。これが別の方法fを言っているのはDefinitionです。これは "参考に透明"です。（名前を変えるまで名前の変更が可能です）名前の出現に対して常に定義の右側を置き換えることができます。

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