The Coq mailing list

[Conor McBride <conor AT strictlypositive.org>]

Hi folks

Nils Anders Danielsson just raised Nicolas's question
on the Agda list, so at risk of duplication, I'll
observe that...

On 6 Jun 2008, at 15:09, Nicolas Oury wrote:

> Greetings,
>
> I was playing with CoInductive types in Coq and found this problem:
> -----------------
>
> (*if you define the type of streams of units:*)
>
> CoInductive Stream : Set :=
>  | cons : Stream -> Stream.
>
> CoFixpoint ones : Stream := cons ones.
>
> (*and a function out such that out (cons xs) := cons xs *)
>
> Definition out (xs : Stream) : Stream :=
>  match xs with
>  | cons ys => cons ys
>  end.
>
> Require Import Logic.
>
> (*Then you can prove: forall xs, xs = out xs *)
>
> Lemma out_eq (xs : Stream) : xs = out xs .
>  intros xs.
>  case_eq xs.
>  intros s eq.
>  reflexivity.

...this should not work.

(out (cons xs)) should not compute to (cons xs)
except en passant, in an outer case analysis
demanding to strip the cons.

If you write

> Definition bout (xs : Stream) : bool :=
>  match xs with
>  | cons ys => true
>  end.

then we should have

  refl : bout (out (cons xs)) = bout (cons xs)

But without such a bout, not at all!

[..]

> Defined.
>
> (* This seems not to be a problem, but we can deduce *)
>
> Definition p : ones = cons ones

Canonicity tells us that p's type should not
be inhabited.

Rather worryingly, this does suggest that
the contexts in which coinductive computation
should happen are perhaps rather more subtly
distinguished than we might have hoped. Perhaps
they may even be type-directed.

Well done, Nicolas, for spotting this problem!

All the best

Conor