3

私は使っている：

$ coqtop -v
The Coq Proof Assistant, version 8.4pl5 (February 2015)
compiled on Feb 06 2015 17:44:41 with OCaml 4.02.1

次のCoInductiveタイプを定義しましたstream:

$ coqtop
Welcome to Coq 8.4pl5 (February 2015)

Coq < CoInductive stream (A : Type) : Type := 
Coq < | Cons : A -> stream A -> stream A.
stream is defined

Coq < Check stream.
stream
     : Type -> Type

Coq < Check Cons.
Cons
     : forall A : Type, A -> stream A -> stream A

次に、次のCoFixpoint定義を定義しようとしましたzeros。

Coq < CoFixpoint zeros : stream nat := Cons 0 zeros.

ただし、代わりに次のエラーが発生しました。

Toplevel input, characters 38-39:
> CoFixpoint zeros : stream nat := Cons 0 zeros.
>                                       ^
Error: In environment
zeros : stream nat
The term "0" has type "nat" while it is expected to have type 
"Type".

変数を明示的にインスタンス化する必要があることがわかりましたA：

Coq < CoFixpoint zeros : stream nat := Cons nat 0 zeros.
zeros is corecursively defined

ACoq が の型を単独で推測しないのはなぜですか? の型を推測するにはどうすればよいAですか?

4

1 に答える 1

4

ACoqに推論を依頼するには、暗黙的として宣言する必要があります。それにはいくつかの方法があります。

  1. 次の宣言をファイルに追加しますSet Implicit Arguments.。これにより、Coq は for などの引数の自動推論を有効にしA、Consを記述できるようにしますCons 0 zeros。

  2. Consファイルの残りの部分に影響を与えずに、に対してのみ暗黙の引数を有効にします。

    Arguments Cons {A} _ _.

    この宣言は暗黙的としてマークAし、他の 2 つの引数を明示的のままにします。

  3. Aの定義で暗黙的としてマークstream:

    CoInductive stream {A : Type} : Type := 
| Cons : A -> stream A -> stream A.

    ただし、個人的にはこれを行うことはお勧めしません。これは、A暗黙的streamとしてもマークされるためです。

暗黙の引数の詳細については、リファレンス マニュアルを参照してください。

于 2015-05-04T16:53:47.250 に答える