The Coq mailing list

[Nicolas Oury <npo AT Cs.Nott.AC.UK>]

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.
Defined.

(* This seems not to be a problem, but we can deduce *)

Definition p : ones = cons ones := out_eq ones.

(* Now, if we want to see how this is proved: *)

Eval compute in p. (* returns refl_equal (cons (cofix ones : Stream :=  
cons ones)) *)

(* but if we feed back the normal form *)

Definition p2 : ones = cons ones :=
refl_equal (cons (cofix ones : Stream := cons ones)).

(* the type checker yells that ones and cons ones are not convertible *)

-------------------------------

It seems there is a well-typed term whose normal form is not well-typed.
That's probably not threatening for the safety of the system, because  
ones and cons ones are extensionaly equal.
But it's still a bit troubling that type preservation does not hold.

Am I missing something?
Is it a known problem with coinductive types?


All the best,

Nicolas.

This message has been checked for viruses but the contents of an attachment
may still contain software viruses, which could damage your computer system:
you are advised to perform your own checks. Email communications with the
University of Nottingham may be monitored as permitted by UK legislation.