Coinduction on Coq, type mismatch

Question

I've been trying out coinductive types and decided to define coinductive versions of the natural numbers and the vectors (lists with their size in the type). I defined them and the infinite number as so:

CoInductive conat : Set :=
| cozero : conat
| cosuc : conat -> conat.

CoInductive covec (A : Set) : conat -> Set :=
| conil : covec A cozero
| cocons : forall (n : conat), A -> covec A n -> covec A (cosuc n).           

CoFixpoint infnum : conat := cosuc infnum.

It all worked except for the definition I gave for an infinite covector

CoFixpoint ones : covec nat infnum := cocons 1 ones.

which gave the following type mismatch

Error:
In environment
ones : covec nat infnum
The term "cocons 1 ones" has type "covec nat (cosuc infnum)" while it is expected to have type
 "covec nat infnum".

I thought the compiler would accept this definition since, by definition, infnum = cosuc infnum. How can I make the compiler understand these expressions are the same?

Answer 1

The standard way to solve this issue is described in Adam Chlipala's CPDT (see the chapter on Coinduction).

Definition frob (c : conat) :=
  match c with
  | cozero => cozero
  | cosuc c' => cosuc c'
  end.

Lemma frob_eq (c : conat) : c = frob c.
Proof. now destruct c. Qed.

You can use the above definitions like so:

CoFixpoint ones : covec nat infnum.
Proof. rewrite frob_eq; exact (cocons 1 ones). Defined.

or, perhaps, in a bit more readable way:

Require Import Coq.Program.Tactics.

Program CoFixpoint ones : covec nat infnum := cocons 1 ones.
Next Obligation. now rewrite frob_eq. Qed.