Почему я не могу определить следующую CoFixpoint?

Question

Я использую:

$ 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

Почему Coq не выводит тип A само собой? Как мне сделать вывод типа A?

Answer 1

Вы должны объявить A как неявно попросить Coq сделать вывод для вас. Есть несколько способов сделать это:

1. Добавьте следующую декларацию в ваш файл: Set Implicit Arguments., Это заставит Coq включить автоматический вывод для таких аргументов, как A за Cons, позволяя вам написать Cons 0 zeros,

2. Включить неявные аргументы только для Cons, не затрагивая остальную часть файла:

   Arguments Cons {A} _ _.
   

   Эта декларация знаменует A как неявный и оставляет два других аргумента как явные.

3. отметка A как подразумевается в определении stream:

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

   Я лично не рекомендую делать это, однако, как это будет отмечать A как подразумевается для stream также.

Вы можете найти больше информации о неявных аргументах в справочном руководстве.