2

私はプログラマーですが、Coq の超初心者であり、チュートリアルを理解しようとしましたが、あまり成功していません。私の質問は非常に単純です: Coq で (自然数の) 順序付けられたペアをどのように定義しますか?

これが私の試みでした：

Variable node1 : nat.
Variable node2 : nat.
Inductive edge : type := node1 -> node2.

(「エッジ」は順序付きペアに使用している名前であることに注意してください。) 3 行目で構文エラーが発生し、「.」が必要であることを示唆しています。文のどこかに。

どうすればいいのかわからない。どんな助けでも素晴らしいでしょう！(また、「Coq チュートリアル」の Google 検索で簡単に見られるものよりも、非常に基本的な Coq の概念を教えるのに役立つチュートリアルはありますか?)

4

1 に答える 1

4

Coq定義を使用するだけで、これを簡単に実行できます。

Definition ordered_pair := (nat * nat) % type.

これordered_pairは のシノニムとして導入されます ( Coqが自然型ではなく型のスコープで解釈するには、 が必要(nat * nat) % typeであることに注意してください)。真の力は次の使用にあります。% type**

Inductive prod (A B:Type) : Type :=
  pair : A -> B -> prod A B.

( http://coq.inria.fr/stdlib/Coq.Init.Datatypes.htmlより)

そこから、必要なすべての排除原則などを取得します。

于 2013-10-02T22:23:37.963 に答える